Implement formatting for eval_ctx

1 files changed, 27 insertions, 15 deletions

diff --git a/src/Contexts.ml b/src/Contexts.ml
index be8e56fa..88af46d4 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -2,25 +2,12 @@ open Types
 open Values
 open Expressions
 open CfimAst
-open Print.Values
 open Errors
 
 type env_value = Var of VarId.id * typed_value | Abs of abs
 
 type env = env_value list
 
-let env_value_to_string (fmt : value_formatter) (ev : env_value) : string =
-  match ev with
-  | Var (vid, tv) ->
-      var_id_to_string vid ^ " -> " ^ typed_value_to_string fmt tv
-  | Abs abs -> abs_to_string fmt abs
-
-let env_to_string (fmt : value_formatter) (env : env) : string =
-  "{\n"
-  ^ String.concat ";\n"
-      (List.map (fun ev -> "  " ^ env_value_to_string fmt ev) env)
-  ^ "\n}"
-
 type 'a eval_result = Stuck | Panic | Res of 'a
 
 type interpreter_mode = ConcreteMode | SymbolicMode
@@ -29,7 +16,7 @@ type config = { mode : interpreter_mode; check_invariants : bool }
 
 type outer_borrows = Borrows of BorrowId.Set.t | Borrow of BorrowId.id
 
-type stack_frame = { vars : var VarId.vector }
+type stack_frame = { vars : VarId.id list }
 (** A function frame
 
     When using the interpreter in concrete mode (i.e, non symbolic) we
@@ -41,9 +28,34 @@ type eval_ctx = {
   type_context : type_def TypeDefId.vector;
   fun_context : fun_def FunDefId.vector;
   type_vars : type_var TypeVarId.vector;
+  vars : var VarId.Map.t;
   frames : stack_frame list;
   env : env;
   symbolic_counter : SymbolicValueId.generator;
-  borrows_counter : BorrowId.generator;
+  borrow_counter : BorrowId.generator;
 }
 (** Evaluation context *)
+
+let fresh_symbolic_value_id (ctx : eval_ctx) : SymbolicValueId.id * eval_ctx =
+  let id, counter' = SymbolicValueId.fresh ctx.symbolic_counter in
+  (id, { ctx with symbolic_counter = counter' })
+
+let fresh_borrow_id (ctx : eval_ctx) : BorrowId.id * eval_ctx =
+  let id, counter' = BorrowId.fresh ctx.borrow_counter in
+  (id, { ctx with borrow_counter = counter' })
+
+let lookup_type_var (ctx : eval_ctx) (vid : TypeVarId.id) : type_var =
+  TypeVarId.nth ctx.type_vars vid
+
+let lookup_var (ctx : eval_ctx) (vid : VarId.id) : var =
+  VarId.Map.find vid ctx.vars
+
+let lookup_var_value (ctx : eval_ctx) (vid : VarId.id) : typed_value =
+  let check_ev (ev : env_value) : typed_value option =
+    match ev with
+    | Var (vid', v) -> if vid' = vid then Some v else None
+    | Abs _ -> None
+  in
+  match List.find_map check_ev ctx.env with
+  | None -> failwith "Unreachable"
+  | Some v -> v