X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FExtractionMain.v;h=df7896b14e5330fecfecbe1c88e5c09a2db56f9e;hp=5be52807b489dfd1a977f4c20bc077d361130385;hb=1a2754d2e135ef3c5fd7ef817e1129af93b533a5;hpb=c64ac559ed9448b8aa24abedbc2ad5ca800d1d24

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index 5be5280..df7896b 100644
--- a/src/ExtractionMain.v
+++ b/src/ExtractionMain.v
@@ -13,6 +13,7 @@ Require Import Preamble.
 Require Import General.
 
 Require Import NaturalDeduction.
+Require Import NaturalDeductionContext.
 
 Require Import HaskKinds.
 Require Import HaskLiterals.
@@ -132,7 +133,7 @@ Section core2proof.
                     OK (eol+++eol+++eol+++
                         "\begin{preview}"+++eol+++
                         "$\displaystyle "+++
-                        toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ e))+++
+                        toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ _ e))+++
                         " $"+++eol+++
                         "\end{preview}"+++eol+++eol+++eol)
                   )))))))).
@@ -234,30 +235,30 @@ Section core2proof.
 
   Definition curry {Γ}{Δ}{a}{s}{Σ}{lev} :
     ND Rule 
-       [ Γ > Δ > Σ             |- [a ---> s @@ lev ] ]
-       [ Γ > Δ > Σ,,[a @@ lev] |-       [ s @@ lev ] ].
-    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 ].
+       [ Γ > Δ > Σ             |- [a ---> s  ]@lev ]
+       [ Γ > Δ > [a @@ lev],,Σ |-       [ s ]@lev ].
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RApp ].
+    eapply nd_comp; [ apply nd_rlecnac | idtac ].
     apply nd_prod.
+    apply nd_id.
     apply nd_rule.
     apply RVar.
-    apply nd_id.
     Defined.
 
   Definition fToC1 {Γ}{Δ}{a}{s}{lev} :
-    ND Rule [] [ Γ > Δ > [        ] |- [a ---> s @@ lev ] ] ->
-    ND Rule [] [ Γ > Δ > [a @@ lev] |-       [ s @@ lev ] ].
+    ND Rule [] [ Γ > Δ > [        ] |- [a ---> s  ]@lev ] ->
+    ND Rule [] [ Γ > Δ > [a @@ lev] |-       [ s  ]@lev ].
     intro pf.
     eapply nd_comp.
     apply pf.
-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanR ].
     apply curry.
     Defined.
 
   Definition fToC2 {Γ}{Δ}{a1}{a2}{s}{lev} :
-    ND Rule [] [ Γ > Δ >                       [] |- [a1 ---> (a2 ---> s) @@ lev ] ] ->
-    ND Rule [] [ Γ > Δ > [a1 @@ lev],,[a2 @@ lev] |-                 [ s @@ lev ] ].
+    ND Rule [] [ Γ > Δ >                       [] |- [a1 ---> (a2 ---> s)  ]@lev ] ->
+    ND Rule [] [ Γ > Δ > [a1 @@ lev],,[a2 @@ lev] |-                  [ s  ]@lev ].
     intro pf.
     eapply nd_comp.
     eapply pf.
@@ -267,7 +268,8 @@ Section core2proof.
     eapply nd_comp.
     eapply nd_rule.
     eapply RArrange.
-    eapply RCanL.
+    eapply ACanR.
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
     apply curry.
     Defined.
 
@@ -337,7 +339,7 @@ Section core2proof.
       Defined.
 
     Definition mkGlob2 {Γ}{Δ}{l}{κ₁}{κ₂}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ ★) x y
-      : ND Rule [] [ Γ > Δ > [] |- [f x y @@ l] ].
+      : ND Rule [] [ Γ > Δ > [] |- [f x y ]@l ].
       apply nd_rule.
       refine (@RGlobal Γ Δ l 
         {| glob_wv    := coreVarToWeakExprVarOrError cv
@@ -356,7 +358,7 @@ Section core2proof.
       Defined.
 
     Definition mkGlob3 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ ★) x y z
-      : ND Rule [] [ Γ > Δ > [] |- [f x y z @@ l] ].
+      : ND Rule [] [ Γ > Δ > [] |- [f x y z ]@l ].
       apply nd_rule.
       refine (@RGlobal Γ Δ l 
         {| glob_wv    := coreVarToWeakExprVarOrError cv
@@ -376,7 +378,7 @@ Section core2proof.
       Defined.
 
     Definition mkGlob4 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}{κ₄}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ κ₄ -> HaskType Γ ★) x y z q
-      : ND Rule [] [ Γ > Δ > [] |- [f x y z q @@ l] ].
+      : ND Rule [] [ Γ > Δ > [] |- [f x y z q ] @l].
       apply nd_rule.
       refine (@RGlobal Γ Δ l 
         {| glob_wv    := coreVarToWeakExprVarOrError cv
@@ -417,10 +419,10 @@ Section core2proof.
     Definition hetmet_unflatten'  := coreVarToWeakExprVarOrError hetmet_unflatten.
     Definition hetmet_flattened_id'  := coreVarToWeakExprVarOrError hetmet_flattened_id.
 
-    Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
-      addErrorMessage ("input CoreSyn: " +++ toString ce)
-      (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
-        coreExprToWeakExpr ce >>= fun we =>
+    Definition coreToCoreExpr' (cex:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
+      addErrorMessage ("input CoreSyn: " +++ toString cex)
+      (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr cex)) (
+        coreExprToWeakExpr cex >>= fun we =>
           addErrorMessage ("WeakExpr: " +++ toString we)
             ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
               ((weakTypeOfWeakExpr we) >>= fun t =>
@@ -431,9 +433,9 @@ Section core2proof.
 
                       (addErrorMessage ("HaskStrong...")
                         (let haskProof := skolemize_and_flatten_proof hetmet_flatten' hetmet_unflatten'
-                                            hetmet_flattened_id' my_ga (@expr2proof _ _ _ _ _ _ e)
+                                            hetmet_flattened_id' my_ga (@expr2proof _ _ _ _ _ _ _ e)
                          in (* insert HaskProof-to-HaskProof manipulations here *)
-                         OK ((@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
+                         OK ((@proof2expr nat _ FreshNat _ _ (flatten_type τ) nil _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
                          >>= fun e' =>
                            (snd e') >>= fun e'' =>
                          strongExprToWeakExpr hetmet_brak' hetmet_esc'