-- |
-- 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 ty0 :: Type
ty0 = [ (TVar
x,Type
t1) | (x :: TVar
x,t1 :: Type
t1) <- Type -> [(TVar, Type)]
go Type
ty0, Int -> Type
forall a. Integral a => a -> Type
tNum (0::Int) Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
/= Type
t1 ]
  where
  go :: Type -> [(TVar, Type)]
go ty :: Type
ty = case Type
ty of
            TVar x :: 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 (0::Int))
            TRec {}     -> []
            TUser _ _ t :: Type
t -> Type -> [(TVar, Type)]
go Type
t
            TCon (TF TCAdd) [t1 :: Type
t1,t2 :: Type
t2] ->
              do (a :: TVar
a,yes :: 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 (a :: TVar
a,yes :: 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 _ _    -> [] -- 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 a :: TVar
a ty :: Type
ty = [Type] -> Maybe Type
forall a. [a] -> Maybe a
listToMaybe [ Type
t | (x :: TVar
x,t :: 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 ty :: Type
ty =
  case Type
ty of
    TVar {}     -> Maybe (Integer, Type)
forall a. Maybe a
Nothing
    TRec {}     -> Maybe (Integer, Type)
forall a. Maybe a
Nothing
    TUser _ _ t :: Type
t -> Type -> Maybe (Integer, Type)
splitConstSummand Type
t
    TCon (TF TCAdd) [t1 :: Type
t1,t2 :: Type
t2] ->
      do (k :: Integer
k,t1' :: Type
t1') <- Type -> Maybe (Integer, Type)
splitConstSummand Type
t1
         case Type
t1' of
           TCon (TC (TCNum 0)) [] -> (Integer, Type) -> Maybe (Integer, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer
k, Type
t2)
           _                      -> (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 k :: Integer
k)) [] -> Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
k Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> 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 (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 ty :: Type
ty =
  case Type
ty of
    TVar {}     -> Maybe (Integer, Type)
forall a. Maybe a
Nothing
    TRec {}     -> Maybe (Integer, Type)
forall a. Maybe a
Nothing
    TUser _ _ t :: Type
t -> Type -> Maybe (Integer, Type)
splitConstFactor Type
t
    TCon (TF TCMul) [t1 :: Type
t1,t2 :: Type
t2] ->
      do (k :: Integer
k,t1' :: 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 k :: Integer
k)) [] -> Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
k Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> 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 (1::Int))
    TCon {}     -> Maybe (Integer, Type)
forall a. Maybe a
Nothing