Make the HaskStrong type representation Kind-indexed, and many supporting changes...

[coq-hetmet.git] / src / HaskCoreTypes.v

diff --git a/src/HaskCoreTypes.v b/src/HaskCoreTypes.v
index 4a7a056..ea4a02a 100644 (file)
--- a/src/HaskCoreTypes.v
+++ b/src/HaskCoreTypes.v
@@ -10,20 +10,16 @@ Require Import Coq.Lists.List.
 Require Import HaskKinds.
 Require Import HaskCoreVars.
 
-Variable TyCon               : Type.                      Extract Inlined Constant TyCon                 => "TyCon.TyCon".
+Variable CoreTyCon           : Type.                      Extract Inlined Constant CoreTyCon             => "TyCon.TyCon".
 Variable CoreDataCon         : Type.                      Extract Inlined Constant CoreDataCon           => "DataCon.DataCon".
 Variable CoreName            : Type.                      Extract Inlined Constant CoreName              => "Name.Name".
 Variable CoreCoercion        : Type.                      Extract Inlined Constant CoreCoercion          => "Coercion.Coercion".
-Variable CoreCoFunConst      : Type.                      Extract Inlined Constant TyCon                 => "TyCon.TyCon".
-Variable CoreTyFunConst      : Type.                      Extract Inlined Constant TyCon                 => "TyCon.TyCon".
 Variable Class_              : Type.                      Extract Inlined Constant Class_                => "Class.Class".
-Variable classTyCon          : Class_ -> TyCon.           Extract Inlined Constant classTyCon            => "Class.classTyCon".
-Variable tyConToString       : TyCon      -> string.      Extract Inlined Constant tyConToString         => "outputableToString".
+Variable classTyCon          : Class_ -> CoreTyCon.       Extract Inlined Constant classTyCon            => "Class.classTyCon".
+Variable tyConToString       : CoreTyCon      -> string.  Extract Inlined Constant tyConToString         => "outputableToString".
 Variable dataConToString     : CoreDataCon-> string.      Extract Inlined Constant dataConToString       => "outputableToString".
-Variable tyFunToString       : CoreTyFunConst -> string.  Extract Inlined Constant tyFunToString         => "outputableToString".
-Variable coFunToString       : CoreCoFunConst -> string.  Extract Inlined Constant coFunToString         => "outputableToString".
-Variable natTostring         : nat->string.               Extract Inlined Constant natTostring           => "natTostring".
 Variable CoreIPName          : Type -> Type.
+
    Extract Constant CoreIPName "’a"        => "BasicTypes.IPName".
    Extraction Inline CoreIPName.
 
@@ -31,7 +27,7 @@ Variable CoreIPName          : Type -> Type.
 Inductive CoreType :=
 | TyVarTy  : CoreVar                    -> CoreType
 | AppTy    : CoreType  ->      CoreType -> CoreType   (* first arg must be AppTy or TyVarTy*)
-| TyConApp : TyCon -> list CoreType -> CoreType
+| TyConApp : CoreTyCon -> list CoreType -> CoreType
 | FunTy    : CoreType  ->      CoreType -> CoreType   (* technically redundant since we have FunTyCon *)
 | ForAllTy : CoreVar   ->      CoreType -> CoreType
 | PredTy   : PredType                   -> CoreType
@@ -44,24 +40,34 @@ Extract Inductive CoreType =>
 Extract Inductive PredType =>
    "TypeRep.PredType" [ "TypeRep.ClassP" "TypeRep.IParam" "TypeRep.EqPred" ].
 
+Variable coreTypeToString      : CoreType     -> string.    Extract Inlined Constant coreTypeToString       => "showType".
+Variable coreNameToString      : CoreName     -> string.    Extract Inlined Constant coreNameToString       => "outputableToString".
+Variable coreCoercionToString  : CoreCoercion -> string.    Extract Inlined Constant coreCoercionToString   => "outputableToString".
+Variable coreCoercionKind : CoreCoercion -> CoreType*CoreType. Extract Inlined Constant coreCoercionKind => "Coercion.coercionKind".
+Variable kindOfCoreType    : CoreType -> Kind.    Extract Inlined Constant kindOfCoreType => "(coreKindToKind . Coercion.typeKind)".
+
+(* once again, we pull the trick of having multiple Coq types map to a single Haskell type to provide stronger typing *)
+Variable TyCon           : Type.                         Extract Inlined Constant TyCon             => "TyCon.TyCon".
+Variable TyFun           : Type.                         Extract Inlined Constant TyFun             => "TyCon.TyCon".
+
 (* GHC provides decision procedures for equality on its primitive types; we tell Coq to blindly trust them *)
+Variable coreTyCon_eq        : EqDecider CoreTyCon.       Extract Inlined Constant coreTyCon_eq          => "(==)".
 Variable tyCon_eq            : EqDecider TyCon.           Extract Inlined Constant tyCon_eq              => "(==)".
+Variable tyFun_eq            : EqDecider TyFun.           Extract Inlined Constant tyFun_eq              => "(==)".
 Variable dataCon_eq          : EqDecider CoreDataCon.     Extract Inlined Constant dataCon_eq            => "(==)".
 Variable coreName_eq         : EqDecider CoreName.        Extract Inlined Constant coreName_eq           => "(==)".
 Variable coretype_eq_dec     : EqDecider CoreType.        Extract Inlined Constant coretype_eq_dec       => "checkTypeEquality".
 Instance CoreTypeEqDecidable : EqDecidable CoreType    := { eqd_dec := coretype_eq_dec }.
+Instance CoreTyConEqDecidable: EqDecidable CoreTyCon   := { eqd_dec := coreTyCon_eq }.
 Instance TyConEqDecidable    : EqDecidable TyCon       := { eqd_dec := tyCon_eq }.
+Instance TyFunEqDecidable    : EqDecidable TyFun       := { eqd_dec := tyFun_eq }.
 Instance DataConEqDecidable  : EqDecidable CoreDataCon := { eqd_dec := dataCon_eq }.
 Instance CoreNameEqDecidable : EqDecidable CoreName    := { eqd_dec := coreName_eq }.
 
-(*
-Variable coreTypeToString      : CoreType     -> string.    Extract Inlined Constant coreTypeToString       => "outputableToString".
-*)
-Variable coreTypeToString      : CoreType     -> string.
-    Extract Inlined Constant coreTypeToString       => "showType".
 
-Variable coreNameToString      : CoreName     -> string.    Extract Inlined Constant coreNameToString       => "outputableToString".
-Variable coreCoercionToString  : CoreCoercion -> string.    Extract Inlined Constant coreCoercionToString   => "outputableToString".
-Variable coreCoercionKind : CoreCoercion -> CoreType*CoreType. Extract Inlined Constant coreCoercionKind => "Coercion.coercionKind".
-Variable kindOfCoreType    : CoreType -> Kind.    Extract Inlined Constant kindOfCoreType => "(coreKindToKind . Coercion.typeKind)".
 
+Instance CoreTypeToString : ToString CoreType := { toString := coreTypeToString }.
+Instance CoreNameToString : ToString CoreName := { toString := coreNameToString }.
+Instance CoreCoercionToString : ToString CoreCoercion := { toString := coreCoercionToString }.
+Instance CoreDataConToString : ToString CoreDataCon := { toString := dataConToString }.
+Instance CoreTyConToString : ToString CoreTyCon := { toString := tyConToString }.