From 371ba4b6eb769d3a9a4518df5d4063cf57a6396b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 21 Feb 2017 15:12:57 -0500 Subject: Add interpf_smart_bound without exprf --- src/Reflection/SmartBound.v | 15 +++++++++++++-- 1 file 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) -- cgit v1.2.3