-- |
-- 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 (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 (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 (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 (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 (m :: * -> *) a. Monad m => a -> m a
return (Integer
k, Type
t2)
           Type
_                      -> (Integer, Type) -> Maybe (Integer, Type)
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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Integer, Type) -> Maybe (Integer, Type)
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 (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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Integer, Type) -> Maybe (Integer, Type)
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