    {-|
    Copyright  :  (C) 2015-2016, University of Twente,
                      2017     , QBayLogic B.V.
    License    :  BSD2 (see the file LICENSE)
    Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com>
    -}

    {-# LANGUAGE CPP       #-}
    {-# LANGUAGE MagicHash #-}

    module GHC.TypeLits.Extra.Solver.Operations
      ( ExtraOp (..)
      , ExtraDefs (..)
      , Normalised (..)
      , NormaliseResult
      , mergeNormalised
      , reifyEOP
      , mergeMax
      , mergeMin
      , mergeDiv
      , mergeMod
      , mergeFLog
      , mergeCLog
      , mergeLog
      , mergeGCD
      , mergeLCM
      , mergeExp
      )
    where

    -- external
    import Control.Monad.Trans.Writer.Strict
    #if MIN_VERSION_ghc_typelits_natnormalise(0,7,0)
    import Data.Set                     as Set
    #endif

    import GHC.Base                     (isTrue#,(==#),(+#))
    import GHC.Integer                  (smallInteger)
    import GHC.Integer.Logarithms       (integerLogBase#)
    import GHC.TypeLits.Normalise.Unify (CType (..), normaliseNat, isNatural)

    -- GHC API
    #if MIN_VERSION_ghc(9,0,0)
    import GHC.Builtin.Types.Literals (typeNatExpTyCon, typeNatSubTyCon)
    import GHC.Core.TyCon (TyCon)
    import GHC.Core.Type (Type, TyVar, mkNumLitTy, mkTyConApp, mkTyVarTy)
    import GHC.Utils.Outputable (Outputable (..), (<+>), integer, text)
    #else
    import Outputable (Outputable (..), (<+>), integer, text)
    import TcTypeNats (typeNatExpTyCon, typeNatSubTyCon)
    import TyCon      (TyCon)
    import Type       (Type, TyVar, mkNumLitTy, mkTyConApp, mkTyVarTy)
    #endif

    -- | Indicates whether normalisation has occured
    data Normalised = Normalised | Untouched
      deriving Normalised -> Normalised -> Bool
    (Normalised -> Normalised -> Bool)
    -> (Normalised -> Normalised -> Bool) -> Eq Normalised
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Normalised -> Normalised -> Bool
    == :: Normalised -> Normalised -> Bool
    $c/= :: Normalised -> Normalised -> Bool
    /= :: Normalised -> Normalised -> Bool
    Eq

    instance Outputable Normalised where
      ppr :: Normalised -> SDoc
    ppr Normalised
    Normalised = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "Normalised"
      ppr Normalised
    Untouched  = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "Untouched"

    mergeNormalised :: Normalised -> Normalised -> Normalised
    mergeNormalised :: Normalised -> Normalised -> Normalised
    mergeNormalised Normalised
    Normalised Normalised
    _ = Normalised
    Normalised
    mergeNormalised Normalised
    _ Normalised
    Normalised = Normalised
    Normalised
    mergeNormalised Normalised
    _ Normalised
    _          = Normalised
    Untouched

    -- | A normalise result contains the ExtraOp and a flag that indicates whether any expression
    -- | was normalised within the ExtraOp.
    type NormaliseResult = (ExtraOp, Normalised)

    data ExtraOp
      = I    Integer
      | V    TyVar
      | C    CType
      | Max  ExtraOp ExtraOp
      | Min  ExtraOp ExtraOp
      | Div  ExtraOp ExtraOp
      | Mod  ExtraOp ExtraOp
      | FLog ExtraOp ExtraOp
      | CLog ExtraOp ExtraOp
      | Log  ExtraOp ExtraOp
      | GCD  ExtraOp ExtraOp
      | LCM  ExtraOp ExtraOp
      | Exp  ExtraOp ExtraOp
      deriving ExtraOp -> ExtraOp -> Bool
    (ExtraOp -> ExtraOp -> Bool)
    -> (ExtraOp -> ExtraOp -> Bool) -> Eq ExtraOp
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: ExtraOp -> ExtraOp -> Bool
    == :: ExtraOp -> ExtraOp -> Bool
    $c/= :: ExtraOp -> ExtraOp -> Bool
    /= :: ExtraOp -> ExtraOp -> Bool
    Eq

    instance Outputable ExtraOp where
      ppr :: ExtraOp -> SDoc
    ppr (I Integer
    i)      = Integer -> SDoc
    forall doc. IsLine doc => Integer -> doc
    integer Integer
    i
      ppr (V TyVar
    v)      = TyVar -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr TyVar
    v
      ppr (C CType
    c)      = CType -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr CType
    c
      ppr (Max ExtraOp
    x ExtraOp
    y)  = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "Max (" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> ExtraOp -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr ExtraOp
    x SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "," SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> ExtraOp -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr ExtraOp
    y SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    ")"
      ppr (Min ExtraOp
    x ExtraOp
    y)  = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "Min (" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> ExtraOp -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr ExtraOp
    x SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "," SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> ExtraOp -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr ExtraOp
    y SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    ")"
      ppr (Div ExtraOp
    x ExtraOp
    y)  = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "Div (" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> ExtraOp -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr ExtraOp
    x SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "," SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> ExtraOp -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr ExtraOp
    y SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    ")"
      ppr (Mod ExtraOp
    x ExtraOp
    y)  = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "Mod (" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> ExtraOp -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr ExtraOp
    x SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "," SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> ExtraOp -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr ExtraOp
    y SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    ")"
      ppr (FLog ExtraOp
    x ExtraOp
    y) = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "FLog (" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> ExtraOp -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr ExtraOp
    x SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "," SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> ExtraOp -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr ExtraOp
    y SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    ")"
      ppr (CLog ExtraOp
    x ExtraOp
    y) = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "CLog (" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> ExtraOp -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr ExtraOp
    x SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "," SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> ExtraOp -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr ExtraOp
    y SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    ")"
      ppr (Log ExtraOp
    x ExtraOp
    y)  = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "Log (" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> ExtraOp -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr ExtraOp
    x SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "," SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> ExtraOp -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr ExtraOp
    y SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    ")"
      ppr (GCD ExtraOp
    x ExtraOp
    y)  = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "GCD (" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> ExtraOp -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr ExtraOp
    x SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "," SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> ExtraOp -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr ExtraOp
    y SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    ")"
      ppr (LCM ExtraOp
    x ExtraOp
    y)  = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "GCD (" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> ExtraOp -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr ExtraOp
    x SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "," SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> ExtraOp -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr ExtraOp
    y SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    ")"
      ppr (Exp ExtraOp
    x ExtraOp
    y)  = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "Exp (" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> ExtraOp -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr ExtraOp
    x SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "," SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> ExtraOp -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr ExtraOp
    y SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    ")"

    data ExtraDefs = ExtraDefs
      { ExtraDefs -> TyCon
    maxTyCon  :: TyCon
      , ExtraDefs -> TyCon
    minTyCon  :: TyCon
      , ExtraDefs -> TyCon
    divTyCon  :: TyCon
      , ExtraDefs -> TyCon
    modTyCon  :: TyCon
      , ExtraDefs -> TyCon
    flogTyCon :: TyCon
      , ExtraDefs -> TyCon
    clogTyCon :: TyCon
      , ExtraDefs -> TyCon
    logTyCon  :: TyCon
      , ExtraDefs -> TyCon
    gcdTyCon  :: TyCon
      , ExtraDefs -> TyCon
    lcmTyCon  :: TyCon
      , ExtraDefs -> TyCon
    ordTyCon  :: TyCon
      , ExtraDefs -> TyCon
    assertTC  :: TyCon
      }

    reifyEOP :: ExtraDefs -> ExtraOp -> Type
    reifyEOP :: ExtraDefs -> ExtraOp -> Type
    reifyEOP ExtraDefs
    _ (I Integer
    i) = Integer -> Type
    mkNumLitTy Integer
    i
    reifyEOP ExtraDefs
    _ (V TyVar
    v) = TyVar -> Type
    mkTyVarTy TyVar
    v
    reifyEOP ExtraDefs
    _ (C (CType Type
    c)) = Type
    c
    reifyEOP ExtraDefs
    defs (Max ExtraOp
    x ExtraOp
    y)  = TyCon -> [Type] -> Type
    mkTyConApp (ExtraDefs -> TyCon
    maxTyCon ExtraDefs
    defs)  [ExtraDefs -> ExtraOp -> Type
    reifyEOP ExtraDefs
    defs ExtraOp
    x
                                                           ,ExtraDefs -> ExtraOp -> Type
    reifyEOP ExtraDefs
    defs ExtraOp
    y]
    reifyEOP ExtraDefs
    defs (Min ExtraOp
    x ExtraOp
    y)  = TyCon -> [Type] -> Type
    mkTyConApp (ExtraDefs -> TyCon
    minTyCon ExtraDefs
    defs)  [ExtraDefs -> ExtraOp -> Type
    reifyEOP ExtraDefs
    defs ExtraOp
    x
                                                           ,ExtraDefs -> ExtraOp -> Type
    reifyEOP ExtraDefs
    defs ExtraOp
    y]
    reifyEOP ExtraDefs
    defs (Div ExtraOp
    x ExtraOp
    y)  = TyCon -> [Type] -> Type
    mkTyConApp (ExtraDefs -> TyCon
    divTyCon ExtraDefs
    defs)  [ExtraDefs -> ExtraOp -> Type
    reifyEOP ExtraDefs
    defs ExtraOp
    x
                                                           ,ExtraDefs -> ExtraOp -> Type
    reifyEOP ExtraDefs
    defs ExtraOp
    y]
    reifyEOP ExtraDefs
    defs (Mod ExtraOp
    x ExtraOp
    y)  = TyCon -> [Type] -> Type
    mkTyConApp (ExtraDefs -> TyCon
    modTyCon ExtraDefs
    defs)  [ExtraDefs -> ExtraOp -> Type
    reifyEOP ExtraDefs
    defs ExtraOp
    x
                                                           ,ExtraDefs -> ExtraOp -> Type
    reifyEOP ExtraDefs
    defs ExtraOp
    y]
    reifyEOP ExtraDefs
    defs (CLog ExtraOp
    x ExtraOp
    y) = TyCon -> [Type] -> Type
    mkTyConApp (ExtraDefs -> TyCon
    clogTyCon ExtraDefs
    defs) [ExtraDefs -> ExtraOp -> Type
    reifyEOP ExtraDefs
    defs ExtraOp
    x
                                                           ,ExtraDefs -> ExtraOp -> Type
    reifyEOP ExtraDefs
    defs ExtraOp
    y]
    reifyEOP ExtraDefs
    defs (FLog ExtraOp
    x ExtraOp
    y) = TyCon -> [Type] -> Type
    mkTyConApp (ExtraDefs -> TyCon
    flogTyCon ExtraDefs
    defs) [ExtraDefs -> ExtraOp -> Type
    reifyEOP ExtraDefs
    defs ExtraOp
    x
                                                           ,ExtraDefs -> ExtraOp -> Type
    reifyEOP ExtraDefs
    defs ExtraOp
    y]
    reifyEOP ExtraDefs
    defs (Log ExtraOp
    x ExtraOp
    y)  = TyCon -> [Type] -> Type
    mkTyConApp (ExtraDefs -> TyCon
    logTyCon ExtraDefs
    defs)  [ExtraDefs -> ExtraOp -> Type
    reifyEOP ExtraDefs
    defs ExtraOp
    x
                                                           ,ExtraDefs -> ExtraOp -> Type
    reifyEOP ExtraDefs
    defs ExtraOp
    y]
    reifyEOP ExtraDefs
    defs (GCD ExtraOp
    x ExtraOp
    y)  = TyCon -> [Type] -> Type
    mkTyConApp (ExtraDefs -> TyCon
    gcdTyCon ExtraDefs
    defs)  [ExtraDefs -> ExtraOp -> Type
    reifyEOP ExtraDefs
    defs ExtraOp
    x
                                                           ,ExtraDefs -> ExtraOp -> Type
    reifyEOP ExtraDefs
    defs ExtraOp
    y]
    reifyEOP ExtraDefs
    defs (LCM ExtraOp
    x ExtraOp
    y)  = TyCon -> [Type] -> Type
    mkTyConApp (ExtraDefs -> TyCon
    lcmTyCon ExtraDefs
    defs)  [ExtraDefs -> ExtraOp -> Type
    reifyEOP ExtraDefs
    defs ExtraOp
    x
                                                           ,ExtraDefs -> ExtraOp -> Type
    reifyEOP ExtraDefs
    defs ExtraOp
    y]
    reifyEOP ExtraDefs
    defs (Exp ExtraOp
    x ExtraOp
    y)  = TyCon -> [Type] -> Type
    mkTyConApp TyCon
    typeNatExpTyCon  [ExtraDefs -> ExtraOp -> Type
    reifyEOP ExtraDefs
    defs ExtraOp
    x
                                                           ,ExtraDefs -> ExtraOp -> Type
    reifyEOP ExtraDefs
    defs ExtraOp
    y]

    mergeMax :: ExtraDefs -> ExtraOp -> ExtraOp -> NormaliseResult
    mergeMax :: ExtraDefs -> ExtraOp -> ExtraOp -> NormaliseResult
    mergeMax ExtraDefs
    _ (I Integer
    0) ExtraOp
    y = (ExtraOp
    y, Normalised
    Normalised)
    mergeMax ExtraDefs
    _ ExtraOp
    x (I Integer
    0) = (ExtraOp
    x, Normalised
    Normalised)
    mergeMax ExtraDefs
    defs ExtraOp
    x ExtraOp
    y =
      let x' :: Type
    x' = ExtraDefs -> ExtraOp -> Type
    reifyEOP ExtraDefs
    defs ExtraOp
    x
          y' :: Type
    y' = ExtraDefs -> ExtraOp -> Type
    reifyEOP ExtraDefs
    defs ExtraOp
    y
          z :: CoreSOP
    z  = (CoreSOP, [(Type, Type)]) -> CoreSOP
    forall a b. (a, b) -> a
    fst (Writer [(Type, Type)] CoreSOP -> (CoreSOP, [(Type, Type)])
    forall w a. Writer w a -> (a, w)
    runWriter (Type -> Writer [(Type, Type)] CoreSOP
    normaliseNat (TyCon -> [Type] -> Type
    mkTyConApp TyCon
    typeNatSubTyCon [Type
    y',Type
    x'])))
    #if MIN_VERSION_ghc_typelits_natnormalise(0,7,0)
      in  case WriterT (Set CType) Maybe Bool -> Maybe (Bool, Set CType)
    forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
    runWriterT (CoreSOP -> WriterT (Set CType) Maybe Bool
    isNatural CoreSOP
    z) of
            Just (Bool
    True , Set CType
    cs) | Set CType -> Bool
    forall a. Set a -> Bool
    Set.null Set CType
    cs -> (ExtraOp
    y, Normalised
    Normalised)
            Just (Bool
    False, Set CType
    cs) | Set CType -> Bool
    forall a. Set a -> Bool
    Set.null Set CType
    cs -> (ExtraOp
    x, Normalised
    Normalised)
    #else
      in  case isNatural z of
            Just True  -> (y, Normalised)
            Just False -> (x, Normalised)
    #endif
            Maybe (Bool, Set CType)
    _ -> (ExtraOp -> ExtraOp -> ExtraOp
    Max ExtraOp
    x ExtraOp
    y, Normalised
    Untouched)

    mergeMin :: ExtraDefs -> ExtraOp -> ExtraOp -> NormaliseResult
    mergeMin :: ExtraDefs -> ExtraOp -> ExtraOp -> NormaliseResult
    mergeMin ExtraDefs
    defs ExtraOp
    x ExtraOp
    y =
      let x' :: Type
    x' = ExtraDefs -> ExtraOp -> Type
    reifyEOP ExtraDefs
    defs ExtraOp
    x
          y' :: Type
    y' = ExtraDefs -> ExtraOp -> Type
    reifyEOP ExtraDefs
    defs ExtraOp
    y
          z :: CoreSOP
    z  = (CoreSOP, [(Type, Type)]) -> CoreSOP
    forall a b. (a, b) -> a
    fst (Writer [(Type, Type)] CoreSOP -> (CoreSOP, [(Type, Type)])
    forall w a. Writer w a -> (a, w)
    runWriter (Type -> Writer [(Type, Type)] CoreSOP
    normaliseNat (TyCon -> [Type] -> Type
    mkTyConApp TyCon
    typeNatSubTyCon [Type
    y',Type
    x'])))
    #if MIN_VERSION_ghc_typelits_natnormalise(0,7,0)
      in  case WriterT (Set CType) Maybe Bool -> Maybe (Bool, Set CType)
    forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
    runWriterT (CoreSOP -> WriterT (Set CType) Maybe Bool
    isNatural CoreSOP
    z) of
            Just (Bool
    True, Set CType
    cs) | Set CType -> Bool
    forall a. Set a -> Bool
    Set.null Set CType
    cs -> (ExtraOp
    x, Normalised
    Normalised)
            Just (Bool
    False,Set CType
    cs) | Set CType -> Bool
    forall a. Set a -> Bool
    Set.null Set CType
    cs -> (ExtraOp
    y, Normalised
    Normalised)
    #else
      in  case isNatural z of
            Just True  -> (x, Normalised)
            Just False -> (y, Normalised)
    #endif
            Maybe (Bool, Set CType)
    _ -> (ExtraOp -> ExtraOp -> ExtraOp
    Min ExtraOp
    x ExtraOp
    y, Normalised
    Untouched)

    mergeDiv :: ExtraOp -> ExtraOp -> Maybe NormaliseResult
    mergeDiv :: ExtraOp -> ExtraOp -> Maybe NormaliseResult
    mergeDiv ExtraOp
    _     (I Integer
    0)      = Maybe NormaliseResult
    forall a. Maybe a
    Nothing
    mergeDiv (I Integer
    i) (I Integer
    j)      = NormaliseResult -> Maybe NormaliseResult
    forall a. a -> Maybe a
    Just (Integer -> ExtraOp
    I (Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    div Integer
    i Integer
    j), Normalised
    Normalised)
    mergeDiv ExtraOp
    x ExtraOp
    y              = NormaliseResult -> Maybe NormaliseResult
    forall a. a -> Maybe a
    Just (ExtraOp -> ExtraOp -> ExtraOp
    Div ExtraOp
    x ExtraOp
    y, Normalised
    Untouched)

    mergeMod :: ExtraOp -> ExtraOp -> Maybe NormaliseResult
    mergeMod :: ExtraOp -> ExtraOp -> Maybe NormaliseResult
    mergeMod ExtraOp
    _     (I Integer
    0)      = Maybe NormaliseResult
    forall a. Maybe a
    Nothing
    mergeMod (I Integer
    i) (I Integer
    j)      = NormaliseResult -> Maybe NormaliseResult
    forall a. a -> Maybe a
    Just (Integer -> ExtraOp
    I (Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    mod Integer
    i Integer
    j), Normalised
    Normalised)
    mergeMod ExtraOp
    x ExtraOp
    y              = NormaliseResult -> Maybe NormaliseResult
    forall a. a -> Maybe a
    Just (ExtraOp -> ExtraOp -> ExtraOp
    Mod ExtraOp
    x ExtraOp
    y, Normalised
    Untouched)

    mergeFLog :: ExtraOp -> ExtraOp -> Maybe NormaliseResult
    mergeFLog :: ExtraOp -> ExtraOp -> Maybe NormaliseResult
    mergeFLog (I Integer
    i) ExtraOp
    _         | Integer
    i Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    2  = Maybe NormaliseResult
    forall a. Maybe a
    Nothing
    mergeFLog ExtraOp
    i     (Exp ExtraOp
    j ExtraOp
    k) | ExtraOp
    i ExtraOp -> ExtraOp -> Bool
    forall a. Eq a => a -> a -> Bool
    == ExtraOp
    j = NormaliseResult -> Maybe NormaliseResult
    forall a. a -> Maybe a
    Just (ExtraOp
    k, Normalised
    Normalised)
    mergeFLog (I Integer
    i) (I Integer
    j)              = (Integer -> NormaliseResult)
    -> Maybe Integer -> Maybe NormaliseResult
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (\Integer
    r -> (Integer -> ExtraOp
    I Integer
    r, Normalised
    Normalised)) (Integer -> Integer -> Maybe Integer
    flogBase Integer
    i Integer
    j)
    mergeFLog ExtraOp
    x     ExtraOp
    y                  = NormaliseResult -> Maybe NormaliseResult
    forall a. a -> Maybe a
    Just (ExtraOp -> ExtraOp -> ExtraOp
    FLog ExtraOp
    x ExtraOp
    y, Normalised
    Untouched)

    mergeCLog :: ExtraOp -> ExtraOp -> Maybe NormaliseResult
    mergeCLog :: ExtraOp -> ExtraOp -> Maybe NormaliseResult
    mergeCLog (I Integer
    i) ExtraOp
    _         | Integer
    i Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    2  = Maybe NormaliseResult
    forall a. Maybe a
    Nothing
    mergeCLog ExtraOp
    i     (Exp ExtraOp
    j ExtraOp
    k) | ExtraOp
    i ExtraOp -> ExtraOp -> Bool
    forall a. Eq a => a -> a -> Bool
    == ExtraOp
    j = NormaliseResult -> Maybe NormaliseResult
    forall a. a -> Maybe a
    Just (ExtraOp
    k, Normalised
    Normalised)
    mergeCLog (I Integer
    i) (I Integer
    j)              = (Integer -> NormaliseResult)
    -> Maybe Integer -> Maybe NormaliseResult
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (\Integer
    r -> (Integer -> ExtraOp
    I Integer
    r, Normalised
    Normalised)) (Integer -> Integer -> Maybe Integer
    clogBase Integer
    i Integer
    j)
    mergeCLog ExtraOp
    x     ExtraOp
    y                  = NormaliseResult -> Maybe NormaliseResult
    forall a. a -> Maybe a
    Just (ExtraOp -> ExtraOp -> ExtraOp
    CLog ExtraOp
    x ExtraOp
    y, Normalised
    Untouched)

    mergeLog :: ExtraOp -> ExtraOp -> Maybe NormaliseResult
    mergeLog :: ExtraOp -> ExtraOp -> Maybe NormaliseResult
    mergeLog (I Integer
    i) ExtraOp
    _          | Integer
    i Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    2   = Maybe NormaliseResult
    forall a. Maybe a
    Nothing
    mergeLog ExtraOp
    b     (Exp ExtraOp
    b' ExtraOp
    y) | ExtraOp
    b ExtraOp -> ExtraOp -> Bool
    forall a. Eq a => a -> a -> Bool
    == ExtraOp
    b' = NormaliseResult -> Maybe NormaliseResult
    forall a. a -> Maybe a
    Just (ExtraOp
    y, Normalised
    Normalised)
    mergeLog (I Integer
    i) (I Integer
    j)                = (Integer -> NormaliseResult)
    -> Maybe Integer -> Maybe NormaliseResult
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (\Integer
    r -> (Integer -> ExtraOp
    I Integer
    r, Normalised
    Normalised)) (Integer -> Integer -> Maybe Integer
    exactLogBase Integer
    i Integer
    j)
    mergeLog ExtraOp
    x     ExtraOp
    y                    = NormaliseResult -> Maybe NormaliseResult
    forall a. a -> Maybe a
    Just (ExtraOp -> ExtraOp -> ExtraOp
    Log ExtraOp
    x ExtraOp
    y, Normalised
    Untouched)

    mergeGCD :: ExtraOp -> ExtraOp -> NormaliseResult
    mergeGCD :: ExtraOp -> ExtraOp -> NormaliseResult
    mergeGCD (I Integer
    i) (I Integer
    j) = (Integer -> ExtraOp
    I (Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    gcd Integer
    i Integer
    j), Normalised
    Normalised)
    mergeGCD ExtraOp
    x     ExtraOp
    y     = (ExtraOp -> ExtraOp -> ExtraOp
    GCD ExtraOp
    x ExtraOp
    y, Normalised
    Untouched)

    mergeLCM :: ExtraOp -> ExtraOp -> NormaliseResult
    mergeLCM :: ExtraOp -> ExtraOp -> NormaliseResult
    mergeLCM (I Integer
    i) (I Integer
    j) = (Integer -> ExtraOp
    I (Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    lcm Integer
    i Integer
    j), Normalised
    Normalised)
    mergeLCM ExtraOp
    x     ExtraOp
    y     = (ExtraOp -> ExtraOp -> ExtraOp
    LCM ExtraOp
    x ExtraOp
    y, Normalised
    Untouched)

    mergeExp :: ExtraOp -> ExtraOp -> NormaliseResult
    mergeExp :: ExtraOp -> ExtraOp -> NormaliseResult
    mergeExp (I Integer
    i) (I Integer
    j)                = (Integer -> ExtraOp
    I (Integer
    iInteger -> Integer -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^Integer
    j), Normalised
    Normalised)
    mergeExp ExtraOp
    b     (Log ExtraOp
    b' ExtraOp
    y) | ExtraOp
    b ExtraOp -> ExtraOp -> Bool
    forall a. Eq a => a -> a -> Bool
    == ExtraOp
    b' = (ExtraOp
    y, Normalised
    Normalised)
    mergeExp ExtraOp
    x     ExtraOp
    y                    = (ExtraOp -> ExtraOp -> ExtraOp
    Exp ExtraOp
    x ExtraOp
    y, Normalised
    Untouched)

    -- | \x y -> logBase x y, x > 1 && y > 0
    flogBase :: Integer -> Integer -> Maybe Integer
    flogBase :: Integer -> Integer -> Maybe Integer
    flogBase Integer
    x Integer
    y | Integer
    y Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Integer
    0 = Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just (Int# -> Integer
    smallInteger (Integer -> Integer -> Int#
    integerLogBase# Integer
    x Integer
    y))
    flogBase Integer
    _ Integer
    _         = Maybe Integer
    forall a. Maybe a
    Nothing

    -- | \x y -> ceiling (logBase x y), x > 1 && y > 0
    clogBase :: Integer -> Integer -> Maybe Integer
    clogBase :: Integer -> Integer -> Maybe Integer
    clogBase Integer
    x Integer
    y | Integer
    y Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Integer
    0 =
      let z1 :: Int#
    z1 = Integer -> Integer -> Int#
    integerLogBase# Integer
    x Integer
    y
          z2 :: Int#
    z2 = Integer -> Integer -> Int#
    integerLogBase# Integer
    x (Integer
    yInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1)
      in  case Integer
    y of
             Integer
    1 -> Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just Integer
    0
             Integer
    _ | Int# -> Bool
    isTrue# (Int#
    z1 Int# -> Int# -> Int#
    ==# Int#
    z2) -> Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just (Int# -> Integer
    smallInteger (Int#
    z1 Int# -> Int# -> Int#
    +# Int#
    1#))
               | Bool
    otherwise           -> Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just (Int# -> Integer
    smallInteger Int#
    z1)
    clogBase Integer
    _ Integer
    _ = Maybe Integer
    forall a. Maybe a
    Nothing

    -- | \x y -> logBase x y, x > 1 && y > 0, logBase x y == ceiling (logBase x y)
    exactLogBase :: Integer -> Integer -> Maybe Integer
    exactLogBase :: Integer -> Integer -> Maybe Integer
    exactLogBase Integer
    x Integer
    y | Integer
    y Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Integer
    0 =
      let z1 :: Int#
    z1 = Integer -> Integer -> Int#
    integerLogBase# Integer
    x Integer
    y
          z2 :: Int#
    z2 = Integer -> Integer -> Int#
    integerLogBase# Integer
    x (Integer
    yInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1)
      in  case Integer
    y of
            Integer
    1 -> Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just Integer
    0
            Integer
    _ | Int# -> Bool
    isTrue# (Int#
    z1 Int# -> Int# -> Int#
    ==# Int#
    z2) -> Maybe Integer
    forall a. Maybe a
    Nothing
              | Bool
    otherwise           -> Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just (Int# -> Integer
    smallInteger Int#
    z1)
    exactLogBase Integer
    _ Integer
    _ = Maybe Integer
    forall a. Maybe a
    Nothing