X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FExtractionMain.v;h=02643e5049ecabf15e3709568526e1b3e00c4acb;hp=dbeb3ccec21ea55152b6015ccd2fa9d0f529cd70;hb=e83fd6f566ed0a7aaff19d67c2c2b64d08f98f7c;hpb=e536cc4194f350ed6de5d465bcf53fda650b3d12

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index dbeb3cc..02643e5 100644
--- a/src/ExtractionMain.v
+++ b/src/ExtractionMain.v
@@ -13,7 +13,6 @@ Require Import Preamble.
 Require Import General.
 
 Require Import NaturalDeduction.
-Require Import NaturalDeductionToLatex.
 
 Require Import HaskKinds.
 Require Import HaskLiteralsAndTyCons.
@@ -36,10 +35,10 @@ Require Import HaskProofToStrong.
 
 Require Import ProgrammingLanguage.
 
+Require Import HaskProofFlattener.
+Require Import HaskProofStratified.
 Require Import HaskProofCategory.
-(*
-Require Import HaskStrongCategory.
-*)
+
 Require Import ReificationsIsomorphicToGeneralizedArrows.
 
 Open Scope string_scope.
@@ -61,8 +60,7 @@ Extract Inductive unit    => "()" [ "()" ].
 Extract Inlined Constant string_dec => "(==)".
 Extract Inlined Constant ascii_dec => "(==)".
 
-(* adapted from ExtrOcamlString.v *)
-Extract Inductive ascii => "Char" [ "bin2ascii" ] "bin2ascii'".
+Extract Inductive ascii => "Char" [ "you_forgot_to_patch_coq" ] "you_forgot_to_patch_coq".
 Extract Constant zero   => "'\000'".
 Extract Constant one    => "'\001'".
 Extract Constant shift  => "shiftAscii".
@@ -109,27 +107,24 @@ Section core2proof.
     end.
 
 
-  (* core-to-string (-dcoqpass) *)
-
   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{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.
 
-
+  (* core-to-string (-dcoqpass) *)
   Definition coreToStringExpr' (ce:@CoreExpr CoreVar) : ???string :=
     addErrorMessage ("input CoreSyn: " +++ toString ce)
     (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
@@ -141,7 +136,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 :=
@@ -228,51 +228,6 @@ Section core2proof.
       apply t.
       Defined.
 
-    Definition env := ★::nil.
-    Definition freshTV : HaskType env ★ := haskTyVarToType (FreshHaskTyVar _).
-    Definition idproof0 : ND Rule [] [env > nil > [] |- [freshTV--->freshTV @@ nil]].
-      eapply nd_comp.
-      eapply nd_comp.
-      eapply nd_rule.
-      apply RVar.
-      eapply nd_rule.
-      eapply (RURule _ _ _ _ (RuCanL _ _)) .
-      eapply nd_rule.
-      eapply RLam.
-      Defined.
-
-(*
-    Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
-    addErrorMessage ("input CoreSyn: " +++ toString ce)
-    (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
-      coreExprToWeakExpr ce >>= fun we =>
-        addErrorMessage ("WeakExpr: " +++ toString we)
-          ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
-            ((weakTypeOfWeakExpr we) >>= fun t =>
-              (addErrorMessage ("WeakType: " +++ toString t)
-                ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
-                  addErrorMessage ("HaskType: " +++ toString τ)
-                  ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
-                        (let haskProof := @expr2proof _ _ _ _ _ _ e
-                          in (* insert HaskProof-to-HaskProof manipulations here *)
-                   (unFresh (@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof))
-                  >>= fun e' => Error (@toString _ (ExprToString _ _ _ _) (projT2 e'))
-(*
-                  >>= fun e' =>
-                    Prelude_error (@toString _ (@ExprToString nat _ _ _ _ _ _) (projT2 e'))
-  *)                  
-)
-)))))))).
-(*                    Error "X").*)
-(*
-                   strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
-                   (projT2 e')
-                         INil
-                         >>= fun q => Error (toString q)
-                  ))))))))).
-*)*)
-
-
     Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
       addErrorMessage ("input CoreSyn: " +++ toString ce)
       (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (