X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskFlattener.v;h=c7625b8874b57ac96cde6ae035274f2ae249f2fa;hp=1731aad97818d64f9789162903b55bd2b82cfbc1;hb=489b12c6c491b96c37839610d33fbdf666ee527f;hpb=af41ffb1692ae207554342ccdc3bf73abaa75a01 diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v index 1731aad..c7625b8 100644 --- a/src/HaskFlattener.v +++ b/src/HaskFlattener.v @@ -46,7 +46,6 @@ Set Printing Width 130. *) Section HaskFlattener. - Ltac eqd_dec_refl' := match goal with | [ |- context[@eqd_dec ?T ?V ?X ?X] ] => @@ -161,9 +160,6 @@ Section HaskFlattener. (*******************************************************************************) - Context (hetmet_flatten : WeakExprVar). - Context (hetmet_unflatten : WeakExprVar). - Context (hetmet_id : WeakExprVar). Context {unitTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ }. Context {prodTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }. Context {gaTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }. @@ -235,12 +231,12 @@ Section HaskFlattener. flatten_type (HaskTAll κ σ) = HaskTAll κ (fun TV ite v => flatten_rawtype (σ TV ite v)). Axiom flatten_commutes_with_HaskTApp : - forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★), - flatten_type (HaskTApp (weakF σ) (FreshHaskTyVar κ)) = - HaskTApp (weakF (fun TV ite v => flatten_rawtype (σ TV ite v))) (FreshHaskTyVar κ). + forall n κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★), + flatten_type (HaskTApp (weakF_ σ) (FreshHaskTyVar_ κ)) = + HaskTApp (weakF_ (fun TV ite v => flatten_rawtype (σ TV ite v))) (FreshHaskTyVar_(n:=n) κ). - Axiom flatten_commutes_with_weakLT : forall (Γ:TypeEnv) κ t, - flatten_leveled_type (weakLT(Γ:=Γ)(κ:=κ) t) = weakLT(Γ:=Γ)(κ:=κ) (flatten_leveled_type t). + Axiom flatten_commutes_with_weakLT : forall n (Γ:TypeEnv) κ t, + flatten_leveled_type (weakLT_(n:=n)(Γ:=Γ)(κ:=κ) t) = weakLT_(n:=n)(Γ:=Γ)(κ:=κ) (flatten_leveled_type t). Axiom globals_do_not_have_code_types : forall (Γ:TypeEnv) (g:Global Γ) v, flatten_type (g v) = g v. @@ -272,12 +268,14 @@ Section HaskFlattener. ; ga_second : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@l] |- [@ga_mk Γ ec (x,,a) (x,,b) ]@l ] ; ga_lit : ∀ Γ Δ ec l lit , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec [] [literalType lit] ]@l ] ; ga_curry : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (a,,[b]) [c] @@ l] |- [@ga_mk Γ ec a [b ---> c] ]@ l ] + ; ga_loopl : ∀ Γ Δ ec l x y z, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (z,,x) (z,,y) @@ l] |- [@ga_mk Γ ec x y ]@ l ] + ; ga_loopr : ∀ Γ Δ ec l x y z, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (x,,z) (y,,z) @@ l] |- [@ga_mk Γ ec x y ]@ l ] ; 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). @@ -408,6 +406,9 @@ Section HaskFlattener. apply precompose. Defined. + + + (* useful for cutting down on the pretty-printed noise Notation "` x" := (take_lev _ x) (at level 20). @@ -637,66 +638,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. @@ -775,9 +819,6 @@ Section HaskFlattener. (fun TV : Kind → Type => take_arg_types ○ t TV))))). reflexivity. unfold flatten_type. - clear hetmet_flatten. - clear hetmet_unflatten. - clear hetmet_id. clear gar. set (t tv ite) as x. admit. @@ -825,7 +866,7 @@ Section HaskFlattener. | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _ | RLam Γ Δ Σ tx te lev => let case_RLam := tt in _ | RCast Γ Δ Σ σ τ lev γ => let case_RCast := tt in _ - | RAbsT Γ Δ Σ κ σ lev => let case_RAbsT := tt in _ + | RAbsT Γ Δ Σ κ σ lev n => let case_RAbsT := tt in _ | RAppT Γ Δ Σ κ σ τ lev => let case_RAppT := tt in _ | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt in _ | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ lev => let case_RAbsCo := tt in _ @@ -886,6 +927,7 @@ Section HaskFlattener. rename l into g. rename σ into l. destruct l as [|ec lev]; simpl. + (* destruct (eqd_dec (g:CoreVar) (hetmet_flatten:CoreVar)). set (flatten_type (g wev)) as t. set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q. @@ -900,6 +942,7 @@ Section HaskFlattener. apply nd_rule. apply q. apply INil. + *) unfold flatten_leveled_type. simpl. apply nd_rule; rewrite globals_do_not_have_code_types. apply RGlobal. @@ -991,7 +1034,11 @@ Section HaskFlattener. unfold x1. rewrite drop_to_nothing. apply arrangeCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ₁₂)). - admit. (* OK *) + induction Σ₁₂; try destruct a; auto. + simpl. + rewrite <- IHΣ₁₂1 at 2. + rewrite <- IHΣ₁₂2 at 2. + reflexivity. eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ALeft; eapply ACanL | idtac ]. set (mapOptionTree flatten_type Σ₁₂) as a. set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as b. @@ -1031,7 +1078,11 @@ Section HaskFlattener. eapply RArrange. eapply ARight. apply arrangeUnCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ)). - admit (* FIXME *). + induction Σ; try destruct a; auto. + simpl. + rewrite <- IHΣ1 at 2. + rewrite <- IHΣ2 at 2. + reflexivity. idtac. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanL ]. apply boost. @@ -1066,7 +1117,11 @@ Section HaskFlattener. eapply RArrange. eapply ALeft. apply arrangeUnCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ)). - admit (* FIXME *). + induction Σ; try destruct a; auto. + simpl. + rewrite <- IHΣ1 at 2. + rewrite <- IHΣ2 at 2. + reflexivity. idtac. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ]. apply boost. @@ -1082,10 +1137,13 @@ Section HaskFlattener. destruct case_RVoid. simpl. - apply nd_rule. destruct l. + apply nd_rule. apply RVoid. - apply (Prelude_error "RVoid at level >0"). + drop_simplify. + take_simplify. + simpl. + apply ga_id. destruct case_RAppT. simpl. destruct lev; simpl. @@ -1105,8 +1163,8 @@ Section HaskFlattener. rewrite flatten_commutes_with_HaskTApp. eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ]. simpl. - set (mapOptionTree (flatten_leveled_type ) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a. - set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (flatten_leveled_type ) Σ)) as q'. + set (mapOptionTree (flatten_leveled_type ) (mapOptionTree (weakLT_(n:=n)(κ:=κ)) Σ)) as a. + set (mapOptionTree (weakLT_(n:=n)(κ:=κ)) (mapOptionTree (flatten_leveled_type ) Σ)) as q'. assert (a=q'). unfold a. unfold q'. @@ -1156,11 +1214,53 @@ Section HaskFlattener. rewrite IHy1. rewrite IHy2. reflexivity. - apply (Prelude_error "LetRec not supported inside brackets yet (FIXME)"). + repeat drop_simplify. + repeat take_simplify. + simpl. + rewrite drop_to_nothing. + eapply nd_comp. + eapply nd_rule. + eapply RArrange. + eapply AComp. + eapply ARight. + apply arrangeCancelEmptyTree with (q:=y). + induction y; try destruct a; auto. + simpl. + rewrite <- IHy1. + rewrite <- IHy2. + reflexivity. + apply ACanL. + rewrite take_lemma'. + set (mapOptionTree (flatten_type ○ unlev) (take_lev (h :: lev) lri)) as lri'. + set (mapOptionTree flatten_leveled_type (drop_lev (h :: lev) lri)) as lri''. + replace (mapOptionTree (flatten_type ○ unlev) (y @@@ (h :: lev))) with (mapOptionTree flatten_type y). + apply boost. + apply ga_loopl. + rewrite <- mapOptionTree_compose. + simpl. + reflexivity. destruct case_RCase. - simpl. - apply (Prelude_error "Case not supported (BIG FIXME)"). + destruct lev; [ idtac | apply (Prelude_error "case at depth >0") ]; simpl. + apply nd_rule. + rewrite <- mapOptionTree_compose. + replace (mapOptionTree + (fun x => flatten_judgment (pcb_judg (snd x))) + alts,, [Γ > Δ > mapOptionTree flatten_leveled_type Σ |- [flatten_type (caseType tc avars)] @ nil]) + with + (mapOptionTree + (fun x => @pcb_judg tc Γ Δ nil (flatten_type tbranches) avars (fst x) (snd x)) + alts,, + [Γ > Δ > mapOptionTree flatten_leveled_type Σ |- [caseType tc avars] @ nil]). + replace (mapOptionTree flatten_leveled_type + (mapOptionTreeAndFlatten + (fun x => (snd x)) alts)) + with (mapOptionTreeAndFlatten + (fun x => + (snd x)) alts). + apply RCase. + admit. + admit. destruct case_SBrak. simpl. @@ -1251,8 +1351,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").