-let destroy_nat annterm =
- let is_zero = function
- | Cic.AMutConstruct (_, uri, 0, 1, _) when Obj.is_nat_URI uri -> true
- | _ -> false
- in
- let is_succ = function
- | Cic.AMutConstruct (_, uri, 0, 2, _) when Obj.is_nat_URI uri -> true
- | _ -> false
- in
- let rec aux acc = function
- | Cic.AAppl (_, [he ; tl]) when is_succ he -> aux (acc + 1) tl
- | t when is_zero t -> Some acc
- | _ -> None in
- aux 0 annterm
-
- (* persistent state *)
-
-let initial_level2_patterns32 () = Hashtbl.create 211
-let initial_interpretations () = Hashtbl.create 211
-
-let level2_patterns32 = ref (initial_level2_patterns32 ())
-(* symb -> id list ref *)
-let interpretations = ref (initial_interpretations ())
-let pattern32_matrix = ref []
-let counter = ref ~-1
-let find_level2_patterns32 pid = Hashtbl.find !level2_patterns32 pid;;
-
-let stack = ref []
-
-let push () =
- stack := (!counter,!level2_patterns32,!interpretations,!pattern32_matrix)::!stack;
- counter := ~-1;
- level2_patterns32 := initial_level2_patterns32 ();
- interpretations := initial_interpretations ();
- pattern32_matrix := []
-;;
-
-let pop () =
- match !stack with
- [] -> assert false
- | (ocounter,olevel2_patterns32,ointerpretations,opattern32_matrix)::old ->
- stack := old;
- counter := ocounter;
- level2_patterns32 := olevel2_patterns32;
- interpretations := ointerpretations;
- pattern32_matrix := opattern32_matrix
-;;
+module IntMap = Map.Make(struct type t = int let compare = compare end);;
+module StringMap = Map.Make(String);;
+
+type db = {
+ counter: int;
+ pattern32_matrix: (bool * NotationPt.cic_appl_pattern * interpretation_id) list;
+ level2_patterns32:
+ (string * string * NotationPt.argument_pattern list *
+ NotationPt.cic_appl_pattern) IntMap.t;
+ interpretations: interpretation_id list StringMap.t; (* symb -> id list *)
+}
+
+let initial_db = {
+ counter = -1;
+ pattern32_matrix = [];
+ level2_patterns32 = IntMap.empty;
+ interpretations = StringMap.empty
+}
+
+class type g_status =
+ object
+ method interp_db: db
+ end
+
+class status =
+ object
+ val interp_db = initial_db
+ method interp_db = interp_db
+ method set_interp_db v = {< interp_db = v >}
+ method set_interp_status
+ : 'status. #g_status as 'status -> 'self
+ = fun o -> {< interp_db = o#interp_db >}
+ end
+
+let find_level2_patterns32 status pid =
+ IntMap.find pid status#interp_db.level2_patterns32