summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2021-11-22 10:43:38 +0100
committerSon Ho2021-11-22 10:44:13 +0100
commitb57a3a0d60fe7d6bdada644724f679bde88ad728 (patch)
tree323421580c61cecad4c3468d49be6adb9184cbec /src
parent3d47e1943547780aed2f86736bfaef31c6431ce0 (diff)
Implement end_borrow_get_borrow_in_env
Diffstat (limited to 'src')
-rw-r--r--src/Interpreter.ml27
-rw-r--r--src/Print.ml2
-rw-r--r--src/main.ml4
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