X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskCoreTypes.v;h=79ab342fb5ed61a53adab31a3acc89e0636e07cd;hp=4a7a056598bef9986e5aaa29795c69628588d7f2;hb=5cb97fa6ed28f55ca888bdadc4f145396cc02236;hpb=bcb16a7fa1ff772f12807c4587609fd756b7762e diff --git a/src/HaskCoreTypes.v b/src/HaskCoreTypes.v index 4a7a056..79ab342 100644 --- a/src/HaskCoreTypes.v +++ b/src/HaskCoreTypes.v @@ -9,29 +9,21 @@ Require Import Coq.Strings.String. 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 CoreCoercionCoAxiom : Type. Extract Inlined Constant CoreCoercionCoAxiom => "Coercion.CoAxiom". +Variable Int : Type. Extract Inlined Constant Int => "Prelude.Int". + +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 @@ -44,24 +36,55 @@ Extract Inductive 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 }. +Inductive CoreCoercion : Type := + CoreCoercionRefl : CoreType -> CoreCoercion + | CoreCoercionTyConAppCo : CoreTyCon -> list CoreCoercion -> CoreCoercion + | CoreCoercionAppCo : CoreCoercion -> CoreCoercion -> CoreCoercion + | CoreCoercionForAllCo : CoreVar -> CoreCoercion -> CoreCoercion + | CoreCoercionCoVarCo : CoreVar -> CoreCoercion + | CoreCoercionAxiomInstCo : CoreCoercionCoAxiom -> list CoreCoercion -> CoreCoercion + | CoreCoercionUnsafeCo : CoreType -> CoreType -> CoreCoercion + | CoreCoercionSymCo : CoreCoercion -> CoreCoercion + | CoreCoercionTransCo : CoreCoercion -> CoreCoercion -> CoreCoercion + | CoreCoercionNthCo : Int -> CoreCoercion -> CoreCoercion + | CoreCoercionInstCo : CoreCoercion -> CoreType -> CoreCoercion. -(* -Variable coreTypeToString : CoreType -> string. Extract Inlined Constant coreTypeToString => "outputableToString". -*) -Variable coreTypeToString : CoreType -> string. - Extract Inlined Constant coreTypeToString => "showType". +Extract Inductive CoreCoercion => + "Coercion.Coercion" [ + "Coercion.Refl" + "Coercion.TyConAppCo" + "Coercion.AppCo" + "Coercion.ForAllCo" + "Coercion.CoVarCo" + "Coercion.AxiomInstCo" + "Coercion.UnsafeCo" + "Coercion.SymCo" + "Coercion.TransCo" + "Coercion.NthCo" + "Coercion.InstCo" ]. 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 . Kind.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 }.