/hole_reset.diff Secret
Created
March 31, 2021 21:27
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
diff --git a/src/core/holeId.ml b/src/core/holeId.ml | |
index c93ee7bb..54d087e1 100644 | |
--- a/src/core/holeId.ml | |
+++ b/src/core/holeId.ml | |
@@ -10,6 +10,8 @@ module Make (_ : UNIT) = struct | |
let x = !counter in | |
incr counter; | |
x | |
+ let reset () = | |
+ counter := 0 | |
end | |
let string_of_hole_id = string_of_int | |
diff --git a/src/core/holeId.mli b/src/core/holeId.mli | |
index fb966d0f..ef3b216a 100644 | |
--- a/src/core/holeId.mli | |
+++ b/src/core/holeId.mli | |
@@ -18,6 +18,7 @@ val string_of_hole_id : t -> string | |
module Make (_ : UNIT) : sig | |
(** Generates the next hole ID. *) | |
val next : unit -> t | |
+ val reset : unit -> unit | |
end | |
(** Converts an option type to a name. *) | |
diff --git a/src/core/holes.ml b/src/core/holes.ml | |
index 6df4d36e..5fc43053 100644 | |
--- a/src/core/holes.ml | |
+++ b/src/core/holes.ml | |
@@ -229,9 +229,14 @@ let add_harpoon_subgoal = DynArray.add harpoon_subgoals | |
let get_harpoon_subgoals () = DynArray.to_list harpoon_subgoals | |
+(* instantiate a counter for hole IDs; | |
+ this module is kept private to Holes *) | |
+module ID = HoleId.Make (Module.Unit) | |
+ | |
let clear () = | |
Hashtbl.clear holes; | |
- DynArray.clear harpoon_subgoals | |
+ DynArray.clear harpoon_subgoals; | |
+ ID.reset () | |
let list () = | |
let f k h l = (k, h) :: l in | |
@@ -249,10 +254,6 @@ let unsafe_parse_lookup_strategy loc (s : string) : lookup_strategy = | |
| Some s -> s | |
| None -> throw loc (InvalidHoleIdentifier s) | |
-(* instantiate a counter for hole IDs; | |
- this module is kept private to Holes *) | |
-module ID = HoleId.Make (Module.Unit) | |
- | |
let allocate () = ID.next () | |
let assign id h = | |
match Hashtbl.find_opt holes id with |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment