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 HaskLiteralsAndTyCons.
  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 Section core2proof.
  62   Context (ce:@CoreExpr CoreVar).
  63
  64   Definition Γ : TypeEnv := nil.
  65
  66   Definition Δ : CoercionEnv Γ := nil.
  67
  68   Definition φ : TyVarResolver Γ :=
  69     fun cv => Error ("unbound tyvar: " +++ (cv:CoreVar)).
  70     (*fun tv => error ("tried to get the representative of an unbound tyvar:" +++ (getCoreVarOccString tv)).*)
  71
  72   Definition ψ : CoVarResolver Γ Δ :=
  73     fun cv => Error ("tried to get the representative of an unbound covar!" (*+++ (getTypeVarOccString cv)*)).
  74
  75   (* We need to be able to resolve unbound exprvars, but we can be sure their types will have no
  76    * free tyvars in them *)
  77   Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ :=
  78     match coreVarToWeakVar cv with
  79       | WExprVar wev => match weakTypeToTypeOfKind φ wev ★ with
  80                           | Error s => Prelude_error ("Error in top-level xi: " +++ s)
  81                           | OK    t => t @@ nil
  82                         end
  83       | WTypeVar _   => Prelude_error "top-level xi got a type variable"
  84       | WCoerVar _   => Prelude_error "top-level xi got a coercion variable"
  85     end.
  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}   % http://cristal.inria.fr/~remy/latex/"+++eol+++
  93     "\usepackage{trfrac}       % http://www.utdallas.edu/~hamlen/trfrac.sty"+++eol+++
  94     "\def\code#1#2{\Box_{#1} #2}"+++eol+++
  95     "\usepackage[paperwidth=200in,centering]{geometry}"+++eol+++
  96     "\usepackage[displaymath,tightpage,active]{preview}"+++eol+++
  97     "\begin{document}"+++eol+++
  98     "\begin{preview}"+++eol.
  99
 100   Definition footer : string :=
 101     eol+++"\end{preview}"+++
 102     eol+++"\end{document}"+++
 103     eol.
 104
 105   Definition handleExpr' (ce:@CoreExpr CoreVar) : ???string :=
 106     addErrorMessage ("input CoreSyn: " +++ ce)
 107     (addErrorMessage ("input CoreType: " +++ coreTypeOfCoreExpr ce) (
 108       coreExprToWeakExpr ce >>= fun we =>
 109         addErrorMessage ("WeakExpr: " +++ we)
 110           ((addErrorMessage ("CoreType of WeakExpr: " +++ coreTypeOfCoreExpr (weakExprToCoreExpr we))
 111             ((weakTypeOfWeakExpr we) >>= fun t =>
 112               (addErrorMessage ("WeakType: " +++ t)
 113                 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
 114                   addErrorMessage ("HaskType: " +++ τ)
 115                   ((weakExprToStrongExpr Γ Δ φ ψ ξ τ nil we) >>= fun e =>
 116                     OK (eol+++"$$"+++ nd_ml_toLatex (@expr2proof _ _ _ _ _ _ e)+++"$$"+++eol)
 117                   )))))))).
 118
 119   Definition handleExpr (ce:@CoreExpr CoreVar) : string :=
 120     match handleExpr' ce with
 121       | OK x => x
 122       | Error s => Prelude_error s
 123     end.
 124
 125   Definition handleBind (bind:@CoreBind CoreVar) : string :=
 126     match bind with
 127       | CoreNonRec _ e => handleExpr e
 128       | CoreRec    lbe => fold_left (fun x y => x+++eol+++eol+++y) (map (fun x => handleExpr (snd x)) lbe) ""
 129     end.
 130
 131   Definition coqPassCoreToString (lbinds:list (@CoreBind CoreVar)) : string :=
 132     header +++
 133     (fold_left (fun x y => x+++eol+++eol+++y) (map handleBind lbinds) "")
 134     +++ footer.
 135
 136   Definition coqPassCoreToCore (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
 137     lbinds.
 138
 139 End core2proof.
 140
 141 Extraction "Extraction.hs" coqPassCoreToString coqPassCoreToCore.
 142