Require Import Coq.Lists.List.
Require Import HaskKinds.
Require Import HaskCoreTypes.
-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
Require Import HaskStrongTypes.
Require Import HaskWeakVars.
(* Figure 3, production $\vdash_E$, Uniform rules *)
Inductive Arrange {T} : Tree ??T -> Tree ??T -> Type :=
+| RId : forall a , Arrange a a
| RCanL : forall a , Arrange ( [],,a ) ( a )
| RCanR : forall a , Arrange ( a,,[] ) ( a )
| RuCanL : forall a , Arrange ( a ) ( [],,a )
(* SystemFC rules *)
| RVar : ∀ Γ Δ σ l, Rule [ ] [Γ>Δ> [σ@@l] |- [σ @@l]]
-| RGlobal : ∀ Γ Δ τ l, WeakExprVar -> Rule [ ] [Γ>Δ> [] |- [τ @@l]]
+| RGlobal : forall Γ Δ l (g:Global Γ) v, Rule [ ] [Γ>Δ> [] |- [g v @@l]]
| RLam : forall Γ Δ Σ (tx:HaskType Γ ★) te l, Rule [Γ>Δ> Σ,,[tx@@l]|- [te@@l] ] [Γ>Δ> Σ |- [tx--->te @@l]]
| RCast : forall Γ Δ Σ (σ₁ σ₂:HaskType Γ ★) l,
HaskCoercion Γ Δ (σ₁∼∼∼σ₂) -> Rule [Γ>Δ> Σ |- [σ₁@@l] ] [Γ>Δ> Σ |- [σ₂ @@l]]
| RJoin : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ , Rule ([Γ > Δ > Σ₁ |- τ₁ ],,[Γ > Δ > Σ₂ |- τ₂ ]) [Γ>Δ> Σ₁,,Σ₂ |- τ₁,,τ₂ ]
-| RApp : ∀ Γ Δ Σ₁ Σ₂ tx te l, Rule ([Γ>Δ> Σ₁ |- [tx--->te @@l]],,[Γ>Δ> Σ₂ |- [tx@@l]]) [Γ>Δ> Σ₁,,Σ₂ |- [te @@l]]
+(* order is important here; we want to be able to skolemize without introducing new RExch'es *)
+| RApp : ∀ Γ Δ Σ₁ Σ₂ tx te l, Rule ([Γ>Δ> Σ₁ |- [tx--->te @@l]],,[Γ>Δ> Σ₂ |- [tx@@l]]) [Γ>Δ> Σ₁,,Σ₂ |- [te @@l]]
-| RLet : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l, Rule ([Γ>Δ> Σ₂ |- [σ₂@@l]],,[Γ>Δ> Σ₁,,[σ₂@@l] |- [σ₁@@l] ]) [Γ>Δ> Σ₁,,Σ₂ |- [σ₁ @@l]]
+| RLet : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l, Rule ([Γ>Δ> Σ₁ |- [σ₁@@l]],,[Γ>Δ> [σ₁@@l],,Σ₂ |- [σ₂@@l] ]) [Γ>Δ> Σ₁,,Σ₂ |- [σ₂ @@l]]
+| RWhere : ∀ Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ l, Rule ([Γ>Δ> Σ₁,,([σ₁@@l],,Σ₃) |- [σ₂@@l] ],,[Γ>Δ> Σ₂ |- [σ₁@@l]]) [Γ>Δ> Σ₁,,(Σ₂,,Σ₃) |- [σ₂ @@l]]
| RVoid : ∀ Γ Δ , Rule [] [Γ > Δ > [] |- [] ]
Rule [Γ > ((σ₁∼∼∼σ₂)::Δ) > Σ |- [σ @@ l]]
[Γ > Δ > Σ |- [σ₁∼∼σ₂⇒ σ @@l]]
-| RLetRec : forall Γ Δ Σ₁ τ₁ τ₂ lev, Rule [Γ > Δ > Σ₁,,(τ₂@@@lev) |- ([τ₁],,τ₂)@@@lev ] [Γ > Δ > Σ₁ |- [τ₁@@lev] ]
+| RLetRec : forall Γ Δ Σ₁ τ₁ τ₂ lev, Rule [Γ > Δ > Σ₁,,(τ₂@@@lev) |- (τ₂,,[τ₁])@@@lev ] [Γ > Δ > Σ₁ |- [τ₁@@lev] ]
| RCase : forall Γ Δ lev tc Σ avars tbranches
(alts:Tree ??{ sac : @StrongAltCon tc & @ProofCaseBranch tc Γ Δ lev tbranches avars sac }),
Rule
destruct X0; destruct s; inversion e.
destruct X0; destruct s; inversion e.
destruct X0; destruct s; inversion e.
+ destruct X0; destruct s; inversion e.
Qed.
Lemma systemfc_all_rules_one_conclusion : forall h c1 c2 (r:Rule h (c1,,c2)), False.
auto.
Qed.
-
+(* "Arrange" objects are parametric in the type of the leaves of the tree *)
+Definition arrangeMap :
+ forall {T} (Σ₁ Σ₂:Tree ??T) {R} (f:T -> R),
+ Arrange Σ₁ Σ₂ ->
+ Arrange (mapOptionTree f Σ₁) (mapOptionTree f Σ₂).
+ intros.
+ induction X; simpl.
+ apply RId.
+ apply RCanL.
+ apply RCanR.
+ apply RuCanL.
+ apply RuCanR.
+ apply RAssoc.
+ apply RCossa.
+ apply RExch.
+ apply RWeak.
+ apply RCont.
+ apply RLeft; auto.
+ apply RRight; auto.
+ eapply RComp; [ apply IHX1 | apply IHX2 ].
+ Defined.
+
+(* a frequently-used Arrange *)
+Definition arrangeSwapMiddle {T} (a b c d:Tree ??T) :
+ Arrange ((a,,b),,(c,,d)) ((a,,c),,(b,,d)).
+ eapply RComp.
+ apply RCossa.
+ eapply RComp.
+ eapply RLeft.
+ eapply RComp.
+ eapply RAssoc.
+ eapply RRight.
+ apply RExch.
+ eapply RComp.
+ eapply RLeft.
+ eapply RCossa.
+ eapply RAssoc.
+ Defined.