restore HaskWeakToStrong functionality that I broke over the weekend

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

diff --git a/src/Extraction.v b/src/Extraction.v
index 1a26e58..65f3f2d 100644 (file)
--- a/src/Extraction.v
+++ b/src/Extraction.v
@@ -50,20 +50,15 @@ Extract Inlined Constant ascii_dec => "(==)".
 Extract Inductive string => "Prelude.String" [ "[]" "(:)" ].
 
 (* adapted from ExtrOcamlString.v *)
-Extract Inductive ascii => "Prelude.Char"
-[
-"{- If this appears, you're using Ascii internals. Please don't -} (\ b0 b1 b2 b3 b4 b5 b6 b7 ->   let f b i = if b then 1 `shiftL` i else 0 in Data.Char.chr (f b0 0 .|. f b1 1 .|. f b2 2 .|. f b3 3 .|. f b4 4 .|. f b5 5 .|. f b6 6 .|. f b7 7))"
-]
-"{- If this appears, you're using Ascii internals. Please don't -} (\ f c -> let n = Char.code c in let h i = (n .&. (1 `shiftL` i)) /= 0 in f (h 0) (h 1) (h 2) (h 3) (h 4) (h 5) (h 6) (h 7))".
-Extract Constant zero  => "'\000'".
-Extract Constant one   => "'\001'".
-Extract Constant shift => "\ b c -> Data.Char.chr (((Char.code c) `shiftL` 1) .&. 255 .|. if b then 1 else 0)".
+Extract Inductive ascii => "Prelude.Char" [ "bin2ascii" ] "bin2ascii'".
+Extract Constant zero   => "'\000'".
+Extract Constant one    => "'\001'".
+Extract Constant shift  => "shiftAscii".
 
 Unset Extraction Optimize.
 Unset Extraction AutoInline.
 
-Axiom fail : forall {A}, string -> A. 
-  Extract Inlined Constant fail => "Prelude.error".
+Variable Prelude_error : forall {A}, string -> A.   Extract Inlined Constant Prelude_error => "Prelude.error".
 
 Section core2proof.
   Context (ce:@CoreExpr CoreVar).
@@ -72,17 +67,24 @@ Section core2proof.
 
   Definition Δ : CoercionEnv Γ := nil.
 
-  Definition φ : CoreVar->HaskTyVar Γ :=
-    fun cv => (fun TV env => fail "unbound tyvar").
+  Definition φ : TyVarResolver Γ :=
+    fun cv => (fun TV env => Prelude_error "unbound tyvar").
     (*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)*)).
+    := fun cv => Prelude_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 ξ : WeakExprVar -> WeakType * list WeakTypeVar
-    := fun (v:WeakExprVar) => ((v:WeakType),nil).
+  Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ :=
+    match coreVarToWeakVar cv with
+      | WExprVar wev => match weakTypeToType'' φ 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 :=
     "\documentclass[9pt]{article}"+++eol+++
@@ -91,25 +93,33 @@ 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
-      | Error s => fail ("unable to convert GHC Core expression into Coq HaskWeak expression due to:\n  "+++s)
-      | OK me   =>
-        match weakExprToStrongExpr (*(makeClosedExpression me)*) me Γ Δ φ ψ ξ nil with
-          | 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
-                                 end
-        end
+      | 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
     end.
 
   Definition handleBind (bind:@CoreBind CoreVar) : string :=
@@ -119,7 +129,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.