diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-02-16 17:32:27 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-02-16 17:32:27 -0500 |
| commit | b10381a153d2b15d767cc8ae7100cd6e1d9715f3 (patch) | |
| tree | b690749b531b6a6d17cdc6274a24f6f88b22a76b /src/Reflection/SmartBound.v | |
| parent | 69993c726503957d3b9901525f8fee1402c52ba1 (diff) | |
Add non-exprf version of interpf_smart_unbound
Diffstat (limited to 'src/Reflection/SmartBound.v')
| -rw-r--r-- | src/Reflection/SmartBound.v | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/src/Reflection/SmartBound.v b/src/Reflection/SmartBound.v index f77fe4274..31e8f4fd4 100644 --- a/src/Reflection/SmartBound.v +++ b/src/Reflection/SmartBound.v @@ -85,7 +85,7 @@ Section language. (f:=fun t v => Tbase _) (fun t bs v => Cast _ t (bound_base_type t bs) (Var v)) bounds e. - Definition interpf_smart_unbound {var t} + Definition interpf_smart_unbound_exprf {var t} (bounds : interp_flat_type interp_base_type_bounds t) (e : interp_flat_type (fun t => exprf (var:=var) (Tbase t)) (bound_flat_type bounds)) : interp_flat_type (fun t => @exprf var (Tbase t)) t @@ -94,6 +94,15 @@ Section language. (fun t bs v => Cast _ (bound_base_type t bs) t v) e. + Definition interpf_smart_unbound + {interp_base_type} + (cast_val : forall A A', interp_base_type A -> interp_base_type A') + {t} + (bounds : interp_flat_type interp_base_type_bounds t) + (e : interp_flat_type interp_base_type (bound_flat_type bounds)) + : interp_flat_type interp_base_type t + := SmartFlatTypeMapUnInterp2 (f:=fun _ _ => Tbase _) (fun t b v => cast_val _ _ v) e. + 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)). @@ -131,7 +140,7 @@ Section language. args (fun args => LetIn - (SmartPairf (interpf_smart_unbound input_bounds (SmartVarfMap (fun _ => Var) args))) + (SmartPairf (interpf_smart_unbound_exprf input_bounds (SmartVarfMap (fun _ => Var) args))) (fun v => smart_boundf (ApplyAll e1 (interp_all_binders_for_of' v)) (ApplyInterpedAll' e_bounds input_bounds))))). |