{-# LANGUAGE LambdaCase #-}

module TcTypeNats
  ( 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 GhcPrelude

import Type
import Pair
import TcType     ( TcType, tcEqType )
import TyCon      ( TyCon, FamTyConFlav(..), mkFamilyTyCon
                  , Injectivity(..) )
import Coercion   ( Role(..) )
import TcRnTypes  ( Xi )
import CoAxiom    ( CoAxiomRule(..), BuiltInSynFamily(..), TypeEqn )
import Name       ( Name, BuiltInSyntax(..) )
import TysWiredIn
import TysPrim    ( mkTemplateAnonTyConBinders )
import PrelNames  ( gHC_TYPELITS
                  , gHC_TYPENATS
                  , typeNatAddTyFamNameKey
                  , typeNatMulTyFamNameKey
                  , typeNatExpTyFamNameKey
                  , typeNatLeqTyFamNameKey
                  , typeNatSubTyFamNameKey
                  , typeNatDivTyFamNameKey
                  , typeNatModTyFamNameKey
                  , typeNatLogTyFamNameKey
                  , typeNatCmpTyFamNameKey
                  , typeSymbolCmpTyFamNameKey
                  , typeSymbolAppendFamNameKey
                  )
import FastString ( FastString
                  , fsLit, nilFS, nullFS, unpackFS, mkFastString, appendFS
                  )
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 TcTypeNats, 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://ghc.haskell.org/trac/ghc/wiki/TypeNats

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 PrelNames. It will likely be of the form
  @myTyFamNameKey = mkPreludeTyConUnique xyz@, where @xyz@ is a number that
  has not been chosen before in PrelNames. There are several examples already
  in PrelNames—see, for instance, typeNatAddTyFamNameKey.

* Adding the type family TyCon itself

  This goes in TcTypeNats. 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 TcTypeNats. (Not doing so caused #14632.)
  - Include it in the typeNatTyCons list, defined in TcTypeNats.

* 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 TcTypeNats.
  (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 TcTypeNats,
  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 "+")
            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 "-")
            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 "*")
            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 "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 "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 "^")
                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 "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 "<=?")
                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 "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 = \_ _ _ _ -> []
    }

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 "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 = \_ _ _ _ -> []
    }

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 "AppendSymbol")
                Unique
typeSymbolAppendFamNameKey TyCon
typeSymbolAppendTyCon



-- Make a unary built-in constructor of kind: Nat -> Nat
mkTypeNatFunTyCon1 :: Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon1 :: Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon1 op :: Name
op tcb :: 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 op :: Name
op tcb :: 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 op :: Name
op tcb :: 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 "AddDef" TyCon
typeNatAddTyCon ((Integer -> Integer -> Maybe Type) -> CoAxiomRule)
-> (Integer -> Integer -> Maybe Type) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$
              \x :: Integer
x y :: 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 "MulDef" TyCon
typeNatMulTyCon ((Integer -> Integer -> Maybe Type) -> CoAxiomRule)
-> (Integer -> Integer -> Maybe Type) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$
              \x :: Integer
x y :: 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 "ExpDef" TyCon
typeNatExpTyCon ((Integer -> Integer -> Maybe Type) -> CoAxiomRule)
-> (Integer -> Integer -> Maybe Type) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$
              \x :: Integer
x y :: 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 "LeqDef" TyCon
typeNatLeqTyCon ((Integer -> Integer -> Maybe Type) -> CoAxiomRule)
-> (Integer -> Integer -> Maybe Type) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$
              \x :: Integer
x y :: 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 "CmpNatDef" TyCon
typeNatCmpTyCon
              ((Integer -> Integer -> Maybe Type) -> CoAxiomRule)
-> (Integer -> Integer -> Maybe Type) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$ \x :: Integer
x y :: 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 "CmpSymbolDef"
    , coaxrAsmpRoles :: [Role]
coaxrAsmpRoles = [Role
Nominal, Role
Nominal]
    , coaxrRole :: Role
