src/HaskCore.v

   1 (*********************************************************************************************************************************)
   2 (* HaskCore: basically GHC's CoreSyn.Expr imported into Coqland                                                                  *)
   3 (*********************************************************************************************************************************)
   4
   5 Generalizable All Variables.
   6 Require Import Preamble.
   7 Require Import General.
   8 Require Import Coq.Strings.String.
   9 Require Import HaskGeneral.
  10 Require Import HaskLiterals.
  11 Require Import HaskCoreTypes.
  12 Require Import HaskCoreVars.
  13
  14 (* this type must extract to EXACTLY match TypeRep.Type *)
  15 Inductive CoreExpr (b:Type) :=
  16 | CoreEVar   : CoreVar                          -> CoreExpr b
  17 | CoreELit   : HaskLiteral                      -> CoreExpr b
  18 | CoreEApp   : CoreExpr b      ->  CoreExpr b   -> CoreExpr b
  19 | CoreELam   :          b      ->  CoreExpr b   -> CoreExpr b
  20 | CoreELet   : CoreBind b      ->  CoreExpr b   -> CoreExpr b
  21 | CoreECase  : CoreExpr b -> b ->  CoreType     -> list (@triple AltCon (list b) (CoreExpr b)) -> CoreExpr b
  22 | CoreECast  : CoreExpr b      ->  CoreCoercion -> CoreExpr b
  23 | CoreENote  : Note            ->  CoreExpr b   -> CoreExpr b
  24 | CoreEType  : CoreType                         -> CoreExpr b
  25 with      CoreBind (b:Type) :=
  26 | CoreNonRec : b -> CoreExpr b       -> CoreBind b
  27 | CoreRec    : list (b * CoreExpr b) -> CoreBind b.
  28 Extract Inductive CoreExpr =>
  29    "CoreSyn.Expr" [
  30       "CoreSyn.Var"
  31       "CoreSyn.Lit"
  32       "CoreSyn.App"
  33       "CoreSyn.Lam"
  34       "CoreSyn.Let"
  35       "CoreSyn.Case"
  36       "CoreSyn.Cast"
  37       "CoreSyn.Note"
  38       "CoreSyn.Type" ].
  39 Extract Inductive CoreBind =>
  40   "CoreSyn.Bind" [ "CoreSyn.NonRec" "CoreSyn.Rec" ].
  41
  42 (* extracts the Name from a CoreVar *)
  43 Variable coreVarCoreName    : CoreVar -> CoreName.   Extract Inlined Constant coreVarCoreName  => "Var.varName".
  44
  45 Extract Constant ArrowTyCon           => "Type.funTyCon".     (* Figure 7, (->) *)
  46 Extract Constant CoFunConst           => "TyCon.TyCon".                        Extraction Implicit CoFunConst [ 1 ].
  47 Extract Constant TyFunConst           => "TyCon.TyCon".                        Extraction Implicit TyFunConst [ 1 ].
  48
  49 (*Extract Inlined Constant getDataCons => "TyCon.tyConDataCons".*)
  50 Variable mkTyConApp : forall n, TyCon n -> list CoreType -> CoreType.
  51   Extract Inlined Constant mkTyConApp => "Type.mkTyConApp".
  52
  53 (* the magic wired-in name for the modal type introduction form *)
  54 Variable hetmet_brak_name   : CoreName.              Extract Inlined Constant hetmet_brak_name => "PrelNames.hetmet_brak_name".
  55
  56 (* the magic wired-in name for the modal type elimination form *)
  57 Variable hetmet_esc_name    : CoreName.              Extract Inlined Constant hetmet_esc_name  => "PrelNames.hetmet_esc_name".
  58
  59