further improvements to flattener

[coq-hetmet.git] / src / ExtractionMain.v

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index 4e5a024..9f094bb 100644 (file)
--- a/src/ExtractionMain.v
+++ b/src/ExtractionMain.v
@@ -33,12 +33,7 @@ Require Import HaskStrongToWeak.
 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.
@@ -105,22 +100,19 @@ Section core2proof.
       | 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.
 
@@ -136,7 +128,12 @@ Section core2proof.
                 ((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 :=
@@ -236,7 +233,7 @@ Section core2proof.
                     ((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' =>
@@ -264,17 +261,22 @@ Section core2proof.
 
   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.