X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=30c176fd2a3cd98188c2aaf8b02955aa4e391c37;hb=fb4cdb69cadc581f4f32e73c055dbadda0ed8703;hp=50095cf1364dc03234ef9ac5f1561a46e023a27f;hpb=715a957a9f7362cb002faa488160a910b9db677e;p=helm.git

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index 50095cf13..30c176fd2 100644
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -51,7 +51,7 @@ let inject_unification_hint =
 
 let eval_unification_hint status t n = 
  let metasenv,subst,status,t =
-  GrafiteDisambiguate.disambiguate_nterm None status [] [] [] ("",0,t) in
+  GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,t) in
  assert (metasenv=[]);
  let t = NCicUntrusted.apply_subst subst [] t in
  let status = basic_eval_unification_hint (t,n) status in
@@ -74,11 +74,11 @@ 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
-  LexiconEngine.set_proof_aliases status ~implicit_aliases:false mode diff
+  GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false mode diff
 ;;
 
 let inject_interpretation =
@@ -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
@@ -346,7 +409,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
      let status, composites =
       NCicCoercDeclaration.eval_ncoercion status name t ty source target
      in
-      LexiconSync.add_aliases_for_objs status composites
+      GrafiteDisambiguate.add_aliases_for_objs status composites
   | GrafiteAst.NQed loc ->
      if status#ng_mode <> `ProofMode then
       raise (GrafiteTypes.Command_error "Not in proof mode")
@@ -416,7 +479,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
            let uris = uri::List.rev uris_rev in
 *)
            let status = status#set_ng_mode `CommandMode in
-           let status = LexiconSync.add_aliases_for_objs status [uri] in
+           let status = GrafiteDisambiguate.add_aliases_for_objs status [uri] in
            let status =
             List.fold_left
              (fun status boxml ->
@@ -479,7 +542,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
              (fun status (name,cpos,arity) ->
                try
                  let metasenv,subst,status,t =
-                  GrafiteDisambiguate.disambiguate_nterm None status [] [] []
+                  GrafiteDisambiguate.disambiguate_nterm status None [] [] []
                    ("",0,NotationPt.Ident (name,None)) in
                  assert (metasenv = [] && subst = []);
                  let status, nuris = 
@@ -487,7 +550,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
                      basic_eval_and_record_ncoercion_from_t_cpos_arity 
                       status (name,t,cpos,arity)
                  in
-                  LexiconSync.add_aliases_for_objs status nuris
+                  GrafiteDisambiguate.add_aliases_for_objs status nuris
                with MultiPassDisambiguator.DisambiguationError _-> 
                  HLog.warn ("error in generating coercion: "^name);
                  status) 
@@ -571,7 +634,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
       let metasenv,subst,status,sort = match sort with
         | None -> [],[],status,NCic.Sort NCic.Prop
         | Some s ->
-           GrafiteDisambiguate.disambiguate_nterm None status [] [] []
+           GrafiteDisambiguate.disambiguate_nterm status None [] [] []
             (text,prefix_len,s) 
       in
       assert (metasenv = []);
@@ -585,7 +648,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
              (NCicPp.ppterm ~metasenv ~subst ~context:[] sort))) in
       let status = status#set_ng_mode `ProofMode in
       let metasenv,subst,status,indty =
-       GrafiteDisambiguate.disambiguate_nterm None status [] [] subst
+       GrafiteDisambiguate.disambiguate_nterm status None [] [] subst
         (text,prefix_len,indty) in
       let indtyno,(_,leftno,tys,_,_) =
        match indty with
@@ -609,37 +672,10 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
       eval_add_constraint status [`Type,u1] [`Type,u2]
   (* ex lexicon commands *)
   | GrafiteAst.Interpretation (loc, dsc, (symbol, args), cic_appl_pattern) ->
-     let rec disambiguate =
-      function
-         NotationPt.ApplPattern l ->
-          NotationPt.ApplPattern (List.map disambiguate l)
-       | NotationPt.VarPattern id
-          when not
-           (List.exists
-            (function (NotationPt.IdentArg (_,id')) -> id'=id) args)
-          ->
-           let item = DisambiguateTypes.Id id in
-            begin
-             try
-              match
-               DisambiguateTypes.Environment.find item
-                status#lstatus.LexiconTypes.aliases
-              with
-                 GrafiteAst.Ident_alias (_, uri) ->
-                  NotationPt.NRefPattern (NReference.reference_of_string uri)
-               | _ -> assert false
-             with Not_found -> 
-              prerr_endline
-               ("LexiconEngine.eval_command: domain item not found: " ^ 
-               (DisambiguateTypes.string_of_domain_item item));
-              LexiconEngine.dump_aliases prerr_endline "" status;
-              raise 
-               (Failure
-                ((DisambiguateTypes.string_of_domain_item item) ^ " not found"))
-	          end
-       | p -> p
+     let cic_appl_pattern =
+      GrafiteDisambiguate.disambiguate_cic_appl_pattern status args
+       cic_appl_pattern
      in
-     let cic_appl_pattern = disambiguate cic_appl_pattern in
       eval_interpretation status (dsc,(symbol, args),cic_appl_pattern)
   | GrafiteAst.Notation (loc, dir, l1, associativity, precedence, l2) ->
       let l1 = 
@@ -647,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 =
@@ -670,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*)
-      LexiconEngine.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