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