diff options
author | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-08 16:54:47 +0000 |
---|---|---|
committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-08 16:54:47 +0000 |
commit | 7e324da8bd211f01593952ac51bd309e80c7546a (patch) | |
tree | a53bb39cedf880b9fd2c21f317cb69c9dce58994 | |
parent | f71cbe1115db9c7997f1d45b5c419da597d30a59 (diff) |
Add more information to IllFormedRecBody exceptions, to show the exact
definition on which it is failing (useful for Program definitions and
others too).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10533 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | kernel/inductive.ml | 13 | ||||
-rw-r--r-- | kernel/type_errors.ml | 6 | ||||
-rw-r--r-- | kernel/type_errors.mli | 4 | ||||
-rw-r--r-- | tactics/decl_proof_instr.ml | 2 | ||||
-rw-r--r-- | toplevel/himsg.ml | 10 |
5 files changed, 21 insertions, 14 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 0b14038e3..aef3d6cc8 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -777,6 +777,8 @@ let check_one_fix renv recpos def = in check_rec_call renv def +let judgment_of_fixpoint (_, types, bodies) = + array_map2 (fun typ body -> { uj_val = body ; uj_type = typ }) types bodies let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = let nbfix = Array.length bodies in @@ -788,8 +790,9 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = or bodynum >= nbfix then anomaly "Ill-formed fix term"; let fixenv = push_rec_types recdef env in + let vdefj = judgment_of_fixpoint recdef in let raise_err env i err = - error_ill_formed_rec_body env err names i in + error_ill_formed_rec_body env err names i fixenv vdefj in (* Check the i-th definition with recarg k *) let find_ind i k def = (* check fi does not appear in the k+1 first abstractions, @@ -815,14 +818,15 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = (Array.map fst rv, Array.map snd rv) -let check_fix env ((nvect,_),(names,_,bodies as _recdef) as fix) = +let check_fix env ((nvect,_),(names,_,bodies as recdef) as fix) = let (minds, rdef) = inductive_of_mutfix env fix in for i = 0 to Array.length bodies - 1 do let (fenv,body) = rdef.(i) in let renv = make_renv fenv minds nvect.(i) minds.(i) in try check_one_fix renv nvect body with FixGuardError (fixenv,err) -> - error_ill_formed_rec_body fixenv err names i + error_ill_formed_rec_body fixenv err names i + (push_rec_types recdef env) (judgment_of_fixpoint recdef) done (* @@ -933,5 +937,6 @@ let check_cofix env (bodynum,(names,types,bodies as recdef)) = let fixenv = push_rec_types recdef env in try check_one_cofix fixenv nbfix bodies.(i) types.(i) with CoFixGuardError (errenv,err) -> - error_ill_formed_rec_body errenv err names i + error_ill_formed_rec_body errenv err names i + fixenv (judgment_of_fixpoint recdef) done diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index bbd3e4bf4..116a74947 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -56,7 +56,7 @@ type type_error = | CantApplyBadType of (int * constr * constr) * unsafe_judgment * unsafe_judgment array | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment array - | IllFormedRecBody of guard_error * name array * int + | IllFormedRecBody of guard_error * name array * int * env * unsafe_judgment array | IllTypedRecBody of int * name array * unsafe_judgment array * types array @@ -105,8 +105,8 @@ let error_cant_apply_not_functional env rator randl = let error_cant_apply_bad_type env t rator randl = raise (TypeError (env, CantApplyBadType (t,rator,randl))) -let error_ill_formed_rec_body env why lna i = - raise (TypeError (env, IllFormedRecBody (why,lna,i))) +let error_ill_formed_rec_body env why lna i fixenv vdefj = + raise (TypeError (env, IllFormedRecBody (why,lna,i,fixenv,vdefj))) let error_ill_typed_rec_body env i lna vdefj vargs = raise (TypeError (env, IllTypedRecBody (i,lna,vdefj,vargs))) diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index 6e480479e..38bd0d394 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -58,7 +58,7 @@ type type_error = | CantApplyBadType of (int * constr * constr) * unsafe_judgment * unsafe_judgment array | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment array - | IllFormedRecBody of guard_error * name array * int + | IllFormedRecBody of guard_error * name array * int * env * unsafe_judgment array | IllTypedRecBody of int * name array * unsafe_judgment array * types array @@ -96,7 +96,7 @@ val error_cant_apply_bad_type : unsafe_judgment -> unsafe_judgment array -> 'a val error_ill_formed_rec_body : - env -> guard_error -> name array -> int -> 'a + env -> guard_error -> name array -> int -> env -> unsafe_judgment array -> 'a val error_ill_typed_rec_body : env -> int -> name array -> unsafe_judgment array -> types array -> 'a diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml index 1d5ab017c..c4b7ad13c 100644 --- a/tactics/decl_proof_instr.ml +++ b/tactics/decl_proof_instr.ml @@ -1471,7 +1471,7 @@ let rec postprocess pts instr = goto_current_focus_or_top (mark_as_done pts) with Type_errors.TypeError(env, - Type_errors.IllFormedRecBody(_,_,_)) -> + Type_errors.IllFormedRecBody(_,_,_,_,_)) -> anomaly "\"end induction\" generated an ill-formed fixpoint" end | Pend _ -> diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 0b69c41e7..16f3971f5 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -214,7 +214,7 @@ let explain_not_product env c = (* TODO: use the names *) (* (co)fixpoints *) -let explain_ill_formed_rec_body env err names i = +let explain_ill_formed_rec_body env err names i fixenv vdefj = let prt_name i = match names.(i) with Name id -> str "Recursive definition of " ++ pr_id id @@ -286,9 +286,11 @@ let explain_ill_formed_rec_body env err names i = strbrk " not in guarded form (should be a constructor," ++ strbrk " an abstraction, a match, a cofix or a recursive call)" in + let pvd, pvdt = pr_ljudge_env fixenv vdefj.(i) in prt_name i ++ str " is ill-formed." ++ fnl () ++ pr_ne_context_of (str "In environment") env ++ - st ++ str "." + st ++ str "." ++ fnl () ++ + str"Recursive definition is:" ++ spc () ++ pvd ++ str "." let explain_ill_typed_rec_body env i names vdefj vargs = let env = make_all_name_different env in @@ -436,8 +438,8 @@ let explain_type_error env err = explain_cant_apply_bad_type env t rator randl | CantApplyNonFunctional (rator, randl) -> explain_cant_apply_not_functional env rator randl - | IllFormedRecBody (err, lna, i) -> - explain_ill_formed_rec_body env err lna i + | IllFormedRecBody (err, lna, i, fixenv, vdefj) -> + explain_ill_formed_rec_body env err lna i fixenv vdefj | IllTypedRecBody (i, lna, vdefj, vargs) -> explain_ill_typed_rec_body env i lna vdefj vargs | WrongCaseInfo (ind,ci) -> |