From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 23 Sep 2005 12:54:23 +0000 (+0000)
Subject: The disambiguation now returns the aliases diff. It used to return the
X-Git-Tag: LAST_BEFORE_NEW~39
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b12aa2f7dc56d9915603339e9a1e1ba23d834b4a;p=helm.git

The disambiguation now returns the aliases diff. It used to return the
new aliases and a slow diff operation was performed later on.
---

diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml
index 4fe206f74..cd4d42420 100644
--- a/helm/matita/matitaDisambiguator.ml
+++ b/helm/matita/matitaDisambiguator.ml
@@ -73,7 +73,8 @@ let disambiguate_thing ~aliases ~universe
       aliases:DisambiguateTypes.environment ->
       universe:DisambiguateTypes.multiple_environment option ->
       'a -> 'b)
-  ~(set_aliases: DisambiguateTypes.environment -> 'b -> 'b)
+  ~(drop_aliases: 'b -> 'b)
+  ~(drop_aliases_and_clear_diff: 'b -> 'b)
   (thing: 'a)
 =
   assert (universe <> None);
@@ -96,11 +97,11 @@ let disambiguate_thing ~aliases ~universe
   in
   let set_aliases (instances,(use_mono_aliases,_,_),_) (_, user_asked as res) =
    if use_mono_aliases && not instances then
-    res
+    drop_aliases res
    else if user_asked then
-    res (* one shot aliases *)
+    drop_aliases res (* one shot aliases *)
    else
-    set_aliases aliases res
+    drop_aliases_and_clear_diff res
   in
   let rec aux =
     function
@@ -120,30 +121,34 @@ let disambiguate_thing ~aliases ~universe
     CoercDb.use_coercions := saved_use_coercions;
     raise exn
 
+type disambiguator_thing =
+ { do_it :
+    'a 'b.
+    aliases:DisambiguateTypes.environment ->
+    universe:DisambiguateTypes.multiple_environment option ->
+    f:(?fresh_instances:bool ->
+       aliases:DisambiguateTypes.environment ->
+       universe:DisambiguateTypes.multiple_environment option ->
+       'a -> 'b * bool) ->
+    drop_aliases:('b * bool -> 'b * bool) ->
+    drop_aliases_and_clear_diff:('b * bool -> 'b * bool) -> 'a -> 'b * bool
+ }
+
 let disambiguate_thing =
  let profiler = CicUtil.profile "disambiguate_thing" in
-  fun ~aliases ~universe
-      ~(f:?fresh_instances:bool ->
-          aliases:DisambiguateTypes.environment ->
-          universe:DisambiguateTypes.multiple_environment option ->
-          'a -> 'b)
-      ~(set_aliases: DisambiguateTypes.environment -> 'b -> 'b)
-      (thing: 'a)
-  -> profiler.CicUtil.profile
-      (disambiguate_thing ~aliases ~universe ~f ~set_aliases) thing
-
-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)
-=
-  Obj.magic disambiguate_thing ~aliases ~universe ~f ~set_aliases thing
+  { do_it =
+     fun ~aliases ~universe ~f ~drop_aliases ~drop_aliases_and_clear_diff thing
+     -> profiler.CicUtil.profile
+         (disambiguate_thing ~aliases ~universe ~f ~drop_aliases
+           ~drop_aliases_and_clear_diff) thing
+  }
+
+let drop_aliases (choices, user_asked) =
+  (List.map (fun (d, a, b, c) -> d, a, b, c) choices),
+  user_asked
 
-let set_aliases aliases (choices, user_asked) =
-  (List.map (fun (_, a, b, c) -> aliases, a, b, c) choices),
+let drop_aliases_and_clear_diff (choices, user_asked) =
+  (List.map (fun (_, a, b, c) -> [], a, b, c) choices),
   user_asked
 
 let disambiguate_term ?fresh_instances ~dbd ~context ~metasenv ?initial_ugraph
@@ -153,9 +158,11 @@ let disambiguate_term ?fresh_instances ~dbd ~context ~metasenv ?initial_ugraph
   let f =
     Disambiguator.disambiguate_term ~dbd ~context ~metasenv ?initial_ugraph
   in
-  disambiguate_thing ~aliases ~universe ~f ~set_aliases term
+  disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
+   ~drop_aliases_and_clear_diff term
 
 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 ~universe ~f ~set_aliases obj
+  disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
+   ~drop_aliases_and_clear_diff obj
diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 644b492fa..365f947c0 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -162,7 +162,7 @@ let singleton = function
 
 let disambiguate_term status_ref term =
   let status = !status_ref in
-  let (aliases, metasenv, cic, _) =
+  let (diff, metasenv, cic, _) =
     singleton
       (MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
         ~aliases:status.aliases ~universe:(Some status.multi_aliases)
@@ -170,7 +170,7 @@ let disambiguate_term status_ref term =
         ~metasenv:(MatitaMisc.get_proof_metasenv status) term)
   in
   let status = MatitaTypes.set_metasenv metasenv status in
-  let status = MatitaSync.compute_diff_and_set_proof_aliases status aliases in
+  let status = MatitaSync.set_proof_aliases status diff in
   status_ref := status;
   cic
   
@@ -182,14 +182,14 @@ let disambiguate_term status_ref term =
 let disambiguate_lazy_term status_ref term =
   (fun context metasenv ugraph ->
     let status = !status_ref in
-    let (aliases, metasenv, cic, ugraph) =
+    let (diff, metasenv, cic, ugraph) =
       singleton
         (MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
           ~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.compute_diff_and_set_proof_aliases status aliases in
+    let status = MatitaSync.set_proof_aliases status diff in
     status_ref := status;
     cic, metasenv, ugraph)
 
@@ -639,7 +639,7 @@ let disambiguate_obj status obj =
        Some (UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".ind"))
     | GrafiteAst.Inductive _ -> assert false
     | GrafiteAst.Theorem _ -> None in
-  let (aliases, metasenv, cic, _) =
+  let (diff, metasenv, cic, _) =
     singleton
       (MatitaDisambiguator.disambiguate_obj ~dbd:(MatitaDb.instance ())
         ~aliases:status.aliases ~universe:(Some status.multi_aliases) ~uri obj)
@@ -652,7 +652,7 @@ let disambiguate_obj status obj =
     | Intermediate _ -> assert false
   in
   let status = { status with proof_status = proof_status } in
-  let status = MatitaSync.compute_diff_and_set_proof_aliases status aliases in
+  let status = MatitaSync.set_proof_aliases status diff in
   status, cic
   
 let disambiguate_command status = function
diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index 3351725db..3d9d74dcc 100644
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -63,11 +63,6 @@ let set_proof_aliases status new_aliases =
     (DisambiguatePp.commands_of_domain_and_codomain_items_list new_aliases)
     new_status
 
-let compute_diff_and_set_proof_aliases status aliases =
- let new_status = { status with aliases = aliases } in
- let diff = alias_diff ~from:status new_status in
-  set_proof_aliases status diff
-  
 (** given a uri and a type list (the contructors types) builds a list of pairs
  *  (name,uri) that is used to generate authomatic aliases **)
 let extract_alias types uri = 
diff --git a/helm/matita/matitaSync.mli b/helm/matita/matitaSync.mli
index 2175a23dc..df5eb84b5 100644
--- a/helm/matita/matitaSync.mli
+++ b/helm/matita/matitaSync.mli
@@ -43,9 +43,6 @@ val set_proof_aliases :
   (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list ->
   MatitaTypes.status
 
-val compute_diff_and_set_proof_aliases :
-  MatitaTypes.status -> DisambiguateTypes.environment -> MatitaTypes.status
-
   (* removes the object from DB, Disk, CoercionsDB, CicEnvironment, getter 
    * asserts the uri is resolved to file:// so it is only for 
    * user's objects *)