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 (hetmet_kappa : WeakExprVar).
185 Context (hetmet_kappa_app : WeakExprVar).
186 Context (uniqueSupply : UniqSupply).
188 Definition useUniqueSupply {T}(ut:UniqM T) : ???T :=
191 f uniqueSupply >>= fun x => OK (snd x)
194 Definition larger : forall ln:list nat, { n:nat & forall n', In n' ln -> gt n n' }.
200 destruct IHln as [n pf].
201 exists (plus (S n) a).
205 fold (@In _ n' ln) in H.
210 Definition FreshNat : @FreshMonad nat.
211 refine {| FMT := fun T => nat -> prod nat T
217 set (larger tl) as q.
218 destruct q as [n' pf].
224 refine {| returnM := fun a (v:a) => _ |}.
225 intro n. exact (n,v).
228 destruct q as [n' v].
233 Definition unFresh {T} : @FreshM _ FreshNat T -> T.
242 Definition coreVarToWeakExprVarOrError cv :=
243 match addErrorMessage ("in coreVarToWeakExprVarOrError" +++ eol) (coreVarToWeakVar' cv) with
244 | OK (WExprVar wv) => wv
245 | Error s => Prelude_error s
246 | _ => Prelude_error "IMPOSSIBLE"
249 Definition curry {Γ}{Δ}{a}{s}{Σ}{lev} :
251 [ Γ > Δ > Σ |- [a ---> s ]@lev ]
252 [ Γ > Δ > [a @@ lev],,Σ |- [ s ]@lev ].
253 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
254 eapply nd_comp; [ idtac | eapply nd_rule; eapply RApp ].
255 eapply nd_comp; [ apply nd_rlecnac | idtac ].
262 Definition fToC1 {Γ}{Δ}{a}{s}{lev} :
263 ND Rule [] [ Γ > Δ > [ ] |- [a ---> s ]@lev ] ->
264 ND Rule [] [ Γ > Δ > [a @@ lev] |- [ s ]@lev ].
268 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanR ].
272 Definition fToC1' {Γ}{Δ}{a}{s}{lev} :
273 ND Rule [] [ Γ > Δ > [ ] |- [a ---> s ]@lev ] ->
274 ND Rule [] [ Γ > Δ > [a @@ lev] |- [ s ]@lev ].
278 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanR ].
282 Definition fToC2 {Γ}{Δ}{a1}{a2}{s}{lev} :
283 ND Rule [] [ Γ > Δ > [] |- [a1 ---> (a2 ---> s) ]@lev ] ->
284 ND Rule [] [ Γ > Δ > [a1 @@ lev],,[a2 @@ lev] |- [ s ]@lev ].
295 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
299 Definition fToCx {Γ}{Δ}{a1}{a2}{a3}{l} Σ :
300 ND Rule [] [ Γ > Δ > [] |- [(a1 ---> a2) ---> a3 ]@l ] ->
301 ND Rule [Γ > Δ > Σ,,[a1 @@ l] |- [a2]@l ]
302 [Γ > Δ > Σ |- [a3]@l ].
304 eapply nd_comp; [ eapply nd_rule; eapply RLam | idtac ].
305 set (fToC1 pf) as pf'.
310 Section coqPassCoreToCore.
313 (do_skolemize : bool)
314 (hetmet_brak : CoreVar)
315 (hetmet_esc : CoreVar)
316 (hetmet_kappa : WeakExprVar)
317 (hetmet_kappa_app : WeakExprVar)
318 (uniqueSupply : UniqSupply)
319 (lbinds:list (@CoreBind CoreVar))
320 (hetmet_PGArrowTyCon : TyFun)
321 (hetmet_PGArrow_unit_TyCon : TyFun)
322 (hetmet_PGArrow_tensor_TyCon : TyFun)
323 (hetmet_PGArrow_exponent_TyCon : TyFun)
324 (hetmet_pga_id : CoreVar)
325 (hetmet_pga_comp : CoreVar)
326 (hetmet_pga_first : CoreVar)
327 (hetmet_pga_second : CoreVar)
328 (hetmet_pga_cancell : CoreVar)
329 (hetmet_pga_cancelr : CoreVar)
330 (hetmet_pga_uncancell : CoreVar)
331 (hetmet_pga_uncancelr : CoreVar)
332 (hetmet_pga_assoc : CoreVar)
333 (hetmet_pga_unassoc : CoreVar)
334 (hetmet_pga_copy : CoreVar)
335 (hetmet_pga_drop : CoreVar)
336 (hetmet_pga_swap : CoreVar)
337 (hetmet_pga_applyl : CoreVar)
338 (hetmet_pga_applyr : CoreVar)
339 (hetmet_pga_curryl : CoreVar)
340 (hetmet_pga_curryr : CoreVar)
341 (hetmet_pga_loopl : CoreVar)
342 (hetmet_pga_loopr : CoreVar)
343 (hetmet_pga_kappa : CoreVar)
347 Definition ga_unit TV (ec:RawHaskType TV ECKind) : RawHaskType TV ★ :=
348 @TyFunApp TV hetmet_PGArrow_unit_TyCon (ECKind::nil) ★ (TyFunApp_cons _ _ ec TyFunApp_nil).
350 Definition ga_prod TV (ec:RawHaskType TV ECKind) (a b:RawHaskType TV ★) : RawHaskType TV ★ :=
352 hetmet_PGArrow_tensor_TyCon
353 (ECKind::★ ::★ ::nil) ★
354 (TyFunApp_cons _ _ ec
359 Definition ga_type {TV}(a:RawHaskType TV ECKind)(b c:RawHaskType TV ★) : RawHaskType TV ★ :=
360 TApp (TApp (TApp (@TyFunApp TV
362 nil _ TyFunApp_nil) a) b) c.
364 Definition ga := @ga_mk ga_unit ga_prod (@ga_type).
366 Definition ga_type' {Γ}(a:HaskType Γ ECKind)(b c:HaskType Γ ★) : HaskType Γ ★ :=
367 fun TV ite => TApp (TApp (TApp (@TyFunApp TV
369 nil _ TyFunApp_nil) (a TV ite)) (b TV ite)) (c TV ite).
371 Definition mkGlob2' {Γ}{κ₁}{κ₂}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ ★) :
372 IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::nil) -> HaskType Γ ★.
379 Definition mkGlob2 {Γ}{Δ}{l}{κ₁}{κ₂}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ ★) x y
380 : ND Rule [] [ Γ > Δ > [] |- [f x y ]@l ].
382 refine (@RGlobal Γ Δ l
383 {| glob_wv := coreVarToWeakExprVarOrError cv
384 ; glob_kinds := κ₁ :: κ₂ :: nil
385 ; glob_tf := mkGlob2'(Γ:=Γ) f
386 |} (ICons _ _ x (ICons _ _ y INil))).
389 Definition mkGlob3' {Γ}{κ₁}{κ₂}{κ₃}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ ★) :
390 IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::κ₃::nil) -> HaskType Γ ★.
398 Definition mkGlob3 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ ★) x y z
399 : ND Rule [] [ Γ > Δ > [] |- [f x y z ]@l ].
401 refine (@RGlobal Γ Δ l
402 {| glob_wv := coreVarToWeakExprVarOrError cv
403 ; glob_kinds := κ₁ :: κ₂ :: κ₃ :: nil
404 ; glob_tf := mkGlob3'(Γ:=Γ) f
405 |} (ICons _ _ x (ICons _ _ y (ICons _ _ z INil)))).
408 Definition mkGlob4' {Γ}{κ₁}{κ₂}{κ₃}{κ₄}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ κ₄ -> HaskType Γ ★) :
409 IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::κ₃::κ₄::nil) -> HaskType Γ ★.
418 Definition mkGlob4 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}{κ₄}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ κ₄ -> HaskType Γ ★) x y z q
419 : ND Rule [] [ Γ > Δ > [] |- [f x y z q ] @l].
421 refine (@RGlobal Γ Δ l
422 {| glob_wv := coreVarToWeakExprVarOrError cv
423 ; glob_kinds := κ₁ :: κ₂ :: κ₃ :: κ₄ :: nil
424 ; glob_tf := mkGlob4'(Γ:=Γ) f
425 |} (ICons _ _ x (ICons _ _ y (ICons _ _ z (ICons _ _ q INil))))).
428 Definition gat {Γ} ec (x:Tree ??(HaskType Γ ★)) := @ga_mk_tree ga_unit ga_prod _ ec x.
430 Instance my_ga : garrow ga_unit ga_prod (@ga_type) :=
431 { ga_id := fun Γ Δ ec l a => mkGlob2 hetmet_pga_id (fun ec a => ga_type' ec a a) ec (gat ec a)
432 ; ga_cancelr := fun Γ Δ ec l a => mkGlob2 hetmet_pga_cancelr (fun ec a => ga_type' ec _ a) ec (gat ec a)
433 ; ga_cancell := fun Γ Δ ec l a => mkGlob2 hetmet_pga_cancell (fun ec a => ga_type' ec _ a) ec (gat ec a)
434 ; ga_uncancelr := fun Γ Δ ec l a => mkGlob2 hetmet_pga_uncancelr (fun ec a => ga_type' ec a _) ec (gat ec a)
435 ; ga_uncancell := fun Γ Δ ec l a => mkGlob2 hetmet_pga_uncancell (fun ec a => ga_type' ec a _) ec (gat ec a)
436 ; 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)
437 ; 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)
438 ; 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)
439 ; ga_drop := fun Γ Δ ec l a => mkGlob2 hetmet_pga_drop (fun ec a => ga_type' ec _ _) ec (gat ec a)
440 ; ga_copy := fun Γ Δ ec l a => mkGlob2 hetmet_pga_copy (fun ec a => ga_type' ec _ _) ec (gat ec a)
441 ; 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))
442 ; 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))
443 ; 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))
444 ; 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))
445 ; 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))
447 ; ga_curry := fun Γ Δ ec l a => Prelude_error "ga_curry"
449 ; ga_apply := fun Γ Δ ec l a => Prelude_error "ga_apply"
450 ; ga_lit := fun Γ Δ ec l a => Prelude_error "ga_lit"
451 (* ; ga_lit := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_lit))*)
452 ; ga_kappa := fun Γ Δ ec l a b c Σ =>
453 fToCx Σ (mkGlob4 hetmet_pga_kappa (fun ec a b c => _) ec (gat ec a) (gat ec b) (gat ec c))
456 Definition hetmet_brak' := coreVarToWeakExprVarOrError hetmet_brak.
457 Definition hetmet_esc' := coreVarToWeakExprVarOrError hetmet_esc.
458 Definition hetmet_kappa' := coreVarToWeakExprVarOrError hetmet_kappa.
459 Definition hetmet_kappa_app' := coreVarToWeakExprVarOrError hetmet_kappa_app.
461 Definition coreToCoreExpr' (cex:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
462 addErrorMessage ("input CoreSyn: " +++ toString cex)
463 (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr cex)) (
464 coreExprToWeakExpr cex >>= fun we =>
465 addErrorMessage ("WeakExpr: " +++ toString we)
466 ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
467 ((weakTypeOfWeakExpr we) >>= fun t =>
468 (addErrorMessage ("WeakType: " +++ toString t)
469 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
471 ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
473 (addErrorMessage ("HaskStrong...")
476 (let haskProof := skolemize_and_flatten_proof my_ga (@expr2proof _ _ _ _ _ _ _ e)
477 in (* insert HaskProof-to-HaskProof manipulations here *)
478 OK ((@proof2expr nat _ FreshNat _ _ (flatten_type τ) nil _
479 (fun _ => Prelude_error "unbound unique") _ haskProof) O)
480 >>= fun e' => (snd e') >>= fun e'' =>
481 strongExprToWeakExpr hetmet_brak' hetmet_esc' (*hetmet_kappa' hetmet_kappa_app'*)
482 mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
484 >>= fun q => OK (weakExprToCoreExpr q))
487 (let haskProof := flatten_proof (@expr2proof _ _ _ _ _ _ _ e)
488 in (* insert HaskProof-to-HaskProof manipulations here *)
489 OK ((@proof2expr nat _ FreshNat _ _ τ nil _
490 (fun _ => Prelude_error "unbound unique") _ haskProof) O)
491 >>= fun e' => (snd e') >>= fun e'' =>
492 strongExprToWeakExpr hetmet_brak' hetmet_esc' (*hetmet_kappa' hetmet_kappa_app'*)
493 mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
495 >>= fun q => OK (weakExprToCoreExpr q))
497 (let haskProof := @expr2proof _ _ _ _ _ _ _ e
498 in (* insert HaskProof-to-HaskProof manipulations here *)
499 OK ((@proof2expr nat _ FreshNat _ _ τ nil _
500 (fun _ => Prelude_error "unbound unique") _ haskProof) O)
501 >>= fun e' => (snd e') >>= fun e'' =>
502 strongExprToWeakExpr hetmet_brak' hetmet_esc' (*hetmet_kappa' hetmet_kappa_app'*)
503 mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
505 >>= fun q => OK (weakExprToCoreExpr q))))
508 Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) :=
509 match coreToCoreExpr' ce with
511 | Error s => Prelude_error s
514 Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar :=
516 | CoreNonRec v e => let e' := coreToCoreExpr e in CoreNonRec (setVarType v (coreTypeOfCoreExpr e')) e'
518 | CoreRec lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
519 (* FIXME: doesn't deal with the case where top level recursive binds change type *)
521 match coreToCoreExpr (CoreELet lbe) (CoreELit HaskMachNullAddr) with
522 | CoreELet (CoreRec lbe') => lbe'
524 ("coreToCoreExpr was given a letrec, " +++
525 "but returned something that wasn't a letrec: " +++ toString x)
530 Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
531 map coreToCoreBind lbinds.
533 End coqPassCoreToCore.
535 Notation "a >>= b" := (@CoreMbind _ _ a b).
537 Definition coqPassCoreToCore
539 (do_skolemize : bool)
540 (dsLookupVar : string -> string -> CoreM CoreVar)
541 (dsLookupTyc : string -> string -> CoreM TyFun)
542 (uniqueSupply : UniqSupply)
543 (lbinds : list (@CoreBind CoreVar))
544 : CoreM (list (@CoreBind CoreVar)) :=
545 dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_brak" >>= fun hetmet_brak =>
546 dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_esc" >>= fun hetmet_esc =>
547 dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_kappa" >>= fun hetmet_kappa =>
548 dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_kappa_app" >>= fun hetmet_kappa_app =>
549 dsLookupTyc "GHC.HetMet.Private" "PGArrow" >>= fun hetmet_PGArrow =>
550 dsLookupTyc "Control.GArrow" "GArrowUnit" >>= fun hetmet_PGArrow_unit =>
551 dsLookupTyc "Control.GArrow" "GArrowTensor" >>= fun hetmet_PGArrow_tensor =>
552 dsLookupTyc "Control.GArrow" "GArrowExponent" >>= fun hetmet_PGArrow_exponent =>
553 dsLookupVar "GHC.HetMet.Private" "pga_id" >>= fun hetmet_pga_id =>
554 dsLookupVar "GHC.HetMet.Private" "pga_comp" >>= fun hetmet_pga_comp =>
555 dsLookupVar "GHC.HetMet.Private" "pga_first" >>= fun hetmet_pga_first =>
556 dsLookupVar "GHC.HetMet.Private" "pga_second" >>= fun hetmet_pga_second =>
557 dsLookupVar "GHC.HetMet.Private" "pga_cancell" >>= fun hetmet_pga_cancell =>
558 dsLookupVar "GHC.HetMet.Private" "pga_cancelr" >>= fun hetmet_pga_cancelr =>
559 dsLookupVar "GHC.HetMet.Private" "pga_uncancell" >>= fun hetmet_pga_uncancell =>
560 dsLookupVar "GHC.HetMet.Private" "pga_uncancelr" >>= fun hetmet_pga_uncancelr =>
561 dsLookupVar "GHC.HetMet.Private" "pga_assoc" >>= fun hetmet_pga_assoc =>
562 dsLookupVar "GHC.HetMet.Private" "pga_unassoc" >>= fun hetmet_pga_unassoc =>
563 dsLookupVar "GHC.HetMet.Private" "pga_copy" >>= fun hetmet_pga_copy =>
564 dsLookupVar "GHC.HetMet.Private" "pga_drop" >>= fun hetmet_pga_drop =>
565 dsLookupVar "GHC.HetMet.Private" "pga_swap" >>= fun hetmet_pga_swap =>
566 dsLookupVar "GHC.HetMet.Private" "pga_applyl" >>= fun hetmet_pga_applyl =>
567 dsLookupVar "GHC.HetMet.Private" "pga_applyr" >>= fun hetmet_pga_applyr =>
568 dsLookupVar "GHC.HetMet.Private" "pga_curryl" >>= fun hetmet_pga_curryl =>
569 dsLookupVar "GHC.HetMet.Private" "pga_curryr" >>= fun hetmet_pga_curryr =>
570 dsLookupVar "GHC.HetMet.Private" "pga_loopl" >>= fun hetmet_pga_loopl =>
571 dsLookupVar "GHC.HetMet.Private" "pga_loopr" >>= fun hetmet_pga_loopr =>
572 dsLookupVar "GHC.HetMet.Private" "pga_kappa" >>= fun hetmet_pga_kappa =>
587 hetmet_PGArrow_tensor
588 (* hetmet_PGArrow_exponent_TyCon*)