diff options
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 117 |
1 files changed, 102 insertions, 15 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index ce12d65614..eb18d4b90e 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -72,7 +72,7 @@ let constructor_instantiate mind u mib c = let s = ind_subst mind mib u in substl s (subst_instance_constr u c) -let instantiate_params full t u args sign = +let instantiate_params t u args sign = let fail () = anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch.") in let (rem_args, subs, ty) = @@ -81,8 +81,7 @@ let instantiate_params full t u args sign = match (decl, largs, kind ty) with | (LocalAssum _, a::args, Prod(_,_,t)) -> (args, a::subs, t) | (LocalDef (_,b,_), _, LetIn(_,_,_,t)) -> - (largs, (substl subs (subst_instance_constr u b))::subs, t) - | (_,[],_) -> if full then fail() else ([], subs, ty) + (largs, (substl subs (subst_instance_constr u b))::subs, t) | _ -> fail ()) sign ~init:(args,[],t) @@ -93,11 +92,11 @@ let instantiate_params full t u args sign = let full_inductive_instantiate mib u params sign = let dummy = Sorts.prop in let t = Term.mkArity (Vars.subst_instance_context u sign,dummy) in - fst (Term.destArity (instantiate_params true t u params mib.mind_params_ctxt)) + fst (Term.destArity (instantiate_params t u params mib.mind_params_ctxt)) let full_constructor_instantiate ((mind,_),u,(mib,_),params) t = let inst_ind = constructor_instantiate mind u mib t in - instantiate_params true inst_ind u params mib.mind_params_ctxt + instantiate_params inst_ind u params mib.mind_params_ctxt (************************************************************************) (************************************************************************) @@ -372,6 +371,91 @@ let check_correct_arity env c pj ind specif params = with LocalArity kinds -> error_elim_arity env ind c pj kinds +(** {6 Changes of representation of Case nodes} *) + +(** Provided: + - a universe instance [u] + - a term substitution [subst] + - name replacements [nas] + [instantiate_context u subst nas ctx] applies both [u] and [subst] to [ctx] + while replacing names using [nas] (order reversed) +*) +let instantiate_context u subst nas ctx = + let rec instantiate i ctx = match ctx with + | [] -> assert (Int.equal i (-1)); [] + | LocalAssum (_, ty) :: ctx -> + let ctx = instantiate (pred i) ctx in + let ty = substnl subst i (subst_instance_constr u ty) in + LocalAssum (nas.(i), ty) :: ctx + | LocalDef (_, ty, bdy) :: ctx -> + let ctx = instantiate (pred i) ctx in + let ty = substnl subst i (subst_instance_constr u ty) in + let bdy = substnl subst i (subst_instance_constr u bdy) in + LocalDef (nas.(i), ty, bdy) :: ctx + in + instantiate (Array.length nas - 1) ctx + +let expand_case_specif mib (ci, u, params, p, iv, c, br) = + (* Γ ⊢ c : I@{u} params args *) + (* Γ, indices, self : I@{u} params indices ⊢ p : Type *) + let mip = mib.mind_packets.(snd ci.ci_ind) in + let paramdecl = Vars.subst_instance_context u mib.mind_params_ctxt in + let paramsubst = Vars.subst_of_rel_context_instance paramdecl (Array.to_list params) in + (* Expand the return clause *) + let ep = + let (nas, p) = p in + let realdecls, _ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in + let self = + let args = Context.Rel.to_extended_vect mkRel 0 mip.mind_arity_ctxt in + let inst = Instance.of_array (Array.init (Instance.length u) Level.var) in + mkApp (mkIndU (ci.ci_ind, inst), args) + in + let realdecls = LocalAssum (Context.anonR, self) :: realdecls in + let realdecls = instantiate_context u paramsubst nas realdecls in + Term.it_mkLambda_or_LetIn p realdecls + in + (* Expand the branches *) + let subst = paramsubst @ ind_subst (fst ci.ci_ind) mib u in + let ebr = + let build_one_branch i (nas, br) (ctx, _) = + let ctx, _ = List.chop mip.mind_consnrealdecls.(i) ctx in + let ctx = instantiate_context u subst nas ctx in + Term.it_mkLambda_or_LetIn br ctx + in + Array.map2_i build_one_branch br mip.mind_nf_lc + in + (ci, ep, iv, c, ebr) + +let expand_case env (ci, _, _, _, _, _, _ as case) = + let specif = Environ.lookup_mind (fst ci.ci_ind) env in + expand_case_specif specif case + +let contract_case env (ci, p, iv, c, br) = + let (mib, mip) = lookup_mind_specif env ci.ci_ind in + let (arity, p) = Term.decompose_lam_n_decls (mip.mind_nrealdecls + 1) p in + let (u, pms) = match arity with + | LocalAssum (_, ty) :: _ -> + (** Last binder is the self binder for the term being eliminated *) + let (ind, args) = decompose_appvect ty in + let (ind, u) = destInd ind in + let () = assert (Ind.CanOrd.equal ind ci.ci_ind) in + let pms = Array.sub args 0 mib.mind_nparams in + (** Unlift the parameters from under the index binders *) + let dummy = List.make mip.mind_nrealdecls mkProp in + let pms = Array.map (fun c -> Vars.substl dummy c) pms in + (u, pms) + | _ -> assert false + in + let p = + let nas = Array.of_list (List.rev_map get_annot arity) in + (nas, p) + in + let map i br = + let (ctx, br) = Term.decompose_lam_n_decls mip.mind_consnrealdecls.(i) br in + let nas = Array.of_list (List.rev_map get_annot ctx) in + (nas, br) + in + (ci, u, pms, p, iv, c, Array.mapi map br) (************************************************************************) (* Type of case branches *) @@ -793,7 +877,8 @@ let rec subterm_specif renv stack t = let f,l = decompose_app (whd_all renv.env t) in match kind f with | Rel k -> subterm_var k renv - | Case (ci,p,_iv,c,lbr) -> (* iv ignored: it's just a cache *) + | Case (ci, u, pms, p, iv, c, lbr) -> (* iv ignored: it's just a cache *) + let (ci, p, _iv, c, lbr) = expand_case renv.env (ci, u, pms, p, iv, c, lbr) in let stack' = push_stack_closures renv l stack in let cases_spec = branches_specif renv (lazy_subterm_specif renv [] c) ci @@ -1018,7 +1103,8 @@ let check_one_fix renv recpos trees def = check_rec_call renv stack (Term.applist(lift p c,l)) end - | Case (ci,p,iv,c_0,lrest) -> (* iv ignored: it's just a cache *) + | Case (ci, u, pms, ret, iv, c_0, br) -> (* iv ignored: it's just a cache *) + let (ci, p, _iv, c_0, lrest) = expand_case renv.env (ci, u, pms, ret, iv, c_0, br) in begin try List.iter (check_rec_call renv []) (c_0::p::l); (* compute the recarg info for the arguments of each branch *) @@ -1040,7 +1126,7 @@ let check_one_fix renv recpos trees def = (* the call to whd_betaiotazeta will reduce the apparent iota redex away *) check_rec_call renv [] - (Term.applist (mkCase (ci,p,iv,c_0,lrest), l)) + (Term.applist (mkCase (ci, u, pms, ret, iv, c_0, br), l)) | _ -> Exninfo.iraise exn end @@ -1324,13 +1410,14 @@ let check_one_cofix env nbfix def deftype = else raise (CoFixGuardError (env,UnguardedRecursiveCall c)) - | Case (_,p,_,tm,vrest) -> (* iv ignored: just a cache *) - begin - let tree = match restrict_spec env (Subterm (Strict, tree)) p with - | Dead_code -> assert false - | Subterm (_, tree') -> tree' - | _ -> raise (CoFixGuardError (env, ReturnPredicateNotCoInductive c)) - in + | Case (ci, u, pms, p, iv, tm, br) -> (* iv ignored: just a cache *) + begin + let (_, p, _iv, tm, vrest) = expand_case env (ci, u, pms, p, iv, tm, br) in + let tree = match restrict_spec env (Subterm (Strict, tree)) p with + | Dead_code -> assert false + | Subterm (_, tree') -> tree' + | _ -> raise (CoFixGuardError (env, ReturnPredicateNotCoInductive c)) + in if (noccur_with_meta n nbfix p) then if (noccur_with_meta n nbfix tm) then if (List.for_all (noccur_with_meta n nbfix) args) then |