-- |
-- Module      :  $Header$
-- Copyright   :  (c) 2013-2015 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable
--
-- This module defines intervals and interval arithmetic.

{-# LANGUAGE Safe #-}
module Cryptol.TypeCheck.Solver.Interval
  ( Interval(..)
  , anything
  , iConst

  , iAdd, iMul, iExp
  , iMin, iMax
  , iLg2, iWidth

  , iSub, iDiv, iMod

  , iLenFromThen, iLenFromTo, iLenFromThenTo

  , iLeq, iLt, iDisjoint
  ) where


import Cryptol.TypeCheck.Solver.InfNat


{- | Representation of intervals.
Intervals always include the lower bound.
Intervals include the upper bound if:
  * either the upper bound is finite, or
  * the upper bound is 'Inf' and @isFinite == False@.

Invariant: if the upper bound is finite, then `isFinite == True`.

> [x,y]     Interval (Nat x) (Nat y) True
> [x,inf]   Interval (Nat x) Inf     False
> [x,inf)   Interval (Nat x) Inf     True

-}
data Interval = Interval
  { lowerBound     :: Nat'  -- ^ Lower bound
  , upperBound     :: Nat'  -- ^ Upper bound
  , isFinite       :: Bool  -- ^ Do we know this to be a finite value.
      -- Note that for @[inf,inf]@ this field is `False`
      -- (i.e., this field is not talking about the size of the interval,
      -- but, rather, about if it contains infinity).
  } deriving Show

-- | Any possible value.
anything :: Interval
anything = Interval { lowerBound = Nat 0
                    , upperBound = Inf
                    , isFinite   = False
                    }

anyFinite :: Interval
anyFinite = anything { isFinite = True }

iConst :: Nat' -> Interval
iConst x = Interval { lowerBound = x, upperBound = x, isFinite = x < Inf }

iAdd :: Interval -> Interval -> Interval
iAdd = liftMono2 nAdd (&&)

iMul :: Interval -> Interval -> Interval
iMul = liftMono2 nMul (&&)

iMin :: Interval -> Interval -> Interval
iMin = liftMono2 nMin (||)

iMax :: Interval -> Interval -> Interval
iMax = liftMono2 nMax (&&)

iLg2 :: Interval -> Interval
iLg2 = liftMono1 nLg2

iWidth :: Interval -> Interval
iWidth = liftMono1 nWidth


iExp :: Interval -> Interval -> Interval
iExp i1 i2 = fixUp (liftMono2 nExp (&&) i1 i2)
  where
  -- exp k : is a monotonic function for k >= 1
  -- exp 0 : is a monotonic from 1 onwards
  -- Example of why we need fixing, consdier:
  -- [0,0] ^ [0,5]
  -- Monotonic computation results in:
  -- [1,0]
  fixUp i3
    | lowerBound i1 == Nat 0 &&
      lowerBound i2 == Nat 0 &&
      upperBound i2 >= Nat 1 =
        Interval { lowerBound = Nat 0
                 , upperBound = nMax (Nat 1) (upperBound i3)
                 , isFinite   = isFinite i3
                 }
  fixUp i3 = i3


iSub :: Interval -> Interval -> Interval
iSub = liftPosNeg nSub

iDiv :: Interval -> Interval -> Interval
iDiv = liftPosNeg nDiv

iMod :: Interval -> Interval -> Interval
iMod _ i2 = Interval { lowerBound = Nat 0
                     , upperBound = case upperBound i2 of
                                      Inf   -> Inf
                                      Nat n -> Nat (n - 1)
                     , isFinite   = True -- we never have infinite reminder.
                     }

-- XXX
iLenFromThen :: Interval -> Interval -> Interval -> Interval
iLenFromThen _ _ _ = anyFinite

-- XXX
iLenFromTo :: Interval -> Interval -> Interval
iLenFromTo _ _ = anyFinite

-- XXX
iLenFromThenTo :: Interval -> Interval -> Interval -> Interval
iLenFromThenTo _ _ _ = anyFinite




-- | The first interval is definiately smaller
iLeq :: Interval -> Interval -> Bool
iLeq i1 i2 = upperBound i1 <= lowerBound i2

-- | The first interval is definiately smaller
iLt :: Interval -> Interval -> Bool
iLt i1 i2 = upperBound i1 < lowerBound i2
         || (isFinite i1 && lowerBound i2 == Inf)

-- | The two intervals do not overlap.
iDisjoint :: Interval -> Interval -> Bool
iDisjoint i1 i2 = iLt i1 i2 || iLt i2 i1


--------------------------------------------------------------------------------


liftMono1 :: (Nat' -> Nat')     -- ^ Binary monotonic fun. to lift
          -> Interval -> Interval
liftMono1 f i =
  let u = f (upperBound i)
  in Interval { lowerBound = f (lowerBound i)
              , upperBound = u
              , isFinite   = mkFin (isFinite i) u
              }

liftMono2 :: (Nat' -> Nat' -> Nat')     -- ^ Binary monotonic fun. to lift
          -> (Bool -> Bool -> Bool)     -- ^ Compute finitneness
          -> Interval -> Interval -> Interval
liftMono2 f isF i1 i2 =
  let u = f (upperBound i1) (upperBound i2)
  in Interval { lowerBound = f (lowerBound i1) (lowerBound i2)
              , upperBound = u
              , isFinite   = mkFin (isF (isFinite i1) (isFinite i2)) u
              }


-- For div and sub, increase in first argument, decrease in second.
liftPosNeg :: (Nat' -> Nat' -> Maybe Nat')
           -> Interval -> Interval -> Interval
liftPosNeg f i1 i2 =
  Interval { lowerBound = case f (lowerBound i1) (upperBound i2) of
                            Nothing -> Nat 0
                            Just n  -> n
          , upperBound  = case f (upperBound i1) (lowerBound i2) of
                            Just n  -> n
                            Nothing -> upperBound i1
          , isFinite    = isFinite i1
          }

mkFin :: Bool -> Nat' -> Bool
mkFin ifInf ub = case ub of
                   Nat _ -> True
                   Inf   -> ifInf