X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProof.v;h=d9c6a7eef94758a8327913aa74aa3b2c71a4afda;hp=4cc4605d1dd0719117cb858c4dbdbfc5d688886e;hb=93ac0d63048027161f816c451a7954fb8a6470c0;hpb=fd337b235014f43000773eb0d95168d89e93a893

diff --git a/src/HaskProof.v b/src/HaskProof.v
index 4cc4605..d9c6a7e 100644
--- a/src/HaskProof.v
+++ b/src/HaskProof.v
@@ -14,7 +14,8 @@ Require Import Coq.Strings.String.
 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.
 
@@ -40,11 +41,11 @@ Record ProofCaseBranch {tc:TyCon}{Γ}{Δ}{lev}{branchtype : HaskType Γ ★}{ava
                   (vec2list (sac_types sac Γ avars))))
                 |- [weakLT' (branchtype @@ lev)]
 }.
-(*Coercion pcb_scb : ProofCaseBranch >-> StrongAltCon.*)
 Implicit Arguments ProofCaseBranch [ ].
 
 (* 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    )
@@ -66,31 +67,38 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type :=
 
 (* λ^α rules *)
 | RBrak : ∀ Γ Δ t v Σ l,                              Rule [Γ > Δ > Σ      |- [t  @@ (v::l) ]]   [Γ > Δ > Σ     |- [<[v|-t]>   @@l]]
-| REsc  : ∀ Γ Δ t v Σ l,                              Rule [Γ > Δ > Σ      |- [<[v|-t]> @@ l]]   [Γ > Δ > Σ     |- [t  @@ (v::l)  ]]
+| REsc  : ∀ Γ Δ t v Σ l,                              Rule [Γ > Δ > Σ      |- [<[v|-t]> @@ l]]   [Γ > Δ > Σ     |- [t    @@ (v::l)]]
 
 (* Part of GHC, but not explicitly in System FC *)
-| RNote   : ∀ Γ Δ Σ τ l,          Note ->             Rule  [Γ > Δ > Σ |- [τ @@ l]] [Γ > Δ > Σ |- [τ @@ l]]
-| RLit    : ∀ Γ Δ v       l,                          Rule  [                                ]   [Γ > Δ > []|- [literalType v @@ l]]
+| RNote   : ∀ Γ Δ Σ τ l,          Note ->             Rule [Γ > Δ > Σ      |- [τ        @@ l]]   [Γ > Δ > Σ     |- [τ          @@l]]
+| RLit    : ∀ Γ Δ v       l,                          Rule [                                 ]   [Γ > Δ > []|- [literalType v  @@l]]
 
 (* 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]]
-| RBindingGroup  : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ ,   Rule ([Γ > Δ > Σ₁ |- τ₁ ],,[Γ > Δ > Σ₂ |- τ₂ ])         [Γ>Δ>  Σ₁,,Σ₂  |- τ₁,,τ₂          ]
-| RApp           : ∀ Γ Δ Σ₁ Σ₂ tx te l,  Rule ([Γ>Δ> Σ₁       |- [tx--->te @@l]],,[Γ>Δ> Σ₂ |- [tx@@l]])  [Γ>Δ> Σ₁,,Σ₂ |- [te   @@l]]
-| RLet           : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l,  Rule ([Γ>Δ> Σ₁,,[σ₂@@l] |- [σ₁@@l] ],,[Γ>Δ> Σ₂ |- [σ₂@@l]])     [Γ>Δ> Σ₁,,Σ₂ |- [σ₁   @@l]]
-| REmptyGroup    : ∀ Γ Δ ,               Rule [] [Γ > Δ > [] |- [] ]
+
+| RJoin  : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ ,   Rule ([Γ > Δ > Σ₁ |- τ₁ ],,[Γ > Δ > Σ₂ |- τ₂ ])         [Γ>Δ>  Σ₁,,Σ₂  |- τ₁,,τ₂          ]
+
+| RApp           : ∀ Γ Δ Σ₁ Σ₂ tx te l,  Rule ([Γ>Δ> Σ₁ |- [tx@@l]],,[Γ>Δ> Σ₂       |- [tx--->te @@l]])  [Γ>Δ> Σ₁,,Σ₂ |- [te   @@l]]
+
+| RLet           : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l,  Rule ([Γ>Δ> Σ₂ |- [σ₂@@l]],,[Γ>Δ> Σ₁,,[σ₂@@l] |- [σ₁@@l] ])     [Γ>Δ> Σ₁,,Σ₂ |- [σ₁   @@l]]
+
+| RVoid    : ∀ Γ Δ ,               Rule [] [Γ > Δ > [] |- [] ]
+
 | RAppT   : forall Γ Δ Σ κ σ (τ:HaskType Γ κ) l,      Rule [Γ>Δ> Σ   |- [HaskTAll κ σ @@l]]      [Γ>Δ>    Σ     |- [substT σ τ @@l]]
 | RAbsT   : ∀ Γ Δ Σ κ σ   l,
   Rule [(κ::Γ)> (weakCE Δ)    >   mapOptionTree weakLT Σ |- [ HaskTApp (weakF σ) (FreshHaskTyVar _) @@ (weakL l)]]
        [Γ>Δ            >    Σ     |- [HaskTAll κ σ   @@ l]]
