- disk dumping of ex-lexicon commands almost implemented

diff --git a/matita/components/content/notationUtil.ml b/matita/components/content/notationUtil.ml
index 98e1ba663b9adaac3868f9e4ac8879e3cb5054f0..a2ab34833cd098ea72335c56d9242c2ec60498cf 100644 (file)
--- 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 f7c1c0cd439625f8a4f286d37055eec552bf1a80..f1c96c5364a27c574b70822cd55fa7171925f324 100644 (file)
--- 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 c229533140e828c9cd912a4591cf62b79c9ec532..1f83a64d57d9b6ff0bc3e09f46d4156d4f0e4c3d 100644 (file)
--- 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 62262c14c5f66880115028f912099b40f1e1deae..1cbef668d98e1c85254455480297f49642311184 100644 (file)
--- 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 032af19fb4e7f93316a7498bd35401be0b088a75..8d299a533411e71502325418a4e682b8041b8b61 100644 (file)
--- 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 d9db8c39f553b40e581296e7e27e48bf0ac9c7dd..1fed8525640c26c3616c67063f1085c491f7c95e 100644 (file)
--- 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].