Predicates as a combinator, the final stretch

Gillian-C/bin/gillian_c.ml

@@ -1,13 +1,14 @@
 open Cgil_lib
-module SMemory = Gillian.Monadic.MonadicSMemory.Lift (MonadicSMemory)
 
 module Gil_to_c_lifter
     (Verification :
       Gillian.Abstraction.Verifier.S
         with type annot = CParserAndCompiler.Annot.t) =
 struct
   include
-    Gillian.Debugger.Lifter.Gil_lifter.Make (SMemory) (CParserAndCompiler)
+    Gillian.Debugger.Lifter.Gil_lifter.Make
+      (MonadicSMemory)
+      (CParserAndCompiler)
       (Verification)
 
   let get_variables =
@@ -16,7 +17,7 @@ struct
 end
 
 module CLI =
-  Gillian.Command_line.Make (Global_env) (CMemory) (SMemory)
+  Gillian.Command_line.Make (Global_env) (CMemory) (MonadicSMemory)
     (CParserAndCompiler)
     (External.M)
     (struct

Gillian-C/lib/MonadicSMemory.ml

@@ -404,7 +404,6 @@ let sure_is_nonempty state =
 
 let get_init_data { genv; _ } = genv
 let clear { genv; _ } = { genv; mem = just_functions genv }
-let copy h = h
 
 let pp_params fmt params =
   let rec aux fmtp = function
@@ -777,17 +776,14 @@ let execute_action ~action_name heap params =
 (* LActions static *)
 
 (* Serialization and operations *)
-let substitution_in_place subst heap =
+let substitution subst heap =
   let open Delayed.Syntax in
   let { mem; genv } = heap in
   let+ mem = Mem.substitution subst mem in
   match mem with
   | Ok mem -> { mem; genv }
   | Error e -> Fmt.failwith "Error in substitution: %a" SHeapTree.pp_err e
 
-let clean_up ?(keep = Expr.Set.empty) _ : Expr.Set.t * Expr.Set.t =
-  (Expr.Set.empty, keep)
-
 let lvars heap = Mem.lvars heap.mem
 let alocs heap = Mem.alocs heap.mem
 

Gillian-C/lib/sRunner.ml

@@ -1,5 +1,5 @@
 open Gillian
-module SMemory = Monadic.MonadicSMemory.Lift (MonadicSMemory)
+module SMemory = MonadicSMemory
 
 module Outcome =
   Bulk.Outcome.Make_Symbolic (SMemory) (CParserAndCompiler)

Gillian-C2/bin/gillian_c2.ml

@@ -4,12 +4,12 @@ module Init_data = Gillian.General.Init_data.Dummy
 
 module Gillian_C2_lifter =
   Gillian.Debugger.Lifter.Gil_fallback_lifter.Make
-    (SMemory)
+    (MonadicSMemory)
     (C2ParserAndCompiler)
     (Lifter.C2_lifter.Make)
 
 module CLI =
-  Gillian.Command_line.Make (Init_data) (CMemory) (SMemory)
+  Gillian.Command_line.Make (Init_data) (CMemory) (MonadicSMemory)
     (C2ParserAndCompiler)
     (External.M)
     (struct

Gillian-C2/lib/lifter/c2_lifter.ml

@@ -12,7 +12,7 @@ module Gil_branch_case = Gillian.Gil_syntax.Branch_case
 module DL = Gillian.Debugger.Logging
 module Exec_map = Gillian.Debugger.Utils.Exec_map
 module Annot = C2_annot
-module SMemory = Memory_model.SMemory
+module SMemory = Memory_model.MonadicSMemory
 open Annot
 open Branch_case
 

Gillian-C2/lib/memory_model/MonadicSMemory.ml

@@ -80,7 +80,6 @@ module Mem = struct
   let to_yojson map = SMap.to_yojson SHeapTree.to_yojson map
   let map_lift_err loc res = DR.map_error res (lift_sheaptree_err loc)
   let empty = SMap.empty
-  let copy x = x
 
   let get_tree_res map loc_name =
     DR.of_option ~none:(MissingLocResource loc_name)
@@ -430,7 +429,6 @@ let make_branch ~heap ?(rets = []) () = (heap, rets)
 
 let init () = { genv = GEnv.empty; mem = Mem.empty }
 let clear h = { h with mem = Mem.empty }
-let copy h = h
 
 let sure_is_nonempty _ =
   (* TODO: Implementing this would require filtering functions
@@ -911,7 +909,7 @@ let execute_action ~action_name heap params =
 (* Interface static *)
 
 (* Serialization and operations *)
-let substitution_in_place subst heap =
+let substitution subst heap =
   let open Delayed.Syntax in
   let { mem; genv } = heap in
   let genv = GEnv.substitution subst genv in
@@ -926,10 +924,6 @@ let substitution_in_place subst heap =
    heap := { mem = nmem; genv = ngenv } *)
 
 let fresh_val _ = Expr.LVar (LVar.alloc ())
-
-let clean_up ?(keep = Expr.Set.empty) _ : Expr.Set.t * Expr.Set.t =
-  (Expr.Set.empty, keep)
-
 let lvars heap = Mem.lvars heap.mem
 let alocs heap = Mem.alocs heap.mem
 

Gillian-JS/lib/Debugging/JSLifter.ml

@@ -67,7 +67,9 @@ struct
     node
 
   let add_memory_vars smemory get_new_scope_id (variables : Variable.ts) =
-    let sorted_locs_with_vals = Legacy_symbolic.sorted_locs_with_vals smemory in
+    let sorted_locs_with_vals =
+      Semantics.Symbolic.sorted_locs_with_vals smemory
+    in
     let value_nodes (loc, ((properties, domain), metadata)) : Variable.t =
       let () = ignore properties in
       let properties =
@@ -263,7 +265,7 @@ struct
       scopes
     else
       let sorted_locs_with_vals =
-        Legacy_symbolic.sorted_locs_with_vals memory
+        Semantics.Symbolic.sorted_locs_with_vals memory
       in
       let loc_to_scope_id = Hashtbl.create 0 in
       let () =