From b57a3a0d60fe7d6bdada644724f679bde88ad728 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 22 Nov 2021 10:43:38 +0100
Subject: Implement end_borrow_get_borrow_in_env

---
 src/Interpreter.ml | 27 ++++++++++++++++++++-------
 src/Print.ml       |  2 ++
 src/main.ml        |  4 +---
 3 files changed, 23 insertions(+), 10 deletions(-)

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index ca821f5b..62aef2a7 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -1,10 +1,23 @@
 open Types
 open Values
+open Print.Values
+open Errors
 
 type env_value = Var of string * 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 (vname, tv) -> vname ^ " -> " ^ 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 result = Stuck | Panic | Res of 'a
 
 type interpreter_mode = ConcreteMode | SymbolicMode
@@ -91,16 +104,16 @@ and end_borrow_get_borrow_in_values config l outer_borrows vl0 :
           (res, v' :: vl')
       | _ -> (res, v' :: vl))
 
-(*let rec end_borrow_get_borrow_in_env config l env0 : borrow_lres * env =
+let rec end_borrow_get_borrow_in_env config l env0 : borrow_lres * env =
   match env0 with
-  | [] -> NotFound
+  | [] -> (NotFound, [])
   | Var (x, v) :: env -> (
-      match end_borrow_get_borrow_in_value config None l v with
+      match end_borrow_get_borrow_in_value config l None v with
       | NotFound, v' ->
-          let res, env' = end_borrow_get_borrow_in_env config l env' in
-          (res, Var (x, v') :: env'')
-      | res, v' -> (res, Var (x, v') :: env'))
-  | Abs _ :: _ -> unimplemented __LOC__*)
+          let res, env' = end_borrow_get_borrow_in_env config l env in
+          (res, Var (x, v') :: env')
+      | res, v' -> (res, Var (x, v') :: env))
+  | Abs _ :: _ -> unimplemented __LOC__
 
 (*let rec end_borrow config (env0 : env) (env : env) (l : BorrowId.id) =
   match env with
diff --git a/src/Print.ml b/src/Print.ml
index 0240a307..874d19fb 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -26,7 +26,9 @@ module Types = struct
   (* TODO: This is probably not the most OCaml-like way of doing this *)
   type 'r type_formatter = {
     r_to_string : 'r -> string;
+    (* TODO: remove this and put the name everywhere instead? *)
     type_var_id_to_string : TypeVarId.id -> string;
+    (* TODO: remove this and put the name everywhere instead? *)
     type_def_id_to_string : TypeDefId.id -> string;
   }
 
diff --git a/src/main.ml b/src/main.ml
index 024209ff..a7388472 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -1,7 +1,5 @@
 open CfimOfJson
-
-(*open Interpreter*)
-open Print
+open Interpreter
 
 let () =
   let json = Yojson.Basic.from_file "../charon/charon/tests/test1.cfim" in
-- 
cgit v1.2.3