Require Import Coq.Lists.List.
Require Import HaskKinds.
Require Import HaskCoreVars.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
-Variable TyCon : Type. Extract Inlined Constant TyCon => "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 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.
+Variable classTyCon : Class_ -> CoreTyCon. Extract Inlined Constant classTyCon => "Class.classTyCon".
+Variable coreTyConToString : CoreTyCon -> string. Extract Inlined Constant coreTyConToString => "outputableToString".
+Variable coreDataConToString : CoreDataCon -> string. Extract Inlined Constant coreDataConToString => "outputableToString".
(* this exracts onto TypeRep.Type, on the nose *)
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
Extract Inductive PredType =>
"TypeRep.PredType" [ "TypeRep.ClassP" "TypeRep.IParam" "TypeRep.EqPred" ].
-(* GHC provides decision procedures for equality on its primitive types; we tell Coq to blindly trust them *)
-Variable tyCon_eq : EqDecider TyCon. Extract Inlined Constant tyCon_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 TyConEqDecidable : EqDecidable TyCon := { eqd_dec := tyCon_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)".
+Variable coreCoercionKind : Kind -> CoreType*CoreType.
+ Extract Inlined Constant coreCoercionKind => "(Coercion.coercionKind . kindToCoreKind)".
+Variable kindOfCoreType : CoreType -> Kind. Extract Inlined Constant kindOfCoreType => "(coreKindToKind . Coercion.typeKind)".
+Variable coreTypeToString : CoreType -> string. Extract Inlined Constant coreTypeToString => "(outputableToString . coreViewDeep)".
+Variable setVarType : CoreVar -> CoreType -> CoreVar. Extract Inlined Constant setVarType => "Var.setVarType".
+
+(* 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 => "(==)".
+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 }.
+Instance CoreTypeToString : ToString CoreType := { toString := coreTypeToString }.
+Instance CoreNameToString : ToString CoreName := { toString := coreNameToString }.
+Instance CoreCoercionToString : ToString CoreCoercion := { toString := coreCoercionToString }.
+Instance CoreDataConToString : ToString CoreDataCon := { toString := coreDataConToString }.
+Instance CoreTyConToString : ToString CoreTyCon := { toString := coreTyConToString }.