X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskSkolemizer.v;h=435b687968922e3066467e7a89b2ddba38b51785;hp=bb4dc924c14fb66be24701290e8f3af0cedabc48;hb=af41ffb1692ae207554342ccdc3bf73abaa75a01;hpb=57e387249da84dac0f1c5a9411e3900831ce2d81 diff --git a/src/HaskSkolemizer.v b/src/HaskSkolemizer.v index bb4dc92..435b687 100644 --- a/src/HaskSkolemizer.v +++ b/src/HaskSkolemizer.v @@ -9,6 +9,7 @@ Generalizable All Variables. Require Import Preamble. Require Import General. Require Import NaturalDeduction. +Require Import NaturalDeductionContext. Require Import Coq.Strings.String. Require Import Coq.Lists.List. @@ -124,14 +125,14 @@ Section HaskSkolemizer. destruct (eqd_dec ([tx],,take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))). rewrite <- e. simpl. - apply RId. + apply AId. unfold take_arg_types_as_tree. Opaque take_arg_types_as_tree. simpl. destruct (count_arg_types (te (fun _ : Kind => unit) (ite_unit Γ))). simpl. replace (tx) with (fun (TV : Kind → Type) (ite : InstantiatedTypeEnv TV Γ) => tx TV ite). - apply RCanR. + apply ACanR. apply phoas_extensionality. reflexivity. apply (Prelude_error "should not be possible"). @@ -145,14 +146,14 @@ Section HaskSkolemizer. destruct (eqd_dec ([tx],,take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))). rewrite <- e. simpl. - apply RId. + apply AId. unfold take_arg_types_as_tree. Opaque take_arg_types_as_tree. simpl. destruct (count_arg_types (te (fun _ : Kind => unit) (ite_unit Γ))). simpl. replace (tx) with (fun (TV : Kind → Type) (ite : InstantiatedTypeEnv TV Γ) => tx TV ite). - apply RuCanR. + apply AuCanR. apply phoas_extensionality. reflexivity. apply (Prelude_error "should not be possible"). @@ -230,9 +231,9 @@ Section HaskSkolemizer. | 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 _ @@ -250,7 +251,7 @@ Section HaskSkolemizer. apply nd_rule. apply SFlat. apply RArrange. - apply RRight. + apply ARight. apply d. destruct case_RBrak. @@ -287,7 +288,7 @@ Section HaskSkolemizer. rewrite H. rewrite H0. simpl. - eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; apply RuCanL ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; apply AuCanL ]. apply nd_rule. apply SFlat. apply RLit. @@ -302,7 +303,7 @@ Section HaskSkolemizer. rewrite H. rewrite H0. simpl. - eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RuCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AuCanR ]. apply nd_rule. apply SFlat. apply RVar. @@ -317,7 +318,7 @@ Section HaskSkolemizer. rewrite H. rewrite H0. simpl. - eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RuCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AuCanR ]. apply nd_rule. apply SFlat. apply RGlobal. @@ -333,9 +334,9 @@ Section HaskSkolemizer. apply nd_rule. apply SFlat. apply RArrange. - eapply RComp. - eapply RCossa. - eapply RLeft. + eapply AComp. + eapply AuAssoc. + eapply ALeft. apply take_arrange. destruct case_RCast. @@ -347,14 +348,6 @@ Section HaskSkolemizer. apply γ. apply (Prelude_error "found RCast at level >0"). - destruct case_RJoin. - simpl. - destruct l. - apply nd_rule. - apply SFlat. - apply RJoin. - apply (Prelude_error "found RJoin at level >0"). - destruct case_RApp. simpl. destruct lev. @@ -369,64 +362,97 @@ Section HaskSkolemizer. rewrite H0. simpl. eapply nd_comp. - eapply nd_prod; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RCanR ]. + eapply nd_prod; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR ]. eapply nd_rule. eapply SFlat. eapply RArrange. - eapply RLeft. + eapply ALeft. eapply take_unarrange. - eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ]. - eapply nd_rule; eapply SFlat; apply RWhere. - - destruct case_RLet. - simpl. - destruct lev. - apply nd_rule. - apply SFlat. - apply RLet. - set (check_hof σ₁) as hof_tx. - destruct hof_tx; [ apply (Prelude_error "attempt to let-bind a higher-order function at depth>0") | idtac ]. - destruct a. - rewrite H. - rewrite H0. - + eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AAssoc ]. + eapply nd_comp; [ apply nd_exch | idtac ]. + eapply nd_rule; eapply SFlat; eapply RCut. + + destruct case_RCut. + simpl; destruct l; [ apply nd_rule; apply SFlat; apply RCut | idtac ]. + set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₃) as Σ₃''. + set (mapOptionTree drop_arg_types_as_tree Σ₃) as Σ₃'''. + set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₁₂) as Σ₁₂''. + set (mapOptionTree drop_arg_types_as_tree Σ₁₂) as Σ₁₂'''. + destruct (decide_tree_empty (Σ₁₂'' @@@ (h::l))); + [ idtac | apply (Prelude_error "used RCut on a variable with function type") ]. + destruct (eqd_dec Σ₁₂ Σ₁₂'''); [ idtac | apply (Prelude_error "used RCut on a variable with function type") ]. + rewrite <- e. + clear e. + destruct s. eapply nd_comp. - eapply nd_prod; [ eapply nd_rule; eapply SFlat; eapply RArrange; eapply RCanR | eapply nd_id ]. - - set (@RLet Γ Δ Σ₁ (Σ₂,,(take_arg_types_as_tree σ₂ @@@ (h::lev))) σ₁ (drop_arg_types_as_tree σ₂) (h::lev)) as q. - eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply q ]. - apply nd_prod. + eapply nd_prod. + eapply nd_rule. + eapply SFlat. + eapply RArrange. + eapply AComp. + eapply ALeft. + eapply arrangeCancelEmptyTree with (q:=x). + apply e. + apply ACanR. apply nd_id. - apply nd_rule. + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AAssoc ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RCut ]. + apply nd_prod. + apply nd_id. + eapply nd_rule. eapply SFlat. eapply RArrange. - eapply RCossa. - - destruct case_RWhere. - simpl. - destruct lev. + eapply AComp. + eapply AuAssoc. + eapply ALeft. + eapply AComp. + eapply AuAssoc. + eapply ALeft. + eapply AId. + + destruct case_RLeft. + simpl; destruct l; [ apply nd_rule; apply SFlat; apply RLeft | idtac ]. + set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₂) as Σ₂'. + set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ) as Σ'. + set (mapOptionTree drop_arg_types_as_tree Σ₂) as Σ₂''. + set (mapOptionTree drop_arg_types_as_tree Σ) as Σ''. + destruct (decide_tree_empty (Σ' @@@ (h::l))); + [ idtac | apply (Prelude_error "used RLeft on a variable with function type") ]. + destruct (eqd_dec Σ Σ''); [ idtac | apply (Prelude_error "used RLeft on a variable with function type") ]. + rewrite <- e. + clear Σ'' e. + destruct s. + set (arrangeUnCancelEmptyTree _ _ e) as q. + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply ARight; eapply q ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AuCanL; eapply q ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ]. apply nd_rule. - apply SFlat. - apply RWhere. - set (check_hof σ₁) as hof_tx. - destruct hof_tx; [ apply (Prelude_error "attempt to let-bind a higher-order function at depth>0") | idtac ]. - destruct a. - rewrite H. - rewrite H0. - - eapply nd_comp. - eapply nd_prod; [ apply nd_id | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RCanR ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RAssoc ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RLeft; eapply RAssoc ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RWhere ]. - apply nd_prod; [ idtac | eapply nd_id ]. - eapply nd_rule; apply SFlat; eapply RArrange. - eapply RComp. - eapply RCossa. - apply RLeft. - eapply RCossa. + eapply SFlat. + eapply RLeft. + + destruct case_RRight. + simpl; destruct l; [ apply nd_rule; apply SFlat; apply RRight | idtac ]. + set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₂) as Σ₂'. + set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ) as Σ'. + set (mapOptionTree drop_arg_types_as_tree Σ₂) as Σ₂''. + set (mapOptionTree drop_arg_types_as_tree Σ) as Σ''. + destruct (decide_tree_empty (Σ' @@@ (h::l))); + [ idtac | apply (Prelude_error "used RRight on a variable with function type") ]. + destruct (eqd_dec Σ Σ''); [ idtac | apply (Prelude_error "used RRight on a variable with function type") ]. + rewrite <- e. + clear Σ'' e. + destruct s. + set (arrangeUnCancelEmptyTree _ _ e) as q. + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply ALeft; eapply q ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AuCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AExch ]. (* yuck *) + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AuAssoc ]. + eapply nd_rule. + eapply SFlat. + apply RRight. destruct case_RVoid. simpl. @@ -434,7 +460,7 @@ Section HaskSkolemizer. apply nd_rule. apply SFlat. apply RVoid. - eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RuCanL ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AuCanL ]. apply nd_rule. apply SFlat. apply RVoid.