diff options
author | Jason Gross <jgross@mit.edu> | 2016-12-02 19:22:41 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2016-12-02 19:22:41 -0500 |
commit | 428c255e87f4b3e4503148cd000dd274f06bac39 (patch) | |
tree | 7abff2514707a07364efadf62f1ccf56cd614229 /src/Reflection/Syntax.v | |
parent | 118f2039566db61cb5ea6158bdf531bd0a4faffd (diff) |
Add SmartFlatTypeMapInterp
Diffstat (limited to 'src/Reflection/Syntax.v')
-rw-r--r-- | src/Reflection/Syntax.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v index 4ee9b8087..fd4a4dfa0 100644 --- a/src/Reflection/Syntax.v +++ b/src/Reflection/Syntax.v @@ -293,6 +293,14 @@ Section language. Definition SmartFlatTypeMap {var'} (f : forall t, var' t -> base_type_code) {t} : interp_flat_type_gen var' t -> flat_type := @smart_interp_flat_map var' (fun _ => flat_type) f (fun _ _ => Prod) t. + Fixpoint SmartFlatTypeMapInterp {var' var''} (f : forall t, var' t -> base_type_code) + (fv : forall t v, var'' (f t v)) {t} {struct t} + : forall v, interp_flat_type_gen var'' (SmartFlatTypeMap f (t:=t) v) + := match t return forall v, interp_flat_type_gen var'' (SmartFlatTypeMap f (t:=t) v) with + | Tbase x => fv _ + | Prod A B => fun xy => (@SmartFlatTypeMapInterp _ _ f fv A (fst xy), + @SmartFlatTypeMapInterp _ _ 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. @@ -431,6 +439,7 @@ Global Arguments SmartValf {_} T _ t. Global Arguments SmartVarVarf {_ _ _ _ _} _. Global Arguments SmartVarfMap {_ _ _} _ {_} _. Global Arguments SmartFlatTypeMap {_ _} _ {_} _. +Global Arguments SmartFlatTypeMapInterp {_ _ _ _} _ {_} _. Global Arguments SmartVarMap_hetero {_ _ _ _ _} _ _ {_} _. Global Arguments SmartVarMap {_ _ _} _ _ {_} _. Global Arguments SmartConstf {_ _ _ _ _} _. |