-- |
-- Module      : Test.LeanCheck.Function.ShowFunction
-- Copyright   : (c) 2015-2018 Rudy Matela
-- License     : 3-Clause BSD  (see the file LICENSE)
-- Maintainer  : Rudy Matela <rudy@matela.com.br>
--
-- This module is part of LeanCheck,
-- a simple enumerative property-based testing library.
--
-- This module exports the 'ShowFunction' typeclass,
-- its instances and related functions.
--
-- Using this module, it is possible to implement
-- a 'Show' instance for functions:
--
-- > import Test.LeanCheck.ShowFunction
-- > instance (Show a, Listable a, ShowFunction b) => Show (a->b) where
-- >   show = showFunction 8
--
-- This shows functions as a case pattern with up to 8 cases.
--
-- It will only work for functions whose ultimate return value is an instance
-- of 'ShowFunction'.  This module provides instances for most standard data
-- types ('Int', 'Bool', 'Maybe', ...).  Please see the 'ShowFunction'
-- typeclass documentation for how to declare istances for user-defined data
-- types.
--
-- The modules
-- "Test.LeanCheck.Function"
-- and
-- "Test.LeanCheck.Function.Show"
-- exports an instance like the one above.
module Test.LeanCheck.Function.ShowFunction
  (
  -- * Showing functions
    showFunction
  , showFunctionLine

  -- * Support for user-defined algebraic datatypes on return values
  , ShowFunction (..)
  , bindtiersShow

  -- * Listing functional bindings
  , Binding
  , bindings

  -- * Pipeline for explaining, describing and clarifying bindings
  , explainedBindings
  , describedBindings
  , clarifiedBindings

  -- * Re-exports
  , Listable
  )
where

import Test.LeanCheck.Core
import Test.LeanCheck.Error (errorToNothing)
import Test.LeanCheck.Utils.Types
import Test.LeanCheck.Stats (classifyOn)
import Data.List (intercalate, sortBy)
import Data.Maybe
import Data.Function (on)

-- | A functional binding in a showable format.
--   Argument values are represented as a list of strings.
--   The result value is represented by 'Just' a 'String' when defined
--   or by 'Nothing' when 'undefined'.
type Binding = ([String], Maybe String)

-- | 'ShowFunction' values are those for which
--   we can return a list of functional bindings.
--
-- Instances for 'show'able algebraic datatypes are defined using
-- 'bindtiersShow':
--
-- > instance ShowFunction Ty where bindtiers = bindtiersShow
class ShowFunction a where
  bindtiers :: a -> [[Binding]]

-- | Given a 'ShowFunction' value, return a list of 'Binding's.
--   If the domain of the given argument function is infinite,
--   the resulting list is infinite.
--
-- Some examples follow.  These are used as running examples in the definition
-- of 'explainedBindings', 'describedBindings' and 'clarifiedBindings'.
--
-- * Defined return values are represented as 'Just' 'String's:
--
--     > > bindings True
--     > [([],Just "True")]
--
-- * Undefined return values are represented as @Nothing@:
--
--     > > bindings undefined
--     > [([],Nothing)]
--
-- * Infinite domains result in an infinite bindings list:
--
--     > > bindings (id::Int->Int)
--     > [ (["0"], Just "0")
--     > , (["1"], Just "1")
--     > , (["-1"], Just "-1")
--     > , ...
--     > ]
--
-- * Finite domains result in a finite bindings list:
--
--     > > bindings (&&)
--     > [ (["False","False"], Just "False")
--     > , (["False","True"], Just "False")
--     > , (["True","False"], Just "False")
--     > , (["True","True"], Just "True")
--     > ]
--
--     > > bindings (||)
--     > [ (["False","False"], Just "False")
--     > , (["False","True"], Just "True")
--     > , (["True","False"], Just "True")
--     > , (["True","True"], Just "True")
--     > ]
--
-- * Even very simple functions are represented by an infinite list of bindings:
--
--     > > bindings (== 0)
--     > [ (["0"], Just "True")
--     > , (["1"], Just "False")
--     > , (["-1"], Just "False")
--     > , ...
--     > ]
--
--     > > bindings (== 1)
--     > [ (["0"], Just "False")
--     > , (["1"], Just "True")
--     > , (["-1"], Just "False")
--     > , ...
--     > ]
--
-- * Ignored arguments are still listed:
--
--     > > bindings ((\_ y -> y == 1) :: Int -> Int -> Bool)
--     > [ (["0","0"], Just "False")
--     > , (["0","1"], Just "True")
--     > , (["1","0"], Just "False")
--     > , ...
--     > ]
--
-- * Again, undefined values are represented as 'Nothing'.
--   Here, the 'head' of an empty list is undefined:
--
--     > > bindings (head :: [Int] -> Int)
--     > [ (["[]"], Nothing)
--     > , (["[0]"], Just "0")
--     > , (["[0,0]"], Just "0")
--     > , (["[1]"], Just "1")
--     > , ...
--     > ]
bindings :: ShowFunction a => a -> [Binding]
bindings = concat . bindtiers


