Merge PR #13563: Revival of #9710 (Compact kernel representation of pattern-matching)

Reviewed-by: mattam82
Reviewed-by: SkySkimmer
Ack-by: gares
Ack-by: jfehrle

1 files changed, 17 insertions, 0 deletions

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:
       <p>Cases (c :: (I args)) of b1..bn end