{-# LANGUAGE LambdaCase #-}

module GHC.Builtin.Types.Literals
  ( 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
  , typeNatLeqTyCon
  , typeNatSubTyCon
  , typeNatDivTyCon
  , typeNatModTyCon
  , typeNatLogTyCon
  , typeNatCmpTyCon
  , typeSymbolCmpTyCon
  , typeSymbolAppendTyCon
  ) where

import GHC.Prelude

import GHC.Core.Type
import GHC.Data.Pair
import GHC.Tc.Utils.TcType ( TcType, tcEqType )
import GHC.Core.TyCon    ( TyCon, FamTyConFlav(..), mkFamilyTyCon
                         , Injectivity(..) )
import GHC.Core.Coercion ( Role(..) )
import GHC.Tc.Types.Constraint ( Xi )
import GHC.Core.Coercion.Axiom ( CoAxiomRule(..), BuiltInSynFamily(..), TypeEqn )
import GHC.Types.Name          ( Name, BuiltInSyntax(..) )
import GHC.Builtin.Types
import GHC.Builtin.Types.Prim  ( mkTemplateAnonTyConBinders )
import GHC.Builtin.Names
                  ( gHC_TYPELITS
                  , gHC_TYPENATS
                  , typeNatAddTyFamNameKey
                  , typeNatMulTyFamNameKey
                  , typeNatExpTyFamNameKey
                  , typeNatLeqTyFamNameKey
                  , typeNatSubTyFamNameKey
                  , typeNatDivTyFamNameKey
                  , typeNatModTyFamNameKey
                  , typeNatLogTyFamNameKey
                  , typeNatCmpTyFamNameKey
                  , typeSymbolCmpTyFamNameKey
                  , typeSymbolAppendFamNameKey
                  )
import GHC.Data.FastString
import qualified Data.Map as Map
import Data.Maybe ( isJust )
import Control.Monad ( guard )
import Data.List  ( isPrefixOf, isSuffixOf )

{-
Note [Type-level literals]
~~~~~~~~~~~~~~~~~~~~~~~~~~
There are currently two forms of type-level literals: natural numbers, and
symbols (even though this module is named GHC.Builtin.Types.Literals, it covers both).

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.

* Exposing associated type family axioms

  When defining the type family TyCon, you will need to define an axiom for
  the type family in general (see, for instance, axAddDef), and perhaps other
  auxiliary axioms for special cases of the type family (see, for instance,
  axAdd0L and axAdd0R).

  After you have defined all of these axioms, be sure to include them in the
  typeNatCoAxiomRules list, defined in GHC.Builtin.Types.Literals.
  (Not doing so caused #14934.)

* 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.
-}

{-------------------------------------------------------------------------------
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 :: [TyCon]
typeNatTyCons =
  [ TyCon
typeNatAddTyCon
  , TyCon
typeNatMulTyCon
  , TyCon
typeNatExpTyCon
  , TyCon
typeNatLeqTyCon
  , TyCon
typeNatSubTyCon
  , TyCon
typeNatDivTyCon
  , TyCon
typeNatModTyCon
  , TyCon
typeNatLogTyCon
  , TyCon
typeNatCmpTyCon
  , TyCon
typeSymbolCmpTyCon
  , TyCon
typeSymbolAppendTyCon
  ]

typeNatAddTyCon :: TyCon
typeNatAddTyCon :: TyCon
typeNatAddTyCon = Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon2 Name
name
  BuiltInSynFamily :: ([Type] -> Maybe (CoAxiomRule, [Type], Type))
-> ([Type] -> Type -> [TypeEqn])
-> ([Type] -> Type -> [Type] -> Type -> [TypeEqn])
-> BuiltInSynFamily
BuiltInSynFamily
    { sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
sfMatchFam      = [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamAdd
    , sfInteractTop :: [Type] -> Type -> [TypeEqn]
sfInteractTop   = [Type] -> Type -> [TypeEqn]
interactTopAdd
    , sfInteractInert :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
sfInteractInert = [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertAdd
    }
  where
  name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_TYPENATS (String -> FastString
fsLit String
"+")
            Unique
typeNatAddTyFamNameKey TyCon
typeNatAddTyCon

typeNatSubTyCon :: TyCon
typeNatSubTyCon :: TyCon
typeNatSubTyCon = Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon2 Name
name
  BuiltInSynFamily :: ([Type] -> Maybe (CoAxiomRule, [Type], Type))
-> ([Type] -> Type -> [TypeEqn])
-> ([Type] -> Type -> [Type] -> Type -> [TypeEqn])
-> BuiltInSynFamily
BuiltInSynFamily
    { sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
sfMatchFam      = [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamSub
    , sfInteractTop :: [Type] -> Type -> [TypeEqn]
sfInteractTop   = [Type] -> Type -> [TypeEqn]
interactTopSub
    , sfInteractInert :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
sfInteractInert = [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertSub
    }
  where
  name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_TYPENATS (String -> FastString
fsLit String
"-")
            Unique
typeNatSubTyFamNameKey TyCon
typeNatSubTyCon

typeNatMulTyCon :: TyCon
typeNatMulTyCon :: TyCon
typeNatMulTyCon = Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon2 Name
name
  BuiltInSynFamily :: ([Type] -> Maybe (CoAxiomRule, [Type], Type))
-> ([Type] -> Type -> [TypeEqn])
-> ([Type] -> Type -> [Type] -> Type -> [TypeEqn])
-> BuiltInSynFamily
BuiltInSynFamily
    { sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
sfMatchFam      = [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamMul
    , sfInteractTop :: [Type] -> Type -> [TypeEqn]
sfInteractTop   = [Type] -> Type -> [TypeEqn]
interactTopMul
    , sfInteractInert :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
sfInteractInert = [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertMul
    }
  where
  name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_TYPENATS (String -> FastString
fsLit String
"*")
            Unique
typeNatMulTyFamNameKey TyCon
typeNatMulTyCon

typeNatDivTyCon :: TyCon
typeNatDivTyCon :: TyCon
typeNatDivTyCon = Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon2 Name
name
  BuiltInSynFamily :: ([Type] -> Maybe (CoAxiomRule, [Type], Type))
-> ([Type] -> Type -> [TypeEqn])
-> ([Type] -> Type -> [Type] -> Type -> [TypeEqn])
-> BuiltInSynFamily
BuiltInSynFamily
    { sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
sfMatchFam      = [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamDiv
    , sfInteractTop :: [Type] -> Type -> [TypeEqn]
sfInteractTop   = [Type] -> Type -> [TypeEqn]
interactTopDiv
    , sfInteractInert :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
sfInteractInert = [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertDiv
    }
  where
  name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_TYPENATS (String -> FastString
fsLit String
"Div")
            Unique
typeNatDivTyFamNameKey TyCon
typeNatDivTyCon

typeNatModTyCon :: TyCon
typeNatModTyCon :: TyCon
typeNatModTyCon = Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon2 Name
name
  BuiltInSynFamily :: ([Type] -> Maybe (CoAxiomRule, [Type], Type))
-> ([Type] -> Type -> [TypeEqn])
-> ([Type] -> Type -> [Type] -> Type -> [TypeEqn])
-> BuiltInSynFamily
BuiltInSynFamily
    { sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
sfMatchFam      = [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamMod
    , sfInteractTop :: [Type] -> Type -> [TypeEqn]
sfInteractTop   = [Type] -> Type -> [TypeEqn]
interactTopMod
    , sfInteractInert :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
sfInteractInert = [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertMod
    }
  where
  name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_TYPENATS (String -> FastString
fsLit String
"Mod")
            Unique
typeNatModTyFamNameKey TyCon
typeNatModTyCon





typeNatExpTyCon :: TyCon
typeNatExpTyCon :: TyCon
typeNatExpTyCon = Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon2 Name
name
  BuiltInSynFamily :: ([Type] -> Maybe (CoAxiomRule, [Type], Type))
-> ([Type] -> Type -> [TypeEqn])
-> ([Type] -> Type -> [Type] -> Type -> [TypeEqn])
-> BuiltInSynFamily
BuiltInSynFamily
    { sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
sfMatchFam      = [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamExp
    , sfInteractTop :: [Type] -> Type -> [TypeEqn]
sfInteractTop   = [Type] -> Type -> [TypeEqn]
interactTopExp
    , sfInteractInert :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
sfInteractInert = [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertExp
    }
  where
  name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_TYPENATS (String -> FastString
fsLit String
"^")
                Unique
typeNatExpTyFamNameKey TyCon
typeNatExpTyCon

typeNatLogTyCon :: TyCon
typeNatLogTyCon :: TyCon
typeNatLogTyCon = Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon1 Name
name
  BuiltInSynFamily :: ([Type] -> Maybe (CoAxiomRule, [Type], Type))
-> ([Type] -> Type -> [TypeEqn])
-> ([Type] -> Type -> [Type] -> Type -> [TypeEqn])
-> BuiltInSynFamily
BuiltInSynFamily
    { sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
sfMatchFam      = [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamLog
    , sfInteractTop :: [Type] -> Type -> [TypeEqn]
sfInteractTop   = [Type] -> Type -> [TypeEqn]
interactTopLog
    , sfInteractInert :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
sfInteractInert = [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertLog
    }
  where
  name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_TYPENATS (String -> FastString
fsLit String
"Log2")
            Unique
typeNatLogTyFamNameKey TyCon
typeNatLogTyCon



typeNatLeqTyCon :: TyCon
typeNatLeqTyCon :: TyCon
typeNatLeqTyCon =
  Name
-> [TyConBinder]
-> Type
-> Maybe Name
-> FamTyConFlav
-> Maybe Class
-> Injectivity
-> TyCon
mkFamilyTyCon Name
name
    ([Type] -> [TyConBinder]
mkTemplateAnonTyConBinders [ Type
typeNatKind, Type
typeNatKind ])
    Type
boolTy
    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_TYPENATS (String -> FastString
fsLit String
"<=?")
                Unique
typeNatLeqTyFamNameKey TyCon
typeNatLeqTyCon
  ops :: BuiltInSynFamily
ops = BuiltInSynFamily :: ([Type] -> Maybe (CoAxiomRule, [Type], Type))
-> ([Type] -> Type -> [TypeEqn])
-> ([Type] -> Type -> [Type] -> Type -> [TypeEqn])
-> BuiltInSynFamily
BuiltInSynFamily
    { sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
sfMatchFam      = [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamLeq
    , sfInteractTop :: [Type] -> Type -> [TypeEqn]
sfInteractTop   = [Type] -> Type -> [TypeEqn]
interactTopLeq
    , sfInteractInert :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
sfInteractInert = [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertLeq
    }

typeNatCmpTyCon :: TyCon
typeNatCmpTyCon :: TyCon
typeNatCmpTyCon =
  Name
-> [TyConBinder]
-> Type
-> Maybe Name
-> FamTyConFlav
-> Maybe Class
-> Injectivity
-> TyCon
mkFamilyTyCon Name
name
    ([Type] -> [TyConBinder]
mkTemplateAnonTyConBinders [ Type
typeNatKind, Type
typeNatKind ])
    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_TYPENATS (String -> FastString
fsLit String
"CmpNat")
                Unique
typeNatCmpTyFamNameKey TyCon
typeNatCmpTyCon
  ops :: BuiltInSynFamily
ops = BuiltInSynFamily :: ([Type] -> Maybe (CoAxiomRule, [Type], Type))
-> ([Type] -> Type -> [TypeEqn])
-> ([Type] -> Type -> [Type] -> Type -> [TypeEqn])
-> BuiltInSynFamily
BuiltInSynFamily
    { sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
sfMatchFam      = [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamCmpNat
    , sfInteractTop :: [Type] -> Type -> [TypeEqn]
sfInteractTop   = [Type] -> Type -> [TypeEqn]
interactTopCmpNat
    , sfInteractInert :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
sfInteractInert = \[Type]
_ Type
_ [Type]
_ Type
_ -> []
    }

typeSymbolCmpTyCon :: TyCon
typeSymbolCmpTyCon :: TyCon
typeSymbolCmpTyCon =
  Name
-> [TyConBinder]
-> Type
-> Maybe Name
-> FamTyConFlav
-> Maybe Class
-> Injectivity
-> TyCon
mkFamilyTyCon Name
name
    ([Type] -> [TyConBinder]
mkTemplateAnonTyConBinders [ Type
typeSymbolKind, Type
typeSymbolKind ])
    Type
orderingKind
    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_TYPELITS (String -> FastString
fsLit String
"CmpSymbol")
                Unique
typeSymbolCmpTyFamNameKey TyCon
typeSymbolCmpTyCon
  ops :: BuiltInSynFamily
ops = BuiltInSynFamily :: ([Type] -> Maybe (CoAxiomRule, [Type], Type))
-> ([Type] -> Type -> [TypeEqn])
-> ([Type] -> Type -> [Type] -> Type -> [TypeEqn])
-> BuiltInSynFamily
BuiltInSynFamily
    { sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
sfMatchFam      = [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamCmpSymbol
    , sfInteractTop :: [Type] -> Type -> [TypeEqn]
sfInteractTop   = [Type] -> Type -> [TypeEqn]
interactTopCmpSymbol
    , sfInteractInert :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
sfInteractInert = \[Type]
_ Type
_ [Type]
_ Type
_ -> []
    }

typeSymbolAppendTyCon :: TyCon
typeSymbolAppendTyCon :: TyCon
typeSymbolAppendTyCon = Name -> BuiltInSynFamily -> TyCon
mkTypeSymbolFunTyCon2 Name
name
  BuiltInSynFamily :: ([Type] -> Maybe (CoAxiomRule, [Type], Type))
-> ([Type] -> Type -> [TypeEqn])
-> ([Type] -> Type -> [Type] -> Type -> [TypeEqn])
-> BuiltInSynFamily
BuiltInSynFamily
    { sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
sfMatchFam      = [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamAppendSymbol
    , sfInteractTop :: [Type] -> Type -> [TypeEqn]
sfInteractTop   = [Type] -> Type -> [TypeEqn]
interactTopAppendSymbol
    , sfInteractInert :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
sfInteractInert = [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertAppendSymbol
    }
  where
  name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_TYPELITS (String -> FastString
fsLit String
"AppendSymbol")
                Unique
typeSymbolAppendFamNameKey TyCon
typeSymbolAppendTyCon



-- Make a unary built-in constructor of kind: Nat -> Nat
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
typeNatKind ])
    Type
typeNatKind
    Maybe Name
forall a. Maybe a
Nothing
    (BuiltInSynFamily -> FamTyConFlav
BuiltInSynFamTyCon BuiltInSynFamily
tcb)
    Maybe Class
forall a. Maybe a
Nothing
    Injectivity
NotInjective


-- Make a binary built-in constructor of kind: Nat -> Nat -> Nat
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
typeNatKind, Type
typeNatKind ])
    Type
typeNatKind
    Maybe Name
forall a. Maybe a
Nothing
    (BuiltInSynFamily -> FamTyConFlav
BuiltInSynFamTyCon BuiltInSynFamily
tcb)
    Maybe Class
forall a. Maybe a
Nothing
    Injectivity
NotInjective

-- Make a binary built-in constructor of kind: Symbol -> Symbol -> Symbol
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


{-------------------------------------------------------------------------------
Built-in rules axioms
-------------------------------------------------------------------------------}

-- If you add additional rules, please remember to add them to
-- `typeNatCoAxiomRules` also.
-- See Note [Adding built-in type families]
axAddDef
  , axMulDef
  , axExpDef
  , axLeqDef
  , axCmpNatDef
  , axCmpSymbolDef
  , axAppendSymbolDef
  , axAdd0L
  , axAdd0R
  , axMul0L
  , axMul0R
  , axMul1L
  , axMul1R
  , axExp1L
  , axExp0R
  , axExp1R
  , axLeqRefl
  , axCmpNatRefl
  , axCmpSymbolRefl
  , axLeq0L
  , axSubDef
  , axSub0R
  , axAppendSymbol0R
  , axAppendSymbol0L
  , axDivDef
  , axDiv1
  , axModDef
  , axMod1
  , axLogDef
  :: CoAxiomRule

axAddDef :: CoAxiomRule
axAddDef = String
-> TyCon -> (Integer -> Integer -> Maybe Type) -> CoAxiomRule
mkBinAxiom String
"AddDef" TyCon
typeNatAddTyCon ((Integer -> Integer -> Maybe Type) -> CoAxiomRule)
-> (Integer -> Integer -> Maybe Type) -> CoAxiomRule
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)

axMulDef :: CoAxiomRule
axMulDef = String
-> TyCon -> (Integer -> Integer -> Maybe Type) -> CoAxiomRule
mkBinAxiom String
"MulDef" TyCon
typeNatMulTyCon ((Integer -> Integer -> Maybe Type) -> CoAxiomRule)
-> (Integer -> Integer -> Maybe Type) -> CoAxiomRule
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)

axExpDef :: CoAxiomRule
axExpDef = String
-> TyCon -> (Integer -> Integer -> Maybe Type) -> CoAxiomRule
mkBinAxiom String
"ExpDef" TyCon
typeNatExpTyCon ((Integer -> Integer -> Maybe Type) -> CoAxiomRule)
-> (Integer -> Integer -> Maybe Type) -> CoAxiomRule
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 b. (Num a, Integral b) => a -> b -> a
^ Integer
y)

axLeqDef :: CoAxiomRule
axLeqDef = String
-> TyCon -> (Integer -> Integer -> Maybe Type) -> CoAxiomRule
mkBinAxiom String
"LeqDef" TyCon
typeNatLeqTyCon ((Integer -> Integer -> Maybe Type) -> CoAxiomRule)
-> (Integer -> Integer -> Maybe Type) -> CoAxiomRule
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
$ Bool -> Type
bool (Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
y)

axCmpNatDef :: CoAxiomRule
axCmpNatDef   = String
-> TyCon -> (Integer -> Integer -> Maybe Type) -> CoAxiomRule
mkBinAxiom String
"CmpNatDef" TyCon
typeNatCmpTyCon
              ((Integer -> Integer -> Maybe Type) -> CoAxiomRule)
-> (Integer -> Integer -> Maybe Type) -> CoAxiomRule
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
$ Ordering -> Type
ordering (Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Integer
x Integer
y)

axCmpSymbolDef :: CoAxiomRule
axCmpSymbolDef =
  CoAxiomRule :: FastString
-> [Role] -> Role -> ([TypeEqn] -> Maybe TypeEqn) -> CoAxiomRule
CoAxiomRule
    { coaxrName :: FastString
coaxrName      = String -> FastString
fsLit String
"CmpSymbolDef"
    , coaxrAsmpRoles :: [Role]
coaxrAsmpRoles = [Role
Nominal, Role
Nominal]
    , coaxrRole :: Role
coaxrRole      = Role
Nominal
    , coaxrProves :: [TypeEqn] -> Maybe TypeEqn
coaxrProves    = \[TypeEqn]
cs ->
        do [Pair Type
s1 Type
s2, Pair Type
t1 Type
t2] <- [TypeEqn] -> Maybe [TypeEqn]
forall (m :: * -> *) a. Monad m => a -> m a
return [TypeEqn]
cs
           FastString
s2' <- Type -> Maybe FastString
isStrLitTy Type
s2
           FastString
t2' <- Type -> Maybe FastString
isStrLitTy Type
t2
           TypeEqn -> Maybe TypeEqn
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCon -> [Type] -> Type
mkTyConApp TyCon
typeSymbolCmpTyCon [Type
s1,Type
t1] Type -> Type -> TypeEqn
===
                   Ordering -> Type
ordering (FastString -> FastString -> Ordering
forall a. Ord a => a -> a -> Ordering
compare FastString
s2' FastString
t2')) }

axAppendSymbolDef :: CoAxiomRule
axAppendSymbolDef = CoAxiomRule :: FastString
-> [Role] -> Role -> ([TypeEqn] -> Maybe TypeEqn) -> CoAxiomRule
CoAxiomRule
    { coaxrName :: FastString
coaxrName      = String -> FastString
fsLit String
"AppendSymbolDef"
    , coaxrAsmpRoles :: [Role]
coaxrAsmpRoles = [Role
Nominal, Role
Nominal]
    , coaxrRole :: Role
coaxrRole      = Role
Nominal
    , coaxrProves :: [TypeEqn] -> Maybe TypeEqn
coaxrProves    = \[TypeEqn]
cs ->
        do [Pair Type
s1 Type
s2, Pair Type
t1 Type
t2] <- [TypeEqn] -> Maybe [TypeEqn]
forall (m :: * -> *) a. Monad m => a -> m a
return [TypeEqn]
cs
           FastString
s2' <- Type -> Maybe FastString
isStrLitTy Type
s2
           FastString
t2' <- Type -> Maybe FastString
isStrLitTy Type
t2
           let z :: Type
z = FastString -> Type
mkStrLitTy (FastString -> FastString -> FastString
appendFS FastString
s2' FastString
t2')
           TypeEqn -> Maybe TypeEqn
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCon -> [Type] -> Type
mkTyConApp TyCon
typeSymbolAppendTyCon [Type
s1, Type
t1] Type -> Type -> TypeEqn
=== Type
z)
    }

axSubDef :: CoAxiomRule
axSubDef = String
-> TyCon -> (Integer -> Integer -> Maybe Type) -> CoAxiomRule
mkBinAxiom String
"SubDef" TyCon
typeNatSubTyCon ((Integer -> Integer -> Maybe Type) -> CoAxiomRule)
-> (Integer -> Integer -> Maybe Type) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$
              \Integer
x Integer
y -> (Integer -> Type) -> Maybe Integer -> Maybe Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Integer -> Type
num (Integer -> Integer -> Maybe Integer
minus Integer
x Integer
y)

axDivDef :: CoAxiomRule
axDivDef = String
-> TyCon -> (Integer -> Integer -> Maybe Type) -> CoAxiomRule
mkBinAxiom String
"DivDef" TyCon
typeNatDivTyCon ((Integer -> Integer -> Maybe Type) -> CoAxiomRule)
-> (Integer -> Integer -> Maybe Type) -> CoAxiomRule
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 (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))

axModDef :: CoAxiomRule
axModDef = String
-> TyCon -> (Integer -> Integer -> Maybe Type) -> CoAxiomRule
mkBinAxiom String
"ModDef" TyCon
typeNatModTyCon ((Integer -> Integer -> Maybe Type) -> CoAxiomRule)
-> (Integer -> Integer -> Maybe Type) -> CoAxiomRule
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 (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))

axLogDef :: CoAxiomRule
axLogDef = String -> TyCon -> (Integer -> Maybe Type) -> CoAxiomRule
mkUnAxiom String
"LogDef" TyCon
typeNatLogTyCon ((Integer -> Maybe Type) -> CoAxiomRule)
-> (Integer -> Maybe Type) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$
              \Integer
x -> do (Integer
a,Bool
_) <- Integer -> Integer -> Maybe (Integer, Bool)
genLog Integer
x Integer
2
                       Type -> Maybe Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Type
num Integer
a)

axAdd0L :: CoAxiomRule
axAdd0L     = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 String
"Add0L"    ((TypeEqn -> TypeEqn) -> CoAxiomRule)
-> (TypeEqn -> TypeEqn) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$ \(Pair Type
s Type
t) -> (Integer -> Type
num Integer
0 Type -> Type -> Type
.+. Type
s) Type -> Type -> TypeEqn
=== Type
t
axAdd0R :: CoAxiomRule
axAdd0R     = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 String
"Add0R"    ((TypeEqn -> TypeEqn) -> CoAxiomRule)
-> (TypeEqn -> TypeEqn) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$ \(Pair Type
s Type
t) -> (Type
s Type -> Type -> Type
.+. Integer -> Type
num Integer
0) Type -> Type -> TypeEqn
=== Type
t
axSub0R :: CoAxiomRule
axSub0R     = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 String
"Sub0R"    ((TypeEqn -> TypeEqn) -> CoAxiomRule)
-> (TypeEqn -> TypeEqn) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$ \(Pair Type
s Type
t) -> (Type
s Type -> Type -> Type
.-. Integer -> Type
num Integer
0) Type -> Type -> TypeEqn
=== Type
t
axMul0L :: CoAxiomRule
axMul0L     = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 String
"Mul0L"    ((TypeEqn -> TypeEqn) -> CoAxiomRule)
-> (TypeEqn -> TypeEqn) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$ \(Pair Type
s Type
_) -> (Integer -> Type
num Integer
0 Type -> Type -> Type
.*. Type
s) Type -> Type -> TypeEqn
=== Integer -> Type
num Integer
0
axMul0R :: CoAxiomRule
axMul0R     = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 String
"Mul0R"    ((TypeEqn -> TypeEqn) -> CoAxiomRule)
-> (TypeEqn -> TypeEqn) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$ \(Pair Type
s Type
_) -> (Type
s Type -> Type -> Type
.*. Integer -> Type
num Integer
0) Type -> Type -> TypeEqn
=== Integer -> Type
num Integer
0
axMul1L :: CoAxiomRule
axMul1L     = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 String
"Mul1L"    ((TypeEqn -> TypeEqn) -> CoAxiomRule)
-> (TypeEqn -> TypeEqn) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$ \(Pair Type
s Type
t) -> (Integer -> Type
num Integer
1 Type -> Type -> Type
.*. Type
s) Type -> Type -> TypeEqn
=== Type
t
axMul1R :: CoAxiomRule
axMul1R     = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 String
"Mul1R"    ((TypeEqn -> TypeEqn) -> CoAxiomRule)
-> (TypeEqn -> TypeEqn) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$ \(Pair Type
s Type
t) -> (Type
s Type -> Type -> Type
.*. Integer -> Type
num Integer
1) Type -> Type -> TypeEqn
=== Type
t
axDiv1 :: CoAxiomRule
axDiv1      = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 String
"Div1"     ((TypeEqn -> TypeEqn) -> CoAxiomRule)
-> (TypeEqn -> TypeEqn) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$ \(Pair Type
s Type
t) -> (Type -> Type -> Type
tDiv Type
s (Integer -> Type
num Integer
1) Type -> Type -> TypeEqn
=== Type
t)
axMod1 :: CoAxiomRule
axMod1      = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 String
"Mod1"     ((TypeEqn -> TypeEqn) -> CoAxiomRule)
-> (TypeEqn -> TypeEqn) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$ \(Pair Type
s Type
_) -> (Type -> Type -> Type
tMod Type
s (Integer -> Type
num Integer
1) Type -> Type -> TypeEqn
=== Integer -> Type
num Integer
0)
                                    -- XXX: Shouldn't we check that _ is 0?
axExp1L :: CoAxiomRule
axExp1L     = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 String
"Exp1L"    ((TypeEqn -> TypeEqn) -> CoAxiomRule)
-> (TypeEqn -> TypeEqn) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$ \(Pair Type
s Type
_) -> (Integer -> Type
num Integer
1 Type -> Type -> Type
.^. Type
s) Type -> Type -> TypeEqn
=== Integer -> Type
num Integer
1
axExp0R :: CoAxiomRule
axExp0R     = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 String
"Exp0R"    ((TypeEqn -> TypeEqn) -> CoAxiomRule)
-> (TypeEqn -> TypeEqn) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$ \(Pair Type
s Type
_) -> (Type
s Type -> Type -> Type
.^. Integer -> Type
num Integer
0) Type -> Type -> TypeEqn
=== Integer -> Type
num Integer
1
axExp1R :: CoAxiomRule
axExp1R     = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 String
"Exp1R"    ((TypeEqn -> TypeEqn) -> CoAxiomRule)
-> (TypeEqn -> TypeEqn) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$ \(Pair Type
s Type
t) -> (Type
s Type -> Type -> Type
.^. Integer -> Type
num Integer
1) Type -> Type -> TypeEqn
=== Type
t
axLeqRefl :: CoAxiomRule
axLeqRefl   = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 String
"LeqRefl"  ((TypeEqn -> TypeEqn) -> CoAxiomRule)
-> (TypeEqn -> TypeEqn) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$ \(Pair Type
s Type
_) -> (Type
s Type -> Type -> Type
<== Type
s) Type -> Type -> TypeEqn
=== Bool -> Type
bool Bool
True
axCmpNatRefl :: CoAxiomRule
axCmpNatRefl    = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 String
"CmpNatRefl"
                ((TypeEqn -> TypeEqn) -> CoAxiomRule)
-> (TypeEqn -> TypeEqn) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$ \(Pair Type
s Type
_) -> (Type -> Type -> Type
cmpNat Type
s Type
s) Type -> Type -> TypeEqn
=== Ordering -> Type
ordering Ordering
EQ
axCmpSymbolRefl :: CoAxiomRule
axCmpSymbolRefl = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 String
"CmpSymbolRefl"
                ((TypeEqn -> TypeEqn) -> CoAxiomRule)
-> (TypeEqn -> TypeEqn) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$ \(Pair Type
s Type
_) -> (Type -> Type -> Type
cmpSymbol Type
s Type
s) Type -> Type -> TypeEqn
=== Ordering -> Type
ordering Ordering
EQ
axLeq0L :: CoAxiomRule
axLeq0L     = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 String
"Leq0L"    ((TypeEqn -> TypeEqn) -> CoAxiomRule)
-> (TypeEqn -> TypeEqn) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$ \(Pair Type
s Type
_) -> (Integer -> Type
num Integer
0 Type -> Type -> Type
<== Type
s) Type -> Type -> TypeEqn
=== Bool -> Type
bool Bool
True
axAppendSymbol0R :: CoAxiomRule
axAppendSymbol0R  = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 String
"Concat0R"
            ((TypeEqn -> TypeEqn) -> CoAxiomRule)
-> (TypeEqn -> TypeEqn) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$ \(Pair Type
s Type
t) -> (FastString -> Type
mkStrLitTy FastString
nilFS Type -> Type -> Type
`appendSymbol` Type
s) Type -> Type -> TypeEqn
=== Type
t
axAppendSymbol0L :: CoAxiomRule
axAppendSymbol0L  = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 String
"Concat0L"
            ((TypeEqn -> TypeEqn) -> CoAxiomRule)
-> (TypeEqn -> TypeEqn) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$ \(Pair Type
s Type
t) -> (Type
s Type -> Type -> Type
`appendSymbol` FastString -> Type
mkStrLitTy FastString
nilFS) Type -> Type -> TypeEqn
=== Type
t

-- 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 :: Map.Map FastString CoAxiomRule
typeNatCoAxiomRules :: Map FastString CoAxiomRule
typeNatCoAxiomRules = [(FastString, CoAxiomRule)] -> Map FastString CoAxiomRule
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(FastString, CoAxiomRule)] -> Map FastString CoAxiomRule)
-> [(FastString, CoAxiomRule)] -> Map FastString CoAxiomRule
forall a b. (a -> b) -> a -> b
$ (CoAxiomRule -> (FastString, CoAxiomRule))
-> [CoAxiomRule] -> [(FastString, CoAxiomRule)]
forall a b. (a -> b) -> [a] -> [b]
map (\CoAxiomRule
x -> (CoAxiomRule -> FastString
coaxrName CoAxiomRule
x, CoAxiomRule
x))
  [ CoAxiomRule
axAddDef
  , CoAxiomRule
axMulDef
  , CoAxiomRule
axExpDef
  , CoAxiomRule
axLeqDef
  , CoAxiomRule
axCmpNatDef
  , CoAxiomRule
axCmpSymbolDef
  , CoAxiomRule
axAppendSymbolDef
  , CoAxiomRule
axAdd0L
  , CoAxiomRule
axAdd0R
  , CoAxiomRule
axMul0L
  , CoAxiomRule
axMul0R
  , CoAxiomRule
axMul1L
  , CoAxiomRule
axMul1R
  , CoAxiomRule
axExp1L
  , CoAxiomRule
axExp0R
  , CoAxiomRule
axExp1R
  , CoAxiomRule
axLeqRefl
  , CoAxiomRule
axCmpNatRefl
  , CoAxiomRule
axCmpSymbolRefl
  , CoAxiomRule
axLeq0L
  , CoAxiomRule
axSubDef
  , CoAxiomRule
axSub0R
  , CoAxiomRule
axAppendSymbol0R
  , CoAxiomRule
axAppendSymbol0L
  , CoAxiomRule
axDivDef
  , CoAxiomRule
axDiv1
  , CoAxiomRule
axModDef
  , CoAxiomRule
axMod1
  , CoAxiomRule
axLogDef
  ]



{-------------------------------------------------------------------------------
Various utilities for making axioms and types
-------------------------------------------------------------------------------}

(.+.) :: Type -> Type -> Type
Type
s .+. :: Type -> Type -> Type
.+. Type
t = TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatAddTyCon [Type
s,Type
t]

(.-.) :: Type -> Type -> Type
Type
s .-. :: Type -> Type -> Type
.-. Type
t = TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatSubTyCon [Type
s,Type
t]

(.*.) :: Type -> Type -> Type
Type
s .*. :: Type -> Type -> Type
.*. Type
t = TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatMulTyCon [Type
s,Type
t]

tDiv :: Type -> Type -> Type
tDiv :: Type -> Type -> Type
tDiv Type
s Type
t = TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatDivTyCon [Type
s,Type
t]

tMod :: Type -> Type -> Type
tMod :: Type -> Type -> Type
tMod Type
s Type
t = TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatModTyCon [Type
s,Type
t]

(.^.) :: Type -> Type -> Type
Type
s .^. :: Type -> Type -> Type
.^. Type
t = TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatExpTyCon [Type
s,Type
t]

(<==) :: Type -> Type -> Type
Type
s <== :: Type -> Type -> Type
<== Type
t = TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatLeqTyCon [Type
s,Type
t]

cmpNat :: Type -> Type -> Type
cmpNat :: Type -> Type -> Type
cmpNat Type
s Type
t = TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatCmpTyCon [Type
s,Type
t]

cmpSymbol :: Type -> Type -> Type
cmpSymbol :: Type -> Type -> Type
cmpSymbol Type
s Type
t = TyCon -> [Type] -> Type
mkTyConApp TyCon
typeSymbolCmpTyCon [Type
s,Type
t]

appendSymbol :: Type -> Type -> Type
appendSymbol :: Type -> Type -> Type
appendSymbol Type
s Type
t = TyCon -> [Type] -> Type
mkTyConApp TyCon
typeSymbolAppendTyCon [Type
s, Type
t]

(===) :: Type -> Type -> Pair Type
Type
x === :: Type -> Type -> TypeEqn
=== Type
y = Type -> Type -> TypeEqn
forall a. a -> a -> Pair a
Pair Type
x Type
y

num :: Integer -> Type
num :: Integer -> Type
num = Integer -> Type
mkNumLitTy

bool :: Bool -> Type
bool :: Bool -> Type
bool Bool
b = if Bool
b then TyCon -> [Type] -> Type
mkTyConApp TyCon
promotedTrueDataCon []
              else TyCon -> [Type] -> Type
mkTyConApp TyCon
promotedFalseDataCon []

isBoolLitTy :: Type -> Maybe Bool
isBoolLitTy :: Type -> Maybe Bool
isBoolLitTy Type
tc =
  do (TyCon
tc,[]) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
tc
     case () of
       ()
_ | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
promotedFalseDataCon -> Bool -> Maybe Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
         | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
promotedTrueDataCon  -> Bool -> Maybe Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
         | Bool
otherwise                   -> Maybe Bool
forall a. Maybe a
Nothing

orderingKind :: Kind
orderingKind :: Type
orderingKind = TyCon -> [Type] -> Type
mkTyConApp TyCon
orderingTyCon []

ordering :: Ordering -> Type
ordering :: Ordering -> Type
ordering Ordering
o =
  case Ordering
o of
    Ordering
LT -> TyCon -> [Type] -> Type
mkTyConApp TyCon
promotedLTDataCon []
    Ordering
EQ -> TyCon -> [Type] -> Type
mkTyConApp TyCon
promotedEQDataCon []
    Ordering
GT -> TyCon -> [Type] -> Type
mkTyConApp TyCon
promotedGTDataCon []

isOrderingLitTy :: Type -> Maybe Ordering
isOrderingLitTy :: Type -> Maybe Ordering
isOrderingLitTy Type
tc =
  do (TyCon
tc1,[]) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
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 (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 (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 (m :: * -> *) a. Monad m => a -> m a
return Ordering
GT
         | Bool
otherwise                -> Maybe Ordering
forall a. Maybe a
Nothing

known :: (Integer -> Bool) -> TcType -> Bool
known :: (Integer -> Bool) -> Type -> Bool
known Integer -> Bool
p Type
x = case Type -> Maybe Integer
isNumLitTy Type
x of
              Just Integer
a  -> Integer -> Bool
p Integer
a
              Maybe Integer
Nothing -> Bool
False


mkUnAxiom :: String -> TyCon -> (Integer -> Maybe Type) -> CoAxiomRule
mkUnAxiom :: String -> TyCon -> (Integer -> Maybe Type) -> CoAxiomRule
mkUnAxiom String
str TyCon
tc Integer -> Maybe Type
f =
  CoAxiomRule :: FastString
-> [Role] -> Role -> ([TypeEqn] -> Maybe TypeEqn) -> CoAxiomRule
CoAxiomRule
    { coaxrName :: FastString
coaxrName      = String -> FastString
fsLit String
str
    , coaxrAsmpRoles :: [Role]
coaxrAsmpRoles = [Role
Nominal]
    , coaxrRole :: Role
coaxrRole      = Role
Nominal
    , coaxrProves :: [TypeEqn] -> Maybe TypeEqn
coaxrProves    = \[TypeEqn]
cs ->
        do [Pair Type
s1 Type
s2] <- [TypeEqn] -> Maybe [TypeEqn]
forall (m :: * -> *) a. Monad m => a -> m a
return [TypeEqn]
cs
           Integer
s2' <- Type -> Maybe Integer
isNumLitTy Type
s2
           Type
z   <- Integer -> Maybe Type
f Integer
s2'
           TypeEqn -> Maybe TypeEqn
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type
s1] Type -> Type -> TypeEqn
=== Type
z)
    }



-- For the definitional axioms
mkBinAxiom :: String -> TyCon ->
              (Integer -> Integer -> Maybe Type) -> CoAxiomRule
mkBinAxiom :: String
-> TyCon -> (Integer -> Integer -> Maybe Type) -> CoAxiomRule
mkBinAxiom String
str TyCon
tc Integer -> Integer -> Maybe Type
f =
  CoAxiomRule :: FastString
-> [Role] -> Role -> ([TypeEqn] -> Maybe TypeEqn) -> CoAxiomRule
CoAxiomRule
    { coaxrName :: FastString
coaxrName      = String -> FastString
fsLit String
str
    , coaxrAsmpRoles :: [Role]
coaxrAsmpRoles = [Role
Nominal, Role
Nominal]
    , coaxrRole :: Role
coaxrRole      = Role
Nominal
    , coaxrProves :: [TypeEqn] -> Maybe TypeEqn
coaxrProves    = \[TypeEqn]
cs ->
        do [Pair Type
s1 Type
s2, Pair Type
t1 Type
t2] <- [TypeEqn] -> Maybe [TypeEqn]
forall (m :: * -> *) a. Monad m => a -> m a
return [TypeEqn]
cs
           Integer
s2' <- Type -> Maybe Integer
isNumLitTy Type
s2
           Integer
t2' <- Type -> Maybe Integer
isNumLitTy Type
t2
           Type
z   <- Integer -> Integer -> Maybe Type
f Integer
s2' Integer
t2'
           TypeEqn -> Maybe TypeEqn
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type
s1,Type
t1] Type -> Type -> TypeEqn
=== Type
z)
    }



mkAxiom1 :: String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 :: String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 String
str TypeEqn -> TypeEqn
f =
  CoAxiomRule :: FastString
-> [Role] -> Role -> ([TypeEqn] -> Maybe TypeEqn) -> CoAxiomRule
CoAxiomRule
    { coaxrName :: FastString
coaxrName      = String -> FastString
fsLit String
str
    , coaxrAsmpRoles :: [Role]
coaxrAsmpRoles = [Role
Nominal]
    , coaxrRole :: Role
coaxrRole      = Role
Nominal
    , coaxrProves :: [TypeEqn] -> Maybe TypeEqn
coaxrProves    = \case [TypeEqn
eqn] -> TypeEqn -> Maybe TypeEqn
forall a. a -> Maybe a
Just (TypeEqn -> TypeEqn
f TypeEqn
eqn)
                             [TypeEqn]
_     -> Maybe TypeEqn
forall a. Maybe a
Nothing
    }


{-------------------------------------------------------------------------------
Evaluation
-------------------------------------------------------------------------------}

matchFamAdd :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamAdd :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamAdd [Type
s,Type
t]
  | Just Integer
0 <- Maybe Integer
mbX = (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axAdd0L, [Type
t], Type
t)
  | Just Integer
0 <- Maybe Integer
mbY = (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axAdd0R, [Type
s], Type
s)
  | Just Integer
x <- Maybe Integer
mbX, Just Integer
y <- Maybe Integer
mbY =
    (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axAddDef, [Type
s,Type
t], Integer -> Type
num (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
y))
  where mbX :: Maybe Integer
mbX = Type -> Maybe Integer
isNumLitTy Type
s
        mbY :: Maybe Integer
mbY = Type -> Maybe Integer
isNumLitTy Type
t
matchFamAdd [Type]
_ = Maybe (CoAxiomRule, [Type], Type)
forall a. Maybe a
Nothing

matchFamSub :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamSub :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamSub [Type
s,Type
t]
  | Just Integer
0 <- Maybe Integer
mbY = (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axSub0R, [Type
s], Type
s)
  | Just Integer
x <- Maybe Integer
mbX, Just Integer
y <- Maybe Integer
mbY, Just Integer
z <- Integer -> Integer -> Maybe Integer
minus Integer
x Integer
y =
    (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axSubDef, [Type
s,Type
t], Integer -> Type
num Integer
z)
  where mbX :: Maybe Integer
mbX = Type -> Maybe Integer
isNumLitTy Type
s
        mbY :: Maybe Integer
mbY = Type -> Maybe Integer
isNumLitTy Type
t
matchFamSub [Type]
_ = Maybe (CoAxiomRule, [Type], Type)
forall a. Maybe a
Nothing

matchFamMul :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamMul :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamMul [Type
s,Type
t]
  | Just Integer
0 <- Maybe Integer
mbX = (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axMul0L, [Type
t], Integer -> Type
num Integer
0)
  | Just Integer
0 <- Maybe Integer
mbY = (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axMul0R, [Type
s], Integer -> Type
num Integer
0)
  | Just Integer
1 <- Maybe Integer
mbX = (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axMul1L, [Type
t], Type
t)
  | Just Integer
1 <- Maybe Integer
mbY = (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axMul1R, [Type
s], Type
s)
  | Just Integer
x <- Maybe Integer
mbX, Just Integer
y <- Maybe Integer
mbY =
    (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axMulDef, [Type
s,Type
t], Integer -> Type
num (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
y))
  where mbX :: Maybe Integer
mbX = Type -> Maybe Integer
isNumLitTy Type
s
        mbY :: Maybe Integer
mbY = Type -> Maybe Integer
isNumLitTy Type
t
matchFamMul [Type]
_ = Maybe (CoAxiomRule, [Type], Type)
forall a. Maybe a
Nothing

matchFamDiv :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamDiv :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamDiv [Type
s,Type
t]
  | Just Integer
1 <- Maybe Integer
mbY = (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axDiv1, [Type
s], Type
s)
  | Just Integer
x <- Maybe Integer
mbX, Just Integer
y <- Maybe Integer
mbY, Integer
y Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0 = (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axDivDef, [Type
s,Type
t], Integer -> Type
num (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div Integer
x Integer
y))
  where mbX :: Maybe Integer
mbX = Type -> Maybe Integer
isNumLitTy Type
s
        mbY :: Maybe Integer
mbY = Type -> Maybe Integer
isNumLitTy Type
t
matchFamDiv [Type]
_ = Maybe (CoAxiomRule, [Type], Type)
forall a. Maybe a
Nothing

matchFamMod :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamMod :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamMod [Type
s,Type
t]
  | Just Integer
1 <- Maybe Integer
mbY = (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axMod1, [Type
s], Integer -> Type
num Integer
0)
  | Just Integer
x <- Maybe Integer
mbX, Just Integer
y <- Maybe Integer
mbY, Integer
y Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0 = (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axModDef, [Type
s,Type
t], Integer -> Type
num (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
mod Integer
x Integer
y))
  where mbX :: Maybe Integer
mbX = Type -> Maybe Integer
isNumLitTy Type
s
        mbY :: Maybe Integer
mbY = Type -> Maybe Integer
isNumLitTy Type
t
matchFamMod [Type]
_ = Maybe (CoAxiomRule, [Type], Type)
forall a. Maybe a
Nothing



matchFamExp :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamExp :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamExp [Type
s,Type
t]
  | Just Integer
0 <- Maybe Integer
mbY = (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axExp0R, [Type
s], Integer -> Type
num Integer
1)
  | Just Integer
1 <- Maybe Integer
mbX = (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axExp1L, [Type
t], Integer -> Type
num Integer
1)
  | Just Integer
1 <- Maybe Integer
mbY = (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axExp1R, [Type
s], Type
s)
  | Just Integer
x <- Maybe Integer
mbX, Just Integer
y <- Maybe Integer
mbY =
    (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axExpDef, [Type
s,Type
t], Integer -> Type
num (Integer
x Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
y))
  where mbX :: Maybe Integer
mbX = Type -> Maybe Integer
isNumLitTy Type
s
        mbY :: Maybe Integer
mbY = Type -> Maybe Integer
isNumLitTy Type
t
matchFamExp [Type]
_ = Maybe (CoAxiomRule, [Type], Type)
forall a. Maybe a
Nothing

matchFamLog :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamLog :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamLog [Type
s]
  | Just Integer
x <- Maybe Integer
mbX, Just (Integer
n,Bool
_) <- Integer -> Integer -> Maybe (Integer, Bool)
genLog Integer
x Integer
2 = (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axLogDef, [Type
s], Integer -> Type
num Integer
n)
  where mbX :: Maybe Integer
mbX = Type -> Maybe Integer
isNumLitTy Type
s
matchFamLog [Type]
_ = Maybe (CoAxiomRule, [Type], Type)
forall a. Maybe a
Nothing


matchFamLeq :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamLeq :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamLeq [Type
s,Type
t]
  | Just Integer
0 <- Maybe Integer
mbX = (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axLeq0L, [Type
t], Bool -> Type
bool Bool
True)
  | Just Integer
x <- Maybe Integer
mbX, Just Integer
y <- Maybe Integer
mbY =
    (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axLeqDef, [Type
s,Type
t], Bool -> Type
bool (Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
y))
  | HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
tcEqType Type
s Type
t  = (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axLeqRefl, [Type
s], Bool -> Type
bool Bool
True)
  where mbX :: Maybe Integer
mbX = Type -> Maybe Integer
isNumLitTy Type
s
        mbY :: Maybe Integer
mbY = Type -> Maybe Integer
isNumLitTy Type
t
matchFamLeq [Type]
_ = Maybe (CoAxiomRule, [Type], Type)
forall a. Maybe a
Nothing

matchFamCmpNat :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamCmpNat :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamCmpNat [Type
s,Type
t]
  | Just Integer
x <- Maybe Integer
mbX, Just Integer
y <- Maybe Integer
mbY =
    (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axCmpNatDef, [Type
s,Type
t], Ordering -> Type
ordering (Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Integer
x Integer
y))
  | HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
tcEqType Type
s Type
t = (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axCmpNatRefl, [Type
s], Ordering -> Type
ordering Ordering
EQ)
  where mbX :: Maybe Integer
mbX = Type -> Maybe Integer
isNumLitTy Type
s
        mbY :: Maybe Integer
mbY = Type -> Maybe Integer
isNumLitTy Type
t
matchFamCmpNat [Type]
_ = Maybe (CoAxiomRule, [Type], Type)
forall a. Maybe a
Nothing

matchFamCmpSymbol :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamCmpSymbol :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamCmpSymbol [Type
s,Type
t]
  | Just FastString
x <- Maybe FastString
mbX, Just FastString
y <- Maybe FastString
mbY =
    (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axCmpSymbolDef, [Type
s,Type
t], Ordering -> Type
ordering (FastString -> FastString -> Ordering
forall a. Ord a => a -> a -> Ordering
compare FastString
x FastString
y))
  | HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
tcEqType Type
s Type
t = (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axCmpSymbolRefl, [Type
s], Ordering -> Type
ordering Ordering
EQ)
  where mbX :: Maybe FastString
mbX = Type -> Maybe FastString
isStrLitTy Type
s
        mbY :: Maybe FastString
mbY = Type -> Maybe FastString
isStrLitTy Type
t
matchFamCmpSymbol [Type]
_ = Maybe (CoAxiomRule, [Type], Type)
forall a. Maybe a
Nothing

matchFamAppendSymbol :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamAppendSymbol :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamAppendSymbol [Type
s,Type
t]
  | Just FastString
x <- Maybe FastString
mbX, FastString -> Bool
nullFS FastString
x = (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axAppendSymbol0R, [Type
t], Type
t)
  | Just FastString
y <- Maybe FastString
mbY, FastString -> Bool
nullFS FastString
y = (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axAppendSymbol0L, [Type
s], Type
s)
  | Just FastString
x <- Maybe FastString
mbX, Just FastString
y <- Maybe FastString
mbY =
    (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axAppendSymbolDef, [Type
s,Type
t], FastString -> Type
mkStrLitTy (FastString -> FastString -> FastString
appendFS FastString
x FastString
y))
  where
  mbX :: Maybe FastString
mbX = Type -> Maybe FastString
isStrLitTy Type
s
  mbY :: Maybe FastString
mbY = Type -> Maybe FastString
isStrLitTy Type
t
matchFamAppendSymbol [Type]
_ = Maybe (CoAxiomRule, [Type], Type)
forall a. Maybe a
Nothing

{-------------------------------------------------------------------------------
Interact with axioms
-------------------------------------------------------------------------------}

interactTopAdd :: [Xi] -> Xi -> [Pair Type]
interactTopAdd :: [Type] -> Type -> [TypeEqn]
interactTopAdd [Type
s,Type
t] Type
r
  | Just Integer
0 <- Maybe Integer
mbZ = [ Type
s Type -> Type -> TypeEqn
=== Integer -> Type
num Integer
0, Type
t Type -> Type -> TypeEqn
=== Integer -> Type
num Integer
0 ]                          -- (s + t ~ 0) => (s ~ 0, t ~ 0)
  | Just Integer
x <- Maybe Integer
mbX, Just Integer
z <- Maybe Integer
mbZ, Just Integer
y <- Integer -> Integer -> Maybe Integer
minus Integer
z Integer
x = [Type
t Type -> Type -> TypeEqn
=== Integer -> Type
num Integer
y]     -- (5 + t ~ 8) => (t ~ 3)
  | Just Integer
y <- Maybe Integer
mbY, Just Integer
z <- Maybe Integer
mbZ, Just Integer
x <- Integer -> Integer -> Maybe Integer
minus Integer
z Integer
y = [Type
s Type -> Type -> TypeEqn
=== Integer -> Type
num Integer
x]     -- (s + 5 ~ 8) => (s ~ 3)
  where
  mbX :: Maybe Integer
mbX = Type -> Maybe Integer
isNumLitTy Type
s
  mbY :: Maybe Integer
mbY = Type -> Maybe Integer
isNumLitTy Type
t
  mbZ :: Maybe Integer
mbZ = Type -> Maybe Integer
isNumLitTy Type
r
interactTopAdd [Type]
_ Type
_ = []

{-
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.
-}
interactTopSub :: [Xi] -> Xi -> [Pair Type]
interactTopSub :: [Type] -> Type -> [TypeEqn]
interactTopSub [Type
s,Type
t] Type
r
  | Just Integer
z <- Maybe Integer
mbZ = [ Type
s Type -> Type -> TypeEqn
=== (Integer -> Type
num Integer
z Type -> Type -> Type
.+. Type
t) ]         -- (s - t ~ 5) => (5 + t ~ s)
  where
  mbZ :: Maybe Integer
mbZ = Type -> Maybe Integer
isNumLitTy Type
r
interactTopSub [Type]
_ Type
_ = []





interactTopMul :: [Xi] -> Xi -> [Pair Type]
interactTopMul :: [Type] -> Type -> [TypeEqn]
interactTopMul [Type
s,Type
t] Type
r
  | Just Integer
1 <- Maybe Integer
mbZ = [ Type
s Type -> Type -> TypeEqn
=== Integer -> Type
num Integer
1, Type
t Type -> Type -> TypeEqn
=== Integer -> Type
num Integer
1 ]                        -- (s * t ~ 1)  => (s ~ 1, t ~ 1)
  | Just Integer
x <- Maybe Integer
mbX, Just Integer
z <- Maybe Integer
mbZ, Just Integer
y <- Integer -> Integer -> Maybe Integer
divide Integer
z Integer
x = [Type
t Type -> Type -> TypeEqn
=== Integer -> Type
num Integer
y]  -- (3 * t ~ 15) => (t ~ 5)
  | Just Integer
y <- Maybe Integer
mbY, Just Integer
z <- Maybe Integer
mbZ, Just Integer
x <- Integer -> Integer -> Maybe Integer
divide Integer
z Integer
y = [Type
s Type -> Type -> TypeEqn
=== Integer -> Type
num Integer
x]  -- (s * 3 ~ 15) => (s ~ 5)
  where
  mbX :: Maybe Integer
mbX = Type -> Maybe Integer
isNumLitTy Type
s
  mbY :: Maybe Integer
mbY = Type -> Maybe Integer
isNumLitTy Type
t
  mbZ :: Maybe Integer
mbZ = Type -> Maybe Integer
isNumLitTy Type
r
interactTopMul [Type]
_ Type
_ = []

interactTopDiv :: [Xi] -> Xi -> [Pair Type]
interactTopDiv :: [Type] -> Type -> [TypeEqn]
interactTopDiv [Type]
_ Type
_ = []   -- I can't think of anything...

interactTopMod :: [Xi] -> Xi -> [Pair Type]
interactTopMod :: [Type] -> Type -> [TypeEqn]
interactTopMod [Type]
_ Type
_ = []   -- I can't think of anything...

interactTopExp :: [Xi] -> Xi -> [Pair Type]
interactTopExp :: [Type] -> Type -> [TypeEqn]
interactTopExp [Type
s,Type
t] Type
r
  | Just Integer
0 <- Maybe Integer
mbZ = [ Type
s Type -> Type -> TypeEqn
=== Integer -> Type
num Integer
0 ]                                       -- (s ^ t ~ 0) => (s ~ 0)
  | Just Integer
x <- Maybe Integer
mbX, Just Integer
z <- Maybe Integer
mbZ, Just Integer
y <- Integer -> Integer -> Maybe Integer
logExact  Integer
z Integer
x = [Type
t Type -> Type -> TypeEqn
=== Integer -> Type
num Integer
y] -- (2 ^ t ~ 8) => (t ~ 3)
  | Just Integer
y <- Maybe Integer
mbY, Just Integer
z <- Maybe Integer
mbZ, Just Integer
x <- Integer -> Integer -> Maybe Integer
rootExact Integer
z Integer
y = [Type
s Type -> Type -> TypeEqn
=== Integer -> Type
num Integer
x] -- (s ^ 2 ~ 9) => (s ~ 3)
  where
  mbX :: Maybe Integer
mbX = Type -> Maybe Integer
isNumLitTy Type
s
  mbY :: Maybe Integer
mbY = Type -> Maybe Integer
isNumLitTy Type
t
  mbZ :: Maybe Integer
mbZ = Type -> Maybe Integer
isNumLitTy Type
r
interactTopExp [Type]
_ Type
_ = []

interactTopLog :: [Xi] -> Xi -> [Pair Type]
interactTopLog :: [Type] -> Type -> [TypeEqn]
interactTopLog [Type]
_ Type
_ = []   -- I can't think of anything...



interactTopLeq :: [Xi] -> Xi -> [Pair Type]
interactTopLeq :: [Type] -> Type -> [TypeEqn]
interactTopLeq [Type
s,Type
t] Type
r
  | Just Integer
0 <- Maybe Integer
mbY, Just Bool
True <- Maybe Bool
mbZ = [ Type
s Type -> Type -> TypeEqn
=== Integer -> Type
num Integer
0 ]                     -- (s <= 0) => (s ~ 0)
  where
  mbY :: Maybe Integer
mbY = Type -> Maybe Integer
isNumLitTy Type
t
  mbZ :: Maybe Bool
mbZ = Type -> Maybe Bool
isBoolLitTy Type
r
interactTopLeq [Type]
_ Type
_ = []

interactTopCmpNat :: [Xi] -> Xi -> [Pair Type]
interactTopCmpNat :: [Type] -> Type -> [TypeEqn]
interactTopCmpNat [Type
s,Type
t] Type
r
  | Just Ordering
EQ <- Type -> Maybe Ordering
isOrderingLitTy Type
r = [ Type
s Type -> Type -> TypeEqn
=== Type
t ]
interactTopCmpNat [Type]
_ Type
_ = []

interactTopCmpSymbol :: [Xi] -> Xi -> [Pair Type]
interactTopCmpSymbol :: [Type] -> Type -> [TypeEqn]
interactTopCmpSymbol [Type
s,Type
t] Type
r
  | Just Ordering
EQ <- Type -> Maybe Ordering
isOrderingLitTy Type
r = [ Type
s Type -> Type -> TypeEqn
=== Type
t ]
interactTopCmpSymbol [Type]
_ Type
_ = []

interactTopAppendSymbol :: [Xi] -> Xi -> [Pair Type]
interactTopAppendSymbol :: [Type] -> Type -> [TypeEqn]
interactTopAppendSymbol [Type
s,Type
t] Type
r
  -- (AppendSymbol a b ~ "") => (a ~ "", b ~ "")
  | Just FastString
z <- Maybe FastString
mbZ, FastString -> Bool
nullFS FastString
z =
    [Type
s Type -> Type -> TypeEqn
=== FastString -> Type
mkStrLitTy FastString
nilFS, Type
t Type -> Type -> TypeEqn
=== FastString -> Type
mkStrLitTy FastString
nilFS ]

  -- (AppendSymbol "foo" b ~ "foobar") => (b ~ "bar")
  | Just String
x <- (FastString -> String) -> Maybe FastString -> Maybe String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FastString -> String
unpackFS Maybe FastString
mbX, Just String
z <- (FastString -> String) -> Maybe FastString -> Maybe String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FastString -> String
unpackFS Maybe FastString
mbZ, String
x String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
z =
    [ Type
t Type -> Type -> TypeEqn
=== FastString -> Type
mkStrLitTy (String -> FastString
mkFastString (String -> FastString) -> String -> FastString
forall a b. (a -> b) -> a -> b
$ Int -> String -> String
forall a. Int -> [a] -> [a]
drop (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
x) String
z) ]

  -- (AppendSymbol f "bar" ~ "foobar") => (f ~ "foo")
  | Just String
y <- (FastString -> String) -> Maybe FastString -> Maybe String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FastString -> String
unpackFS Maybe FastString
mbY, Just String
z <- (FastString -> String) -> Maybe FastString -> Maybe String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FastString -> String
unpackFS Maybe FastString
mbZ, String
y String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isSuffixOf` String
z =
    [ Type
t Type -> Type -> TypeEqn
=== FastString -> Type
mkStrLitTy (String -> FastString
mkFastString (String -> FastString) -> String -> FastString
forall a b. (a -> b) -> a -> b
$ Int -> String -> String
forall a. Int -> [a] -> [a]
take (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
z Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
y) String
z) ]

  where
  mbX :: Maybe FastString
mbX = Type -> Maybe FastString
isStrLitTy Type
s
  mbY :: Maybe FastString
mbY = Type -> Maybe FastString
isStrLitTy Type
t
  mbZ :: Maybe FastString
mbZ = Type -> Maybe FastString
isStrLitTy Type
r

interactTopAppendSymbol [Type]
_ Type
_ = []

{-------------------------------------------------------------------------------
Interaction with inerts
-------------------------------------------------------------------------------}

interactInertAdd :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
interactInertAdd :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertAdd [Type
x1,Type
y1] Type
z1 [Type
x2,Type
y2] Type
z2
  | Bool
sameZ Bool -> Bool -> Bool
&& HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
tcEqType Type
x1 Type
x2         = [ Type
y1 Type -> Type -> TypeEqn
=== Type
y2 ]
  | Bool
sameZ Bool -> Bool -> Bool
&& HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
tcEqType Type
y1 Type
y2         = [ Type
x1 Type -> Type -> TypeEqn
=== Type
x2 ]
  where sameZ :: Bool
sameZ = HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
tcEqType Type
z1 Type
z2
interactInertAdd [Type]
_ Type
_ [Type]
_ Type
_ = []

interactInertSub :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
interactInertSub :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertSub [Type
x1,Type
y1] Type
z1 [Type
x2,Type
y2] Type
z2
  | Bool
sameZ Bool -> Bool -> Bool
&& HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
tcEqType Type
x1 Type
x2         = [ Type
y1 Type -> Type -> TypeEqn
=== Type
y2 ]
  | Bool
sameZ Bool -> Bool -> Bool
&& HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
tcEqType Type
y1 Type
y2         = [ Type
x1 Type -> Type -> TypeEqn
=== Type
x2 ]
  where sameZ :: Bool
sameZ = HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
tcEqType Type
z1 Type
z2
interactInertSub [Type]
_ Type
_ [Type]
_ Type
_ = []

interactInertMul :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
interactInertMul :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertMul [Type
x1,Type
y1] Type
z1 [Type
x2,Type
y2] Type
z2
  | Bool
sameZ Bool -> Bool -> Bool
&& (Integer -> Bool) -> Type -> Bool
known (Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0) Type
x1 Bool -> Bool -> Bool
&& HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
tcEqType Type
x1 Type
x2 = [ Type
y1 Type -> Type -> TypeEqn
=== Type
y2 ]
  | Bool
sameZ Bool -> Bool -> Bool
&& (Integer -> Bool) -> Type -> Bool
known (Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0) Type
y1 Bool -> Bool -> Bool
&& HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
tcEqType Type
y1 Type
y2 = [ Type
x1 Type -> Type -> TypeEqn
=== Type
x2 ]
  where sameZ :: Bool
sameZ   = HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
tcEqType Type
z1 Type
z2

interactInertMul [Type]
_ Type
_ [Type]
_ Type
_ = []

interactInertDiv :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
interactInertDiv :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertDiv [Type]
_ Type
_ [Type]
_ Type
_ = []

interactInertMod :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
interactInertMod :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertMod [Type]
_ Type
_ [Type]
_ Type
_ = []

interactInertExp :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
interactInertExp :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertExp [Type
x1,Type
y1] Type
z1 [Type
x2,Type
y2] Type
z2
  | Bool
sameZ Bool -> Bool -> Bool
&& (Integer -> Bool) -> Type -> Bool
known (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
1) Type
x1 Bool -> Bool -> Bool
&& HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
tcEqType Type
x1 Type
x2 = [ Type
y1 Type -> Type -> TypeEqn
=== Type
y2 ]
  | Bool
sameZ Bool -> Bool -> Bool
&& (Integer -> Bool) -> Type -> Bool
known (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0) Type
y1 Bool -> Bool -> Bool
&& HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
tcEqType Type
y1 Type
y2 = [ Type
x1 Type -> Type -> TypeEqn
=== Type
x2 ]
  where sameZ :: Bool
sameZ = HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
tcEqType Type
z1 Type
z2

interactInertExp [Type]
_ Type
_ [Type]
_ Type
_ = []

interactInertLog :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
interactInertLog :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertLog [Type]
_ Type
_ [Type]
_ Type
_ = []


interactInertLeq :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
interactInertLeq :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertLeq [Type
x1,Type
y1] Type
z1 [Type
x2,Type
y2] Type
z2
  | Bool
bothTrue Bool -> Bool -> Bool
&& HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
tcEqType Type
x1 Type
y2 Bool -> Bool -> Bool
&& HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
tcEqType Type
y1 Type
x2 = [ Type
x1 Type -> Type -> TypeEqn
=== Type
y1 ]
  | Bool
bothTrue Bool -> Bool -> Bool
&& HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
tcEqType Type
y1 Type
x2                 = [ (Type
x1 Type -> Type -> Type
<== Type
y2) Type -> Type -> TypeEqn
=== Bool -> Type
bool Bool
True ]
  | Bool
bothTrue Bool -> Bool -> Bool
&& HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
tcEqType Type
y2 Type
x1                 = [ (Type
x2 Type -> Type -> Type
<== Type
y1) Type -> Type -> TypeEqn
=== Bool -> Type
bool Bool
True ]
  where bothTrue :: Bool
bothTrue = Maybe () -> Bool
forall a. Maybe a -> Bool
isJust (Maybe () -> Bool) -> Maybe () -> Bool
forall a b. (a -> b) -> a -> b
$ do Bool
True <- Type -> Maybe Bool
isBoolLitTy Type
z1
                               Bool
True <- Type -> Maybe Bool
isBoolLitTy Type
z2
                               () -> Maybe ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

interactInertLeq [Type]
_ Type
_ [Type]
_ Type
_ = []


interactInertAppendSymbol :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
interactInertAppendSymbol :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertAppendSymbol [Type
x1,Type
y1] Type
z1 [Type
x2,Type
y2] Type
z2
  | Bool
sameZ Bool -> Bool -> Bool
&& HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
tcEqType Type
x1 Type
x2         = [ Type
y1 Type -> Type -> TypeEqn
=== Type
y2 ]
  | Bool
sameZ Bool -> Bool -> Bool
&& HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
tcEqType Type
y1 Type
y2         = [ Type
x1 Type -> Type -> TypeEqn
=== Type
x2 ]
  where sameZ :: Bool
sameZ = HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
tcEqType Type
z1 Type
z2
interactInertAppendSymbol [Type]
_ Type
_ [Type]
_ Type
_ = []



{- -----------------------------------------------------------------------------
These inverse functions are used for simplifying propositions using
concrete natural numbers.
----------------------------------------------------------------------------- -}

-- | Subtract two natural numbers.
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

-- | Compute the exact logarithm of a natural number.
-- The logarithm base is the second argument.
logExact :: Integer -> Integer -> Maybe Integer
logExact :: Integer -> Integer -> Maybe Integer
logExact Integer
x Integer
y = do (Integer
z,Bool
True) <- Integer -> Integer -> Maybe (Integer, Bool)
genLog Integer
x Integer
y
                  Integer -> Maybe Integer
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
z


-- | Divide two natural numbers.
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

-- | Compute the exact root of a natural number.
-- The second argument specifies which root we are computing.
rootExact :: Integer -> Integer -> Maybe Integer
rootExact :: Integer -> Integer -> Maybe Integer
rootExact Integer
x Integer
y = do (Integer
z,Bool
True) <- Integer -> Integer -> Maybe (Integer, Bool)
genRoot Integer
x Integer
y
                   Integer -> Maybe Integer
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
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 :: 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)

{- | 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 :: 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)
forall {a}. Num a => a -> Integer -> (a, Bool)
exactLoop Integer
0 Integer
x)
  where
  exactLoop :: a -> Integer -> (a, Bool)
exactLoop a
s Integer
i
    | Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1     = (a
s,Bool
True)
    | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
base   = (a
s,Bool
False)
    | Bool
otherwise  =
        let s1 :: a
s1 = a
s a -> a -> a
forall a. Num a => a -> a -> a
+ a
1
        in a
s1 a -> (a, Bool) -> (a, Bool)
`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    -> a -> Integer -> (a, Bool)
exactLoop a
s1 Integer
j
                        | Bool
otherwise -> (a -> Integer -> a
forall {t}. Num t => t -> Integer -> t
underLoop a
s1 Integer
j, Bool
False)

  underLoop :: t -> Integer -> t
underLoop t
s Integer
i
    | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
base  = t
s
    | Bool
otherwise = let s1 :: t
s1 = t
s t -> t -> t
forall a. Num a => a -> a -> a
+ t
1 in t
s1 t -> t -> t
`seq` t -> Integer -> t
underLoop t
s1 (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div Integer
i Integer
base)