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.

1 files changed, 23 insertions, 9 deletions

diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 882dfe2848..2add7b0b5e 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -20,6 +20,8 @@ type t = Evd.econstr
 type types = t
 type constr = t
 type existential = t pexistential
+type case_return = t pcase_return
+type case_branch = t pcase_branch
 type fixpoint = (t, t) pfixpoint
 type cofixpoint = (t, t) pcofixpoint
 type unsafe_judgment = (constr, types) Environ.punsafe_judgment
@@ -58,6 +60,9 @@ sig
   val is_empty : t -> bool
 end
 
+type case_invert = (t, EInstance.t) pcase_invert
+type case = (t, t, EInstance.t) pcase
+
 type 'a puniverses = 'a * EInstance.t
 
 (** {5 Destructors} *)
@@ -128,7 +133,7 @@ val mkIndU : inductive * EInstance.t -> t
 val mkConstruct : constructor -> t
 val mkConstructU : constructor * EInstance.t -> t
 val mkConstructUi : (inductive * EInstance.t) * int -> t
-val mkCase : case_info * t * (t,EInstance.t) case_invert * t * t array -> t
+val mkCase : case -> t
 val mkFix : (t, t) pfixpoint -> t
 val mkCoFix : (t, t) pcofixpoint -> t
 val mkArrow : t -> Sorts.relevance  -> t -> t
@@ -199,7 +204,7 @@ val destConst : Evd.evar_map -> t -> Constant.t * EInstance.t
 val destEvar : Evd.evar_map -> t -> t pexistential
 val destInd : Evd.evar_map -> t -> inductive * EInstance.t
 val destConstruct : Evd.evar_map -> t -> constructor * EInstance.t
-val destCase : Evd.evar_map -> t -> case_info * t * (t,EInstance.t) case_invert * t * t array
+val destCase : Evd.evar_map -> t -> case
 val destProj : Evd.evar_map -> t -> Projection.t * t
 val destFix : Evd.evar_map -> t -> (t, t) pfixpoint
 val destCoFix : Evd.evar_map -> t -> (t, t) pcofixpoint
@@ -250,14 +255,12 @@ val compare_constr : Evd.evar_map -> (t -> t -> bool) -> t -> t -> bool
 (** {6 Iterators} *)
 
 val map : Evd.evar_map -> (t -> t) -> t -> t
-val map_user_view : Evd.evar_map -> (t -> t) -> t -> t
 val map_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> t) -> 'a -> t -> t
-val map_under_context : (t -> t) -> int -> t -> t
-val map_branches : (t -> t) -> case_info -> t array -> t array
-val map_return_predicate : (t -> t) -> case_info -> t -> t
+val map_branches : (t -> t) -> case_branch array -> case_branch array
+val map_return_predicate : (t -> t) -> case_return -> case_return
 val iter : Evd.evar_map -> (t -> unit) -> t -> unit
 val iter_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit
-val iter_with_full_binders : Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit
+val iter_with_full_binders : Environ.env -> Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit
 val fold : Evd.evar_map -> ('a -> t -> 'a) -> 'a -> t -> 'a
 
 (** Gather the universes transitively used in the term, including in the
@@ -337,6 +340,17 @@ val fresh_global :
 val is_global : Evd.evar_map -> GlobRef.t -> t -> bool
 [@@ocaml.deprecated "Use [EConstr.isRefX] instead."]
 
+val expand_case : Environ.env -> Evd.evar_map ->
+  case -> (case_info * t * case_invert * t * t array)
+
+val expand_branch : Environ.env -> Evd.evar_map ->
+  EInstance.t -> t array -> constructor -> case_branch -> rel_context
+(** Given a universe instance and parameters for the inductive type,
+    constructs the typed context in which the branch lives. *)
+
+val contract_case : Environ.env -> Evd.evar_map ->
+  (case_info * t * case_invert * t * t array) -> case
+
 (** {5 Extra} *)
 
 val of_existential : Constr.existential -> existential
@@ -345,7 +359,7 @@ val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, typ
 
 val to_rel_decl : Evd.evar_map -> (t, types) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt
 
-val of_case_invert : (Constr.t,Univ.Instance.t) case_invert -> (t,EInstance.t) case_invert
+val of_case_invert : Constr.case_invert -> case_invert
 
 (** {5 Unsafe operations} *)
 
@@ -371,7 +385,7 @@ sig
   val to_instance : EInstance.t -> Univ.Instance.t
   (** Physical identity. Does not care for normalization. *)
 
-  val to_case_invert : (t,EInstance.t) case_invert -> (Constr.t,Univ.Instance.t) case_invert
+  val to_case_invert : case_invert -> Constr.case_invert
 
   val eq : (t, Constr.t) eq
   (** Use for transparent cast between types. *)