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.
16 Require Import NaturalDeductionContext.
18 Require Import HaskKinds.
19 Require Import HaskLiterals.
20 Require Import HaskTyCons.
21 Require Import HaskCoreVars.
22 Require Import HaskCoreTypes.
23 Require Import HaskCore.
24 Require Import HaskWeakVars.
25 Require Import HaskWeakTypes.
26 Require Import HaskWeak.
27 Require Import HaskStrongTypes.
28 Require Import HaskStrong.
29 Require Import HaskProof.
30 Require Import HaskCoreToWeak.
31 Require Import HaskWeakToStrong.
32 Require Import HaskStrongToProof.
33 Require Import HaskProofToLatex.
34 Require Import HaskStrongToWeak.
35 Require Import HaskWeakToCore.
36 Require Import HaskProofToStrong.
38 Require Import HaskFlattener.
40 Open Scope string_scope.
41 Extraction Language Haskell.
43 (*Extract Inductive vec => "([])" [ "([])" "(:)" ].*)
44 (*Extract Inductive Tree => "([])" [ "([])" "(:)" ].*)
45 (*Extract Inlined Constant map => "Prelude.map".*)
47 (* I try to reuse Haskell types mostly to get the "deriving Show" aspect *)
48 Extract Inductive option => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ].
49 Extract Inductive list => "([])" [ "([])" "(:)" ].
50 Extract Inductive string => "Prelude.String" [ "[]" "(:)" ].
51 Extract Inductive prod => "(,)" [ "(,)" ].
52 Extract Inductive sum => "Prelude.Either" [ "Prelude.Left" "Prelude.Right" ].
53 Extract Inductive sumbool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
54 Extract Inductive bool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
55 Extract Inductive unit => "()" [ "()" ].
56 Extract Inlined Constant string_dec => "(==)".
57 Extract Inlined Constant ascii_dec => "(==)".
59 Extract Inductive ascii => "Char" [ "you_forgot_to_patch_coq" ] "you_forgot_to_patch_coq".
60 Extract Constant zero => "'\000'".
61 Extract Constant one => "'\001'".
62 Extract Constant shift => "shiftAscii".
64 Unset Extraction Optimize.
65 Unset Extraction AutoInline.
67 Variable Name : Type. Extract Inlined Constant Name => "Name.Name".
68 Variable mkSystemName : Unique -> string -> nat -> Name.
69 Extract Inlined Constant mkSystemName =>
70 "(\u s d -> Name.mkSystemName u (OccName.mkOccName (OccName.varNameDepth (nat2int d)) s))".
71 Variable mkTyVar : Name -> Kind -> CoreVar.
72 Extract Inlined Constant mkTyVar => "(\n k -> Var.mkTyVar n (kindToCoreKind k))".
73 Variable mkCoVar : Name -> CoreType -> CoreType -> CoreVar.
74 Extract Inlined Constant mkCoVar => "(\n t1 t2 -> Var.mkCoVar n (Coercion.mkCoKind t1 t2))".
75 Variable mkExVar : Name -> CoreType -> CoreVar.
76 Extract Inlined Constant mkExVar => "Id.mkLocalId".
79 Context (ce:@CoreExpr CoreVar).
81 Definition Γ : TypeEnv := nil.
83 Definition Δ : CoercionEnv Γ := nil.
85 Definition φ : TyVarResolver Γ :=
86 fun cv => Error ("unbound tyvar: " +++ toString (cv:CoreVar)).
87 (*fun tv => error ("tried to get the representative of an unbound tyvar:" +++ (getCoreVarOccString tv)).*)
89 Definition ψ : CoVarResolver Γ Δ :=
90 fun cv => Error ("tried to get the representative of an unbound covar!" (*+++ (getTypeVarOccString cv)*)).
92 (* We need to be able to resolve unbound exprvars, but we can be sure their types will have no
93 * free tyvars in them *)
94 Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ :=
95 match coreVarToWeakVar cv with
96 | WExprVar wev => match weakTypeToTypeOfKind φ wev ★ with
97 | Error s => Prelude_error ("Error converting weakType of top-level variable "+++
98 toString cv+++": " +++ s)
101 | WTypeVar _ => Prelude_error "top-level xi got a type variable"
102 | WCoerVar _ => Prelude_error "top-level xi got a coercion variable"
105 Definition header : string :=
106 "\documentclass{article}"+++eol+++
107 "\usepackage{amsmath}"+++eol+++
108 "\usepackage{amssymb}"+++eol+++
109 "\usepackage{proof}"+++eol+++
110 "\usepackage{trfrac} % http://www.utdallas.edu/~hamlen/trfrac.sty"+++eol+++
111 "\def\code#1#2{\Box_{#1} #2}"+++eol+++
112 "\usepackage[paperwidth=\maxdimen,paperheight=\maxdimen]{geometry}"+++eol+++
113 "\usepackage[tightpage,active]{preview}"+++eol+++
114 "\begin{document}"+++eol+++
115 "\setlength\PreviewBorder{5pt}"+++eol.
117 Definition footer : string :=
118 eol+++"\end{document}"+++
121 (* core-to-string (-dcoqpass) *)
122 Definition coreToStringExpr' (ce:@CoreExpr CoreVar) : ???string :=
123 addErrorMessage ("input CoreSyn: " +++ toString ce)
124 (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
125 coreExprToWeakExpr ce >>= fun we =>
126 addErrorMessage ("WeakExpr: " +++ toString we)
127 ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
128 ((weakTypeOfWeakExpr we) >>= fun t =>
129 (addErrorMessage ("WeakType: " +++ toString t)
130 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
131 addErrorMessage ("HaskType: " +++ toString τ)
132 ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => false) τ nil we) >>= fun e =>
133 OK (eol+++eol+++eol+++
134 "\begin{preview}"+++eol+++
136 toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ _ e))+++
138 "\end{preview}"+++eol+++eol+++eol)
141 Definition coreToStringExpr (ce:@CoreExpr CoreVar) : string :=
142 match coreToStringExpr' ce with
144 | Error s => Prelude_error s
147 Definition coreToStringBind (binds:@CoreBind CoreVar) : string :=
149 | CoreNonRec _ e => coreToStringExpr e
150 | CoreRec lbe => fold_left (fun x y => x+++eol+++eol+++y) (map (fun x => coreToStringExpr (snd x)) lbe) ""
153 Definition coqPassCoreToString (lbinds:list (@CoreBind CoreVar)) : string :=
155 (fold_left (fun x y => x+++eol+++eol+++y) (map coreToStringBind lbinds) "")
159 (* core-to-core (-fcoqpass) *)
162 Definition mkWeakTypeVar (u:Unique)(k:Kind) : WeakTypeVar :=
163 weakTypeVar (mkTyVar (mkSystemName u "tv" O) k) k.
164 Definition mkWeakCoerVar (u:Unique)(k:Kind)(t1 t2:WeakType) : WeakCoerVar :=
165 weakCoerVar (mkCoVar (mkSystemName u "cv" O) (weakTypeToCoreType t1) (weakTypeToCoreType t2)) t1 t2.
166 Definition mkWeakExprVar (u:Unique)(t:WeakType) : WeakExprVar :=
167 weakExprVar (mkExVar (mkSystemName u "ev" O) (weakTypeToCoreType t)) t.
169 Context (hetmet_brak : WeakExprVar).
170 Context (hetmet_esc : WeakExprVar).
171 Context (hetmet_flatten : WeakExprVar).
172 Context (hetmet_unflatten : WeakExprVar).
173 Context (hetmet_flattened_id : WeakExprVar).
174 Context (uniqueSupply : UniqSupply).
176 Definition useUniqueSupply {T}(ut:UniqM T) : ???T :=
179 f uniqueSupply >>= fun x => OK (snd x)
182 Definition larger : forall ln:list nat, { n:nat & forall n', In n' ln -> gt n n' }.
188 destruct IHln as [n pf].
189 exists (plus (S n) a).
193 fold (@In _ n' ln) in H.
198 Definition FreshNat : @FreshMonad nat.
199 refine {| FMT := fun T => nat -> prod nat T
205 set (larger tl) as q.
206 destruct q as [n' pf].
212 refine {| returnM := fun a (v:a) => _ |}.
213 intro n. exact (n,v).
216 destruct q as [n' v].
221 Definition unFresh {T} : @FreshM _ FreshNat T -> T.
230 Definition coreVarToWeakExprVarOrError cv :=
231 match coreVarToWeakVar cv with
233 | _ => Prelude_error "IMPOSSIBLE"
236 Definition curry {Γ}{Δ}{a}{s}{Σ}{lev} :
238 [ Γ > Δ > Σ |- [a ---> s ]@lev ]
239 [ Γ > Δ > [a @@ lev],,Σ |- [ s ]@lev ].
240 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
241 eapply nd_comp; [ idtac | eapply nd_rule; eapply RApp ].
242 eapply nd_comp; [ apply nd_rlecnac | idtac ].
249 Definition fToC1 {Γ}{Δ}{a}{s}{lev} :
250 ND Rule [] [ Γ > Δ > [ ] |- [a ---> s ]@lev ] ->
251 ND Rule [] [ Γ > Δ > [a @@ lev] |- [ s ]@lev ].
255 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanR ].
259 Definition fToC2 {Γ}{Δ}{a1}{a2}{s}{lev} :
260 ND Rule [] [ Γ > Δ > [] |- [a1 ---> (a2 ---> s) ]@lev ] ->
261 ND Rule [] [ Γ > Δ > [a1 @@ lev],,[a2 @@ lev] |- [ s ]@lev ].
272 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
276 Section coqPassCoreToCore.
279 (do_skolemize : bool)
280 (hetmet_brak : CoreVar)
281 (hetmet_esc : CoreVar)
282 (hetmet_flatten : CoreVar)
283 (hetmet_unflatten : CoreVar)
284 (hetmet_flattened_id : CoreVar)
285 (uniqueSupply : UniqSupply)
286 (lbinds:list (@CoreBind CoreVar))
287 (hetmet_PGArrowTyCon : TyFun)
288 (hetmet_PGArrow_unit_TyCon : TyFun)
289 (hetmet_PGArrow_tensor_TyCon : TyFun)
290 (hetmet_PGArrow_exponent_TyCon : TyFun)
291 (hetmet_pga_id : CoreVar)
292 (hetmet_pga_comp : CoreVar)
293 (hetmet_pga_first : CoreVar)
294 (hetmet_pga_second : CoreVar)
295 (hetmet_pga_cancell : CoreVar)
296 (hetmet_pga_cancelr : CoreVar)
297 (hetmet_pga_uncancell : CoreVar)
298 (hetmet_pga_uncancelr : CoreVar)
299 (hetmet_pga_assoc : CoreVar)
300 (hetmet_pga_unassoc : CoreVar)
301 (hetmet_pga_copy : CoreVar)
302 (hetmet_pga_drop : CoreVar)
303 (hetmet_pga_swap : CoreVar)
304 (hetmet_pga_applyl : CoreVar)
305 (hetmet_pga_applyr : CoreVar)
306 (hetmet_pga_curryl : CoreVar)
307 (hetmet_pga_curryr : CoreVar)
311 Definition ga_unit TV (ec:RawHaskType TV ECKind) : RawHaskType TV ★ :=
312 @TyFunApp TV hetmet_PGArrow_unit_TyCon (ECKind::nil) ★ (TyFunApp_cons _ _ ec TyFunApp_nil).
314 Definition ga_prod TV (ec:RawHaskType TV ECKind) (a b:RawHaskType TV ★) : RawHaskType TV ★ :=
316 hetmet_PGArrow_tensor_TyCon
317 (ECKind::★ ::★ ::nil) ★
318 (TyFunApp_cons _ _ ec
323 Definition ga_type {TV}(a:RawHaskType TV ECKind)(b c:RawHaskType TV ★) : RawHaskType TV ★ :=
324 TApp (TApp (TApp (@TyFunApp TV
326 nil _ TyFunApp_nil) a) b) c.
328 Definition ga := @ga_mk ga_unit ga_prod (@ga_type).
330 Definition ga_type' {Γ}(a:HaskType Γ ECKind)(b c:HaskType Γ ★) : HaskType Γ ★ :=
331 fun TV ite => TApp (TApp (TApp (@TyFunApp TV
333 nil _ TyFunApp_nil) (a TV ite)) (b TV ite)) (c TV ite).
335 Definition mkGlob2' {Γ}{κ₁}{κ₂}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ ★) :
336 IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::nil) -> HaskType Γ ★.
343 Definition mkGlob2 {Γ}{Δ}{l}{κ₁}{κ₂}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ ★) x y
344 : ND Rule [] [ Γ > Δ > [] |- [f x y ]@l ].
346 refine (@RGlobal Γ Δ l
347 {| glob_wv := coreVarToWeakExprVarOrError cv
348 ; glob_kinds := κ₁ :: κ₂ :: nil
349 ; glob_tf := mkGlob2'(Γ:=Γ) f
350 |} (ICons _ _ x (ICons _ _ y INil))).
353 Definition mkGlob3' {Γ}{κ₁}{κ₂}{κ₃}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ ★) :
354 IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::κ₃::nil) -> HaskType Γ ★.
362 Definition mkGlob3 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ ★) x y z
363 : ND Rule [] [ Γ > Δ > [] |- [f x y z ]@l ].
365 refine (@RGlobal Γ Δ l
366 {| glob_wv := coreVarToWeakExprVarOrError cv
367 ; glob_kinds := κ₁ :: κ₂ :: κ₃ :: nil
368 ; glob_tf := mkGlob3'(Γ:=Γ) f
369 |} (ICons _ _ x (ICons _ _ y (ICons _ _ z INil)))).
372 Definition mkGlob4' {Γ}{κ₁}{κ₂}{κ₃}{κ₄}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ κ₄ -> HaskType Γ ★) :
373 IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::κ₃::κ₄::nil) -> HaskType Γ ★.
382 Definition mkGlob4 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}{κ₄}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ κ₄ -> HaskType Γ ★) x y z q
383 : ND Rule [] [ Γ > Δ > [] |- [f x y z q ] @l].
385 refine (@RGlobal Γ Δ l
386 {| glob_wv := coreVarToWeakExprVarOrError cv
387 ; glob_kinds := κ₁ :: κ₂ :: κ₃ :: κ₄ :: nil
388 ; glob_tf := mkGlob4'(Γ:=Γ) f
389 |} (ICons _ _ x (ICons _ _ y (ICons _ _ z (ICons _ _ q INil))))).
392 Definition gat {Γ} ec (x:Tree ??(HaskType Γ ★)) := @ga_mk_tree ga_unit ga_prod _ ec x.
394 Instance my_ga : garrow ga_unit ga_prod (@ga_type) :=
395 { ga_id := fun Γ Δ ec l a => mkGlob2 hetmet_pga_id (fun ec a => ga_type' ec a a) ec (gat ec a)
396 ; ga_cancelr := fun Γ Δ ec l a => mkGlob2 hetmet_pga_cancelr (fun ec a => ga_type' ec _ a) ec (gat ec a)
397 ; ga_cancell := fun Γ Δ ec l a => mkGlob2 hetmet_pga_cancell (fun ec a => ga_type' ec _ a) ec (gat ec a)
398 ; ga_uncancelr := fun Γ Δ ec l a => mkGlob2 hetmet_pga_uncancelr (fun ec a => ga_type' ec a _) ec (gat ec a)
399 ; ga_uncancell := fun Γ Δ ec l a => mkGlob2 hetmet_pga_uncancell (fun ec a => ga_type' ec a _) ec (gat ec a)
400 ; 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)
401 ; 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)
402 ; 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)
403 ; ga_drop := fun Γ Δ ec l a => mkGlob2 hetmet_pga_drop (fun ec a => ga_type' ec _ _) ec (gat ec a)
404 ; ga_copy := fun Γ Δ ec l a => mkGlob2 hetmet_pga_copy (fun ec a => ga_type' ec _ _) ec (gat ec a)
405 ; 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))
406 ; 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))
407 ; 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))
408 (* ; ga_lit := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_lit))*)
409 (* ; ga_curry := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_curry))*)
410 (* ; ga_apply := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_apply))*)
411 (* ; ga_kappa := fun Γ Δ ec l a => fToC1 (nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_kappa)))*)
412 ; ga_lit := fun Γ Δ ec l a => Prelude_error "ga_lit"
413 ; ga_curry := fun Γ Δ ec l a b c => Prelude_error "ga_curry"
414 ; ga_apply := fun Γ Δ ec l a b c => Prelude_error "ga_apply"
415 ; ga_kappa := fun Γ Δ ec l a => Prelude_error "ga_kappa"
418 Definition hetmet_brak' := coreVarToWeakExprVarOrError hetmet_brak.
419 Definition hetmet_esc' := coreVarToWeakExprVarOrError hetmet_esc.
420 Definition hetmet_flatten' := coreVarToWeakExprVarOrError hetmet_flatten.
421 Definition hetmet_unflatten' := coreVarToWeakExprVarOrError hetmet_unflatten.
422 Definition hetmet_flattened_id' := coreVarToWeakExprVarOrError hetmet_flattened_id.
424 Definition coreToCoreExpr' (cex:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
425 addErrorMessage ("input CoreSyn: " +++ toString cex)
426 (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr cex)) (
427 coreExprToWeakExpr cex >>= fun we =>
428 addErrorMessage ("WeakExpr: " +++ toString we)
429 ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
430 ((weakTypeOfWeakExpr we) >>= fun t =>
431 (addErrorMessage ("WeakType: " +++ toString t)
432 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
434 ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
436 (addErrorMessage ("HaskStrong...")
439 (let haskProof := skolemize_and_flatten_proof hetmet_flatten' hetmet_unflatten'
440 hetmet_flattened_id' my_ga (@expr2proof _ _ _ _ _ _ _ e)
441 in (* insert HaskProof-to-HaskProof manipulations here *)
442 OK ((@proof2expr nat _ FreshNat _ _ (flatten_type τ) nil _
443 (fun _ => Prelude_error "unbound unique") _ haskProof) O)
444 >>= fun e' => (snd e') >>= fun e'' =>
445 strongExprToWeakExpr hetmet_brak' hetmet_esc'
446 mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
448 >>= fun q => OK (weakExprToCoreExpr q))
451 (let haskProof := flatten_proof (*hetmet_flatten' hetmet_unflatten'
452 hetmet_flattened_id' my_ga*) (@expr2proof _ _ _ _ _ _ _ e)
453 in (* insert HaskProof-to-HaskProof manipulations here *)
454 OK ((@proof2expr nat _ FreshNat _ _ τ nil _
455 (fun _ => Prelude_error "unbound unique") _ haskProof) O)
456 >>= fun e' => (snd e') >>= fun e'' =>
457 strongExprToWeakExpr hetmet_brak' hetmet_esc'
458 mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
460 >>= fun q => OK (weakExprToCoreExpr q))
462 (let haskProof := @expr2proof _ _ _ _ _ _ _ e
463 in (* insert HaskProof-to-HaskProof manipulations here *)
464 OK ((@proof2expr nat _ FreshNat _ _ τ nil _
465 (fun _ => Prelude_error "unbound unique") _ haskProof) O)
466 >>= fun e' => (snd e') >>= fun e'' =>
467 strongExprToWeakExpr hetmet_brak' hetmet_esc'
468 mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
470 >>= fun q => OK (weakExprToCoreExpr q))))
473 Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) :=
474 match coreToCoreExpr' ce with
476 | Error s => Prelude_error s
479 Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar :=
481 | CoreNonRec v e => let e' := coreToCoreExpr e in CoreNonRec (setVarType v (coreTypeOfCoreExpr e')) e'
483 | CoreRec lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
484 (* FIXME: doesn't deal with the case where top level recursive binds change type *)
486 match coreToCoreExpr (CoreELet lbe) (CoreELit HaskMachNullAddr) with
487 | CoreELet (CoreRec lbe') => lbe'
489 ("coreToCoreExpr was given a letrec, " +++
490 "but returned something that wasn't a letrec: " +++ toString x)
495 Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
496 map coreToCoreBind lbinds.
498 End coqPassCoreToCore.
500 Definition coqPassCoreToCore
502 (do_skolemize : bool)
503 (hetmet_brak : CoreVar)
504 (hetmet_esc : CoreVar)
505 (hetmet_flatten : CoreVar)
506 (hetmet_unflatten : CoreVar)
507 (hetmet_flattened_id : CoreVar)
508 (uniqueSupply : UniqSupply)
509 (lbinds:list (@CoreBind CoreVar))
510 (hetmet_PGArrowTyCon : TyFun)
511 (hetmet_PGArrow_unit_TyCon : TyFun)
512 (hetmet_PGArrow_tensor_TyCon : TyFun)
513 (hetmet_PGArrow_exponent_TyCon : TyFun)
514 (hetmet_pga_id : CoreVar)
515 (hetmet_pga_comp : CoreVar)
516 (hetmet_pga_first : CoreVar)
517 (hetmet_pga_second : CoreVar)
518 (hetmet_pga_cancell : CoreVar)
519 (hetmet_pga_cancelr : CoreVar)
520 (hetmet_pga_uncancell : CoreVar)
521 (hetmet_pga_uncancelr : CoreVar)
522 (hetmet_pga_assoc : CoreVar)
523 (hetmet_pga_unassoc : CoreVar)
524 (hetmet_pga_copy : CoreVar)
525 (hetmet_pga_drop : CoreVar)
526 (hetmet_pga_swap : CoreVar)
527 (hetmet_pga_applyl : CoreVar)
528 (hetmet_pga_applyr : CoreVar)
529 (hetmet_pga_curryl : CoreVar)
530 (hetmet_pga_curryr : CoreVar) : list (@CoreBind CoreVar) :=
541 hetmet_PGArrow_unit_TyCon
542 hetmet_PGArrow_tensor_TyCon
543 (* hetmet_PGArrow_exponent_TyCon*)