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 ReificationsIsomorphicToGeneralizedArrows.
  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" [ "you_forgot_to_patch_coq" ] "you_forgot_to_patch_coq".
  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 converting weakType of top-level variable "+++
 104                                                          toString cv+++": " +++ s)
 105                           | OK    t => t @@ nil
 106                         end
 107       | WTypeVar _   => Prelude_error "top-level xi got a type variable"
 108       | WCoerVar _   => Prelude_error "top-level xi got a coercion variable"
 109     end.
 110
 111
 112   (* core-to-string (-dcoqpass) *)
 113
 114   Definition header : string :=
 115     "\documentclass[9pt]{article}"+++eol+++
 116     "\usepackage{amsmath}"+++eol+++
 117     "\usepackage{amssymb}"+++eol+++
 118     "\usepackage{proof}"+++eol+++
 119     "\usepackage{mathpartir}   % http://cristal.inria.fr/~remy/latex/"+++eol+++
 120     "\usepackage{trfrac}       % http://www.utdallas.edu/~hamlen/trfrac.sty"+++eol+++
 121     "\def\code#1#2{\Box_{#1} #2}"+++eol+++
 122     "\usepackage[paperwidth=200in,centering]{geometry}"+++eol+++
 123     "\usepackage[displaymath,tightpage,active]{preview}"+++eol+++
 124     "\begin{document}"+++eol+++
 125     "\begin{preview}"+++eol.
 126
 127   Definition footer : string :=
 128     eol+++"\end{preview}"+++
 129     eol+++"\end{document}"+++
 130     eol.
 131
 132
 133   Definition coreToStringExpr' (ce:@CoreExpr CoreVar) : ???string :=
 134     addErrorMessage ("input CoreSyn: " +++ toString ce)
 135     (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
 136       coreExprToWeakExpr ce >>= fun we =>
 137         addErrorMessage ("WeakExpr: " +++ toString we)
 138           ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
 139             ((weakTypeOfWeakExpr we) >>= fun t =>
 140               (addErrorMessage ("WeakType: " +++ toString t)
 141                 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
 142                   addErrorMessage ("HaskType: " +++ toString τ)
 143                   ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => false) τ nil we) >>= fun e =>
 144                     OK (eol+++"$$"+++ toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ e))+++"$$"+++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 env := ★::nil.
 232     Definition freshTV : HaskType env ★ := haskTyVarToType (FreshHaskTyVar _).
 233     Definition idproof0 : ND Rule [] [env > nil > [] |- [freshTV--->freshTV @@ nil]].
 234       eapply nd_comp.
 235       eapply nd_comp.
 236       eapply nd_rule.
 237       apply RVar.
 238       eapply nd_rule.
 239       eapply (RURule _ _ _ _ (RuCanL _ _)) .
 240       eapply nd_rule.
 241       eapply RLam.
 242       Defined.
 243
 244 (*
 245     Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
 246     addErrorMessage ("input CoreSyn: " +++ toString ce)
 247     (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
 248       coreExprToWeakExpr ce >>= fun we =>
 249         addErrorMessage ("WeakExpr: " +++ toString we)
 250           ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
 251             ((weakTypeOfWeakExpr we) >>= fun t =>
 252               (addErrorMessage ("WeakType: " +++ toString t)
 253                 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
 254                   addErrorMessage ("HaskType: " +++ toString τ)
 255                   ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
 256                         (let haskProof := @expr2proof _ _ _ _ _ _ e
 257                           in (* insert HaskProof-to-HaskProof manipulations here *)
 258                    (unFresh (@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof))
 259                   >>= fun e' => Error (@toString _ (ExprToString _ _ _ _) (projT2 e'))
 260 (*
 261                   >>= fun e' =>
 262                     Prelude_error (@toString _ (@ExprToString nat _ _ _ _ _ _) (projT2 e'))
 263   *)
 264 )
 265 )))))))).
 266 (*                    Error "X").*)
 267 (*
 268                    strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
 269                    (projT2 e')
 270                          INil
 271                          >>= fun q => Error (toString q)
 272                   ))))))))).
 273 *)*)
 274
 275
 276     Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
 277       addErrorMessage ("input CoreSyn: " +++ toString ce)
 278       (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
 279         coreExprToWeakExpr ce >>= fun we =>
 280           addErrorMessage ("WeakExpr: " +++ toString we)
 281             ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
 282               ((weakTypeOfWeakExpr we) >>= fun t =>
 283                 (addErrorMessage ("WeakType: " +++ toString t)
 284                   ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
 285
 286                     ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
 287
 288                       (addErrorMessage ("HaskStrong...")
 289                         (let haskProof := @expr2proof _ _ _ _ _ _ e
 290                          in (* insert HaskProof-to-HaskProof manipulations here *)
 291                          OK ((@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
 292                          >>= fun e' =>
 293                            (snd e') >>= fun e'' =>
 294                          strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
 295                            (projT2 e'') INil
 296                          >>= fun q =>
 297                            OK (weakExprToCoreExpr q)
 298                     )))))))))).
 299
 300     Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) :=
 301       match coreToCoreExpr' ce with
 302         | OK x    => x
 303         | Error s => Prelude_error s
 304       end.
 305
 306     Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar :=
 307       match binds with
 308         | CoreNonRec v e => CoreNonRec v (coreToCoreExpr e)
 309         | CoreRec    lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
 310       end.
 311
 312     Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
 313       map coreToCoreBind lbinds.
 314
 315   End CoreToCore.
 316
 317   Definition coqPassCoreToCore
 318     (hetmet_brak  : CoreVar)
 319     (hetmet_esc   : CoreVar)
 320     (uniqueSupply : UniqSupply)
 321     (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
 322     match coreVarToWeakVar hetmet_brak with
 323       | WExprVar hetmet_brak' => match coreVarToWeakVar hetmet_esc with
 324                                    | WExprVar hetmet_esc' => coqPassCoreToCore' hetmet_brak' hetmet_esc' uniqueSupply lbinds
 325                                    | _ => Prelude_error "IMPOSSIBLE"
 326                                  end
 327       | _ => Prelude_error "IMPOSSIBLE"
 328     end.
 329
 330 End core2proof.