]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/cic_disambiguation/disambiguate.ml
- Disambiguation error exception enriched with more information
[helm.git] / helm / software / components / cic_disambiguation / disambiguate.ml
index 352b043a4df4704ff8d6b288efbfca16ac77e418..04357ef92ac1e3e3e52ca48b461ecfcdaad2b662 100644 (file)
@@ -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 *)
@@ -945,7 +948,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 +959,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 +990,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,11 +1011,11 @@ 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
@@ -1019,7 +1023,26 @@ in refine_profiler.HExtlib.profile foo ()
       try
         let res =
          match aux aliases [] None todo_dom base_univ with
-         | [],errors -> raise (NoWellTypedInterpretation (0,errors))
+         | [],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