Adding combinators preserving expanded form of branches and pred. of "match".

More precisely: the lambda-let-expanded canonical form of branches and
return predicate is considered as part of the structure of a "match"
and is preserved.

6 files changed, 71 insertions, 8 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 3dc1933a14..2913645c1c 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -259,7 +259,17 @@ let decompose_prod_n_assum sigma n c =
 
 let existential_type = Evd.existential_type
 
-let map sigma f c = match kind sigma c with
+let map_under_context f n c =
+  let f c = unsafe_to_constr (f (of_constr c)) in
+  of_constr (Constr.map_under_context f n (unsafe_to_constr c))
+let map_branches f ci br =
+  let f c = unsafe_to_constr (f (of_constr c)) in
+  of_constr_array (Constr.map_branches f ci (unsafe_to_constr_array br))
+let map_return_predicate f ci p =
+  let f c = unsafe_to_constr (f (of_constr c)) in
+  of_constr (Constr.map_return_predicate f ci (unsafe_to_constr p))
+
+let map_gen userview sigma f c = match kind sigma c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> c
   | Cast (b,k,t) ->
@@ -296,6 +306,12 @@ let map sigma f c = match kind sigma c with
       let l' = Array.Smart.map f l in
       if l'==l then c
       else mkEvar (e, l')
+  | Case (ci,p,b,bl) when userview ->
+      let b' = f b in
+      let p' = map_return_predicate f ci p in
+      let bl' = map_branches f ci bl in
+      if b'==b && p'==p && bl'==bl then c
+      else mkCase (ci, p', b', bl')
   | Case (ci,p,b,bl) ->
       let b' = f b in
       let p' = f p in
@@ -313,6 +329,9 @@ let map sigma f c = match kind sigma c with
       if tl'==tl && bl'==bl then c
       else mkCoFix (ln,(lna,tl',bl'))
 
+let map_user_view = map_gen true
+let map = map_gen false
+
 let map_with_binders sigma g f l c0 = match kind sigma c0 with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> c0
@@ -794,6 +813,7 @@ struct
 let to_sorts = ESorts.unsafe_to_sorts
 let to_instance = EInstance.unsafe_to_instance
 let to_constr = unsafe_to_constr
+let to_constr_array = unsafe_to_constr_array
 let to_rel_decl = unsafe_to_rel_decl
 let to_named_decl = unsafe_to_named_decl
 let to_named_context =
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index ecb36615f3..f897448557 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -224,7 +224,11 @@ 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 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
@@ -315,6 +319,9 @@ sig
   val to_constr : t -> Constr.t
   (** Physical identity. Does not care for defined evars. *)
 
+  val to_constr_array : t array -> Constr.t array
+  (** Physical identity. Does not care for defined evars. *)
+
   val to_rel_decl : (t, types) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt
   (** Physical identity. Does not care for defined evars. *)
 
diff --git a/engine/evd.ml b/engine/evd.ml
index d1c7fef738..faf5f02353 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1267,7 +1267,9 @@ module MiniEConstr = struct
   let kind_of_type sigma c = Term.kind_of_type (whd_evar sigma c)
   let of_kind = Constr.of_kind
   let of_constr c = c
+  let of_constr_array v = v
   let unsafe_to_constr c = c
+  let unsafe_to_constr_array v = v
   let unsafe_eq = Refl
 
   let to_constr ?(abort_on_undefined_evars=true) sigma c =
diff --git a/engine/evd.mli b/engine/evd.mli
index db2bd4eedf..1a5614988d 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -657,10 +657,12 @@ module MiniEConstr : sig
   val of_kind : (t, t, ESorts.t, EInstance.t) Constr.kind_of_term -> t
 
   val of_constr : Constr.t -> t
+  val of_constr_array : Constr.t array -> t array
 
   val to_constr : ?abort_on_undefined_evars:bool -> evar_map -> t -> Constr.t
 
   val unsafe_to_constr : t -> Constr.t
+  val unsafe_to_constr_array : t array -> Constr.t array
 
   val unsafe_eq : (t, Constr.t) eq
 
diff --git a/engine/termops.ml b/engine/termops.ml
index e4c8ae66bc..156d1370e3 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -715,10 +715,26 @@ let map_constr_with_binders_left_to_right sigma g f l c =
 	then c
 	else mkCoFix (ln,(lna,tl',bl'))
 
+let map_under_context_with_full_binders sigma g f l n d =
+  let open EConstr in
+  let f l c = Unsafe.to_constr (f l (of_constr c)) in
+  let g d l = g (of_rel_decl d) l in
+  let d = EConstr.Unsafe.to_constr (EConstr.whd_evar sigma d) in
+  EConstr.of_constr (Constr.map_under_context_with_full_binders g f l n d)
+
+let map_branches_with_full_binders sigma g f l ci bl =
+  let tags = Array.map List.length ci.ci_pp_info.cstr_tags in
+  let bl' = Array.map2 (map_under_context_with_full_binders sigma g f l) tags bl in
+  if Array.for_all2 (==) bl' bl then bl else bl'
+
+let map_return_predicate_with_full_binders sigma g f l ci p =
+  let n = List.length ci.ci_pp_info.ind_tags in
+  let p' = map_under_context_with_full_binders sigma g f l n p in
+  if p' == p then p else p'
+
 (* strong *)
-let map_constr_with_full_binders sigma g f l cstr =
+let map_constr_with_full_binders_gen userview sigma g f l cstr =
   let open EConstr in
-  let open RelDecl in
   match EConstr.kind sigma cstr with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> cstr
@@ -728,16 +744,16 @@ let map_constr_with_full_binders sigma g f l cstr =
       if c==c' && t==t' then cstr else mkCast (c', k, t')
   | Prod (na,t,c) ->
       let t' = f l t in
-      let c' = f (g (LocalAssum (na, t)) l) c in
+      let c' = f (g (RelDecl.LocalAssum (na, t)) l) c in
       if t==t' && c==c' then cstr else mkProd (na, t', c')
   | Lambda (na,t,c) ->
       let t' = f l t in
-      let c' = f (g (LocalAssum (na, t)) l) c in
+      let c' = f (g (RelDecl.LocalAssum (na, t)) l) c in
       if t==t' && c==c' then cstr else  mkLambda (na, t', c')
   | LetIn (na,b,t,c) ->
       let b' = f l b in
       let t' = f l t in
-      let c' = f (g (LocalDef (na, b, t)) l) c in
+      let c' = f (g (RelDecl.LocalDef (na, b, t)) l) c in
       if b==b' && t==t' && c==c' then cstr else mkLetIn (na, b', t', c')
   | App (c,al) ->
       let c' = f l c in
@@ -749,6 +765,12 @@ let map_constr_with_full_binders sigma g f l cstr =
   | Evar (e,al) ->
       let al' = Array.map (f l) al in
       if Array.for_all2 (==) al al' then cstr else mkEvar (e, al')
