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_flatten : WeakExprVar).
185 Context (hetmet_unflatten : WeakExprVar).
186 Context (hetmet_flattened_id : WeakExprVar).
187 Context (uniqueSupply : UniqSupply).
189 Definition useUniqueSupply {T}(ut:UniqM T) : ???T :=
192 f uniqueSupply >>= fun x => OK (snd x)
195 Definition larger : forall ln:list nat, { n:nat & forall n', In n' ln -> gt n n' }.
201 destruct IHln as [n pf].
202 exists (plus (S n) a).
206 fold (@In _ n' ln) in H.
211 Definition FreshNat : @FreshMonad nat.
212 refine {| FMT := fun T => nat -> prod nat T
218 set (larger tl) as q.
219 destruct q as [n' pf].
225 refine {| returnM := fun a (v:a) => _ |}.
226 intro n. exact (n,v).
229 destruct q as [n' v].
234 Definition unFresh {T} : @FreshM _ FreshNat T -> T.
243 Definition coreVarToWeakExprVarOrError cv :=
244 match addErrorMessage ("in coreVarToWeakExprVarOrError" +++ eol) (coreVarToWeakVar' cv) with
245 | OK (WExprVar wv) => wv
246 | Error s => Prelude_error s
247 | _ => Prelude_error "IMPOSSIBLE"
250 Definition curry {Γ}{Δ}{a}{s}{Σ}{lev} :
252 [ Γ > Δ > Σ |- [a ---> s ]@lev ]
253 [ Γ > Δ > [a @@ lev],,Σ |- [ s ]@lev ].
254 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
255 eapply nd_comp; [ idtac | eapply nd_rule; eapply RApp ].
256 eapply nd_comp; [ apply nd_rlecnac | idtac ].
263 Definition fToC1 {Γ}{Δ}{a}{s}{lev} :
264 ND Rule [] [ Γ > Δ > [ ] |- [a ---> s ]@lev ] ->
265 ND Rule [] [ Γ > Δ > [a @@ lev] |- [ s ]@lev ].
269 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanR ].
273 Definition fToC2 {Γ}{Δ}{a1}{a2}{s}{lev} :
274 ND Rule [] [ Γ > Δ > [] |- [a1 ---> (a2 ---> s) ]@lev ] ->
275 ND Rule [] [ Γ > Δ > [a1 @@ lev],,[a2 @@ lev] |- [ s ]@lev ].
286 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
290 Section coqPassCoreToCore.
293 (do_skolemize : bool)
294 (hetmet_brak : CoreVar)
295 (hetmet_esc : CoreVar)
296 (hetmet_flatten : CoreVar)
297 (hetmet_unflatten : CoreVar)
298 (hetmet_flattened_id : CoreVar)
299 (uniqueSupply : UniqSupply)
300 (lbinds:list (@CoreBind CoreVar))
301 (hetmet_PGArrowTyCon : TyFun)
302 (hetmet_PGArrow_unit_TyCon : TyFun)
303 (hetmet_PGArrow_tensor_TyCon : TyFun)
304 (hetmet_PGArrow_exponent_TyCon : TyFun)
305 (hetmet_pga_id : CoreVar)
306 (hetmet_pga_comp : CoreVar)
307 (hetmet_pga_first : CoreVar)
308 (hetmet_pga_second : CoreVar)
309 (hetmet_pga_cancell : CoreVar)
310 (hetmet_pga_cancelr : CoreVar)
311 (hetmet_pga_uncancell : CoreVar)
312 (hetmet_pga_uncancelr : CoreVar)
313 (hetmet_pga_assoc : CoreVar)
314 (hetmet_pga_unassoc : CoreVar)
315 (hetmet_pga_copy : CoreVar)
316 (hetmet_pga_drop : CoreVar)
317 (hetmet_pga_swap : CoreVar)
318 (hetmet_pga_applyl : CoreVar)
319 (hetmet_pga_applyr : CoreVar)
320 (hetmet_pga_curryl : CoreVar)
321 (hetmet_pga_curryr : CoreVar)
322 (hetmet_pga_loopl : CoreVar)
323 (hetmet_pga_loopr : CoreVar)
327 Definition ga_unit TV (ec:RawHaskType TV ECKind) : RawHaskType TV ★ :=
328 @TyFunApp TV hetmet_PGArrow_unit_TyCon (ECKind::nil) ★ (TyFunApp_cons _ _ ec TyFunApp_nil).
330 Definition ga_prod TV (ec:RawHaskType TV ECKind) (a b:RawHaskType TV ★) : RawHaskType TV ★ :=
332 hetmet_PGArrow_tensor_TyCon
333 (ECKind::★ ::★ ::nil) ★
334 (TyFunApp_cons _ _ ec
339 Definition ga_type {TV}(a:RawHaskType TV ECKind)(b c:RawHaskType TV ★) : RawHaskType TV ★ :=
340 TApp (TApp (TApp (@TyFunApp TV
342 nil _ TyFunApp_nil) a) b) c.
344 Definition ga := @ga_mk ga_unit ga_prod (@ga_type).
346 Definition ga_type' {Γ}(a:HaskType Γ ECKind)(b c:HaskType Γ ★) : HaskType Γ ★ :=
347 fun TV ite => TApp (TApp (TApp (@TyFunApp TV
349 nil _ TyFunApp_nil) (a TV ite)) (b TV ite)) (c TV ite).
351 Definition mkGlob2' {Γ}{κ₁}{κ₂}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ ★) :
352 IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::nil) -> HaskType Γ ★.
359 Definition mkGlob2 {Γ}{Δ}{l}{κ₁}{κ₂}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ ★) x y
360 : ND Rule [] [ Γ > Δ > [] |- [f x y ]@l ].
362 refine (@RGlobal Γ Δ l
363 {| glob_wv := coreVarToWeakExprVarOrError cv
364 ; glob_kinds := κ₁ :: κ₂ :: nil
365 ; glob_tf := mkGlob2'(Γ:=Γ) f
366 |} (ICons _ _ x (ICons _ _ y INil))).
369 Definition mkGlob3' {Γ}{κ₁}{κ₂}{κ₃}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ ★) :
370 IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::κ₃::nil) -> HaskType Γ ★.
378 Definition mkGlob3 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ ★) x y z
379 : ND Rule [] [ Γ > Δ > [] |- [f x y z ]@l ].
381 refine (@RGlobal Γ Δ l
382 {| glob_wv := coreVarToWeakExprVarOrError cv
383 ; glob_kinds := κ₁ :: κ₂ :: κ₃ :: nil
384 ; glob_tf := mkGlob3'(Γ:=Γ) f
385 |} (ICons _ _ x (ICons _ _ y (ICons _ _ z INil)))).
388 Definition mkGlob4' {Γ}{κ₁}{κ₂}{κ₃}{κ₄}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ κ₄ -> HaskType Γ ★) :
389 IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::κ₃::κ₄::nil) -> HaskType Γ ★.
398 Definition mkGlob4 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}{κ₄}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ κ₄ -> HaskType Γ ★) x y z q
399 : ND Rule [] [ Γ > Δ > [] |- [f x y z q ] @l].
401 refine (@RGlobal Γ Δ l
402 {| glob_wv := coreVarToWeakExprVarOrError cv
403 ; glob_kinds := κ₁ :: κ₂ :: κ₃ :: κ₄ :: nil
404 ; glob_tf := mkGlob4'(Γ:=Γ) f
405 |} (ICons _ _ x (ICons _ _ y (ICons _ _ z (ICons _ _ q INil))))).
408 Definition gat {Γ} ec (x:Tree ??(HaskType Γ ★)) := @ga_mk_tree ga_unit ga_prod _ ec x.
410 Instance my_ga : garrow ga_unit ga_prod (@ga_type) :=
411 { ga_id := fun Γ Δ ec l a => mkGlob2 hetmet_pga_id (fun ec a => ga_type' ec a a) ec (gat ec a)
412 ; ga_cancelr := fun Γ Δ ec l a => mkGlob2 hetmet_pga_cancelr (fun ec a => ga_type' ec _ a) ec (gat ec a)
413 ; ga_cancell := fun Γ Δ ec l a => mkGlob2 hetmet_pga_cancell (fun ec a => ga_type' ec _ a) ec (gat ec a)
414 ; ga_uncancelr := fun Γ Δ ec l a => mkGlob2 hetmet_pga_uncancelr (fun ec a => ga_type' ec a _) ec (gat ec a)
415 ; ga_uncancell := fun Γ Δ ec l a => mkGlob2 hetmet_pga_uncancell (fun ec a => ga_type' ec a _) ec (gat ec a)
416 ; 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)
417 ; 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)
418 ; 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)
419 ; ga_drop := fun Γ Δ ec l a => mkGlob2 hetmet_pga_drop (fun ec a => ga_type' ec _ _) ec (gat ec a)
420 ; ga_copy := fun Γ Δ ec l a => mkGlob2 hetmet_pga_copy (fun ec a => ga_type' ec _ _) ec (gat ec a)
421 ; 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))
422 ; 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))
423 ; 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))
424 (* ; ga_lit := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_lit))*)
425 (* ; ga_curry := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_curry))*)
426 (* ; ga_apply := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_apply))*)
427 (* ; ga_kappa := fun Γ Δ ec l a => fToC1 (nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_kappa)))*)
428 ; 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))
429 ; 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))
430 ; ga_lit := fun Γ Δ ec l a => Prelude_error "ga_lit"
431 ; ga_curry := fun Γ Δ ec l a b c => Prelude_error "ga_curry"
432 ; ga_apply := fun Γ Δ ec l a b c => Prelude_error "ga_apply"
433 ; ga_kappa := fun Γ Δ ec l a => Prelude_error "ga_kappa"
436 Definition hetmet_brak' := coreVarToWeakExprVarOrError hetmet_brak.
437 Definition hetmet_esc' := coreVarToWeakExprVarOrError hetmet_esc.
438 Definition hetmet_flatten' := coreVarToWeakExprVarOrError hetmet_flatten.
439 Definition hetmet_unflatten' := coreVarToWeakExprVarOrError hetmet_unflatten.
440 Definition hetmet_flattened_id' := coreVarToWeakExprVarOrError hetmet_flattened_id.
442 Definition coreToCoreExpr' (cex:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
443 addErrorMessage ("input CoreSyn: " +++ toString cex)
444 (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr cex)) (
445 coreExprToWeakExpr cex >>= fun we =>
446 addErrorMessage ("WeakExpr: " +++ toString we)
447 ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
448 ((weakTypeOfWeakExpr we) >>= fun t =>
449 (addErrorMessage ("WeakType: " +++ toString t)
450 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
452 ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
454 (addErrorMessage ("HaskStrong...")
457 (let haskProof := skolemize_and_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 _ _ (flatten_type τ) 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))
469 (let haskProof := flatten_proof (*hetmet_flatten' hetmet_unflatten'
470 hetmet_flattened_id' my_ga*) (@expr2proof _ _ _ _ _ _ _ e)
471 in (* insert HaskProof-to-HaskProof manipulations here *)
472 OK ((@proof2expr nat _ FreshNat _ _ τ 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))
480 (let haskProof := @expr2proof _ _ _ _ _ _ _ e
481 in (* insert HaskProof-to-HaskProof manipulations here *)
482 OK ((@proof2expr nat _ FreshNat _ _ τ nil _
483 (fun _ => Prelude_error "unbound unique") _ haskProof) O)
484 >>= fun e' => (snd e') >>= fun e'' =>
485 strongExprToWeakExpr hetmet_brak' hetmet_esc'
486 mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
488 >>= fun q => OK (weakExprToCoreExpr q))))
491 Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) :=
492 match coreToCoreExpr' ce with
494 | Error s => Prelude_error s
497 Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar :=
499 | CoreNonRec v e => let e' := coreToCoreExpr e in CoreNonRec (setVarType v (coreTypeOfCoreExpr e')) e'
501 | CoreRec lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
502 (* FIXME: doesn't deal with the case where top level recursive binds change type *)
504 match coreToCoreExpr (CoreELet lbe) (CoreELit HaskMachNullAddr) with
505 | CoreELet (CoreRec lbe') => lbe'
507 ("coreToCoreExpr was given a letrec, " +++
508 "but returned something that wasn't a letrec: " +++ toString x)
513 Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
514 map coreToCoreBind lbinds.
516 End coqPassCoreToCore.
518 Notation "a >>= b" := (@CoreMbind _ _ a b).
520 Definition coqPassCoreToCore
522 (do_skolemize : bool)
523 (dsLookupVar : string -> string -> CoreM CoreVar)
524 (dsLookupTyc : string -> string -> CoreM TyFun)
525 (uniqueSupply : UniqSupply)
526 (lbinds : list (@CoreBind CoreVar))
527 : CoreM (list (@CoreBind CoreVar)) :=
528 dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_brak" >>= fun hetmet_brak =>
529 dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_esc" >>= fun hetmet_esc =>
530 dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_flatten" >>= fun hetmet_flatten =>
531 dsLookupVar "GHC.HetMet.CodeTypes" "pga_unflatten" >>= fun hetmet_unflatten =>
532 dsLookupVar "GHC.HetMet.CodeTypes" "pga_flattened_id" >>= fun hetmet_flattened_id =>
533 dsLookupTyc "GHC.HetMet.Private" "PGArrow" >>= fun hetmet_PGArrow =>
534 dsLookupTyc "GHC.HetMet.GArrow" "GArrowUnit" >>= fun hetmet_PGArrow_unit =>
535 dsLookupTyc "GHC.HetMet.GArrow" "GArrowTensor" >>= fun hetmet_PGArrow_tensor =>
536 dsLookupTyc "GHC.HetMet.GArrow" "GArrowExponent" >>= fun hetmet_PGArrow_exponent =>
537 dsLookupVar "GHC.HetMet.Private" "pga_id" >>= fun hetmet_pga_id =>
538 dsLookupVar "GHC.HetMet.Private" "pga_comp" >>= fun hetmet_pga_comp =>
539 dsLookupVar "GHC.HetMet.Private" "pga_first" >>= fun hetmet_pga_first =>
540 dsLookupVar "GHC.HetMet.Private" "pga_second" >>= fun hetmet_pga_second =>
541 dsLookupVar "GHC.HetMet.Private" "pga_cancell" >>= fun hetmet_pga_cancell =>
542 dsLookupVar "GHC.HetMet.Private" "pga_cancelr" >>= fun hetmet_pga_cancelr =>
543 dsLookupVar "GHC.HetMet.Private" "pga_uncancell" >>= fun hetmet_pga_uncancell =>
544 dsLookupVar "GHC.HetMet.Private" "pga_uncancelr" >>= fun hetmet_pga_uncancelr =>
545 dsLookupVar "GHC.HetMet.Private" "pga_assoc" >>= fun hetmet_pga_assoc =>
546 dsLookupVar "GHC.HetMet.Private" "pga_unassoc" >>= fun hetmet_pga_unassoc =>
547 dsLookupVar "GHC.HetMet.Private" "pga_copy" >>= fun hetmet_pga_copy =>
548 dsLookupVar "GHC.HetMet.Private" "pga_drop" >>= fun hetmet_pga_drop =>
549 dsLookupVar "GHC.HetMet.Private" "pga_swap" >>= fun hetmet_pga_swap =>
550 dsLookupVar "GHC.HetMet.Private" "pga_applyl" >>= fun hetmet_pga_applyl =>
551 dsLookupVar "GHC.HetMet.Private" "pga_applyr" >>= fun hetmet_pga_applyr =>
552 dsLookupVar "GHC.HetMet.Private" "pga_curryl" >>= fun hetmet_pga_curryl =>
553 dsLookupVar "GHC.HetMet.Private" "pga_curryr" >>= fun hetmet_pga_curryr =>
554 dsLookupVar "GHC.HetMet.Private" "pga_loopl" >>= fun hetmet_pga_loopl =>
555 dsLookupVar "GHC.HetMet.Private" "pga_loopr" >>= fun hetmet_pga_loopr =>
569 hetmet_PGArrow_tensor
570 (* hetmet_PGArrow_exponent_TyCon*)