diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/closure.ml | 4 | ||||
| -rw-r--r-- | kernel/indtypes.ml | 17 | ||||
| -rw-r--r-- | kernel/inductive.ml | 28 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 15 | ||||
| -rw-r--r-- | kernel/term.ml | 42 | ||||
| -rw-r--r-- | kernel/term.mli | 15 | ||||
| -rw-r--r-- | kernel/typeops.ml | 79 |
7 files changed, 88 insertions, 112 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml index 178e5a9de7..783017e8a4 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -395,8 +395,8 @@ let rec norm_head info env t stack = (* stack grows (remove casts) *) | IsAppL (head,args) -> (* Applied terms are normalized immediately; they could be computed when getting out of the stack *) - let nargs = List.map (cbv_stack_term info TOP env) args in - norm_head info env head (stack_app nargs stack) + let nargs = Array.map (cbv_stack_term info TOP env) args in + norm_head info env head (stack_app (Array.to_list nargs) stack) | IsMutCase (ci,p,c,v) -> norm_head info env c (CASE(p,v,ci,env,stack)) | IsCast (ct,_) -> norm_head info env ct stack diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 534a95c944..b8649ffb2e 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -175,7 +175,7 @@ let decomp_par n c = snd (mind_extract_params n c) let listrec_mconstr env ntypes nparams i indlc = (* check the inductive types occur positively in [c] *) let rec check_pos n c = - let x,largs = whd_betadeltaiota_stack env Evd.empty c [] in + let x,largs = whd_betadeltaiota_stack env Evd.empty c in match kind_of_term x with | IsProd (na,b,d) -> assert (largs = []); @@ -258,12 +258,23 @@ let listrec_mconstr env ntypes nparams i indlc = and check_construct check_head = let rec check_constr_rec lrec n c = - let x,largs = whd_betadeltaiota_stack env Evd.empty c [] in + let x,largs = whd_betadeltaiota_stack env Evd.empty c in match kind_of_term x with + | IsProd (na,b,d) -> assert (largs = []); let recarg = check_pos n b in - check_constr_rec (recarg::lrec) (n+1) d + check_constr_rec (recarg::lrec) (n+1) d + + (* LetIn's must be free of occurrence of the inductive types and + they do not contribute to recargs *) + | IsLetIn (na,b,t,d) -> + assert (largs = []); + if not (noccur_between n ntypes b & noccur_between n ntypes t) then + raise (IllFormedInd (LocalNonPos n)); + let recarg = check_pos n b in + check_constr_rec lrec (n+1) d + | hd -> if check_head then if hd = IsRel (n+ntypes-i) then diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 569b681e9a..2f5e02ad43 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -182,29 +182,29 @@ let ith_constructor_of_inductive (ind_sp,args) i = ((ind_sp,i),args) exception Induc let extract_mrectype t = - let (t,l) = whd_stack t [] in - match t with - | DOPN(MutInd ind_sp,args) -> ((ind_sp,args),l) + let (t, l) = whd_stack t in + match kind_of_term t with + | IsMutInd ind -> (ind, l) | _ -> raise Induc let find_mrectype env sigma c = - let (t,l) = whd_betadeltaiota_stack env sigma c [] in - match t with - | DOPN(MutInd ind_sp,args) -> ((ind_sp,args),l) + let (t, l) = whd_betadeltaiota_stack env sigma c in + match kind_of_term t with + | IsMutInd ind -> (ind, l) | _ -> raise Induc let find_minductype env sigma c = - let (t,l) = whd_betadeltaiota_stack env sigma c [] in - match t with - | DOPN(MutInd (sp,i),_) - when mind_type_finite (lookup_mind sp env) i -> (destMutInd t,l) + let (t, l) = whd_betadeltaiota_stack env sigma c in + match kind_of_term t with + | IsMutInd ((sp,i),_ as ind) + when mind_type_finite (lookup_mind sp env) i -> (ind, l) | _ -> raise Induc let find_mcoinductype env sigma c = - let (t,l) = whd_betadeltaiota_stack env sigma c [] in - match t with - | DOPN(MutInd (sp,i),_) - when not (mind_type_finite (lookup_mind sp env) i) -> (destMutInd t,l) + let (t, l) = whd_betadeltaiota_stack env sigma c in + match kind_of_term t with + | IsMutInd ((sp,i),_ as ind) + when not (mind_type_finite (lookup_mind sp env) i) -> (ind, l) | _ -> raise Induc (* raise Induc if not an inductive type *) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index e0c951c224..5c1493e2a8 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -94,8 +94,9 @@ let rec execute mf env cstr = | IsAppL (f,args) -> let (j,cst1) = execute mf env f in - let (jl,cst2) = execute_list mf env args in - let (j,cst3) = apply_rel_list env Evd.empty mf.nocheck jl j in + let (jl,cst2) = execute_array mf env args in + let (j,cst3) = + apply_rel_list env Evd.empty mf.nocheck (Array.to_list jl) j in let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in (j, cst) @@ -205,16 +206,6 @@ let unsafe_infer_type env constr = let type_of env c = let (j,_) = safe_infer env c in nf_betaiota env Evd.empty (body_of_type j.uj_type) -(* obsolètes -let type_of_type env c = - let tt = safe_infer_type env c in DOP0 (Sort (level_of_type tt.typ) - -let unsafe_type_of env c = - let (j,_) = unsafe_infer env c in nf_betaiota env Evd.empty j.uj_type - -let unsafe_type_of_type env c = - let tt = unsafe_infer_type env c in DOP0 (Sort tt.typ) -*) (* Typing of several terms. *) let safe_infer_l env cl = diff --git a/kernel/term.ml b/kernel/term.ml index 1933483901..e6c5fa4b51 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -495,8 +495,9 @@ let mkNamedProd_wo_LetIn (id,body,t) c = let mkArrow t1 t2 = mkProd (Anonymous, t1, t2) (* If lt = [t1; ...; tn], constructs the application (t1 ... tn) *) -let mkAppL a = DOPN (AppL, a) -let mkAppList a l = DOPN (AppL, Array.of_list (a::l)) +let mkAppL (f, a) = DOPN (AppL, Array.append [|f|] a) +let mkAppList l = DOPN (AppL, Array.of_list l) +let mkAppA v = DOPN (AppL, v) (* Constructs a constant *) (* The array of terms correspond to the variables introduced in the section *) @@ -609,6 +610,10 @@ let destXtra = function | _ -> invalid_arg "destXtra" (* Destructs a type *) +let isSort = function + | (DOP0 (Sort s)) -> true + | _ -> false + let destSort = function | (DOP0 (Sort s)) -> s | _ -> invalid_arg "destSort" @@ -674,6 +679,10 @@ let under_outer_cast f = function | DOP2 (Cast,b,t) -> DOP2 (Cast,f b,f t) | c -> f c +let rec under_casts f = function + | DOP2 (Cast,c,t) -> DOP2 (Cast,under_casts f c, t) + | c -> f c + let rec strip_all_casts t = match t with | DOP2 (Cast, b, _) -> strip_all_casts b @@ -779,20 +788,6 @@ let num_of_evar = function | DOPN (Evar n, _) -> n | _ -> anomaly "num_of_evar called with bad args" -(* -(* Destructs an abstract term *) -let destAbst = function - | DOPN (Abst sp, a) -> (sp, a) - | _ -> invalid_arg "destAbst" - -let path_of_abst = function - | DOPN(Abst sp,_) -> sp - | _ -> anomaly "path_of_abst called with bad args" - -let args_of_abst = function - | DOPN(Abst _,args) -> args - | _ -> anomaly "args_of_abst called with bad args" -*) (* Destructs a (co)inductive type named sp *) let destMutInd = function | DOPN (MutInd ind_sp, l) -> (ind_sp,l) @@ -898,7 +893,7 @@ type kindOfTerm = | IsProd of name * constr * constr | IsLambda of name * constr * constr | IsLetIn of name * constr * constr * constr - | IsAppL of constr * constr list + | IsAppL of constr * constr array | IsEvar of existential | IsConst of constant | IsMutInd of inductive @@ -924,8 +919,7 @@ let kind_of_term c = | CPrd (x,t1,t2) -> IsProd (x,t1,t2) | CLam (x,t1,t2) -> IsLambda (x,t1,t2) | CLet (x,b,t1,t2) -> IsLetIn (x,b,t1,t2) - | DOPN (AppL,a) when Array.length a <> 0 -> - IsAppL (a.(0), List.tl (Array.to_list a)) + | DOPN (AppL,a) when Array.length a <> 0 -> IsAppL (a.(0), array_tl a) | DOPN (Const sp, a) -> IsConst (sp,a) | DOPN (Evar sp, a) -> IsEvar (sp,a) | DOPN (MutInd ind_sp, l) -> IsMutInd (ind_sp,l) @@ -1922,7 +1916,7 @@ let fold_constr f acc c = match kind_of_term c with | IsProd (_,t,c) -> f (f acc t) c | IsLambda (_,t,c) -> f (f acc t) c | IsLetIn (_,b,t,c) -> f (f (f acc b) t) c - | IsAppL (c,l) -> List.fold_left f (f acc c) l + | IsAppL (c,l) -> Array.fold_left f (f acc c) l | IsEvar (_,l) -> Array.fold_left f acc l | IsConst (_,l) -> Array.fold_left f acc l | IsMutInd (_,l) -> Array.fold_left f acc l @@ -1937,7 +1931,7 @@ let fold_constr_with_binders g f n acc c = match kind_of_term c with | IsProd (_,t,c) -> f (g n) (f n acc t) c | IsLambda (_,t,c) -> f (g n) (f n acc t) c | IsLetIn (_,b,t,c) -> f (g n) (f n (f n acc b) t) c - | IsAppL (c,l) -> List.fold_left (f n) (f n acc c) l + | IsAppL (c,l) -> Array.fold_left (f n) (f n acc c) l | IsEvar (_,l) -> Array.fold_left (f n) acc l | IsConst (_,l) -> Array.fold_left (f n) acc l | IsMutInd (_,l) -> Array.fold_left (f n) acc l @@ -1956,7 +1950,7 @@ let iter_constr_with_binders g f n c = match kind_of_term c with | IsProd (_,t,c) -> f n t; f (g n) c | IsLambda (_,t,c) -> f n t; f (g n) c | IsLetIn (_,b,t,c) -> f n b; f n t; f (g n) c - | IsAppL (c,l) -> f n c; List.iter (f n) l + | IsAppL (c,l) -> f n c; Array.iter (f n) l | IsEvar (_,l) -> Array.iter (f n) l | IsConst (_,l) -> Array.iter (f n) l | IsMutInd (_,l) -> Array.iter (f n) l @@ -1973,7 +1967,7 @@ let map_constr f c = match kind_of_term c with | IsProd (na,t,c) -> mkProd (na, f t, f c) | IsLambda (na,t,c) -> mkLambda (na, f t, f c) | IsLetIn (na,b,t,c) -> mkLetIn (na, f b, f t, f c) - | IsAppL (c,l) -> applist (f c, List.map f l) + | IsAppL (c,l) -> appvect (f c, Array.map f l) | IsEvar (e,l) -> mkEvar (e, Array.map f l) | IsConst (c,l) -> mkConst (c, Array.map f l) | IsMutInd (c,l) -> mkMutInd (c, Array.map f l) @@ -1988,7 +1982,7 @@ let map_constr_with_binders g f l c = match kind_of_term c with | IsProd (na,t,c) -> mkProd (na, f l t, f (g na l) c) | IsLambda (na,t,c) -> mkLambda (na, f l t, f (g na l) c) | IsLetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g na l) c) - | IsAppL (c,al) -> applist (f l c, List.map (f l) al) + | IsAppL (c,al) -> appvect (f l c, Array.map (f l) al) | IsEvar (e,al) -> mkEvar (e, Array.map (f l) al) | IsConst (c,al) -> mkConst (c, Array.map (f l) al) | IsMutInd (c,al) -> mkMutInd (c, Array.map (f l) al) diff --git a/kernel/term.mli b/kernel/term.mli index fe3996c5c6..fa0d076730 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -134,7 +134,7 @@ type kindOfTerm = | IsProd of name * constr * constr | IsLambda of name * constr * constr | IsLetIn of name * constr * constr * constr - | IsAppL of constr * constr list + | IsAppL of constr * constr array | IsEvar of existential | IsConst of constant | IsMutInd of inductive @@ -216,10 +216,11 @@ val mkNamedLambda : identifier -> constr -> constr -> constr (* [mkLambda_string s t c] constructs $[s:t]c$ *) val mkLambda_string : string -> constr -> constr -> constr -(* If $a = [| t_1; \dots; t_n |]$, constructs the application - $(t_1~\dots~t_n)$. *) -val mkAppL : constr array -> constr -val mkAppList : constr -> constr list -> constr +(* [mkAppL (f,[| t_1; ...; t_n |]] constructs the application + $(f~t_1~\dots~t_n)$. *) +val mkAppL : constr * constr array -> constr +val mkAppList : constr list -> constr +val mkAppA : constr array -> constr (* Constructs a constant *) (* The array of terms correspond to the variables introduced in the section *) @@ -307,6 +308,7 @@ val is_Set : constr -> bool val isprop : constr -> bool val is_Type : constr -> bool val iskind : constr -> bool +val isSort : constr -> bool val is_existential_oper : sorts oper -> bool @@ -324,6 +326,9 @@ val strip_outer_cast : constr -> constr (* Special function, which keep the key casts under Fix and MutCase. *) val strip_all_casts : constr -> constr +(* Apply a function letting Casted types in place *) +val under_casts : (constr -> constr) -> constr -> constr + (* Tests if a de Bruijn index *) val isRel : constr -> bool diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 078b6b96b1..58295ee35e 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -337,6 +337,7 @@ let apply_rel_list env sigma nocheck argjl funj = error_cant_apply_bad_type CCI env sigma (n,body_of_type hj.uj_type,c1) funj argjl) + | _ -> error_cant_apply_not_functional CCI env funj argjl in @@ -395,13 +396,13 @@ let check_term env mind_recvec f = crec let is_inst_var env sigma k c = - match whd_betadeltaiota_stack env sigma c [] with - | (Rel n,_) -> n=k + match kind_of_term (fst (whd_betadeltaiota_stack env sigma c)) with + | IsRel n -> n=k | _ -> false let is_subterm_specif env sigma lcx mind_recvec = let rec crec n lst c = - let f,l = whd_betadeltaiota_stack env sigma c [] in + let f,l = whd_betadeltaiota_stack env sigma c in match kind_of_term f with | IsRel k -> find_sorted_assoc k lst @@ -495,7 +496,7 @@ let rec check_subterm_rec_meta env sigma vectn k def = (* n gives the index of the recursive variable *) (noccur_with_meta (n+k+1) nfi t) or (* no recursive call in the term *) - (let f,l = whd_betadeltaiota_stack env sigma t [] in + (let f,l = whd_betadeltaiota_stack env sigma t in match kind_of_term f with | IsRel p -> if n+k+1 <= p & p < n+k+nfi+1 then @@ -617,7 +618,7 @@ let rec check_subterm_rec_meta env sigma vectn k def = | IsAppL (f,la) -> (check_rec_call n lst f) && - (List.for_all (check_rec_call n lst) la) && + (array_for_all (check_rec_call n lst) la) && (List.for_all (check_rec_call n lst) l) | IsCoFix (i,(typarray,funnames,bodies)) -> @@ -686,15 +687,16 @@ let check_guard_rec_meta env sigma nbfix def deftype = let rec check_rec_call alreadygrd n vlra t = if noccur_with_meta n nbfix t then true - else - match whd_betadeltaiota_stack env sigma t [] with - | (DOP0 (Meta _), l) -> true + else + let c,args = whd_betadeltaiota_stack env sigma t in + match kind_of_term c with + | IsMeta _ -> true - | (Rel p,l) -> + | IsRel p -> if n <= p && p < n+nbfix then (* recursive call *) if alreadygrd then - if List.for_all (noccur_with_meta n nbfix) l then + if List.for_all (noccur_with_meta n nbfix) args then true else raise (CoFixGuardError NestedRecursiveOccurrences) @@ -703,7 +705,7 @@ let check_guard_rec_meta env sigma nbfix def deftype = else error "check_guard_rec_meta: ???" (* ??? *) - | (DOPN (MutConstruct(_,i as cstr_sp),l), args) -> + | IsMutConstruct ((_,i as cstr_sp),l) -> let lra =vlra.(i-1) in let mI = inductive_of_constructor (cstr_sp,l) in let mis = lookup_mind_specif mI env in @@ -741,38 +743,37 @@ let check_guard_rec_meta env sigma nbfix def deftype = in (process_args_of_constr realargs lra) - | (DOP2(Lambda,a,DLAM(_,b)),[]) -> + | IsLambda (_,a,b) -> + assert (args = []); if (noccur_with_meta n nbfix a) then check_rec_call alreadygrd (n+1) vlra b else raise (CoFixGuardError (RecCallInTypeOfAbstraction t)) - | (DOPN(CoFix(j),vargs) as cofix,l) -> - if (List.for_all (noccur_with_meta n nbfix) l) + | IsCoFix (j,(varit,lna,vdefs)) -> + if (List.for_all (noccur_with_meta n nbfix) args) then - let (j,(varit,lna,vdefs)) = destFix cofix in let nbfix = Array.length vdefs in if (array_for_all (noccur_with_meta n nbfix) varit) then (array_for_all (check_rec_call alreadygrd (n+1) vlra) vdefs) && - (List.for_all (check_rec_call alreadygrd (n+1) vlra) l) + (List.for_all (check_rec_call alreadygrd (n+1) vlra) args) else - raise (CoFixGuardError (RecCallInTypeOfDef cofix)) + raise (CoFixGuardError (RecCallInTypeOfDef c)) else - raise (CoFixGuardError (UnguardedRecursiveCall cofix)) + raise (CoFixGuardError (UnguardedRecursiveCall c)) - | (DOPN(MutCase _,_) as mc,l) -> - let (_,p,c,vrest) = destCase mc in + | IsMutCase (_,p,tm,vrest) -> if (noccur_with_meta n nbfix p) then - if (noccur_with_meta n nbfix c) then - if (List.for_all (noccur_with_meta n nbfix) l) then + if (noccur_with_meta n nbfix tm) then + if (List.for_all (noccur_with_meta n nbfix) args) then (array_for_all (check_rec_call alreadygrd n vlra) vrest) else - raise (CoFixGuardError (RecCallInCaseFun mc)) + raise (CoFixGuardError (RecCallInCaseFun c)) else - raise (CoFixGuardError (RecCallInCaseArg mc)) + raise (CoFixGuardError (RecCallInCaseArg c)) else - raise (CoFixGuardError (RecCallInCasePred mc)) + raise (CoFixGuardError (RecCallInCasePred c)) | _ -> raise (CoFixGuardError NotGuardedForm) @@ -790,32 +791,6 @@ let check_cofix env sigma (bodynum,(types,names,bodies)) = with CoFixGuardError err -> error_ill_formed_rec_body CCI env err (List.rev names) i bodies done -(* -let check_cofix env sigma f = - match f with - | DOPN(CoFix(j),vargs) -> - let nbfix = let nv = Array.length vargs in - if nv < 2 then - error "Ill-formed recursive definition" - else - nv-1 - in - let varit = Array.sub vargs 0 nbfix in - let ldef = array_last vargs in - let la = Array.length varit in - let (lna,vdefs) = decomp_DLAMV_name la ldef in - let vlna = Array.of_list lna in - let check_type i = - try - let _ = - check_guard_rec_meta env sigma nbfix vdefs.(i) varit.(i) in - () - with UserError (s,str) -> - error_ill_formed_rec_body CCI env str lna i vdefs - in - for i = 0 to nbfix-1 do check_type i done - | _ -> assert false -*) (* Checks the type of a (co)fixpoint. Fix and CoFix are typed the same way; only the guard condition differs. *) @@ -856,7 +831,7 @@ let control_only_guard env sigma = | IsMutConstruct (_,cl) -> Array.iter control_rec cl | IsConst (_,cl) -> Array.iter control_rec cl | IsEvar (_,cl) -> Array.iter control_rec cl - | IsAppL (_,cl) -> List.iter control_rec cl + | IsAppL (_,cl) -> Array.iter control_rec cl | IsCast (c1,c2) -> control_rec c1; control_rec c2 | IsProd (_,c1,c2) -> control_rec c1; control_rec c2 | IsLambda (_,c1,c2) -> control_rec c1; control_rec c2 |