Yet another implementation of the single aliases / multi aliases idea.

The new implementation is much simpler: single aliases are used everywhere
in the disambiguation phase; however, when a term needs to be looked for in
the library, it can be looked in a user-provided multi aliases environment instead.

NOTE: the new implementation fixes a bug of the previous implementation: the
most recent alias in the multi-alias set was printed last in the .moo files,
changing the performances of the system.

diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml
index b7de40ed966eb580740c5b506f4bb53103180b4e..5a7fe0b9f45ff925fcb0ca28947f3900597c49b0 100644 (file)
--- a/helm/matita/matitaDisambiguator.ml
+++ b/helm/matita/matitaDisambiguator.ml
@@ -68,14 +68,18 @@ module Disambiguator = Disambiguate.Make (Callbacks)
 
 (* implement module's API *)
 
-let disambiguate_thing ~aliases
-  ~(f:?fresh_instances:bool -> aliases:Disambiguate.aliases -> 'a -> 'b)
+let disambiguate_thing ~aliases ~universe
+  ~(f:?fresh_instances:bool ->
+      aliases:DisambiguateTypes.environment ->
+      universe:DisambiguateTypes.multiple_environment option ->
+      'a -> 'b)
   ~(set_aliases: DisambiguateTypes.environment -> 'b -> 'b)
   (thing: 'a)
 =
-  let library = true, DisambiguateTypes.empty_environment in
-  let multi_aliases = true, aliases in
-  let mono_aliases = false, aliases in
+  assert (universe <> None);
+  let library = false, DisambiguateTypes.Environment.empty, None in
+  let multi_aliases=false, DisambiguateTypes.Environment.empty, universe in
+  let mono_aliases = true, aliases, None in
   let passes =  (* <fresh_instances?, aliases, coercions?> *)
     [ (false, mono_aliases, false);
       (false, multi_aliases, false);
@@ -86,12 +90,12 @@ let disambiguate_thing ~aliases
       (true, library, true);
     ]
   in
-  let try_pass (fresh_instances, aliases, use_coercions) =
+  let try_pass (fresh_instances, (_, aliases, universe), use_coercions) =
     CoercDb.use_coercions := use_coercions;
-    f ~fresh_instances ~aliases thing
+    f ~fresh_instances ~aliases ~universe thing
   in
-  let set_aliases (instances,(use_multi_aliases,_),_) (_, user_asked as res) =
-   if not use_multi_aliases && not instances then
+  let set_aliases (instances,(use_mono_aliases,_,_),_) (_, user_asked as res) =
+   if use_mono_aliases && not instances then
     res
    else if user_asked then
     res (* one shot aliases *)
@@ -120,13 +124,17 @@ let set_aliases aliases (choices, user_asked) =
   (List.map (fun (_, a, b, c) -> aliases, a, b, c) choices),
   user_asked
 
-let disambiguate_term ~dbd ~context ~metasenv ?initial_ugraph ~aliases term =
+let disambiguate_term ?fresh_instances ~dbd ~context ~metasenv ?initial_ugraph
+  ~aliases ~universe term
+ =
+  assert (fresh_instances = None);
   let f =
     Disambiguator.disambiguate_term ~dbd ~context ~metasenv ?initial_ugraph
   in
-  disambiguate_thing ~aliases ~f ~set_aliases term
+  disambiguate_thing ~aliases ~universe ~f ~set_aliases term
 
-let disambiguate_obj ~dbd ~aliases ~uri obj =
+let disambiguate_obj ?fresh_instances ~dbd ~aliases ~universe ~uri obj =
+  assert (fresh_instances = None);
   let f = Disambiguator.disambiguate_obj ~dbd ~uri in
-  disambiguate_thing ~aliases ~f ~set_aliases obj
+  disambiguate_thing ~aliases ~universe ~f ~set_aliases obj
 

diff --git a/helm/matita/matitaDisambiguator.mli b/helm/matita/matitaDisambiguator.mli
index a5d0aed44e465d9f5c3ca4cf783ff70e0071e166..01fa97ef08810b9741a4efa6ebcaaac80152a86e 100644 (file)
--- a/helm/matita/matitaDisambiguator.mli
+++ b/helm/matita/matitaDisambiguator.mli
@@ -47,28 +47,4 @@ val mono_interp_callback: choose_interp_callback
 
 (** for GUI callbacks see MatitaGui.interactive_{interp,user_uri}_choice *)
 
-val disambiguate_term :
-  dbd:Mysql.dbd ->
-  context:Cic.context ->
-  metasenv:Cic.metasenv ->
-  ?initial_ugraph:CicUniv.universe_graph -> 
-  aliases:DisambiguateTypes.environment -> (* previous interpretation status *)
-  DisambiguateTypes.term ->
-  (DisambiguateTypes.environment * (* new interpretation status *)
-   Cic.metasenv *                  (* new metasenv *)
-   Cic.term *
-   CicUniv.universe_graph) list *  (* disambiguated term *)
-  bool  (* has interactive_interpretation_choice been invoked? *)
-
-(** @param fresh_instances as per disambiguate_term *)
-val disambiguate_obj :
-  dbd:Mysql.dbd ->
-  aliases:DisambiguateTypes.environment -> (* previous interpretation status *)
-  uri:UriManager.uri option ->     (* required only for inductive types *)
-  GrafiteAst.obj ->
-  (DisambiguateTypes.environment * (* new interpretation status *)
-   Cic.metasenv *                  (* new metasenv *)
-   Cic.obj *
-   CicUniv.universe_graph) list *  (* disambiguated obj *)
-  bool  (* has interactive_interpretation_choice been invoked? *)
-
+include Disambiguate.Disambiguator

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 8c891b04355759f28ff7a8522329fed6dcb54293..577e243a6744879152b0706965c3dde1ff8afddd 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -165,7 +165,8 @@ let disambiguate_term status_ref term =
   let (aliases, metasenv, cic, _) =
     singleton
       (MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
-        ~aliases:(status.aliases) ~context:(MatitaMisc.get_proof_context status)
+        ~aliases:status.aliases ~universe:(Some status.multi_aliases)
+        ~context:(MatitaMisc.get_proof_context status)
         ~metasenv:(MatitaMisc.get_proof_metasenv status) term)
   in
   let status = MatitaTypes.set_metasenv metasenv status in
@@ -184,8 +185,8 @@ let disambiguate_lazy_term status_ref term =
     let (aliases, metasenv, cic, ugraph) =
       singleton
         (MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
-          ~initial_ugraph:ugraph ~aliases:status.aliases ~context ~metasenv
-            term)
+          ~initial_ugraph:ugraph ~aliases:status.aliases
+          ~universe:(Some status.multi_aliases) ~context ~metasenv term)
     in
     let status = MatitaTypes.set_metasenv metasenv status in
     let status = MatitaSync.set_proof_aliases status aliases in
@@ -511,7 +512,7 @@ let disambiguate_obj status obj =
   let (aliases, metasenv, cic, _) =
     singleton
       (MatitaDisambiguator.disambiguate_obj ~dbd:(MatitaDb.instance ())
-        ~aliases:(status.aliases) ~uri obj)
+        ~aliases:status.aliases ~universe:(Some status.multi_aliases) ~uri obj)
   in
   let proof_status =
     match status.proof_status with
