{-# 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
  , typeNatSubTyCon
  , typeNatDivTyCon
  , typeNatModTyCon
  , typeNatLogTyCon
  , typeNatCmpTyCon
  , typeSymbolCmpTyCon
  , typeSymbolAppendTyCon
  , typeCharCmpTyCon
  , typeConsSymbolTyCon
  , typeUnconsSymbolTyCon
  , typeCharToNatTyCon
  , typeNatToCharTyCon
  ) where

import GHC.Prelude

import GHC.Core.Type
import GHC.Data.Pair
import GHC.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.Core.TyCo.Compare   ( tcEqType )
import GHC.Types.Name          ( Name, BuiltInSyntax(..) )
import GHC.Types.Unique.FM
import GHC.Builtin.Types
import GHC.Builtin.Types.Prim  ( mkTemplateAnonTyConBinders )
import GHC.Builtin.Names
                  ( gHC_INTERNAL_TYPELITS
                  , gHC_INTERNAL_TYPELITS_INTERNAL
                  , gHC_INTERNAL_TYPENATS
                  , gHC_INTERNAL_TYPENATS_INTERNAL
                  , typeNatAddTyFamNameKey
                  , typeNatMulTyFamNameKey
                  , typeNatExpTyFamNameKey
                  , typeNatSubTyFamNameKey
                  , typeNatDivTyFamNameKey
                  , typeNatModTyFamNameKey
                  , typeNatLogTyFamNameKey
                  , typeNatCmpTyFamNameKey
                  , typeSymbolCmpTyFamNameKey
                  , typeSymbolAppendFamNameKey
                  , typeCharCmpTyFamNameKey
                  , typeConsSymbolTyFamNameKey
                  , typeUnconsSymbolTyFamNameKey
                  , typeCharToNatTyFamNameKey
                  , typeNatToCharTyFamNameKey
                  )
import GHC.Data.FastString
import Control.Monad ( guard )
import Data.List  ( isPrefixOf, isSuffixOf )
import qualified Data.Char as Char

