- disambiguation code moved from matitaEngine to grafiteDisambiguate

- grafiteDisambiguate.db is now opaque

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index 7fa62ff743120c2f95b4cd4d5ace80071cd0ede0..032af19fb4e7f93316a7498bd35401be0b088a75 100644 (file)
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -609,37 +609,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#disambiguate_db.GrafiteDisambiguate.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));
-              GrafiteDisambiguate.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 = 

diff --git a/matita/components/lexicon/grafiteDisambiguate.ml b/matita/components/lexicon/grafiteDisambiguate.ml
index 5b27aba1b613f41f242049c6c5ac0edfa665a42b..058ddaec3879eca4d4e2e860bb2192af408721c9 100644 (file)
--- a/matita/components/lexicon/grafiteDisambiguate.ml
+++ b/matita/components/lexicon/grafiteDisambiguate.ml
@@ -54,6 +54,14 @@ class status =
       = fun o -> ((self#set_interp_status o)#set_disambiguate_db o#disambiguate_db)
  end
 
+let eval_with_new_aliases status f =
+ let status =
+  status#set_disambiguate_db { status#disambiguate_db with new_aliases = [] } in
+ let res = f status in
+ let new_aliases = status#disambiguate_db.new_aliases in
+  new_aliases,res
+;;
+
 let dump_aliases out msg status =
    out (if msg = "" then "aliases dump:" else msg ^ ": aliases dump:");
    DisambiguateTypes.Environment.iter (fun _ x -> out (GrafiteAstPp.pp_alias x))
@@ -272,3 +280,37 @@ let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) =
   in
    estatus, cic
 ;;
+
+let disambiguate_cic_appl_pattern status args =
+ 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#disambiguate_db.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));
+         dump_aliases prerr_endline "" status;
+         raise 
+          (Failure
+           ((DisambiguateTypes.string_of_domain_item item) ^ " not found"))
+             end
+  | p -> p
+ in
+  disambiguate
+;;

diff --git a/matita/components/lexicon/grafiteDisambiguate.mli b/matita/components/lexicon/grafiteDisambiguate.mli
index 6b203cab4c1241df21099359f91b97606b02426c..401eba1152ada7565b7dfc1919dd8220c1e4ab4c 100644 (file)
--- a/matita/components/lexicon/grafiteDisambiguate.mli
+++ b/matita/components/lexicon/grafiteDisambiguate.mli
@@ -23,11 +23,7 @@
  * http://helm.cs.unibo.it/
  *)
 
-type db = {
-  aliases: GrafiteAst.alias_spec DisambiguateTypes.Environment.t;
-  multi_aliases: GrafiteAst.alias_spec list DisambiguateTypes.Environment.t;
-  new_aliases: (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list
-}
+type db
 
 class type g_status =
  object
@@ -43,6 +39,10 @@ class status :
   method set_disambiguate_status: #g_status -> 'self
  end
 
+val eval_with_new_aliases:
+ #status as 'status -> ('status -> 'a) ->
+  (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list * 'a
+
 val set_proof_aliases:
  #status as 'status ->
   implicit_aliases:bool -> (* implicit ones are made explicit *)
@@ -71,3 +71,8 @@ type pattern =
 
 val disambiguate_npattern:
   GrafiteAst.npattern Disambiguate.disambiguator_input -> pattern
+
+val disambiguate_cic_appl_pattern:
+ #status ->
+  NotationPt.argument_pattern list ->
+   NotationPt.cic_appl_pattern -> NotationPt.cic_appl_pattern

diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml
index a95936c9740b3bbf0f27ad321bb232562af4f18d..4c246a2539657b5da052a5be203bb84551141aa0 100644 (file)
--- a/matita/matita/matitaEngine.ml
+++ b/matita/matita/matitaEngine.ml
@@ -53,12 +53,11 @@ let eval_macro_screenshot (status : GrafiteTypes.status) name =
 
 let eval_ast ~include_paths ?do_heavy_checks status (text,prefix_len,ast) =
  let baseuri = status#baseuri in
- let status =
-  status#set_disambiguate_db { status#disambiguate_db with GrafiteDisambiguate.new_aliases = [] } in
- let status =
-  GrafiteEngine.eval_ast ~include_paths ?do_heavy_checks status
-   (text,prefix_len,ast) in
- let new_aliases = status#disambiguate_db.GrafiteDisambiguate.new_aliases in
+ let new_aliases,status =
+  GrafiteDisambiguate.eval_with_new_aliases status
+   (fun status ->
+     GrafiteEngine.eval_ast ~include_paths ?do_heavy_checks status
+      (text,prefix_len,ast)) in
  let _,intermediate_states = 
   List.fold_left
    (fun (status,acc) (k,value) ->