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 Coq.Lists.List.
  10 Require Import HaskKinds.
  11 Require Import HaskCoreVars.
  12
  13 Variable TyCon               : Type.                      Extract Inlined Constant TyCon                 => "TyCon.TyCon".
  14 Variable CoreDataCon         : Type.                      Extract Inlined Constant CoreDataCon           => "DataCon.DataCon".
  15 Variable CoreName            : Type.                      Extract Inlined Constant CoreName              => "Name.Name".
  16 Variable CoreCoercion        : Type.                      Extract Inlined Constant CoreCoercion          => "Coercion.Coercion".
  17 Variable CoreCoFunConst      : Type.                      Extract Inlined Constant TyCon                 => "TyCon.TyCon".
  18 Variable CoreTyFunConst      : Type.                      Extract Inlined Constant TyCon                 => "TyCon.TyCon".
  19 Variable Class_              : Type.                      Extract Inlined Constant Class_                => "Class.Class".
  20 Variable classTyCon          : Class_ -> TyCon.           Extract Inlined Constant classTyCon            => "Class.classTyCon".
  21 Variable tyConToString       : TyCon      -> string.      Extract Inlined Constant tyConToString         => "outputableToString".
  22 Variable dataConToString     : CoreDataCon-> string.      Extract Inlined Constant dataConToString       => "outputableToString".
  23 Variable tyFunToString       : CoreTyFunConst -> string.  Extract Inlined Constant tyFunToString         => "outputableToString".
  24 Variable coFunToString       : CoreCoFunConst -> string.  Extract Inlined Constant coFunToString         => "outputableToString".
  25 Variable natTostring         : nat->string.               Extract Inlined Constant natTostring           => "natTostring".
  26 Variable CoreIPName          : Type -> Type.
  27    Extract Constant CoreIPName "’a"        => "BasicTypes.IPName".
  28    Extraction Inline CoreIPName.
  29
  30 (* this exracts onto TypeRep.Type, on the nose *)
  31 Inductive CoreType :=
  32 | TyVarTy  : CoreVar                    -> CoreType
  33 | AppTy    : CoreType  ->      CoreType -> CoreType   (* first arg must be AppTy or TyVarTy*)
  34 | TyConApp : TyCon -> list CoreType -> CoreType
  35 | FunTy    : CoreType  ->      CoreType -> CoreType   (* technically redundant since we have FunTyCon *)
  36 | ForAllTy : CoreVar   ->      CoreType -> CoreType
  37 | PredTy   : PredType                   -> CoreType
  38 with PredType :=
  39 | ClassP   : Class_              -> list CoreType -> PredType
  40 | IParam   : CoreIPName CoreName -> CoreType      -> PredType
  41 | EqPred   : CoreType            -> CoreType      -> PredType.
  42 Extract Inductive CoreType =>
  43    "TypeRep.Type" [ "TypeRep.TyVarTy" "TypeRep.AppTy" "TypeRep.TyConApp" "TypeRep.FunTy" "TypeRep.ForAllTy" "TypeRep.PredTy" ].
  44 Extract Inductive PredType =>
  45    "TypeRep.PredType" [ "TypeRep.ClassP" "TypeRep.IParam" "TypeRep.EqPred" ].
  46
  47 (* GHC provides decision procedures for equality on its primitive types; we tell Coq to blindly trust them *)
  48 Variable tyCon_eq            : EqDecider TyCon.           Extract Inlined Constant tyCon_eq              => "(==)".
  49 Variable dataCon_eq          : EqDecider CoreDataCon.     Extract Inlined Constant dataCon_eq            => "(==)".
  50 Variable coreName_eq         : EqDecider CoreName.        Extract Inlined Constant coreName_eq           => "(==)".
  51 Variable coretype_eq_dec     : EqDecider CoreType.        Extract Inlined Constant coretype_eq_dec       => "checkTypeEquality".
  52 Instance CoreTypeEqDecidable : EqDecidable CoreType    := { eqd_dec := coretype_eq_dec }.
  53 Instance TyConEqDecidable    : EqDecidable TyCon       := { eqd_dec := tyCon_eq }.
  54 Instance DataConEqDecidable  : EqDecidable CoreDataCon := { eqd_dec := dataCon_eq }.
  55 Instance CoreNameEqDecidable : EqDecidable CoreName    := { eqd_dec := coreName_eq }.
  56
  57 (*
  58 Variable coreTypeToString      : CoreType     -> string.    Extract Inlined Constant coreTypeToString       => "outputableToString".
  59 *)
  60 Variable coreTypeToString      : CoreType     -> string.
  61     Extract Inlined Constant coreTypeToString       => "showType".
  62
  63 Variable coreNameToString      : CoreName     -> string.    Extract Inlined Constant coreNameToString       => "outputableToString".
  64 Variable coreCoercionToString  : CoreCoercion -> string.    Extract Inlined Constant coreCoercionToString   => "outputableToString".
  65 Variable coreCoercionKind : CoreCoercion -> CoreType*CoreType. Extract Inlined Constant coreCoercionKind => "Coercion.coercionKind".
  66 Variable kindOfCoreType    : CoreType -> Kind.    Extract Inlined Constant kindOfCoreType => "(coreKindToKind . Coercion.typeKind)".
  67