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 HaskGeneral.
10 Require Import HaskLiterals.
11 Require Import HaskCoreVars.
13 Variable CoreName : Type. Extract Inlined Constant CoreName => "Name.Name".
14 Variable coreName_eq : forall (a b:CoreName), sumbool (a=b) (not (a=b)). Extract Inlined Constant coreName_eq => "(==)".
15 Axiom coreName_eq_refl : ∀ v, (coreName_eq v v)=(left _ (refl_equal v)).
16 Instance CoreNameEqDecidable : EqDecidable CoreName :=
17 { eqd_dec := coreName_eq
18 ; eqd_dec_reflexive := coreName_eq_refl
21 Inductive CoreIPName : Type -> Type := . Extract Inductive CoreIPName => "CoreSyn.IPName" [ ].
23 (* this exracts onto TypeRep.Type, on the nose *)
25 | TyVarTy : CoreVar -> CoreType
26 | AppTy : CoreType -> CoreType -> CoreType (* first arg must be AppTy or TyVarTy*)
27 | TyConApp : forall {n}, TyCon n -> list CoreType -> CoreType
28 | FunTy : CoreType -> CoreType -> CoreType (* technically redundant since we have FunTyCon *)
29 | ForAllTy : CoreVar -> CoreType -> CoreType
30 | PredTy : PredType -> CoreType
32 | ClassP : forall {n}, Class_ n -> list CoreType -> PredType
33 | IParam : CoreIPName CoreName -> CoreType -> PredType
34 | EqPred : CoreType -> CoreType -> PredType.
35 Extract Inductive CoreType =>
36 "TypeRep.Type" [ "TypeRep.TyVarTy" "TypeRep.AppTy" "TypeRep.TyConApp" "TypeRep.FunTy" "TypeRep.ForAllTy" "TypeRep.PredTy" ].
37 Extract Inductive PredType =>
38 "TypeRep.PredType" [ "TypeRep.ClassP" "TypeRep.IParam" "TypeRep.EqPred" ].
40 Variable kindOfCoreType : CoreType -> Kind. Extract Inlined Constant kindOfCoreType => "(coreKindToKind . Coercion.typeKind)".
42 Definition haskLiteralToCoreType lit : CoreType :=
43 TyConApp (haskLiteralToTyCon lit) nil.
45 Inductive CoreVarSort : Type :=
46 | CoreExprVar : CoreType -> CoreVarSort
47 | CoreTypeVar : Kind -> CoreVarSort
48 | CoreCoerVar : CoreType * CoreType -> CoreVarSort.
50 Variable coreVarSort : CoreVar -> CoreVarSort. Extract Inlined Constant coreVarSort => "coreVarSort".
52 Variable coreTypeToString : CoreType -> string. Extract Inlined Constant coreTypeToString => "outputableToString".
53 Variable coreNameToString : CoreName -> string. Extract Inlined Constant coreNameToString => "outputableToString".
55 Variable CoreCoercion : Type. Extract Inlined Constant CoreCoercion => "Coercion.Coercion".
56 Variable coreCoercionToString : CoreCoercion -> string. Extract Inlined Constant coreCoercionToString => "outputableToString".
57 Variable coreCoercionKind : CoreCoercion -> CoreType*CoreType.
58 Extract Inlined Constant coreCoercionKind => "Coercion.coercionKind".