X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FExtractionMain.v;h=e628f268153b1602c975584a4820bb5c2be96ac1;hp=dbeb3ccec21ea55152b6015ccd2fa9d0f529cd70;hb=b4857a6f575dffd5c9c9d5decbc21ff63a338270;hpb=e536cc4194f350ed6de5d465bcf53fda650b3d12

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index dbeb3cc..e628f26 100644
--- a/src/ExtractionMain.v
+++ b/src/ExtractionMain.v
@@ -13,7 +13,6 @@ Require Import Preamble.
 Require Import General.
 
 Require Import NaturalDeduction.
-Require Import NaturalDeductionToLatex.
 
 Require Import HaskKinds.
 Require Import HaskLiteralsAndTyCons.
@@ -34,13 +33,7 @@ Require Import HaskStrongToWeak.
 Require Import HaskWeakToCore.
 Require Import HaskProofToStrong.
 
-Require Import ProgrammingLanguage.
-
-Require Import HaskProofCategory.
-(*
-Require Import HaskStrongCategory.
-*)
-Require Import ReificationsIsomorphicToGeneralizedArrows.
+Require Import HaskFlattener.
 
 Open Scope string_scope.
 Extraction Language Haskell.
@@ -61,8 +54,7 @@ Extract Inductive unit    => "()" [ "()" ].
 Extract Inlined Constant string_dec => "(==)".
 Extract Inlined Constant ascii_dec => "(==)".
 
-(* adapted from ExtrOcamlString.v *)
-Extract Inductive ascii => "Char" [ "bin2ascii" ] "bin2ascii'".
+Extract Inductive ascii => "Char" [ "you_forgot_to_patch_coq" ] "you_forgot_to_patch_coq".
 Extract Constant zero   => "'\000'".
 Extract Constant one    => "'\001'".
 Extract Constant shift  => "shiftAscii".
@@ -108,28 +100,23 @@ Section core2proof.
       | WCoerVar _   => Prelude_error "top-level xi got a coercion variable"
     end.
 
-
-  (* core-to-string (-dcoqpass) *)
-
   Definition header : string :=
-    "\documentclass[9pt]{article}"+++eol+++
+    "\documentclass{article}"+++eol+++
     "\usepackage{amsmath}"+++eol+++
     "\usepackage{amssymb}"+++eol+++
     "\usepackage{proof}"+++eol+++
-    "\usepackage{mathpartir}   % http://cristal.inria.fr/~remy/latex/"+++eol+++
     "\usepackage{trfrac}       % http://www.utdallas.edu/~hamlen/trfrac.sty"+++eol+++
     "\def\code#1#2{\Box_{#1} #2}"+++eol+++
-    "\usepackage[paperwidth=200in,centering]{geometry}"+++eol+++
-    "\usepackage[displaymath,tightpage,active]{preview}"+++eol+++
+    "\usepackage[paperwidth=\maxdimen,paperheight=\maxdimen]{geometry}"+++eol+++
+    "\usepackage[tightpage,active]{preview}"+++eol+++
     "\begin{document}"+++eol+++
-    "\begin{preview}"+++eol.
+    "\setlength\PreviewBorder{5pt}"+++eol.
 
   Definition footer : string :=
-    eol+++"\end{preview}"+++
     eol+++"\end{document}"+++
     eol.
 
-
+  (* core-to-string (-dcoqpass) *)
   Definition coreToStringExpr' (ce:@CoreExpr CoreVar) : ???string :=
     addErrorMessage ("input CoreSyn: " +++ toString ce)
     (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
@@ -141,7 +128,12 @@ Section core2proof.
                 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
                   addErrorMessage ("HaskType: " +++ toString τ)
                   ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => false) τ nil we) >>= fun e =>
-                    OK (eol+++"$$"+++ toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ e))+++"$$"+++eol)
+                    OK (eol+++eol+++eol+++
+                        "\begin{preview}"+++eol+++
+                        "$\displaystyle "+++
+                        toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ e))+++
+                        " $"+++eol+++
+                        "\end{preview}"+++eol+++eol+++eol)
                   )))))))).
 
   Definition coreToStringExpr (ce:@CoreExpr CoreVar) : string :=
