X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProofToStrong.v;h=ab10fd82545bf6add1720110a24f2c5202ca0f36;hp=b16d4a8a00d1004881d5f6fa25dd9c7862ea332c;hb=489b12c6c491b96c37839610d33fbdf666ee527f;hpb=c90b598203ef23bf8d44d6b5b4a5a4b5901039cf

diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v
index b16d4a8..ab10fd8 100644
--- a/src/HaskProofToStrong.v
+++ b/src/HaskProofToStrong.v
@@ -393,9 +393,9 @@ Section HaskProofToStrong.
     exists x; auto.
     Defined.
 
-  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).
+  Definition fix_indexing X Y (J:X->Type)(t:Tree ??(X*Y))
+    :  ITree (X * Y) (fun x => J (fst x))                                t
+    -> ITree X       (fun x:X => J x)   (mapOptionTree (@fst _ _) t).
     intro it.
     induction it; simpl in *.
     apply INone.
@@ -418,12 +418,13 @@ Section HaskProofToStrong.
     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'} ->
+    forall pcb:(StrongAltCon * Tree ??(LeveledHaskType Γ ★)),
+     prod (judg2exprType (@pcb_judg tc Γ Δ lev tbranches avars (fst pcb) (snd pcb)))
+     {vars' : Tree ??VV & (snd pcb) = mapOptionTree ξ vars'} ->
      ((fun sac => FreshM
        { scb : StrongCaseBranchWithVVs VV eqdec_vv tc avars sac
          & Expr (sac_gamma sac Γ) (sac_delta sac Γ avars (weakCK'' Δ)) (scbwv_xi scb ξ lev)
-         (weakT' tbranches) (weakL' lev) }) (projT1 pcb)).
+         (weakT' tbranches) (weakL' lev) }) (fst pcb)).
     intro pcb.
     intro X.
     simpl in X.
@@ -435,7 +436,7 @@ Section HaskProofToStrong.
     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) _  ; _).
