X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProofToStrong.v;h=b6e8efee00b3730606325935a866162a67bb9ffa;hp=3dee0fecf5967ce4e9a600c0f91822a2ae7287d2;hb=93ac0d63048027161f816c451a7954fb8a6470c0;hpb=97552c1a6dfb32098d4491951929ab1d4aca96a0

diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v
index 3dee0fe..b6e8efe 100644
--- a/src/HaskProofToStrong.v
+++ b/src/HaskProofToStrong.v
@@ -25,12 +25,6 @@ Section HaskProofToStrong.
 
   Definition ExprVarResolver Γ := VV -> LeveledHaskType Γ ★.
 
-  Definition ujudg2exprType {Γ}{Δ}(ξ:ExprVarResolver Γ)(j:UJudg Γ Δ) : Type :=
-    match j with
-      mkUJudg Σ τ => forall vars, Σ = mapOptionTree ξ vars ->
-        FreshM (ITree _ (fun t => Expr Γ Δ ξ t) τ)
-      end.
-
   Definition judg2exprType (j:Judg) : Type :=
     match j with
       (Γ > Δ > Σ |- τ) => forall (ξ:ExprVarResolver Γ) vars, Σ = mapOptionTree ξ vars ->
@@ -228,172 +222,136 @@ Section HaskProofToStrong.
       inversion pf2.
     Defined.
 
