From 2092bbef3ff70bc661dbc75bb9cbde9d15ce21eb Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 1 Sep 2022 22:32:52 -0400 Subject: [PATCH] feat(gensym): add reset --- src/core/gensym.ml | 2 ++ src/core/gensym.mli | 3 +++ 2 files changed, 5 insertions(+) diff --git a/src/core/gensym.ml b/src/core/gensym.ml index 09bc2f6e..b8d63461 100644 --- a/src/core/gensym.ml +++ b/src/core/gensym.ml @@ -43,6 +43,8 @@ let create tst : t = incr id_; { tst; self_id; fresh = 0 } +let reset self = self.fresh <- 0 + let fresh_term ?(opaque_to_cc = false) (self : t) ~pre (ty : ty) : Term.t = let id = self.fresh in self.fresh <- 1 + self.fresh; diff --git a/src/core/gensym.mli b/src/core/gensym.mli index 00fcd5a8..69684af0 100644 --- a/src/core/gensym.mli +++ b/src/core/gensym.mli @@ -17,3 +17,6 @@ val create : Term.store -> t val fresh_term : ?opaque_to_cc:bool -> t -> pre:string -> ty -> term (** Make a fresh term of the given type *) + +val reset : t -> unit +(** Reset to initial state *)