@@ -628,17 +629,17 @@ let eval_command opts status cmd =
              code in DisambiguatePp *)
       match spec with
       | GrafiteAst.Ident_alias (id,uri) -> 
-         DisambiguateTypes.Environment.cons
+         DisambiguateTypes.Environment.add
           (DisambiguateTypes.Id id) 
           (uri,(fun _ _ _-> CicUtil.term_of_uri (UriManager.uri_of_string uri)))
           status.aliases 
       | GrafiteAst.Symbol_alias (symb, instance, desc) ->
-         DisambiguateTypes.Environment.cons
+         DisambiguateTypes.Environment.add
           (DisambiguateTypes.Symbol (symb,instance))
           (DisambiguateChoices.lookup_symbol_by_dsc symb desc)
           status.aliases
       | GrafiteAst.Number_alias (instance,desc) ->
-         DisambiguateTypes.Environment.cons
+         DisambiguateTypes.Environment.add
           (DisambiguateTypes.Num instance)
           (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases
      in
@@ -648,7 +649,7 @@ let eval_command opts status cmd =
   | GrafiteAst.Interpretation (_, dsc, (symbol, _), _) as stm ->
       let status' = add_moo_content [stm] status in
       let aliases' =
-        DisambiguateTypes.Environment.cons
+        DisambiguateTypes.Environment.add
           (DisambiguateTypes.Symbol (symbol, 0))
           (DisambiguateChoices.lookup_symbol_by_dsc symbol dsc)
           status.aliases
@@ -800,7 +801,8 @@ let default_options () =
 
 let initial_status =
   lazy {
-    aliases = DisambiguateTypes.empty_environment;
+    aliases = DisambiguateTypes.Environment.empty;
+    multi_aliases = DisambiguateTypes.Environment.empty;
     moo_content_rev = [];
     proof_status = No_proof;
     options = default_options ();

diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml
index 78e780a155224da1ee8b24a0c042cf34a9595dbe..97d6cac4738b2b0a12c53ceaaad7cfc99d19dda5 100644 (file)
--- a/helm/matita/matitaMisc.ml
+++ b/helm/matita/matitaMisc.ml
@@ -275,8 +275,6 @@ let get_proof_conclusion status =
       conclusion
   | _ -> statement_error "no ongoing proof"
  
-let get_proof_aliases status = status.aliases
-
 let qualify status name = get_string_option status "baseuri" ^ "/" ^ name
 
 let unopt = function None -> failwith "unopt: None" | Some v -> v

diff --git a/helm/matita/matitaMisc.mli b/helm/matita/matitaMisc.mli
index 568bcc5ed8ee9270825957d1b95a80660fb98f64..21045c0a3b1134e5429c50ab2296fcedf979dd96 100644 (file)
--- a/helm/matita/matitaMisc.mli
+++ b/helm/matita/matitaMisc.mli
@@ -113,7 +113,6 @@ val get_proof_status: MatitaTypes.status -> ProofEngineTypes.status
 val get_proof_metasenv: MatitaTypes.status ->  Cic.metasenv
 val get_proof_context: MatitaTypes.status -> Cic.context 
 val get_proof_conclusion: MatitaTypes.status -> Cic.term 
-val get_proof_aliases: MatitaTypes.status -> DisambiguateTypes.environment 
 
   (** given the base name of an image, returns its full path *)
 val image_path: string -> string

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 8ef5146ca8d72689f65646d67e40ab02748fe5b6..f12ac877dad2af34b1ca45fb31030d117861e322 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -118,7 +118,7 @@ let eval_with_engine guistuff status user_goal parsed_text st =
   let initial_space,status,new_status_and_text_list_rev = 
     let module DTE = DisambiguateTypes.Environment in
     let module UM = UriManager in
-    DTE.fold_flatten (
+    DTE.fold (
       fun k ((v,_) as value) (initial_space,status,acc) -> 
         let b = 
           try
@@ -133,9 +133,9 @@ let eval_with_engine guistuff status user_goal parsed_text st =
           let initial_space =
            if initial_space = "" then "\n" else initial_space in
             initial_space ^
-             DisambiguatePp.pp_environment(DTE.cons k value DTE.empty) in
+             DisambiguatePp.pp_environment(DTE.add k value DTE.empty) in
          let new_status =
-          {status with aliases = DTE.cons k value status.aliases}
+          MatitaSync.set_proof_aliases status (DTE.add k value status.aliases)
          in
           "\n",new_status,((new_status, new_text)::acc)
     ) new_aliases (initial_space,status,[]) in
@@ -206,8 +206,9 @@ let disambiguate term status =
   let dbd = MatitaDb.instance () in
   let metasenv = MatitaMisc.get_proof_metasenv status in
   let context = MatitaMisc.get_proof_context status in
-  let aliases = MatitaMisc.get_proof_aliases status in
-  let interps = MD.disambiguate_term dbd context metasenv aliases term in
+  let interps =
+   MD.disambiguate_term ~dbd ~context ~metasenv ~aliases:status.aliases
+    ~universe:(Some status.multi_aliases) term in
   match interps with 
   | [_,_,x,_], _ -> x
   | _ -> assert false
@@ -294,10 +295,9 @@ let eval_macro guistuff status unparsed_text parsed_text script mac =
   | TA.Check (_,term) ->
       let metasenv = MatitaMisc.get_proof_metasenv status in
       let context = MatitaMisc.get_proof_context status in
-      let aliases = MatitaMisc.get_proof_aliases status in
       let interps = 
-        MatitaDisambiguator.disambiguate_term 
-          dbd context metasenv aliases term 
+        MatitaDisambiguator.disambiguate_term ~dbd ~context ~metasenv
+         ~aliases:status.aliases ~universe:(Some status.multi_aliases) term
       in
       let _, metasenv , term, ugraph =
         match interps with 

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index 55cb4a45c09d45c887e07c26602934283bc61679..c4f8f554724a5422bed9f80c2e03a94d252727bf 100644 (file)
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -29,23 +29,19 @@ open MatitaTypes
 
 let alias_diff ~from status = 
   let module Map = DisambiguateTypes.Environment in
-  Map.fold_flatten
+  Map.fold
     (fun domain_item codomain_item acc ->
        if not (Map.mem domain_item from.aliases) then
-         Map.cons domain_item codomain_item acc
+         Map.add domain_item codomain_item acc
        else
          begin
            try 
-             let codomain1 = Map.find domain_item from.aliases in
-             let codomain2 = Map.find domain_item status.aliases in
-             List.fold_right
-              (fun item env ->
-                let dsc = fst item in
-                if not (List.exists (fun (dsc', _) -> dsc'=dsc) codomain1) then
-                  Map.cons domain_item codomain_item env
-                else
-                  env)
-              codomain2 acc
+            let description1 = fst(Map.find domain_item from.aliases) in
+            let description2 = fst(Map.find domain_item status.aliases) in
+            if description1 <> description2 then
+              Map.add domain_item codomain_item acc
+            else
+              acc
            with Not_found -> acc
          end)
     status.aliases Map.empty
@@ -53,6 +49,10 @@ let alias_diff ~from status =
 let set_proof_aliases status aliases =
  let new_status = { status with aliases = aliases } in
  let diff = alias_diff ~from:status new_status in
+ let multi_aliases =
+  DisambiguateTypes.Environment.fold DisambiguateTypes.Environment.cons
+   diff status.multi_aliases in
+ let new_status = { new_status with multi_aliases = multi_aliases } in
  if DisambiguateTypes.Environment.is_empty diff then
    new_status
  else

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index 4ac480cf1761b5fed5fbcbcac80d313f995185d0..5df68ea86dca84d94d0ff52b4c86c082a9081935 100644 (file)
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -61,6 +61,7 @@ type ast_command = (CicNotationPt.term, GrafiteAst.obj) GrafiteAst.command
 
 type status = {
   aliases: DisambiguateTypes.environment;
+  multi_aliases: DisambiguateTypes.multiple_environment;
   moo_content_rev: ast_command list;
   proof_status: proof_status;
   options: options;

diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli
index c0946c89f8a0c8990d073ff489a3afa8b1be7c32..51744f15296240242f0e5e51747e339dc551069f 100644 (file)
--- a/helm/matita/matitaTypes.mli
+++ b/helm/matita/matitaTypes.mli
@@ -51,6 +51,7 @@ type ast_command = (CicNotationPt.term, GrafiteAst.obj) GrafiteAst.command
 
 type status = {
   aliases: DisambiguateTypes.environment;   (** disambiguation aliases *)
+  multi_aliases: DisambiguateTypes.multiple_environment;
   moo_content_rev: ast_command list;
   proof_status: proof_status;
   options: options;