diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/inductive.ml | 13 | ||||
| -rw-r--r-- | kernel/type_errors.ml | 6 | ||||
| -rw-r--r-- | kernel/type_errors.mli | 4 |
3 files changed, 14 insertions, 9 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 0b14038e34..aef3d6cc82 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 bbd3e4bf4e..116a749476 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 6e480479ef..38bd0d394b 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 |