src/Extraction.v

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