summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/Identifiers.ml9
-rw-r--r--src/Interpreter.ml20
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.