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