diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-02-21 15:12:57 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-02-21 15:12:57 -0500 |
| commit | 371ba4b6eb769d3a9a4518df5d4063cf57a6396b (patch) | |
| tree | f482abb3c85844a9fc1088c6cd7ebad1083cc992 /src/Reflection/SmartBound.v | |
| parent | b7d2af40ff07a4bc88024fa8448672d786cdcd66 (diff) | |
Add interpf_smart_bound without exprf
Diffstat (limited to 'src/Reflection/SmartBound.v')
| -rw-r--r-- | src/Reflection/SmartBound.v | 15 |
1 files changed, 13 insertions, 2 deletions
diff --git a/src/Reflection/SmartBound.v b/src/Reflection/SmartBound.v index 31e8f4fd4..74345ef98 100644 --- a/src/Reflection/SmartBound.v +++ b/src/Reflection/SmartBound.v @@ -78,7 +78,7 @@ Section language. end. Section smart_bound. - Definition interpf_smart_bound {var t} + Definition interpf_smart_bound_exprf {var t} (e : interp_flat_type var t) (bounds : interp_flat_type interp_base_type_bounds t) : interp_flat_type (fun t => exprf (var:=var) (Tbase t)) (bound_flat_type bounds) := SmartFlatTypeMap2Interp2 @@ -94,6 +94,17 @@ Section language. (fun t bs v => Cast _ (bound_base_type t bs) t v) e. + Definition interpf_smart_bound + {interp_base_type} + (cast_val : forall A A', interp_base_type A -> interp_base_type A') + {t} + (e : interp_flat_type interp_base_type t) + (bounds : interp_flat_type interp_base_type_bounds t) + : interp_flat_type interp_base_type (bound_flat_type bounds) + := SmartFlatTypeMap2Interp2 + (f:=fun t v => Tbase _) + (fun t bs v => cast_val t (bound_base_type t bs) v) + bounds e. Definition interpf_smart_unbound {interp_base_type} (cast_val : forall A A', interp_base_type A -> interp_base_type A') @@ -105,7 +116,7 @@ Section language. Definition smart_boundf {var t1} (e1 : exprf (var:=var) t1) (bounds : interp_flat_type interp_base_type_bounds t1) : exprf (var:=var) (bound_flat_type bounds) - := LetIn e1 (fun e1' => SmartPairf (var:=var) (interpf_smart_bound e1' bounds)). + := LetIn e1 (fun e1' => SmartPairf (var:=var) (interpf_smart_bound_exprf e1' bounds)). Fixpoint UnSmartArrow {P t} : forall (e_bounds : interp_type interp_base_type_bounds t) (input_bounds : interp_all_binders_for' t interp_base_type_bounds) |