diff options
Diffstat (limited to 'toplevel/himsg.ml')
-rw-r--r-- | toplevel/himsg.ml | 1267 |
1 files changed, 0 insertions, 1267 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml deleted file mode 100644 index f98505c3..00000000 --- a/toplevel/himsg.ml +++ /dev/null @@ -1,1267 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Pp -open Util -open Names -open Nameops -open Namegen -open Term -open Termops -open Indtypes -open Environ -open Pretype_errors -open Type_errors -open Typeclasses_errors -open Indrec -open Cases -open Logic -open Printer -open Evd -open Context.Rel.Declaration - -(* This simplifies the typing context of Cases clauses *) -(* hope it does not disturb other typing contexts *) -let contract env lc = - let l = ref [] in - let contract_context decl env = - match decl with - | LocalDef (_,c',_) when isRel c' -> - l := (Vars.substl !l c') :: !l; - env - | _ -> - let t' = Vars.substl !l (get_type decl) in - let c' = Option.map (Vars.substl !l) (get_value decl) in - let na' = named_hd env t' (get_name decl) in - l := (mkRel 1) :: List.map (Vars.lift 1) !l; - match c' with - | None -> push_rel (LocalAssum (na',t')) env - | Some c' -> push_rel (LocalDef (na',c',t')) env - in - let env = process_rel_context contract_context env in - (env, List.map (Vars.substl !l) lc) - -let contract2 env a b = match contract env [a;b] with - | env, [a;b] -> env,a,b | _ -> assert false - -let contract3 env a b c = match contract env [a;b;c] with - | env, [a;b;c] -> env,a,b,c | _ -> assert false - -let contract4 env a b c d = match contract env [a;b;c;d] with - | env, [a;b;c;d] -> (env,a,b,c),d | _ -> assert false - -let contract1_vect env a v = - match contract env (a :: Array.to_list v) with - | env, a::l -> env,a,Array.of_list l - | _ -> assert false - -let rec contract3' env a b c = function - | OccurCheck (evk,d) -> let x,d = contract4 env a b c d in x,OccurCheck(evk,d) - | NotClean ((evk,args),env',d) -> - let env',d,args = contract1_vect env' d args in - contract3 env a b c,NotClean((evk,args),env',d) - | ConversionFailed (env',t1,t2) -> - let (env',t1,t2) = contract2 env' t1 t2 in - contract3 env a b c, ConversionFailed (env',t1,t2) - | NotSameArgSize | NotSameHead | NoCanonicalStructure - | MetaOccurInBody _ | InstanceNotSameType _ | ProblemBeyondCapabilities - | UnifUnivInconsistency _ as x -> contract3 env a b c, x - | CannotSolveConstraint ((pb,env',t,u),x) -> - let env',t,u = contract2 env' t u in - let y,x = contract3' env a b c x in - y,CannotSolveConstraint ((pb,env',t,u),x) - -(** Ad-hoc reductions *) - -let j_nf_betaiotaevar sigma j = - { uj_val = Evarutil.nf_evar sigma j.uj_val; - uj_type = Reductionops.nf_betaiota sigma j.uj_type } - -let jv_nf_betaiotaevar sigma jl = - Array.map (j_nf_betaiotaevar sigma) jl - -(** Printers *) - -let pr_lconstr c = quote (pr_lconstr c) -let pr_lconstr_env e s c = quote (pr_lconstr_env e s c) -let pr_ljudge_env e s c = let v,t = pr_ljudge_env e s c in (quote v,quote t) - -(** A canonisation procedure for constr such that comparing there - externalisation catches more equalities *) -let canonize_constr c = - (* replaces all the names in binders by [dn] ("default name"), - ensures that [alpha]-equivalent terms will have the same - externalisation. *) - let dn = Name.Anonymous in - let rec canonize_binders c = - match Term.kind_of_term c with - | Prod (_,t,b) -> mkProd(dn,t,b) - | Lambda (_,t,b) -> mkLambda(dn,t,b) - | LetIn (_,u,t,b) -> mkLetIn(dn,u,t,b) - | _ -> Term.map_constr canonize_binders c - in - canonize_binders c - -(** Tries to realize when the two terms, albeit different are printed the same. *) -let display_eq ~flags env sigma t1 t2 = - (* terms are canonized, then their externalisation is compared syntactically *) - let open Constrextern in - let t1 = canonize_constr t1 in - let t2 = canonize_constr t2 in - let ct1 = Flags.with_options flags (fun () -> extern_constr false env sigma t1) () in - let ct2 = Flags.with_options flags (fun () -> extern_constr false env sigma t2) () in - Constrexpr_ops.constr_expr_eq ct1 ct2 - -(** This function adds some explicit printing flags if the two arguments are - printed alike. *) -let rec pr_explicit_aux env sigma t1 t2 = function -| [] -> - (** no specified flags: default. *) - (quote (Printer.pr_lconstr_env env sigma t1), quote (Printer.pr_lconstr_env env sigma t2)) -| flags :: rem -> - let equal = display_eq ~flags env sigma t1 t2 in - if equal then - (** The two terms are the same from the user point of view *) - pr_explicit_aux env sigma t1 t2 rem - else - let open Constrextern in - let ct1 = Flags.with_options flags (fun () -> extern_constr false env sigma t1) () - in - let ct2 = Flags.with_options flags (fun () -> extern_constr false env sigma t2) () - in - quote (Ppconstr.pr_lconstr_expr ct1), quote (Ppconstr.pr_lconstr_expr ct2) - -let explicit_flags = - let open Constrextern in - [ []; (** First, try with the current flags *) - [print_implicits]; (** Then with implicit *) - [print_universes]; (** Then with universes *) - [print_universes; print_implicits]; (** With universes AND implicits *) - [print_implicits; print_coercions; print_no_symbol]; (** Then more! *) - [print_universes; print_implicits; print_coercions; print_no_symbol] (** and more! *) ] - -let pr_explicit env sigma t1 t2 = pr_explicit_aux env sigma t1 t2 explicit_flags - -let pr_db env i = - try - match lookup_rel i env |> get_name with - | Name id -> pr_id id - | Anonymous -> str "<>" - with Not_found -> str "UNBOUND_REL_" ++ int i - -let explain_unbound_rel env sigma n = - let pe = pr_ne_context_of (str "In environment") env sigma in - 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 "." - -let explain_not_type env sigma j = - let j = Evarutil.j_nf_evar sigma j in - let pe = pr_ne_context_of (str "In environment") env sigma in - let pc,pt = pr_ljudge_env env sigma 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." - -let explain_bad_assumption env sigma j = - let pe = pr_ne_context_of (str "In environment") env sigma in - let pc,pt = pr_ljudge_env env sigma j in - 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 id c = - (* c is intended to be a global reference *) - let pc = pr_global (Globnames.global_of_constr c) in - pc ++ strbrk " depends on the variable " ++ pr_id id ++ - strbrk " which is not declared in the context." - -let rec pr_disjunction pr = function - | [a] -> pr a - | [a;b] -> pr a ++ str " or" ++ spc () ++ pr b - | a::l -> pr a ++ str "," ++ spc () ++ pr_disjunction pr l - | [] -> assert false - -let pr_puniverses f env (c,u) = - f env c ++ - (if Flags.is_universe_polymorphism () && not (Univ.Instance.is_empty u) then - str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)" - else mt()) - -let explain_elim_arity env sigma ind sorts c pj okinds = - let env = make_all_name_different env in - let pi = pr_inductive env (fst ind) in - let pc = pr_lconstr_env env sigma c in - let msg = match okinds with - | Some(kp,ki,explanation) -> - let pki = pr_sort_family ki in - let pkp = pr_sort_family kp in - let explanation = match explanation with - | NonInformativeToInformative -> - "proofs can be eliminated only to build proofs" - | StrongEliminationOnNonSmallType -> - "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 sigma ((strip_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 "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 "ill-formed elimination predicate." - in - hov 0 ( - str "Incorrect elimination of" ++ spc () ++ pc ++ spc () ++ - str "in the inductive type" ++ spc () ++ quote pi ++ str ":") ++ - fnl () ++ msg - -let explain_case_not_inductive env sigma cj = - let cj = Evarutil.j_nf_evar sigma cj in - let env = make_all_name_different env in - let pc = pr_lconstr_env env sigma cj.uj_val in - let pct = pr_lconstr_env env sigma cj.uj_type in - match kind_of_term cj.uj_type with - | 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." - -let explain_number_branches env sigma cj expn = - let cj = Evarutil.j_nf_evar sigma cj in - let env = make_all_name_different env in - let pc = pr_lconstr_env env sigma cj.uj_val in - let pct = pr_lconstr_env env sigma cj.uj_type in - str "Matching on term" ++ brk(1,1) ++ pc ++ spc () ++ - str "of type" ++ brk(1,1) ++ pct ++ spc () ++ - str "expects " ++ int expn ++ str " branches." - -let explain_ill_formed_branch env sigma c ci actty expty = - let simp t = Reduction.nf_betaiota env (Evarutil.nf_evar sigma t) in - let c = Evarutil.nf_evar sigma c in - let env = make_all_name_different env in - let pc = pr_lconstr_env env sigma c in - let pa, pe = pr_explicit env sigma (simp actty) (simp expty) in - strbrk "In pattern-matching on term" ++ brk(1,1) ++ pc ++ - spc () ++ strbrk "the branch for constructor" ++ spc () ++ - quote (pr_puniverses pr_constructor env ci) ++ - spc () ++ str "has type" ++ brk(1,1) ++ pa ++ spc () ++ - str "which should be" ++ brk(1,1) ++ pe ++ str "." - -let explain_generalization env sigma (name,var) j = - let pe = pr_ne_context_of (str "In environment") env sigma in - let pv = pr_ltype_env env sigma var in - let (pc,pt) = pr_ljudge_env (push_rel_assum (name,var) env) sigma j in - 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_unification_error env sigma p1 p2 = function - | None -> mt() - | Some e -> - let rec aux p1 p2 = function - | OccurCheck (evk,rhs) -> - let rhs = Evarutil.nf_evar sigma rhs in - [str "cannot define " ++ quote (pr_existential_key sigma evk) ++ - strbrk " with term " ++ pr_lconstr_env env sigma rhs ++ - strbrk " that would depend on itself"] - | NotClean ((evk,args),env,c) -> - let c = Evarutil.nf_evar sigma c in - let args = Array.map (Evarutil.nf_evar sigma) args in - [str "cannot instantiate " ++ quote (pr_existential_key sigma evk) - ++ strbrk " because " ++ pr_lconstr_env env sigma c ++ - strbrk " is not in its scope" ++ - (if Array.is_empty args then mt() else - strbrk ": available arguments are " ++ - pr_sequence (pr_lconstr_env env sigma) (List.rev (Array.to_list args)))] - | NotSameArgSize | NotSameHead | NoCanonicalStructure -> - (* Error speaks from itself *) [] - | ConversionFailed (env,t1,t2) -> - if Term.eq_constr t1 p1 && Term.eq_constr t2 p2 then [] else - let env = make_all_name_different env in - let t1 = Evarutil.nf_evar sigma t1 in - let t2 = Evarutil.nf_evar sigma t2 in - if not (Term.eq_constr t1 p1) || not (Term.eq_constr t2 p2) then - let t1, t2 = pr_explicit env sigma t1 t2 in - [str "cannot unify " ++ t1 ++ strbrk " and " ++ t2] - else [] - | MetaOccurInBody evk -> - [str "instance for " ++ quote (pr_existential_key sigma evk) ++ - strbrk " refers to a metavariable - please report your example" ++ - strbrk "at " ++ str Coq_config.wwwbugtracker ++ str "."] - | InstanceNotSameType (evk,env,t,u) -> - let t, u = pr_explicit env sigma t u in - [str "unable to find a well-typed instantiation for " ++ - quote (pr_existential_key sigma evk) ++ - strbrk ": cannot ensure that " ++ - t ++ strbrk " is a subtype of " ++ u] - | UnifUnivInconsistency p -> - if !Constrextern.print_universes then - [str "universe inconsistency: " ++ - Univ.explain_universe_inconsistency Universes.pr_with_global_universes p] - else - [str "universe inconsistency"] - | CannotSolveConstraint ((pb,env,t,u),e) -> - let t = Evarutil.nf_evar sigma t in - let u = Evarutil.nf_evar sigma u in - let env = make_all_name_different env in - (strbrk "cannot satisfy constraint " ++ pr_lconstr_env env sigma t ++ - str " == " ++ pr_lconstr_env env sigma u) - :: aux t u e - | ProblemBeyondCapabilities -> - [] - in - match aux p1 p2 e with - | [] -> mt () - | l -> spc () ++ str "(" ++ - prlist_with_sep pr_semicolon (fun x -> x) l ++ str ")" - -let explain_actual_type env sigma j t reason = - let env = make_all_name_different env in - let j = j_nf_betaiotaevar sigma j in - let t = Reductionops.nf_betaiota sigma t in - (** Actually print *) - let pe = pr_ne_context_of (str "In environment") env sigma in - let pc = pr_lconstr_env env sigma (Environ.j_val j) in - let (pt, pct) = pr_explicit env sigma t (Environ.j_type j) in - let ppreason = explain_unification_error env sigma j.uj_type t reason in - pe ++ - hov 0 ( - str "The term" ++ brk(1,1) ++ pc ++ spc () ++ - str "has type" ++ brk(1,1) ++ pct ++ spc () ++ - str "while it is expected to have type" ++ brk(1,1) ++ pt ++ - ppreason ++ str ".") - -let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl = - let randl = jv_nf_betaiotaevar sigma randl in - let exptyp = Evarutil.nf_evar sigma exptyp in - let actualtyp = Reductionops.nf_betaiota sigma actualtyp in - let rator = Evarutil.j_nf_evar sigma rator in - let env = make_all_name_different env in - let actualtyp, exptyp = pr_explicit env sigma actualtyp exptyp in - let nargs = Array.length randl in -(* let pe = pr_ne_context_of (str "in environment") env sigma in*) - let pr,prt = pr_ljudge_env env sigma rator in - let term_string1 = str (String.plural nargs "term") in - let term_string2 = - if nargs>1 then str "The " ++ pr_nth n ++ str " term" else str "This term" - in - let appl = prvect_with_sep fnl - (fun c -> - let pc,pct = pr_ljudge_env env sigma c in - hov 2 (pc ++ spc () ++ str ": " ++ pct)) randl - in - str "Illegal application: " ++ (* 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) ++ actualtyp ++ spc () ++ - str "which should be coercible to" ++ brk(1,1) ++ - exptyp ++ str "." - -let explain_cant_apply_not_functional env sigma rator randl = - let randl = Evarutil.jv_nf_evar sigma randl in - let rator = Evarutil.j_nf_evar sigma rator in - let env = make_all_name_different env in - let nargs = Array.length randl in -(* let pe = pr_ne_context_of (str "in environment") env sigma in*) - let pr = pr_lconstr_env env sigma rator.uj_val in - let prt = pr_lconstr_env env sigma rator.uj_type in - let appl = prvect_with_sep fnl - (fun c -> - let pc = pr_lconstr_env env sigma c.uj_val in - let pct = pr_lconstr_env env sigma c.uj_type in - hov 2 (pc ++ spc () ++ str ": " ++ pct)) randl - in - 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 " ++ str (String.plural nargs "term") ++ - fnl () ++ str " " ++ v 0 appl - -let explain_unexpected_type env sigma actual_type expected_type = - let actual_type = Evarutil.nf_evar sigma actual_type in - let expected_type = Evarutil.nf_evar sigma expected_type in - let pract, prexp = pr_explicit env sigma actual_type expected_type in - str "Found type" ++ spc () ++ pract ++ spc () ++ - str "where" ++ spc () ++ prexp ++ str " was expected." - -let explain_not_product env sigma c = - let c = Evarutil.nf_evar sigma c in - let pr = pr_lconstr_env env sigma 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 "." - -(* TODO: use the names *) -(* (co)fixpoints *) -let explain_ill_formed_rec_body env sigma err names i fixenv vdefj = - let prt_name i = - match names.(i) with - Name id -> str "Recursive definition of " ++ pr_id id - | Anonymous -> str "The " ++ pr_nth i ++ str " definition" in - - let st = match err with - - (* Fixpoint guard errors *) - | NotEnoughAbstractionInFixBody -> - str "Not enough abstractions in the definition" - | RecursionNotOnInductiveType c -> - str "Recursive definition on" ++ spc () ++ pr_lconstr_env env sigma c ++ - spc () ++ str "which should be an inductive type" - | RecursionOnIllegalTerm(j,(arg_env, arg),le,lt) -> - let arg_env = make_all_name_different arg_env in - let called = - match names.(j) with - Name id -> pr_id id - | Anonymous -> str "the " ++ pr_nth i ++ str " definition" in - let pr_db x = quote (pr_db env x) in - let vars = - match (lt,le) with - ([],[]) -> assert false - | ([],[x]) -> str "a subterm of " ++ pr_db x - | ([],_) -> str "a subterm of the following variables: " ++ - pr_sequence pr_db le - | ([x],_) -> pr_db x - | _ -> - str "one of the following variables: " ++ - pr_sequence pr_db lt in - str "Recursive call to " ++ called ++ spc () ++ - strbrk "has principal argument equal to" ++ spc () ++ - pr_lconstr_env arg_env sigma arg ++ strbrk " instead of " ++ vars - - | NotEnoughArgumentsForFixCall j -> - let called = - match names.(j) with - Name id -> pr_id id - | Anonymous -> str "the " ++ pr_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 sigma c ++ spc () ++ - str "which should be a coinductive type" - | NestedRecursiveOccurrences -> - str "Nested recursive occurrences" - | UnguardedRecursiveCall c -> - str "Unguarded recursive call in" ++ spc () ++ pr_lconstr_env env sigma c - | RecCallInTypeOfAbstraction c -> - str "Recursive call forbidden in the domain of an abstraction:" ++ - spc () ++ pr_lconstr_env env sigma c - | RecCallInNonRecArgOfConstructor c -> - str "Recursive call on a non-recursive argument of constructor" ++ - spc () ++ pr_lconstr_env env sigma c - | RecCallInTypeOfDef c -> - str "Recursive call forbidden in the type of a recursive definition" ++ - spc () ++ pr_lconstr_env env sigma c - | RecCallInCaseFun c -> - str "Invalid recursive call in a branch of" ++ - spc () ++ pr_lconstr_env env sigma c - | RecCallInCaseArg c -> - str "Invalid recursive call in the argument of \"match\" in" ++ spc () ++ - pr_lconstr_env env sigma c - | RecCallInCasePred c -> - str "Invalid recursive call in the \"return\" clause of \"match\" in" ++ - spc () ++ pr_lconstr_env env sigma c - | NotGuardedForm c -> - str "Sub-expression " ++ pr_lconstr_env env sigma c ++ - strbrk " not in guarded form (should be a constructor," ++ - strbrk " an abstraction, a match, a cofix or a recursive call)" - | ReturnPredicateNotCoInductive c -> - str "The return clause of the following pattern matching should be" ++ - strbrk " a coinductive type:" ++ - spc () ++ pr_lconstr_env env sigma c - in - prt_name i ++ str " is ill-formed." ++ fnl () ++ - pr_ne_context_of (str "In environment") env sigma ++ - st ++ str "." ++ fnl () ++ - (try (* May fail with unresolved globals. *) - let fixenv = make_all_name_different fixenv in - let pvd = pr_lconstr_env fixenv sigma vdefj.(i).uj_val in - str"Recursive definition is:" ++ spc () ++ pvd ++ str "." - with e when CErrors.noncritical e -> mt ()) - -let explain_ill_typed_rec_body env sigma i names vdefj vargs = - let vdefj = Evarutil.jv_nf_evar sigma vdefj in - let vargs = Array.map (Evarutil.nf_evar sigma) vargs in - let env = make_all_name_different env in - let pvd = pr_lconstr_env env sigma vdefj.(i).uj_val in - let pvdt, pv = pr_explicit env sigma vdefj.(i).uj_type vargs.(i) in - str "The " ++ - (match vdefj with [|_|] -> mt () | _ -> pr_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 sigma c = - let c = Evarutil.nf_evar sigma c in - let env = make_all_name_different env in - let pe = pr_lconstr_env env sigma c in - str "Cannot infer the return type of pattern-matching on" ++ ws 1 ++ - pe ++ str "." - -let explain_occur_check env sigma ev rhs = - let rhs = Evarutil.nf_evar sigma rhs in - let env = make_all_name_different env in - let pt = pr_lconstr_env env sigma rhs in - str "Cannot define " ++ pr_existential_key sigma ev ++ str " with term" ++ - brk(1,1) ++ pt ++ spc () ++ str "that would depend on itself." - -let pr_trailing_ne_context_of env sigma = - if List.is_empty (Environ.rel_context env) && - List.is_empty (Environ.named_context env) - then str "." - else (str " in environment:"++ pr_context_unlimited env sigma) - -let rec explain_evar_kind env sigma evk ty = function - | Evar_kinds.QuestionMark _ -> - strbrk "this placeholder of type " ++ ty - | Evar_kinds.CasesType false -> - strbrk "the type of this pattern-matching problem" - | Evar_kinds.CasesType true -> - strbrk "a subterm of type " ++ ty ++ - strbrk " in the type of this pattern-matching problem" - | Evar_kinds.BinderType (Name id) -> - strbrk "the type of " ++ Nameops.pr_id id - | Evar_kinds.BinderType Anonymous -> - strbrk "the type of this anonymous binder" - | Evar_kinds.ImplicitArg (c,(n,ido),b) -> - let id = Option.get ido in - strbrk "the implicit parameter " ++ pr_id id ++ spc () ++ str "of" ++ - spc () ++ Nametab.pr_global_env Id.Set.empty c ++ - strbrk " whose type is " ++ ty - | Evar_kinds.InternalHole -> strbrk "an internal placeholder of type " ++ ty - | Evar_kinds.TomatchTypeParameter (tyi,n) -> - strbrk "the " ++ pr_nth n ++ - strbrk " argument of the inductive type (" ++ pr_inductive env tyi ++ - strbrk ") of this term" - | Evar_kinds.GoalEvar -> - strbrk "an existential variable of type " ++ ty - | Evar_kinds.ImpossibleCase -> - strbrk "the type of an impossible pattern-matching clause" - | Evar_kinds.MatchingVar _ -> - assert false - | Evar_kinds.VarInstance id -> - strbrk "an instance of type " ++ ty ++ - str " for the variable " ++ pr_id id - | Evar_kinds.SubEvar evk' -> - let evi = Evd.find sigma evk' in - let pc = match evi.evar_body with - | Evar_defined c -> pr_lconstr_env env sigma (Evarutil.nf_evar sigma c) - | Evar_empty -> assert false in - let ty' = Evarutil.nf_evar sigma evi.evar_concl in - pr_existential_key sigma evk ++ str " of type " ++ ty ++ - str " in the partial instance " ++ pc ++ - str " found for " ++ explain_evar_kind env sigma evk' - (pr_lconstr_env env sigma ty') (snd evi.evar_source) - -let explain_typeclass_resolution env sigma evi k = - match Typeclasses.class_of_constr evi.evar_concl with - | Some _ -> - let env = Evd.evar_filtered_env evi in - fnl () ++ str "Could not find an instance for " ++ - pr_lconstr_env env sigma evi.evar_concl ++ - pr_trailing_ne_context_of env sigma - | _ -> mt() - -let explain_placeholder_kind env sigma c e = - match e with - | Some (SeveralInstancesFound n) -> - strbrk " (several distinct possible type class instances found)" - | None -> - match Typeclasses.class_of_constr c with - | Some _ -> strbrk " (no type class instance found)" - | _ -> mt () - -let explain_unsolvable_implicit env sigma evk explain = - let evi = Evarutil.nf_evar_info sigma (Evd.find_undefined sigma evk) in - let env = Evd.evar_filtered_env evi in - let type_of_hole = pr_lconstr_env env sigma evi.evar_concl in - let pe = pr_trailing_ne_context_of env sigma in - strbrk "Cannot infer " ++ - explain_evar_kind env sigma evk type_of_hole (snd evi.evar_source) ++ - explain_placeholder_kind env sigma evi.evar_concl explain ++ pe - -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,u) ci = - let pi = pr_inductive (Global.env()) ind in - if eq_ind ci.ci_ind ind then - str "Pattern-matching expression on an object of inductive type" ++ - spc () ++ pi ++ spc () ++ str "has invalid information." - else - 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 sigma m n e = - let env = make_all_name_different env in - let m = Evarutil.nf_evar sigma m in - let n = Evarutil.nf_evar sigma n in - let pm, pn = pr_explicit env sigma m n in - let ppreason = explain_unification_error env sigma m n e in - let pe = pr_ne_context_of (str "In environment") env sigma in - pe ++ str "Unable to unify" ++ brk(1,1) ++ pm ++ spc () ++ - str "with" ++ brk(1,1) ++ pn ++ ppreason ++ str "." - -let explain_cannot_unify_local env sigma m n subn = - let pm = pr_lconstr_env env sigma m in - let pn = pr_lconstr_env env sigma n in - let psubn = pr_lconstr_env env sigma subn in - str "Unable 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 sigma ty = - str "Cannot find a well-typed generalisation of the goal with type: " ++ - pr_lconstr_env env sigma ty ++ str "." - -let explain_no_occurrence_found env sigma c id = - str "Found no subterm matching " ++ pr_lconstr_env env sigma c ++ - str " in " ++ - (match id with - | Some id -> pr_id id - | None -> str"the current goal") ++ str "." - -let explain_cannot_unify_binding_type env sigma m n = - let pm = pr_lconstr_env env sigma m in - let pn = pr_lconstr_env env sigma n in - str "This binding has type" ++ brk(1,1) ++ pm ++ spc () ++ - str "which should be unifiable with" ++ brk(1,1) ++ pn ++ str "." - -let explain_cannot_find_well_typed_abstraction env sigma p l e = - str "Abstracting over the " ++ - str (String.plural (List.length l) "term") ++ spc () ++ - hov 0 (pr_enum (pr_lconstr_env env sigma) l) ++ spc () ++ - str "leads to a term" ++ spc () ++ pr_lconstr_goal_style_env env sigma p ++ - spc () ++ str "which is ill-typed." ++ - (match e with None -> mt () | Some e -> fnl () ++ str "Reason is: " ++ e) - -let explain_wrong_abstraction_type env sigma na abs expected result = - let ppname = match na with Name id -> pr_id id ++ spc () | _ -> mt () in - str "Cannot instantiate metavariable " ++ ppname ++ strbrk "of type " ++ - pr_lconstr_env env sigma expected ++ strbrk " with abstraction " ++ - pr_lconstr_env env sigma abs ++ strbrk " of incompatible type " ++ - pr_lconstr_env env sigma result ++ str "." - -let explain_abstraction_over_meta _ m n = - strbrk "Too complex unification problem: cannot find a solution for both " ++ - pr_name m ++ spc () ++ str "and " ++ pr_name n ++ str "." - -let explain_non_linear_unification env sigma m t = - strbrk "Cannot unambiguously instantiate " ++ - pr_name m ++ str ":" ++ - strbrk " which would require to abstract twice on " ++ - pr_lconstr_env env sigma t ++ str "." - -let explain_unsatisfied_constraints env sigma cst = - strbrk "Unsatisfied constraints: " ++ - Univ.pr_constraints (Evd.pr_evd_level sigma) cst ++ - spc () ++ str "(maybe a bugged tactic)." - -let explain_type_error env sigma err = - let env = make_all_name_different env in - match err with - | UnboundRel n -> - explain_unbound_rel env sigma n - | UnboundVar v -> - explain_unbound_var env v - | NotAType j -> - explain_not_type env sigma j - | BadAssumption c -> - explain_bad_assumption env sigma c - | ReferenceVariables (id,c) -> - explain_reference_variables id c - | ElimArity (ind, aritylst, c, pj, okinds) -> - explain_elim_arity env sigma ind aritylst c pj okinds - | CaseNotInductive cj -> - explain_case_not_inductive env sigma cj - | NumberBranches (cj, n) -> - explain_number_branches env sigma cj n - | IllFormedBranch (c, i, actty, expty) -> - explain_ill_formed_branch env sigma c i actty expty - | Generalization (nvar, c) -> - explain_generalization env sigma nvar c - | ActualType (j, pt) -> - explain_actual_type env sigma j pt None - | CantApplyBadType (t, rator, randl) -> - explain_cant_apply_bad_type env sigma t rator randl - | CantApplyNonFunctional (rator, randl) -> - explain_cant_apply_not_functional env sigma rator randl - | IllFormedRecBody (err, lna, i, fixenv, vdefj) -> - explain_ill_formed_rec_body env sigma err lna i fixenv vdefj - | IllTypedRecBody (i, lna, vdefj, vargs) -> - explain_ill_typed_rec_body env sigma i lna vdefj vargs - | WrongCaseInfo (ind,ci) -> - explain_wrong_case_info env ind ci - | UnsatisfiedConstraints cst -> - explain_unsatisfied_constraints env sigma cst - -let pr_position (cl,pos) = - let clpos = match cl with - | None -> str " of the goal" - | Some (id,Locus.InHyp) -> str " of hypothesis " ++ pr_id id - | Some (id,Locus.InHypTypeOnly) -> str " of the type of hypothesis " ++ pr_id id - | Some (id,Locus.InHypValueOnly) -> str " of the body of hypothesis " ++ pr_id id in - int pos ++ clpos - -let explain_cannot_unify_occurrences env sigma nested ((cl2,pos2),t2) ((cl1,pos1),t1) e = - if nested then - str "Found nested occurrences of the pattern at positions " ++ - int pos1 ++ strbrk " and " ++ pr_position (cl2,pos2) ++ str "." - else - let ppreason = match e with None -> mt() | Some (c1,c2,e) -> explain_unification_error env sigma c1 c2 (Some e) in - str "Found incompatible occurrences of the pattern" ++ str ":" ++ - spc () ++ str "Matched term " ++ pr_lconstr_env env sigma t2 ++ - strbrk " at position " ++ pr_position (cl2,pos2) ++ - strbrk " is not compatible with matched term " ++ - pr_lconstr_env env sigma t1 ++ strbrk " at position " ++ - pr_position (cl1,pos1) ++ ppreason ++ str "." - -let pr_constraints printenv env sigma evars cstrs = - let (ev, evi) = Evar.Map.choose evars in - if Evar.Map.for_all (fun ev' evi' -> - eq_named_context_val evi.evar_hyps evi'.evar_hyps) evars - then - let l = Evar.Map.bindings evars in - let env' = reset_with_named_context evi.evar_hyps env in - let pe = - if printenv then - pr_ne_context_of (str "In environment:") env' sigma - else mt () - in - let evs = - prlist - (fun (ev, evi) -> fnl () ++ pr_existential_key sigma ev ++ - str " : " ++ pr_lconstr_env env' sigma evi.evar_concl ++ fnl ()) l - in - h 0 (pe ++ evs ++ pr_evar_constraints cstrs) - else - let filter evk _ = Evar.Map.mem evk evars in - pr_evar_map_filter ~with_univs:false filter sigma - -let explain_unsatisfiable_constraints env sigma constr comp = - let (_, constraints) = Evd.extract_all_conv_pbs sigma in - let undef = Evd.undefined_map (Evarutil.nf_evar_map_undefined sigma) in - (** Only keep evars that are subject to resolution and members of the given - component. *) - let is_kept evk evi = match comp with - | None -> Typeclasses.is_resolvable evi - | Some comp -> Typeclasses.is_resolvable evi && Evar.Set.mem evk comp - in - let undef = - let m = Evar.Map.filter is_kept undef in - if Evar.Map.is_empty m then undef - else m - in - match constr with - | None -> - str "Unable to satisfy the following constraints:" ++ fnl () ++ - pr_constraints true env sigma undef constraints - | Some (ev, k) -> - let cstr = - let remaining = Evar.Map.remove ev undef in - if not (Evar.Map.is_empty remaining) then - str "With the following constraints:" ++ fnl () ++ - pr_constraints false env sigma remaining constraints - else mt () - in - let info = Evar.Map.find ev undef in - explain_typeclass_resolution env sigma info k ++ fnl () ++ cstr - -let explain_pretype_error env sigma err = - let env = Evardefine.env_nf_betaiotaevar sigma env in - let env = make_all_name_different env in - match err with - | CantFindCaseType c -> explain_cant_find_case_type env sigma c - | ActualTypeNotCoercible (j,t,e) -> - let {uj_val = c; uj_type = actty} = j in - let (env, c, actty, expty), e = contract3' env c actty t e in - let j = {uj_val = c; uj_type = actty} in - explain_actual_type env sigma j expty (Some e) - | UnifOccurCheck (ev,rhs) -> explain_occur_check env sigma ev rhs - | UnsolvableImplicit (evk,exp) -> explain_unsolvable_implicit env sigma evk exp - | VarNotFound id -> explain_var_not_found env id - | UnexpectedType (actual,expect) -> - let env, actual, expect = contract2 env actual expect in - explain_unexpected_type env sigma actual expect - | NotProduct c -> explain_not_product env sigma c - | CannotUnify (m,n,e) -> - let env, m, n = contract2 env m n in - explain_cannot_unify env sigma m n e - | CannotUnifyLocal (m,n,sn) -> explain_cannot_unify_local env sigma m n sn - | CannotGeneralize ty -> explain_refiner_cannot_generalize env sigma ty - | NoOccurrenceFound (c, id) -> explain_no_occurrence_found env sigma c id - | CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type env sigma m n - | CannotFindWellTypedAbstraction (p,l,e) -> - explain_cannot_find_well_typed_abstraction env sigma p l - (Option.map (fun (env',e) -> explain_type_error env' sigma e) e) - | WrongAbstractionType (n,a,t,u) -> - explain_wrong_abstraction_type env sigma n a t u - | AbstractionOverMeta (m,n) -> explain_abstraction_over_meta env m n - | NonLinearUnification (m,c) -> explain_non_linear_unification env sigma m c - | TypingError t -> explain_type_error env sigma t - | CannotUnifyOccurrences (b,c1,c2,e) -> explain_cannot_unify_occurrences env sigma b c1 c2 e - | UnsatisfiableConstraints (c,comp) -> explain_unsatisfiable_constraints env sigma c comp -(* Module errors *) - -open Modops - -let explain_not_match_error = function - | InductiveFieldExpected _ -> - strbrk "an inductive definition is expected" - | DefinitionFieldExpected -> - strbrk "a definition is expected" - | ModuleFieldExpected -> - strbrk "a module is expected" - | ModuleTypeFieldExpected -> - strbrk "a module type is expected" - | NotConvertibleInductiveField id | NotConvertibleConstructorField id -> - str "types given to " ++ pr_id id ++ str " differ" - | NotConvertibleBodyField -> - str "the body of definitions differs" - | NotConvertibleTypeField (env, typ1, typ2) -> - str "expected type" ++ spc () ++ - quote (Printer.safe_pr_lconstr_env env Evd.empty typ2) ++ spc () ++ - str "but found type" ++ spc () ++ - quote (Printer.safe_pr_lconstr_env env Evd.empty typ1) - | NotSameConstructorNamesField -> - str "constructor names differ" - | NotSameInductiveNameInBlockField -> - str "inductive types names differ" - | FiniteInductiveFieldExpected isfinite -> - str "type is expected to be " ++ - str (if isfinite then "coinductive" else "inductive") - | InductiveNumbersFieldExpected n -> - str "number of inductive types differs" - | InductiveParamsNumberField n -> - str "inductive type has not the right number of parameters" - | RecordFieldExpected isrecord -> - str "type is expected " ++ str (if isrecord then "" else "not ") ++ - str "to be a record" - | RecordProjectionsExpected nal -> - (if List.length nal >= 2 then str "expected projection names are " - else str "expected projection name is ") ++ - pr_enum (function Name id -> pr_id id | _ -> str "_") nal - | NotEqualInductiveAliases -> - str "Aliases to inductive types do not match" - | NoTypeConstraintExpected -> - strbrk "a definition whose type is constrained can only be subtype " ++ - strbrk "of a definition whose type is itself constrained" - | PolymorphicStatusExpected b -> - let status b = if b then str"polymorphic" else str"monomorphic" in - str "a " ++ status b ++ str" declaration was expected, but a " ++ - status (not b) ++ str" declaration was found" - | IncompatibleInstances -> - str"polymorphic universe instances do not match" - | IncompatibleUniverses incon -> - str"the universe constraints are inconsistent: " ++ - Univ.explain_universe_inconsistency Universes.pr_with_global_universes incon - | IncompatiblePolymorphism (env, t1, t2) -> - str "conversion of polymorphic values generates additional constraints: " ++ - quote (Printer.safe_pr_lconstr_env env Evd.empty t1) ++ spc () ++ - str "compared to " ++ spc () ++ - quote (Printer.safe_pr_lconstr_env env Evd.empty t2) - | IncompatibleConstraints cst -> - str " the expected (polymorphic) constraints do not imply " ++ - quote (Univ.pr_constraints (Evd.pr_evd_level Evd.empty) cst) - -let explain_signature_mismatch l spec why = - str "Signature components for label " ++ pr_label l ++ - str " do not match:" ++ spc () ++ explain_not_match_error why ++ str "." - -let explain_label_already_declared l = - str "The label " ++ pr_label l ++ str " is already declared." - -let explain_application_to_not_path _ = - strbrk "A module cannot be applied to another module application or " ++ - strbrk "with-expression; you must give a name to the intermediate result " ++ - strbrk "module first." - -let explain_not_a_functor () = - str "Application of a non-functor." - -let explain_is_a_functor () = - str "Illegal use of a functor." - -let explain_incompatible_module_types mexpr1 mexpr2 = - let open Declarations in - let rec get_arg = function - | NoFunctor _ -> 0 - | MoreFunctor (_, _, ty) -> succ (get_arg ty) - in - let len1 = get_arg mexpr1.mod_type in - let len2 = get_arg mexpr2.mod_type in - if len1 <> len2 then - str "Incompatible module types: module expects " ++ int len2 ++ - str " arguments, found " ++ int len1 ++ str "." - else str "Incompatible module types." - -let explain_not_equal_module_paths mp1 mp2 = - str "Non equal modules." - -let explain_no_such_label l = - str "No such label " ++ pr_label l ++ str "." - -let explain_incompatible_labels l l' = - str "Opening and closing labels are not the same: " ++ - pr_label l ++ str " <> " ++ pr_label l' ++ str "!" - -let explain_not_a_module s = - quote (str s) ++ str " is not a module." - -let explain_not_a_module_type s = - quote (str s) ++ str " is not a module type." - -let explain_not_a_constant l = - quote (pr_label l) ++ str " is not a constant." - -let explain_incorrect_label_constraint l = - str "Incorrect constraint for label " ++ - quote (pr_label l) ++ str "." - -let explain_generative_module_expected l = - str "The module " ++ pr_label l ++ str " is not generative." ++ - strbrk " Only components of generative modules can be changed" ++ - strbrk " using the \"with\" construct." - -let explain_label_missing l s = - str "The field " ++ pr_label l ++ str " is missing in " - ++ str s ++ str "." - -let explain_include_restricted_functor mp = - let q = Nametab.shortest_qualid_of_module mp in - str "Cannot include the functor " ++ Libnames.pr_qualid q ++ - strbrk " since it has a restricted signature. " ++ - strbrk "You may name first an instance of this functor, and include it." - -let explain_module_error = function - | SignatureMismatch (l,spec,err) -> explain_signature_mismatch l spec err - | LabelAlreadyDeclared l -> explain_label_already_declared l - | ApplicationToNotPath mexpr -> explain_application_to_not_path mexpr - | NotAFunctor -> explain_not_a_functor () - | IsAFunctor -> explain_is_a_functor () - | IncompatibleModuleTypes (m1,m2) -> explain_incompatible_module_types m1 m2 - | NotEqualModulePaths (mp1,mp2) -> explain_not_equal_module_paths mp1 mp2 - | NoSuchLabel l -> explain_no_such_label l - | IncompatibleLabels (l1,l2) -> explain_incompatible_labels l1 l2 - | NotAModule s -> explain_not_a_module s - | NotAModuleType s -> explain_not_a_module_type s - | NotAConstant l -> explain_not_a_constant l - | IncorrectWithConstraint l -> explain_incorrect_label_constraint l - | GenerativeModuleExpected l -> explain_generative_module_expected l - | LabelMissing (l,s) -> explain_label_missing l s - | IncludeRestrictedFunctor mp -> explain_include_restricted_functor mp - -(* Module internalization errors *) - -(* -let explain_declaration_not_path _ = - str "Declaration is not a path." - -*) - -let explain_not_module_nor_modtype s = - quote (str s) ++ str " is not a module or module type." - -let explain_incorrect_with_in_module () = - str "The syntax \"with\" is not allowed for modules." - -let explain_incorrect_module_application () = - str "Illegal application to a module type." - -open Modintern - -let explain_module_internalization_error = function - | NotAModuleNorModtype s -> explain_not_module_nor_modtype s - | IncorrectWithInModule -> explain_incorrect_with_in_module () - | IncorrectModuleApplication -> explain_incorrect_module_application () - -(* Typeclass errors *) - -let explain_not_a_class env c = - pr_constr_env env Evd.empty c ++ str" is not a declared type class." - -let explain_unbound_method env cid id = - str "Unbound method name " ++ Nameops.pr_id (snd id) ++ spc () ++ - str"of class" ++ spc () ++ pr_global cid ++ str "." - -let pr_constr_exprs exprs = - hv 0 (List.fold_right - (fun d pps -> ws 2 ++ Ppconstr.pr_constr_expr d ++ pps) - exprs (mt ())) - -let explain_mismatched_contexts env c i j = - str"Mismatched contexts while declaring instance: " ++ brk (1,1) ++ - hov 1 (str"Expected:" ++ brk (1, 1) ++ pr_rel_context env Evd.empty j) ++ - fnl () ++ brk (1,1) ++ - hov 1 (str"Found:" ++ brk (1, 1) ++ pr_constr_exprs i) - -let explain_typeclass_error env = function - | NotAClass c -> explain_not_a_class env c - | UnboundMethod (cid, id) -> explain_unbound_method env cid id - | MismatchedContextInstance (c,i,j) -> explain_mismatched_contexts env c i j - -(* Refiner errors *) - -let explain_refiner_bad_type arg ty conclty = - 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 "." - -let explain_refiner_unresolved_bindings l = - str "Unable to find an instance for the " ++ - str (String.plural (List.length l) "variable") ++ spc () ++ - prlist_with_sep pr_comma pr_name l ++ str"." - -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) ++ - pr_lconstr harg ++ str "." - -let explain_refiner_not_well_typed c = - str "The term " ++ pr_lconstr c ++ str " is not well-typed." - -let explain_intro_needs_product () = - 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 "." - -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." - -let explain_meta_in_type c = - str "In refiner, a meta appears in the type " ++ brk(1,1) ++ pr_lconstr c ++ - str " of another meta" - -let explain_no_such_hyp id = - str "No such hypothesis: " ++ pr_id id - -let explain_refiner_error = function - | BadType (arg,ty,conclty) -> explain_refiner_bad_type arg ty conclty - | UnresolvedBindings t -> explain_refiner_unresolved_bindings t - | CannotApply (t,harg) -> explain_refiner_cannot_apply t harg - | NotWellTyped c -> explain_refiner_not_well_typed c - | IntroNeedsProduct -> explain_intro_needs_product () - | DoesNotOccurIn (c,hyp) -> explain_does_not_occur_in c hyp - | NonLinearProof c -> explain_non_linear_proof c - | MetaInType c -> explain_meta_in_type c - | NoSuchHyp id -> explain_no_such_hyp id - -(* Inductive errors *) - -let error_non_strictly_positive env c v = - let pc = pr_lconstr_env env Evd.empty c in - let pv = pr_lconstr_env env Evd.empty v in - str "Non strictly positive occurrence of " ++ pv ++ str " in" ++ - brk(1,1) ++ pc ++ str "." - -let error_ill_formed_inductive env c v = - let pc = pr_lconstr_env env Evd.empty c in - let pv = pr_lconstr_env env Evd.empty v in - str "Not enough arguments applied to the " ++ pv ++ - str " in" ++ brk(1,1) ++ pc ++ str "." - -let error_ill_formed_constructor env id c v nparams nargs = - let pv = pr_lconstr_env env Evd.empty v in - let atomic = Int.equal (nb_prod c) 0 in - str "The type of constructor" ++ brk(1,1) ++ pr_id id ++ brk(1,1) ++ - str "is not valid;" ++ brk(1,1) ++ - strbrk (if atomic then "it must be " else "its conclusion must be ") ++ - pv ++ - (* warning: because of implicit arguments it is difficult to say which - parameters must be explicitly given *) - (if not (Int.equal nparams 0) then - strbrk " applied to its " ++ str (String.plural nparams "parameter") - else - mt()) ++ - (if not (Int.equal nargs 0) then - str (if not (Int.equal nparams 0) then " and" else " applied") ++ - strbrk " to some " ++ str (String.plural nargs "argument") - else - mt()) ++ str "." - -let pr_ltype_using_barendregt_convention_env env c = - (* Use goal_concl_style as an approximation of Barendregt's convention (?) *) - quote (pr_goal_concl_style_env env Evd.empty c) - -let error_bad_ind_parameters env c n v1 v2 = - let pc = pr_ltype_using_barendregt_convention_env env c in - let pv1 = pr_lconstr_env env Evd.empty v1 in - let pv2 = pr_lconstr_env env Evd.empty v2 in - str "Last occurrence of " ++ pv2 ++ str " must have " ++ pv1 ++ - str " as " ++ pr_nth n ++ str " argument in" ++ brk(1,1) ++ pc ++ str "." - -let error_same_names_types id = - str "The name" ++ spc () ++ pr_id id ++ spc () ++ - str "is used more than once." - -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 = - strbrk "The following names are used both as type names and constructor " ++ - str "names:" ++ spc () ++ - prlist_with_sep pr_comma pr_id idl ++ str "." - -let error_not_an_arity env c = - str "The type" ++ spc () ++ pr_lconstr_env env Evd.empty c ++ spc () ++ - str "is not an arity." - -let error_bad_entry () = - str "Bad inductive definition." - -let error_large_non_prop_inductive_not_in_type () = - str "Large non-propositional inductive types must be in Type." - -(* Recursion schemes errors *) - -let error_not_allowed_case_analysis isrec kind i = - str (if isrec then "Induction" else "Case analysis") ++ - strbrk " on sort " ++ pr_sort Evd.empty kind ++ - strbrk " is not allowed for inductive definition " ++ - pr_inductive (Global.env()) (fst i) ++ str "." - -let error_not_allowed_dependent_analysis isrec i = - str "Dependent " ++ str (if isrec then "Induction" else "Case analysis") ++ - strbrk " is not allowed for inductive definition " ++ - pr_inductive (Global.env()) i ++ str "." - -let error_not_mutual_in_scheme ind ind' = - if eq_ind 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 *) - -let explain_inductive_error = function - | NonPos (env,c,v) -> error_non_strictly_positive env c v - | NotEnoughArgs (env,c,v) -> error_ill_formed_inductive env c v - | NotConstructor (env,id,c,v,n,m) -> - error_ill_formed_constructor env id c v n m - | NonPar (env,c,n,v1,v2) -> error_bad_ind_parameters env c n v1 v2 - | SameNamesTypes id -> error_same_names_types id - | SameNamesConstructors id -> error_same_names_constructors id - | SameNamesOverlap idl -> error_same_names_overlap idl - | NotAnArity (env, c) -> error_not_an_arity env c - | BadEntry -> error_bad_entry () - | LargeNonPropInductiveNotInType -> - error_large_non_prop_inductive_not_in_type () - -(* Recursion schemes errors *) - -let explain_recursion_scheme_error = function - | NotAllowedCaseAnalysis (isrec,k,i) -> - error_not_allowed_case_analysis isrec k i - | NotMutualInScheme (ind,ind')-> error_not_mutual_in_scheme ind ind' - | NotAllowedDependentAnalysis (isrec, i) -> - error_not_allowed_dependent_analysis isrec i - -(* Pattern-matching errors *) - -let explain_bad_pattern env sigma cstr ty = - let env = make_all_name_different env in - let pt = pr_lconstr_env env sigma 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." - -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." - -let decline_string n s = - if Int.equal n 0 then str "no " ++ str s ++ str "s" - else if Int.equal n 1 then str "1 " ++ str s - else (int n ++ str " " ++ str s ++ str "s") - -let explain_wrong_numarg_constructor env cstr n = - str "The constructor " ++ pr_constructor env cstr ++ - str " (in type " ++ pr_inductive env (inductive_of_constructor cstr) ++ - str ") expects " ++ decline_string n "argument" ++ str "." - -let explain_wrong_numarg_inductive env ind n = - str "The inductive type " ++ pr_inductive env ind ++ - str " expects " ++ decline_string n "argument" ++ str "." - -let explain_unused_clause env pats = -(* Without localisation - let s = if List.length pats > 1 then "s" else "" in - (str ("Unused clause with pattern"^s) ++ spc () ++ - hov 0 (pr_sequence pr_cases_pattern pats) ++ str ")") -*) - str "This clause is redundant." - -let explain_non_exhaustive env pats = - str "Non exhaustive pattern-matching: no clause found for " ++ - str (String.plural (List.length pats) "pattern") ++ - spc () ++ hov 0 (prlist_with_sep pr_comma pr_cases_pattern pats) - -let explain_cannot_infer_predicate env sigma typs = - let env = make_all_name_different env in - let pr_branch (cstr,typ) = - let cstr,_ = decompose_app cstr in - str "For " ++ pr_lconstr_env env sigma cstr ++ str ": " ++ pr_lconstr_env env sigma typ - in - str "Unable to unify the types found in the branches:" ++ - spc () ++ hov 0 (prlist_with_sep fnl pr_branch (Array.to_list typs)) - -let explain_pattern_matching_error env sigma = function - | BadPattern (c,t) -> - explain_bad_pattern env sigma c t - | BadConstructor (c,ind) -> - explain_bad_constructor env c ind - | WrongNumargConstructor (c,n) -> - explain_wrong_numarg_constructor env c n - | WrongNumargInductive (c,n) -> - explain_wrong_numarg_inductive env c n - | UnusedClause tms -> - explain_unused_clause env tms - | NonExhaustive tms -> - explain_non_exhaustive env tms - | CannotInferPredicate typs -> - explain_cannot_infer_predicate env sigma typs - -let explain_reduction_tactic_error = function - | Tacred.InvalidAbstraction (env,sigma,c,(env',e)) -> - str "The abstracted term" ++ spc () ++ - quote (pr_goal_concl_style_env env sigma c) ++ - spc () ++ str "is not well typed." ++ fnl () ++ - explain_type_error env' Evd.empty e |