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