-- | A drop-in implementation of 'bindtiers' for 'show'able types.
--
-- Define instances for 'show'able algebraic datatypes as:
--
-- > instance ShowFunction Ty where bindtiers = bindtiersShow
bindtiersShow :: Show a => a -> [[Binding]]
bindtiersShow x = [[([],errorToNothing $ show x)]]

instance ShowFunction ()       where bindtiers = bindtiersShow
instance ShowFunction Bool     where bindtiers = bindtiersShow
instance ShowFunction Int      where bindtiers = bindtiersShow
instance ShowFunction Integer  where bindtiers = bindtiersShow
instance ShowFunction Char     where bindtiers = bindtiersShow
instance ShowFunction Float    where bindtiers = bindtiersShow
instance ShowFunction Double   where bindtiers = bindtiersShow
instance ShowFunction Ordering where bindtiers = bindtiersShow
instance Show a => ShowFunction [a]       where bindtiers = bindtiersShow
instance Show a => ShowFunction (Maybe a) where bindtiers = bindtiersShow
instance (Show a, Show b) => ShowFunction (Either a b) where bindtiers = bindtiersShow
instance (Show a, Show b) => ShowFunction (a,b) where bindtiers = bindtiersShow

-- instance for functional value type --
instance (Show a, Listable a, ShowFunction b) => ShowFunction (a->b) where
  bindtiers f = concatMapT bindtiersFor tiers
    where bindtiersFor x = mapFst (show x:) `mapT` bindtiers (f x)
          mapFst f (x,y) = (f x, y)

paren :: String -> String
paren s = "(" ++ s ++ ")"

varnamesFor :: ShowFunction a => a -> [String]
varnamesFor = zipWith const varnames . fst . head . bindings
  where varnames = ["x","y","z","w"] ++ map (++"'") varnames

showTuple :: [String] -> String
showTuple [x]  =  x
showTuple xs | all (== "_") xs  =  "_"
             | otherwise        =  paren $ intercalate "," xs

showBindings :: [Binding] -> [String]
showBindings bs = [ showTuple as ++ " -> " ++ r | (as, Just r) <- bs ]

showNBindings :: Bool -> Int -> [Binding] -> [String]
showNBindings infinite n bs' = take n bs ++ ["..." | infinite || length bs > n]
  where
  bs = showBindings bs'

isValue :: ShowFunction a => a -> Bool
isValue f = case bindings f of
              [([],_)] -> True
              _        -> False

showValueOf :: ShowFunction a => a -> String
showValueOf x = case snd . head . bindings $ x of
                  Nothing -> "undefined"
                  Just x' -> x'

-- | Given the number of patterns to show, shows a 'ShowFunction' value.
--
-- > > putStrLn $ showFunction undefined True
-- > True
-- >
-- > > putStrLn $ showFunction 3 (id::Int->Int)
-- > \x -> case x of
-- >       0 -> 0
-- >       1 -> 1
-- >       -1 -> -1
-- >       ...
-- >
-- > > putStrLn $ showFunction 4 (&&)
-- > \x y -> case (x,y) of
-- >         (True,True) -> True
-- >         _ -> False
-- >
--
-- In the examples above, "@...@" should be interpreted literally.
--
-- This can be used as an implementation of 'show' for functions:
--
-- > instance (Show a, Listable a, ShowFunction b) => Show (a->b) where
-- >   show = showFunction 8
--
-- See 'showFunctionLine' for an alternative without line breaks.
showFunction :: ShowFunction a => Int -> a -> String
showFunction n = showFunctionL False (n*n+1) n

-- | Same as 'showFunction', but has no line breaks.
--
-- > > putStrLn $ showFunctionLine 3 (id::Int->Int)
-- > \x -> case x of 0 -> 0; 1 -> 1; -1 -> -1; ...
-- > > putStrLn $ showFunctionLine 3 (&&)
-- > \x y -> case (x,y) of (True,True) -> True; _ -> False
--
-- This can be used as an implementation of 'show' for functions:
--
-- > instance (Show a, Listable a, ShowFunction b) => Show (a->b) where
-- >   show = showFunction 8
showFunctionLine :: ShowFunction a => Int -> a -> String
showFunctionLine n = showFunctionL True (n*n+1) n

