X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProofToStrong.v;h=69e8bb1f7914a8519d42f9c6fe757ac3086843f7;hp=19f2f62d8dd7a53105c6c4ebf185a7f42e586bdb;hb=a45824c7d03fcf797e22d2919187a7e97fb567cc;hpb=164cdbf41ca206079b0dcfc18cd13625b286c38c

diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v
index 19f2f62..69e8bb1 100644
--- a/src/HaskProofToStrong.v
+++ b/src/HaskProofToStrong.v
@@ -42,7 +42,7 @@ Section HaskProofToStrong.
     Defined.
 
   Lemma update_branches : forall Γ (ξ:VV -> LeveledHaskType Γ ★) lev l1 l2 q,
-    update_ξ ξ lev (app l1 l2) q = update_ξ (update_ξ ξ lev l2) lev l1 q.
+    update_xi ξ lev (app l1 l2) q = update_xi (update_xi ξ lev l2) lev l1 q.
     intros.
     induction l1.
       reflexivity.
@@ -122,7 +122,7 @@ Section HaskProofToStrong.
   Lemma fresh_lemma'' Γ 
     : forall types ξ lev, 
     FreshM { varstypes : _
-      |  mapOptionTree (update_ξ(Γ:=Γ)   ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev)
+      |  mapOptionTree (update_xi(Γ:=Γ)   ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev)
       /\ distinct (leaves (mapOptionTree (@fst _ _) varstypes)) }.
   admit.
   Defined.
@@ -130,8 +130,8 @@ Section HaskProofToStrong.
   Lemma fresh_lemma' Γ 
     : forall types vars Σ ξ lev, Σ = mapOptionTree ξ vars ->
     FreshM { varstypes : _
-      |  mapOptionTree (update_ξ(Γ:=Γ) ξ lev (leaves varstypes)) vars = Σ
-      /\ mapOptionTree (update_ξ       ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev)
+      |  mapOptionTree (update_xi(Γ:=Γ) ξ lev (leaves varstypes)) vars = Σ
+      /\ mapOptionTree (update_xi       ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev)
       /\ distinct (leaves (mapOptionTree (@fst _ _) varstypes)) }.
     induction types.
       intros; destruct a.
@@ -164,7 +164,7 @@ Section HaskProofToStrong.
         intros vars Σ ξ lev pf; refine (bind x2 = IHtypes2 vars Σ ξ lev pf; _).
           apply FreshMon.
           destruct x2 as [vt2 [pf21 [pf22 pfdist]]].
-          refine (bind x1 = IHtypes1 (vars,,(mapOptionTree (@fst _ _) vt2)) (Σ,,(types2@@@lev)) (update_ξ ξ lev
+          refine (bind x1 = IHtypes1 (vars,,(mapOptionTree (@fst _ _) vt2)) (Σ,,(types2@@@lev)) (update_xi ξ lev
             (leaves vt2)) _ _; return _).
           apply FreshMon.
           simpl.
@@ -204,8 +204,8 @@ Section HaskProofToStrong.
   Lemma fresh_lemma Γ ξ vars Σ Σ' lev
     : Σ = mapOptionTree ξ vars ->
     FreshM { vars' : _
-      |  mapOptionTree (update_ξ(Γ:=Γ) ξ lev ((vars',Σ')::nil)) vars = Σ
-      /\ mapOptionTree (update_ξ ξ lev ((vars',Σ')::nil)) [vars'] = [Σ' @@ lev] }.
+      |  mapOptionTree (update_xi(Γ:=Γ) ξ lev ((vars',Σ')::nil)) vars = Σ
+      /\ mapOptionTree (update_xi ξ lev ((vars',Σ')::nil)) [vars'] = [Σ' @@ lev] }.
     intros.
     set (fresh_lemma' Γ [Σ'] vars Σ ξ lev H) as q.
     refine (q >>>= fun q' => return _).
@@ -239,6 +239,7 @@ Section HaskProofToStrong.
  with
           | RLeft   h c ctx r => let case_RLeft  := tt in (fun e => _) (urule2expr _ _ _ r)
           | RRight  h c ctx r => let case_RRight := tt in (fun e => _) (urule2expr _ _ _ r)
+          | RId     a       => let case_RId    := tt in _
           | RCanL   a       => let case_RCanL  := tt in _
           | RCanR   a       => let case_RCanR  := tt in _
           | RuCanL  a       => let case_RuCanL := tt in _
@@ -251,6 +252,9 @@ Section HaskProofToStrong.
           | RComp   a b c f g => let case_RComp  := tt in (fun e1 e2 => _) (urule2expr _ _ _ f) (urule2expr _ _ _ g)
           end); clear urule2expr; intros.
 
+      destruct case_RId.
+        apply X.
+
       destruct case_RCanL.
         simpl; unfold ujudg2exprType; intros.
         simpl in X.
@@ -415,7 +419,7 @@ Section HaskProofToStrong.
      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)).
+         & Expr (sac_gamma sac Γ) (sac_delta sac Γ avars (weakCK'' Δ)) (scbwv_xi scb ξ lev) (weakLT' (tbranches @@  lev)) }) (projT1 pcb)).
     intro pcb.
     intro X.
     simpl in X.
@@ -441,10 +445,10 @@ Section HaskProofToStrong.
     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 _).
