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.
13 Variable TyCon : Type. Extract Inlined Constant TyCon => "TyCon.TyCon".
14 Variable CoreDataCon : Type. Extract Inlined Constant CoreDataCon => "DataCon.DataCon".
15 Variable CoreName : Type. Extract Inlined Constant CoreName => "Name.Name".
16 Variable CoreCoercion : Type. Extract Inlined Constant CoreCoercion => "Coercion.Coercion".
17 Variable CoreCoFunConst : Type. Extract Inlined Constant TyCon => "TyCon.TyCon".
18 Variable CoreTyFunConst : Type. Extract Inlined Constant TyCon => "TyCon.TyCon".
19 Variable Class_ : Type. Extract Inlined Constant Class_ => "Class.Class".
20 Variable classTyCon : Class_ -> TyCon. Extract Inlined Constant classTyCon => "Class.classTyCon".
21 Variable tyConToString : TyCon -> string. Extract Inlined Constant tyConToString => "outputableToString".
22 Variable dataConToString : CoreDataCon-> string. Extract Inlined Constant dataConToString => "outputableToString".
23 Variable tyFunToString : CoreTyFunConst -> string. Extract Inlined Constant tyFunToString => "outputableToString".
24 Variable coFunToString : CoreCoFunConst -> string. Extract Inlined Constant coFunToString => "outputableToString".
25 Variable natTostring : nat->string. Extract Inlined Constant natTostring => "natTostring".
26 Variable CoreIPName : Type -> Type.
27 Extract Constant CoreIPName "’a" => "BasicTypes.IPName".
28 Extraction Inline CoreIPName.
30 (* this exracts onto TypeRep.Type, on the nose *)
32 | TyVarTy : CoreVar -> CoreType
33 | AppTy : CoreType -> CoreType -> CoreType (* first arg must be AppTy or TyVarTy*)
34 | TyConApp : TyCon -> list CoreType -> CoreType
35 | FunTy : CoreType -> CoreType -> CoreType (* technically redundant since we have FunTyCon *)
36 | ForAllTy : CoreVar -> CoreType -> CoreType
37 | PredTy : PredType -> CoreType
39 | ClassP : Class_ -> list CoreType -> PredType
40 | IParam : CoreIPName CoreName -> CoreType -> PredType
41 | EqPred : CoreType -> CoreType -> PredType.
42 Extract Inductive CoreType =>
43 "TypeRep.Type" [ "TypeRep.TyVarTy" "TypeRep.AppTy" "TypeRep.TyConApp" "TypeRep.FunTy" "TypeRep.ForAllTy" "TypeRep.PredTy" ].
44 Extract Inductive PredType =>
45 "TypeRep.PredType" [ "TypeRep.ClassP" "TypeRep.IParam" "TypeRep.EqPred" ].
47 (* GHC provides decision procedures for equality on its primitive types; we tell Coq to blindly trust them *)
48 Variable tyCon_eq : EqDecider TyCon. Extract Inlined Constant tyCon_eq => "(==)".
49 Variable dataCon_eq : EqDecider CoreDataCon. Extract Inlined Constant dataCon_eq => "(==)".
50 Variable coreName_eq : EqDecider CoreName. Extract Inlined Constant coreName_eq => "(==)".
51 Variable coretype_eq_dec : EqDecider CoreType. Extract Inlined Constant coretype_eq_dec => "checkTypeEquality".
52 Instance CoreTypeEqDecidable : EqDecidable CoreType := { eqd_dec := coretype_eq_dec }.
53 Instance TyConEqDecidable : EqDecidable TyCon := { eqd_dec := tyCon_eq }.
54 Instance DataConEqDecidable : EqDecidable CoreDataCon := { eqd_dec := dataCon_eq }.
55 Instance CoreNameEqDecidable : EqDecidable CoreName := { eqd_dec := coreName_eq }.
58 Variable coreTypeToString : CoreType -> string. Extract Inlined Constant coreTypeToString => "outputableToString".
60 Variable coreTypeToString : CoreType -> string.
61 Extract Inlined Constant coreTypeToString => "showType".
63 Variable coreNameToString : CoreName -> string. Extract Inlined Constant coreNameToString => "outputableToString".
64 Variable coreCoercionToString : CoreCoercion -> string. Extract Inlined Constant coreCoercionToString => "outputableToString".
65 Variable coreCoercionKind : CoreCoercion -> CoreType*CoreType. Extract Inlined Constant coreCoercionKind => "Coercion.coercionKind".
66 Variable kindOfCoreType : CoreType -> Kind. Extract Inlined Constant kindOfCoreType => "(coreKindToKind . Coercion.typeKind)".