Require Import NaturalDeductionToLatex.
Require Import HaskKinds.
-Require Import HaskCoreLiterals.
+Require Import HaskLiteralsAndTyCons.
Require Import HaskCoreVars.
Require Import HaskCoreTypes.
Require Import HaskCore.
Unset Extraction Optimize.
Unset Extraction AutoInline.
-Variable Prelude_error : forall {A}, string -> A. Extract Inlined Constant Prelude_error => "Prelude.error".
-
Section core2proof.
Context (ce:@CoreExpr CoreVar).
* free tyvars in them *)
Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ :=
match coreVarToWeakVar cv with
- | WExprVar wev => match weakTypeToType'' φ wev ★ with
+ | WExprVar wev => match weakTypeToTypeOfKind φ wev ★ with
| Error s => Prelude_error ("Error in top-level xi: " +++ s)
| OK t => t @@ nil
end
"\usepackage{amsmath}"+++eol+++
"\usepackage{amssymb}"+++eol+++
"\usepackage{proof}"+++eol+++
- "\usepackage{mathpartir}"+++eol+++
- "\usepackage{trfrac}"+++eol+++
+ "\usepackage{mathpartir} % http://cristal.inria.fr/~remy/latex/"+++eol+++
+ "\usepackage{trfrac} % http://www.utdallas.edu/~hamlen/trfrac.sty"+++eol+++
"\def\code#1#2{\Box_{#1} #2}"+++eol+++
- "\usepackage[paperwidth=20in,centering]{geometry}"+++eol+++
+ "\usepackage[paperwidth=200in,centering]{geometry}"+++eol+++
"\usepackage[displaymath,tightpage,active]{preview}"+++eol+++
"\begin{document}"+++eol+++
"\begin{preview}"+++eol.
((addErrorMessage ("CoreType of WeakExpr: " +++ coreTypeOfCoreExpr (weakExprToCoreExpr we))
((weakTypeOfWeakExpr we) >>= fun t =>
(addErrorMessage ("WeakType: " +++ t)
- ((weakTypeToType'' φ t ★) >>= fun τ =>
+ ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
addErrorMessage ("HaskType: " +++ τ)
((weakExprToStrongExpr Γ Δ φ ψ ξ τ nil we) >>= fun e =>
OK (eol+++"$$"+++ nd_ml_toLatex (@expr2proof _ _ _ _ _ _ e)+++"$$"+++eol)