diff options
| -rw-r--r-- | src/Reflection/SmartBound.v | 13 | ||||
| -rw-r--r-- | src/Reflection/SmartBoundWf.v | 16 |
2 files changed, 19 insertions, 10 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))))). diff --git a/src/Reflection/SmartBoundWf.v b/src/Reflection/SmartBoundWf.v index 91f4b1837..0b16577d0 100644 --- a/src/Reflection/SmartBoundWf.v +++ b/src/Reflection/SmartBoundWf.v @@ -33,7 +33,7 @@ Section language. Local Notation smart_bound := (@smart_bound _ _ interp_base_type_bounds bound_base_type Cast). Local Notation UnSmartArrow := (@UnSmartArrow _ interp_base_type_bounds bound_base_type). Local Notation interpf_smart_bound := (@interpf_smart_bound _ op interp_base_type_bounds bound_base_type Cast). - Local Notation interpf_smart_unbound := (@interpf_smart_unbound _ op interp_base_type_bounds bound_base_type Cast). + Local Notation interpf_smart_unbound_exprf := (@interpf_smart_unbound_exprf _ op interp_base_type_bounds bound_base_type Cast). Local Notation bound_op := (@bound_op _ _ _ interp_op_bounds bound_base_type _ base_type_bl_transparent base_type_leb Cast genericize_op). Local Notation wff_SmartCast_match := (@wff_SmartCast_match _ op _ base_type_bl_transparent Cast wff_Cast). @@ -121,20 +121,20 @@ Section language. Local Hint Resolve List.in_app_or List.in_or_app. - Lemma wff_SmartPairf_interpf_smart_unbound var1 var2 t input_bounds x1 x2 + Lemma wff_SmartPairf_interpf_smart_unbound_exprf var1 var2 t input_bounds x1 x2 : wff (flatten_binding_list x1 x2) (SmartPairf (var:=var1) - (interpf_smart_unbound input_bounds - (SmartVarfMap (fun t => Var) x1))) + (interpf_smart_unbound_exprf input_bounds + (SmartVarfMap (fun t => Var) x1))) (SmartPairf (var:=var2) (t:=t) - (interpf_smart_unbound input_bounds - (SmartVarfMap (fun t => Var) x2))). + (interpf_smart_unbound_exprf input_bounds + (SmartVarfMap (fun t => Var) x2))). Proof. clear -wff_Cast. - unfold SmartPairf, SmartVarfMap, interpf_smart_unbound; induction t; + unfold SmartPairf, SmartVarfMap, interpf_smart_unbound_exprf; induction t; repeat match goal with | _ => progress simpl in * | [ |- wff _ (Cast _ _ _ _) (Cast _ _ _ _) ] @@ -147,7 +147,7 @@ Section language. end. Qed. - Local Hint Resolve wff_SmartPairf_interpf_smart_unbound : wf. + Local Hint Resolve wff_SmartPairf_interpf_smart_unbound_exprf : wf. Axiom proof_admitted : False. |