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
  62 Variable Name : Type.  Extract Inlined Constant Name => "Name.Name".
  63 Variable mkSystemName : Unique -> string -> nat -> Name.
  64   Extract Inlined Constant mkSystemName => "(\u s d -> Name.mkSystemName u (OccName.mkOccName (OccName.varNameDepth (nat2int d)) s))".
  65 Variable mkTyVar : Name -> Kind -> CoreVar.
  66   Extract Inlined Constant mkTyVar => "(\n k -> Var.mkTyVar n (kindToCoreKind k))".
  67 Variable mkCoVar : Name -> CoreType -> CoreType -> CoreVar.
  68   Extract Inlined Constant mkCoVar => "(\n t1 t2 -> Var.mkCoVar n (Coercion.mkCoKind t1 t2))".
  69 Variable mkExVar : Name -> CoreType -> CoreVar.
  70   Extract Inlined Constant mkExVar => "Id.mkLocalId".
  71
  72 Section core2proof.
  73   Context (ce:@CoreExpr CoreVar).
  74
  75   Definition Γ : TypeEnv := nil.
  76
  77   Definition Δ : CoercionEnv Γ := nil.
  78
  79   Definition φ : TyVarResolver Γ :=
  80     fun cv => Error ("unbound tyvar: " +++ (cv:CoreVar)).
  81     (*fun tv => error ("tried to get the representative of an unbound tyvar:" +++ (getCoreVarOccString tv)).*)
  82
  83   Definition ψ : CoVarResolver Γ Δ :=
  84     fun cv => Error ("tried to get the representative of an unbound covar!" (*+++ (getTypeVarOccString cv)*)).
  85
  86   (* We need to be able to resolve unbound exprvars, but we can be sure their types will have no
  87    * free tyvars in them *)
  88   Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ :=
  89     match coreVarToWeakVar cv with
  90       | WExprVar wev => match weakTypeToTypeOfKind φ wev ★ with
  91                           | Error s => Prelude_error ("Error in top-level xi: " +++ s)
  92                           | OK    t => t @@ nil
  93                         end
  94       | WTypeVar _   => Prelude_error "top-level xi got a type variable"
  95       | WCoerVar _   => Prelude_error "top-level xi got a coercion variable"
  96     end.
  97
  98
  99   (* core-to-string (-dcoqpass) *)
 100
 101   Definition header : string :=
 102     "\documentclass[9pt]{article}"+++eol+++
 103     "\usepackage{amsmath}"+++eol+++
 104     "\usepackage{amssymb}"+++eol+++
 105     "\usepackage{proof}"+++eol+++
 106     "\usepackage{mathpartir}   % http://cristal.inria.fr/~remy/latex/"+++eol+++
 107     "\usepackage{trfrac}       % http://www.utdallas.edu/~hamlen/trfrac.sty"+++eol+++
 108     "\def\code#1#2{\Box_{#1} #2}"+++eol+++
 109     "\usepackage[paperwidth=200in,centering]{geometry}"+++eol+++
 110     "\usepackage[displaymath,tightpage,active]{preview}"+++eol+++
 111     "\begin{document}"+++eol+++
 112     "\begin{preview}"+++eol.
 113
 114   Definition footer : string :=
 115     eol+++"\end{preview}"+++
 116     eol+++"\end{document}"+++
 117     eol.
 118
 119   Definition coreToStringExpr' (ce:@CoreExpr CoreVar) : ???string :=
 120     addErrorMessage ("input CoreSyn: " +++ ce)
 121     (addErrorMessage ("input CoreType: " +++ coreTypeOfCoreExpr ce) (
 122       coreExprToWeakExpr ce >>= fun we =>
 123         addErrorMessage ("WeakExpr: " +++ we)
 124           ((addErrorMessage ("CoreType of WeakExpr: " +++ coreTypeOfCoreExpr (weakExprToCoreExpr we))
 125             ((weakTypeOfWeakExpr we) >>= fun t =>
 126               (addErrorMessage ("WeakType: " +++ t)
 127                 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
 128                   addErrorMessage ("HaskType: " +++ τ)
 129                   ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
 130                     OK (eol+++"$$"+++ nd_ml_toLatex (@expr2proof _ _ _ _ _ _ e)+++"$$"+++eol)
 131                   )))))))).
 132
 133   Definition coreToStringExpr (ce:@CoreExpr CoreVar) : string :=
 134     match coreToStringExpr' ce with
 135       | OK x => x
 136       | Error s => Prelude_error s
 137     end.
 138
 139   Definition coreToStringBind (binds:@CoreBind CoreVar) : string :=
 140     match binds with
 141       | CoreNonRec _ e => coreToStringExpr e
 142       | CoreRec    lbe => fold_left (fun x y => x+++eol+++eol+++y) (map (fun x => coreToStringExpr (snd x)) lbe) ""
 143     end.
 144
 145   Definition coqPassCoreToString (lbinds:list (@CoreBind CoreVar)) : string :=
 146     header +++
 147     (fold_left (fun x y => x+++eol+++eol+++y) (map coreToStringBind lbinds) "")
 148     +++ footer.
 149
 150
 151   (* core-to-core (-fcoqpass) *)
 152   Section CoreToCore.
 153
 154     Definition mkWeakTypeVar (u:Unique)(k:Kind)                 : WeakTypeVar :=
 155       weakTypeVar (mkTyVar (mkSystemName u "tv" O) k) k.
 156     Definition mkWeakCoerVar (u:Unique)(k:Kind)(t1 t2:WeakType) : WeakCoerVar :=
 157       weakCoerVar (mkCoVar (mkSystemName u "cv" O) (weakTypeToCoreType t1) (weakTypeToCoreType t2)) k t1 t2.
 158     Definition mkWeakExprVar (u:Unique)(t:WeakType)             : WeakExprVar :=
 159       weakExprVar (mkExVar (mkSystemName u "ev" O) (weakTypeToCoreType t)) t.
 160
 161     Context (hetmet_brak  : WeakExprVar).
 162     Context (hetmet_esc   : WeakExprVar).
 163     Context (uniqueSupply : UniqSupply).
 164
 165     Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
 166       addErrorMessage ("input CoreSyn: " +++ ce)
 167       (addErrorMessage ("input CoreType: " +++ coreTypeOfCoreExpr ce) (
 168         coreExprToWeakExpr ce >>= fun we =>
 169           addErrorMessage ("WeakExpr: " +++ we)
 170             ((addErrorMessage ("CoreType of WeakExpr: " +++ coreTypeOfCoreExpr (weakExprToCoreExpr we))
 171               ((weakTypeOfWeakExpr we) >>= fun t =>
 172                 (addErrorMessage ("WeakType: " +++ t)
 173                   ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
 174
 175                     ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
 176                       (* insert HaskStrong-to-HaskStrong manipulations here *)
 177                       strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply e INil
 178                       >>= fun q => OK (weakExprToCoreExpr q)
 179 (*
 180                     OK (weakExprToCoreExpr we)
 181 *)
 182                     )))))))).
 183
 184     Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) :=
 185       match coreToCoreExpr' ce with
 186         | OK x    => x
 187         | Error s => Prelude_error s
 188       end.
 189
 190     Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar :=
 191       match binds with
 192         | CoreNonRec v e => CoreNonRec v (coreToCoreExpr e)
 193         | CoreRec    lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
 194       end.
 195
 196     Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
 197       map coreToCoreBind lbinds.
 198
 199   End CoreToCore.
 200
 201   Definition coqPassCoreToCore
 202     (hetmet_brak  : CoreVar)
 203     (hetmet_esc   : CoreVar)
 204     (uniqueSupply : UniqSupply)
 205     (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
 206     match coreVarToWeakVar hetmet_brak with
 207       | WExprVar hetmet_brak' => match coreVarToWeakVar hetmet_esc with
 208                                    | WExprVar hetmet_esc' => coqPassCoreToCore' hetmet_brak' hetmet_esc' uniqueSupply lbinds
 209                                    | _ => Prelude_error "IMPOSSIBLE"
 210                                  end
 211       | _ => Prelude_error "IMPOSSIBLE"
 212     end.
 213
 214 End core2proof.
 215
 216 Extraction "Extraction.hs" coqPassCoreToString coqPassCoreToCore.
 217