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         rewrite <- H.
 234         unfold HaskType; intros.
 235         apply TCon.
 236         Defined.
 237
 238     Definition idproof1 : ND Rule [] [nil > nil > [TInt @@ nil] |- [TInt @@ nil]].
 239       apply nd_rule.
 240       apply RVar.
 241       Defined.
 242
 243     Definition idtype :=
 244         HaskTAll(Γ:=nil) ★ (fun TV ite tv => (TApp (TApp TArrow (TVar tv)) (TVar tv))).
 245
 246     Definition idproof : ND Rule [] [nil > nil > [] |- [idtype @@ nil]].
 247       eapply nd_comp; [ idtac | eapply nd_rule ; eapply RAbsT ].
 248       apply idproof0.
 249       Defined.
 250 *)
 251 (*
 252     Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
 253     addErrorMessage ("input CoreSyn: " +++ ce)
 254     (addErrorMessage ("input CoreType: " +++ coreTypeOfCoreExpr ce) (
 255       coreExprToWeakExpr ce >>= fun we =>
 256         addErrorMessage ("WeakExpr: " +++ we)
 257           ((addErrorMessage ("CoreType of WeakExpr: " +++ coreTypeOfCoreExpr (weakExprToCoreExpr we))
 258             ((weakTypeOfWeakExpr we) >>= fun t =>
 259               (addErrorMessage ("WeakType: " +++ t)
 260                 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
 261                   addErrorMessage ("HaskType: " +++ τ)
 262                   ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
 263                         (let haskProof := @expr2proof _ _ _ _ _ _ e
 264                           in (* insert HaskProof-to-HaskProof manipulations here *)
 265                    (unFresh (@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof))
 266                   >>= fun e' => Error (@toString _ (ExprToString _ _ _ _) (projT2 e'))
 267 (*
 268                   >>= fun e' =>
 269                     Prelude_error (@toString _ (@ExprToString nat _ _ _ _ _ _) (projT2 e'))
 270   *)
 271 )
 272 )))))))).
 273 (*                    Error "X").*)
 274 (*
 275                    strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
 276                    (projT2 e')
 277                          INil
 278                          >>= fun q => Error (toString q)
 279                   ))))))))).
 280 *)
 281 *)
 282
 283     Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
 284       addErrorMessage ("input CoreSyn: " +++ ce)
 285       (addErrorMessage ("input CoreType: " +++ coreTypeOfCoreExpr ce) (
 286         coreExprToWeakExpr ce >>= fun we =>
 287           addErrorMessage ("WeakExpr: " +++ we)
 288             ((addErrorMessage ("CoreType of WeakExpr: " +++ coreTypeOfCoreExpr (weakExprToCoreExpr we))
 289               ((weakTypeOfWeakExpr we) >>= fun t =>
 290                 (addErrorMessage ("WeakType: " +++ t)
 291                   ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
 292
 293                     ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
 294
 295                       (addErrorMessage ("HaskStrong...")
 296                         (let haskProof := @expr2proof _ _ _ _ _ _ e
 297                          in (* insert HaskProof-to-HaskProof manipulations here *)
 298                          OK ((@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
 299                          >>= fun e' =>
 300                            (snd e') >>= fun e'' =>
 301                          strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
 302                            (projT2 e'') INil
 303                          >>= fun q =>
 304                            OK (weakExprToCoreExpr q)
 305                     )))))))))).
 306
 307     Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) :=
 308       match coreToCoreExpr' ce with
 309         | OK x    => x
 310         | Error s => Prelude_error s
 311       end.
 312
 313     Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar :=
 314       match binds with
 315         | CoreNonRec v e => CoreNonRec v (coreToCoreExpr e)
 316         | CoreRec    lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
 317       end.
 318
 319     Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
 320       map coreToCoreBind lbinds.
 321
 322   End CoreToCore.
 323
 324   Definition coqPassCoreToCore
 325     (hetmet_brak  : CoreVar)
 326     (hetmet_esc   : CoreVar)
 327     (uniqueSupply : UniqSupply)
 328     (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
 329     match coreVarToWeakVar hetmet_brak with
 330       | WExprVar hetmet_brak' => match coreVarToWeakVar hetmet_esc with
 331                                    | WExprVar hetmet_esc' => coqPassCoreToCore' hetmet_brak' hetmet_esc' uniqueSupply lbinds
 332                                    | _ => Prelude_error "IMPOSSIBLE"
 333                                  end
 334       | _ => Prelude_error "IMPOSSIBLE"
 335     end.
 336
 337 End core2proof.
 338 (*Set Extraction Optimize.*)
 339 (*Set Extraction AutoInline.*)
 340 Extraction "Extraction.hs" coqPassCoreToString coqPassCoreToCore.
 341