update Demo.hs

[coq-hetmet.git] / src / ExtractionMain.v

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index 3cd8ff6..6364a5a 100644 (file)
--- a/src/ExtractionMain.v
+++ b/src/ExtractionMain.v
@@ -235,10 +235,11 @@ Section core2proof.
   Definition curry {Γ}{Δ}{a}{s}{Σ}{lev} :
     ND Rule 
        [ Γ > Δ > Σ             |- [a ---> s @@ lev ] ]
-       [ Γ > Δ > Σ,,[a @@ lev] |-       [ s @@ lev ] ].
-    eapply nd_comp; [ idtac | eapply nd_rule; apply (@RApp Γ Δ Σ [a@@lev] a s lev) ].
+       [ Γ > Δ > [a @@ lev],,Σ |-       [ s @@ lev ] ].
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RApp ].
     eapply nd_comp; [ apply nd_rlecnac | idtac ].
-    apply nd_prod.    
+    apply nd_prod.
     apply nd_id.
     apply nd_rule.
     apply RVar.
@@ -250,13 +251,13 @@ Section core2proof.
     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 RCanR ].
     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 @@ lev],,[a2 @@ lev] |-                  [ s @@ lev ] ].
     intro pf.
     eapply nd_comp.
     eapply pf.
@@ -266,7 +267,8 @@ Section core2proof.
     eapply nd_comp.
     eapply nd_rule.
     eapply RArrange.
-    eapply RCanL.
+    eapply RCanR.
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
     apply curry.
     Defined.
 
@@ -305,12 +307,21 @@ Section core2proof.
 
     Definition ga_unit TV (ec:RawHaskType TV ECKind) : RawHaskType TV ★ :=
       @TyFunApp TV hetmet_PGArrow_unit_TyCon (ECKind::nil) ★ (TyFunApp_cons _ _ ec TyFunApp_nil).
+
     Definition ga_prod TV (ec:RawHaskType TV ECKind) (a b:RawHaskType TV ★) : RawHaskType TV ★  :=
-      TApp (TApp (@TyFunApp TV hetmet_PGArrow_tensor_TyCon (ECKind::nil) _ (TyFunApp_cons _ _ ec TyFunApp_nil)) a) b.
+      (@TyFunApp TV
+        hetmet_PGArrow_tensor_TyCon
+        (ECKind::★ ::★ ::nil) ★
+        (TyFunApp_cons _ _ ec
+          (TyFunApp_cons _ _ a
+            (TyFunApp_cons _ _ b
+          TyFunApp_nil)))).
+
     Definition ga_type {TV}(a:RawHaskType TV ECKind)(b c:RawHaskType TV ★) : RawHaskType TV ★ :=
       TApp (TApp (TApp (@TyFunApp TV 
         hetmet_PGArrowTyCon
         nil _ TyFunApp_nil) a) b) c.
+
     Definition ga := @ga_mk ga_unit ga_prod (@ga_type).
 
     Definition ga_type' {Γ}(a:HaskType Γ ECKind)(b c:HaskType Γ ★) : HaskType Γ ★ :=
@@ -420,7 +431,7 @@ Section core2proof.
                     ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
 
                       (addErrorMessage ("HaskStrong...")
-                        (let haskProof := flatten_proof hetmet_flatten' hetmet_unflatten'
+                        (let haskProof := skolemize_and_flatten_proof hetmet_flatten' hetmet_unflatten'
                                             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)
@@ -519,6 +530,7 @@ Section core2proof.
        hetmet_pga_applyr 
        hetmet_pga_curryl 
        *)
+
        .
 
 End core2proof.