From: Claudio Sacerdoti Coen Date: Wed, 18 Oct 2006 12:11:48 +0000 (+0000) Subject: Disambiguation errors now carry more information (i.e. the patches to apply to X-Git-Tag: 0.4.95@7852~884 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9dec56b0dcc55853244fa5ca401c1c19dac3d9d2;p=helm.git 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/components/cic_disambiguation/disambiguate.ml b/components/cic_disambiguation/disambiguate.ml index 243f7c8bf..bfeb65d37 100644 --- a/components/cic_disambiguation/disambiguate.ml +++ b/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/components/cic_disambiguation/disambiguate.mli b/components/cic_disambiguation/disambiguate.mli index e7c6b777f..88162df7b 100644 --- a/components/cic_disambiguation/disambiguate.mli +++ b/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/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml index 9528d45e1..e9dc23328 100644 --- a/components/grafite_parser/grafiteDisambiguate.ml +++ b/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/components/grafite_parser/grafiteDisambiguator.ml b/components/grafite_parser/grafiteDisambiguator.ml index 181532462..ee156674f 100644 --- a/components/grafite_parser/grafiteDisambiguator.ml +++ b/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/components/grafite_parser/grafiteDisambiguator.mli b/components/grafite_parser/grafiteDisambiguator.mli index 52add3974..78b0353d8 100644 --- a/components/grafite_parser/grafiteDisambiguator.mli +++ b/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/matita/matitaExcPp.ml b/matita/matitaExcPp.ml index 24608be42..f378e99b0 100644 --- a/matita/matitaExcPp.ml +++ b/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