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{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=\maxdimen,paperheight=\maxdimen]{geometry}"+++eol+++
 119     "\usepackage[tightpage,active]{preview}"+++eol+++
 120     "\begin{document}"+++eol+++
 121     "\setlength\PreviewBorder{5pt}"+++eol+++.
 122
 123   Definition footer : string :=
 124     eol+++"\end{document}"+++
 125     eol.
 126
 127   (* core-to-string (-dcoqpass) *)
 128   Definition coreToStringExpr' (ce:@CoreExpr CoreVar) : ???string :=
 129     addErrorMessage ("input CoreSyn: " +++ toString ce)
 130     (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
 131       coreExprToWeakExpr ce >>= fun we =>
 132         addErrorMessage ("WeakExpr: " +++ toString we)
 133           ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
 134             ((weakTypeOfWeakExpr we) >>= fun t =>
 135               (addErrorMessage ("WeakType: " +++ toString t)
 136                 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
 137                   addErrorMessage ("HaskType: " +++ toString τ)
 138                   ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => false) τ nil we) >>= fun e =>
 139                     OK (eol+++eol+++eol+++
 140                         "\begin{preview}"+++eol
 141                         "$\displaystyle "+++
 142                         toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ e))+++
 143                         " $"+++eol+++
 144                         "\end{preview}"+++eol+++eol+++eol)
 145                   )))))))).
 146
 147   Definition coreToStringExpr (ce:@CoreExpr CoreVar) : string :=
 148     match coreToStringExpr' ce with
 149       | OK x => x
 150       | Error s => Prelude_error s
 151     end.
 152
 153   Definition coreToStringBind (binds:@CoreBind CoreVar) : string :=
 154     match binds with
 155       | CoreNonRec _ e => coreToStringExpr e
 156       | CoreRec    lbe => fold_left (fun x y => x+++eol+++eol+++y) (map (fun x => coreToStringExpr (snd x)) lbe) ""
 157     end.
 158
 159   Definition coqPassCoreToString (lbinds:list (@CoreBind CoreVar)) : string :=
 160     header +++
 161     (fold_left (fun x y => x+++eol+++eol+++y) (map coreToStringBind lbinds) "")
 162     +++ footer.
 163
 164
 165   (* core-to-core (-fcoqpass) *)
 166   Section CoreToCore.
 167
 168     Definition mkWeakTypeVar (u:Unique)(k:Kind)                 : WeakTypeVar :=
 169       weakTypeVar (mkTyVar (mkSystemName u "tv" O) k) k.
 170     Definition mkWeakCoerVar (u:Unique)(k:Kind)(t1 t2:WeakType) : WeakCoerVar :=
 171       weakCoerVar (mkCoVar (mkSystemName u "cv" O) (weakTypeToCoreType t1) (weakTypeToCoreType t2)) k t1 t2.
 172     Definition mkWeakExprVar (u:Unique)(t:WeakType)             : WeakExprVar :=
 173       weakExprVar (mkExVar (mkSystemName u "ev" O) (weakTypeToCoreType t)) t.
 174
 175     Context (hetmet_brak  : WeakExprVar).
 176     Context (hetmet_esc   : WeakExprVar).
 177     Context (uniqueSupply : UniqSupply).
 178
 179     Definition useUniqueSupply {T}(ut:UniqM T) : ???T :=
 180       match ut with
 181         uniqM f =>
 182          f uniqueSupply >>= fun x => OK (snd x)
 183       end.
 184
 185     Definition larger : forall ln:list nat, { n:nat & forall n', In n' ln -> gt n n' }.
 186       intros.
 187       induction ln.
 188       exists O.
 189       intros.
 190       inversion H.
 191       destruct IHln as [n pf].
 192       exists (plus (S n) a).
 193       intros.
 194       destruct H.
 195       omega.
 196       fold (@In _ n' ln) in H.
 197       set (pf n' H) as q.
 198       omega.
 199       Defined.
 200
 201   Definition FreshNat : @FreshMonad nat.
 202     refine {| FMT       := fun T => nat -> prod nat T
 203             ; FMT_fresh := _
 204            |}.
 205     Focus 2.
 206     intros.
 207     refine ((S H),_).
 208     set (larger tl) as q.
 209     destruct q as [n' pf].
 210     exists n'.
 211     intros.
 212     set (pf _ H0) as qq.
 213     omega.
 214
 215     refine {| returnM := fun a (v:a) => _ |}.
 216       intro n. exact (n,v).
 217       intros.
 218       set (X H) as q.
 219       destruct q as [n' v].
 220       set (X0 v n') as q'.
 221       exact q'.
 222       Defined.
 223
 224     Definition unFresh {T} : @FreshM _ FreshNat T -> T.
 225       intros.
 226       destruct X.
 227       exact O.
 228       apply t.
 229       Defined.
 230
 231     Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
 232       addErrorMessage ("input CoreSyn: " +++ toString ce)
 233       (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
 234         coreExprToWeakExpr ce >>= fun we =>
 235           addErrorMessage ("WeakExpr: " +++ toString we)
 236             ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
 237               ((weakTypeOfWeakExpr we) >>= fun t =>
 238                 (addErrorMessage ("WeakType: " +++ toString t)
 239                   ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
 240
 241                     ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
 242
 243                       (addErrorMessage ("HaskStrong...")
 244                         (let haskProof := @expr2proof _ _ _ _ _ _ e
 245                          in (* insert HaskProof-to-HaskProof manipulations here *)
 246                          OK ((@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
 247                          >>= fun e' =>
 248                            (snd e') >>= fun e'' =>
 249                          strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
 250                            (projT2 e'') INil
 251                          >>= fun q =>
 252                            OK (weakExprToCoreExpr q)
 253                     )))))))))).
 254
 255     Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) :=
 256       match coreToCoreExpr' ce with
 257         | OK x    => x
 258         | Error s => Prelude_error s
 259       end.
 260
 261     Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar :=
 262       match binds with
 263         | CoreNonRec v e => CoreNonRec v (coreToCoreExpr e)
 264         | CoreRec    lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
 265       end.
 266
 267     Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
 268       map coreToCoreBind lbinds.
 269
 270   End CoreToCore.
 271
 272   Definition coqPassCoreToCore
 273     (hetmet_brak  : CoreVar)
 274     (hetmet_esc   : CoreVar)
 275     (uniqueSupply : UniqSupply)
 276     (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
 277     match coreVarToWeakVar hetmet_brak with
 278       | WExprVar hetmet_brak' => match coreVarToWeakVar hetmet_esc with
 279                                    | WExprVar hetmet_esc' => coqPassCoreToCore' hetmet_brak' hetmet_esc' uniqueSupply lbinds
 280                                    | _ => Prelude_error "IMPOSSIBLE"
 281                                  end
 282       | _ => Prelude_error "IMPOSSIBLE"
 283     end.
 284
 285 End core2proof.