diff options
| -rw-r--r-- | src/Identifiers.ml | 9 | ||||
| -rw-r--r-- | src/Interpreter.ml | 20 |
2 files changed, 28 insertions, 1 deletions
diff --git a/src/Identifiers.ml b/src/Identifiers.ml index 21898498..cab1bafa 100644 --- a/src/Identifiers.ml +++ b/src/Identifiers.ml @@ -9,11 +9,14 @@ open Errors module type Id = sig type id + type generator + (** Id generator - simply a counter *) + type 'a vector val zero : id - val incr : id -> id + val fresh : generator -> id * generator val to_string : id -> string @@ -53,6 +56,8 @@ module IdGen () : Id = struct (* TODO: use Int64.t *) type id = int + type generator = id + type 'a vector = 'a list let zero = 0 @@ -63,6 +68,8 @@ module IdGen () : Id = struct * they happen *) if x == max_int then raise (Errors.IntegerOverflow ()) else x + 1 + let fresh gen = (gen, incr gen) + let to_string = string_of_int let empty_vector = [] diff --git a/src/Interpreter.ml b/src/Interpreter.ml index b8943a9a..3b16a1e3 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -1,6 +1,7 @@ open Types open Values open Expressions +open CfimAst open Print.Values open Errors @@ -28,6 +29,25 @@ 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 } +(** A function frame + + When using the interpreter in concrete mode (i.e, non symbolic) we + push a function frame whenever we enter a function body (and pop it + upon leaving it). + *) + +type eval_ctx = { + type_context : type_def TypeDefId.vector; + fun_context : fun_def FunDefId.vector; + type_vars : type_var TypeVarId.vector; + frames : stack_frame list; + env : env; + symbolic_counter : SymbolicValueId.generator; + borrows_counter : BorrowId.generator; +} +(** Evaluation context *) + (** The following type identifies the relative position of expressions (in particular borrows) in other expressions. |