+Axiom fail : forall {A}, string -> A.
+ Extract Inlined Constant fail => "Prelude.error".
+
+Section core2proof.
+ Context (ce:@CoreExpr CoreVar).
+
+ Definition Γ : TypeEnv := nil.
+
+ Definition Δ : CoercionEnv Γ := nil.
+
+ Definition φ : CoreVar->HaskTyVar Γ :=
+ fun cv => (fun TV env => fail "unbound tyvar").
+ (*fun tv => error ("tried to get the representative of an unbound tyvar:" +++ (getCoreVarOccString tv)).*)
+
+ Definition ψ : CoreVar->HaskCoVar nil Δ
+ := fun cv => fail ("tried to get the representative of an unbound covar!" (*+++ (getTypeVarOccString cv)*)).
+
+ (* We need to be able to resolve unbound exprvars, but we can be sure their types will have no
+ * free tyvars in them *)
+ Definition ξ : WeakExprVar -> WeakType * list WeakTypeVar
+ := fun (v:WeakExprVar) => ((v:WeakType),nil).
+
+ Definition header : string :=
+ "\documentclass[9pt]{article}"+++eol+++
+ "\usepackage{amsmath}"+++eol+++
+ "\usepackage{amssymb}"+++eol+++
+ "\usepackage{proof}"+++eol+++
+ "\usepackage{mathpartir}"+++eol+++
+ "\usepackage{trfrac}"+++eol+++
+ "\def\code#1#2{\Box_{#1} #2}"+++eol+++
+ "\usepackage[paperwidth=20in,centering]{geometry}"+++eol+++
+ "\usepackage[displaymath,tightpage,active]{preview}"+++eol+++
+ "\begin{document}"+++eol+++
+ "\begin{preview}"+++eol.
+
+ Definition footer : string :=
+ eol+++"\end{preview}"+++
+ eol+++"\end{document}"+++
+ eol.
+
+ Definition handleExpr (ce:@CoreExpr CoreVar) : string :=
+ match coreExprToWeakExpr ce with
+ | Error s => fail ("unable to convert GHC Core expression into Coq HaskWeak expression due to:\n "+++s)
+ | OK me =>
+ match weakExprToStrongExpr (*(makeClosedExpression me)*) me Γ Δ φ ψ ξ nil with
+ | Indexed_Error s => fail ("unable to convert HaskWeak to HaskStrong due to:\n "+++s)
+ | Indexed_OK τ e => match e with
+ | Error s => fail ("unable to convert HaskWeak to HaskStrong due to:\n "+++s)
+ | OK e' =>
+ eol+++"$$"+++
+ nd_ml_toLatex (@expr2proof _ _ _ _ _ _ e')+++
+ "$$"+++eol
+ end
+ end
+ end.
+
+ Definition handleBind (bind:@CoreBind CoreVar) : string :=
+ match bind with
+ | CoreNonRec _ e => handleExpr e
+ | CoreRec lbe => fold_left (fun x y => x+++eol+++eol+++y) (map (fun x => handleExpr (snd x)) lbe) ""
+ end.
+
+ Definition coqPassCoreToString (lbinds:list (@CoreBind CoreVar)) : string :=
+ header +++
+ (fold_left (fun x y => x+++eol+++eol+++y) (map handleBind lbinds) "")
+ +++ footer.
+
+ Definition coqPassCoreToCore (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
+ lbinds.
+
+End core2proof.