X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fdisambiguation%2Fdisambiguate.ml;fp=matitaB%2Fcomponents%2Fdisambiguation%2Fdisambiguate.ml;h=7e395e1c19bb096a7bc57845002624ba54c48b66;hb=86b0a224bd9251ed22648de04bc0d00f11dbd0fc;hp=e78ca54a36b34dde2d156ff7910a698637dbc79f;hpb=e499c2e36d8a39c4749b8e0e34438b49532d15b8;p=helm.git

diff --git a/matitaB/components/disambiguation/disambiguate.ml b/matitaB/components/disambiguation/disambiguate.ml
index e78ca54a3..7e395e1c1 100644
--- a/matitaB/components/disambiguation/disambiguate.ml
+++ b/matitaB/components/disambiguation/disambiguate.ml
@@ -31,10 +31,7 @@ open DisambiguateTypes
 
 module Ast = NotationPt
 
-(* hard errors, spurious errors *)
-exception NoWellTypedInterpretation of
- ((Stdpp.location * string) list *
-  (Stdpp.location * string) list)
+exception NoWellTypedInterpretation of (Stdpp.location * string)
 
 exception PathNotWellFormed
 
@@ -140,8 +137,6 @@ type ('alias,'ast_thing,'metasenv,'subst,'thing,'ugraph) disamb_result =
        * node; each ast is associated with the actual instantiation of the node, 
        * the refinement error, and the location at which refinement fails *)
   | Disamb_failure of
-      (* hard errors, spurious errors *) 
-      (('ast_thing * 'alias option * Stdpp.location * string) list * Stdpp.location) list *
       (('ast_thing * 'alias option * Stdpp.location * string) list * Stdpp.location) list
 
 let resolve ~env ~universe ~mk_choice item interpr arg =
@@ -623,8 +618,10 @@ let test_interpr ~context ~metasenv ~subst ~use_coercions ~expty ~env ~universe
      (*| Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg))
      | Invalid_choice loc_msg -> Ko loc_msg*)
      | Invalid_choice x -> 
-        let loc,err = Lazy.force x in Some (loc,err)
-     | _ -> None
+        let loc,err = Lazy.force x in 
+        debug_print (lazy ("test_interpr invalid choice: " ^ err)); 
+        Some (loc,err)
+     | e -> debug_print (lazy ("uncaught error: "^ Printexc.to_string e));None
 ;;
 
 exception Not_ambiguous;;
@@ -699,6 +696,8 @@ let rec disambiguate_list
           "\nin " ^ pp_thing (ctx t)));
           (* get possible instantiations of t *)
           let instances = get_instances ctx t in
+          if instances = [] then
+            raise (NoWellTypedInterpretation (loc_t, "No choices for " ^ astpp t));
           debug_print (lazy "-- possible instances:");
 (*          List.iter 
            (fun u0 -> debug_print (lazy ("-- instance: " ^ (pp_thing u0))))
@@ -758,27 +757,37 @@ let disambiguate_thing
      match refine_thing metasenv subst context uri ~use_coercions t' expty
           base_univ ~localization_tbl with
     | Ok (t',m',s',u') -> t,m',s',t',u'
-    | Uncertain x ->
-        let _,err = Lazy.force x in
+    | Uncertain x | Ko x ->
+        let loc,err = Lazy.force x in
         debug_print (lazy ("refinement uncertain after disambiguation: " ^ err));
-        assert false
-    | _ -> assert false
+        raise (NoWellTypedInterpretation (loc,err))
   in
   match (test_interpr thing) with
   | Some (loc,err) ->
-(*     debug_print (lazy ("preliminary test fail: " ^ pp_thing thing)); *)
-     Disamb_failure ([[thing,None,loc,err],loc],[])
+     debug_print (lazy ("preliminary test fail: " ^ pp_thing thing)); 
+     Disamb_failure ([[thing,None,loc,err],loc])
   | None -> 
     let res,errors = aux [thing] in
-    let res = 
-      HExtlib.filter_map (fun t ->
-        try Some (refine t)
-        with _ -> 
-(*          debug_print (lazy ("can't interpretate/refine " ^ (pp_thing t)));*)
-                None) res
+    let res,inner_errors =
+      List.split 
+      (List.map (fun t ->
+        try (Some (refine t), None)
+        (* this error is actually a singleton *)
+        with NoWellTypedInterpretation loc_err -> 
+          debug_print (lazy ("can't interpretate/refine " ^ (pp_thing t)));
+                None, Some loc_err) res) in
+    let res = HExtlib.filter_map (fun x -> x) res in
+    let inner_errors = 
+      HExtlib.filter_map 
+        (function Some (loc,err) -> Some (thing,None,loc,err) | None -> None) 
+        inner_errors 
+    in
+    let errors = 
+      if inner_errors <> [] then (inner_errors,Stdpp.dummy_loc)::errors
+         else errors
     in
     (match res with
-    | [] -> Disamb_failure (errors,[])
+    | [] -> prerr_endline ((string_of_int (List.length errors)) ^ " error frames");Disamb_failure errors
     | _ -> Disamb_success res) 
 ;;