diff options
-rw-r--r-- | kernel/inductive.ml | 4 | ||||
-rw-r--r-- | kernel/reduction.ml | 36 | ||||
-rw-r--r-- | kernel/reduction.mli | 9 | ||||
-rw-r--r-- | kernel/term.ml | 63 | ||||
-rw-r--r-- | kernel/term.mli | 24 | ||||
-rw-r--r-- | pretyping/inductiveops.ml | 2 | ||||
-rw-r--r-- | pretyping/typing.ml | 3 |
7 files changed, 103 insertions, 38 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 466d48715..632b4daea 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -357,14 +357,14 @@ let build_branches_type (ind,u) (_,mip as specif) params p = let cstr = ith_constructor_of_inductive ind (i+1) in let dep_cstr = applist (mkConstructU (cstr,u),lparams@(extended_rel_list 0 cstrsign)) in vargs @ [dep_cstr] in - let base = betazeta_appvect (mip.mind_nrealdecls+1) (lift nargs p) (Array.of_list cargs) in + let base = lambda_appvect_assum (mip.mind_nrealdecls+1) (lift nargs p) (Array.of_list cargs) in it_mkProd_or_LetIn base cstrsign in Array.mapi build_one_branch mip.mind_nf_lc (* [p] is the predicate, [c] is the match object, [realargs] is the list of real args of the inductive type *) let build_case_type env n p c realargs = - whd_betaiota env (betazeta_appvect (n+1) p (Array.of_list (realargs@[c]))) + whd_betaiota env (lambda_appvect_assum (n+1) p (Array.of_list (realargs@[c]))) let type_case_branches env (pind,largs) pj c = let specif = lookup_mind_specif env (fst pind) in diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 110555011..33beca28a 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -120,24 +120,6 @@ let whd_betadeltaiota_nolet env t = Prod _|Lambda _|Fix _|CoFix _|LetIn _) -> t | _ -> whd_val (create_clos_infos betadeltaiotanolet env) (inject t) -(* Beta *) - -let beta_appvect c v = - let rec stacklam env t stack = - match kind_of_term t, stack with - Lambda(_,_,c), arg::stacktl -> stacklam (arg::env) c stacktl - | _ -> applist (substl env t, stack) in - stacklam [] c (Array.to_list v) - -let betazeta_appvect n c v = - let rec stacklam n env t stack = - if Int.equal n 0 then applist (substl env t, stack) else - match kind_of_term t, stack with - Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl - | LetIn(_,b,_,c), _ -> stacklam (n-1) (substl env b::env) c stack - | _ -> anomaly (Pp.str "Not enough lambda/let's") in - stacklam n [] c (Array.to_list v) - (********************************************************************) (* Conversion *) (********************************************************************) @@ -733,12 +715,28 @@ let conv env t1 t2 = Profile.profile4 convleqkey conv env t1 t2;; *) +(* Application with on-the-fly reduction *) + +let beta_applist c l = + let rec app subst c l = + match kind_of_term c, l with + | Lambda(_,_,c), arg::l -> app (arg::subst) c l + | _ -> applist (substl subst c, l) in + app [] c l + +let beta_appvect c v = beta_applist c (Array.to_list v) + +let beta_app c a = beta_applist c [a] + +(* Compatibility *) +let betazeta_appvect = lambda_appvect_assum + (********************************************************************) (* Special-Purpose Reduction *) (********************************************************************) (* pseudo-reduction rule: - * [hnf_prod_app env s (Prod(_,B)) N --> B[N] + * [hnf_prod_app env (Prod(_,B)) N --> B[N] * with an HNF on the first argument to produce a product. * if this does not work, then we use the string S as part of our * error message. *) diff --git a/kernel/reduction.mli b/kernel/reduction.mli index ef764f34f..7db7e57bb 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -97,14 +97,19 @@ val default_conv_leq : ?l2r:bool -> types conversion_function (************************************************************************) (** Builds an application node, reducing beta redexes it may produce. *) +val beta_applist : constr -> constr list -> constr + +(** Builds an application node, reducing beta redexes it may produce. *) val beta_appvect : constr -> constr array -> constr -(** Builds an application node, reducing the [n] first beta-zeta redexes. *) -val betazeta_appvect : int -> constr -> constr array -> constr +(** Builds an application node, reducing beta redexe it may produce. *) +val beta_app : constr -> constr -> constr (** Pseudo-reduction rule Prod(x,A,B) a --> B[x\a] *) val hnf_prod_applist : env -> types -> constr list -> types +(** Compatibility alias for Term.lambda_appvect_assum *) +val betazeta_appvect : int -> constr -> constr array -> constr (*********************************************************************** s Recognizing products and arities modulo reduction *) diff --git a/kernel/term.ml b/kernel/term.ml index 7d47c4609..455248dd5 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -471,6 +471,36 @@ let rec to_prod n lam = | Cast (c,_,_) -> to_prod n c | _ -> errorlabstrm "to_prod" (mt ()) +let it_mkProd_or_LetIn = List.fold_left (fun c d -> mkProd_or_LetIn d c) +let it_mkLambda_or_LetIn = List.fold_left (fun c d -> mkLambda_or_LetIn d c) + +(* Application with expected on-the-fly reduction *) + +let lambda_applist c l = + let rec app subst c l = + match kind_of_term c, l with + | Lambda(_,_,c), arg::l -> app (arg::subst) c l + | _, [] -> substl subst c + | _ -> anomaly (Pp.str "Not enough lambda's") in + app [] c l + +let lambda_appvect c v = lambda_applist c (Array.to_list v) + +let lambda_app c a = lambda_applist c [a] + +let lambda_applist_assum n c l = + let rec app n subst t l = + if Int.equal n 0 then + if l == [] then substl subst t + else anomaly (Pp.str "Not enough arguments") + else match kind_of_term t, l with + | Lambda(_,_,c), arg::l -> app (n-1) (arg::subst) c l + | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l + | _ -> anomaly (Pp.str "Not enough lambda/let's") in + app n [] c l + +let lambda_appvect_assum n c v = lambda_applist_assum n c (Array.to_list v) + (* pseudo-reduction rule: * [prod_app s (Prod(_,B)) N --> B[N] * with an strip_outer_cast on the first argument to produce a product *) @@ -478,19 +508,32 @@ let rec to_prod n lam = let prod_app t n = match kind_of_term (strip_outer_cast t) with | Prod (_,_,b) -> subst1 n b - | _ -> - errorlabstrm "prod_app" - (str"Needed a product, but didn't find one" ++ fnl ()) - - -(* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *) -let prod_appvect t nL = Array.fold_left prod_app t nL + | _ -> anomaly (str"Needed a product, but didn't find one") (* prod_applist T [ a1 ; ... ; an ] -> (T a1 ... an) *) -let prod_applist t nL = List.fold_left prod_app t nL +let prod_applist c l = + let rec app subst c l = + match kind_of_term c, l with + | Prod(_,_,c), arg::l -> app (arg::subst) c l + | _, [] -> substl subst c + | _ -> anomaly (Pp.str "Not enough prod's") in + app [] c l -let it_mkProd_or_LetIn = List.fold_left (fun c d -> mkProd_or_LetIn d c) -let it_mkLambda_or_LetIn = List.fold_left (fun c d -> mkLambda_or_LetIn d c) +(* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *) +let prod_appvect c v = prod_applist c (Array.to_list v) + +let prod_applist_assum n c l = + let rec app n subst t l = + if Int.equal n 0 then + if l == [] then substl subst t + else anomaly (Pp.str "Not enough arguments") + else match kind_of_term t, l with + | Prod(_,_,c), arg::l -> app (n-1) (arg::subst) c l + | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l + | _ -> anomaly (Pp.str "Not enough prod/let's") in + app n [] c l + +let prod_appvect_assum n c v = prod_applist_assum n c (Array.to_list v) (*********************************) (* Other term destructors *) diff --git a/kernel/term.mli b/kernel/term.mli index 69adb517a..972a67ebe 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -262,14 +262,34 @@ val to_lambda : int -> constr -> constr where [l] is [fun (x_1:T_1)...(x_n:T_n) => T] *) val to_prod : int -> constr -> constr +val it_mkLambda_or_LetIn : constr -> rel_context -> constr +val it_mkProd_or_LetIn : types -> rel_context -> types + +(** In [lambda_applist c args], [c] is supposed to have the form + [λΓ.c] with [Γ] without let-in; it returns [c] with the variables + of [Γ] instantiated by [args]. *) +val lambda_applist : constr -> constr list -> constr +val lambda_appvect : constr -> constr array -> constr + +(** In [lambda_applist_assum n c args], [c] is supposed to have the + form [λΓ.c] with [Γ] of length [m] and possibly with let-ins; it + returns [c] with the assumptions of [Γ] instantiated by [args] and + the local definitions of [Γ] expanded. *) +val lambda_applist_assum : int -> constr -> constr list -> constr +val lambda_appvect_assum : int -> constr -> constr array -> constr + (** pseudo-reduction rule *) (** [prod_appvect] [forall (x1:B1;...;xn:Bn), B] [a1...an] @return [B[a1...an]] *) val prod_appvect : constr -> constr array -> constr val prod_applist : constr -> constr list -> constr -val it_mkLambda_or_LetIn : constr -> rel_context -> constr -val it_mkProd_or_LetIn : types -> rel_context -> types +(** In [prod_appvect_assum n c args], [c] is supposed to have the + form [∀Γ.c] with [Γ] of length [m] and possibly with let-ins; it + returns [c] with the assumptions of [Γ] instantiated by [args] and + the local definitions of [Γ] expanded. *) +val prod_appvect_assum : int -> constr -> constr array -> constr +val prod_applist_assum : int -> constr -> constr list -> constr (** {5 Other term destructors. } *) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index cc4ea5a4a..82168f9c4 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -518,7 +518,7 @@ let type_case_branches_with_names env indspec p c = let (params,realargs) = List.chop nparams args in let lbrty = Inductive.build_branches_type ind specif params p in (* Build case type *) - let conclty = Reduction.betazeta_appvect (mip.mind_nrealdecls+1) p (Array.of_list (realargs@[c])) in + let conclty = lambda_appvect_assum (mip.mind_nrealdecls+1) p (Array.of_list (realargs@[c])) in (* Adjust names *) if is_elim_predicate_explicitly_dependent env p (ind,params) then (set_pattern_names env (fst ind) lbrty, conclty) diff --git a/pretyping/typing.ml b/pretyping/typing.ml index fb5927dbf..15abfefb1 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -112,8 +112,7 @@ let e_type_case_branches env evdref (ind,largs) pj c = let univ = 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 + let ty = whd_betaiota !evdref (lambda_applist_assum (n+1) p (realargs@[c])) in (lc, ty, univ) let e_judge_of_case env evdref ci pj cj lfj = |