X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskFlattener.v;h=1731aad97818d64f9789162903b55bd2b82cfbc1;hp=1bb35c6579faec1e2020809f4547df7ae2340dd5;hb=af41ffb1692ae207554342ccdc3bf73abaa75a01;hpb=1a2754d2e135ef3c5fd7ef817e1129af93b533a5 diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v index 1bb35c6..1731aad 100644 --- a/src/HaskFlattener.v +++ b/src/HaskFlattener.v @@ -288,7 +288,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 +304,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 +327,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 +348,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 +371,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 +394,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 +450,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 +537,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 +576,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 +643,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. @@ -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). @@ -815,9 +830,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 _ - | RWhere Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ lev => let case_RWhere := tt in _ - | RJoin Γ p lri m x q l => let case_RJoin := 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 _ @@ -913,12 +928,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. @@ -947,58 +956,129 @@ Section HaskFlattener. Notation "!<[@]> x" := (mapOptionTree flatten_leveled_type x) (at level 1). *) - destruct case_RLet. + destruct case_RCut. simpl. - destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ]. - repeat drop_simplify. - repeat take_simplify. + 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 (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 ]. + 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 ACanL | idtac ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch (* okay *)]. + 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_RWhere. + destruct case_RLeft. simpl. - destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RWhere; auto | idtac ]. - repeat take_simplify. + 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. - - 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 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. @@ -1142,7 +1222,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. @@ -1178,6 +1258,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 +1274,7 @@ Section HaskFlattener. intros. rewrite mapOptionTree_compose. rewrite mapOptionTree_compose. - apply flatten_proof. + apply flatten_skolemized_proof. apply skolemize_proof. apply X. Defined.