X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FExtraction.v;h=57e08a3dc313cc21d3d55bf496ad795a7b31fc66;hb=b8f6adf700fa3c67feefaea3d2cf5c4626300489;hp=363e17fcec2b309cfdedce82a79f00b5341b4b95;hpb=ff44b3a9529a8660185f292897aae2f243af51a2;p=coq-hetmet.git

diff --git a/src/Extraction.v b/src/Extraction.v
index 363e17f..57e08a3 100644
--- a/src/Extraction.v
+++ b/src/Extraction.v
@@ -25,7 +25,7 @@ Require Import HaskProof.
 Require Import HaskCoreToWeak.
 Require Import HaskWeakToStrong.
 Require Import HaskStrongToProof.
-(*Require Import HaskProofToStrong.*)
+Require Import HaskProofToStrong.
 Require Import HaskProofToLatex.
 Require Import HaskStrongToWeak.
 Require Import HaskWeakToCore.
@@ -91,13 +91,16 @@ Section core2proof.
     "\usepackage{proof}"+++eol+++
     "\usepackage{mathpartir}"+++eol+++
     "\usepackage{trfrac}"+++eol+++
-    "\pdfpagewidth 50in"+++eol+++
-    "\pdfpageheight 10in"+++eol+++
     "\def\code#1#2{\Box_{#1} #2}"+++eol+++
-    "\begin{document}"+++eol.
+    "\usepackage[paperwidth=20in,centering]{geometry}"+++eol+++
+    "\usepackage[displaymath,tightpage,active]{preview}"+++eol+++
+    "\begin{document}"+++eol+++
+    "\begin{preview}"+++eol.
 
   Definition footer : string :=
-    eol+++"\end{document}"+++eol.
+    eol+++"\end{preview}"+++
+    eol+++"\end{document}"+++
+    eol.
 
   Definition handleExpr (ce:@CoreExpr CoreVar) : string :=
     match coreExprToWeakExpr ce with
@@ -107,7 +110,10 @@ Section core2proof.
           | 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'   => header +++ (nd_ml_toLatex (@expr2proof _ _ _ _ _ _ e')) +++ footer
+                                   | OK e'   =>
+                                     eol+++"$$"+++
+                                     nd_ml_toLatex (@expr2proof _ _ _ _ _ _ e')+++
+                                     "$$"+++eol
                                  end
         end
     end.
@@ -119,7 +125,9 @@ Section core2proof.
     end.
 
   Definition coqPassCoreToString (lbinds:list (@CoreBind CoreVar)) : string :=
-    fold_left (fun x y => x+++eol+++eol+++y) (map handleBind lbinds) "".
+    header +++
+    (fold_left (fun x y => x+++eol+++eol+++y) (map handleBind lbinds) "")
+    +++ footer.
 
   Definition coqPassCoreToCore (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
     lbinds.