    -- |
    -- Module      :  Cryptol.TypeCheck.Solver.Utils
    -- Copyright   :  (c) 2013-2016 Galois, Inc.
    -- License     :  BSD3
    -- Maintainer  :  cryptol@galois.com
    -- Stability   :  provisional
    -- Portability :  portable

    module Cryptol.TypeCheck.Solver.Utils where

    import Cryptol.TypeCheck.AST hiding (tMul)
    import Cryptol.TypeCheck.SimpType(tAdd,tMul)
    import Control.Monad(mplus,guard)
    import Data.Maybe(listToMaybe)

    -- | All ways to split a type in the form: @a + t1@, where @a@ is a variable.
    splitVarSummands :: Type -> [(TVar,Type)]
    splitVarSummands :: Type -> [(TVar, Type)]
    splitVarSummands Type
    ty0 = [ (TVar
    x,Type
    t1) | (TVar
    x,Type
    t1) <- Type -> [(TVar, Type)]
    go Type
    ty0, Int -> Type
    forall a. Integral a => a -> Type
    tNum (Int
    0::Int) Type -> Type -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Type
    t1 ]
      where
      go :: Type -> [(TVar, Type)]
    go Type
    ty = case Type
    ty of
                TVar TVar
    x      -> (TVar, Type) -> [(TVar, Type)]
    forall a. a -> [a]
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TVar
    x, Int -> Type
    forall a. Integral a => a -> Type
    tNum (Int
    0::Int))
                TRec {}     -> []
                TNewtype{}  -> []
                TUser Name
    _ [Type]
    _ Type
    t -> Type -> [(TVar, Type)]
    go Type
    t
                TCon (TF TFun
    TCAdd) [Type
    t1,Type
    t2] ->
                  do (TVar
    a,Type
    yes) <- Type -> [(TVar, Type)]
    go Type
    t1
                     (TVar, Type) -> [(TVar, Type)]
    forall a. a -> [a]
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TVar
    a, Type -> Type -> Type
    tAdd Type
    yes Type
    t2)
                  [(TVar, Type)] -> [(TVar, Type)] -> [(TVar, Type)]
    forall a. [a] -> [a] -> [a]
    forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
    `mplus`
                  do (TVar
    a,Type
    yes) <- Type -> [(TVar, Type)]
    go Type
    t2
                     (TVar, Type) -> [(TVar, Type)]
    forall a. a -> [a]
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TVar
    a, Type -> Type -> Type
    tAdd Type
    t1 Type
    yes)
                TCon TCon
    _ [Type]
    _    -> [] -- XXX: we could do some distributivity etc

    -- | Check if we can express a type in the form: @a + t1@.
    splitVarSummand :: TVar -> Type -> Maybe Type
    splitVarSummand :: TVar -> Type -> Maybe Type
    splitVarSummand TVar
    a Type
    ty = [Type] -> Maybe Type
    forall a. [a] -> Maybe a
    listToMaybe [ Type
    t | (TVar
    x,Type
    t) <- Type -> [(TVar, Type)]
    splitVarSummands Type
    ty, TVar
    x TVar -> TVar -> Bool
    forall a. Eq a => a -> a -> Bool
    == TVar
    a ]

    {- | Check if we can express a type in the form: @k + t1@,
    where @k@ is a constant > 0.
    This assumes that the type has been simplified already,
    so that constants are floated to the left. -}
    splitConstSummand :: Type -> Maybe (Integer, Type)
    splitConstSummand :: Type -> Maybe (Integer, Type)
    splitConstSummand Type
    ty =
      case Type
    ty of
        TVar {}     -> Maybe (Integer, Type)
    forall a. Maybe a
    Nothing
        TRec {}     -> Maybe (Integer, Type)
    forall a. Maybe a
    Nothing
        TNewtype{}  -> Maybe (Integer, Type)
    forall a. Maybe a
    Nothing
        TUser Name
    _ [Type]
    _ Type
    t -> Type -> Maybe (Integer, Type)
    splitConstSummand Type
    t
        TCon (TF TFun
    TCAdd) [Type
    t1,Type
    t2] ->
          do (Integer
    k,Type
    t1') <- Type -> Maybe (Integer, Type)
    splitConstSummand Type
    t1
             case Type
    t1' of
               TCon (TC (TCNum Integer
    0)) [] -> (Integer, Type) -> Maybe (Integer, Type)
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Integer
    k, Type
    t2)
               Type
    _                      -> (Integer, Type) -> Maybe (Integer, Type)
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Integer
    k, Type -> Type -> Type
    tAdd Type
    t1' Type
    t2)
        TCon (TC (TCNum Integer
    k)) [] -> Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Integer
    k Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Integer
    0) Maybe () -> Maybe (Integer, Type) -> Maybe (Integer, Type)
    forall a b. Maybe a -> Maybe b -> Maybe b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> (Integer, Type) -> Maybe (Integer, Type)
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Integer
    k, Int -> Type
    forall a. Integral a => a -> Type
    tNum (Int
    0::Int))
        TCon {}     -> Maybe (Integer, Type)
    forall a. Maybe a
    Nothing

    {- | Check if we can express a type in the form: @k * t1@,
    where @k@ is a constant > 1.
    This assumes that the type has been simplified already,
    so that constants are floated to the left. -}
    splitConstFactor :: Type -> Maybe (Integer, Type)
    splitConstFactor :: Type -> Maybe (Integer, Type)
    splitConstFactor Type
    ty =
      case Type
    ty of
        TVar {}     -> Maybe (Integer, Type)
    forall a. Maybe a
    Nothing
        TRec {}     -> Maybe (Integer, Type)
    forall a. Maybe a
    Nothing
        TNewtype{}  -> Maybe (Integer, Type)
    forall a. Maybe a
    Nothing
        TUser Name
    _ [Type]
    _ Type
    t -> Type -> Maybe (Integer, Type)
    splitConstFactor Type
    t
        TCon (TF TFun
    TCMul) [Type
    t1,Type
    t2] ->
          do (Integer
    k,Type
    t1') <- Type -> Maybe (Integer, Type)
    splitConstFactor Type
    t1
             (Integer, Type) -> Maybe (Integer, Type)
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Integer
    k, Type -> Type -> Type
    tMul Type
    t1' Type
    t2)
        TCon (TC (TCNum Integer
    k)) [] -> Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Integer
    k Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Integer
    1) Maybe () -> Maybe (Integer, Type) -> Maybe (Integer, Type)
    forall a b. Maybe a -> Maybe b -> Maybe b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> (Integer, Type) -> Maybe (Integer, Type)
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Integer
    k, Int -> Type
    forall a. Integral a => a -> Type
    tNum (Int
    1::Int))
        TCon {}     -> Maybe (Integer, Type)
    forall a. Maybe a
    Nothing