Disambiguation errors now carry more information (i.e. the patches to apply to

the current interpretation to re-obtain the refinement errors).

diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml
index 243f7c8bfe22313aa71e0f2643d7c91b28518187..bfeb65d37ea2d39888abb3303026ead0ad5d62e7 100644 (file)
--- a/helm/software/components/cic_disambiguation/disambiguate.ml
+++ b/helm/software/components/cic_disambiguation/disambiguate.ml
@@ -32,7 +32,7 @@ open UriManager
 
 (* the integer is an offset to be added to each location *)
 exception NoWellTypedInterpretation of
- int * (Token.flocation option * string Lazy.t) list
+ int * ((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 +945,7 @@ 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),_ -> [],[loc,msg])
+            | Ko (loc,msg),_ | Uncertain (loc,msg),_ -> [],[diff,loc,msg])
         | (locs,item) :: remaining_dom ->
             debug_print (lazy (sprintf "CHOOSED ITEM: %s"
              (string_of_domain_item item)));
@@ -955,7 +955,8 @@ in refine_profiler.HExtlib.profile foo ()
               | Some choices -> choices in
             match choices with
                [] ->
-                [], [Some (List.hd locs),
+                [], [diff,
+                     Some (List.hd locs),
                      lazy ("No choices for " ^ string_of_domain_item item)]
              | [codomain_item] ->
                  (* just one choice. We perform a one-step look-up and
@@ -985,11 +986,11 @@ in refine_profiler.HExtlib.profile foo ()
                             remaining_dom new_univ)
                     | Uncertain (loc,msg),new_univ ->
                         (match remaining_dom with
-                        | [] -> [], [loc,msg]
+                        | [] -> [], [diff,loc,msg]
                         | _ ->
                            aux new_env new_diff lookup_in_todo_dom
                             remaining_dom new_univ)
-                    | Ko (loc,msg),_ -> [], [loc,msg])
+                    | Ko (loc,msg),_ -> [], [diff,loc,msg])
              | _::_ ->
                let rec filter univ = function 
                 | [] -> [],[]
@@ -1000,17 +1001,17 @@ in refine_profiler.HExtlib.profile foo ()
                     (match test_env new_env remaining_dom univ with
                     | Ok (thing, metasenv),new_univ ->
                         (match remaining_dom with
-                        | [] -> [ new_env, new_diff, metasenv, thing, new_univ ], []
+                        | [] -> [new_env,new_diff,metasenv,thing,new_univ], []
                         | _ -> aux new_env new_diff None remaining_dom new_univ
                         ) @@ 
                           filter univ tl
                     | Uncertain (loc,msg),new_univ ->
                         (match remaining_dom with
-                        | [] -> [],[loc,msg]
+                        | [] -> [],[diff,loc,msg]
                         | _ -> aux new_env new_diff None remaining_dom new_univ
                         ) @@ 
                           filter univ tl
-                    | Ko (loc,msg),_ -> ([],[loc,msg]) @@ filter univ tl)
+                    | Ko (loc,msg),_ -> ([],[diff,loc,msg]) @@ filter univ tl)
                in
                 filter base_univ choices
       in

diff --git a/helm/software/components/cic_disambiguation/disambiguate.mli b/helm/software/components/cic_disambiguation/disambiguate.mli
index e7c6b777fda44e7a228eda88fd7825b97f775bbb..88162df7bfdff900564f179a1008ad97950c68ac 100644 (file)
--- a/helm/software/components/cic_disambiguation/disambiguate.mli
+++ b/helm/software/components/cic_disambiguation/disambiguate.mli
@@ -27,7 +27,7 @@
 
 (* the integer is an offset to be added to each location *)
 exception NoWellTypedInterpretation of
- int * (Token.flocation option * string Lazy.t) list
+ int * ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * Token.flocation option * string Lazy.t) list
 exception PathNotWellFormed
 
 val interpretate_path :

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 9528d45e12f240dc7fd63c09143ecd8e714df5a9..e9dc23328f338fb5b184552638b636bb74e27c3c 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -157,7 +157,7 @@ let disambiguate_tactic
                     metasenv,(GrafiteAst.Type (uri, tyno) :: types)
                 | _ ->
                   raise (GrafiteDisambiguator.DisambiguationError
-                   (0,[[None,lazy "Decompose works only on inductive types"]])))
+                   (0,[[[],None,lazy "Decompose works only on inductive types"]])))
         in
         let metasenv,types =
          List.fold_left disambiguate (metasenv,[]) types

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguator.ml b/helm/software/components/grafite_parser/grafiteDisambiguator.ml
index 181532462b7b370140297ee48a119e7510e30991..ee156674f0a6abe284b21babb08b34467801891f 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguator.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguator.ml
@@ -30,7 +30,8 @@ open Printf
 exception Ambiguous_input
 (* the integer is an offset to be added to each location *)
 exception DisambiguationError of
- int * (Token.flocation option * string Lazy.t) list list
+ int * ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
+ Token.flocation option * string Lazy.t) list list
   (** parameters are: option name, error message *)
 exception Unbound_identifier of string
 

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguator.mli b/helm/software/components/grafite_parser/grafiteDisambiguator.mli
index 52add3974c8304f567f774b6a64c23834e6a3a99..78b0353d8c1b4391d6aed0dc149fe689e9dc7d49 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguator.mli
+++ b/helm/software/components/grafite_parser/grafiteDisambiguator.mli
@@ -28,7 +28,8 @@
 exception Ambiguous_input
 (* the integer is an offset to be added to each location *)
 exception DisambiguationError of
- int * (Token.flocation option * string Lazy.t) list list
+ int * ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
+ Token.flocation option * string Lazy.t) list list
 
 (** initially false; for debugging only (???) *)
 val only_one_pass: bool ref

diff --git a/helm/software/matita/matitaExcPp.ml b/helm/software/matita/matitaExcPp.ml
index 24608be42260bdb5bc3d3c2018b5af7eb9268283..f378e99b0e0c54d65d8528506a71c5a8ce630955 100644 (file)
--- a/helm/software/matita/matitaExcPp.ml
+++ b/helm/software/matita/matitaExcPp.ml
@@ -71,7 +71,7 @@ let rec to_string =
        | phase::tl ->
           let msg =
            String.concat "\n\n\n"
-            (List.map (fun (floc,msg) ->
+            (List.map (fun (_,floc,msg) ->
               let loc_descr =
                match floc with
                   None -> ""
@@ -88,7 +88,7 @@ let rec to_string =
              (aux (n+1) (msg,[n]) tl) in
      let loc =
       match errorll with
-         ((Some floc,_)::_)::_ ->
+         ((_,Some floc,_)::_)::_ ->
           let (x, y) = HExtlib.loc_of_floc floc in
           let x = x + offset in
           let y = y + offset in