-- | isUndefined checks if a function is totally undefined
--   for the given maximum number of values
isUndefined :: ShowFunction a => Int -> a -> Bool
isUndefined m = all (isNothing . snd) . take m . bindings

-- | checks if a function is constant
--   for the given maximum number of values
isConstant :: ShowFunction a => Int -> a -> Bool
isConstant m f = case take m $ bindings f of
                 []          -> False -- uninhabited type?
                 ((_,r'):bs) -> all (\(_,r) -> r == r') bs

-- | shows a constant function
showConstant :: ShowFunction a => Int -> a -> String
showConstant m f = "\\" ++ unwords vs ++ " -> " ++ fromMaybe "undefined" r
  where
  (as,r) = head $ bindings f
  vs = replicate (length as) "_"

-- The first boolean parameter tells if we are showing
-- the function on a single line
showFunctionL :: ShowFunction a => Bool -> Int -> Int -> a -> String
showFunctionL singleLine m n f | isValue f = showValueOf f
showFunctionL singleLine m n f | isConstant m f = showConstant m f
--showFunctionL singleLine m n f | canName m f = showName m f
showFunctionL singleLine m n f | otherwise = lambdaPat ++ caseExp
  where
    lambdaPat = "\\" ++ unwords vs ++ " -> "
    casePat = "case " ++ showTuple (filter (/= "_") vs) ++ " of"
    (vs, bindings) = clarifiedBindings m n f
    bs = showNBindings (length bindings >= m) n bindings
    sep | singleLine = " "
        | otherwise = "\n"
    cases | singleLine = intercalate "; " bs
          | otherwise  = unlines
                       $ (replicate (length lambdaPat) ' ' ++) `map` bs
    caseExp = if isUndefined m f
                then "undefined"
                else casePat ++ sep ++ cases

-- instances for further tuple arities --
instance (Show a, Show b, Show c)
      => ShowFunction (a,b,c) where bindtiers = bindtiersShow
instance (Show a, Show b, Show c, Show d)
      => ShowFunction (a,b,c,d) where bindtiers = bindtiersShow
instance (Show a, Show b, Show c, Show d, Show e)
      => ShowFunction (a,b,c,d,e) where bindtiers = bindtiersShow
instance (Show a, Show b, Show c, Show d, Show e, Show f)
      => ShowFunction (a,b,c,d,e,f) where bindtiers = bindtiersShow
instance (Show a, Show b, Show c, Show d, Show e, Show f, Show g)
      => ShowFunction (a,b,c,d,e,f,g) where bindtiers = bindtiersShow
instance (Show a, Show b, Show c, Show d, Show e, Show f, Show g, Show h)
      => ShowFunction (a,b,c,d,e,f,g,h) where bindtiers = bindtiersShow

-- instance for types from Test.LeanCheck.Utils.Types
instance ShowFunction Nat   where bindtiers = bindtiersShow
instance ShowFunction Nat1  where bindtiers = bindtiersShow
instance ShowFunction Nat2  where bindtiers = bindtiersShow
instance ShowFunction Nat3  where bindtiers = bindtiersShow
instance ShowFunction Nat4  where bindtiers = bindtiersShow
instance ShowFunction Nat5  where bindtiers = bindtiersShow
instance ShowFunction Nat6  where bindtiers = bindtiersShow
instance ShowFunction Nat7  where bindtiers = bindtiersShow
instance ShowFunction Int1  where bindtiers = bindtiersShow
instance ShowFunction Int2  where bindtiers = bindtiersShow
instance ShowFunction Int3  where bindtiers = bindtiersShow
instance ShowFunction Int4  where bindtiers = bindtiersShow
instance ShowFunction Word1 where bindtiers = bindtiersShow
instance ShowFunction Word2 where bindtiers = bindtiersShow
instance ShowFunction Word3 where bindtiers = bindtiersShow
instance ShowFunction Word4 where bindtiers = bindtiersShow

-- | Hard coded function names and bindings
--   Search this list for a short name for your function.
functionNames :: [(String, [Binding])]
functionNames =
  [ "id"    `for` (id          :: () -> ())
  , "const" `for` (const       :: () -> () -> ())

  -- booleans
  , "id"    `for` (id          :: Bool -> Bool)
  , "not"   `for` (not         :: Bool -> Bool)
  , "const" `for` (const :: Bool -> Bool -> Bool)

  , "(&&)"  `for` (&&)
  , "(||)"  `for` (||)

  -- numeric types
  , "id"      `for` (id      :: Int -> Int)
  , "const"   `for` (const   :: Int -> Int -> Int)

  -- Num typeclass
  , "(+)"     `for` ((+)     :: Int -> Int -> Int)
  , "(-)"     `for` ((-)     :: Int -> Int -> Int)
  , "(*)"     `for` ((*)     :: Int -> Int -> Int)
  , "negate"  `for` (negate  :: Int -> Int)
  , "abs"     `for` (abs     :: Int -> Int)
  , "signum"  `for` (signum  :: Int -> Int)

  -- integer properties
  , "odd"     `for` (odd     :: Int -> Bool)
  , "even"    `for` (even    :: Int -> Bool)
  ]
  where
  n `for` f = (n, bindings f)

-- | Tries to name a function heuristically
name :: ShowFunction a => Int -> a -> Maybe String
name n f = listToMaybe [ nm | (nm, bs) <- functionNames
                            , take n bs == take n (bindings f)]

canName :: ShowFunction a => Int -> a -> Bool
canName n = isJust . name n

showName :: ShowFunction a => Int -> a -> String
showName n = fromMaybe "unknown" . name n

-- | Returns a set of variables and a set of bindings
--   describing how a function works.
--
-- Some argument values are generalized to "@_@" when possible.
-- If one of the function arguments is not used altogether, it is ommited in
-- the set of bindings and appears as "_" in the variables list.
--
-- This is the /last/ function in the clarification pipeline.
--
-- It takes two integer arguments:
--
-- 1. @m@: the maximum number of cases considered for computing the description;
-- 2. @n@: the maximum number of cases in the actual description.
--
-- As a general rule of thumb, set @m=n*n+1@.
--
-- Some examples follow:
--
-- * When all arguments are used, the result is the same as 'describedBindings':
--
--     > > clarifiedBindings 100 10 (==1)
--     > ( ["x"], [ (["1"],Just "True"),
--     >          , (["_"],Just "False") ] )
--
-- * When some arguments are unused, they are omitted in the list of bindings and
--   appear as @"_"@ in the list of variables.
--
--     > > clarifiedBindings 100 10 (\_ y -> y == 1)
--     > ( ["_", "y"], [ (["1"],Just "True")
--     >               , (["_"],Just "False") ] )
clarifiedBindings :: ShowFunction a => Int -> Int -> a -> ([String],[Binding])
clarifiedBindings m n = clarifyBindings . describedBindings m n

clarifyBindings :: [Binding] -> ([String],[Binding])
clarifyBindings bs  =  (varnamesByUsage used, map (mapFst $ select used) bs)
  where
  mapFst f (x,y) = (f x, y)
  used = usedArgs bs

varnamesByUsage :: [Bool] -> [String]
varnamesByUsage = zipWith used varnames
  where
  used s False = "_"
  used s True  = s
  varnames = ["x","y","z","w"] ++ map (++"'") varnames

usedArgs :: [Binding] -> [Bool]
usedArgs = foldr1 (zipWith (||))
         . map (map (/= "_") . fst)

-- | Returns a set of bindings describing how a function works.
-- Some argument values are generalized to "@_@" when possible.
-- It takes two integer arguments:
--
-- 1. @m@: the maximum number of cases considered for computing description;
-- 2. @n@: the maximum number of cases in the actual description.
--
-- As a general rule of thumb, set @m=n*n+1@.
--
-- This is the /second/ function in the clarification pipeline.
--
-- This function processes the result of 'explainedBindings'
-- to sometimes return shorter descriptions.
-- It chooses the shortest of the following (in order):
--
-- * regular unexplained-undescribed 'bindings';
-- * regular 'explainedBindings';
-- * 'explainedBindings' with least occurring cases generalized first;
--
-- Here are some examples:
--
-- * Sometimes the result is the same as 'explainedBindings':
--
--     > > describedBindings 100 10 (||)
--     > [ (["False","False"],Just "False")
--     > , (["_","_"],Just "True") ]
--
--     > > describedBindings 100 10 (==0)
--     > [ (["0"],Just "True")
--     > , (["_"],Just "False") ]
--
-- * but sometimes it is shorter because we consider generalizing least
--   occurring cases first:
--
--     > > describedBindings 100 10 (&&)
--     > [ ( ["True","True"],Just "True")
--     > , ( ["_","_"],Just "False") ]
--
--     > > describedBindings 100 10 (==1)
--     > [ (["1"],Just "True"),
--     > , (["_"],Just "False") ]
--
--     > > describedBindings 100 10 (\_ y -> y == 1)
--     > [ (["_","1"],Just "True")
--     > , (["_","_"],Just "False") ]
describedBindings :: ShowFunction a => Int -> Int -> a -> [Binding]
describedBindings m n f
  | length bs1 <= n  =  bs1
  | otherwise        =  bs0
  where
  bs0  =  take m $ bindings f
  bs1  =  describeBindings bs0

describeBindings :: [Binding] -> [Binding]
describeBindings bs = head $ sortOn length $
  [ bs
  , explainBindings bs
  , explainBindings . concat . sortOn length $ classifyOn snd bs
  ]

-- | Returns a set of bindings explaining how a function works.
--   Some argument values are generalized to "@_@" when possible.
--   It takes as argument the maximum number of cases
--   considered for computing the explanation.
--
-- A measure of success in this generalization process is if this function
-- returns less values than the asked maximum number of cases.
--
-- This is the /first/ function in the clarification pipeline.
--
-- * In some cases, 'bindings' cannot be "explained"
--   an almost unchanged result of 'bindings' is returned
--   with the last binding having variables replaced by "@_@":
--
--     > > explainedBindings 4 (id::Int->Int)
--     > [ (["0"],Just "0")
--     > , (["1"],Just "1")
--     > , (["-1"],Just "-1")
--     > , (["_"],Just "2") ]
--
-- * When possible, some cases are generalized using @_@:
--
--     > > explainedBindings 10 (||)
--     > [ (["False","False"],Just "False")
--     > , (["_","_"],Just "True") ]
--
--     but the resulting "explanation" might not be the shortest possible
--     (cf. 'describedBindings'):
--
--     > > explainedBindings 10 (&&)
--     > [ ( ["False","_"],Just "False")
--     > , (["_","False"],Just "False")
--     > , (["_","_"],Just "True") ]
--
-- * Generalization works for infinite domains (heuristically):
--
--     > > explainedBindings 10 (==0)
--     > [ (["0"],Just "True")
--     > , (["_"],Just "False") ]
--
-- * Generalization for each item is processed in the order they are generated by 'bindings'
--   hence explanations are not always the shortest possible (cf. 'describedBindings').
--   In the following examples, the first case is redundant.
--
--     > > explainedBindings 10 (==1)
--     > [ (["0"],Just "False")
--     > , (["1"],Just "True"),
--     > , (["_"],Just "False") ]
--
--     > > explainedBindings 10 (\_ y -> y == 1)
--     > [ (["_","0"],Just "False")
--     > , (["_","1"],Just "True")
--     > , (["_","_"],Just "False") ]
explainedBindings :: ShowFunction a => Int -> a -> [Binding]
explainedBindings m = explainBindings . take m . bindings

explainBindings :: [Binding] -> [Binding]
explainBindings = explain []
  where
  explain :: [Binding] -> [Binding] -> [Binding]
  explain bs' []           =  reverse bs'
  explain bs' ((as,r):bs)  =  explain (bs''++bs') [b | b <- bs, none (b <~~) bs'']
    where
    bs'' = discardLater (<~~)
         [ (gas,r) | gas <- generalizations as
                   , and [r' == r | (as',r') <- bs, as' <~ gas] ]

