src/Extraction.v

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