Utils.hs

-- |
-- 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 ty0 = [ (x,t1) | (x,t1) <- go ty0, tNum (0::Int) /= t1 ]
  where
  go ty = case ty of
            TVar x      -> return (x, tNum (0::Int))
            TRec {}     -> []
            TNominal {}  -> []
            TUser _ _ t -> go t
            TCon (TF TCAdd) [t1,t2] ->
              do (a,yes) <- go t1
                 return (a, tAdd yes t2)
              `mplus`
              do (a,yes) <- go t2
                 return (a, tAdd t1 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 a ty = listToMaybe [ t | (x,t) <- splitVarSummands ty, x == 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 ty =
  case ty of
    TVar {}     -> Nothing
    TRec {}     -> Nothing
    TNominal {} -> Nothing
    TUser _ _ t -> splitConstSummand t
    TCon (TF TCAdd) [t1,t2] ->
      do (k,t1') <- splitConstSummand t1
         case t1' of
           TCon (TC (TCNum 0)) [] -> return (k, t2)
           _                      -> return (k, tAdd t1' t2)
    TCon (TC (TCNum k)) [] -> guard (k > 0) >> return (k, tNum (0::Int))
    TCon {}     -> 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 ty =
  case ty of
    TVar {}     -> Nothing
    TRec {}     -> Nothing
    TNominal {} -> Nothing
    TUser _ _ t -> splitConstFactor t
    TCon (TF TCMul) [t1,t2] ->
      do (k,t1') <- splitConstFactor t1
         return (k, tMul t1' t2)
    TCon (TC (TCNum k)) [] -> guard (k > 1) >> return (k, tNum (1::Int))
    TCon {}     -> Nothing