generalizations :: [String] -> [[String]]
generalizations []     = [[]]
generalizations (v:vs) = map ("_":) gvs ++ map (v:) gvs
  where
  gvs = generalizations vs

-- | Should be read as "is generalized by":
--
-- > > ["1","2","3"] <~ ["_","_","_"]
-- > True
-- > > ["_","_","_"] <~ ["1","2","3"]
-- > False
-- > > ["1","3"] <~ ["_","3"]
-- > True
-- > > ["_","3"] <~ ["_","4"]
-- > False
(<~) :: [String] -> [String] -> Bool
[]     <~ []       =  True
(v:vs) <~ ("_":ws) =  vs <~ ws
(v:vs) <~ (w:ws)   =  v == w && vs <~ ws
_      <~ _        =  False

-- | Should be read as "is generalized by".
(<~~) :: Binding -> Binding -> Bool
(as,r) <~~ (as',r') = as <~ as' && r == r'


-- general auxiliary functions

discard :: (a -> Bool) -> [a] -> [a]
discard p = filter (not . p)

discardLater :: (a -> a -> Bool) -> [a] -> [a]
discardLater (?>) = dl
  where
  dl []     = []
  dl (x:xs) = x : discard (?> x) (dl xs)

none :: (a -> Bool) -> [a] -> Bool
none p = not . any p

-- sortOn is only available on GHC > 7.8
sortOn :: Ord b => (a -> b) -> [a] -> [a]
sortOn f = sortBy (compare `on` f)

select :: [Bool] -> [a] -> [a]
select [] _ = []
select _ [] = []
select (p:ps) (x:xs) = if p then x : xs' else xs' where xs' = select ps xs