X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaDisambiguator.ml;h=24a8355237b7d1e4a7b81d4b58068a01537bc22d;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=4fe206f74618953b4ed9d5110cbd553ab77d2397;hpb=2534f543cfce5f39b0445e593df5810ba2cbf5ad;p=helm.git

diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml
index 4fe206f74..24a835523 100644
--- a/helm/matita/matitaDisambiguator.ml
+++ b/helm/matita/matitaDisambiguator.ml
@@ -28,6 +28,7 @@ open Printf
 open MatitaTypes
 
 exception Ambiguous_input
+exception DisambiguationError of string Lazy.t list list
 
 type choose_uris_callback =
   id:string -> UriManager.uri list -> UriManager.uri list
@@ -73,7 +74,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,54 +98,63 @@ 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 =
+  let rec aux errors =
     function
-    | [ pass ] -> set_aliases pass (try_pass pass)
+    | [ pass ] ->
+        (try
+          set_aliases pass (try_pass pass)
+         with Disambiguate.NoWellTypedInterpretation newerrors ->
+          raise (DisambiguationError (errors @ [newerrors])))
     | hd :: tl ->
         (try
           set_aliases hd (try_pass hd)
-        with Disambiguate.NoWellTypedInterpretation -> aux tl)
+        with Disambiguate.NoWellTypedInterpretation newerrors ->
+         aux (errors @ [newerrors]) tl)
     | [] -> assert false
   in
   let saved_use_coercions = !CoercDb.use_coercions in
   try
-    let res = aux passes in
+    let res = aux [] passes in
     CoercDb.use_coercions := saved_use_coercions;
     res
   with exn ->
     CoercDb.use_coercions := saved_use_coercions;
     raise exn
 
-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
+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 ~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
+let disambiguate_thing =
+ let profiler = HExtlib.profile "disambiguate_thing" in
+  { do_it =
+     fun ~aliases ~universe ~f ~drop_aliases ~drop_aliases_and_clear_diff thing
+     -> profiler.HExtlib.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 +164,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