From d72e5c154faeea1d55387bc8c039d97f63ebd1c4 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 3 Mar 2019 21:03:37 +0100 Subject: Change the representation of kernel case. We store bound variable names instead of functions for both branches and predicate, and we furthermore add the parameters in the node. Let bindings are not taken into account and require an environment lookup for retrieval. --- kernel/inductive.mli | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) (limited to 'kernel/inductive.mli') diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 78658dc4de..5808a3fa65 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -79,6 +79,23 @@ val arities_of_specif : MutInd.t puniverses -> mind_specif -> types array val inductive_params : mind_specif -> int +(** Given a pattern-matching represented compactly, expands it so as to produce + lambda and let abstractions in front of the return clause and the pattern + branches. *) +val expand_case : env -> case -> (case_info * constr * case_invert * constr * constr array) + +val expand_case_specif : mutual_inductive_body -> case -> (case_info * constr * case_invert * constr * constr array) + +(** Dual operation of the above. Fails if the return clause or branch has not + the expected form. *) +val contract_case : env -> (case_info * constr * case_invert * constr * constr array) -> case + +(** [instantiate_context u subst nas ctx] applies both [u] and [subst] + to [ctx] while replacing names using [nas] (order reversed). In particular, + assumes that [ctx] and [nas] have the same length. *) +val instantiate_context : Instance.t -> Vars.substl -> Name.t Context.binder_annot array -> + rel_context -> rel_context + (** [type_case_branches env (I,args) (p:A) c] computes useful types about the following Cases expression:

Cases (c :: (I args)) of b1..bn end -- cgit v1.2.3