Add SmartVarMapT

1 files changed, 15 insertions, 0 deletions

diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v
index 35277b8d2..7df4c2a4d 100644
--- a/src/Reflection/Syntax.v
+++ b/src/Reflection/Syntax.v
@@ -155,6 +155,18 @@ Section language.
                                        (@smart_interp_flat_map f g h pair A (fst v))
                                        (@smart_interp_flat_map f g h pair B (snd v))
            end.
+      Fixpoint smart_interp_map {f g}
+               (h : forall x, f x -> g (Tflat (Tbase x)))
+               (h' : forall x, g (Tflat (Tbase x)) -> f x)
+               (pair : forall A B, g (Tflat A) -> g (Tflat B) -> g (Prod A B))
+               (abs : forall A B, (g (Tflat (Tbase A)) -> g B) -> g (Arrow A B))
+               {t}
+        : interp_type_gen (interp_flat_type_gen f) t -> g t
+        := match t return interp_type_gen (interp_flat_type_gen f) t -> g t with
+           | Tflat _ => @smart_interp_flat_map f (fun x => g (Tflat x)) h pair _
+           | Arrow A B => fun v => abs _ _
+                                       (fun x => @smart_interp_map f g h h' pair abs B (v (h' _ x)))
+           end.
       Fixpoint SmartVal {T} (val : forall t : base_type_code, T t) t : interp_flat_type_gen T t
         := match t return interp_flat_type_gen T t with
            | Tbase _ => val _
@@ -169,6 +181,9 @@ Section language.
       Definition SmartVarMap {var var'} (f : forall t, var t -> var' t) {t}
         : interp_flat_type_gen var t -> interp_flat_type_gen var' t
         := @smart_interp_flat_map var (interp_flat_type_gen var') f (fun A B x y => pair x y) t.
+      Definition SmartVarMapT {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.
       Definition SmartVarVar {t} : interp_flat_type_gen var t -> interp_flat_type_gen exprf t
         := SmartVarMap (fun t => Var).
       Definition SmartConst {t} : interp_flat_type t -> interp_flat_type_gen exprf t