+    refine (bind q = (f (scbwv_xi scb ξ lev) (vars,,(unleaves (vec2list (scbwv_exprvars scb)))) _) ; return _).
       apply FreshMon.
       simpl.
-      unfold scbwv_ξ.
+      unfold scbwv_xi.
       rewrite vars_pf.
       rewrite <- mapOptionTree_compose.
       clear localvars_pf1.
@@ -520,8 +524,9 @@ Section HaskProofToStrong.
       | RAbsCo  Γ Δ Σ κ σ  σ₁ σ₂  y   => let case_RAbsCo := tt        in _
       | RApp    Γ Δ Σ₁ Σ₂ tx te p     => let case_RApp := tt          in _
       | RLet    Γ Δ Σ₁ Σ₂ σ₁ σ₂ p     => let case_RLet := tt          in _
-      | RJoin Γ p lri m x q   => let case_RJoin := tt in _
-      | RVoid _ _               => let case_RVoid := tt   in _
+      | RWhere  Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ p  => let case_RWhere := tt          in _
+      | RJoin   Γ p lri m x q         => let case_RJoin := tt in _
+      | RVoid   _ _                   => 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 _
       | RCase   Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt         in _
@@ -576,7 +581,7 @@ Section HaskProofToStrong.
     refine (fresh_lemma _ ξ vars _ tx x H >>>= (fun pf => _)).
     apply FreshMon.
     destruct pf as [ vnew [ pf1 pf2 ]].
-    set (update_ξ ξ x (((vnew, tx  )) :: nil)) as ξ' in *.
+    set (update_xi ξ x (((vnew, tx  )) :: nil)) as ξ' in *.
     refine (X_ ξ' (vars,,[vnew]) _ >>>= _).
     apply FreshMon.
     simpl.
@@ -632,42 +637,84 @@ Section HaskProofToStrong.
     apply ileaf in q1'.
     apply ileaf in q2'.
     simpl in *.
-    apply (EApp _ _ _ _ _ _ q2' q1').
+    apply (EApp _ _ _ _ _ _ q1' q2').
 
   destruct case_RLet.
     apply ILeaf.
     simpl in *; intros.
     destruct vars; try destruct o; inversion H.
-    refine (fresh_lemma _ ξ vars1 _ σ₂ p H1 >>>= (fun pf => _)).
+
+    refine (fresh_lemma _ ξ _ _ σ₁ p H2 >>>= (fun pf => _)).
     apply FreshMon.
+
     destruct pf as [ vnew [ pf1 pf2 ]].
-    set (update_ξ ξ p (((vnew, σ₂ )) :: nil)) as ξ' in *.
+    set (update_xi ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *.
     inversion X_.
     apply ileaf in X.
     apply ileaf in X0.
     simpl in *.
-    refine (X ξ  vars2 _ >>>= fun X0' => _).
+
+    refine (X ξ vars1 _ >>>= fun X0' => _).
     apply FreshMon.
+    simpl.
     auto.
 
-    refine (X0 ξ' (vars1,,[vnew]) _ >>>= fun X1' => _).
+    refine (X0 ξ' ([vnew],,vars2) _ >>>= fun X1' => _).
     apply FreshMon.
-    rewrite H1.
     simpl.
     rewrite pf2.
     rewrite pf1.
-    rewrite H1.
     reflexivity.
+    apply FreshMon.
 
-    refine (return _).
     apply ILeaf.
-    apply ileaf in X0'.
     apply ileaf in X1'.
+    apply ileaf in X0'.
     simpl in *.
-    apply ELet with (ev:=vnew)(tv:=σ₂).
+    apply ELet with (ev:=vnew)(tv:=σ₁).
     apply X0'.
     apply X1'.
 
+  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_RVoid.
     apply ILeaf; simpl; intros.
     refine (return _).
@@ -704,7 +751,7 @@ Section HaskProofToStrong.
     apply ILeaf; simpl; intros.
     refine (bind ξvars = fresh_lemma' _ y _ _ _ t H; _). apply FreshMon.
     destruct ξvars as [ varstypes [ pf1[ pf2 pfdist]]].
-    refine (X_ ((update_ξ ξ t (leaves varstypes)))
+    refine (X_ ((update_xi ξ t (leaves varstypes)))
       (vars,,(mapOptionTree (@fst _ _) varstypes)) _ >>>= fun X => return _); clear X_.  apply FreshMon.
     simpl.
     rewrite pf2.
@@ -716,11 +763,11 @@ Section HaskProofToStrong.
     apply (@ELetRec _ _ _ _ _ _ _ varstypes).
     auto.
     apply (@letrec_helper Γ Δ t varstypes).
-    rewrite <- pf2 in X1.
+    rewrite <- pf2 in X0.
     rewrite mapOptionTree_compose.
-    apply X1.
-    apply ileaf in X0.
     apply X0.
+    apply ileaf in X1.
+    apply X1.
 
   destruct case_RCase.
     apply ILeaf; simpl; intros.
@@ -777,7 +824,7 @@ Section HaskProofToStrong.
     clear q.
     destruct q' as [varstypes [pf1 [pf2 distpf]]].
     exists (mapOptionTree (@fst _ _) varstypes).
-    exists (update_ξ ξ l (leaves varstypes)).
+    exists (update_xi ξ l (leaves varstypes)).
     symmetry; auto.
     refine (return _).
     exists [].