X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskFlattener.v;h=59636bf87830880d016ab7372c6f2629a4cd453f;hp=d822dd6700cb7f959aae9b25c047a4e81e71427e;hb=3a2879d925d4e13e9c89bc768df111684d2b4a59;hpb=16fef762b0a81544a31b6392059d148431e984be diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v index d822dd6..59636bf 100644 --- a/src/HaskFlattener.v +++ b/src/HaskFlattener.v @@ -161,9 +161,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 ★ }. @@ -272,6 +269,8 @@ 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 ] @@ -288,7 +287,7 @@ Section HaskFlattener. ND Rule [ Γ > Δ > ant |- [x]@lev ] [ Γ > Δ > ant |- [y]@lev ]. intros. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ]. - eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ]. + eapply nd_comp; [ idtac | apply RLet ]. eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod. apply nd_id. @@ -304,7 +303,7 @@ Section HaskFlattener. [ Γ > Δ > a |- [@ga_mk _ ec y z ]@lev ] [ Γ > Δ > a,,[@ga_mk _ ec x y @@ lev] |- [@ga_mk _ ec x z ]@lev ]. intros. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. + eapply nd_comp; [ idtac | eapply RLet ]. eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod. apply nd_id. @@ -327,7 +326,7 @@ Section HaskFlattener. [ Γ > Δ > a |- [@ga_mk _ ec x y ]@lev ] [ Γ > Δ > a,,[@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z ]@lev ]. intros. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. + eapply nd_comp; [ idtac | eapply RLet ]. eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod. apply nd_id. @@ -348,7 +347,7 @@ Section HaskFlattener. [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) ]@lev ]. intros. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ]. - eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ]. + eapply nd_comp; [ idtac | apply RLet ]. eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod. apply nd_id. @@ -371,7 +370,7 @@ Section HaskFlattener. [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) ]@lev ]. intros. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ]. - eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ]. + eapply nd_comp; [ idtac | apply RLet ]. eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod. apply nd_id. @@ -394,12 +393,12 @@ Section HaskFlattener. [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x b ]@l ]. intros. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. + eapply nd_comp; [ idtac | eapply RLet ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. apply nd_prod. apply ga_first. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. + eapply nd_comp; [ idtac | eapply RLet ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. apply nd_prod. apply postcompose. @@ -450,14 +449,14 @@ Section HaskFlattener. set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) b)) as b' in *. set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) c)) as c' in *. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ]. - eapply nd_comp; [ idtac | eapply nd_rule; apply + eapply nd_comp; [ idtac | apply (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' b') (@ga_mk _ (v2t ec) a' c')) ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. apply nd_prod. apply r2'. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ]. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ]. - eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ]. + eapply nd_comp; [ idtac | apply RLet ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. eapply nd_prod. apply r1'. @@ -537,13 +536,13 @@ Section HaskFlattener. intro pfb. apply secondify with (c:=a) in pfb. apply firstify with (c:=[]) in pfa. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. + eapply nd_comp; [ idtac | eapply RLet ]. eapply nd_comp; [ eapply nd_llecnac | idtac ]. apply nd_prod. apply pfa. clear pfa. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. + eapply nd_comp; [ idtac | eapply RLet ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. apply nd_prod. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ]. @@ -576,7 +575,7 @@ Section HaskFlattener. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ]. simpl. eapply nd_comp; [ apply nd_llecnac | idtac ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. + eapply nd_comp; [ idtac | eapply RLet ]. apply nd_prod. Focus 2. apply nd_id. @@ -643,7 +642,7 @@ Section HaskFlattener. 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 | eapply nd_rule; apply RLet ]. + eapply nd_comp; [ idtac | apply RLet ]. clear q''. eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod. @@ -775,9 +774,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. @@ -830,11 +826,9 @@ Section HaskFlattener. | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt in _ | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ lev => let case_RAbsCo := tt in _ | RApp Γ Δ Σ₁ Σ₂ tx te lev => let case_RApp := tt in _ - | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev => let case_RLet := tt in _ - | RCut Γ Δ Σ₁ Σ₁₂ Σ₂ Σ₃ l => let case_RCut := tt in _ - | RLeft Γ Δ Σ₁ Σ₂ Σ l => let case_RLeft := tt in _ - | RRight Γ Δ Σ₁ Σ₂ Σ l => let case_RRight := tt in _ - | RWhere Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ lev => let case_RWhere := tt in _ + | RCut Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l => let case_RCut := tt in _ + | RLeft Γ Δ Σ₁ Σ₂ Σ l => let case_RLeft := tt in _ + | RRight Γ Δ Σ₁ Σ₂ Σ l => let case_RRight := tt in _ | RVoid _ _ l => let case_RVoid := tt in _ | RBrak Γ Δ t ec succ lev => let case_RBrak := tt in _ | REsc Γ Δ t ec succ lev => let case_REsc := tt in _ @@ -888,6 +882,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. @@ -902,6 +897,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. @@ -958,59 +954,6 @@ Section HaskFlattener. Notation "!<[@]> x" := (mapOptionTree flatten_leveled_type x) (at level 1). *) - destruct case_RLet. - simpl. - destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ]. - repeat drop_simplify. - repeat take_simplify. - simpl. - - set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as Σ₁'. - set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as Σ₂'. - set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₁)) as Σ₁''. - set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as Σ₂''. - - eapply nd_comp. - eapply nd_prod; [ idtac | apply nd_id ]. - eapply boost. - apply (ga_first _ _ _ _ _ _ Σ₂'). - - eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. - apply nd_prod. - apply nd_id. - eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ACanL | idtac ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch (* okay *)]. - apply precompose. - - destruct case_RWhere. - simpl. - destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RWhere; auto | idtac ]. - repeat take_simplify. - repeat drop_simplify. - simpl. - - set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as Σ₁'. - set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as Σ₂'. - set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₃)) as Σ₃'. - set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₁)) as Σ₁''. - set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as Σ₂''. - set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₃)) as Σ₃''. - - eapply nd_comp. - eapply nd_prod; [ eapply nd_id | idtac ]. - eapply (first_nd _ _ _ _ _ _ Σ₃'). - eapply nd_comp. - eapply nd_prod; [ eapply nd_id | idtac ]. - eapply (second_nd _ _ _ _ _ _ Σ₁'). - - eapply nd_comp; [ idtac | eapply nd_rule; eapply RWhere ]. - apply nd_prod; [ idtac | apply nd_id ]. - eapply nd_comp; [ idtac | eapply precompose' ]. - apply nd_rule. - apply RArrange. - apply ALeft. - apply ACanL. - destruct case_RCut. simpl. destruct l as [|ec lev]; simpl. @@ -1022,41 +965,50 @@ Section HaskFlattener. rewrite <- IHΣ₁₂1. rewrite <- IHΣ₁₂2. reflexivity. - simpl. - repeat drop_simplify. - simpl. - repeat take_simplify. + simpl; repeat drop_simplify. + simpl; repeat take_simplify. simpl. set (drop_lev (ec :: lev) (Σ₁₂ @@@ (ec :: lev))) as x1. rewrite take_lemma'. rewrite mapOptionTree_compose. rewrite mapOptionTree_compose. rewrite mapOptionTree_compose. + rewrite mapOptionTree_compose. rewrite unlev_relev. rewrite <- mapOptionTree_compose. rewrite <- mapOptionTree_compose. + rewrite <- mapOptionTree_compose. eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ]. apply nd_prod. apply nd_id. eapply nd_comp. eapply nd_rule. eapply RArrange. + eapply ALeft. eapply ARight. unfold x1. rewrite drop_to_nothing. apply arrangeCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ₁₂)). - admit. (* OK *) - eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ACanL | idtac ]. + 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. set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as c. set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as d. + set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ)) as e. + set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ)) as f. eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. apply nd_prod. simpl. - eapply ga_first. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ]. + eapply secondify. + apply ga_first. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; eapply AExch ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuAssoc ]. simpl. apply precompose. @@ -1081,7 +1033,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. @@ -1116,7 +1072,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. @@ -1132,10 +1092,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. @@ -1206,7 +1169,31 @@ 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. @@ -1272,7 +1259,7 @@ Section HaskFlattener. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ]. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ]. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. + eapply nd_comp; [ idtac | eapply RLet ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. apply nd_prod; [ idtac | eapply boost ]. induction x.