make StrongAlt a parameter rather than field in StrongCaseBranch and ProofCaseBranch

diff --git a/src/Extraction.v b/src/Extraction.v
index d1c84e4..c23d1c5 100644 (file)
--- a/src/Extraction.v
+++ b/src/Extraction.v
@@ -25,10 +25,10 @@ Require Import HaskProof.
 Require Import HaskCoreToWeak.
 Require Import HaskWeakToStrong.
 Require Import HaskStrongToProof.
-Require Import HaskProofToStrong.
 Require Import HaskProofToLatex.
 Require Import HaskStrongToWeak.
 Require Import HaskWeakToCore.
+Require Import HaskProofToStrong.
 
 Open Scope string_scope.
 Extraction Language Haskell.

diff --git a/src/General.v b/src/General.v
index 4e73755..2a1a398 100644 (file)
--- a/src/General.v
+++ b/src/General.v
@@ -893,7 +893,7 @@ Lemma unleaves_injective : forall T (t1 t2:list T), unleaves t1 = unleaves t2 ->
 
 Lemma fst_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@fst _ _) (vec_zip v1 v2) = v1.
   admit.
-  Qed.
+  Defined.
 
 Lemma snd_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@snd _ _) (vec_zip v1 v2) = v2.
   admit.

diff --git a/src/HaskProof.v b/src/HaskProof.v
index 046e28e..55b0b03 100644 (file)
--- 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.
 

diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v
index 6f75235..f907514 100644 (file)
--- a/src/HaskProofToStrong.v
+++ b/src/HaskProofToStrong.v
@@ -125,6 +125,14 @@ Section HaskProofToStrong.
     reflexivity.
     Qed.
     
