From: Adam Megacz Date: Fri, 24 Jun 2011 11:29:06 +0000 (-0700) Subject: HaskFlattener: use pga_kappa a bit more, but not everywhere yet X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=6282ce834832ba35e81d8019cae1ca38d187d07e HaskFlattener: use pga_kappa a bit more, but not everywhere yet --- diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v index 05e9c0b..88714c7 100644 --- a/src/ExtractionMain.v +++ b/src/ExtractionMain.v @@ -267,6 +267,16 @@ Section core2proof. apply curry. Defined. + Definition fToC1' {Γ}{Δ}{a}{s}{lev} : + ND Rule [] [ Γ > Δ > [ ] |- [a ---> s ]@lev ] -> + ND Rule [] [ Γ > Δ > [a @@ lev] |- [ s ]@lev ]. + intro pf. + eapply nd_comp. + apply pf. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanR ]. + apply curry. + Defined. + Definition fToC2 {Γ}{Δ}{a1}{a2}{s}{lev} : ND Rule [] [ Γ > Δ > [] |- [a1 ---> (a2 ---> s) ]@lev ] -> ND Rule [] [ Γ > Δ > [a1 @@ lev],,[a2 @@ lev] |- [ s ]@lev ]. @@ -284,6 +294,17 @@ Section core2proof. apply curry. Defined. + Definition fToCx {Γ}{Δ}{a1}{a2}{a3}{l} Σ : + ND Rule [] [ Γ > Δ > [] |- [(a1 ---> a2) ---> a3 ]@l ] -> + ND Rule [Γ > Δ > Σ,,[a1 @@ l] |- [a2]@l ] + [Γ > Δ > Σ |- [a3]@l ]. + intro pf. + eapply nd_comp; [ eapply nd_rule; eapply RLam | idtac ]. + set (fToC1 pf) as pf'. + apply boost. + apply pf'. + Defined. + Section coqPassCoreToCore. Context (do_flatten : bool) @@ -315,6 +336,7 @@ Section core2proof. (hetmet_pga_curryr : CoreVar) (hetmet_pga_loopl : CoreVar) (hetmet_pga_loopr : CoreVar) + (hetmet_pga_kappa : CoreVar) . @@ -415,16 +437,16 @@ Section core2proof. ; ga_first := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_first (fun ec a b c => _) ec (gat ec a) (gat ec b) (gat ec x)) ; ga_second := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_second (fun ec a b c => _) ec (gat ec a) (gat ec b) (gat ec x)) ; ga_comp := fun Γ Δ ec l a b c => fToC2 (mkGlob4 hetmet_pga_comp (fun ec a b c => _) ec (gat ec a) (gat ec b) (gat ec c)) -(* ; ga_lit := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_lit))*) -(* ; ga_curry := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_curry))*) -(* ; ga_apply := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_apply))*) -(* ; ga_kappa := fun Γ Δ ec l a => fToC1 (nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_kappa)))*) ; ga_loopl := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_loopl (fun ec a b c => _) ec (gat ec a) (gat ec b) (gat ec x)) ; ga_loopr := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_loopr (fun ec a b c => _) ec (gat ec a) (gat ec b) (gat ec x)) + + ; ga_curry := fun Γ Δ ec l a => Prelude_error "ga_curry" + + ; ga_apply := fun Γ Δ ec l a => Prelude_error "ga_apply" ; ga_lit := fun Γ Δ ec l a => Prelude_error "ga_lit" - ; ga_curry := fun Γ Δ ec l a b c => Prelude_error "ga_curry" - ; ga_apply := fun Γ Δ ec l a b c => Prelude_error "ga_apply" - ; ga_kappa := fun Γ Δ ec l a => Prelude_error "ga_kappa" +(* ; ga_lit := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_lit))*) + ; ga_kappa := fun Γ Δ ec l a b c Σ => + fToCx Σ (mkGlob4 hetmet_pga_kappa (fun ec a b c => _) ec (gat ec a) (gat ec b) (gat ec c)) }. Definition hetmet_brak' := coreVarToWeakExprVarOrError hetmet_brak. @@ -539,6 +561,7 @@ Section core2proof. dsLookupVar "GHC.HetMet.Private" "pga_curryr" >>= fun hetmet_pga_curryr => dsLookupVar "GHC.HetMet.Private" "pga_loopl" >>= fun hetmet_pga_loopl => dsLookupVar "GHC.HetMet.Private" "pga_loopr" >>= fun hetmet_pga_loopr => + dsLookupVar "GHC.HetMet.Private" "pga_kappa" >>= fun hetmet_pga_kappa => CoreMreturn (coqPassCoreToCore' @@ -566,6 +589,7 @@ Section core2proof. hetmet_pga_swap hetmet_pga_loopl hetmet_pga_loopr + hetmet_pga_kappa lbinds (* hetmet_pga_applyl diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v index b352398..dd07482 100644 --- a/src/HaskFlattener.v +++ b/src/HaskFlattener.v @@ -274,9 +274,9 @@ Section HaskFlattener. ; ga_comp : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l],,[@ga_mk Γ ec b c @@ l] |- [@ga_mk Γ ec a c ]@l ] ; ga_apply : ∀ Γ Δ ec l a a' b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a [b ---> c] @@ l],,[@ga_mk Γ ec a' [b] @@ l] |- [@ga_mk Γ ec (a,,a') [c] ]@l ] - ; ga_kappa : ∀ Γ Δ ec l a b Σ, ND Rule - [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b ]@l ] - [Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@l ] + ; ga_kappa : ∀ Γ Δ ec l a b c Σ, ND Rule + [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec b c ]@l ] + [Γ > Δ > Σ |- [@ga_mk Γ ec (a,,b) c ]@l ] }. Context `(gar:garrow). @@ -636,66 +636,109 @@ Section HaskFlattener. clear y q. set (mapOptionTree flatten_leveled_type (dropT (mkFlags (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ))) as q. - destruct (decide_tree_empty q); [ idtac | apply (Prelude_error "escapifying open code not yet supported") ]. - destruct s. + destruct (decide_tree_empty q). - simpl. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AExch ]. - set (fun z z' => @RLet Γ Δ z (mapOptionTree flatten_leveled_type q') t z' nil) as q''. - eapply nd_comp; [ idtac | apply RLet ]. - clear q''. - eapply nd_comp; [ apply nd_rlecnac | idtac ]. - apply nd_prod. - apply nd_rule. - apply RArrange. - eapply AComp; [ idtac | apply ACanR ]. - apply ALeft. - apply (@arrangeCancelEmptyTree _ _ _ _ e). - - eapply nd_comp. - eapply nd_rule. - eapply (@RVar Γ Δ t nil). - apply nd_rule. + destruct s. + simpl. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AExch ]. + set (fun z z' => @RLet Γ Δ z (mapOptionTree flatten_leveled_type q') t z' nil) as q''. + eapply nd_comp; [ idtac | apply RLet ]. + clear q''. + eapply nd_comp; [ apply nd_rlecnac | idtac ]. + apply nd_prod. + apply nd_rule. apply RArrange. - eapply AComp. - apply AuCanR. + eapply AComp; [ idtac | apply ACanR ]. apply ALeft. - apply AWeak. -(* - eapply decide_tree_empty. - - simpl. - set (dropT (mkFlags (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ)) as escapified. - destruct (decide_tree_empty escapified). + apply (@arrangeCancelEmptyTree _ _ _ _ e). + + eapply nd_comp. + eapply nd_rule. + eapply (@RVar Γ Δ t nil). + apply nd_rule. + apply RArrange. + eapply AComp. + apply AuCanR. + apply ALeft. + apply AWeak. - induction succ. - destruct a. - unfold drop_lev. - destruct l. simpl. - unfold mkDropFlags; simpl. + clear q. + unfold q'. + clear q'. + apply nd_rule. + apply RArrange. + induction succ. + destruct a. + destruct l as [t' l']. + simpl. + Transparent drop_lev. + simpl. unfold take_lev. unfold mkTakeFlags. simpl. - destruct (General.list_eq_dec h0 (ec :: nil)). - simpl. - rewrite e. - apply nd_id. - simpl. - apply nd_rule. - apply RArrange. - apply ALeft. - apply AWeak. + unfold drop_lev. simpl. - apply nd_rule. - unfold take_lev. - simpl. - apply RArrange. - apply ALeft. - apply AWeak. - apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported"). -*) - Defined. + unfold mkDropFlags. + simpl. + unfold flatten_leveled_type. + destruct (General.list_eq_dec l' (ec :: nil)); simpl. + rewrite e. + unfold levels_to_tcode. + eapply AComp. + apply ACanL. + apply AuCanR. + eapply AComp. + apply ACanR. + eapply AComp. + apply AuCanL. + apply ARight. + apply AWeak. + + simpl. + apply ARight. + apply AWeak. + + drop_simplify. + simpl. + set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ2)) as d2 in *. + set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ1)) as d1 in *. + set (mapOptionTree flatten_leveled_type (dropT (mkFlags + (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ1))) as s1 in *. + set (mapOptionTree flatten_leveled_type (dropT (mkFlags + (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ2))) as s2 in *. + set (mapOptionTree (flatten_type ○ unlev) (dropT (mkFlags + (liftBoolFunc true (bnot ○ levelMatch (ec :: nil))) succ1))) as s1' in *. + set (mapOptionTree (flatten_type ○ unlev) (dropT (mkFlags + (liftBoolFunc true (bnot ○ levelMatch (ec :: nil))) succ2))) as s2' in *. + + eapply AComp. + apply arrangeSwapMiddle. + + eapply AComp. + eapply ALeft. + apply IHsucc2. + + eapply AComp. + eapply ARight. + apply IHsucc1. + + eapply AComp. + apply arrangeSwapMiddle. + apply ARight. + unfold take_lev. + unfold mkTakeFlags. + + unfold s1'. + unfold s2'. + clear s1' s2'. + set (mapOptionTree (flatten_type ○ unlev) (dropT (mkFlags + (liftBoolFunc true (bnot ○ levelMatch (ec :: nil))) succ1))) as s1' in *. + set (mapOptionTree (flatten_type ○ unlev) (dropT (mkFlags + (liftBoolFunc true (bnot ○ levelMatch (ec :: nil))) succ2))) as s2' in *. + + apply (Prelude_error "almost there!"). + Defined. Lemma unlev_relev : forall {Γ}(t:Tree ??(HaskType Γ ★)) lev, mapOptionTree unlev (t @@@ lev) = t. intros. @@ -1306,8 +1349,37 @@ Section HaskFlattener. apply secondify. apply IHx2. - (* environment has non-empty leaves *) - apply (Prelude_error "ga_kappa not supported yet (BIG FIXME)"). + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ]. + + replace (mapOptionTree (fun ht => levels_to_tcode (unlev ht) (getlev ht) @@ nil) (drop_lev (ec :: nil) succ)) + with (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)). + eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply AExch | idtac ]. + apply ga_kappa. + induction succ. + destruct a. + destruct l. + Transparent drop_lev. + simpl. + unfold drop_lev. + Opaque drop_lev. + unfold mkDropFlags. + simpl. + destruct (General.list_eq_dec h1 (ec :: nil)). + simpl. + auto. + simpl. + unfold flatten_leveled_type. + simpl. + auto. + simpl. + auto. + simpl. + drop_simplify. + simpl. + rewrite IHsucc1. + rewrite IHsucc2. + reflexivity. (* nesting too deep *) apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").