From: Claudio Sacerdoti Coen Date: Thu, 25 Oct 2007 16:23:06 +0000 (+0000) Subject: 1. More localization: interpretation errors are now loosely localized. X-Git-Tag: make_still_working~5952 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7d4c0852a28f35c6b9f7c56b26421f0ef81dfe1b;p=helm.git 1. More localization: interpretation errors are now loosely localized. 2. Interpretation of pattern matching highly improved: a) missing branches are now detected b) additional branches are now detected c) permutated branches are handled correctly Still to do: d) check that every constructor is given as parameters exactly the number of expected arguments --- diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml index 0b8674c0c..020d038ac 100644 --- a/helm/software/components/cic_disambiguation/disambiguate.ml +++ b/helm/software/components/cic_disambiguation/disambiguate.ml @@ -217,7 +217,7 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~ in do_branch' context args in - let (indtype_uri, indtype_no) = + let indtype_uri, indtype_no = if create_dummy_ids then (UriManager.uri_of_string "cic:/fake_indty.con", 0) else @@ -229,12 +229,12 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~ 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!"))) + raise (Invalid_choice (Some loc, 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 (lazy "The type of the term to be matched is an inductive type without constructors that cannot be determined")) + | [] -> raise (Invalid_choice (Some loc, 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, _, _) -> @@ -243,7 +243,45 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~ 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!"))) + raise (Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!"))) + in + let branches = + match fst(CicEnvironment.get_obj CicUniv.empty_ugraph indtype_uri) with + Cic.InductiveDefinition (il,_,_,_) -> + let _,_,_,cl = + try + List.nth il indtype_no + with _ -> assert false + in + let rec sort branches cl = + match cl with + [] -> + if branches = [] then [] + else + raise (Invalid_choice + (Some loc, + lazy + ("Unrecognized constructors: " ^ + String.concat " " + (List.map (fun ((head,_,_),_) -> head) branches)))) + | (name,_)::cltl -> + let rec find_and_remove = + function + [] -> + raise + (Invalid_choice + (Some loc, lazy ("Missing case: " ^ name))) + | ((name',_,_),_) as branch :: tl when name = name' -> + branch,tl + | branch::tl -> + let found,rest = find_and_remove tl in + found, branch::rest + in + let branch,tl = find_and_remove branches in + branch::sort tl cltl + in + sort branches cl + | _ -> assert false in Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term, (List.map do_branch branches)) @@ -386,7 +424,7 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~ (try List.assoc s ids_to_uris, aux ~localize loc context term with Not_found -> - raise (Invalid_choice (lazy "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on")))) + raise (Invalid_choice (Some loc, 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 @@ -430,10 +468,10 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~ *) t | _ -> - raise (Invalid_choice (lazy "??? Can this happen?")) + raise (Invalid_choice (Some loc, lazy "??? Can this happen?")) with CicEnvironment.CircularDependency _ -> - raise (Invalid_choice (lazy "Circular dependency in the environment")))) + raise (Invalid_choice (None, 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 () @@ -990,7 +1028,7 @@ let foo () = in refine_profiler.HExtlib.profile foo () with | Try_again msg -> Uncertain (None,msg), ugraph - | Invalid_choice msg -> Ko (None,msg), ugraph + | Invalid_choice (loc,msg) -> Ko (loc,msg), ugraph in (* (4) build all possible interpretations *) let (@@) (l1,l2,l3) (l1',l2',l3') = l1@l1', l2@l2', l3@l3' in diff --git a/helm/software/components/cic_disambiguation/disambiguateChoices.ml b/helm/software/components/cic_disambiguation/disambiguateChoices.ml index 64d2cf8e0..c3fa7efb2 100644 --- a/helm/software/components/cic_disambiguation/disambiguateChoices.ml +++ b/helm/software/components/cic_disambiguation/disambiguateChoices.ml @@ -62,7 +62,7 @@ let mk_choice (dsc, args, appl_pattern) = try combine_with_rest names cic_args with Invalid_argument _ -> - raise (Invalid_choice (lazy ("The notation " ^ dsc ^ " expects more arguments"))) + raise (Invalid_choice (None, lazy ("The notation " ^ dsc ^ " expects more arguments"))) in let combined = TermAcicContent.instantiate_appl_pattern env' appl_pattern diff --git a/helm/software/components/cic_disambiguation/disambiguateTypes.ml b/helm/software/components/cic_disambiguation/disambiguateTypes.ml index 150482fbf..1eade4ca0 100644 --- a/helm/software/components/cic_disambiguation/disambiguateTypes.ml +++ b/helm/software/components/cic_disambiguation/disambiguateTypes.ml @@ -40,7 +40,7 @@ type domain_item = | Symbol of string * int (* literal, instance num *) | Num of int (* instance num *) -exception Invalid_choice of string Lazy.t +exception Invalid_choice of Stdpp.location option * string Lazy.t module OrderedDomain = struct diff --git a/helm/software/components/cic_disambiguation/disambiguateTypes.mli b/helm/software/components/cic_disambiguation/disambiguateTypes.mli index 961056701..00fe4114c 100644 --- a/helm/software/components/cic_disambiguation/disambiguateTypes.mli +++ b/helm/software/components/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 of string Lazy.t +exception Invalid_choice of Stdpp.location option * string Lazy.t type codomain_item = string * (* description *) diff --git a/helm/software/components/cic_disambiguation/number_notation.ml b/helm/software/components/cic_disambiguation/number_notation.ml index 781deb90e..78135d9be 100644 --- a/helm/software/components/cic_disambiguation/number_notation.ml +++ b/helm/software/components/cic_disambiguation/number_notation.ml @@ -40,7 +40,7 @@ let _ = (fun _ num _ -> let num = int_of_string num in if num = 0 then - raise (DisambiguateTypes.Invalid_choice (lazy "0 is not a valid positive number")) + raise (DisambiguateTypes.Invalid_choice (None, lazy "0 is not a valid positive number")) else HelmLibraryObjects.build_bin_pos num)); DisambiguateChoices.add_num_choice