@@ -227,51 +219,218 @@ Section core2proof.
       exact O.
       apply t.
       Defined.
+(*
+    Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
+      addErrorMessage ("input CoreSyn: " +++ toString ce)
+      (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
+        coreExprToWeakExpr ce >>= fun we =>
+          addErrorMessage ("WeakExpr: " +++ toString we)
+            ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
+              ((weakTypeOfWeakExpr we) >>= fun t =>
+                (addErrorMessage ("WeakType: " +++ toString t)
+                  ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
+
+                    ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
+
+                      (addErrorMessage ("HaskStrong...")
+                        (let haskProof := (*flatten_proof'*) (@expr2proof _ _ _ _ _ _ e)
+                         in (* insert HaskProof-to-HaskProof manipulations here *)
+                         OK ((@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
+                         >>= fun e' =>
+                           (snd e') >>= fun e'' =>
+                         strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
+                           (projT2 e'') INil
+                         >>= fun q =>
+                           OK (weakExprToCoreExpr q)
+                    )))))))))).
+
+    Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) :=
+      match coreToCoreExpr' ce with
+        | OK x    => x
+        | Error s => Prelude_error s
+      end.
+  
+    Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar :=
+      match binds with
+        | CoreNonRec v e => CoreNonRec v (coreToCoreExpr e)
+        | CoreRec    lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
+      end.
 
-    Definition env := ★::nil.
-    Definition freshTV : HaskType env ★ := haskTyVarToType (FreshHaskTyVar _).
-    Definition idproof0 : ND Rule [] [env > nil > [] |- [freshTV--->freshTV @@ nil]].
-      eapply nd_comp.
-      eapply nd_comp.
-      eapply nd_rule.
-      apply RVar.
-      eapply nd_rule.
-      eapply (RURule _ _ _ _ (RuCanL _ _)) .
-      eapply nd_rule.
-      eapply RLam.
+    Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
+      map coreToCoreBind lbinds.
+  *)
+
+  End CoreToCore.
+
+  Definition coreVarToWeakExprVarOrError cv :=
+    match coreVarToWeakVar cv with
+      | WExprVar wv => wv
+      | _           => Prelude_error "IMPOSSIBLE"
+    end.
+
+  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) ].
+    eapply nd_comp; [ apply nd_rlecnac | idtac ].
+    apply nd_prod.    
+    apply nd_id.
+    apply nd_rule.
+    apply RVar.
+    Defined.
+
+  Definition fToC1 {Γ}{Δ}{a}{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 ].
+    apply curry.
+    Defined.
+
+  Definition fToC2 {Γ}{Δ}{a1}{a2}{s}{lev} :
+    ND Rule [] [ Γ > Δ >                       [] |- [a1 ---> (a2 ---> s) @@ lev ] ] ->
+    ND Rule [] [ Γ > Δ > [a1 @@ lev],,[a2 @@ lev] |-                 [ s @@ lev ] ].
+    intro pf.
+    eapply nd_comp.
+    eapply pf.
+    clear pf.
+    eapply nd_comp.
+    eapply curry.
+    eapply nd_comp.
+    eapply nd_rule.
+    eapply RArrange.
+    eapply RCanL.
+    apply curry.
+    Defined.
+
+  Section coqPassCoreToCore.
+    Context
+    (hetmet_brak  : CoreVar)
+    (hetmet_esc   : CoreVar)
+    (uniqueSupply : UniqSupply)
+    (lbinds:list (@CoreBind CoreVar))
+    (hetmet_PGArrowTyCon : TyFun)
+    (hetmet_pga_id : CoreVar)
+    (hetmet_pga_comp : CoreVar)
+    (hetmet_pga_first : CoreVar)
+    (hetmet_pga_second : CoreVar)
+    (hetmet_pga_cancell : CoreVar)
+    (hetmet_pga_cancelr : CoreVar)
+    (hetmet_pga_uncancell : CoreVar)
+    (hetmet_pga_uncancelr : CoreVar)
+    (hetmet_pga_assoc : CoreVar)
+    (hetmet_pga_unassoc : CoreVar)
+    (hetmet_pga_copy : CoreVar)
+    (hetmet_pga_drop : CoreVar)
+    (hetmet_pga_swap : CoreVar)
+    (hetmet_pga_applyl : CoreVar)
+    (hetmet_pga_applyr : CoreVar)
+    (hetmet_pga_curryl : CoreVar)
+    (hetmet_pga_curryr : CoreVar)
+    .
+
+    Definition ga_unit TV : RawHaskType TV ★ := @TyFunApp TV UnitTyCon nil         ★ TyFunApp_nil.
+    Definition ga_prod TV (a b:RawHaskType TV ★) : RawHaskType TV ★  :=
+      TApp (TApp (@TyFunApp TV PairTyCon nil _ TyFunApp_nil) a) b.
+    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 Γ ★ :=
+      fun TV ite => TApp (TApp (TApp (@TyFunApp TV 
+        hetmet_PGArrowTyCon
+        nil _ TyFunApp_nil) (a TV ite)) (b TV ite)) (c TV ite).
+
+    Definition mkGlob2' {Γ}{κ₁}{κ₂}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ ★) :
+      IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::nil) -> HaskType Γ ★.
+      intros.
+      inversion X; subst.
+      inversion X1; subst.
+      apply f; auto.
       Defined.
 
