add HaskStrongToProof

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

diff --git a/src/Extraction.v b/src/Extraction.v
index 542b5d4..22564a2 100644 (file)
--- 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.
@@ -40,12 +62,69 @@ Extract Constant shift => "\ b c -> Data.Char.chr (((Char.code c) `shiftL` 1) .&
 Unset Extraction Optimize.
 Unset Extraction AutoInline.
 
-Definition coqCoreToStringPass (s:@CoreExpr CoreVar) : string
-   := "FIXME".
-(*
-Definition coqCoreToCorePass (s:CoreExpr CoreVar) : CoreExpr CoreVar
-   :=
-*)
+Axiom fail : forall {A}, string -> A. 
+  Extract Inlined Constant fail => "Prelude.error".
+
+Section core2proof.
+  Context (ce:@CoreExpr CoreVar).
+
+  Definition Γ : TypeEnv := nil.
+
+  Definition Δ : CoercionEnv Γ := nil.
+
+  Definition φ : CoreVar->HaskTyVar Γ :=
+    fun cv => (fun TV env => fail "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)*)).
+
+  (* 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 header : string :=
+    "\documentclass[9pt]{article}"+++eol+++
+    "\usepackage{amsmath}"+++eol+++
+    "\usepackage{amssymb}"+++eol+++
+    "\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.
+
+  Definition footer : string :=
+    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
+    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 :=
+    fold_left (fun x y => x+++eol+++eol+++y) (map handleBind lbinds) "".
+
+  Definition coqPassCoreToCore (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
+    lbinds.
+
+End core2proof.
 
-Extraction "Extraction.hs" coqCoreToStringPass.
+Extraction "Extraction.hs" coqPassCoreToString coqPassCoreToCore.