X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FExtraction.v;h=d83a937ac8e05750da60102ca753bfff38d9b887;hb=54e3d85658516dcf7d8504e94f973a87e255f8f3;hp=542b5d49d7fc8d462a8666b19ad4722467951b80;hpb=703bff3b209bd7d114b49cb736da8af167a4ec71;p=coq-hetmet.git

diff --git a/src/Extraction.v b/src/Extraction.v
index 542b5d4..d83a937 100644
--- a/src/Extraction.v
+++ b/src/Extraction.v
@@ -4,9 +4,31 @@ Set Printing Width 1300000.
 Require Import Coq.Lists.List.
 Require Import Coq.Strings.Ascii.
 Require Import Coq.Strings.String.
-Require Import Main.
+
+Require Import Preamble.
+Require Import General.
+
+Require Import NaturalDeduction.
+Require Import NaturalDeductionToLatex.
+
+Require Import HaskKinds.
+Require Import HaskCoreLiterals.
 Require Import HaskCoreVars.
+Require Import HaskCoreTypes.
 Require Import HaskCore.
+Require Import HaskWeakVars.
+Require Import HaskWeakTypes.
+Require Import HaskWeak.
+Require Import HaskStrongTypes.
+Require Import HaskStrong.
+Require Import HaskProof.
+Require Import HaskCoreToWeak.
+Require Import HaskWeakToStrong.
+Require Import HaskStrongToProof.
+Require Import HaskProofToStrong.
+Require Import HaskProofToLatex.
+Require Import HaskStrongToWeak.
+Require Import HaskWeakToCore.
 
 Open Scope string_scope.
 Extraction Language Haskell.
@@ -28,24 +50,95 @@ 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.
 
-Definition coqCoreToStringPass (s:@CoreExpr CoreVar) : string
-   := "FIXME".
-(*
-Definition coqCoreToCorePass (s:CoreExpr CoreVar) : CoreExpr CoreVar
-   :=
-*)
+Variable Prelude_error : forall {A}, string -> A.   Extract Inlined Constant Prelude_error => "Prelude.error".
+
+Section core2proof.
+  Context (ce:@CoreExpr CoreVar).
+
+  Definition Γ : TypeEnv := nil.
+
+  Definition Δ : CoercionEnv Γ := nil.
+
+  Definition φ : TyVarResolver Γ :=
+    fun cv => Error ("unbound tyvar: " +++ (cv:CoreVar)).
+    (*fun tv => error ("tried to get the representative of an unbound tyvar:" +++ (getCoreVarOccString tv)).*)
+
+  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
+                          | 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+++
+    "\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+++
+    "\begin{document}"+++eol+++
+    "\begin{preview}"+++eol.
+
+  Definition footer : string :=
+    eol+++"\end{preview}"+++
+    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)
+                ((weakTypeToType'' φ t ★) >>= fun τ =>
+                  addErrorMessage ("HaskType: " +++ τ)
+                  ((weakExprToStrongExpr Γ Δ φ ψ ξ τ nil we) >>= fun e =>
+                    OK (eol+++"$$"+++ nd_ml_toLatex (@expr2proof _ _ _ _ _ _ e)+++"$$"+++eol)
+                  )))))))).
+
+  Definition handleExpr (ce:@CoreExpr CoreVar) : string :=
+    match handleExpr' ce with
+      | OK x => x
+      | Error s => Prelude_error s
+    end.
+
+  Definition handleBind (bind:@CoreBind CoreVar) : string :=
+    match bind with
+      | CoreNonRec _ e => handleExpr e
+      | CoreRec    lbe => fold_left (fun x y => x+++eol+++eol+++y) (map (fun x => handleExpr (snd x)) lbe) ""
+    end.
+
+  Definition coqPassCoreToString (lbinds:list (@CoreBind CoreVar)) : string :=
+    header +++
+    (fold_left (fun x y => x+++eol+++eol+++y) (map handleBind lbinds) "")
+    +++ footer.
+
+  Definition coqPassCoreToCore (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
+    lbinds.
+
+End core2proof.
 
-Extraction "Extraction.hs" coqCoreToStringPass.
+Extraction "Extraction.hs" coqPassCoreToString coqPassCoreToCore.