+      (mapOptionTree weakLT' pcb) (weakLT' ○ ξ) (weakL' lev) _  ; _).
       apply FreshMon.
       rewrite vars_pf.
       rewrite <- mapOptionTree_compose.
@@ -470,14 +471,15 @@ Section HaskProofToStrong.
     Defined.
 
   Definition gather_branch_variables
-    Γ Δ (ξ:VV -> LeveledHaskType Γ ★) tc avars tbranches lev (alts:Tree ?? {sac : StrongAltCon &
-                ProofCaseBranch tc Γ Δ lev tbranches avars sac})
+    Γ Δ
+    (ξ:VV -> LeveledHaskType Γ ★) tc avars tbranches lev
+    (alts:Tree ??(@StrongAltCon tc * Tree ??(LeveledHaskType Γ ★)))
     :
     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' })
+    mapOptionTreeAndFlatten (fun x => snd x) alts = mapOptionTree ξ vars
+    -> ITree Judg judg2exprType (mapOptionTree (fun x => @pcb_judg tc Γ Δ lev avars tbranches (fst x) (snd x)) alts)
+    -> ITree _ (fun q => prod (judg2exprType (@pcb_judg tc Γ Δ lev avars tbranches (fst q) (snd q))) 
+      { vars' : _ & (snd q) = mapOptionTree ξ vars' })
   alts.
     induction alts;
     intro vars;
@@ -487,7 +489,7 @@ Section HaskProofToStrong.
     simpl in *.
     apply ileaf in source.
     apply ILeaf.
-    destruct s as [sac pcb].
+    destruct p as [sac pcb].
     simpl in *.
     split.
     intros.
@@ -758,17 +760,14 @@ Section HaskProofToStrong.
       | RGlobal Γ Δ σ l wev           => let case_RGlobal := tt       in _
       | RLam    Γ Δ Σ tx te     x     => let case_RLam := tt          in _
       | RCast   Γ Δ Σ σ τ γ     x     => let case_RCast := tt         in _
-      | RAbsT   Γ Δ Σ κ σ a           => let case_RAbsT := tt         in _
+      | RAbsT   Γ Δ Σ κ σ a n         => let case_RAbsT := tt         in _
       | RAppT   Γ Δ Σ κ σ τ     y     => let case_RAppT := tt         in _
       | RAppCo  Γ Δ Σ κ σ₁ σ₂ γ σ l   => let case_RAppCo := tt        in _
       | RAbsCo  Γ Δ Σ κ σ  σ₁ σ₂  y   => let case_RAbsCo := tt        in _
       | RApp    Γ Δ Σ₁ Σ₂ tx te p     => let case_RApp := tt          in _
-      | RLet    Γ Δ Σ₁ Σ₂ σ₁ σ₂ p     => let case_RLet := tt          in _
-      | RCut    Γ Δ Σ₁ Σ₁₂ Σ₂ Σ₃ l    => let case_RCut := tt          in _
+      | RCut    Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l  => let case_RCut := tt          in _
       | RLeft   Γ Δ Σ₁ Σ₂  Σ     l    => let case_RLeft := tt in _
       | RRight  Γ Δ Σ₁ Σ₂  Σ     l    => let case_RRight := tt in _
-      | RWhere  Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ p  => let case_RWhere := tt          in _
-      | RJoin   Γ p lri m x q l       => let case_RJoin := tt in _
       | RVoid   _ _ l                 => let case_RVoid := tt   in _
       | RBrak   Σ a b c n m           => let case_RBrak := tt         in _
       | REsc    Σ a b c n m           => let case_REsc := tt          in _
@@ -849,19 +848,6 @@ Section HaskProofToStrong.
     apply ileaf in X. simpl in X.
     apply X.
 
-  destruct case_RJoin.
-    apply ILeaf; simpl; intros.
-    inversion X_.
-    apply ileaf in X.
-    apply ileaf in X0.
-    simpl in *.
-    destruct vars; inversion H.
-    destruct o; inversion H3.
-    refine (X ξ vars1 H3 >>>= fun X' => X0 ξ vars2 H4 >>>= fun X0' => return _).
-    apply FreshMon.
-    apply FreshMon.
-    apply IBranch; auto.
-
   destruct case_RApp.    
     apply ILeaf.
     inversion X_.
@@ -883,54 +869,19 @@ Section HaskProofToStrong.
     simpl in *.
     apply (EApp _ _ _ _ _ _ q1' q2').
 
-  destruct case_RLet.
-    eapply rlet.
-    apply X_.
-
-  destruct case_RWhere.
-    apply ILeaf.
-    simpl in *; intros.
-    destruct vars;  try destruct o; inversion H.
-    destruct vars2; try destruct o; inversion H2.
-    clear H2.
-
-    assert ((Σ₁,,Σ₃) = mapOptionTree ξ (vars1,,vars2_2)) as H13; simpl; subst; auto.
-    refine (fresh_lemma _ ξ _ _ σ₁ p H13 >>>= (fun pf => _)).
-    apply FreshMon.
-
-    destruct pf as [ vnew [ pf1 pf2 ]].
-    set (update_xi ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *.
-    inversion X_.
-    apply ileaf in X.
-    apply ileaf in X0.
-    simpl in *.
-
-    refine (X ξ' (vars1,,([vnew],,vars2_2)) _ >>>= fun X0' => _).
-    apply FreshMon.
-    simpl.
-    inversion pf1.
-    rewrite H3.
-    rewrite H4.
-    rewrite pf2.
-    reflexivity.
-
-    refine (X0 ξ vars2_1 _ >>>= fun X1' => _).
-    apply FreshMon.
-    reflexivity.
-    apply FreshMon.
-
-    apply ILeaf.
-    apply ileaf in X0'.
-    apply ileaf in X1'.
-    simpl in *.
-    apply ELet with (ev:=vnew)(tv:=σ₁).
-    apply X1'.
-    apply X0'.
-
   destruct case_RCut.
+    apply rassoc.
+    apply swapr.
+    apply rassoc'.
+
     inversion X_.
     subst.
     clear X_.
+
+    apply rassoc' in X0.
+    apply swapr in X0.
+    apply rassoc in X0.
+
     induction Σ₃.
     destruct a.
     subst.
@@ -989,12 +940,12 @@ Section HaskProofToStrong.
     apply (ileaf X).
 
   destruct case_RAbsT.
-    apply ILeaf; simpl; intros; refine (X_ (weakLT ○ ξ) vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
+    apply ILeaf; simpl; intros; refine (X_ (weakLT_ ○ ξ) vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
     rewrite mapOptionTree_compose.
     rewrite <- H.
     reflexivity.
     apply ileaf in X. simpl in *.
-    apply ETyLam.
+    apply (ETyLam _ _ _ _ _ _ n).
     apply X.
 
   destruct case_RAppCo.
@@ -1015,7 +966,7 @@ Section HaskProofToStrong.
     refine (bind ξvars = fresh_lemma' _ y _ _ _ t H; _). apply FreshMon.
     destruct ξvars as [ varstypes [ pf1[ pf2 pfdist]]].
     refine (X_ ((update_xi ξ t (leaves varstypes)))
-      (vars,,(mapOptionTree (@fst _ _) varstypes)) _ >>>= fun X => return _); clear X_.  apply FreshMon.
+      ((mapOptionTree (@fst _ _) varstypes),,vars) _ >>>= fun X => return _); clear X_.  apply FreshMon.
     simpl.
     rewrite pf2.
     rewrite pf1.