diff --git a/src/core/index.ml b/src/core/index.ml index bd6c844c8..9e8eaa4f7 100644 --- a/src/core/index.ml +++ b/src/core/index.ml @@ -1913,7 +1913,7 @@ module Make_indexer (Indexing_state : Index_state.INDEXING_STATE) = struct ; comp_context ; proof } = - with_parent_scope state (fun state -> + with_parent_frame state (fun state -> with_indexed_meta_context state meta_context (fun state meta_context' -> with_indexed_comp_context state comp_context @@ -1964,7 +1964,7 @@ module Make_indexer (Indexing_state : Index_state.INDEXING_STATE) = struct let index_harpoon_proof state proof = disallow_free_variables state (fun state -> let proof' = - with_scope state (fun state -> index_harpoon_proof state proof) + with_frame state (fun state -> index_harpoon_proof state proof) in Synapx.Comp.Proof proof') diff --git a/src/core/index_state.ml b/src/core/index_state.ml index a7802de3d..e53dab711 100644 --- a/src/core/index_state.ml +++ b/src/core/index_state.ml @@ -678,9 +678,9 @@ module type INDEXING_STATE = sig -> Identifier.t -> Unit.t - val with_scope : state -> (state -> 'a) -> 'a + val with_frame : state -> (state -> 'a) -> 'a - val with_parent_scope : state -> (state -> 'a) -> 'a + val with_parent_frame : state -> (state -> 'a) -> 'a val with_bindings_checkpoint : state -> (state -> 'a) -> 'a @@ -739,20 +739,20 @@ module Indexing_state = struct (** The length of [cG], the context of computation-level variables. *) } - type scope = - | Plain_scope of { bindings : bindings } - | Pattern_scope of + type frame = + | Plain_frame of { bindings : bindings } + | Pattern_frame of { pattern_bindings : bindings ; mutable pattern_variables_rev : Identifier.t List.t ; expression_bindings : bindings } - | Module_scope of + | Module_frame of { bindings : bindings ; declarations : entry_binding_tree } type state = - { mutable scopes : scope List1.t + { mutable frames : frame List1.t ; mutable free_variables_allowed : Bool.t ; mutable generated_fresh_variables_count : Int.t } @@ -770,20 +770,20 @@ module Indexing_state = struct ; comp_context_size = 0 } - let[@inline] create_empty_module_scope () = - Module_scope + let[@inline] create_empty_module_frame () = + Module_frame { bindings = create_empty_bindings () ; declarations = Binding_tree.create () } let[@inline] create_initial_state () = - { scopes = List1.singleton (create_empty_module_scope ()) + { frames = List1.singleton (create_empty_module_frame ()) ; free_variables_allowed = false ; generated_fresh_variables_count = 0 } let clear_state state = - state.scopes <- List1.singleton (create_empty_module_scope ()); + state.frames <- List1.singleton (create_empty_module_frame ()); state.free_variables_allowed <- false; state.generated_fresh_variables_count <- 0 @@ -812,79 +812,81 @@ module Indexing_state = struct | Option.Some identifier -> identifier | Option.None -> fresh_identifier state - let[@inline] get_scope_bindings_state = function - | Pattern_scope { pattern_bindings = bindings; _ } - | Module_scope { bindings; _ } - | Plain_scope { bindings } -> + let[@inline] get_frame_bindings_state = function + | Pattern_frame { pattern_bindings = bindings; _ } + | Module_frame { bindings; _ } + | Plain_frame { bindings } -> bindings - let[@inline] get_scope_bindings state = - (get_scope_bindings_state state).bindings + let[@inline] get_frame_bindings state = + (get_frame_bindings_state state).bindings - let[@inline] push_scope state scope = - state.scopes <- List1.cons scope state.scopes + let[@inline] push_frame state frame = + state.frames <- List1.cons frame state.frames - let pop_scope state = - match state.scopes with + let pop_frame state = + match state.frames with | List1.T (x1, x2 :: xs) -> - state.scopes <- List1.from x2 xs; + state.frames <- List1.from x2 xs; x1 | List1.T (_x, []) -> - (* This suggests a mismanaged scopes state, where there are more - [pop_scope] operations than there are [push_scope] operations. *) + (* This suggests a mismanaged frames state, where there are more + [pop_frame] operations than there are [push_frame] operations. *) Error.raise_violation - (Format.asprintf "[%s] cannot pop the last scope" __FUNCTION__) + (Format.asprintf "[%s] cannot pop the last frame" __FUNCTION__) - let[@inline] get_current_scope state = List1.head state.scopes + let[@inline] get_current_frame state = List1.head state.frames - let[@inline] get_current_scope_bindings_state state = - get_scope_bindings_state (get_current_scope state) + let[@inline] get_current_frame_bindings_state state = + get_frame_bindings_state (get_current_frame state) - let[@inline] get_current_scope_bindings state = - let current_scope_bindings_state = - get_current_scope_bindings_state state + let[@inline] get_current_frame_bindings state = + let current_frame_bindings_state = + get_current_frame_bindings_state state in - current_scope_bindings_state.bindings + current_frame_bindings_state.bindings - (** [push_new_plain_scope state] pushes a new empty plain scope to [state]. + (** [push_new_plain_frame state] pushes a new empty plain frame to [state]. The LF, meta and computation context sizes are carried over. *) - let push_new_plain_scope state = - let current_scope_bindings_state = - get_current_scope_bindings_state state + let push_new_plain_frame state = + let current_frame_bindings_state = + get_current_frame_bindings_state state in let bindings = - { current_scope_bindings_state (* Copy context sizes *) with - bindings = Binding_tree.create () + { bindings = Binding_tree.create () + ; lf_context_size = current_frame_bindings_state.lf_context_size + ; meta_context_size = current_frame_bindings_state.meta_context_size + ; comp_context_size = current_frame_bindings_state.comp_context_size } in - let scope = Plain_scope { bindings } in - push_scope state scope + let frame = Plain_frame { bindings } in + push_frame state frame let entry_is_not_variable entry = Bool.not (Entry.is_variable entry) - let lookup_toplevel_in_scope scope query = - Binding_tree.lookup_toplevel_opt query (get_scope_bindings scope) + let lookup_toplevel_in_frame frame query = + Binding_tree.lookup_toplevel_opt query (get_frame_bindings frame) - let lookup_toplevel_in_scopes scopes query = - List.find_map (fun scope -> lookup_toplevel_in_scope scope query) scopes + let lookup_toplevel_in_frames frames query = + List.find_map (fun frame -> lookup_toplevel_in_frame frame query) frames - let rec lookup_toplevel_declaration_in_scopes scopes query = - match scopes with - | [] -> (* Exhausted the list of scopes to check. *) Option.none - | scope :: scopes -> ( - let scope_bindings = get_scope_bindings scope in - match Binding_tree.lookup_toplevel_opt query scope_bindings with + let rec lookup_toplevel_declaration_in_frames frames query = + match frames with + | [] -> (* Exhausted the list of frames to check. *) Option.none + | frame :: frames -> ( + let frame_bindings = get_frame_bindings frame in + match Binding_tree.lookup_toplevel_opt query frame_bindings with | Option.Some (entry, subtree) when entry_is_not_variable entry -> - (* [query] is bound to a declaration in [scope]. *) + (* [query] is bound to a declaration in [frame]. *) Option.some (entry, subtree) | Option.Some _ -> - (* [query] is bound to a variable in [scope], so any declaration - in [scopes] bound to [query] is shadowed. *) + (* [query] is bound to a variable in [frame], so any declaration + in [frames] bound to [query] is shadowed. *) Option.none | Option.None -> - (* [query] is unbound in [scope], so check in the parent - scopes. *) - lookup_toplevel_declaration_in_scopes scopes query) + (* [query] is unbound in [frame], so check in the parent + frames. *) + lookup_toplevel_declaration_in_frames frames query) (** [lookup_toplevel_opt state query] is the entry and subtree bound to the identifier [query] in [state]. The "toplevel" here refers to [query] @@ -893,30 +895,30 @@ module Indexing_state = struct {!val:lookup}. The entry bound to [query] in [state] is the first entry found in a - scope in the stack of scopes in [state]. + frame in the stack of frames in [state]. - Exceptionally for pattern scopes, we ignore bound variables in outer - scopes. This means that in the computation-level Beluga expression + Exceptionally for pattern frames, we ignore bound variables in outer + frames. This means that in the computation-level Beluga expression [let x = ? in case ? of p => ?], the pattern [p] may not refer to [x]. The name [x] can be used in [p], but it is considered a free variable. *) let lookup_toplevel_opt state query = - match state.scopes with - | List1.T ((Pattern_scope _ as scope), scopes) -> ( - match lookup_toplevel_in_scope scope query with + match state.frames with + | List1.T ((Pattern_frame _ as frame), frames) -> ( + match lookup_toplevel_in_frame frame query with | Option.Some x -> Option.some x - | Option.None -> lookup_toplevel_declaration_in_scopes scopes query) - | List1.T (scope, scopes) -> - lookup_toplevel_in_scopes (scope :: scopes) query + | Option.None -> lookup_toplevel_declaration_in_frames frames query) + | List1.T (frame, frames) -> + lookup_toplevel_in_frames (frame :: frames) query - let rec lookup_in_scopes scopes identifiers = - match scopes with + let rec lookup_in_frames frames identifiers = + match frames with | [] -> Error.raise (Unbound_qualified_identifier (Qualified_identifier.from_list1 identifiers)) - | scope :: scopes -> ( + | frame :: frames -> ( match - Binding_tree.maximum_lookup identifiers (get_scope_bindings scope) + Binding_tree.maximum_lookup identifiers (get_frame_bindings frame) with | Binding_tree.Bound { entry; subtree; _ } -> (entry, subtree) | Binding_tree.Partially_bound { leading_segments; segment; _ } -> @@ -924,24 +926,24 @@ module Indexing_state = struct (Unbound_namespace (Qualified_identifier.make ~namespaces:leading_segments segment)) - | Binding_tree.Unbound _ -> lookup_in_scopes scopes identifiers) + | Binding_tree.Unbound _ -> lookup_in_frames frames identifiers) - let rec lookup_declaration_in_scopes scopes identifiers = - match scopes with + let rec lookup_declaration_in_frames frames identifiers = + match frames with | [] -> Error.raise (Unbound_qualified_identifier (Qualified_identifier.from_list1 identifiers)) - | scope :: scopes -> ( - let scope_bindings = get_scope_bindings scope in - match Binding_tree.maximum_lookup identifiers scope_bindings with + | frame :: frames -> ( + let frame_bindings = get_frame_bindings frame in + match Binding_tree.maximum_lookup identifiers frame_bindings with | Binding_tree.Bound { entry; subtree; _ } when entry_is_not_variable entry -> - (* [query] is bound to a declaration in [scope]. *) + (* [query] is bound to a declaration in [frame]. *) (entry, subtree) | Binding_tree.Bound _result -> - (* [query is bound to a variable in [scope], so any declaration - in [scopes] bound to [query] is shadowed. *) + (* [query is bound to a variable in [frame], so any declaration + in [frames] bound to [query] is shadowed. *) assert (List1.length identifiers = 1) (* Variables can't be in namespaces *); Error.raise @@ -953,23 +955,23 @@ module Indexing_state = struct (Qualified_identifier.make ~namespaces:leading_segments segment)) | Binding_tree.Unbound _ -> - lookup_declaration_in_scopes scopes identifiers) + lookup_declaration_in_frames frames identifiers) (** [lookup state query] is the entry and subtree bound to the qualified identifier [query] in [state]. To lookup simple identifiers, see {!val:lookup_toplevel}. The entry bound to [query] in [state] is the first entry found in a - scope in the stack of scopes in [state]. If a scope has [entry] as + frame in the stack of frames in [state]. If a frame has [entry] as partially bound (meaning that only the first few namespaces of [query] - are bound in that scope), then [query] is considered to be unbound + are bound in that frame), then [query] is considered to be unbound because one of its namespaces is unbound. *) let lookup state query = let identifiers = Qualified_identifier.to_list1 query in - match state.scopes with - | List1.T ((Pattern_scope _ as scope), scopes) -> ( + match state.frames with + | List1.T ((Pattern_frame _ as frame), frames) -> ( match - Binding_tree.maximum_lookup identifiers (get_scope_bindings scope) + Binding_tree.maximum_lookup identifiers (get_frame_bindings frame) with | Binding_tree.Bound { entry; subtree; _ } -> (entry, subtree) | Binding_tree.Partially_bound { leading_segments; segment; _ } -> @@ -978,15 +980,15 @@ module Indexing_state = struct (Qualified_identifier.make ~namespaces:leading_segments segment)) | Binding_tree.Unbound _ -> - lookup_declaration_in_scopes scopes identifiers) - | List1.T (scope, scopes) -> - lookup_in_scopes (scope :: scopes) identifiers + lookup_declaration_in_frames frames identifiers) + | List1.T (frame, frames) -> + lookup_in_frames (frame :: frames) identifiers let add_binding state identifier ?subtree entry = - match get_current_scope state with - | Plain_scope { bindings } - | Pattern_scope { pattern_bindings = bindings; _ } - | Module_scope { bindings; _ } -> + match get_current_frame state with + | Plain_frame { bindings } + | Pattern_frame { pattern_bindings = bindings; _ } + | Module_frame { bindings; _ } -> Binding_tree.add_toplevel identifier entry ?subtree bindings.bindings let[@inline] increment_lf_context_size bindings = @@ -1007,47 +1009,57 @@ module Indexing_state = struct let[@inline] decrement_comp_context_size bindings = bindings.comp_context_size <- bindings.comp_context_size - 1 + (** [remove_lf_binding state identifier] removes the latest binding of + [identifier] from [state]. It is assumed that this binding is that of + an LF variable, and that it was introduced in the current frame. *) let remove_lf_binding state identifier = - match get_current_scope state with - | Plain_scope { bindings } - | Pattern_scope { pattern_bindings = bindings; _ } - | Module_scope { bindings; _ } -> + match get_current_frame state with + | Plain_frame { bindings } + | Pattern_frame { pattern_bindings = bindings; _ } + | Module_frame { bindings; _ } -> Binding_tree.remove identifier bindings.bindings; decrement_lf_context_size bindings + (** [remove_meta_binding state identifier] removes the latest binding of + [identifier] from [state]. It is assumed that this binding is that of a + meta-level variable, and that it was introduced in the current frame. *) let remove_meta_binding state identifier = - match get_current_scope state with - | Plain_scope { bindings } - | Pattern_scope { pattern_bindings = bindings; _ } - | Module_scope { bindings; _ } -> + match get_current_frame state with + | Plain_frame { bindings } + | Pattern_frame { pattern_bindings = bindings; _ } + | Module_frame { bindings; _ } -> Binding_tree.remove identifier bindings.bindings; decrement_meta_context_size bindings + (** [remove_comp_binding state identifier] removes the latest binding of + [identifier] from [state]. It is assumed that this binding is that of a + computation-level variable, and that it was introduced in the current + frame. *) let remove_comp_binding state identifier = - match get_current_scope state with - | Plain_scope { bindings } - | Pattern_scope { pattern_bindings = bindings; _ } - | Module_scope { bindings; _ } -> + match get_current_frame state with + | Plain_frame { bindings } + | Pattern_frame { pattern_bindings = bindings; _ } + | Module_frame { bindings; _ } -> Binding_tree.remove identifier bindings.bindings; decrement_comp_context_size bindings let add_declaration state identifier ?subtree entry = - match get_current_scope state with - | Plain_scope _ -> + match get_current_frame state with + | Plain_frame _ -> Error.raise_violation (Format.asprintf - "[%s] invalid plain scope, expected a module scope" __FUNCTION__) - | Pattern_scope _ -> + "[%s] invalid plain frame, expected a module frame" __FUNCTION__) + | Pattern_frame _ -> Error.raise_violation (Format.asprintf - "[%s] invalid pattern scope, expected a module scope" + "[%s] invalid pattern frame, expected a module frame" __FUNCTION__) - | Module_scope { bindings; declarations } -> + | Module_frame { bindings; declarations } -> Binding_tree.add_toplevel identifier entry ?subtree bindings.bindings; Binding_tree.add_toplevel identifier entry ?subtree declarations let add_lf_level_variable state identifier make_entry = - let bindings = get_current_scope_bindings_state state in + let bindings = get_current_frame_bindings_state state in let entry = make_entry ~lf_level:(Option.some (Lf_level.of_int bindings.lf_context_size)) @@ -1056,7 +1068,7 @@ module Indexing_state = struct Binding_tree.add_toplevel identifier entry bindings.bindings let add_meta_level_variable state identifier make_entry = - let bindings = get_current_scope_bindings_state state in + let bindings = get_current_frame_bindings_state state in let entry = make_entry ~meta_level: @@ -1066,7 +1078,7 @@ module Indexing_state = struct Binding_tree.add_toplevel identifier entry bindings.bindings let add_comp_level_variable state identifier make_entry = - let bindings = get_current_scope_bindings_state state in + let bindings = get_current_frame_bindings_state state in let entry = make_entry ~comp_level: @@ -1104,27 +1116,27 @@ module Indexing_state = struct (Entry.make_computation_variable_entry ?location identifier) let shift_lf_context state = - let bindings_state = get_current_scope_bindings_state state in + let bindings_state = get_current_frame_bindings_state state in increment_lf_context_size bindings_state let unshift_lf_context state = - let bindings_state = get_current_scope_bindings_state state in + let bindings_state = get_current_frame_bindings_state state in decrement_lf_context_size bindings_state let shift_meta_context state = - let bindings_state = get_current_scope_bindings_state state in + let bindings_state = get_current_frame_bindings_state state in increment_meta_context_size bindings_state let unshift_meta_context state = - let bindings_state = get_current_scope_bindings_state state in + let bindings_state = get_current_frame_bindings_state state in decrement_meta_context_size bindings_state let shift_comp_context state = - let bindings_state = get_current_scope_bindings_state state in + let bindings_state = get_current_frame_bindings_state state in increment_comp_context_size bindings_state let unshift_comp_context state = - let bindings_state = get_current_scope_bindings_state state in + let bindings_state = get_current_frame_bindings_state state in decrement_comp_context_size bindings_state let actual_binding_exn = Entry.actual_binding_exn @@ -1293,22 +1305,22 @@ module Indexing_state = struct (actual_binding_exn qualified_identifier entry)) let[@inline] get_lf_context_size state = - let current_scope_bindings_state = - get_current_scope_bindings_state state + let current_frame_bindings_state = + get_current_frame_bindings_state state in - current_scope_bindings_state.lf_context_size + current_frame_bindings_state.lf_context_size let[@inline] get_meta_context_size state = - let current_scope_bindings_state = - get_current_scope_bindings_state state + let current_frame_bindings_state = + get_current_frame_bindings_state state in - current_scope_bindings_state.meta_context_size + current_frame_bindings_state.meta_context_size let[@inline] get_comp_context_size state = - let current_scope_bindings_state = - get_current_scope_bindings_state state + let current_frame_bindings_state = + get_current_frame_bindings_state state in - current_scope_bindings_state.comp_context_size + current_frame_bindings_state.comp_context_size let[@inline] index_of_lf_level state lf_level = let lf_context_size = get_lf_context_size state in @@ -1557,7 +1569,7 @@ module Indexing_state = struct let open_namespace state identifier = let _entry, subtree = lookup state identifier in - let bindings = get_current_scope_bindings state in + let bindings = get_current_frame_bindings state in Binding_tree.add_all bindings subtree let open_module state ?location identifier = @@ -1608,36 +1620,36 @@ module Indexing_state = struct let add_free_lf_level_variable _state _identifier _make_entry = () let add_free_meta_level_variable state identifier make_entry = - match get_current_scope state with - | Pattern_scope scope -> + match get_current_frame state with + | Pattern_frame frame -> let entry = make_entry ~meta_level:Option.none in - scope.pattern_variables_rev <- - identifier :: scope.pattern_variables_rev; + frame.pattern_variables_rev <- + identifier :: frame.pattern_variables_rev; Binding_tree.add_toplevel identifier entry - scope.pattern_bindings.bindings; + frame.pattern_bindings.bindings; Binding_tree.add_toplevel identifier entry - scope.expression_bindings.bindings - | Plain_scope _ - | Module_scope _ -> + frame.expression_bindings.bindings + | Plain_frame _ + | Module_frame _ -> () let add_free_comp_level_variable state identifier make_entry = - match get_current_scope state with - | Pattern_scope scope -> + match get_current_frame state with + | Pattern_frame frame -> let entry = make_entry ~comp_level: (Option.some (Comp_level.of_int - scope.expression_bindings.comp_context_size)) + frame.expression_bindings.comp_context_size)) in - scope.pattern_variables_rev <- - identifier :: scope.pattern_variables_rev; + frame.pattern_variables_rev <- + identifier :: frame.pattern_variables_rev; Binding_tree.add_toplevel identifier entry - scope.expression_bindings.bindings; - increment_comp_context_size scope.expression_bindings - | Plain_scope _ - | Module_scope _ -> + frame.expression_bindings.bindings; + increment_comp_context_size frame.expression_bindings + | Plain_frame _ + | Module_frame _ -> () let add_free_lf_variable state ?location identifier = @@ -1760,38 +1772,38 @@ module Indexing_state = struct let add_bound_pattern_meta_level_variable state ?location identifier make_entry = - match get_current_scope state with - | Pattern_scope scope -> + match get_current_frame state with + | Pattern_frame frame -> let pattern_entry = make_entry ?location identifier ~meta_level: (Option.some - (Meta_level.of_int scope.pattern_bindings.meta_context_size)) + (Meta_level.of_int frame.pattern_bindings.meta_context_size)) in let expression_entry = make_entry ?location identifier ~meta_level: (Option.some (Meta_level.of_int - scope.expression_bindings.meta_context_size)) + frame.expression_bindings.meta_context_size)) in Binding_tree.add_toplevel identifier pattern_entry - scope.pattern_bindings.bindings; - increment_meta_context_size scope.pattern_bindings; - scope.pattern_variables_rev <- - identifier :: scope.pattern_variables_rev; + frame.pattern_bindings.bindings; + increment_meta_context_size frame.pattern_bindings; + frame.pattern_variables_rev <- + identifier :: frame.pattern_variables_rev; Binding_tree.add_toplevel identifier expression_entry - scope.expression_bindings.bindings; - increment_meta_context_size scope.expression_bindings - | Plain_scope _ -> + frame.expression_bindings.bindings; + increment_meta_context_size frame.expression_bindings + | Plain_frame _ -> Error.raise_violation (Format.asprintf - "[%s] invalid plain scope, expected a pattern scope" + "[%s] invalid plain frame, expected a pattern frame" __FUNCTION__) - | Module_scope _ -> + | Module_frame _ -> Error.raise_violation (Format.asprintf - "[%s] invalid module scope, expected a pattern scope" + "[%s] invalid module frame, expected a pattern frame" __FUNCTION__) let add_bound_pattern_meta_variable state ?location identifier = @@ -1942,72 +1954,72 @@ module Indexing_state = struct add_declaration state identifier (Entry.make_program_constant_entry ?location identifier cid) - let push_new_module_scope state = - let current_scope_bindings_state = - get_current_scope_bindings_state state + let push_new_module_frame state = + let current_frame_bindings_state = + get_current_frame_bindings_state state in - let module_scope = - Module_scope + let module_frame = + Module_frame { bindings = - { current_scope_bindings_state with + { current_frame_bindings_state with bindings = Binding_tree.create () } ; declarations = Binding_tree.create () } in - push_scope state module_scope + push_frame state module_frame let add_module state ?location identifier cid m = - push_new_module_scope state; + push_new_module_frame state; let x = m state in - (match get_current_scope state with - | Plain_scope _ -> + (match get_current_frame state with + | Plain_frame _ -> Error.raise_violation (Format.asprintf - "[%s] invalid plain scope, expected a module scope" __FUNCTION__) - | Pattern_scope _ -> + "[%s] invalid plain frame, expected a module frame" __FUNCTION__) + | Pattern_frame _ -> Error.raise_violation (Format.asprintf - "[%s] invalid pattern scope, expected a module scope" + "[%s] invalid pattern frame, expected a module frame" __FUNCTION__) - | Module_scope { declarations; _ } -> - ignore (pop_scope state); + | Module_frame { declarations; _ } -> + ignore (pop_frame state); add_declaration state ~subtree:declarations identifier (Entry.make_module_entry ?location identifier cid)); x - let with_scope state m = - push_new_plain_scope state; + let with_frame state m = + push_new_plain_frame state; let x = m state in - ignore (pop_scope state); + ignore (pop_frame state); x - let with_parent_scope state m = - let scope = pop_scope state in - let x = with_scope state m in - push_scope state scope; + let with_parent_frame state m = + let frame = pop_frame state in + let x = with_frame state m in + push_frame state frame; x let with_bindings_checkpoint state m = - let original_scopes_count = List1.length state.scopes in - (* Push a fresh module scope so that [m] may add declarations *) - push_new_module_scope state; + let original_frames_count = List1.length state.frames in + (* Push a fresh module frame so that [m] may add declarations *) + push_new_module_frame state; Fun.protect ~finally:(fun () -> - let final_scopes_count = List1.length state.scopes in + let final_frames_count = List1.length state.frames in if - final_scopes_count - original_scopes_count - >= 1 (* We expect there to at least be the new module scope *) + final_frames_count - original_frames_count + >= 1 (* We expect there to at least be the new module frame *) then - (* We have to count scopes because [m] may add new scopes. This is - not foolproof because [m] could have discarded too many scopes + (* We have to count frames because [m] may add new frames. This is + not foolproof because [m] could have discarded too many frames and added some more. *) - Fun.repeat (final_scopes_count - original_scopes_count) (fun () -> - ignore (pop_scope state)) + Fun.repeat (final_frames_count - original_frames_count) (fun () -> + ignore (pop_frame state)) else Error.raise_violation (Format.asprintf - "[%s] invalid states, there are fewer scopes than there \ + "[%s] invalid states, there are fewer frames than there \ originally were" __FUNCTION__)) (fun () -> m state) @@ -2027,33 +2039,37 @@ module Indexing_state = struct x let with_free_variables_as_pattern_variables state ~pattern ~expression = - let current_scope_bindings_state = - get_current_scope_bindings_state state + let current_frame_bindings_state = + get_current_frame_bindings_state state in - let pattern_scope = - Pattern_scope + let pattern_frame = + Pattern_frame { pattern_bindings = create_empty_bindings () ; pattern_variables_rev = [] ; expression_bindings = - { current_scope_bindings_state (* Copy context sizes *) with - bindings = Binding_tree.create () + { bindings = Binding_tree.create () + ; lf_context_size = current_frame_bindings_state.lf_context_size + ; meta_context_size = + current_frame_bindings_state.meta_context_size + ; comp_context_size = + current_frame_bindings_state.comp_context_size } } in - push_scope state pattern_scope; + push_frame state pattern_frame; let pattern' = allow_free_variables state (fun state -> pattern state) in - match pop_scope state with - | Module_scope _ -> + match pop_frame state with + | Module_frame _ -> Error.raise_violation (Format.asprintf - "[%s] invalid module scope, expected a pattern scope" + "[%s] invalid module frame, expected a pattern frame" __FUNCTION__) - | Plain_scope _ -> + | Plain_frame _ -> Error.raise_violation (Format.asprintf - "[%s] invalid plain scope, expected a pattern scope" + "[%s] invalid plain frame, expected a pattern frame" __FUNCTION__) - | Pattern_scope { pattern_variables_rev; expression_bindings; _ } -> ( + | Pattern_frame { pattern_variables_rev; expression_bindings; _ } -> ( match Identifier.find_duplicates (List.rev pattern_variables_rev) with @@ -2062,9 +2078,9 @@ module Indexing_state = struct (fun identifiers -> Duplicate_pattern_variables identifiers) duplicates | Option.None -> - push_scope state (Plain_scope { bindings = expression_bindings }); + push_frame state (Plain_frame { bindings = expression_bindings }); let expression' = expression state pattern' in - ignore (pop_scope state); + ignore (pop_frame state); expression') let rec add_all_mctx state cD = @@ -2106,30 +2122,30 @@ module Indexing_state = struct ; comp_context_size (* Immutable *) } - let snapshot_scope = function - | Plain_scope { bindings } -> + let snapshot_frame = function + | Plain_frame { bindings } -> let bindings' = snapshot_bindings bindings in - Plain_scope { bindings = bindings' } - | Pattern_scope + Plain_frame { bindings = bindings' } + | Pattern_frame { pattern_bindings; pattern_variables_rev; expression_bindings } -> let pattern_bindings' = snapshot_bindings pattern_bindings in let expression_bindings' = snapshot_bindings expression_bindings in - Pattern_scope + Pattern_frame { pattern_bindings = pattern_bindings' ; pattern_variables_rev (* Immutable *) ; expression_bindings = expression_bindings' } - | Module_scope { bindings; declarations } -> + | Module_frame { bindings; declarations } -> let bindings' = snapshot_bindings bindings in let declarations' = Binding_tree.snapshot declarations in - Module_scope { bindings = bindings'; declarations = declarations' } + Module_frame { bindings = bindings'; declarations = declarations' } - let snapshot_scopes scopes = List1.map snapshot_scope scopes + let snapshot_frames frames = List1.map snapshot_frame frames let snapshot_state - { scopes; free_variables_allowed; generated_fresh_variables_count } = - let scopes' = snapshot_scopes scopes in - { scopes = scopes' + { frames; free_variables_allowed; generated_fresh_variables_count } = + let frames' = snapshot_frames frames in + { frames = frames' ; free_variables_allowed (* Immutable *) ; generated_fresh_variables_count (* Immutable *) } diff --git a/src/core/index_state.mli b/src/core/index_state.mli index fdb3e94e2..ae2e54b92 100644 --- a/src/core/index_state.mli +++ b/src/core/index_state.mli @@ -287,7 +287,7 @@ module type INDEXING_STATE = sig (** [open_module state ?location module_identifier] opens the module [module_identifier] it is a bound module. This effectively adds all the - declarations in that module to the current scope, but not as + declarations in that module to the current frame, but not as declarations (i.e., this opens the module like in OCaml). *) val open_module : state -> ?location:Location.t -> Qualified_identifier.t -> Unit.t @@ -299,9 +299,16 @@ module type INDEXING_STATE = sig -> Identifier.t -> Unit.t - val with_scope : state -> (state -> 'a) -> 'a + (** [with_frame state m] runs [m] in a nested bindings frame that is + discarded afterwards. *) + val with_frame : state -> (state -> 'a) -> 'a - val with_parent_scope : state -> (state -> 'a) -> 'a + (** [with_parent_frame state m] runs [m] while ignoring the topmost frame. + + This is used for indexing Harpoon proof scripts because Harpoon + hypotheticals are already serialized with all the identifiers in the + meta-level and computation-level contexts of the proof. *) + val with_parent_frame : state -> (state -> 'a) -> 'a (** [with_bindings_checkpoint state m] runs [m] with a checkpoint on the bindings' state to backtrack to in case [m] raises an exception. diff --git a/src/core/recsgn.ml b/src/core/recsgn.ml index 108c00ac7..fb3ce25c5 100644 --- a/src/core/recsgn.ml +++ b/src/core/recsgn.ml @@ -410,23 +410,26 @@ module Make Synint.Sgn.DefaultAssocPrag { associativity; location } | Synext.Signature.Pragma.Prefix_fixity { constant; precedence; postponed; location } -> - (if postponed then - add_postponed_prefix_notation state ?precedence constant - else add_prefix_notation state ?precedence constant); - Synint.Sgn.PrefixFixityPrag { constant; precedence; postponed; location } + if postponed then + add_postponed_prefix_notation state ?precedence constant + else add_prefix_notation state ?precedence constant; + Synint.Sgn.PrefixFixityPrag + { constant; precedence; postponed; location } | Synext.Signature.Pragma.Infix_fixity { constant; precedence; associativity; postponed; location } -> - (if postponed then - add_postponed_infix_notation state ?precedence ?associativity constant - else add_infix_notation state ?precedence ?associativity constant); + if postponed then + add_postponed_infix_notation state ?precedence ?associativity + constant + else add_infix_notation state ?precedence ?associativity constant; Synint.Sgn.InfixFixityPrag { constant; precedence; associativity; postponed; location } | Synext.Signature.Pragma.Postfix_fixity { constant; precedence; postponed; location } -> - (if postponed then - add_postponed_postfix_notation state ?precedence constant - else add_postfix_notation state ?precedence constant); - Synint.Sgn.PostfixFixityPrag { constant; precedence; postponed; location } + if postponed then + add_postponed_postfix_notation state ?precedence constant + else add_postfix_notation state ?precedence constant; + Synint.Sgn.PostfixFixityPrag + { constant; precedence; postponed; location } | Synext.Signature.Pragma.Open_module { location; module_identifier } -> freeze_all_unfrozen_declarations state; open_module state ~location module_identifier; diff --git a/src/core/recsgn_state.ml b/src/core/recsgn_state.ml index ae3527d4f..b50b50195 100644 --- a/src/core/recsgn_state.ml +++ b/src/core/recsgn_state.ml @@ -529,7 +529,8 @@ struct let precedence = get_default_precedence_opt state precedence in let associativity = get_default_associativity_opt state associativity in add_postponed_notation state - (Postponed_infix_fixity { location; precedence; associativity; constant }) + (Postponed_infix_fixity + { location; precedence; associativity; constant }) let add_postponed_postfix_notation state ?location ?precedence constant = let precedence = get_default_precedence_opt state precedence in @@ -545,7 +546,8 @@ struct let apply_postponed_fixity_pragma state = function | Postponed_prefix_fixity { location; constant; precedence } -> add_prefix_notation state ?location ~precedence constant - | Postponed_infix_fixity { location; constant; precedence; associativity } -> + | Postponed_infix_fixity + { location; constant; precedence; associativity } -> add_infix_notation state ?location ~precedence ~associativity constant | Postponed_postfix_fixity { location; constant; precedence } -> diff --git a/src/html/synext_html_pp_state.ml b/src/html/synext_html_pp_state.ml index 7def997c5..56ed743c6 100644 --- a/src/html/synext_html_pp_state.ml +++ b/src/html/synext_html_pp_state.ml @@ -211,8 +211,8 @@ module Entry = struct end module Html_printing_state = struct - type scope = - | Module_scope of + type frame = + | Module_frame of { bindings : Entry.t Binding_tree.t ; declarations : Entry.t Binding_tree.t ; default_associativity : Associativity.t @@ -248,7 +248,7 @@ module Html_printing_state = struct generation of new HTML IDs. *) ; mutable formatter : Format.formatter (** The formatter for pretty-printing. *) - ; mutable scopes : scope List1.t + ; mutable frames : frame List1.t ; mutable default_precedence : Int.t (** The default precedence of user-defined operators. *) ; mutable default_associativity : Associativity.t @@ -273,9 +273,9 @@ module Html_printing_state = struct end) : Format_state.S with type state := state) - let create_module_scope ?(default_precedence = default_precedence) + let create_module_frame ?(default_precedence = default_precedence) ?(default_associativity = default_associativity) () = - Module_scope + Module_frame { bindings = Binding_tree.create () ; declarations = Binding_tree.create () ; default_precedence @@ -287,7 +287,7 @@ module Html_printing_state = struct ; formatter ; ids = String.Set.empty ; max_suffix_by_id = String.Hashtbl.create 16 - ; scopes = List1.singleton (create_module_scope ()) + ; frames = List1.singleton (create_module_frame ()) ; default_precedence ; default_associativity ; postponed_fixity_pragmas = [] @@ -376,24 +376,24 @@ module Html_printing_state = struct let set_formatter state formatter = state.formatter <- formatter - let get_scope_bindings = function - | Module_scope { bindings; _ } -> bindings + let get_frame_bindings = function + | Module_frame { bindings; _ } -> bindings - let get_current_scope state = List1.head state.scopes + let get_current_frame state = List1.head state.frames - let get_current_scope_bindings state = - get_scope_bindings (get_current_scope state) + let get_current_frame_bindings state = + get_frame_bindings (get_current_frame state) - let push_scope state scope = state.scopes <- List1.cons scope state.scopes + let push_frame state frame = state.frames <- List1.cons frame state.frames - let pop_scope state = - match state.scopes with + let pop_frame state = + match state.frames with | List1.T (x1, x2 :: xs) -> - state.scopes <- List1.from x2 xs; + state.frames <- List1.from x2 xs; x1 | List1.T (_x, []) -> Error.raise_violation - (Format.asprintf "[%s] cannot pop the last scope" __FUNCTION__) + (Format.asprintf "[%s] cannot pop the last frame" __FUNCTION__) let set_default_associativity state default_associativity = state.default_associativity <- default_associativity @@ -414,13 +414,13 @@ module Html_printing_state = struct | Option.Some precedence -> precedence let add_binding state identifier ?subtree entry = - match get_current_scope state with - | Module_scope { bindings; _ } -> + match get_current_frame state with + | Module_frame { bindings; _ } -> Binding_tree.add_toplevel identifier entry ?subtree bindings let add_declaration state identifier ?subtree entry = - match get_current_scope state with - | Module_scope + match get_current_frame state with + | Module_frame { bindings ; declarations ; default_associativity = _ @@ -486,15 +486,15 @@ module Html_printing_state = struct let add_module state ?location identifier ~id f = let default_associativity = get_default_associativity state in let default_precedence = get_default_precedence state in - let module_scope = - create_module_scope ~default_associativity ~default_precedence () + let module_frame = + create_module_frame ~default_associativity ~default_precedence () in - push_scope state module_scope; + push_frame state module_frame; let x = f state in - (match get_current_scope state with - | Module_scope + (match get_current_frame state with + | Module_frame { declarations; default_associativity; default_precedence; _ } -> - ignore (pop_scope state); + ignore (pop_frame state); add_declaration state identifier ~subtree:declarations (Entry.make_module_entry ?location ~page:state.current_page ~id identifier); @@ -502,15 +502,15 @@ module Html_printing_state = struct set_default_precedence state default_precedence); x - let rec lookup_in_scopes scopes identifiers = - match scopes with + let rec lookup_in_frames frames identifiers = + match frames with | [] -> Error.raise (Qualified_identifier.Unbound_qualified_identifier (Qualified_identifier.from_list1 identifiers)) - | scope :: scopes -> ( + | frame :: frames -> ( match - Binding_tree.maximum_lookup identifiers (get_scope_bindings scope) + Binding_tree.maximum_lookup identifiers (get_frame_bindings frame) with | Binding_tree.Bound { entry; subtree; _ } -> (entry, subtree) | Binding_tree.Partially_bound { leading_segments; segment; _ } -> @@ -518,11 +518,11 @@ module Html_printing_state = struct (Qualified_identifier.Unbound_namespace (Qualified_identifier.make ~namespaces:leading_segments segment)) - | Binding_tree.Unbound _ -> lookup_in_scopes scopes identifiers) + | Binding_tree.Unbound _ -> lookup_in_frames frames identifiers) let lookup state query = let identifiers = Qualified_identifier.to_list1 query in - try lookup_in_scopes (List1.to_list state.scopes) identifiers with + try lookup_in_frames (List1.to_list state.frames) identifiers with | exn -> Error.re_raise (Error.located_exception1 @@ -547,14 +547,14 @@ module Html_printing_state = struct let modify_operator state identifier f = let entry, subtree = lookup state identifier in let entry' = Entry.modify_operator f entry in - let bindings = get_current_scope_bindings state in + let bindings = get_current_frame_bindings state in if Binding_tree.mem identifier bindings then Binding_tree.replace identifier (fun _entry _subtree -> (entry', subtree)) bindings else Binding_tree.add identifier ~subtree entry' bindings; - match get_current_scope state with - | Module_scope { declarations; _ } -> + match get_current_frame state with + | Module_frame { declarations; _ } -> if Binding_tree.mem identifier declarations then Binding_tree.replace identifier (fun _entry subtree -> (entry', subtree)) @@ -615,7 +615,7 @@ module Html_printing_state = struct let open_namespace state identifier = let _entry, subtree = lookup state identifier in - let bindings = get_current_scope_bindings state in + let bindings = get_current_frame_bindings state in Binding_tree.add_all bindings subtree let open_module state identifier = open_namespace state identifier diff --git a/src/parser/disambiguation_state.ml b/src/parser/disambiguation_state.ml index c581a6b19..830cd241b 100644 --- a/src/parser/disambiguation_state.ml +++ b/src/parser/disambiguation_state.ml @@ -639,9 +639,9 @@ module type DISAMBIGUATION_STATE = sig val with_free_variables_as_pattern_variables : state -> pattern:(state -> 'a) -> expression:(state -> 'a -> 'b) -> 'b - val with_scope : state -> (state -> 'a) -> 'a + val with_frame : state -> (state -> 'a) -> 'a - val with_parent_scope : state -> (state -> 'a) -> 'a + val with_parent_frame : state -> (state -> 'a) -> 'a val with_bindings_checkpoint : state -> (state -> 'a) -> 'a @@ -771,17 +771,17 @@ module Disambiguation_state = struct (** A bindings environment is a binding tree of entries. *) type bindings = Entry.t Binding_tree.t - (** A referencing environment is a stack of scopes (LIFO data structure). + (** A referencing environment is a stack of frames (LIFO data structure). An identifier is unbound in a referencing environment if it is unbound - in each of its scopes. An identifier is bound to an entry if it is - bound in one of the scopes. In lookups, the returned entry is the one - in the first scope that has the identifier bound. *) - type referencing_environment = scope List1.t - - and scope = - | Plain_scope of { bindings : bindings } - (** Plain scopes are scopes without special operations. *) - | Pattern_scope of + in each of its frames. An identifier is bound to an entry if it is + bound in one of the frames. In lookups, the returned entry is the one + in the first frame that has the identifier bound. *) + type referencing_environment = frame List1.t + + and frame = + | Plain_frame of { bindings : bindings } + (** Plain frames are frames without special operations. *) + | Pattern_frame of { pattern_bindings : bindings (** The bindings to use to disambiguate nodes in the pattern AST. *) @@ -792,14 +792,14 @@ module Disambiguation_state = struct (** The bindings to use for disambiguating the expression using the accumulated free variables as bound variables. *) } - (** Pattern scopes are scopes that keep track of added free variables + (** Pattern frames are frames that keep track of added free variables in patterns in order to add them to the expression bindings as bound variables. *) - | Module_scope of + | Module_frame of { bindings : bindings ; declarations : bindings } - (** Module scopes are scopes that keep track of added declarations in + (** Module frames are frames that keep track of added declarations in order to add them as declarations in the module being disambiguated. *) @@ -823,7 +823,7 @@ module Disambiguation_state = struct } type state = - { mutable scopes : referencing_environment + { mutable frames : referencing_environment ; mutable default_associativity : Associativity.t (** The default associativity to use for user-defined operators. *) ; mutable default_precedence : Int.t @@ -839,40 +839,40 @@ module Disambiguation_state = struct end) : Imperative_state.IMPERATIVE_STATE with type state := state) - let create_empty_plain_scope () = - Plain_scope { bindings = Binding_tree.create () } + let create_empty_plain_frame () = + Plain_frame { bindings = Binding_tree.create () } - let create_plain_scope bindings = Plain_scope { bindings } + let create_plain_frame bindings = Plain_frame { bindings } - let create_pattern_scope () = - Pattern_scope + let create_pattern_frame () = + Pattern_frame { pattern_bindings = Binding_tree.create () ; pattern_variables_rev = [] ; expression_bindings = Binding_tree.create () } - let create_module_scope () = - Module_scope + let create_module_frame () = + Module_frame { bindings = Binding_tree.create () ; declarations = Binding_tree.create () } let create_initial_state () = - { scopes = List1.singleton (create_module_scope ()) + { frames = List1.singleton (create_module_frame ()) ; default_precedence = Synext.default_precedence ; default_associativity = Synext.default_associativity ; postponed_fixity_pragmas = [] } let clear_state state = - state.scopes <- List1.singleton (create_module_scope ()); + state.frames <- List1.singleton (create_module_frame ()); state.default_precedence <- Synext.default_precedence; state.default_associativity <- Synext.default_associativity - let get_scope_bindings = function - | Plain_scope { bindings } -> bindings - | Module_scope { bindings; _ } -> bindings - | Pattern_scope { pattern_bindings; _ } -> pattern_bindings + let get_frame_bindings = function + | Plain_frame { bindings } -> bindings + | Module_frame { bindings; _ } -> bindings + | Pattern_frame { pattern_bindings; _ } -> pattern_bindings let set_default_associativity state default_associativity = state.default_associativity <- default_associativity @@ -892,52 +892,55 @@ module Disambiguation_state = struct | Option.None -> get_default_precedence state | Option.Some precedence -> precedence - let[@inline] push_scope state scope = - state.scopes <- List1.cons scope state.scopes + let[@inline] push_frame state frame = + state.frames <- List1.cons frame state.frames - let pop_scope state = - match state.scopes with + let pop_frame state = + match state.frames with | List1.T (x1, x2 :: xs) -> - state.scopes <- List1.from x2 xs; + state.frames <- List1.from x2 xs; x1 | List1.T (_x, []) -> Error.raise_violation - (Format.asprintf "[%s] cannot pop the last scope" __FUNCTION__) + (Format.asprintf "[%s] cannot pop the last frame" __FUNCTION__) - let[@inline] get_current_scope state = List1.head state.scopes + let[@inline] get_current_frame state = List1.head state.frames - let[@inline] get_current_scope_bindings state = - get_scope_bindings (get_current_scope state) + let[@inline] get_current_frame_bindings state = + get_frame_bindings (get_current_frame state) let add_binding state identifier ?subtree entry = - match get_current_scope state with - | Plain_scope { bindings } - | Pattern_scope { pattern_bindings = bindings; _ } - | Module_scope { bindings; _ } -> + match get_current_frame state with + | Plain_frame { bindings } + | Pattern_frame { pattern_bindings = bindings; _ } + | Module_frame { bindings; _ } -> Binding_tree.add_toplevel identifier entry ?subtree bindings + (** [remove_binding state identifier] removes the latest binding of + [identifier] from [state]. It is assumed that this binding was + introduced in the current frame. *) let remove_binding state identifier = - match get_current_scope state with - | Plain_scope { bindings } - | Pattern_scope { pattern_bindings = bindings; _ } - | Module_scope { bindings; _ } -> + match get_current_frame state with + | Plain_frame { bindings } + | Pattern_frame { pattern_bindings = bindings; _ } + | Module_frame { bindings; _ } -> Binding_tree.remove identifier bindings (** [add_declaration state identifier ?subtree entry] adds - [(entry, subtree)] as a declaration in the current module scope, bound - to [identifier] in [state]. It is assumed that the current scope in - [state] is indeed a module scope. *) + [(entry, subtree)] as a declaration in the current module frame, bound + to [identifier] in [state]. It is assumed that the current frame in + [state] is indeed a module frame. *) let add_declaration state identifier ?subtree entry = - match get_current_scope state with - | Plain_scope _ -> + match get_current_frame state with + | Plain_frame _ -> Error.raise_violation - (Format.asprintf "[%s] invalid plain scope disambiguation state" + (Format.asprintf "[%s] invalid plain frame disambiguation state" __FUNCTION__) - | Pattern_scope _ -> + | Pattern_frame _ -> Error.raise_violation - (Format.asprintf "[%s] invalid pattern scope disambiguation state" + (Format.asprintf "[%s] invalid pattern frame disambiguation state" __FUNCTION__) - | Module_scope { bindings; declarations } -> + | Module_frame { bindings; declarations } -> Binding_tree.add_toplevel identifier entry ?subtree bindings; Binding_tree.add_toplevel identifier entry ?subtree declarations @@ -1023,27 +1026,27 @@ module Disambiguation_state = struct nothing. *) let add_free_meta_level_variable state identifier entry = - match get_current_scope state with - | Pattern_scope scope -> + match get_current_frame state with + | Pattern_frame frame -> (* Free meta-level variables will have reconstructed binders in the pattern meta-context, so they are hereafter considered as bound in the pattern. *) - Binding_tree.add_toplevel identifier entry scope.pattern_bindings; - Binding_tree.add_toplevel identifier entry scope.expression_bindings; - scope.pattern_variables_rev <- - identifier :: scope.pattern_variables_rev - | Module_scope _ - | Plain_scope _ -> + Binding_tree.add_toplevel identifier entry frame.pattern_bindings; + Binding_tree.add_toplevel identifier entry frame.expression_bindings; + frame.pattern_variables_rev <- + identifier :: frame.pattern_variables_rev + | Module_frame _ + | Plain_frame _ -> () (* Currently not keeping track of free variables. *) let add_free_comp_level_variable state identifier entry = - match get_current_scope state with - | Pattern_scope scope -> - Binding_tree.add_toplevel identifier entry scope.expression_bindings; - scope.pattern_variables_rev <- - identifier :: scope.pattern_variables_rev - | Module_scope _ - | Plain_scope _ -> + match get_current_frame state with + | Pattern_frame frame -> + Binding_tree.add_toplevel identifier entry frame.expression_bindings; + frame.pattern_variables_rev <- + identifier :: frame.pattern_variables_rev + | Module_frame _ + | Plain_frame _ -> () (* Currently not keeping track of free variables. *) let add_free_lf_variable state ?location identifier = @@ -1072,85 +1075,85 @@ module Disambiguation_state = struct let entry_is_not_variable entry = Bool.not (Entry.is_variable entry) - let lookup_toplevel_in_scope scope query = - Binding_tree.lookup_toplevel_opt query (get_scope_bindings scope) + let lookup_toplevel_in_frame frame query = + Binding_tree.lookup_toplevel_opt query (get_frame_bindings frame) - let lookup_toplevel_in_scopes scopes query = - List.find_map (fun scope -> lookup_toplevel_in_scope scope query) scopes + let lookup_toplevel_in_frames frames query = + List.find_map (fun frame -> lookup_toplevel_in_frame frame query) frames - let rec lookup_toplevel_declaration_in_scopes scopes query = - match scopes with - | [] -> (* Exhausted the list of scopes to check. *) Option.none - | scope :: scopes -> ( - let scope_bindings = get_scope_bindings scope in - match Binding_tree.lookup_toplevel_opt query scope_bindings with + let rec lookup_toplevel_declaration_in_frames frames query = + match frames with + | [] -> (* Exhausted the list of frames to check. *) Option.none + | frame :: frames -> ( + let frame_bindings = get_frame_bindings frame in + match Binding_tree.lookup_toplevel_opt query frame_bindings with | Option.Some (entry, subtree) when entry_is_not_variable entry -> - (* [query] is bound to a declaration in [scope]. *) + (* [query] is bound to a declaration in [frame]. *) Option.some (entry, subtree) | Option.Some _ -> - (* [query] is bound to a variable in [scope], so any declaration - in [scopes] bound to [query] is shadowed. *) + (* [query] is bound to a variable in [frame], so any declaration + in [frames] bound to [query] is shadowed. *) Option.none | Option.None -> - (* [query] is unbound in [scope], so check in the parent - scopes. *) - lookup_toplevel_declaration_in_scopes scopes query) + (* [query] is unbound in [frame], so check in the parent + frames. *) + lookup_toplevel_declaration_in_frames frames query) let internal_lookup_toplevel_opt state query = - match state.scopes with - | List1.T ((Pattern_scope _ as scope), scopes) -> ( - (* Overridden behaviour for pattern scopes. Variables can only be - looked up in that pattern scope, and declarations can only be - looked up in parent scopes. *) - match lookup_toplevel_in_scope scope query with + match state.frames with + | List1.T ((Pattern_frame _ as frame), frames) -> ( + (* Overridden behaviour for pattern frames. Variables can only be + looked up in that pattern frame, and declarations can only be + looked up in parent frames. *) + match lookup_toplevel_in_frame frame query with | Option.Some x -> Option.some x - | Option.None -> lookup_toplevel_declaration_in_scopes scopes query) - | List1.T (scope, scopes) -> - lookup_toplevel_in_scopes (scope :: scopes) query + | Option.None -> lookup_toplevel_declaration_in_frames frames query) + | List1.T (frame, frames) -> + lookup_toplevel_in_frames (frame :: frames) query - (** [lookup_in_scopes scopes identifiers] looks up for an entry bound to + (** [lookup_in_frames frames identifiers] looks up for an entry bound to the qualified identifier formed by [identifiers] successively in - [scopes]. The qualified identifier being represented as a list of + [frames]. The qualified identifier being represented as a list of identifiers is an optimization. If an entry is fully bound or partially - bound in a scope, then the search ends. The [scopes] are arranged as a + bound in a frame, then the search ends. The [frames] are arranged as a stack. *) - let rec lookup_in_scopes scopes identifiers = - match scopes with + let rec lookup_in_frames frames identifiers = + match frames with | [] -> Error.raise (Unbound_qualified_identifier (Qualified_identifier.from_list1 identifiers)) - | scope :: scopes -> ( + | frame :: frames -> ( match - Binding_tree.maximum_lookup identifiers (get_scope_bindings scope) + Binding_tree.maximum_lookup identifiers (get_frame_bindings frame) with | Binding_tree.Bound { entry; subtree; _ } -> (entry, subtree) | Binding_tree.Partially_bound { leading_segments; segment; _ } -> - (* The [leading_segments] are bound in [scope], so any binding - for [identifiers] in [scopes] is shadowed. *) + (* The [leading_segments] are bound in [frame], so any binding + for [identifiers] in [frames] is shadowed. *) Error.raise (Unbound_namespace (Qualified_identifier.make ~namespaces:leading_segments segment)) - | Binding_tree.Unbound _ -> lookup_in_scopes scopes identifiers) + | Binding_tree.Unbound _ -> lookup_in_frames frames identifiers) - let rec lookup_declaration_in_scopes scopes identifiers = - match scopes with + let rec lookup_declaration_in_frames frames identifiers = + match frames with | [] -> - (* Exhausted the list of scopes to check. *) + (* Exhausted the list of frames to check. *) Error.raise (Unbound_qualified_identifier (Qualified_identifier.from_list1 identifiers)) - | scope :: scopes -> ( - let scope_bindings = get_scope_bindings scope in - match Binding_tree.maximum_lookup identifiers scope_bindings with + | frame :: frames -> ( + let frame_bindings = get_frame_bindings frame in + match Binding_tree.maximum_lookup identifiers frame_bindings with | Binding_tree.Bound { entry; subtree; _ } when entry_is_not_variable entry -> - (* [query] is bound to a declaration in [scope]. *) + (* [query] is bound to a declaration in [frame]. *) (entry, subtree) | Binding_tree.Bound _result -> - (* [query is bound to a variable in [scope], so any declaration - in [scopes] bound to [query] is shadowed. *) + (* [query is bound to a variable in [frame], so any declaration + in [frames] bound to [query] is shadowed. *) assert (List1.length identifiers = 1) (* Variables can't be in namespaces *); Error.raise @@ -1162,7 +1165,7 @@ module Disambiguation_state = struct (Qualified_identifier.make ~namespaces:leading_segments segment)) | Binding_tree.Unbound _ -> - lookup_declaration_in_scopes scopes identifiers) + lookup_declaration_in_frames frames identifiers) (** [internal_lookup state query] is [(entry, subtree)], where [entry] is the entry bound to [query] in [state], and [subtree] is the tree of @@ -1172,16 +1175,16 @@ module Disambiguation_state = struct [subtree] is returned. *) let internal_lookup state query = let identifiers = Qualified_identifier.to_list1 query in - match state.scopes with - | List1.T ((Pattern_scope _ as scope), scopes) -> ( - (* Overridden behaviour for pattern scopes. Variables can only be - looked up in that pattern scope, and declarations can only be - looked up in parent scopes. *) + match state.frames with + | List1.T ((Pattern_frame _ as frame), frames) -> ( + (* Overridden behaviour for pattern frames. Variables can only be + looked up in that pattern frame, and declarations can only be + looked up in parent frames. *) match - Binding_tree.maximum_lookup identifiers (get_scope_bindings scope) + Binding_tree.maximum_lookup identifiers (get_frame_bindings frame) with | Binding_tree.Bound { entry; subtree; _ } -> - (* An inner pattern variable is in scope *) (entry, subtree) + (* An inner pattern variable is in frame *) (entry, subtree) | Binding_tree.Partially_bound { leading_segments; segment; _ } -> (* An inner pattern variable shadowed a namespace *) Error.raise @@ -1189,9 +1192,9 @@ module Disambiguation_state = struct (Qualified_identifier.make ~namespaces:leading_segments segment)) | Binding_tree.Unbound _ -> - lookup_declaration_in_scopes scopes identifiers) - | List1.T (scope, scopes) -> - lookup_in_scopes (scope :: scopes) identifiers + lookup_declaration_in_frames frames identifiers) + | List1.T (frame, frames) -> + lookup_in_frames (frame :: frames) identifiers type maximum_lookup_result = | Unbound of { segments : Identifier.t List1.t } @@ -1203,12 +1206,12 @@ module Disambiguation_state = struct } | Bound of { entry : Entry.t } - let rec maximum_lookup_in_scopes scopes identifiers = - match scopes with + let rec maximum_lookup_in_frames frames identifiers = + match frames with | [] -> Unbound { segments = identifiers } - | scope :: scopes -> ( + | frame :: frames -> ( match - Binding_tree.maximum_lookup identifiers (get_scope_bindings scope) + Binding_tree.maximum_lookup identifiers (get_frame_bindings frame) with | Binding_tree.Bound { entry; _ } -> Bound { entry } | Binding_tree.Partially_bound @@ -1216,14 +1219,14 @@ module Disambiguation_state = struct Partially_bound { leading_segments; segment; entry; trailing_segments } | Binding_tree.Unbound _ -> - maximum_lookup_in_scopes scopes identifiers) + maximum_lookup_in_frames frames identifiers) - let rec maximum_lookup_declaration_in_scopes scopes identifiers = - match scopes with + let rec maximum_lookup_declaration_in_frames frames identifiers = + match frames with | [] -> Unbound { segments = identifiers } - | scope :: scopes -> ( + | frame :: frames -> ( match - Binding_tree.maximum_lookup identifiers (get_scope_bindings scope) + Binding_tree.maximum_lookup identifiers (get_frame_bindings frame) with | Binding_tree.Bound { entry; _ } -> if Entry.is_variable entry then @@ -1234,16 +1237,16 @@ module Disambiguation_state = struct Partially_bound { leading_segments; segment; entry; trailing_segments } | Binding_tree.Unbound _ -> - maximum_lookup_declaration_in_scopes scopes identifiers) + maximum_lookup_declaration_in_frames frames identifiers) let maximum_lookup state identifiers = - match state.scopes with - | List1.T ((Pattern_scope _ as scope), scopes) -> ( - (* Overridden behaviour for pattern scopes. Variables can only be - looked up in that pattern scope, and declarations can only be - looked up in parent scopes. *) + match state.frames with + | List1.T ((Pattern_frame _ as frame), frames) -> ( + (* Overridden behaviour for pattern frames. Variables can only be + looked up in that pattern frame, and declarations can only be + looked up in parent frames. *) match - Binding_tree.maximum_lookup identifiers (get_scope_bindings scope) + Binding_tree.maximum_lookup identifiers (get_frame_bindings frame) with | Binding_tree.Bound { entry; _ } -> Bound { entry } | Binding_tree.Partially_bound @@ -1251,9 +1254,9 @@ module Disambiguation_state = struct Partially_bound { leading_segments; segment; entry; trailing_segments } | Binding_tree.Unbound _ -> - maximum_lookup_declaration_in_scopes scopes identifiers) - | List1.T (scope, scopes) -> - maximum_lookup_in_scopes (scope :: scopes) identifiers + maximum_lookup_declaration_in_frames frames identifiers) + | List1.T (frame, frames) -> + maximum_lookup_in_frames (frame :: frames) identifiers let raise_duplicate_identifiers_exception f duplicates = match duplicates with @@ -1289,19 +1292,19 @@ module Disambiguation_state = struct (actual_binding_exn identifier entry))) entry in - (* Update the entry in the current scope only *) - let bindings = get_current_scope_bindings state in + (* Update the entry in the current frame only *) + let bindings = get_current_frame_bindings state in if Binding_tree.mem identifier bindings then Binding_tree.replace identifier (fun _entry _subtree -> (entry', subtree)) bindings else Binding_tree.add identifier ~subtree entry' bindings; - (* If we're currently in a module scope, additionally update the exported + (* If we're currently in a module frame, additionally update the exported declaration *) - match get_current_scope state with - | Plain_scope _ -> () - | Pattern_scope _ -> () - | Module_scope { declarations; _ } -> + match get_current_frame state with + | Plain_frame _ -> () + | Pattern_frame _ -> () + | Module_frame { declarations; _ } -> if Binding_tree.mem identifier declarations then Binding_tree.replace identifier (fun _entry subtree -> (entry', subtree)) @@ -1381,7 +1384,7 @@ module Disambiguation_state = struct let open_namespace state identifier = let _entry, subtree = internal_lookup state identifier in - let bindings = get_current_scope_bindings state in + let bindings = get_current_frame_bindings state in Binding_tree.add_all bindings subtree let open_module state identifier = @@ -1473,67 +1476,67 @@ module Disambiguation_state = struct remove_binding state identifier; x - let push_new_module_scope state = - let module_scope = create_module_scope () in - push_scope state module_scope + let push_new_module_frame state = + let module_frame = create_module_frame () in + push_frame state module_frame let add_module state ?location identifier m = let default_associativity = get_default_associativity state in let default_precedence = get_default_precedence state in - push_new_module_scope state; + push_new_module_frame state; let x = m state in match - pop_scope - state (* We expect the newly pushed module scope to be popped *) + pop_frame + state (* We expect the newly pushed module frame to be popped *) with - | Plain_scope _ -> + | Plain_frame _ -> Error.raise_violation - (Format.asprintf "[%s] invalid plain scope state" __FUNCTION__) - | Pattern_scope _ -> + (Format.asprintf "[%s] invalid plain frame state" __FUNCTION__) + | Pattern_frame _ -> Error.raise_violation - (Format.asprintf "[%s] invalid pattern scope state" __FUNCTION__) - | Module_scope { declarations; _ } -> + (Format.asprintf "[%s] invalid pattern frame state" __FUNCTION__) + | Module_frame { declarations; _ } -> add_declaration state identifier ~subtree:declarations (Entry.make_module_entry ?location identifier); set_default_associativity state default_associativity; set_default_precedence state default_precedence; x - let with_scope state m = - let scope = create_empty_plain_scope () in - push_scope state scope; + let with_frame state m = + let frame = create_empty_plain_frame () in + push_frame state frame; let x = m state in - ignore (pop_scope state); + ignore (pop_frame state); x - let with_parent_scope state m = - let scope = pop_scope state in - let x = with_scope state m in - push_scope state scope; + let with_parent_frame state m = + let frame = pop_frame state in + let x = with_frame state m in + push_frame state frame; x let with_bindings_checkpoint state m = - let original_scopes_count = List1.length state.scopes in - (* Push a fresh module scope so that [m] may add declarations *) - push_new_module_scope state; + let original_frames_count = List1.length state.frames in + (* Push a fresh module frame so that [m] may add declarations *) + push_new_module_frame state; Fun.protect ~finally:(fun () -> - let final_scopes_count = List1.length state.scopes in - let scopes_to_pop_count = - final_scopes_count - original_scopes_count + let final_frames_count = List1.length state.frames in + let frames_to_pop_count = + final_frames_count - original_frames_count in if - scopes_to_pop_count - >= 1 (* We expect there to at least be the new module scope *) + frames_to_pop_count + >= 1 (* We expect there to at least be the new module frame *) then - (* We have to count scopes because [m] may add new scopes. This is - not foolproof because [m] could have discarded too many scopes + (* We have to count frames because [m] may add new frames. This is + not foolproof because [m] could have discarded too many frames and added some more. *) - Fun.repeat scopes_to_pop_count (fun () -> ignore (pop_scope state)) + Fun.repeat frames_to_pop_count (fun () -> ignore (pop_frame state)) else Error.raise_violation (Format.asprintf - "[%s] invalid states, there are fewer scopes than there \ + "[%s] invalid states, there are fewer frames than there \ originally were" __FUNCTION__)) (fun () -> m state) @@ -1561,17 +1564,17 @@ module Disambiguation_state = struct let with_free_variables_as_pattern_variables state ~pattern:disambiguate_pattern ~expression:disambiguate_expression = - let pattern_scope = create_pattern_scope () in - push_scope state pattern_scope; + let pattern_frame = create_pattern_frame () in + push_frame state pattern_frame; let pattern' = disambiguate_pattern state in - match pop_scope state (* We expect [pattern_scope] to be popped *) with - | Plain_scope _ -> + match pop_frame state (* We expect [pattern_frame] to be popped *) with + | Plain_frame _ -> Error.raise_violation - (Format.asprintf "[%s] invalid plain scope state" __FUNCTION__) - | Module_scope _ -> + (Format.asprintf "[%s] invalid plain frame state" __FUNCTION__) + | Module_frame _ -> Error.raise_violation - (Format.asprintf "[%s] invalid module scope state" __FUNCTION__) - | Pattern_scope + (Format.asprintf "[%s] invalid module frame state" __FUNCTION__) + | Pattern_frame { pattern_bindings = _; pattern_variables_rev; expression_bindings } -> ( match @@ -1582,11 +1585,11 @@ module Disambiguation_state = struct (fun identifiers -> Duplicate_pattern_variables identifiers) duplicates | Option.None -> - let expression_scope = create_plain_scope expression_bindings in - push_scope state expression_scope; + let expression_frame = create_plain_frame expression_bindings in + push_frame state expression_frame; let expression' = disambiguate_expression state pattern' in - ignore (pop_scope state) - (* We expect [expression_scope] to be popped *); + ignore (pop_frame state) + (* We expect [expression_frame] to be popped *); expression') let lookup_toplevel state identifier = @@ -1606,36 +1609,36 @@ module Disambiguation_state = struct | (exception Unbound_qualified_identifier _) -> Option.none - let snapshot_scope = function - | Plain_scope { bindings } -> + let snapshot_frame = function + | Plain_frame { bindings } -> let bindings' = Binding_tree.snapshot bindings in - Plain_scope { bindings = bindings' } - | Pattern_scope + Plain_frame { bindings = bindings' } + | Pattern_frame { pattern_bindings; pattern_variables_rev; expression_bindings } -> let pattern_bindings' = Binding_tree.snapshot pattern_bindings in let expression_bindings' = Binding_tree.snapshot expression_bindings in - Pattern_scope + Pattern_frame { pattern_bindings = pattern_bindings' ; pattern_variables_rev (* Immutable *) ; expression_bindings = expression_bindings' } - | Module_scope { bindings; declarations } -> + | Module_frame { bindings; declarations } -> let bindings' = Binding_tree.snapshot bindings in let declarations' = Binding_tree.snapshot declarations in - Module_scope { bindings = bindings'; declarations = declarations' } + Module_frame { bindings = bindings'; declarations = declarations' } - let snapshot_scopes scopes = List1.map snapshot_scope scopes + let snapshot_frames frames = List1.map snapshot_frame frames let snapshot_state - { scopes + { frames ; default_associativity ; default_precedence ; postponed_fixity_pragmas } = - let scopes' = snapshot_scopes scopes in - { scopes = scopes' + let frames' = snapshot_frames frames in + { frames = frames' ; default_associativity (* Immutable *) ; default_precedence (* Immutable *) ; postponed_fixity_pragmas (* Immutable *) diff --git a/src/parser/disambiguation_state.mli b/src/parser/disambiguation_state.mli index a310068a7..d7018fdc2 100644 --- a/src/parser/disambiguation_state.mli +++ b/src/parser/disambiguation_state.mli @@ -348,16 +348,16 @@ module type DISAMBIGUATION_STATE = sig val with_free_variables_as_pattern_variables : state -> pattern:(state -> 'a) -> expression:(state -> 'a -> 'b) -> 'b - (** [with_scope state m] runs [m] in a nested bindings scope that is + (** [with_frame state m] runs [m] in a nested bindings frame that is discarded afterwards. *) - val with_scope : state -> (state -> 'a) -> 'a + val with_frame : state -> (state -> 'a) -> 'a - (** [with_parent_scope state m] runs [m] while ignoring the topmost scope. + (** [with_parent_frame state m] runs [m] while ignoring the topmost frame. This is used for the disambiguation of Harpoon proof scripts because Harpoon hypotheticals are already serialized with all the identifiers in the meta-level and computation-level contexts of the proof. *) - val with_parent_scope : state -> (state -> 'a) -> 'a + val with_parent_frame : state -> (state -> 'a) -> 'a (** [with_bindings_checkpoint state m] runs [m] with a checkpoint on the bindings' state to backtrack to in case [m] raises an exception. @@ -371,7 +371,7 @@ module type DISAMBIGUATION_STATE = sig This checkpoint mechanism does not perform a copy or snapshot of the referencing environment. You need to make sure that [m] does not pop - too many scopes. *) + too many frames. *) val with_bindings_checkpoint : state -> (state -> 'a) -> 'a (** {1 Constants} *) diff --git a/src/parser/harpoon_disambiguation.ml b/src/parser/harpoon_disambiguation.ml index f54dd44cf..4a75be4f2 100644 --- a/src/parser/harpoon_disambiguation.ml +++ b/src/parser/harpoon_disambiguation.ml @@ -176,7 +176,7 @@ struct ; comp_context ; proof } -> - with_parent_scope state (fun state -> + with_parent_frame state (fun state -> with_disambiguated_meta_context state meta_context (fun state meta_context' -> with_disambiguated_comp_context state comp_context diff --git a/src/parser/signature_disambiguation.ml b/src/parser/signature_disambiguation.ml index 15752c11b..c80cf1fae 100644 --- a/src/parser/signature_disambiguation.ml +++ b/src/parser/signature_disambiguation.ml @@ -571,7 +571,7 @@ struct traverse_option state disambiguate_totality_declaration order in let body' = - with_scope state (fun state -> + with_frame state (fun state -> disambiguate_harpoon_proof state body) in Synext.Signature.Declaration.Proof diff --git a/src/syntax/synext/synext_pp_state.ml b/src/syntax/synext/synext_pp_state.ml index 342ecc71e..81607ea07 100644 --- a/src/syntax/synext/synext_pp_state.ml +++ b/src/syntax/synext/synext_pp_state.ml @@ -135,8 +135,8 @@ module Entry = struct end module Printing_state = struct - type scope = - | Module_scope of + type frame = + | Module_frame of { bindings : Entry.t Binding_tree.t ; declarations : Entry.t Binding_tree.t } @@ -162,7 +162,7 @@ module Printing_state = struct type state = { mutable formatter : Format.formatter - ; mutable scopes : scope List1.t + ; mutable frames : frame List1.t ; mutable default_precedence : Int.t ; mutable default_associativity : Associativity.t ; mutable postponed_fixity_pragmas : postponed_fixity_pragma List.t @@ -178,15 +178,15 @@ module Printing_state = struct end) : Format_state.S with type state := state) - let create_module_scope () = - Module_scope + let create_module_frame () = + Module_frame { bindings = Binding_tree.create () ; declarations = Binding_tree.create () } let create_initial_state formatter = { formatter - ; scopes = List1.singleton (create_module_scope ()) + ; frames = List1.singleton (create_module_frame ()) ; default_precedence ; default_associativity ; postponed_fixity_pragmas = [] @@ -194,24 +194,24 @@ module Printing_state = struct let set_formatter state formatter = state.formatter <- formatter - let get_scope_bindings = function - | Module_scope { bindings; _ } -> bindings + let get_frame_bindings = function + | Module_frame { bindings; _ } -> bindings - let get_current_scope state = List1.head state.scopes + let get_current_frame state = List1.head state.frames - let get_current_scope_bindings state = - get_scope_bindings (get_current_scope state) + let get_current_frame_bindings state = + get_frame_bindings (get_current_frame state) - let push_scope state scope = state.scopes <- List1.cons scope state.scopes + let push_frame state frame = state.frames <- List1.cons frame state.frames - let pop_scope state = - match state.scopes with + let pop_frame state = + match state.frames with | List1.T (x1, x2 :: xs) -> - state.scopes <- List1.from x2 xs; + state.frames <- List1.from x2 xs; x1 | List1.T (_x, []) -> Error.raise_violation - (Format.asprintf "[%s] cannot pop the last scope" __FUNCTION__) + (Format.asprintf "[%s] cannot pop the last frame" __FUNCTION__) let set_default_associativity state default_associativity = state.default_associativity <- default_associativity @@ -232,13 +232,13 @@ module Printing_state = struct | Option.Some precedence -> precedence let add_binding state identifier ?subtree entry = - match get_current_scope state with - | Module_scope { bindings; _ } -> + match get_current_frame state with + | Module_frame { bindings; _ } -> Binding_tree.add_toplevel identifier entry ?subtree bindings let add_declaration state identifier ?subtree entry = - match get_current_scope state with - | Module_scope { bindings; declarations } -> + match get_current_frame state with + | Module_frame { bindings; declarations } -> Binding_tree.add_toplevel identifier entry ?subtree bindings; Binding_tree.add_toplevel identifier entry ?subtree declarations @@ -289,26 +289,26 @@ module Printing_state = struct let add_module state ?location identifier f = let default_associativity = get_default_associativity state in let default_precedence = get_default_precedence state in - let module_scope = create_module_scope () in - push_scope state module_scope; + let module_frame = create_module_frame () in + push_frame state module_frame; let x = f state in - match pop_scope state with - | Module_scope { declarations; _ } -> + match pop_frame state with + | Module_frame { declarations; _ } -> add_declaration state identifier ~subtree:declarations (Entry.make_module_entry ?location identifier); set_default_associativity state default_associativity; set_default_precedence state default_precedence; x - let rec lookup_in_scopes scopes identifiers = - match scopes with + let rec lookup_in_frames frames identifiers = + match frames with | [] -> Error.raise (Qualified_identifier.Unbound_qualified_identifier (Qualified_identifier.from_list1 identifiers)) - | scope :: scopes -> ( + | frame :: frames -> ( match - Binding_tree.maximum_lookup identifiers (get_scope_bindings scope) + Binding_tree.maximum_lookup identifiers (get_frame_bindings frame) with | Binding_tree.Bound { entry; subtree; _ } -> (entry, subtree) | Binding_tree.Partially_bound { leading_segments; segment; _ } -> @@ -316,11 +316,11 @@ module Printing_state = struct (Qualified_identifier.Unbound_namespace (Qualified_identifier.make ~namespaces:leading_segments segment)) - | Binding_tree.Unbound _ -> lookup_in_scopes scopes identifiers) + | Binding_tree.Unbound _ -> lookup_in_frames frames identifiers) let lookup state query = let identifiers = Qualified_identifier.to_list1 query in - try lookup_in_scopes (List1.to_list state.scopes) identifiers with + try lookup_in_frames (List1.to_list state.frames) identifiers with | exn -> Error.re_raise (Error.located_exception1 @@ -337,14 +337,14 @@ module Printing_state = struct let modify_operator state identifier f = let entry, subtree = lookup state identifier in let entry' = Entry.modify_operator f entry in - let bindings = get_current_scope_bindings state in + let bindings = get_current_frame_bindings state in if Binding_tree.mem identifier bindings then Binding_tree.replace identifier (fun _entry _subtree -> (entry', subtree)) bindings else Binding_tree.add identifier ~subtree entry' bindings; - match get_current_scope state with - | Module_scope { declarations; _ } -> + match get_current_frame state with + | Module_frame { declarations; _ } -> if Binding_tree.mem identifier declarations then Binding_tree.replace identifier (fun _entry subtree -> (entry', subtree)) @@ -405,7 +405,7 @@ module Printing_state = struct let open_namespace state identifier = let _entry, subtree = lookup state identifier in - let bindings = get_current_scope_bindings state in + let bindings = get_current_frame_bindings state in Binding_tree.add_all bindings subtree let open_module state identifier = open_namespace state identifier