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