X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_disambiguation%2Fdisambiguate.ml;h=f3600b7cbc34602ba9e8a433ae853aaf66f4d3b8;hb=36014ac060f150e7d93f607c914a0b06239715c0;hp=352b043a4df4704ff8d6b288efbfca16ac77e418;hpb=79f497094d49963fe9f335e00b58aecc79cbc461;p=helm.git

diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml
index 352b043a4..f3600b7cb 100644
--- a/helm/software/components/cic_disambiguation/disambiguate.ml
+++ b/helm/software/components/cic_disambiguation/disambiguate.ml
@@ -32,7 +32,10 @@ open UriManager
 
 (* the integer is an offset to be added to each location *)
 exception NoWellTypedInterpretation of
- int * ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * Token.flocation option * string Lazy.t) list
+ int *
+ ((Token.flocation list * string * string) list *
+  (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
+  Token.flocation option * string Lazy.t) list
 exception PathNotWellFormed
 
   (** raised when an environment is not enough informative to decide *)
@@ -724,12 +727,12 @@ let domain_of_obj ~context ast =
        List.flatten
         (List.rev_map (fun (_,ty,_,_) -> domain_rev_of_term [] ty) fields) in
       let dom =
-       List.fold_left
-        (fun dom (_,ty) ->
+       List.fold_right
+        (fun (_,ty) dom ->
           match ty with
              None -> dom
-           | Some ty -> domain_rev_of_term [] ty @ dom
-        ) (dom @ domain_rev_of_term [] ty) params
+           | Some ty -> dom @ domain_rev_of_term [] ty
+        ) params (dom @ domain_rev_of_term [] ty)
       in
        List.filter
         (fun (_,name) ->
@@ -863,8 +866,11 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
               match item with
               | Id id -> choices_of_id dbd id
               | Symbol (symb, _) ->
-                  List.map DisambiguateChoices.mk_choice
+                 (try
+                   List.map DisambiguateChoices.mk_choice
                     (TermAcicContent.lookup_interpretations symb)
+                  with
+                   TermAcicContent.Interpretation_not_found -> [])
               | Num instance ->
                   DisambiguateChoices.lookup_num_choices ()
             in
@@ -945,7 +951,8 @@ in refine_profiler.HExtlib.profile foo ()
             (match test_env aliases [] base_univ with
             | Ok (thing, metasenv),new_univ -> 
                [ aliases, diff, metasenv, thing, new_univ ], []
-            | Ko (loc,msg),_ | Uncertain (loc,msg),_ -> [],[diff,loc,msg])
+            | Ko (loc,msg),_
+            | Uncertain (loc,msg),_ -> [],[aliases,diff,loc,msg])
         | (locs,item) :: remaining_dom ->
             debug_print (lazy (sprintf "CHOOSED ITEM: %s"
              (string_of_domain_item item)));
@@ -955,7 +962,7 @@ in refine_profiler.HExtlib.profile foo ()
               | Some choices -> choices in
             match choices with
                [] ->
-                [], [diff,
+                [], [aliases, diff,
                      Some (List.hd locs),
                      lazy ("No choices for " ^ string_of_domain_item item)]
              | [codomain_item] ->
@@ -986,11 +993,11 @@ in refine_profiler.HExtlib.profile foo ()
                             remaining_dom new_univ)
                     | Uncertain (loc,msg),new_univ ->
                         (match remaining_dom with
-                        | [] -> [], [new_diff,loc,msg]
+                        | [] -> [], [new_env,new_diff,loc,msg]
                         | _ ->
                            aux new_env new_diff lookup_in_todo_dom
                             remaining_dom new_univ)
-                    | Ko (loc,msg),_ -> [], [new_diff,loc,msg])
+                    | Ko (loc,msg),_ -> [], [new_env,new_diff,loc,msg])
              | _::_ ->
                let rec filter univ = function 
                 | [] -> [],[]
@@ -1007,19 +1014,44 @@ in refine_profiler.HExtlib.profile foo ()
                           filter univ tl
                     | Uncertain (loc,msg),new_univ ->
                         (match remaining_dom with
-                        | [] -> [],[new_diff,loc,msg]
+                        | [] -> [],[new_env,new_diff,loc,msg]
                         | _ -> aux new_env new_diff None remaining_dom new_univ
                         ) @@ 
                           filter univ tl
-                    | Ko (loc,msg),_ -> ([],[new_diff,loc,msg]) @@ filter univ tl)
+                    | Ko (loc,msg),_ -> ([],[new_env,new_diff,loc,msg]) @@ filter univ tl)
                in
                 filter base_univ choices
       in
+      let aux' aliases diff lookup_in_todo_dom todo_dom base_univ =
+       match test_env aliases todo_dom base_univ with
+        | Ok _,_
+        | Uncertain _,_ ->
+           aux aliases diff lookup_in_todo_dom todo_dom base_univ
+        | Ko (loc,msg),_ -> ([],[aliases,diff,loc,msg]) in
       let base_univ = initial_ugraph in
       try
         let res =
-         match aux aliases [] None todo_dom base_univ with
-         | [],errors -> raise (NoWellTypedInterpretation (0,errors))
+         match aux' aliases [] None todo_dom base_univ with
+         | [],errors ->
+            let errors =
+             List.map
+              (fun (env,diff,loc,msg) ->
+                let env' =
+                 HExtlib.filter_map
+                   (fun (locs,domain_item) ->
+                     try
+                      let description =
+                       fst (Environment.find domain_item env)
+                      in
+                       Some (locs,descr_of_domain_item domain_item,description)
+                     with
+                      Not_found -> None)
+                   thing_dom
+                in
+                 env',diff,loc,msg
+              ) errors
+            in
+             raise (NoWellTypedInterpretation (0,errors))
          | [_,diff,metasenv,t,ugraph],_ ->
              debug_print (lazy "SINGLE INTERPRETATION");
              [diff,metasenv,t,ugraph], false