From 5e4deb64b7cae2df0a51425e3768ca316c297953 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 18 Oct 2006 15:06:03 +0000 Subject: [PATCH] - Disambiguation error exception enriched with more information (the same returned in case of correct disambiguation) - The disambiguation error interface now shows the complete environment in which the error occurs. I am not sure if this is better or worst than showing only the diffs. --- components/cic_disambiguation/disambiguate.ml | 39 +++++++++++++++---- .../cic_disambiguation/disambiguate.mli | 5 ++- .../grafite_parser/grafiteDisambiguate.ml | 2 +- .../grafite_parser/grafiteDisambiguator.ml | 6 ++- .../grafite_parser/grafiteDisambiguator.mli | 7 +++- matita/matitaExcPp.ml | 4 +- matita/matitaGui.ml | 37 ++++++++---------- 7 files changed, 63 insertions(+), 37 deletions(-) diff --git a/components/cic_disambiguation/disambiguate.ml b/components/cic_disambiguation/disambiguate.ml index 352b043a4..04357ef92 100644 --- a/components/cic_disambiguation/disambiguate.ml +++ b/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 *) @@ -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 diff --git a/components/cic_disambiguation/disambiguate.mli b/components/cic_disambiguation/disambiguate.mli index 88162df7b..4a8f90b00 100644 --- a/components/cic_disambiguation/disambiguate.mli +++ b/components/cic_disambiguation/disambiguate.mli @@ -27,7 +27,10 @@ (* 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 val interpretate_path : diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml index e9dc23328..9a4cb472d 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 ee156674f..2c38dd8a9 100644 --- a/components/grafite_parser/grafiteDisambiguator.ml +++ b/components/grafite_parser/grafiteDisambiguator.ml @@ -30,8 +30,10 @@ open Printf exception Ambiguous_input (* the integer is an offset to be added to each location *) exception DisambiguationError of - int * ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * - Token.flocation option * string Lazy.t) list list + int * + ((Token.flocation list * string * string) list * + (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 78b0353d8..1b63690d7 100644 --- a/components/grafite_parser/grafiteDisambiguator.mli +++ b/components/grafite_parser/grafiteDisambiguator.mli @@ -28,8 +28,11 @@ exception Ambiguous_input (* the integer is an offset to be added to each location *) exception DisambiguationError of - int * ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * - Token.flocation option * string Lazy.t) list list + int * + ((Token.flocation list * string * string) list * + (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * + Token.flocation option * string Lazy.t) list list + (** parameters are: option name, error message *) (** initially false; for debugging only (???) *) val only_one_pass: bool ref diff --git a/matita/matitaExcPp.ml b/matita/matitaExcPp.ml index f378e99b0..a314556bd 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 diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml index ec9cea531..50c55619e 100644 --- a/matita/matitaGui.ml +++ b/matita/matitaGui.ml @@ -150,26 +150,27 @@ class interpErrorModel = let idx = ref 0 in fun interp -> try - List.assoc "0" interp + let _,_,y = List.find (fun (_,x,y) -> x="0") interp in y with Not_found -> incr idx; string_of_int !idx in tree_store#clear (); let idx = ref ~-1 in List.iter - (fun _,interp,_,_ -> + (fun pass,env,_,_,_ -> incr idx; let interp_row = tree_store#append () in tree_store#set ~row:interp_row ~column:id_col - (name_of_interp interp); + ("Pass " ^ string_of_int pass ^ + "; Interpretation " ^ name_of_interp env); tree_store#set ~row:interp_row ~column:interp_no_col !idx; List.iter - (fun (id, dsc) -> + (fun (_, id, dsc) -> let row = tree_store#append ~parent:interp_row () in tree_store#set ~row ~column:id_col id; tree_store#set ~row ~column:dsc_col dsc; tree_store#set ~row ~column:interp_no_col !idx) - interp) + env) choices method get_interp_no tree_path = @@ -184,21 +185,15 @@ let rec interactive_error_interp ?(all_passes=false) source_buffer notify_exn let errorll' = if all_passes then errorll else List.rev (List.tl (List.tl (List.rev errorll))) in let choices = + let pass = ref 0 in List.flatten (List.map - (List.map - (fun (choices,offset,msg) -> - let textual_choices = - List.map - (fun (dom,(descr,_)) -> - DisambiguateTypes.string_of_domain_item dom, descr - ) choices - in - choices, textual_choices, offset, msg - ) + (fun l -> + incr pass; + List.map (fun (env,diff,offset,msg) -> !pass, env, diff, offset, msg) l ) errorll') in - let choices_eq (_,c1,_,_) (_,c2,_,_) = c1 = c2 in - let choices_compare (_,c1,_,_) (_,c2,_,_) = compare c1 c2 in + let choices_eq (_,e1,_,_,_) (_,e2,_,_,_) = e1 = e2 in + let choices_compare (_,e1,_,_,_) (_,e2,_,_,_) = compare e1 e2 in (* Here we are doing a stable sort and list_uniq returns the latter "equal" element. I.e. we are showing the error corresponding to the most advanced disambiguation pass *) @@ -208,10 +203,10 @@ let rec interactive_error_interp ?(all_passes=false) source_buffer notify_exn in match choices with [] -> assert false - | [interp,_,loffset,msg] -> + | [_,env,diff,loffset,msg] -> notify_exn (GrafiteDisambiguator.DisambiguationError - (offset,[[interp,loffset,msg]])); + (offset,[[env,diff,loffset,msg]])); | _::_ -> let dialog = new disambiguationErrors () in dialog#check_widgets (); @@ -226,7 +221,7 @@ let rec interactive_error_interp ?(all_passes=false) source_buffer notify_exn None -> assert false | Some tp -> tp in let idx = model#get_interp_no tree_path in - let interp,_,loffset,msg = List.nth choices idx in + let _,env,diff,loffset,msg = List.nth choices idx in let script = MatitaScript.current () in let error_tag = script#error_tag in source_buffer#remove_tag error_tag @@ -234,7 +229,7 @@ let rec interactive_error_interp ?(all_passes=false) source_buffer notify_exn ~stop:source_buffer#end_iter; notify_exn (GrafiteDisambiguator.DisambiguationError - (offset,[[interp,loffset,msg]])) + (offset,[[env,diff,loffset,msg]])) )); let return _ = dialog#disambiguationErrors#destroy (); -- 2.39.2