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"
  54 [
  55 "{- 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))"
  56 ]
  57 "{- 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))".
  58 Extract Constant zero  => "'\000'".
  59 Extract Constant one   => "'\001'".
  60 Extract Constant shift => "\ b c -> Data.Char.chr (((Char.code c) `shiftL` 1) .&. 255 .|. if b then 1 else 0)".
  61
  62 Unset Extraction Optimize.
  63 Unset Extraction AutoInline.
  64
  65 Axiom fail : forall {A}, string -> A.
  66   Extract Inlined Constant fail => "Prelude.error".
  67
  68 Section core2proof.
  69   Context (ce:@CoreExpr CoreVar).
  70
  71   Definition Γ : TypeEnv := nil.
  72
  73   Definition Δ : CoercionEnv Γ := nil.
  74
  75   Definition φ : CoreVar->HaskTyVar Γ :=
  76     fun cv => (fun TV env => fail "unbound tyvar").
  77     (*fun tv => error ("tried to get the representative of an unbound tyvar:" +++ (getCoreVarOccString tv)).*)
  78
  79   Definition ψ : CoreVar->HaskCoVar nil Δ
  80     := fun cv => fail ("tried to get the representative of an unbound covar!" (*+++ (getTypeVarOccString cv)*)).
  81
  82   (* We need to be able to resolve unbound exprvars, but we can be sure their types will have no
  83    * free tyvars in them *)
  84   Definition ξ : WeakExprVar -> WeakType * list WeakTypeVar
  85     := fun (v:WeakExprVar) => ((v:WeakType),nil).
  86
  87   Definition header : string :=
  88     "\documentclass[9pt]{article}"+++eol+++
  89     "\usepackage{amsmath}"+++eol+++
  90     "\usepackage{amssymb}"+++eol+++
  91     "\usepackage{proof}"+++eol+++
  92     "\usepackage{mathpartir}"+++eol+++
  93     "\usepackage{trfrac}"+++eol+++
  94     "\pdfpagewidth 50in"+++eol+++
  95     "\pdfpageheight 10in"+++eol+++
  96     "\def\code#1#2{\Box_{#1} #2}"+++eol+++
  97     "\begin{document}"+++eol.
  98
  99   Definition footer : string :=
 100     eol+++"\end{document}"+++eol.
 101
 102   Definition handleExpr (ce:@CoreExpr CoreVar) : string :=
 103     match coreExprToWeakExpr ce with
 104       | Error s => fail ("unable to convert GHC Core expression into Coq HaskWeak expression due to:\n  "+++s)
 105       | OK me   =>
 106         match weakExprToStrongExpr (*(makeClosedExpression me)*) me Γ Δ φ ψ ξ nil with
 107           | Indexed_Error  s  => fail ("unable to convert HaskWeak to HaskStrong due to:\n  "+++s)
 108           | Indexed_OK    τ e => match e with
 109                                    | Error s => fail ("unable to convert HaskWeak to HaskStrong due to:\n  "+++s)
 110                                    | OK e'   => header +++ (nd_ml_toLatex (@expr2proof _ _ _ _ _ _ e')) +++ footer
 111                                  end
 112         end
 113     end.
 114
 115   Definition handleBind (bind:@CoreBind CoreVar) : string :=
 116     match bind with
 117       | CoreNonRec _ e => handleExpr e
 118       | CoreRec    lbe => fold_left (fun x y => x+++eol+++eol+++y) (map (fun x => handleExpr (snd x)) lbe) ""
 119     end.
 120
 121   Definition coqPassCoreToString (lbinds:list (@CoreBind CoreVar)) : string :=
 122     fold_left (fun x y => x+++eol+++eol+++y) (map handleBind lbinds) "".
 123
 124   Definition coqPassCoreToCore (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
 125     lbinds.
 126
 127 End core2proof.
 128
 129 Extraction "Extraction.hs" coqPassCoreToString coqPassCoreToCore.
 130