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

@@ -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')
 

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.

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;

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 } ->

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,43 +486,43 @@ 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);
         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; _ } ->
             Error.raise
               (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