diff options
| -rw-r--r-- | kernel/indtypes.ml | 8 | ||||
| -rw-r--r-- | kernel/indtypes.mli | 2 | ||||
| -rw-r--r-- | lib/util.ml | 16 | ||||
| -rw-r--r-- | lib/util.mli | 7 | ||||
| -rw-r--r-- | pretyping/indrec.ml | 8 | ||||
| -rw-r--r-- | pretyping/indrec.mli | 2 | ||||
| -rw-r--r-- | toplevel/command.ml | 11 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 448 |
8 files changed, 248 insertions, 254 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index e8f9dbc32..600d4bfa4 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -39,7 +39,7 @@ type inductive_error = | NotConstructor of env * constr * constr | NonPar of env * constr * int * constr * constr | SameNamesTypes of identifier - | SameNamesConstructors of identifier * identifier + | SameNamesConstructors of identifier | SameNamesOverlap of identifier list | NotAnArity of identifier | BadEntry @@ -51,12 +51,12 @@ exception InductiveError of inductive_error of names. The name [id] is the name of the current inductive type, used when reporting the error. *) -let check_constructors_names id = +let check_constructors_names = let rec check idset = function | [] -> idset | c::cl -> if Idset.mem c idset then - raise (InductiveError (SameNamesConstructors (id,c))) + raise (InductiveError (SameNamesConstructors c)) else check (Idset.add c idset) cl in @@ -75,7 +75,7 @@ let mind_check_names mie = if Idset.mem id indset then raise (InductiveError (SameNamesTypes id)) else - let cstset' = check_constructors_names id cstset cl in + let cstset' = check_constructors_names cstset cl in check (Idset.add id indset) cstset' inds in check Idset.empty Idset.empty mie.mind_entry_inds diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 05534ec36..620cbf580 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -29,7 +29,7 @@ type inductive_error = | NotConstructor of env * constr * constr | NonPar of env * constr * int * constr * constr | SameNamesTypes of identifier - | SameNamesConstructors of identifier * identifier + | SameNamesConstructors of identifier | SameNamesOverlap of identifier list | NotAnArity of identifier | BadEntry diff --git a/lib/util.ml b/lib/util.ml index 8b3fb2428..a1c011ce1 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -101,6 +101,10 @@ let string_string_contains ~where ~what = let plural n s = if n>1 then s^"s" else s +let ordinal n = + let s = match n mod 10 with 1 -> "st" | 2 -> "nd" | 3 -> "rd" | _ -> "th" in + string_of_int n ^ s + (* string parsing *) let parse_loadpath s = @@ -325,6 +329,12 @@ let rec list_distinct l = | [] -> true in loop l +let rec list_duplicates = function + | [] -> [] + | x::l -> + let l' = list_duplicates l in + if List.mem x l then list_add_set x l' else l' + let rec list_filter2 f = function | [], [] as p -> p | d::dp, l::lp -> @@ -802,9 +812,7 @@ let pr_bar () = str "|" ++ spc () let pr_arg pr x = spc () ++ pr x let pr_opt pr = function None -> mt () | Some x -> pr_arg pr x -let pr_ord n = - let suff = match n mod 10 with 1 -> "st" | 2 -> "nd" | _ -> "th" in - int n ++ str suff +let nth n = str (ordinal n) let rec prlist elem l = match l with | [] -> mt () @@ -842,6 +850,8 @@ let prvect_with_sep sep elem v = let n = Array.length v in if n = 0 then mt () else pr (n - 1) +let prvect elem v = prvect_with_sep mt elem v + let surround p = hov 1 (str"(" ++ p ++ str")") (*s Size of ocaml values. *) diff --git a/lib/util.mli b/lib/util.mli index 8a406519e..5c5970821 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -69,6 +69,7 @@ val implode : string list -> string val string_index_from : string -> int -> string -> int val string_string_contains : where:string -> what:string -> bool val plural : int -> string -> string +val ordinal : int -> string val parse_loadpath : string -> string list @@ -89,6 +90,7 @@ val list_chop : int -> 'a list -> 'a list * 'a list val list_tabulate : (int -> 'a) -> int -> 'a list val list_assign : 'a list -> int -> 'a -> 'a list val list_distinct : 'a list -> bool +val list_duplicates : 'a list -> 'a list val list_filter2 : ('a -> 'b -> bool) -> 'a list * 'b list -> 'a list * 'b list (* [list_smartmap f [a1...an] = List.map f [a1...an]] but if for all i @@ -232,14 +234,15 @@ val pr_str : string -> std_ppcmds val pr_coma : unit -> std_ppcmds val pr_semicolon : unit -> std_ppcmds val pr_bar : unit -> std_ppcmds -val pr_ord : int -> std_ppcmds val pr_arg : ('a -> std_ppcmds) -> 'a -> std_ppcmds val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds +val nth : int -> std_ppcmds val prlist : ('a -> std_ppcmds) -> 'a list -> std_ppcmds -val prvecti : (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds val prlist_with_sep : (unit -> std_ppcmds) -> ('b -> std_ppcmds) -> 'b list -> std_ppcmds +val prvect : ('a -> std_ppcmds) -> 'a array -> std_ppcmds +val prvecti : (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds val prvect_with_sep : (unit -> std_ppcmds) -> ('b -> std_ppcmds) -> 'b array -> std_ppcmds val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 7fd65050c..84f35241a 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -31,7 +31,7 @@ open Sign type recursion_scheme_error = | NotAllowedCaseAnalysis of bool * sorts * inductive | BadInduction of bool * identifier * sorts - | NotMutualInScheme + | NotMutualInScheme of inductive * inductive exception RecursionSchemeError of recursion_scheme_error @@ -501,13 +501,13 @@ let instantiate_type_indrec_scheme sort npars term = let check_arities listdepkind = let _ = List.fold_left - (fun ln ((_,ni),mibi,mipi,dep,kind) -> + (fun ln ((_,ni as mind),mibi,mipi,dep,kind) -> let id = mipi.mind_typename in let kelim = elim_sorts (mibi,mipi) in if not (List.exists ((=) kind) kelim) then raise (RecursionSchemeError (BadInduction (dep,id,new_sort_in_family kind))) else if List.mem ni ln then raise - (RecursionSchemeError NotMutualInScheme) + (RecursionSchemeError (NotMutualInScheme (mind,mind))) else ni::ln) [] listdepkind in true @@ -524,7 +524,7 @@ let build_mutual_indrec env sigma = function let (mibi',mipi') = lookup_mind_specif env mind' in (mind',mibi',mipi',dep',s') else - raise (RecursionSchemeError NotMutualInScheme)) + raise (RecursionSchemeError (NotMutualInScheme (mind,mind')))) lrecspec) in let _ = check_arities listdepkind in diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli index f0f7747cb..b172935f5 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.mli @@ -22,7 +22,7 @@ open Evd type recursion_scheme_error = | NotAllowedCaseAnalysis of bool * sorts * inductive | BadInduction of bool * identifier * sorts - | NotMutualInScheme + | NotMutualInScheme of inductive * inductive exception RecursionSchemeError of recursion_scheme_error diff --git a/toplevel/command.ml b/toplevel/command.ml index f0a9792fd..6fd56536b 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -295,9 +295,14 @@ let minductive_message = function spc () ++ str "are defined") let check_all_names_different indl = - let get_names ind = ind.ind_name::List.map fst ind.ind_lc in - if not (list_distinct (List.flatten (List.map get_names indl))) then - error "Two inductive objects have the same name" + let ind_names = List.map (fun ind -> ind.ind_name) indl in + let cstr_names = list_map_append (fun ind -> List.map fst ind.ind_lc) indl in + let l = list_duplicates ind_names in + if l <> [] then raise (InductiveError (SameNamesTypes (List.hd l))); + let l = list_duplicates cstr_names in + if l <> [] then raise (InductiveError (SameNamesConstructors (List.hd l))); + let l = list_intersect ind_names cstr_names in + if l <> [] then raise (InductiveError (SameNamesOverlap l)) let mk_mltype_data isevars env assums arity indname = let is_ml_type = is_sort env (Evd.evars_of !isevars) arity in diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 49a1d07f7..7e45efe94 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -34,44 +34,40 @@ let pr_lconstr_env e c = quote (pr_lconstr_env e c) let pr_lconstr_env_at_top e c = quote (pr_lconstr_env_at_top e c) let pr_ljudge_env e c = let v,t = pr_ljudge_env e c in (quote v,quote t) -let nth i = - let many = match i mod 10 with 1 -> "st" | 2 -> "nd" | _ -> "th" in - int i ++ str many - let pr_db env i = try match lookup_rel i env with Name id, _, _ -> pr_id id - | Anonymous, _, _ -> str"<>" - with Not_found -> str"UNBOUND_REL_"++int i + | Anonymous, _, _ -> str "<>" + with Not_found -> str "UNBOUND_REL_" ++ int i let explain_unbound_rel env n = let pe = pr_ne_context_of (str "In environment") env in - str"Unbound reference: " ++ pe ++ - str"The reference " ++ int n ++ str " is free" + str "Unbound reference: " ++ pe ++ + str "The reference " ++ int n ++ str " is free." let explain_unbound_var env v = let var = pr_id v in - str"No such section variable or assumption : " ++ var + str "No such section variable or assumption: " ++ var ++ str "." let explain_not_type env j = - let pe = pr_ne_context_of (str"In environment") env in + let pe = pr_ne_context_of (str "In environment") env in let pc,pt = pr_ljudge_env env j in - pe ++ str "the term" ++ brk(1,1) ++ pc ++ spc () ++ - str"has type" ++ spc () ++ pt ++ spc () ++ - str"which should be Set, Prop or Type." + pe ++ str "The term" ++ brk(1,1) ++ pc ++ spc () ++ + str "has type" ++ spc () ++ pt ++ spc () ++ + str "which should be Set, Prop or Type." let explain_bad_assumption env j = - let pe = pr_ne_context_of (str"In environment") env in + let pe = pr_ne_context_of (str "In environment") env in let pc,pt = pr_ljudge_env env j in - pe ++ str "cannot declare a variable or hypothesis over the term" ++ - brk(1,1) ++ pc ++ spc () ++ str"of type" ++ spc () ++ pt ++ spc () ++ + pe ++ str "Cannot declare a variable or hypothesis over the term" ++ + brk(1,1) ++ pc ++ spc () ++ str "of type" ++ spc () ++ pt ++ spc () ++ str "because this term is not a type." let explain_reference_variables c = let pc = pr_lconstr c in - str "the constant" ++ spc () ++ pc ++ spc () ++ - str "refers to variables which are not in the context" + str "The constant" ++ spc () ++ pc ++ spc () ++ + str "refers to variables which are not in the context." let rec pr_disjunction pr = function | [a] -> pr a @@ -79,7 +75,7 @@ let rec pr_disjunction pr = function | a::l -> pr a ++ str "," ++ spc () ++ pr_disjunction pr l | [] -> assert false -let explain_elim_arity env ind sorts c pj okinds = +let explain_elim_arity env ind sorts c pj okinds = let env = make_all_name_different env in let pi = pr_inductive env ind in let pc = pr_lconstr_env env c in @@ -91,26 +87,26 @@ let explain_elim_arity env ind sorts c pj okinds = | NonInformativeToInformative -> "proofs can be eliminated only to build proofs" | StrongEliminationOnNonSmallType -> - "strong elimination on non-small inductive types leads to paradoxes." + "strong elimination on non-small inductive types leads to paradoxes" | WrongArity -> "wrong arity" in let ppar = pr_disjunction (fun s -> quote (pr_sort_family s)) sorts in let ppt = pr_lconstr_env env (snd (decompose_prod_assum pj.uj_type)) in - hov 0 - (str "the return type has sort" ++ spc() ++ ppt ++ spc() ++ - str "while it" ++ spc() ++ str "should be " ++ ppar ++ str ".") ++ - fnl() ++ + hov 0 + (str "the return type has sort" ++ spc () ++ ppt ++ spc () ++ + str "while it" ++ spc () ++ str "should be " ++ ppar ++ str ".") ++ + fnl () ++ hov 0 (str "Elimination of an inductive object of sort " ++ pki ++ brk(1,0) ++ - str "is not allowed on a predicate in sort " ++ pkp ++ fnl() ++ - str "because" ++ spc() ++ str explanation ++ str ".") - | None -> + str "is not allowed on a predicate in sort " ++ pkp ++ fnl () ++ + str "because" ++ spc () ++ str explanation ++ str ".") + | None -> str "ill-formed elimination predicate." in hov 0 ( - str "Incorrect elimination of" ++ spc() ++ pc ++ spc () ++ - str "in the inductive type" ++ spc() ++ quote pi ++ str":") ++ + str "Incorrect elimination of" ++ spc () ++ pc ++ spc () ++ + str "in the inductive type" ++ spc () ++ quote pi ++ str ":") ++ fnl () ++ msg let explain_case_not_inductive env cj = @@ -118,24 +114,20 @@ let explain_case_not_inductive env cj = let pc = pr_lconstr_env env cj.uj_val in let pct = pr_lconstr_env env cj.uj_type in match kind_of_term cj.uj_type with - | Evar _ -> - str "Cannot infer a type for this expression" + | Evar _ -> + str "Cannot infer a type for this expression." | _ -> - str "The term" ++ brk(1,1) ++ pc ++ spc () ++ - str "has type" ++ brk(1,1) ++ pct ++ spc () ++ - str "which is not a (co-)inductive type" + str "The term" ++ brk(1,1) ++ pc ++ spc () ++ + str "has type" ++ brk(1,1) ++ pct ++ spc () ++ + str "which is not a (co-)inductive type." let explain_number_branches env cj expn = let env = make_all_name_different env in let pc = pr_lconstr_env env cj.uj_val in let pct = pr_lconstr_env env cj.uj_type in - str "Matching on term" ++ brk(1,1) ++ pc ++ spc () ++ + str "Matching on term" ++ brk(1,1) ++ pc ++ spc () ++ str "of type" ++ brk(1,1) ++ pct ++ spc () ++ - str "expects " ++ int expn ++ str " branches" - -let ordinal n = - let s = match n mod 10 with 1 -> "st" | 2 -> "nd" | 3 -> "rd" | _ -> "th" in - string_of_int n ^ s + str "expects " ++ int expn ++ str " branches." let explain_ill_formed_branch env c i actty expty = let env = make_all_name_different env in @@ -143,84 +135,81 @@ let explain_ill_formed_branch env c i actty expty = let pa = pr_lconstr_env env actty in let pe = pr_lconstr_env env expty in str "In pattern-matching on term" ++ brk(1,1) ++ pc ++ - spc () ++ str "the " ++ str (ordinal (i+1)) ++ str " branch has type" ++ - brk(1,1) ++ pa ++ spc () ++ - str "which should be" ++ brk(1,1) ++ pe + spc () ++ str "the " ++ nth (i+1) ++ str " branch has type" ++ + brk(1,1) ++ pa ++ spc () ++ + str "which should be" ++ brk(1,1) ++ pe ++ str "." let explain_generalization env (name,var) j = let pe = pr_ne_context_of (str "In environment") env in let pv = pr_ltype_env env var in let (pc,pt) = pr_ljudge_env (push_rel_assum (name,var) env) j in - str"Illegal generalization: " ++ pe ++ - str"Cannot generalize" ++ brk(1,1) ++ pv ++ spc () ++ - str"over" ++ brk(1,1) ++ pc ++ str"," ++ spc () ++ - str"it has type" ++ spc () ++ pt ++ - spc () ++ str"which should be Set, Prop or Type." + pe ++ str "Cannot generalize" ++ brk(1,1) ++ pv ++ spc () ++ + str "over" ++ brk(1,1) ++ pc ++ str "," ++ spc () ++ + str "it has type" ++ spc () ++ pt ++ + spc () ++ str "which should be Set, Prop or Type." let explain_actual_type env j pt = let pe = pr_ne_context_of (str "In environment") env in let (pc,pct) = pr_ljudge_env env j in let pt = pr_lconstr_env env pt in pe ++ - str "The term" ++ brk(1,1) ++ pc ++ spc () ++ - str "has type" ++ brk(1,1) ++ pct ++ brk(1,1) ++ - str "while it is expected to have type" ++ brk(1,1) ++ pt + str "The term" ++ brk(1,1) ++ pc ++ spc () ++ + str "has type" ++ brk(1,1) ++ pct ++ brk(1,1) ++ + str "while it is expected to have type" ++ brk(1,1) ++ pt ++ str "." let explain_cant_apply_bad_type env (n,exptyp,actualtyp) rator randl = let env = make_all_name_different env in - let randl = Array.to_list randl in -(* let pe = pr_ne_context_of (str"in environment") env in*) + let nargs = Array.length randl in +(* let pe = pr_ne_context_of (str "in environment") env in*) let pr,prt = pr_ljudge_env env rator in - let term_string1,term_string2 = - if List.length randl > 1 then - str "terms", (str"The "++nth n++str" term") - else - str "term", str "This term" in - let appl = prlist_with_sep pr_fnl + let term_string1 = str (plural nargs "term") in + let term_string2 = + if nargs>1 then str "The " ++ nth n ++ str " term" else str "This term" in + let appl = prvect_with_sep pr_fnl (fun c -> let pc,pct = pr_ljudge_env env c in - hov 2 (pc ++ spc () ++ str": " ++ pct)) randl + hov 2 (pc ++ spc () ++ str ": " ++ pct)) randl in - str"Illegal application (Type Error): " ++ (* pe ++ *) fnl () ++ - str"The term" ++ brk(1,1) ++ pr ++ spc () ++ - str"of type" ++ brk(1,1) ++ prt ++ spc () ++ - str"cannot be applied to the " ++ term_string1 ++ fnl () ++ - str" " ++ v 0 appl ++ fnl () ++ term_string2 ++ str" has type" ++ + str "Illegal application (Type Error): " ++ (* pe ++ *) fnl () ++ + str "The term" ++ brk(1,1) ++ pr ++ spc () ++ + str "of type" ++ brk(1,1) ++ prt ++ spc () ++ + str "cannot be applied to the " ++ term_string1 ++ fnl () ++ + str " " ++ v 0 appl ++ fnl () ++ term_string2 ++ str " has type" ++ brk(1,1) ++ pr_lconstr_env env actualtyp ++ spc () ++ - str"which should be coercible to" ++ brk(1,1) ++ pr_lconstr_env env exptyp + str "which should be coercible to" ++ brk(1,1) ++ + pr_lconstr_env env exptyp ++ str "." let explain_cant_apply_not_functional env rator randl = let env = make_all_name_different env in - let randl = Array.to_list randl in -(* let pe = pr_ne_context_of (str"in environment") env in*) + let nargs = Array.length randl in +(* let pe = pr_ne_context_of (str "in environment") env in*) let pr = pr_lconstr_env env rator.uj_val in let prt = pr_lconstr_env env rator.uj_type in - let term_string = if List.length randl > 1 then "terms" else "term" in - let appl = prlist_with_sep pr_fnl + let appl = prvect_with_sep pr_fnl (fun c -> let pc = pr_lconstr_env env c.uj_val in let pct = pr_lconstr_env env c.uj_type in - hov 2 (pc ++ spc () ++ str": " ++ pct)) randl + hov 2 (pc ++ spc () ++ str ": " ++ pct)) randl in - str"Illegal application (Non-functional construction): " ++ + str "Illegal application (Non-functional construction): " ++ (* pe ++ *) fnl () ++ - str"The expression" ++ brk(1,1) ++ pr ++ spc () ++ - str"of type" ++ brk(1,1) ++ prt ++ spc () ++ - str("cannot be applied to the "^term_string) ++ fnl () ++ - str" " ++ v 0 appl + str "The expression" ++ brk(1,1) ++ pr ++ spc () ++ + str "of type" ++ brk(1,1) ++ prt ++ spc () ++ + str "cannot be applied to the " ++ str (plural nargs "term") ++ fnl () ++ + str " " ++ v 0 appl let explain_unexpected_type env actual_type expected_type = let pract = pr_lconstr_env env actual_type in let prexp = pr_lconstr_env env expected_type in - str"This type is" ++ spc () ++ pract ++ spc () ++ + str "This type is" ++ spc () ++ pract ++ spc () ++ str "but is expected to be" ++ - spc () ++ prexp + spc () ++ prexp ++ str "." let explain_not_product env c = let pr = pr_lconstr_env env c in - str"The type of this term is a product," ++ spc () ++ - str"while it is expected to be" ++ - if is_Type c then str " a sort" else (brk(1,1) ++ pr) + str "The type of this term is a product" ++ spc () ++ + str "while it is expected to be" ++ + (if is_Type c then str " a sort" else (brk(1,1) ++ pr)) ++ str "." (* TODO: use the names *) (* (co)fixpoints *) @@ -228,7 +217,7 @@ let explain_ill_formed_rec_body env err names i = let prt_name i = match names.(i) with Name id -> str "Recursive definition of " ++ pr_id id - | Anonymous -> str"The " ++ nth i ++ str" definition" in + | Anonymous -> str "The " ++ nth i ++ str " definition" in let st = match err with @@ -236,16 +225,16 @@ let explain_ill_formed_rec_body env err names i = | NotEnoughAbstractionInFixBody -> str "Not enough abstractions in the definition" | RecursionNotOnInductiveType c -> - str "Recursive definition on" ++ spc() ++ pr_lconstr_env env c ++ spc() ++ + str "Recursive definition on" ++ spc () ++ pr_lconstr_env env c ++ spc () ++ str "which should be an inductive type" | RecursionOnIllegalTerm(j,arg,le,lt) -> let called = match names.(j) with Name id -> pr_id id - | Anonymous -> str"the " ++ nth i ++ str" definition" in + | Anonymous -> str "the " ++ nth i ++ str " definition" in let vars = match (lt,le) with - ([],[]) -> mt() + ([],[]) -> assert false | ([],[x]) -> str "a subterm of " ++ pr_db env x | ([],_) -> @@ -255,78 +244,72 @@ let explain_ill_formed_rec_body env err names i = | _ -> str "one of the following variables: " ++ prlist_with_sep pr_spc (pr_db env) lt in - str "Recursive call to " ++ called ++ spc() ++ - str "has principal argument equal to" ++ spc() ++ - pr_lconstr_env env arg ++ fnl() ++ str "instead of " ++ vars + str "Recursive call to " ++ called ++ spc () ++ + str "has principal argument equal to" ++ spc () ++ + pr_lconstr_env env arg ++ fnl () ++ str "instead of " ++ vars | NotEnoughArgumentsForFixCall j -> let called = match names.(j) with Name id -> pr_id id - | Anonymous -> str"the " ++ nth i ++ str" definition" in - str "Recursive call to " ++ called ++ str " had not enough arguments" + | Anonymous -> str "the " ++ nth i ++ str " definition" in + str "Recursive call to " ++ called ++ str " has not enough arguments" (* CoFixpoint guard errors *) | CodomainNotInductiveType c -> - str "the codomain is" ++ spc () ++ pr_lconstr_env env c ++ spc () ++ + str "The codomain is" ++ spc () ++ pr_lconstr_env env c ++ spc () ++ str "which should be a coinductive type" | NestedRecursiveOccurrences -> - str "nested recursive occurrences" + str "Nested recursive occurrences" | UnguardedRecursiveCall c -> - str "unguarded recursive call in" ++ spc() ++ pr_lconstr_env env c + str "Unguarded recursive call in" ++ spc () ++ pr_lconstr_env env c | RecCallInTypeOfAbstraction c -> - str "recursive call forbidden in the domain of an abstraction:" ++ - spc() ++ pr_lconstr_env env c + str "Recursive call forbidden in the domain of an abstraction:" ++ + spc () ++ pr_lconstr_env env c | RecCallInNonRecArgOfConstructor c -> - str "recursive call on a non-recursive argument of constructor" ++ - spc() ++ pr_lconstr_env env c + str "Recursive call on a non-recursive argument of constructor" ++ + spc () ++ pr_lconstr_env env c | RecCallInTypeOfDef c -> - str "recursive call forbidden in the type of a recursive definition" ++ - spc() ++ pr_lconstr_env env c + str "Recursive call forbidden in the type of a recursive definition" ++ + spc () ++ pr_lconstr_env env c | RecCallInCaseFun c -> - str "recursive call in a branch of" ++ spc() ++ pr_lconstr_env env c - | RecCallInCaseArg c -> - str "recursive call in the argument of cases in" ++ spc() ++ + str "Recursive call in a branch of" ++ spc () ++ pr_lconstr_env env c + | RecCallInCaseArg c -> + str "Recursive call in the argument of cases in" ++ spc () ++ pr_lconstr_env env c | RecCallInCasePred c -> - str "recursive call in the type of cases in" ++ spc() ++ + str "Recursive call in the type of cases in" ++ spc () ++ pr_lconstr_env env c | NotGuardedForm c -> - str "sub-expression " ++ pr_lconstr_env env c ++ spc() ++ - str "not in guarded form" ++ spc()++ - str"(should be a constructor, an abstraction, a match, a cofix or a recursive call)" + str "Sub-expression " ++ pr_lconstr_env env c ++ + strbrk " not in guarded form (should be a constructor," ++ + strbrk " an abstraction, a match, a cofix or a recursive call)" in - prt_name i ++ str" is ill-formed." ++ fnl() ++ + prt_name i ++ str " is ill-formed." ++ fnl () ++ pr_ne_context_of (str "In environment") env ++ - st + st ++ str "." let explain_ill_typed_rec_body env i names vdefj vargs = let env = make_all_name_different env in let pvd,pvdt = pr_ljudge_env env (vdefj.(i)) in let pv = pr_lconstr_env env vargs.(i) in - str"The " ++ - (if Array.length vdefj = 1 then mt () else int (i+1) ++ str "-th") ++ - str"recursive definition" ++ spc () ++ pvd ++ spc () ++ - str "has type" ++ spc () ++ pvdt ++spc () ++ - str "it should be" ++ spc () ++ pv -(* -let explain_not_inductive env c = - let env = make_all_name_different env in - let pc = pr_lconstr_env env c in - str"The term" ++ brk(1,1) ++ pc ++ spc () ++ - str "is not an inductive definition" -*) + str "The " ++ + (if Array.length vdefj = 1 then mt () else nth (i+1) ++ spc ()) ++ + str "recursive definition" ++ spc () ++ pvd ++ spc () ++ + str "has type" ++ spc () ++ pvdt ++ spc () ++ + str "while it should be" ++ spc () ++ pv ++ str "." + let explain_cant_find_case_type env c = let env = make_all_name_different env in let pe = pr_lconstr_env env c in - hov 3 (str "Cannot infer type of pattern-matching on" ++ ws 1 ++ pe) + str "Cannot infer type of pattern-matching on" ++ ws 1 ++ pe ++ str "." let explain_occur_check env ev rhs = let env = make_all_name_different env in let id = Evd.string_of_existential ev in let pt = pr_lconstr_env env rhs in - str"Occur check failed: tried to define " ++ str id ++ - str" with term" ++ brk(1,1) ++ pt + str "Cannot define " ++ str id ++ str " with term" ++ brk(1,1) ++ + pt ++ spc () ++ str "that would depend on itself." let explain_hole_kind env = function | QuestionMark _ -> str "a term for this placeholder" @@ -344,7 +327,7 @@ let explain_hole_kind env = function | InternalHole -> str "a term for an internal placeholder" | TomatchTypeParameter (tyi,n) -> - str "the " ++ pr_ord n ++ + str "the " ++ nth n ++ str " argument of the inductive type (" ++ pr_inductive env tyi ++ str ") of this term" @@ -353,48 +336,46 @@ let explain_not_clean env ev t k = let c = mkRel (Intset.choose (free_rels t)) in let id = Evd.string_of_existential ev in let var = pr_lconstr_env env c in - str"Tried to define " ++ explain_hole_kind env k ++ - str" (" ++ str id ++ str ")" ++ spc() ++ - str"with a term using variable " ++ var ++ spc () ++ - str"which is not in its scope." + str "Tried to define " ++ explain_hole_kind env k ++ + str " (" ++ str id ++ str ")" ++ spc () ++ + str "with a term using variable " ++ var ++ spc () ++ + str "which is not in its scope." let explain_unsolvable_implicit env k = - str "Cannot infer " ++ explain_hole_kind env k - + str "Cannot infer " ++ explain_hole_kind env k ++ str "." -let explain_var_not_found env id = - str "The variable" ++ spc () ++ str (string_of_id id) ++ - spc () ++ str "was not found" ++ - spc () ++ str "in the current" ++ spc () ++ str "environment" +let explain_var_not_found env id = + str "The variable" ++ spc () ++ pr_id id ++ + spc () ++ str "was not found" ++ + spc () ++ str "in the current" ++ spc () ++ str "environment" ++ str "." let explain_wrong_case_info env ind ci = - let pi = pr_lconstr (mkInd ind) in + let pi = pr_inductive (Global.env()) ind in if ci.ci_ind = ind then - str"Pattern-matching expression on an object of inductive" ++ spc () ++ pi ++ - spc () ++ str"has invalid information" + str "Pattern-matching expression on an object of inductive type" ++ + spc () ++ pi ++ spc () ++ str "has invalid information." else - let pc = pr_lconstr (mkInd ci.ci_ind) in - str"A term of inductive type" ++ spc () ++ pi ++ spc () ++ - str"was given to a pattern-matching expression on the inductive type" ++ - spc () ++ pc - + let pc = pr_inductive (Global.env()) ci.ci_ind in + str "A term of inductive type" ++ spc () ++ pi ++ spc () ++ + str "was given to a pattern-matching expression on the inductive type" ++ + spc () ++ pc ++ str "." let explain_cannot_unify env m n = - let pm = pr_lconstr_env env m in + let pm = pr_lconstr_env env m in let pn = pr_lconstr_env env n in - str"Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++ - str"with" ++ brk(1,1) ++ pn + str "Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++ + str "with" ++ brk(1,1) ++ pn let explain_cannot_unify_local env m n subn = - let pm = pr_lconstr_env env m in + let pm = pr_lconstr_env env m in let pn = pr_lconstr_env env n in let psubn = pr_lconstr_env env subn in - str"Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++ - str"with" ++ brk(1,1) ++ pn ++ spc() ++ str"as" ++ brk(1,1) ++ - psubn ++ str" contains local variables" + str "Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++ + str "with" ++ brk(1,1) ++ pn ++ spc () ++ str "as" ++ brk(1,1) ++ + psubn ++ str " contains local variables" let explain_refiner_cannot_generalize env ty = - str "Cannot find a well-typed generalisation of the goal with type : " ++ + str "Cannot find a well-typed generalisation of the goal with type : " ++ pr_lconstr_env env ty let explain_no_occurrence_found env c = @@ -402,35 +383,35 @@ let explain_no_occurrence_found env c = str " in the current goal" let explain_cannot_unify_binding_type env m n = - let pm = pr_lconstr_env env m in + let pm = pr_lconstr_env env m in let pn = pr_lconstr_env env n in - str "This binding has type" ++ brk(1,1) ++ pm ++ spc () ++ + str "This binding has type" ++ brk(1,1) ++ pm ++ spc () ++ str "which should be unifiable with" ++ brk(1,1) ++ pn let explain_type_error env err = let env = make_all_name_different env in match err with - | UnboundRel n -> + | UnboundRel n -> explain_unbound_rel env n - | UnboundVar v -> + | UnboundVar v -> explain_unbound_var env v - | NotAType j -> + | NotAType j -> explain_not_type env j - | BadAssumption c -> + | BadAssumption c -> explain_bad_assumption env c - | ReferenceVariables id -> + | ReferenceVariables id -> explain_reference_variables id | ElimArity (ind, aritylst, c, pj, okinds) -> - explain_elim_arity env ind aritylst c pj okinds - | CaseNotInductive cj -> + explain_elim_arity env ind aritylst c pj okinds + | CaseNotInductive cj -> explain_case_not_inductive env cj - | NumberBranches (cj, n) -> + | NumberBranches (cj, n) -> explain_number_branches env cj n - | IllFormedBranch (c, i, actty, expty) -> - explain_ill_formed_branch env c i actty expty + | IllFormedBranch (c, i, actty, expty) -> + explain_ill_formed_branch env c i actty expty | Generalization (nvar, c) -> explain_generalization env nvar c - | ActualType (j, pt) -> + | ActualType (j, pt) -> explain_actual_type env j pt | CantApplyBadType (t, rator, randl) -> explain_cant_apply_bad_type env t rator randl @@ -438,14 +419,11 @@ let explain_type_error env err = explain_cant_apply_not_functional env rator randl | IllFormedRecBody (err, lna, i) -> explain_ill_formed_rec_body env err lna i - | IllTypedRecBody (i, lna, vdefj, vargs) -> + | IllTypedRecBody (i, lna, vdefj, vargs) -> explain_ill_typed_rec_body env i lna vdefj vargs | WrongCaseInfo (ind,ci) -> explain_wrong_case_info env ind ci -(* - | NotInductive c -> - explain_not_inductive env c -*) + let explain_pretype_error env err = let env = make_all_name_different env in match err with @@ -465,38 +443,38 @@ let explain_pretype_error env err = (* Refiner errors *) let explain_refiner_bad_type arg ty conclty = - str"refiner was given an argument" ++ brk(1,1) ++ + str "refiner was given an argument" ++ brk(1,1) ++ pr_lconstr arg ++ spc () ++ - str"of type" ++ brk(1,1) ++ pr_lconstr ty ++ spc () ++ - str"instead of" ++ brk(1,1) ++ pr_lconstr conclty + str "of type" ++ brk(1,1) ++ pr_lconstr ty ++ spc () ++ + str "instead of" ++ brk(1,1) ++ pr_lconstr conclty let explain_refiner_occur_meta t = - str"cannot refine with term" ++ brk(1,1) ++ pr_lconstr t ++ - spc () ++ str"because there are metavariables, and it is" ++ - spc () ++ str"neither an application nor a Case" + str "cannot refine with term" ++ brk(1,1) ++ pr_lconstr t ++ + spc () ++ str "because there are metavariables, and it is" ++ + spc () ++ str "neither an application nor a Case" let explain_refiner_occur_meta_goal t = - str"generated subgoal" ++ brk(1,1) ++ pr_lconstr t ++ - spc () ++ str"has metavariables in it" + str "generated subgoal" ++ brk(1,1) ++ pr_lconstr t ++ + spc () ++ str "has metavariables in it" let explain_refiner_cannot_apply t harg = - str"in refiner, a term of type " ++ brk(1,1) ++ - pr_lconstr t ++ spc () ++ str"could not be applied to" ++ brk(1,1) ++ + str "in refiner, a term of type " ++ brk(1,1) ++ + pr_lconstr t ++ spc () ++ str "could not be applied to" ++ brk(1,1) ++ pr_lconstr harg let explain_refiner_not_well_typed c = - str"The term " ++ pr_lconstr c ++ str" is not well-typed" + str "The term " ++ pr_lconstr c ++ str " is not well-typed" let explain_intro_needs_product () = - str "Introduction tactics needs products" + str "Introduction tactics needs products." let explain_does_not_occur_in c hyp = - str "The term" ++ spc () ++ pr_lconstr c ++ spc () ++ str "does not occur in" ++ - spc () ++ pr_id hyp + str "The term" ++ spc () ++ pr_lconstr c ++ spc () ++ + str "does not occur in" ++ spc () ++ pr_id hyp ++ str "." let explain_non_linear_proof c = str "cannot refine with term" ++ brk(1,1) ++ pr_lconstr c ++ - spc () ++ str"because a metavariable has several occurrences" + spc () ++ str "because a metavariable has several occurrences." let explain_refiner_error = function | BadType (arg,ty,conclty) -> explain_refiner_bad_type arg ty conclty @@ -514,48 +492,40 @@ let error_non_strictly_positive env c v = let pc = pr_lconstr_env env c in let pv = pr_lconstr_env env v in str "Non strictly positive occurrence of " ++ pv ++ str " in" ++ - brk(1,1) ++ pc + brk(1,1) ++ pc ++ str "." let error_ill_formed_inductive env c v = let pc = pr_lconstr_env env c in let pv = pr_lconstr_env env v in str "Not enough arguments applied to the " ++ pv ++ - str " in" ++ brk(1,1) ++ pc + str " in" ++ brk(1,1) ++ pc ++ str "." let error_ill_formed_constructor env c v = let pc = pr_lconstr_env env c in let pv = pr_lconstr_env env v in - str "The conclusion of" ++ brk(1,1) ++ pc ++ brk(1,1) ++ - str "is not valid;" ++ brk(1,1) ++ str "it must be built from " ++ pv - -let str_of_nth n = - (string_of_int n)^ - (match n mod 10 with - | 1 -> "st" - | 2 -> "nd" - | 3 -> "rd" - | _ -> "th") + str "The conclusion of" ++ brk(1,1) ++ pc ++ brk(1,1) ++ + str "is not valid;" ++ brk(1,1) ++ str "it must be built from " ++ + pv ++ str "." let error_bad_ind_parameters env c n v1 v2 = let pc = pr_lconstr_env_at_top env c in let pv1 = pr_lconstr_env env v1 in let pv2 = pr_lconstr_env env v2 in - str ("The "^(str_of_nth n)^" argument of ") ++ pv2 ++ brk(1,1) ++ - str "must be " ++ pv1 ++ str " in" ++ brk(1,1) ++ pc + str "The " ++ nth n ++ str " argument of " ++ pv2 ++ brk(1,1) ++ + str "must be " ++ pv1 ++ str " in" ++ brk(1,1) ++ pc ++ str "." let error_same_names_types id = - str "The name" ++ spc () ++ pr_id id ++ spc () ++ - str "is used twice is the inductive types definition." + str "The name" ++ spc () ++ pr_id id ++ spc () ++ + str "is used more than once." -let error_same_names_constructors id cid = - str "The constructor name" ++ spc () ++ pr_id cid ++ spc () ++ - str "is used twice is the definition of type" ++ spc () ++ - pr_id id +let error_same_names_constructors id = + str "The constructor name" ++ spc () ++ pr_id id ++ spc () ++ + str "is used more than once." -let error_same_names_overlap idl = - str "The following names" ++ spc () ++ - str "are used both as type names and constructor names:" ++ spc () ++ - prlist_with_sep pr_coma pr_id idl +let error_same_names_overlap idl = + strbrk "The following names are used both as type names and constructor " ++ + str "names:" ++ spc () ++ + prlist_with_sep pr_coma pr_id idl ++ str "." let error_not_an_arity id = str "The type of" ++ spc () ++ pr_id id ++ spc () ++ str "is not an arity." @@ -567,16 +537,22 @@ let error_not_allowed_case_analysis dep kind i = str (if dep then "Dependent" else "Non Dependent") ++ str " case analysis on sort: " ++ pr_sort kind ++ fnl () ++ str "is not allowed for inductive definition: " ++ - pr_inductive (Global.env()) i + pr_inductive (Global.env()) i ++ str "." let error_bad_induction dep indid kind = str (if dep then "Dependent" else "Non dependent") ++ str " induction for type " ++ pr_id indid ++ str " and sort " ++ pr_sort kind ++ spc () ++ - str "is not allowed" + str "is not allowed." -let error_not_mutual_in_scheme () = - str "Induction schemes are concerned only with distinct mutually inductive types" +let error_not_mutual_in_scheme ind ind' = + if ind = ind' then + str "The inductive type " ++ pr_inductive (Global.env()) ind ++ + str "occurs twice." + else + str "The inductive types " ++ pr_inductive (Global.env()) ind ++ spc () ++ + str "and" ++ spc () ++ pr_inductive (Global.env()) ind' ++ spc () ++ + str "are not mutually defined." (* Inductive constructions errors *) @@ -586,7 +562,7 @@ let explain_inductive_error = function | NotConstructor (env,c,v) -> error_ill_formed_constructor env c v | NonPar (env,c,n,v1,v2) -> error_bad_ind_parameters env c n v1 v2 | SameNamesTypes id -> error_same_names_types id - | SameNamesConstructors (id,cid) -> error_same_names_constructors id cid + | SameNamesConstructors id -> error_same_names_constructors id | SameNamesOverlap idl -> error_same_names_overlap idl | NotAnArity id -> error_not_an_arity id | BadEntry -> error_bad_entry () @@ -597,25 +573,25 @@ let explain_recursion_scheme_error = function | NotAllowedCaseAnalysis (dep,k,i) -> error_not_allowed_case_analysis dep k i | BadInduction (dep,indid,kind) -> error_bad_induction dep indid kind - | NotMutualInScheme -> error_not_mutual_in_scheme () + | NotMutualInScheme (ind,ind')-> error_not_mutual_in_scheme ind ind' (* Pattern-matching errors *) -let explain_bad_pattern env cstr ty = +let explain_bad_pattern env cstr ty = let env = make_all_name_different env in let pt = pr_lconstr_env env ty in let pc = pr_constructor env cstr in - str "Found the constructor " ++ pc ++ brk(1,1) ++ - str "while matching a term of type " ++ pt ++ brk(1,1) ++ - str "which is not an inductive type" + str "Found the constructor " ++ pc ++ brk(1,1) ++ + str "while matching a term of type " ++ pt ++ brk(1,1) ++ + str "which is not an inductive type." let explain_bad_constructor env cstr ind = let pi = pr_inductive env ind in (* let pc = pr_constructor env cstr in*) let pt = pr_inductive env (inductive_of_constructor cstr) in - str "Found a constructor of inductive type " ++ pt ++ brk(1,1) ++ - str "while a constructor of " ++ pi ++ brk(1,1) ++ - str "is expected" + str "Found a constructor of inductive type " ++ pt ++ brk(1,1) ++ + str "while a constructor of " ++ pi ++ brk(1,1) ++ + str "is expected." let decline_string n s = if n = 0 then "no "^s @@ -623,28 +599,28 @@ let decline_string n s = else (string_of_int n^" "^s^"s") let explain_wrong_numarg_constructor env cstr n = - str "The constructor " ++ pr_constructor env cstr ++ - str " expects " ++ str (decline_string n "argument") + str "The constructor " ++ pr_constructor env cstr ++ + str " expects " ++ str (decline_string n "argument") ++ str "." let explain_wrong_numarg_inductive env ind n = - str "The inductive type " ++ pr_inductive env ind ++ - str " expects " ++ str (decline_string n "argument") + str "The inductive type " ++ pr_inductive env ind ++ + str " expects " ++ str (decline_string n "argument") ++ str "." let explain_wrong_predicate_arity env pred nondep_arity dep_arity= let env = make_all_name_different env in let pp = pr_lconstr_env env pred in str "The elimination predicate " ++ spc () ++ pp ++ fnl () ++ - str "should be of arity" ++ spc () ++ - pr_lconstr_env env nondep_arity ++ spc () ++ - str "(for non dependent case) or" ++ - spc () ++ pr_lconstr_env env dep_arity ++ spc () ++ str "(for dependent case)." + str "should be of arity" ++ spc () ++ + pr_lconstr_env env nondep_arity ++ spc () ++ + str "(for non dependent case) or" ++ + spc () ++ pr_lconstr_env env dep_arity ++ spc () ++ str "(for dependent case)." let explain_needs_inversion env x t = let env = make_all_name_different env in let px = pr_lconstr_env env x in let pt = pr_lconstr_env env t in - str "Sorry, I need inversion to compile pattern matching of term " ++ - px ++ str " of type: " ++ pt + str "Sorry, I need inversion to compile pattern matching on term " ++ + px ++ str " of type: " ++ pt ++ str "." let explain_unused_clause env pats = (* Without localisation @@ -652,11 +628,11 @@ let explain_unused_clause env pats = (str ("Unused clause with pattern"^s) ++ spc () ++ hov 0 (prlist_with_sep pr_spc pr_cases_pattern pats) ++ str ")") *) - str "This clause is redundant" + str "This clause is redundant." let explain_non_exhaustive env pats = - let s = if List.length pats > 1 then "s" else "" in - str ("Non exhaustive pattern-matching: no clause found for pattern"^s) ++ + str "Non exhaustive pattern-matching: no clause found for " ++ + str (plural (List.length pats) "pattern") ++ spc () ++ hov 0 (prlist_with_sep pr_spc pr_cases_pattern pats) let explain_cannot_infer_predicate env typs = @@ -669,7 +645,7 @@ let explain_cannot_infer_predicate env typs = spc () ++ hov 0 (prlist_with_sep pr_fnl pr_branch (Array.to_list typs)) let explain_pattern_matching_error env = function - | BadPattern (c,t) -> + | BadPattern (c,t) -> explain_bad_pattern env c t | BadConstructor (c,ind) -> explain_bad_constructor env c ind @@ -690,6 +666,6 @@ let explain_pattern_matching_error env = function let explain_reduction_tactic_error = function | Tacred.InvalidAbstraction (env,c,(env',e)) -> - str "The abstracted term" ++ spc() ++ pr_lconstr_env_at_top env c ++ - spc() ++ str "is not well typed." ++ fnl () ++ + str "The abstracted term" ++ spc () ++ pr_lconstr_env_at_top env c ++ + spc () ++ str "is not well typed." ++ fnl () ++ explain_type_error env' e |