From: Adam Megacz <megacz@cs.berkeley.edu>
Date: Thu, 12 May 2011 22:28:14 +0000 (-0700)
Subject: swap order of hypotheses in RApp to match RLet
X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=164cdbf41ca206079b0dcfc18cd13625b286c38c

swap order of hypotheses in RApp to match RLet
---

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index 3cd8ff6..e4281d7 100644
--- a/src/ExtractionMain.v
+++ b/src/ExtractionMain.v
@@ -236,12 +236,13 @@ Section core2proof.
     ND Rule 
        [ Γ > Δ > Σ             |- [a ---> s @@ lev ] ]
        [ Γ > Δ > Σ,,[a @@ lev] |-       [ s @@ lev ] ].
-    eapply nd_comp; [ idtac | eapply nd_rule; apply (@RApp Γ Δ Σ [a@@lev] a s lev) ].
-    eapply nd_comp; [ apply nd_rlecnac | idtac ].
-    apply nd_prod.    
-    apply nd_id.
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
+    eapply nd_comp; [ idtac | eapply nd_rule; apply (@RApp Γ Δ [a@@lev] Σ a s lev) ].
+    eapply nd_comp; [ apply nd_llecnac | idtac ].
+    apply nd_prod.
     apply nd_rule.
     apply RVar.
+    apply nd_id.
     Defined.
 
   Definition fToC1 {Γ}{Δ}{a}{s}{lev} :
diff --git a/src/HaskProof.v b/src/HaskProof.v
index d28db62..ee536b0 100644
--- a/src/HaskProof.v
+++ b/src/HaskProof.v
@@ -81,7 +81,7 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type :=
 
 | RJoin  : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ ,   Rule ([Γ > Δ > Σ₁ |- τ₁ ],,[Γ > Δ > Σ₂ |- τ₂ ])         [Γ>Δ>  Σ₁,,Σ₂  |- τ₁,,τ₂          ]
 
-| RApp           : ∀ Γ Δ Σ₁ Σ₂ tx te l,  Rule ([Γ>Δ> Σ₁       |- [tx--->te @@l]],,[Γ>Δ> Σ₂ |- [tx@@l]])  [Γ>Δ> Σ₁,,Σ₂ |- [te   @@l]]
+| RApp           : ∀ Γ Δ Σ₁ Σ₂ tx te l,  Rule ([Γ>Δ> Σ₁ |- [tx@@l]],,[Γ>Δ> Σ₂       |- [tx--->te @@l]])  [Γ>Δ> Σ₁,,Σ₂ |- [te   @@l]]
 
 | RLet           : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l,  Rule ([Γ>Δ> Σ₂ |- [σ₂@@l]],,[Γ>Δ> Σ₁,,[σ₂@@l] |- [σ₁@@l] ])     [Γ>Δ> Σ₁,,Σ₂ |- [σ₁   @@l]]
 
diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v
index b14a53e..19f2f62 100644
--- a/src/HaskProofToStrong.v
+++ b/src/HaskProofToStrong.v
@@ -632,7 +632,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.
diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v
index 8cd5688..9c3b041 100644
--- a/src/HaskStrongToProof.v
+++ b/src/HaskStrongToProof.v
@@ -522,7 +522,7 @@ Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ?
   | EGlobal  Γ Δ ξ _ _ _                          => []
   | EVar     Γ Δ ξ ev                             => [ev]
   | ELit     Γ Δ ξ lit lev                        => []
-  | EApp     Γ Δ ξ t1 t2 lev e1 e2                => (expr2antecedent e1),,(expr2antecedent e2)
+  | EApp     Γ Δ ξ t1 t2 lev e1 e2                => (expr2antecedent e2),,(expr2antecedent e1)
   | ELam     Γ Δ ξ t1 t2 lev v    e               => stripOutVars (v::nil) (expr2antecedent e)
   | ELet     Γ Δ ξ tv t  lev v ev ebody           => ((stripOutVars (v::nil) (expr2antecedent ebody)),,(expr2antecedent ev))
   | EEsc     Γ Δ ξ ec t lev e                     => expr2antecedent e
@@ -997,11 +997,11 @@ Definition expr2proof  :
 
     destruct case_EApp.
       unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
-      eapply nd_comp; [ idtac | eapply nd_rule; apply RApp ].
+      eapply nd_comp; [ idtac
+        | eapply nd_rule;
+          apply (@RApp _ _ _ _ t2 t1) ].
       eapply nd_comp; [ apply nd_llecnac | idtac ].
       apply nd_prod; auto.
-      apply e1'.
-      apply e2'.
 
     destruct case_ELam; intros.
       unfold mapOptionTree; simpl; fold (mapOptionTree ξ).