diff options
Diffstat (limited to 'pretyping')
-rw-r--r-- | pretyping/cases.ml | 15 | ||||
-rw-r--r-- | pretyping/cases.mli | 2 | ||||
-rw-r--r-- | pretyping/coercion.ml | 42 | ||||
-rw-r--r-- | pretyping/evarconv.ml | 15 | ||||
-rw-r--r-- | pretyping/evarutil.ml | 57 | ||||
-rw-r--r-- | pretyping/evarutil.mli | 18 | ||||
-rw-r--r-- | pretyping/pretype_errors.ml | 115 | ||||
-rw-r--r-- | pretyping/pretype_errors.mli | 61 | ||||
-rw-r--r-- | pretyping/pretyping.ml | 91 | ||||
-rw-r--r-- | pretyping/tacred.ml | 16 | ||||
-rw-r--r-- | pretyping/tacred.mli | 4 | ||||
-rw-r--r-- | pretyping/typing.ml | 4 |
12 files changed, 266 insertions, 174 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index b207f4247..f69ca6084 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -102,7 +102,7 @@ let branch_scheme env isevars isrec (IndFamily (mis,params) as indf) = (* B) Building ML like case expressions without types *) let concl_n env sigma = - let rec decrec m c = if m = 0 then c else + let rec decrec m c = if m = 0 then (nf_evar sigma c) else match kind_of_term (whd_betadeltaiota env sigma c) with | IsProd (n,_,c_0) -> decrec (m-1) c_0 | _ -> failwith "Typing.concl_n" @@ -151,12 +151,15 @@ let pred_case_ml_fail env sigma isrec (IndType (indf,realargs)) (i,ft) = let pred_case_ml loc env sigma isrec indt lf (i,ft) = try pred_case_ml_fail env sigma isrec indt (i,ft) - with NotInferable e -> error_ml_case_loc loc env e indt lf.(i-1) ft + with NotInferable e -> + let j = {uj_val=lf.(i-1); uj_type=ft} in + error_ml_case_loc loc env sigma e indt j (* similar to pred_case_ml but does not expect the list lf of braches *) -let pred_case_ml_onebranch loc env sigma isrec indt (i,f,ft) = - try pred_case_ml_fail env sigma isrec indt (i,ft) - with NotInferable e -> error_ml_case_loc loc env e indt f ft +let pred_case_ml_onebranch loc env sigma isrec indt (i,fj) = + try pred_case_ml_fail env sigma isrec indt (i,fj.uj_type) + with NotInferable e -> + error_ml_case_loc loc env sigma e indt fj (************************************************************************) (* Pattern-matching compilation (Cases) *) @@ -1316,7 +1319,7 @@ let coerce_row typing_fun isevars env cstropt tomatch = (constructor_of_rawconstructor c) mind with Induc -> error_case_not_inductive_loc - (loc_of_rawconstr tomatch) CCI env j.uj_val typ) + (loc_of_rawconstr tomatch) CCI env (evars_of isevars) j) | None -> try IsInd (typ,find_rectype env (evars_of isevars) typ) with Induc -> NotInd typ diff --git a/pretyping/cases.mli b/pretyping/cases.mli index a7dddb5cb..7e5fda903 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -35,7 +35,7 @@ val branch_scheme : env -> 'a evar_defs -> bool -> inductive_family -> constr array val pred_case_ml_onebranch : loc -> env -> 'c evar_map -> bool -> - inductive_type -> int * constr * constr -> constr + inductive_type -> int * unsafe_judgment -> constr (* Compilation of pattern-matching. *) diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 3e5e064bc..3cad7122c 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -22,13 +22,7 @@ open Retyping (* Typing operations dealing with coercions *) -let class_of1 env sigma t = class_of env sigma (nf_ise1 sigma t) - -let j_nf_ise env sigma {uj_val=v;uj_type=t} = - { uj_val = nf_ise1 sigma v; - uj_type = nf_ise1 sigma t } - -let jl_nf_ise env sigma = List.map (j_nf_ise env sigma) +let class_of1 env sigma t = class_of env sigma (nf_evar sigma t) (* Here, funj is a coercion therefore already typed in global context *) let apply_coercion_args env argl funj = @@ -150,10 +144,9 @@ let inh_conv_coerce_to loc env isevars cj t = let cj' = try inh_conv_coerce_to_fail env isevars t cj - with NoCoercion -> - let rcj = j_nf_ise env (evars_of isevars) cj in - let at = nf_ise1 (evars_of isevars) t in - error_actual_type_loc loc env rcj.uj_val rcj.uj_type at + with NoCoercion -> + let sigma = evars_of isevars in + error_actual_type_loc loc env sigma cj t in { uj_val = cj'.uj_val; uj_type = t } @@ -165,40 +158,25 @@ let inh_apply_rel_list apploc env isevars argjl (funloc,funj) tycon = let rec apply_rec env n resj = function | [] -> resj | (loc,hj)::restjl -> + let sigma = evars_of isevars in let resj = inh_app_fun env isevars resj in - let ntyp = whd_betadeltaiota env (evars_of isevars) resj.uj_type in + let ntyp = whd_betadeltaiota env sigma resj.uj_type in match kind_of_term ntyp with | IsProd (na,c1,c2) -> let hj' = try inh_conv_coerce_to_fail env isevars c1 hj with NoCoercion -> -(* - error_cant_apply_bad_type_loc apploc env - (n,nf_ise1 (evars_of isevars) c1, - nf_ise1 (evars_of isevars) hj.uj_type) - (j_nf_ise env (evars_of isevars) funj) - (jl_nf_ise env (evars_of isevars) argjl) in -*) - error_cant_apply_bad_type_loc apploc env - (1,nf_ise1 (evars_of isevars) c1, - nf_ise1 (evars_of isevars) hj.uj_type) - (j_nf_ise env (evars_of isevars) resj) - (jl_nf_ise env (evars_of isevars) (List.map snd restjl)) in + error_cant_apply_bad_type_loc apploc env sigma + (1,c1,hj.uj_type) resj (List.map snd restjl) in let newresj = { uj_val = applist (j_val resj, [j_val hj']); uj_type = subst1 hj'.uj_val c2 } in apply_rec (push_rel_assum (na,c1) env) (n+1) newresj restjl | _ -> -(* - error_cant_apply_not_functional_loc apploc env - (j_nf_ise env (evars_of isevars) funj) - (jl_nf_ise env (evars_of isevars) argjl) -*) error_cant_apply_not_functional_loc - (Rawterm.join_loc funloc loc) env - (j_nf_ise env (evars_of isevars) resj) - (jl_nf_ise env (evars_of isevars) (List.map snd restjl)) + (Rawterm.join_loc funloc loc) env sigma resj + (List.map snd restjl) in apply_rec env 1 funj argjl diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 766e6e0e9..6783e70a4 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -52,8 +52,9 @@ let evar_apprec env isevars stack c = * possibly applied to arguments. *) let rec evar_conv_x env isevars pbty term1 term2 = - let term1 = whd_ise1 (evars_of isevars) term1 in - let term2 = whd_ise1 (evars_of isevars) term2 in + let sigma = evars_of isevars in + let term1 = whd_castappevar sigma term1 in + let term2 = whd_castappevar sigma term2 in (* if eq_constr term1 term2 then true @@ -63,7 +64,7 @@ let rec evar_conv_x env isevars pbty term1 term2 = is_fconv pbty env (evars_of isevars) term1 term2 else *) - (is_fconv pbty env (evars_of isevars) term1 term2) or + (is_fconv pbty env sigma term1 term2) or if ise_undefined isevars term1 then solve_simple_eqn evar_conv_x env isevars (pbty,destEvar term1,term2) else if ise_undefined isevars term2 then @@ -206,15 +207,15 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = | IsLambda (na,c1,c'1), IsLambda (_,c2,c'2) when l1=[] & l2=[] -> evar_conv_x env isevars CONV c1 c2 & - (let c = nf_ise1 (evars_of isevars) c1 in + (let c = nf_evar (evars_of isevars) c1 in evar_conv_x (push_rel_assum (na,c) env) isevars CONV c'1 c'2) | IsLetIn (na,b1,t1,c'1), IsLetIn (_,b2,_,c'2) -> let f1 () = evar_conv_x env isevars CONV b1 b2 & - (let b = nf_ise1 (evars_of isevars) b1 in - let t = nf_ise1 (evars_of isevars) t1 in + (let b = nf_evar (evars_of isevars) b1 in + let t = nf_evar (evars_of isevars) t1 in evar_conv_x (push_rel_def (na,b,t) env) isevars pbty c'1 c'2) & (List.length l1 = List.length l2) & (List.for_all2 (evar_conv_x env isevars CONV) l1 l2) @@ -236,7 +237,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = | IsProd (n,c1,c'1), IsProd (_,c2,c'2) when l1=[] & l2=[] -> evar_conv_x env isevars CONV c1 c2 & - (let c = nf_ise1 (evars_of isevars) c1 in + (let c = nf_evar (evars_of isevars) c1 in evar_conv_x (push_rel_assum (n,c) env) isevars pbty c'1 c'2) | IsMutInd (sp1,cl1), IsMutInd (sp2,cl2) -> diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index f10973afb..5b4a0dccb 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -47,6 +47,44 @@ let filter_sign p sign x = (x,[],nil_sign) *) +(* Expanding existential variables (pretyping.ml) *) +(* 1- whd_ise fails if an existential is undefined *) + +exception Uninstantiated_evar of int + +let rec whd_ise sigma c = + match kind_of_term c with + | IsEvar (ev,args) when Evd.in_dom sigma ev -> + if Evd.is_defined sigma ev then + whd_ise sigma (existential_value sigma (ev,args)) + else raise (Uninstantiated_evar ev) + | _ -> c + + +(* Expand evars, possibly in the head of an application *) +let whd_castappevar_stack sigma c = + let rec whrec (c, l as s) = + match kind_of_term c with + | IsEvar (ev,args) when Evd.in_dom sigma ev & Evd.is_defined sigma ev -> + whrec (existential_value sigma (ev,args), l) + | IsCast (c,_) -> whrec (c, l) + | IsApp (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l) + | _ -> s + in + whrec (c, []) + +let whd_castappevar sigma c = applist (whd_castappevar_stack sigma c) + +let nf_evar = Pretype_errors.nf_evar +let j_nf_evar = Pretype_errors.j_nf_evar +let jl_nf_evar = Pretype_errors.jl_nf_evar +let jv_nf_evar = Pretype_errors.jv_nf_evar +let tj_nf_evar = Pretype_errors.tj_nf_evar + +(**********************) +(* Creating new evars *) +(**********************) + let evar_env evd = Global.env_of_context evd.evar_hyps (* Generator of existential names *) @@ -200,7 +238,7 @@ let need_restriction isevars args = not (array_for_all closed0 args) * false. The problem is that we won't get the right error message. *) -let real_clean isevars sp args rhs = +let real_clean isevars ev args rhs = let subst = List.map (fun (x,y) -> (y,mkVar x)) (filter_unique args) in let rec subs k t = match kind_of_term t with @@ -224,7 +262,8 @@ let real_clean isevars sp args rhs = | _ -> map_constr_with_binders succ subs k t in let body = subs 0 rhs in - if not (closed0 body) then error_not_clean empty_env sp body; + if not (closed0 body) + then error_not_clean empty_env isevars.evars ev body; body let make_evar_instance_with_rel env = @@ -280,7 +319,8 @@ let keep_rels_and_vars c = match kind_of_term c with | _ -> mkImplicit (* Mettre mkMeta ?? *) let evar_define isevars (ev,argsv) rhs = - if occur_evar ev rhs then error_occur_check empty_env ev rhs; + if occur_evar ev rhs + then error_occur_check empty_env (evars_of isevars) ev rhs; let args = List.map keep_rels_and_vars (Array.to_list argsv) in let evd = ise_map isevars ev in (* the substitution to invert *) @@ -407,7 +447,7 @@ let solve_refl conv_algo env isevars ev argsv1 argsv2 = (* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *) let solve_simple_eqn conv_algo env isevars (pbty,(n1,args1 as ev1),t2) = - let t2 = nf_ise1 isevars.evars t2 in + let t2 = nf_evar isevars.evars t2 in let lsp = match kind_of_term t2 with | IsEvar (n2,args2 as ev2) when not (Evd.is_defined isevars.evars n2) -> @@ -462,16 +502,17 @@ let mk_valcon c = Some c let split_tycon loc env isevars = function | None -> None,None | Some c -> - let t = whd_betadeltaiota env isevars.evars c in + let sigma = evars_of isevars in + let t = whd_betadeltaiota env sigma c in match kind_of_term t with | IsProd (na,dom,rng) -> Some dom, Some rng | _ -> if ise_undefined isevars t then - let (sigma,dom,rng) = split_evar_to_arrow isevars.evars t in - isevars.evars <- sigma; + let (sigma',dom,rng) = split_evar_to_arrow sigma t in + evars_reset_evd sigma' isevars; Some dom, Some rng else - error_not_product_loc loc env c + error_not_product_loc loc env sigma c let valcon_of_tycon x = x diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index c31b57a4a..0295b7dfe 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -19,6 +19,24 @@ open Reduction (*s This modules provides useful functions for unification modulo evars *) +(* [whd_ise] raise [Uninstantiated_evar] if an evar remains uninstantiated; *) +(* *[whd_evar]* and *[nf_evar]* leave uninstantiated evar as is *) + +val nf_evar : 'a Evd.evar_map -> constr -> constr +val j_nf_evar : 'a Evd.evar_map -> unsafe_judgment -> unsafe_judgment +val jl_nf_evar : + 'a Evd.evar_map -> unsafe_judgment list -> unsafe_judgment list +val jv_nf_evar : + 'a Evd.evar_map -> unsafe_judgment array -> unsafe_judgment array +val tj_nf_evar : + 'a Evd.evar_map -> unsafe_type_judgment -> unsafe_type_judgment + +(* Replacing all evars *) +exception Uninstantiated_evar of int +val whd_ise : 'a evar_map -> constr -> constr +val whd_castappevar : 'a evar_map -> constr -> constr + +(* Creating new existential variables *) val new_evar : unit -> evar val new_evar_in_sign : env -> constr diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index f35b1b10b..4d6af242b 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -14,6 +14,7 @@ open Term open Environ open Type_errors open Rawterm +open Inductive type ml_case_error = | MlCaseAbsurd @@ -21,7 +22,7 @@ type ml_case_error = type pretype_error = (* Old Case *) - | MlCase of ml_case_error + | MlCase of ml_case_error * inductive_type * unsafe_judgment | CantFindCaseType of constr (* Unification *) | OccurCheck of int * constr @@ -33,58 +34,104 @@ type pretype_error = exception PretypeError of env * pretype_error -let raise_pretype_error (loc,ctx,te) = - Stdpp.raise_with_loc loc (PretypeError(ctx,te)) +(* Replacing defined evars for error messages *) +let rec whd_evar sigma c = + match kind_of_term c with + | IsEvar (ev,args) when Evd.in_dom sigma ev & Evd.is_defined sigma ev -> + whd_evar sigma (Instantiate.existential_value sigma (ev,args)) + | _ -> collapse_appl c -let raise_located_type_error (loc,k,ctx,te) = - Stdpp.raise_with_loc loc (TypeError(k,ctx,te)) +let nf_evar sigma = Reduction.local_strong (whd_evar sigma) +let j_nf_evar sigma j = + { uj_val = nf_evar sigma j.uj_val; + uj_type = nf_evar sigma j.uj_type } +let jl_nf_evar sigma jl = List.map (j_nf_evar 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=type_app (nf_evar sigma) v;utj_type=t} -let error_cant_find_case_type_loc loc env expr = - raise_pretype_error (loc, env, CantFindCaseType expr) -let error_ill_formed_branch_loc loc k env c i actty expty = - raise_located_type_error (loc, k, env, IllFormedBranch (c,i,actty,expty)) +let env_ise sigma env = + map_context (nf_evar sigma) env -let error_actual_type_loc loc env c actty expty = - raise_located_type_error (loc, CCI, env, ActualType (c,actty,expty)) -let error_cant_apply_not_functional_loc loc env rator randl = +let raise_pretype_error (loc,ctx,sigma,te) = + Stdpp.raise_with_loc loc (PretypeError(env_ise sigma ctx,te)) + +let raise_located_type_error (loc,k,ctx,sigma,te) = + Stdpp.raise_with_loc loc (TypeError(k,env_ise sigma ctx,te)) + + +let error_actual_type_loc loc env sigma {uj_val=c;uj_type=actty} expty = + raise_located_type_error + (loc, CCI, env, sigma, + ActualType (c,nf_evar sigma actty, nf_evar sigma expty)) + +let error_cant_apply_not_functional_loc loc env sigma rator randl = + raise_located_type_error + (loc, CCI, env, sigma, + CantApplyNonFunctional (j_nf_evar sigma rator, jl_nf_evar sigma randl)) + +let error_cant_apply_bad_type_loc loc env sigma (n,c,t) rator randl = raise_located_type_error - (loc,CCI,env, CantApplyNonFunctional (rator,randl)) + (loc, CCI, env, sigma, + CantApplyBadType + ((n,nf_evar sigma c, nf_evar sigma t), + j_nf_evar sigma rator, jl_nf_evar sigma randl)) -let error_cant_apply_bad_type_loc loc env t rator randl = - raise_located_type_error (loc, CCI, env, CantApplyBadType (t,rator,randl)) +let error_cant_find_case_type_loc loc env sigma expr = + raise_pretype_error + (loc, env, sigma, CantFindCaseType (nf_evar sigma expr)) -let error_ill_formed_branch k env c i actty expty = - raise (TypeError (k, env, IllFormedBranch (c,i,actty,expty))) +let error_ill_formed_branch_loc loc k env sigma c i actty expty = + let simp t = Reduction.nf_betaiota (nf_evar sigma t) in + raise_located_type_error + (loc, k, env, sigma, + IllFormedBranch (nf_evar sigma c,i,simp actty, simp expty)) -let error_number_branches_loc loc k env c ct expn = - raise_located_type_error (loc, k, env, NumberBranches (c,ct,expn)) +let error_number_branches_loc loc k env sigma cj expn = + raise_located_type_error + (loc, k, env, sigma, + NumberBranches (j_nf_evar sigma cj, expn)) -let error_case_not_inductive_loc loc k env c ct = - raise_located_type_error (loc, k, env, CaseNotInductive (c,ct)) +let error_case_not_inductive_loc loc k env sigma cj = + raise_located_type_error + (loc, k, env, sigma, CaseNotInductive (j_nf_evar sigma cj)) +let error_ill_typed_rec_body_loc loc k env sigma i na jl tys = + raise_located_type_error + (loc, k, env, sigma, + IllTypedRecBody (i,na,jv_nf_evar sigma jl, + Array.map (nf_evar sigma) tys)) -(*s Implicit arguments synthesis errors *) +(*s Implicit arguments synthesis errors. It is hard to find + a precise location. *) -let error_occur_check env ev c = - raise (PretypeError (env, OccurCheck (ev,c))) +let error_occur_check env sigma ev c = + let c = nf_evar sigma c in + raise (PretypeError (env_ise sigma env, OccurCheck (ev,c))) -let error_not_clean env ev c = - raise (PretypeError (env, NotClean (ev,c))) +let error_not_clean env sigma ev c = + let c = nf_evar sigma c in + raise (PretypeError (env_ise sigma env, NotClean (ev,c))) (*s Ml Case errors *) -let error_ml_case_loc loc env mes = - raise_pretype_error (loc, env, MlCase mes) +let error_ml_case_loc loc env sigma mes indt j = + raise_pretype_error + (loc, env, sigma, MlCase (mes, indt, j_nf_evar sigma j)) (*s Pretyping errors *) -let error_var_not_found_loc loc s = - raise_pretype_error (loc, Global.env() (*bidon*), VarNotFound s) +let error_unexpected_type_loc loc env sigma actty expty = + raise_pretype_error + (loc, env, sigma, + UnexpectedType (nf_evar sigma actty, nf_evar sigma expty)) + +let error_not_product_loc loc env sigma c = + raise_pretype_error (loc, env, sigma, NotProduct (nf_evar sigma c)) -let error_unexpected_type_loc loc env actty expty = - raise_pretype_error (loc, env, UnexpectedType (actty, expty)) +(*s Error in conversion from AST to rawterms *) -let error_not_product_loc loc env c = - raise_pretype_error (loc, env, NotProduct c) +let error_var_not_found_loc loc s = + raise_pretype_error (loc, empty_env, Evd.empty, VarNotFound s) diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 717191aa8..90d90120e 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -14,8 +14,8 @@ open Names open Term open Sign open Environ -open Type_errors open Rawterm +open Inductive (*i*) (*s The type of errors raised by the pretyper *) @@ -26,7 +26,7 @@ type ml_case_error = type pretype_error = (* Old Case *) - | MlCase of ml_case_error + | MlCase of ml_case_error * inductive_type * unsafe_judgment | CantFindCaseType of constr (* Unification *) | OccurCheck of int * constr @@ -38,42 +38,67 @@ type pretype_error = exception PretypeError of env * pretype_error -val error_cant_find_case_type_loc : - loc -> env -> constr -> 'a +(* Presenting terms without solved evars *) +val nf_evar : 'a Evd.evar_map -> constr -> constr +val j_nf_evar : 'a Evd.evar_map -> unsafe_judgment -> unsafe_judgment +val jl_nf_evar : + 'a Evd.evar_map -> unsafe_judgment list -> unsafe_judgment list +val jv_nf_evar : + 'a Evd.evar_map -> unsafe_judgment array -> unsafe_judgment array +val tj_nf_evar : + 'a Evd.evar_map -> unsafe_type_judgment -> unsafe_type_judgment -val error_ill_formed_branch_loc : - loc -> path_kind -> env -> constr -> int -> constr -> constr -> 'b +(* Raising errors *) val error_actual_type_loc : - loc -> env -> constr -> constr -> constr -> 'b + loc -> env -> 'a Evd.evar_map -> unsafe_judgment -> constr -> 'b val error_cant_apply_not_functional_loc : - loc -> env -> unsafe_judgment -> unsafe_judgment list -> 'b + loc -> env -> 'a Evd.evar_map -> + unsafe_judgment -> unsafe_judgment list -> 'b val error_cant_apply_bad_type_loc : - loc -> env -> int * constr * constr -> + loc -> env -> 'a Evd.evar_map -> int * constr * constr -> unsafe_judgment -> unsafe_judgment list -> 'b -val error_number_branches_loc : - loc -> path_kind -> env -> constr -> constr -> int -> 'b +val error_cant_find_case_type_loc : + loc -> env -> 'a Evd.evar_map -> constr -> 'b val error_case_not_inductive_loc : - loc -> path_kind -> env -> constr -> constr -> 'b + loc -> path_kind -> env -> 'a Evd.evar_map -> unsafe_judgment -> 'b + +val error_ill_formed_branch_loc : + loc -> path_kind -> env -> 'a Evd.evar_map -> + constr -> int -> constr -> constr -> 'b + +val error_number_branches_loc : + loc -> path_kind -> env -> 'a Evd.evar_map -> + unsafe_judgment -> int -> 'b + +val error_ill_typed_rec_body_loc : + loc -> path_kind -> env -> 'a Evd.evar_map -> + int -> name array -> unsafe_judgment array -> types array -> 'b (*s Implicit arguments synthesis errors *) -val error_occur_check : env -> int -> constr -> 'a +val error_occur_check : env -> 'a Evd.evar_map -> int -> constr -> 'b -val error_not_clean : env -> int -> constr -> 'a +val error_not_clean : env -> 'a Evd.evar_map -> int -> constr -> 'b (*s Ml Case errors *) -val error_ml_case_loc : loc -> env -> ml_case_error -> 'a +val error_ml_case_loc : + loc -> env -> 'a Evd.evar_map -> + ml_case_error -> inductive_type -> unsafe_judgment -> 'b (*s Pretyping errors *) -val error_var_not_found_loc : loc -> identifier -> 'a +val error_unexpected_type_loc : + loc -> env -> 'a Evd.evar_map -> constr -> constr -> 'b + +val error_not_product_loc : + loc -> env -> 'a Evd.evar_map -> constr -> 'b -val error_unexpected_type_loc : loc -> env -> constr -> constr -> 'b +(*s Error in conversion from AST to rawterms *) -val error_not_product_loc : loc -> env -> constr -> 'a +val error_var_not_found_loc : loc -> identifier -> 'b diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index c06e0d580..d2855a64f 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -37,17 +37,18 @@ let lift_context n l = let k = List.length l in list_map_i (fun i (name,c) -> (name,liftn n (k-i) c)) 0 l -let transform_rec loc env sigma (p,c,lf) (indt,pt) = +let transform_rec loc env sigma (pj,c,lf) indt = + let p = pj.uj_val in let (indf,realargs) = dest_ind_type indt in let (mispec,params) = dest_ind_family indf in let mI = mkMutInd (mis_inductive mispec) in let recargs = mis_recarg mispec in let tyi = mis_index mispec in if Array.length lf <> mis_nconstr mispec then - error_number_branches_loc loc CCI env c - (mkAppliedInd indt) (mis_nconstr mispec); + (let cj = {uj_val=c; uj_type=mkAppliedInd indt} in + error_number_branches_loc loc CCI env sigma cj (mis_nconstr mispec)); if mis_is_recursive_subset [tyi] mispec then - let (dep,_) = find_case_dep_nparams env sigma (c,p) indf pt in + let (dep,_) = find_case_dep_nparams env sigma (c,pj) indf in let init_depFvec i = if i = tyi then Some(dep,mkRel 1) else None in let depFvec = Array.init (mis_ntypes mispec) init_depFvec in (* build now the fixpoint *) @@ -107,44 +108,27 @@ let mt_evd = Evd.empty let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t) -let j_nf_ise sigma {uj_val=v;uj_type=t} = - {uj_val=nf_ise1 sigma v;uj_type=type_app (nf_ise1 sigma) t} - -let jv_nf_ise sigma = Array.map (j_nf_ise sigma) - -let tj_nf_ise sigma {utj_val=v;utj_type=t} = - {utj_val=type_app (nf_ise1 sigma) v;utj_type=t} - (* Utilisé pour inférer le prédicat des Cases *) (* Semble exagérement fort *) (* Faudra préférer une unification entre les types de toutes les clauses *) (* et autoriser des ? à rester dans le résultat de l'unification *) -let evar_type_fixpoint env isevars lna lar vdefj = +let evar_type_fixpoint loc env isevars lna lar vdefj = let lt = Array.length vdefj in if Array.length lar = lt then for i = 0 to lt-1 do if not (the_conv_x_leq env isevars (vdefj.(i)).uj_type (lift lt lar.(i))) then - error_ill_typed_rec_body CCI env i lna - (jv_nf_ise (evars_of isevars) vdefj) - (Array.map (type_app (nf_ise1 (evars_of isevars))) lar) + error_ill_typed_rec_body_loc loc CCI env (evars_of isevars) + i lna vdefj lar done -let wrong_number_of_cases_message loc env isevars (c,ct) expn = - let c = nf_ise1 (evars_of isevars) c - and ct = nf_ise1 (evars_of isevars) ct in - error_number_branches_loc loc CCI env c ct expn - let check_branches_message loc env isevars c (explft,lft) = for i = 0 to Array.length explft - 1 do if not (the_conv_x_leq env isevars lft.(i) explft.(i)) then - let c = nf_ise1 (evars_of isevars) c - and lfi = nf_betaiota env (evars_of isevars) - (nf_ise1 (evars_of isevars) lft.(i)) in - error_ill_formed_branch_loc loc CCI env c i lfi - (nf_betaiota env (evars_of isevars) explft.(i)) + let sigma = evars_of isevars in + error_ill_formed_branch_loc loc CCI env sigma c i lft.(i) explft.(i) done (* coerce to tycon if any *) @@ -275,7 +259,7 @@ let rec pretype tycon env isevars lvar lmeta = function pretype (mk_tycon (lift nbfix (larj.(i).utj_val))) newenv isevars lvar lmeta def) vdef in - evar_type_fixpoint env isevars names lara vdefj; + evar_type_fixpoint loc env isevars names lara vdefj; let fixj = match fixkind with | RFix (vn,i as vni) -> @@ -310,14 +294,10 @@ let rec pretype tycon env isevars lvar lmeta = function apply_rec env (n+1) newresj rest | _ -> - let j_nf_ise env sigma {uj_val=v;uj_type=t} = - { uj_val = nf_ise1 sigma v; - uj_type = nf_ise1 sigma t } in let hj = pretype empty_tycon env isevars lvar lmeta c in error_cant_apply_not_functional_loc - (Rawterm.join_loc floc argloc) env - (j_nf_ise env (evars_of isevars) resj) - [j_nf_ise env (evars_of isevars) hj] + (Rawterm.join_loc floc argloc) env (evars_of isevars) + resj [hj] in let resj = apply_rec env 1 fj args in (* @@ -365,9 +345,8 @@ let rec pretype tycon env isevars lvar lmeta = function let cj = pretype empty_tycon env isevars lvar lmeta c in let (IndType (indf,realargs) as indt) = try find_rectype env (evars_of isevars) cj.uj_type - with Induc -> error_case_not_inductive CCI env - (nf_ise1 (evars_of isevars) cj.uj_val) - (nf_ise1 (evars_of isevars) cj.uj_type) in + with Induc -> + error_case_not_inductive_loc loc CCI env (evars_of isevars) cj in let pj = match po with | Some p -> pretype empty_tycon env isevars lvar lmeta p | None -> @@ -379,17 +358,17 @@ let rec pretype tycon env isevars lvar lmeta = function let expbr = Cases.branch_scheme env isevars isrec indf in let rec findtype i = if i >= Array.length lf - then error_cant_find_case_type_loc loc env cj.uj_val + then + let sigma = evars_of isevars in + error_cant_find_case_type_loc loc env sigma cj.uj_val else try let expti = expbr.(i) in let fj = pretype (mk_tycon expti) env isevars lvar lmeta lf.(i) in - let efjt = nf_ise1 (evars_of isevars) fj.uj_type in let pred = Cases.pred_case_ml_onebranch - loc env (evars_of isevars) isrec indt - (i,fj.uj_val,efjt) in + loc env (evars_of isevars) isrec indt (i,fj) in if has_undefined_isevars isevars pred then findtype (i+1) else let pty = @@ -398,33 +377,31 @@ let rec pretype tycon env isevars lvar lmeta = function uj_type = pty } with UserError _ -> findtype (i+1) in findtype 0 in - - let evalPt = nf_ise1 (evars_of isevars) pj.uj_type in + let pj = j_nf_evar (evars_of isevars) pj in let (dep,_) = find_case_dep_nparams env (evars_of isevars) - (cj.uj_val,pj.uj_val) indf evalPt in + (cj.uj_val,pj) indf in - let (p,pt) = - if dep then (pj.uj_val, evalPt) else + let pj = + if dep then pj else let n = List.length realargs in let rec decomp n p = if n=0 then p else match kind_of_term p with | IsLambda (_,_,c) -> decomp (n-1) c | _ -> decomp (n-1) (applist (lift 1 p, [mkRel 1])) in - let sign,s = decompose_prod_n n evalPt in + let sign,s = decompose_prod_n n pj.uj_type in let ind = build_dependent_inductive indf in let s' = mkProd (Anonymous, ind, s) in let ccl = lift 1 (decomp n pj.uj_val) in let ccl' = mkLambda (Anonymous, ind, ccl) in - (lam_it ccl' sign, prod_it s' sign) in + {uj_val=lam_it ccl' sign; uj_type=prod_it s' sign} in let (bty,rsty) = Indrec.type_rec_branches - isrec env (evars_of isevars) indt pt p cj.uj_val in + isrec env (evars_of isevars) indt pj cj.uj_val in if Array.length bty <> Array.length lf then - wrong_number_of_cases_message loc env isevars - (cj.uj_val,nf_ise1 (evars_of isevars) cj.uj_type) - (Array.length bty) + error_number_branches_loc loc CCI env (evars_of isevars) + cj (Array.length bty) else let lfj = array_map2 @@ -436,11 +413,12 @@ let rec pretype tycon env isevars lvar lmeta = function let v = if isrec then - transform_rec loc env (evars_of isevars)(p,cj.uj_val,lfv) (indt,pt) + transform_rec loc env (evars_of isevars)(pj,cj.uj_val,lfv) indt else let mis,_ = dest_ind_family indf in let ci = make_default_case_info mis in - mkMutCase (ci, p, cj.uj_val, Array.map (fun j-> j.uj_val) lfj) + mkMutCase (ci, pj.uj_val, cj.uj_val, + Array.map (fun j-> j.uj_val) lfj) in {uj_val = v; uj_type = rsty } @@ -475,16 +453,17 @@ and pretype_type valcon env isevars lvar lmeta = function | Some v -> if the_conv_x_leq env isevars v tj.utj_val then tj else - error_unexpected_type_loc (loc_of_rawconstr c) env tj.utj_val v + error_unexpected_type_loc + (loc_of_rawconstr c) env (evars_of isevars) tj.utj_val v let unsafe_infer tycon isevars env lvar lmeta constr = let j = pretype tycon env isevars lvar lmeta constr in - j_nf_ise (evars_of isevars) j + j_nf_evar (evars_of isevars) j let unsafe_infer_type valcon isevars env lvar lmeta constr = let tj = pretype_type valcon env isevars lvar lmeta constr in - tj_nf_ise (evars_of isevars) tj + tj_nf_evar (evars_of isevars) tj (* If fail_evar is false, [process_evars] builds a meta_map with the unresolved Evar that were not in initial sigma; otherwise it fail diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 72ebb6626..f3f010e5e 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -342,7 +342,7 @@ let rec red_elim_const env sigma ref largs = let co = construct_const env sigma in (match reduce_fix_use_function f co (destFix d) lrest with | NotReducible -> raise Redelimination - | Reduced (c,rest) -> (nf_beta env sigma c, rest)) + | Reduced (c,rest) -> (nf_beta c, rest)) | EliminationMutualFix (min,refgoal,refinfos) when stack_args_size largs >= min -> let rec descend ref args = @@ -358,7 +358,7 @@ let rec red_elim_const env sigma ref largs = let co = construct_const env sigma in (match reduce_fix_use_function f co (destFix d) lrest with | NotReducible -> raise Redelimination - | Reduced (c,rest) -> (nf_beta env sigma c, rest)) + | Reduced (c,rest) -> (nf_beta c, rest)) | _ -> raise Redelimination and construct_const env sigma = @@ -413,7 +413,7 @@ let internal_red_product env sigma c = | None -> raise Redelimination | Some c -> c) | _ -> raise Redelimination - in nf_betaiota env sigma (redrec env c) + in nf_betaiota (redrec env c) let red_product env sigma c = try internal_red_product env sigma c @@ -609,7 +609,7 @@ let unfoldoccs env sigma (occl,name) c = | [] -> unfold env sigma name c | l -> match substlin env name 1 (Sort.list (<) l) c with - | (_,[],uc) -> nf_betaiota env sigma uc + | (_,[],uc) -> nf_betaiota uc | (1,_,_) -> error ((string_of_evaluable_ref name)^" does not occur") | _ -> error ("bad occurrence numbers of " ^(string_of_evaluable_ref name)) @@ -633,9 +633,9 @@ let fold_commands cl env sigma c = let cbv_norm_flags flags env sigma t = cbv_norm (create_cbv_infos flags env sigma) t -let cbv_beta env = cbv_norm_flags beta env -let cbv_betaiota env = cbv_norm_flags betaiota env -let cbv_betadeltaiota env = cbv_norm_flags betadeltaiota env +let cbv_beta = cbv_norm_flags beta empty_env Evd.empty +let cbv_betaiota = cbv_norm_flags betaiota empty_env Evd.empty +let cbv_betadeltaiota env sigma = cbv_norm_flags betadeltaiota env sigma let compute = cbv_betadeltaiota @@ -725,7 +725,7 @@ let reduce_to_mind env sigma t = elimrec (push_rel_assum (n,t) env) t' ((n,None,ty)::l) | _ -> (try - let t' = nf_betaiota env sigma (one_step_reduce env sigma t) in + let t' = nf_betaiota (one_step_reduce env sigma t) in elimrec env t' l with UserError _ -> errorlabstrm "tactics__reduce_to_mind" [< 'sTR"Not an inductive product." >]) diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index 4d248983f..c75f33794 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -43,8 +43,8 @@ val pattern_occs : (int list * constr * constr) list -> 'a reduction_function (* Call by value strategy (uses Closures) *) val cbv_norm_flags : Closure.flags -> 'a reduction_function - val cbv_beta : 'a reduction_function - val cbv_betaiota : 'a reduction_function + val cbv_beta : local_reduction_function + val cbv_betaiota : local_reduction_function val cbv_betadeltaiota : 'a reduction_function val compute : 'a reduction_function (* = [cbv_betadeltaiota] *) diff --git a/pretyping/typing.ml b/pretyping/typing.ml index f78216336..f9110c62a 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -38,7 +38,7 @@ let rec execute mf env sigma cstr = { uj_val = cstr; uj_type = jty } | IsRel n -> - relative env sigma n + relative env n | IsVar id -> (try @@ -158,7 +158,7 @@ let unsafe_machine env sigma constr = let type_of env sigma c = let j = safe_machine env sigma c in - nf_betaiota env sigma (body_of_type j.uj_type) + nf_betaiota (body_of_type j.uj_type) (* The typed type of a judgment. *) |