{-# LANGUAGE LambdaCase #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}   -- See calls to mkTemplateTyVars

module GHC.Builtin.Types.Literals
  ( tryInteractInertFam, tryInteractTopFam, tryMatchFam

  , typeNatTyCons
  , typeNatCoAxiomRules
  , BuiltInSynFamily(..)

    -- If you define a new built-in type family, make sure to export its TyCon
    -- from here as well.
    -- See Note [Adding built-in type families]
  , typeNatAddTyCon
  , typeNatMulTyCon
  , typeNatExpTyCon
  , typeNatSubTyCon
  , typeNatDivTyCon
  , typeNatModTyCon
  , typeNatLogTyCon
  , typeNatCmpTyCon
  , typeSymbolCmpTyCon
  , typeSymbolAppendTyCon
  , typeCharCmpTyCon
  , typeConsSymbolTyCon
  , typeUnconsSymbolTyCon
  , typeCharToNatTyCon
  , typeNatToCharTyCon
  ) where

import GHC.Prelude

import GHC.Core.Type
import GHC.Core.Unify      ( tcMatchTys )
import GHC.Data.Pair
import GHC.Core.TyCon    ( TyCon, FamTyConFlav(..), mkFamilyTyCon, tyConArity
                         , Injectivity(..), isBuiltInSynFamTyCon_maybe )
import GHC.Core.Coercion.Axiom
import GHC.Core.TyCo.Compare   ( tcEqType )
import GHC.Types.Name          ( Name, BuiltInSyntax(..) )
import GHC.Types.Unique.FM
import GHC.Builtin.Types
import GHC.Builtin.Types.Prim  ( mkTemplateAnonTyConBinders, mkTemplateTyVars )
import GHC.Builtin.Names
                  ( gHC_INTERNAL_TYPELITS
                  , gHC_INTERNAL_TYPELITS_INTERNAL
                  , gHC_INTERNAL_TYPENATS
                  , gHC_INTERNAL_TYPENATS_INTERNAL
                  , typeNatAddTyFamNameKey
                  , typeNatMulTyFamNameKey
                  , typeNatExpTyFamNameKey
                  , typeNatSubTyFamNameKey
                  , typeNatDivTyFamNameKey
                  , typeNatModTyFamNameKey
                  , typeNatLogTyFamNameKey
                  , typeNatCmpTyFamNameKey
                  , typeSymbolCmpTyFamNameKey
                  , typeSymbolAppendFamNameKey
                  , typeCharCmpTyFamNameKey
                  , typeConsSymbolTyFamNameKey
                  , typeUnconsSymbolTyFamNameKey
                  , typeCharToNatTyFamNameKey
                  , typeNatToCharTyFamNameKey
                  )
import GHC.Data.FastString
import GHC.Utils.Panic
import GHC.Utils.Outputable

import Control.Monad ( guard )
import Data.List  ( isPrefixOf, isSuffixOf )
import Data.Maybe ( listToMaybe )
import qualified Data.Char as Char

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

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

See also the Wiki page:

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

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

* Adding a unique for the type family TyCon

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

* Adding the type family TyCon itself

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

  Once your TyCon has been defined, be sure to:

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

* Define the type family somewhere

  Finally, you will need to define the type family somewhere, likely in @base@.
  Currently, all of the built-in type families are defined in GHC.TypeLits or
  GHC.TypeNats, so those are likely candidates.

  Since the behavior of your built-in type family is specified in GHC.Builtin.Types.Literals,
  you should give an open type family definition with no instances, like so:

    type family MyTypeFam (m :: Nat) (n :: Nat) :: Nat

  Changing the argument and result kinds as appropriate.

* Update the relevant test cases

  The GHC test suite will likely need to be updated after you add your built-in
  type family. For instance:

  - The T9181 test prints the :browse contents of GHC.TypeLits, so if you added
    a test there, the expected output of T9181 will need to change.
  - The TcTypeNatSimple and TcTypeSymbolSimple tests have compile-time unit
    tests, as well as TcTypeNatSimpleRun and TcTypeSymbolSimpleRun, which have
    runtime unit tests. Consider adding further unit tests to those if your
    built-in type family deals with Nats or Symbols, respectively.

Note [Inlining axiom constructors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We have a number of constructor functions with types like
   mkUnaryConstFoldAxiom :: TyCon -> String
                         -> (Type -> Maybe a)
                         -> (a -> Maybe Type)
                         -> BuiltInFamRewrite

For very type-family-heavy code, these higher order argument are inefficient;
e.g. the fourth argument might always return (Just ty) in the above. Inlining
them is a bit brutal, but not bad, makes a few-percent difference in, say
perf test T13386.

These functions aren't exported, so the effect is very local.

-}

-------------------------------------------------------------------------------
--     Key utility functions
-------------------------------------------------------------------------------

tryInteractTopFam :: BuiltInSynFamily -> TyCon -> [Type] -> Type
                  -> [(CoAxiomRule, TypeEqn)]
-- The returned CoAxiomRule is always unary
tryInteractTopFam :: BuiltInSynFamily
-> TyCon -> [Type] -> Type -> [(CoAxiomRule, TypeEqn)]
tryInteractTopFam BuiltInSynFamily
fam TyCon
fam_tc [Type]
tys Type
r
  = [(BuiltInFamInjectivity -> CoAxiomRule
bifinj_axr BuiltInFamInjectivity
bif, TypeEqn
eqn_out) | BuiltInFamInjectivity
bif  <- BuiltInSynFamily -> [BuiltInFamInjectivity]
sfInteract BuiltInSynFamily
fam
                               , Just TypeEqn
eqn_out <- [BuiltInFamInjectivity -> TypeEqn -> Maybe TypeEqn
bifinj_proves BuiltInFamInjectivity
bif TypeEqn
eqn_in] ]
  where
    eqn_in :: TypeEqn
    eqn_in :: TypeEqn
eqn_in = Type -> Type -> TypeEqn
forall a. a -> a -> Pair a
Pair (TyCon -> [Type] -> Type
mkTyConApp TyCon
fam_tc [Type]
tys) Type
r

tryInteractInertFam :: BuiltInSynFamily -> TyCon
                    -> [Type] -> [Type] -- F tys1 ~ F tys2
                    -> [(CoAxiomRule, TypeEqn)]
tryInteractInertFam :: BuiltInSynFamily
-> TyCon -> [Type] -> [Type] -> [(CoAxiomRule, TypeEqn)]
tryInteractInertFam BuiltInSynFamily
builtin_fam TyCon
fam_tc [Type]
tys1 [Type]
tys2
  = [(BuiltInFamInjectivity -> CoAxiomRule
bifinj_axr BuiltInFamInjectivity
bif, TypeEqn
eqn_out) | BuiltInFamInjectivity
bif <- BuiltInSynFamily -> [BuiltInFamInjectivity]
sfInteract BuiltInSynFamily
builtin_fam
                               , Just TypeEqn
eqn_out <- [BuiltInFamInjectivity -> TypeEqn -> Maybe TypeEqn
bifinj_proves BuiltInFamInjectivity
bif TypeEqn
eqn_in] ]
  where
    eqn_in :: TypeEqn
eqn_in = Type -> Type -> TypeEqn
forall a. a -> a -> Pair a
Pair (TyCon -> [Type] -> Type
mkTyConApp TyCon
fam_tc [Type]
tys1) (TyCon -> [Type] -> Type
mkTyConApp TyCon
fam_tc [Type]
tys2)

tryMatchFam :: BuiltInSynFamily -> [Type]
            -> Maybe (CoAxiomRule, [Type], Type)
-- Does this reduce on the given arguments?
-- If it does, returns (CoAxiomRule, types to instantiate the rule at, rhs type)
-- That is: mkAxiomCo (BuiltInFamRew ax) (map mkNomReflCo ts)
--              :: F tys ~r rhs,
tryMatchFam :: BuiltInSynFamily -> [Type] -> Maybe (CoAxiomRule, [Type], Type)
tryMatchFam BuiltInSynFamily
builtin_fam [Type]
arg_tys
  = [(CoAxiomRule, [Type], Type)] -> Maybe (CoAxiomRule, [Type], Type)
forall a. [a] -> Maybe a
listToMaybe ([(CoAxiomRule, [Type], Type)]
 -> Maybe (CoAxiomRule, [Type], Type))
-> [(CoAxiomRule, [Type], Type)]
-> Maybe (CoAxiomRule, [Type], Type)
forall a b. (a -> b) -> a -> b
$   -- Pick first rule to match
    [ (BuiltInFamRewrite -> CoAxiomRule
bifrw_axr BuiltInFamRewrite
rw_ax, [Type]
inst_tys, Type
res_ty)
    | BuiltInFamRewrite
rw_ax <- BuiltInSynFamily -> [BuiltInFamRewrite]
sfMatchFam BuiltInSynFamily
builtin_fam
    , Just ([Type]
inst_tys,Type
res_ty) <- [BuiltInFamRewrite -> [Type] -> Maybe ([Type], Type)
bifrw_match BuiltInFamRewrite
rw_ax [Type]
arg_tys] ]

-------------------------------------------------------------------------------
--          Constructing BuiltInFamInjectivity, BuiltInFamRewrite
-------------------------------------------------------------------------------

mkUnaryConstFoldAxiom :: TyCon -> String
                      -> (Type -> Maybe a)
                      -> (a -> Maybe Type)
                      -> BuiltInFamRewrite
-- For the definitional axioms, like  (3+4 --> 7)
{-# INLINE mkUnaryConstFoldAxiom #-}  -- See Note [Inlining axiom constructors]
mkUnaryConstFoldAxiom :: forall a.
TyCon
-> String
-> (Type -> Maybe a)
-> (a -> Maybe Type)
-> BuiltInFamRewrite
mkUnaryConstFoldAxiom TyCon
fam_tc String
str Type -> Maybe a
isReqTy a -> Maybe Type
f
  = BuiltInFamRewrite
bif
  where
    bif :: BuiltInFamRewrite
bif = BIF_Rewrite
      { bifrw_name :: FastString
bifrw_name   = String -> FastString
fsLit String
str
      , bifrw_axr :: CoAxiomRule
bifrw_axr    = BuiltInFamRewrite -> CoAxiomRule
BuiltInFamRew BuiltInFamRewrite
bif
      , bifrw_fam_tc :: TyCon
bifrw_fam_tc = TyCon
fam_tc
      , bifrw_arity :: Int
bifrw_arity  = Int
1
      , bifrw_match :: [Type] -> Maybe ([Type], Type)
bifrw_match  = \[Type]
ts -> do { [t1] <- [Type] -> Maybe [Type]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return [Type]
ts
                                 ; t1' <- isReqTy t1
                                 ; res <- f t1'
                                 ; return ([t1], res) }
      , bifrw_proves :: [TypeEqn] -> Maybe TypeEqn
bifrw_proves = \[TypeEqn]
cs -> do { [Pair s1 s2] <- [TypeEqn] -> Maybe [TypeEqn]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return [TypeEqn]
cs
                                 ; s2' <- isReqTy s2
                                 ; z   <- f s2'
                                 ; return (mkTyConApp fam_tc [s1] === z) }
      }

mkBinConstFoldAxiom :: TyCon -> String
                    -> (Type -> Maybe a)
                    -> (Type -> Maybe b)
                    -> (a -> b -> Maybe Type)
                    -> BuiltInFamRewrite
-- For the definitional axioms, like  (3+4 --> 7)
{-# INLINE mkBinConstFoldAxiom #-}  -- See Note [Inlining axiom constructors]
mkBinConstFoldAxiom :: forall a b.
TyCon
-> String
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> BuiltInFamRewrite
mkBinConstFoldAxiom TyCon
fam_tc String
str Type -> Maybe a
isReqTy1 Type -> Maybe b
isReqTy2 a -> b -> Maybe Type
f
  = BuiltInFamRewrite
bif
  where
    bif :: BuiltInFamRewrite
bif = BIF_Rewrite
      { bifrw_name :: FastString
bifrw_name   = String -> FastString
fsLit String
str
      , bifrw_axr :: CoAxiomRule
bifrw_axr    = BuiltInFamRewrite -> CoAxiomRule
BuiltInFamRew BuiltInFamRewrite
bif
      , bifrw_fam_tc :: TyCon
bifrw_fam_tc = TyCon
fam_tc
      , bifrw_arity :: Int
bifrw_arity  = Int
2
      , bifrw_match :: [Type] -> Maybe ([Type], Type)
bifrw_match  = \[Type]
ts -> do { [t1,t2] <- [Type] -> Maybe [Type]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return [Type]
ts
                                 ; t1' <- isReqTy1 t1
                                 ; t2' <- isReqTy2 t2
                                 ; res <- f t1' t2'
                                 ; return ([t1,t2], res) }
      , bifrw_proves :: [TypeEqn] -> Maybe TypeEqn
bifrw_proves = \[TypeEqn]
cs -> do { [Pair s1 s2, Pair t1 t2] <- [TypeEqn] -> Maybe [TypeEqn]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return [TypeEqn]
cs
                                 ; s2' <- isReqTy1 s2
                                 ; t2' <- isReqTy2 t2
                                 ; z   <- f s2' t2'
                                 ; return (mkTyConApp fam_tc [s1,t1] === z) }
      }

mkRewriteAxiom :: TyCon -> String
               -> [TyVar] -> [Type]  -- LHS of axiom
               -> Type               -- RHS of axiom
               -> BuiltInFamRewrite
-- Not higher order, no benefit in inlining
-- See Note [Inlining axiom constructors]
mkRewriteAxiom :: TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
mkRewriteAxiom TyCon
fam_tc String
str [TyVar]
tpl_tvs [Type]
lhs_tys Type
rhs_ty
  = Bool -> SDoc -> BuiltInFamRewrite -> BuiltInFamRewrite
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (TyCon -> Int
tyConArity TyCon
fam_tc Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
lhs_tys) (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
str SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
lhs_tys) (BuiltInFamRewrite -> BuiltInFamRewrite)
-> BuiltInFamRewrite -> BuiltInFamRewrite
forall a b. (a -> b) -> a -> b
$
    BuiltInFamRewrite
bif
  where
    bif :: BuiltInFamRewrite
bif = BIF_Rewrite
      { bifrw_name :: FastString
bifrw_name   = String -> FastString
fsLit String
str
      , bifrw_axr :: CoAxiomRule
bifrw_axr    = BuiltInFamRewrite -> CoAxiomRule
BuiltInFamRew BuiltInFamRewrite
bif
      , bifrw_fam_tc :: TyCon
bifrw_fam_tc = TyCon
fam_tc
      , bifrw_arity :: Int
bifrw_arity  = Int
bif_arity
      , bifrw_match :: [Type] -> Maybe ([Type], Type)
bifrw_match  = [Type] -> Maybe ([Type], Type)
match_fn
      , bifrw_proves :: [TypeEqn] -> Maybe TypeEqn
bifrw_proves = [TypeEqn] -> Maybe TypeEqn
inst_fn }

    bif_arity :: Int
bif_arity = [TyVar] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TyVar]
tpl_tvs

    match_fn :: [Type] -> Maybe ([Type],Type)
    match_fn :: [Type] -> Maybe ([Type], Type)
match_fn [Type]
arg_tys
      = Bool -> SDoc -> Maybe ([Type], Type) -> Maybe ([Type], Type)
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (TyCon -> Int
tyConArity TyCon
fam_tc Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
arg_tys) (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
str SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
arg_tys) (Maybe ([Type], Type) -> Maybe ([Type], Type))
-> Maybe ([Type], Type) -> Maybe ([Type], Type)
forall a b. (a -> b) -> a -> b
$
        case [Type] -> [Type] -> Maybe Subst
tcMatchTys [Type]
lhs_tys [Type]
arg_tys of
          Maybe Subst
Nothing    -> Maybe ([Type], Type)
forall a. Maybe a
Nothing
          Just Subst
subst -> ([Type], Type) -> Maybe ([Type], Type)
forall a. a -> Maybe a
Just (Subst -> [TyVar] -> [Type]
substTyVars Subst
subst [TyVar]
tpl_tvs, HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst Type
rhs_ty)

    inst_fn :: [TypeEqn] -> Maybe TypeEqn
    inst_fn :: [TypeEqn] -> Maybe TypeEqn
inst_fn [TypeEqn]
inst_eqns
      = Bool -> SDoc -> Maybe TypeEqn -> Maybe TypeEqn
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr ([TypeEqn] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeEqn]
inst_eqns Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
bif_arity) (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
str SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [TypeEqn] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TypeEqn]
inst_eqns) (Maybe TypeEqn -> Maybe TypeEqn) -> Maybe TypeEqn -> Maybe TypeEqn
forall a b. (a -> b) -> a -> b
$
        TypeEqn -> Maybe TypeEqn
