src/HaskCoreTypes.v

   1 (*********************************************************************************************************************************)
   2 (* HaskCoreTypes: basically GHC's TypeRep.Type 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 HaskCoreVars.
  12
  13 Variable CoreName           : Type.                                               Extract Inlined Constant CoreName => "Name.Name".
  14 Variable coreName_eq        : forall (a b:CoreName),   sumbool (a=b) (not (a=b)). Extract Inlined Constant coreName_eq => "(==)".
  15 Axiom    coreName_eq_refl   : ∀ v, (coreName_eq v v)=(left _ (refl_equal v)).
  16 Instance CoreNameEqDecidable : EqDecidable CoreName :=
  17 { eqd_dec            := coreName_eq
  18 ; eqd_dec_reflexive  := coreName_eq_refl
  19 }.
  20
  21 Inductive CoreIPName        : Type -> Type := .                               Extract Inductive CoreIPName => "CoreSyn.IPName" [ ].
  22
  23 (* this exracts onto TypeRep.Type, on the nose *)
  24 Inductive CoreType :=
  25 | TyVarTy  :             CoreVar                   -> CoreType
  26 | AppTy    :             CoreType ->      CoreType -> CoreType   (* first arg must be AppTy or TyVarTy*)
  27 | TyConApp : forall {n}, TyCon n  -> list CoreType -> CoreType
  28 | FunTy    :             CoreType ->      CoreType -> CoreType   (* technically redundant since we have FunTyCon *)
  29 | ForAllTy :             CoreVar  ->      CoreType -> CoreType
  30 | PredTy   :             PredType                  -> CoreType
  31 with PredType :=
  32 | ClassP   : forall {n}, Class_ n            -> list CoreType -> PredType
  33 | IParam   :             CoreIPName CoreName -> CoreType      -> PredType
  34 | EqPred   :             CoreType            -> CoreType      -> PredType.
  35 Extract Inductive CoreType =>
  36    "TypeRep.Type" [ "TypeRep.TyVarTy" "TypeRep.AppTy" "TypeRep.TyConApp" "TypeRep.FunTy" "TypeRep.ForAllTy" "TypeRep.PredTy" ].
  37 Extract Inductive PredType =>
  38    "TypeRep.PredType" [ "TypeRep.ClassP" "TypeRep.IParam" "TypeRep.EqPred" ].
  39
  40 Variable kindOfCoreType : CoreType -> Kind.        Extract Inlined Constant kindOfCoreType => "(coreKindToKind . Coercion.typeKind)".
  41
  42 Definition haskLiteralToCoreType lit : CoreType :=
  43   TyConApp (haskLiteralToTyCon lit) nil.
  44
  45 Inductive CoreVarSort : Type :=
  46 | CoreExprVar : CoreType            -> CoreVarSort
  47 | CoreTypeVar : Kind                -> CoreVarSort
  48 | CoreCoerVar : CoreType * CoreType -> CoreVarSort.
  49
  50 Variable coreVarSort           : CoreVar  -> CoreVarSort.   Extract Inlined Constant coreVarSort    => "coreVarSort".
  51
  52 Variable coreTypeToString      : CoreType     -> string.    Extract Inlined Constant coreTypeToString       => "outputableToString".
  53 Variable coreNameToString      : CoreName     -> string.    Extract Inlined Constant coreNameToString       => "outputableToString".
  54
  55 Variable CoreCoercion          : Type.                      Extract Inlined Constant CoreCoercion           => "Coercion.Coercion".
  56 Variable coreCoercionToString  : CoreCoercion -> string.    Extract Inlined Constant coreCoercionToString   => "outputableToString".
  57 Variable coreCoercionKind      : CoreCoercion -> CoreType*CoreType.
  58  Extract Inlined Constant coreCoercionKind => "Coercion.coercionKind".