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.mkCoType 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 | OK (WExprVar wev) => match weakTypeToTypeOfKind φ wev ★ with
97 | Error s => Prelude_error ("Error converting weakType of top-level variable "+++
98 toString cv+++": " +++ s)
101 | OK (WTypeVar _) => Prelude_error "top-level xi got a type variable"
102 | OK (WCoerVar _) => Prelude_error "top-level xi got a coercion variable"
103 | Error s => Prelude_error s
106 Definition header : string :=
107 "\documentclass{article}"+++eol+++
108 "\usepackage{amsmath}"+++eol+++
109 "\usepackage{amssymb}"+++eol+++
110 "\usepackage{proof}"+++eol+++
111 "\usepackage{trfrac} % http://www.utdallas.edu/~hamlen/trfrac.sty"+++eol+++
112 "\def\code#1#2{\Box_{#1} #2}"+++eol+++
113 "\usepackage[paperwidth=\maxdimen,paperheight=\maxdimen]{geometry}"+++eol+++
114 "\usepackage[tightpage,active]{preview}"+++eol+++
115 "\begin{document}"+++eol+++
116 "\setlength\PreviewBorder{5pt}"+++eol.
118 Definition footer : string :=
119 eol+++"\end{document}"+++
122 (* core-to-string (-dcoqpass) *)
123 Definition coreToStringExpr' (ce:@CoreExpr CoreVar) : ???string :=
124 addErrorMessage ("input CoreSyn: " +++ toString ce)
125 (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
126 coreExprToWeakExpr ce >>= fun we =>
127 addErrorMessage ("WeakExpr: " +++ toString we)
128 ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
129 ((weakTypeOfWeakExpr we) >>= fun t =>
130 (addErrorMessage ("WeakType: " +++ toString t)
131 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
132 addErrorMessage ("HaskType: " +++ toString τ)
133 ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => false) τ nil we) >>= fun e =>
134 OK (eol+++eol+++eol+++
135 "\begin{preview}"+++eol+++
137 toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ _ e))+++
139 "\end{preview}"+++eol+++eol+++eol)
142 Definition coreToStringExpr (ce:@CoreExpr CoreVar) : string :=
143 match coreToStringExpr' ce with
145 | Error s => Prelude_error s
148 Definition coreToStringBind (binds:@CoreBind CoreVar) : string :=
150 | CoreNonRec _ e => coreToStringExpr e
151 | CoreRec lbe => fold_left (fun x y => x+++eol+++eol+++y) (map (fun x => coreToStringExpr (snd x)) lbe) ""
154 Definition coqPassCoreToString (lbinds:list (@CoreBind CoreVar)) : string :=
156 (fold_left (fun x y => x+++eol+++eol+++y) (map coreToStringBind lbinds) "")
160 (* core-to-core (-fcoqpass) *)
163 Definition mkWeakTypeVar (u:Unique)(k:Kind) : WeakTypeVar :=
164 weakTypeVar (mkTyVar (mkSystemName u "tv" O) k) k.
165 Definition mkWeakCoerVar (u:Unique)(k:Kind)(t1 t2:WeakType) : WeakCoerVar :=
166 weakCoerVar (mkCoVar (mkSystemName u "cv" O) (weakTypeToCoreType t1) (weakTypeToCoreType t2)) t1 t2.
167 Definition mkWeakExprVar (u:Unique)(t:WeakType) : WeakExprVar :=
168 weakExprVar (mkExVar (mkSystemName u "ev" O) (weakTypeToCoreType t)) t.
170 Context (hetmet_brak : WeakExprVar).
171 Context (hetmet_esc : WeakExprVar).
172 Context (hetmet_flatten : WeakExprVar).
173 Context (hetmet_unflatten : WeakExprVar).
174 Context (hetmet_flattened_id : WeakExprVar).
175 Context (uniqueSupply : UniqSupply).
177 Definition useUniqueSupply {T}(ut:UniqM T) : ???T :=
180 f uniqueSupply >>= fun x => OK (snd x)
183 Definition larger : forall ln:list nat, { n:nat & forall n', In n' ln -> gt n n' }.
189 destruct IHln as [n pf].
190 exists (plus (S n) a).
194 fold (@In _ n' ln) in H.
199 Definition FreshNat : @FreshMonad nat.
200 refine {| FMT := fun T => nat -> prod nat T
206 set (larger tl) as q.
207 destruct q as [n' pf].
213 refine {| returnM := fun a (v:a) => _ |}.
214 intro n. exact (n,v).
217 destruct q as [n' v].
222 Definition unFresh {T} : @FreshM _ FreshNat T -> T.
231 Definition coreVarToWeakExprVarOrError cv :=
232 match addErrorMessage ("in coreVarToWeakExprVarOrError" +++ eol) (coreVarToWeakVar' cv) with
233 | OK (WExprVar wv) => wv
234 | Error s => Prelude_error s
235 | _ => Prelude_error "IMPOSSIBLE"
238 Definition curry {Γ}{Δ}{a}{s}{Σ}{lev} :
240 [ Γ > Δ > Σ |- [a ---> s ]@lev ]
241 [ Γ > Δ > [a @@ lev],,Σ |- [ s ]@lev ].
242 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
243 eapply nd_comp; [ idtac | eapply nd_rule; eapply RApp ].
244 eapply nd_comp; [ apply nd_rlecnac | idtac ].
251 Definition fToC1 {Γ}{Δ}{a}{s}{lev} :
252 ND Rule [] [ Γ > Δ > [ ] |- [a ---> s ]@lev ] ->
253 ND Rule [] [ Γ > Δ > [a @@ lev] |- [ s ]@lev ].
257 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanR ].
261 Definition fToC2 {Γ}{Δ}{a1}{a2}{s}{lev} :
262 ND Rule [] [ Γ > Δ > [] |- [a1 ---> (a2 ---> s) ]@lev ] ->
263 ND Rule [] [ Γ > Δ > [a1 @@ lev],,[a2 @@ lev] |- [ s ]@lev ].
274 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
278 Section coqPassCoreToCore.
281 (do_skolemize : bool)
282 (hetmet_brak : CoreVar)
283 (hetmet_esc : CoreVar)
284 (hetmet_flatten : CoreVar)
285 (hetmet_unflatten : CoreVar)
286 (hetmet_flattened_id : CoreVar)
287 (uniqueSupply : UniqSupply)
288 (lbinds:list (@CoreBind CoreVar))
289 (hetmet_PGArrowTyCon : TyFun)
290 (hetmet_PGArrow_unit_TyCon : TyFun)
291 (hetmet_PGArrow_tensor_TyCon : TyFun)
292 (hetmet_PGArrow_exponent_TyCon : TyFun)
293 (hetmet_pga_id : CoreVar)
294 (hetmet_pga_comp : CoreVar)
295 (hetmet_pga_first : CoreVar)
296 (hetmet_pga_second : CoreVar)
297 (hetmet_pga_cancell : CoreVar)
298 (hetmet_pga_cancelr : CoreVar)
299 (hetmet_pga_uncancell : CoreVar)
300 (hetmet_pga_uncancelr : CoreVar)
301 (hetmet_pga_assoc : CoreVar)
302 (hetmet_pga_unassoc : CoreVar)
303 (hetmet_pga_copy : CoreVar)
304 (hetmet_pga_drop : CoreVar)
305 (hetmet_pga_swap : CoreVar)
306 (hetmet_pga_applyl : CoreVar)
307 (hetmet_pga_applyr : CoreVar)
308 (hetmet_pga_curryl : CoreVar)
309 (hetmet_pga_curryr : CoreVar)
310 (hetmet_pga_loopl : CoreVar)
311 (hetmet_pga_loopr : CoreVar)
315 Definition ga_unit TV (ec:RawHaskType TV ECKind) : RawHaskType TV ★ :=
316 @TyFunApp TV hetmet_PGArrow_unit_TyCon (ECKind::nil) ★ (TyFunApp_cons _ _ ec TyFunApp_nil).
318 Definition ga_prod TV (ec:RawHaskType TV ECKind) (a b:RawHaskType TV ★) : RawHaskType TV ★ :=
320 hetmet_PGArrow_tensor_TyCon
321 (ECKind::★ ::★ ::nil) ★
322 (TyFunApp_cons _ _ ec
327 Definition ga_type {TV}(a:RawHaskType TV ECKind)(b c:RawHaskType TV ★) : RawHaskType TV ★ :=
328 TApp (TApp (TApp (@TyFunApp TV
330 nil _ TyFunApp_nil) a) b) c.
332 Definition ga := @ga_mk ga_unit ga_prod (@ga_type).
334 Definition ga_type' {Γ}(a:HaskType Γ ECKind)(b c:HaskType Γ ★) : HaskType Γ ★ :=
335 fun TV ite => TApp (TApp (TApp (@TyFunApp TV
337 nil _ TyFunApp_nil) (a TV ite)) (b TV ite)) (c TV ite).
339 Definition mkGlob2' {Γ}{κ₁}{κ₂}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ ★) :
340 IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::nil) -> HaskType Γ ★.
347 Definition mkGlob2 {Γ}{Δ}{l}{κ₁}{κ₂}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ ★) x y
348 : ND Rule [] [ Γ > Δ > [] |- [f x y ]@l ].
350 refine (@RGlobal Γ Δ l
351 {| glob_wv := coreVarToWeakExprVarOrError cv
352 ; glob_kinds := κ₁ :: κ₂ :: nil
353 ; glob_tf := mkGlob2'(Γ:=Γ) f
354 |} (ICons _ _ x (ICons _ _ y INil))).
357 Definition mkGlob3' {Γ}{κ₁}{κ₂}{κ₃}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ ★) :
358 IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::κ₃::nil) -> HaskType Γ ★.
366 Definition mkGlob3 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ ★) x y z
367 : ND Rule [] [ Γ > Δ > [] |- [f x y z ]@l ].
369 refine (@RGlobal Γ Δ l
370 {| glob_wv := coreVarToWeakExprVarOrError cv
371 ; glob_kinds := κ₁ :: κ₂ :: κ₃ :: nil
372 ; glob_tf := mkGlob3'(Γ:=Γ) f
373 |} (ICons _ _ x (ICons _ _ y (ICons _ _ z INil)))).
376 Definition mkGlob4' {Γ}{κ₁}{κ₂}{κ₃}{κ₄}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ κ₄ -> HaskType Γ ★) :
377 IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::κ₃::κ₄::nil) -> HaskType Γ ★.
386 Definition mkGlob4 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}{κ₄}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ κ₄ -> HaskType Γ ★) x y z q
387 : ND Rule [] [ Γ > Δ > [] |- [f x y z q ] @l].
389 refine (@RGlobal Γ Δ l
390 {| glob_wv := coreVarToWeakExprVarOrError cv
391 ; glob_kinds := κ₁ :: κ₂ :: κ₃ :: κ₄ :: nil
392 ; glob_tf := mkGlob4'(Γ:=Γ) f
393 |} (ICons _ _ x (ICons _ _ y (ICons _ _ z (ICons _ _ q INil))))).
396 Definition gat {Γ} ec (x:Tree ??(HaskType Γ ★)) := @ga_mk_tree ga_unit ga_prod _ ec x.
398 Instance my_ga : garrow ga_unit ga_prod (@ga_type) :=
399 { ga_id := fun Γ Δ ec l a => mkGlob2 hetmet_pga_id (fun ec a => ga_type' ec a a) ec (gat ec a)
400 ; ga_cancelr := fun Γ Δ ec l a => mkGlob2 hetmet_pga_cancelr (fun ec a => ga_type' ec _ a) ec (gat ec a)
401 ; ga_cancell := fun Γ Δ ec l a => mkGlob2 hetmet_pga_cancell (fun ec a => ga_type' ec _ a) ec (gat ec a)
402 ; ga_uncancelr := fun Γ Δ ec l a => mkGlob2 hetmet_pga_uncancelr (fun ec a => ga_type' ec a _) ec (gat ec a)
403 ; ga_uncancell := fun Γ Δ ec l a => mkGlob2 hetmet_pga_uncancell (fun ec a => ga_type' ec a _) ec (gat ec a)
404 ; 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)
405 ; 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)
406 ; 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)
407 ; ga_drop := fun Γ Δ ec l a => mkGlob2 hetmet_pga_drop (fun ec a => ga_type' ec _ _) ec (gat ec a)
408 ; ga_copy := fun Γ Δ ec l a => mkGlob2 hetmet_pga_copy (fun ec a => ga_type' ec _ _) ec (gat ec a)
409 ; 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))
410 ; 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))
411 ; 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))
412 (* ; ga_lit := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_lit))*)
413 (* ; ga_curry := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_curry))*)
414 (* ; ga_apply := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_apply))*)
415 (* ; ga_kappa := fun Γ Δ ec l a => fToC1 (nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_kappa)))*)
416 ; ga_loopl := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_loopl (fun ec a b c => _) ec (gat ec a) (gat ec b) (gat ec x))
417 ; ga_loopr := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_loopr (fun ec a b c => _) ec (gat ec a) (gat ec b) (gat ec x))
418 ; ga_lit := fun Γ Δ ec l a => Prelude_error "ga_lit"
419 ; ga_curry := fun Γ Δ ec l a b c => Prelude_error "ga_curry"
420 ; ga_apply := fun Γ Δ ec l a b c => Prelude_error "ga_apply"
421 ; ga_kappa := fun Γ Δ ec l a => Prelude_error "ga_kappa"
424 Definition hetmet_brak' := coreVarToWeakExprVarOrError hetmet_brak.
425 Definition hetmet_esc' := coreVarToWeakExprVarOrError hetmet_esc.
426 Definition hetmet_flatten' := coreVarToWeakExprVarOrError hetmet_flatten.
427 Definition hetmet_unflatten' := coreVarToWeakExprVarOrError hetmet_unflatten.
428 Definition hetmet_flattened_id' := coreVarToWeakExprVarOrError hetmet_flattened_id.
430 Definition coreToCoreExpr' (cex:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
431 addErrorMessage ("input CoreSyn: " +++ toString cex)
432 (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr cex)) (
433 coreExprToWeakExpr cex >>= fun we =>
434 addErrorMessage ("WeakExpr: " +++ toString we)
435 ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
436 ((weakTypeOfWeakExpr we) >>= fun t =>
437 (addErrorMessage ("WeakType: " +++ toString t)
438 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
440 ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
442 (addErrorMessage ("HaskStrong...")
445 (let haskProof := skolemize_and_flatten_proof hetmet_flatten' hetmet_unflatten'
446 hetmet_flattened_id' my_ga (@expr2proof _ _ _ _ _ _ _ e)
447 in (* insert HaskProof-to-HaskProof manipulations here *)
448 OK ((@proof2expr nat _ FreshNat _ _ (flatten_type τ) nil _
449 (fun _ => Prelude_error "unbound unique") _ haskProof) O)
450 >>= fun e' => (snd e') >>= fun e'' =>
451 strongExprToWeakExpr hetmet_brak' hetmet_esc'
452 mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
454 >>= fun q => OK (weakExprToCoreExpr q))
457 (let haskProof := flatten_proof (*hetmet_flatten' hetmet_unflatten'
458 hetmet_flattened_id' my_ga*) (@expr2proof _ _ _ _ _ _ _ e)
459 in (* insert HaskProof-to-HaskProof manipulations here *)
460 OK ((@proof2expr nat _ FreshNat _ _ τ nil _
461 (fun _ => Prelude_error "unbound unique") _ haskProof) O)
462 >>= fun e' => (snd e') >>= fun e'' =>
463 strongExprToWeakExpr hetmet_brak' hetmet_esc'
464 mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
466 >>= fun q => OK (weakExprToCoreExpr q))
468 (let haskProof := @expr2proof _ _ _ _ _ _ _ e
469 in (* insert HaskProof-to-HaskProof manipulations here *)
470 OK ((@proof2expr nat _ FreshNat _ _ τ nil _
471 (fun _ => Prelude_error "unbound unique") _ haskProof) O)
472 >>= fun e' => (snd e') >>= fun e'' =>
473 strongExprToWeakExpr hetmet_brak' hetmet_esc'
474 mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
476 >>= fun q => OK (weakExprToCoreExpr q))))
479 Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) :=
480 match coreToCoreExpr' ce with
482 | Error s => Prelude_error s
485 Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar :=
487 | CoreNonRec v e => let e' := coreToCoreExpr e in CoreNonRec (setVarType v (coreTypeOfCoreExpr e')) e'
489 | CoreRec lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
490 (* FIXME: doesn't deal with the case where top level recursive binds change type *)
492 match coreToCoreExpr (CoreELet lbe) (CoreELit HaskMachNullAddr) with
493 | CoreELet (CoreRec lbe') => lbe'
495 ("coreToCoreExpr was given a letrec, " +++
496 "but returned something that wasn't a letrec: " +++ toString x)
501 Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
502 map coreToCoreBind lbinds.
504 End coqPassCoreToCore.
506 Definition coqPassCoreToCore
508 (do_skolemize : bool)
509 (hetmet_brak : CoreVar)
510 (hetmet_esc : CoreVar)
511 (hetmet_flatten : CoreVar)
512 (hetmet_unflatten : CoreVar)
513 (hetmet_flattened_id : CoreVar)
514 (uniqueSupply : UniqSupply)
515 (lbinds:list (@CoreBind CoreVar))
516 (hetmet_PGArrowTyCon : TyFun)
517 (hetmet_PGArrow_unit_TyCon : TyFun)
518 (hetmet_PGArrow_tensor_TyCon : TyFun)
519 (hetmet_PGArrow_exponent_TyCon : TyFun)
520 (hetmet_pga_id : CoreVar)
521 (hetmet_pga_comp : CoreVar)
522 (hetmet_pga_first : CoreVar)
523 (hetmet_pga_second : CoreVar)
524 (hetmet_pga_cancell : CoreVar)
525 (hetmet_pga_cancelr : CoreVar)
526 (hetmet_pga_uncancell : CoreVar)
527 (hetmet_pga_uncancelr : CoreVar)
528 (hetmet_pga_assoc : CoreVar)
529 (hetmet_pga_unassoc : CoreVar)
530 (hetmet_pga_copy : CoreVar)
531 (hetmet_pga_drop : CoreVar)
532 (hetmet_pga_swap : CoreVar)
533 (hetmet_pga_applyl : CoreVar)
534 (hetmet_pga_applyr : CoreVar)
535 (hetmet_pga_curryl : CoreVar)
536 (hetmet_pga_curryr : CoreVar)
537 (hetmet_pga_loopl : CoreVar)
538 (hetmet_pga_loopr : CoreVar)
539 : list (@CoreBind CoreVar) :=
550 hetmet_PGArrow_unit_TyCon
551 hetmet_PGArrow_tensor_TyCon
552 (* hetmet_PGArrow_exponent_TyCon*)