minor cleanups, deleted dead code, eliminated use of (==) on CoreType

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

diff --git a/src/Extraction.v b/src/Extraction.v
index 65f3f2d..ae55381 100644 (file)
--- a/src/Extraction.v
+++ b/src/Extraction.v
@@ -58,8 +58,6 @@ Extract Constant shift  => "shiftAscii".
 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).
 
@@ -68,17 +66,17 @@ Section core2proof.
   Definition Δ : CoercionEnv Γ := nil.
 
   Definition φ : TyVarResolver Γ :=
-    fun cv => (fun TV env => Prelude_error "unbound tyvar").
+    fun cv => Error ("unbound tyvar: " +++ (cv:CoreVar)).
     (*fun tv => error ("tried to get the representative of an unbound tyvar:" +++ (getCoreVarOccString tv)).*)
 
-  Definition ψ : CoreVar->HaskCoVar nil Δ
-    := fun cv => Prelude_error ("tried to get the representative of an unbound covar!" (*+++ (getTypeVarOccString cv)*)).
+  Definition ψ : CoVarResolver Γ Δ :=
+    fun cv => Error ("tried to get the representative of an unbound covar!" (*+++ (getTypeVarOccString cv)*)).
 
   (* We need to be able to resolve unbound exprvars, but we can be sure their types will have no
    * 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
@@ -91,10 +89,10 @@ Section core2proof.
     "\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.
@@ -104,22 +102,24 @@ Section core2proof.
     eol+++"\end{document}"+++
     eol.
 
+  Definition handleExpr' (ce:@CoreExpr CoreVar) : ???string :=
+    addErrorMessage ("input CoreSyn: " +++ ce)
+    (addErrorMessage ("input CoreType: " +++ coreTypeOfCoreExpr ce) (
+      coreExprToWeakExpr ce >>= fun we =>
+        addErrorMessage ("WeakExpr: " +++ we)
+          ((addErrorMessage ("CoreType of WeakExpr: " +++ coreTypeOfCoreExpr (weakExprToCoreExpr we))
+            ((weakTypeOfWeakExpr we) >>= fun t =>
+              (addErrorMessage ("WeakType: " +++ t)
+                ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
+                  addErrorMessage ("HaskType: " +++ τ)
+                  ((weakExprToStrongExpr Γ Δ φ ψ ξ τ nil we) >>= fun e =>
+                    OK (eol+++"$$"+++ nd_ml_toLatex (@expr2proof _ _ _ _ _ _ e)+++"$$"+++eol)
+                  )))))))).
+
   Definition handleExpr (ce:@CoreExpr CoreVar) : string :=
-    match coreExprToWeakExpr ce with
-      | Error s => Prelude_error ("unable to convert GHC Core expression into Coq HaskWeak expression due to:\n  "+++s)
-      | OK we   =>  match weakTypeOfWeakExpr we >>= fun t => weakTypeToType φ t with
-                      | Error s => Prelude_error ("unable to calculate HaskType of a HaskWeak expression because: " +++ s)
-                      | OK τ    => match τ with
-                                     | haskTypeOfSomeKind ★  τ' =>
-                                       match weakExprToStrongExpr Γ Δ φ ψ ξ τ' nil (*(makeClosedExpression*) we (* ) *) with
-                                         | Error s => Prelude_error ("unable to convert HaskWeak to HaskStrong due to:\n  "+++s)
-                                         | OK e'   => eol+++"$$"+++ nd_ml_toLatex (@expr2proof _ _ _ _ _ _ e')+++"$$"+++eol
-                                       end
-                                     | haskTypeOfSomeKind κ τ' =>
-                                       Prelude_error ("encountered 'expression' of kind "+++κ+++" at top level (type "+++τ'
-                                              +++"); shouldn't happen")
-                                   end
-                    end
+    match handleExpr' ce with
+      | OK x => x
+      | Error s => Prelude_error s
     end.
 
   Definition handleBind (bind:@CoreBind CoreVar) : string :=