Rename unify to matching, convert state types to records (#277)

* Rename unification to matching

* Rename unification to matching in extension

* Convert SState.t to a record

* Convert BiState.t to a record

Gillian-JS/lib/Semantics/JSILSMemory.ml

@@ -528,7 +528,7 @@ module M = struct
     Ok [ (heap, [], [], []) ]
 
   let execute_action
-      ?unification:_
+      ?matching:_
       (action : string)
       (heap : t)
       (pfs : PFS.t)

GillianCore/BulkTesting/Runner.ml

@@ -124,8 +124,8 @@ module Make (Backend : functor (Outcome : Outcome.S) (Suite : Suite.S) ->
             in
             let prog = Gil_parsing.eprog_to_prog ~other_imports e_prog in
             if should_execute prog filename prev_results_opt then
-              match UP.init_prog prog with
-              | Error _ -> failwith "Failed to create unification plans"
+              match MP.init_prog prog with
+              | Error _ -> failwith "Failed to create matching plans"
               | Ok prog ->
                   let () = before_execution () in
                   let ret =

GillianCore/GIL_Syntax/Expr.ml

@@ -493,9 +493,9 @@ let var_to_expr (x : string) : t =
   if Names.is_lvar_name x then LVar x
   else if is_aloc_name x then ALoc x
   else if is_pvar_name x then PVar x
-  else raise (Failure ("var_to_expr: Impossible unifiable: " ^ x))
+  else raise (Failure ("var_to_expr: Impossible matchable: " ^ x))
 
-let is_unifiable (e : t) : bool =
+let is_matchable (e : t) : bool =
   match e with
   | PVar _ | LVar _ | ALoc _ | UnOp (LstLen, PVar _) | UnOp (LstLen, LVar _) ->
       true

GillianCore/GIL_Syntax/Gil_syntax.mli

@@ -401,8 +401,8 @@ module Expr : sig
   (** [var_to_expr x] returns the expression representing the program/logical variable or abstract location [x] *)
   val var_to_expr : string -> t
 
-  (** [is_unifiable x] returns whether or not the expression [e] is unifiable *)
-  val is_unifiable : t -> bool
+  (** [is_matchable x] returns whether or not the expression [e] is matchable *)
+  val is_matchable : t -> bool
 
   (** Sub-expression check *)
   val sub_expr : t -> t -> bool

GillianCore/command_line/act_console.ml

@@ -56,7 +56,7 @@ struct
       (labeled_prog, init_data, None)
 
   let emit_specs e_prog prog file =
-    let () = Prog.update_specs e_prog UP.(prog.prog) in
+    let () = Prog.update_specs e_prog MP.(prog.prog) in
     let fname = Filename.chop_extension (Filename.basename file) in
     let dirname = Filename.dirname file in
     let out_path = Filename.concat dirname (fname ^ "_bi.gil") in
@@ -115,8 +115,8 @@ struct
     let () = L.normal (fun m -> m "*** Stage 3: Symbolic Execution.@\n") in
     let () = Config.unfolding := false in
     let prog = LogicPreprocessing.preprocess prog true in
-    match UP.init_prog prog with
-    | Error _ -> failwith "Creation of unification plans failed."
+    match MP.init_prog prog with
+    | Error _ -> failwith "Creation of matching plans failed."
     | Ok prog' ->
         let () =
           Abductor.test_prog ~init_data ~call_graph prog' incremental

GillianCore/command_line/c_interpreter_console.ml

@@ -27,7 +27,7 @@ struct
 
   let run debug (prog : ('a, int) Prog.t) init_data : unit =
     let prog =
-      match UP.init_prog prog with
+      match MP.init_prog prog with
       | Ok prog -> prog
       | _ -> failwith "Program could not be initialised"
     in

GillianCore/command_line/s_interpreter_console.ml

@@ -63,7 +63,7 @@ struct
       let prev_source_files, prev_call_graph = read_symbolic_results () in
       let proc_changes =
         get_sym_changes
-          UP.(prog.prog)
+          MP.(prog.prog)
           ~prev_source_files ~prev_call_graph ~cur_source_files
       in
       let changed_procs =
@@ -87,7 +87,7 @@ struct
       let call_graph = S_interpreter.call_graph in
       write_symbolic_results cur_source_files call_graph ~diff:""
 
-    let f (prog : PC.Annot.t UP.prog) init_data incremental source_files =
+    let f (prog : PC.Annot.t MP.prog) init_data incremental source_files =
       if incremental && prev_results_exist () then
         run_incr source_files prog init_data
       else rerun_all source_files prog init_data
@@ -149,8 +149,8 @@ struct
       L.normal (fun m -> m "\n*** Stage 2: DONE transforming the program.\n")
     in
     let () = L.normal (fun m -> m "*** Stage 3: Symbolic Execution.\n") in
-    match UP.init_prog prog with
-    | Error _ -> failwith "Creation of unification plans failed"
+    match MP.init_prog prog with
+    | Error _ -> failwith "Creation of matching plans failed"
     | Ok prog' -> run prog' init_data incremental source_files_opt
 
   let wpst

GillianCore/debugging/adapter/debug_protocol_ext.ml

@@ -79,17 +79,17 @@ module Custom_commands (Debugger : Debugger.S) = struct
     end
   end
 
-  module Unification_command = struct
-    let type_ = "unification"
+  module Matching_command = struct
+    let type_ = "matching"
 
     module Arguments = struct
       type t = { id : L.Report_id.t } [@@deriving yojson]
     end
 
     module Result = struct
       type t = {
-        unify_id : L.Report_id.t; [@key "unifyId"]
-        unify_map : Unify_map.t; [@key "unifyMap"]
+        match_id : L.Report_id.t; [@key "matchId"]
+        match_map : Match_map.t; [@key "matchMap"]
       }
       [@@deriving yojson, make]
     end

GillianCore/debugging/adapter/inspect.ml

@@ -70,11 +70,11 @@ module Make (Debugger : Debugger.S) = struct
     DL.set_rpc_command_handler rpc ~name:"Debugger state"
       (module Debugger_state_command)
       (fun _ -> Lwt.return (Debugger.Inspect.get_debug_state dbg));
-    DL.set_rpc_command_handler rpc ~name:"Unification"
-      (module Unification_command)
+    DL.set_rpc_command_handler rpc ~name:"Matching"
+      (module Matching_command)
       (fun { id } ->
-        let unify_map = dbg |> Debugger.Inspect.get_unify_map id in
-        let result = Unification_command.Result.make ~unify_id:id ~unify_map in
+        let match_map = dbg |> Debugger.Inspect.get_match_map id in
+        let result = Matching_command.Result.make ~match_id:id ~match_map in
         Lwt.return result);
     Lwt.return ()
 end

GillianCore/debugging/debugger/base_debugger.ml

@@ -82,28 +82,28 @@ struct
     val launch_proc :
       proc_name:string -> debug_state_ext base_debug_state -> result_t cont_func
 
-    module Unify : sig
-      val unify_final_cmd :
+    module Match : sig
+      val match_final_cmd :
         L.Report_id.t ->
         proc_name:string ->
         (state_t, state_vt, err_t) Exec_res.t ->
         debug_state_ext base_debug_state ->
-        Exec_map.unification list
+        Exec_map.matching list
 
-      val get_unifys :
+      val get_matches :
         L.Report_id.t ->
         debug_state_ext base_debug_state ->
         proc_state_ext base_proc_state ->
-        Exec_map.unification list
+        Exec_map.matching list
 
-      val get_unify_map :
-        L.Report_id.t -> debug_state_ext base_debug_state -> Unify_map.t
+      val get_match_map :
+        L.Report_id.t -> debug_state_ext base_debug_state -> Match_map.t
     end
   end
 
   module Make (Debugger_impl : Debugger_impl) = struct
     open Debugger_impl
-    open Debugger_impl.Unify
+    open Debugger_impl.Match
 
     type nonrec breakpoints = breakpoints
     type nonrec tl_ast = tl_ast
@@ -150,7 +150,7 @@ struct
         exec_map : Exec_map.Packaged.t; [@key "execMap"]
         lifted_exec_map : Exec_map.Packaged.t option; [@key "liftedExecMap"]
         current_cmd_id : L.Report_id.t; [@key "currentCmdId"]
-        unifys : Exec_map.unification list;
+        matches : Exec_map.matching list;
         proc_name : string; [@key "procName"]
       }
       [@@deriving yojson]
@@ -185,15 +185,21 @@ struct
           Hashtbl.fold
             (fun proc_name state acc ->
               let current_cmd_id = state.cur_report_id in
-              let unifys =
-                state.lifter_state |> Lifter.get_unifys_at_id current_cmd_id
+              let matches =
+                state.lifter_state |> Lifter.get_matches_at_id current_cmd_id
               in
               let exec_map = state.lifter_state |> Lifter.get_gil_map in
               let lifted_exec_map =
                 state.lifter_state |> Lifter.get_lifted_map
               in
               let proc =
-                { exec_map; lifted_exec_map; current_cmd_id; unifys; proc_name }
+                {
+                  exec_map;
+                  lifted_exec_map;
+                  current_cmd_id;
+                  matches;
+                  proc_name;
+                }
               in
               (proc_name, proc) :: acc)
             procs []
@@ -205,7 +211,7 @@ struct
           procs;
         }
 
-      let get_unify_map id { debug_state; _ } = get_unify_map id debug_state
+      let get_match_map id { debug_state; _ } = get_match_map id debug_state
     end
 
     let top_level_scopes : Variable.scope list =
@@ -460,9 +466,9 @@ struct
       let cmd = content |> of_yojson_string Logging.ConfigReport.of_yojson in
       let proc_name = (List.hd cmd.callstack).pid in
       let errors = show_result_errors result in
-      let unifys = unify_final_cmd prev_id ~proc_name result debug_state in
+      let matches = match_final_cmd prev_id ~proc_name result debug_state in
       let exec_data =
-        Lift.make_executed_cmd_data Exec_map.Final prev_id cmd ~unifys ~errors
+        Lift.make_executed_cmd_data Exec_map.Final prev_id cmd ~matches ~errors
           branch_path
       in
       (exec_data, cmd)
@@ -567,10 +573,12 @@ struct
                  update_proc_state cur_report_id debug_state proc_state;
                  let cmd = content |> of_yojson_string ConfigReport.of_yojson in
                  let cmd_kind = Exec_map.kind_of_cases new_branch_cases in
-                 let unifys = get_unifys cur_report_id debug_state proc_state in
+                 let matches =
+                   get_matches cur_report_id debug_state proc_state
+                 in
                  let exec_data =
                    Lift.make_executed_cmd_data cmd_kind cur_report_id cmd
-                     ~unifys branch_path
+                     ~matches branch_path
                  in
                  proc_state.lifter_state
                  |> Lifter.handle_cmd prev_id_in_frame branch_case exec_data

GillianCore/debugging/debugger/debugger_intf.ml

@@ -6,7 +6,7 @@ module type S = sig
     type debug_state_view [@@deriving yojson]
 
     val get_debug_state : t -> debug_state_view
-    val get_unify_map : Logging.Report_id.t -> t -> Unify_map.t
+    val get_match_map : Logging.Report_id.t -> t -> Match_map.t
   end
 
   val launch : string -> string option -> (t, string) result

GillianCore/debugging/debugger/symbolic_debugger.ml

@@ -25,21 +25,21 @@ struct
     let launch_proc ~proc_name (debug_state : debug_state_ext base_debug_state)
         =
       let prog =
-        match UP.init_prog debug_state.prog with
-        | Error _ -> failwith "Creation of unification plans failed"
+        match MP.init_prog debug_state.prog with
+        | Error _ -> failwith "Creation of matching plans failed"
         | Ok prog -> prog
       in
       Verification.SAInterpreter.init_evaluate_proc
         (fun x -> x)
         prog proc_name []
         (State.init debug_state.init_data)
 
-    module Unify = struct
-      let unify_final_cmd _ ~proc_name:_ _ _ = []
-      let get_unifys _ _ _ = []
+    module Match = struct
+      let match_final_cmd _ ~proc_name:_ _ _ = []
+      let get_matches _ _ _ = []
 
-      let get_unify_map _ _ =
-        failwith "Can't get unification in symbolic debugging!"
+      let get_match_map _ _ =
+        failwith "Can't get matching in symbolic debugging!"
     end
   end