diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Interpreter.ml | 27 | ||||
| -rw-r--r-- | src/Print.ml | 2 | ||||
| -rw-r--r-- | 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 |