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 Variable coretype_eq_dec : forall (c1 c2:CoreType), sumbool (eq c1 c2) (not (eq c1 c2)).
  46   Extract Inlined Constant coretype_eq_dec => "Type.coreEqType".
  47
  48 Extract Constant ArrowTyCon           => "Type.funTyCon".     (* Figure 7, (->) *)
  49 Extract Constant CoFunConst           => "TyCon.TyCon".                        Extraction Implicit CoFunConst [ 1 ].
  50 Extract Constant TyFunConst           => "TyCon.TyCon".                        Extraction Implicit TyFunConst [ 1 ].
  51
  52 (*Extract Inlined Constant getDataCons => "TyCon.tyConDataCons".*)
  53 Variable mkTyConApp : forall n, TyCon n -> list CoreType -> CoreType.
  54   Extract Inlined Constant mkTyConApp => "Type.mkTyConApp".
  55
  56 (* the magic wired-in name for the modal type introduction form *)
  57 Variable hetmet_brak_name   : CoreName.              Extract Inlined Constant hetmet_brak_name => "PrelNames.hetmet_brak_name".
  58
  59 (* the magic wired-in name for the modal type elimination form *)
  60 Variable hetmet_esc_name    : CoreName.              Extract Inlined Constant hetmet_esc_name  => "PrelNames.hetmet_esc_name".
  61
  62 (* detects our crude Core-encoding of modal type introduction/elimination forms *)
  63 Definition isBrak (ce:CoreExpr CoreVar) : ??CoreVar :=
  64 match ce with
  65   | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
  66     => if coreName_eq hetmet_brak_name (coreVarCoreName v) then Some ec else None
  67   | _ => None
  68 end.
  69 Definition isEsc (ce:CoreExpr CoreVar) : ??CoreVar :=
  70 match ce with
  71   | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
  72     => if coreName_eq hetmet_esc_name (coreVarCoreName v) then Some ec else None
  73   | _ => None
  74 end.
  75
  76