+  Lemma fresh_lemma'' Γ 
+    : forall types ξ lev, 
+    FreshM { varstypes : _
+      |  mapOptionTree (update_ξ(Γ:=Γ)   ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev)
+      /\ distinct (leaves (mapOptionTree (@fst _ _) varstypes)) }.
+  admit.
+  Defined.
+
   Lemma fresh_lemma' Γ 
     : forall types vars Σ ξ lev, Σ = mapOptionTree ξ vars ->
     FreshM { varstypes : _
@@ -415,72 +423,88 @@ Section HaskProofToStrong.
       apply IHvarstypes2; inversion X; auto.
     Defined.
 
-  Definition case_helper tc Γ Δ lev tbranches avars ξ (Σ:Tree ??VV) :
-    forall pcb : ProofCaseBranch tc Γ Δ lev tbranches avars,
-    judg2exprType (pcb_judg pcb) ->
-    (pcb_freevars pcb) = mapOptionTree ξ Σ ->
-    FreshM
-    {scb : StrongCaseBranchWithVVs VV eqdec_vv tc avars &
-    Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars (weakCK'' Δ)) 
-    (scbwv_ξ scb ξ lev) (weakLT' (tbranches @@  lev))}.
+  Definition unindex_tree {V}{F} : forall {t:Tree ??V}, ITree V F t -> Tree ??{ v:V & F v }.
+    refine (fix rec t it := match it as IT return Tree ??{ v:V & F v } with
+      | INone => T_Leaf None
+      | ILeaf x y => T_Leaf (Some _)
+      | IBranch _ _ b1 b2 => (rec _ b1),,(rec _ b2)
+            end).
+    exists x; auto.
+    Defined.
 
-    intros.
+  Definition fix_indexing X (F:X->Type)(J:X->Type)(t:Tree ??{ x:X & F x })
+    :  ITree { x:X & F x } (fun x => J (projT1 x))                                t
+    -> ITree X             (fun x:X => J x)   (mapOptionTree (@projT1 _ _) t).
+    intro it.
+    induction it; simpl in *.
+    apply INone.
+    apply ILeaf.
+    apply f.
+    simpl; apply IBranch; auto.
+    Defined.
+
+  Definition fix2 {X}{F} : Tree ??{ x:X & FreshM (F x) } -> Tree ??(FreshM { x:X & F x }).
+    refine (fix rec t := match t with
+      | T_Leaf None => T_Leaf None
+      | T_Leaf (Some x) => T_Leaf (Some _)
+      | T_Branch b1 b2 => T_Branch (rec b1) (rec b2)
+            end).
+    destruct x as [x fx].
+    refine (bind fx' = fx ; return _).
+    apply FreshMon.
+    exists x.
+    apply fx'.
+    Defined.
+  
+  Definition case_helper tc Γ Δ lev tbranches avars ξ :
+    forall pcb:{sac : StrongAltCon & ProofCaseBranch tc Γ Δ lev tbranches avars sac},
+     prod (judg2exprType (pcb_judg (projT2 pcb))) {vars' : Tree ??VV & pcb_freevars (projT2 pcb) = mapOptionTree ξ vars'} ->
+     ((fun sac => FreshM
+       { scb : StrongCaseBranchWithVVs VV eqdec_vv tc avars sac
+         & Expr (sac_Γ sac Γ) (sac_Δ sac Γ avars (weakCK'' Δ)) (scbwv_ξ scb ξ lev) (weakLT' (tbranches @@  lev)) }) (projT1 pcb)).
+    intro pcb.
+    intro X.
     simpl in X.
-    destruct pcb.
+    simpl.
+    destruct pcb as [sac pcb].
     simpl in *.
-    set (sac_types pcb_scb _ avars) as boundvars.
-    refine (fresh_lemma' _ (unleaves (vec2list boundvars)) Σ (mapOptionTree weakLT' pcb_freevars) (weakLT' ○ ξ) (weakL' lev) _
-      >>>= fun ξvars => _). apply FreshMon.
-    rewrite H.
-    rewrite <- mapOptionTree_compose.
-    reflexivity.
-      destruct ξvars as [ exprvars [pf1 [pf2 pfdistinct]]].
-      set (list2vec (leaves (mapOptionTree (@fst _ _) exprvars))) as exprvars'. 
-
-   assert (distinct (vec2list exprvars')) as pfdistinct'.
-     unfold exprvars'.
-     rewrite vec2list_list2vec.
-     apply pfdistinct.
-
-      assert (sac_numExprVars pcb_scb = Datatypes.length (leaves (mapOptionTree (@fst _ _) exprvars))) as H'.
-        rewrite <- mapOptionTree_compose in pf2.
-        simpl in pf2.
-        rewrite mapleaves.
-        rewrite <- map_preserves_length.
-        rewrite map_preserves_length with (f:=
-          (@update_ξ VV eqdec_vv (@sac_Γ tc pcb_scb Γ)
-            (@weakLT' Γ (@vec2list (@sac_numExTyVars tc pcb_scb) Kind (@sac_ekinds tc pcb_scb)) ★ ○ ξ)
-            (@weakL'  Γ (@vec2list (@sac_numExTyVars tc pcb_scb) Kind (@sac_ekinds tc pcb_scb)) lev)
-            (@leaves (VV * HaskType (@sac_Γ tc pcb_scb Γ) ★) exprvars) ○ @fst VV (HaskType (@sac_Γ tc pcb_scb Γ) ★))).
-        rewrite <- mapleaves.
-        rewrite pf2.       
-        rewrite <- mapleaves'.
-        rewrite leaves_unleaves.
-        rewrite vec2list_map_list2vec.
-        rewrite vec2list_len.
-        reflexivity.
-
-        clear pfdistinct'.
-     rewrite <- H' in exprvars'.
-       clear H'.
-   assert (distinct (vec2list exprvars')) as pfdistinct'.
-     admit.
-
-   set (@Build_StrongCaseBranchWithVVs VV _ tc _ avars pcb_scb exprvars' pfdistinct') as scb.
-      set (scbwv_ξ scb ξ lev) as ξ'.
-      refine (X ξ' (Σ,,(unleaves (vec2list exprvars'))) _ >>>= fun X' => return _). apply FreshMon.
+
+    destruct X.
+    destruct s as [vars vars_pf].
+
+    refine (bind localvars = fresh_lemma' _ (unleaves  (vec2list (sac_types sac _ avars))) vars 
+      (mapOptionTree weakLT' (pcb_freevars pcb)) (weakLT' ○ ξ) (weakL' lev) _  ; _).
+      apply FreshMon.
+      rewrite vars_pf.
+      rewrite <- mapOptionTree_compose.
+      reflexivity.
+      destruct localvars as [localvars [localvars_pf1 [localvars_pf2 localvars_dist ]]].
+      set (mapOptionTree (@fst _ _) localvars) as localvars'.
+
+    set (list2vec (leaves localvars')) as localvars''.
+    cut (length (leaves localvars') = sac_numExprVars sac). intro H''.
+      rewrite H'' in localvars''.
+    cut (distinct (vec2list localvars'')). intro H'''.
+    set (@Build_StrongCaseBranchWithVVs _ _ _ _ avars sac localvars'' H''') as scb.
+
+    refine (bind q = (f (scbwv_ξ scb ξ lev) (vars,,(unleaves (vec2list (scbwv_exprvars scb)))) _) ; return _).
+      apply FreshMon.
       simpl.
-      unfold ξ'.
       unfold scbwv_ξ.
+      rewrite vars_pf.
+      rewrite <- mapOptionTree_compose.
+      clear localvars_pf1.
       simpl.
-      admit.
-
-    apply ileaf in X'.
-      simpl in X'.
-      exists scb.
-      unfold weakCK''.
-      unfold ξ' in X'.
-      apply X'.
+      rewrite mapleaves'.
+
+    admit.
+
+    exists scb.
+    apply ileaf in q.
+    apply q.
+
+    admit.
+    admit.
     Defined.
 
   Fixpoint treeM {T}(t:Tree ??(FreshM T)) : FreshM (Tree ??T) :=
@@ -490,18 +514,46 @@ Section HaskProofToStrong.
       | T_Branch b1 b2  => bind b1' = treeM b1 ; bind b2' = treeM b2 ; return (b1',,b2')
     end.
 
-  Lemma itree_mapOptionTree : forall T T' F (f:T->T') t,
-    ITree _ F (mapOptionTree f t) ->
-    ITree _ (F ○ f) t.
+  Definition gather_branch_variables
+    Γ Δ (ξ:VV -> LeveledHaskType Γ ★) tc avars tbranches lev (alts:Tree ?? {sac : StrongAltCon &
+                ProofCaseBranch tc Γ Δ lev tbranches avars sac})
+    :
+    forall vars,
+    mapOptionTreeAndFlatten (fun x => pcb_freevars(Γ:=Γ) (projT2 x)) alts = mapOptionTree ξ vars
+    -> ITree Judg judg2exprType (mapOptionTree (fun x => pcb_judg (projT2 x)) alts)
+    -> ITree _ (fun q => prod (judg2exprType (pcb_judg (projT2 q))) 
+      { vars' : _ & pcb_freevars (projT2 q) = mapOptionTree ξ vars' })
+  alts.
+    induction alts;
+    intro vars;
+    intro pf;
+    intro source.
+    destruct a; [ idtac | apply INone ].
+    simpl in *.
+    apply ileaf in source.
+    apply ILeaf.
+    destruct s as [sac pcb].
+    simpl in *.
+    split.
     intros.
-    induction t; try destruct a; simpl in *.
-      apply ILeaf.
-      inversion X; auto.
-      apply INone.
-      apply IBranch.
-        apply IHt1; inversion X; auto.
-        apply IHt2; inversion X; auto.
-        Defined.
+    eapply source.
+    apply H.
+    clear source.
+
+    exists vars.
+    auto.
+
+    simpl in pf.
+    destruct vars; try destruct o; simpl in pf; inversion pf.
+    simpl in source.
+    inversion source.
+    subst.
+    apply IBranch.
+    apply (IHalts1 vars1 H0 X); auto.
+    apply (IHalts2 vars2 H1 X0); auto.
+
+    Defined.
+
 
   Definition rule2expr : forall h j (r:Rule h j), ITree _ judg2exprType h -> ITree _ judg2exprType j.
 
@@ -729,27 +781,33 @@ Section HaskProofToStrong.
     subst.
     apply ileaf in X0.
     simpl in X0.
-    set (mapOptionTreeAndFlatten pcb_freevars alts) as Σalts in *.
-    refine (bind ξvars = fresh_lemma' _ (mapOptionTree unlev (Σalts,,Σ)) _ _ _ lev H ; _).
-      apply FreshMon.
-      destruct vars; try destruct o; inversion H; clear H.
-      rename vars1 into varsalts.
-      rename vars2 into varsΣ.
 
-    refine ( _ >>>= fun Y => X0 ξ varsΣ _ >>>= fun X => return ILeaf _ (@ECase _ _ _ _ _ _ _ _ _ (ileaf X) Y)); auto.
+    (* body_freevars and alts_freevars are the types of variables in the body and alternatives (respectively) which are free
+     * from the viewpoint just outside the case block -- i.e. not bound by any of the branches *)
+    rename Σ into body_freevars_types.
+    rename vars into all_freevars.
+    rename X0 into body_expr.
+    rename X  into alts_exprs.
+
+    destruct all_freevars; try destruct o; inversion H.
+    rename all_freevars2 into body_freevars.
+    rename all_freevars1 into alts_freevars.
+
+    set (gather_branch_variables _ _ _ _ _ _ _ _ _ H1 alts_exprs) as q.
+    set (itmap (fun pcb alt_expr => case_helper tc Γ Δ lev tbranches avars ξ pcb alt_expr) q) as alts_exprs'.
+    apply fix_indexing in alts_exprs'.
+    simpl in alts_exprs'.
+    apply unindex_tree in alts_exprs'.
+    simpl in alts_exprs'.
+    apply fix2 in alts_exprs'.
+    apply treeM in alts_exprs'.
+
+    refine ( alts_exprs' >>>= fun Y =>
+      body_expr ξ _ _
+      >>>= fun X => return ILeaf _ (@ECase _ _ _ _ _ _ _ _ _ (ileaf X) Y)); auto.
       apply FreshMon.
-      destruct ξvars as [varstypes [pf1 pf2]].
-
-      apply treeM.
-      apply itree_mapOptionTree in X.
-      refine (itree_to_tree (itmap _ X)).
-      intros.
-      eapply case_helper.
-      apply X1.
-      instantiate (1:=varsΣ).
-      rewrite <- H2.
-      admit.
       apply FreshMon.
+      apply H2.
     Defined.
 
   Definition closed2expr : forall c (pn:@ClosedND _ Rule c), ITree _ judg2exprType c.

diff --git a/src/HaskStrong.v b/src/HaskStrong.v
index 151e8d2..1f4d03b 100644 (file)
--- a/src/HaskStrong.v
+++ b/src/HaskStrong.v
@@ -20,15 +20,14 @@ Section HaskStrong.
 
   (* a StrongCaseBranchWithVVs contains all the data found in a case branch except the expression itself *)
 
-  Record StrongCaseBranchWithVVs {tc:TyCon}{Γ}{atypes:IList _ (HaskType Γ) (tyConKind tc)} :=
-  { scbwv_sac               :  @StrongAltCon tc
-  ; scbwv_exprvars          :  vec VV (sac_numExprVars scbwv_sac)
+  Record StrongCaseBranchWithVVs {tc:TyCon}{Γ}{atypes:IList _ (HaskType Γ) (tyConKind tc)}{sac:@StrongAltCon tc} :=
+  { scbwv_exprvars          :  vec VV (sac_numExprVars sac)
   ; scbwv_exprvars_distinct :  distinct (vec2list scbwv_exprvars)
-  ; scbwv_varstypes         := vec_zip scbwv_exprvars (sac_types scbwv_sac Γ atypes)
+  ; scbwv_varstypes         := vec_zip scbwv_exprvars (sac_types sac Γ atypes)
   ; scbwv_ξ                 := fun ξ lev =>  update_ξ (weakLT'○ξ) (weakL' lev) (vec2list scbwv_varstypes)
   }.
   Implicit Arguments StrongCaseBranchWithVVs [[Γ]].
-  Coercion scbwv_sac : StrongCaseBranchWithVVs >-> StrongAltCon.
+  (*Coercion scbwv_sac : StrongCaseBranchWithVVs >-> StrongAltCon.*)
 
   Inductive Expr : forall Γ (Δ:CoercionEnv Γ), (VV -> LeveledHaskType Γ ★) -> LeveledHaskType Γ ★ -> Type :=
 
@@ -54,11 +53,12 @@ Section HaskStrong.
     Expr (κ::Γ) (weakCE Δ) (weakLT○ξ) (HaskTApp (weakF σ) (FreshHaskTyVar _)@@(weakL l))-> Expr Γ Δ ξ (HaskTAll κ σ @@ l)
   | ECase    : forall Γ Δ ξ l tc tbranches atypes,
                Expr Γ Δ ξ (caseType tc atypes @@ l) ->
-               Tree ??{ scb : StrongCaseBranchWithVVs tc atypes
-                            & Expr (sac_Γ scb Γ)
-                                   (sac_Δ scb Γ atypes (weakCK'' Δ))
+               Tree ??{ sac : _
+                    & { scb : StrongCaseBranchWithVVs tc atypes sac
+                    &         Expr (sac_Γ sac Γ)
+                                   (sac_Δ sac Γ atypes (weakCK'' Δ))
                                    (scbwv_ξ scb ξ l)
-                                   (weakLT' (tbranches@@l)) } ->
+                                   (weakLT' (tbranches@@l)) } } ->
                Expr Γ Δ ξ (tbranches @@ l)
 
   | ELetRec  : ∀ Γ Δ ξ l τ vars,

diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v
index fa7dcae..79e16cd 100644 (file)
--- a/src/HaskStrongToProof.v
+++ b/src/HaskStrongToProof.v
@@ -348,15 +348,15 @@ Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ?
    in     stripOutVars (leaves (mapOptionTree (@fst _ _ ) vars)) all_contexts
   | ECase    Γ Δ ξ l tc tbranches atypes e' alts =>
     ((fix varsfromalts (alts:
-               Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes
-                            & Expr (sac_Γ scb Γ)
-                                   (sac_Δ scb Γ atypes (weakCK'' Δ))
+               Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
+                            & Expr (sac_Γ sac Γ)
+                                   (sac_Δ sac Γ atypes (weakCK'' Δ))
                                    (scbwv_ξ scb ξ l)
-                                   (weakLT' (tbranches@@l)) }
+                                   (weakLT' (tbranches@@l)) } }
       ): Tree ??VV :=
       match alts with
         | T_Leaf None     => []
-        | T_Leaf (Some h) => stripOutVars (vec2list (scbwv_exprvars (projT1 h))) (expr2antecedent (projT2 h))
+        | T_Leaf (Some h) => stripOutVars (vec2list (scbwv_exprvars (projT1 (projT2 h)))) (expr2antecedent (projT2 (projT2 h)))
         | T_Branch b1 b2  => (varsfromalts b1),,(varsfromalts b2)
       end) alts),,(expr2antecedent e')
 end
@@ -368,15 +368,18 @@ match elrb with
 end.
 
 Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes}
-  (alt: { scb : StrongCaseBranchWithVVs _ _ tc atypes
-                            & Expr (sac_Γ scb Γ)
-                                   (sac_Δ scb Γ atypes (weakCK'' Δ))
+(alt : { sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
+                            & Expr (sac_Γ sac Γ)
+                                   (sac_Δ sac Γ atypes (weakCK'' Δ))
                                    (scbwv_ξ scb ξ l)
-                                   (weakLT' (tbranches@@l)) })
-  : ProofCaseBranch tc Γ Δ l tbranches atypes.
+                                   (weakLT' (tbranches@@l)) } })
+  : { sac : _ & ProofCaseBranch tc Γ Δ l tbranches atypes sac }.
+  destruct alt.
+  exists x.
   exact
-    {| pcb_scb := projT1 alt
-     ; pcb_freevars := mapOptionTree ξ (stripOutVars (vec2list (scbwv_exprvars (projT1 alt))) (expr2antecedent (projT2 alt)))
+    {| pcb_freevars := mapOptionTree ξ
+      (stripOutVars (vec2list (scbwv_exprvars (projT1 s)))
+        (expr2antecedent (projT2 s)))
      |}.
      Defined.
 
@@ -693,16 +696,16 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree  :
     apply disti.
     Defined.
 
-Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _} :
-  forall scb:StrongCaseBranchWithVVs _ _ tc atypes,
+Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _}{sac} :
+  forall scb:StrongCaseBranchWithVVs _ _ tc atypes sac,
     forall l ξ,
       vec2list (vec_map (scbwv_ξ scb ξ l) (scbwv_exprvars scb)) =
-      vec2list (vec_map (fun t => t @@ weakL' l) (sac_types (scbwv_sac scb) _ atypes)).
+      vec2list (vec_map (fun t => t @@ weakL' l) (sac_types sac _ atypes)).
   intros.
   unfold scbwv_ξ.
   unfold scbwv_varstypes.
   set (@update_ξ_lemma _ _ (weakLT' ○ ξ) (weakL' l)
-    (unleaves (vec2list (vec_zip (scbwv_exprvars scb) (sac_types (scbwv_sac scb) Γ atypes))))
+    (unleaves (vec2list (vec_zip (scbwv_exprvars scb) (sac_types sac Γ atypes))))
     ) as q.
   rewrite <- mapleaves' in q.
   rewrite <- mapleaves' in q.
@@ -722,18 +725,28 @@ Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _} :
   apply scbwv_exprvars_distinct.
   Qed.
 
-Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e alts',
-  mapOptionTree ξ (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts'))
-  = ((mapOptionTreeAndFlatten pcb_freevars (mapOptionTree mkProofCaseBranch alts')),,mapOptionTree ξ  (expr2antecedent e)).
+
+Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e
+   (alts':Tree
+            ??{sac : StrongAltCon &
+              {scb : StrongCaseBranchWithVVs VV eqd_vv tc atypes sac &
+              Expr (sac_Γ sac Γ) (sac_Δ sac Γ atypes (weakCK'' Δ))
+                (scbwv_ξ scb ξ l) (weakLT' (tbranches @@  l))}}),
+
+      (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x))
+        (mapOptionTree mkProofCaseBranch alts'))
+    ,,
+    mapOptionTree ξ  (expr2antecedent e) =
+  mapOptionTree ξ
+        (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts')).
   intros.
   simpl.
   Ltac hack := match goal with [ |- ?A,,?B = ?C,,?D ] => assert (A=C) end.
   hack.
   induction alts'.
-  simpl.
-  destruct a.
+  destruct a; simpl.
+  destruct s; simpl.
   unfold mkProofCaseBranch.
-  simpl.
   reflexivity.
   reflexivity.
   simpl.
@@ -744,7 +757,6 @@ Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e alts',
   reflexivity.
   Qed.
 
-
 Definition expr2proof  :
   forall Γ Δ ξ τ (e:Expr Γ Δ ξ τ),
     ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [τ]].
@@ -783,18 +795,19 @@ Definition expr2proof  :
     | ECase    Γ Δ ξ l tc tbranches atypes e alts' => 
       let dcsp :=
         ((fix mkdcsp (alts:
-               Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes
-                            & Expr (sac_Γ scb Γ)
-                                   (sac_Δ scb Γ atypes (weakCK'' Δ))
+               Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
+                            & Expr (sac_Γ sac Γ)
+                                   (sac_Δ sac Γ atypes (weakCK'' Δ))
                                    (scbwv_ξ scb ξ l)
-                                   (weakLT' (tbranches@@l)) })
-          : ND Rule [] (mapOptionTree (pcb_judg ○ mkProofCaseBranch) alts) :=
-        match alts as ALTS return ND Rule [] (mapOptionTree (pcb_judg ○ mkProofCaseBranch) ALTS) with
+                                   (weakLT' (tbranches@@l)) } })
+          : ND Rule [] (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) alts) :=
+        match alts as ALTS return ND Rule [] 
+          (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) ALTS) with
           | T_Leaf None      => let case_nil := tt in _
           | T_Branch b1 b2   => let case_branch := tt in (fun b1' b2' => _) (mkdcsp b1) (mkdcsp b2)
           | T_Leaf (Some x)  =>
-            match x as X return ND Rule [] [(pcb_judg ○ mkProofCaseBranch) X] with
-            existT scbx ex =>
+            match x as X return ND Rule [] [pcb_judg (projT2 (mkProofCaseBranch X))] with
+            existT sac (existT scbx ex) =>
             (fun e' => let case_leaf := tt in _) (expr2proof _ _ _ _ ex)
         end
         end) alts')
@@ -912,10 +925,6 @@ Definition expr2proof  :
       clear o x alts alts' e.
       eapply nd_comp; [ apply e' | idtac ].
       clear e'.
-      set (existT
-              (fun scb : StrongCaseBranchWithVVs VV eqd_vv tc atypes =>
-               Expr (sac_Γ scb Γ) (sac_Δ scb Γ atypes (weakCK'' Δ))
-                 (scbwv_ξ scb ξ l) (weakLT' (tbranches @@  l))) scbx ex) as stuff.
       set (fun q r x1 x2 y1 y2 => @UND_to_ND q r [q >> r > x1 |- y1] [q >> r > x2 |- y2]).
       simpl in n.
       apply n.
@@ -957,7 +966,8 @@ Definition expr2proof  :
       apply b2'.
 
     destruct case_ECase.
-      rewrite case_lemma.
+    set (@RCase Γ Δ l tc) as q.
+      rewrite <- case_lemma.
       eapply nd_comp; [ idtac | eapply nd_rule; eapply RCase ].
       eapply nd_comp; [ apply nd_llecnac | idtac ]; apply nd_prod.
       rewrite <- mapOptionTree_compose.

diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v
index dacdcae..ad1dee7 100644 (file)
--- a/src/HaskStrongToWeak.v
+++ b/src/HaskStrongToWeak.v
@@ -156,11 +156,13 @@ Section HaskStrongToWeak.
                   ; bind tbranches' = @typeToWeakType Γ _ tbranches ite
                   ; bind escrut'    = exprToWeakExpr χ escrut ite
                   ; bind branches'  =
-                      ((fix caseBranches (tree:Tree ??{scb : StrongCaseBranchWithVVs VV _ _ _ & Expr _ _ _ _  })
+                      ((fix caseBranches (tree:Tree ??{sac : _ & { scb : StrongCaseBranchWithVVs VV _ _ _ sac & Expr _ _ _ _ } })
                             : UniqM (Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
                             match tree with
                               | T_Leaf None           => return []
-                              | T_Leaf (Some x)       => let (scb,e) := x in
+                              | T_Leaf (Some x)       =>
+                                let (sac,scb_e) := x in
+                                let (scb,e) := scb_e in
                                 let varstypes := vec2list (scbwv_varstypes scb) in
                                       bind evars_ite = mfresh _ ite
                                     ; bind exprvars  = seqM (map (fun vt:VV * HaskType _ ★
@@ -170,7 +172,7 @@ Section HaskStrongToWeak.
                                                                 varstypes)
                                     ; let χ' := update_χ' χ exprvars in
                                       bind e'' = exprToWeakExpr χ' e (snd evars_ite)
-                                    ; return [(sac_altcon scb, vec2list (fst evars_ite), nil, (map (@snd _ _) exprvars), e'')]
+                                    ; return [(sac_altcon sac, vec2list (fst evars_ite), nil, (map (@snd _ _) exprvars), e'')]
                               | T_Branch b1 b2        => bind b1' = caseBranches b1
                                                        ; bind b2' = caseBranches b2
                                                        ; return (b1',,b2')

diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v
index f2ceddf..bbc9cc7 100644 (file)
--- a/src/HaskWeakToStrong.v
+++ b/src/HaskWeakToStrong.v
@@ -656,8 +656,8 @@ Definition weakExprToStrongExpr : forall
             else mkAvars avars (tyConKind tc) φ >>= fun avars' =>
                 weakTypeToTypeOfKind φ tbranches ★  >>= fun tbranches' =>
                   (fix mkTree (t:Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree
-                      ??{scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' &
-                        Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ))(scbwv_ξ scb ξ lev)(weakLT' (tbranches' @@  lev))}) := 
+                      ??{ sac : _ & {scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' sac &
+                        Expr (sac_Γ sac Γ) (sac_Δ sac Γ avars' (weakCK'' Δ))(scbwv_ξ scb ξ lev)(weakLT' (tbranches' @@  lev))}}) := 
                     match t with
                       | T_Leaf None           => OK []
                       | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) => 
@@ -666,7 +666,7 @@ Definition weakExprToStrongExpr : forall
                           >>= fun exprvars' =>
                             (let case_pf := tt in _) >>= fun pf =>
                             let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' pf in
-                              weakExprToStrongExpr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ)
+                              weakExprToStrongExpr (sac_Γ sac Γ) (sac_Δ sac Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ)
                               (sacpj_ψ sac _ _ avars' ψ)
                               (scbwv_ξ scb ξ lev)
                               (update_ig ig (map (@fst _ _) (vec2list (scbwv_varstypes scb))))
@@ -708,6 +708,7 @@ Definition weakExprToStrongExpr : forall
       apply OK; auto.
 
     destruct case_case.
+      exists sac.
       exists scb.
       apply ebranch'.