From 38a45e85483b476a83a601d28096c45dc2366bb7 Mon Sep 17 00:00:00 2001 From: Marc-Antoine Ouimet Date: Wed, 20 Dec 2023 22:33:02 -0500 Subject: [PATCH] Rename "scope" operations to "frame" operations A frame is a lexical region of an AST wherein variable declarations and references can be made. A scope is a frame in which name resolution is uniform, meaning that references are resolved to the same declaration site irrespective of the AST node in the scope. The current implementation for name resolution uses frames, not scopes. --- src/core/index.ml | 4 +- src/core/index_state.ml | 452 +++++++++++++------------ src/core/index_state.mli | 13 +- src/core/recsgn.ml | 25 +- src/core/recsgn_state.ml | 6 +- src/html/synext_html_pp_state.ml | 72 ++-- src/parser/disambiguation_state.ml | 415 ++++++++++++----------- src/parser/disambiguation_state.mli | 10 +- src/parser/harpoon_disambiguation.ml | 2 +- src/parser/signature_disambiguation.ml | 2 +- src/syntax/synext/synext_pp_state.ml | 68 ++-- 11 files changed, 550 insertions(+), 519 deletions(-) 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