diff options
Diffstat (limited to 'pretyping/pretype_errors.ml')
| -rw-r--r-- | pretyping/pretype_errors.ml | 79 |
1 files changed, 30 insertions, 49 deletions
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index eb07addb07..cd2ed76c1f 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -38,8 +38,9 @@ type pretype_error = | VarNotFound of identifier | UnexpectedType of constr * constr | NotProduct of constr + | TypingError of type_error -exception PretypeError of env * pretype_error +exception PretypeError of env * Evd.evar_map * pretype_error let precatchable_exception = function | Util.UserError _ | TypeError _ | PretypeError _ @@ -55,13 +56,13 @@ let j_nf_betaiotaevar sigma j = { uj_val = nf_evar sigma j.uj_val; uj_type = Reductionops.nf_betaiota sigma j.uj_type } let jl_nf_evar sigma jl = List.map (j_nf_evar sigma) jl -let jl_nf_betaiotaevar sigma jl = - List.map (j_nf_betaiotaevar sigma) jl +let jv_nf_betaiotaevar sigma jl = + Array.map (j_nf_betaiotaevar sigma) jl let jv_nf_evar sigma = Array.map (j_nf_evar sigma) let tj_nf_evar sigma {utj_val=v;utj_type=t} = {utj_val=nf_evar sigma v;utj_type=t} -let env_ise sigma env = +let env_nf_evar sigma env = let sign = named_context_val env in let ctxt = rel_context env in let env0 = reset_with_named_context sign env in @@ -97,110 +98,90 @@ let contract2 env a b = match contract env [a;b] with let contract3 env a b c = match contract env [a;b;c] with | env, [a;b;c] -> env,a,b,c | _ -> assert false -let raise_pretype_error (loc,ctx,sigma,te) = - Loc.raise loc (PretypeError(env_ise sigma ctx,te)) +let raise_pretype_error (loc,env,sigma,te) = + Loc.raise loc (PretypeError(env,sigma,te)) -let raise_located_type_error (loc,ctx,sigma,te) = - Loc.raise loc (TypeError(env_ise sigma ctx,te)) +let raise_located_type_error (loc,env,sigma,te) = + Loc.raise loc (PretypeError(env,sigma,TypingError te)) let error_actual_type_loc loc env sigma {uj_val=c;uj_type=actty} expty = let env, c, actty, expty = contract3 env c actty expty in - let j = j_nf_evar sigma {uj_val=c;uj_type=actty} in - raise_located_type_error - (loc, env, sigma, ActualType (j, nf_evar sigma expty)) + let j = {uj_val=c;uj_type=actty} in + raise_located_type_error (loc, env, sigma, ActualType (j, expty)) let error_cant_apply_not_functional_loc loc env sigma rator randl = - let ja = Array.of_list (jl_nf_evar sigma randl) in raise_located_type_error - (loc, env, sigma, - CantApplyNonFunctional (j_nf_evar sigma rator, ja)) + (loc, env, sigma, CantApplyNonFunctional (rator, Array.of_list randl)) let error_cant_apply_bad_type_loc loc env sigma (n,c,t) rator randl = - let ja = Array.of_list (jl_nf_betaiotaevar sigma randl) in raise_located_type_error (loc, env, sigma, - CantApplyBadType - ((n,nf_evar sigma c, Reductionops.nf_betaiota sigma t), - j_nf_evar sigma rator, ja)) + CantApplyBadType ((n,c,t), rator, Array.of_list randl)) let error_ill_formed_branch_loc loc env sigma c i actty expty = - let simp t = Reduction.nf_betaiota (nf_evar sigma t) in raise_located_type_error - (loc, env, sigma, - IllFormedBranch (nf_evar sigma c,i,simp actty, simp expty)) + (loc, env, sigma, IllFormedBranch (c, i, actty, expty)) let error_number_branches_loc loc env sigma cj expn = - raise_located_type_error - (loc, env, sigma, - NumberBranches (j_nf_evar sigma cj, expn)) + raise_located_type_error (loc, env, sigma, NumberBranches (cj, expn)) let error_case_not_inductive_loc loc env sigma cj = - raise_located_type_error - (loc, env, sigma, CaseNotInductive (j_nf_evar sigma cj)) + raise_located_type_error (loc, env, sigma, CaseNotInductive cj) let error_ill_typed_rec_body_loc loc env sigma i na jl tys = raise_located_type_error - (loc, env, sigma, - IllTypedRecBody (i,na,jv_nf_evar sigma jl, - Array.map (nf_evar sigma) tys)) + (loc, env, sigma, IllTypedRecBody (i, na, jl, tys)) let error_not_a_type_loc loc env sigma j = - raise_located_type_error (loc, env, sigma, NotAType (j_nf_evar sigma j)) + raise_located_type_error (loc, env, sigma, NotAType j) (*s Implicit arguments synthesis errors. It is hard to find a precise location. *) let error_occur_check env sigma ev c = - let c = nf_evar sigma c in - raise (PretypeError (env_ise sigma env, OccurCheck (ev,c))) + raise (PretypeError (env, sigma, OccurCheck (ev,c))) let error_not_clean env sigma ev c (loc,k) = - let c = nf_evar sigma c in - Loc.raise loc - (PretypeError (env_ise sigma env, NotClean (ev,c,k))) + Loc.raise loc (PretypeError (env, sigma, NotClean (ev,c,k))) let error_unsolvable_implicit loc env sigma evi e explain = Loc.raise loc - (PretypeError (env_ise sigma env, UnsolvableImplicit (evi, e, explain))) + (PretypeError (env, sigma, UnsolvableImplicit (evi, e, explain))) let error_cannot_unify env sigma (m,n) = - let m = nf_evar sigma m and n = nf_evar sigma n in - raise (PretypeError (env_ise sigma env,CannotUnify (m,n))) + raise (PretypeError (env, sigma,CannotUnify (m,n))) let error_cannot_unify_local env sigma (m,n,sn) = - raise (PretypeError (env_ise sigma env,CannotUnifyLocal (m,n,sn))) + raise (PretypeError (env, sigma,CannotUnifyLocal (m,n,sn))) let error_cannot_coerce env sigma (m,n) = - raise (PretypeError (env_ise sigma env,CannotUnify (m,n))) + raise (PretypeError (env, sigma,CannotUnify (m,n))) let error_cannot_find_well_typed_abstraction env sigma p l = - raise (PretypeError (env_ise sigma env,CannotFindWellTypedAbstraction (p,l))) + raise (PretypeError (env, sigma,CannotFindWellTypedAbstraction (p,l))) let error_abstraction_over_meta env sigma hdmeta metaarg = let m = Evd.meta_name sigma hdmeta and n = Evd.meta_name sigma metaarg in - raise (PretypeError (env_ise sigma env,AbstractionOverMeta (m,n))) + raise (PretypeError (env, sigma,AbstractionOverMeta (m,n))) let error_non_linear_unification env sigma hdmeta t = let m = Evd.meta_name sigma hdmeta in - raise (PretypeError (env_ise sigma env,NonLinearUnification (m,t))) + raise (PretypeError (env, sigma,NonLinearUnification (m,t))) (*s Ml Case errors *) let error_cant_find_case_type_loc loc env sigma expr = - raise_pretype_error - (loc, env, sigma, CantFindCaseType (nf_evar sigma expr)) + raise_pretype_error (loc, env, sigma, CantFindCaseType expr) (*s Pretyping errors *) let error_unexpected_type_loc loc env sigma actty expty = let env, actty, expty = contract2 env actty expty in - raise_pretype_error - (loc, env, sigma, - UnexpectedType (nf_evar sigma actty, nf_evar sigma expty)) + raise_pretype_error (loc, env, sigma, UnexpectedType (actty, expty)) let error_not_product_loc loc env sigma c = - raise_pretype_error (loc, env, sigma, NotProduct (nf_evar sigma c)) + raise_pretype_error (loc, env, sigma, NotProduct c) (*s Error in conversion from AST to rawterms *) |