+
 | RAppCo  : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ l,
     Rule [Γ>Δ> Σ |- [σ₁∼∼σ₂ ⇒ σ@@l]] [Γ>Δ>    Σ     |- [σ        @@l]]
 | RAbsCo  : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) σ l,
    Rule [Γ > ((σ₁∼∼∼σ₂)::Δ)            > Σ |- [σ @@ l]]
         [Γ > Δ >                         Σ |- [σ₁∼∼σ₂⇒ σ @@l]]
+
 | RLetRec        : forall Γ Δ Σ₁ τ₁ τ₂ lev, Rule [Γ > Δ > Σ₁,,(τ₂@@@lev) |- ([τ₁],,τ₂)@@@lev ] [Γ > Δ > Σ₁ |- [τ₁@@lev] ]
 | RCase          : forall Γ Δ lev tc Σ avars tbranches
   (alts:Tree ??{ sac : @StrongAltCon tc & @ProofCaseBranch tc Γ Δ lev tbranches avars sac }),
@@ -102,6 +110,7 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type :=
 
 
 (* A rule is considered "flat" if it is neither RBrak nor REsc *)
+(* TODO: change this to (if RBrak/REsc -> False) *)
 Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop :=
 | Flat_RArrange         : ∀ Γ Δ  h c r          a ,  Rule_Flat (RArrange Γ Δ h c r a)
 | Flat_RNote            : ∀ Γ Δ Σ τ l n            ,  Rule_Flat (RNote Γ Δ Σ τ l n)
@@ -115,8 +124,8 @@ Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop :=
 | Flat_RAbsCo           : ∀ Γ   Σ κ σ  σ₁ σ₂ q1 q2   , Rule_Flat (RAbsCo Γ   Σ κ σ  σ₁ σ₂  q1 q2   )
 | Flat_RApp             : ∀ Γ Δ  Σ tx te   p     l,  Rule_Flat (RApp Γ Δ  Σ tx te   p l)
 | Flat_RLet             : ∀ Γ Δ  Σ σ₁ σ₂   p     l,  Rule_Flat (RLet Γ Δ  Σ σ₁ σ₂   p l)
-| Flat_RBindingGroup    : ∀ q a b c d e ,  Rule_Flat (RBindingGroup q a b c d e)
-| Flat_REmptyGroup      : ∀ q a                  ,  Rule_Flat (REmptyGroup q a)
+| Flat_RJoin    : ∀ q a b c d e ,  Rule_Flat (RJoin q a b c d e)
+| Flat_RVoid      : ∀ q a                  ,  Rule_Flat (RVoid q a)
 | Flat_RCase            : ∀ Σ Γ  T κlen κ θ l x  , Rule_Flat (RCase Σ Γ T κlen κ θ l x)
 | Flat_RLetRec          : ∀ Γ Δ Σ₁ τ₁ τ₂ lev,      Rule_Flat (RLetRec Γ Δ Σ₁ τ₁ τ₂ lev).
 
@@ -161,4 +170,41 @@ Lemma systemfc_all_rules_one_conclusion : forall h c1 c2 (r:Rule h (c1,,c2)), Fa
   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.