ghc-9.12.1: GHC/Builtin/Types/Literals.hs
{-# LANGUAGE LambdaCase #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} -- See calls to mkTemplateTyVars
module GHC.Builtin.Types.Literals
( tryInteractInertFam, tryInteractTopFam, tryMatchFam
, typeNatTyCons
, typeNatCoAxiomRules
, BuiltInSynFamily(..)
-- If you define a new built-in type family, make sure to export its TyCon
-- from here as well.
-- See Note [Adding built-in type families]
, 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
{-
Note [Type-level literals]
~~~~~~~~~~~~~~~~~~~~~~~~~~
There are currently three forms of type-level literals: natural numbers, symbols, and
characters.
Type-level literals are supported by CoAxiomRules (conditional axioms), which
power the built-in type families (see Note [Adding built-in type families]).
Currently, all built-in type families are for the express purpose of supporting
type-level literals.
See also the Wiki page:
https://gitlab.haskell.org/ghc/ghc/wikis/type-nats
Note [Adding built-in type families]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
There are a few steps to adding a built-in type family:
* Adding a unique for the type family TyCon
These go in GHC.Builtin.Names. It will likely be of the form
@myTyFamNameKey = mkPreludeTyConUnique xyz@, where @xyz@ is a number that
has not been chosen before in GHC.Builtin.Names. There are several examples already
in GHC.Builtin.Names—see, for instance, typeNatAddTyFamNameKey.
* Adding the type family TyCon itself
This goes in GHC.Builtin.Types.Literals. There are plenty of examples of how to define
these -- see, for instance, typeNatAddTyCon.
Once your TyCon has been defined, be sure to:
- Export it from GHC.Builtin.Types.Literals. (Not doing so caused #14632.)
- Include it in the typeNatTyCons list, defined in GHC.Builtin.Types.Literals.
* Define the type family somewhere
Finally, you will need to define the type family somewhere, likely in @base@.
Currently, all of the built-in type families are defined in GHC.TypeLits or
GHC.TypeNats, so those are likely candidates.
Since the behavior of your built-in type family is specified in GHC.Builtin.Types.Literals,
you should give an open type family definition with no instances, like so:
type family MyTypeFam (m :: Nat) (n :: Nat) :: Nat
Changing the argument and result kinds as appropriate.
* Update the relevant test cases
The GHC test suite will likely need to be updated after you add your built-in
type family. For instance:
- The T9181 test prints the :browse contents of GHC.TypeLits, so if you added
a test there, the expected output of T9181 will need to change.
- The TcTypeNatSimple and TcTypeSymbolSimple tests have compile-time unit
tests, as well as TcTypeNatSimpleRun and TcTypeSymbolSimpleRun, which have
runtime unit tests. Consider adding further unit tests to those if your
built-in type family deals with Nats or Symbols, respectively.
Note [Inlining axiom constructors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We have a number of constructor functions with types like
mkUnaryConstFoldAxiom :: TyCon -> String
-> (Type -> Maybe a)
-> (a -> Maybe Type)
-> BuiltInFamRewrite
For very type-family-heavy code, these higher order argument are inefficient;
e.g. the fourth argument might always return (Just ty) in the above. Inlining
them is a bit brutal, but not bad, makes a few-percent difference in, say
perf test T13386.
These functions aren't exported, so the effect is very local.
-}
-------------------------------------------------------------------------------
-- Key utility functions
-------------------------------------------------------------------------------
tryInteractTopFam :: BuiltInSynFamily -> TyCon -> [Type] -> Type
-> [(CoAxiomRule, TypeEqn)]
-- The returned CoAxiomRule is always unary
tryInteractTopFam fam fam_tc tys r
= [(bifinj_axr bif, eqn_out) | bif <- sfInteract fam
, Just eqn_out <- [bifinj_proves bif eqn_in] ]
where
eqn_in :: TypeEqn
eqn_in = Pair (mkTyConApp fam_tc tys) r
tryInteractInertFam :: BuiltInSynFamily -> TyCon
-> [Type] -> [Type] -- F tys1 ~ F tys2
-> [(CoAxiomRule, TypeEqn)]
tryInteractInertFam builtin_fam fam_tc tys1 tys2
= [(bifinj_axr bif, eqn_out) | bif <- sfInteract builtin_fam
, Just eqn_out <- [bifinj_proves bif eqn_in] ]
where
eqn_in = Pair (mkTyConApp fam_tc tys1) (mkTyConApp fam_tc tys2)
tryMatchFam :: BuiltInSynFamily -> [Type]
-> Maybe (CoAxiomRule, [Type], Type)
-- Does this reduce on the given arguments?
-- If it does, returns (CoAxiomRule, types to instantiate the rule at, rhs type)
-- That is: mkAxiomCo (BuiltInFamRew ax) (map mkNomReflCo ts)
-- :: F tys ~r rhs,
tryMatchFam builtin_fam arg_tys
= listToMaybe $ -- Pick first rule to match
[ (bifrw_axr rw_ax, inst_tys, res_ty)
| rw_ax <- sfMatchFam builtin_fam
, Just (inst_tys,res_ty) <- [bifrw_match rw_ax arg_tys] ]
-------------------------------------------------------------------------------
-- Constructing BuiltInFamInjectivity, BuiltInFamRewrite
-------------------------------------------------------------------------------
mkUnaryConstFoldAxiom :: TyCon -> String
-> (Type -> Maybe a)
-> (a -> Maybe Type)
-> BuiltInFamRewrite
-- For the definitional axioms, like (3+4 --> 7)
{-# INLINE mkUnaryConstFoldAxiom #-} -- See Note [Inlining axiom constructors]
mkUnaryConstFoldAxiom fam_tc str isReqTy f
= bif
where
bif = BIF_Rewrite
{ bifrw_name = fsLit str
, bifrw_axr = BuiltInFamRew bif
, bifrw_fam_tc = fam_tc
, bifrw_arity = 1
, bifrw_match = \ts -> do { [t1] <- return ts
; t1' <- isReqTy t1
; res <- f t1'
; return ([t1], res) }
, bifrw_proves = \cs -> do { [Pair s1 s2] <- return 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
-- For the definitional axioms, like (3+4 --> 7)
{-# INLINE mkBinConstFoldAxiom #-} -- See Note [Inlining axiom constructors]
mkBinConstFoldAxiom fam_tc str isReqTy1 isReqTy2 f
= bif
where
bif = BIF_Rewrite
{ bifrw_name = fsLit str
, bifrw_axr = BuiltInFamRew bif
, bifrw_fam_tc = fam_tc
, bifrw_arity = 2
, bifrw_match = \ts -> do { [t1,t2] <- return ts
; t1' <- isReqTy1 t1
; t2' <- isReqTy2 t2
; res <- f t1' t2'
; return ([t1,t2], res) }
, bifrw_proves = \cs -> do { [Pair s1 s2, Pair t1 t2] <- return cs
; s2' <- isReqTy1 s2
; t2' <- isReqTy2 t2
; z <- f s2' t2'
; return (mkTyConApp fam_tc [s1,t1] === z) }
}
mkRewriteAxiom :: TyCon -> String
-> [TyVar] -> [Type] -- LHS of axiom
-> Type -- RHS of axiom
-> BuiltInFamRewrite
-- Not higher order, no benefit in inlining
-- See Note [Inlining axiom constructors]
mkRewriteAxiom fam_tc str tpl_tvs lhs_tys rhs_ty
= assertPpr (tyConArity fam_tc == length lhs_tys) (text str <+> ppr lhs_tys) $
bif
where
bif = BIF_Rewrite
{ bifrw_name = fsLit str
, bifrw_axr = BuiltInFamRew bif
, bifrw_fam_tc = fam_tc
, bifrw_arity = bif_arity
, bifrw_match = match_fn
, bifrw_proves = inst_fn }
bif_arity = length tpl_tvs
match_fn :: [Type] -> Maybe ([Type],Type)
match_fn arg_tys
= assertPpr (tyConArity fam_tc == length arg_tys) (text str <+> ppr arg_tys) $
case tcMatchTys lhs_tys arg_tys of
Nothing -> Nothing
Just subst -> Just (substTyVars subst tpl_tvs, substTy subst rhs_ty)
inst_fn :: [TypeEqn] -> Maybe TypeEqn
inst_fn inst_eqns
= assertPpr (length inst_eqns == bif_arity) (text str $$ ppr inst_eqns) $
Just (mkTyConApp fam_tc (substTys (zipTCvSubst tpl_tvs tys1) lhs_tys)
===
substTy (zipTCvSubst tpl_tvs tys2) rhs_ty)
where
(tys1, tys2) = unzipPairs inst_eqns
mkTopUnaryFamDeduction :: String -> TyCon
-> (Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
-- Deduction from (F s ~ r) where `F` is a unary type function
{-# INLINE mkTopUnaryFamDeduction #-} -- See Note [Inlining axiom constructors]
mkTopUnaryFamDeduction str fam_tc f
= bif
where
bif = BIF_Interact
{ bifinj_name = fsLit str
, bifinj_axr = BuiltInFamInj bif
, bifinj_proves = \(Pair lhs rhs)
-> do { (tc, [a]) <- splitTyConApp_maybe lhs
; massertPpr (tc == fam_tc) (ppr tc $$ ppr fam_tc)
; f a rhs } }
mkTopBinFamDeduction :: String -> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
-- Deduction from (F s t ~ r) where `F` is a binary type function
{-# INLINE mkTopBinFamDeduction #-} -- See Note [Inlining axiom constructors]
mkTopBinFamDeduction str fam_tc f
= bif
where
bif = BIF_Interact
{ bifinj_name = fsLit str
, bifinj_axr = BuiltInFamInj bif
, bifinj_proves = \(Pair lhs rhs) ->
do { (tc, [a,b]) <- splitTyConApp_maybe lhs
; massertPpr (tc == fam_tc) (ppr tc $$ ppr fam_tc)
; f a b rhs } }
mkUnaryBIF :: String -> TyCon -> BuiltInFamInjectivity
-- Not higher order, no benefit in inlining
-- See Note [Inlining axiom constructors]
mkUnaryBIF str fam_tc
= bif
where
bif = BIF_Interact { bifinj_name = fsLit str
, bifinj_axr = BuiltInFamInj bif
, bifinj_proves = proves }
proves (Pair lhs rhs)
= do { (tc2, [x2]) <- splitTyConApp_maybe 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) -- The guard on the equal args, if any
-> BuiltInFamInjectivity
{-# INLINE mkBinBIF #-} -- See Note [Inlining axiom constructors]
mkBinBIF str fam_tc eq1 eq2 check_me
= bif
where
bif = BIF_Interact { bifinj_name = fsLit str
, bifinj_axr = BuiltInFamInj bif
, bifinj_proves = proves }
proves (Pair lhs rhs)
= do { (tc2, [x2,y2]) <- splitTyConApp_maybe rhs
; guard (tc2 == fam_tc)
; (tc1, [x1,y1]) <- splitTyConApp_maybe lhs
; massertPpr (tc1 == fam_tc) (ppr tc1 $$ ppr fam_tc)
; case (eq1, eq2) of
(ArgX,ArgX) -> do_it x1 x2 y1 y2
(ArgX,ArgY) -> do_it x1 y2 x2 y1
(ArgY,ArgX) -> do_it y1 x2 y2 x1
(ArgY,ArgY) -> do_it y1 y2 x1 x2 }
do_it a1 a2 b1 b2 = do { same a1 a2; guard (check_me a1); return (Pair b1 b2) }
noGuard :: Type -> Bool
noGuard _ = True
numGuard :: (Integer -> Bool) -> Type -> Bool
numGuard pred ty = case isNumLitTy ty of
Just n -> pred n
Nothing -> False
data WhichArg = ArgX | ArgY
-------------------------------------------------------------------------------
-- Built-in type constructors for functions on type-level nats
-------------------------------------------------------------------------------
-- The list of built-in type family TyCons that GHC uses.
-- If you define a built-in type family, make sure to add it to this list.
-- See Note [Adding built-in type families]
typeNatTyCons :: [TyCon]
typeNatTyCons =
[ typeNatAddTyCon
, typeNatMulTyCon
, typeNatExpTyCon
, typeNatSubTyCon
, typeNatDivTyCon
, typeNatModTyCon
, typeNatLogTyCon
, typeNatCmpTyCon
, typeSymbolCmpTyCon
, typeSymbolAppendTyCon
, typeCharCmpTyCon
, typeConsSymbolTyCon
, typeUnconsSymbolTyCon
, typeCharToNatTyCon
, typeNatToCharTyCon
]
-- The list of built-in type family axioms that GHC uses.
-- If you define new axioms, make sure to include them in this list.
-- See Note [Adding built-in type families]
typeNatCoAxiomRules :: UniqFM FastString CoAxiomRule
typeNatCoAxiomRules
= listToUFM $
[ pr | tc <- typeNatTyCons
, Just ops <- [isBuiltInSynFamTyCon_maybe tc]
, pr <- [ (bifinj_name bif, bifinj_axr bif) | bif <- sfInteract ops ]
++ [ (bifrw_name bif, bifrw_axr bif) | bif <- sfMatchFam ops ] ]
-------------------------------------------------------------------------------
-- Addition (+)
-------------------------------------------------------------------------------
typeNatAddTyCon :: TyCon
typeNatAddTyCon = mkTypeNatFunTyCon2 name
BuiltInSynFamily
{ sfMatchFam = axAddRewrites
, sfInteract = axAddInjectivity
}
where
name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPENATS (fsLit "+")
typeNatAddTyFamNameKey typeNatAddTyCon
sn,tn :: TyVar -- Of kind Natural
(sn: tn: _) = mkTemplateTyVars (repeat typeSymbolKind)
axAddRewrites :: [BuiltInFamRewrite]
axAddRewrites
= [ mkRewriteAxiom tc "Add0L" [tn] [num 0, var tn] (var tn) -- 0 + t --> t
, mkRewriteAxiom tc "Add0R" [sn] [var sn, num 0] (var sn) -- s + 0 --> s
, mkBinConstFoldAxiom tc "AddDef" isNumLitTy isNumLitTy $ -- 3 + 4 --> 7
\x y -> Just $ num (x + y) ]
where
tc = typeNatAddTyCon
axAddInjectivity :: [BuiltInFamInjectivity]
axAddInjectivity
= [ -- (s + t ~ 0) => (s ~ 0)
mkTopBinFamDeduction "AddT-0L" tc $ \ a _b r ->
do { _ <- known r (== 0); return (Pair a (num 0)) }
, -- (s + t ~ 0) => (t ~ 0)
mkTopBinFamDeduction "AddT-0R" tc $ \ _a b r ->
do { _ <- known r (== 0); return (Pair b (num 0)) }
, -- (5 + t ~ 8) => (t ~ 3)
mkTopBinFamDeduction "AddT-KKL" tc $ \ a b r ->
do { na <- isNumLitTy a; nr <- known r (>= na); return (Pair b (num (nr-na))) }
, -- (s + 5 ~ 8) => (s ~ 3)
mkTopBinFamDeduction "AddT-KKR" tc $ \ a b r ->
do { nb <- isNumLitTy b; nr <- known r (>= nb); return (Pair a (num (nr-nb))) }
, mkBinBIF "AddI-xx" tc ArgX ArgX noGuard -- x1+y1~x2+y2 {x1=x2}=> (y1 ~ y2)
, mkBinBIF "AddI-xy" tc ArgX ArgY noGuard -- x1+y1~x2+y2 {x1=y2}=> (x2 ~ y1)
, mkBinBIF "AddI-yx" tc ArgY ArgX noGuard -- x1+y1~x2+y2 {y1=x2}=> (x1 ~ y2)
, mkBinBIF "AddI-yy" tc ArgY ArgY noGuard -- x1+y1~x2+y2 {y1=y2}=> (x1 ~ x2)
]
where
tc = typeNatAddTyCon
-------------------------------------------------------------------------------
-- Subtraction (-)
-------------------------------------------------------------------------------
typeNatSubTyCon :: TyCon
typeNatSubTyCon = mkTypeNatFunTyCon2 name
BuiltInSynFamily
{ sfMatchFam = axSubRewrites
, sfInteract = axSubInjectivity
}
where
name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPENATS (fsLit "-")
typeNatSubTyFamNameKey typeNatSubTyCon
axSubRewrites :: [BuiltInFamRewrite]
axSubRewrites
= [ mkRewriteAxiom tc "Sub0R" [sn] [var sn, num 0] (var sn) -- s - 0 --> s
, mkBinConstFoldAxiom tc "SubDef" isNumLitTy isNumLitTy $ -- 4 - 3 --> 1 if x>=y
\x y -> fmap num (minus x y) ]
where
tc = typeNatSubTyCon
axSubInjectivity :: [BuiltInFamInjectivity]
axSubInjectivity
= [ -- (a - b ~ 5) => (5 + b ~ a)
mkTopBinFamDeduction "SubT" tc $ \ a b r ->
do { _ <- isNumLitTy r; return (Pair (r .+. b) a) }
, mkBinBIF "SubI-xx" tc ArgX ArgX noGuard -- (x-y1 ~ x-y2) => (y1 ~ y2)
, mkBinBIF "SubI-yy" tc ArgY ArgY noGuard -- (x1-y ~ x2-y) => (x1 ~ x2)
]
where
tc = typeNatSubTyCon
{-
Note [Weakened interaction rule for subtraction]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
A simpler interaction here might be:
`s - t ~ r` --> `t + r ~ s`
This would enable us to reuse all the code for addition.
Unfortunately, this works a little too well at the moment.
Consider the following example:
0 - 5 ~ r --> 5 + r ~ 0 --> (5 = 0, r = 0)
This (correctly) spots that the constraint cannot be solved.
However, this may be a problem if the constraint did not
need to be solved in the first place! Consider the following example:
f :: Proxy (If (5 <=? 0) (0 - 5) (5 - 0)) -> Proxy 5
f = id
Currently, GHC is strict while evaluating functions, so this does not
work, because even though the `If` should evaluate to `5 - 0`, we
also evaluate the "then" branch which generates the constraint `0 - 5 ~ r`,
which fails.
So, for the time being, we only add an improvement when the RHS is a constant,
which happens to work OK for the moment, although clearly we need to do
something more general.
-}
-------------------------------------------------------------------------------
-- Multiplication (*)
-------------------------------------------------------------------------------
typeNatMulTyCon :: TyCon
typeNatMulTyCon = mkTypeNatFunTyCon2 name
BuiltInSynFamily { sfMatchFam = axMulRewrites
, sfInteract = axMulInjectivity }
where
name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPENATS (fsLit "*")
typeNatMulTyFamNameKey typeNatMulTyCon
axMulRewrites :: [BuiltInFamRewrite]
axMulRewrites
= [ mkRewriteAxiom tc "Mul0L" [tn] [num 0, var tn] (num 0) -- 0 * t --> 0
, mkRewriteAxiom tc "Mul0R" [sn] [var sn, num 0] (num 0) -- s * 0 --> 0
, mkRewriteAxiom tc "Mul1L" [tn] [num 1, var tn] (var tn) -- 1 * t --> t
, mkRewriteAxiom tc "Mul1R" [sn] [var sn, num 1] (var sn) -- s * 1 --> s
, mkBinConstFoldAxiom tc "MulDef" isNumLitTy isNumLitTy $ -- 3 + 4 --> 12
\x y -> Just $ num (x * y) ]
where
tc = typeNatMulTyCon
axMulInjectivity :: [BuiltInFamInjectivity]
axMulInjectivity
= [ -- (s * t ~ 1) => (s ~ 1)
mkTopBinFamDeduction "MulT1" tc $ \ s _t r ->
do { _ <- known r (== 1); return (Pair s r) }
, -- (s * t ~ 1) => (t ~ 1)
mkTopBinFamDeduction "MulT2" tc $ \ _s t r ->
do { _ <- known r (== 1); return (Pair t r) }
, -- (3 * t ~ 15) => (t ~ 5)
mkTopBinFamDeduction "MulT3" tc $ \ s t r ->
do { ns <- isNumLitTy s; nr <- isNumLitTy r; y <- divide nr ns; return (Pair t (num y)) }
, -- (s * 3 ~ 15) => (s ~ 5)
mkTopBinFamDeduction "MulT4" tc $ \ s t r ->
do { nt <- isNumLitTy t; nr <- isNumLitTy r; y <- divide nr nt; return (Pair s (num y)) }
, mkBinBIF "MulI-xx" tc ArgX ArgX (numGuard (/= 0)) -- (x*y1 ~ x*y2) {x/=0}=> (y1 ~ y2)
, mkBinBIF "MulI-yy" tc ArgY ArgY (numGuard (/= 0)) -- (x1*y ~ x2*y) {y/=0}=> (x1 ~ x2)
]
where
tc = typeNatMulTyCon
-------------------------------------------------------------------------------
-- Division: Div and Mod
-------------------------------------------------------------------------------
typeNatDivTyCon :: TyCon
typeNatDivTyCon = mkTypeNatFunTyCon2 name
BuiltInSynFamily { sfMatchFam = axDivRewrites
, sfInteract = [] }
where
name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPENATS (fsLit "Div")
typeNatDivTyFamNameKey typeNatDivTyCon
typeNatModTyCon :: TyCon
typeNatModTyCon = mkTypeNatFunTyCon2 name
BuiltInSynFamily { sfMatchFam = axModRewrites
, sfInteract = [] }
where
name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPENATS (fsLit "Mod")
typeNatModTyFamNameKey typeNatModTyCon
axDivRewrites :: [BuiltInFamRewrite]
axDivRewrites
= [ mkRewriteAxiom tc "Div1" [sn] [var sn, num 1] (var sn) -- s `div` 1 --> s
, mkBinConstFoldAxiom tc "DivDef" isNumLitTy isNumLitTy $ -- 8 `div` 4 --> 2
\x y -> do { guard (y /= 0); return (num (div x y)) } ]
where
tc = typeNatDivTyCon
axModRewrites :: [BuiltInFamRewrite]
axModRewrites
= [ mkRewriteAxiom tc "Mod1" [sn] [var sn, num 1] (num 0) -- s `mod` 1 --> 0
, mkBinConstFoldAxiom tc "ModDef" isNumLitTy isNumLitTy $ -- 8 `mod` 3 --> 2
\x y -> do { guard (y /= 0); return (num (mod x y)) } ]
where
tc = typeNatModTyCon
-------------------------------------------------------------------------------
-- Exponentiation: Exp
-------------------------------------------------------------------------------
typeNatExpTyCon :: TyCon -- Exponentiation
typeNatExpTyCon = mkTypeNatFunTyCon2 name
BuiltInSynFamily { sfMatchFam = axExpRewrites
, sfInteract = axExpInjectivity }
where
name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPENATS (fsLit "^")
typeNatExpTyFamNameKey typeNatExpTyCon
axExpRewrites :: [BuiltInFamRewrite]
axExpRewrites
= [ mkRewriteAxiom tc "Exp0R" [sn] [var sn, num 0] (num 1) -- s ^ 0 --> 1
, mkRewriteAxiom tc "Exp1L" [tn] [num 1, var tn] (num 1) -- 1 ^ t --> 1
, mkRewriteAxiom tc "Exp1R" [sn] [var sn, num 1] (var sn) -- s ^ 1 --> s
, mkBinConstFoldAxiom tc "ExpDef" isNumLitTy isNumLitTy $ -- 2 ^ 3 --> 8
\x y -> Just (num (x ^ y)) ]
where
tc = typeNatExpTyCon
axExpInjectivity :: [BuiltInFamInjectivity]
axExpInjectivity
= [ -- (s ^ t ~ 0) => (s ~ 0)
mkTopBinFamDeduction "ExpT1" tc $ \ s _t r ->
do { 0 <- isNumLitTy r; return (Pair s r) }
, -- (2 ^ t ~ 8) => (t ~ 3)
mkTopBinFamDeduction "ExpT2" tc $ \ s t r ->
do { ns <- isNumLitTy s; nr <- isNumLitTy r; y <- logExact nr ns; return (Pair t (num y)) }
, -- (s ^ 2 ~ 9) => (s ~ 3)
mkTopBinFamDeduction "ExpT3" tc $ \ s t r ->
do { nt <- isNumLitTy t; nr <- isNumLitTy r; y <- rootExact nr nt; return (Pair s (num y)) }
, mkBinBIF "ExpI-xx" tc ArgX ArgX (numGuard (> 1)) -- (x^y1 ~ x^y2) {x>1}=> (y1 ~ y2)
, mkBinBIF "ExpI-yy" tc ArgY ArgY (numGuard (/= 0)) -- (x1*y ~ x2*y) {y/=0}=> (x1 ~ x2)
]
where
tc = typeNatExpTyCon
-------------------------------------------------------------------------------
-- Logarithm: Log2
-------------------------------------------------------------------------------
typeNatLogTyCon :: TyCon
typeNatLogTyCon = mkTypeNatFunTyCon1 name
BuiltInSynFamily { sfMatchFam = axLogRewrites
, sfInteract = [] }
where
name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPENATS (fsLit "Log2")
typeNatLogTyFamNameKey typeNatLogTyCon
axLogRewrites :: [BuiltInFamRewrite]
axLogRewrites
= [ mkUnaryConstFoldAxiom tc "LogDef" isNumLitTy $ -- log 8 --> 3
\x -> do { (a,_) <- genLog x 2; return (num a) } ]
where
tc = typeNatLogTyCon
-------------------------------------------------------------------------------
-- Comparision of Nats: CmpNat
-------------------------------------------------------------------------------
typeNatCmpTyCon :: TyCon
typeNatCmpTyCon
= mkFamilyTyCon name
(mkTemplateAnonTyConBinders [ naturalTy, naturalTy ])
orderingKind
Nothing
(BuiltInSynFamTyCon ops)
Nothing
NotInjective
where
name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPENATS_INTERNAL (fsLit "CmpNat")
typeNatCmpTyFamNameKey typeNatCmpTyCon
ops = BuiltInSynFamily { sfMatchFam = axCmpNatRewrites
, sfInteract = axCmpNatInjectivity }
axCmpNatRewrites :: [BuiltInFamRewrite]
axCmpNatRewrites
= [ mkRewriteAxiom tc "CmpNatRefl" [sn] [var sn, var sn] (ordering EQ) -- s `cmp` s --> EQ
, mkBinConstFoldAxiom tc "CmpNatDef" isNumLitTy isNumLitTy $ -- 2 `cmp` 3 --> LT
\x y -> Just (ordering (compare x y)) ]
where
tc = typeNatCmpTyCon
axCmpNatInjectivity :: [BuiltInFamInjectivity]
axCmpNatInjectivity
= [ -- s `cmp` t ~ EQ ==> s ~ t
mkTopBinFamDeduction "CmpNatT3" typeNatCmpTyCon $ \ s t r ->
do { EQ <- isOrderingLitTy r; return (Pair s t) } ]
-------------------------------------------------------------------------------
-- Comparsion of Symbols: CmpSymbol
-------------------------------------------------------------------------------
typeSymbolCmpTyCon :: TyCon
typeSymbolCmpTyCon =
mkFamilyTyCon name
(mkTemplateAnonTyConBinders [typeSymbolKind, typeSymbolKind])
orderingKind
Nothing
(BuiltInSynFamTyCon ops)
Nothing
NotInjective
where
name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPELITS_INTERNAL (fsLit "CmpSymbol")
typeSymbolCmpTyFamNameKey typeSymbolCmpTyCon
ops = BuiltInSynFamily { sfMatchFam = axSymbolCmpRewrites
, sfInteract = axSymbolCmpInjectivity }
ss,ts :: TyVar -- Of kind Symbol
(ss: ts: _) = mkTemplateTyVars (repeat typeSymbolKind)
axSymbolCmpRewrites :: [BuiltInFamRewrite]
axSymbolCmpRewrites
= [ mkRewriteAxiom tc "CmpSymbolRefl" [ss] [var ss, var ss] (ordering EQ) -- s `cmp` s --> EQ
, mkBinConstFoldAxiom tc "CmpSymbolDef" isStrLitTy isStrLitTy $ -- "a" `cmp` "b" --> LT
\x y -> Just (ordering (lexicalCompareFS x y)) ]
where
tc = typeSymbolCmpTyCon
axSymbolCmpInjectivity :: [BuiltInFamInjectivity]
axSymbolCmpInjectivity
= [ mkTopBinFamDeduction "CmpSymbolT" typeSymbolCmpTyCon $ \ s t r ->
do { EQ <- isOrderingLitTy r; return (Pair s t) } ]
-------------------------------------------------------------------------------
-- AppendSymbol
-------------------------------------------------------------------------------
typeSymbolAppendTyCon :: TyCon
typeSymbolAppendTyCon = mkTypeSymbolFunTyCon2 name
BuiltInSynFamily { sfMatchFam = axAppendRewrites
, sfInteract = axAppendInjectivity }
where
name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPELITS (fsLit "AppendSymbol")
typeSymbolAppendFamNameKey typeSymbolAppendTyCon
axAppendRewrites :: [BuiltInFamRewrite]
axAppendRewrites
= [ mkRewriteAxiom tc "Concat0R" [ts] [nullStrLitTy, var ts] (var ts) -- "" ++ t --> t
, mkRewriteAxiom tc "Concat0L" [ss] [var ss, nullStrLitTy] (var ss) -- s ++ "" --> s
, mkBinConstFoldAxiom tc "AppendSymbolDef" isStrLitTy isStrLitTy $ -- "a" ++ "b" --> "ab"
\x y -> Just (mkStrLitTy (appendFS x y)) ]
where
tc = typeSymbolAppendTyCon
axAppendInjectivity :: [BuiltInFamInjectivity]
axAppendInjectivity
= [ -- (AppendSymbol a b ~ "") => (a ~ "")
mkTopBinFamDeduction "AppendSymbolT1" tc $ \ a _b r ->
do { rs <- isStrLitTy r; guard (nullFS rs); return (Pair a nullStrLitTy) }
, -- (AppendSymbol a b ~ "") => (b ~ "")
mkTopBinFamDeduction "AppendSymbolT2" tc $ \ _a b r ->
do { rs <- isStrLitTy r; guard (nullFS rs); return (Pair b nullStrLitTy) }
, -- (AppendSymbol "foo" b ~ "foobar") => (b ~ "bar")
mkTopBinFamDeduction "AppendSymbolT3" tc $ \ a b r ->
do { as <- isStrLitTyS a; rs <- isStrLitTyS r; guard (as `isPrefixOf` rs)
; return (Pair b (mkStrLitTyS (drop (length as) rs))) }
, -- (AppendSymbol f "bar" ~ "foobar") => (f ~ "foo")
mkTopBinFamDeduction "AppendSymbolT3" tc $ \ a b r ->
do { bs <- isStrLitTyS b; rs <- isStrLitTyS r; guard (bs `isSuffixOf` rs)
; return (Pair a (mkStrLitTyS (take (length rs - length bs) rs))) }
, mkBinBIF "AppI-xx" tc ArgX ArgX noGuard -- (x++y1 ~ x++y2) => (y1 ~ y2)
, mkBinBIF "AppI-yy" tc ArgY ArgY noGuard -- (x1++y ~ x2++y) => (x1 ~ x2)
]
where
tc = typeSymbolAppendTyCon
-------------------------------------------------------------------------------
-- ConsSymbol
-------------------------------------------------------------------------------
typeConsSymbolTyCon :: TyCon
typeConsSymbolTyCon =
mkFamilyTyCon name
(mkTemplateAnonTyConBinders [ charTy, typeSymbolKind ])
typeSymbolKind
Nothing
(BuiltInSynFamTyCon ops)
Nothing
(Injective [True, True])
where
name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPELITS (fsLit "ConsSymbol")
typeConsSymbolTyFamNameKey typeConsSymbolTyCon
ops = BuiltInSynFamily { sfMatchFam = axConsRewrites
, sfInteract = axConsInjectivity }
axConsRewrites :: [BuiltInFamRewrite]
axConsRewrites
= [ mkBinConstFoldAxiom tc "ConsSymbolDef" isCharLitTy isStrLitTy $ -- 'a' : "bc" --> "abc"
\x y -> Just $ mkStrLitTy (consFS x y) ]
where
tc = typeConsSymbolTyCon
axConsInjectivity :: [BuiltInFamInjectivity]
axConsInjectivity
= [ -- ConsSymbol a b ~ "blah" => (a ~ 'b')
mkTopBinFamDeduction "ConsSymbolT1" tc $ \ a _b r ->
do { rs <- isStrLitTy r; (x,_) <- unconsFS rs; return (Pair a (mkCharLitTy x)) }
, -- ConsSymbol a b ~ "blah" => (b ~ "lah")
mkTopBinFamDeduction "ConsSymbolT2" tc $ \ _a b r ->
do { rs <- isStrLitTy r; (_,xs) <- unconsFS rs; return (Pair b (mkStrLitTy xs)) }
, mkBinBIF "ConsI-xx" tc ArgX ArgX noGuard -- (x:y1 ~ x:y2) => (y1 ~ y2)
, mkBinBIF "ConsI-yy" tc ArgY ArgY noGuard -- (x1:y ~ x2:y) => (x1 ~ x2)
]
where
tc = typeConsSymbolTyCon
-------------------------------------------------------------------------------
-- UnconsSymbol
-------------------------------------------------------------------------------
typeUnconsSymbolTyCon :: TyCon
typeUnconsSymbolTyCon =
mkFamilyTyCon name
(mkTemplateAnonTyConBinders [ typeSymbolKind ])
(mkMaybeTy charSymbolPairKind)
Nothing
(BuiltInSynFamTyCon ops)
Nothing
(Injective [True])
where
name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPELITS (fsLit "UnconsSymbol")
typeUnconsSymbolTyFamNameKey typeUnconsSymbolTyCon
ops = BuiltInSynFamily { sfMatchFam = axUnconsRewrites
, sfInteract = axUnconsInjectivity }
computeUncons :: FastString -> Type
computeUncons str
= mkPromotedMaybeTy charSymbolPairKind (fmap reify (unconsFS str))
where
reify :: (Char, FastString) -> Type
reify (c, s) = charSymbolPair (mkCharLitTy c) (mkStrLitTy s)
axUnconsRewrites :: [BuiltInFamRewrite]
axUnconsRewrites
= [ mkUnaryConstFoldAxiom tc "ConsSymbolDef" isStrLitTy $ -- 'a' : "bc" --> "abc"
\x -> Just $ computeUncons x ]
where
tc = typeUnconsSymbolTyCon
axUnconsInjectivity :: [BuiltInFamInjectivity]
axUnconsInjectivity
= [ -- (UnconsSymbol b ~ Nothing) => (b ~ "")
mkTopUnaryFamDeduction "UnconsSymbolT1" tc $ \b r ->
do { Nothing <- isPromotedMaybeTy r; return (Pair b nullStrLitTy) }
, -- (UnconsSymbol b ~ Just ('f',"oobar")) => (b ~ "foobar")
mkTopUnaryFamDeduction "UnconsSymbolT2" tc $ \b r ->
do { Just pr <- isPromotedMaybeTy r
; (c,s) <- isPromotedPairType pr
; chr <- isCharLitTy c
; str <- isStrLitTy s
; return (Pair b (mkStrLitTy (consFS chr str))) }
, mkUnaryBIF "UnconsI1" tc -- (UnconsSymbol x1 ~ z, UnconsSymbol x2 ~ z) => (x1 ~ x2)
]
where
tc = typeUnconsSymbolTyCon
-------------------------------------------------------------------------------
-- CharToNat
-------------------------------------------------------------------------------
typeCharToNatTyCon :: TyCon
typeCharToNatTyCon =
mkFamilyTyCon name
(mkTemplateAnonTyConBinders [ charTy ])
naturalTy
Nothing
(BuiltInSynFamTyCon ops)
Nothing
(Injective [True])
where
name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPELITS (fsLit "CharToNat")
typeCharToNatTyFamNameKey typeCharToNatTyCon
ops = BuiltInSynFamily { sfMatchFam = axCharToNatRewrites
, sfInteract = axCharToNatInjectivity }
axCharToNatRewrites :: [BuiltInFamRewrite]
axCharToNatRewrites
= [ mkUnaryConstFoldAxiom tc "CharToNatDef" isCharLitTy $ -- CharToNat 'a' --> 97
\x -> Just $ num (charToInteger x) ]
where
tc = typeCharToNatTyCon
axCharToNatInjectivity :: [BuiltInFamInjectivity]
axCharToNatInjectivity
= [ -- (CharToNat c ~ 122) => (c ~ 'z')
mkTopUnaryFamDeduction "CharToNatT1" typeCharToNatTyCon $ \c r ->
do { nr <- isNumLitTy r; chr <- integerToChar nr; return (Pair c (mkCharLitTy chr)) } ]
-------------------------------------------------------------------------------
-- NatToChar
-------------------------------------------------------------------------------
typeNatToCharTyCon :: TyCon
typeNatToCharTyCon =
mkFamilyTyCon name
(mkTemplateAnonTyConBinders [ naturalTy ])
charTy
Nothing
(BuiltInSynFamTyCon ops)
Nothing
(Injective [True])
where
name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPELITS (fsLit "NatToChar")
typeNatToCharTyFamNameKey typeNatToCharTyCon
ops = BuiltInSynFamily { sfMatchFam = axNatToCharRewrites
, sfInteract = axNatToCharInjectivity }
axNatToCharRewrites :: [BuiltInFamRewrite]
axNatToCharRewrites
= [ mkUnaryConstFoldAxiom tc "NatToCharDef" isNumLitTy $ -- NatToChar 97 --> 'a'
\n -> fmap mkCharLitTy (integerToChar n) ]
where
tc = typeNatToCharTyCon
axNatToCharInjectivity :: [BuiltInFamInjectivity]
axNatToCharInjectivity
= [ -- (NatToChar n ~ 'z') => (n ~ 122)
mkTopUnaryFamDeduction "CharToNatT1" typeNatToCharTyCon $ \n r ->
do { c <- isCharLitTy r; return (Pair n (mkNumLitTy (charToInteger c))) } ]
-----------------------------------------------------------------------------
-- CmpChar
-----------------------------------------------------------------------------
typeCharCmpTyCon :: TyCon
typeCharCmpTyCon =
mkFamilyTyCon name
(mkTemplateAnonTyConBinders [ charTy, charTy ])
orderingKind
Nothing
(BuiltInSynFamTyCon ops)
Nothing
NotInjective
where
name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPELITS_INTERNAL (fsLit "CmpChar")
typeCharCmpTyFamNameKey typeCharCmpTyCon
ops = BuiltInSynFamily { sfMatchFam = axCharCmpRewrites
, sfInteract = axCharCmpInjectivity }
sc :: TyVar -- Of kind Char
(sc: _) = mkTemplateTyVars (repeat charTy)
axCharCmpRewrites :: [BuiltInFamRewrite]
axCharCmpRewrites
= [ mkRewriteAxiom tc "CmpCharRefl" [sc] [var sc, var sc] (ordering EQ) -- s `cmp` s --> EQ
, mkBinConstFoldAxiom tc "CmpCharDef" isCharLitTy isCharLitTy $ -- 'a' `cmp` 'b' --> LT
\chr1 chr2 -> Just $ ordering $ compare chr1 chr2 ]
where
tc = typeCharCmpTyCon
axCharCmpInjectivity :: [BuiltInFamInjectivity]
axCharCmpInjectivity
= [ -- (CmpChar s t ~ EQ) => s ~ t
mkTopBinFamDeduction "CmpCharT" typeCharCmpTyCon $ \ s t r ->
do { EQ <- isOrderingLitTy r; return (Pair s t) } ]
{-------------------------------------------------------------------------------
Various utilities for making axioms and types
-------------------------------------------------------------------------------}
(===) :: Type -> Type -> Pair Type
x === y = Pair x y
num :: Integer -> Type
num = mkNumLitTy
var :: TyVar -> Type
var = mkTyVarTy
(.+.) :: Type -> Type -> Type
s .+. t = mkTyConApp typeNatAddTyCon [s,t]
{-
(.-.) :: Type -> Type -> Type
s .-. t = mkTyConApp typeNatSubTyCon [s,t]
(.*.) :: Type -> Type -> Type
s .*. t = mkTyConApp typeNatMulTyCon [s,t]
tDiv :: Type -> Type -> Type
tDiv s t = mkTyConApp typeNatDivTyCon [s,t]
tMod :: Type -> Type -> Type
tMod s t = mkTyConApp typeNatModTyCon [s,t]
(.^.) :: Type -> Type -> Type
s .^. t = mkTyConApp typeNatExpTyCon [s,t]
cmpNat :: Type -> Type -> Type
cmpNat s t = mkTyConApp typeNatCmpTyCon [s,t]
cmpSymbol :: Type -> Type -> Type
cmpSymbol s t = mkTyConApp typeSymbolCmpTyCon [s,t]
appendSymbol :: Type -> Type -> Type
appendSymbol s t = mkTyConApp typeSymbolAppendTyCon [s, t]
-}
nullStrLitTy :: Type -- The type ""
nullStrLitTy = mkStrLitTy nilFS
isStrLitTyS :: Type -> Maybe String
isStrLitTyS ty = do { fs <- isStrLitTy ty; return (unpackFS fs) }
mkStrLitTyS :: String -> Type
mkStrLitTyS s = mkStrLitTy (mkFastString s)
charSymbolPair :: Type -> Type -> Type
charSymbolPair = mkPromotedPairTy charTy typeSymbolKind
charSymbolPairKind :: Kind
charSymbolPairKind = mkTyConApp pairTyCon [charTy, typeSymbolKind]
orderingKind :: Kind
orderingKind = mkTyConApp orderingTyCon []
ordering :: Ordering -> Type
ordering o =
case o of
LT -> mkTyConApp promotedLTDataCon []
EQ -> mkTyConApp promotedEQDataCon []
GT -> mkTyConApp promotedGTDataCon []
isOrderingLitTy :: Type -> Maybe Ordering
isOrderingLitTy tc =
do (tc1,[]) <- splitTyConApp_maybe tc
case () of
_ | tc1 == promotedLTDataCon -> return LT
| tc1 == promotedEQDataCon -> return EQ
| tc1 == promotedGTDataCon -> return GT
| otherwise -> Nothing
-- Make a unary built-in constructor of kind: Nat -> Nat
mkTypeNatFunTyCon1 :: Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon1 op tcb =
mkFamilyTyCon op
(mkTemplateAnonTyConBinders [ naturalTy ])
naturalTy
Nothing
(BuiltInSynFamTyCon tcb)
Nothing
NotInjective
-- Make a binary built-in constructor of kind: Nat -> Nat -> Nat
mkTypeNatFunTyCon2 :: Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon2 op tcb =
mkFamilyTyCon op
(mkTemplateAnonTyConBinders [ naturalTy, naturalTy ])
naturalTy
Nothing
(BuiltInSynFamTyCon tcb)
Nothing
NotInjective
-- Make a binary built-in constructor of kind: Symbol -> Symbol -> Symbol
mkTypeSymbolFunTyCon2 :: Name -> BuiltInSynFamily -> TyCon
mkTypeSymbolFunTyCon2 op tcb =
mkFamilyTyCon op
(mkTemplateAnonTyConBinders [ typeSymbolKind, typeSymbolKind ])
typeSymbolKind
Nothing
(BuiltInSynFamTyCon tcb)
Nothing
NotInjective
same :: Type -> Type -> Maybe ()
same ty1 ty2 = guard (ty1 `tcEqType` ty2)
known :: Type -> (Integer -> Bool) -> Maybe Integer
known x p = do { nx <- isNumLitTy x; guard (p nx); return nx }
charToInteger :: Char -> Integer
charToInteger c = fromIntegral (Char.ord c)
integerToChar :: Integer -> Maybe Char
integerToChar n | inBounds = Just (Char.chr (fromInteger n))
where inBounds = n >= charToInteger minBound &&
n <= charToInteger maxBound
integerToChar _ = Nothing
{- -----------------------------------------------------------------------------
These inverse functions are used for simplifying propositions using
concrete natural numbers.
----------------------------------------------------------------------------- -}
-- | Subtract two natural numbers.
minus :: Integer -> Integer -> Maybe Integer
minus x y = if x >= y then Just (x - y) else Nothing
-- | Compute the exact logarithm of a natural number.
-- The logarithm base is the second argument.
logExact :: Integer -> Integer -> Maybe Integer
logExact x y = do (z,True) <- genLog x y
return z
-- | Divide two natural numbers.
divide :: Integer -> Integer -> Maybe Integer
divide _ 0 = Nothing
divide x y = case divMod x y of
(a,0) -> Just a
_ -> Nothing
-- | Compute the exact root of a natural number.
-- The second argument specifies which root we are computing.
rootExact :: Integer -> Integer -> Maybe Integer
rootExact x y = do (z,True) <- genRoot x y
return z
{- | Compute the n-th root of a natural number, rounded down to
the closest natural number. The boolean indicates if the result
is exact (i.e., True means no rounding was done, False means rounded down).
The second argument specifies which root we are computing. -}
genRoot :: Integer -> Integer -> Maybe (Integer, Bool)
genRoot _ 0 = Nothing
genRoot x0 1 = Just (x0, True)
genRoot x0 root = Just (search 0 (x0+1))
where
search from to = let x = from + div (to - from) 2
a = x ^ root
in case compare a x0 of
EQ -> (x, True)
LT | x /= from -> search x to
| otherwise -> (from, False)
GT | x /= to -> search from x
| otherwise -> (from, False)
{- | Compute the logarithm of a number in the given base, rounded down to the
closest integer. The boolean indicates if we the result is exact
(i.e., True means no rounding happened, False means we rounded down).
The logarithm base is the second argument. -}
genLog :: Integer -> Integer -> Maybe (Integer, Bool)
genLog x 0 = if x == 1 then Just (0, True) else Nothing
genLog _ 1 = Nothing
genLog 0 _ = Nothing
genLog x base = Just (exactLoop 0 x)
where
exactLoop s i
| i == 1 = (s,True)
| i < base = (s,False)
| otherwise =
let s1 = s + 1
in s1 `seq` case divMod i base of
(j,r)
| r == 0 -> exactLoop s1 j
| otherwise -> (underLoop s1 j, False)
underLoop s i
| i < base = s
| otherwise = let s1 = s + 1 in s1 `seq` underLoop s1 (div i base)