coaxrRole      = Role
Nominal
    , coaxrProves :: [TypeEqn] -> Maybe TypeEqn
coaxrProves    = \cs :: [TypeEqn]
cs ->
        do [Pair s1 :: Type
s1 s2 :: Type
s2, Pair t1 :: Type
t1 t2 :: 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 "AppendSymbolDef"
    , coaxrAsmpRoles :: [Role]
coaxrAsmpRoles = [Role
Nominal, Role
Nominal]
    , coaxrRole :: Role
coaxrRole      = Role
Nominal
    , coaxrProves :: [TypeEqn] -> Maybe TypeEqn
coaxrProves    = \cs :: [TypeEqn]
cs ->
        do [Pair s1 :: Type
s1 s2 :: Type
s2, Pair t1 :: Type
t1 t2 :: 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 "SubDef" TyCon
typeNatSubTyCon ((Integer -> Integer -> Maybe Type) -> CoAxiomRule)
-> (Integer -> Integer -> Maybe Type) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$
              \x :: Integer
x y :: 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 "DivDef" TyCon
typeNatDivTyCon ((Integer -> Integer -> Maybe Type) -> CoAxiomRule)
-> (Integer -> Integer -> Maybe Type) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$
              \x :: Integer
x y :: Integer
y -> do Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
y Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= 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 "ModDef" TyCon
typeNatModTyCon ((Integer -> Integer -> Maybe Type) -> CoAxiomRule)
-> (Integer -> Integer -> Maybe Type) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$
              \x :: Integer
x y :: Integer
y -> do Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
y Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= 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 "LogDef" TyCon
typeNatLogTyCon ((Integer -> Maybe Type) -> CoAxiomRule)
-> (Integer -> Maybe Type) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$
              \x :: Integer
x -> do (a :: Integer
a,_) <- Integer -> Integer -> Maybe (Integer, Bool)
genLog Integer
x 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 "Add0L"    ((TypeEqn -> TypeEqn) -> CoAxiomRule)
-> (TypeEqn -> TypeEqn) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$ \(Pair s :: Type
s t :: Type
t) -> (Integer -> Type
num 0 Type -> Type -> Type
.+. Type
s) Type -> Type -> TypeEqn
=== Type
t
axAdd0R :: CoAxiomRule
axAdd0R     = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 "Add0R"    ((TypeEqn -> TypeEqn) -> CoAxiomRule)
-> (TypeEqn -> TypeEqn) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$ \(Pair s :: Type
s t :: Type
t) -> (Type
s Type -> Type -> Type
.+. Integer -> Type
num 0) Type -> Type -> TypeEqn
=== Type
t
axSub0R :: CoAxiomRule
axSub0R     = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 "Sub0R"    ((TypeEqn -> TypeEqn) -> CoAxiomRule)
-> (TypeEqn -> TypeEqn) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$ \(Pair s :: Type
s t :: Type
t) -> (Type
s Type -> Type -> Type
.-. Integer -> Type
num 0) Type -> Type -> TypeEqn
=== Type
t
axMul0L :: CoAxiomRule
axMul0L     = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 "Mul0L"    ((TypeEqn -> TypeEqn) -> CoAxiomRule)
-> (TypeEqn -> TypeEqn) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$ \(Pair s :: Type
s _) -> (Integer -> Type
num 0 Type -> Type -> Type
.*. Type
s) Type -> Type -> TypeEqn
=== Integer -> Type
num 0
axMul0R :: CoAxiomRule
axMul0R     = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 "Mul0R"    ((TypeEqn -> TypeEqn) -> CoAxiomRule)
-> (TypeEqn -> TypeEqn) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$ \(Pair s :: Type
s _) -> (Type
s Type -> Type -> Type
.*. Integer -> Type
num 0) Type -> Type -> TypeEqn
=== Integer -> Type
num 0
axMul1L :: CoAxiomRule
axMul1L     = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 "Mul1L"    ((TypeEqn -> TypeEqn) -> CoAxiomRule)
-> (TypeEqn -> TypeEqn) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$ \(Pair s :: Type
s t :: Type
t) -> (Integer -> Type
num 1 Type -> Type -> Type
.*. Type
s) Type -> Type -> TypeEqn
=== Type
t
axMul1R :: CoAxiomRule
axMul1R     = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 "Mul1R"    ((TypeEqn -> TypeEqn) -> CoAxiomRule)
-> (TypeEqn -> TypeEqn) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$ \(Pair s :: Type
s t :: Type
t) -> (Type
s Type -> Type -> Type
.*. Integer -> Type
num 1) Type -> Type -> TypeEqn
=== Type
t
axDiv1 :: CoAxiomRule
axDiv1      = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 "Div1"     ((TypeEqn -> TypeEqn) -> CoAxiomRule)
-> (TypeEqn -> TypeEqn) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$ \(Pair s :: Type
s t :: Type
t) -> (Type -> Type -> Type
tDiv Type
s (Integer -> Type
num 1) Type -> Type -> TypeEqn
=== Type
t)
axMod1 :: CoAxiomRule
axMod1      = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 "Mod1"     ((TypeEqn -> TypeEqn) -> CoAxiomRule)
-> (TypeEqn -> TypeEqn) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$ \(Pair s :: Type
s _) -> (Type -> Type -> Type
tMod Type
s (Integer -> Type
num 1) Type -> Type -> TypeEqn
=== Integer -> Type
num 0)
                                    -- XXX: Shouldn't we check that _ is 0?
axExp1L :: CoAxiomRule
axExp1L     = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 "Exp1L"    ((TypeEqn -> TypeEqn) -> CoAxiomRule)
-> (TypeEqn -> TypeEqn) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$ \(Pair s :: Type
s _) -> (Integer -> Type
num 1 Type -> Type -> Type
.^. Type
s) Type -> Type -> TypeEqn
=== Integer -> Type
num 1
axExp0R :: CoAxiomRule
axExp0R     = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 "Exp0R"    ((TypeEqn -> TypeEqn) -> CoAxiomRule)
-> (TypeEqn -> TypeEqn) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$ \(Pair s :: Type
s _) -> (Type
s Type -> Type -> Type
.^. Integer -> Type
num 0) Type -> Type -> TypeEqn
=== Integer -> Type
num 1
axExp1R :: CoAxiomRule
axExp1R     = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 "Exp1R"    ((TypeEqn -> TypeEqn) -> CoAxiomRule)
-> (TypeEqn -> TypeEqn) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$ \(Pair s :: Type
s t :: Type
t) -> (Type
s Type -> Type -> Type
.^. Integer -> Type
num 1) Type -> Type -> TypeEqn
=== Type
t
axLeqRefl :: CoAxiomRule
axLeqRefl   = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 "LeqRefl"  ((TypeEqn -> TypeEqn) -> CoAxiomRule)
-> (TypeEqn -> TypeEqn) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$ \(Pair s :: Type
s _) -> (Type
s Type -> Type -> Type
<== Type
s) Type -> Type -> TypeEqn
=== Bool -> Type
bool Bool
True
axCmpNatRefl :: CoAxiomRule
axCmpNatRefl    = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 "CmpNatRefl"
                ((TypeEqn -> TypeEqn) -> CoAxiomRule)
-> (TypeEqn -> TypeEqn) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$ \(Pair s :: Type
s _) -> (Type -> Type -> Type
cmpNat Type
s Type
s) Type -> Type -> TypeEqn
=== Ordering -> Type
ordering Ordering
EQ
axCmpSymbolRefl :: CoAxiomRule
axCmpSymbolRefl = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 "CmpSymbolRefl"
                ((TypeEqn -> TypeEqn) -> CoAxiomRule)
-> (TypeEqn -> TypeEqn) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$ \(Pair s :: Type
s _) -> (Type -> Type -> Type
cmpSymbol Type
s Type
s) Type -> Type -> TypeEqn
=== Ordering -> Type
ordering Ordering
EQ
axLeq0L :: CoAxiomRule
axLeq0L     = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 "Leq0L"    ((TypeEqn -> TypeEqn) -> CoAxiomRule)
-> (TypeEqn -> TypeEqn) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$ \(Pair s :: Type
s _) -> (Integer -> Type
num 0 Type -> Type -> Type
<== Type
s) Type -> Type -> TypeEqn
=== Bool -> Type
bool Bool
True
axAppendSymbol0R :: CoAxiomRule
axAppendSymbol0R  = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 "Concat0R"
            ((TypeEqn -> TypeEqn) -> CoAxiomRule)
-> (TypeEqn -> TypeEqn) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$ \(Pair s :: Type
s t :: 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 "Concat0L"
            ((TypeEqn -> TypeEqn) -> CoAxiomRule)
-> (TypeEqn -> TypeEqn) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$ \(Pair s :: Type
s t :: 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 (\x :: 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
s :: Type
s .+. :: Type -> Type -> Type
.+. t :: Type
t = TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatAddTyCon [Type
s,Type
t]

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

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

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

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

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

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

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

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

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

(===) :: Type -> Type -> Pair Type
x :: Type
x === :: Type -> Type -> TypeEqn
=== y :: 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 b :: 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 tc :: Type
tc =
  do (tc :: 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 o :: Ordering
o =
  case Ordering
o of
    LT -> TyCon -> [Type] -> Type
mkTyConApp TyCon
promotedLTDataCon []
    EQ -> TyCon -> [Type] -> Type
mkTyConApp TyCon
promotedEQDataCon []
    GT -> TyCon -> [Type] -> Type
mkTyConApp TyCon
promotedGTDataCon []

isOrderingLitTy :: Type -> Maybe Ordering
isOrderingLitTy :: Type -> Maybe Ordering
isOrderingLitTy tc :: Type
tc =
  do (tc1 :: 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 p :: Integer -> Bool
p x :: Type
x = case Type -> Maybe Integer
isNumLitTy Type
x of
              Just a :: Integer
a  -> Integer -> Bool
p Integer
a
              Nothing -> Bool
False


mkUnAxiom :: String -> TyCon -> (Integer -> Maybe Type) -> CoAxiomRule
mkUnAxiom :: String -> TyCon -> (Integer -> Maybe Type) -> CoAxiomRule
mkUnAxiom str :: String
str tc :: TyCon
tc f :: 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    = \cs :: [TypeEqn]
cs ->
        do [Pair s1 :: Type
s1 s2 :: 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 str :: String
str tc :: TyCon
tc f :: 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    = \cs :: [TypeEqn]
cs ->
        do [Pair s1 :: Type
s1 s2 :: Type
s2, Pair t1 :: Type
t1 t2 :: 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 str :: String
str f :: 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 [eqn :: TypeEqn
eqn] -> TypeEqn -> Maybe TypeEqn
forall a. a -> Maybe a
Just (TypeEqn -> TypeEqn
f TypeEqn
eqn)
                             _     -> Maybe TypeEqn
forall a. Maybe a
Nothing
    }


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

matchFamAdd :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamAdd :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamAdd [s :: Type
s,t :: Type
t]
  | Just 0 <- Maybe Integer
mbX = (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axAdd0L, [Type
t], Type
t)
  | Just 0 <- Maybe Integer
mbY = (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axAdd0R, [Type
s], Type
s)
  | Just x :: Integer
x <- Maybe Integer
mbX, Just y :: 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 _ = Maybe (CoAxiomRule, [Type], Type)
forall a. Maybe a
Nothing

matchFamSub :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamSub :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamSub [s :: Type
s,t :: Type
t]
  | Just 0 <- Maybe Integer
mbY = (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axSub0R, [Type
s], Type
s)
  | Just x :: Integer
x <- Maybe Integer
mbX, Just y :: Integer
y <- Maybe Integer
mbY, Just z :: 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 _ = Maybe (CoAxiomRule, [Type], Type)
forall a. Maybe a
Nothing

matchFamMul :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamMul :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamMul [s :: Type
s,t :: Type
t]
  | Just 0 <- Maybe Integer
mbX = (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axMul0L, [Type
t], Integer -> Type
num 0)
  | Just 0 <- Maybe Integer
mbY = (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axMul0R, [Type
s], Integer -> Type
num 0)
  | Just 1 <- Maybe Integer
mbX = (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axMul1L, [Type
t], Type
t)
  | Just 1 <- Maybe Integer
mbY = (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axMul1R, [Type
s], Type
s)
  | Just x :: Integer
x <- Maybe Integer
mbX, Just y :: 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 _ = Maybe (CoAxiomRule, [Type], Type)
forall a. Maybe a
Nothing

matchFamDiv :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamDiv :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamDiv [s :: Type
s,t :: Type
t]
  | Just 1 <- Maybe Integer
mbY = (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axDiv1, [Type
s], Type
s)
  | Just x :: Integer
x <- Maybe Integer
mbX, Just y :: Integer
y <- Maybe Integer
mbY, Integer
y Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= 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 _ = Maybe (CoAxiomRule, [Type], Type)
forall a. Maybe a
Nothing

matchFamMod :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamMod :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamMod [s :: Type
s,t :: Type
t]
  | Just 1 <- Maybe Integer
mbY = (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axMod1, [Type
s], Integer -> Type
num 0)
  | Just x :: Integer
x <- Maybe Integer
mbX, Just y :: Integer
y <- Maybe Integer
mbY, Integer
y Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= 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 _ = Maybe (CoAxiomRule, [Type], Type)
forall a. Maybe a
Nothing



matchFamExp :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamExp :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamExp [s :: Type
s,t :: Type
t]
  | Just 0 <- Maybe Integer
mbY = (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axExp0R, [Type
s], Integer -> Type
num 1)
  | Just 1 <- Maybe Integer
mbX = (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axExp1L, [Type
t], Integer -> Type
num 1)
  | Just 1 <- Maybe Integer
mbY = (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axExp1R, [Type
s], Type
s)
  | Just x :: Integer
x <- Maybe Integer
mbX, Just y :: 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 _ = Maybe (CoAxiomRule, [Type], Type)
forall a. Maybe a
Nothing

matchFamLog :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamLog :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamLog [s :: Type
s]
  | Just x :: Integer
x <- Maybe Integer
mbX, Just (n :: Integer
n,_) <- Integer -> Integer -> Maybe (Integer, Bool)
genLog Integer
x 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 _ = Maybe (CoAxiomRule, [Type], Type)
forall a. Maybe a
Nothing


matchFamLeq :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamLeq :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamLeq [s :: Type
s,t :: Type
t]
  | Just 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 x :: Integer
x <- Maybe Integer
mbX, Just y :: 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 _ = Maybe (CoAxiomRule, [Type], Type)
forall a. Maybe a
Nothing

matchFamCmpNat :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamCmpNat :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamCmpNat [s :: Type
s,t :: Type
t]
  | Just x :: Integer
x <- Maybe Integer
mbX, Just y :: 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 _ = Maybe (CoAxiomRule, [Type], Type)
forall a. Maybe a
Nothing

matchFamCmpSymbol :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamCmpSymbol :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamCmpSymbol [s :: Type
s,t :: Type
t]
  | Just x :: FastString
x <- Maybe FastString
mbX, Just y :: 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 _ = Maybe (CoAxiomRule, [Type], Type)
forall a. Maybe a
Nothing

matchFamAppendSymbol :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamAppendSymbol :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamAppendSymbol [s :: Type
s,t :: Type
t]
  | Just x :: 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 y :: 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 x :: FastString
x <- Maybe FastString
mbX, Just y :: 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 _ = Maybe (CoAxiomRule, [Type], Type)
forall a. Maybe a
Nothing

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

interactTopAdd :: [Xi] -> Xi -> [Pair Type]
interactTopAdd :: [Type] -> Type -> [TypeEqn]
interactTopAdd [s :: Type
s,t :: Type
t] r :: Type
r
  | Just 0 <- Maybe Integer
mbZ = [ Type
s Type -> Type -> TypeEqn
=== Integer -> Type
num 0, Type
t Type -> Type -> TypeEqn
=== Integer -> Type
num 0 ]                          -- (s + t ~ 0) => (s ~ 0, t ~ 0)
  | Just x :: Integer
x <- Maybe Integer
mbX, Just z :: Integer
z <- Maybe Integer
mbZ, Just y :: 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 y :: Integer
y <- Maybe Integer
mbY, Just z :: Integer
z <- Maybe Integer
mbZ, Just x :: 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 _ _ = []

{-
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 [s :: Type
s,t :: Type
t] r :: Type
r
  | Just z :: 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 _ _ = []





interactTopMul :: [Xi] -> Xi -> [Pair Type]
interactTopMul :: [Type] -> Type -> [TypeEqn]
interactTopMul [s :: Type
s,t :: Type
t] r :: Type
r
  | Just 1 <- Maybe Integer
mbZ = [ Type
s Type -> Type -> TypeEqn
=== Integer -> Type
num 1, Type
t Type -> Type -> TypeEqn
=== Integer -> Type
num 1 ]                        -- (s * t ~ 1)  => (s ~ 1, t ~ 1)
  | Just x :: Integer
x <- Maybe Integer
mbX, Just z :: Integer
z <- Maybe Integer
mbZ, Just y :: 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 y :: Integer
y <- Maybe Integer
mbY, Just z :: Integer
z <- Maybe Integer
mbZ, Just x :: 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 _ _ = []

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

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

interactTopExp :: [Xi] -> Xi -> [Pair Type]
interactTopExp :: [Type] -> Type -> [TypeEqn]
interactTopExp [s :: Type
s,t :: Type
t] r :: Type
r
  | Just 0 <- Maybe Integer
mbZ = [ Type
s Type -> Type -> TypeEqn
=== Integer -> Type
num 0 ]                                       -- (s ^ t ~ 0) => (s ~ 0)
  | Just x :: Integer
x <- Maybe Integer
mbX, Just z :: Integer
z <- Maybe Integer
mbZ, Just y :: 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 y :: Integer
y <- Maybe Integer
mbY, Just z :: Integer
z <- Maybe Integer
mbZ, Just x :: 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 _ _ = []

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



interactTopLeq :: [Xi] -> Xi -> [Pair Type]
interactTopLeq :: [Type] -> Type -> [TypeEqn]
interactTopLeq [s :: Type
s,t :: Type
t] r :: Type
r
  | Just 0 <- Maybe Integer
mbY, Just True <- Maybe Bool
mbZ = [ Type
s Type -> Type -> TypeEqn
=== Integer -> Type
num 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 _ _ = []

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

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

interactTopAppendSymbol :: [Xi] -> Xi -> [Pair Type]
interactTopAppendSymbol :: [Type] -> Type -> [TypeEqn]
interactTopAppendSymbol [s :: Type
s,t :: Type
t] r :: Type
r
  -- (AppendSymbol a b ~ "") => (a ~ "", b ~ "")
  | Just z :: 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 x :: 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 z :: 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 y :: 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 z :: 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 _ _ = []

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

interactInertAdd :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
interactInertAdd :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertAdd [x1 :: Type
x1,y1 :: Type
y1] z1 :: Type
z1 [x2 :: Type
x2,y2 :: Type
y2] z2 :: 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 _ _ _ _ = []

interactInertSub :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
interactInertSub :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertSub [x1 :: Type
x1,y1 :: Type
y1] z1 :: Type
z1 [x2 :: Type
x2,y2 :: Type
y2] z2 :: 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 _ _ _ _ = []

interactInertMul :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
interactInertMul :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertMul [x1 :: Type
x1,y1 :: Type
y1] z1 :: Type
z1 [x2 :: Type
x2,y2 :: Type
y2] z2 :: Type
z2
  | Bool
sameZ Bool -> Bool -> Bool
&& (Integer -> Bool) -> Type -> Bool
known (Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= 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
/= 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 _ _ _ _ = []

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

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

interactInertExp :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
interactInertExp :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertExp [x1 :: Type
x1,y1 :: Type
y1] z1 :: Type
z1 [x2 :: Type
x2,y2 :: Type
y2] z2 :: Type
z2
  | Bool
sameZ Bool -> Bool -> Bool
&& (Integer -> Bool) -> Type -> Bool
known (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> 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
> 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 _ _ _ _ = []

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


interactInertLeq :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
interactInertLeq :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertLeq [x1 :: Type
x1,y1 :: Type
y1] z1 :: Type
z1 [x2 :: Type
x2,y2 :: Type
y2] z2 :: 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 _ _ _ _ = []


interactInertAppendSymbol :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
interactInertAppendSymbol :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertAppendSymbol [x1 :: Type
x1,y1 :: Type
y1] z1 :: Type
z1 [x2 :: Type
x2,y2 :: Type
y2] z2 :: 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 _ _ _ _ = []



{- -----------------------------------------------------------------------------
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 x :: Integer
x y :: 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 x :: Integer
x y :: Integer
y = do (z :: Integer
z,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 _ 0  = Maybe Integer
forall a. Maybe a
Nothing
divide x :: Integer
x y :: Integer
y  = case Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
divMod Integer
x Integer
y of
                (a :: Integer
a,0) -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
a
                _     -> 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 x :: Integer
x y :: Integer
y = do (z :: Integer
z,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 _  0    = Maybe (Integer, Bool)
forall a. Maybe a
Nothing
genRoot x0 :: Integer
x0 1    = (Integer, Bool) -> Maybe (Integer, Bool)
forall a. a -> Maybe a
Just (Integer
x0, Bool
True)
genRoot x0 :: Integer
x0 root :: Integer
root = (Integer, Bool) -> Maybe (Integer, Bool)
forall a. a -> Maybe a
Just (Integer -> Integer -> (Integer, Bool)
search 0 (Integer
x0Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+1))
  where
  search :: Integer -> Integer -> (Integer, Bool)
search from :: Integer
from to :: 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) 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
                        EQ              -> (Integer
x, Bool
True)
                        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)
                        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 x :: Integer
x 0    = if Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== 1 then (Integer, Bool) -> Maybe (Integer, Bool)
forall a. a -> Maybe a
Just (0, Bool
True) else Maybe (Integer, Bool)
forall a. Maybe a
Nothing
genLog _ 1    = Maybe (Integer, Bool)
forall a. Maybe a
Nothing
genLog 0 _    = Maybe (Integer, Bool)
forall a. Maybe a
Nothing
genLog x :: Integer
x base :: Integer
base = (Integer, Bool) -> Maybe (Integer, Bool)
forall a. a -> Maybe a
Just (Integer -> Integer -> (Integer, Bool)
forall t. Num t => t -> Integer -> (t, Bool)
exactLoop 0 Integer
x)
  where
  exactLoop :: t -> Integer -> (t, Bool)
exactLoop s :: t
s i :: Integer
i
    | Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== 1     = (t
s,Bool
True)
    | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
base   = (t
s,Bool
False)
    | Bool
otherwise  =
        let s1 :: t
s1 = t
s t -> t -> t
forall a. Num a => a -> a -> a
+ 1
        in t
s1 t -> (t, Bool) -> (t, Bool)
forall a b. a -> b -> b
`seq` case Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
divMod Integer
i Integer
base of
                      (j :: Integer
j,r :: Integer
r)
                        | Integer
r Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== 0    -> t -> Integer -> (t, Bool)
exactLoop t
s1 Integer
j
                        | Bool
otherwise -> (t -> Integer -> t
forall t. Num t => t -> Integer -> t
underLoop t
s1 Integer
j, Bool
False)

  underLoop :: t -> Integer -> t
underLoop s :: t
s i :: 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
+ 1 in t
s1 t -> t -> t
forall a b. a -> b -> b
`seq` t -> Integer -> t
underLoop t
s1 (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div Integer
i Integer
base)