Use a list for newly_defined constants

Gbury · Jun 20, 2023 · 5780a85 · 5780a85
1 parent 38005d1
commit 5780a85
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 20 deletions.
diff --git a/src/model/loop.ml b/src/model/loop.ml
@@ -345,7 +345,7 @@ module Make
               Dolmen.Std.Loc.fmt_compact (Dolmen.Std.Loc.full_loc loc)
               Dolmen.Std.Expr.Term.Const.print cst
               Value.print value;
-          let newly_defined = Model.C.add cst value newly_defined in
+          let newly_defined = cst :: newly_defined in
           let model = Model.Cst.add cst value model in
           (st, model, newly_defined)
         | `Instanceof (_id, cst, ty_args, ty_params, term_params, body) ->
@@ -357,7 +357,7 @@ module Make
               Dolmen.Std.Expr.Term.Const.print cst
               (Format.pp_print_list ~pp_sep Dolmen.Std.Expr.Ty.print) ty_args
               Dolmen.Std.Expr.Term.print (Dolmen.Std.Expr.Term.lam ([], term_params) body);
-          let newly_defined = Model.C.add cst Value.dummy newly_defined in
+          let newly_defined = cst :: newly_defined in
           let model = Fun.add_ad_hoc_instance model ~cst ~ty_args ~term_params ~body in
           if State.get State.debug st then
             Format.eprintf "[model][typed] %a@." Model.print model;
@@ -410,7 +410,7 @@ module Make
     let input = `Response file in
     (* let st = Typer.push ~input st 1 in *)
     let st, model, newly_defined, parsed =
-      type_model_defined ~input ?attrs st model Model.C.empty parsed
+      type_model_defined ~input ?attrs st model [] parsed
     in
     (* let st = Typer.pop st ~input 1 in *)
     st, model, newly_defined, parsed
@@ -500,22 +500,21 @@ module Make
 
   and eval_newly_defined st model delayed evaluated_goals newly_defined =
     let newly_defined_and_needed =
-      Model.C.merge (fun _cst value_opt acc_opt ->
-          match value_opt, acc_opt with
-            | Some _, (Some _ as res) -> res
-            | None as res, _
-            | Some _, (None as res) -> res
-        ) newly_defined delayed
+      List.filter_map (fun cst ->
+          match Model.C.find_opt cst delayed with
+          | Some acc -> Some (cst, acc)
+          | None -> None
+        ) newly_defined
     in
     eval_delayed st model delayed evaluated_goals newly_defined_and_needed
 
   and eval_delayed st model delayed evaluated_goals to_eval =
-    Model.C.fold (fun cst acc_list (st, model, delayed, evaluated_goals) ->
+    List.fold_left (fun (st, model, delayed, evaluated_goals) (cst, acc_list) ->
         let delayed = Model.C.remove cst delayed in
         List.fold_left (fun (st, model, delayed, evaluated_goals) acc ->
             eval_acc st model delayed evaluated_goals acc
           ) (st, model, delayed, evaluated_goals) acc_list
-      ) to_eval (st, model, delayed, evaluated_goals)
+      ) (st, model, delayed, evaluated_goals) to_eval
 
   and eval_acc_direct ~reraise st model delayed evaluated_goals = function
     | Def def ->
@@ -578,9 +577,9 @@ module Make
               Value.print value
           end;
           let model = Model.Cst.add cst value model in
-          let newly_defined = Model.C.add cst value newly_defined in
+          let newly_defined = cst :: newly_defined in
           model, newly_defined
-        ) (model, Model.C.empty) defs
+        ) (model, []) defs
     in
     let st, model, delayed, evaluated_goals =
       eval_newly_defined st model delayed evaluated_goals newly_defined

diff --git a/src/model/model.ml b/src/model/model.ml
@@ -27,9 +27,6 @@ type t = {
 let empty =
   { vars = V.empty; csts = C.empty; }
 
-let vars { vars; _ } = vars
-let csts { csts; _ } = csts
-
 let print fmt model =
   Format.fprintf fmt "@[<hv>@[<hv 2>{";
   V.iter (fun var value ->

diff --git a/src/model/model.mli b/src/model/model.mli
@@ -25,10 +25,6 @@ val empty : t
 val print : Format.formatter -> t -> unit
 (** Print function *)
 
-val vars : t -> Value.t V.t
-
-val csts : t -> Value.t C.t
-
 val disjoint_union : t -> t -> t
 (** Disjoint union *)