src/ExtractionMain.v

   1 (*********************************************************************************************************************************)
   2 (* ExtractionMain:                                                                                                               *)
   3 (*                                                                                                                               *)
   4 (*    This module is the "top level" for extraction                                                                              *)
   5 (*                                                                                                                               *)
   6 (*********************************************************************************************************************************)
   7
   8 Require Import Coq.Strings.Ascii.
   9 Require Import Coq.Strings.String.
  10 Require Import Coq.Lists.List.
  11
  12 Require Import Preamble.
  13 Require Import General.
  14
  15 Require Import NaturalDeduction.
  16
  17 Require Import HaskKinds.
  18 Require Import HaskLiteralsAndTyCons.
  19 Require Import HaskCoreVars.
  20 Require Import HaskCoreTypes.
  21 Require Import HaskCore.
  22 Require Import HaskWeakVars.
  23 Require Import HaskWeakTypes.
  24 Require Import HaskWeak.
  25 Require Import HaskStrongTypes.
  26 Require Import HaskStrong.
  27 Require Import HaskProof.
  28 Require Import HaskCoreToWeak.
  29 Require Import HaskWeakToStrong.
  30 Require Import HaskStrongToProof.
  31 Require Import HaskProofToLatex.
  32 Require Import HaskStrongToWeak.
  33 Require Import HaskWeakToCore.
  34 Require Import HaskProofToStrong.
  35
  36 Require Import ProgrammingLanguage.
  37
  38 Require Import HaskProofFlattener.
  39 Require Import HaskProofStratified.
  40
  41 Require Import ReificationsIsomorphicToGeneralizedArrows.
  42
  43 Open Scope string_scope.
  44 Extraction Language Haskell.
  45
  46 (*Extract Inductive vec    => "([])" [ "([])" "(:)" ].*)
  47 (*Extract Inductive Tree   => "([])" [ "([])" "(:)" ].*)
  48 (*Extract Inlined Constant map => "Prelude.map".*)
  49
  50 (* I try to reuse Haskell types mostly to get the "deriving Show" aspect *)
  51 Extract Inductive option => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ].
  52 Extract Inductive list   => "([])" [ "([])" "(:)" ].
  53 Extract Inductive string => "Prelude.String" [ "[]" "(:)" ].
  54 Extract Inductive prod   => "(,)" [ "(,)" ].
  55 Extract Inductive sum    => "Prelude.Either" [ "Prelude.Left" "Prelude.Right" ].
  56 Extract Inductive sumbool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
  57 Extract Inductive bool    => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
  58 Extract Inductive unit    => "()" [ "()" ].
  59 Extract Inlined Constant string_dec => "(==)".
  60 Extract Inlined Constant ascii_dec => "(==)".
  61
  62 Extract Inductive ascii => "Char" [ "you_forgot_to_patch_coq" ] "you_forgot_to_patch_coq".
  63 Extract Constant zero   => "'\000'".
  64 Extract Constant one    => "'\001'".
  65 Extract Constant shift  => "shiftAscii".
  66
  67 Unset Extraction Optimize.
  68 Unset Extraction AutoInline.
  69
  70 Variable Name : Type.  Extract Inlined Constant Name => "Name.Name".
  71 Variable mkSystemName : Unique -> string -> nat -> Name.
  72   Extract Inlined Constant mkSystemName =>
  73     "(\u s d -> Name.mkSystemName u (OccName.mkOccName (OccName.varNameDepth (nat2int d)) s))".
  74 Variable mkTyVar : Name -> Kind -> CoreVar.
  75   Extract Inlined Constant mkTyVar => "(\n k -> Var.mkTyVar n (kindToCoreKind k))".
  76 Variable mkCoVar : Name -> CoreType -> CoreType -> CoreVar.
  77   Extract Inlined Constant mkCoVar => "(\n t1 t2 -> Var.mkCoVar n (Coercion.mkCoKind t1 t2))".
  78 Variable mkExVar : Name -> CoreType -> CoreVar.
  79   Extract Inlined Constant mkExVar => "Id.mkLocalId".
  80
  81 Section core2proof.
  82   Context (ce:@CoreExpr CoreVar).
  83
  84   Definition Γ : TypeEnv := nil.
  85
  86   Definition Δ : CoercionEnv Γ := nil.
  87
  88   Definition φ : TyVarResolver Γ :=
  89     fun cv => Error ("unbound tyvar: " +++ toString (cv:CoreVar)).
  90     (*fun tv => error ("tried to get the representative of an unbound tyvar:" +++ (getCoreVarOccString tv)).*)
  91
  92   Definition ψ : CoVarResolver Γ Δ :=
  93     fun cv => Error ("tried to get the representative of an unbound covar!" (*+++ (getTypeVarOccString cv)*)).
  94
  95   (* We need to be able to resolve unbound exprvars, but we can be sure their types will have no
  96    * free tyvars in them *)
  97   Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ :=
  98     match coreVarToWeakVar cv with
  99       | WExprVar wev => match weakTypeToTypeOfKind φ wev ★ with
 100                           | Error s => Prelude_error ("Error converting weakType of top-level variable "+++
 101                                                          toString cv+++": " +++ s)
 102                           | OK    t => t @@ nil
 103                         end
 104       | WTypeVar _   => Prelude_error "top-level xi got a type variable"
 105       | WCoerVar _   => Prelude_error "top-level xi got a coercion variable"
 106     end.
 107
 108
 109   Definition header : string :=
 110     "\documentclass{article}"+++eol+++
 111     "\usepackage{amsmath}"+++eol+++
 112     "\usepackage{amssymb}"+++eol+++
 113     "\usepackage{proof}"+++eol+++
 114 (*    "\usepackage{mathpartir}   % http://cristal.inria.fr/~remy/latex/"+++eol+++*)
 115     "\usepackage{trfrac}       % http://www.utdallas.edu/~hamlen/trfrac.sty"+++eol+++
 116     "\def\code#1#2{\Box_{#1} #2}"+++eol+++
 117     "\usepackage[paperwidth=\maxdimen,paperheight=\maxdimen]{geometry}"+++eol+++
 118     "\usepackage[tightpage,active]{preview}"+++eol+++
 119     "\begin{document}"+++eol+++
 120     "\setlength\PreviewBorder{5pt}"+++eol.
 121
 122   Definition footer : string :=
 123     eol+++"\end{document}"+++
 124     eol.
 125
 126   (* core-to-string (-dcoqpass) *)
 127   Definition coreToStringExpr' (ce:@CoreExpr CoreVar) : ???string :=
 128     addErrorMessage ("input CoreSyn: " +++ toString ce)
 129     (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
 130       coreExprToWeakExpr ce >>= fun we =>
 131         addErrorMessage ("WeakExpr: " +++ toString we)
 132           ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
 133             ((weakTypeOfWeakExpr we) >>= fun t =>
 134               (addErrorMessage ("WeakType: " +++ toString t)
 135                 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
 136                   addErrorMessage ("HaskType: " +++ toString τ)
 137                   ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => false) τ nil we) >>= fun e =>
 138                     OK (eol+++eol+++eol+++
 139                         "\begin{preview}"+++eol+++
 140                         "$\displaystyle "+++
 141                         toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ e))+++
 142                         " $"+++eol+++
 143                         "\end{preview}"+++eol+++eol+++eol)
 144                   )))))))).
 145
 146   Definition coreToStringExpr (ce:@CoreExpr CoreVar) : string :=
 147     match coreToStringExpr' ce with
 148       | OK x => x
 149       | Error s => Prelude_error s
 150     end.
 151
 152   Definition coreToStringBind (binds:@CoreBind CoreVar) : string :=
 153     match binds with
 154       | CoreNonRec _ e => coreToStringExpr e
 155       | CoreRec    lbe => fold_left (fun x y => x+++eol+++eol+++y) (map (fun x => coreToStringExpr (snd x)) lbe) ""
 156     end.
 157
 158   Definition coqPassCoreToString (lbinds:list (@CoreBind CoreVar)) : string :=
 159     header +++
 160     (fold_left (fun x y => x+++eol+++eol+++y) (map coreToStringBind lbinds) "")
 161     +++ footer.
 162
 163
 164   (* core-to-core (-fcoqpass) *)
 165   Section CoreToCore.
 166
 167     Definition mkWeakTypeVar (u:Unique)(k:Kind)                 : WeakTypeVar :=
 168       weakTypeVar (mkTyVar (mkSystemName u "tv" O) k) k.
 169     Definition mkWeakCoerVar (u:Unique)(k:Kind)(t1 t2:WeakType) : WeakCoerVar :=
 170       weakCoerVar (mkCoVar (mkSystemName u "cv" O) (weakTypeToCoreType t1) (weakTypeToCoreType t2)) k t1 t2.
 171     Definition mkWeakExprVar (u:Unique)(t:WeakType)             : WeakExprVar :=
 172       weakExprVar (mkExVar (mkSystemName u "ev" O) (weakTypeToCoreType t)) t.
 173
 174     Context (hetmet_brak  : WeakExprVar).
 175     Context (hetmet_esc   : WeakExprVar).
 176     Context (uniqueSupply : UniqSupply).
 177
 178     Definition useUniqueSupply {T}(ut:UniqM T) : ???T :=
 179       match ut with
 180         uniqM f =>
 181          f uniqueSupply >>= fun x => OK (snd x)
 182       end.
 183
 184     Definition larger : forall ln:list nat, { n:nat & forall n', In n' ln -> gt n n' }.
 185       intros.
 186       induction ln.
 187       exists O.
 188       intros.
 189       inversion H.
 190       destruct IHln as [n pf].
 191       exists (plus (S n) a).
 192       intros.
 193       destruct H.
 194       omega.
 195       fold (@In _ n' ln) in H.
 196       set (pf n' H) as q.
 197       omega.
 198       Defined.
 199
 200   Definition FreshNat : @FreshMonad nat.
 201     refine {| FMT       := fun T => nat -> prod nat T
 202             ; FMT_fresh := _
 203            |}.
 204     Focus 2.
 205     intros.
 206     refine ((S H),_).
 207     set (larger tl) as q.
 208     destruct q as [n' pf].
 209     exists n'.
 210     intros.
 211     set (pf _ H0) as qq.
 212     omega.
 213
 214     refine {| returnM := fun a (v:a) => _ |}.
 215       intro n. exact (n,v).
 216       intros.
 217       set (X H) as q.
 218       destruct q as [n' v].
 219       set (X0 v n') as q'.
 220       exact q'.
 221       Defined.
 222
 223     Definition unFresh {T} : @FreshM _ FreshNat T -> T.
 224       intros.
 225       destruct X.
 226       exact O.
 227       apply t.
 228       Defined.
 229
 230     Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
 231       addErrorMessage ("input CoreSyn: " +++ toString ce)
 232       (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
 233         coreExprToWeakExpr ce >>= fun we =>
 234           addErrorMessage ("WeakExpr: " +++ toString we)
 235             ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
 236               ((weakTypeOfWeakExpr we) >>= fun t =>
 237                 (addErrorMessage ("WeakType: " +++ toString t)
 238                   ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
 239
 240                     ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
 241
 242                       (addErrorMessage ("HaskStrong...")
 243                         (let haskProof := @expr2proof _ _ _ _ _ _ e
 244                          in (* insert HaskProof-to-HaskProof manipulations here *)
 245                          OK ((@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
 246                          >>= fun e' =>
 247                            (snd e') >>= fun e'' =>
 248                          strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
 249                            (projT2 e'') INil
 250                          >>= fun q =>
 251                            OK (weakExprToCoreExpr q)
 252                     )))))))))).
 253
 254     Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) :=
 255       match coreToCoreExpr' ce with
 256         | OK x    => x
 257         | Error s => Prelude_error s
 258       end.
 259
 260     Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar :=
 261       match binds with
 262         | CoreNonRec v e => CoreNonRec v (coreToCoreExpr e)
 263         | CoreRec    lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
 264       end.
 265
 266     Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
 267       map coreToCoreBind lbinds.
 268
 269   End CoreToCore.
 270
 271   Definition coqPassCoreToCore
 272     (hetmet_brak  : CoreVar)
 273     (hetmet_esc   : CoreVar)
 274     (uniqueSupply : UniqSupply)
 275     (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
 276     match coreVarToWeakVar hetmet_brak with
 277       | WExprVar hetmet_brak' => match coreVarToWeakVar hetmet_esc with
 278                                    | WExprVar hetmet_esc' => coqPassCoreToCore' hetmet_brak' hetmet_esc' uniqueSupply lbinds
 279                                    | _ => Prelude_error "IMPOSSIBLE"
 280                                  end
 281       | _ => Prelude_error "IMPOSSIBLE"
 282     end.
 283
 284 End core2proof.