diff options
| -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 | ||||
| -rw-r--r-- | pretyping/cases.ml | 31 | ||||
| -rw-r--r-- | pretyping/indrec.ml | 55 | ||||
| -rw-r--r-- | pretyping/inductiveops.ml | 4 | ||||
| -rw-r--r-- | pretyping/inductiveops.mli | 2 | ||||
| -rw-r--r-- | pretyping/termops.ml | 19 | ||||
| -rw-r--r-- | pretyping/termops.mli | 2 | ||||
| -rw-r--r-- | test-suite/success/Inductive.v | 32 | ||||
| -rw-r--r-- | test-suite/success/induct.v | 19 |
16 files changed, 182 insertions, 31 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 = diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 057f342aa6..1f9cc0f1f4 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -954,14 +954,18 @@ let adjust_impossible_cases pb pred tomatch submat = (* s.t Gamma,x1'..xn' |- match Pushed(x1')..Pushed(xn') rest with..end :pred'*) (* *) (*****************************************************************************) -let specialize_predicate newtomatchs (names,(depna,_)) cs tms ccl = +let specialize_predicate newtomatchs (names,(depna,_)) arsign cs tms ccl = (* Assume some gamma st: gamma, (X,x:=realargs,copt), tms |- ccl *) let nrealargs = List.length names in let k = nrealargs + (if depna<>Anonymous then 1 else 0) in (* We adjust pred st: gamma, x1..xn, (X,x:=realargs,copt), tms |- ccl' *) let n = cs.cs_nargs in let ccl' = liftn_predicate n (k+1) ccl tms in - let argsi = if nrealargs <> 0 then Array.to_list cs.cs_concl_realargs else [] in + let argsi = + if nrealargs <> 0 then + adjust_subst_to_rel_context arsign (Array.to_list cs.cs_concl_realargs) + else + [] in let copti = if depna<>Anonymous then Some (build_dependent_constructor cs) else None in (* The substituends argsi, copti are all defined in gamma, x1...xn *) (* We need _parallel_ bindings to get gamma, x1...xn, tms |- ccl'' *) @@ -1063,7 +1067,7 @@ let shift_problem ((current,t),_,(nadep,_)) pb = mat = List.map remove_current_pattern pb.mat } (* Building the sub-pattern-matching problem for a given branch *) -let build_branch current deps (realnames,dep) pb eqns const_info = +let build_branch current deps (realnames,dep) pb arsign eqns const_info = (* We remember that we descend through a constructor *) let alias_type = if Array.length const_info.cs_concl_realargs = 0 @@ -1120,7 +1124,7 @@ let build_branch current deps (realnames,dep) pb eqns const_info = 1 typs' (List.rev dep_sign) in let pred = - specialize_predicate typs'' (realnames,dep) const_info tomatch pb.pred in + specialize_predicate typs'' (realnames,dep) arsign const_info tomatch pb.pred in let currents = List.map (fun x -> Pushed x) typs'' in @@ -1179,6 +1183,7 @@ and match_current pb tomatch = | IsInd (_,(IndType(indf,realargs) as indt),names) -> let mind,_ = dest_ind_family indf in let cstrs = get_constructors pb.env indf in + let arsign, _ = get_arity pb.env indf in let eqns,onlydflt = group_equations pb mind current cstrs pb.mat in if (Array.length cstrs <> 0 or pb.mat <> []) & onlydflt then compile (shift_problem ct pb) @@ -1189,7 +1194,7 @@ and match_current pb tomatch = let pb = generalize_problem (names,dep) pb deps in (* We compile branches *) - let brs = array_map2 (compile_branch current (names,dep) deps pb) eqns cstrs in + let brs = array_map2 (compile_branch current (names,dep) deps pb arsign) eqns cstrs in (* We build the (elementary) case analysis *) let brvals = Array.map (fun (v,_) -> v) brs in @@ -1202,8 +1207,8 @@ and match_current pb tomatch = { uj_val = applist (case, inst); uj_type = substl inst typ } -and compile_branch current names deps pb eqn cstr = - let sign, pb = build_branch current deps names pb eqn cstr in +and compile_branch current names deps pb arsign eqn cstr = + let sign, pb = build_branch current deps names pb arsign eqn cstr in let j = compile pb in (it_mkLambda_or_LetIn j.uj_val sign, j.uj_type) @@ -1550,19 +1555,19 @@ let extract_arity_signature env0 tomatchl tmsign = str"Unexpected type annotation for a term of non inductive type.")) | IsInd (term,IndType(indf,realargs),_) -> let indf' = lift_inductive_family n indf in - let (ind,params) = dest_ind_family indf' in - let nrealargs = List.length realargs in + let (ind,_) = dest_ind_family indf' in + let nparams_ctxt,nrealargs_ctxt = inductive_nargs env0 ind in + let arsign = fst (get_arity env0 indf') in let realnal = match t with | Some (loc,ind',nparams,realnal) -> if ind <> ind' then user_err_loc (loc,"",str "Wrong inductive type."); - if List.length params <> nparams - or nrealargs <> List.length realnal then + if nparams_ctxt <> nparams + or nrealargs_ctxt <> List.length realnal then anomaly "Ill-formed 'in' clause in cases"; List.rev realnal - | None -> list_make nrealargs Anonymous in - let arsign = fst (get_arity env0 indf') in + | None -> list_make nrealargs_ctxt Anonymous in (* let na = *) (* match na with *) (* | Name _ -> na *) diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 6a4c066ce5..0b07bc8599 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -58,7 +58,7 @@ let mis_make_case_com depopt env sigma ind (mib,mip as specif) kind = (RecursionSchemeError (NotAllowedCaseAnalysis (false,new_sort_in_family kind,ind))); - let ndepar = mip.mind_nrealargs + 1 in + let ndepar = mip.mind_nrealargs_ctxt + 1 in (* Pas génant car env ne sert pas à typer mais juste à renommer les Anonym *) (* mais pas très joli ... (mais manque get_sort_of à ce niveau) *) @@ -594,3 +594,56 @@ let lookup_eliminator ind_sp s = pr_global_env Idset.empty (IndRef ind_sp) ++ strbrk " on sort " ++ pr_sort_family s ++ strbrk " is probably not allowed.") + +(* Build the congruence lemma associated to an inductive type + I p1..pn a1..am with one constructor C : I q1..qn b1..bm *) + +(* TODO: extend it to types with more than one index *) + +let build_congr env (eq,refl) ind (mib,mip) = + if Array.length mib.mind_packets <> 1 or Array.length mip.mind_nf_lc <> 1 then + error "Not an inductive type with a single constructor."; + if mip.mind_nrealargs <> 1 then + error "Expect an inductive type with one predicate parameter."; + let i = 1 in + let realsign,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in + if List.exists (fun (_,b,_) -> b <> None) realsign then + error "Inductive equalities with local definitions in arity not supported"; + let env_with_arity = push_rel_context mip.mind_arity_ctxt env in + let (_,_,ty) = lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity in + let _,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in + let _,constrargs = decompose_app ccl in + let c = List.nth constrargs (i - 1) in + let varB = id_of_string "B" in + let varH = id_of_string "H" in + let varf = id_of_string "f" in + let ci = make_case_info (Global.env()) ind RegularStyle in + let my_it_mkLambda_or_LetIn s c = it_mkLambda_or_LetIn ~init:c s in + let my_it_mkLambda_or_LetIn_name s c = it_mkLambda_or_LetIn_name env c s in + my_it_mkLambda_or_LetIn mib.mind_params_ctxt + (mkNamedLambda varB (new_Type ()) + (mkNamedLambda varf (mkArrow (lift 1 ty) (mkVar varB)) + (my_it_mkLambda_or_LetIn_name (lift_rel_context 2 realsign) + (mkNamedLambda varH + (applist + (mkInd ind, + extended_rel_list (mip.mind_nrealargs+2) mib.mind_params_ctxt @ + extended_rel_list 0 realsign)) + (mkCase (ci, + my_it_mkLambda_or_LetIn_name + (lift_rel_context (mip.mind_nrealargs+3) realsign) + (mkLambda + (Anonymous, + applist + (mkInd ind, + extended_rel_list (2*mip.mind_nrealargs+3) mib.mind_params_ctxt + @ extended_rel_list 0 realsign), + mkApp (eq, + [|mkVar varB; + mkApp (mkVar varf, [|lift (2*mip.mind_nrealargs+3) c|]); + mkApp (mkVar varf, [|mkRel (mip.mind_nrealargs - i + 2)|])|]))), + mkVar varH, + [|mkApp (refl, + [|mkVar varB; + mkApp (mkVar varf, [|lift (mip.mind_nrealargs+2) c|])|])|])))))) + diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 45fbe3227b..3150ed63b5 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -129,7 +129,7 @@ let get_full_arity_sign env ind = let inductive_nargs env ind = let (mib,mip) = Inductive.lookup_mind_specif env ind in - mib.mind_nparams, mip.mind_nrealargs + (rel_context_length (mib.mind_params_ctxt), mip.mind_nrealargs_ctxt) let allowed_sorts env (kn,i as ind) = let (mib,mip) = Inductive.lookup_mind_specif env ind in @@ -138,7 +138,7 @@ let allowed_sorts env (kn,i as ind) = (* Annotation for cases *) let make_case_info env ind style = let (mib,mip) = Inductive.lookup_mind_specif env ind in - let print_info = { ind_nargs = mip.mind_nrealargs; style = style } in + let print_info = { ind_nargs = mip.mind_nrealargs_ctxt; style = style } in { ci_ind = ind; ci_npar = mib.mind_nparams; ci_cstr_nargs = mip.mind_consnrealdecls; diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 357fb09082..cc1bb7f418 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -58,7 +58,7 @@ val mis_nf_constructor_type : val mis_constr_nargs : inductive -> int array val mis_constr_nargs_env : env -> inductive -> int array -(* Return number of expected parameters and of expected real arguments *) +(* Return the lengths of parameters signature and real arguments signature *) val inductive_nargs : env -> inductive -> int * int val mis_constructor_nargs_env : env -> constructor -> int diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 4034d86674..47bc972513 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -1096,6 +1096,25 @@ let substl_rel_context l = let lift_rel_context n = map_rel_context_with_binders (liftn n) +let smash_rel_context sign = + let rec aux acc = function + | [] -> acc + | (_,None,_ as d) :: l -> aux (d::acc) l + | (_,Some b,_) :: l -> + (* Quadratic in the number of let but there are probably a few of them *) + aux (List.rev (substl_rel_context [b] (List.rev acc))) l + in List.rev (aux [] sign) + +let adjust_subst_to_rel_context sign l = + let rec aux subst sign l = + match sign, l with + | (_,None,_)::sign', a::args' -> aux (a::subst) sign' args' + | (_,Some c,_)::sign', args' -> + aux (substl (List.rev subst) c :: subst) sign' args' + | [], [] -> List.rev subst + | _ -> anomaly "Instance and signature do not match" + in aux [] (List.rev sign) l + let fold_named_context_both_sides f l ~init = list_fold_right_and_left f l init let rec mem_named_context id = function diff --git a/pretyping/termops.mli b/pretyping/termops.mli index f9d4329077..3d167ebb03 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -267,6 +267,8 @@ val process_rel_context : (rel_declaration -> env -> env) -> env -> env val assums_of_rel_context : rel_context -> (name * constr) list val lift_rel_context : int -> rel_context -> rel_context val substl_rel_context : constr list -> rel_context -> rel_context +val smash_rel_context : rel_context -> rel_context (* expand lets in context *) +val adjust_subst_to_rel_context : rel_context -> constr list -> constr list val map_rel_context_in_env : (env -> constr -> constr) -> env -> rel_context -> rel_context val map_rel_context_with_binders : diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index 1adcbd39a1..724ba502c7 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -1,4 +1,32 @@ -(* Check local definitions in context of inductive types *) +(* Test des definitions inductives imbriquees *) + +Require Import List. + +Inductive X : Set := + cons1 : list X -> X. + +Inductive Y : Set := + cons2 : list (Y * Y) -> Y. + +(* Test inductive types with local definitions (arity) *) + +Inductive eq1 : forall A:Type, let B:=A in A -> Prop := + refl1 : eq1 True I. + +Check + fun (P : forall A : Type, let B := A in A -> Type) (f : P True I) (A : Type) => + let B := A in + fun (a : A) (e : eq1 A a) => + match e in (eq1 A0 B0 a0) return (P A0 a0) with + | refl1 => f + end. + +Inductive eq2 (A:Type) (a:A) + : forall B C:Type, let D:=(A*B*C)%type in D -> Prop := + refl2 : eq2 A a unit bool (a,tt,true). + +(* Check inductive types with local definitions (parameters) *) + Inductive A (C D : Prop) (E:=C) (F:=D) (x y : E -> F) : E -> Set := I : forall z : E, A C D x y z. @@ -9,7 +37,7 @@ Check fun (x y : E -> F) (P : forall c : C, A C D x y c -> Type) (f : forall z : C, P z (I C D x y z)) (y0 : C) (a : A C D x y y0) => - match a as a0 in (A _ _ _ _ y1) return (P y1 a0) with + match a as a0 in (A _ _ _ _ _ _ y1) return (P y1 a0) with | I x0 => f x0 end). diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index 2aec6e9b1c..1cf707583b 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -5,7 +5,8 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Teste des definitions inductives imbriquees *) + +(* Test des definitions inductives imbriquees *) Require Import List. @@ -15,3 +16,19 @@ Inductive X : Set := Inductive Y : Set := cons2 : list (Y * Y) -> Y. +(* Test inductive types with local definitions *) + +Inductive eq1 : forall A:Type, let B:=A in A -> Prop := + refl1 : eq1 True I. + +Check + fun (P : forall A : Type, let B := A in A -> Type) (f : P True I) (A : Type) => + let B := A in + fun (a : A) (e : eq1 A a) => + match e in (eq1 A0 B0 a0) return (P A0 a0) with + | refl1 => f + end. + +Inductive eq2 (A:Type) (a:A) + : forall B C:Type, let D:=(A*B*C)%type in D -> Prop := + refl2 : eq2 A a unit bool (a,tt,true). |