diff options
Diffstat (limited to '')
-rw-r--r-- | src/Identifiers.ml | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/src/Identifiers.ml b/src/Identifiers.ml index 757c9df5..dfcbb631 100644 --- a/src/Identifiers.ml +++ b/src/Identifiers.ml @@ -16,8 +16,12 @@ module type Id = sig val generator_zero : generator + val generator_from_incr_id : id -> generator + val fresh_stateful_generator : unit -> generator ref * (unit -> id) + val incr : id -> id + (* TODO: this should be stateful! - but we may want to be able to duplicate contexts... Maybe we could have a `fresh` and a `global_fresh` @@ -35,6 +39,10 @@ module type Id = sig val compare_id : id -> id -> int + val max : id -> id -> id + + val min : id -> id -> id + val pp_generator : Format.formatter -> generator -> unit val show_generator : generator -> string @@ -91,6 +99,10 @@ module IdGen () : Id = struct * they happen *) if x == max_int then raise (Errors.IntegerOverflow ()) else x + 1 + let generator_from_incr_id id = + let id = incr id in + id + let fresh_stateful_generator () = let g = ref 0 in let fresh () = @@ -116,6 +128,10 @@ module IdGen () : Id = struct let compare_id = compare + let max id0 id1 = if id0 > id1 then id0 else id1 + + let min id0 id1 = if id0 < id1 then id0 else id1 + let nth v id = List.nth v id let nth_opt v id = List.nth_opt v id |