Add SmartFlatTypeMapUnInterp

1 files changed, 12 insertions, 0 deletions

diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v
index 39ca3059b..a6f57648d 100644
--- a/src/Reflection/Syntax.v
+++ b/src/Reflection/Syntax.v
@@ -301,6 +301,17 @@ Section language.
            | Prod A B => fun xy => (@SmartFlatTypeMapInterp _ _ f fv A (fst xy),
                                     @SmartFlatTypeMapInterp _ _ f fv B (snd xy))
            end.
+      Fixpoint SmartFlatTypeMapUnInterp var' var'' var''' (f : forall t, var' t -> base_type_code)
+               (fv : forall t (v : var' t), var'' (f t v) -> var''' t)
+               {t} {struct t}
+        : forall v, interp_flat_type_gen var'' (SmartFlatTypeMap f (t:=t) v)
+                    -> interp_flat_type_gen var''' t
+        := match t return forall v, interp_flat_type_gen var'' (SmartFlatTypeMap f (t:=t) v)
+                                    -> interp_flat_type_gen var''' t with
+           | Tbase x => fv _
+           | Prod A B => fun v xy => (@SmartFlatTypeMapUnInterp _ _ _ f fv A _ (fst xy),
+                                      @SmartFlatTypeMapUnInterp _ _ _ f fv B _ (snd xy))
+           end.
       Definition SmartVarMap {var var'} (f : forall t, var t -> var' t) (f' : forall t, var' t -> var t) {t}
         : interp_type_gen (interp_flat_type_gen var) t -> interp_type_gen (interp_flat_type_gen var') t
         := @smart_interp_map var (interp_type_gen (interp_flat_type_gen var')) f f' (fun A B x y => pair x y) (fun A B f x => f x) t.
@@ -453,6 +464,7 @@ Global Arguments SmartVarVarf {_ _ _ _ _} _.
 Global Arguments SmartVarfMap {_ _ _} _ {_} _.
 Global Arguments SmartFlatTypeMap {_ _} _ {_} _.
 Global Arguments SmartFlatTypeMapInterp {_ _ _ _} _ {_} _.
+Global Arguments SmartFlatTypeMapUnInterp {_ _ _ _ _} fv {_ _} _.
 Global Arguments SmartVarMap_hetero {_ _ _ _ _} _ _ {_} _.
 Global Arguments SmartVarMap {_ _ _} _ _ {_} _.
 Global Arguments SmartConstf {_ _ _ _ _} _.