diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/declarations.ml | 4 | ||||
| -rw-r--r-- | kernel/declarations.mli | 3 | ||||
| -rw-r--r-- | kernel/indtypes.ml | 2 | ||||
| -rw-r--r-- | kernel/inductive.ml | 24 | ||||
| -rw-r--r-- | kernel/reduction.ml | 9 | ||||
| -rw-r--r-- | kernel/reduction.mli | 3 | ||||
| -rw-r--r-- | kernel/term.ml | 2 | ||||
| -rw-r--r-- | kernel/term.mli | 2 |
8 files changed, 38 insertions, 11 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 725859321c..8b2402bb54 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -135,6 +135,9 @@ type one_inductive_body = { (* Number of expected real arguments of the type (no let, no params) *) mind_nrealargs : int; + (* Length of realargs context (with let, no params) *) + mind_nrealargs_ctxt : int; + (* List of allowed elimination sorts *) mind_kelim : sorts_family list; @@ -223,6 +226,7 @@ let subst_mind_packet sub mbp = mind_arity = subst_arity sub mbp.mind_arity; mind_user_lc = array_smartmap (subst_mps sub) mbp.mind_user_lc; mind_nrealargs = mbp.mind_nrealargs; + mind_nrealargs_ctxt = mbp.mind_nrealargs_ctxt; mind_kelim = mbp.mind_kelim; mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*); mind_nb_constant = mbp.mind_nb_constant; diff --git a/kernel/declarations.mli b/kernel/declarations.mli index fb8317cdcb..454debd736 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -115,6 +115,9 @@ type one_inductive_body = { (* Number of expected real arguments of the type (no let, no params) *) mind_nrealargs : int; + (* Length of realargs context (with let, no params) *) + mind_nrealargs_ctxt : int; + (* List of allowed elimination sorts *) mind_kelim : sorts_family list; diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 4aac096fc4..ccf9b3f6c5 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -588,6 +588,7 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst = (* Compute the set of used section variables *) let hyps = used_section_variables env inds in let nparamargs = rel_context_nhyps params in + let nparamdecls = rel_context_length params in (* Check one inductive *) let build_one_packet (id,cnames,lc,(ar_sign,ar_kind)) recarg = (* Type of constructors in normal form *) @@ -629,6 +630,7 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst = mind_arity = arkind; mind_arity_ctxt = ar_sign; mind_nrealargs = rel_context_nhyps ar_sign - nparamargs; + mind_nrealargs_ctxt = rel_context_length ar_sign - nparamdecls; mind_kelim = kelim; mind_consnames = Array.of_list cnames; mind_consnrealdecls = consnrealargs; diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 23cd99d1e9..6da102a940 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -270,16 +270,20 @@ let get_instantiated_arity (mib,mip) params = let elim_sorts (_,mip) = mip.mind_kelim -let rel_list n m = - let rec reln l p = - if p>m then l else reln (mkRel(n+p)::l) (p+1) +let extended_rel_list n hyps = + let rec reln l p = function + | (_,None,_) :: hyps -> reln (mkRel (n+p) :: l) (p+1) hyps + | (_,Some _,_) :: hyps -> reln l (p+1) hyps + | [] -> l in - reln [] 1 + reln [] 1 hyps let build_dependent_inductive ind (_,mip) params = - let nrealargs = mip.mind_nrealargs in + let realargs,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in applist - (mkInd ind, (List.map (lift nrealargs) params)@(rel_list 0 nrealargs)) + (mkInd ind, + List.map (lift mip.mind_nrealargs_ctxt) params + @ extended_rel_list 0 realargs) (* This exception is local *) exception LocalArity of (sorts_family * sorts_family * arity_error) option @@ -309,6 +313,8 @@ let is_correct_arity env c pj ind specif params = with NotConvertible -> raise (LocalArity None) in check_allowed_sort ksort specif; Constraint.union u univ + | _, (_,Some _,_ as d)::ar' -> + srec (push_rel d env) (lift 1 pt') ar' u | _ -> raise (LocalArity None) in @@ -339,8 +345,8 @@ let build_branches_type ind (_,mip as specif) params p = (* [p] is the predicate, [c] is the match object, [realargs] is the list of real args of the inductive type *) -let build_case_type p c realargs = - beta_appvect p (Array.of_list (realargs@[c])) +let build_case_type n p c realargs = + betazeta_appvect (n+1) p (Array.of_list (realargs@[c])) let type_case_branches env (ind,largs) pj c = let specif = lookup_mind_specif env ind in @@ -349,7 +355,7 @@ let type_case_branches env (ind,largs) pj c = let p = pj.uj_val in let univ = is_correct_arity env c pj ind specif params in let lc = build_branches_type ind specif params p in - let ty = build_case_type p c realargs in + let ty = build_case_type (snd specif).mind_nrealargs_ctxt p c realargs in (lc, ty, univ) diff --git a/kernel/reduction.ml b/kernel/reduction.ml index f1a44b5cac..89f1b443b9 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -117,6 +117,15 @@ let beta_appvect c v = | _ -> 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 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) (b::env) c stack + | _ -> anomaly "Not enough lambda/let's" in + stacklam n [] c (Array.to_list v) + (********************************************************************) (* Conversion *) (********************************************************************) diff --git a/kernel/reduction.mli b/kernel/reduction.mli index de926bd1d6..9960513294 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -66,6 +66,9 @@ val default_conv_leq : types conversion_function (* 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 + (* Pseudo-reduction rule Prod(x,A,B) a --> B[x\a] *) val hnf_prod_applist : env -> types -> constr list -> types diff --git a/kernel/term.ml b/kernel/term.ml index da8a778837..8a2c3278cb 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -26,7 +26,7 @@ type metavariable = int (* This defines Cases annotations *) type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle type case_printing = - { ind_nargs : int; (* number of real args of the inductive type *) + { ind_nargs : int; (* length of the arity of the inductive type *) style : case_style } type case_info = { ci_ind : inductive; diff --git a/kernel/term.mli b/kernel/term.mli index 8f45e39f09..bc1cac44ae 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -42,7 +42,7 @@ type metavariable = int (*s Case annotation *) type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle type case_printing = - { ind_nargs : int; (* number of real args of the inductive type *) + { ind_nargs : int; (* length of the arity of the inductive type *) style : case_style } (* the integer is the number of real args, needed for reduction *) type case_info = |