diff options
Diffstat (limited to 'pretyping')
| -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 |
6 files changed, 96 insertions, 17 deletions
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 : |