1 (*********************************************************************************************************************************)
2 (* HaskCoreTypes: basically GHC's TypeRep.Type imported into Coqland *)
3 (*********************************************************************************************************************************)
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.
15 Variable CoreCoercionCoAxiom : Type. Extract Inlined Constant CoreCoercionCoAxiom => "Coercion.CoAxiom".
16 Variable Int : Type. Extract Inlined Constant Int => "Prelude.Int".
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".
22 (* this exracts onto TypeRep.Type, on the nose *)
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
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" ].
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.
52 Extract Inductive CoreCoercion =>
59 "Coercion.AxiomInstCo"
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".
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 }.