forall a. a -> Maybe a
Just (TyCon -> [Type] -> Type
mkTyConApp TyCon
fam_tc (HasDebugCallStack => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
substTys ([TyVar] -> [Type] -> Subst
HasDebugCallStack => [TyVar] -> [Type] -> Subst
zipTCvSubst [TyVar]
tpl_tvs [Type]
tys1) [Type]
lhs_tys)
              Type -> Type -> TypeEqn
===
              HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy ([TyVar] -> [Type] -> Subst
HasDebugCallStack => [TyVar] -> [Type] -> Subst
zipTCvSubst [TyVar]
tpl_tvs [Type]
tys2) Type
rhs_ty)
      where
        ([Type]
tys1, [Type]
tys2) = [TypeEqn] -> ([Type], [Type])
forall a. [Pair a] -> ([a], [a])
unzipPairs [TypeEqn]
inst_eqns

mkTopUnaryFamDeduction :: String -> TyCon
                     -> (Type -> Type -> Maybe TypeEqn)
                     -> BuiltInFamInjectivity
-- Deduction from (F s ~ r) where `F` is a unary type function
{-# INLINE mkTopUnaryFamDeduction #-}  -- See Note [Inlining axiom constructors]
mkTopUnaryFamDeduction :: String
-> TyCon
-> (Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopUnaryFamDeduction String
str TyCon
fam_tc Type -> Type -> Maybe TypeEqn
f
  = BuiltInFamInjectivity
bif
  where
    bif :: BuiltInFamInjectivity
bif = BIF_Interact
      { bifinj_name :: FastString
bifinj_name   = String -> FastString
fsLit String
str
      , bifinj_axr :: CoAxiomRule
bifinj_axr    = BuiltInFamInjectivity -> CoAxiomRule
BuiltInFamInj BuiltInFamInjectivity
bif
      , bifinj_proves :: TypeEqn -> Maybe TypeEqn
bifinj_proves = \(Pair Type
lhs Type
rhs)
                        -> do { (tc, [a]) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
lhs
                              ; massertPpr (tc == fam_tc) (ppr tc $$ ppr fam_tc)
                              ; f a rhs } }

mkTopBinFamDeduction :: String -> TyCon
                     -> (Type -> Type -> Type -> Maybe TypeEqn)
                     -> BuiltInFamInjectivity
-- Deduction from (F s t  ~ r) where `F` is a binary type function
{-# INLINE mkTopBinFamDeduction #-}  -- See Note [Inlining axiom constructors]
mkTopBinFamDeduction :: String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
str TyCon
fam_tc Type -> Type -> Type -> Maybe TypeEqn
f
  = BuiltInFamInjectivity
bif
  where
    bif :: BuiltInFamInjectivity
bif = BIF_Interact
      { bifinj_name :: FastString
bifinj_name   = String -> FastString
fsLit String
str
      , bifinj_axr :: CoAxiomRule
bifinj_axr    = BuiltInFamInjectivity -> CoAxiomRule
BuiltInFamInj BuiltInFamInjectivity
bif
      , bifinj_proves :: TypeEqn -> Maybe TypeEqn
bifinj_proves = \(Pair Type
lhs Type
rhs) ->
                        do { (tc, [a,b]) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
lhs
                           ; massertPpr (tc == fam_tc) (ppr tc $$ ppr fam_tc)
                           ; f a b rhs } }

mkUnaryBIF :: String -> TyCon -> BuiltInFamInjectivity
-- Not higher order, no benefit in inlining
-- See Note [Inlining axiom constructors]
mkUnaryBIF :: String -> TyCon -> BuiltInFamInjectivity
mkUnaryBIF String
str TyCon
fam_tc
  = BuiltInFamInjectivity
bif
  where
    bif :: BuiltInFamInjectivity
bif = BIF_Interact { bifinj_name :: FastString
bifinj_name   = String -> FastString
fsLit String
str
                       , bifinj_axr :: CoAxiomRule
bifinj_axr    = BuiltInFamInjectivity -> CoAxiomRule
BuiltInFamInj BuiltInFamInjectivity
bif
                       , bifinj_proves :: TypeEqn -> Maybe TypeEqn
bifinj_proves = TypeEqn -> Maybe TypeEqn
proves }
    proves :: TypeEqn -> Maybe TypeEqn
proves (Pair Type
lhs Type
rhs)
      = do { (tc2, [x2]) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
rhs
           ; guard (tc2 == fam_tc)
           ; (tc1, [x1]) <- splitTyConApp_maybe lhs
           ; massertPpr (tc1 == fam_tc) (ppr tc1 $$ ppr fam_tc)
           ; return (Pair x1 x2) }

mkBinBIF :: String -> TyCon
         -> WhichArg -> WhichArg
         -> (Type -> Bool)         -- The guard on the equal args, if any
         -> BuiltInFamInjectivity
{-# INLINE mkBinBIF #-}  -- See Note [Inlining axiom constructors]
mkBinBIF :: String
-> TyCon
-> WhichArg
-> WhichArg
-> (Type -> Bool)
-> BuiltInFamInjectivity
mkBinBIF String
str TyCon
fam_tc WhichArg
eq1 WhichArg
eq2 Type -> Bool
check_me
  = BuiltInFamInjectivity
bif
  where
    bif :: BuiltInFamInjectivity
bif = BIF_Interact { bifinj_name :: FastString
bifinj_name   = String -> FastString
fsLit String
str
                       , bifinj_axr :: CoAxiomRule
bifinj_axr    = BuiltInFamInjectivity -> CoAxiomRule
BuiltInFamInj BuiltInFamInjectivity
bif
                       , bifinj_proves :: TypeEqn -> Maybe TypeEqn
bifinj_proves = TypeEqn -> Maybe TypeEqn
proves }
    proves :: TypeEqn -> Maybe TypeEqn
proves (Pair Type
lhs Type
rhs)
      = do { (tc2, [x2,y2]) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
rhs
           ; guard (tc2 == fam_tc)
           ; (tc1, [x1,y1]) <- splitTyConApp_maybe lhs
           ; massertPpr (tc1 == fam_tc) (ppr tc1 $$ ppr fam_tc)
           ; case (eq1, eq2) of
               (WhichArg
ArgX,WhichArg
ArgX) -> Type -> Type -> Type -> Type -> Maybe TypeEqn
do_it Type
x1 Type
x2 Type
y1 Type
y2
               (WhichArg
ArgX,WhichArg
ArgY) -> Type -> Type -> Type -> Type -> Maybe TypeEqn
do_it Type
x1 Type
y2 Type
x2 Type
y1
               (WhichArg
ArgY,WhichArg
ArgX) -> Type -> Type -> Type -> Type -> Maybe TypeEqn
do_it Type
y1 Type
x2 Type
y2 Type
x1
               (WhichArg
ArgY,WhichArg
ArgY) -> Type -> Type -> Type -> Type -> Maybe TypeEqn
do_it Type
y1 Type
y2 Type
x1 Type
x2 }

    do_it :: Type -> Type -> Type -> Type -> Maybe TypeEqn
do_it Type
a1 Type
a2 Type
b1 Type
b2 = do { Type -> Type -> Maybe ()
same Type
a1 Type
a2; Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Type -> Bool
check_me Type
a1); TypeEqn -> Maybe TypeEqn
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Type -> TypeEqn
forall a. a -> a -> Pair a
Pair Type
b1 Type
b2) }

noGuard :: Type -> Bool
noGuard :: Type -> Bool
noGuard Type
_ = Bool
True

numGuard :: (Integer -> Bool) -> Type -> Bool
numGuard :: (Integer -> Bool) -> Type -> Bool
numGuard Integer -> Bool
pred Type
ty = case Type -> Maybe Integer
isNumLitTy Type
ty of
                      Just Integer
n  -> Integer -> Bool
pred Integer
n
                      Maybe Integer
Nothing -> Bool
False

data WhichArg = ArgX | ArgY


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


-- 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
$
    [ (FastString, CoAxiomRule)
pr | TyCon
tc <- [TyCon]
typeNatTyCons
         , Just BuiltInSynFamily
ops <- [TyCon -> Maybe BuiltInSynFamily
isBuiltInSynFamTyCon_maybe TyCon
tc]
         , (FastString, CoAxiomRule)
pr <- [ (BuiltInFamInjectivity -> FastString
bifinj_name BuiltInFamInjectivity
bif, BuiltInFamInjectivity -> CoAxiomRule
bifinj_axr BuiltInFamInjectivity
bif) | BuiltInFamInjectivity
bif <- BuiltInSynFamily -> [BuiltInFamInjectivity]
sfInteract BuiltInSynFamily
ops ]
              [(FastString, CoAxiomRule)]
-> [(FastString, CoAxiomRule)] -> [(FastString, CoAxiomRule)]
forall a. [a] -> [a] -> [a]
++ [ (BuiltInFamRewrite -> FastString
bifrw_name BuiltInFamRewrite
bif,  BuiltInFamRewrite -> CoAxiomRule
bifrw_axr BuiltInFamRewrite
bif)  | BuiltInFamRewrite
bif <- BuiltInSynFamily -> [BuiltInFamRewrite]
sfMatchFam BuiltInSynFamily
ops ] ]

-------------------------------------------------------------------------------
--                   Addition (+)
-------------------------------------------------------------------------------

typeNatAddTyCon :: TyCon
typeNatAddTyCon :: TyCon
typeNatAddTyCon = Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon2 Name
name
  BuiltInSynFamily
    { sfMatchFam :: [BuiltInFamRewrite]
sfMatchFam  = [BuiltInFamRewrite]
axAddRewrites
    , sfInteract :: [BuiltInFamInjectivity]
sfInteract  = [BuiltInFamInjectivity]
axAddInjectivity
    }
  where
    name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_INTERNAL_TYPENATS (String -> FastString
fsLit String
"+")
              Unique
typeNatAddTyFamNameKey TyCon
typeNatAddTyCon


sn,tn :: TyVar  -- Of kind Natural
(TyVar
sn: TyVar
tn: [TyVar]
_) = [Type] -> [TyVar]
mkTemplateTyVars (Type -> [Type]
forall a. a -> [a]
repeat Type
typeSymbolKind)

axAddRewrites :: [BuiltInFamRewrite]
axAddRewrites :: [BuiltInFamRewrite]
axAddRewrites
  = [ TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
mkRewriteAxiom   TyCon
tc String
"Add0L" [TyVar
tn] [Integer -> Type
num Integer
0, TyVar -> Type
var TyVar
tn] (TyVar -> Type
var TyVar
tn)   -- 0 + t --> t
    , TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
mkRewriteAxiom   TyCon
tc String
"Add0R" [TyVar
sn] [TyVar -> Type
var TyVar
sn, Integer -> Type
num Integer
0] (TyVar -> Type
var TyVar
sn)   -- s + 0 --> s
    , TyCon
-> String
-> (Type -> Maybe Integer)
-> (Type -> Maybe Integer)
-> (Integer -> Integer -> Maybe Type)
-> BuiltInFamRewrite
forall a b.
TyCon
-> String
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> BuiltInFamRewrite
mkBinConstFoldAxiom TyCon
tc String
"AddDef" Type -> Maybe Integer
isNumLitTy Type -> Maybe Integer
isNumLitTy ((Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite)
-> (Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite
forall a b. (a -> b) -> a -> b
$     -- 3 + 4 --> 7
      \Integer
x Integer
y -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Integer -> Type
num (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
y) ]
  where
    tc :: TyCon
tc = TyCon
typeNatAddTyCon

axAddInjectivity :: [BuiltInFamInjectivity]
axAddInjectivity :: [BuiltInFamInjectivity]
axAddInjectivity
  = [ -- (s + t ~ 0) => (s ~ 0)
      String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"AddT-0L" TyCon
tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
a Type
_b Type
r ->
      do { _ <- Type -> (Integer -> Bool) -> Maybe Integer
known Type
r (Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0); return (Pair a (num 0)) }

    , -- (s + t ~ 0) => (t ~ 0)
      String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"AddT-0R" TyCon
tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
_a Type
b Type
r ->
      do { _ <- Type -> (Integer -> Bool) -> Maybe Integer
known Type
r (Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0); return (Pair b (num 0)) }

    , -- (5 + t ~ 8) => (t ~ 3)
      String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"AddT-KKL" TyCon
tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
a Type
b Type
r ->
      do { na <- Type -> Maybe Integer
isNumLitTy Type
a; nr <- known r (>= na); return (Pair b (num (nr-na))) }

    , -- (s + 5 ~ 8) => (s ~ 3)
      String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"AddT-KKR" TyCon
tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
a Type
b Type
r ->
      do { nb <- Type -> Maybe Integer
isNumLitTy Type
b; nr <- known r (>= nb); return (Pair a (num (nr-nb))) }

    , String
-> TyCon
-> WhichArg
-> WhichArg
-> (Type -> Bool)
-> BuiltInFamInjectivity
mkBinBIF String
"AddI-xx" TyCon
tc WhichArg
ArgX WhichArg
ArgX Type -> Bool
noGuard  -- x1+y1~x2+y2 {x1=x2}=> (y1 ~ y2)
    , String
-> TyCon
-> WhichArg
-> WhichArg
-> (Type -> Bool)
-> BuiltInFamInjectivity
mkBinBIF String
"AddI-xy" TyCon
tc WhichArg
ArgX WhichArg
ArgY Type -> Bool
noGuard  -- x1+y1~x2+y2 {x1=y2}=> (x2 ~ y1)
    , String
-> TyCon
-> WhichArg
-> WhichArg
-> (Type -> Bool)
-> BuiltInFamInjectivity
mkBinBIF String
"AddI-yx" TyCon
tc WhichArg
ArgY WhichArg
ArgX Type -> Bool
noGuard  -- x1+y1~x2+y2 {y1=x2}=> (x1 ~ y2)
    , String
-> TyCon
-> WhichArg
-> WhichArg
-> (Type -> Bool)
-> BuiltInFamInjectivity
mkBinBIF String
"AddI-yy" TyCon
tc WhichArg
ArgY WhichArg
ArgY Type -> Bool
noGuard  -- x1+y1~x2+y2 {y1=y2}=> (x1 ~ x2)
    ]
  where
    tc :: TyCon
tc = TyCon
typeNatAddTyCon

-------------------------------------------------------------------------------
--                   Subtraction (-)
-------------------------------------------------------------------------------

typeNatSubTyCon :: TyCon
typeNatSubTyCon :: TyCon
typeNatSubTyCon = Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon2 Name
name
  BuiltInSynFamily
    { sfMatchFam :: [BuiltInFamRewrite]
sfMatchFam = [BuiltInFamRewrite]
axSubRewrites
    , sfInteract :: [BuiltInFamInjectivity]
sfInteract = [BuiltInFamInjectivity]
axSubInjectivity
    }
  where
  name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_INTERNAL_TYPENATS (String -> FastString
fsLit String
"-")
            Unique
typeNatSubTyFamNameKey TyCon
typeNatSubTyCon

axSubRewrites :: [BuiltInFamRewrite]
axSubRewrites :: [BuiltInFamRewrite]
axSubRewrites
  = [ TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
mkRewriteAxiom   TyCon
tc String
"Sub0R" [TyVar
sn] [TyVar -> Type
var TyVar
sn, Integer -> Type
num Integer
0] (TyVar -> Type
var TyVar
sn)   -- s - 0 --> s
    , TyCon
-> String
-> (Type -> Maybe Integer)
-> (Type -> Maybe Integer)
-> (Integer -> Integer -> Maybe Type)
-> BuiltInFamRewrite
forall a b.
TyCon
-> String
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> BuiltInFamRewrite
mkBinConstFoldAxiom TyCon
tc String
"SubDef" Type -> Maybe Integer
isNumLitTy Type -> Maybe Integer
isNumLitTy ((Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite)
-> (Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite
forall a b. (a -> b) -> a -> b
$     -- 4 - 3 --> 1  if x>=y
      \Integer
x Integer
y -> (Integer -> Type) -> Maybe Integer -> Maybe Type
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Integer -> Type
num (Integer -> Integer -> Maybe Integer
minus Integer
x Integer
y) ]
  where
    tc :: TyCon
tc = TyCon
typeNatSubTyCon

axSubInjectivity :: [BuiltInFamInjectivity]
axSubInjectivity :: [BuiltInFamInjectivity]
axSubInjectivity
  = [ -- (a - b ~ 5) => (5 + b ~ a)
      String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"SubT" TyCon
tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
a Type
b Type
r ->
      do { _ <- Type -> Maybe Integer
isNumLitTy Type
r; return (Pair (r .+. b) a) }

    , String
-> TyCon
-> WhichArg
-> WhichArg
-> (Type -> Bool)
-> BuiltInFamInjectivity
mkBinBIF String
"SubI-xx" TyCon
tc WhichArg
ArgX WhichArg
ArgX Type -> Bool
noGuard -- (x-y1 ~ x-y2) => (y1 ~ y2)
    , String
-> TyCon
-> WhichArg
-> WhichArg
-> (Type -> Bool)
-> BuiltInFamInjectivity
mkBinBIF String
"SubI-yy" TyCon
tc WhichArg
ArgY WhichArg
ArgY Type -> Bool
noGuard -- (x1-y ~ x2-y) => (x1 ~ x2)
    ]
  where
    tc :: TyCon
tc = TyCon
typeNatSubTyCon

{-
Note [Weakened interaction rule for subtraction]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
A simpler interaction here might be:

  `s - t ~ r` --> `t + r ~ s`

This would enable us to reuse all the code for addition.
Unfortunately, this works a little too well at the moment.
Consider the following example:

    0 - 5 ~ r --> 5 + r ~ 0 --> (5 = 0, r = 0)

This (correctly) spots that the constraint cannot be solved.

However, this may be a problem if the constraint did not
need to be solved in the first place!  Consider the following example:

f :: Proxy (If (5 <=? 0) (0 - 5) (5 - 0)) -> Proxy 5
f = id

Currently, GHC is strict while evaluating functions, so this does not
work, because even though the `If` should evaluate to `5 - 0`, we
also evaluate the "then" branch which generates the constraint `0 - 5 ~ r`,
which fails.

So, for the time being, we only add an improvement when the RHS is a constant,
which happens to work OK for the moment, although clearly we need to do
something more general.
-}


-------------------------------------------------------------------------------
--                   Multiplication (*)
-------------------------------------------------------------------------------

typeNatMulTyCon :: TyCon
typeNatMulTyCon :: TyCon
typeNatMulTyCon = Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon2 Name
name
  BuiltInSynFamily { sfMatchFam :: [BuiltInFamRewrite]
sfMatchFam = [BuiltInFamRewrite]
axMulRewrites
                   , sfInteract :: [BuiltInFamInjectivity]
sfInteract = [BuiltInFamInjectivity]
axMulInjectivity  }
  where
    name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_INTERNAL_TYPENATS (String -> FastString
fsLit String
"*")
              Unique
typeNatMulTyFamNameKey TyCon
typeNatMulTyCon

axMulRewrites :: [BuiltInFamRewrite]
axMulRewrites :: [BuiltInFamRewrite]
axMulRewrites
  = [ TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
mkRewriteAxiom   TyCon
tc String
"Mul0L" [TyVar
tn] [Integer -> Type
num Integer
0, TyVar -> Type
var TyVar
tn] (Integer -> Type
num Integer
0)   -- 0 * t --> 0
    , TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
mkRewriteAxiom   TyCon
tc String
"Mul0R" [TyVar
sn] [TyVar -> Type
var TyVar
sn, Integer -> Type
num Integer
0] (Integer -> Type
num Integer
0)   -- s * 0 --> 0
    , TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
mkRewriteAxiom   TyCon
tc String
"Mul1L" [TyVar
tn] [Integer -> Type
num Integer
1, TyVar -> Type
var TyVar
tn] (TyVar -> Type
var TyVar
tn)  -- 1 * t --> t
    , TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
mkRewriteAxiom   TyCon
tc String
"Mul1R" [TyVar
sn] [TyVar -> Type
var TyVar
sn, Integer -> Type
num Integer
1] (TyVar -> Type
var TyVar
sn)  -- s * 1 --> s
    , TyCon
-> String
-> (Type -> Maybe Integer)
-> (Type -> Maybe Integer)
-> (Integer -> Integer -> Maybe Type)
-> BuiltInFamRewrite
forall a b.
TyCon
-> String
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> BuiltInFamRewrite
mkBinConstFoldAxiom TyCon
tc String
"MulDef" Type -> Maybe Integer
isNumLitTy Type -> Maybe Integer
isNumLitTy ((Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite)
-> (Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite
forall a b. (a -> b) -> a -> b
$    -- 3 + 4 --> 12
      \Integer
x Integer
y -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Integer -> Type
num (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
y) ]
  where
    tc :: TyCon
tc = TyCon
typeNatMulTyCon

axMulInjectivity :: [BuiltInFamInjectivity]
axMulInjectivity :: [BuiltInFamInjectivity]
axMulInjectivity
  = [ -- (s * t ~ 1)  => (s ~ 1)
      String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"MulT1" TyCon
tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
s Type
_t Type
r ->
      do { _ <- Type -> (Integer -> Bool) -> Maybe Integer
known Type
r (Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1); return (Pair s r) }

    , -- (s * t ~ 1)  => (t ~ 1)
      String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"MulT2" TyCon
tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
_s Type
t Type
r ->
      do { _ <- Type -> (Integer -> Bool) -> Maybe Integer
known Type
r (Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1); return (Pair t r) }

    , -- (3 * t ~ 15) => (t ~ 5)
      String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"MulT3" TyCon
tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
s Type
t Type
r ->
      do { ns <- Type -> Maybe Integer
isNumLitTy Type
s; nr <- isNumLitTy r; y <- divide nr ns; return (Pair t (num y)) }

    , -- (s * 3 ~ 15) => (s ~ 5)
      String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"MulT4" TyCon
tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
s Type
t Type
r ->
      do { nt <- Type -> Maybe Integer
isNumLitTy Type
t; nr <- isNumLitTy r; y <- divide nr nt; return (Pair s (num y)) }

    , String
-> TyCon
-> WhichArg
-> WhichArg
-> (Type -> Bool)
-> BuiltInFamInjectivity
mkBinBIF String
"MulI-xx" TyCon
tc WhichArg
ArgX WhichArg
ArgX ((Integer -> Bool) -> Type -> Bool
numGuard (Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0))    -- (x*y1 ~ x*y2) {x/=0}=> (y1 ~ y2)
    , String
-> TyCon
-> WhichArg
-> WhichArg
-> (Type -> Bool)
-> BuiltInFamInjectivity
mkBinBIF String
"MulI-yy" TyCon
tc WhichArg
ArgY WhichArg
ArgY ((Integer -> Bool) -> Type -> Bool
numGuard (Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0))    -- (x1*y ~ x2*y) {y/=0}=> (x1 ~ x2)
    ]
  where
    tc :: TyCon
tc = TyCon
typeNatMulTyCon


-------------------------------------------------------------------------------
--                   Division: Div and Mod
-------------------------------------------------------------------------------

typeNatDivTyCon :: TyCon
typeNatDivTyCon :: TyCon
typeNatDivTyCon = Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon2 Name
name
  BuiltInSynFamily { sfMatchFam :: [BuiltInFamRewrite]
sfMatchFam = [BuiltInFamRewrite]
axDivRewrites
                   , sfInteract :: [BuiltInFamInjectivity]
sfInteract = [] }
  where
  name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_INTERNAL_TYPENATS (String -> FastString
fsLit String
"Div")
            Unique
typeNatDivTyFamNameKey TyCon
typeNatDivTyCon

typeNatModTyCon :: TyCon
typeNatModTyCon :: TyCon
typeNatModTyCon = Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon2 Name
name
  BuiltInSynFamily { sfMatchFam :: [BuiltInFamRewrite]
sfMatchFam = [BuiltInFamRewrite]
axModRewrites
                   , sfInteract :: [BuiltInFamInjectivity]
sfInteract = [] }
  where
  name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_INTERNAL_TYPENATS (String -> FastString
fsLit String
"Mod")
            Unique
typeNatModTyFamNameKey TyCon
typeNatModTyCon

axDivRewrites :: [BuiltInFamRewrite]
axDivRewrites :: [BuiltInFamRewrite]
axDivRewrites
  = [ TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
mkRewriteAxiom   TyCon
tc String
"Div1" [TyVar
sn] [TyVar -> Type
var TyVar
sn, Integer -> Type
num Integer
1] (TyVar -> Type
var TyVar
sn)   -- s `div` 1 --> s
    , TyCon
-> String
-> (Type -> Maybe Integer)
-> (Type -> Maybe Integer)
-> (Integer -> Integer -> Maybe Type)
-> BuiltInFamRewrite
forall a b.
TyCon
-> String
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> BuiltInFamRewrite
mkBinConstFoldAxiom TyCon
tc String
"DivDef" Type -> Maybe Integer
isNumLitTy Type -> Maybe Integer
isNumLitTy ((Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite)
-> (Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite
forall a b. (a -> b) -> a -> b
$    -- 8 `div` 4 --> 2
      \Integer
x Integer
y -> do { Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
y Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0); Type -> Maybe Type
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Type
num (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div Integer
x Integer
y)) } ]
  where
    tc :: TyCon
tc = TyCon
typeNatDivTyCon

axModRewrites :: [BuiltInFamRewrite]
axModRewrites :: [BuiltInFamRewrite]
axModRewrites
  = [ TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
mkRewriteAxiom   TyCon
tc String
"Mod1" [TyVar
sn] [TyVar -> Type
var TyVar
sn, Integer -> Type
num Integer
1] (Integer -> Type
num Integer
0)   -- s `mod` 1 --> 0
    , TyCon
-> String
-> (Type -> Maybe Integer)
-> (Type -> Maybe Integer)
-> (Integer -> Integer -> Maybe Type)
-> BuiltInFamRewrite
forall a b.
TyCon
-> String
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> BuiltInFamRewrite
mkBinConstFoldAxiom TyCon
tc String
"ModDef" Type -> Maybe Integer
isNumLitTy Type -> Maybe Integer
isNumLitTy ((Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite)
-> (Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite
forall a b. (a -> b) -> a -> b
$   -- 8 `mod` 3 --> 2
      \Integer
x Integer
y -> do { Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
y Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0); Type -> Maybe Type
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Type
num (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
mod Integer
x Integer
y)) } ]
  where
    tc :: TyCon
tc = TyCon
typeNatModTyCon

-------------------------------------------------------------------------------
--                   Exponentiation: Exp
-------------------------------------------------------------------------------

typeNatExpTyCon :: TyCon  -- Exponentiation
typeNatExpTyCon :: TyCon
typeNatExpTyCon = Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon2 Name
name
  BuiltInSynFamily { sfMatchFam :: [BuiltInFamRewrite]
sfMatchFam = [BuiltInFamRewrite]
axExpRewrites
                   , sfInteract :: [BuiltInFamInjectivity]
sfInteract = [BuiltInFamInjectivity]
axExpInjectivity }
  where
  name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_INTERNAL_TYPENATS (String -> FastString
fsLit String
"^")
                Unique
typeNatExpTyFamNameKey TyCon
typeNatExpTyCon

axExpRewrites :: [BuiltInFamRewrite]
axExpRewrites :: [BuiltInFamRewrite]
axExpRewrites
  = [ TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
mkRewriteAxiom   TyCon
tc String
"Exp0R" [TyVar
sn] [TyVar -> Type
var TyVar
sn, Integer -> Type
num Integer
0] (Integer -> Type
num Integer
1)   -- s ^ 0 --> 1
    , TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
mkRewriteAxiom   TyCon
tc String
"Exp1L" [TyVar
tn] [Integer -> Type
num Integer
1, TyVar -> Type
var TyVar
tn] (Integer -> Type
num Integer
1)   -- 1 ^ t --> 1
    , TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
mkRewriteAxiom   TyCon
tc String
"Exp1R" [TyVar
sn] [TyVar -> Type
var TyVar
sn, Integer -> Type
num Integer
1] (TyVar -> Type
var TyVar
sn)  -- s ^ 1 --> s
    , TyCon
-> String
-> (Type -> Maybe Integer)
-> (Type -> Maybe Integer)
-> (Integer -> Integer -> Maybe Type)
-> BuiltInFamRewrite
forall a b.
TyCon
-> String
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> BuiltInFamRewrite
mkBinConstFoldAxiom TyCon
tc String
"ExpDef" Type -> Maybe Integer
isNumLitTy Type -> Maybe Integer
isNumLitTy ((Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite)
-> (Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite
forall a b. (a -> b) -> a -> b
$    -- 2 ^ 3 --> 8
      \Integer
x Integer
y -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Integer -> Type
num (Integer
x Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
y)) ]
  where
    tc :: TyCon
tc = TyCon
typeNatExpTyCon

axExpInjectivity :: [BuiltInFamInjectivity]
axExpInjectivity :: [BuiltInFamInjectivity]
axExpInjectivity
  = [ -- (s ^ t ~ 0) => (s ~ 0)
      String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"ExpT1" TyCon
tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
s Type
_t Type
r ->
      do { Integer -> Maybe TypeEqn
0 <- Type -> Maybe Integer
isNumLitTy Type
r; return (Pair s r) }

    , -- (2 ^ t ~ 8) => (t ~ 3)
      String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"ExpT2" TyCon
tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
s Type
t Type
r ->
      do { ns <- Type -> Maybe Integer
isNumLitTy Type
s; nr <- isNumLitTy r; y <- logExact nr ns; return (Pair t (num y)) }

    , -- (s ^ 2 ~ 9) => (s ~ 3)
      String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"ExpT3" TyCon
tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
s Type
t Type
r ->
      do { nt <- Type -> Maybe Integer
isNumLitTy Type
t; nr <- isNumLitTy r; y <- rootExact nr nt; return (Pair s (num y)) }

    , String
-> TyCon
-> WhichArg
-> WhichArg
-> (Type -> Bool)
-> BuiltInFamInjectivity
mkBinBIF String
"ExpI-xx" TyCon
tc WhichArg
ArgX WhichArg
ArgX ((Integer -> Bool) -> Type -> Bool
numGuard (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
1))    -- (x^y1 ~ x^y2) {x>1}=> (y1 ~ y2)
    , String
-> TyCon
-> WhichArg
-> WhichArg
-> (Type -> Bool)
-> BuiltInFamInjectivity
mkBinBIF String
"ExpI-yy" TyCon
tc WhichArg
ArgY WhichArg
ArgY ((Integer -> Bool) -> Type -> Bool
numGuard (Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0))   -- (x1*y ~ x2*y) {y/=0}=> (x1 ~ x2)
    ]
  where
    tc :: TyCon
tc = TyCon
typeNatExpTyCon

-------------------------------------------------------------------------------
--                   Logarithm: Log2
-------------------------------------------------------------------------------

typeNatLogTyCon :: TyCon
typeNatLogTyCon :: TyCon
typeNatLogTyCon = Name -> BuiltInSynFamily -> TyCon
mkTypeNatFunTyCon1 Name
name
  BuiltInSynFamily { sfMatchFam :: [BuiltInFamRewrite]
sfMatchFam = [BuiltInFamRewrite]
axLogRewrites
                   , sfInteract :: [BuiltInFamInjectivity]
sfInteract = [] }
  where
  name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_INTERNAL_TYPENATS (String -> FastString
fsLit String
"Log2")
            Unique
typeNatLogTyFamNameKey TyCon
typeNatLogTyCon

axLogRewrites :: [BuiltInFamRewrite]
axLogRewrites :: [BuiltInFamRewrite]
axLogRewrites
  = [ TyCon
-> String
-> (Type -> Maybe Integer)
-> (Integer -> Maybe Type)
-> BuiltInFamRewrite
forall a.
TyCon
-> String
-> (Type -> Maybe a)
-> (a -> Maybe Type)
-> BuiltInFamRewrite
mkUnaryConstFoldAxiom TyCon
tc String
"LogDef" Type -> Maybe Integer
isNumLitTy ((Integer -> Maybe Type) -> BuiltInFamRewrite)
-> (Integer -> Maybe Type) -> BuiltInFamRewrite
forall a b. (a -> b) -> a -> b
$       -- log 8 --> 3
      \Integer
x -> do { (a,_) <- Integer -> Integer -> Maybe (Integer, Bool)
genLog Integer
x Integer
2; return (num a) } ]
  where
    tc :: TyCon
tc = TyCon
typeNatLogTyCon

-------------------------------------------------------------------------------
--               Comparision of Nats: CmpNat
-------------------------------------------------------------------------------

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

  where
    name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_INTERNAL_TYPENATS_INTERNAL (String -> FastString
fsLit String
"CmpNat")
                  Unique
typeNatCmpTyFamNameKey TyCon
typeNatCmpTyCon
    ops :: BuiltInSynFamily
ops = BuiltInSynFamily { sfMatchFam :: [BuiltInFamRewrite]
sfMatchFam = [BuiltInFamRewrite]
axCmpNatRewrites
                           , sfInteract :: [BuiltInFamInjectivity]
sfInteract = [BuiltInFamInjectivity]
axCmpNatInjectivity }

axCmpNatRewrites :: [BuiltInFamRewrite]
axCmpNatRewrites :: [BuiltInFamRewrite]
axCmpNatRewrites
  = [ TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
mkRewriteAxiom   TyCon
tc String
"CmpNatRefl" [TyVar
sn] [TyVar -> Type
var TyVar
sn, TyVar -> Type
var TyVar
sn] (Ordering -> Type
ordering Ordering
EQ)    -- s `cmp` s --> EQ
    , TyCon
-> String
-> (Type -> Maybe Integer)
-> (Type -> Maybe Integer)
-> (Integer -> Integer -> Maybe Type)
-> BuiltInFamRewrite
forall a b.
TyCon
-> String
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> BuiltInFamRewrite
mkBinConstFoldAxiom TyCon
tc String
"CmpNatDef" Type -> Maybe Integer
isNumLitTy Type -> Maybe Integer
isNumLitTy ((Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite)
-> (Integer -> Integer -> Maybe Type) -> BuiltInFamRewrite
forall a b. (a -> b) -> a -> b
$              -- 2 `cmp` 3 --> LT
      \Integer
x Integer
y -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Ordering -> Type
ordering (Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Integer
x Integer
y)) ]
  where
    tc :: TyCon
tc = TyCon
typeNatCmpTyCon

axCmpNatInjectivity :: [BuiltInFamInjectivity]
axCmpNatInjectivity :: [BuiltInFamInjectivity]
axCmpNatInjectivity
  = [ -- s `cmp` t ~ EQ   ==>   s ~ t
      String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"CmpNatT3" TyCon
typeNatCmpTyCon ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
s Type
t Type
r ->
      do { Ordering -> Maybe TypeEqn
EQ <- Type -> Maybe Ordering
isOrderingLitTy Type
r; return (Pair s t) } ]

-------------------------------------------------------------------------------
--              Comparsion of Symbols: CmpSymbol
-------------------------------------------------------------------------------

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

  where
  name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_INTERNAL_TYPELITS_INTERNAL (String -> FastString
fsLit String
"CmpSymbol")
                Unique
typeSymbolCmpTyFamNameKey TyCon
typeSymbolCmpTyCon
  ops :: BuiltInSynFamily
ops = BuiltInSynFamily { sfMatchFam :: [BuiltInFamRewrite]
sfMatchFam = [BuiltInFamRewrite]
axSymbolCmpRewrites
                         , sfInteract :: [BuiltInFamInjectivity]
sfInteract = [BuiltInFamInjectivity]
axSymbolCmpInjectivity }

ss,ts :: TyVar  -- Of kind Symbol
(TyVar
ss: TyVar
ts: [TyVar]
_) = [Type] -> [TyVar]
mkTemplateTyVars (Type -> [Type]
forall a. a -> [a]
repeat Type
typeSymbolKind)

axSymbolCmpRewrites :: [BuiltInFamRewrite]
axSymbolCmpRewrites :: [BuiltInFamRewrite]
axSymbolCmpRewrites
  = [ TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
mkRewriteAxiom   TyCon
tc String
"CmpSymbolRefl" [TyVar
ss] [TyVar -> Type
var TyVar
ss, TyVar -> Type
var TyVar
ss] (Ordering -> Type
ordering Ordering
EQ) -- s `cmp` s --> EQ
    , TyCon
-> String
-> (Type -> Maybe FastString)
-> (Type -> Maybe FastString)
-> (FastString -> FastString -> Maybe Type)
-> BuiltInFamRewrite
forall a b.
TyCon
-> String
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> BuiltInFamRewrite
mkBinConstFoldAxiom TyCon
tc String
"CmpSymbolDef" Type -> Maybe FastString
isStrLitTy Type -> Maybe FastString
isStrLitTy ((FastString -> FastString -> Maybe Type) -> BuiltInFamRewrite)
-> (FastString -> FastString -> Maybe Type) -> BuiltInFamRewrite
forall a b. (a -> b) -> a -> b
$           -- "a" `cmp` "b" --> LT
      \FastString
x FastString
y -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Ordering -> Type
ordering (FastString -> FastString -> Ordering
lexicalCompareFS FastString
x FastString
y)) ]
  where
    tc :: TyCon
tc = TyCon
typeSymbolCmpTyCon

axSymbolCmpInjectivity :: [BuiltInFamInjectivity]
axSymbolCmpInjectivity :: [BuiltInFamInjectivity]
axSymbolCmpInjectivity
  = [ String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"CmpSymbolT" TyCon
typeSymbolCmpTyCon ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
s Type
t Type
r ->
      do { Ordering -> Maybe TypeEqn
EQ <- Type -> Maybe Ordering
isOrderingLitTy Type
r; return (Pair s t) } ]


-------------------------------------------------------------------------------
--            AppendSymbol
-------------------------------------------------------------------------------

typeSymbolAppendTyCon :: TyCon
typeSymbolAppendTyCon :: TyCon
typeSymbolAppendTyCon = Name -> BuiltInSynFamily -> TyCon
mkTypeSymbolFunTyCon2 Name
name
  BuiltInSynFamily { sfMatchFam :: [BuiltInFamRewrite]
sfMatchFam = [BuiltInFamRewrite]
axAppendRewrites
                   , sfInteract :: [BuiltInFamInjectivity]
sfInteract = [BuiltInFamInjectivity]
axAppendInjectivity }
  where
  name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_INTERNAL_TYPELITS (String -> FastString
fsLit String
"AppendSymbol")
                Unique
typeSymbolAppendFamNameKey TyCon
typeSymbolAppendTyCon

axAppendRewrites :: [BuiltInFamRewrite]
axAppendRewrites :: [BuiltInFamRewrite]
axAppendRewrites
  = [ TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
mkRewriteAxiom   TyCon
tc String
"Concat0R" [TyVar
ts] [Type
nullStrLitTy, TyVar -> Type
var TyVar
ts] (TyVar -> Type
var TyVar
ts) -- "" ++ t --> t
    , TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
mkRewriteAxiom   TyCon
tc String
"Concat0L" [TyVar
ss] [TyVar -> Type
var TyVar
ss, Type
nullStrLitTy] (TyVar -> Type
var TyVar
ss) -- s ++ "" --> s
    , TyCon
-> String
-> (Type -> Maybe FastString)
-> (Type -> Maybe FastString)
-> (FastString -> FastString -> Maybe Type)
-> BuiltInFamRewrite
forall a b.
TyCon
-> String
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> BuiltInFamRewrite
mkBinConstFoldAxiom TyCon
tc String
"AppendSymbolDef" Type -> Maybe FastString
isStrLitTy Type -> Maybe FastString
isStrLitTy ((FastString -> FastString -> Maybe Type) -> BuiltInFamRewrite)
-> (FastString -> FastString -> Maybe Type) -> BuiltInFamRewrite
forall a b. (a -> b) -> a -> b
$    -- "a" ++ "b" --> "ab"
      \FastString
x FastString
y -> Type -> Maybe Type
forall a. a -> Maybe a
Just (FastString -> Type
mkStrLitTy (FastString -> FastString -> FastString
appendFS FastString
x FastString
y)) ]
  where
    tc :: TyCon
tc = TyCon
typeSymbolAppendTyCon

axAppendInjectivity :: [BuiltInFamInjectivity]
axAppendInjectivity :: [BuiltInFamInjectivity]
axAppendInjectivity
 = [ -- (AppendSymbol a b ~ "") => (a ~ "")
     String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"AppendSymbolT1" TyCon
tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
a Type
_b Type
r ->
     do { rs <- Type -> Maybe FastString
isStrLitTy Type
r; guard (nullFS rs); return (Pair a nullStrLitTy) }

   , -- (AppendSymbol a b ~ "") => (b ~ "")
     String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"AppendSymbolT2" TyCon
tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
_a Type
b Type
r ->
     do { rs <- Type -> Maybe FastString
isStrLitTy Type
r; guard (nullFS rs); return (Pair b nullStrLitTy) }

   , -- (AppendSymbol "foo" b ~ "foobar") => (b ~ "bar")
     String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"AppendSymbolT3" TyCon
tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
a Type
b Type
r ->
     do { as <- Type -> Maybe String
isStrLitTyS Type
a; rs <- isStrLitTyS r; guard (as `isPrefixOf` rs)
        ; return (Pair b (mkStrLitTyS (drop (length as) rs))) }

   , -- (AppendSymbol f "bar" ~ "foobar") => (f ~ "foo")
     String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"AppendSymbolT3" TyCon
tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
a Type
b Type
r ->
     do { bs <- Type -> Maybe String
isStrLitTyS Type
b; rs <- isStrLitTyS r; guard (bs `isSuffixOf` rs)
        ; return (Pair a (mkStrLitTyS (take (length rs - length bs) rs))) }

    , String
-> TyCon
-> WhichArg
-> WhichArg
-> (Type -> Bool)
-> BuiltInFamInjectivity
mkBinBIF String
"AppI-xx" TyCon
tc WhichArg
ArgX WhichArg
ArgX Type -> Bool
noGuard  -- (x++y1 ~ x++y2) => (y1 ~ y2)
    , String
-> TyCon
-> WhichArg
-> WhichArg
-> (Type -> Bool)
-> BuiltInFamInjectivity
mkBinBIF String
"AppI-yy" TyCon
tc WhichArg
ArgY WhichArg
ArgY Type -> Bool
noGuard  -- (x1++y ~ x2++y) => (x1 ~ x2)
    ]
  where
    tc :: TyCon
tc = TyCon
typeSymbolAppendTyCon

-------------------------------------------------------------------------------
--            ConsSymbol
-------------------------------------------------------------------------------

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

axConsRewrites :: [BuiltInFamRewrite]
axConsRewrites :: [BuiltInFamRewrite]
axConsRewrites
  = [ TyCon
-> String
-> (Type -> Maybe Char)
-> (Type -> Maybe FastString)
-> (Char -> FastString -> Maybe Type)
-> BuiltInFamRewrite
forall a b.
TyCon
-> String
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> BuiltInFamRewrite
mkBinConstFoldAxiom TyCon
tc String
"ConsSymbolDef" Type -> Maybe Char
isCharLitTy Type -> Maybe FastString
isStrLitTy ((Char -> FastString -> Maybe Type) -> BuiltInFamRewrite)
-> (Char -> FastString -> Maybe Type) -> BuiltInFamRewrite
forall a b. (a -> b) -> a -> b
$    -- 'a' : "bc" --> "abc"
      \Char
x FastString
y -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ FastString -> Type
mkStrLitTy (Char -> FastString -> FastString
consFS Char
x FastString
y) ]
  where
    tc :: TyCon
tc = TyCon
typeConsSymbolTyCon

axConsInjectivity :: [BuiltInFamInjectivity]
axConsInjectivity :: [BuiltInFamInjectivity]
axConsInjectivity
  = [ -- ConsSymbol a b ~ "blah" => (a ~ 'b')
      String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"ConsSymbolT1" TyCon
tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
a Type
_b Type
r ->
      do { rs <- Type -> Maybe FastString
isStrLitTy Type
r; (x,_) <- unconsFS rs; return (Pair a (mkCharLitTy x)) }

    , -- ConsSymbol a b ~ "blah" => (b ~ "lah")
      String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"ConsSymbolT2" TyCon
tc ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
_a Type
b Type
r ->
      do { rs <- Type -> Maybe FastString
isStrLitTy Type
r; (_,xs) <- unconsFS rs; return (Pair b (mkStrLitTy xs)) }


    , String
-> TyCon
-> WhichArg
-> WhichArg
-> (Type -> Bool)
-> BuiltInFamInjectivity
mkBinBIF String
"ConsI-xx" TyCon
tc WhichArg
ArgX WhichArg
ArgX Type -> Bool
noGuard  -- (x:y1 ~ x:y2) => (y1 ~ y2)
    , String
-> TyCon
-> WhichArg
-> WhichArg
-> (Type -> Bool)
-> BuiltInFamInjectivity
mkBinBIF String
"ConsI-yy" TyCon
tc WhichArg
ArgY WhichArg
ArgY Type -> Bool
noGuard  -- (x1:y ~ x2:y) => (x1 ~ x2)
    ]
  where
    tc :: TyCon
tc = TyCon
typeConsSymbolTyCon

-------------------------------------------------------------------------------
--            UnconsSymbol
-------------------------------------------------------------------------------

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

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

axUnconsRewrites :: [BuiltInFamRewrite]
axUnconsRewrites :: [BuiltInFamRewrite]
axUnconsRewrites
  = [ TyCon
-> String
-> (Type -> Maybe FastString)
-> (FastString -> Maybe Type)
-> BuiltInFamRewrite
forall a.
TyCon
-> String
-> (Type -> Maybe a)
-> (a -> Maybe Type)
-> BuiltInFamRewrite
mkUnaryConstFoldAxiom TyCon
tc String
"ConsSymbolDef" Type -> Maybe FastString
isStrLitTy ((FastString -> Maybe Type) -> BuiltInFamRewrite)
-> (FastString -> Maybe Type) -> BuiltInFamRewrite
forall a b. (a -> b) -> a -> b
$    -- 'a' : "bc" --> "abc"
      \FastString
x -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ FastString -> Type
computeUncons FastString
x ]
  where
    tc :: TyCon
tc = TyCon
typeUnconsSymbolTyCon

axUnconsInjectivity :: [BuiltInFamInjectivity]
axUnconsInjectivity :: [BuiltInFamInjectivity]
axUnconsInjectivity
  = [ -- (UnconsSymbol b ~ Nothing) => (b ~ "")
      String
-> TyCon
-> (Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopUnaryFamDeduction String
"UnconsSymbolT1" TyCon
tc ((Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \Type
b Type
r ->
      do { Maybe Type -> Maybe TypeEqn
Nothing  <- Type -> Maybe (Maybe Type)
isPromotedMaybeTy Type
r; return (Pair b nullStrLitTy) }

    , -- (UnconsSymbol b ~ Just ('f',"oobar")) => (b ~ "foobar")
      String
-> TyCon
-> (Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopUnaryFamDeduction String
"UnconsSymbolT2" TyCon
tc ((Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \Type
b Type
r ->
      do { Just pr <- Type -> Maybe (Maybe Type)
isPromotedMaybeTy Type
r
         ; (c,s) <- isPromotedPairType pr
         ; chr <- isCharLitTy c
         ; str <- isStrLitTy s
         ; return (Pair b (mkStrLitTy (consFS chr str))) }

    , String -> TyCon -> BuiltInFamInjectivity
mkUnaryBIF String
"UnconsI1" TyCon
tc  -- (UnconsSymbol x1 ~ z, UnconsSymbol x2 ~ z) => (x1 ~ x2)
    ]
  where
    tc :: TyCon
tc = TyCon
typeUnconsSymbolTyCon

-------------------------------------------------------------------------------
--            CharToNat
-------------------------------------------------------------------------------

typeCharToNatTyCon :: TyCon
typeCharToNatTyCon :: TyCon
typeCharToNatTyCon =
  Name
-> [TyConBinder]
-> Type
-> Maybe Name
-> FamTyConFlav
-> Maybe Class
-> Injectivity
-> TyCon
mkFamilyTyCon Name
name
    ([Type] -> [TyConBinder]
mkTemplateAnonTyConBinders [ Type
charTy ])
    Type
naturalTy
    Maybe Name
forall a. Maybe a
Nothing
    (BuiltInSynFamily -> FamTyConFlav
BuiltInSynFamTyCon BuiltInSynFamily
ops)
    Maybe Class
forall a. Maybe a
Nothing
    ([Bool] -> Injectivity
Injective [Bool
True])
  where
  name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_INTERNAL_TYPELITS (String -> FastString
fsLit String
"CharToNat")
                  Unique
typeCharToNatTyFamNameKey TyCon
typeCharToNatTyCon
  ops :: BuiltInSynFamily
ops = BuiltInSynFamily { sfMatchFam :: [BuiltInFamRewrite]
sfMatchFam = [BuiltInFamRewrite]
axCharToNatRewrites
                         , sfInteract :: [BuiltInFamInjectivity]
sfInteract = [BuiltInFamInjectivity]
axCharToNatInjectivity }

axCharToNatRewrites :: [BuiltInFamRewrite]
axCharToNatRewrites :: [BuiltInFamRewrite]
axCharToNatRewrites
  = [ TyCon
-> String
-> (Type -> Maybe Char)
-> (Char -> Maybe Type)
-> BuiltInFamRewrite
forall a.
TyCon
-> String
-> (Type -> Maybe a)
-> (a -> Maybe Type)
-> BuiltInFamRewrite
mkUnaryConstFoldAxiom TyCon
tc String
"CharToNatDef" Type -> Maybe Char
isCharLitTy ((Char -> Maybe Type) -> BuiltInFamRewrite)
-> (Char -> Maybe Type) -> BuiltInFamRewrite
forall a b. (a -> b) -> a -> b
$    -- CharToNat 'a' --> 97
      \Char
x -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Integer -> Type
num (Char -> Integer
charToInteger Char
x) ]
  where
    tc :: TyCon
tc = TyCon
typeCharToNatTyCon

axCharToNatInjectivity :: [BuiltInFamInjectivity]
axCharToNatInjectivity :: [BuiltInFamInjectivity]
axCharToNatInjectivity
  = [ -- (CharToNat c ~ 122) => (c ~ 'z')
      String
-> TyCon
-> (Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopUnaryFamDeduction String
"CharToNatT1" TyCon
typeCharToNatTyCon ((Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \Type
c Type
r ->
      do { nr <- Type -> Maybe Integer
isNumLitTy Type
r; chr <- integerToChar nr; return (Pair c (mkCharLitTy chr)) } ]

-------------------------------------------------------------------------------
--            NatToChar
-------------------------------------------------------------------------------

typeNatToCharTyCon :: TyCon
typeNatToCharTyCon :: TyCon
typeNatToCharTyCon =
  Name
-> [TyConBinder]
-> Type
-> Maybe Name
-> FamTyConFlav
-> Maybe Class
-> Injectivity
-> TyCon
mkFamilyTyCon Name
name
    ([Type] -> [TyConBinder]
mkTemplateAnonTyConBinders [ Type
naturalTy ])
    Type
charTy
    Maybe Name
forall a. Maybe a
Nothing
    (BuiltInSynFamily -> FamTyConFlav
BuiltInSynFamTyCon BuiltInSynFamily
ops)
    Maybe Class
forall a. Maybe a
Nothing
    ([Bool] -> Injectivity
Injective [Bool
True])
  where
  name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_INTERNAL_TYPELITS (String -> FastString
fsLit String
"NatToChar")
                  Unique
typeNatToCharTyFamNameKey TyCon
typeNatToCharTyCon
  ops :: BuiltInSynFamily
ops = BuiltInSynFamily { sfMatchFam :: [BuiltInFamRewrite]
sfMatchFam = [BuiltInFamRewrite]
axNatToCharRewrites
                         , sfInteract :: [BuiltInFamInjectivity]
sfInteract = [BuiltInFamInjectivity]
axNatToCharInjectivity }

axNatToCharRewrites :: [BuiltInFamRewrite]
axNatToCharRewrites :: [BuiltInFamRewrite]
axNatToCharRewrites
  = [ TyCon
-> String
-> (Type -> Maybe Integer)
-> (Integer -> Maybe Type)
-> BuiltInFamRewrite
forall a.
TyCon
-> String
-> (Type -> Maybe a)
-> (a -> Maybe Type)
-> BuiltInFamRewrite
mkUnaryConstFoldAxiom TyCon
tc String
"NatToCharDef" Type -> Maybe Integer
isNumLitTy ((Integer -> Maybe Type) -> BuiltInFamRewrite)
-> (Integer -> Maybe Type) -> BuiltInFamRewrite
forall a b. (a -> b) -> a -> b
$    -- NatToChar 97 --> 'a'
      \Integer
n -> (Char -> Type) -> Maybe Char -> Maybe Type
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Char -> Type
mkCharLitTy (Integer -> Maybe Char
integerToChar Integer
n) ]
  where
    tc :: TyCon
tc = TyCon
typeNatToCharTyCon

axNatToCharInjectivity :: [BuiltInFamInjectivity]
axNatToCharInjectivity :: [BuiltInFamInjectivity]
axNatToCharInjectivity
  = [ -- (NatToChar n ~ 'z') => (n ~ 122)
      String
-> TyCon
-> (Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopUnaryFamDeduction String
"CharToNatT1" TyCon
typeNatToCharTyCon ((Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \Type
n Type
r ->
      do { c <- Type -> Maybe Char
isCharLitTy Type
r; return (Pair n (mkNumLitTy (charToInteger c))) } ]


-----------------------------------------------------------------------------
--                       CmpChar
-----------------------------------------------------------------------------

typeCharCmpTyCon :: TyCon
typeCharCmpTyCon :: TyCon
typeCharCmpTyCon =
  Name
-> [TyConBinder]
-> Type
-> Maybe Name
-> FamTyConFlav
-> Maybe Class
-> Injectivity
-> TyCon
mkFamilyTyCon Name
name
    ([Type] -> [TyConBinder]
mkTemplateAnonTyConBinders [ Type
charTy, Type
charTy ])
    Type
orderingKind
    Maybe Name
forall a. Maybe a
Nothing
    (BuiltInSynFamily -> FamTyConFlav
BuiltInSynFamTyCon BuiltInSynFamily
ops)
    Maybe Class
forall a. Maybe a
Nothing
    Injectivity
NotInjective
  where
  name :: Name
name = BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
mkWiredInTyConName BuiltInSyntax
UserSyntax Module
gHC_INTERNAL_TYPELITS_INTERNAL (String -> FastString
fsLit String
"CmpChar")
                  Unique
typeCharCmpTyFamNameKey TyCon
typeCharCmpTyCon
  ops :: BuiltInSynFamily
ops = BuiltInSynFamily { sfMatchFam :: [BuiltInFamRewrite]
sfMatchFam = [BuiltInFamRewrite]
axCharCmpRewrites
                         , sfInteract :: [BuiltInFamInjectivity]
sfInteract = [BuiltInFamInjectivity]
axCharCmpInjectivity }

sc :: TyVar  -- Of kind Char
(TyVar
sc: [TyVar]
_) = [Type] -> [TyVar]
mkTemplateTyVars (Type -> [Type]
forall a. a -> [a]
repeat Type
charTy)

axCharCmpRewrites :: [BuiltInFamRewrite]
axCharCmpRewrites :: [BuiltInFamRewrite]
axCharCmpRewrites
  = [ TyCon -> String -> [TyVar] -> [Type] -> Type -> BuiltInFamRewrite
mkRewriteAxiom   TyCon
tc String
"CmpCharRefl" [TyVar
sc] [TyVar -> Type
var TyVar
sc, TyVar -> Type
var TyVar
sc] (Ordering -> Type
ordering Ordering
EQ) -- s `cmp` s --> EQ
    , TyCon
-> String
-> (Type -> Maybe Char)
-> (Type -> Maybe Char)
-> (Char -> Char -> Maybe Type)
-> BuiltInFamRewrite
forall a b.
TyCon
-> String
-> (Type -> Maybe a)
-> (Type -> Maybe b)
-> (a -> b -> Maybe Type)
-> BuiltInFamRewrite
mkBinConstFoldAxiom TyCon
tc String
"CmpCharDef" Type -> Maybe Char
isCharLitTy Type -> Maybe Char
isCharLitTy ((Char -> Char -> Maybe Type) -> BuiltInFamRewrite)
-> (Char -> Char -> Maybe Type) -> BuiltInFamRewrite
forall a b. (a -> b) -> a -> b
$         -- 'a' `cmp` 'b' --> LT
      \Char
chr1 Char
chr2 -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Ordering -> Type
ordering (Ordering -> Type) -> Ordering -> Type
forall a b. (a -> b) -> a -> b
$ Char -> Char -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Char
chr1 Char
chr2 ]
  where
    tc :: TyCon
tc = TyCon
typeCharCmpTyCon

axCharCmpInjectivity :: [BuiltInFamInjectivity]
axCharCmpInjectivity :: [BuiltInFamInjectivity]
axCharCmpInjectivity
  = [  -- (CmpChar s t ~ EQ) => s ~ t
      String
-> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
-> BuiltInFamInjectivity
mkTopBinFamDeduction String
"CmpCharT" TyCon
typeCharCmpTyCon ((Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity)
-> (Type -> Type -> Type -> Maybe TypeEqn) -> BuiltInFamInjectivity
forall a b. (a -> b) -> a -> b
$ \ Type
s Type
t Type
r ->
      do { Ordering -> Maybe TypeEqn
EQ <- Type -> Maybe Ordering
isOrderingLitTy Type
r; return (Pair s t) } ]


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

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

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

var :: TyVar -> Type
var :: TyVar -> Type
var = TyVar -> Type
mkTyVarTy

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

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

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

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

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

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

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

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

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


nullStrLitTy :: Type  -- The type ""
nullStrLitTy :: Type
nullStrLitTy = FastString -> Type
mkStrLitTy FastString
nilFS

isStrLitTyS :: Type -> Maybe String
isStrLitTyS :: Type -> Maybe String
isStrLitTyS Type
ty = do { fs <- Type -> Maybe FastString
isStrLitTy Type
ty; return (unpackFS fs) }

mkStrLitTyS :: String -> Type
mkStrLitTyS :: String -> Type
mkStrLitTyS String
s = FastString -> Type
mkStrLitTy (String -> FastString
mkFastString String
s)

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

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

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

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

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

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

same :: Type -> Type -> Maybe ()
same :: Type -> Type -> Maybe ()
same Type
ty1 Type
ty2 = Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Type
ty1 HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`tcEqType` Type
ty2)

known :: Type -> (Integer -> Bool) -> Maybe Integer
known :: Type -> (Integer -> Bool) -> Maybe Integer
known Type
x Integer -> Bool
p = do { nx <- Type -> Maybe Integer
isNumLitTy Type
x; guard (p nx); return nx }

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

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


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