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".
78 Variable CoreM : Type -> Type.
79 Extract Constant CoreM "a" => "CoreMonad.CoreM".
80 Extraction Inline CoreM.
81 Variable CoreMreturn : forall a, a -> CoreM a.
82 Extraction Implicit CoreMreturn [a].
83 Implicit Arguments CoreMreturn [[a]].
84 Extract Inlined Constant CoreMreturn => "Prelude.return".
85 Variable CoreMbind : forall a b, CoreM a -> (a -> CoreM b) -> CoreM b.
86 Extraction Implicit CoreMbind [a b].
87 Implicit Arguments CoreMbind [[a] [b]].
88 Extract Inlined Constant CoreMbind => "(Prelude.>>=)".
91 Context (ce:@CoreExpr CoreVar).
93 Definition Γ : TypeEnv := nil.
95 Definition Δ : CoercionEnv Γ := nil.
97 Definition φ : TyVarResolver Γ :=
98 fun cv => Error ("unbound tyvar: " +++ toString (cv:CoreVar)).
99 (*fun tv => error ("tried to get the representative of an unbound tyvar:" +++ (getCoreVarOccString tv)).*)
101 Definition ψ : CoVarResolver Γ Δ :=
102 fun cv => Error ("tried to get the representative of an unbound covar!" (*+++ (getTypeVarOccString cv)*)).
104 (* We need to be able to resolve unbound exprvars, but we can be sure their types will have no
105 * free tyvars in them *)
106 Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ :=
107 match coreVarToWeakVar' cv with
108 | OK (WExprVar wev) => match weakTypeToTypeOfKind φ wev ★ with
109 | Error s => Prelude_error ("Error converting weakType of top-level variable "+++
110 toString cv+++": " +++ s)
113 | OK (WTypeVar _) => Prelude_error "top-level xi got a type variable"
114 | OK (WCoerVar _) => Prelude_error "top-level xi got a coercion variable"
115 | Error s => Prelude_error s
118 Definition header : string :=
119 "\documentclass{article}"+++eol+++
120 "\usepackage{amsmath}"+++eol+++
121 "\usepackage{amssymb}"+++eol+++
122 "\usepackage{proof}"+++eol+++
123 "\usepackage{trfrac} % http://www.utdallas.edu/~hamlen/trfrac.sty"+++eol+++
124 "\def\code#1#2{\Box_{#1} #2}"+++eol+++
125 "\usepackage[paperwidth=\maxdimen,paperheight=\maxdimen]{geometry}"+++eol+++
126 "\usepackage[tightpage,active]{preview}"+++eol+++
127 "\begin{document}"+++eol+++
128 "\setlength\PreviewBorder{5pt}"+++eol.
130 Definition footer : string :=
131 eol+++"\end{document}"+++
134 (* core-to-string (-dcoqpass) *)
135 Definition coreToStringExpr' (ce:@CoreExpr CoreVar) : ???string :=
136 addErrorMessage ("input CoreSyn: " +++ toString ce)
137 (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
138 coreExprToWeakExpr ce >>= fun we =>
139 addErrorMessage ("WeakExpr: " +++ toString we)
140 ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
141 ((weakTypeOfWeakExpr we) >>= fun t =>
142 (addErrorMessage ("WeakType: " +++ toString t)
143 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
144 addErrorMessage ("HaskType: " +++ toString τ)
145 ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => false) τ nil we) >>= fun e =>
146 OK (eol+++eol+++eol+++
147 "\begin{preview}"+++eol+++
149 toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ _ e))+++
151 "\end{preview}"+++eol+++eol+++eol)
154 Definition coreToStringExpr (ce:@CoreExpr CoreVar) : string :=
155 match coreToStringExpr' ce with
157 | Error s => Prelude_error s
160 Definition coreToStringBind (binds:@CoreBind CoreVar) : string :=
162 | CoreNonRec _ e => coreToStringExpr e
163 | CoreRec lbe => fold_left (fun x y => x+++eol+++eol+++y) (map (fun x => coreToStringExpr (snd x)) lbe) ""
166 Definition coqPassCoreToString (lbinds:list (@CoreBind CoreVar)) : string :=
168 (fold_left (fun x y => x+++eol+++eol+++y) (map coreToStringBind lbinds) "")
172 (* core-to-core (-fcoqpass) *)
175 Definition mkWeakTypeVar (u:Unique)(k:Kind) : WeakTypeVar :=
176 weakTypeVar (mkTyVar (mkSystemName u "tv" O) k) k.
177 Definition mkWeakCoerVar (u:Unique)(k:Kind)(t1 t2:WeakType) : WeakCoerVar :=
178 weakCoerVar (mkCoVar (mkSystemName u "cv" O) (weakTypeToCoreType t1) (weakTypeToCoreType t2)) t1 t2.
179 Definition mkWeakExprVar (u:Unique)(t:WeakType) : WeakExprVar :=
180 weakExprVar (mkExVar (mkSystemName u "ev" O) (weakTypeToCoreType t)) t.
182 Context (hetmet_brak : WeakExprVar).
183 Context (hetmet_esc : WeakExprVar).
184 Context (uniqueSupply : UniqSupply).
186 Definition useUniqueSupply {T}(ut:UniqM T) : ???T :=
189 f uniqueSupply >>= fun x => OK (snd x)
192 Definition larger : forall ln:list nat, { n:nat & forall n', In n' ln -> gt n n' }.
198 destruct IHln as [n pf].
199 exists (plus (S n) a).
203 fold (@In _ n' ln) in H.
208 Definition FreshNat : @FreshMonad nat.
209 refine {| FMT := fun T => nat -> prod nat T
215 set (larger tl) as q.
216 destruct q as [n' pf].
222 refine {| returnM := fun a (v:a) => _ |}.
223 intro n. exact (n,v).
226 destruct q as [n' v].
231 Definition unFresh {T} : @FreshM _ FreshNat T -> T.
240 Definition coreVarToWeakExprVarOrError cv :=
241 match addErrorMessage ("in coreVarToWeakExprVarOrError" +++ eol) (coreVarToWeakVar' cv) with
242 | OK (WExprVar wv) => wv
243 | Error s => Prelude_error s
244 | _ => Prelude_error "IMPOSSIBLE"
247 Definition curry {Γ}{Δ}{a}{s}{Σ}{lev} :
249 [ Γ > Δ > Σ |- [a ---> s ]@lev ]
250 [ Γ > Δ > [a @@ lev],,Σ |- [ s ]@lev ].
251 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
252 eapply nd_comp; [ idtac | eapply nd_rule; eapply RApp ].
253 eapply nd_comp; [ apply nd_rlecnac | idtac ].
260 Definition fToC1 {Γ}{Δ}{a}{s}{lev} :
261 ND Rule [] [ Γ > Δ > [ ] |- [a ---> s ]@lev ] ->
262 ND Rule [] [ Γ > Δ > [a @@ lev] |- [ s ]@lev ].
266 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanR ].
270 Definition fToC1' {Γ}{Δ}{a}{s}{lev} :
271 ND Rule [] [ Γ > Δ > [ ] |- [a ---> s ]@lev ] ->
272 ND Rule [] [ Γ > Δ > [a @@ lev] |- [ s ]@lev ].
276 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanR ].
280 Definition fToC2 {Γ}{Δ}{a1}{a2}{s}{lev} :
281 ND Rule [] [ Γ > Δ > [] |- [a1 ---> (a2 ---> s) ]@lev ] ->
282 ND Rule [] [ Γ > Δ > [a1 @@ lev],,[a2 @@ lev] |- [ s ]@lev ].
293 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
297 Definition fToCx {Γ}{Δ}{a1}{a2}{a3}{l} Σ :
298 ND Rule [] [ Γ > Δ > [] |- [(a1 ---> a2) ---> a3 ]@l ] ->
299 ND Rule [Γ > Δ > Σ,,[a1 @@ l] |- [a2]@l ]
300 [Γ > Δ > Σ |- [a3]@l ].
302 eapply nd_comp; [ eapply nd_rule; eapply RLam | idtac ].
303 set (fToC1 pf) as pf'.
308 Section coqPassCoreToCore.
311 (do_skolemize : bool)
312 (hetmet_brak : CoreVar)
313 (hetmet_esc : CoreVar)
314 (uniqueSupply : UniqSupply)
315 (lbinds:list (@CoreBind CoreVar))
316 (hetmet_PGArrowTyCon : TyFun)
317 (hetmet_PGArrow_unit_TyCon : TyFun)
318 (hetmet_PGArrow_tensor_TyCon : TyFun)
319 (hetmet_PGArrow_exponent_TyCon : TyFun)
320 (hetmet_pga_id : CoreVar)
321 (hetmet_pga_comp : CoreVar)
322 (hetmet_pga_first : CoreVar)
323 (hetmet_pga_second : CoreVar)
324 (hetmet_pga_cancell : CoreVar)
325 (hetmet_pga_cancelr : CoreVar)
326 (hetmet_pga_uncancell : CoreVar)
327 (hetmet_pga_uncancelr : CoreVar)
328 (hetmet_pga_assoc : CoreVar)
329 (hetmet_pga_unassoc : CoreVar)
330 (hetmet_pga_copy : CoreVar)
331 (hetmet_pga_drop : CoreVar)
332 (hetmet_pga_swap : CoreVar)
333 (hetmet_pga_applyl : CoreVar)
334 (hetmet_pga_applyr : CoreVar)
335 (hetmet_pga_curryl : CoreVar)
336 (hetmet_pga_curryr : CoreVar)
337 (hetmet_pga_loopl : CoreVar)
338 (hetmet_pga_loopr : CoreVar)
339 (hetmet_pga_kappa : CoreVar)
343 Definition ga_unit TV (ec:RawHaskType TV ECKind) : RawHaskType TV ★ :=
344 @TyFunApp TV hetmet_PGArrow_unit_TyCon (ECKind::nil) ★ (TyFunApp_cons _ _ ec TyFunApp_nil).
346 Definition ga_prod TV (ec:RawHaskType TV ECKind) (a b:RawHaskType TV ★) : RawHaskType TV ★ :=
348 hetmet_PGArrow_tensor_TyCon
349 (ECKind::★ ::★ ::nil) ★
350 (TyFunApp_cons _ _ ec
355 Definition ga_type {TV}(a:RawHaskType TV ECKind)(b c:RawHaskType TV ★) : RawHaskType TV ★ :=
356 TApp (TApp (TApp (@TyFunApp TV
358 nil _ TyFunApp_nil) a) b) c.
360 Definition ga := @ga_mk ga_unit ga_prod (@ga_type).
362 Definition ga_type' {Γ}(a:HaskType Γ ECKind)(b c:HaskType Γ ★) : HaskType Γ ★ :=
363 fun TV ite => TApp (TApp (TApp (@TyFunApp TV
365 nil _ TyFunApp_nil) (a TV ite)) (b TV ite)) (c TV ite).
367 Definition mkGlob2' {Γ}{κ₁}{κ₂}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ ★) :
368 IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::nil) -> HaskType Γ ★.
375 Definition mkGlob2 {Γ}{Δ}{l}{κ₁}{κ₂}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ ★) x y
376 : ND Rule [] [ Γ > Δ > [] |- [f x y ]@l ].
378 refine (@RGlobal Γ Δ l
379 {| glob_wv := coreVarToWeakExprVarOrError cv
380 ; glob_kinds := κ₁ :: κ₂ :: nil
381 ; glob_tf := mkGlob2'(Γ:=Γ) f
382 |} (ICons _ _ x (ICons _ _ y INil))).
385 Definition mkGlob3' {Γ}{κ₁}{κ₂}{κ₃}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ ★) :
386 IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::κ₃::nil) -> HaskType Γ ★.
394 Definition mkGlob3 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ ★) x y z
395 : ND Rule [] [ Γ > Δ > [] |- [f x y z ]@l ].
397 refine (@RGlobal Γ Δ l
398 {| glob_wv := coreVarToWeakExprVarOrError cv
399 ; glob_kinds := κ₁ :: κ₂ :: κ₃ :: nil
400 ; glob_tf := mkGlob3'(Γ:=Γ) f
401 |} (ICons _ _ x (ICons _ _ y (ICons _ _ z INil)))).
404 Definition mkGlob4' {Γ}{κ₁}{κ₂}{κ₃}{κ₄}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ κ₄ -> HaskType Γ ★) :
405 IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::κ₃::κ₄::nil) -> HaskType Γ ★.
414 Definition mkGlob4 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}{κ₄}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ κ₄ -> HaskType Γ ★) x y z q
415 : ND Rule [] [ Γ > Δ > [] |- [f x y z q ] @l].
417 refine (@RGlobal Γ Δ l
418 {| glob_wv := coreVarToWeakExprVarOrError cv
419 ; glob_kinds := κ₁ :: κ₂ :: κ₃ :: κ₄ :: nil
420 ; glob_tf := mkGlob4'(Γ:=Γ) f
421 |} (ICons _ _ x (ICons _ _ y (ICons _ _ z (ICons _ _ q INil))))).
424 Definition gat {Γ} ec (x:Tree ??(HaskType Γ ★)) := @ga_mk_tree ga_unit ga_prod _ ec x.
426 Instance my_ga : garrow ga_unit ga_prod (@ga_type) :=
427 { ga_id := fun Γ Δ ec l a => mkGlob2 hetmet_pga_id (fun ec a => ga_type' ec a a) ec (gat ec a)
428 ; ga_cancelr := fun Γ Δ ec l a => mkGlob2 hetmet_pga_cancelr (fun ec a => ga_type' ec _ a) ec (gat ec a)
429 ; ga_cancell := fun Γ Δ ec l a => mkGlob2 hetmet_pga_cancell (fun ec a => ga_type' ec _ a) ec (gat ec a)
430 ; ga_uncancelr := fun Γ Δ ec l a => mkGlob2 hetmet_pga_uncancelr (fun ec a => ga_type' ec a _) ec (gat ec a)
431 ; ga_uncancell := fun Γ Δ ec l a => mkGlob2 hetmet_pga_uncancell (fun ec a => ga_type' ec a _) ec (gat ec a)
432 ; 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)
433 ; 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)
434 ; 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)
435 ; ga_drop := fun Γ Δ ec l a => mkGlob2 hetmet_pga_drop (fun ec a => ga_type' ec _ _) ec (gat ec a)
436 ; ga_copy := fun Γ Δ ec l a => mkGlob2 hetmet_pga_copy (fun ec a => ga_type' ec _ _) ec (gat ec a)
437 ; 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))
438 ; 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))
439 ; 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))
440 ; 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))
441 ; 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))
443 ; ga_curry := fun Γ Δ ec l a => Prelude_error "ga_curry"
445 ; ga_apply := fun Γ Δ ec l a => Prelude_error "ga_apply"
446 ; ga_lit := fun Γ Δ ec l a => Prelude_error "ga_lit"
447 (* ; ga_lit := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_lit))*)
448 ; ga_kappa := fun Γ Δ ec l a b c Σ =>
449 fToCx Σ (mkGlob4 hetmet_pga_kappa (fun ec a b c => _) ec (gat ec a) (gat ec b) (gat ec c))
452 Definition hetmet_brak' := coreVarToWeakExprVarOrError hetmet_brak.
453 Definition hetmet_esc' := coreVarToWeakExprVarOrError hetmet_esc.
455 Definition coreToCoreExpr' (cex:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
456 addErrorMessage ("input CoreSyn: " +++ toString cex)
457 (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr cex)) (
458 coreExprToWeakExpr cex >>= fun we =>
459 addErrorMessage ("WeakExpr: " +++ toString we)
460 ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
461 ((weakTypeOfWeakExpr we) >>= fun t =>
462 (addErrorMessage ("WeakType: " +++ toString t)
463 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
465 ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
467 (addErrorMessage ("HaskStrong...")
470 (let haskProof := skolemize_and_flatten_proof my_ga (@expr2proof _ _ _ _ _ _ _ e)
471 in (* insert HaskProof-to-HaskProof manipulations here *)
472 OK ((@proof2expr nat _ FreshNat _ _ (flatten_type τ) nil _
473 (fun _ => Prelude_error "unbound unique") _ haskProof) O)
474 >>= fun e' => (snd e') >>= fun e'' =>
475 strongExprToWeakExpr hetmet_brak' hetmet_esc'
476 mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
478 >>= fun q => OK (weakExprToCoreExpr q))
481 (let haskProof := flatten_proof (@expr2proof _ _ _ _ _ _ _ e)
482 in (* insert HaskProof-to-HaskProof manipulations here *)
483 OK ((@proof2expr nat _ FreshNat _ _ τ nil _
484 (fun _ => Prelude_error "unbound unique") _ haskProof) O)
485 >>= fun e' => (snd e') >>= fun e'' =>
486 strongExprToWeakExpr hetmet_brak' hetmet_esc'
487 mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
489 >>= fun q => OK (weakExprToCoreExpr q))
491 (let haskProof := @expr2proof _ _ _ _ _ _ _ e
492 in (* insert HaskProof-to-HaskProof manipulations here *)
493 OK ((@proof2expr nat _ FreshNat _ _ τ nil _
494 (fun _ => Prelude_error "unbound unique") _ haskProof) O)
495 >>= fun e' => (snd e') >>= fun e'' =>
496 strongExprToWeakExpr hetmet_brak' hetmet_esc'
497 mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
499 >>= fun q => OK (weakExprToCoreExpr q))))
502 Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) :=
503 match coreToCoreExpr' ce with
505 | Error s => Prelude_error s
508 Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar :=
510 | CoreNonRec v e => let e' := coreToCoreExpr e in CoreNonRec (setVarType v (coreTypeOfCoreExpr e')) e'
512 | CoreRec lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
513 (* FIXME: doesn't deal with the case where top level recursive binds change type *)
515 match coreToCoreExpr (CoreELet lbe) (CoreELit HaskMachNullAddr) with
516 | CoreELet (CoreRec lbe') => lbe'
518 ("coreToCoreExpr was given a letrec, " +++
519 "but returned something that wasn't a letrec: " +++ toString x)
524 Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
525 map coreToCoreBind lbinds.
527 End coqPassCoreToCore.
529 Notation "a >>= b" := (@CoreMbind _ _ a b).
531 Definition coqPassCoreToCore
533 (do_skolemize : bool)
534 (dsLookupVar : string -> string -> CoreM CoreVar)
535 (dsLookupTyc : string -> string -> CoreM TyFun)
536 (uniqueSupply : UniqSupply)
537 (lbinds : list (@CoreBind CoreVar))
538 : CoreM (list (@CoreBind CoreVar)) :=
539 dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_brak" >>= fun hetmet_brak =>
540 dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_esc" >>= fun hetmet_esc =>
541 dsLookupTyc "GHC.HetMet.Private" "PGArrow" >>= fun hetmet_PGArrow =>
542 dsLookupTyc "GHC.HetMet.GArrow" "GArrowUnit" >>= fun hetmet_PGArrow_unit =>
543 dsLookupTyc "GHC.HetMet.GArrow" "GArrowTensor" >>= fun hetmet_PGArrow_tensor =>
544 dsLookupTyc "GHC.HetMet.GArrow" "GArrowExponent" >>= fun hetmet_PGArrow_exponent =>
545 dsLookupVar "GHC.HetMet.Private" "pga_id" >>= fun hetmet_pga_id =>
546 dsLookupVar "GHC.HetMet.Private" "pga_comp" >>= fun hetmet_pga_comp =>
547 dsLookupVar "GHC.HetMet.Private" "pga_first" >>= fun hetmet_pga_first =>
548 dsLookupVar "GHC.HetMet.Private" "pga_second" >>= fun hetmet_pga_second =>
549 dsLookupVar "GHC.HetMet.Private" "pga_cancell" >>= fun hetmet_pga_cancell =>
550 dsLookupVar "GHC.HetMet.Private" "pga_cancelr" >>= fun hetmet_pga_cancelr =>
551 dsLookupVar "GHC.HetMet.Private" "pga_uncancell" >>= fun hetmet_pga_uncancell =>
552 dsLookupVar "GHC.HetMet.Private" "pga_uncancelr" >>= fun hetmet_pga_uncancelr =>
553 dsLookupVar "GHC.HetMet.Private" "pga_assoc" >>= fun hetmet_pga_assoc =>
554 dsLookupVar "GHC.HetMet.Private" "pga_unassoc" >>= fun hetmet_pga_unassoc =>
555 dsLookupVar "GHC.HetMet.Private" "pga_copy" >>= fun hetmet_pga_copy =>
556 dsLookupVar "GHC.HetMet.Private" "pga_drop" >>= fun hetmet_pga_drop =>
557 dsLookupVar "GHC.HetMet.Private" "pga_swap" >>= fun hetmet_pga_swap =>
558 dsLookupVar "GHC.HetMet.Private" "pga_applyl" >>= fun hetmet_pga_applyl =>
559 dsLookupVar "GHC.HetMet.Private" "pga_applyr" >>= fun hetmet_pga_applyr =>
560 dsLookupVar "GHC.HetMet.Private" "pga_curryl" >>= fun hetmet_pga_curryl =>
561 dsLookupVar "GHC.HetMet.Private" "pga_curryr" >>= fun hetmet_pga_curryr =>
562 dsLookupVar "GHC.HetMet.Private" "pga_loopl" >>= fun hetmet_pga_loopl =>
563 dsLookupVar "GHC.HetMet.Private" "pga_loopr" >>= fun hetmet_pga_loopr =>
564 dsLookupVar "GHC.HetMet.Private" "pga_kappa" >>= fun hetmet_pga_kappa =>
575 hetmet_PGArrow_tensor
576 (* hetmet_PGArrow_exponent_TyCon*)