{-# LANGUAGE LambdaCase #-}
module GHC.Builtin.Types.Literals
( typeNatTyCons
, typeNatCoAxiomRules
, BuiltInSynFamily(..)
, typeNatAddTyCon
, typeNatMulTyCon
, typeNatExpTyCon
, typeNatSubTyCon
, typeNatDivTyCon
, typeNatModTyCon
, typeNatLogTyCon
, typeNatCmpTyCon
, typeSymbolCmpTyCon
, typeSymbolAppendTyCon
, typeCharCmpTyCon
, typeConsSymbolTyCon
, typeUnconsSymbolTyCon
, typeCharToNatTyCon
, typeNatToCharTyCon
) where
import GHC.Prelude
import GHC.Core.Type
import GHC.Data.Pair
import GHC.Tc.Utils.TcType ( TcType, tcEqType )
import GHC.Core.TyCon ( TyCon, FamTyConFlav(..), mkFamilyTyCon
, Injectivity(..) )
import GHC.Core.Coercion ( Role(..) )
import GHC.Tc.Types.Constraint ( Xi )
import GHC.Core.Coercion.Axiom ( CoAxiomRule(..), BuiltInSynFamily(..), TypeEqn )
import GHC.Types.Name ( Name, BuiltInSyntax(..) )
import GHC.Types.Unique.FM
import GHC.Builtin.Types
import GHC.Builtin.Types.Prim ( mkTemplateAnonTyConBinders )
import GHC.Builtin.Names
( gHC_TYPELITS
, gHC_TYPELITS_INTERNAL
, gHC_TYPENATS
, gHC_TYPENATS_INTERNAL
, typeNatAddTyFamNameKey
, typeNatMulTyFamNameKey
, typeNatExpTyFamNameKey
, typeNatSubTyFamNameKey
, typeNatDivTyFamNameKey
, typeNatModTyFamNameKey
, typeNatLogTyFamNameKey
, typeNatCmpTyFamNameKey
, typeSymbolCmpTyFamNameKey
, typeSymbolAppendFamNameKey
, typeCharCmpTyFamNameKey
, typeConsSymbolTyFamNameKey
, typeUnconsSymbolTyFamNameKey
, typeCharToNatTyFamNameKey
, typeNatToCharTyFamNameKey
)
import GHC.Data.FastString
import Control.Monad ( guard )
import Data.List ( isPrefixOf, isSuffixOf )
import qualified Data.Char as Char
typeNatTyCons :: [TyCon]
typeNatTyCons :: [TyCon]
typeNatTyCons =
[ TyCon
typeNatAddTyCon
, TyCon
typeNatMulTyCon
, TyCon
typeNatExpTyCon
, TyCon
typeNatSubTyCon
, TyCon
typeNatDivTyCon
, TyCon
typeNatModTyCon
, TyCon
typeNatLogTyCon
, TyCon
typeNatCmpTyCon
, TyCon
typeSymbolCmpTyCon
, TyCon
typeSymbolAppendTyCon
, TyCon
typeCharCmpTyCon
, TyCon
typeConsSymbolTyCon
, TyCon
typeUnconsSymbolTyCon
, TyCon
typeCharToNatTyCon
, TyCon
typeNatToCharTyCon
]
typeNatAddTyCon :: TyCon
typeNatAddTyCon :: TyCon
typeNatAddTyCon = Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon2 Name
name
BuiltInSynFamily
{ sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
sfMatchFam = [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamAdd
, sfInteractTop :: [Type] -> Type -> [TypeEqn]
sfInteractTop = [Type] -> Type -> [TypeEqn]
interactTopAdd
, sfInteractInert :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
sfInteractInert = [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertAdd
}
where
name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_TYPENATS (String -> FastString
fsLit String
"+")
Unique
typeNatAddTyFamNameKey TyCon
typeNatAddTyCon
typeNatSubTyCon :: TyCon
typeNatSubTyCon :: TyCon
typeNatSubTyCon = Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon2 Name
name
BuiltInSynFamily
{ sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
sfMatchFam = [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamSub
, sfInteractTop :: [Type] -> Type -> [TypeEqn]
sfInteractTop = [Type] -> Type -> [TypeEqn]
interactTopSub
, sfInteractInert :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
sfInteractInert = [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertSub
}
where
name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_TYPENATS (String -> FastString
fsLit String
"-")
Unique
typeNatSubTyFamNameKey TyCon
typeNatSubTyCon
typeNatMulTyCon :: TyCon
typeNatMulTyCon :: TyCon
typeNatMulTyCon = Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon2 Name
name
BuiltInSynFamily
{ sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
sfMatchFam = [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamMul
, sfInteractTop :: [Type] -> Type -> [TypeEqn]
sfInteractTop = [Type] -> Type -> [TypeEqn]
interactTopMul
, sfInteractInert :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
sfInteractInert = [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertMul
}
where
name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_TYPENATS (String -> FastString
fsLit String
"*")
Unique
typeNatMulTyFamNameKey TyCon
typeNatMulTyCon
typeNatDivTyCon :: TyCon
typeNatDivTyCon :: TyCon
typeNatDivTyCon = Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon2 Name
name
BuiltInSynFamily
{ sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
sfMatchFam = [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamDiv
, sfInteractTop :: [Type] -> Type -> [TypeEqn]
sfInteractTop = [Type] -> Type -> [TypeEqn]
interactTopDiv
, sfInteractInert :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
sfInteractInert = [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertDiv
}
where
name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_TYPENATS (String -> FastString
fsLit String
"Div")
Unique
typeNatDivTyFamNameKey TyCon
typeNatDivTyCon
typeNatModTyCon :: TyCon
typeNatModTyCon :: TyCon
typeNatModTyCon = Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon2 Name
name
BuiltInSynFamily
{ sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
sfMatchFam = [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamMod
, sfInteractTop :: [Type] -> Type -> [TypeEqn]
sfInteractTop = [Type] -> Type -> [TypeEqn]
interactTopMod
, sfInteractInert :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
sfInteractInert = [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertMod
}
where
name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_TYPENATS (String -> FastString
fsLit String
"Mod")
Unique
typeNatModTyFamNameKey TyCon
typeNatModTyCon
typeNatExpTyCon :: TyCon
typeNatExpTyCon :: TyCon
typeNatExpTyCon = Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon2 Name
name
BuiltInSynFamily
{ sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
sfMatchFam = [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamExp
, sfInteractTop :: [Type] -> Type -> [TypeEqn]
sfInteractTop = [Type] -> Type -> [TypeEqn]
interactTopExp
, sfInteractInert :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
sfInteractInert = [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertExp
}
where
name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_TYPENATS (String -> FastString
fsLit String
"^")
Unique
typeNatExpTyFamNameKey TyCon
typeNatExpTyCon
typeNatLogTyCon :: TyCon
typeNatLogTyCon :: TyCon
typeNatLogTyCon = Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon1 Name
name
BuiltInSynFamily
{ sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
sfMatchFam = [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamLog
, sfInteractTop :: [Type] -> Type -> [TypeEqn]
sfInteractTop = [Type] -> Type -> [TypeEqn]
interactTopLog
, sfInteractInert :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
sfInteractInert = [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertLog
}
where
name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_TYPENATS (String -> FastString
fsLit String
"Log2")
Unique
typeNatLogTyFamNameKey TyCon
typeNatLogTyCon
typeNatCmpTyCon :: TyCon
typeNatCmpTyCon :: TyCon
typeNatCmpTyCon =
Name
-> [TyConBinder]
-> Type
-> Maybe Name
-> FamTyConFlav
-> Maybe Class
-> Injectivity
-> TyCon
mkFamilyTyCon Name
name
([Type] -> [TyConBinder]
mkTemplateAnonTyConBinders [ Type
naturalTy, Type
naturalTy ])
Type
orderingKind
forall a. Maybe a
Nothing
(BuiltInSynFamily -> FamTyConFlav
BuiltInSynFamTyCon BuiltInSynFamily
ops)
forall a. Maybe a
Nothing
Injectivity
NotInjective
where
name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_TYPENATS_INTERNAL (String -> FastString
fsLit String
"CmpNat")
Unique
typeNatCmpTyFamNameKey TyCon
typeNatCmpTyCon
ops :: BuiltInSynFamily
ops = BuiltInSynFamily
{ sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
sfMatchFam = [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamCmpNat
, sfInteractTop :: [Type] -> Type -> [TypeEqn]
sfInteractTop = [Type] -> Type -> [TypeEqn]
interactTopCmpNat
, sfInteractInert :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
sfInteractInert = \[Type]
_ Type
_ [Type]
_ Type
_ -> []
}
typeSymbolCmpTyCon :: TyCon
typeSymbolCmpTyCon :: TyCon
typeSymbolCmpTyCon =
Name
-> [TyConBinder]
-> Type
-> Maybe Name
-> FamTyConFlav
-> Maybe Class
-> Injectivity
-> TyCon
mkFamilyTyCon Name
name
([Type] -> [TyConBinder]
mkTemplateAnonTyConBinders [ Type
typeSymbolKind, Type
typeSymbolKind ])
Type
orderingKind
forall a. Maybe a
Nothing
(BuiltInSynFamily -> FamTyConFlav
BuiltInSynFamTyCon BuiltInSynFamily
ops)
forall a. Maybe a
Nothing
Injectivity
NotInjective
where
name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_TYPELITS_INTERNAL (String -> FastString
fsLit String
"CmpSymbol")
Unique
typeSymbolCmpTyFamNameKey TyCon
typeSymbolCmpTyCon
ops :: BuiltInSynFamily
ops = BuiltInSynFamily
{ sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
sfMatchFam = [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamCmpSymbol
, sfInteractTop :: [Type] -> Type -> [TypeEqn]
sfInteractTop = [Type] -> Type -> [TypeEqn]
interactTopCmpSymbol
, sfInteractInert :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
sfInteractInert = \[Type]
_ Type
_ [Type]
_ Type
_ -> []
}
typeSymbolAppendTyCon :: TyCon
typeSymbolAppendTyCon :: TyCon
typeSymbolAppendTyCon = Name -> BuiltInSynFamily -> TyCon
mkTypeSymbolFunTyCon2 Name
name
BuiltInSynFamily
{ sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
sfMatchFam = [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamAppendSymbol
, sfInteractTop :: [Type] -> Type -> [TypeEqn]
sfInteractTop = [Type] -> Type -> [TypeEqn]
interactTopAppendSymbol
, sfInteractInert :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
sfInteractInert = [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertAppendSymbol
}
where
name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_TYPELITS (String -> FastString
fsLit String
"AppendSymbol")
Unique
typeSymbolAppendFamNameKey TyCon
typeSymbolAppendTyCon
typeConsSymbolTyCon :: TyCon
typeConsSymbolTyCon :: TyCon
typeConsSymbolTyCon =
Name
-> [TyConBinder]
-> Type
-> Maybe Name
-> FamTyConFlav
-> Maybe Class
-> Injectivity
-> TyCon
mkFamilyTyCon Name
name
([Type] -> [TyConBinder]
mkTemplateAnonTyConBinders [ Type
charTy, Type
typeSymbolKind ])
Type
typeSymbolKind
forall a. Maybe a
Nothing
(BuiltInSynFamily -> FamTyConFlav
BuiltInSynFamTyCon BuiltInSynFamily
ops)
forall a. Maybe a
Nothing
([Bool] -> Injectivity
Injective [Bool
True, Bool
True])
where
name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_TYPELITS (String -> FastString
fsLit String
"ConsSymbol")
Unique
typeConsSymbolTyFamNameKey TyCon
typeConsSymbolTyCon
ops :: BuiltInSynFamily
ops = BuiltInSynFamily
{ sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
sfMatchFam = [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamConsSymbol
, sfInteractTop :: [Type] -> Type -> [TypeEqn]
sfInteractTop = [Type] -> Type -> [TypeEqn]
interactTopConsSymbol
, sfInteractInert :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
sfInteractInert = [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertConsSymbol
}
typeUnconsSymbolTyCon :: TyCon
typeUnconsSymbolTyCon :: TyCon
typeUnconsSymbolTyCon =
Name
-> [TyConBinder]
-> Type
-> Maybe Name
-> FamTyConFlav
-> Maybe Class
-> Injectivity
-> TyCon
mkFamilyTyCon Name
name
([Type] -> [TyConBinder]
mkTemplateAnonTyConBinders [ Type
typeSymbolKind ])
(Type -> Type
mkMaybeTy Type
charSymbolPairKind)
forall a. Maybe a
Nothing
(BuiltInSynFamily -> FamTyConFlav
BuiltInSynFamTyCon BuiltInSynFamily
ops)
forall a. Maybe a
Nothing
([Bool] -> Injectivity
Injective [Bool
True])
where
name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_TYPELITS (String -> FastString
fsLit String
"UnconsSymbol")
Unique
typeUnconsSymbolTyFamNameKey TyCon
typeUnconsSymbolTyCon
ops :: BuiltInSynFamily
ops = BuiltInSynFamily
{ sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
sfMatchFam = [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamUnconsSymbol
, sfInteractTop :: [Type] -> Type -> [TypeEqn]
sfInteractTop = [Type] -> Type -> [TypeEqn]
interactTopUnconsSymbol
, sfInteractInert :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
sfInteractInert = [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertUnconsSymbol
}
typeCharToNatTyCon :: TyCon
typeCharToNatTyCon :: TyCon
typeCharToNatTyCon =
Name
-> [TyConBinder]
-> Type
-> Maybe Name
-> FamTyConFlav
-> Maybe Class
-> Injectivity
-> TyCon
mkFamilyTyCon Name
name
([Type] -> [TyConBinder]
mkTemplateAnonTyConBinders [ Type
charTy ])
Type
naturalTy
forall a. Maybe a
Nothing
(BuiltInSynFamily -> FamTyConFlav
BuiltInSynFamTyCon BuiltInSynFamily
ops)
forall a. Maybe a
Nothing
([Bool] -> Injectivity
Injective [Bool
True])
where
name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_TYPELITS (String -> FastString
fsLit String
"CharToNat")
Unique
typeCharToNatTyFamNameKey TyCon
typeCharToNatTyCon
ops :: BuiltInSynFamily
ops = BuiltInSynFamily
{ sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
sfMatchFam = [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamCharToNat
, sfInteractTop :: [Type] -> Type -> [TypeEqn]
sfInteractTop = [Type] -> Type -> [TypeEqn]
interactTopCharToNat
, sfInteractInert :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
sfInteractInert = \[Type]
_ Type
_ [Type]
_ Type
_ -> []
}
typeNatToCharTyCon :: TyCon
typeNatToCharTyCon :: TyCon
typeNatToCharTyCon =
Name
-> [TyConBinder]
-> Type
-> Maybe Name
-> FamTyConFlav
-> Maybe Class
-> Injectivity
-> TyCon
mkFamilyTyCon Name
name
([Type] -> [TyConBinder]
mkTemplateAnonTyConBinders [ Type
naturalTy ])
Type
charTy
forall a. Maybe a
Nothing
(BuiltInSynFamily -> FamTyConFlav
BuiltInSynFamTyCon BuiltInSynFamily
ops)
forall a. Maybe a
Nothing
([Bool] -> Injectivity
Injective [Bool
True])
where
name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_TYPELITS (String -> FastString
fsLit String
"NatToChar")
Unique
typeNatToCharTyFamNameKey TyCon
typeNatToCharTyCon
ops :: BuiltInSynFamily
ops = BuiltInSynFamily
{ sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
sfMatchFam = [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamNatToChar
, sfInteractTop :: [Type] -> Type -> [TypeEqn]
sfInteractTop = [Type] -> Type -> [TypeEqn]
interactTopNatToChar
, sfInteractInert :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
sfInteractInert = \[Type]
_ Type
_ [Type]
_ Type
_ -> []
}
mkTypeNatFunTyCon1 :: Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon1 :: Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon1 Name
op BuiltInSynFamily
tcb =
Name
-> [TyConBinder]
-> Type
-> Maybe Name
-> FamTyConFlav
-> Maybe Class
-> Injectivity
-> TyCon
mkFamilyTyCon Name
op
([Type] -> [TyConBinder]
mkTemplateAnonTyConBinders [ Type
naturalTy ])
Type
naturalTy
forall a. Maybe a
Nothing
(BuiltInSynFamily -> FamTyConFlav
BuiltInSynFamTyCon BuiltInSynFamily
tcb)
forall a. Maybe a
Nothing
Injectivity
NotInjective
mkTypeNatFunTyCon2 :: Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon2 :: Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon2 Name
op BuiltInSynFamily
tcb =
Name
-> [TyConBinder]
-> Type
-> Maybe Name
-> FamTyConFlav
-> Maybe Class
-> Injectivity
-> TyCon
mkFamilyTyCon Name
op
([Type] -> [TyConBinder]
mkTemplateAnonTyConBinders [ Type
naturalTy, Type
naturalTy ])
Type
naturalTy
forall a. Maybe a
Nothing
(BuiltInSynFamily -> FamTyConFlav
BuiltInSynFamTyCon BuiltInSynFamily
tcb)
forall a. Maybe a
Nothing
Injectivity
NotInjective
mkTypeSymbolFunTyCon2 :: Name -> BuiltInSynFamily -> TyCon
mkTypeSymbolFunTyCon2 :: Name -> BuiltInSynFamily -> TyCon
mkTypeSymbolFunTyCon2 Name
op BuiltInSynFamily
tcb =
Name
-> [TyConBinder]
-> Type
-> Maybe Name
-> FamTyConFlav
-> Maybe Class
-> Injectivity
-> TyCon
mkFamilyTyCon Name
op
([Type] -> [TyConBinder]
mkTemplateAnonTyConBinders [ Type
typeSymbolKind, Type
typeSymbolKind ])
Type
typeSymbolKind
forall a. Maybe a
Nothing
(BuiltInSynFamily -> FamTyConFlav
BuiltInSynFamTyCon BuiltInSynFamily
tcb)
forall a. Maybe a
Nothing
Injectivity
NotInjective
axAddDef
, axMulDef
, axExpDef
, axCmpNatDef
, axCmpSymbolDef
, axAppendSymbolDef
, axConsSymbolDef
, axUnconsSymbolDef
, axCharToNatDef
, axNatToCharDef
, axAdd0L
, axAdd0R
, axMul0L
, axMul0R
, axMul1L
, axMul1R
, axExp1L
, axExp0R
, axExp1R
, axCmpNatRefl
, axCmpSymbolRefl
, axSubDef
, axSub0R
, axAppendSymbol0R
, axAppendSymbol0L
, axDivDef
, axDiv1
, axModDef
, axMod1
, axLogDef
:: CoAxiomRule
axAddDef :: CoAxiomRule
axAddDef = forall a b.
String
-> TyCon
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> CoAxiomRule
mkBinAxiom String
"AddDef" TyCon
typeNatAddTyCon Type -> Maybe Integer
isNumLitTy Type -> Maybe Integer
isNumLitTy forall a b. (a -> b) -> a -> b
$
\Integer
x Integer
y -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Integer -> Type
num (Integer
x forall a. Num a => a -> a -> a
+ Integer
y)
axMulDef :: CoAxiomRule
axMulDef = forall a b.
String
-> TyCon
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> CoAxiomRule
mkBinAxiom String
"MulDef" TyCon
typeNatMulTyCon Type -> Maybe Integer
isNumLitTy Type -> Maybe Integer
isNumLitTy forall a b. (a -> b) -> a -> b
$
\Integer
x Integer
y -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Integer -> Type
num (Integer
x forall a. Num a => a -> a -> a
* Integer
y)
axExpDef :: CoAxiomRule
axExpDef = forall a b.
String
-> TyCon
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> CoAxiomRule
mkBinAxiom String
"ExpDef" TyCon
typeNatExpTyCon Type -> Maybe Integer
isNumLitTy Type -> Maybe Integer
isNumLitTy forall a b. (a -> b) -> a -> b
$
\Integer
x Integer
y -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Integer -> Type
num (Integer
x forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
y)
axCmpNatDef :: CoAxiomRule
axCmpNatDef = forall a b.
String
-> TyCon
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> CoAxiomRule
mkBinAxiom String
"CmpNatDef" TyCon
typeNatCmpTyCon Type -> Maybe Integer
isNumLitTy Type -> Maybe Integer
isNumLitTy
forall a b. (a -> b) -> a -> b
$ \Integer
x Integer
y -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Ordering -> Type
ordering (forall a. Ord a => a -> a -> Ordering
compare Integer
x Integer
y)
axCmpSymbolDef :: CoAxiomRule
axCmpSymbolDef =
CoAxiomRule
{ coaxrName :: FastString
coaxrName = String -> FastString
fsLit String
"CmpSymbolDef"
, coaxrAsmpRoles :: [Role]
coaxrAsmpRoles = [Role
Nominal, Role
Nominal]
, coaxrRole :: Role
coaxrRole = Role
Nominal
, coaxrProves :: [TypeEqn] -> Maybe TypeEqn
coaxrProves = \[TypeEqn]
cs ->
do [Pair Type
s1 Type
s2, Pair Type
t1 Type
t2] <- forall (m :: * -> *) a. Monad m => a -> m a
return [TypeEqn]
cs
FastString
s2' <- Type -> Maybe FastString
isStrLitTy Type
s2
FastString
t2' <- Type -> Maybe FastString
isStrLitTy Type
t2
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCon -> [Type] -> Type
mkTyConApp TyCon
typeSymbolCmpTyCon [Type
s1,Type
t1] Type -> Type -> TypeEqn
===
Ordering -> Type
ordering (FastString -> FastString -> Ordering
lexicalCompareFS FastString
s2' FastString
t2')) }
axAppendSymbolDef :: CoAxiomRule
axAppendSymbolDef = CoAxiomRule
{ coaxrName :: FastString
coaxrName = String -> FastString
fsLit String
"AppendSymbolDef"
, coaxrAsmpRoles :: [Role]
coaxrAsmpRoles = [Role
Nominal, Role
Nominal]
, coaxrRole :: Role
coaxrRole = Role
Nominal
, coaxrProves :: [TypeEqn] -> Maybe TypeEqn
coaxrProves = \[TypeEqn]
cs ->
do [Pair Type
s1 Type
s2, Pair Type
t1 Type
t2] <- forall (m :: * -> *) a. Monad m => a -> m a
return [TypeEqn]
cs
FastString
s2' <- Type -> Maybe FastString
isStrLitTy Type
s2
FastString
t2' <- Type -> Maybe FastString
isStrLitTy Type
t2
let z :: Type
z = FastString -> Type
mkStrLitTy (FastString -> FastString -> FastString
appendFS FastString
s2' FastString
t2')
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCon -> [Type] -> Type
mkTyConApp TyCon
typeSymbolAppendTyCon [Type
s1, Type
t1] Type -> Type -> TypeEqn
=== Type
z)
}
axConsSymbolDef :: CoAxiomRule
axConsSymbolDef =
forall a b.
String
-> TyCon
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> CoAxiomRule
mkBinAxiom String
"ConsSymbolDef" TyCon
typeConsSymbolTyCon Type -> Maybe Char
isCharLitTy Type -> Maybe FastString
isStrLitTy forall a b. (a -> b) -> a -> b
$
\Char
c FastString
str -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ FastString -> Type
mkStrLitTy (Char -> FastString -> FastString
consFS Char
c FastString
str)
axUnconsSymbolDef :: CoAxiomRule
axUnconsSymbolDef =
forall a.
String
-> TyCon -> (Type -> Maybe a) -> (a -> Maybe Type) -> CoAxiomRule
mkUnAxiom String
"UnconsSymbolDef" TyCon
typeUnconsSymbolTyCon Type -> Maybe FastString
isStrLitTy forall a b. (a -> b) -> a -> b
$
\FastString
str -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$
Type -> Maybe Type -> Type
mkPromotedMaybeTy Type
charSymbolPairKind (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Char, FastString) -> Type
reifyCharSymbolPairTy (FastString -> Maybe (Char, FastString)
unconsFS FastString
str))
axCharToNatDef :: CoAxiomRule
axCharToNatDef =
forall a.
String
-> TyCon -> (Type -> Maybe a) -> (a -> Maybe Type) -> CoAxiomRule
mkUnAxiom String
"CharToNatDef" TyCon
typeCharToNatTyCon Type -> Maybe Char
isCharLitTy forall a b. (a -> b) -> a -> b
$
\Char
c -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Integer -> Type
num (Char -> Integer
charToInteger Char
c)
axNatToCharDef :: CoAxiomRule
axNatToCharDef =
forall a.
String
-> TyCon -> (Type -> Maybe a) -> (a -> Maybe Type) -> CoAxiomRule
mkUnAxiom String
"NatToCharDef" TyCon
typeNatToCharTyCon Type -> Maybe Integer
isNumLitTy forall a b. (a -> b) -> a -> b
$
\Integer
n -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Char -> Type
mkCharLitTy (Integer -> Maybe Char
integerToChar Integer
n)
axSubDef :: CoAxiomRule
axSubDef = forall a b.
String
-> TyCon
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> CoAxiomRule
mkBinAxiom String
"SubDef" TyCon
typeNatSubTyCon Type -> Maybe Integer
isNumLitTy Type -> Maybe Integer
isNumLitTy forall a b. (a -> b) -> a -> b
$
\Integer
x Integer
y -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Integer -> Type
num (Integer -> Integer -> Maybe Integer
minus Integer
x Integer
y)
axDivDef :: CoAxiomRule
axDivDef = forall a b.
String
-> TyCon
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> CoAxiomRule
mkBinAxiom String
"DivDef" TyCon
typeNatDivTyCon Type -> Maybe Integer
isNumLitTy Type -> Maybe Integer
isNumLitTy forall a b. (a -> b) -> a -> b
$
\Integer
x Integer
y -> do forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
y forall a. Eq a => a -> a -> Bool
/= Integer
0)
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Type
num (forall a. Integral a => a -> a -> a
div Integer
x Integer
y))
axModDef :: CoAxiomRule
axModDef = forall a b.
String
-> TyCon
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> CoAxiomRule
mkBinAxiom String
"ModDef" TyCon
typeNatModTyCon Type -> Maybe Integer
isNumLitTy Type -> Maybe Integer
isNumLitTy forall a b. (a -> b) -> a -> b
$
\Integer
x Integer
y -> do forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
y forall a. Eq a => a -> a -> Bool
/= Integer
0)
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Type
num (forall a. Integral a => a -> a -> a
mod Integer
x Integer
y))
axLogDef :: CoAxiomRule
axLogDef = forall a.
String
-> TyCon -> (Type -> Maybe a) -> (a -> Maybe Type) -> CoAxiomRule
mkUnAxiom String
"LogDef" TyCon
typeNatLogTyCon Type -> Maybe Integer
isNumLitTy forall a b. (a -> b) -> a -> b
$
\Integer
x -> do (Integer
a,Bool
_) <- Integer -> Integer -> Maybe (Integer, Bool)
genLog Integer
x Integer
2
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Type
num Integer
a)
axAdd0L :: CoAxiomRule
axAdd0L = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 String
"Add0L" forall a b. (a -> b) -> a -> b
$ \(Pair Type
s Type
t) -> (Integer -> Type
num Integer
0 Type -> Type -> Type
.+. Type
s) Type -> Type -> TypeEqn
=== Type
t
axAdd0R :: CoAxiomRule
axAdd0R = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 String
"Add0R" forall a b. (a -> b) -> a -> b
$ \(Pair Type
s Type
t) -> (Type
s Type -> Type -> Type
.+. Integer -> Type
num Integer
0) Type -> Type -> TypeEqn
=== Type
t
axSub0R :: CoAxiomRule
axSub0R = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 String
"Sub0R" forall a b. (a -> b) -> a -> b
$ \(Pair Type
s Type
t) -> (Type
s Type -> Type -> Type
.-. Integer -> Type
num Integer
0) Type -> Type -> TypeEqn
=== Type
t
axMul0L :: CoAxiomRule
axMul0L = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 String
"Mul0L" forall a b. (a -> b) -> a -> b
$ \(Pair Type
s Type
_) -> (Integer -> Type
num Integer
0 Type -> Type -> Type
.*. Type
s) Type -> Type -> TypeEqn
=== Integer -> Type
num Integer
0
axMul0R :: CoAxiomRule
axMul0R = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 String
"Mul0R" forall a b. (a -> b) -> a -> b
$ \(Pair Type
s Type
_) -> (Type
s Type -> Type -> Type
.*. Integer -> Type
num Integer
0) Type -> Type -> TypeEqn
=== Integer -> Type
num Integer
0
axMul1L :: CoAxiomRule
axMul1L = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 String
"Mul1L" forall a b. (a -> b) -> a -> b
$ \(Pair Type
s Type
t) -> (Integer -> Type
num Integer
1 Type -> Type -> Type
.*. Type
s) Type -> Type -> TypeEqn
=== Type
t
axMul1R :: CoAxiomRule
axMul1R = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 String
"Mul1R" forall a b. (a -> b) -> a -> b
$ \(Pair Type
s Type
t) -> (Type
s Type -> Type -> Type
.*. Integer -> Type
num Integer
1) Type -> Type -> TypeEqn
=== Type
t
axDiv1 :: CoAxiomRule
axDiv1 = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 String
"Div1" forall a b. (a -> b) -> a -> b
$ \(Pair Type
s Type
t) -> (Type -> Type -> Type
tDiv Type
s (Integer -> Type
num Integer
1) Type -> Type -> TypeEqn
=== Type
t)
axMod1 :: CoAxiomRule
axMod1 = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 String
"Mod1" forall a b. (a -> b) -> a -> b
$ \(Pair Type
s Type
_) -> (Type -> Type -> Type
tMod Type
s (Integer -> Type
num Integer
1) Type -> Type -> TypeEqn
=== Integer -> Type
num Integer
0)
axExp1L :: CoAxiomRule
axExp1L = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 String
"Exp1L" forall a b. (a -> b) -> a -> b
$ \(Pair Type
s Type
_) -> (Integer -> Type
num Integer
1 Type -> Type -> Type
.^. Type
s) Type -> Type -> TypeEqn
=== Integer -> Type
num Integer
1
axExp0R :: CoAxiomRule
axExp0R = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 String
"Exp0R" forall a b. (a -> b) -> a -> b
$ \(Pair Type
s Type
_) -> (Type
s Type -> Type -> Type
.^. Integer -> Type
num Integer
0) Type -> Type -> TypeEqn
=== Integer -> Type
num Integer
1
axExp1R :: CoAxiomRule
axExp1R = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 String
"Exp1R" forall a b. (a -> b) -> a -> b
$ \(Pair Type
s Type
t) -> (Type
s Type -> Type -> Type
.^. Integer -> Type
num Integer
1) Type -> Type -> TypeEqn
=== Type
t
axCmpNatRefl :: CoAxiomRule
axCmpNatRefl = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 String
"CmpNatRefl"
forall a b. (a -> b) -> a -> b
$ \(Pair Type
s Type
_) -> (Type -> Type -> Type
cmpNat Type
s Type
s) Type -> Type -> TypeEqn
=== Ordering -> Type
ordering Ordering
EQ
axCmpSymbolRefl :: CoAxiomRule
axCmpSymbolRefl = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 String
"CmpSymbolRefl"
forall a b. (a -> b) -> a -> b
$ \(Pair Type
s Type
_) -> (Type -> Type -> Type
cmpSymbol Type
s Type
s) Type -> Type -> TypeEqn
=== Ordering -> Type
ordering Ordering
EQ
axAppendSymbol0R :: CoAxiomRule
axAppendSymbol0R = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 String
"Concat0R"
forall a b. (a -> b) -> a -> b
$ \(Pair Type
s Type
t) -> (FastString -> Type
mkStrLitTy FastString
nilFS Type -> Type -> Type
`appendSymbol` Type
s) Type -> Type -> TypeEqn
=== Type
t
axAppendSymbol0L :: CoAxiomRule
axAppendSymbol0L = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 String
"Concat0L"
forall a b. (a -> b) -> a -> b
$ \(Pair Type
s Type
t) -> (Type
s Type -> Type -> Type
`appendSymbol` FastString -> Type
mkStrLitTy FastString
nilFS) Type -> Type -> TypeEqn
=== Type
t
typeNatCoAxiomRules :: UniqFM FastString CoAxiomRule
typeNatCoAxiomRules :: UniqFM FastString CoAxiomRule
typeNatCoAxiomRules = forall key elt. Uniquable key => [(key, elt)] -> UniqFM key elt
listToUFM forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\CoAxiomRule
x -> (CoAxiomRule -> FastString
coaxrName CoAxiomRule
x, CoAxiomRule
x))
[ CoAxiomRule
axAddDef
, CoAxiomRule
axMulDef
, CoAxiomRule
axExpDef
, CoAxiomRule
axCmpNatDef
, CoAxiomRule
axCmpSymbolDef
, CoAxiomRule
axCmpCharDef
, CoAxiomRule
axAppendSymbolDef
, CoAxiomRule
axConsSymbolDef
, CoAxiomRule
axUnconsSymbolDef
, CoAxiomRule
axCharToNatDef
, CoAxiomRule
axNatToCharDef
, CoAxiomRule
axAdd0L
, CoAxiomRule
axAdd0R
, CoAxiomRule
axMul0L
, CoAxiomRule
axMul0R
, CoAxiomRule
axMul1L
, CoAxiomRule
axMul1R
, CoAxiomRule
axExp1L
, CoAxiomRule
axExp0R
, CoAxiomRule
axExp1R
, CoAxiomRule
axCmpNatRefl
, CoAxiomRule
axCmpSymbolRefl
, CoAxiomRule
axCmpCharRefl
, CoAxiomRule
axSubDef
, CoAxiomRule
axSub0R
, CoAxiomRule
axAppendSymbol0R
, CoAxiomRule
axAppendSymbol0L
, CoAxiomRule
axDivDef
, CoAxiomRule
axDiv1
, CoAxiomRule
axModDef
, CoAxiomRule
axMod1
, CoAxiomRule
axLogDef
]
(.+.) :: Type -> Type -> Type
Type
s .+. :: Type -> Type -> Type
.+. Type
t = TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatAddTyCon [Type
s,Type
t]
(.-.) :: Type -> Type -> Type
Type
s .-. :: Type -> Type -> Type
.-. Type
t = TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatSubTyCon [Type
s,Type
t]
(.*.) :: Type -> Type -> Type
Type
s .*. :: Type -> Type -> Type
.*. Type
t = TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatMulTyCon [Type
s,Type
t]
tDiv :: Type -> Type -> Type
tDiv :: Type -> Type -> Type
tDiv Type
s Type
t = TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatDivTyCon [Type
s,Type
t]
tMod :: Type -> Type -> Type
tMod :: Type -> Type -> Type
tMod Type
s Type
t = TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatModTyCon [Type
s,Type
t]
(.^.) :: Type -> Type -> Type
Type
s .^. :: Type -> Type -> Type
.^. Type
t = TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatExpTyCon [Type
s,Type
t]
cmpNat :: Type -> Type -> Type
cmpNat :: Type -> Type -> Type
cmpNat Type
s Type
t = TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatCmpTyCon [Type
s,Type
t]
cmpSymbol :: Type -> Type -> Type
cmpSymbol :: Type -> Type -> Type
cmpSymbol Type
s Type
t = TyCon -> [Type] -> Type
mkTyConApp TyCon
typeSymbolCmpTyCon [Type
s,Type
t]
appendSymbol :: Type -> Type -> Type
appendSymbol :: Type -> Type -> Type
appendSymbol Type
s Type
t = TyCon -> [Type] -> Type
mkTyConApp TyCon
typeSymbolAppendTyCon [Type
s, Type
t]
(===) :: Type -> Type -> Pair Type
Type
x === :: Type -> Type -> TypeEqn
=== Type
y = forall a. a -> a -> Pair a
Pair Type
x Type
y
num :: Integer -> Type
num :: Integer -> Type
num = Integer -> Type
mkNumLitTy
charSymbolPair :: Type -> Type -> Type
charSymbolPair :: Type -> Type -> Type
charSymbolPair = Type -> Type -> Type -> Type -> Type
mkPromotedPairTy Type
charTy Type
typeSymbolKind
charSymbolPairKind :: Kind
charSymbolPairKind :: Type
charSymbolPairKind = TyCon -> [Type] -> Type
mkTyConApp TyCon
pairTyCon [Type
charTy, Type
typeSymbolKind]
orderingKind :: Kind
orderingKind :: Type
orderingKind = TyCon -> [Type] -> Type
mkTyConApp TyCon
orderingTyCon []
ordering :: Ordering -> Type
ordering :: Ordering -> Type
ordering Ordering
o =
case Ordering
o of
Ordering
LT -> TyCon -> [Type] -> Type
mkTyConApp TyCon
promotedLTDataCon []
Ordering
EQ -> TyCon -> [Type] -> Type
mkTyConApp TyCon
promotedEQDataCon []
Ordering
GT -> TyCon -> [Type] -> Type
mkTyConApp TyCon
promotedGTDataCon []
isOrderingLitTy :: Type -> Maybe Ordering
isOrderingLitTy :: Type -> Maybe Ordering
isOrderingLitTy Type
tc =
do (TyCon
tc1,[]) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
tc
case () of
()
_ | TyCon
tc1 forall a. Eq a => a -> a -> Bool
== TyCon
promotedLTDataCon -> forall (m :: * -> *) a. Monad m => a -> m a
return Ordering
LT
| TyCon
tc1 forall a. Eq a => a -> a -> Bool
== TyCon
promotedEQDataCon -> forall (m :: * -> *) a. Monad m => a -> m a
return Ordering
EQ
| TyCon
tc1 forall a. Eq a => a -> a -> Bool
== TyCon
promotedGTDataCon -> forall (m :: * -> *) a. Monad m => a -> m a
return Ordering
GT
| Bool
otherwise -> forall a. Maybe a
Nothing
known :: (Integer -> Bool) -> TcType -> Bool
known :: (Integer -> Bool) -> Type -> Bool
known Integer -> Bool
p Type
x = case Type -> Maybe Integer
isNumLitTy Type
x of
Just Integer
a -> Integer -> Bool
p Integer
a
Maybe Integer
Nothing -> Bool
False
mkUnAxiom :: String -> TyCon -> (Type -> Maybe a) -> (a -> Maybe Type) -> CoAxiomRule
mkUnAxiom :: forall a.
String
-> TyCon -> (Type -> Maybe a) -> (a -> Maybe Type) -> CoAxiomRule
mkUnAxiom String
str TyCon
tc Type -> Maybe a
isReqTy a -> Maybe Type
f =
CoAxiomRule
{ coaxrName :: FastString
coaxrName = String -> FastString
fsLit String
str
, coaxrAsmpRoles :: [Role]
coaxrAsmpRoles = [Role
Nominal]
, coaxrRole :: Role
coaxrRole = Role
Nominal
, coaxrProves :: [TypeEqn] -> Maybe TypeEqn
coaxrProves = \[TypeEqn]
cs ->
do [Pair Type
s1 Type
s2] <- forall (m :: * -> *) a. Monad m => a -> m a
return [TypeEqn]
cs
a
s2' <- Type -> Maybe a
isReqTy Type
s2
Type
z <- a -> Maybe Type
f a
s2'
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type
s1] Type -> Type -> TypeEqn
=== Type
z)
}
mkBinAxiom :: String -> TyCon ->
(Type -> Maybe a) ->
(Type -> Maybe b) ->
(a -> b -> Maybe Type) -> CoAxiomRule
mkBinAxiom :: forall a b.
String
-> TyCon
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> CoAxiomRule
mkBinAxiom String
str TyCon
tc Type -> Maybe a
isReqTy1 Type -> Maybe b
isReqTy2 a -> b -> Maybe Type
f =
CoAxiomRule
{ coaxrName :: FastString
coaxrName = String -> FastString
fsLit String
str
, coaxrAsmpRoles :: [Role]
coaxrAsmpRoles = [Role
Nominal, Role
Nominal]
, coaxrRole :: Role
coaxrRole = Role
Nominal
, coaxrProves :: [TypeEqn] -> Maybe TypeEqn
coaxrProves = \[TypeEqn]
cs ->
do [Pair Type
s1 Type
s2, Pair Type
t1 Type
t2] <- forall (m :: * -> *) a. Monad m => a -> m a
return [TypeEqn]
cs
a
s2' <- Type -> Maybe a
isReqTy1 Type
s2
b
t2' <- Type -> Maybe b
isReqTy2 Type
t2
Type
z <- a -> b -> Maybe Type
f a
s2' b
t2'
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type
s1,Type
t1] Type -> Type -> TypeEqn
=== Type
z)
}
mkAxiom1 :: String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 :: String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 String
str TypeEqn -> TypeEqn
f =
CoAxiomRule
{ coaxrName :: FastString
coaxrName = String -> FastString
fsLit String
str
, coaxrAsmpRoles :: [Role]
coaxrAsmpRoles = [Role
Nominal]
, coaxrRole :: Role
coaxrRole = Role
Nominal
, coaxrProves :: [TypeEqn] -> Maybe TypeEqn
coaxrProves = \case [TypeEqn
eqn] -> forall a. a -> Maybe a
Just (TypeEqn -> TypeEqn
f TypeEqn
eqn)
[TypeEqn]
_ -> forall a. Maybe a
Nothing
}
matchFamAdd :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamAdd :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamAdd [Type
s,Type
t]
| Just Integer
0 <- Maybe Integer
mbX = forall a. a -> Maybe a
Just (CoAxiomRule
axAdd0L, [Type
t], Type
t)
| Just Integer
0 <- Maybe Integer
mbY = forall a. a -> Maybe a
Just (CoAxiomRule
axAdd0R, [Type
s], Type
s)
| Just Integer
x <- Maybe Integer
mbX, Just Integer
y <- Maybe Integer
mbY =
forall a. a -> Maybe a
Just (CoAxiomRule
axAddDef, [Type
s,Type
t], Integer -> Type
num (Integer
x forall a. Num a => a -> a -> a
+ Integer
y))
where mbX :: Maybe Integer
mbX = Type -> Maybe Integer
isNumLitTy Type
s
mbY :: Maybe Integer
mbY = Type -> Maybe Integer
isNumLitTy Type
t
matchFamAdd [Type]
_ = forall a. Maybe a
Nothing
matchFamSub :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamSub :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamSub [Type
s,Type
t]
| Just Integer
0 <- Maybe Integer
mbY = forall a. a -> Maybe a
Just (CoAxiomRule
axSub0R, [Type
s], Type
s)
| Just Integer
x <- Maybe Integer
mbX, Just Integer
y <- Maybe Integer
mbY, Just Integer
z <- Integer -> Integer -> Maybe Integer
minus Integer
x Integer
y =
forall a. a -> Maybe a
Just (CoAxiomRule
axSubDef, [Type
s,Type
t], Integer -> Type
num Integer
z)
where mbX :: Maybe Integer
mbX = Type -> Maybe Integer
isNumLitTy Type
s
mbY :: Maybe Integer
mbY = Type -> Maybe Integer
isNumLitTy Type
t
matchFamSub [Type]
_ = forall a. Maybe a
Nothing
matchFamMul :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamMul :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamMul [Type
s,Type
t]
| Just Integer
0 <- Maybe Integer
mbX = forall a. a -> Maybe a
Just (CoAxiomRule
axMul0L, [Type
t], Integer -> Type
num Integer
0)
| Just Integer
0 <- Maybe Integer
mbY = forall a. a -> Maybe a
Just (CoAxiomRule
axMul0R, [Type
s], Integer -> Type
num Integer
0)
| Just Integer
1 <- Maybe Integer
mbX = forall a. a -> Maybe a
Just (CoAxiomRule
axMul1L, [Type
t], Type
t)
| Just Integer
1 <- Maybe Integer
mbY = forall a. a -> Maybe a
Just (CoAxiomRule
axMul1R, [Type
s], Type
s)
| Just Integer
x <- Maybe Integer
mbX, Just Integer
y <- Maybe Integer
mbY =
forall a. a -> Maybe a
Just (CoAxiomRule
axMulDef, [Type
s,Type
t], Integer -> Type
num (Integer
x forall a. Num a => a -> a -> a
* Integer
y))
where mbX :: Maybe Integer
mbX = Type -> Maybe Integer
isNumLitTy Type
s
mbY :: Maybe Integer
mbY = Type -> Maybe Integer
isNumLitTy Type
t
matchFamMul [Type]
_ = forall a. Maybe a
Nothing
matchFamDiv :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamDiv :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamDiv [Type
s,Type
t]
| Just Integer
1 <- Maybe Integer
mbY = forall a. a -> Maybe a
Just (CoAxiomRule
axDiv1, [Type
s], Type
s)
| Just Integer
x <- Maybe Integer
mbX, Just Integer
y <- Maybe Integer
mbY, Integer
y forall a. Eq a => a -> a -> Bool
/= Integer
0 = forall a. a -> Maybe a
Just (CoAxiomRule
axDivDef, [Type
s,Type
t], Integer -> Type
num (forall a. Integral a => a -> a -> a
div Integer
x Integer
y))
where mbX :: Maybe Integer
mbX = Type -> Maybe Integer
isNumLitTy Type
s
mbY :: Maybe Integer
mbY = Type -> Maybe Integer
isNumLitTy Type
t
matchFamDiv [Type]
_ = forall a. Maybe a
Nothing
matchFamMod :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamMod :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamMod [Type
s,Type
t]
| Just Integer
1 <- Maybe Integer
mbY = forall a. a -> Maybe a
Just (CoAxiomRule
axMod1, [Type
s], Integer -> Type
num Integer
0)
| Just Integer
x <- Maybe Integer
mbX, Just Integer
y <- Maybe Integer
mbY, Integer
y forall a. Eq a => a -> a -> Bool
/= Integer
0 = forall a. a -> Maybe a
Just (CoAxiomRule
axModDef, [Type
s,Type
t], Integer -> Type
num (forall a. Integral a => a -> a -> a
mod Integer
x Integer
y))
where mbX :: Maybe Integer
mbX = Type -> Maybe Integer
isNumLitTy Type
s
mbY :: Maybe Integer
mbY = Type -> Maybe Integer
isNumLitTy Type
t
matchFamMod [Type]
_ = forall a. Maybe a
Nothing
matchFamExp :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamExp :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamExp [Type
s,Type
t]
| Just Integer
0 <- Maybe Integer
mbY = forall a. a -> Maybe a
Just (CoAxiomRule
axExp0R, [Type
s], Integer -> Type
num Integer
1)
| Just Integer
1 <- Maybe Integer
mbX = forall a. a -> Maybe a
Just (CoAxiomRule
axExp1L, [Type
t], Integer -> Type
num Integer
1)
| Just Integer
1 <- Maybe Integer
mbY = forall a. a -> Maybe a
Just (CoAxiomRule
axExp1R, [Type
s], Type
s)
| Just Integer
x <- Maybe Integer
mbX, Just Integer
y <- Maybe Integer
mbY =
forall a. a -> Maybe a
Just (CoAxiomRule
axExpDef, [Type
s,Type
t], Integer -> Type
num (Integer
x forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
y))
where mbX :: Maybe Integer
mbX = Type -> Maybe Integer
isNumLitTy Type
s
mbY :: Maybe Integer
mbY = Type -> Maybe Integer
isNumLitTy Type
t
matchFamExp [Type]
_ = forall a. Maybe a
Nothing
matchFamLog :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamLog :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamLog [Type
s]
| Just Integer
x <- Maybe Integer
mbX, Just (Integer
n,Bool
_) <- Integer -> Integer -> Maybe (Integer, Bool)
genLog Integer
x Integer
2 = forall a. a -> Maybe a
Just (CoAxiomRule
axLogDef, [Type
s], Integer -> Type
num Integer
n)
where mbX :: Maybe Integer
mbX = Type -> Maybe Integer
isNumLitTy Type
s
matchFamLog [Type]
_ = forall a. Maybe a
Nothing
matchFamCmpNat :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamCmpNat :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamCmpNat [Type
s,Type
t]
| Just Integer
x <- Maybe Integer
mbX, Just Integer
y <- Maybe Integer
mbY =
forall a. a -> Maybe a
Just (CoAxiomRule
axCmpNatDef, [Type
s,Type
t], Ordering -> Type
ordering (forall a. Ord a => a -> a -> Ordering
compare Integer
x Integer
y))
| HasDebugCallStack => Type -> Type -> Bool
tcEqType Type
s Type
t = forall a. a -> Maybe a
Just (CoAxiomRule
axCmpNatRefl, [Type
s], Ordering -> Type
ordering Ordering
EQ)
where mbX :: Maybe Integer
mbX = Type -> Maybe Integer
isNumLitTy Type
s
mbY :: Maybe Integer
mbY = Type -> Maybe Integer
isNumLitTy Type
t
matchFamCmpNat [Type]
_ = forall a. Maybe a
Nothing
matchFamCmpSymbol :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamCmpSymbol :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamCmpSymbol [Type
s,Type
t]
| Just FastString
x <- Maybe FastString
mbX, Just FastString
y <- Maybe FastString
mbY =
forall a. a -> Maybe a
Just (CoAxiomRule
axCmpSymbolDef, [Type
s,Type
t], Ordering -> Type
ordering (FastString -> FastString -> Ordering
lexicalCompareFS FastString
x FastString
y))
| HasDebugCallStack => Type -> Type -> Bool
tcEqType Type
s Type
t = forall a. a -> Maybe a
Just (CoAxiomRule
axCmpSymbolRefl, [Type
s], Ordering -> Type
ordering Ordering
EQ)
where mbX :: Maybe FastString
mbX = Type -> Maybe FastString
isStrLitTy Type
s
mbY :: Maybe FastString
mbY = Type -> Maybe FastString
isStrLitTy Type
t
matchFamCmpSymbol [Type]
_ = forall a. Maybe a
Nothing
matchFamAppendSymbol :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamAppendSymbol :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamAppendSymbol [Type
s,Type
t]
| Just FastString
x <- Maybe FastString
mbX, FastString -> Bool
nullFS FastString
x = forall a. a -> Maybe a
Just (CoAxiomRule
axAppendSymbol0R, [Type
t], Type
t)
| Just FastString
y <- Maybe FastString
mbY, FastString -> Bool
nullFS FastString
y = forall a. a -> Maybe a
Just (CoAxiomRule
axAppendSymbol0L, [Type
s], Type
s)
| Just FastString
x <- Maybe FastString
mbX, Just FastString
y <- Maybe FastString
mbY =
forall a. a -> Maybe a
Just (CoAxiomRule
axAppendSymbolDef, [Type
s,Type
t], FastString -> Type
mkStrLitTy (FastString -> FastString -> FastString
appendFS FastString
x FastString
y))
where
mbX :: Maybe FastString
mbX = Type -> Maybe FastString
isStrLitTy Type
s
mbY :: Maybe FastString
mbY = Type -> Maybe FastString
isStrLitTy Type
t
matchFamAppendSymbol [Type]
_ = forall a. Maybe a
Nothing
matchFamConsSymbol :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamConsSymbol :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamConsSymbol [Type
s,Type
t]
| Just Char
x <- Maybe Char
mbX, Just FastString
y <- Maybe FastString
mbY =
forall a. a -> Maybe a
Just (CoAxiomRule
axConsSymbolDef, [Type
s,Type
t], FastString -> Type
mkStrLitTy (Char -> FastString -> FastString
consFS Char
x FastString
y))
where
mbX :: Maybe Char
mbX = Type -> Maybe Char
isCharLitTy Type
s
mbY :: Maybe FastString
mbY = Type -> Maybe FastString
isStrLitTy Type
t
matchFamConsSymbol [Type]
_ = forall a. Maybe a
Nothing
reifyCharSymbolPairTy :: (Char, FastString) -> Type
reifyCharSymbolPairTy :: (Char, FastString) -> Type
reifyCharSymbolPairTy (Char
c, FastString
s) = Type -> Type -> Type
charSymbolPair (Char -> Type
mkCharLitTy Char
c) (FastString -> Type
mkStrLitTy FastString
s)
matchFamUnconsSymbol :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamUnconsSymbol :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamUnconsSymbol [Type
s]
| Just FastString
x <- Maybe FastString
mbX =
forall a. a -> Maybe a
Just (CoAxiomRule
axUnconsSymbolDef, [Type
s]
, Type -> Maybe Type -> Type
mkPromotedMaybeTy Type
charSymbolPairKind (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Char, FastString) -> Type
reifyCharSymbolPairTy (FastString -> Maybe (Char, FastString)
unconsFS FastString
x)))
where
mbX :: Maybe FastString
mbX = Type -> Maybe FastString
isStrLitTy Type
s
matchFamUnconsSymbol [Type]
_ = forall a. Maybe a
Nothing
matchFamCharToNat :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamCharToNat :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamCharToNat [Type
c]
| Just Char
c' <- Type -> Maybe Char
isCharLitTy Type
c, Integer
n <- Char -> Integer
charToInteger Char
c'
= forall a. a -> Maybe a
Just (CoAxiomRule
axCharToNatDef, [Type
c], Integer -> Type
mkNumLitTy Integer
n)
| Bool
otherwise = forall a. Maybe a
Nothing
matchFamCharToNat [Type]
_ = forall a. Maybe a
Nothing
matchFamNatToChar :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamNatToChar :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamNatToChar [Type
n]
| Just Integer
n' <- Type -> Maybe Integer
isNumLitTy Type
n, Just Char
c <- Integer -> Maybe Char
integerToChar Integer
n'
= forall a. a -> Maybe a
Just (CoAxiomRule
axNatToCharDef, [Type
n], Char -> Type
mkCharLitTy Char
c)
| Bool
otherwise = forall a. Maybe a
Nothing
matchFamNatToChar [Type]
_ = forall a. Maybe a
Nothing
charToInteger :: Char -> Integer
charToInteger :: Char -> Integer
charToInteger Char
c = forall a b. (Integral a, Num b) => a -> b
fromIntegral (Char -> Int
Char.ord Char
c)
integerToChar :: Integer -> Maybe Char
integerToChar :: Integer -> Maybe Char
integerToChar Integer
n | Bool
inBounds = forall a. a -> Maybe a
Just (Int -> Char
Char.chr (forall a. Num a => Integer -> a
fromInteger Integer
n))
where inBounds :: Bool
inBounds = Integer
n forall a. Ord a => a -> a -> Bool
>= Char -> Integer
charToInteger forall a. Bounded a => a
minBound Bool -> Bool -> Bool
&&
Integer
n forall a. Ord a => a -> a -> Bool
<= Char -> Integer
charToInteger forall a. Bounded a => a
maxBound
integerToChar Integer
_ = forall a. Maybe a
Nothing
interactTopAdd :: [Xi] -> Xi -> [Pair Type]
interactTopAdd :: [Type] -> Type -> [TypeEqn]
interactTopAdd [Type
s,Type
t] Type
r
| Just Integer
0 <- Maybe Integer
mbZ = [ Type
s Type -> Type -> TypeEqn
=== Integer -> Type
num Integer
0, Type
t Type -> Type -> TypeEqn
=== Integer -> Type
num Integer
0 ]
| Just Integer
x <- Maybe Integer
mbX, Just Integer
z <- Maybe Integer
mbZ, Just Integer
y <- Integer -> Integer -> Maybe Integer
minus Integer
z Integer
x = [Type
t Type -> Type -> TypeEqn
=== Integer -> Type
num Integer
y]
| Just Integer
y <- Maybe Integer
mbY, Just Integer
z <- Maybe Integer
mbZ, Just Integer
x <- Integer -> Integer -> Maybe Integer
minus Integer
z Integer
y = [Type
s Type -> Type -> TypeEqn
=== Integer -> Type
num Integer
x]
where
mbX :: Maybe Integer
mbX = Type -> Maybe Integer
isNumLitTy Type
s
mbY :: Maybe Integer
mbY = Type -> Maybe Integer
isNumLitTy Type
t
mbZ :: Maybe Integer
mbZ = Type -> Maybe Integer
isNumLitTy Type
r
interactTopAdd [Type]
_ Type
_ = []
interactTopSub :: [Xi] -> Xi -> [Pair Type]
interactTopSub :: [Type] -> Type -> [TypeEqn]
interactTopSub [Type
s,Type
t] Type
r
| Just Integer
z <- Maybe Integer
mbZ = [ Type
s Type -> Type -> TypeEqn
=== (Integer -> Type
num Integer
z Type -> Type -> Type
.+. Type
t) ]
where
mbZ :: Maybe Integer
mbZ = Type -> Maybe Integer
isNumLitTy Type
r
interactTopSub [Type]
_ Type
_ = []
interactTopMul :: [Xi] -> Xi -> [Pair Type]
interactTopMul :: [Type] -> Type -> [TypeEqn]
interactTopMul [Type
s,Type
t] Type
r
| Just Integer
1 <- Maybe Integer
mbZ = [ Type
s Type -> Type -> TypeEqn
=== Integer -> Type
num Integer
1, Type
t Type -> Type -> TypeEqn
=== Integer -> Type
num Integer
1 ]
| Just Integer
x <- Maybe Integer
mbX, Just Integer
z <- Maybe Integer
mbZ, Just Integer
y <- Integer -> Integer -> Maybe Integer
divide Integer
z Integer
x = [Type
t Type -> Type -> TypeEqn
=== Integer -> Type
num Integer
y]
| Just Integer
y <- Maybe Integer
mbY, Just Integer
z <- Maybe Integer
mbZ, Just Integer
x <- Integer -> Integer -> Maybe Integer
divide Integer
z Integer
y = [Type
s Type -> Type -> TypeEqn
=== Integer -> Type
num Integer
x]
where
mbX :: Maybe Integer
mbX = Type -> Maybe Integer
isNumLitTy Type
s
mbY :: Maybe Integer
mbY = Type -> Maybe Integer
isNumLitTy Type
t
mbZ :: Maybe Integer
mbZ = Type -> Maybe Integer
isNumLitTy Type
r
interactTopMul [Type]
_ Type
_ = []
interactTopDiv :: [Xi] -> Xi -> [Pair Type]
interactTopDiv :: [Type] -> Type -> [TypeEqn]
interactTopDiv [Type]
_ Type
_ = []
interactTopMod :: [Xi] -> Xi -> [Pair Type]
interactTopMod :: [Type] -> Type -> [TypeEqn]
interactTopMod [Type]
_ Type
_ = []
interactTopExp :: [Xi] -> Xi -> [Pair Type]
interactTopExp :: [Type] -> Type -> [TypeEqn]
interactTopExp [Type
s,Type
t] Type
r
| Just Integer
0 <- Maybe Integer
mbZ = [ Type
s Type -> Type -> TypeEqn
=== Integer -> Type
num Integer
0 ]
| Just Integer
x <- Maybe Integer
mbX, Just Integer
z <- Maybe Integer
mbZ, Just Integer
y <- Integer -> Integer -> Maybe Integer
logExact Integer
z Integer
x = [Type
t Type -> Type -> TypeEqn
=== Integer -> Type
num Integer
y]
| Just Integer
y <- Maybe Integer
mbY, Just Integer
z <- Maybe Integer
mbZ, Just Integer
x <- Integer -> Integer -> Maybe Integer
rootExact Integer
z Integer
y = [Type
s Type -> Type -> TypeEqn
=== Integer -> Type
num Integer
x]
where
mbX :: Maybe Integer
mbX = Type -> Maybe Integer
isNumLitTy Type
s
mbY :: Maybe Integer
mbY = Type -> Maybe Integer
isNumLitTy Type
t
mbZ :: Maybe Integer
mbZ = Type -> Maybe Integer
isNumLitTy Type
r
interactTopExp [Type]
_ Type
_ = []
interactTopLog :: [Xi] -> Xi -> [Pair Type]
interactTopLog :: [Type] -> Type -> [TypeEqn]
interactTopLog [Type]
_ Type
_ = []
interactTopCmpNat :: [Xi] -> Xi -> [Pair Type]
interactTopCmpNat :: [Type] -> Type -> [TypeEqn]
interactTopCmpNat [Type
s,Type
t] Type
r
| Just Ordering
EQ <- Type -> Maybe Ordering
isOrderingLitTy Type
r = [ Type
s Type -> Type -> TypeEqn
=== Type
t ]
interactTopCmpNat [Type]
_ Type
_ = []
interactTopCmpSymbol :: [Xi] -> Xi -> [Pair Type]
interactTopCmpSymbol :: [Type] -> Type -> [TypeEqn]
interactTopCmpSymbol [Type
s,Type
t] Type
r
| Just Ordering
EQ <- Type -> Maybe Ordering
isOrderingLitTy Type
r = [ Type
s Type -> Type -> TypeEqn
=== Type
t ]
interactTopCmpSymbol [Type]
_ Type
_ = []
interactTopAppendSymbol :: [Xi] -> Xi -> [Pair Type]
interactTopAppendSymbol :: [Type] -> Type -> [TypeEqn]
interactTopAppendSymbol [Type
s,Type
t] Type
r
| Just FastString
z <- Maybe FastString
mbZ, FastString -> Bool
nullFS FastString
z =
[Type
s Type -> Type -> TypeEqn
=== FastString -> Type
mkStrLitTy FastString
nilFS, Type
t Type -> Type -> TypeEqn
=== FastString -> Type
mkStrLitTy FastString
nilFS ]
| Just String
x <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FastString -> String
unpackFS Maybe FastString
mbX, Just String
z <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FastString -> String
unpackFS Maybe FastString
mbZ, String
x forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
z =
[ Type
t Type -> Type -> TypeEqn
=== FastString -> Type
mkStrLitTy (String -> FastString
mkFastString forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
drop (forall (t :: * -> *) a. Foldable t => t a -> Int
length String
x) String
z) ]
| Just String
y <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FastString -> String
unpackFS Maybe FastString
mbY, Just String
z <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FastString -> String
unpackFS Maybe FastString
mbZ, String
y forall a. Eq a => [a] -> [a] -> Bool
`isSuffixOf` String
z =
[ Type
t Type -> Type -> TypeEqn
=== FastString -> Type
mkStrLitTy (String -> FastString
mkFastString forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
take (forall (t :: * -> *) a. Foldable t => t a -> Int
length String
z forall a. Num a => a -> a -> a
- forall (t :: * -> *) a. Foldable t => t a -> Int
length String
y) String
z) ]
where
mbX :: Maybe FastString
mbX = Type -> Maybe FastString
isStrLitTy Type
s
mbY :: Maybe FastString
mbY = Type -> Maybe FastString
isStrLitTy Type
t
mbZ :: Maybe FastString
mbZ = Type -> Maybe FastString
isStrLitTy Type
r
interactTopAppendSymbol [Type]
_ Type
_ = []
interactTopConsSymbol :: [Xi] -> Xi -> [Pair Type]
interactTopConsSymbol :: [Type] -> Type -> [TypeEqn]
interactTopConsSymbol [Type
s,Type
t] Type
r
| Just FastString
fs <- Type -> Maybe FastString
isStrLitTy Type
r
, Just (Char
x, FastString
xs) <- FastString -> Maybe (Char, FastString)
unconsFS FastString
fs =
[ Type
s Type -> Type -> TypeEqn
=== Char -> Type
mkCharLitTy Char
x, Type
t Type -> Type -> TypeEqn
=== FastString -> Type
mkStrLitTy FastString
xs ]
interactTopConsSymbol [Type]
_ Type
_ = []
interactTopUnconsSymbol :: [Xi] -> Xi -> [Pair Type]
interactTopUnconsSymbol :: [Type] -> Type -> [TypeEqn]
interactTopUnconsSymbol [Type
s] Type
r
| Just Maybe Type
Nothing <- Maybe (Maybe Type)
mbX =
[ Type
s Type -> Type -> TypeEqn
=== FastString -> Type
mkStrLitTy FastString
nilFS ]
| Just (Just Type
r) <- Maybe (Maybe Type)
mbX
, Just (Type
c, Type
str) <- Type -> Maybe (Type, Type)
isPromotedPairType Type
r
, Just Char
chr <- Type -> Maybe Char
isCharLitTy Type
c
, Just FastString
str1 <- Type -> Maybe FastString
isStrLitTy Type
str =
[ Type
s Type -> Type -> TypeEqn
=== (FastString -> Type
mkStrLitTy forall a b. (a -> b) -> a -> b
$ Char -> FastString -> FastString
consFS Char
chr FastString
str1) ]
where
mbX :: Maybe (Maybe Type)
mbX = Type -> Maybe (Maybe Type)
isPromotedMaybeTy Type
r
interactTopUnconsSymbol [Type]
_ Type
_ = []
interactTopCharToNat :: [Xi] -> Xi -> [Pair Type]
interactTopCharToNat :: [Type] -> Type -> [TypeEqn]
interactTopCharToNat [Type
s] Type
r
| Just Integer
n <- Type -> Maybe Integer
isNumLitTy Type
r
, Just Char
c <- Integer -> Maybe Char
integerToChar Integer
n
= [ Type
s Type -> Type -> TypeEqn
=== Char -> Type
mkCharLitTy Char
c ]
interactTopCharToNat [Type]
_ Type
_ = []
interactTopNatToChar :: [Xi] -> Xi -> [Pair Type]
interactTopNatToChar :: [Type] -> Type -> [TypeEqn]
interactTopNatToChar [Type
s] Type
r
| Just Char
c <- Type -> Maybe Char
isCharLitTy Type
r
= [ Type
s Type -> Type -> TypeEqn
=== Integer -> Type
mkNumLitTy (Char -> Integer
charToInteger Char
c) ]
interactTopNatToChar [Type]
_ Type
_ = []
interactInertAdd :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
interactInertAdd :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertAdd [Type
x1,Type
y1] Type
z1 [Type
x2,Type
y2] Type
z2
| Bool
sameZ Bool -> Bool -> Bool
&& HasDebugCallStack => Type -> Type -> Bool
tcEqType Type
x1 Type
x2 = [ Type
y1 Type -> Type -> TypeEqn
=== Type
y2 ]
| Bool
sameZ Bool -> Bool -> Bool
&& HasDebugCallStack => Type -> Type -> Bool
tcEqType Type
y1 Type
y2 = [ Type
x1 Type -> Type -> TypeEqn
=== Type
x2 ]
where sameZ :: Bool
sameZ = HasDebugCallStack => Type -> Type -> Bool
tcEqType Type
z1 Type
z2
interactInertAdd [Type]
_ Type
_ [Type]
_ Type
_ = []
interactInertSub :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
interactInertSub :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertSub [Type
x1,Type
y1] Type
z1 [Type
x2,Type
y2] Type
z2
| Bool
sameZ Bool -> Bool -> Bool
&& HasDebugCallStack => Type -> Type -> Bool
tcEqType Type
x1 Type
x2 = [ Type
y1 Type -> Type -> TypeEqn
=== Type
y2 ]
| Bool
sameZ Bool -> Bool -> Bool
&& HasDebugCallStack => Type -> Type -> Bool
tcEqType Type
y1 Type
y2 = [ Type
x1 Type -> Type -> TypeEqn
=== Type
x2 ]
where sameZ :: Bool
sameZ = HasDebugCallStack => Type -> Type -> Bool
tcEqType Type
z1 Type
z2
interactInertSub [Type]
_ Type
_ [Type]
_ Type
_ = []
interactInertMul :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
interactInertMul :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertMul [Type
x1,Type
y1] Type
z1 [Type
x2,Type
y2] Type
z2
| Bool
sameZ Bool -> Bool -> Bool
&& (Integer -> Bool) -> Type -> Bool
known (forall a. Eq a => a -> a -> Bool
/= Integer
0) Type
x1 Bool -> Bool -> Bool
&& HasDebugCallStack => Type -> Type -> Bool
tcEqType Type
x1 Type
x2 = [ Type
y1 Type -> Type -> TypeEqn
=== Type
y2 ]
| Bool
sameZ Bool -> Bool -> Bool
&& (Integer -> Bool) -> Type -> Bool
known (forall a. Eq a => a -> a -> Bool
/= Integer
0) Type
y1 Bool -> Bool -> Bool
&& HasDebugCallStack => Type -> Type -> Bool
tcEqType Type
y1 Type
y2 = [ Type
x1 Type -> Type -> TypeEqn
=== Type
x2 ]
where sameZ :: Bool
sameZ = HasDebugCallStack => Type -> Type -> Bool
tcEqType Type
z1 Type
z2
interactInertMul [Type]
_ Type
_ [Type]
_ Type
_ = []
interactInertDiv :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
interactInertDiv :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertDiv [Type]
_ Type
_ [Type]
_ Type
_ = []
interactInertMod :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
interactInertMod :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertMod [Type]
_ Type
_ [Type]
_ Type
_ = []
interactInertExp :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
interactInertExp :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertExp [Type
x1,Type
y1] Type
z1 [Type
x2,Type
y2] Type
z2
| Bool
sameZ Bool -> Bool -> Bool
&& (Integer -> Bool) -> Type -> Bool
known (forall a. Ord a => a -> a -> Bool
> Integer
1) Type
x1 Bool -> Bool -> Bool
&& HasDebugCallStack => Type -> Type -> Bool
tcEqType Type
x1 Type
x2 = [ Type
y1 Type -> Type -> TypeEqn
=== Type
y2 ]
| Bool
sameZ Bool -> Bool -> Bool
&& (Integer -> Bool) -> Type -> Bool
known (forall a. Ord a => a -> a -> Bool
> Integer
0) Type
y1 Bool -> Bool -> Bool
&& HasDebugCallStack => Type -> Type -> Bool
tcEqType Type
y1 Type
y2 = [ Type
x1 Type -> Type -> TypeEqn
=== Type
x2 ]
where sameZ :: Bool
sameZ = HasDebugCallStack => Type -> Type -> Bool
tcEqType Type
z1 Type
z2
interactInertExp [Type]
_ Type
_ [Type]
_ Type
_ = []
interactInertLog :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
interactInertLog :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertLog [Type]
_ Type
_ [Type]
_ Type
_ = []
interactInertAppendSymbol :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
interactInertAppendSymbol :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertAppendSymbol [Type
x1,Type
y1] Type
z1 [Type
x2,Type
y2] Type
z2
| Bool
sameZ Bool -> Bool -> Bool
&& HasDebugCallStack => Type -> Type -> Bool
tcEqType Type
x1 Type
x2 = [ Type
y1 Type -> Type -> TypeEqn
=== Type
y2 ]
| Bool
sameZ Bool -> Bool -> Bool
&& HasDebugCallStack => Type -> Type -> Bool
tcEqType Type
y1 Type
y2 = [ Type
x1 Type -> Type -> TypeEqn
=== Type
x2 ]
where sameZ :: Bool
sameZ = HasDebugCallStack => Type -> Type -> Bool
tcEqType Type
z1 Type
z2
interactInertAppendSymbol [Type]
_ Type
_ [Type]
_ Type
_ = []
interactInertConsSymbol :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
interactInertConsSymbol :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertConsSymbol [Type
x1, Type
y1] Type
z1 [Type
x2, Type
y2] Type
z2
| Bool
sameZ = [ Type
x1 Type -> Type -> TypeEqn
=== Type
x2, Type
y1 Type -> Type -> TypeEqn
=== Type
y2 ]
where sameZ :: Bool
sameZ = HasDebugCallStack => Type -> Type -> Bool
tcEqType Type
z1 Type
z2
interactInertConsSymbol [Type]
_ Type
_ [Type]
_ Type
_ = []
interactInertUnconsSymbol :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
interactInertUnconsSymbol :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertUnconsSymbol [Type
x1] Type
z1 [Type
x2] Type
z2
| HasDebugCallStack => Type -> Type -> Bool
tcEqType Type
z1 Type
z2 = [ Type
x1 Type -> Type -> TypeEqn
=== Type
x2 ]
interactInertUnconsSymbol [Type]
_ Type
_ [Type]
_ Type
_ = []
minus :: Integer -> Integer -> Maybe Integer
minus :: Integer -> Integer -> Maybe Integer
minus Integer
x Integer
y = if Integer
x forall a. Ord a => a -> a -> Bool
>= Integer
y then forall a. a -> Maybe a
Just (Integer
x forall a. Num a => a -> a -> a
- Integer
y) else forall a. Maybe a
Nothing
logExact :: Integer -> Integer -> Maybe Integer
logExact :: Integer -> Integer -> Maybe Integer
logExact Integer
x Integer
y = do (Integer
z,Bool
True) <- Integer -> Integer -> Maybe (Integer, Bool)
genLog Integer
x Integer
y
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
z
divide :: Integer -> Integer -> Maybe Integer
divide :: Integer -> Integer -> Maybe Integer
divide Integer
_ Integer
0 = forall a. Maybe a
Nothing
divide Integer
x Integer
y = case forall a. Integral a => a -> a -> (a, a)
divMod Integer
x Integer
y of
(Integer
a,Integer
0) -> forall a. a -> Maybe a
Just Integer
a
(Integer, Integer)
_ -> forall a. Maybe a
Nothing
rootExact :: Integer -> Integer -> Maybe Integer
rootExact :: Integer -> Integer -> Maybe Integer
rootExact Integer
x Integer
y = do (Integer
z,Bool
True) <- Integer -> Integer -> Maybe (Integer, Bool)
genRoot Integer
x Integer
y
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
z
genRoot :: Integer -> Integer -> Maybe (Integer, Bool)
genRoot :: Integer -> Integer -> Maybe (Integer, Bool)
genRoot Integer
_ Integer
0 = forall a. Maybe a
Nothing
genRoot Integer
x0 Integer
1 = forall a. a -> Maybe a
Just (Integer
x0, Bool
True)
genRoot Integer
x0 Integer
root = forall a. a -> Maybe a
Just (Integer -> Integer -> (Integer, Bool)
search Integer
0 (Integer
x0forall a. Num a => a -> a -> a
+Integer
1))
where
search :: Integer -> Integer -> (Integer, Bool)
search Integer
from Integer
to = let x :: Integer
x = Integer
from forall a. Num a => a -> a -> a
+ forall a. Integral a => a -> a -> a
div (Integer
to forall a. Num a => a -> a -> a
- Integer
from) Integer
2
a :: Integer
a = Integer
x forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
root
in case forall a. Ord a => a -> a -> Ordering
compare Integer
a Integer
x0 of
Ordering
EQ -> (Integer
x, Bool
True)
Ordering
LT | Integer
x forall a. Eq a => a -> a -> Bool
/= Integer
from -> Integer -> Integer -> (Integer, Bool)
search Integer
x Integer
to
| Bool
otherwise -> (Integer
from, Bool
False)
Ordering
GT | Integer
x forall a. Eq a => a -> a -> Bool
/= Integer
to -> Integer -> Integer -> (Integer, Bool)
search Integer
from Integer
x
| Bool
otherwise -> (Integer
from, Bool
False)
genLog :: Integer -> Integer -> Maybe (Integer, Bool)
genLog :: Integer -> Integer -> Maybe (Integer, Bool)
genLog Integer
x Integer
0 = if Integer
x forall a. Eq a => a -> a -> Bool
== Integer
1 then forall a. a -> Maybe a
Just (Integer
0, Bool
True) else forall a. Maybe a
Nothing
genLog Integer
_ Integer
1 = forall a. Maybe a
Nothing
genLog Integer
0 Integer
_ = forall a. Maybe a
Nothing
genLog Integer
x Integer
base = forall a. a -> Maybe a
Just (Integer -> Integer -> (Integer, Bool)
exactLoop Integer
0 Integer
x)
where
exactLoop :: Integer -> Integer -> (Integer, Bool)
exactLoop Integer
s Integer
i
| Integer
i forall a. Eq a => a -> a -> Bool
== Integer
1 = (Integer
s,Bool
True)
| Integer
i forall a. Ord a => a -> a -> Bool
< Integer
base = (Integer
s,Bool
False)
| Bool
otherwise =
let s1 :: Integer
s1 = Integer
s forall a. Num a => a -> a -> a
+ Integer
1
in Integer
s1 seq :: forall a b. a -> b -> b
`seq` case forall a. Integral a => a -> a -> (a, a)
divMod Integer
i Integer
base of
(Integer
j,Integer
r)
| Integer
r forall a. Eq a => a -> a -> Bool
== Integer
0 -> Integer -> Integer -> (Integer, Bool)
exactLoop Integer
s1 Integer
j
| Bool
otherwise -> (Integer -> Integer -> Integer
underLoop Integer
s1 Integer
j, Bool
False)
underLoop :: Integer -> Integer -> Integer
underLoop Integer
s Integer
i
| Integer
i forall a. Ord a => a -> a -> Bool
< Integer
base = Integer
s
| Bool
otherwise = let s1 :: Integer
s1 = Integer
s forall a. Num a => a -> a -> a
+ Integer
1 in Integer
s1 seq :: forall a b. a -> b -> b
`seq` Integer -> Integer -> Integer
underLoop Integer
s1 (forall a. Integral a => a -> a -> a
div Integer
i Integer
base)
typeCharCmpTyCon :: TyCon
typeCharCmpTyCon :: TyCon
typeCharCmpTyCon =
Name
-> [TyConBinder]
-> Type
-> Maybe Name
-> FamTyConFlav
-> Maybe Class
-> Injectivity
-> TyCon
mkFamilyTyCon Name
name
([Type] -> [TyConBinder]
mkTemplateAnonTyConBinders [ Type
charTy, Type
charTy ])
Type
orderingKind
forall a. Maybe a
Nothing
(BuiltInSynFamily -> FamTyConFlav
BuiltInSynFamTyCon BuiltInSynFamily
ops)
forall a. Maybe a
Nothing
Injectivity
NotInjective
where
name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_TYPELITS_INTERNAL (String -> FastString
fsLit String
"CmpChar")
Unique
typeCharCmpTyFamNameKey TyCon
typeCharCmpTyCon
ops :: BuiltInSynFamily
ops = BuiltInSynFamily
{ sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
sfMatchFam = [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamCmpChar
, sfInteractTop :: [Type] -> Type -> [TypeEqn]
sfInteractTop = [Type] -> Type -> [TypeEqn]
interactTopCmpChar
, sfInteractInert :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
sfInteractInert = \[Type]
_ Type
_ [Type]
_ Type
_ -> []
}
interactTopCmpChar :: [Xi] -> Xi -> [Pair Type]
interactTopCmpChar :: [Type] -> Type -> [TypeEqn]
interactTopCmpChar [Type
s,Type
t] Type
r
| Just Ordering
EQ <- Type -> Maybe Ordering
isOrderingLitTy Type
r = [ Type
s Type -> Type -> TypeEqn
=== Type
t ]
interactTopCmpChar [Type]
_ Type
_ = []
cmpChar :: Type -> Type -> Type
cmpChar :: Type -> Type -> Type
cmpChar Type
s Type
t = TyCon -> [Type] -> Type
mkTyConApp TyCon
typeCharCmpTyCon [Type
s,Type
t]
axCmpCharDef, axCmpCharRefl :: CoAxiomRule
axCmpCharDef :: CoAxiomRule
axCmpCharDef =
forall a b.
String
-> TyCon
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> CoAxiomRule
mkBinAxiom String
"CmpCharDef" TyCon
typeCharCmpTyCon Type -> Maybe Char
isCharLitTy Type -> Maybe Char
isCharLitTy forall a b. (a -> b) -> a -> b
$
\Char
chr1 Char
chr2 -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Ordering -> Type
ordering forall a b. (a -> b) -> a -> b
$ forall a. Ord a => a -> a -> Ordering
compare Char
chr1 Char
chr2
axCmpCharRefl :: CoAxiomRule
axCmpCharRefl = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 String
"CmpCharRefl"
forall a b. (a -> b) -> a -> b
$ \(Pair Type
s Type
_) -> (Type -> Type -> Type
cmpChar Type
s Type
s) Type -> Type -> TypeEqn
=== Ordering -> Type
ordering Ordering
EQ
matchFamCmpChar :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamCmpChar :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamCmpChar [Type
s,Type
t]
| Just Char
x <- Maybe Char
mbX, Just Char
y <- Maybe Char
mbY =
forall a. a -> Maybe a
Just (CoAxiomRule
axCmpCharDef, [Type
s,Type
t], Ordering -> Type
ordering (forall a. Ord a => a -> a -> Ordering
compare Char
x Char
y))
| HasDebugCallStack => Type -> Type -> Bool
tcEqType Type
s Type
t = forall a. a -> Maybe a
Just (CoAxiomRule
axCmpCharRefl, [Type
s], Ordering -> Type
ordering Ordering
EQ)
where mbX :: Maybe Char
mbX = Type -> Maybe Char
isCharLitTy Type
s
mbY :: Maybe Char
mbY = Type -> Maybe Char
isCharLitTy Type
t
matchFamCmpChar [Type]
_ = forall a. Maybe a
Nothing