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 HaskKinds.
  10 Require Import HaskLiterals.
  11 Require Import HaskTyCons.
  12 Require Import HaskCoreTypes.
  13 Require Import HaskCoreVars.
  14
  15 (* this type must extract to EXACTLY match TypeRep.Type *)
  16 Inductive CoreExpr {b:Type} :=
  17 | CoreEVar   : CoreVar                          -> CoreExpr
  18 | CoreELit   : HaskLiteral                      -> CoreExpr
  19 | CoreEApp   : CoreExpr        ->  CoreExpr     -> CoreExpr
  20 | CoreELam   : b               ->  CoreExpr     -> CoreExpr
  21 | CoreELet   : CoreBind        ->  CoreExpr     -> CoreExpr
  22 | CoreECase  : CoreExpr   -> b ->  CoreType     -> list (@triple CoreAltCon (list b) CoreExpr) -> CoreExpr
  23 | CoreECast  : CoreExpr        ->  CoreCoercion -> CoreExpr
  24 | CoreENote  : Note            ->  CoreExpr     -> CoreExpr
  25 | CoreEType  : CoreType                         -> CoreExpr
  26 | CoreECoercion : CoreCoercion                  -> CoreExpr
  27 with      CoreBind {b:Type} :=
  28 | CoreNonRec : b -> CoreExpr         -> CoreBind
  29 | CoreRec    : list (b * CoreExpr  ) -> CoreBind.
  30 Extract Inductive CoreExpr =>
  31    "CoreSyn.Expr" [
  32       "CoreSyn.Var"
  33       "CoreSyn.Lit"
  34       "CoreSyn.App"
  35       "CoreSyn.Lam"
  36       "CoreSyn.Let"
  37       "CoreSyn.Case"
  38       "CoreSyn.Cast"
  39       "CoreSyn.Note"
  40       "CoreSyn.Type"
  41       "CoreSyn.Coercion"
  42    ].
  43 Extract Inductive CoreBind =>
  44   "CoreSyn.Bind" [ "CoreSyn.NonRec" "CoreSyn.Rec" ].
  45
  46 Variable coreExprToString : @CoreExpr CoreVar -> string.  Extract Inlined Constant coreExprToString => "outputableToString".
  47 Instance CoreExprToString : ToString (@CoreExpr CoreVar) := { toString := coreExprToString }.
  48
  49 Variable coreTypeOfCoreExpr    : @CoreExpr CoreVar -> CoreType.
  50   Extract Inlined Constant coreTypeOfCoreExpr => "CoreUtils.exprType".