X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FHaskProof.v;h=ef669eee0abc1dd87000d2035893700e283c9e15;hb=bb960df7c29c851ca9d13f2d0c8f351ac24045ca;hp=046e28e7c55d2420ebd45baac72cc35d488c2380;hpb=539d675a181f178e24c15b2a6ad3c990492eed79;p=coq-hetmet.git

diff --git a/src/HaskProof.v b/src/HaskProof.v
index 046e28e..ef669ee 100644
--- a/src/HaskProof.v
+++ b/src/HaskProof.v
@@ -50,15 +50,14 @@ Definition UJudg2judg {Γ}{Δ}(ej:@UJudg Γ Δ) : Judg :=
   Coercion UJudg2judg : UJudg >-> Judg.
 
 (* information needed to define a case branch in a HaskProof *)
-Record ProofCaseBranch {tc:TyCon}{Γ}{Δ}{lev}{branchtype : HaskType Γ ★}{avars} :=
-{ pcb_scb            :  @StrongAltCon tc
-; pcb_freevars       :  Tree ??(LeveledHaskType Γ ★)
-; pcb_judg           := sac_Γ pcb_scb Γ > sac_Δ pcb_scb Γ avars (map weakCK' Δ)
+Record ProofCaseBranch {tc:TyCon}{Γ}{Δ}{lev}{branchtype : HaskType Γ ★}{avars}{sac:@StrongAltCon tc} :=
+{ pcb_freevars       :  Tree ??(LeveledHaskType Γ ★)
+; pcb_judg           := sac_Γ sac Γ > sac_Δ sac Γ avars (map weakCK' Δ)
                 > (mapOptionTree weakLT' pcb_freevars),,(unleaves (map (fun t => t@@weakL' lev)
-                  (vec2list (sac_types pcb_scb Γ avars))))
+                  (vec2list (sac_types sac Γ avars))))
                 |- [weakLT' (branchtype @@ lev)]
 }.
-Coercion pcb_scb : ProofCaseBranch >-> StrongAltCon.
+(*Coercion pcb_scb : ProofCaseBranch >-> StrongAltCon.*)
 Implicit Arguments ProofCaseBranch [ ].
 
 (* Figure 3, production $\vdash_E$, Uniform rules *)
@@ -111,11 +110,11 @@ HaskCoercion Γ Δ (σ₁∼∼∼σ₂) ->
         [Γ > Δ >                         Σ |- [σ₁∼∼σ₂⇒ σ @@l]]
 | RLetRec        : forall Γ Δ Σ₁ τ₁ τ₂ lev, Rule [Γ > Δ > Σ₁,,(τ₂@@@lev) |- ([τ₁],,τ₂)@@@lev ] [Γ > Δ > Σ₁ |- [τ₁@@lev] ]
 | RCase          : forall Γ Δ lev tc Σ avars tbranches
-  (alts:Tree ??(@ProofCaseBranch tc Γ Δ lev tbranches avars)),
+  (alts:Tree ??{ sac : @StrongAltCon tc & @ProofCaseBranch tc Γ Δ lev tbranches avars sac }),
                    Rule
-                       ((mapOptionTree pcb_judg alts),,
+                       ((mapOptionTree (fun x => pcb_judg (projT2 x)) alts),,
                         [Γ > Δ >                                              Σ |- [ caseType tc avars @@ lev ] ])
-                        [Γ > Δ > (mapOptionTreeAndFlatten pcb_freevars alts),,Σ |- [ tbranches         @@ lev ] ]
+                        [Γ > Δ > (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x)) alts),,Σ |- [ tbranches         @@ lev ] ]
 .
 Coercion RURule : URule >-> Rule.
 
@@ -134,7 +133,8 @@ Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop :=
 | 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_RCase            : ∀ Σ Γ  T κlen κ θ l x  , Rule_Flat (RCase Σ Γ T κlen κ θ l x).
+| Flat_RCase            : ∀ Σ Γ  T κlen κ θ l x  , Rule_Flat (RCase Σ Γ T κlen κ θ l x)
+| Flat_RLetRec          : ∀ Γ Δ Σ₁ τ₁ τ₂ lev,      Rule_Flat (RLetRec Γ Δ Σ₁ τ₁ τ₂ lev).
 
 (* given a proof that uses only uniform rules, we can produce a general proof *)
 Definition UND_to_ND Γ Δ h c : ND (@URule Γ Δ) h c -> ND Rule (mapOptionTree UJudg2judg h) (mapOptionTree UJudg2judg c)