X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FHaskProofToStrong.v;h=6ba094e9fe98e7e3c373a86d1cf281b18e0ca532;hb=ada4d4ef74dbd3ca46b4f80eec68e10b903d75f4;hp=2b63c4a9442bdf70c40deb4a5fdb8893a662f568;hpb=75a5863eb9fb6cdfa1f07e538f6f948ffec80331;p=coq-hetmet.git

diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v
index 2b63c4a..6ba094e 100644
--- a/src/HaskProofToStrong.v
+++ b/src/HaskProofToStrong.v
@@ -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.
@@ -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 _
-      | RBindingGroup Γ p lri m x q   => let case_RBindingGroup := tt in _
-      | REmptyGroup _ _               => let case_REmptyGroup := 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 _
@@ -569,7 +574,6 @@ Section HaskProofToStrong.
   destruct case_RGlobal.
     apply ILeaf; simpl; intros; refine (return ILeaf _ _).
     apply EGlobal.
-    apply wev.
 
   destruct case_RLam.
     apply ILeaf.
@@ -577,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_ξ ξ x (((vnew, tx  )) :: nil)) as ξ' in *.
     refine (X_ ξ' (vars,,[vnew]) _ >>>= _).
     apply FreshMon.
     simpl.
@@ -601,7 +605,7 @@ Section HaskProofToStrong.
     apply ileaf in X. simpl in X.
     apply X.
 
-  destruct case_RBindingGroup.
+  destruct case_RJoin.
     apply ILeaf; simpl; intros.
     inversion X_.
     apply ileaf in X.
@@ -639,37 +643,79 @@ Section HaskProofToStrong.
     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_ξ ξ 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_REmptyGroup.
+  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_ξ ξ 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 _).
     apply INone.
@@ -715,12 +761,13 @@ Section HaskProofToStrong.
     inversion X; subst; clear X.
 
     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.
@@ -758,15 +805,12 @@ Section HaskProofToStrong.
       apply H2.
     Defined.
 
-  Definition closed2expr : forall c (pn:@ClosedND _ Rule c), ITree _ judg2exprType c.
-    refine ((
-      fix closed2expr' j (pn:@ClosedND _ Rule j) {struct pn} : ITree _ judg2exprType j :=
-      match pn in @ClosedND _ _ J return ITree _ judg2exprType J with
-      | cnd_weak             => let case_nil    := tt in INone _ _
-      | cnd_rule h c cnd' r  => let case_rule   := tt in rule2expr _ _ r (closed2expr' _ cnd')
-      | cnd_branch _ _ c1 c2 => let case_branch := tt in IBranch _ _ (closed2expr' _ c1) (closed2expr' _ c2)
-      end)); clear closed2expr'; intros; subst.
-        Defined.
+  Fixpoint closed2expr h j (pn:@SIND _ Rule h j) {struct pn} : ITree _ judg2exprType h -> ITree _ judg2exprType j :=
+    match pn in @SIND _ _ H J return ITree _ judg2exprType H -> ITree _ judg2exprType J with
+    | scnd_weak   _             => let case_nil    := tt in fun _ => INone _ _
+    | scnd_comp   x h c cnd' r  => let case_rule   := tt in fun q => rule2expr _ _ r (closed2expr _ _ cnd' q)
+    | scnd_branch _ _ _ c1 c2   => let case_branch := tt in fun q => IBranch _ _ (closed2expr _ _ c1 q) (closed2expr _ _ c2 q)
+    end.
 
   Lemma manyFresh : forall Γ Σ (ξ0:VV -> LeveledHaskType Γ ★),
     FreshM { vars : _ & { ξ : VV -> LeveledHaskType Γ ★ & Σ = mapOptionTree ξ vars } }.
@@ -804,7 +848,7 @@ Section HaskProofToStrong.
     {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ]] ->
     FreshM (???{ ξ : _ & Expr Γ Δ ξ τ}).
     intro pf.
-    set (closedFromSCND _ _ (mkSCND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) cnd_weak) as cnd.
+    set (mkSIND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) as cnd.
     apply closed2expr in cnd.
     apply ileaf in cnd.
     simpl in *.
@@ -819,6 +863,7 @@ Section HaskProofToStrong.
     refine (return OK _).
     exists ξ.
     apply (ileaf it).
+    apply INone.
     Defined.
 
 End HaskProofToStrong.