From 1caab3250f877ebff8fefc99dd7f5e7fd0596795 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 4 Nov 2010 23:37:01 +0000 Subject: [PATCH] - disk dumping of ex-lexicon commands almost implemented --- matita/components/content/notationUtil.ml | 1 + matita/components/content/notationUtil.mli | 1 + .../content_pres/cicNotationParser.ml | 3 + .../content_pres/cicNotationParser.mli | 2 + .../grafite_engine/grafiteEngine.ml | 79 ++++++++++++++++--- matita/matita/nlibrary/logic/pts.ma | 2 + 6 files changed, 77 insertions(+), 11 deletions(-) diff --git a/matita/components/content/notationUtil.ml b/matita/components/content/notationUtil.ml index 98e1ba663..a2ab34833 100644 --- a/matita/components/content/notationUtil.ml +++ b/matita/components/content/notationUtil.ml @@ -397,3 +397,4 @@ let freshen_obj obj = let freshen_term = freshen_term ?index:None +let refresh_uri_in_term t = assert false diff --git a/matita/components/content/notationUtil.mli b/matita/components/content/notationUtil.mli index f7c1c0cd4..f1c96c536 100644 --- a/matita/components/content/notationUtil.mli +++ b/matita/components/content/notationUtil.mli @@ -92,3 +92,4 @@ type notation_id val fresh_id: unit -> notation_id +val refresh_uri_in_term: NotationPt.term -> NotationPt.term diff --git a/matita/components/content_pres/cicNotationParser.ml b/matita/components/content_pres/cicNotationParser.ml index c22953314..1f83a64d5 100644 --- a/matita/components/content_pres/cicNotationParser.ml +++ b/matita/components/content_pres/cicNotationParser.ml @@ -48,6 +48,9 @@ type ('a,'b,'c,'d) grammars = { type checked_l1_pattern = CL1P of NotationPt.term * int +let refresh_uri_in_checked_l1_pattern (CL1P (t,n)) = + CL1P (NotationUtil.refresh_uri_in_term t, n) + type binding = | NoBinding | Binding of string * Env.value_type diff --git a/matita/components/content_pres/cicNotationParser.mli b/matita/components/content_pres/cicNotationParser.mli index 62262c14c..1cbef668d 100644 --- a/matita/components/content_pres/cicNotationParser.mli +++ b/matita/components/content_pres/cicNotationParser.mli @@ -42,6 +42,8 @@ class status: keywords:string list -> type checked_l1_pattern = private CL1P of NotationPt.term * int +val refresh_uri_in_checked_l1_pattern: checked_l1_pattern -> checked_l1_pattern + (** {2 Parsing functions} *) (** concrete syntax pattern: notation level 1, the diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index 032af19fb..8d299a533 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -74,7 +74,7 @@ let basic_eval_interpretation (dsc, (symbol, args), cic_appl_pattern) status = let status = Interpretations.add_interpretation status dsc (symbol, args) cic_appl_pattern in - let mode = GrafiteAst.WithPreferences (*assert false*) in (* VEDI SOTTO *) + let mode = GrafiteAst.WithPreferences (*assert false*) in (* MATITA 1.0 VEDI SOTTO *) let diff = [DisambiguateTypes.Symbol (symbol, 0), GrafiteAst.Symbol_alias (symbol,0,dsc)] in @@ -107,6 +107,69 @@ let eval_interpretation status data= status#set_dump dump ;; +let basic_eval_alias (mode,diff) status = + GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false mode diff +;; + +let inject_alias = + let basic_eval_alias (mode,diff) ~refresh_uri_in_universe ~refresh_uri_in_term= + basic_eval_alias (mode,diff) + in + GrafiteTypes.Serializer.register#run "alias" basic_eval_alias +;; + +let eval_alias status data= + let status = basic_eval_alias data status in + let dump = inject_alias data::status#dump in + status#set_dump dump +;; + +let basic_eval_input_notation (l1,l2) status = + GrafiteParser.extend status l1 + (fun env loc -> + NotationPt.AttributedTerm + (`Loc loc,TermContentPres.instantiate_level2 env l2)) +;; + +let inject_input_notation = + let basic_eval_input_notation (l1,l2) + ~refresh_uri_in_universe ~refresh_uri_in_term + = + let l1 = CicNotationParser.refresh_uri_in_checked_l1_pattern l1 in + let l2 = NotationUtil.refresh_uri_in_term l2 in + basic_eval_input_notation (l1,l2) + in + GrafiteTypes.Serializer.register#run "input_notation" + basic_eval_input_notation +;; + +let eval_input_notation status data= + let status = basic_eval_input_notation data status in + let dump = inject_input_notation data::status#dump in + status#set_dump dump +;; + +let basic_eval_output_notation (l1,l2) status = + TermContentPres.add_pretty_printer status l2 l1 +;; + +let inject_output_notation = + let basic_eval_output_notation (l1,l2) + ~refresh_uri_in_universe ~refresh_uri_in_term + = + let l1 = CicNotationParser.refresh_uri_in_checked_l1_pattern l1 in + let l2 = NotationUtil.refresh_uri_in_term l2 in + basic_eval_output_notation (l1,l2) + in + GrafiteTypes.Serializer.register#run "output_notation" + basic_eval_output_notation +;; + +let eval_output_notation status data= + let status = basic_eval_output_notation data status in + let dump = inject_output_notation data::status#dump in + status#set_dump dump +;; let record_index_obj = let aux l @@ -338,7 +401,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = GrafiteTypes.Serializer.require ~baseuri:(NUri.uri_of_string baseuri) status in let status = status#set_dump (obj::status#dump) in - assert false; (* mode must be passed to GrafiteTypes.Serializer.require + (*assert false;*) (* MATITA 1.0mode must be passed to GrafiteTypes.Serializer.require somehow *) status | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n @@ -620,15 +683,10 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = l1 (dir = Some `RightToLeft) precedence associativity in let status = - if dir <> Some `RightToLeft then - GrafiteParser.extend status l1 - (fun env loc -> - NotationPt.AttributedTerm - (`Loc loc,TermContentPres.instantiate_level2 env l2)) + if dir <> Some `RightToLeft then eval_input_notation status (l1,l2) else status in - if dir <> Some `LeftToRight then - TermContentPres.add_pretty_printer status l2 l1 + if dir <> Some `LeftToRight then eval_output_notation status (l1,l2) else status | GrafiteAst.Alias (loc, spec) -> let diff = @@ -643,8 +701,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = [DisambiguateTypes.Num instance,spec] in let mode = GrafiteAst.WithPreferences in(*assert false in (* VEDI SOPRA *) MATITA 1.0*) - GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false mode diff - (* assert false (* MANCA SALVATAGGIO SU DISCO *) *) + eval_alias status (mode,diff) ;; let eval_comment opts status (text,prefix_len,c) = status diff --git a/matita/matita/nlibrary/logic/pts.ma b/matita/matita/nlibrary/logic/pts.ma index d9db8c39f..1fed85256 100644 --- a/matita/matita/nlibrary/logic/pts.ma +++ b/matita/matita/nlibrary/logic/pts.ma @@ -12,6 +12,8 @@ (* *) (**************************************************************************) +include "core_notation.ma". + universe constraint Type[0] < Type[1]. universe constraint Type[1] < Type[2]. universe constraint Type[2] < Type[3]. -- 2.39.2