-(*
-    Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
-    addErrorMessage ("input CoreSyn: " +++ toString ce)
-    (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
-      coreExprToWeakExpr ce >>= fun we =>
-        addErrorMessage ("WeakExpr: " +++ toString we)
-          ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
-            ((weakTypeOfWeakExpr we) >>= fun t =>
-              (addErrorMessage ("WeakType: " +++ toString t)
-                ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
-                  addErrorMessage ("HaskType: " +++ toString τ)
-                  ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
-                        (let haskProof := @expr2proof _ _ _ _ _ _ e
-                          in (* insert HaskProof-to-HaskProof manipulations here *)
-                   (unFresh (@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof))
-                  >>= fun e' => Error (@toString _ (ExprToString _ _ _ _) (projT2 e'))
-(*
-                  >>= fun e' =>
-                    Prelude_error (@toString _ (@ExprToString nat _ _ _ _ _ _) (projT2 e'))
-  *)                  
-)
-)))))))).
-(*                    Error "X").*)
-(*
-                   strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
-                   (projT2 e')
-                         INil
-                         >>= fun q => Error (toString q)
-                  ))))))))).
-*)*)
+    Definition mkGlob2 {Γ}{Δ}{l}{κ₁}{κ₂}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ ★) x y
+      : ND Rule [] [ Γ > Δ > [] |- [f x y @@ l] ].
+      apply nd_rule.
+      refine (@RGlobal Γ Δ l 
+        {| glob_wv    := coreVarToWeakExprVarOrError cv
+          ; glob_kinds := κ₁ :: κ₂ :: nil
+          ; glob_tf    := mkGlob2'(Γ:=Γ) f
+          |} (ICons _ _ x (ICons _ _ y INil))).
+      Defined.
+
+    Definition mkGlob3' {Γ}{κ₁}{κ₂}{κ₃}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ ★) :
+      IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::κ₃::nil) -> HaskType Γ ★.
+      intros.
+      inversion X; subst.
+      inversion X1; subst.
+      inversion X3; subst.
+      apply f; auto.
+      Defined.
+
+    Definition mkGlob3 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ ★) x y z
+      : ND Rule [] [ Γ > Δ > [] |- [f x y z @@ l] ].
+      apply nd_rule.
+      refine (@RGlobal Γ Δ l 
+        {| glob_wv    := coreVarToWeakExprVarOrError cv
+          ; glob_kinds := κ₁ :: κ₂ :: κ₃ :: nil
+          ; glob_tf    := mkGlob3'(Γ:=Γ) f
+          |} (ICons _ _ x (ICons _ _ y (ICons _ _ z INil)))).
+      Defined.
 