+  | Case (ci,p,c,bl) when userview ->
+      let p' = map_return_predicate_with_full_binders sigma g f l ci p in
+      let c' = f l c in
+      let bl' = map_branches_with_full_binders sigma g f l ci bl in
+      if p==p' && c==c' && bl'==bl then cstr else
+        mkCase (ci, p', c', bl')
   | Case (ci,p,c,bl) ->
       let p' = f l p in
       let c' = f l c in
@@ -758,7 +780,7 @@ let map_constr_with_full_binders sigma g f l cstr =
   | Fix (ln,(lna,tl,bl)) ->
       let tl' = Array.map (f l) tl in
       let l' =
-        Array.fold_left2 (fun l na t -> g (LocalAssum (na, t)) l) l lna tl in
+        Array.fold_left2 (fun l na t -> g (RelDecl.LocalAssum (na, t)) l) l lna tl in
       let bl' = Array.map (f l') bl in
       if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
       then cstr
@@ -766,12 +788,18 @@ let map_constr_with_full_binders sigma g f l cstr =
   | CoFix(ln,(lna,tl,bl)) ->
       let tl' = Array.map (f l) tl in
       let l' =
-        Array.fold_left2 (fun l na t -> g (LocalAssum (na, t)) l) l lna tl in
+        Array.fold_left2 (fun l na t -> g (RelDecl.LocalAssum (na, t)) l) l lna tl in
       let bl' = Array.map (f l') bl in
       if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
       then cstr
       else mkCoFix (ln,(lna,tl',bl'))
 
+let map_constr_with_full_binders sigma g f =
+  map_constr_with_full_binders_gen false sigma g f
+
+let map_constr_with_full_binders_user_view sigma g f =
+  map_constr_with_full_binders_gen true sigma g f
+
 (* [fold_constr_with_binders g f n acc c] folds [f n] on the immediate
    subterms of [c] starting from [acc] and proceeding from left to
    right according to the usual representation of the constructions as
diff --git a/engine/termops.mli b/engine/termops.mli
index 80988989f1..b967bb6abb 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -63,6 +63,10 @@ val map_constr_with_full_binders :
   Evd.evar_map ->
   (rel_declaration -> 'a -> 'a) ->
   ('a -> constr -> constr) -> 'a -> constr -> constr
+val map_constr_with_full_binders_user_view :
+  Evd.evar_map ->
+  (rel_declaration -> 'a -> 'a) ->
+  ('a -> constr -> constr) -> 'a -> constr -> constr
 
 (** [fold_constr_with_binders g f n acc c] folds [f n] on the immediate
    subterms of [c] starting from [acc] and proceeding from left to