diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-01-24 17:51:39 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-01-24 17:51:39 -0500 |
| commit | 7cc3f0e665564a11e1ee2cdc200dca481df4a6dc (patch) | |
| tree | 3a59d3693f67627d4ea73ea0277477bb32e0cf91 /src/Reflection/Syntax.v | |
| parent | e14e304755e166b9421f16bbce6119bcfe03a825 (diff) | |
Add SmartFlatTypeUnMap
Diffstat (limited to 'src/Reflection/Syntax.v')
| -rw-r--r-- | src/Reflection/Syntax.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v index 2c9451cea..922e03d64 100644 --- a/src/Reflection/Syntax.v +++ b/src/Reflection/Syntax.v @@ -210,6 +210,9 @@ 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 Unit (fun _ _ => Prod) t. + Definition SmartFlatTypeUnMap (t : flat_type) + : interp_flat_type_gen (fun _ => base_type_code) t + := SmartValf (fun t => t) 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) @@ -356,6 +359,7 @@ Global Arguments SmartVarfPropMap {_ _} _ {_} _. Global Arguments SmartVarfTypeMap2 {_ _ _} _ {t} _ _. Global Arguments SmartVarfPropMap2 {_ _ _} _ {t} _ _. Global Arguments SmartFlatTypeMap {_ _} _ {_} _. +Global Arguments SmartFlatTypeUnMap {_} _ : assert. Global Arguments SmartFlatTypeMapInterp {_ _ _ _} _ {_} _. Global Arguments SmartFlatTypeMapUnInterp {_ _ _ _ _} fv {_ _} _. Global Arguments SmartVarMap_hetero {_ _ _ _ _} _ _ {_} _. |