+    Definition mkGlob4' {Γ}{κ₁}{κ₂}{κ₃}{κ₄}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ κ₄ -> HaskType Γ ★) :
+      IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::κ₃::κ₄::nil) -> HaskType Γ ★.
+      intros.
+      inversion X; subst.
+      inversion X1; subst.
+      inversion X3; subst.
+      inversion X5; subst.
+      apply f; auto.
+      Defined.
+
+    Definition mkGlob4 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}{κ₄}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ κ₄ -> HaskType Γ ★) x y z q
+      : ND Rule [] [ Γ > Δ > [] |- [f x y z q @@ l] ].
+      apply nd_rule.
+      refine (@RGlobal Γ Δ l 
+        {| glob_wv    := coreVarToWeakExprVarOrError cv
+          ; glob_kinds := κ₁ :: κ₂ :: κ₃ :: κ₄ :: nil
+          ; glob_tf    := mkGlob4'(Γ:=Γ) f
+          |} (ICons _ _ x (ICons _ _ y (ICons _ _ z (ICons _ _ q INil))))).
+      Defined.
+
+    Definition gat {Γ}(x:Tree ??(HaskType Γ ★))  := @ga_mk_tree ga_unit ga_prod _ x.
+
+    Instance my_ga : garrow ga_unit ga_prod (@ga_type) :=
+    { ga_id        := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_id        (fun ec a => ga_type' ec a a) ec (gat a)
+    ; ga_cancelr   := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_cancelr   (fun ec a => ga_type' ec _ a) ec (gat a)
+    ; ga_cancell   := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_cancell   (fun ec a => ga_type' ec _ a) ec (gat a)
+    ; ga_uncancelr := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_uncancelr (fun ec a => ga_type' ec a _) ec (gat a)
+    ; ga_uncancell := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_uncancell (fun ec a => ga_type' ec a _) ec (gat a)
+    ; ga_assoc     := fun Γ Δ ec l a b c => mkGlob4 hetmet_pga_assoc     (fun ec a b c => ga_type' ec _ _) ec (gat a) (gat b) (gat c)
+    ; ga_unassoc   := fun Γ Δ ec l a b c => mkGlob4 hetmet_pga_unassoc   (fun ec a b c => ga_type' ec _ _) ec (gat a) (gat b) (gat c)
+    ; ga_swap      := fun Γ Δ ec l a b   => mkGlob3 hetmet_pga_swap      (fun ec a b => ga_type' ec _ _) ec (gat a) (gat b)
+    ; ga_drop      := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_drop      (fun ec a => ga_type' ec _ _) ec (gat a)
+    ; ga_copy      := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_copy      (fun ec a => ga_type' ec _ _) ec (gat a)
+    ; ga_first     := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_first (fun ec a b c => _) ec (gat a) (gat b) (gat x))
+    ; ga_second    := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_second (fun ec a b c => _) ec (gat a) (gat b) (gat x))
+    ; ga_comp      := fun Γ Δ ec l a b c => fToC2 (mkGlob4 hetmet_pga_comp (fun ec a b c => _) ec (gat a) (gat b) (gat c))
+(*  ; ga_lit       := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_lit))*)
+(*  ; ga_curry     := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_curry))*)
+(*  ; ga_apply     := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_apply))*)
+(*  ; ga_kappa     := fun Γ Δ ec l a     => fToC1 (nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_kappa)))*)
+    ; ga_lit       := fun Γ Δ ec l a     => Prelude_error "ga_lit"
+    ; ga_curry     := fun Γ Δ ec l a b c => Prelude_error "ga_curry"
+    ; ga_apply     := fun Γ Δ ec l a b c => Prelude_error "ga_apply"
+    ; ga_kappa     := fun Γ Δ ec l a     => Prelude_error "ga_kappa"
+    }.
+
+    Definition hetmet_brak' := coreVarToWeakExprVarOrError hetmet_brak.
+    Definition hetmet_esc'  := coreVarToWeakExprVarOrError hetmet_esc.
 
     Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
       addErrorMessage ("input CoreSyn: " +++ toString ce)
