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 Require Import HaskLiterals.
  13 Require Import HaskTyCons.
  14
  15 Variable CoreCoercionCoAxiom : Type.  Extract Inlined Constant CoreCoercionCoAxiom => "Coercion.CoAxiom".
  16 Variable Int : Type.                  Extract Inlined Constant Int => "Prelude.Int".
  17
  18 Variable classTyCon          : Class_ -> CoreTyCon.       Extract Inlined Constant classTyCon            => "Class.classTyCon".
  19 Variable coreTyConToString   : CoreTyCon   -> string.     Extract Inlined Constant coreTyConToString     => "outputableToString".
  20 Variable coreDataConToString : CoreDataCon -> string.     Extract Inlined Constant coreDataConToString   => "outputableToString".
  21
  22 (* this exracts onto TypeRep.Type, on the nose *)
  23 Inductive CoreType :=
  24 | TyVarTy  : CoreVar                    -> CoreType
  25 | AppTy    : CoreType  ->      CoreType -> CoreType   (* first arg must be AppTy or TyVarTy*)
  26 | TyConApp : CoreTyCon -> list CoreType -> CoreType
  27 | FunTy    : CoreType  ->      CoreType -> CoreType   (* technically redundant since we have FunTyCon *)
  28 | ForAllTy : CoreVar   ->      CoreType -> CoreType
  29 | PredTy   : PredType                   -> CoreType
  30 with PredType :=
  31 | ClassP   : Class_              -> list CoreType -> PredType
  32 | IParam   : CoreIPName CoreName -> CoreType      -> PredType
  33 | EqPred   : CoreType            -> CoreType      -> PredType.
  34 Extract Inductive CoreType =>
  35    "TypeRep.Type" [ "TypeRep.TyVarTy" "TypeRep.AppTy" "TypeRep.TyConApp" "TypeRep.FunTy" "TypeRep.ForAllTy" "TypeRep.PredTy" ].
  36 Extract Inductive PredType =>
  37    "TypeRep.PredType" [ "TypeRep.ClassP" "TypeRep.IParam" "TypeRep.EqPred" ].
  38
  39 Inductive CoreCoercion : Type :=
  40     CoreCoercionRefl        : CoreType                                 -> CoreCoercion
  41   | CoreCoercionTyConAppCo  : CoreTyCon    -> list CoreCoercion        -> CoreCoercion
  42   | CoreCoercionAppCo       : CoreCoercion -> CoreCoercion             -> CoreCoercion
  43   | CoreCoercionForAllCo    : CoreVar      -> CoreCoercion             -> CoreCoercion
  44   | CoreCoercionCoVarCo     : CoreVar                                  -> CoreCoercion
  45   | CoreCoercionAxiomInstCo : CoreCoercionCoAxiom -> list CoreCoercion -> CoreCoercion
  46   | CoreCoercionUnsafeCo    : CoreType -> CoreType                     -> CoreCoercion
  47   | CoreCoercionSymCo       : CoreCoercion                             -> CoreCoercion
  48   | CoreCoercionTransCo     : CoreCoercion -> CoreCoercion             -> CoreCoercion
  49   | CoreCoercionNthCo       : Int -> CoreCoercion                      -> CoreCoercion
  50   | CoreCoercionInstCo      : CoreCoercion -> CoreType                 -> CoreCoercion.
  51
  52 Extract Inductive CoreCoercion =>
  53   "Coercion.Coercion" [
  54   "Coercion.Refl"
  55   "Coercion.TyConAppCo"
  56   "Coercion.AppCo"
  57   "Coercion.ForAllCo"
  58   "Coercion.CoVarCo"
  59   "Coercion.AxiomInstCo"
  60   "Coercion.UnsafeCo"
  61   "Coercion.SymCo"
  62   "Coercion.TransCo"
  63   "Coercion.NthCo"
  64   "Coercion.InstCo" ].
  65
  66 Variable coreNameToString      : CoreName     -> string.    Extract Inlined Constant coreNameToString       => "outputableToString".
  67 Variable coreCoercionToString  : CoreCoercion -> string.    Extract Inlined Constant coreCoercionToString   => "outputableToString".
  68 Variable coreCoercionKind : Kind -> CoreType*CoreType.
  69   Extract Inlined Constant coreCoercionKind => "(Coercion.coercionKind . kindToCoreKind)".
  70 Variable kindOfCoreType   : CoreType -> Kind.   Extract Inlined Constant kindOfCoreType   => "(coreKindToKind . Kind.typeKind)".
  71 Variable coreTypeToString : CoreType -> string. Extract Inlined Constant coreTypeToString => "(outputableToString . coreViewDeep)".
  72 Variable setVarType       : CoreVar -> CoreType -> CoreVar. Extract Inlined Constant setVarType       => "Var.setVarType".
  73
  74 (* GHC provides decision procedures for equality on its primitive types; we tell Coq to blindly trust them *)
  75 Variable coreTyCon_eq         : EqDecider CoreTyCon.       Extract Inlined Constant coreTyCon_eq          => "(==)".
  76 Variable tyCon_eq             : EqDecider TyCon.           Extract Inlined Constant tyCon_eq              => "(==)".
  77 Variable tyFun_eq             : EqDecider TyFun.           Extract Inlined Constant tyFun_eq              => "(==)".
  78 Variable dataCon_eq           : EqDecider CoreDataCon.     Extract Inlined Constant dataCon_eq            => "(==)".
  79 Variable coreName_eq          : EqDecider CoreName.        Extract Inlined Constant coreName_eq           => "(==)".
  80 Instance CoreTyConEqDecidable : EqDecidable CoreTyCon   := { eqd_dec := coreTyCon_eq }.
  81 Instance TyConEqDecidable     : EqDecidable TyCon       := { eqd_dec := tyCon_eq }.
  82 Instance TyFunEqDecidable     : EqDecidable TyFun       := { eqd_dec := tyFun_eq }.
  83 Instance DataConEqDecidable   : EqDecidable CoreDataCon := { eqd_dec := dataCon_eq }.
  84 Instance CoreNameEqDecidable  : EqDecidable CoreName    := { eqd_dec := coreName_eq }.
  85 Instance CoreTypeToString     : ToString CoreType       := { toString := coreTypeToString }.
  86 Instance CoreNameToString     : ToString CoreName       := { toString := coreNameToString }.
  87 Instance CoreCoercionToString : ToString CoreCoercion   := { toString := coreCoercionToString }.
  88 Instance CoreDataConToString  : ToString CoreDataCon    := { toString := coreDataConToString }.
  89 Instance CoreTyConToString    : ToString CoreTyCon      := { toString := coreTyConToString }.
  90