Require Import HaskWeakToCore.
Require Import HaskProofToStrong.
-Require Import ProgrammingLanguage.
-
-Require Import HaskProofStratified.
-Require Import HaskProofFlattener.
-
-Require Import ReificationsIsomorphicToGeneralizedArrows.
+Require Import HaskFlattener.
Open Scope string_scope.
Extraction Language Haskell.
| WCoerVar _ => Prelude_error "top-level xi got a coercion variable"
end.
-
Definition header : string :=
- "\documentclass[9pt]{article}"+++eol+++
+ "\documentclass{article}"+++eol+++
"\usepackage{amsmath}"+++eol+++
"\usepackage{amssymb}"+++eol+++
"\usepackage{proof}"+++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=200in,centering]{geometry}"+++eol+++
- "\usepackage[displaymath,tightpage,active]{preview}"+++eol+++
+ "\usepackage[paperwidth=\maxdimen,paperheight=\maxdimen]{geometry}"+++eol+++
+ "\usepackage[tightpage,active]{preview}"+++eol+++
"\begin{document}"+++eol+++
- "\begin{preview}"+++eol.
+ "\setlength\PreviewBorder{5pt}"+++eol.
Definition footer : string :=
- eol+++"\end{preview}"+++
eol+++"\end{document}"+++
eol.
((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
addErrorMessage ("HaskType: " +++ toString τ)
((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => false) τ nil we) >>= fun e =>
- OK (eol+++"$$"+++ toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ e))+++"$$"+++eol)
+ OK (eol+++eol+++eol+++
+ "\begin{preview}"+++eol+++
+ "$\displaystyle "+++
+ toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ e))+++
+ " $"+++eol+++
+ "\end{preview}"+++eol+++eol+++eol)
)))))))).
Definition coreToStringExpr (ce:@CoreExpr CoreVar) : string :=
((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
(addErrorMessage ("HaskStrong...")
- (let haskProof := @expr2proof _ _ _ _ _ _ e
+ (let haskProof := (*flatten_proof'*) (@expr2proof _ _ _ _ _ _ e)
in (* insert HaskProof-to-HaskProof manipulations here *)
OK ((@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
>>= fun e' =>
End CoreToCore.
+ Definition coreVarToWeakExprVarOrError cv :=
+ match coreVarToWeakVar cv with
+ | WExprVar wv => wv
+ | _ => Prelude_error "IMPOSSIBLE"
+ end.
+
Definition coqPassCoreToCore
(hetmet_brak : CoreVar)
(hetmet_esc : CoreVar)
(uniqueSupply : UniqSupply)
- (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
- match coreVarToWeakVar hetmet_brak with
- | WExprVar hetmet_brak' => match coreVarToWeakVar hetmet_esc with
- | WExprVar hetmet_esc' => coqPassCoreToCore' hetmet_brak' hetmet_esc' uniqueSupply lbinds
- | _ => Prelude_error "IMPOSSIBLE"
- end
- | _ => Prelude_error "IMPOSSIBLE"
- end.
+ (lbinds:list (@CoreBind CoreVar)
+ ) : list (@CoreBind CoreVar) :=
+ coqPassCoreToCore'
+ (coreVarToWeakExprVarOrError hetmet_brak)
+ (coreVarToWeakExprVarOrError hetmet_esc)
+ uniqueSupply
+ lbinds.
End core2proof.