From eb9ca860db8cb06083765f7698179f16dee5303e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 26 Sep 2008 12:28:15 +0000 Subject: [PATCH] include statement better implemented: - push/pop operation for both Lexicon and Grafite stuff, instead of reset - this (if properly working) opens the doors to a completely functional matita status --- .../acic_content/termAcicContent.ml | 57 +++++++++++++------ .../acic_content/termAcicContent.mli | 4 +- .../content_pres/cicNotationParser.ml | 23 +++++++- .../content_pres/cicNotationParser.mli | 2 + .../content_pres/termContentPres.ml | 38 +++++++++---- .../content_pres/termContentPres.mli | 4 +- .../components/lexicon/cicNotation.ml | 13 ++++- .../components/lexicon/cicNotation.mli | 9 +-- .../components/lexicon/lexiconSync.ml | 2 + .../components/lexicon/lexiconSync.mli | 2 + helm/software/matita/matitaScript.ml | 17 ++---- 11 files changed, 112 insertions(+), 59 deletions(-) diff --git a/helm/software/components/acic_content/termAcicContent.ml b/helm/software/components/acic_content/termAcicContent.ml index edb22c944..470ab6b3f 100644 --- a/helm/software/components/acic_content/termAcicContent.ml +++ b/helm/software/components/acic_content/termAcicContent.ml @@ -281,11 +281,38 @@ let ast_of_acic0 ~output_type term_info acic k = (* 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 @@ -351,7 +378,7 @@ let rec ast_of_acic1 ~output_type term_info annterm = 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 @@ -371,12 +398,6 @@ let ast_of_acic ~output_type id_to_sort annterm = 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; @@ -384,13 +405,13 @@ let fresh_id = 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 () = @@ -398,7 +419,7 @@ 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)) @@ -429,19 +450,19 @@ let lookup_interpretations symbol = (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; diff --git a/helm/software/components/acic_content/termAcicContent.mli b/helm/software/components/acic_content/termAcicContent.mli index 4f366c9c2..aec8d598c 100644 --- a/helm/software/components/acic_content/termAcicContent.mli +++ b/helm/software/components/acic_content/termAcicContent.mli @@ -68,5 +68,5 @@ val instantiate_appl_pattern: (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 diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml index 859697cd6..bb6033981 100644 --- a/helm/software/components/content_pres/cicNotationParser.ml +++ b/helm/software/components/content_pres/cicNotationParser.ml @@ -226,7 +226,24 @@ let compare_rule_id x y = 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 @@ -322,13 +339,13 @@ let extend (CL1P (level1_pattern,precedence)) action = 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 diff --git a/helm/software/components/content_pres/cicNotationParser.mli b/helm/software/components/content_pres/cicNotationParser.mli index a348d9088..6c9b3f5ec 100644 --- a/helm/software/components/content_pres/cicNotationParser.mli +++ b/helm/software/components/content_pres/cicNotationParser.mli @@ -75,3 +75,5 @@ val parse_term: Ulexing.lexbuf -> CicNotationPt.term (** print "level2_pattern" entry on stdout, flushing afterwards *) val print_l2_pattern: unit -> unit +val push: unit -> unit +val pop: unit -> unit diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml index 29845af1d..378708bce 100644 --- a/helm/software/components/content_pres/termContentPres.ml +++ b/helm/software/components/content_pres/termContentPres.ml @@ -281,11 +281,32 @@ let pp_ast0 t k = (* 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 @@ -441,7 +462,7 @@ let rec pp_ast1 term = 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) @@ -470,11 +491,6 @@ let fill_pos_info l1_pattern = l1_pattern in aux true l1_pattern *) -let counter = ref ~-1 -let reset () = - counter := ~-1; - Hashtbl.clear level1_patterns21 -;; let fresh_id = fun () -> incr counter; @@ -484,14 +500,14 @@ let add_pretty_printer l2 (CicNotationParser.CL1P (l1,precedence)) = 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 diff --git a/helm/software/components/content_pres/termContentPres.mli b/helm/software/components/content_pres/termContentPres.mli index 9b36a9345..40e8fc021 100644 --- a/helm/software/components/content_pres/termContentPres.mli +++ b/helm/software/components/content_pres/termContentPres.mli @@ -48,5 +48,5 @@ val instantiate_level2: CicNotationEnv.t -> CicNotationPt.term -> CicNotationPt.term -(* hack. seee cicNotation for explanation *) -val reset: unit -> unit +val push: unit -> unit +val pop: unit -> unit diff --git a/helm/software/components/lexicon/cicNotation.ml b/helm/software/components/lexicon/cicNotation.ml index 248e08bcb..32cb3f638 100644 --- a/helm/software/components/lexicon/cicNotation.ml +++ b/helm/software/components/lexicon/cicNotation.ml @@ -106,7 +106,14 @@ let set_active_notations ids = 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 () ;; diff --git a/helm/software/components/lexicon/cicNotation.mli b/helm/software/components/lexicon/cicNotation.mli index 6c8647ad8..9e231e331 100644 --- a/helm/software/components/lexicon/cicNotation.mli +++ b/helm/software/components/lexicon/cicNotation.mli @@ -40,10 +40,5 @@ val get_all_notations: unit -> (notation_id * string) list (* id, dsc *) 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 diff --git a/helm/software/components/lexicon/lexiconSync.ml b/helm/software/components/lexicon/lexiconSync.ml index b9c9b1cc2..ed243fe19 100644 --- a/helm/software/components/lexicon/lexiconSync.ml +++ b/helm/software/components/lexicon/lexiconSync.ml @@ -109,3 +109,5 @@ let time_travel ~present ~past = in List.iter CicNotation.remove_notation notation_to_remove +let push () = CicNotation.push ();; +let pop () = CicNotation.pop ();; diff --git a/helm/software/components/lexicon/lexiconSync.mli b/helm/software/components/lexicon/lexiconSync.mli index bba152a9f..a291b3a9b 100644 --- a/helm/software/components/lexicon/lexiconSync.mli +++ b/helm/software/components/lexicon/lexiconSync.mli @@ -37,3 +37,5 @@ val alias_diff: from:LexiconEngine.status -> LexiconEngine.status -> (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list +val push: unit -> unit +val pop: unit -> unit diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index a92b5b789..0234c4824 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -118,23 +118,14 @@ let wrap_with_make include_paths (f : GrafiteParser.statement) x = 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)); -- 2.39.2