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