Commit 7f3524ef authored by Danya Rogozin's avatar Danya Rogozin Committed by Marge Bot
Browse files

The Char kind (#11342)


Co-authored-by: Rinat Striungis's avatarRinat Stryungis <rinat.stryungis@serokell.io>

Implement GHC Proposal #387

* Parse char literals 'x' at the type level
* New built-in type families CmpChar, ConsSymbol, UnconsSymbol
* New KnownChar class (cf. KnownSymbol and KnownNat)
* New SomeChar type (cf. SomeSymbol and SomeNat)
* CharTyLit support in template-haskell

Updated submodules: binary, haddock.

Metric Decrease:
    T5205
    haddock.base

Metric Increase:
    Naperian
    T13035
parent 640a3ece
......@@ -247,12 +247,13 @@ basicKnownKeyNames
typeLitSortTyConName,
typeLitSymbolDataConName,
typeLitNatDataConName,
typeLitCharDataConName,
typeRepIdName,
mkTrTypeName,
mkTrConName,
mkTrAppName,
mkTrFunName,
typeSymbolTypeRepName, typeNatTypeRepName,
typeSymbolTypeRepName, typeNatTypeRepName, typeCharTypeRepName,
trGhcPrimModuleName,
-- KindReps for common cases
......@@ -439,7 +440,7 @@ basicKnownKeyNames
randomClassName, randomGenClassName, monadPlusClassName,
-- Type-level naturals
knownNatClassName, knownSymbolClassName,
knownNatClassName, knownSymbolClassName, knownCharClassName,
-- Overloaded labels
isLabelClassName,
......@@ -1405,10 +1406,12 @@ kindRepTypeLitDDataConName = dcQual gHC_TYPES (fsLit "KindRepTypeLitD") kind
typeLitSortTyConName
, typeLitSymbolDataConName
, typeLitNatDataConName
, typeLitCharDataConName
:: Name
typeLitSortTyConName = tcQual gHC_TYPES (fsLit "TypeLitSort") typeLitSortTyConKey
typeLitSymbolDataConName = dcQual gHC_TYPES (fsLit "TypeLitSymbol") typeLitSymbolDataConKey
typeLitNatDataConName = dcQual gHC_TYPES (fsLit "TypeLitNat") typeLitNatDataConKey
typeLitCharDataConName = dcQual gHC_TYPES (fsLit "TypeLitChar") typeLitCharDataConKey
-- Class Typeable, and functions for constructing `Typeable` dictionaries
typeableClassName
......@@ -1422,6 +1425,7 @@ typeableClassName
, typeRepIdName
, typeNatTypeRepName
, typeSymbolTypeRepName
, typeCharTypeRepName
, trGhcPrimModuleName
:: Name
typeableClassName = clsQual tYPEABLE_INTERNAL (fsLit "Typeable") typeableClassKey
......@@ -1435,6 +1439,7 @@ mkTrAppName = varQual tYPEABLE_INTERNAL (fsLit "mkTrApp") mkTrA
mkTrFunName = varQual tYPEABLE_INTERNAL (fsLit "mkTrFun") mkTrFunKey
typeNatTypeRepName = varQual tYPEABLE_INTERNAL (fsLit "typeNatTypeRep") typeNatTypeRepKey
typeSymbolTypeRepName = varQual tYPEABLE_INTERNAL (fsLit "typeSymbolTypeRep") typeSymbolTypeRepKey
typeCharTypeRepName = varQual tYPEABLE_INTERNAL (fsLit "typeCharTypeRep") typeCharTypeRepKey
-- this is the Typeable 'Module' for GHC.Prim (which has no code, so we place in GHC.Types)
-- See Note [Grand plan for Typeable] in GHC.Tc.Instance.Typeable.
trGhcPrimModuleName = varQual gHC_TYPES (fsLit "tr$ModuleGHCPrim") trGhcPrimModuleKey
......@@ -1617,6 +1622,8 @@ knownNatClassName :: Name
knownNatClassName = clsQual gHC_TYPENATS (fsLit "KnownNat") knownNatClassNameKey
knownSymbolClassName :: Name
knownSymbolClassName = clsQual gHC_TYPELITS (fsLit "KnownSymbol") knownSymbolClassNameKey
knownCharClassName :: Name
knownCharClassName = clsQual gHC_TYPELITS (fsLit "KnownChar") knownCharClassNameKey
-- Overloaded labels
isLabelClassName :: Name
......@@ -1773,23 +1780,26 @@ knownNatClassNameKey = mkPreludeClassUnique 42
knownSymbolClassNameKey :: Unique
knownSymbolClassNameKey = mkPreludeClassUnique 43
knownCharClassNameKey :: Unique
knownCharClassNameKey = mkPreludeClassUnique 44
ghciIoClassKey :: Unique
ghciIoClassKey = mkPreludeClassUnique 44
ghciIoClassKey = mkPreludeClassUnique 45
isLabelClassNameKey :: Unique
isLabelClassNameKey = mkPreludeClassUnique 45
isLabelClassNameKey = mkPreludeClassUnique 46
semigroupClassKey, monoidClassKey :: Unique
semigroupClassKey = mkPreludeClassUnique 46
monoidClassKey = mkPreludeClassUnique 47
semigroupClassKey = mkPreludeClassUnique 47
monoidClassKey = mkPreludeClassUnique 48
-- Implicit Parameters
ipClassKey :: Unique
ipClassKey = mkPreludeClassUnique 48
ipClassKey = mkPreludeClassUnique 49
-- Overloaded record fields
hasFieldClassNameKey :: Unique
hasFieldClassNameKey = mkPreludeClassUnique 49
hasFieldClassNameKey = mkPreludeClassUnique 50
---------------- Template Haskell -------------------
......@@ -1973,81 +1983,88 @@ uIntTyConKey = mkPreludeTyConUnique 162
uWordTyConKey = mkPreludeTyConUnique 163
-- Type-level naturals
typeSymbolKindConNameKey,
typeSymbolKindConNameKey, typeCharKindConNameKey,
typeNatAddTyFamNameKey, typeNatMulTyFamNameKey, typeNatExpTyFamNameKey,
typeNatLeqTyFamNameKey, typeNatSubTyFamNameKey
, typeSymbolCmpTyFamNameKey, typeNatCmpTyFamNameKey
, typeSymbolCmpTyFamNameKey, typeNatCmpTyFamNameKey, typeCharCmpTyFamNameKey
, typeLeqCharTyFamNameKey
, typeNatDivTyFamNameKey
, typeNatModTyFamNameKey
, typeNatLogTyFamNameKey
, typeConsSymbolTyFamNameKey, typeUnconsSymbolTyFamNameKey
:: Unique
typeSymbolKindConNameKey = mkPreludeTyConUnique 165
typeNatAddTyFamNameKey = mkPreludeTyConUnique 166
typeNatMulTyFamNameKey = mkPreludeTyConUnique 167
typeNatExpTyFamNameKey = mkPreludeTyConUnique 168
typeNatLeqTyFamNameKey = mkPreludeTyConUnique 169
typeNatSubTyFamNameKey = mkPreludeTyConUnique 170
typeSymbolCmpTyFamNameKey = mkPreludeTyConUnique 171
typeNatCmpTyFamNameKey = mkPreludeTyConUnique 172
typeNatDivTyFamNameKey = mkPreludeTyConUnique 173
typeNatModTyFamNameKey = mkPreludeTyConUnique 174
typeNatLogTyFamNameKey = mkPreludeTyConUnique 175
typeCharKindConNameKey = mkPreludeTyConUnique 166
typeNatAddTyFamNameKey = mkPreludeTyConUnique 167
typeNatMulTyFamNameKey = mkPreludeTyConUnique 168
typeNatExpTyFamNameKey = mkPreludeTyConUnique 169
typeNatLeqTyFamNameKey = mkPreludeTyConUnique 170
typeNatSubTyFamNameKey = mkPreludeTyConUnique 171
typeSymbolCmpTyFamNameKey = mkPreludeTyConUnique 172
typeNatCmpTyFamNameKey = mkPreludeTyConUnique 173
typeCharCmpTyFamNameKey = mkPreludeTyConUnique 174
typeLeqCharTyFamNameKey = mkPreludeTyConUnique 175
typeNatDivTyFamNameKey = mkPreludeTyConUnique 176
typeNatModTyFamNameKey = mkPreludeTyConUnique 177
typeNatLogTyFamNameKey = mkPreludeTyConUnique 178
typeConsSymbolTyFamNameKey = mkPreludeTyConUnique 179
typeUnconsSymbolTyFamNameKey = mkPreludeTyConUnique 180
-- Custom user type-errors
errorMessageTypeErrorFamKey :: Unique
errorMessageTypeErrorFamKey = mkPreludeTyConUnique 176
errorMessageTypeErrorFamKey = mkPreludeTyConUnique 181
ntTyConKey:: Unique
ntTyConKey = mkPreludeTyConUnique 177
ntTyConKey = mkPreludeTyConUnique 182
coercibleTyConKey :: Unique
coercibleTyConKey = mkPreludeTyConUnique 178
coercibleTyConKey = mkPreludeTyConUnique 183
proxyPrimTyConKey :: Unique
proxyPrimTyConKey = mkPreludeTyConUnique 179
proxyPrimTyConKey = mkPreludeTyConUnique 184
specTyConKey :: Unique
specTyConKey = mkPreludeTyConUnique 180
specTyConKey = mkPreludeTyConUnique 185
anyTyConKey :: Unique
anyTyConKey = mkPreludeTyConUnique 181
anyTyConKey = mkPreludeTyConUnique 186
smallArrayPrimTyConKey = mkPreludeTyConUnique 182
smallMutableArrayPrimTyConKey = mkPreludeTyConUnique 183
smallArrayPrimTyConKey = mkPreludeTyConUnique 187
smallMutableArrayPrimTyConKey = mkPreludeTyConUnique 188
staticPtrTyConKey :: Unique
staticPtrTyConKey = mkPreludeTyConUnique 184
staticPtrTyConKey = mkPreludeTyConUnique 189
staticPtrInfoTyConKey :: Unique
staticPtrInfoTyConKey = mkPreludeTyConUnique 185
staticPtrInfoTyConKey = mkPreludeTyConUnique 190
callStackTyConKey :: Unique
callStackTyConKey = mkPreludeTyConUnique 186
callStackTyConKey = mkPreludeTyConUnique 191
-- Typeables
typeRepTyConKey, someTypeRepTyConKey, someTypeRepDataConKey :: Unique
typeRepTyConKey = mkPreludeTyConUnique 187
someTypeRepTyConKey = mkPreludeTyConUnique 188
someTypeRepDataConKey = mkPreludeTyConUnique 189
typeRepTyConKey = mkPreludeTyConUnique 192
someTypeRepTyConKey = mkPreludeTyConUnique 193
someTypeRepDataConKey = mkPreludeTyConUnique 194
typeSymbolAppendFamNameKey :: Unique
typeSymbolAppendFamNameKey = mkPreludeTyConUnique 190
typeSymbolAppendFamNameKey = mkPreludeTyConUnique 195
-- Unsafe equality
unsafeEqualityTyConKey :: Unique
unsafeEqualityTyConKey = mkPreludeTyConUnique 191
unsafeEqualityTyConKey = mkPreludeTyConUnique 196
-- Linear types
multiplicityTyConKey :: Unique
multiplicityTyConKey = mkPreludeTyConUnique 192
multiplicityTyConKey = mkPreludeTyConUnique 197
unrestrictedFunTyConKey :: Unique
unrestrictedFunTyConKey = mkPreludeTyConUnique 193
unrestrictedFunTyConKey = mkPreludeTyConUnique 198
multMulTyConKey :: Unique
multMulTyConKey = mkPreludeTyConUnique 194
multMulTyConKey = mkPreludeTyConUnique 199
---------------- Template Haskell -------------------
-- GHC.Builtin.Names.TH: USES TyConUniques 200-299
......@@ -2212,19 +2229,20 @@ kindRepTYPEDataConKey = mkPreludeDataConUnique 109
kindRepTypeLitSDataConKey = mkPreludeDataConUnique 110
kindRepTypeLitDDataConKey = mkPreludeDataConUnique 111
typeLitSymbolDataConKey, typeLitNatDataConKey :: Unique
typeLitSymbolDataConKey, typeLitNatDataConKey, typeLitCharDataConKey :: Unique
typeLitSymbolDataConKey = mkPreludeDataConUnique 112
typeLitNatDataConKey = mkPreludeDataConUnique 113
typeLitCharDataConKey = mkPreludeDataConUnique 114
-- Unsafe equality
unsafeReflDataConKey :: Unique
unsafeReflDataConKey = mkPreludeDataConUnique 114
unsafeReflDataConKey = mkPreludeDataConUnique 115
-- Multiplicity
oneDataConKey, manyDataConKey :: Unique
oneDataConKey = mkPreludeDataConUnique 115
manyDataConKey = mkPreludeDataConUnique 116
oneDataConKey = mkPreludeDataConUnique 116
manyDataConKey = mkPreludeDataConUnique 117
-- ghc-bignum
integerISDataConKey, integerINDataConKey, integerIPDataConKey,
......@@ -2451,6 +2469,7 @@ mkTyConKey
, mkTrFunKey
, typeNatTypeRepKey
, typeSymbolTypeRepKey
, typeCharTypeRepKey
, typeRepIdKey
:: Unique
mkTyConKey = mkPreludeMiscIdUnique 503
......@@ -2459,8 +2478,9 @@ mkTrConKey = mkPreludeMiscIdUnique 505
mkTrAppKey = mkPreludeMiscIdUnique 506
typeNatTypeRepKey = mkPreludeMiscIdUnique 507
typeSymbolTypeRepKey = mkPreludeMiscIdUnique 508
typeRepIdKey = mkPreludeMiscIdUnique 509
mkTrFunKey = mkPreludeMiscIdUnique 510
typeCharTypeRepKey = mkPreludeMiscIdUnique 509
typeRepIdKey = mkPreludeMiscIdUnique 510
mkTrFunKey = mkPreludeMiscIdUnique 511
-- Representations for primitive types
trTYPEKey
......@@ -2468,10 +2488,10 @@ trTYPEKey
, trRuntimeRepKey
, tr'PtrRepLiftedKey
:: Unique
trTYPEKey = mkPreludeMiscIdUnique 511
trTYPE'PtrRepLiftedKey = mkPreludeMiscIdUnique 512
trRuntimeRepKey = mkPreludeMiscIdUnique 513
tr'PtrRepLiftedKey = mkPreludeMiscIdUnique 514
trTYPEKey = mkPreludeMiscIdUnique 512
trTYPE'PtrRepLiftedKey = mkPreludeMiscIdUnique 513
trRuntimeRepKey = mkPreludeMiscIdUnique 514
tr'PtrRepLiftedKey = mkPreludeMiscIdUnique 515
-- KindReps for common cases
starKindRepKey, starArrStarKindRepKey, starArrStarArrStarKindRepKey :: Unique
......
......@@ -104,7 +104,7 @@ templateHaskellNames = [
promotedTName, promotedTupleTName, promotedNilTName, promotedConsTName,
wildCardTName, implicitParamTName,
-- TyLit
numTyLitName, strTyLitName,
numTyLitName, strTyLitName, charTyLitName,
-- TyVarBndr
plainTVName, kindedTVName,
plainInvisTVName, kindedInvisTVName,
......@@ -470,9 +470,10 @@ infixTName = libFun (fsLit "infixT") infixTIdKey
implicitParamTName = libFun (fsLit "implicitParamT") implicitParamTIdKey
-- data TyLit = ...
numTyLitName, strTyLitName :: Name
numTyLitName, strTyLitName, charTyLitName :: Name
numTyLitName = libFun (fsLit "numTyLit") numTyLitIdKey
strTyLitName = libFun (fsLit "strTyLit") strTyLitIdKey
charTyLitName = libFun (fsLit "charTyLit") charTyLitIdKey
-- data TyVarBndr = ...
plainTVName, kindedTVName :: Name
......@@ -991,14 +992,15 @@ implicitParamTIdKey = mkPreludeMiscIdUnique 409
infixTIdKey = mkPreludeMiscIdUnique 410
-- data TyLit = ...
numTyLitIdKey, strTyLitIdKey :: Unique
numTyLitIdKey = mkPreludeMiscIdUnique 411
strTyLitIdKey = mkPreludeMiscIdUnique 412
numTyLitIdKey, strTyLitIdKey, charTyLitIdKey :: Unique
numTyLitIdKey = mkPreludeMiscIdUnique 411
strTyLitIdKey = mkPreludeMiscIdUnique 412
charTyLitIdKey = mkPreludeMiscIdUnique 413
-- data TyVarBndr = ...
plainTVIdKey, kindedTVIdKey :: Unique
plainTVIdKey = mkPreludeMiscIdUnique 413
kindedTVIdKey = mkPreludeMiscIdUnique 414
plainTVIdKey = mkPreludeMiscIdUnique 414
kindedTVIdKey = mkPreludeMiscIdUnique 415
plainInvisTVIdKey, kindedInvisTVIdKey :: Unique
plainInvisTVIdKey = mkPreludeMiscIdUnique 482
......@@ -1006,10 +1008,10 @@ kindedInvisTVIdKey = mkPreludeMiscIdUnique 483
-- data Role = ...
nominalRIdKey, representationalRIdKey, phantomRIdKey, inferRIdKey :: Unique
nominalRIdKey = mkPreludeMiscIdUnique 415
representationalRIdKey = mkPreludeMiscIdUnique 416
phantomRIdKey = mkPreludeMiscIdUnique 417
inferRIdKey = mkPreludeMiscIdUnique 418
nominalRIdKey = mkPreludeMiscIdUnique 416
representationalRIdKey = mkPreludeMiscIdUnique 417
phantomRIdKey = mkPreludeMiscIdUnique 418
inferRIdKey = mkPreludeMiscIdUnique 419
-- data Kind = ...
starKIdKey, constraintKIdKey :: Unique
......
......@@ -68,13 +68,14 @@ module GHC.Builtin.Types (
maybeTyCon, maybeTyConName,
nothingDataCon, nothingDataConName, promotedNothingDataCon,
justDataCon, justDataConName, promotedJustDataCon,
mkPromotedMaybeTy, mkMaybeTy, isPromotedMaybeTy,
-- * Tuples
mkTupleTy, mkTupleTy1, mkBoxedTupleTy, mkTupleStr,
tupleTyCon, tupleDataCon, tupleTyConName, tupleDataConName,
promotedTupleDataCon,
unitTyCon, unitDataCon, unitDataConId, unitTy, unitTyConKey,
pairTyCon,
pairTyCon, mkPromotedPairTy, isPromotedPairType,
unboxedUnitTy,
unboxedUnitTyCon, unboxedUnitDataCon,
unboxedTupleKind, unboxedSumKind,
......@@ -1005,6 +1006,16 @@ tupleDataCon Unboxed i = snd (unboxedTupleArr ! i)
tupleDataConName :: Boxity -> Arity -> Name
tupleDataConName sort i = dataConName (tupleDataCon sort i)
mkPromotedPairTy :: Kind -> Kind -> Type -> Type -> Type
mkPromotedPairTy k1 k2 t1 t2 = mkTyConApp (promotedTupleDataCon Boxed 2) [k1,k2,t1,t2]
isPromotedPairType :: Type -> Maybe (Type, Type)
isPromotedPairType t
| Just (tc, [_,_,x,y]) <- splitTyConApp_maybe t
, tc == promotedTupleDataCon Boxed 2
= Just (x, y)
| otherwise = Nothing
boxedTupleArr, unboxedTupleArr :: Array Int (TyCon,DataCon)
boxedTupleArr = listArray (0,mAX_TUPLE_SIZE) [mk_tuple Boxed i | i <- [0..mAX_TUPLE_SIZE]]
unboxedTupleArr = listArray (0,mAX_TUPLE_SIZE) [mk_tuple Unboxed i | i <- [0..mAX_TUPLE_SIZE]]
......@@ -1791,6 +1802,20 @@ nothingDataCon = pcDataCon nothingDataConName alpha_tyvar [] maybeTyCon
justDataCon :: DataCon
justDataCon = pcDataCon justDataConName alpha_tyvar [alphaTy] maybeTyCon
mkPromotedMaybeTy :: Kind -> Maybe Type -> Type
mkPromotedMaybeTy k (Just x) = mkTyConApp promotedJustDataCon [k,x]
mkPromotedMaybeTy k Nothing = mkTyConApp promotedNothingDataCon [k]
mkMaybeTy :: Type -> Kind
mkMaybeTy t = mkTyConApp maybeTyCon [t]
isPromotedMaybeTy :: Type -> Maybe (Maybe Type)
isPromotedMaybeTy t
| Just (tc,[_,x]) <- splitTyConApp_maybe t, tc == promotedJustDataCon = return $ Just x
| Just (tc,[_]) <- splitTyConApp_maybe t, tc == promotedNothingDataCon = return $ Nothing
| otherwise = Nothing
{-
** *********************************************************************
* *
......
......@@ -9,6 +9,7 @@ import {-# SOURCE #-} GHC.Types.Name (Name)
listTyCon :: TyCon
typeSymbolKind :: Type
charTy :: Type
mkBoxedTupleTy :: [Type] -> Type
coercibleTyCon, heqTyCon :: TyCon
......
......@@ -19,6 +19,9 @@ module GHC.Builtin.Types.Literals
, typeNatCmpTyCon
, typeSymbolCmpTyCon
, typeSymbolAppendTyCon
, typeCharCmpTyCon
, typeConsSymbolTyCon
, typeUnconsSymbolTyCon
) where
import GHC.Prelude
......@@ -49,6 +52,9 @@ import GHC.Builtin.Names
, typeNatCmpTyFamNameKey
, typeSymbolCmpTyFamNameKey
, typeSymbolAppendFamNameKey
, typeCharCmpTyFamNameKey
, typeConsSymbolTyFamNameKey
, typeUnconsSymbolTyFamNameKey
)
import GHC.Data.FastString
import Data.Maybe ( isJust )
......@@ -58,8 +64,8 @@ import Data.List ( isPrefixOf, isSuffixOf )
{-
Note [Type-level literals]
~~~~~~~~~~~~~~~~~~~~~~~~~~
There are currently two forms of type-level literals: natural numbers, and
symbols (even though this module is named GHC.Builtin.Types.Literals, it covers both).
There are currently three forms of type-level literals: natural numbers, symbols, and
characters.
Type-level literals are supported by CoAxiomRules (conditional axioms), which
power the built-in type families (see Note [Adding built-in type families]).
......@@ -148,6 +154,9 @@ typeNatTyCons =
, typeNatCmpTyCon
, typeSymbolCmpTyCon
, typeSymbolAppendTyCon
, typeCharCmpTyCon
, typeConsSymbolTyCon
, typeUnconsSymbolTyCon
]
typeNatAddTyCon :: TyCon
......@@ -205,10 +214,6 @@ typeNatModTyCon = mkTypeNatFunTyCon2 name
name = mkWiredInTyConName UserSyntax gHC_TYPENATS (fsLit "Mod")
typeNatModTyFamNameKey typeNatModTyCon
typeNatExpTyCon :: TyCon
typeNatExpTyCon = mkTypeNatFunTyCon2 name
BuiltInSynFamily
......@@ -231,8 +236,6 @@ typeNatLogTyCon = mkTypeNatFunTyCon1 name
name = mkWiredInTyConName UserSyntax gHC_TYPENATS (fsLit "Log2")
typeNatLogTyFamNameKey typeNatLogTyCon
typeNatLeqTyCon :: TyCon
typeNatLeqTyCon =
mkFamilyTyCon name
......@@ -301,6 +304,42 @@ typeSymbolAppendTyCon = mkTypeSymbolFunTyCon2 name
name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "AppendSymbol")
typeSymbolAppendFamNameKey typeSymbolAppendTyCon
typeConsSymbolTyCon :: TyCon
typeConsSymbolTyCon =
mkFamilyTyCon name
(mkTemplateAnonTyConBinders [ charTy, typeSymbolKind ])
typeSymbolKind
Nothing
(BuiltInSynFamTyCon ops)
Nothing
(Injective [True, True])
where
name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "ConsSymbol")
typeConsSymbolTyFamNameKey typeConsSymbolTyCon
ops = BuiltInSynFamily
{ sfMatchFam = matchFamConsSymbol
, sfInteractTop = interactTopConsSymbol
, sfInteractInert = interactInertConsSymbol
}
typeUnconsSymbolTyCon :: TyCon
typeUnconsSymbolTyCon =
mkFamilyTyCon name
(mkTemplateAnonTyConBinders [ typeSymbolKind ])
(mkMaybeTy charSymbolPairKind)
Nothing
(BuiltInSynFamTyCon ops)
Nothing
(Injective [True])
where
name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "UnconsSymbol")
typeUnconsSymbolTyFamNameKey typeUnconsSymbolTyCon
ops = BuiltInSynFamily
{ sfMatchFam = matchFamUnconsSymbol
, sfInteractTop = interactTopUnconsSymbol
, sfInteractInert = interactInertUnconsSymbol
}
-- Make a unary built-in constructor of kind: Nat -> Nat
mkTypeNatFunTyCon1 :: Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon1 op tcb =
......@@ -312,7 +351,6 @@ mkTypeNatFunTyCon1 op tcb =
Nothing
NotInjective
-- Make a binary built-in constructor of kind: Nat -> Nat -> Nat
mkTypeNatFunTyCon2 :: Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon2 op tcb =
......@@ -335,7 +373,6 @@ mkTypeSymbolFunTyCon2 op tcb =
Nothing
NotInjective
{-------------------------------------------------------------------------------
Built-in rules axioms
-------------------------------------------------------------------------------}
......@@ -350,6 +387,8 @@ axAddDef
, axCmpNatDef
, axCmpSymbolDef
, axAppendSymbolDef
, axConsSymbolDef
, axUnconsSymbolDef
, axAdd0L
, axAdd0R
, axMul0L
......@@ -374,19 +413,19 @@ axAddDef
, axLogDef
:: CoAxiomRule
axAddDef = mkBinAxiom "AddDef" typeNatAddTyCon $
axAddDef = mkBinAxiom "AddDef" typeNatAddTyCon isNumLitTy isNumLitTy $
\x y -> Just $ num (x + y)
axMulDef = mkBinAxiom "MulDef" typeNatMulTyCon $
axMulDef = mkBinAxiom "MulDef" typeNatMulTyCon isNumLitTy isNumLitTy $
\x y -> Just $ num (x * y)
axExpDef = mkBinAxiom "ExpDef" typeNatExpTyCon $
axExpDef = mkBinAxiom "ExpDef" typeNatExpTyCon isNumLitTy isNumLitTy $
\x y -> Just $ num (x ^ y)
axLeqDef = mkBinAxiom "LeqDef" typeNatLeqTyCon $
axLeqDef = mkBinAxiom "LeqDef" typeNatLeqTyCon isNumLitTy isNumLitTy $
\x y -> Just $ bool (x <= y)
axCmpNatDef = mkBinAxiom "CmpNatDef" typeNatCmpTyCon
axCmpNatDef = mkBinAxiom "CmpNatDef" typeNatCmpTyCon isNumLitTy isNumLitTy
$ \x y -> Just $ ordering (compare x y)
axCmpSymbolDef =
......@@ -413,18 +452,27 @@ axAppendSymbolDef = CoAxiomRule
return (mkTyConApp typeSymbolAppendTyCon [s1, t1] === z)
}
axSubDef = mkBinAxiom "SubDef" typeNatSubTyCon $
axConsSymbolDef =
mkBinAxiom "ConsSymbolDef" typeConsSymbolTyCon isCharLitTy isStrLitTy $
\c str -> Just $ mkStrLitTy (consFS c str)
axUnconsSymbolDef =
mkUnAxiom "UnconsSymbolDef" typeUnconsSymbolTyCon isStrLitTy $
\str -> Just $
mkPromotedMaybeTy charSymbolPairKind (fmap reifyCharSymbolPairTy (unconsFS str))
axSubDef = mkBinAxiom "SubDef" typeNatSubTyCon isNumLitTy isNumLitTy $
\x y -> fmap num (minus x y)
axDivDef = mkBinAxiom "DivDef" typeNatDivTyCon $
axDivDef = mkBinAxiom "DivDef" typeNatDivTyCon isNumLitTy isNumLitTy $
\x y -> do guard (y /= 0)
return (num (div x y))
axModDef = mkBinAxiom "ModDef" typeNatModTyCon $
axModDef = mkBinAxiom "ModDef" typeNatModTyCon isNumLitTy isNumLitTy $
\x y -> do guard (y /= 0)
return (num (mod x y))
axLogDef = mkUnAxiom "LogDef" typeNatLogTyCon $
axLogDef = mkUnAxiom "LogDef" typeNatLogTyCon isNumLitTy $
\x -> do (a,_) <- genLog x 2
return (num a)
......@@ -463,7 +511,10 @@ typeNatCoAxiomRules = listToUFM $ map (\x -> (coaxrName x, x))
, axLeqDef
, axCmpNatDef
, axCmpSymbolDef
, axCmpCharDef
, axAppendSymbolDef
, axConsSymbolDef
, axUnconsSymbolDef
, axAdd0L
, axAdd0R
, axMul0L
......@@ -476,6 +527,7 @@ typeNatCoAxiomRules = listToUFM $ map (\x -> (coaxrName x, x))
, axLeqRefl
, axCmpNatRefl
, axCmpSymbolRefl
, axCmpCharRefl
, axLeq0L
, axSubDef
, axSub0R
......@@ -534,6 +586,12 @@ bool :: Bool -> Type
bool b = if b then mkTyConApp promotedTrueDataCon []
else mkTyConApp promotedFalseDataCon []
charSymbolPair :: Type -> Type -> Type
charSymbolPair = mkPromotedPairTy charTy typeSymbolKind
charSymbolPairKind :: Kind
charSymbolPairKind = mkTyConApp pairTyCon [charTy, typeSymbolKind]
isBoolLitTy :: Type -> Maybe Bool
isBoolLitTy tc =
do (tc,[]) <- splitTyConApp_maybe tc
......@@ -566,40 +624,37 @@ known p x = case isNumLitTy x of
Just a -> p a
Nothing -> False
mkUnAxiom :: String -> TyCon -> (Integer -> Maybe Type) -> CoAxiomRule
mkUnAxiom str tc f =
mkUnAxiom :: String -> TyCon -> (Type -> Maybe a) -> (a -> Maybe Type) -> CoAxiomRule
mkUnAxiom str tc isReqTy f =
CoAxiomRule
{ coaxrName = fsLit str
, coaxrAsmpRoles = [Nominal]