{-# OPTIONS -Wall #-}
----------------------------------------------------------------------
-- |
-- Module      :  Data.SImproving
-- Copyright   :  (c) Conal Elliott 2008
-- License     :  BSD3
-- 
-- Maintainer  :  conal@conal.net
-- Stability   :  experimental
-- 
-- \"Improving values\" from Warren Burton's \"Encapsulating Nondeterminacy
-- in an Abstract Data Type with Deterministic Semantics\".
-- 
-- This implementation is simple but not efficient, as it accumulates lots
-- of lower bounds.
----------------------------------------------------------------------

module Reactive.SImproving
  (
    Improving(..), exactly, exact, improveMbs
  -- * Misc speculation tools
  , spec, specNY, specYY, start
  ) where

import Data.Function (on)
-- import Debug.Trace

import Control.Parallel (par)

-- | Progressive information about a value (e.g., a time).  Represented as
-- a non-empty list of monotonically non-decreasing values.  The last one
-- is the actual value.  (The operations here ensure that the values are
-- strictly increasing, but they only rely on non-decreasing.)
newtype Improving a = Imp { unImp :: [a] } deriving Show

-- | Apply a unary function inside an 'Improving' representation.
inImp :: ([a] -> [b]) -> (Improving a -> Improving b)
inImp f = Imp . f . unImp

-- | Apply a unary function inside an 'Improving' representation.
inImp2 :: ([a] -> [b] -> [c]) -> (Improving a -> Improving b -> Improving c)
inImp2 f = inImp . f . unImp

-- | A known improving value (which doesn't really improve)
exactly :: Ord a => a -> Improving a
exactly = Imp . (:[])

-- | Extract an exact value from an improving value
exact :: Improving a -> a
exact = last . unImp

instance Eq a => Eq (Improving a) where
  (==) = (==) `on` exact

instance Ord a => Ord (Improving a) where
  Imp xs `compare` Imp ys = -- trace "Improving: compare" $
                            xs `compares` ys
  -- experimental.  probably eliminate.
  Imp xs <= Imp ys = xs `leq` ys
  min = inImp2 shortMerge
  max = inImp2 (specNY monotonicAppend)

-- This one wasn't in the Improving Values papers.  Here so that
-- 'compare', '(<=)', etc are defined on Improving.
compares :: Ord a => [a] -> [a] -> Ordering
compares [] _    = error "compares: emptied first argument"
compares _ []    = error "compares: emptied second argument"
compares [x] (y:_) | x < y = LT
compares (x:_) [y] | x > y = GT
compares [x] [y] = compare x y
-- we know x >= y and length ys >= 2
compares xs@[_] (_:ys') = compares xs ys'
-- we know x <= y and length xs >= 2
compares (_:xs') ys@[_] = compares xs' ys
-- neither list is down to last element.  progress where less is known.
compares xs@(x:xs') ys@(y:ys') | x == y    = compares xs' ys'
                               | x  < y    = compares xs' ys
                               | otherwise = compares xs  ys'

-- Hm!  The test I really want is (<=), which can get an answer based on
-- slightly less information than compares.

leq :: Ord a => [a] -> [a] -> Bool
leq [] _    = error "leq: emptied first argument"
leq _ []    = error "leq: emptied second argument"
leq [x] (y:_) | x <= y = True
leq (x:_) [y] | x >  y = False
leq [x] [y] = x <= y
-- we know x > y and length ys >= 2
leq xs@[_] (_:ys') = leq xs ys'
-- we know x <= y and length xs >= 2
leq (_:xs') ys@[_] = leq xs' ys
-- neither list is down to last element.  progress where less is known.
leq xs@(x:xs') ys@(y:ys') | x == y    = leq xs' ys'
                          | x  < y    = leq xs' ys
                          | otherwise = leq xs  ys'

-- leq didn't fix the bug I'm finding in phooey (src/Examples/Monad, t5)
-- when using SReactive instead of PrimReactive in Data/Reactive.
-- Probably remove leq later.


shortMerge :: Ord a => [a] -> [a] -> [a]
shortMerge [] _ = []
shortMerge _ [] = []
shortMerge xs@(x:xs') ys@(y:ys')
  | x == y    = x : shortMerge xs' ys'
  | x <  y    = x : shortMerge xs' ys
  | otherwise = y : shortMerge xs  ys'

monotonicAppend :: Ord a => [a] -> [a] -> [a]
-- monotonicAppend [x]     ys = x : dropWhile (<= x) ys
-- monotonicAppend (x:xs') ys = x : monotonicAppend xs' ys
-- monotonicAppend []      _  = error "monotonicAppend: empty list"

-- From "Encapsulating nondeterminacy in an abstract data type with
-- deterministic semantics"
monotonicAppend xs ys = xs ++ dropWhile (<= last xs) ys


-- TODO: consider trimming ys as we go, rather than later.  However, I
-- have a fuzzy understanding of why spec_max and not just max in the
-- papers.

-- | Interpret 'Nothing' values as lower bounds
improveMbs :: [(t, Maybe a)] -> [(Improving t, a)]
improveMbs = foldr f []
 where
   f (t,Just a ) qs = (Imp [t],a) : qs
   f (t,Nothing) ~((Imp ts', a) : qs') = (Imp (t:ts'), a) : qs'
   -- f (_,Nothing) [] = error "improveMbs: input ends in a Nothing"

-- The lazy pattern (~) above is essential for laziness.  It also
-- complicates giving an error message if the input ends in a Nothing.

-- improveMbs [] = []
-- improveMbs ((t,Just a ) : ps') = (Imp [{-tr True-} t],a) : improveMbs ps'
-- improveMbs ((t,Nothing) : ps') = (Imp ({-tr False-} t:ts'), a) : qs'
--  where
--     (Imp ts', a) : qs' = improveMbs ps'

-- tr :: (Show x, Show t) => x -> t -> t
-- tr x t = t
--          -- trace (show (t, x)) t

-- improveMbs = foldr f []
--  where
--    f (t,Just a ) qs = (Imp [t],a) : qs
--    f (t,Nothing) qs =
--      case qs of ((Imp ts', a) : qs') -> (Imp (t:ts'), a) : qs'
--                 [] -> error "improveMbs: input ends in a Nothing"

-- TODO: re-think the case of input ending in a Nothing.


---- Misc

spec :: (a -> b) -> (a -> b)
spec f a = a `par` f a

specNY :: (a -> b -> c) -> (a -> b -> c)
specNY f a = spec (f a)

specYY :: (a -> b -> c) -> (a -> b -> c)
specYY f a = spec (spec f a)

start :: [a] -> [a]
start [] = []
start (x:xs) = specYY (:) x (start xs)

-- Hm. Does this specNY really do anything?  How far does 'par' evaluate?
-- Probably to WHNF, which wouldn't help much, would it?  And I don't
-- understand the point yet.  Read further in the paper.