diff options
author | Jason Gross <jgross@mit.edu> | 2017-01-26 18:19:54 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-01-26 18:20:08 -0500 |
commit | 39c70ae2abd720ec76e01c85d2aa0e56aeae3414 (patch) | |
tree | b8ca8c8c4e935a078813d1f753f29db7e95f91d4 /src/Reflection/Map.v | |
parent | 0cf72bdda642db646e25cba8af97f3c63d88764d (diff) |
Split off some bits of Reflection.Syntax
Also split off some bits of Util.Tactics
Diffstat (limited to 'src/Reflection/Map.v')
-rw-r--r-- | src/Reflection/Map.v | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/src/Reflection/Map.v b/src/Reflection/Map.v new file mode 100644 index 000000000..9faa69eb9 --- /dev/null +++ b/src/Reflection/Map.v @@ -0,0 +1,30 @@ +Require Import Crypto.Reflection.Syntax. + +Section language. + Context {base_type_code : Type} + {op : flat_type base_type_code -> flat_type base_type_code -> Type} + {var1 var2 : base_type_code -> Type} + (fvar12 : forall t, var1 t -> var2 t) + (fvar21 : forall t, var2 t -> var1 t). + Local Notation exprf := (@exprf base_type_code op). + Fixpoint mapf_interp_flat_type {t} (e : interp_flat_type var2 t) {struct t} + : interp_flat_type var1 t + := match t return interp_flat_type _ t -> interp_flat_type _ t with + | Tbase _ => fvar21 _ + | Unit => fun v : unit => v + | Prod x y => fun xy => (@mapf_interp_flat_type _ (fst xy), + @mapf_interp_flat_type _ (snd xy)) + end e. + + Fixpoint mapf {t} (e : @exprf var1 t) : @exprf var2 t + := match e in Syntax.exprf _ _ t return exprf t with + | TT => TT + | Var _ x => Var (fvar12 _ x) + | Op _ _ op args => Op op (@mapf _ args) + | LetIn _ ex _ eC => LetIn (@mapf _ ex) (fun x => @mapf _ (eC (mapf_interp_flat_type x))) + | Pair _ ex _ ey => Pair (@mapf _ ex) (@mapf _ ey) + end. +End language. + +Global Arguments mapf_interp_flat_type {_ _ _} _ {t} _. +Global Arguments mapf {_ _ _ _} _ _ {t} _. |