From 2bb6c98121db82a1c67565bb528787f2def7192d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 19 Nov 2005 15:02:08 +0000 Subject: [PATCH] Disambiguation errors are no longer thrown away. They are now collected and presented (in a not understandable way) to the user. --- helm/matita/.depend | 6 +- helm/matita/Makefile.in | 6 +- helm/matita/matitaDisambiguator.ml | 14 +++- helm/matita/matitaDisambiguator.mli | 1 + helm/matita/matitaEngine.ml | 2 +- helm/matita/matitaExcPp.ml | 11 +++ helm/ocaml/cic_disambiguation/disambiguate.ml | 80 ++++++++++--------- .../ocaml/cic_disambiguation/disambiguate.mli | 2 +- .../cic_disambiguation/disambiguateChoices.ml | 3 +- .../cic_disambiguation/disambiguateTypes.ml | 2 +- .../cic_disambiguation/disambiguateTypes.mli | 2 +- .../cic_disambiguation/number_notation.ml | 2 +- 12 files changed, 80 insertions(+), 51 deletions(-) diff --git a/helm/matita/.depend b/helm/matita/.depend index a531aed7b..ff2e6c935 100644 --- a/helm/matita/.depend +++ b/helm/matita/.depend @@ -30,8 +30,10 @@ matitaEngine.cmo: matitacleanLib.cmi matitaTypes.cmi matitaSync.cmi \ matitaEngine.cmx: matitacleanLib.cmx matitaTypes.cmx matitaSync.cmx \ matitaMoo.cmx matitaMisc.cmx matitaLog.cmx matitaDisambiguator.cmx \ matitaDb.cmx matitaEngine.cmi -matitaExcPp.cmo: matitaTypes.cmi matitaMoo.cmi matitaExcPp.cmi -matitaExcPp.cmx: matitaTypes.cmx matitaMoo.cmx matitaExcPp.cmi +matitaExcPp.cmo: matitaTypes.cmi matitaMoo.cmi matitaDisambiguator.cmi \ + matitaExcPp.cmi +matitaExcPp.cmx: matitaTypes.cmx matitaMoo.cmx matitaDisambiguator.cmx \ + matitaExcPp.cmi matitaGeneratedGui.cmo: matitaGeneratedGui.cmi matitaGeneratedGui.cmx: matitaGeneratedGui.cmi matitaGtkMisc.cmo: matitaTypes.cmi matitaGeneratedGui.cmi matitaGtkMisc.cmi diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index c489fe33d..127f8a407 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -39,14 +39,14 @@ CMOS = \ matitaLog.cmo \ matitaTypes.cmo \ matitaMoo.cmo \ - matitaExcPp.cmo \ matitaMisc.cmo \ matitaDb.cmo \ matitamakeLib.cmo \ matitaInit.cmo \ matitaSync.cmo \ - matitacleanLib.cmo \ matitaDisambiguator.cmo \ + matitaExcPp.cmo \ + matitacleanLib.cmo \ matitaEngine.cmo \ matitacLib.cmo \ matitaScript.cmo \ @@ -61,13 +61,13 @@ CCMOS = \ matitaLog.cmo \ matitaTypes.cmo \ matitaMoo.cmo \ - matitaExcPp.cmo \ matitaMisc.cmo \ matitaDb.cmo \ matitamakeLib.cmo \ matitaInit.cmo \ matitaSync.cmo \ matitaDisambiguator.cmo \ + matitaExcPp.cmo \ matitacleanLib.cmo \ matitaEngine.cmo \ matitacLib.cmo \ diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml index 22819536f..24a835523 100644 --- a/helm/matita/matitaDisambiguator.ml +++ b/helm/matita/matitaDisambiguator.ml @@ -28,6 +28,7 @@ open Printf open MatitaTypes exception Ambiguous_input +exception DisambiguationError of string Lazy.t list list type choose_uris_callback = id:string -> UriManager.uri list -> UriManager.uri list @@ -103,18 +104,23 @@ let disambiguate_thing ~aliases ~universe else drop_aliases_and_clear_diff res in - let rec aux = + let rec aux errors = function - | [ pass ] -> set_aliases pass (try_pass pass) + | [ pass ] -> + (try + set_aliases pass (try_pass pass) + with Disambiguate.NoWellTypedInterpretation newerrors -> + raise (DisambiguationError (errors @ [newerrors]))) | hd :: tl -> (try set_aliases hd (try_pass hd) - with Disambiguate.NoWellTypedInterpretation -> aux tl) + with Disambiguate.NoWellTypedInterpretation newerrors -> + aux (errors @ [newerrors]) tl) | [] -> assert false in let saved_use_coercions = !CoercDb.use_coercions in try - let res = aux passes in + let res = aux [] passes in CoercDb.use_coercions := saved_use_coercions; res with exn -> diff --git a/helm/matita/matitaDisambiguator.mli b/helm/matita/matitaDisambiguator.mli index 01fa97ef0..7e207e12f 100644 --- a/helm/matita/matitaDisambiguator.mli +++ b/helm/matita/matitaDisambiguator.mli @@ -28,6 +28,7 @@ open MatitaTypes (** raised when ambiguous input is found but not expected (e.g. in the batch * compiler) *) exception Ambiguous_input +exception DisambiguationError of string Lazy.t list list type choose_uris_callback = id:string -> UriManager.uri list -> UriManager.uri list type choose_interp_callback = (string * string) list list -> int list diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 503d4a06a..bf39a1cac 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -253,7 +253,7 @@ let disambiguate_tactic status goal tactic = with | Cic.MutInd (uri, tyno, _) -> (GrafiteAst.Type (uri, tyno) :: types) - | _ -> raise Disambiguate.NoWellTypedInterpretation) + | _ -> raise (MatitaDisambiguator.DisambiguationError [[lazy "Decompose works only on inductive types"]])) in let types = List.fold_left disambiguate [] types in GrafiteAst.Decompose (loc, types, what, names) diff --git a/helm/matita/matitaExcPp.ml b/helm/matita/matitaExcPp.ml index 6dccc429f..a5a2f4d86 100644 --- a/helm/matita/matitaExcPp.ml +++ b/helm/matita/matitaExcPp.ml @@ -55,5 +55,16 @@ let to_string = "Type checking error: " ^ Lazy.force msg | CicTypeChecker.AssertFailure msg -> "Type checking assertion failed: " ^ Lazy.force msg + | MatitaDisambiguator.DisambiguationError errorll -> + let rec aux n = + function + [] -> "" + | phase::tl -> + aux (n+1) tl ^ + "Errors obtained during phase " ^ string_of_int n ^":\n" ^ + String.concat "\n" (List.map Lazy.force phase) ^ "\n" ^ "\n" + in + "DISAMBIGUATION ERROR:\n" ^ + aux 1 errorll | exn -> "Uncaught exception: " ^ Printexc.to_string exn diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index 4aae8515e..c8016c0ba 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -29,11 +29,11 @@ open DisambiguateTypes open UriManager exception No_choices of domain_item -exception NoWellTypedInterpretation +exception NoWellTypedInterpretation of string Lazy.t list exception PathNotWellFormed (** raised when an environment is not enough informative to decide *) -exception Try_again +exception Try_again of string Lazy.t type aliases = bool * DisambiguateTypes.environment @@ -56,8 +56,8 @@ let descr_of_domain_item = function type 'a test_result = | Ok of 'a * Cic.metasenv - | Ko - | Uncertain + | Ko of string Lazy.t + | Uncertain of string Lazy.t let refine_term metasenv context uri term ugraph = (* if benchmark then incr actual_refinements; *) @@ -70,11 +70,11 @@ let refine_term metasenv context uri term ugraph = with | CicRefine.Uncertain s -> debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force s) ^ "] " ^ CicPp.ppterm term)) ; - Uncertain,ugraph + Uncertain s,ugraph | CicRefine.RefineFailure msg -> debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" (CicPp.ppterm term) (Lazy.force msg))); - Ko,ugraph + Ko msg,ugraph let refine_obj metasenv context uri obj ugraph = assert (context = []); @@ -85,11 +85,11 @@ let refine_obj metasenv context uri obj ugraph = with | CicRefine.Uncertain s -> debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force s) ^ "] " ^ CicPp.ppobj obj)) ; - Uncertain,ugraph + Uncertain s,ugraph | CicRefine.RefineFailure msg -> debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" (CicPp.ppobj obj) (Lazy.force msg))) ; - Ko,ugraph + Ko msg,ugraph let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () = try @@ -149,21 +149,27 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast = let (indtype_uri, indtype_no) = match indty_ident with | Some (indty_ident, _) -> - (match resolve env (Id indty_ident) () with + (match resolve env (Id indty_ident) () with | Cic.MutInd (uri, tyno, _) -> (uri, tyno) - | Cic.Implicit _ -> raise Try_again - | _ -> raise Invalid_choice) + | Cic.Implicit _ -> + raise (Try_again (lazy "The type of the term to be matched + is still unknown")) + | _ -> + raise (Invalid_choice (lazy "The type of the term to be matched is not (co)inductive!"))) | None -> let fst_constructor = match branches with | ((head, _, _), _) :: _ -> head - | [] -> raise Invalid_choice + | [] -> raise (Invalid_choice (lazy "The type of the term to be matched is an inductive type without constructors that cannot be determined")) in (match resolve env (Id fst_constructor) () with | Cic.MutConstruct (indtype_uri, indtype_no, _, _) -> (indtype_uri, indtype_no) - | Cic.Implicit _ -> raise Try_again - | _ -> raise Invalid_choice) + | Cic.Implicit _ -> + raise (Try_again (lazy "The type of the term to be matched + is still unknown")) + | _ -> + raise (Invalid_choice (lazy "The type of the term to be matched is not (co)inductive!"))) in Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term, (List.map do_branch branches)) @@ -263,7 +269,7 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast = (try List.assoc s ids_to_uris, aux loc context term with Not_found -> - raise Invalid_choice)) + raise (Invalid_choice (lazy "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on")))) subst | None -> List.map (fun uri -> uri, Cic.Implicit None) uris) in @@ -307,10 +313,10 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast = *) t | _ -> - raise Invalid_choice + raise (Invalid_choice (lazy "??? Can this happen?")) with CicEnvironment.CircularDependency _ -> - raise Invalid_choice)) + raise (Invalid_choice (lazy "Circular dependency in the environment")))) | CicNotationPt.Implicit -> Cic.Implicit None | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole) | CicNotationPt.Num (num, i) -> resolve env (Num i) ~num () @@ -793,18 +799,19 @@ let foo () = (k , ugraph1 ) in refine_profiler.HExtlib.profile foo () with - | Try_again -> Uncertain, ugraph - | Invalid_choice -> Ko, ugraph + | Try_again msg -> Uncertain msg, ugraph + | Invalid_choice msg -> Ko msg, ugraph in (* (4) build all possible interpretations *) + let (@@) (l1,l2) (l1',l2') = l1@l1, l2@l2' in let rec aux aliases diff lookup_in_todo_dom todo_dom base_univ = match todo_dom with | [] -> assert (lookup_in_todo_dom = None); (match test_env aliases [] base_univ with | Ok (thing, metasenv),new_univ -> - [ aliases, diff, metasenv, thing, new_univ ] - | Ko,_ | Uncertain,_ -> []) + [ aliases, diff, metasenv, thing, new_univ ], [] + | Ko msg,_ | Uncertain msg,_ -> [],[msg]) | item :: remaining_dom -> debug_print (lazy (sprintf "CHOOSED ITEM: %s" (string_of_domain_item item))); @@ -813,7 +820,7 @@ in refine_profiler.HExtlib.profile foo () None -> lookup_choices item | Some choices -> choices in match choices with - [] -> [] + [] -> [], [lazy "No choices"] | [codomain_item] -> (* just one choice. We perform a one-step look-up and if the next set of choices is also a singleton we @@ -835,20 +842,21 @@ in refine_profiler.HExtlib.profile foo () (match test_env new_env remaining_dom base_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 lookup_in_todo_dom remaining_dom new_univ) - | Uncertain,new_univ -> + | Uncertain msg,new_univ -> (match remaining_dom with - | [] -> [] + | [] -> [], [msg] | _ -> aux new_env new_diff lookup_in_todo_dom remaining_dom new_univ) - | Ko,_ -> []) + | Ko msg,_ -> [], [msg]) | _::_ -> let rec filter univ = function - | [] -> [] + | [] -> [],[] | codomain_item :: tl -> debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item))); let new_env = Environment.add item codomain_item aliases in @@ -856,17 +864,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,new_univ -> + | Uncertain msg,new_univ -> (match remaining_dom with - | [] -> [] + | [] -> [],[msg] | _ -> aux new_env new_diff None remaining_dom new_univ - ) @ + ) @@ filter univ tl - | Ko,_ -> filter univ tl) + | Ko msg,_ -> ([],[msg]) @@ filter univ tl) in filter base_univ choices in @@ -874,11 +882,11 @@ in refine_profiler.HExtlib.profile foo () try let res = match aux aliases [] None todo_dom base_univ with - | [] -> raise NoWellTypedInterpretation - | [_,diff,metasenv,t,ugraph] -> + | [],errors -> raise (NoWellTypedInterpretation errors) + | [_,diff,metasenv,t,ugraph],_ -> debug_print (lazy "SINGLE INTERPRETATION"); [diff,metasenv,t,ugraph], false - | l -> + | l,_ -> debug_print (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l))); let choices = List.map diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli index 5b0e0da1e..e8d21c0cd 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.mli +++ b/helm/ocaml/cic_disambiguation/disambiguate.mli @@ -25,7 +25,7 @@ (** {2 Disambiguation interface} *) -exception NoWellTypedInterpretation +exception NoWellTypedInterpretation of string Lazy.t list exception PathNotWellFormed val interpretate_path : diff --git a/helm/ocaml/cic_disambiguation/disambiguateChoices.ml b/helm/ocaml/cic_disambiguation/disambiguateChoices.ml index c660bb6b0..b7f241036 100644 --- a/helm/ocaml/cic_disambiguation/disambiguateChoices.ml +++ b/helm/ocaml/cic_disambiguation/disambiguateChoices.ml @@ -51,7 +51,8 @@ let mk_choice (dsc, args, appl_pattern) = in try List.combine names cic_args - with Invalid_argument _ -> raise Invalid_choice + with Invalid_argument _ -> + raise (Invalid_choice (lazy "The notation expects a different number of arguments")) in CicNotationFwd.instantiate_appl_pattern env' appl_pattern) diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml index a3c7c82c6..b323f9231 100644 --- a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml +++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml @@ -36,7 +36,7 @@ type domain_item = | Symbol of string * int (* literal, instance num *) | Num of int (* instance num *) -exception Invalid_choice +exception Invalid_choice of string Lazy.t module OrderedDomain = struct diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli index 7f955d673..4d077f2f8 100644 --- a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli +++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli @@ -41,7 +41,7 @@ end (** to be raised when a choice is invalid due to some given parameter (e.g. * wrong number of Cic.term arguments received) *) -exception Invalid_choice +exception Invalid_choice of string Lazy.t type codomain_item = string * (* description *) diff --git a/helm/ocaml/cic_disambiguation/number_notation.ml b/helm/ocaml/cic_disambiguation/number_notation.ml index 7ce0ec0a0..09f488e86 100644 --- a/helm/ocaml/cic_disambiguation/number_notation.ml +++ b/helm/ocaml/cic_disambiguation/number_notation.ml @@ -38,7 +38,7 @@ let _ = (fun _ num _ -> let num = int_of_string num in if num = 0 then - raise DisambiguateTypes.Invalid_choice + raise (DisambiguateTypes.Invalid_choice (lazy "0 is not a valid positive number")) else HelmLibraryObjects.build_bin_pos num)); DisambiguateChoices.add_num_choice -- 2.39.2