X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_disambiguation%2FgrafiteDisambiguate.ml;h=c39ac161d939d56dac961b2f0527589a07f8b759;hb=04168c737e0916ebdbcdb1457f228bef670c657b;hp=544128befd29ea706c6247c50e2056f38b08ee8b;hpb=24fc5e5485245fe879e17d46176530b688930b3b;p=helm.git

diff --git a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
index 544128bef..c39ac161d 100644
--- a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
+++ b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
@@ -79,6 +79,18 @@ class virtual status uid =
 (* reports the first source of ambiguity and its possible interpretations *)
 exception Ambiguous_input of (Stdpp.location * GrafiteAst.alias_spec list)
 
+(* reports disambiguation errors *)
+exception Error of 
+  (* location of a choice point *)
+  (Stdpp.location * 
+    (* one possible choice (or no valid choice) *)
+    (GrafiteAst.alias_spec option *
+      (* list of asts together with the failing location and error msg *)  
+      ((Stdpp.location * GrafiteAst.alias_spec) list * 
+        Stdpp.location * string) list) 
+      list) 
+  list
+
 let dump_aliases out msg status =
    out (if msg = "" then "aliases dump:" else msg ^ ": aliases dump:");
    DisambiguateTypes.InterprEnv.iter (fun _ x -> out (GrafiteAstPp.pp_alias x))
@@ -306,9 +318,20 @@ let rec find_diffs l =
     find_diffs tls
 ;;
 
+(* clusterize a list of errors according to the last chosen interpretation *)
+let clusterize diff (eframe,loc0) =
+  let rec aux = function
+  | [] -> []
+  | (_,choice,_,_ as x)::l0 -> 
+       let matches,others = List.partition (fun (_,c,_,_) -> c = choice) l0 in
+       (choice,List.map (fun (a,_,l,e) -> diff a,l,e) (x::matches)) ::
+               aux others
+  in loc0, aux eframe
+
 let disambiguate_nterm status expty context metasenv subst thing
 =
-  let choices, _ = NCicDisambiguate.disambiguate_term
+  let _,_,thing' = thing in
+  match NCicDisambiguate.disambiguate_term
         status
         ~aliases:status#disambiguate_db.interpr
         ~expty 
@@ -318,21 +341,21 @@ let disambiguate_nterm status expty context metasenv subst thing
         ~mk_implicit ~fix_instance
         ~description_of_alias:GrafiteAst.description_of_alias
         ~context ~metasenv ~subst thing
-  in
-  let _,_,thing' = thing in
-  match choices with
-  | [newast, metasenv, subst, cic] -> 
+  with
+  | Disambiguate.Disamb_success [newast,metasenv,subst,cic,_] ->
       let diff = diff_term Stdpp.dummy_loc thing' newast in
       let status = add_to_interpr status diff 
       in
       metasenv, subst, status, cic
-  | [] -> assert false
-  | _ -> 
+  | Disambiguate.Disamb_success (_::_ as choices) ->
       let diffs = 
-        List.map (fun (ast,_,_,_) -> 
+        List.map (fun (ast,_,_,_,_) -> 
           diff_term Stdpp.dummy_loc thing' ast) choices 
-      in
-      raise (Ambiguous_input (find_diffs diffs))
+      in 
+      raise (Ambiguous_input (find_diffs diffs)) 
+  | Disambiguate.Disamb_failure (l,_) ->
+      raise (Error (List.map (clusterize (diff_term Stdpp.dummy_loc thing')) l))
+  | _ -> assert false
 ;;
 
 type pattern = 
@@ -397,7 +420,7 @@ let disambiguate_nobj status ?baseuri (text,prefix_len,obj as obj') =
      NUri.uri_of_string (baseuri ^ "/" ^ name)
   in
 
-  let choices, _ = NCicDisambiguate.disambiguate_obj
+  match NCicDisambiguate.disambiguate_obj
       status
       ~lookup_in_library:(nlookup_in_library status)
       ~description_of_alias:GrafiteAst.description_of_alias
@@ -406,20 +429,20 @@ let disambiguate_nobj status ?baseuri (text,prefix_len,obj as obj') =
       ~aliases:status#disambiguate_db.interpr
       ~universe:(status#disambiguate_db.multi_aliases) 
       obj'
-  in
-  match choices with
-  | [ast, _, _, cic] -> 
-      let diff = diff_obj Stdpp.dummy_loc obj ast in
-      let status = add_to_interpr status diff
-      in
-      status, cic
-  | [] -> assert false
-  | _ -> 
+  with
+  | Disambiguate.Disamb_success [newast,_,_,cic,_] ->
+      let diff = diff_obj Stdpp.dummy_loc obj newast in
+      let status = add_to_interpr status diff 
+      in status, cic
+  | Disambiguate.Disamb_success (_::_ as choices) ->
       let diffs = 
-        List.map (fun (ast,_,_,_) -> 
+        List.map (fun (ast,_,_,_,_) -> 
           diff_obj Stdpp.dummy_loc obj ast) choices 
       in
-      raise (Ambiguous_input (find_diffs diffs))
+      raise (Ambiguous_input (find_diffs diffs)) 
+  | Disambiguate.Disamb_failure (l,_) -> 
+      raise (Error (List.map (clusterize (diff_obj Stdpp.dummy_loc obj)) l))
+  | _ -> assert false
 ;;
 
 let disambiguate_cic_appl_pattern status args =