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