diff options
Diffstat (limited to 'pretyping/typing.ml')
| -rw-r--r-- | pretyping/typing.ml | 56 |
1 files changed, 33 insertions, 23 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index eb16628b..9e9997f7 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Term open Vars @@ -18,6 +18,7 @@ open Inductive open Inductiveops open Typeops open Arguments_renaming +open Context.Rel.Declaration let meta_type evd mv = let ty = @@ -35,10 +36,10 @@ let inductive_type_knowing_parameters env (ind,u) jl = Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp let e_type_judgment env evdref j = - match kind_of_term (whd_betadeltaiota env !evdref j.uj_type) with + match kind_of_term (whd_all env !evdref j.uj_type) with | Sort s -> {utj_val = j.uj_val; utj_type = s } | Evar ev -> - let (evd,s) = Evarutil.define_evar_as_sort env !evdref ev in + let (evd,s) = Evardefine.define_evar_as_sort env !evdref ev in evdref := evd; { utj_val = j.uj_val; utj_type = s } | _ -> error_not_type env j @@ -53,14 +54,14 @@ let e_judge_of_apply env evdref funj argjv = { uj_val = mkApp (j_val funj, Array.map j_val argjv); uj_type = typ } | hj::restjl -> - match kind_of_term (whd_betadeltaiota env !evdref typ) with + match kind_of_term (whd_all env !evdref typ) with | Prod (_,c1,c2) -> if Evarconv.e_cumul env evdref hj.uj_type c1 then apply_rec (n+1) (subst1 hj.uj_val c2) restjl else error_cant_apply_bad_type env (n,c1, hj.uj_type) funj argjv | Evar ev -> - let (evd',t) = Evarutil.define_evar_as_product !evdref ev in + let (evd',t) = Evardefine.define_evar_as_product !evdref ev in evdref := evd'; let (_,_,c2) = destProd t in apply_rec (n+1) (subst1 hj.uj_val c2) restjl @@ -86,18 +87,18 @@ let e_is_correct_arity env evdref c pj ind specif params = let allowed_sorts = elim_sorts specif in let error () = error_elim_arity env ind allowed_sorts c pj None in let rec srec env pt ar = - let pt' = whd_betadeltaiota env !evdref pt in + let pt' = whd_all env !evdref pt in match kind_of_term pt', ar with - | Prod (na1,a1,t), (_,None,a1')::ar' -> + | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' -> if not (Evarconv.e_cumul env evdref a1 a1') then error (); - srec (push_rel (na1,None,a1) env) t ar' + srec (push_rel (LocalAssum (na1,a1)) env) t ar' | Sort s, [] -> if not (Sorts.List.mem (Sorts.family s) allowed_sorts) then error () | Evar (ev,_), [] -> let evd, s = Evd.fresh_sort_in_family env !evdref (max_sort allowed_sorts) in evdref := Evd.define ev (mkSort s) evd - | _, (_,Some _,_ as d)::ar' -> + | _, (LocalDef _ as d)::ar' -> srec (push_rel d env) (lift 1 pt') ar' | _ -> error () @@ -109,23 +110,32 @@ let e_type_case_branches env evdref (ind,largs) pj c = let nparams = inductive_params specif in let (params,realargs) = List.chop nparams largs in let p = pj.uj_val in - let univ = e_is_correct_arity env evdref c pj ind specif params in + let () = e_is_correct_arity env evdref c pj ind specif params in let lc = build_branches_type ind specif params p in - let n = (snd specif).Declarations.mind_nrealargs in - let ty = - whd_betaiota !evdref (Reduction.betazeta_appvect (n+1) p (Array.of_list (realargs@[c]))) in - (lc, ty, univ) + let n = (snd specif).Declarations.mind_nrealdecls in + let ty = whd_betaiota !evdref (lambda_applist_assum (n+1) p (realargs@[c])) in + (lc, ty) let e_judge_of_case env evdref ci pj cj lfj = let indspec = try find_mrectype env !evdref cj.uj_type with Not_found -> error_case_not_inductive env cj in let _ = check_case_info env (fst indspec) ci in - let (bty,rslty,univ) = e_type_case_branches env evdref indspec pj cj.uj_val in + let (bty,rslty) = e_type_case_branches env evdref indspec pj cj.uj_val in e_check_branch_types env evdref (fst indspec) cj (lfj,bty); { uj_val = mkCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj); uj_type = rslty } +let check_type_fixpoint loc env evdref lna lar vdefj = + let lt = Array.length vdefj in + if Int.equal (Array.length lar) lt then + for i = 0 to lt-1 do + if not (Evarconv.e_cumul env evdref (vdefj.(i)).uj_type + (lift lt lar.(i))) then + Pretype_errors.error_ill_typed_rec_body_loc loc env !evdref + i lna vdefj lar + done + (* FIXME: might depend on the level of actual parameters!*) let check_allowed_sort env sigma ind c p = let pj = Retyping.get_judgment_of env sigma p in @@ -230,14 +240,14 @@ let rec execute env evdref cstr = | Lambda (name,c1,c2) -> let j = execute env evdref c1 in let var = e_type_judgment env evdref j in - let env1 = push_rel (name,None,var.utj_val) env in + let env1 = push_rel (LocalAssum (name, var.utj_val)) env in let j' = execute env1 evdref c2 in judge_of_abstraction env1 name var j' | Prod (name,c1,c2) -> let j = execute env evdref c1 in let varj = e_type_judgment env evdref j in - let env1 = push_rel (name,None,varj.utj_val) env in + let env1 = push_rel (LocalAssum (name, varj.utj_val)) env in let j' = execute env1 evdref c2 in let varj' = e_type_judgment env1 evdref j' in judge_of_product env name varj varj' @@ -247,7 +257,7 @@ let rec execute env evdref cstr = let j2 = execute env evdref c2 in let j2 = e_type_judgment env evdref j2 in let _ = e_judge_of_cast env evdref j1 DEFAULTcast j2 in - let env1 = push_rel (name,Some j1.uj_val,j2.utj_val) env in + let env1 = push_rel (LocalDef (name, j1.uj_val, j2.utj_val)) env in let j3 = execute env1 evdref c3 in judge_of_letin env name j1 j2 j3 @@ -263,12 +273,12 @@ and execute_recdef env evdref (names,lar,vdef) = let env1 = push_rec_types (names,lara,vdef) env in let vdefj = execute_array env1 evdref vdef in let vdefv = Array.map j_val vdefj in - let _ = type_fixpoint env1 names lara vdefj in + let _ = check_type_fixpoint Loc.ghost env1 evdref names lara vdefj in (names,lara,vdefv) and execute_array env evdref = Array.map (execute env evdref) -let check env evdref c t = +let e_check env evdref c t = let env = enrich_env env evdref in let j = execute env evdref c in if not (Evarconv.e_cumul env evdref j.uj_type t) then @@ -284,7 +294,7 @@ let unsafe_type_of env evd c = (* Sort of a type *) -let sort_of env evdref c = +let e_sort_of env evdref c = let env = enrich_env env evdref in let j = execute env evdref c in let a = e_type_judgment env evdref j in @@ -311,10 +321,10 @@ let e_type_of ?(refresh=false) env evdref c = c else j.uj_type -let solve_evars env evdref c = +let e_solve_evars env evdref c = let env = enrich_env env evdref in let c = (execute env evdref c).uj_val in (* side-effect on evdref *) nf_evar !evdref c -let _ = Evarconv.set_solve_evars solve_evars +let _ = Evarconv.set_solve_evars e_solve_evars |