src/Extraction.v

   1 (* need this or the Haskell extraction fails *)
   2 Set Printing Width 1300000.
   3
   4 Require Import Coq.Lists.List.
   5 Require Import Coq.Strings.Ascii.
   6 Require Import Coq.Strings.String.
   7
   8 Require Import Preamble.
   9 Require Import General.
  10
  11 Require Import NaturalDeduction.
  12 Require Import NaturalDeductionToLatex.
  13
  14 Require Import HaskKinds.
  15 Require Import HaskCoreLiterals.
  16 Require Import HaskCoreVars.
  17 Require Import HaskCoreTypes.
  18 Require Import HaskCore.
  19 Require Import HaskWeakVars.
  20 Require Import HaskWeakTypes.
  21 Require Import HaskWeak.
  22 Require Import HaskStrongTypes.
  23 Require Import HaskStrong.
  24 Require Import HaskProof.
  25 Require Import HaskCoreToWeak.
  26 Require Import HaskWeakToStrong.
  27 Require Import HaskStrongToProof.
  28 Require Import HaskProofToStrong.
  29 Require Import HaskProofToLatex.
  30 Require Import HaskStrongToWeak.
  31 Require Import HaskWeakToCore.
  32
  33 Open Scope string_scope.
  34 Extraction Language Haskell.
  35
  36 (* I try to reuse Haskell types mostly to get the "deriving Show" aspect *)
  37 Extract Inductive option => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ].
  38 Extract Inductive list   => "([])" [ "([])" "(:)" ].
  39 (*Extract Inductive vec    => "([])" [ "([])" "(:)" ].*)
  40 (*Extract Inductive Tree   => "([])" [ "([])" "(:)" ].*)
  41 Extract Inlined Constant map => "Prelude.map".
  42 Extract Inductive string => "Prelude.String" [ "([])" "(:)" ].
  43 Extract Inductive prod   => "(,)" [ "(,)" ].
  44 Extract Inductive sum    => "Prelude.Either" [ "Prelude.Left" "Prelude.Right" ].
  45 Extract Inductive sumbool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
  46 Extract Inductive bool    => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
  47 Extract Inductive unit    => "()" [ "()" ].
  48 Extract Inlined Constant string_dec => "(==)".
  49 Extract Inlined Constant ascii_dec => "(==)".
  50 Extract Inductive string => "Prelude.String" [ "[]" "(:)" ].
  51
  52 (* adapted from ExtrOcamlString.v *)
  53 Extract Inductive ascii => "Prelude.Char" [ "bin2ascii" ] "bin2ascii'".
  54 Extract Constant zero   => "'\000'".
  55 Extract Constant one    => "'\001'".
  56 Extract Constant shift  => "shiftAscii".
  57
  58 Unset Extraction Optimize.
  59 Unset Extraction AutoInline.
  60
  61 Axiom fail : forall {A}, string -> A.
  62   Extract Inlined Constant fail => "Prelude.error".
  63
  64 Section core2proof.
  65   Context (ce:@CoreExpr CoreVar).
  66
  67   Definition Γ : TypeEnv := nil.
  68
  69   Definition Δ : CoercionEnv Γ := nil.
  70
  71   Definition φ : TyVarResolver Γ :=
  72     fun cv => (fun TV env => fail "unbound tyvar").
  73     (*fun tv => error ("tried to get the representative of an unbound tyvar:" +++ (getCoreVarOccString tv)).*)
  74
  75   Definition ψ : CoreVar->HaskCoVar nil Δ
  76     := fun cv => fail ("tried to get the representative of an unbound covar!" (*+++ (getTypeVarOccString cv)*)).
  77
  78   (* We need to be able to resolve unbound exprvars, but we can be sure their types will have no
  79    * free tyvars in them *)
  80   Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ :=
  81     match coreVarToWeakVar cv with
  82       | WExprVar wev => match weakTypeToType' φ wev ★ with
  83                           | Error s => fail ("Error in top-level xi: " +++ s)
  84                           | OK    t => t @@ nil
  85                         end
  86       | WTypeVar _   => fail "top-level xi got a type variable"
  87       | WCoerVar _   => fail "top-level xi got a coercion variable"
  88     end.
  89
  90   Definition header : string :=
  91     "\documentclass[9pt]{article}"+++eol+++
  92     "\usepackage{amsmath}"+++eol+++
  93     "\usepackage{amssymb}"+++eol+++
  94     "\usepackage{proof}"+++eol+++
  95     "\usepackage{mathpartir}"+++eol+++
  96     "\usepackage{trfrac}"+++eol+++
  97     "\def\code#1#2{\Box_{#1} #2}"+++eol+++
  98     "\usepackage[paperwidth=20in,centering]{geometry}"+++eol+++
  99     "\usepackage[displaymath,tightpage,active]{preview}"+++eol+++
 100     "\begin{document}"+++eol+++
 101     "\begin{preview}"+++eol.
 102
 103   Definition footer : string :=
 104     eol+++"\end{preview}"+++
 105     eol+++"\end{document}"+++
 106     eol.
 107
 108   Definition handleExpr (ce:@CoreExpr CoreVar) : string :=
 109     match coreExprToWeakExpr ce with
 110       | Error s => fail ("unable to convert GHC Core expression into Coq HaskWeak expression due to:\n  "+++s)
 111       | OK we   =>  match weakTypeOfWeakExpr we >>= fun t => weakTypeToType φ t with
 112                       | Error s => fail ("unable to calculate HaskType of a HaskWeak expression because: " +++ s)
 113                       | OK τ    => match τ with
 114                                      | haskTypeOfSomeKind ★  τ' =>
 115                                        match weakExprToStrongExpr Γ Δ φ ψ ξ τ' nil (*(makeClosedExpression*) we (* ) *) with
 116                                          | Error s => fail ("unable to convert HaskWeak to HaskStrong due to:\n  "+++s)
 117                                          | OK e'   => eol+++"$$"+++ nd_ml_toLatex (@expr2proof _ _ _ _ _ _ e')+++"$$"+++eol
 118                                        end
 119                                      | haskTypeOfSomeKind κ τ' =>
 120                                        fail ("encountered 'expression' of kind "+++κ+++" at top level (type "+++τ'
 121                                               +++"); shouldn't happen")
 122                                    end
 123                     end
 124     end.
 125
 126   Definition handleBind (bind:@CoreBind CoreVar) : string :=
 127     match bind with
 128       | CoreNonRec _ e => handleExpr e
 129       | CoreRec    lbe => fold_left (fun x y => x+++eol+++eol+++y) (map (fun x => handleExpr (snd x)) lbe) ""
 130     end.
 131
 132   Definition coqPassCoreToString (lbinds:list (@CoreBind CoreVar)) : string :=
 133     header +++
 134     (fold_left (fun x y => x+++eol+++eol+++y) (map handleBind lbinds) "")
 135     +++ footer.
 136
 137   Definition coqPassCoreToCore (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
 138     lbinds.
 139
 140 End core2proof.
 141
 142 Extraction "Extraction.hs" coqPassCoreToString coqPassCoreToCore.
 143