-  Definition urule2expr  : forall Γ Δ h j (r:@URule Γ Δ h j) (ξ:VV -> LeveledHaskType Γ ★),
-    ITree _ (ujudg2exprType ξ) h -> ITree _ (ujudg2exprType ξ) j.
-
-      refine (fix urule2expr Γ Δ h j (r:@URule Γ Δ h j) ξ {struct r} : 
-        ITree _ (ujudg2exprType ξ) h -> ITree _ (ujudg2exprType ξ) j :=
-        match r as R in URule H C return ITree _ (ujudg2exprType ξ) H -> ITree _ (ujudg2exprType ξ) C 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)
-          | RCanL   t a       => let case_RCanL  := tt in _
-          | RCanR   t a       => let case_RCanR  := tt in _
-          | RuCanL  t a       => let case_RuCanL := tt in _
-          | RuCanR  t a       => let case_RuCanR := tt in _
-          | RAssoc  t a b c   => let case_RAssoc := tt in _
-          | RCossa  t a b c   => let case_RCossa := tt in _
-          | RExch   t a b     => let case_RExch  := tt in _
-          | RWeak   t a       => let case_RWeak  := tt in _
-          | RCont   t a       => let case_RCont  := tt in _
+  Definition ujudg2exprType Γ (ξ:ExprVarResolver Γ)(Δ:CoercionEnv Γ) Σ τ : Type :=
+    forall vars, Σ = mapOptionTree ξ vars -> FreshM (ITree _ (fun t => Expr Γ Δ ξ t) τ).
+
+  Definition urule2expr  : forall Γ Δ h j t (r:@Arrange _ h j) (ξ:VV -> LeveledHaskType Γ ★),
+    ujudg2exprType Γ ξ Δ h t ->
+    ujudg2exprType Γ ξ Δ j t
+    .
+    intros Γ Δ.
+      refine (fix urule2expr h j t (r:@Arrange _ h j) ξ {struct r} : 
+    ujudg2exprType Γ ξ Δ h t ->
+    ujudg2exprType Γ ξ Δ j t :=
+        match r as R in Arrange H C return
+    ujudg2exprType Γ ξ Δ H t ->
+    ujudg2exprType Γ ξ Δ C t
+ 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 _
+          | RuCanR  a       => let case_RuCanR := tt in _
+          | RAssoc  a b c   => let case_RAssoc := tt in _
+          | RCossa  a b c   => let case_RCossa := tt in _
+          | RExch   a b     => let case_RExch  := tt in _
+          | RWeak   a       => let case_RWeak  := tt in _
+          | RCont   a       => let case_RCont  := tt in _
+          | 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.
-        apply ILeaf; simpl; intros.
-        inversion X.
-        simpl in X0.
-        apply (X0 ([],,vars)).
+        simpl; unfold ujudg2exprType; intros.
+        simpl in X.
+        apply (X ([],,vars)).
         simpl; rewrite <- H; auto.
 
       destruct case_RCanR.
-        apply ILeaf; simpl; intros.
-        inversion X.
-        simpl in X0.
-        apply (X0 (vars,,[])).
+        simpl; unfold ujudg2exprType; intros.
+        simpl in X.
+        apply (X (vars,,[])).
         simpl; rewrite <- H; auto.
 
       destruct case_RuCanL.
-        apply ILeaf; simpl; intros.
+        simpl; unfold ujudg2exprType; intros.
         destruct vars; try destruct o; inversion H.
-        inversion X.
-        simpl in X0.
-        apply (X0 vars2); auto.
+        simpl in X.
+        apply (X vars2); auto.
 
       destruct case_RuCanR.
-        apply ILeaf; simpl; intros.
+        simpl; unfold ujudg2exprType; intros.
         destruct vars; try destruct o; inversion H.
-        inversion X.
-        simpl in X0.
-        apply (X0 vars1); auto.
+        simpl in X.
+        apply (X vars1); auto.
 
       destruct case_RAssoc.
-        apply ILeaf; simpl; intros.
-        inversion X.
-        simpl in X0.
+        simpl; unfold ujudg2exprType; intros.
+        simpl in X.
         destruct vars; try destruct o; inversion H.
         destruct vars1; try destruct o; inversion H.
-        apply (X0 (vars1_1,,(vars1_2,,vars2))).
+        apply (X (vars1_1,,(vars1_2,,vars2))).
         subst; auto.
 
       destruct case_RCossa.
-        apply ILeaf; simpl; intros.
-        inversion X.
-        simpl in X0.
+        simpl; unfold ujudg2exprType; intros.
+        simpl in X.
         destruct vars; try destruct o; inversion H.
         destruct vars2; try destruct o; inversion H.
-        apply (X0 ((vars1,,vars2_1),,vars2_2)).
+        apply (X ((vars1,,vars2_1),,vars2_2)).
         subst; auto.
 
+      destruct case_RExch.
+        simpl; unfold ujudg2exprType ; intros.
+        simpl in X.
+        destruct vars; try destruct o; inversion H.
+        apply (X (vars2,,vars1)).
+        inversion H; subst; auto.
+        
+      destruct case_RWeak.
+        simpl; unfold ujudg2exprType; intros.
+        simpl in X.
+        apply (X []).
+        auto.
+        
+      destruct case_RCont.
+        simpl; unfold ujudg2exprType ; intros.
+        simpl in X.
+        apply (X (vars,,vars)).
+        simpl.
+        rewrite <- H.
+        auto.
+
       destruct case_RLeft.
-        destruct c; [ idtac | apply no_urules_with_multiple_conclusions in r0; inversion r0; exists c1; exists c2; auto ].
-        destruct o; [ idtac | apply INone ].
-        destruct u; simpl in *.
-        apply ILeaf; simpl; intros.
+        intro vars; unfold ujudg2exprType; intro H.
         destruct vars; try destruct o; inversion H.
-        set (fun q => ileaf (e ξ q)) as r'.
-        simpl in r'.
-        apply r' with (vars:=vars2).
-        clear r' e.
-        clear r0.
-        induction h0.
-          destruct a.
-          destruct u.
+        apply (fun q => e ξ q vars2 H2).
+        clear r0 e H2.
           simpl in X.
-          apply ileaf in X. 
-          apply ILeaf.
           simpl.
-          simpl in X.
+          unfold ujudg2exprType.
           intros.
           apply X with (vars:=vars1,,vars).
-          simpl.
           rewrite H0.
           rewrite H1.
+          simpl.
           reflexivity.
-          apply INone.
-          apply IBranch.
-          apply IHh0_1. inversion X; auto.
-          apply IHh0_2. inversion X; auto.
-          auto.
-        
+
       destruct case_RRight.
-        destruct c; [ idtac | apply no_urules_with_multiple_conclusions in r0; inversion r0; exists c1; exists c2; auto ].
-        destruct o; [ idtac | apply INone ].
-        destruct u; simpl in *.
-        apply ILeaf; simpl; intros.
+        intro vars; unfold ujudg2exprType; intro H.
         destruct vars; try destruct o; inversion H.
-        set (fun q => ileaf (e ξ q)) as r'.
-        simpl in r'.
-        apply r' with (vars:=vars1).
-        clear r' e.
-        clear r0.
-        induction h0.
-          destruct a.
-          destruct u.
+        apply (fun q => e ξ q vars1 H1).
+        clear r0 e H2.
           simpl in X.
-          apply ileaf in X. 
-          apply ILeaf.
           simpl.
-          simpl in X.
+          unfold ujudg2exprType.
           intros.
           apply X with (vars:=vars,,vars2).
-          simpl.
           rewrite H0.
-          rewrite H2.
+          inversion H.
+          simpl.
           reflexivity.
-          apply INone.
-          apply IBranch.
-          apply IHh0_1. inversion X; auto.
-          apply IHh0_2. inversion X; auto.
-          auto.
 
-      destruct case_RExch.
-        apply ILeaf; simpl; intros.
-        inversion X.
-        simpl in X0.
-        destruct vars; try destruct o; inversion H.
-        apply (X0 (vars2,,vars1)).
-        inversion H; subst; auto.
-        
-      destruct case_RWeak.
-        apply ILeaf; simpl; intros.
-        inversion X.
-        simpl in X0.
-        apply (X0 []).
-        auto.
-        
-      destruct case_RCont.
-        apply ILeaf; simpl; intros.
-        inversion X.
-        simpl in X0.
-        apply (X0 (vars,,vars)).
-        simpl.
-        rewrite <- H.
-        auto.
+      destruct case_RComp.
+        apply e2.
+        apply e1.
+        apply X.
         Defined.
 
-  Definition bridge Γ Δ (c:Tree ??(UJudg Γ Δ)) ξ :
-    ITree Judg judg2exprType (mapOptionTree UJudg2judg c) -> ITree (UJudg Γ Δ) (ujudg2exprType ξ) c.
-    intro it.
-    induction c.
-    destruct a.
-      destruct u; simpl in *.
-      apply ileaf in it.
-      apply ILeaf.
-      simpl in *.
-      intros; apply it with (vars:=vars); auto.
-    apply INone.
-    apply IBranch; [ apply IHc1 | apply IHc2 ]; inversion it; auto.
-    Defined.
-
   Definition letrec_helper Γ Δ l (varstypes:Tree ??(VV * HaskType Γ ★)) ξ' :
     ITree (LeveledHaskType Γ ★)
          (fun t : LeveledHaskType Γ ★ => Expr Γ Δ ξ' t)
@@ -553,7 +511,7 @@ Section HaskProofToStrong.
     intros h j r.
 
       refine (match r as R in Rule H C return ITree _ judg2exprType H -> ITree _ judg2exprType C with
-      | RURule a b c d e              => let case_RURule := tt        in _
+      | RArrange a b c d e  r         => let case_RURule := tt        in _
       | RNote   Γ Δ Σ τ l n           => let case_RNote := tt         in _
       | RLit    Γ Δ l     _           => let case_RLit := tt          in _
       | RVar    Γ Δ σ         p       => let case_RVar := tt          in _
@@ -566,27 +524,26 @@ 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 _
+      | 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 _
       | RLetRec Γ Δ lri x y t         => let case_RLetRec := tt       in _
       end); intro X_; try apply ileaf in X_; simpl in X_.
 
-  destruct case_RURule.
-    destruct d; try destruct o.
-      apply ILeaf; destruct u; simpl; intros.
-      set (@urule2expr a b _ _ e ξ) as q.
-      set (fun z => ileaf (q z)) as q'.
+    destruct case_RURule.
+      apply ILeaf. simpl. intros.
+      set (@urule2expr a b _ _ e r0 ξ) as q.
+      set (fun z => q z) as q'.
       simpl in q'.
       apply q' with (vars:=vars).
       clear q' q.
-      apply bridge.
-      apply X_.
+      unfold ujudg2exprType.
+      intros.
+      apply X_ with (vars:=vars0).
+      auto.
       auto.
-      apply no_urules_with_empty_conclusion in e; inversion e; auto.
-      apply no_urules_with_multiple_conclusions in e; inversion e; auto; exists d1; exists d2; auto.
 
   destruct case_RBrak.
     apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
@@ -616,7 +573,6 @@ Section HaskProofToStrong.
   destruct case_RGlobal.
     apply ILeaf; simpl; intros; refine (return ILeaf _ _).
     apply EGlobal.
-    apply wev.
 
   destruct case_RLam.
     apply ILeaf.
@@ -624,7 +580,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.
@@ -648,7 +604,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.
@@ -680,7 +636,7 @@ Section HaskProofToStrong.
     apply ileaf in q1'.
     apply ileaf in q2'.
     simpl in *.
-    apply (EApp _ _ _ _ _ _ q1' q2').
+    apply (EApp _ _ _ _ _ _ q2' q1').
 
   destruct case_RLet.
     apply ILeaf.
@@ -689,15 +645,16 @@ Section HaskProofToStrong.
     refine (fresh_lemma _ ξ vars1 _ σ₂ p H1 >>>= (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 (X0 ξ  vars2 _ >>>= fun X0' => _).
+    refine (X ξ  vars2 _ >>>= fun X0' => _).
     apply FreshMon.
     auto.
-    refine (X  ξ' (vars1,,[vnew]) _ >>>= fun X1' => _).
+
+    refine (X0 ξ' (vars1,,[vnew]) _ >>>= fun X1' => _).
     apply FreshMon.
     rewrite H1.
     simpl.
@@ -705,6 +662,7 @@ Section HaskProofToStrong.
     rewrite pf1.
     rewrite H1.
     reflexivity.
+
     refine (return _).
     apply ILeaf.
     apply ileaf in X0'.
@@ -714,7 +672,7 @@ Section HaskProofToStrong.
     apply X0'.
     apply X1'.
 
-  destruct case_REmptyGroup.
+  destruct case_RVoid.
     apply ILeaf; simpl; intros.
     refine (return _).
     apply INone.
@@ -760,6 +718,7 @@ Section HaskProofToStrong.
     inversion X; subst; clear X.
 
     apply (@ELetRec _ _ _ _ _ _ _ varstypes).
+    auto.
     apply (@letrec_helper Γ Δ t varstypes).
     rewrite <- pf2 in X1.
     rewrite mapOptionTree_compose.
@@ -803,15 +762,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 } }.
@@ -849,7 +805,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 *.
@@ -864,6 +820,7 @@ Section HaskProofToStrong.
     refine (return OK _).
     exists ξ.
     apply (ileaf it).
+    apply INone.
     Defined.
 
 End HaskProofToStrong.