{-# LANGUAGE LambdaCase #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
module GHC.Builtin.Types.Literals
( tryInteractInertFam, tryInteractTopFam, tryMatchFam
, 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.Core.Unify ( tcMatchTys )
import GHC.Data.Pair
import GHC.Core.TyCon ( TyCon, FamTyConFlav(..), mkFamilyTyCon, tyConArity
, Injectivity(..), isBuiltInSynFamTyCon_maybe )
import GHC.Core.Coercion.Axiom
import GHC.Core.TyCo.Compare ( tcEqType )
import GHC.Types.Name ( Name, BuiltInSyntax(..) )
import GHC.Types.Unique.FM
import GHC.Builtin.Types
import GHC.Builtin.Types.Prim ( mkTemplateAnonTyConBinders, mkTemplateTyVars )
import GHC.Builtin.Names
( gHC_INTERNAL_TYPELITS
, gHC_INTERNAL_TYPELITS_INTERNAL
, gHC_INTERNAL_TYPENATS
, gHC_INTERNAL_TYPENATS_INTERNAL
, typeNatAddTyFamNameKey
, typeNatMulTyFamNameKey
, typeNatExpTyFamNameKey
, typeNatSubTyFamNameKey
, typeNatDivTyFamNameKey
, typeNatModTyFamNameKey
, typeNatLogTyFamNameKey
, typeNatCmpTyFamNameKey
, typeSymbolCmpTyFamNameKey
, typeSymbolAppendFamNameKey
, typeCharCmpTyFamNameKey
, typeConsSymbolTyFamNameKey
, typeUnconsSymbolTyFamNameKey
, typeCharToNatTyFamNameKey
, typeNatToCharTyFamNameKey
)
import GHC.Data.FastString
import GHC.Utils.Panic
import GHC.Utils.Outputable
import Control.Monad ( guard )
import Data.List ( isPrefixOf, isSuffixOf )
import Data.Maybe ( listToMaybe )
import qualified Data.Char as Char
tryInteractTopFam :: BuiltInSynFamily -> TyCon -> [Type] -> Type
-> [(CoAxiomRule, TypeEqn)]
tryInteractTopFam :: BuiltInSynFamily
-> TyCon -> [Type] -> Type -> [(CoAxiomRule, TypeEqn)]
tryInteractTopFam BuiltInSynFamily
fam TyCon
fam_tc [Type]
tys Type
r
= [(BuiltInFamInjectivity -> CoAxiomRule
bifinj_axr BuiltInFamInjectivity
bif, TypeEqn
eqn_out) | BuiltInFamInjectivity
bif <- BuiltInSynFamily -> [BuiltInFamInjectivity]
sfInteract BuiltInSynFamily
fam
, Just TypeEqn
eqn_out <- [BuiltInFamInjectivity -> TypeEqn -> Maybe TypeEqn
bifinj_proves BuiltInFamInjectivity
bif TypeEqn
eqn_in] ]
where
eqn_in :: TypeEqn
eqn_in :: TypeEqn
eqn_in = Type -> Type -> TypeEqn
forall a. a -> a -> Pair a
Pair (TyCon -> [Type] -> Type
mkTyConApp TyCon
fam_tc [Type]
tys) Type
r
tryInteractInertFam :: BuiltInSynFamily -> TyCon
-> [Type] -> [Type]
-> [(CoAxiomRule, TypeEqn)]
tryInteractInertFam :: BuiltInSynFamily
-> TyCon -> [Type] -> [Type] -> [(CoAxiomRule, TypeEqn)]
tryInteractInertFam BuiltInSynFamily
builtin_fam TyCon
fam_tc [Type]
tys1 [Type]
tys2
= [(BuiltInFamInjectivity -> CoAxiomRule
bifinj_axr BuiltInFamInjectivity
bif, TypeEqn
eqn_out) | BuiltInFamInjectivity
bif <- BuiltInSynFamily -> [BuiltInFamInjectivity]
sfInteract BuiltInSynFamily
builtin_fam
, Just TypeEqn
eqn_out <- [BuiltInFamInjectivity -> TypeEqn -> Maybe TypeEqn
bifinj_proves BuiltInFamInjectivity
bif TypeEqn
eqn_in] ]
where
eqn_in :: TypeEqn
eqn_in = Type -> Type -> TypeEqn
forall a. a -> a -> Pair a
Pair (TyCon -> [Type] -> Type
mkTyConApp TyCon
fam_tc [Type]
tys1) (TyCon -> [Type] -> Type
mkTyConApp TyCon
fam_tc [Type]
tys2)
tryMatchFam :: BuiltInSynFamily -> [Type]
-> Maybe (CoAxiomRule, [Type], Type)
tryMatchFam :: BuiltInSynFamily -> [Type] -> Maybe (CoAxiomRule, [Type], Type)
tryMatchFam BuiltInSynFamily
builtin_fam [Type]
arg_tys
= [(CoAxiomRule, [Type], Type)] -> Maybe (CoAxiomRule, [Type], Type)
forall a. [a] -> Maybe a
listToMaybe ([(CoAxiomRule, [Type], Type)]
-> Maybe (CoAxiomRule, [Type], Type))
-> [(CoAxiomRule, [Type], Type)]
-> Maybe (CoAxiomRule, [Type], Type)
forall a b. (a -> b) -> a -> b
$
[ (BuiltInFamRewrite -> CoAxiomRule
bifrw_axr BuiltInFamRewrite
rw_ax, [Type]
inst_tys, Type
res_ty)
| BuiltInFamRewrite
rw_ax <- BuiltInSynFamily -> [BuiltInFamRewrite]
sfMatchFam BuiltInSynFamily
builtin_fam
, Just ([Type]
inst_tys,Type
res_ty) <- [BuiltInFamRewrite -> [Type] -> Maybe ([Type], Type)
bifrw_match BuiltInFamRewrite
rw_ax [Type]
arg_tys] ]
mkUnaryConstFoldAxiom :: TyCon -> String
-> (Type -> Maybe a)
-> (a -> Maybe Type)
-> BuiltInFamRewrite
{-# INLINE mkUnaryConstFoldAxiom #-}
mkUnaryConstFoldAxiom :: forall a.
TyCon
-> String
-> (Type -> Maybe a)
-> (a -> Maybe Type)
-> BuiltInFamRewrite
mkUnaryConstFoldAxiom TyCon
fam_tc String
str Type -> Maybe a
isReqTy a -> Maybe Type
f
= BuiltInFamRewrite
bif
where
bif :: BuiltInFamRewrite
bif = BIF_Rewrite
{ bifrw_name :: FastString
bifrw_name = String -> FastString
fsLit String
str
, bifrw_axr :: CoAxiomRule
bifrw_axr = BuiltInFamRewrite -> CoAxiomRule
BuiltInFamRew BuiltInFamRewrite
bif
, bifrw_fam_tc :: TyCon
bifrw_fam_tc = TyCon
fam_tc
, bifrw_arity :: Int
bifrw_arity = Int
1
, bifrw_match :: [Type] -> Maybe ([Type], Type)
bifrw_match = \[Type]
ts -> do { [t1] <- [Type] -> Maybe [Type]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return [Type]
ts
; t1' <- isReqTy t1
; res <- f t1'
; return ([t1], res) }
, bifrw_proves :: [TypeEqn] -> Maybe TypeEqn
bifrw_proves = \[TypeEqn]
cs -> do { [Pair s1 s2] <- [TypeEqn] -> Maybe [TypeEqn]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return [TypeEqn]
cs
; s2' <- isReqTy s2
; z <- f s2'
; return (mkTyConApp fam_tc [s1] === z) }
}
mkBinConstFoldAxiom :: TyCon -> String
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> BuiltInFamRewrite
{-# INLINE mkBinConstFoldAxiom #-}
mkBinConstFoldAxiom :: forall a b.
TyCon
-> String
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> BuiltInFamRewrite
mkBinConstFoldAxiom TyCon
fam_tc String
str Type -> Maybe a
isReqTy1 Type -> Maybe b
isReqTy2 a -> b -> Maybe Type
f
= BuiltInFamRewrite
bif
where
bif :: BuiltInFamRewrite
bif = BIF_Rewrite
{ bifrw_name :: FastString
bifrw_name = String -> FastString
fsLit String
str
, bifrw_axr :: CoAxiomRule
bifrw_axr = BuiltInFamRewrite -> CoAxiomRule
BuiltInFamRew BuiltInFamRewrite
bif
, bifrw_fam_tc :: TyCon
bifrw_fam_tc = TyCon
fam_tc
, bifrw_arity :: Int
bifrw_arity = Int
2
, bifrw_match :: [Type] -> Maybe ([Type], Type)
bifrw_match = \[Type]
ts -> do { [t1,t2] <- [Type] -> Maybe [Type]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return [Type]
ts
; t1' <- isReqTy1 t1
; t2' <- isReqTy2 t2
; res <- f t1' t2'
; return ([t1,t2], res) }
, bifrw_proves :: [TypeEqn] -> Maybe TypeEqn
bifrw_proves = \[TypeEqn]
cs -> do { [Pair s1 s2, Pair t1 t2] <- [TypeEqn] -> Maybe [TypeEqn]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return [TypeEqn]
cs
; s2' <- isReqTy1 s2
; t2' <- isReqTy2 t2
; z <- f s2' t2'
; return (mkTyConApp fam_tc [s1,t1] === z) }
}
mkRewriteAxiom :: TyCon -> String
-> [TyVar] -> [Type]
-> Type
-> BuiltInFamRewrite
mkRewriteAxiom :: TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
mkRewriteAxiom TyCon
fam_tc String
str [TyVar]
tpl_tvs [Type]
lhs_tys Type
rhs_ty
= Bool -> SDoc -> BuiltInFamRewrite -> BuiltInFamRewrite
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (TyCon -> Int
tyConArity TyCon
fam_tc Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
lhs_tys) (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
str SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
lhs_tys) (BuiltInFamRewrite -> BuiltInFamRewrite)
-> BuiltInFamRewrite -> BuiltInFamRewrite
forall a b. (a -> b) -> a -> b
$
BuiltInFamRewrite
bif
where
bif :: BuiltInFamRewrite
bif = BIF_Rewrite
{ bifrw_name :: FastString
bifrw_name = String -> FastString
fsLit String
str
, bifrw_axr :: CoAxiomRule
bifrw_axr = BuiltInFamRewrite -> CoAxiomRule
BuiltInFamRew BuiltInFamRewrite
bif
, bifrw_fam_tc :: TyCon
bifrw_fam_tc = TyCon
fam_tc
, bifrw_arity :: Int
bifrw_arity = Int
bif_arity
, bifrw_match :: [Type] -> Maybe ([Type], Type)
bifrw_match = [Type] -> Maybe ([Type], Type)
match_fn
, bifrw_proves :: [TypeEqn] -> Maybe TypeEqn
bifrw_proves = [TypeEqn] -> Maybe TypeEqn
inst_fn }
bif_arity :: Int
bif_arity = [TyVar] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TyVar]
tpl_tvs
match_fn :: [Type] -> Maybe ([Type],Type)
match_fn :: [Type] -> Maybe ([Type], Type)
match_fn [Type]
arg_tys
= Bool -> SDoc -> Maybe ([Type], Type) -> Maybe ([Type], Type)
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (TyCon -> Int
tyConArity TyCon
fam_tc Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
arg_tys) (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
str SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
arg_tys) (Maybe ([Type], Type) -> Maybe ([Type], Type))
-> Maybe ([Type], Type) -> Maybe ([Type], Type)
forall a b. (a -> b) -> a -> b
$
case [Type] -> [Type] -> Maybe Subst
tcMatchTys [Type]
lhs_tys [Type]
arg_tys of
Maybe Subst
Nothing -> Maybe ([Type], Type)
forall a. Maybe a
Nothing
Just Subst
subst -> ([Type], Type) -> Maybe ([Type], Type)
forall a. a -> Maybe a
Just (Subst -> [TyVar] -> [Type]
substTyVars Subst
subst [TyVar]
tpl_tvs, HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst Type
rhs_ty)
inst_fn :: [TypeEqn] -> Maybe TypeEqn
inst_fn :: [TypeEqn] -> Maybe TypeEqn
inst_fn [TypeEqn]
inst_eqns
= Bool -> SDoc -> Maybe TypeEqn -> Maybe TypeEqn
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr ([TypeEqn] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeEqn]
inst_eqns Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
bif_arity) (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
str SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [TypeEqn] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TypeEqn]
inst_eqns) (Maybe TypeEqn -> Maybe TypeEqn) -> Maybe TypeEqn -> Maybe TypeEqn
forall a b. (a -> b) -> a -> b
$
TypeEqn -> Maybe TypeEqn
forall a. a -> Maybe a
Just (TyCon -> [Type] -> Type
mkTyConApp TyCon
fam_tc (HasDebugCallStack => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
substTys ([TyVar] -> [Type] -> Subst
HasDebugCallStack => [TyVar] -> [Type] -> Subst
zipTCvSubst [TyVar]
tpl_tvs [Type]
tys1) [Type]
lhs_tys)
Type -> Type -> TypeEqn
===
HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy ([TyVar] -> [Type] -> Subst
HasDebugCallStack => [TyVar] -> [Type] -> Subst
zipTCvSubst [TyVar]
tpl_tvs [Type]
tys2) Type
rhs_ty)
where
([Type]
tys1, [Type]
tys2) = [TypeEqn] -> ([Type], [Type])
forall a. [Pair a] -> ([a], [a])
unzipPairs [TypeEqn]
inst_eqns
mkTopUnaryFamDeduction :: String -> TyCon
-> (Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
{-# INLINE mkTopUnaryFamDeduction #-}
mkTopUnaryFamDeduction :: String
-> TyCon
-> (Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopUnaryFamDeduction String
str TyCon
fam_tc Type -> Type -> Maybe TypeEqn
f
= BuiltInFamInjectivity
bif
where
bif :: BuiltInFamInjectivity
bif = BIF_Interact
{ bifinj_name :: FastString
bifinj_name = String -> FastString
fsLit String
str
, bifinj_axr :: CoAxiomRule
bifinj_axr = BuiltInFamInjectivity -> CoAxiomRule
BuiltInFamInj BuiltInFamInjectivity
bif
, bifinj_proves :: TypeEqn -> Maybe TypeEqn
bifinj_proves = \(Pair Type
lhs Type
rhs)
-> do { (tc, [a]) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
lhs
; massertPpr (tc == fam_tc) (ppr tc $$ ppr fam_tc)
; f a rhs } }
mkTopBinFamDeduction :: String -> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
{-# INLINE mkTopBinFamDeduction #-}
mkTopBinFamDeduction :: String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
str TyCon
fam_tc Type -> Type -> Type -> Maybe TypeEqn
f
= BuiltInFamInjectivity
bif
where
bif :: BuiltInFamInjectivity
bif = BIF_Interact
{ bifinj_name :: FastString
bifinj_name = String -> FastString
fsLit String
str
, bifinj_axr :: CoAxiomRule
bifinj_axr = BuiltInFamInjectivity -> CoAxiomRule
BuiltInFamInj BuiltInFamInjectivity
bif
, bifinj_proves :: TypeEqn -> Maybe TypeEqn
bifinj_proves = \(Pair Type
lhs Type
rhs) ->
do { (tc, [a,b]) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
lhs
; massertPpr (tc == fam_tc) (ppr tc $$ ppr fam_tc)
; f a b rhs } }
mkUnaryBIF :: String -> TyCon -> BuiltInFamInjectivity
mkUnaryBIF :: String -> TyCon -> BuiltInFamInjectivity
mkUnaryBIF String
str TyCon
fam_tc
= BuiltInFamInjectivity
bif
where
bif :: BuiltInFamInjectivity
bif = BIF_Interact { bifinj_name :: FastString
bifinj_name = String -> FastString
fsLit String
str
, bifinj_axr :: CoAxiomRule
bifinj_axr = BuiltInFamInjectivity -> CoAxiomRule
BuiltInFamInj BuiltInFamInjectivity
bif
, bifinj_proves :: TypeEqn -> Maybe TypeEqn
bifinj_proves = TypeEqn -> Maybe TypeEqn
proves }
proves :: TypeEqn -> Maybe TypeEqn
proves (Pair Type
lhs Type
rhs)
= do { (tc2, [x2]) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
rhs
; guard (tc2 == fam_tc)
; (tc1, [x1]) <- splitTyConApp_maybe lhs
; massertPpr (tc1 == fam_tc) (ppr tc1 $$ ppr fam_tc)
; return (Pair x1 x2) }
mkBinBIF :: String -> TyCon
-> WhichArg -> WhichArg
-> (Type -> Bool)
-> BuiltInFamInjectivity
{-# INLINE mkBinBIF #-}
mkBinBIF :: String
-> TyCon
-> WhichArg
-> WhichArg
-> (Type -> Bool)
-> BuiltInFamInjectivity
mkBinBIF String
str TyCon
fam_tc WhichArg
eq1 WhichArg
eq2 Type -> Bool
check_me
= BuiltInFamInjectivity
bif
where
bif :: BuiltInFamInjectivity
bif = BIF_Interact { bifinj_name :: FastString
bifinj_name = String -> FastString
fsLit String
str
, bifinj_axr :: CoAxiomRule
bifinj_axr = BuiltInFamInjectivity -> CoAxiomRule
BuiltInFamInj BuiltInFamInjectivity
bif
, bifinj_proves :: TypeEqn -> Maybe TypeEqn
bifinj_proves = TypeEqn -> Maybe TypeEqn
proves }
proves :: TypeEqn -> Maybe TypeEqn
proves (Pair Type
lhs Type
rhs)
= do { (tc2, [x2,y2]) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
rhs
; guard (tc2 == fam_tc)
; (tc1, [x1,y1]) <- splitTyConApp_maybe lhs
; massertPpr (tc1 == fam_tc) (ppr tc1 $$ ppr fam_tc)
; case (eq1, eq2) of
(WhichArg
ArgX,WhichArg
ArgX) -> Type -> Type -> Type -> Type -> Maybe TypeEqn
do_it Type
x1 Type
x2 Type
y1 Type
y2
(WhichArg
ArgX,WhichArg
ArgY) -> Type -> Type -> Type -> Type -> Maybe TypeEqn
do_it Type
x1 Type
y2 Type
x2 Type
y1
(WhichArg
ArgY,WhichArg
ArgX) -> Type -> Type -> Type -> Type -> Maybe TypeEqn
do_it Type
y1 Type
x2 Type
y2 Type
x1
(WhichArg
ArgY,WhichArg
ArgY) -> Type -> Type -> Type -> Type -> Maybe TypeEqn
do_it Type
y1 Type
y2 Type
x1 Type
x2 }
do_it :: Type -> Type -> Type -> Type -> Maybe TypeEqn
do_it Type
a1 Type
a2 Type
b1 Type
b2 = do { Type -> Type -> Maybe ()
same Type
a1 Type
a2; Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Type -> Bool
check_me Type
a1); TypeEqn -> Maybe TypeEqn
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Type -> TypeEqn
forall a. a -> a -> Pair a
Pair Type
b1 Type
b2) }
noGuard :: Type -> Bool
noGuard :: Type -> Bool
noGuard Type
_ = Bool
True
numGuard :: (Integer -> Bool) -> Type -> Bool
numGuard :: (Integer -> Bool) -> Type -> Bool
numGuard Integer -> Bool
pred Type
ty = case Type -> Maybe Integer
isNumLitTy Type
ty of
Just Integer
n -> Integer -> Bool
pred Integer
n
Maybe Integer
Nothing -> Bool
False
data WhichArg = ArgX | ArgY
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
]
typeNatCoAxiomRules :: UniqFM FastString CoAxiomRule
typeNatCoAxiomRules :: UniqFM FastString CoAxiomRule
typeNatCoAxiomRules
= [(FastString, CoAxiomRule)] -> UniqFM FastString CoAxiomRule
forall key elt. Uniquable key => [(key, elt)] -> UniqFM key elt
listToUFM ([(FastString, CoAxiomRule)] -> UniqFM FastString CoAxiomRule)
-> [(FastString, CoAxiomRule)] -> UniqFM FastString CoAxiomRule
forall a b. (a -> b) -> a -> b
$
[ (FastString, CoAxiomRule)
pr | TyCon
tc <- [TyCon]
typeNatTyCons
, Just BuiltInSynFamily
ops <- [TyCon -> Maybe BuiltInSynFamily
isBuiltInSynFamTyCon_maybe TyCon
tc]
, (FastString, CoAxiomRule)
pr <- [ (BuiltInFamInjectivity -> FastString
bifinj_name BuiltInFamInjectivity
bif, BuiltInFamInjectivity -> CoAxiomRule
bifinj_axr BuiltInFamInjectivity
bif) | BuiltInFamInjectivity
bif <- BuiltInSynFamily -> [BuiltInFamInjectivity]
sfInteract BuiltInSynFamily
ops ]
[(FastString, CoAxiomRule)]
-> [(FastString, CoAxiomRule)] -> [(FastString, CoAxiomRule)]
forall a. [a] -> [a] -> [a]
++ [ (BuiltInFamRewrite -> FastString
bifrw_name BuiltInFamRewrite
bif, BuiltInFamRewrite -> CoAxiomRule
bifrw_axr BuiltInFamRewrite
bif) | BuiltInFamRewrite
bif <- BuiltInSynFamily -> [BuiltInFamRewrite]
sfMatchFam BuiltInSynFamily
ops ] ]
typeNatAddTyCon :: TyCon
typeNatAddTyCon :: TyCon
typeNatAddTyCon = Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon2 Name
name
BuiltInSynFamily
{ sfMatchFam :: [BuiltInFamRewrite]
sfMatchFam = [BuiltInFamRewrite]
axAddRewrites
, sfInteract :: [BuiltInFamInjectivity]
sfInteract = [BuiltInFamInjectivity]
axAddInjectivity
}
where
name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_INTERNAL_TYPENATS (String -> FastString
fsLit String
"+")
Unique
typeNatAddTyFamNameKey TyCon
typeNatAddTyCon
sn,tn :: TyVar
(TyVar
sn: TyVar
tn: [TyVar]
_) = [Type] -> [TyVar]
mkTemplateTyVars (Type -> [Type]
forall a. a -> [a]
repeat Type
typeSymbolKind)
axAddRewrites :: [BuiltInFamRewrite]
axAddRewrites :: [BuiltInFamRewrite]
axAddRewrites
= [ TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
mkRewriteAxiom TyCon
tc String
"Add0L" [TyVar
tn] [Integer -> Type
num Integer
0, TyVar -> Type
var TyVar
tn] (TyVar -> Type
var TyVar
tn)
, TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
mkRewriteAxiom TyCon
tc String
"Add0R" [TyVar
sn] [TyVar -> Type
var TyVar
sn, Integer -> Type
num Integer
0] (TyVar -> Type
var TyVar
sn)
, TyCon
-> String
-> (Type -> Maybe Integer)
-> (Type -> Maybe Integer)
-> (Integer -> Integer -> Maybe Type)
-> BuiltInFamRewrite
forall a b.
TyCon
-> String
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> BuiltInFamRewrite
mkBinConstFoldAxiom TyCon
tc String
"AddDef" Type -> Maybe Integer
isNumLitTy Type -> Maybe Integer
isNumLitTy ((Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite)
-> (Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite
forall a b. (a -> b) -> a -> b
$
\Integer
x Integer
y -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Integer -> Type
num (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
y) ]
where
tc :: TyCon
tc = TyCon
typeNatAddTyCon
axAddInjectivity :: [BuiltInFamInjectivity]
axAddInjectivity :: [BuiltInFamInjectivity]
axAddInjectivity
= [
String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"AddT-0L" TyCon
tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
a Type
_b Type
r ->
do { _ <- Type -> (Integer -> Bool) -> Maybe Integer
known Type
r (Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0); return (Pair a (num 0)) }
,
String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"AddT-0R" TyCon
tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
_a Type
b Type
r ->
do { _ <- Type -> (Integer -> Bool) -> Maybe Integer
known Type
r (Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0); return (Pair b (num 0)) }
,
String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"AddT-KKL" TyCon
tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
a Type
b Type
r ->
do { na <- Type -> Maybe Integer
isNumLitTy Type
a; nr <- known r (>= na); return (Pair b (num (nr-na))) }
,
String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"AddT-KKR" TyCon
tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
a Type
b Type
r ->
do { nb <- Type -> Maybe Integer
isNumLitTy Type
b; nr <- known r (>= nb); return (Pair a (num (nr-nb))) }
, String
-> TyCon
-> WhichArg
-> WhichArg
-> (Type -> Bool)
-> BuiltInFamInjectivity
mkBinBIF String
"AddI-xx" TyCon
tc WhichArg
ArgX WhichArg
ArgX Type -> Bool
noGuard
, String
-> TyCon
-> WhichArg
-> WhichArg
-> (Type -> Bool)
-> BuiltInFamInjectivity
mkBinBIF String
"AddI-xy" TyCon
tc WhichArg
ArgX WhichArg
ArgY Type -> Bool
noGuard
, String
-> TyCon
-> WhichArg
-> WhichArg
-> (Type -> Bool)
-> BuiltInFamInjectivity
mkBinBIF String
"AddI-yx" TyCon
tc WhichArg
ArgY WhichArg
ArgX Type -> Bool
noGuard
, String
-> TyCon
-> WhichArg
-> WhichArg
-> (Type -> Bool)
-> BuiltInFamInjectivity
mkBinBIF String
"AddI-yy" TyCon
tc WhichArg
ArgY WhichArg
ArgY Type -> Bool
noGuard
]
where
tc :: TyCon
tc = TyCon
typeNatAddTyCon
typeNatSubTyCon :: TyCon
typeNatSubTyCon :: TyCon
typeNatSubTyCon = Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon2 Name
name
BuiltInSynFamily
{ sfMatchFam :: [BuiltInFamRewrite]
sfMatchFam = [BuiltInFamRewrite]
axSubRewrites
, sfInteract :: [BuiltInFamInjectivity]
sfInteract = [BuiltInFamInjectivity]
axSubInjectivity
}
where
name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_INTERNAL_TYPENATS (String -> FastString
fsLit String
"-")
Unique
typeNatSubTyFamNameKey TyCon
typeNatSubTyCon
axSubRewrites :: [BuiltInFamRewrite]
axSubRewrites :: [BuiltInFamRewrite]
axSubRewrites
= [ TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
mkRewriteAxiom TyCon
tc String
"Sub0R" [TyVar
sn] [TyVar -> Type
var TyVar
sn, Integer -> Type
num Integer
0] (TyVar -> Type
var TyVar
sn)
, TyCon
-> String
-> (Type -> Maybe Integer)
-> (Type -> Maybe Integer)
-> (Integer -> Integer -> Maybe Type)
-> BuiltInFamRewrite
forall a b.
TyCon
-> String
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> BuiltInFamRewrite
mkBinConstFoldAxiom TyCon
tc String
"SubDef" Type -> Maybe Integer
isNumLitTy Type -> Maybe Integer
isNumLitTy ((Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite)
-> (Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite
forall a b. (a -> b) -> a -> b
$
\Integer
x Integer
y -> (Integer -> Type) -> Maybe Integer -> Maybe Type
forall a b. (a -> b) -> Maybe a -> Maybe b
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) ]
where
tc :: TyCon
tc = TyCon
typeNatSubTyCon
axSubInjectivity :: [BuiltInFamInjectivity]
axSubInjectivity :: [BuiltInFamInjectivity]
axSubInjectivity
= [
String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"SubT" TyCon
tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
a Type
b Type
r ->
do { _ <- Type -> Maybe Integer
isNumLitTy Type
r; return (Pair (r .+. b) a) }
, String
-> TyCon
-> WhichArg
-> WhichArg
-> (Type -> Bool)
-> BuiltInFamInjectivity
mkBinBIF String
"SubI-xx" TyCon
tc WhichArg
ArgX WhichArg
ArgX Type -> Bool
noGuard
, String
-> TyCon
-> WhichArg
-> WhichArg
-> (Type -> Bool)
-> BuiltInFamInjectivity
mkBinBIF String
"SubI-yy" TyCon
tc WhichArg
ArgY WhichArg
ArgY Type -> Bool
noGuard
]
where
tc :: TyCon
tc = TyCon
typeNatSubTyCon
typeNatMulTyCon :: TyCon
typeNatMulTyCon :: TyCon
typeNatMulTyCon = Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon2 Name
name
BuiltInSynFamily { sfMatchFam :: [BuiltInFamRewrite]
sfMatchFam = [BuiltInFamRewrite]
axMulRewrites
, sfInteract :: [BuiltInFamInjectivity]
sfInteract = [BuiltInFamInjectivity]
axMulInjectivity }
where
name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_INTERNAL_TYPENATS (String -> FastString
fsLit String
"*")
Unique
typeNatMulTyFamNameKey TyCon
typeNatMulTyCon
axMulRewrites :: [BuiltInFamRewrite]
axMulRewrites :: [BuiltInFamRewrite]
axMulRewrites
= [ TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
mkRewriteAxiom TyCon
tc String
"Mul0L" [TyVar
tn] [Integer -> Type
num Integer
0, TyVar -> Type
var TyVar
tn] (Integer -> Type
num Integer
0)
, TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
mkRewriteAxiom TyCon
tc String
"Mul0R" [TyVar
sn] [TyVar -> Type
var TyVar
sn, Integer -> Type
num Integer
0] (Integer -> Type
num Integer
0)
, TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
mkRewriteAxiom TyCon
tc String
"Mul1L" [TyVar
tn] [Integer -> Type
num Integer
1, TyVar -> Type
var TyVar
tn] (TyVar -> Type
var TyVar
tn)
, TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
mkRewriteAxiom TyCon
tc String
"Mul1R" [TyVar
sn] [TyVar -> Type
var TyVar
sn, Integer -> Type
num Integer
1] (TyVar -> Type
var TyVar
sn)
, TyCon
-> String
-> (Type -> Maybe Integer)
-> (Type -> Maybe Integer)
-> (Integer -> Integer -> Maybe Type)
-> BuiltInFamRewrite
forall a b.
TyCon
-> String
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> BuiltInFamRewrite
mkBinConstFoldAxiom TyCon
tc String
"MulDef" Type -> Maybe Integer
isNumLitTy Type -> Maybe Integer
isNumLitTy ((Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite)
-> (Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite
forall a b. (a -> b) -> a -> b
$
\Integer
x Integer
y -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Integer -> Type
num (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
y) ]
where
tc :: TyCon
tc = TyCon
typeNatMulTyCon
axMulInjectivity :: [BuiltInFamInjectivity]
axMulInjectivity :: [BuiltInFamInjectivity]
axMulInjectivity
= [
String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"MulT1" TyCon
tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
s Type
_t Type
r ->
do { _ <- Type -> (Integer -> Bool) -> Maybe Integer
known Type
r (Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1); return (Pair s r) }
,
String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"MulT2" TyCon
tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
_s Type
t Type
r ->
do { _ <- Type -> (Integer -> Bool) -> Maybe Integer
known Type
r (Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1); return (Pair t r) }
,
String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"MulT3" TyCon
tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
s Type
t Type
r ->
do { ns <- Type -> Maybe Integer
isNumLitTy Type
s; nr <- isNumLitTy r; y <- divide nr ns; return (Pair t (num y)) }
,
String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"MulT4" TyCon
tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
s Type
t Type
r ->
do { nt <- Type -> Maybe Integer
isNumLitTy Type
t; nr <- isNumLitTy r; y <- divide nr nt; return (Pair s (num y)) }
, String
-> TyCon
-> WhichArg
-> WhichArg
-> (Type -> Bool)
-> BuiltInFamInjectivity
mkBinBIF String
"MulI-xx" TyCon
tc WhichArg
ArgX WhichArg
ArgX ((Integer -> Bool) -> Type -> Bool
numGuard (Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0))
, String
-> TyCon
-> WhichArg
-> WhichArg
-> (Type -> Bool)
-> BuiltInFamInjectivity
mkBinBIF String
"MulI-yy" TyCon
tc WhichArg
ArgY WhichArg
ArgY ((Integer -> Bool) -> Type -> Bool
numGuard (Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0))
]
where
tc :: TyCon
tc = TyCon
typeNatMulTyCon
typeNatDivTyCon :: TyCon
typeNatDivTyCon :: TyCon
typeNatDivTyCon = Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon2 Name
name
BuiltInSynFamily { sfMatchFam :: [BuiltInFamRewrite]
sfMatchFam = [BuiltInFamRewrite]
axDivRewrites
, sfInteract :: [BuiltInFamInjectivity]
sfInteract = [] }
where
name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_INTERNAL_TYPENATS (String -> FastString
fsLit String
"Div")
Unique
typeNatDivTyFamNameKey TyCon
typeNatDivTyCon
typeNatModTyCon :: TyCon
typeNatModTyCon :: TyCon
typeNatModTyCon = Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon2 Name
name
BuiltInSynFamily { sfMatchFam :: [BuiltInFamRewrite]
sfMatchFam = [BuiltInFamRewrite]
axModRewrites
, sfInteract :: [BuiltInFamInjectivity]
sfInteract = [] }
where
name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_INTERNAL_TYPENATS (String -> FastString
fsLit String
"Mod")
Unique
typeNatModTyFamNameKey TyCon
typeNatModTyCon
axDivRewrites :: [BuiltInFamRewrite]
axDivRewrites :: [BuiltInFamRewrite]
axDivRewrites
= [ TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
mkRewriteAxiom TyCon
tc String
"Div1" [TyVar
sn] [TyVar -> Type
var TyVar
sn, Integer -> Type
num Integer
1] (TyVar -> Type
var TyVar
sn)
, TyCon
-> String
-> (Type -> Maybe Integer)
-> (Type -> Maybe Integer)
-> (Integer -> Integer -> Maybe Type)
-> BuiltInFamRewrite
forall a b.
TyCon
-> String
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> BuiltInFamRewrite
mkBinConstFoldAxiom TyCon
tc String
"DivDef" Type -> Maybe Integer
isNumLitTy Type -> Maybe Integer
isNumLitTy ((Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite)
-> (Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite
forall a b. (a -> b) -> a -> b
$
\Integer
x Integer
y -> do { Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
y Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0); Type -> Maybe Type
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Type
num (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div Integer
x Integer
y)) } ]
where
tc :: TyCon
tc = TyCon
typeNatDivTyCon
axModRewrites :: [BuiltInFamRewrite]
axModRewrites :: [BuiltInFamRewrite]
axModRewrites
= [ TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
mkRewriteAxiom TyCon
tc String
"Mod1" [TyVar
sn] [TyVar -> Type
var TyVar
sn, Integer -> Type
num Integer
1] (Integer -> Type
num Integer
0)
, TyCon
-> String
-> (Type -> Maybe Integer)
-> (Type -> Maybe Integer)
-> (Integer -> Integer -> Maybe Type)
-> BuiltInFamRewrite
forall a b.
TyCon
-> String
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> BuiltInFamRewrite
mkBinConstFoldAxiom TyCon
tc String
"ModDef" Type -> Maybe Integer
isNumLitTy Type -> Maybe Integer
isNumLitTy ((Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite)
-> (Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite
forall a b. (a -> b) -> a -> b
$
\Integer
x Integer
y -> do { Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
y Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0); Type -> Maybe Type
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Type
num (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
mod Integer
x Integer
y)) } ]
where
tc :: TyCon
tc = TyCon
typeNatModTyCon
typeNatExpTyCon :: TyCon
typeNatExpTyCon :: TyCon
typeNatExpTyCon = Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon2 Name
name
BuiltInSynFamily { sfMatchFam :: [BuiltInFamRewrite]
sfMatchFam = [BuiltInFamRewrite]
axExpRewrites
, sfInteract :: [BuiltInFamInjectivity]
sfInteract = [BuiltInFamInjectivity]
axExpInjectivity }
where
name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_INTERNAL_TYPENATS (String -> FastString
fsLit String
"^")
Unique
typeNatExpTyFamNameKey TyCon
typeNatExpTyCon
axExpRewrites :: [BuiltInFamRewrite]
axExpRewrites :: [BuiltInFamRewrite]
axExpRewrites
= [ TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
mkRewriteAxiom TyCon
tc String
"Exp0R" [TyVar
sn] [TyVar -> Type
var TyVar
sn, Integer -> Type
num Integer
0] (Integer -> Type
num Integer
1)
, TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
mkRewriteAxiom TyCon
tc String
"Exp1L" [TyVar
tn] [Integer -> Type
num Integer
1, TyVar -> Type
var TyVar
tn] (Integer -> Type
num Integer
1)
, TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
mkRewriteAxiom TyCon
tc String
"Exp1R" [TyVar
sn] [TyVar -> Type
var TyVar
sn, Integer -> Type
num Integer
1] (TyVar -> Type
var TyVar
sn)
, TyCon
-> String
-> (Type -> Maybe Integer)
-> (Type -> Maybe Integer)
-> (Integer -> Integer -> Maybe Type)
-> BuiltInFamRewrite
forall a b.
TyCon
-> String
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> BuiltInFamRewrite
mkBinConstFoldAxiom TyCon
tc String
"ExpDef" Type -> Maybe Integer
isNumLitTy Type -> Maybe Integer
isNumLitTy ((Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite)
-> (Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite
forall a b. (a -> b) -> a -> b
$
\Integer
x Integer
y -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Integer -> Type
num (Integer
x Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
y)) ]
where
tc :: TyCon
tc = TyCon
typeNatExpTyCon
axExpInjectivity :: [BuiltInFamInjectivity]
axExpInjectivity :: [BuiltInFamInjectivity]
axExpInjectivity
= [
String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"ExpT1" TyCon
tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
s Type
_t Type
r ->
do { Integer -> Maybe TypeEqn
0 <- Type -> Maybe Integer
isNumLitTy Type
r; return (Pair s r) }
,
String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"ExpT2" TyCon
tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
s Type
t Type
r ->
do { ns <- Type -> Maybe Integer
isNumLitTy Type
s; nr <- isNumLitTy r; y <- logExact nr ns; return (Pair t (num y)) }
,
String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"ExpT3" TyCon
tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
s Type
t Type
r ->
do { nt <- Type -> Maybe Integer
isNumLitTy Type
t; nr <- isNumLitTy r; y <- rootExact nr nt; return (Pair s (num y)) }
, String
-> TyCon
-> WhichArg
-> WhichArg
-> (Type -> Bool)
-> BuiltInFamInjectivity
mkBinBIF String
"ExpI-xx" TyCon
tc WhichArg
ArgX WhichArg
ArgX ((Integer -> Bool) -> Type -> Bool
numGuard (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
1))
, String
-> TyCon
-> WhichArg
-> WhichArg
-> (Type -> Bool)
-> BuiltInFamInjectivity
mkBinBIF String
"ExpI-yy" TyCon
tc WhichArg
ArgY WhichArg
ArgY ((Integer -> Bool) -> Type -> Bool
numGuard (Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0))
]
where
tc :: TyCon
tc = TyCon
typeNatExpTyCon
typeNatLogTyCon :: TyCon
typeNatLogTyCon :: TyCon
typeNatLogTyCon = Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon1 Name
name
BuiltInSynFamily { sfMatchFam :: [BuiltInFamRewrite]
sfMatchFam = [BuiltInFamRewrite]
axLogRewrites
, sfInteract :: [BuiltInFamInjectivity]
sfInteract = [] }
where
name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_INTERNAL_TYPENATS (String -> FastString
fsLit String
"Log2")
Unique
typeNatLogTyFamNameKey TyCon
typeNatLogTyCon
axLogRewrites :: [BuiltInFamRewrite]
axLogRewrites :: [BuiltInFamRewrite]
axLogRewrites
= [ TyCon
-> String
-> (Type -> Maybe Integer)
-> (Integer -> Maybe Type)
-> BuiltInFamRewrite
forall a.
TyCon
-> String
-> (Type -> Maybe a)
-> (a -> Maybe Type)
-> BuiltInFamRewrite
mkUnaryConstFoldAxiom TyCon
tc String
"LogDef" Type -> Maybe Integer
isNumLitTy ((Integer -> Maybe Type) -> BuiltInFamRewrite)
-> (Integer -> Maybe Type) -> BuiltInFamRewrite
forall a b. (a -> b) -> a -> b
$
\Integer
x -> do { (a,_) <- Integer -> Integer -> Maybe (Integer, Bool)
genLog Integer
x Integer
2; return (num a) } ]
where
tc :: TyCon
tc = 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
Maybe Name
forall a. Maybe a
Nothing
(BuiltInSynFamily -> FamTyConFlav
BuiltInSynFamTyCon BuiltInSynFamily
ops)
Maybe Class
forall a. Maybe a
Nothing
Injectivity
NotInjective
where
name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_INTERNAL_TYPENATS_INTERNAL (String -> FastString
fsLit String
"CmpNat")
Unique
typeNatCmpTyFamNameKey TyCon
typeNatCmpTyCon
ops :: BuiltInSynFamily
ops = BuiltInSynFamily { sfMatchFam :: [BuiltInFamRewrite]
sfMatchFam = [BuiltInFamRewrite]
axCmpNatRewrites
, sfInteract :: [BuiltInFamInjectivity]
sfInteract = [BuiltInFamInjectivity]
axCmpNatInjectivity }
axCmpNatRewrites :: [BuiltInFamRewrite]
axCmpNatRewrites :: [BuiltInFamRewrite]
axCmpNatRewrites
= [ TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
mkRewriteAxiom TyCon
tc String
"CmpNatRefl" [TyVar
sn] [TyVar -> Type
var TyVar
sn, TyVar -> Type
var TyVar
sn] (Ordering -> Type
ordering Ordering
EQ)
, TyCon
-> String
-> (Type -> Maybe Integer)
-> (Type -> Maybe Integer)
-> (Integer -> Integer -> Maybe Type)
-> BuiltInFamRewrite
forall a b.
TyCon
-> String
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> BuiltInFamRewrite
mkBinConstFoldAxiom TyCon
tc String
"CmpNatDef" Type -> Maybe Integer
isNumLitTy Type -> Maybe Integer
isNumLitTy ((Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite)
-> (Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite
forall a b. (a -> b) -> a -> b
$
\Integer
x Integer
y -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Ordering -> Type
ordering (Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Integer
x Integer
y)) ]
where
tc :: TyCon
tc = TyCon
typeNatCmpTyCon
axCmpNatInjectivity :: [BuiltInFamInjectivity]
axCmpNatInjectivity :: [BuiltInFamInjectivity]
axCmpNatInjectivity
= [
String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"CmpNatT3" TyCon
typeNatCmpTyCon ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
s Type
t Type
r ->
do { Ordering -> Maybe TypeEqn
EQ <- Type -> Maybe Ordering
isOrderingLitTy Type
r; return (Pair s t) } ]
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
Maybe Name
forall a. Maybe a
Nothing
(BuiltInSynFamily -> FamTyConFlav
BuiltInSynFamTyCon BuiltInSynFamily
ops)
Maybe Class
forall a. Maybe a
Nothing
Injectivity
NotInjective
where
name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_INTERNAL_TYPELITS_INTERNAL (String -> FastString
fsLit String
"CmpSymbol")
Unique
typeSymbolCmpTyFamNameKey TyCon
typeSymbolCmpTyCon
ops :: BuiltInSynFamily
ops = BuiltInSynFamily { sfMatchFam :: [BuiltInFamRewrite]
sfMatchFam = [BuiltInFamRewrite]
axSymbolCmpRewrites
, sfInteract :: [BuiltInFamInjectivity]
sfInteract = [BuiltInFamInjectivity]
axSymbolCmpInjectivity }
ss,ts :: TyVar
(TyVar
ss: TyVar
ts: [TyVar]
_) = [Type] -> [TyVar]
mkTemplateTyVars (Type -> [Type]
forall a. a -> [a]
repeat Type
typeSymbolKind)
axSymbolCmpRewrites :: [BuiltInFamRewrite]
axSymbolCmpRewrites :: [BuiltInFamRewrite]
axSymbolCmpRewrites
= [ TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
mkRewriteAxiom TyCon
tc String
"CmpSymbolRefl" [TyVar
ss] [TyVar -> Type
var TyVar
ss, TyVar -> Type
var TyVar
ss] (Ordering -> Type
ordering Ordering
EQ)
, TyCon
-> String
-> (Type -> Maybe FastString)
-> (Type -> Maybe FastString)
-> (FastString -> FastString -> Maybe Type)
-> BuiltInFamRewrite
forall a b.
TyCon
-> String
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> BuiltInFamRewrite
mkBinConstFoldAxiom TyCon
tc String
"CmpSymbolDef" Type -> Maybe FastString
isStrLitTy Type -> Maybe FastString
isStrLitTy ((FastString -> FastString -> Maybe Type) -> BuiltInFamRewrite)
-> (FastString -> FastString -> Maybe Type) -> BuiltInFamRewrite
forall a b. (a -> b) -> a -> b
$
\FastString
x FastString
y -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Ordering -> Type
ordering (FastString -> FastString -> Ordering
lexicalCompareFS FastString
x FastString
y)) ]
where
tc :: TyCon
tc = TyCon
typeSymbolCmpTyCon
axSymbolCmpInjectivity :: [BuiltInFamInjectivity]
axSymbolCmpInjectivity :: [BuiltInFamInjectivity]
axSymbolCmpInjectivity
= [ String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"CmpSymbolT" TyCon
typeSymbolCmpTyCon ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
s Type
t Type
r ->
do { Ordering -> Maybe TypeEqn
EQ <- Type -> Maybe Ordering
isOrderingLitTy Type
r; return (Pair s t) } ]
typeSymbolAppendTyCon :: TyCon
typeSymbolAppendTyCon :: TyCon
typeSymbolAppendTyCon = Name -> BuiltInSynFamily -> TyCon
mkTypeSymbolFunTyCon2 Name
name
BuiltInSynFamily { sfMatchFam :: [BuiltInFamRewrite]
sfMatchFam = [BuiltInFamRewrite]
axAppendRewrites
, sfInteract :: [BuiltInFamInjectivity]
sfInteract = [BuiltInFamInjectivity]
axAppendInjectivity }
where
name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_INTERNAL_TYPELITS (String -> FastString
fsLit String
"AppendSymbol")
Unique
typeSymbolAppendFamNameKey TyCon
typeSymbolAppendTyCon
axAppendRewrites :: [BuiltInFamRewrite]
axAppendRewrites :: [BuiltInFamRewrite]
axAppendRewrites
= [ TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
mkRewriteAxiom TyCon
tc String
"Concat0R" [TyVar
ts] [Type
nullStrLitTy, TyVar -> Type
var TyVar
ts] (TyVar -> Type
var TyVar
ts)
, TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
mkRewriteAxiom TyCon
tc String
"Concat0L" [TyVar
ss] [TyVar -> Type
var TyVar
ss, Type
nullStrLitTy] (TyVar -> Type
var TyVar
ss)
, TyCon
-> String
-> (Type -> Maybe FastString)
-> (Type -> Maybe FastString)
-> (FastString -> FastString -> Maybe Type)
-> BuiltInFamRewrite
forall a b.
TyCon
-> String
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> BuiltInFamRewrite
mkBinConstFoldAxiom TyCon
tc String
"AppendSymbolDef" Type -> Maybe FastString
isStrLitTy Type -> Maybe FastString
isStrLitTy ((FastString -> FastString -> Maybe Type) -> BuiltInFamRewrite)
-> (FastString -> FastString -> Maybe Type) -> BuiltInFamRewrite
forall a b. (a -> b) -> a -> b
$
\FastString
x FastString
y -> Type -> Maybe Type
forall a. a -> Maybe a
Just (FastString -> Type
mkStrLitTy (FastString -> FastString -> FastString
appendFS FastString
x FastString
y)) ]
where
tc :: TyCon
tc = TyCon
typeSymbolAppendTyCon
axAppendInjectivity :: [BuiltInFamInjectivity]
axAppendInjectivity :: [BuiltInFamInjectivity]
axAppendInjectivity
= [
String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"AppendSymbolT1" TyCon
tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
a Type
_b Type
r ->
do { rs <- Type -> Maybe FastString
isStrLitTy Type
r; guard (nullFS rs); return (Pair a nullStrLitTy) }
,
String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"AppendSymbolT2" TyCon
tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
_a Type
b Type
r ->
do { rs <- Type -> Maybe FastString
isStrLitTy Type
r; guard (nullFS rs); return (Pair b nullStrLitTy) }
,
String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"AppendSymbolT3" TyCon
tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
a Type
b Type
r ->
do { as <- Type -> Maybe String
isStrLitTyS Type
a; rs <- isStrLitTyS r; guard (as `isPrefixOf` rs)
; return (Pair b (mkStrLitTyS (drop (length as) rs))) }
,
String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"AppendSymbolT3" TyCon
tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
a Type
b Type
r ->
do { bs <- Type -> Maybe String
isStrLitTyS Type
b; rs <- isStrLitTyS r; guard (bs `isSuffixOf` rs)
; return (Pair a (mkStrLitTyS (take (length rs - length bs) rs))) }
, String
-> TyCon
-> WhichArg
-> WhichArg
-> (Type -> Bool)
-> BuiltInFamInjectivity
mkBinBIF String
"AppI-xx" TyCon
tc WhichArg
ArgX WhichArg
ArgX Type -> Bool
noGuard
, String
-> TyCon
-> WhichArg
-> WhichArg
-> (Type -> Bool)
-> BuiltInFamInjectivity
mkBinBIF String
"AppI-yy" TyCon
tc WhichArg
ArgY WhichArg
ArgY Type -> Bool
noGuard
]
where
tc :: TyCon
tc = 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
Maybe Name
forall a. Maybe a
Nothing
(BuiltInSynFamily -> FamTyConFlav
BuiltInSynFamTyCon BuiltInSynFamily
ops)
Maybe Class
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_INTERNAL_TYPELITS (String -> FastString
fsLit String
"ConsSymbol")
Unique
typeConsSymbolTyFamNameKey TyCon
typeConsSymbolTyCon
ops :: BuiltInSynFamily
ops = BuiltInSynFamily { sfMatchFam :: [BuiltInFamRewrite]
sfMatchFam = [BuiltInFamRewrite]
axConsRewrites
, sfInteract :: [BuiltInFamInjectivity]
sfInteract = [BuiltInFamInjectivity]
axConsInjectivity }
axConsRewrites :: [BuiltInFamRewrite]
axConsRewrites :: [BuiltInFamRewrite]
axConsRewrites
= [ TyCon
-> String
-> (Type -> Maybe Char)
-> (Type -> Maybe FastString)
-> (Char -> FastString -> Maybe Type)
-> BuiltInFamRewrite
forall a b.
TyCon
-> String
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> BuiltInFamRewrite
mkBinConstFoldAxiom TyCon
tc String
"ConsSymbolDef" Type -> Maybe Char
isCharLitTy Type -> Maybe FastString
isStrLitTy ((Char -> FastString -> Maybe Type) -> BuiltInFamRewrite)
-> (Char -> FastString -> Maybe Type) -> BuiltInFamRewrite
forall a b. (a -> b) -> a -> b
$
\Char
x FastString
y -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ FastString -> Type
mkStrLitTy (Char -> FastString -> FastString
consFS Char
x FastString
y) ]
where
tc :: TyCon
tc = TyCon
typeConsSymbolTyCon
axConsInjectivity :: [BuiltInFamInjectivity]
axConsInjectivity :: [BuiltInFamInjectivity]
axConsInjectivity
= [
String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"ConsSymbolT1" TyCon
tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
a Type
_b Type
r ->
do { rs <- Type -> Maybe FastString
isStrLitTy Type
r; (x,_) <- unconsFS rs; return (Pair a (mkCharLitTy x)) }
,
String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"ConsSymbolT2" TyCon
tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
_a Type
b Type
r ->
do { rs <- Type -> Maybe FastString
isStrLitTy Type
r; (_,xs) <- unconsFS rs; return (Pair b (mkStrLitTy xs)) }
, String
-> TyCon
-> WhichArg
-> WhichArg
-> (Type -> Bool)
-> BuiltInFamInjectivity
mkBinBIF String
"ConsI-xx" TyCon
tc WhichArg
ArgX WhichArg
ArgX Type -> Bool
noGuard
, String
-> TyCon
-> WhichArg
-> WhichArg
-> (Type -> Bool)
-> BuiltInFamInjectivity
mkBinBIF String
"ConsI-yy" TyCon
tc WhichArg
ArgY WhichArg
ArgY Type -> Bool
noGuard
]
where
tc :: TyCon
tc = TyCon
typeConsSymbolTyCon
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)
Maybe Name
forall a. Maybe a
Nothing
(BuiltInSynFamily -> FamTyConFlav
BuiltInSynFamTyCon BuiltInSynFamily
ops)
Maybe Class
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_INTERNAL_TYPELITS (String -> FastString
fsLit String
"UnconsSymbol")
Unique
typeUnconsSymbolTyFamNameKey TyCon
typeUnconsSymbolTyCon
ops :: BuiltInSynFamily
ops = BuiltInSynFamily { sfMatchFam :: [BuiltInFamRewrite]
sfMatchFam = [BuiltInFamRewrite]
axUnconsRewrites
, sfInteract :: [BuiltInFamInjectivity]
sfInteract = [BuiltInFamInjectivity]
axUnconsInjectivity }
computeUncons :: FastString -> Type
computeUncons :: FastString -> Type
computeUncons FastString
str
= Type -> Maybe Type -> Type
mkPromotedMaybeTy Type
charSymbolPairKind (((Char, FastString) -> Type)
-> Maybe (Char, FastString) -> Maybe Type
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Char, FastString) -> Type
reify (FastString -> Maybe (Char, FastString)
unconsFS FastString
str))
where
reify :: (Char, FastString) -> Type
reify :: (Char, FastString) -> Type
reify (Char
c, FastString
s) = Type -> Type -> Type
charSymbolPair (Char -> Type
mkCharLitTy Char
c) (FastString -> Type
mkStrLitTy FastString
s)
axUnconsRewrites :: [BuiltInFamRewrite]
axUnconsRewrites :: [BuiltInFamRewrite]
axUnconsRewrites
= [ TyCon
-> String
-> (Type -> Maybe FastString)
-> (FastString -> Maybe Type)
-> BuiltInFamRewrite
forall a.
TyCon
-> String
-> (Type -> Maybe a)
-> (a -> Maybe Type)
-> BuiltInFamRewrite
mkUnaryConstFoldAxiom TyCon
tc String
"ConsSymbolDef" Type -> Maybe FastString
isStrLitTy ((FastString -> Maybe Type) -> BuiltInFamRewrite)
-> (FastString -> Maybe Type) -> BuiltInFamRewrite
forall a b. (a -> b) -> a -> b
$
\FastString
x -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ FastString -> Type
computeUncons FastString
x ]
where
tc :: TyCon
tc = TyCon
typeUnconsSymbolTyCon
axUnconsInjectivity :: [BuiltInFamInjectivity]
axUnconsInjectivity :: [BuiltInFamInjectivity]
axUnconsInjectivity
= [
String
-> TyCon
-> (Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopUnaryFamDeduction String
"UnconsSymbolT1" TyCon
tc ((Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \Type
b Type
r ->
do { Maybe Type -> Maybe TypeEqn
Nothing <- Type -> Maybe (Maybe Type)
isPromotedMaybeTy Type
r; return (Pair b nullStrLitTy) }
,
String
-> TyCon
-> (Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopUnaryFamDeduction String
"UnconsSymbolT2" TyCon
tc ((Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \Type
b Type
r ->
do { Just pr <- Type -> Maybe (Maybe Type)
isPromotedMaybeTy Type
r
; (c,s) <- isPromotedPairType pr
; chr <- isCharLitTy c
; str <- isStrLitTy s
; return (Pair b (mkStrLitTy (consFS chr str))) }
, String -> TyCon -> BuiltInFamInjectivity
mkUnaryBIF String
"UnconsI1" TyCon
tc
]
where
tc :: TyCon
tc = TyCon
typeUnconsSymbolTyCon
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
Maybe Name
forall a. Maybe a
Nothing
(BuiltInSynFamily -> FamTyConFlav
BuiltInSynFamTyCon BuiltInSynFamily
ops)
Maybe Class
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_INTERNAL_TYPELITS (String -> FastString
fsLit String
"CharToNat")
Unique
typeCharToNatTyFamNameKey TyCon
typeCharToNatTyCon
ops :: BuiltInSynFamily
ops = BuiltInSynFamily { sfMatchFam :: [BuiltInFamRewrite]
sfMatchFam = [BuiltInFamRewrite]
axCharToNatRewrites
, sfInteract :: [BuiltInFamInjectivity]
sfInteract = [BuiltInFamInjectivity]
axCharToNatInjectivity }
axCharToNatRewrites :: [BuiltInFamRewrite]
axCharToNatRewrites :: [BuiltInFamRewrite]
axCharToNatRewrites
= [ TyCon
-> String
-> (Type -> Maybe Char)
-> (Char -> Maybe Type)
-> BuiltInFamRewrite
forall a.
TyCon
-> String
-> (Type -> Maybe a)
-> (a -> Maybe Type)
-> BuiltInFamRewrite
mkUnaryConstFoldAxiom TyCon
tc String
"CharToNatDef" Type -> Maybe Char
isCharLitTy ((Char -> Maybe Type) -> BuiltInFamRewrite)
-> (Char -> Maybe Type) -> BuiltInFamRewrite
forall a b. (a -> b) -> a -> b
$
\Char
x -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Integer -> Type
num (Char -> Integer
charToInteger Char
x) ]
where
tc :: TyCon
tc = TyCon
typeCharToNatTyCon
axCharToNatInjectivity :: [BuiltInFamInjectivity]
axCharToNatInjectivity :: [BuiltInFamInjectivity]
axCharToNatInjectivity
= [
String
-> TyCon
-> (Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopUnaryFamDeduction String
"CharToNatT1" TyCon
typeCharToNatTyCon ((Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \Type
c Type
r ->
do { nr <- Type -> Maybe Integer
isNumLitTy Type
r; chr <- integerToChar nr; return (Pair c (mkCharLitTy chr)) } ]
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
Maybe Name
forall a. Maybe a
Nothing
(BuiltInSynFamily -> FamTyConFlav
BuiltInSynFamTyCon BuiltInSynFamily
ops)
Maybe Class
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_INTERNAL_TYPELITS (String -> FastString
fsLit String
"NatToChar")
Unique
typeNatToCharTyFamNameKey TyCon
typeNatToCharTyCon
ops :: BuiltInSynFamily
ops = BuiltInSynFamily { sfMatchFam :: [BuiltInFamRewrite]
sfMatchFam = [BuiltInFamRewrite]
axNatToCharRewrites
, sfInteract :: [BuiltInFamInjectivity]
sfInteract = [BuiltInFamInjectivity]
axNatToCharInjectivity }
axNatToCharRewrites :: [BuiltInFamRewrite]
axNatToCharRewrites :: [BuiltInFamRewrite]
axNatToCharRewrites
= [ TyCon
-> String
-> (Type -> Maybe Integer)
-> (Integer -> Maybe Type)
-> BuiltInFamRewrite
forall a.
TyCon
-> String
-> (Type -> Maybe a)
-> (a -> Maybe Type)
-> BuiltInFamRewrite
mkUnaryConstFoldAxiom TyCon
tc String
"NatToCharDef" Type -> Maybe Integer
isNumLitTy ((Integer -> Maybe Type) -> BuiltInFamRewrite)
-> (Integer -> Maybe Type) -> BuiltInFamRewrite
forall a b. (a -> b) -> a -> b
$
\Integer
n -> (Char -> Type) -> Maybe Char -> Maybe Type
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Char -> Type
mkCharLitTy (Integer -> Maybe Char
integerToChar Integer
n) ]
where
tc :: TyCon
tc = TyCon
typeNatToCharTyCon
axNatToCharInjectivity :: [BuiltInFamInjectivity]
axNatToCharInjectivity :: [BuiltInFamInjectivity]
axNatToCharInjectivity
= [
String
-> TyCon
-> (Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopUnaryFamDeduction String
"CharToNatT1" TyCon
typeNatToCharTyCon ((Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \Type
n Type
r ->
do { c <- Type -> Maybe Char
isCharLitTy Type
r; return (Pair n (mkNumLitTy (charToInteger c))) } ]
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
Maybe Name
forall a. Maybe a
Nothing
(BuiltInSynFamily -> FamTyConFlav
BuiltInSynFamTyCon BuiltInSynFamily
ops)
Maybe Class
forall a. Maybe a
Nothing
Injectivity
NotInjective
where
name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_INTERNAL_TYPELITS_INTERNAL (String -> FastString
fsLit String
"CmpChar")
Unique
typeCharCmpTyFamNameKey TyCon
typeCharCmpTyCon
ops :: BuiltInSynFamily
ops = BuiltInSynFamily { sfMatchFam :: [BuiltInFamRewrite]
sfMatchFam = [BuiltInFamRewrite]
axCharCmpRewrites
, sfInteract :: [BuiltInFamInjectivity]
sfInteract = [BuiltInFamInjectivity]
axCharCmpInjectivity }
sc :: TyVar
(TyVar
sc: [TyVar]
_) = [Type] -> [TyVar]
mkTemplateTyVars (Type -> [Type]
forall a. a -> [a]
repeat Type
charTy)
axCharCmpRewrites :: [BuiltInFamRewrite]
axCharCmpRewrites :: [BuiltInFamRewrite]
axCharCmpRewrites
= [ TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
mkRewriteAxiom TyCon
tc String
"CmpCharRefl" [TyVar
sc] [TyVar -> Type
var TyVar
sc, TyVar -> Type
var TyVar
sc] (Ordering -> Type
ordering Ordering
EQ)
, TyCon
-> String
-> (Type -> Maybe Char)
-> (Type -> Maybe Char)
-> (Char -> Char -> Maybe Type)
-> BuiltInFamRewrite
forall a b.
TyCon
-> String
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> BuiltInFamRewrite
mkBinConstFoldAxiom TyCon
tc String
"CmpCharDef" Type -> Maybe Char
isCharLitTy Type -> Maybe Char
isCharLitTy ((Char -> Char -> Maybe Type) -> BuiltInFamRewrite)
-> (Char -> Char -> Maybe Type) -> BuiltInFamRewrite
forall a b. (a -> b) -> a -> b
$
\Char
chr1 Char
chr2 -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Ordering -> Type
ordering (Ordering -> Type) -> Ordering -> Type
forall a b. (a -> b) -> a -> b
$ Char -> Char -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Char
chr1 Char
chr2 ]
where
tc :: TyCon
tc = TyCon
typeCharCmpTyCon
axCharCmpInjectivity :: [BuiltInFamInjectivity]
axCharCmpInjectivity :: [BuiltInFamInjectivity]
axCharCmpInjectivity
= [
String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"CmpCharT" TyCon
typeCharCmpTyCon ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
s Type
t Type
r ->
do { Ordering -> Maybe TypeEqn
EQ <- Type -> Maybe Ordering
isOrderingLitTy Type
r; return (Pair s t) } ]
(===) :: Type -> Type -> Pair Type
Type
x === :: Type -> Type -> TypeEqn
=== Type
y = Type -> Type -> TypeEqn
forall a. a -> a -> Pair a
Pair Type
x Type
y
num :: Integer -> Type
num :: Integer -> Type
num = Integer -> Type
mkNumLitTy
var :: TyVar -> Type
var :: TyVar -> Type
var = TyVar -> Type
mkTyVarTy
(.+.) :: Type -> Type -> Type
Type
s .+. :: Type -> Type -> Type
.+. Type
t = TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatAddTyCon [Type
s,Type
t]
nullStrLitTy :: Type
nullStrLitTy :: Type
nullStrLitTy = FastString -> Type
mkStrLitTy FastString
nilFS
isStrLitTyS :: Type -> Maybe String
isStrLitTyS :: Type -> Maybe String
isStrLitTyS Type
ty = do { fs <- Type -> Maybe FastString
isStrLitTy Type
ty; return (unpackFS fs) }
mkStrLitTyS :: String -> Type
mkStrLitTyS :: String -> Type
mkStrLitTyS String
s = FastString -> Type
mkStrLitTy (String -> FastString
mkFastString String
s)
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 (tc1,[]) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
tc
case () of
()
_ | TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
promotedLTDataCon -> Ordering -> Maybe Ordering
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Ordering
LT
| TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
promotedEQDataCon -> Ordering -> Maybe Ordering
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Ordering
EQ
| TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
promotedGTDataCon -> Ordering -> Maybe Ordering
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Ordering
GT
| Bool
otherwise -> Maybe Ordering
forall a. Maybe a
Nothing
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
Maybe Name
forall a. Maybe a
Nothing
(BuiltInSynFamily -> FamTyConFlav
BuiltInSynFamTyCon BuiltInSynFamily
tcb)
Maybe Class
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
Maybe Name
forall a. Maybe a
Nothing
(BuiltInSynFamily -> FamTyConFlav
BuiltInSynFamTyCon BuiltInSynFamily
tcb)
Maybe Class
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
Maybe Name
forall a. Maybe a
Nothing
(BuiltInSynFamily -> FamTyConFlav
BuiltInSynFamTyCon BuiltInSynFamily
tcb)
Maybe Class
forall a. Maybe a
Nothing
Injectivity
NotInjective
same :: Type -> Type -> Maybe ()
same :: Type -> Type -> Maybe ()
same Type
ty1 Type
ty2 = Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Type
ty1 HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`tcEqType` Type
ty2)
known :: Type -> (Integer -> Bool) -> Maybe Integer
known :: Type -> (Integer -> Bool) -> Maybe Integer
known Type
x Integer -> Bool
p = do { nx <- Type -> Maybe Integer
isNumLitTy Type
x; guard (p nx); return nx }
charToInteger :: Char -> Integer
charToInteger :: Char -> Integer
charToInteger Char
c = Int -> Integer
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 = Char -> Maybe Char
forall a. a -> Maybe a
Just (Int -> Char
Char.chr (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
n))
where inBounds :: Bool
inBounds = Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Char -> Integer
charToInteger Char
forall a. Bounded a => a
minBound Bool -> Bool -> Bool
&&
Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Char -> Integer
charToInteger Char
forall a. Bounded a => a
maxBound
integerToChar Integer
_ = Maybe Char
forall a. Maybe a
Nothing
minus :: Integer -> Integer -> Maybe Integer
minus :: Integer -> Integer -> Maybe Integer
minus Integer
x Integer
y = if Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
y then Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
y) else Maybe Integer
forall a. Maybe a
Nothing
logExact :: Integer -> Integer -> Maybe Integer
logExact :: Integer -> Integer -> Maybe Integer
logExact Integer
x Integer
y = do (z,True) <- Integer -> Integer -> Maybe (Integer, Bool)
genLog Integer
x Integer
y
return z
divide :: Integer -> Integer -> Maybe Integer
divide :: Integer -> Integer -> Maybe Integer
divide Integer
_ Integer
0 = Maybe Integer
forall a. Maybe a
Nothing
divide Integer
x Integer
y = case Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
divMod Integer
x Integer
y of
(Integer
a,Integer
0) -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
a
(Integer, Integer)
_ -> Maybe Integer
forall a. Maybe a
Nothing
rootExact :: Integer -> Integer -> Maybe Integer
rootExact :: Integer -> Integer -> Maybe Integer
rootExact Integer
x Integer
y = do (z,True) <- Integer -> Integer -> Maybe (Integer, Bool)
genRoot Integer
x Integer
y
return z
genRoot :: Integer -> Integer -> Maybe (Integer, Bool)
genRoot :: Integer -> Integer -> Maybe (Integer, Bool)
genRoot Integer
_ Integer
0 = Maybe (Integer, Bool)
forall a. Maybe a
Nothing
genRoot Integer
x0 Integer
1 = (Integer, Bool) -> Maybe (Integer, Bool)
forall a. a -> Maybe a
Just (Integer
x0, Bool
True)
genRoot Integer
x0 Integer
root = (Integer, Bool) -> Maybe (Integer, Bool)
forall a. a -> Maybe a
Just (Integer -> Integer -> (Integer, Bool)
search Integer
0 (Integer
x0Integer -> Integer -> Integer
forall 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 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div (Integer
to Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
from) Integer
2
a :: Integer
a = Integer
x Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
root
in case Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Integer
a Integer
x0 of
Ordering
EQ -> (Integer
x, Bool
True)
Ordering
LT | Integer
x Integer -> Integer -> Bool
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 Integer -> Integer -> Bool
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 Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1 then (Integer, Bool) -> Maybe (Integer, Bool)
forall a. a -> Maybe a
Just (Integer
0, Bool
True) else Maybe (Integer, Bool)
forall a. Maybe a
Nothing
genLog Integer
_ Integer
1 = Maybe (Integer, Bool)
forall a. Maybe a
Nothing
genLog Integer
0 Integer
_ = Maybe (Integer, Bool)
forall a. Maybe a
Nothing
genLog Integer
x Integer
base = (Integer, Bool) -> Maybe (Integer, Bool)
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 Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1 = (Integer
s,Bool
True)
| Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
base = (Integer
s,Bool
False)
| Bool
otherwise =
let s1 :: Integer
s1 = Integer
s Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1
in Integer
s1 Integer -> (Integer, Bool) -> (Integer, Bool)
forall a b. a -> b -> b
`seq` case Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
divMod Integer
i Integer
base of
(Integer
j,Integer
r)
| Integer
r Integer -> Integer -> Bool
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 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
base = Integer
s
| Bool
otherwise = let s1 :: Integer
s1 = Integer
s Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1 in Integer
s1 Integer -> Integer -> Integer
forall a b. a -> b -> b
`seq` Integer -> Integer -> Integer
underLoop Integer
s1 (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div Integer
i Integer
base)