{-
Note [Type-level literals]
~~~~~~~~~~~~~~~~~~~~~~~~~~
There are currently three forms of type-level literals: natural numbers, symbols, and
characters.

Type-level literals are supported by CoAxiomRules (conditional axioms), which
power the built-in type families (see Note [Adding built-in type families]).
Currently, all built-in type families are for the express purpose of supporting
type-level literals.

See also the Wiki page:

    https://gitlab.haskell.org/ghc/ghc/wikis/type-nats

Note [Adding built-in type families]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
There are a few steps to adding a built-in type family:

* Adding a unique for the type family TyCon

  These go in GHC.Builtin.Names. It will likely be of the form
  @myTyFamNameKey = mkPreludeTyConUnique xyz@, where @xyz@ is a number that
  has not been chosen before in GHC.Builtin.Names. There are several examples already
  in GHC.Builtin.Names—see, for instance, typeNatAddTyFamNameKey.

* Adding the type family TyCon itself

  This goes in GHC.Builtin.Types.Literals. There are plenty of examples of how to define
  these—see, for instance, typeNatAddTyCon.

  Once your TyCon has been defined, be sure to:

  - Export it from GHC.Builtin.Types.Literals. (Not doing so caused #14632.)
  - Include it in the typeNatTyCons list, defined in GHC.Builtin.Types.Literals.

* 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
typeNatSubTyCon
  , TyCon
typeNatDivTyCon
  , TyCon
typeNatModTyCon
  , TyCon
typeNatLogTyCon
  , TyCon
typeNatCmpTyCon
  , TyCon
typeSymbolCmpTyCon
  , TyCon
typeSymbolAppendTyCon
  , TyCon
typeCharCmpTyCon
  , TyCon
typeConsSymbolTyCon
  , TyCon
typeUnconsSymbolTyCon
  , TyCon
typeCharToNatTyCon
  , TyCon
typeNatToCharTyCon
  ]

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

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

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

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

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

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

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



typeNatCmpTyCon :: TyCon
typeNatCmpTyCon :: TyCon
typeNatCmpTyCon =
  Name
-> [TyConBinder]
-> Type
-> Maybe Name
-> FamTyConFlav
-> Maybe Class
-> Injectivity
-> TyCon
mkFamilyTyCon Name
name
    ([Type] -> [TyConBinder]
mkTemplateAnonTyConBinders [ Type
naturalTy, Type
naturalTy ])
    Type
orderingKind
    Maybe Name
forall a. Maybe a
Nothing
    (BuiltInSynFamily -> FamTyConFlav
BuiltInSynFamTyCon BuiltInSynFamily
ops)
    Maybe Class
forall a. Maybe a
Nothing
    Injectivity
NotInjective

  where
  name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_INTERNAL_TYPENATS_INTERNAL (String -> FastString
fsLit String
"CmpNat")
                Unique
typeNatCmpTyFamNameKey TyCon
typeNatCmpTyCon
  ops :: BuiltInSynFamily
ops = BuiltInSynFamily
    { sfMatchFam :: [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_INTERNAL_TYPELITS_INTERNAL (String -> FastString
fsLit String
"CmpSymbol")
                Unique
typeSymbolCmpTyFamNameKey TyCon
typeSymbolCmpTyCon
  ops :: BuiltInSynFamily
ops = BuiltInSynFamily
    { sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
sfMatchFam      = [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamCmpSymbol
    , sfInteractTop :: [Type] -> Type -> [TypeEqn]
sfInteractTop   = [Type] -> Type -> [TypeEqn]
interactTopCmpSymbol
    , sfInteractInert :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
sfInteractInert = \[Type]
_ Type
_ [Type]
_ Type
_ -> []
    }

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

typeConsSymbolTyCon :: TyCon
typeConsSymbolTyCon :: TyCon
typeConsSymbolTyCon =
  Name
-> [TyConBinder]
-> Type
-> Maybe Name
-> FamTyConFlav
-> Maybe Class
-> Injectivity
-> TyCon
mkFamilyTyCon Name
name
    ([Type] -> [TyConBinder]
mkTemplateAnonTyConBinders [ Type
charTy, Type
typeSymbolKind ])
    Type
typeSymbolKind
    Maybe Name
forall a. Maybe a
Nothing
    (BuiltInSynFamily -> FamTyConFlav
BuiltInSynFamTyCon BuiltInSynFamily
ops)
    Maybe Class
forall a. Maybe a
Nothing
    ([Bool] -> Injectivity
Injective [Bool
True, Bool
True])
  where
  name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_INTERNAL_TYPELITS (String -> FastString
fsLit String
"ConsSymbol")
                  Unique
typeConsSymbolTyFamNameKey TyCon
typeConsSymbolTyCon
  ops :: BuiltInSynFamily
ops = BuiltInSynFamily
      { sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
sfMatchFam      = [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamConsSymbol
      , sfInteractTop :: [Type] -> Type -> [TypeEqn]
sfInteractTop   = [Type] -> Type -> [TypeEqn]
interactTopConsSymbol
      , sfInteractInert :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
sfInteractInert = [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertConsSymbol
      }

typeUnconsSymbolTyCon :: TyCon
typeUnconsSymbolTyCon :: TyCon
typeUnconsSymbolTyCon =
  Name
-> [TyConBinder]
-> Type
-> Maybe Name
-> FamTyConFlav
-> Maybe Class
-> Injectivity
-> TyCon
mkFamilyTyCon Name
name
    ([Type] -> [TyConBinder]
mkTemplateAnonTyConBinders [ Type
typeSymbolKind ])
    (Type -> Type
mkMaybeTy Type
charSymbolPairKind)
    Maybe Name
forall a. Maybe a
Nothing
    (BuiltInSynFamily -> FamTyConFlav
BuiltInSynFamTyCon BuiltInSynFamily
ops)
    Maybe Class
forall a. Maybe a
Nothing
    ([Bool] -> Injectivity
Injective [Bool
True])
  where
  name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_INTERNAL_TYPELITS (String -> FastString
fsLit String
"UnconsSymbol")
                  Unique
typeUnconsSymbolTyFamNameKey TyCon
typeUnconsSymbolTyCon
  ops :: BuiltInSynFamily
ops = BuiltInSynFamily
      { sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
sfMatchFam      = [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamUnconsSymbol
      , sfInteractTop :: [Type] -> Type -> [TypeEqn]
sfInteractTop   = [Type] -> Type -> [TypeEqn]
interactTopUnconsSymbol
      , sfInteractInert :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
sfInteractInert = [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertUnconsSymbol
      }

typeCharToNatTyCon :: TyCon
typeCharToNatTyCon :: TyCon
typeCharToNatTyCon =
  Name
-> [TyConBinder]
-> Type
-> Maybe Name
-> FamTyConFlav
-> Maybe Class
-> Injectivity
-> TyCon
mkFamilyTyCon Name
name
    ([Type] -> [TyConBinder]
mkTemplateAnonTyConBinders [ Type
charTy ])
    Type
naturalTy
    Maybe Name
forall a. Maybe a
Nothing
    (BuiltInSynFamily -> FamTyConFlav
BuiltInSynFamTyCon BuiltInSynFamily
ops)
    Maybe Class
forall a. Maybe a
Nothing
    ([Bool] -> Injectivity
Injective [Bool
True])
  where
  name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_INTERNAL_TYPELITS (String -> FastString
fsLit String
"CharToNat")
                  Unique
typeCharToNatTyFamNameKey TyCon
typeCharToNatTyCon
  ops :: BuiltInSynFamily
ops = BuiltInSynFamily
      { sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
sfMatchFam      = [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamCharToNat
      , sfInteractTop :: [Type] -> Type -> [TypeEqn]
sfInteractTop   = [Type] -> Type -> [TypeEqn]
interactTopCharToNat
      , sfInteractInert :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
sfInteractInert = \[Type]
_ Type
_ [Type]
_ Type
_ -> []
      }


typeNatToCharTyCon :: TyCon
typeNatToCharTyCon :: TyCon
typeNatToCharTyCon =
  Name
-> [TyConBinder]
-> Type
-> Maybe Name
-> FamTyConFlav
-> Maybe Class
-> Injectivity
-> TyCon
mkFamilyTyCon Name
name
    ([Type] -> [TyConBinder]
mkTemplateAnonTyConBinders [ Type
naturalTy ])
    Type
charTy
    Maybe Name
forall a. Maybe a
Nothing
    (BuiltInSynFamily -> FamTyConFlav
BuiltInSynFamTyCon BuiltInSynFamily
ops)
    Maybe Class
forall a. Maybe a
Nothing
    ([Bool] -> Injectivity
Injective [Bool
True])
  where
  name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_INTERNAL_TYPELITS (String -> FastString
fsLit String
"NatToChar")
                  Unique
typeNatToCharTyFamNameKey TyCon
typeNatToCharTyCon
  ops :: BuiltInSynFamily
ops = BuiltInSynFamily
      { sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
sfMatchFam      = [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamNatToChar
      , sfInteractTop :: [Type] -> Type -> [TypeEqn]
sfInteractTop   = [Type] -> Type -> [TypeEqn]
interactTopNatToChar
      , sfInteractInert :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
sfInteractInert = \[Type]
_ Type
_ [Type]
_ Type
_ -> []
      }

-- 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
naturalTy ])
    Type
naturalTy
    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
naturalTy, Type
naturalTy ])
    Type
naturalTy
    Maybe Name
forall a. Maybe a
Nothing
    (BuiltInSynFamily -> FamTyConFlav
BuiltInSynFamTyCon BuiltInSynFamily
tcb)
    Maybe Class
forall a. Maybe a
Nothing
    Injectivity
NotInjective

-- 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
  , axCmpNatDef
  , axCmpSymbolDef
  , axAppendSymbolDef
  , axConsSymbolDef
  , axUnconsSymbolDef
  , axCharToNatDef
  , axNatToCharDef
  , axAdd0L
  , axAdd0R
  , axMul0L
  , axMul0R
  , axMul1L
  , axMul1R
  , axExp1L
  , axExp0R
  , axExp1R
  , axCmpNatRefl
  , axCmpSymbolRefl
  , axSubDef
  , axSub0R
  , axAppendSymbol0R
  , axAppendSymbol0L
  , axDivDef
  , axDiv1
  , axModDef
  , axMod1
  , axLogDef
  :: CoAxiomRule

axAddDef :: CoAxiomRule
axAddDef = String
-> TyCon
-> (Type -> Maybe Integer)
-> (Type -> Maybe Integer)
-> (Integer -> Integer -> Maybe Type)
-> CoAxiomRule
forall a b.
String
-> TyCon
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> CoAxiomRule
mkBinAxiom String
"AddDef" TyCon
typeNatAddTyCon Type -> Maybe Integer
isNumLitTy Type -> Maybe Integer
isNumLitTy ((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
-> (Type -> Maybe Integer)
-> (Type -> Maybe Integer)
-> (Integer -> Integer -> Maybe Type)
-> CoAxiomRule
forall a b.
String
-> TyCon
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> CoAxiomRule
mkBinAxiom String
"MulDef" TyCon
typeNatMulTyCon Type -> Maybe Integer
isNumLitTy Type -> Maybe Integer
isNumLitTy ((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
-> (Type -> Maybe Integer)
-> (Type -> Maybe Integer)
-> (Integer -> Integer -> Maybe Type)
-> CoAxiomRule
forall a b.
String
-> TyCon
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> CoAxiomRule
mkBinAxiom String
"ExpDef" TyCon
typeNatExpTyCon Type -> Maybe Integer
isNumLitTy Type -> Maybe Integer
isNumLitTy ((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)

axCmpNatDef :: CoAxiomRule
axCmpNatDef   = String
-> TyCon
-> (Type -> Maybe Integer)
-> (Type -> Maybe Integer)
-> (Integer -> Integer -> Maybe Type)
-> CoAxiomRule
forall a b.
String
-> TyCon
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> CoAxiomRule
mkBinAxiom String
"CmpNatDef" TyCon
typeNatCmpTyCon Type -> Maybe Integer
isNumLitTy Type -> Maybe Integer
isNumLitTy
              ((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
    { 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 s1 s2, Pair t1 t2] <- [TypeEqn] -> Maybe [TypeEqn]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return [TypeEqn]
cs
           s2' <- isStrLitTy s2
           t2' <- isStrLitTy t2
           return (mkTyConApp typeSymbolCmpTyCon [s1,t1] ===
                   ordering (lexicalCompareFS s2' t2')) }

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

axConsSymbolDef :: CoAxiomRule
axConsSymbolDef =
  String
-> TyCon
-> (Type -> Maybe Char)
-> (Type -> Maybe FastString)
-> (Char -> FastString -> Maybe Type)
-> CoAxiomRule
forall a b.
String
-> TyCon
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> CoAxiomRule
mkBinAxiom String
"ConsSymbolDef" TyCon
typeConsSymbolTyCon Type -> Maybe Char
isCharLitTy Type -> Maybe FastString
isStrLitTy ((Char -> FastString -> Maybe Type) -> CoAxiomRule)
-> (Char -> FastString -> Maybe Type) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$
    \Char
c FastString
str -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ FastString -> Type
mkStrLitTy (Char -> FastString -> FastString
consFS Char
c FastString
str)

axUnconsSymbolDef :: CoAxiomRule
axUnconsSymbolDef =
  String
-> TyCon
-> (Type -> Maybe FastString)
-> (FastString -> Maybe Type)
-> CoAxiomRule
forall a.
String
-> TyCon -> (Type -> Maybe a) -> (a -> Maybe Type) -> CoAxiomRule
mkUnAxiom String
"UnconsSymbolDef" TyCon
typeUnconsSymbolTyCon Type -> Maybe FastString
isStrLitTy ((FastString -> Maybe Type) -> CoAxiomRule)
-> (FastString -> Maybe Type) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$
    \FastString
str -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ FastString -> Type
computeUncons FastString
str

axCharToNatDef :: CoAxiomRule
axCharToNatDef =
  String
-> TyCon
-> (Type -> Maybe Char)
-> (Char -> Maybe Type)
-> CoAxiomRule
forall a.
String
-> TyCon -> (Type -> Maybe a) -> (a -> Maybe Type) -> CoAxiomRule
mkUnAxiom String
"CharToNatDef" TyCon
typeCharToNatTyCon Type -> Maybe Char
isCharLitTy ((Char -> Maybe Type) -> CoAxiomRule)
-> (Char -> Maybe Type) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$
    \Char
c -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Integer -> Type
num (Char -> Integer
charToInteger Char
c)

axNatToCharDef :: CoAxiomRule
axNatToCharDef =
  String
-> TyCon
-> (Type -> Maybe Integer)
-> (Integer -> Maybe Type)
-> CoAxiomRule
forall a.
String
-> TyCon -> (Type -> Maybe a) -> (a -> Maybe Type) -> CoAxiomRule
mkUnAxiom String
"NatToCharDef" TyCon
typeNatToCharTyCon Type -> Maybe Integer
isNumLitTy ((Integer -> Maybe Type) -> CoAxiomRule)
-> (Integer -> Maybe Type) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$
    \Integer
n -> (Char -> Type) -> Maybe Char -> Maybe Type
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Char -> Type
mkCharLitTy (Integer -> Maybe Char
integerToChar Integer
n)

axSubDef :: CoAxiomRule
axSubDef = String
-> TyCon
-> (Type -> Maybe Integer)
-> (Type -> Maybe Integer)
-> (Integer -> Integer -> Maybe Type)
-> CoAxiomRule
forall a b.
String
-> TyCon
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> CoAxiomRule
mkBinAxiom String
"SubDef" TyCon
typeNatSubTyCon Type -> Maybe Integer
isNumLitTy Type -> Maybe Integer
isNumLitTy ((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 a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Integer -> Type
num (Integer -> Integer -> Maybe Integer
minus Integer
x Integer
y)

axDivDef :: CoAxiomRule
axDivDef = String
-> TyCon
-> (Type -> Maybe Integer)
-> (Type -> Maybe Integer)
-> (Integer -> Integer -> Maybe Type)
-> CoAxiomRule
forall a b.
String
-> TyCon
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> CoAxiomRule
mkBinAxiom String
"DivDef" TyCon
typeNatDivTyCon Type -> Maybe Integer
isNumLitTy Type -> Maybe Integer
isNumLitTy ((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 a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Type
num (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div Integer
x Integer
y))

axModDef :: CoAxiomRule
axModDef = String
-> TyCon
-> (Type -> Maybe Integer)
-> (Type -> Maybe Integer)
-> (Integer -> Integer -> Maybe Type)
-> CoAxiomRule
forall a b.
String
-> TyCon
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> CoAxiomRule
mkBinAxiom String
"ModDef" TyCon
typeNatModTyCon Type -> Maybe Integer
isNumLitTy Type -> Maybe Integer
isNumLitTy ((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 a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Type
num (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
mod Integer
x Integer
y))

axLogDef :: CoAxiomRule
axLogDef = String
-> TyCon
-> (Type -> Maybe Integer)
-> (Integer -> Maybe Type)
-> CoAxiomRule
forall a.
String
-> TyCon -> (Type -> Maybe a) -> (a -> Maybe Type) -> CoAxiomRule
mkUnAxiom String
"LogDef" TyCon
typeNatLogTyCon Type -> Maybe Integer
isNumLitTy ((Integer -> Maybe Type) -> CoAxiomRule)
-> (Integer -> Maybe Type) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$
              \Integer
x -> do (a,_) <- Integer -> Integer -> Maybe (Integer, Bool)
genLog Integer
x Integer
2
                       return (num 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
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
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 :: UniqFM FastString CoAxiomRule
typeNatCoAxiomRules :: UniqFM FastString CoAxiomRule
typeNatCoAxiomRules = [(FastString, CoAxiomRule)] -> UniqFM FastString CoAxiomRule
forall key elt. Uniquable key => [(key, elt)] -> UniqFM key elt
listToUFM ([(FastString, CoAxiomRule)] -> UniqFM FastString CoAxiomRule)
-> [(FastString, CoAxiomRule)] -> UniqFM FastString CoAxiomRule
forall a b. (a -> b) -> a -> b
$ (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
axCmpNatDef
  , CoAxiomRule
axCmpSymbolDef
  , CoAxiomRule
axCmpCharDef
  , CoAxiomRule
axAppendSymbolDef
  , CoAxiomRule
axConsSymbolDef
  , CoAxiomRule
axUnconsSymbolDef
  , CoAxiomRule
axCharToNatDef
  , CoAxiomRule
axNatToCharDef
  , CoAxiomRule
axAdd0L
  , CoAxiomRule
axAdd0R
  , CoAxiomRule
axMul0L
  , CoAxiomRule
axMul0R
  , CoAxiomRule
axMul1L
  , CoAxiomRule
axMul1R
  , CoAxiomRule
axExp1L
  , CoAxiomRule
axExp0R
  , CoAxiomRule
axExp1R
  , CoAxiomRule
axCmpNatRefl
  , CoAxiomRule
axCmpSymbolRefl
  , CoAxiomRule
axCmpCharRefl
  , CoAxiomRule
axSubDef
  , CoAxiomRule
axSub0R
  , CoAxiomRule
axAppendSymbol0R
  , CoAxiomRule
axAppendSymbol0L
  , CoAxiomRule
axDivDef
  , CoAxiomRule
axDiv1
  , CoAxiomRule
axModDef
  , CoAxiomRule
axMod1
  , CoAxiomRule
axLogDef
  ]



{-------------------------------------------------------------------------------
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]

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

charSymbolPair :: Type -> Type -> Type
charSymbolPair :: Type -> Type -> Type
charSymbolPair = Type -> Type -> Type -> Type -> Type
mkPromotedPairTy Type
charTy Type
typeSymbolKind

charSymbolPairKind :: Kind
charSymbolPairKind :: Type
charSymbolPairKind = TyCon -> [Type] -> Type
mkTyConApp TyCon
pairTyCon [Type
charTy, Type
typeSymbolKind]

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

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

isOrderingLitTy :: Type -> Maybe Ordering
isOrderingLitTy :: Type -> Maybe Ordering
isOrderingLitTy Type
tc =
  do (tc1,[]) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
tc
     case () of
       ()
_ | TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
promotedLTDataCon -> Ordering -> Maybe Ordering
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Ordering
LT
         | TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
promotedEQDataCon -> Ordering -> Maybe Ordering
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Ordering
EQ
         | TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
promotedGTDataCon -> Ordering -> Maybe Ordering
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Ordering
GT
         | Bool
otherwise                -> Maybe Ordering
forall a. Maybe a
Nothing

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

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

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

mkAxiom1 :: String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 :: String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 String
str TypeEqn -> TypeEqn
f =
  CoAxiomRule
    { coaxrName :: FastString
coaxrName      = String -> FastString
fsLit String
str
    , coaxrAsmpRoles :: [Role]
coaxrAsmpRoles = [Role
Nominal]
    , coaxrRole :: Role
coaxrRole      = Role
Nominal
    , coaxrProves :: [TypeEqn] -> Maybe TypeEqn
coaxrProves    = \case [TypeEqn
eqn] -> 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


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
lexicalCompareFS 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

matchFamConsSymbol :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamConsSymbol :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamConsSymbol [Type
s,Type
t]
  | Just Char
x <- Maybe Char
mbX, Just FastString
y <- Maybe FastString
mbY =
    (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axConsSymbolDef, [Type
s,Type
t], FastString -> Type
mkStrLitTy (Char -> FastString -> FastString
consFS Char
x FastString
y))
  where
  mbX :: Maybe Char
mbX = Type -> Maybe Char
isCharLitTy Type
s
  mbY :: Maybe FastString
mbY = Type -> Maybe FastString
isStrLitTy Type
t
matchFamConsSymbol [Type]
_ = Maybe (CoAxiomRule, [Type], Type)
forall a. Maybe a
Nothing

computeUncons :: FastString -> Type
computeUncons :: FastString -> Type
computeUncons FastString
str = Type -> Maybe Type -> Type
mkPromotedMaybeTy Type
charSymbolPairKind (((Char, FastString) -> Type)
-> Maybe (Char, FastString) -> Maybe Type
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Char, FastString) -> Type
reifyCharSymbolPairTy (FastString -> Maybe (Char, FastString)
unconsFS FastString
str))
  where reifyCharSymbolPairTy :: (Char, FastString) -> Type
        reifyCharSymbolPairTy :: (Char, FastString) -> Type
reifyCharSymbolPairTy (Char
c, FastString
s) = Type -> Type -> Type
charSymbolPair (Char -> Type
mkCharLitTy Char
c) (FastString -> Type
mkStrLitTy FastString
s)

matchFamUnconsSymbol :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamUnconsSymbol :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamUnconsSymbol [Type
s]
  | Just FastString
x <- Maybe FastString
mbX =
    (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axUnconsSymbolDef, [Type
s], FastString -> Type
computeUncons FastString
x)
  where
  mbX :: Maybe FastString
mbX = Type -> Maybe FastString
isStrLitTy Type
s
matchFamUnconsSymbol [Type]
_ = Maybe (CoAxiomRule, [Type], Type)
forall a. Maybe a
Nothing

matchFamCharToNat :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamCharToNat :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamCharToNat [Type
c]
  | Just Char
c' <- Type -> Maybe Char
isCharLitTy Type
c, Integer
n <- Char -> Integer
charToInteger Char
c'
  = (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axCharToNatDef, [Type
c], Integer -> Type
mkNumLitTy Integer
n)
  | Bool
otherwise = Maybe (CoAxiomRule, [Type], Type)
forall a. Maybe a
Nothing
matchFamCharToNat [Type]
_ = Maybe (CoAxiomRule, [Type], Type)
forall a. Maybe a
Nothing

matchFamNatToChar :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamNatToChar :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamNatToChar [Type
n]
  | Just Integer
n' <- Type -> Maybe Integer
isNumLitTy Type
n, Just Char
c <- Integer -> Maybe Char
integerToChar Integer
n'
  = (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axNatToCharDef, [Type
n], Char -> Type
mkCharLitTy Char
c)
  | Bool
otherwise = Maybe (CoAxiomRule, [Type], Type)
forall a. Maybe a
Nothing
matchFamNatToChar [Type]
_ = Maybe (CoAxiomRule, [Type], Type)
forall a. Maybe a
Nothing

charToInteger :: Char -> Integer
charToInteger :: Char -> Integer
charToInteger Char
c = Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Char -> Int
Char.ord Char
c)

integerToChar :: Integer -> Maybe Char
integerToChar :: Integer -> Maybe Char
integerToChar Integer
n | Bool
inBounds = Char -> Maybe Char
forall a. a -> Maybe a
Just (Int -> Char
Char.chr (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
n))
  where inBounds :: Bool
inBounds = Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Char -> Integer
charToInteger Char
forall a. Bounded a => a
minBound Bool -> Bool -> Bool
&&
                   Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Char -> Integer
charToInteger Char
forall a. Bounded a => a
maxBound
integerToChar Integer
_ = Maybe Char
forall a. Maybe a
Nothing

{-------------------------------------------------------------------------------
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...



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 a b. (a -> b) -> Maybe a -> Maybe b
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 a b. (a -> b) -> Maybe a -> Maybe b
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 a. [a] -> 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 a b. (a -> b) -> Maybe a -> Maybe b
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 a b. (a -> b) -> Maybe a -> Maybe b
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 a. [a] -> 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 a. [a] -> 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
_ = []

interactTopConsSymbol :: [Xi] -> Xi -> [Pair Type]
interactTopConsSymbol :: [Type] -> Type -> [TypeEqn]
interactTopConsSymbol [Type
s,Type
t] Type
r
  -- ConsSymbol a b ~ "blah" => (a ~ 'b', b ~ "lah")
  | Just FastString
fs <- Type -> Maybe FastString
isStrLitTy Type
r
  , Just (Char
x, FastString
xs) <- FastString -> Maybe (Char, FastString)
unconsFS FastString
fs =
    [ Type
s Type -> Type -> TypeEqn
=== Char -> Type
mkCharLitTy Char
x, Type
t Type -> Type -> TypeEqn
=== FastString -> Type
mkStrLitTy FastString
xs ]

interactTopConsSymbol [Type]
_ Type
_ = []

interactTopUnconsSymbol :: [Xi] -> Xi -> [Pair Type]
interactTopUnconsSymbol :: [Type] -> Type -> [TypeEqn]
interactTopUnconsSymbol [Type
s] Type
r
  -- (UnconsSymbol b ~ Nothing) => (b ~ "")
  | Just Maybe Type
Nothing <- Maybe (Maybe Type)
mbX =
    [ Type
s Type -> Type -> TypeEqn
=== FastString -> Type
mkStrLitTy FastString
nilFS ]
  -- (UnconsSymbol b ~ Just ('f',"oobar")) => (b ~ "foobar")
  | Just (Just Type
r) <- Maybe (Maybe Type)
mbX
  , Just (Type
c, Type
str) <- Type -> Maybe (Type, Type)
isPromotedPairType Type
r
  , Just Char
chr <- Type -> Maybe Char
isCharLitTy Type
c
  , Just FastString
str1 <- Type -> Maybe FastString
isStrLitTy Type
str =
    [ Type
s Type -> Type -> TypeEqn
=== (FastString -> Type
mkStrLitTy (FastString -> Type) -> FastString -> Type
forall a b. (a -> b) -> a -> b
$ Char -> FastString -> FastString
consFS Char
chr FastString
str1) ]

  where
  mbX :: Maybe (Maybe Type)
mbX = Type -> Maybe (Maybe Type)
isPromotedMaybeTy Type
r

interactTopUnconsSymbol [Type]
_ Type
_ = []

interactTopCharToNat :: [Xi] -> Xi -> [Pair Type]
interactTopCharToNat :: [Type] -> Type -> [TypeEqn]
interactTopCharToNat [Type
s] Type
r
  -- (CharToNat c ~ 122) => (c ~ 'z')
  | Just Integer
n <- Type -> Maybe Integer
isNumLitTy Type
r
  , Just Char
c <- Integer -> Maybe Char
integerToChar Integer
n
  = [ Type
s Type -> Type -> TypeEqn
=== Char -> Type
mkCharLitTy Char
c ]
interactTopCharToNat [Type]
_ Type
_ = []

interactTopNatToChar :: [Xi] -> Xi -> [Pair Type]
interactTopNatToChar :: [Type] -> Type -> [TypeEqn]
interactTopNatToChar [Type
s] Type
r
  -- (NatToChar n ~ 'z') => (n ~ 122)
  | Just Char
c <- Type -> Maybe Char
isCharLitTy Type
r
  = [ Type
s Type -> Type -> TypeEqn
=== Integer -> Type
mkNumLitTy (Char -> Integer
charToInteger Char
c) ]
interactTopNatToChar [Type]
_ Type
_ = []

{-------------------------------------------------------------------------------
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
_ = []


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


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

interactInertUnconsSymbol :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
interactInertUnconsSymbol :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
interactInertUnconsSymbol [Type
x1] Type
z1 [Type
x2] Type
z2
  | HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
tcEqType Type
z1 Type
z2 = [ Type
x1 Type -> Type -> TypeEqn
=== Type
x2 ]
interactInertUnconsSymbol [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 (z,True) <- Integer -> Integer -> Maybe (Integer, Bool)
genLog Integer
x Integer
y
                  return 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 (z,True) <- Integer -> Integer -> Maybe (Integer, Bool)
genRoot Integer
x Integer
y
                   return z



{- | Compute the n-th root of a natural number, rounded down to
the closest natural number.  The boolean indicates if the result
is exact (i.e., True means no rounding was done, False means rounded down).
The second argument specifies which root we are computing. -}
genRoot :: Integer -> Integer -> Maybe (Integer, Bool)
genRoot :: 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)
exactLoop Integer
0 Integer
x)
  where
  exactLoop :: Integer -> Integer -> (Integer, Bool)
exactLoop Integer
s Integer
i
    | Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1     = (Integer
s,Bool
True)
    | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
base   = (Integer
s,Bool
False)
    | Bool
otherwise  =
        let s1 :: Integer
s1 = Integer
s Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1
        in Integer
s1 Integer -> (Integer, Bool) -> (Integer, Bool)
forall a b. a -> b -> b
`seq` case Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
divMod Integer
i Integer
base of
                      (Integer
j,Integer
r)
                        | Integer
r Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0    -> Integer -> Integer -> (Integer, Bool)
exactLoop Integer
s1 Integer
j
                        | Bool
otherwise -> (Integer -> Integer -> Integer
underLoop Integer
s1 Integer
j, Bool
False)

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

-----------------------------------------------------------------------------

typeCharCmpTyCon :: TyCon
typeCharCmpTyCon :: TyCon
typeCharCmpTyCon =
  Name
-> [TyConBinder]
-> Type
-> Maybe Name
-> FamTyConFlav
-> Maybe Class
-> Injectivity
-> TyCon
mkFamilyTyCon Name
name
    ([Type] -> [TyConBinder]
mkTemplateAnonTyConBinders [ Type
charTy, Type
charTy ])
    Type
orderingKind
    Maybe Name
forall a. Maybe a
Nothing
    (BuiltInSynFamily -> FamTyConFlav
BuiltInSynFamTyCon BuiltInSynFamily
ops)
    Maybe Class
forall a. Maybe a
Nothing
    Injectivity
NotInjective
  where
  name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_INTERNAL_TYPELITS_INTERNAL (String -> FastString
fsLit String
"CmpChar")
                  Unique
typeCharCmpTyFamNameKey TyCon
typeCharCmpTyCon
  ops :: BuiltInSynFamily
ops = BuiltInSynFamily
      { sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
sfMatchFam      = [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamCmpChar
      , sfInteractTop :: [Type] -> Type -> [TypeEqn]
sfInteractTop   = [Type] -> Type -> [TypeEqn]
interactTopCmpChar
      , sfInteractInert :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
sfInteractInert = \[Type]
_ Type
_ [Type]
_ Type
_ -> []
      }

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

cmpChar :: Type -> Type -> Type
cmpChar :: Type -> Type -> Type
cmpChar Type
s Type
t = TyCon -> [Type] -> Type
mkTyConApp TyCon
typeCharCmpTyCon [Type
s,Type
t]

axCmpCharDef, axCmpCharRefl :: CoAxiomRule
axCmpCharDef :: CoAxiomRule
axCmpCharDef =
  String
-> TyCon
-> (Type -> Maybe Char)
-> (Type -> Maybe Char)
-> (Char -> Char -> Maybe Type)
-> CoAxiomRule
forall a b.
String
-> TyCon
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> CoAxiomRule
mkBinAxiom String
"CmpCharDef" TyCon
typeCharCmpTyCon Type -> Maybe Char
isCharLitTy Type -> Maybe Char
isCharLitTy ((Char -> Char -> Maybe Type) -> CoAxiomRule)
-> (Char -> Char -> Maybe Type) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$
    \Char
chr1 Char
chr2 -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Ordering -> Type
ordering (Ordering -> Type) -> Ordering -> Type
forall a b. (a -> b) -> a -> b
$ Char -> Char -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Char
chr1 Char
chr2
axCmpCharRefl :: CoAxiomRule
axCmpCharRefl = String -> (TypeEqn -> TypeEqn) -> CoAxiomRule
mkAxiom1 String
"CmpCharRefl"
  ((TypeEqn -> TypeEqn) -> CoAxiomRule)
-> (TypeEqn -> TypeEqn) -> CoAxiomRule
forall a b. (a -> b) -> a -> b
$ \(Pair Type
s Type
_) -> (Type -> Type -> Type
cmpChar Type
s Type
s) Type -> Type -> TypeEqn
=== Ordering -> Type
ordering Ordering
EQ

matchFamCmpChar :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamCmpChar :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamCmpChar [Type
s,Type
t]
  | Just Char
x <- Maybe Char
mbX, Just Char
y <- Maybe Char
mbY =
    (CoAxiomRule, [Type], Type) -> Maybe (CoAxiomRule, [Type], Type)
forall a. a -> Maybe a
Just (CoAxiomRule
axCmpCharDef, [Type
s,Type
t], Ordering -> Type
ordering (Char -> Char -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Char
x Char
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
axCmpCharRefl, [Type
s], Ordering -> Type
ordering Ordering
EQ)
  where mbX :: Maybe Char
mbX = Type -> Maybe Char
isCharLitTy Type
s
        mbY :: Maybe Char
mbY = Type -> Maybe Char
isCharLitTy Type
t
matchFamCmpChar [Type]
_ = Maybe (CoAxiomRule, [Type], Type)
forall a. Maybe a
Nothing