X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FExtractionMain.v;h=5be52807b489dfd1a977f4c20bc077d361130385;hp=05d059a81b4fc4c78b73ab23d3868cac0fc6cf60;hb=c64ac559ed9448b8aa24abedbc2ad5ca800d1d24;hpb=20a9b4934a97e6801d6785ac940f771cb74a8cc1 diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v index 05d059a..5be5280 100644 --- a/src/ExtractionMain.v +++ b/src/ExtractionMain.v @@ -13,10 +13,10 @@ Require Import Preamble. Require Import General. Require Import NaturalDeduction. -Require Import NaturalDeductionToLatex. Require Import HaskKinds. -Require Import HaskLiteralsAndTyCons. +Require Import HaskLiterals. +Require Import HaskTyCons. Require Import HaskCoreVars. Require Import HaskCoreTypes. Require Import HaskCore. @@ -34,13 +34,7 @@ Require Import HaskStrongToWeak. Require Import HaskWeakToCore. Require Import HaskProofToStrong. -Require Import ProgrammingLanguage. - -Require Import HaskProofCategory. -(* -Require Import HaskStrongCategory. -*) -Require Import ReificationsEquivalentToGeneralizedArrows. +Require Import HaskFlattener. Open Scope string_scope. Extraction Language Haskell. @@ -61,8 +55,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 +101,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 +129,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 := @@ -168,13 +161,16 @@ Section core2proof. Definition mkWeakTypeVar (u:Unique)(k:Kind) : WeakTypeVar := weakTypeVar (mkTyVar (mkSystemName u "tv" O) k) k. Definition mkWeakCoerVar (u:Unique)(k:Kind)(t1 t2:WeakType) : WeakCoerVar := - weakCoerVar (mkCoVar (mkSystemName u "cv" O) (weakTypeToCoreType t1) (weakTypeToCoreType t2)) k t1 t2. + weakCoerVar (mkCoVar (mkSystemName u "cv" O) (weakTypeToCoreType t1) (weakTypeToCoreType t2)) t1 t2. Definition mkWeakExprVar (u:Unique)(t:WeakType) : WeakExprVar := weakExprVar (mkExVar (mkSystemName u "ev" O) (weakTypeToCoreType t)) t. - Context (hetmet_brak : WeakExprVar). - Context (hetmet_esc : WeakExprVar). - Context (uniqueSupply : UniqSupply). + Context (hetmet_brak : WeakExprVar). + Context (hetmet_esc : WeakExprVar). + Context (hetmet_flatten : WeakExprVar). + Context (hetmet_unflatten : WeakExprVar). + Context (hetmet_flattened_id : WeakExprVar). + Context (uniqueSupply : UniqSupply). Definition useUniqueSupply {T}(ut:UniqM T) : ???T := match ut with @@ -228,50 +224,198 @@ Section core2proof. apply t. Defined. - 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. + 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; 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} : + 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) + (hetmet_flatten : CoreVar) + (hetmet_unflatten : CoreVar) + (hetmet_flattened_id : CoreVar) + (uniqueSupply : UniqSupply) + (lbinds:list (@CoreBind CoreVar)) + (hetmet_PGArrowTyCon : TyFun) + (hetmet_PGArrow_unit_TyCon : TyFun) + (hetmet_PGArrow_tensor_TyCon : TyFun) + (hetmet_PGArrow_exponent_TyCon : 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 (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 ★ := + (@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 Γ ★ := + 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 {Γ} ec (x:Tree ??(HaskType Γ ★)) := @ga_mk_tree ga_unit ga_prod _ ec 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 ec a) + ; ga_cancelr := fun Γ Δ ec l a => mkGlob2 hetmet_pga_cancelr (fun ec a => ga_type' ec _ a) ec (gat ec a) + ; ga_cancell := fun Γ Δ ec l a => mkGlob2 hetmet_pga_cancell (fun ec a => ga_type' ec _ a) ec (gat ec a) + ; ga_uncancelr := fun Γ Δ ec l a => mkGlob2 hetmet_pga_uncancelr (fun ec a => ga_type' ec a _) ec (gat ec a) + ; ga_uncancell := fun Γ Δ ec l a => mkGlob2 hetmet_pga_uncancell (fun ec a => ga_type' ec a _) ec (gat ec a) + ; ga_assoc := fun Γ Δ ec l a b c => mkGlob4 hetmet_pga_assoc (fun ec a b c => ga_type' ec _ _) ec (gat ec a) (gat ec b) (gat ec c) + ; ga_unassoc := fun Γ Δ ec l a b c => mkGlob4 hetmet_pga_unassoc (fun ec a b c => ga_type' ec _ _) ec (gat ec a) (gat ec b) (gat ec c) + ; ga_swap := fun Γ Δ ec l a b => mkGlob3 hetmet_pga_swap (fun ec a b => ga_type' ec _ _) ec (gat ec a) (gat ec b) + ; ga_drop := fun Γ Δ ec l a => mkGlob2 hetmet_pga_drop (fun ec a => ga_type' ec _ _) ec (gat ec a) + ; ga_copy := fun Γ Δ ec l a => mkGlob2 hetmet_pga_copy (fun ec a => ga_type' ec _ _) ec (gat ec a) + ; ga_first := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_first (fun ec a b c => _) ec (gat ec a) (gat ec b) (gat ec x)) + ; ga_second := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_second (fun ec a b c => _) ec (gat ec a) (gat ec b) (gat ec x)) + ; ga_comp := fun Γ Δ ec l a b c => fToC2 (mkGlob4 hetmet_pga_comp (fun ec a b c => _) ec (gat ec a) (gat ec b) (gat ec 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 hetmet_flatten' := coreVarToWeakExprVarOrError hetmet_flatten. + 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) @@ -286,12 +430,14 @@ Section core2proof. ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e => (addErrorMessage ("HaskStrong...") - (let haskProof := @expr2proof _ _ _ _ _ _ e + (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) >>= 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) @@ -302,29 +448,88 @@ Section core2proof. | 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) + | CoreNonRec v e => let e' := coreToCoreExpr e in CoreNonRec (setVarType v (coreTypeOfCoreExpr e')) e' + | CoreRec lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe) + (* FIXME: doesn't deal with the case where top level recursive binds change type *) +(* + match coreToCoreExpr (CoreELet lbe) (CoreELit HaskMachNullAddr) with + | CoreELet (CoreRec lbe') => lbe' + | x => Prelude_error + ("coreToCoreExpr was given a letrec, " +++ + "but returned something that wasn't a letrec: " +++ toString x) + end +*) 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) + (hetmet_flatten : CoreVar) + (hetmet_unflatten : CoreVar) + (hetmet_flattened_id : 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_PGArrow_unit_TyCon : TyFun) + (hetmet_PGArrow_tensor_TyCon : TyFun) + (hetmet_PGArrow_exponent_TyCon : 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 + hetmet_flatten + hetmet_unflatten + hetmet_flattened_id + uniqueSupply + hetmet_PGArrowTyCon + hetmet_PGArrow_unit_TyCon + hetmet_PGArrow_tensor_TyCon +(* hetmet_PGArrow_exponent_TyCon*) + 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.