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 e2e3800..ae55381 100644 (file)
--- a/src/Extraction.v
+++ b/src/Extraction.v
@@ -58,9 +58,6 @@ Extract Constant shift  => "shiftAscii".
 Unset Extraction Optimize.
 Unset Extraction AutoInline.
 
-Axiom fail : forall {A}, string -> A. 
-  Extract Inlined Constant fail => "Prelude.error".
-
 Section core2proof.
   Context (ce:@CoreExpr CoreVar).
 
@@ -69,18 +66,22 @@ Section core2proof.
   Definition Δ : CoercionEnv Γ := nil.
 
   Definition φ : TyVarResolver Γ :=
-    fun cv => (fun TV env => fail "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 => fail ("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 ξ (wev:WeakExprVar) : LeveledHaskType Γ ★ :=
-    match weakTypeToType' φ wev ★ with
-      | Error s => fail ("Error in top-level xi: " +++ s)
-      | OK    t => t @@ nil
+  Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ :=
+    match coreVarToWeakVar cv with
+      | WExprVar wev => match weakTypeToTypeOfKind φ wev ★ with
+                          | Error s => Prelude_error ("Error in top-level xi: " +++ s)
+                          | OK    t => t @@ nil
+                        end
+      | WTypeVar _   => Prelude_error "top-level xi got a type variable"
+      | WCoerVar _   => Prelude_error "top-level xi got a coercion variable"
     end.
 
   Definition header : string :=
@@ -88,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.
@@ -101,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 => fail ("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 => fail ("unable to calculate HaskType of a HaskWeak expression because: " +++ s)
-                      | OK τ    => match τ with
-                                     | haskTypeOfSomeKind ★  τ' =>
-                                       match weakExprToStrongExpr Γ Δ φ ψ ξ τ' nil (*(makeClosedExpression*) we (* ) *) with
-                                         | Error s => fail ("unable to convert HaskWeak to HaskStrong due to:\n  "+++s)
-                                         | OK e'   => eol+++"$$"+++ nd_ml_toLatex (@expr2proof _ _ _ _ _ _ e')+++"$$"+++eol
-                                       end
-                                     | haskTypeOfSomeKind κ τ' =>
-                                       fail ("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 :=