(* persistent state *)
-let level2_patterns32 = Hashtbl.create 211
-let interpretations = Hashtbl.create 211 (* symb -> id list ref *)
+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 compiled32 = ref None
let pattern32_matrix = ref []
+let counter = ref ~-1
+
+let stack = ref []
+
+let push () =
+ stack := (!counter,!level2_patterns32,!interpretations,!compiled32,!pattern32_matrix)::!stack;
+ counter := ~-1;
+ level2_patterns32 := initial_level2_patterns32 ();
+ interpretations := initial_interpretations ();
+ compiled32 := None;
+ pattern32_matrix := []
+;;
+
+let pop () =
+ match !stack with
+ [] -> assert false
+ | (ocounter,olevel2_patterns32,ointerpretations,ocompiled32,opattern32_matrix)::old ->
+ stack := old;
+ counter := ocounter;
+ level2_patterns32 := olevel2_patterns32;
+ interpretations := ointerpretations;
+ compiled32 := ocompiled32;
+ pattern32_matrix := opattern32_matrix
+;;
let get_compiled32 () =
match !compiled32 with
in
let _, symbol, args, _ =
try
- Hashtbl.find level2_patterns32 pid
+ Hashtbl.find !level2_patterns32 pid
with Not_found -> assert false
in
let ast = instantiate32 term_info idrefs env' symbol args in
debug_print (lazy ("ast_of_acic -> " ^ CicNotationPp.pp_term ast));
ast, term_info.uri
-let counter = ref ~-1
-let reset () =
- counter := ~-1;
- Hashtbl.clear level2_patterns32;
- Hashtbl.clear interpretations
-;;
let fresh_id =
fun () ->
incr counter;
let add_interpretation dsc (symbol, args) appl_pattern =
let id = fresh_id () in
- Hashtbl.add level2_patterns32 id (dsc, symbol, args, appl_pattern);
+ Hashtbl.add !level2_patterns32 id (dsc, symbol, args, appl_pattern);
pattern32_matrix := (true, appl_pattern, id) :: !pattern32_matrix;
load_patterns32 !pattern32_matrix;
(try
- let ids = Hashtbl.find interpretations symbol in
+ let ids = Hashtbl.find !interpretations symbol in
ids := id :: !ids
- with Not_found -> Hashtbl.add interpretations symbol (ref [id]));
+ with Not_found -> Hashtbl.add !interpretations symbol (ref [id]));
id
let get_all_interpretations () =
(function (_, _, id) ->
let (dsc, _, _, _) =
try
- Hashtbl.find level2_patterns32 id
+ Hashtbl.find !level2_patterns32 id
with Not_found -> assert false
in
(id, dsc))
(fun id ->
let (dsc, _, args, appl_pattern) =
try
- Hashtbl.find level2_patterns32 id
+ Hashtbl.find !level2_patterns32 id
with Not_found -> assert false
in
dsc, args, appl_pattern)
- !(Hashtbl.find interpretations symbol)))
+ !(Hashtbl.find !interpretations symbol)))
with Not_found -> raise Interpretation_not_found
let remove_interpretation id =
(try
- let dsc, symbol, _, _ = Hashtbl.find level2_patterns32 id in
- let ids = Hashtbl.find interpretations symbol in
+ let dsc, symbol, _, _ = Hashtbl.find !level2_patterns32 id in
+ let ids = Hashtbl.find !interpretations symbol in
ids := List.filter ((<>) id) !ids;
- Hashtbl.remove level2_patterns32 id;
+ Hashtbl.remove !level2_patterns32 id;
with Not_found -> raise Interpretation_not_found);
pattern32_matrix :=
List.filter (fun (_, _, id') -> id <> id') !pattern32_matrix;
(string * Cic.term) list -> CicNotationPt.cic_appl_pattern ->
Cic.term
-(* hack. seee cicNotation for explanation *)
-val reset: unit -> unit
+val push: unit -> unit
+val pop: unit -> unit
aux (x,y)
(* mapping: rule_id -> owned keywords. (rule_id, string list) Hashtbl.t *)
-let owned_keywords = Hashtbl.create 23
+let initial_owned_keywords () = Hashtbl.create 23
+
+let owned_keywords = ref (initial_owned_keywords ())
+
+let history = ref [];;
+
+let push () =
+ history := !owned_keywords :: !history;
+ owned_keywords := (initial_owned_keywords ())
+;;
+
+let pop () =
+ match !history with
+ | [] -> assert false
+ | hd :: old_history ->
+ owned_keywords := hd;
+ history := old_history
+;;
type checked_l1_pattern = CL1P of CicNotationPt.term * int
let keywords = CicNotationUtil.keywords_of_term level1_pattern in
let rule_id = p_atoms in
List.iter CicNotationLexer.add_level2_ast_keyword keywords;
- Hashtbl.add owned_keywords rule_id keywords; (* keywords may be [] *)
+ Hashtbl.add !owned_keywords rule_id keywords; (* keywords may be [] *)
rule_id
let delete rule_id =
let atoms = rule_id in
(try
- let keywords = Hashtbl.find owned_keywords rule_id in
+ let keywords = Hashtbl.find !owned_keywords rule_id in
List.iter CicNotationLexer.remove_level2_ast_keyword keywords
with Not_found -> assert false);
Grammar.delete_rule term atoms
(** print "level2_pattern" entry on stdout, flushing afterwards *)
val print_l2_pattern: unit -> unit
+val push: unit -> unit
+val pop: unit -> unit
(* persistent state *)
-let level1_patterns21 = Hashtbl.create 211
-
+let initial_level1_patterns21 () = Hashtbl.create 211
+let level1_patterns21 = ref (initial_level1_patterns21 ())
let compiled21 = ref None
-
let pattern21_matrix = ref []
+let counter = ref ~-1
+
+let stack = ref [];;
+
+let push () =
+ stack := (!counter,!level1_patterns21,!compiled21,!pattern21_matrix)::!stack;
+ counter := ~-1;
+ level1_patterns21 := initial_level1_patterns21 ();
+ compiled21 := None;
+ pattern21_matrix := []
+;;
+
+let pop () =
+ match !stack with
+ [] -> assert false
+ | (ocounter,olevel1_patterns21,ocompiled21,opatterns21_matrix)::old ->
+ stack := old;
+ counter := ocounter;
+ level1_patterns21 := olevel1_patterns21;
+ compiled21 := ocompiled21;
+ pattern21_matrix := opatterns21_matrix
+;;
let get_compiled21 () =
match !compiled21 with
in
let l1 =
try
- Hashtbl.find level1_patterns21 pid
+ Hashtbl.find !level1_patterns21 pid
with Not_found -> assert false
in
instantiate21 idrefs (ast_env_of_env env) l1)
in
aux true l1_pattern *)
-let counter = ref ~-1
-let reset () =
- counter := ~-1;
- Hashtbl.clear level1_patterns21
-;;
let fresh_id =
fun () ->
incr counter;
let id = fresh_id () in
let l1' = add_level_info precedence (fill_pos_info l1) in
let l2' = CicNotationUtil.strip_attributes l2 in
- Hashtbl.add level1_patterns21 id l1';
+ Hashtbl.add !level1_patterns21 id l1';
pattern21_matrix := (l2', id) :: !pattern21_matrix;
load_patterns21 !pattern21_matrix;
id
let remove_pretty_printer id =
(try
- Hashtbl.remove level1_patterns21 id;
+ Hashtbl.remove !level1_patterns21 id;
with Not_found -> raise Pretty_printer_not_found);
pattern21_matrix := List.filter (fun (_, id') -> id <> id') !pattern21_matrix;
load_patterns21 !pattern21_matrix
CicNotationEnv.t -> CicNotationPt.term ->
CicNotationPt.term
-(* hack. seee cicNotation for explanation *)
-val reset: unit -> unit
+val push: unit -> unit
+val pop: unit -> unit
in
TermAcicContent.set_active_interpretations interp_ids
-let reset () =
- TermContentPres.reset ();
- TermAcicContent.reset ()
+let push () =
+ TermContentPres.push ();
+ TermAcicContent.push ();
+ CicNotationParser.push ()
+;;
+
+let pop () =
+ TermContentPres.pop ();
+ TermAcicContent.pop ();
+ CicNotationParser.pop ()
;;
val get_active_notations: unit -> notation_id list
val set_active_notations: notation_id list -> unit
-(* resets internal couenters. this is an hack used in matitaScript.
- * if you are in the middle of a script (with an history you may use to undo
- * with some notations id inside) and you want to compile an external file
- * in an empty environment you need, after its compilation, to restore
- * the previous environment (re-executing all notations commands) and this must
- * produce the same ids as before, otherwise history is wrong. *)
- val reset: unit -> unit
+val push: unit -> unit
+val pop: unit -> unit
in
List.iter CicNotation.remove_notation notation_to_remove
+let push () = CicNotation.push ();;
+let pop () = CicNotation.pop ();;
from:LexiconEngine.status -> LexiconEngine.status ->
(DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list
+val push: unit -> unit
+val pop: unit -> unit
HLog.error "please create it.";
raise (Failure ("No root file for "^mafilename))
in
- let initial_lexicon_status =
- CicNotation2.load_notation ~include_paths:[] BuildTimeConf.core_notation_script
- in
- let b,x =
+ let b =
try
GrafiteSync.push ();
- LexiconSync.time_travel ~present:x ~past:initial_lexicon_status;
+ LexiconSync.push ();
let rc = MatitacLib.Make.make root [tgt] in
+ LexiconSync.pop ();
GrafiteSync.pop ();
- CicNotation.reset ();
- ignore(CicNotation2.load_notation ~include_paths:[]
- BuildTimeConf.core_notation_script);
- let x = List.fold_left (fun s c -> LexiconEngine.eval_command s c)
- initial_lexicon_status (List.rev
- x.LexiconEngine.lexicon_content_rev)
- in
- rc,x
+ rc
with
| exn ->
HLog.error ("Unexpected " ^ snd(MatitaExcPp.to_string exn));
projects / helm.git / commitdiff