diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cClosure.ml | 21 | ||||
| -rw-r--r-- | kernel/esubst.ml | 3 | ||||
| -rw-r--r-- | kernel/esubst.mli | 2 | ||||
| -rw-r--r-- | kernel/nativelambda.ml | 2 | ||||
| -rw-r--r-- | kernel/typeops.ml | 2 | ||||
| -rw-r--r-- | kernel/vmlambda.ml | 2 |
6 files changed, 19 insertions, 13 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index c9326615dc..d2256720c4 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -759,6 +759,10 @@ let get_nth_arg head n stk = | ((ZcaseT _ | Zproj _ | Zfix _ | Zprimitive _) :: _ | []) as s -> (None, List.rev rstk @ s) in strip_rec [] head n stk +let rec subs_consn v i n s = + if Int.equal i n then s + else subs_consn v (i + 1) n (subs_cons v.(i) s) + (* Beta reduction: look for an applied argument in the stack. Since the encountered update marks are removed, h must be a whnf *) let rec get_args n tys f e = function @@ -770,14 +774,13 @@ let rec get_args n tys f e = function get_args n tys f (subs_shft (k,e)) s | Zapp l :: s -> let na = Array.length l in - if n == na then (Inl (subs_cons(l,e)),s) + if n == na then (Inl (subs_consn l 0 na e), s) else if n < na then (* more arguments *) - let args = Array.sub l 0 n in let eargs = Array.sub l n (na-n) in - (Inl (subs_cons(args,e)), Zapp eargs :: s) + (Inl (subs_consn l 0 n e), Zapp eargs :: s) else (* more lambdas *) let etys = List.skipn na tys in - get_args (n-na) etys f (subs_cons(l,e)) s + get_args (n-na) etys f (subs_consn l 0 na e) s | ((ZcaseT _ | Zproj _ | Zfix _ | Zprimitive _) :: _ | []) as stk -> (Inr {mark=mark Cstr Unknown;term=FLambda(n,tys,f,e)}, stk) @@ -931,7 +934,11 @@ let contract_fix_vect fix = env, Array.length bds) | _ -> assert false in - (subs_cons(Array.init nfix make_body, env), thisbody) + let rec mk_subs env i = + if Int.equal i nfix then env + else mk_subs (subs_cons (make_body i) env) (i + 1) + in + (mk_subs env 0, thisbody) let unfold_projection info p = if red_projection info.i_flags p @@ -1367,7 +1374,7 @@ let rec knr info tab m stk = knit info tab fxe fxbd (args@stk') | (_,args, ((Zapp _ | Zfix _ | Zshift _ | Zupdate _ | Zprimitive _) :: _ | [] as s)) -> (m,args@s)) | FLetIn (_,v,_,bd,e) when red_set info.i_flags fZETA -> - knit info tab (subs_cons([|v|],e)) bd stk + knit info tab (subs_cons v e) bd stk | FEvar(ev,env) -> (match info.i_cache.i_sigma ev with Some c -> knit info tab env c stk @@ -1417,7 +1424,7 @@ and case_inversion info tab ci (univs,args) v = let env = info_env info in let ind = ci.ci_ind in let params, indices = Array.chop ci.ci_npar args in - let psubst = subs_cons (params, subs_id 0) in + let psubst = subs_consn params 0 ci.ci_npar (subs_id 0) in let mib = Environ.lookup_mind (fst ind) env in let mip = mib.mind_packets.(snd ind) in (* indtyping enforces 1 ctor with no letins in the context *) diff --git a/kernel/esubst.ml b/kernel/esubst.ml index 97acd698e8..f61dd5a078 100644 --- a/kernel/esubst.ml +++ b/kernel/esubst.ml @@ -134,8 +134,7 @@ let is_subs_id = function | Nil w -> Int.equal w 0 | Cons (_, _, _) -> false -let subs_cons (v, s) = - Array.fold_left (fun accu x -> cons (Arg x) accu) s v +let subs_cons v s = cons (Arg v) s let rec push_vars i s = if Int.equal i 0 then s diff --git a/kernel/esubst.mli b/kernel/esubst.mli index 551c6f1732..9ad422275e 100644 --- a/kernel/esubst.mli +++ b/kernel/esubst.mli @@ -22,7 +22,7 @@ type 'a subs (** Derived constructors granting basic invariants *) val subs_id : int -> 'a subs -val subs_cons: 'a array * 'a subs -> 'a subs +val subs_cons: 'a -> 'a subs -> 'a subs val subs_shft: int * 'a subs -> 'a subs val subs_lift: 'a subs -> 'a subs val subs_liftn: int -> 'a subs -> 'a subs diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 18f16f427d..b27c53ef0f 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -102,7 +102,7 @@ let decompose_Llam_Llet lam = let subst_id = subs_id 0 let lift = subs_lift let liftn = subs_liftn -let cons v subst = subs_cons([|v|], subst) +let cons v subst = subs_cons v subst let shift subst = subs_shft (1, subst) (* Linked code location utilities *) diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 85e24f87b7..802a32b0e7 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -198,7 +198,7 @@ let type_of_apply env func funt argsv argstv = let argt = argstv.(i) in let c1 = term_of_fconstr c1 in begin match conv_leq false env argt c1 with - | () -> apply_rec (i+1) (mk_clos (Esubst.subs_cons ([| inject arg |], e)) c2) + | () -> apply_rec (i+1) (mk_clos (Esubst.subs_cons (inject arg) e) c2) | exception NotConvertible -> error_cant_apply_bad_type env (i+1,c1,argt) diff --git a/kernel/vmlambda.ml b/kernel/vmlambda.ml index 9cca204e8c..390fa58883 100644 --- a/kernel/vmlambda.ml +++ b/kernel/vmlambda.ml @@ -179,7 +179,7 @@ let decompose_Llam lam = let subst_id = subs_id 0 let lift = subs_lift let liftn = subs_liftn -let cons v subst = subs_cons([|v|], subst) +let cons v subst = subs_cons v subst let shift subst = subs_shft (1, subst) (* A generic map function *) |