@@ -286,12 +445,12 @@ Section core2proof.
                     ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
 
                       (addErrorMessage ("HaskStrong...")
-                        (let haskProof := @expr2proof _ _ _ _ _ _ e
+                        (let haskProof := flatten_proof my_ga (@expr2proof _ _ _ _ _ _ e)
                          in (* insert HaskProof-to-HaskProof manipulations here *)
                          OK ((@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
                          >>= fun e' =>
                            (snd e') >>= fun e'' =>
-                         strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
+                         strongExprToWeakExpr hetmet_brak' hetmet_esc' mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
                            (projT2 e'') INil
                          >>= fun q =>
                            OK (weakExprToCoreExpr q)
@@ -308,23 +467,59 @@ Section core2proof.
         | CoreNonRec v e => CoreNonRec v (coreToCoreExpr e)
         | CoreRec    lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
       end.
-  
+
     Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
       map coreToCoreBind lbinds.
 
-  End CoreToCore.
+  End coqPassCoreToCore.
 
-  Definition coqPassCoreToCore
+    Definition coqPassCoreToCore 
     (hetmet_brak  : CoreVar)
     (hetmet_esc   : CoreVar)
     (uniqueSupply : UniqSupply)
-    (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
-    match coreVarToWeakVar hetmet_brak with
-      | WExprVar hetmet_brak' => match coreVarToWeakVar hetmet_esc with
-                                   | WExprVar hetmet_esc' => coqPassCoreToCore' hetmet_brak' hetmet_esc' uniqueSupply lbinds
-                                   | _ => Prelude_error "IMPOSSIBLE"
-                                 end
-      | _ => Prelude_error "IMPOSSIBLE"
-    end.
+    (lbinds:list (@CoreBind CoreVar))
+    (hetmet_PGArrowTyCon : TyFun)
+    (hetmet_pga_id : CoreVar)
+    (hetmet_pga_comp : CoreVar)
+    (hetmet_pga_first : CoreVar)
+    (hetmet_pga_second : CoreVar)
+    (hetmet_pga_cancell : CoreVar)
+    (hetmet_pga_cancelr : CoreVar)
+    (hetmet_pga_uncancell : CoreVar)
+    (hetmet_pga_uncancelr : CoreVar)
+    (hetmet_pga_assoc : CoreVar)
+    (hetmet_pga_unassoc : CoreVar)
+    (hetmet_pga_copy : CoreVar)
+    (hetmet_pga_drop : CoreVar)
+    (hetmet_pga_swap : CoreVar)
+    (hetmet_pga_applyl : CoreVar)
+    (hetmet_pga_applyr : CoreVar)
+    (hetmet_pga_curryl : CoreVar)
+    (hetmet_pga_curryr : CoreVar) : list (@CoreBind CoreVar) :=
+    coqPassCoreToCore'
+       hetmet_brak  
+       hetmet_esc   
+       uniqueSupply 
+       hetmet_PGArrowTyCon
+       hetmet_pga_id 
+       hetmet_pga_comp 
+       hetmet_pga_first 
+       hetmet_pga_second 
+       hetmet_pga_cancell 
+       hetmet_pga_cancelr 
+       hetmet_pga_uncancell 
+       hetmet_pga_uncancelr 
+       hetmet_pga_assoc 
+       hetmet_pga_unassoc 
+       hetmet_pga_copy 
+       hetmet_pga_drop 
+       hetmet_pga_swap 
+       lbinds
+       (*
+       hetmet_pga_applyl 
+       hetmet_pga_applyr 
+       hetmet_pga_curryl 
+       *)
+       .
 
 End core2proof.