summaryrefslogtreecommitdiff
path: root/src/Identifiers.ml
diff options
context:
space:
mode:
authorSon Ho2021-11-23 13:09:36 +0100
committerSon Ho2021-11-23 13:09:36 +0100
commit932780e18f311c1776ef4e45c41f4e13c1092138 (patch)
treef31468237c1024e9f5863fcb83756ad0accf9711 /src/Identifiers.ml
parentb5571409847c1d910c90ff7d2aca1d691f85c028 (diff)
Define evaluation contexts
Diffstat (limited to 'src/Identifiers.ml')
-rw-r--r--src/Identifiers.ml9
1 files changed, 8 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 = []