X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskFlattener.v;h=c42842a0d85e3ce12d68e0eec67554f0c6953475;hp=51fd7846ae8f38d04110282baf22938b5e837eec;hb=6a7c6977507488245ba4b8cabcf323920c25baef;hpb=91f06dc68cf5888360f1819429b10e054f94b243 diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v index 51fd784..c42842a 100644 --- a/src/HaskFlattener.v +++ b/src/HaskFlattener.v @@ -287,7 +287,7 @@ Section HaskFlattener. ND Rule [] [ Γ > Δ > [x@@lev] |- [y]@lev ] -> ND Rule [ Γ > Δ > ant |- [x]@lev ] [ Γ > Δ > ant |- [y]@lev ]. intros. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ]. eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ]. eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod. @@ -296,7 +296,7 @@ Section HaskFlattener. apply X. eapply nd_rule. eapply RArrange. - apply RuCanR. + apply AuCanR. Defined. Definition precompose Γ Δ ec : forall a x y z lev, @@ -308,7 +308,7 @@ Section HaskFlattener. eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod. apply nd_id. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ]. apply ga_comp. Defined. @@ -317,8 +317,8 @@ Section HaskFlattener. [ Γ > Δ > a,,b |- [@ga_mk _ ec y z ]@lev ] [ Γ > Δ > a,,([@ga_mk _ ec x y @@ lev],,b) |- [@ga_mk _ ec x z ]@lev ]. intros. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RLeft; eapply RExch ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCossa ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; eapply AExch ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuAssoc ]. apply precompose. Defined. @@ -338,7 +338,7 @@ Section HaskFlattener. ND Rule [] [ Γ > Δ > [] |- [@ga_mk _ ec x y ]@lev ] -> ND Rule [] [ Γ > Δ > [@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z ]@lev ]. intros. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ]. eapply nd_comp; [ idtac | eapply postcompose_ ]. apply X. Defined. @@ -347,12 +347,12 @@ Section HaskFlattener. ND Rule [ Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@lev ] [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) ]@lev ]. intros. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ]. eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ]. eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod. apply nd_id. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ]. apply ga_first. Defined. @@ -370,12 +370,12 @@ Section HaskFlattener. [ Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@lev ] [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) ]@lev ]. intros. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ]. eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ]. eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod. apply nd_id. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ]. apply ga_second. Defined. @@ -393,7 +393,7 @@ Section HaskFlattener. [Γ > Δ > Σ |- [@ga_mk Γ ec (a,,x) b ]@l ] [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x b ]@l ]. intros. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ]. eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. apply nd_prod. @@ -404,7 +404,7 @@ Section HaskFlattener. apply nd_prod. apply postcompose. apply ga_uncancell. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ]. apply precompose. Defined. @@ -430,38 +430,38 @@ Section HaskFlattener. (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) B)) (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) A)) ]@nil] with - | RId a => let case_RId := tt in ga_id _ _ _ _ _ - | RCanL a => let case_RCanL := tt in ga_uncancell _ _ _ _ _ - | RCanR a => let case_RCanR := tt in ga_uncancelr _ _ _ _ _ - | RuCanL a => let case_RuCanL := tt in ga_cancell _ _ _ _ _ - | RuCanR a => let case_RuCanR := tt in ga_cancelr _ _ _ _ _ - | RAssoc a b c => let case_RAssoc := tt in ga_assoc _ _ _ _ _ _ _ - | RCossa a b c => let case_RCossa := tt in ga_unassoc _ _ _ _ _ _ _ - | RExch a b => let case_RExch := tt in ga_swap _ _ _ _ _ _ - | RWeak a => let case_RWeak := tt in ga_drop _ _ _ _ _ - | RCont a => let case_RCont := tt in ga_copy _ _ _ _ _ - | RLeft a b c r' => let case_RLeft := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _) - | RRight a b c r' => let case_RRight := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_first _ _ _ _ _ _ _) - | RComp c b a r1 r2 => let case_RComp := tt in (fun r1' r2' => _) (flatten _ _ r1) (flatten _ _ r2) + | AId a => let case_AId := tt in ga_id _ _ _ _ _ + | ACanL a => let case_ACanL := tt in ga_uncancell _ _ _ _ _ + | ACanR a => let case_ACanR := tt in ga_uncancelr _ _ _ _ _ + | AuCanL a => let case_AuCanL := tt in ga_cancell _ _ _ _ _ + | AuCanR a => let case_AuCanR := tt in ga_cancelr _ _ _ _ _ + | AAssoc a b c => let case_AAssoc := tt in ga_assoc _ _ _ _ _ _ _ + | AuAssoc a b c => let case_AuAssoc := tt in ga_unassoc _ _ _ _ _ _ _ + | AExch a b => let case_AExch := tt in ga_swap _ _ _ _ _ _ + | AWeak a => let case_AWeak := tt in ga_drop _ _ _ _ _ + | ACont a => let case_ACont := tt in ga_copy _ _ _ _ _ + | ALeft a b c r' => let case_ALeft := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _) + | ARight a b c r' => let case_ARight := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_first _ _ _ _ _ _ _) + | AComp c b a r1 r2 => let case_AComp := tt in (fun r1' r2' => _) (flatten _ _ r1) (flatten _ _ r2) end); clear flatten; repeat take_simplify; repeat drop_simplify; intros. - destruct case_RComp. + destruct case_AComp. set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) a)) as a' in *. 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 RCanL ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ]. eapply nd_comp; [ idtac | eapply nd_rule; 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 RuCanR ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ]. + 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; [ apply nd_llecnac | idtac ]. eapply nd_prod. apply r1'. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ]. apply ga_comp. Defined. @@ -485,19 +485,19 @@ Section HaskFlattener. match r as R in Arrange A B return Arrange (mapOptionTree (flatten_leveled_type ) (drop_lev _ A)) (mapOptionTree (flatten_leveled_type ) (drop_lev _ B)) with - | RId a => let case_RId := tt in RId _ - | RCanL a => let case_RCanL := tt in RCanL _ - | RCanR a => let case_RCanR := tt in RCanR _ - | RuCanL a => let case_RuCanL := tt in RuCanL _ - | RuCanR a => let case_RuCanR := tt in RuCanR _ - | RAssoc a b c => let case_RAssoc := tt in RAssoc _ _ _ - | RCossa a b c => let case_RCossa := tt in RCossa _ _ _ - | RExch a b => let case_RExch := tt in RExch _ _ - | RWeak a => let case_RWeak := tt in RWeak _ - | RCont a => let case_RCont := tt in RCont _ - | RLeft a b c r' => let case_RLeft := tt in RLeft _ (flatten _ _ r') - | RRight a b c r' => let case_RRight := tt in RRight _ (flatten _ _ r') - | RComp a b c r1 r2 => let case_RComp := tt in RComp (flatten _ _ r1) (flatten _ _ r2) + | AId a => let case_AId := tt in AId _ + | ACanL a => let case_ACanL := tt in ACanL _ + | ACanR a => let case_ACanR := tt in ACanR _ + | AuCanL a => let case_AuCanL := tt in AuCanL _ + | AuCanR a => let case_AuCanR := tt in AuCanR _ + | AAssoc a b c => let case_AAssoc := tt in AAssoc _ _ _ + | AuAssoc a b c => let case_AuAssoc := tt in AuAssoc _ _ _ + | AExch a b => let case_AExch := tt in AExch _ _ + | AWeak a => let case_AWeak := tt in AWeak _ + | ACont a => let case_ACont := tt in ACont _ + | ALeft a b c r' => let case_ALeft := tt in ALeft _ (flatten _ _ r') + | ARight a b c r' => let case_ARight := tt in ARight _ (flatten _ _ r') + | AComp a b c r1 r2 => let case_AComp := tt in AComp (flatten _ _ r1) (flatten _ _ r2) end) ant1 ant2 r); clear flatten; repeat take_simplify; repeat drop_simplify; intros. Defined. @@ -511,19 +511,19 @@ Section HaskFlattener. apply nd_rule. apply RArrange. induction r; simpl. - apply RId. - apply RCanL. - apply RCanR. - apply RuCanL. - apply RuCanR. - apply RAssoc. - apply RCossa. - apply RExch. (* TO DO: check for all-leaf trees here *) - apply RWeak. - apply RCont. - apply RLeft; auto. - apply RRight; auto. - eapply RComp; [ apply IHr1 | apply IHr2 ]. + apply AId. + apply ACanL. + apply ACanR. + apply AuCanL. + apply AuCanR. + apply AAssoc. + apply AuAssoc. + apply AExch. (* TO DO: check for all-leaf trees here *) + apply AWeak. + apply ACont. + apply ALeft; auto. + apply ARight; auto. + eapply AComp; [ apply IHr1 | apply IHr2 ]. apply flatten_arrangement. apply r. @@ -546,11 +546,11 @@ Section HaskFlattener. eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. apply nd_prod. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ]. eapply nd_comp; [ idtac | eapply postcompose_ ]. apply ga_uncancelr. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ]. eapply nd_comp; [ idtac | eapply precompose ]. apply pfb. Defined. @@ -573,7 +573,7 @@ Section HaskFlattener. apply y. idtac. clear y q. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ]. + 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 ]. @@ -641,7 +641,7 @@ Section HaskFlattener. destruct s. simpl. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ]. + 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 ]. clear q''. @@ -649,8 +649,8 @@ Section HaskFlattener. apply nd_prod. apply nd_rule. apply RArrange. - eapply RComp; [ idtac | apply RCanR ]. - apply RLeft. + eapply AComp; [ idtac | apply ACanR ]. + apply ALeft. apply (@arrangeCancelEmptyTree _ _ _ _ e). eapply nd_comp. @@ -658,10 +658,10 @@ Section HaskFlattener. eapply (@RVar Γ Δ t nil). apply nd_rule. apply RArrange. - eapply RComp. - apply RuCanR. - apply RLeft. - apply RWeak. + eapply AComp. + apply AuCanR. + apply ALeft. + apply AWeak. (* eapply decide_tree_empty. @@ -685,15 +685,15 @@ Section HaskFlattener. simpl. apply nd_rule. apply RArrange. - apply RLeft. - apply RWeak. + apply ALeft. + apply AWeak. simpl. apply nd_rule. unfold take_lev. simpl. apply RArrange. - apply RLeft. - apply RWeak. + apply ALeft. + apply AWeak. apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported"). *) Defined. @@ -714,17 +714,17 @@ Section HaskFlattener. simpl. drop_simplify. simpl. - apply RId. + apply AId. simpl. - apply RId. - eapply RComp; [ idtac | apply RCanL ]. - eapply RComp; [ idtac | eapply RLeft; apply IHt2 ]. + apply AId. + eapply AComp; [ idtac | apply ACanL ]. + eapply AComp; [ idtac | eapply ALeft; apply IHt2 ]. Opaque drop_lev. simpl. Transparent drop_lev. idtac. drop_simplify. - apply RRight. + apply ARight. apply IHt1. Defined. @@ -735,17 +735,17 @@ Section HaskFlattener. simpl. drop_simplify. simpl. - apply RId. + apply AId. simpl. - apply RId. - eapply RComp; [ apply RuCanL | idtac ]. - eapply RComp; [ eapply RRight; apply IHt1 | idtac ]. + apply AId. + eapply AComp; [ apply AuCanL | idtac ]. + eapply AComp; [ eapply ARight; apply IHt1 | idtac ]. Opaque drop_lev. simpl. Transparent drop_lev. idtac. drop_simplify. - apply RLeft. + apply ALeft. apply IHt2. Defined. @@ -784,7 +784,22 @@ Section HaskFlattener. admit. Qed. - Definition flatten_proof : + Lemma drop_to_nothing : forall (Γ:TypeEnv) Σ (lev:HaskLevel Γ), + drop_lev lev (Σ @@@ lev) = mapTree (fun _ => None) (mapTree (fun _ => tt) Σ). + intros. + induction Σ. + destruct a; simpl. + drop_simplify. + auto. + drop_simplify. + auto. + simpl. + rewrite <- IHΣ1. + rewrite <- IHΣ2. + reflexivity. + Qed. + + Definition flatten_skolemized_proof : forall {h}{c}, ND SRule h c -> ND Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c). @@ -816,8 +831,10 @@ Section HaskFlattener. | 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 _ - | RJoin Γ p lri m x q l => let case_RJoin := 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 _ @@ -901,7 +918,7 @@ Section HaskFlattener. eapply nd_rule. eapply RArrange. simpl. - apply RCanR. + apply ACanR. apply boost. simpl. apply ga_curry. @@ -913,12 +930,6 @@ Section HaskFlattener. apply flatten_coercion; auto. apply (Prelude_error "RCast at level >0; casting inside of code brackets is currently not supported"). - destruct case_RJoin. - simpl. - destruct l; - [ apply nd_rule; apply RJoin | idtac ]; - apply (Prelude_error "RJoin at depth >0"). - destruct case_RApp. simpl. @@ -967,8 +978,8 @@ Section HaskFlattener. eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. apply nd_prod. apply nd_id. - eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply RCanL | idtac ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch (* okay *)]. + 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. @@ -997,8 +1008,132 @@ Section HaskFlattener. eapply nd_comp; [ idtac | eapply precompose' ]. apply nd_rule. apply RArrange. - apply RLeft. - apply RCanL. + apply ALeft. + apply ACanL. + + destruct case_RCut. + simpl. + destruct l as [|ec lev]; simpl. + apply nd_rule. + replace (mapOptionTree flatten_leveled_type (Σ₁₂ @@@ nil)) with (mapOptionTree flatten_type Σ₁₂ @@@ nil). + apply RCut. + induction Σ₁₂; try destruct a; auto. + simpl. + rewrite <- IHΣ₁₂1. + rewrite <- IHΣ₁₂2. + reflexivity. + 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 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 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. + + destruct case_RLeft. + simpl. + destruct l as [|ec lev]. + simpl. + replace (mapOptionTree flatten_leveled_type (Σ @@@ nil)) with (mapOptionTree flatten_type Σ @@@ nil). + apply nd_rule. + apply RLeft. + induction Σ; try destruct a; auto. + simpl. + rewrite <- IHΣ1. + rewrite <- IHΣ2. + reflexivity. + repeat drop_simplify. + rewrite drop_to_nothing. + simpl. + eapply nd_comp. + Focus 2. + eapply nd_rule. + eapply RArrange. + eapply ARight. + apply arrangeUnCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ)). + admit (* FIXME *). + idtac. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanL ]. + apply boost. + take_simplify. + simpl. + replace (take_lev (ec :: lev) (Σ @@@ (ec :: lev))) with (Σ @@@ (ec::lev)). + rewrite mapOptionTree_compose. + rewrite mapOptionTree_compose. + rewrite unlev_relev. + apply ga_second. + rewrite take_lemma'. + reflexivity. + + destruct case_RRight. + simpl. + destruct l as [|ec lev]. + simpl. + replace (mapOptionTree flatten_leveled_type (Σ @@@ nil)) with (mapOptionTree flatten_type Σ @@@ nil). + apply nd_rule. + apply RRight. + induction Σ; try destruct a; auto. + simpl. + rewrite <- IHΣ1. + rewrite <- IHΣ2. + reflexivity. + repeat drop_simplify. + rewrite drop_to_nothing. + simpl. + eapply nd_comp. + Focus 2. + eapply nd_rule. + eapply RArrange. + eapply ALeft. + apply arrangeUnCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ)). + admit (* FIXME *). + idtac. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ]. + apply boost. + take_simplify. + simpl. + replace (take_lev (ec :: lev) (Σ @@@ (ec :: lev))) with (Σ @@@ (ec::lev)). + rewrite mapOptionTree_compose. + rewrite mapOptionTree_compose. + rewrite unlev_relev. + apply ga_first. + rewrite take_lemma'. + reflexivity. destruct case_RVoid. simpl. @@ -1100,15 +1235,15 @@ Section HaskFlattener. set (mapOptionTree (flatten_type ○ unlev)(take_lev (ec :: nil) succ)) as succ_guest. set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args. unfold empty_tree. - eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply RLeft; apply tree_of_nothing | idtac ]. - eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply RCanR | idtac ]. + eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ALeft; apply tree_of_nothing | idtac ]. + eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ACanR | idtac ]. refine (ga_unkappa Γ Δ (v2t ec) nil _ _ _ _ ;; _). eapply nd_comp; [ idtac | eapply arrange_brak ]. unfold succ_host. unfold succ_guest. eapply nd_rule. eapply RArrange. - apply RExch. + apply AExch. apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported"). destruct case_SEsc. @@ -1122,8 +1257,8 @@ Section HaskFlattener. take_simplify. drop_simplify. simpl. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RLeft; apply tree_of_nothing' ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; apply tree_of_nothing' ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ]. simpl. rewrite take_lemma'. rewrite unlev_relev. @@ -1139,15 +1274,15 @@ Section HaskFlattener. set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host. set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanR ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanR ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ]. + 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; [ apply nd_llecnac | idtac ]. apply nd_prod; [ idtac | eapply boost ]. induction x. apply ga_id. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ]. simpl. apply ga_join. apply IHx1. @@ -1178,6 +1313,13 @@ Section HaskFlattener. apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported"). Defined. + Definition flatten_proof : + forall {h}{c}, + ND Rule h c -> + ND Rule h c. + apply (Prelude_error "sorry, non-skolemized flattening isn't implemented"). + Defined. + Definition skolemize_and_flatten_proof : forall {h}{c}, ND Rule h c -> @@ -1187,7 +1329,7 @@ Section HaskFlattener. intros. rewrite mapOptionTree_compose. rewrite mapOptionTree_compose. - apply flatten_proof. + apply flatten_skolemized_proof. apply skolemize_proof. apply X. Defined.