1 (*********************************************************************************************************************************)
4 (* This module is the "top level" for extraction *)
6 (*********************************************************************************************************************************)
8 Require Import Coq.Strings.Ascii.
9 Require Import Coq.Strings.String.
10 Require Import Coq.Lists.List.
12 Require Import Preamble.
13 Require Import General.
15 Require Import NaturalDeduction.
17 Require Import HaskKinds.
18 Require Import HaskLiterals.
19 Require Import HaskTyCons.
20 Require Import HaskCoreVars.
21 Require Import HaskCoreTypes.
22 Require Import HaskCore.
23 Require Import HaskWeakVars.
24 Require Import HaskWeakTypes.
25 Require Import HaskWeak.
26 Require Import HaskStrongTypes.
27 Require Import HaskStrong.
28 Require Import HaskProof.
29 Require Import HaskCoreToWeak.
30 Require Import HaskWeakToStrong.
31 Require Import HaskStrongToProof.
32 Require Import HaskProofToLatex.
33 Require Import HaskStrongToWeak.
34 Require Import HaskWeakToCore.
35 Require Import HaskProofToStrong.
37 Require Import HaskFlattener.
39 Open Scope string_scope.
40 Extraction Language Haskell.
42 (*Extract Inductive vec => "([])" [ "([])" "(:)" ].*)
43 (*Extract Inductive Tree => "([])" [ "([])" "(:)" ].*)
44 (*Extract Inlined Constant map => "Prelude.map".*)
46 (* I try to reuse Haskell types mostly to get the "deriving Show" aspect *)
47 Extract Inductive option => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ].
48 Extract Inductive list => "([])" [ "([])" "(:)" ].
49 Extract Inductive string => "Prelude.String" [ "[]" "(:)" ].
50 Extract Inductive prod => "(,)" [ "(,)" ].
51 Extract Inductive sum => "Prelude.Either" [ "Prelude.Left" "Prelude.Right" ].
52 Extract Inductive sumbool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
53 Extract Inductive bool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
54 Extract Inductive unit => "()" [ "()" ].
55 Extract Inlined Constant string_dec => "(==)".
56 Extract Inlined Constant ascii_dec => "(==)".
58 Extract Inductive ascii => "Char" [ "you_forgot_to_patch_coq" ] "you_forgot_to_patch_coq".
59 Extract Constant zero => "'\000'".
60 Extract Constant one => "'\001'".
61 Extract Constant shift => "shiftAscii".
63 Unset Extraction Optimize.
64 Unset Extraction AutoInline.
66 Variable Name : Type. Extract Inlined Constant Name => "Name.Name".
67 Variable mkSystemName : Unique -> string -> nat -> Name.
68 Extract Inlined Constant mkSystemName =>
69 "(\u s d -> Name.mkSystemName u (OccName.mkOccName (OccName.varNameDepth (nat2int d)) s))".
70 Variable mkTyVar : Name -> Kind -> CoreVar.
71 Extract Inlined Constant mkTyVar => "(\n k -> Var.mkTyVar n (kindToCoreKind k))".
72 Variable mkCoVar : Name -> CoreType -> CoreType -> CoreVar.
73 Extract Inlined Constant mkCoVar => "(\n t1 t2 -> Var.mkCoVar n (Coercion.mkCoKind t1 t2))".
74 Variable mkExVar : Name -> CoreType -> CoreVar.
75 Extract Inlined Constant mkExVar => "Id.mkLocalId".
78 Context (ce:@CoreExpr CoreVar).
80 Definition Γ : TypeEnv := nil.
82 Definition Δ : CoercionEnv Γ := nil.
84 Definition φ : TyVarResolver Γ :=
85 fun cv => Error ("unbound tyvar: " +++ toString (cv:CoreVar)).
86 (*fun tv => error ("tried to get the representative of an unbound tyvar:" +++ (getCoreVarOccString tv)).*)
88 Definition ψ : CoVarResolver Γ Δ :=
89 fun cv => Error ("tried to get the representative of an unbound covar!" (*+++ (getTypeVarOccString cv)*)).
91 (* We need to be able to resolve unbound exprvars, but we can be sure their types will have no
92 * free tyvars in them *)
93 Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ :=
94 match coreVarToWeakVar cv with
95 | WExprVar wev => match weakTypeToTypeOfKind φ wev ★ with
96 | Error s => Prelude_error ("Error converting weakType of top-level variable "+++
97 toString cv+++": " +++ s)
100 | WTypeVar _ => Prelude_error "top-level xi got a type variable"
101 | WCoerVar _ => Prelude_error "top-level xi got a coercion variable"
104 Definition header : string :=
105 "\documentclass{article}"+++eol+++
106 "\usepackage{amsmath}"+++eol+++
107 "\usepackage{amssymb}"+++eol+++
108 "\usepackage{proof}"+++eol+++
109 "\usepackage{trfrac} % http://www.utdallas.edu/~hamlen/trfrac.sty"+++eol+++
110 "\def\code#1#2{\Box_{#1} #2}"+++eol+++
111 "\usepackage[paperwidth=\maxdimen,paperheight=\maxdimen]{geometry}"+++eol+++
112 "\usepackage[tightpage,active]{preview}"+++eol+++
113 "\begin{document}"+++eol+++
114 "\setlength\PreviewBorder{5pt}"+++eol.
116 Definition footer : string :=
117 eol+++"\end{document}"+++
120 (* core-to-string (-dcoqpass) *)
121 Definition coreToStringExpr' (ce:@CoreExpr CoreVar) : ???string :=
122 addErrorMessage ("input CoreSyn: " +++ toString ce)
123 (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
124 coreExprToWeakExpr ce >>= fun we =>
125 addErrorMessage ("WeakExpr: " +++ toString we)
126 ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
127 ((weakTypeOfWeakExpr we) >>= fun t =>
128 (addErrorMessage ("WeakType: " +++ toString t)
129 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
130 addErrorMessage ("HaskType: " +++ toString τ)
131 ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => false) τ nil we) >>= fun e =>
132 OK (eol+++eol+++eol+++
133 "\begin{preview}"+++eol+++
135 toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ e))+++
137 "\end{preview}"+++eol+++eol+++eol)
140 Definition coreToStringExpr (ce:@CoreExpr CoreVar) : string :=
141 match coreToStringExpr' ce with
143 | Error s => Prelude_error s
146 Definition coreToStringBind (binds:@CoreBind CoreVar) : string :=
148 | CoreNonRec _ e => coreToStringExpr e
149 | CoreRec lbe => fold_left (fun x y => x+++eol+++eol+++y) (map (fun x => coreToStringExpr (snd x)) lbe) ""
152 Definition coqPassCoreToString (lbinds:list (@CoreBind CoreVar)) : string :=
154 (fold_left (fun x y => x+++eol+++eol+++y) (map coreToStringBind lbinds) "")
158 (* core-to-core (-fcoqpass) *)
161 Definition mkWeakTypeVar (u:Unique)(k:Kind) : WeakTypeVar :=
162 weakTypeVar (mkTyVar (mkSystemName u "tv" O) k) k.
163 Definition mkWeakCoerVar (u:Unique)(k:Kind)(t1 t2:WeakType) : WeakCoerVar :=
164 weakCoerVar (mkCoVar (mkSystemName u "cv" O) (weakTypeToCoreType t1) (weakTypeToCoreType t2)) t1 t2.
165 Definition mkWeakExprVar (u:Unique)(t:WeakType) : WeakExprVar :=
166 weakExprVar (mkExVar (mkSystemName u "ev" O) (weakTypeToCoreType t)) t.
168 Context (hetmet_brak : WeakExprVar).
169 Context (hetmet_esc : WeakExprVar).
170 Context (hetmet_flatten : WeakExprVar).
171 Context (hetmet_unflatten : WeakExprVar).
172 Context (hetmet_flattened_id : WeakExprVar).
173 Context (uniqueSupply : UniqSupply).
175 Definition useUniqueSupply {T}(ut:UniqM T) : ???T :=
178 f uniqueSupply >>= fun x => OK (snd x)
181 Definition larger : forall ln:list nat, { n:nat & forall n', In n' ln -> gt n n' }.
187 destruct IHln as [n pf].
188 exists (plus (S n) a).
192 fold (@In _ n' ln) in H.
197 Definition FreshNat : @FreshMonad nat.
198 refine {| FMT := fun T => nat -> prod nat T
204 set (larger tl) as q.
205 destruct q as [n' pf].
211 refine {| returnM := fun a (v:a) => _ |}.
212 intro n. exact (n,v).
215 destruct q as [n' v].
220 Definition unFresh {T} : @FreshM _ FreshNat T -> T.
229 Definition coreVarToWeakExprVarOrError cv :=
230 match coreVarToWeakVar cv with
232 | _ => Prelude_error "IMPOSSIBLE"
235 Definition curry {Γ}{Δ}{a}{s}{Σ}{lev} :
237 [ Γ > Δ > Σ |- [a ---> s ]@lev ]
238 [ Γ > Δ > [a @@ lev],,Σ |- [ s ]@lev ].
239 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
240 eapply nd_comp; [ idtac | eapply nd_rule; eapply RApp ].
241 eapply nd_comp; [ apply nd_rlecnac | idtac ].
248 Definition fToC1 {Γ}{Δ}{a}{s}{lev} :
249 ND Rule [] [ Γ > Δ > [ ] |- [a ---> s ]@lev ] ->
250 ND Rule [] [ Γ > Δ > [a @@ lev] |- [ s ]@lev ].
254 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ].
258 Definition fToC2 {Γ}{Δ}{a1}{a2}{s}{lev} :
259 ND Rule [] [ Γ > Δ > [] |- [a1 ---> (a2 ---> s) ]@lev ] ->
260 ND Rule [] [ Γ > Δ > [a1 @@ lev],,[a2 @@ lev] |- [ s ]@lev ].
271 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
275 Section coqPassCoreToCore.
277 (hetmet_brak : CoreVar)
278 (hetmet_esc : CoreVar)
279 (hetmet_flatten : CoreVar)
280 (hetmet_unflatten : CoreVar)
281 (hetmet_flattened_id : CoreVar)
282 (uniqueSupply : UniqSupply)
283 (lbinds:list (@CoreBind CoreVar))
284 (hetmet_PGArrowTyCon : TyFun)
285 (hetmet_PGArrow_unit_TyCon : TyFun)
286 (hetmet_PGArrow_tensor_TyCon : TyFun)
287 (hetmet_PGArrow_exponent_TyCon : TyFun)
288 (hetmet_pga_id : CoreVar)
289 (hetmet_pga_comp : CoreVar)
290 (hetmet_pga_first : CoreVar)
291 (hetmet_pga_second : CoreVar)
292 (hetmet_pga_cancell : CoreVar)
293 (hetmet_pga_cancelr : CoreVar)
294 (hetmet_pga_uncancell : CoreVar)
295 (hetmet_pga_uncancelr : CoreVar)
296 (hetmet_pga_assoc : CoreVar)
297 (hetmet_pga_unassoc : CoreVar)
298 (hetmet_pga_copy : CoreVar)
299 (hetmet_pga_drop : CoreVar)
300 (hetmet_pga_swap : CoreVar)
301 (hetmet_pga_applyl : CoreVar)
302 (hetmet_pga_applyr : CoreVar)
303 (hetmet_pga_curryl : CoreVar)
304 (hetmet_pga_curryr : CoreVar)
308 Definition ga_unit TV (ec:RawHaskType TV ECKind) : RawHaskType TV ★ :=
309 @TyFunApp TV hetmet_PGArrow_unit_TyCon (ECKind::nil) ★ (TyFunApp_cons _ _ ec TyFunApp_nil).
311 Definition ga_prod TV (ec:RawHaskType TV ECKind) (a b:RawHaskType TV ★) : RawHaskType TV ★ :=
313 hetmet_PGArrow_tensor_TyCon
314 (ECKind::★ ::★ ::nil) ★
315 (TyFunApp_cons _ _ ec
320 Definition ga_type {TV}(a:RawHaskType TV ECKind)(b c:RawHaskType TV ★) : RawHaskType TV ★ :=
321 TApp (TApp (TApp (@TyFunApp TV
323 nil _ TyFunApp_nil) a) b) c.
325 Definition ga := @ga_mk ga_unit ga_prod (@ga_type).
327 Definition ga_type' {Γ}(a:HaskType Γ ECKind)(b c:HaskType Γ ★) : HaskType Γ ★ :=
328 fun TV ite => TApp (TApp (TApp (@TyFunApp TV
330 nil _ TyFunApp_nil) (a TV ite)) (b TV ite)) (c TV ite).
332 Definition mkGlob2' {Γ}{κ₁}{κ₂}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ ★) :
333 IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::nil) -> HaskType Γ ★.
340 Definition mkGlob2 {Γ}{Δ}{l}{κ₁}{κ₂}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ ★) x y
341 : ND Rule [] [ Γ > Δ > [] |- [f x y ]@l ].
343 refine (@RGlobal Γ Δ l
344 {| glob_wv := coreVarToWeakExprVarOrError cv
345 ; glob_kinds := κ₁ :: κ₂ :: nil
346 ; glob_tf := mkGlob2'(Γ:=Γ) f
347 |} (ICons _ _ x (ICons _ _ y INil))).
350 Definition mkGlob3' {Γ}{κ₁}{κ₂}{κ₃}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ ★) :
351 IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::κ₃::nil) -> HaskType Γ ★.
359 Definition mkGlob3 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ ★) x y z
360 : ND Rule [] [ Γ > Δ > [] |- [f x y z ]@l ].
362 refine (@RGlobal Γ Δ l
363 {| glob_wv := coreVarToWeakExprVarOrError cv
364 ; glob_kinds := κ₁ :: κ₂ :: κ₃ :: nil
365 ; glob_tf := mkGlob3'(Γ:=Γ) f
366 |} (ICons _ _ x (ICons _ _ y (ICons _ _ z INil)))).
369 Definition mkGlob4' {Γ}{κ₁}{κ₂}{κ₃}{κ₄}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ κ₄ -> HaskType Γ ★) :
370 IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::κ₃::κ₄::nil) -> HaskType Γ ★.
379 Definition mkGlob4 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}{κ₄}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ κ₄ -> HaskType Γ ★) x y z q
380 : ND Rule [] [ Γ > Δ > [] |- [f x y z q ] @l].
382 refine (@RGlobal Γ Δ l
383 {| glob_wv := coreVarToWeakExprVarOrError cv
384 ; glob_kinds := κ₁ :: κ₂ :: κ₃ :: κ₄ :: nil
385 ; glob_tf := mkGlob4'(Γ:=Γ) f
386 |} (ICons _ _ x (ICons _ _ y (ICons _ _ z (ICons _ _ q INil))))).
389 Definition gat {Γ} ec (x:Tree ??(HaskType Γ ★)) := @ga_mk_tree ga_unit ga_prod _ ec x.
391 Instance my_ga : garrow ga_unit ga_prod (@ga_type) :=
392 { ga_id := fun Γ Δ ec l a => mkGlob2 hetmet_pga_id (fun ec a => ga_type' ec a a) ec (gat ec a)
393 ; ga_cancelr := fun Γ Δ ec l a => mkGlob2 hetmet_pga_cancelr (fun ec a => ga_type' ec _ a) ec (gat ec a)
394 ; ga_cancell := fun Γ Δ ec l a => mkGlob2 hetmet_pga_cancell (fun ec a => ga_type' ec _ a) ec (gat ec a)
395 ; ga_uncancelr := fun Γ Δ ec l a => mkGlob2 hetmet_pga_uncancelr (fun ec a => ga_type' ec a _) ec (gat ec a)
396 ; ga_uncancell := fun Γ Δ ec l a => mkGlob2 hetmet_pga_uncancell (fun ec a => ga_type' ec a _) ec (gat ec a)
397 ; 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)
398 ; 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)
399 ; 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)
400 ; ga_drop := fun Γ Δ ec l a => mkGlob2 hetmet_pga_drop (fun ec a => ga_type' ec _ _) ec (gat ec a)
401 ; ga_copy := fun Γ Δ ec l a => mkGlob2 hetmet_pga_copy (fun ec a => ga_type' ec _ _) ec (gat ec a)
402 ; 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))
403 ; 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))
404 ; 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))
405 (* ; ga_lit := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_lit))*)
406 (* ; ga_curry := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_curry))*)
407 (* ; ga_apply := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_apply))*)
408 (* ; ga_kappa := fun Γ Δ ec l a => fToC1 (nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_kappa)))*)
409 ; ga_lit := fun Γ Δ ec l a => Prelude_error "ga_lit"
410 ; ga_curry := fun Γ Δ ec l a b c => Prelude_error "ga_curry"
411 ; ga_apply := fun Γ Δ ec l a b c => Prelude_error "ga_apply"
412 ; ga_kappa := fun Γ Δ ec l a => Prelude_error "ga_kappa"
415 Definition hetmet_brak' := coreVarToWeakExprVarOrError hetmet_brak.
416 Definition hetmet_esc' := coreVarToWeakExprVarOrError hetmet_esc.
417 Definition hetmet_flatten' := coreVarToWeakExprVarOrError hetmet_flatten.
418 Definition hetmet_unflatten' := coreVarToWeakExprVarOrError hetmet_unflatten.
419 Definition hetmet_flattened_id' := coreVarToWeakExprVarOrError hetmet_flattened_id.
421 Definition coreToCoreExpr' (cex:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
422 addErrorMessage ("input CoreSyn: " +++ toString cex)
423 (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr cex)) (
424 coreExprToWeakExpr cex >>= fun we =>
425 addErrorMessage ("WeakExpr: " +++ toString we)
426 ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
427 ((weakTypeOfWeakExpr we) >>= fun t =>
428 (addErrorMessage ("WeakType: " +++ toString t)
429 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
431 ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
433 (addErrorMessage ("HaskStrong...")
434 (let haskProof := skolemize_and_flatten_proof hetmet_flatten' hetmet_unflatten'
435 hetmet_flattened_id' my_ga (@expr2proof _ _ _ _ _ _ e)
436 in (* insert HaskProof-to-HaskProof manipulations here *)
437 OK ((@proof2expr nat _ FreshNat _ _ (flatten_type τ@@nil) _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
439 (snd e') >>= fun e'' =>
440 strongExprToWeakExpr hetmet_brak' hetmet_esc'
441 mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
444 OK (weakExprToCoreExpr q)
447 Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) :=
448 match coreToCoreExpr' ce with
450 | Error s => Prelude_error s
453 Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar :=
455 | CoreNonRec v e => let e' := coreToCoreExpr e in CoreNonRec (setVarType v (coreTypeOfCoreExpr e')) e'
457 | CoreRec lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
458 (* FIXME: doesn't deal with the case where top level recursive binds change type *)
460 match coreToCoreExpr (CoreELet lbe) (CoreELit HaskMachNullAddr) with
461 | CoreELet (CoreRec lbe') => lbe'
463 ("coreToCoreExpr was given a letrec, " +++
464 "but returned something that wasn't a letrec: " +++ toString x)
469 Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
470 map coreToCoreBind lbinds.
472 End coqPassCoreToCore.
474 Definition coqPassCoreToCore
475 (hetmet_brak : CoreVar)
476 (hetmet_esc : CoreVar)
477 (hetmet_flatten : CoreVar)
478 (hetmet_unflatten : CoreVar)
479 (hetmet_flattened_id : CoreVar)
480 (uniqueSupply : UniqSupply)
481 (lbinds:list (@CoreBind CoreVar))
482 (hetmet_PGArrowTyCon : TyFun)
483 (hetmet_PGArrow_unit_TyCon : TyFun)
484 (hetmet_PGArrow_tensor_TyCon : TyFun)
485 (hetmet_PGArrow_exponent_TyCon : TyFun)
486 (hetmet_pga_id : CoreVar)
487 (hetmet_pga_comp : CoreVar)
488 (hetmet_pga_first : CoreVar)
489 (hetmet_pga_second : CoreVar)
490 (hetmet_pga_cancell : CoreVar)
491 (hetmet_pga_cancelr : CoreVar)
492 (hetmet_pga_uncancell : CoreVar)
493 (hetmet_pga_uncancelr : CoreVar)
494 (hetmet_pga_assoc : CoreVar)
495 (hetmet_pga_unassoc : CoreVar)
496 (hetmet_pga_copy : CoreVar)
497 (hetmet_pga_drop : CoreVar)
498 (hetmet_pga_swap : CoreVar)
499 (hetmet_pga_applyl : CoreVar)
500 (hetmet_pga_applyr : CoreVar)
501 (hetmet_pga_curryl : CoreVar)
502 (hetmet_pga_curryr : CoreVar) : list (@CoreBind CoreVar) :=
511 hetmet_PGArrow_unit_TyCon
512 hetmet_PGArrow_tensor_TyCon
513 (* hetmet_PGArrow_exponent_TyCon*)