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