-- | Concrete functions
--
-- Intended for qualified import.
--
-- > import Data.Falsify.ConcreteFun ((:->)(..))
-- > import qualified Data.Falsify.ConcreteFun as ConcreteFun
module Data.Falsify.ConcreteFun (
    (:->)(..)
    -- * Construction
  , map
    -- * Application
  , apply
    -- * Rendering
  , render
  ) where

import Prelude hiding (map)

import Control.Monad
import Data.Bifunctor
import Data.Foldable (toList)
import Data.Kind
import Data.List (intercalate)
import Data.Maybe (fromMaybe, mapMaybe)

import Data.Falsify.Tree (Tree(..))

import qualified Data.Falsify.Tree as Tree

{-------------------------------------------------------------------------------
  Definition

  NOTE: @Nil@ is useful as a separate constructor, since it does not have an
  @Eq@ constraint.
-------------------------------------------------------------------------------}

-- | Concrete function
--
-- A concrete function is essentially a deep embedding: an explicit
-- representation of the ouput value of the function for every input value in
-- the function's domain.
--
-- Concrete functions are the central building block for generating random
-- functions, as proposed by Koen Claessen in \"Shrinking and showing
-- functions\", Haskell Symposium 2012
-- (<https://dl.acm.org/doi/10.1145/2430532.2364516>). Koen's key insight is
-- that we can start with an infinite concrete function that is defined on every
-- value in the input domain, but since in any given test that function is only
-- applied to a finite number of inputs, we can then shrink the concrete
-- function, throwing away entire chunks of the input domain, until we are left
-- with a finite representation which can be printed as part of a test output.
--
-- All of the cleverness for /generating/ concrete functions is about reducing
-- the explicitly represented /domain/ of the function. To shrink the /outputs/
-- of the function nothing special is needed, and we can just rely on Haskell's
-- laziness and the fact that @falsify@ is carefully constructed so that it can
-- generate infinite data types.
data (:->) :: Type -> Type -> Type where
  Nil   :: a :-> b
  Unit  :: a -> () :-> a
  Table :: Ord a => Tree (a, Maybe b) -> a :-> b
  Sum   :: (a :-> c) -> (b :-> c) -> (Either a b :-> c)
  Prod  :: (a :-> (b :-> c)) -> (a, b) :-> c
  Map   :: (b -> a) -> (a -> b) -> (a :-> c) -> (b :-> c)

{-------------------------------------------------------------------------------
  Construction
-------------------------------------------------------------------------------}

instance Functor ((:->) a) where
  fmap :: forall a b. (a -> b) -> (a :-> a) -> a :-> b
fmap a -> b
_ a :-> a
Nil           = a :-> b
forall a b. a :-> b
Nil
  fmap a -> b
f (Unit a
x)      = b -> () :-> b
forall a. a -> () :-> a
Unit (a -> b
f a
x)
  fmap a -> b
f (Table Tree (a, Maybe a)
xs)    = Tree (a, Maybe b) -> a :-> b
forall a b. Ord a => Tree (a, Maybe b) -> a :-> b
Table (((a, Maybe a) -> (a, Maybe b))
-> Tree (a, Maybe a) -> Tree (a, Maybe b)
forall a b. (a -> b) -> Tree a -> Tree b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Maybe a -> Maybe b) -> (a, Maybe a) -> (a, Maybe b)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ((a -> b) -> Maybe a -> Maybe b
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f)) Tree (a, Maybe a)
xs)
  fmap a -> b
f (Sum a :-> a
x b :-> a
y)     = (a :-> b) -> (b :-> b) -> Either a b :-> b
forall a c b. (a :-> c) -> (b :-> c) -> Either a b :-> c
Sum ((a -> b) -> (a :-> a) -> a :-> b
forall a b. (a -> b) -> (a :-> a) -> a :-> b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f a :-> a
x) ((a -> b) -> (b :-> a) -> b :-> b
forall a b. (a -> b) -> (b :-> a) -> b :-> b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f b :-> a
y)
  fmap a -> b
f (Prod a :-> (b :-> a)
x)      = (a :-> (b :-> b)) -> (a, b) :-> b
forall a b c. (a :-> (b :-> c)) -> (a, b) :-> c
Prod (((b :-> a) -> b :-> b) -> (a :-> (b :-> a)) -> a :-> (b :-> b)
forall a b. (a -> b) -> (a :-> a) -> a :-> b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> b) -> (b :-> a) -> b :-> b
forall a b. (a -> b) -> (b :-> a) -> b :-> b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f) a :-> (b :-> a)
x)
  fmap a -> b
f (Map a -> a
ab a -> a
ba a :-> a
x) = (a -> a) -> (a -> a) -> (a :-> b) -> a :-> b
forall b a c. (b -> a) -> (a -> b) -> (a :-> c) -> b :-> c
Map a -> a
ab a -> a
ba ((a -> b) -> (a :-> a) -> a :-> b
forall a b. (a -> b) -> (a :-> a) -> a :-> b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f a :-> a
x)

-- | Change domain of concrete function
--
-- This is the basic building block for constructing new concrete functions.
map :: (b -> a) -> (a -> b) -> (a :-> c) -> b :-> c
map :: forall b a c. (b -> a) -> (a -> b) -> (a :-> c) -> b :-> c
map = (b -> a) -> (a -> b) -> (a :-> c) -> b :-> c
forall b a c. (b -> a) -> (a -> b) -> (a :-> c) -> b :-> c
Map

{-------------------------------------------------------------------------------
  Application
-------------------------------------------------------------------------------}

-- | Apply concrete function
apply :: (a :-> b) -> b -> (a -> b)
apply :: forall a b. (a :-> b) -> b -> a -> b
apply a :-> b
Nil         b
d a
_     = b
d
apply (Unit b
x)    b
_ a
_     = b
x
apply (Prod a :-> (b :-> b)
p)    b
d (a
x,b
y) = (a :-> b) -> b -> a -> b
forall a b. (a :-> b) -> b -> a -> b
apply (((b :-> b) -> b) -> (a :-> (b :-> b)) -> a :-> b
forall a b. (a -> b) -> (a :-> a) -> a :-> b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\b :-> b
q -> (b :-> b) -> b -> b -> b
forall a b. (a :-> b) -> b -> a -> b
apply b :-> b
q b
d b
y) a :-> (b :-> b)
p) b
d a
x
apply (Sum a :-> b
p b :-> b
q)   b
d a
exy   = (a -> b) -> (b -> b) -> Either a b -> b
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ((a :-> b) -> b -> a -> b
forall a b. (a :-> b) -> b -> a -> b
apply a :-> b
p b
d) ((b :-> b) -> b -> b -> b
forall a b. (a :-> b) -> b -> a -> b
apply b :-> b
q b
d) a
Either a b
exy
apply (Table Tree (a, Maybe b)
xys) b
d a
x     = b -> Maybe b -> b
forall a. a -> Maybe a -> a
fromMaybe b
d (Maybe b -> b)
-> (Maybe (Maybe b) -> Maybe b) -> Maybe (Maybe b) -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe (Maybe b) -> Maybe b
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Maybe (Maybe b) -> b) -> Maybe (Maybe b) -> b
forall a b. (a -> b) -> a -> b
$ a -> Tree (a, Maybe b) -> Maybe (Maybe b)
forall a b. Ord a => a -> Tree (a, b) -> Maybe b
Tree.lookup a
x Tree (a, Maybe b)
xys
apply (Map a -> a
g a -> a
_ a :-> b
p) b
d a
x     = (a :-> b) -> b -> a -> b
forall a b. (a :-> b) -> b -> a -> b
apply a :-> b
p b
d (a -> a
g a
x)

{-------------------------------------------------------------------------------
  Rendering
-------------------------------------------------------------------------------}

-- | Show concrete function
--
-- Only use this on finite functions!
render :: (Show a, Show b) => (a :-> b) -> b -> String
render :: forall a b. (Show a, Show b) => (a :-> b) -> b -> String
render a :-> b
p b
d = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [
      String
"{"
    , String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [
          [ a -> String
forall a. Show a => a -> String
show a
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"->" String -> String -> String
forall a. [a] -> [a] -> [a]
++ b -> String
forall a. Show a => a -> String
show b
c
          | (a
x,b
c) <- (a :-> b) -> [(a, b)]
forall a b. (a :-> b) -> [(a, b)]
toTable a :-> b
p
          ]
        , [String
"_->" String -> String -> String
forall a. [a] -> [a] -> [a]
++ b -> String
forall a. Show a => a -> String
show b
d]
        ]
    , String
"}"
    ]

{-------------------------------------------------------------------------------
  Internal auxiliary
-------------------------------------------------------------------------------}

-- | Generating a table from a concrete function
--
-- Used in 'render'.
toTable :: (a :-> b) -> [(a, b)]
toTable :: forall a b. (a :-> b) -> [(a, b)]
toTable a :-> b
Nil         = []
toTable (Unit b
x)    = [((), b
x)]
toTable (Prod a :-> (b :-> b)
p)    = [ ((a
x,b
y),b
c) | (a
x,b :-> b
q) <- (a :-> (b :-> b)) -> [(a, b :-> b)]
forall a b. (a :-> b) -> [(a, b)]
toTable a :-> (b :-> b)
p, (b
y,b
c) <- (b :-> b) -> [(b, b)]
forall a b. (a :-> b) -> [(a, b)]
toTable b :-> b
q ]
toTable (Sum a :-> b
p b :-> b
q)   = [ (a -> Either a b
forall a b. a -> Either a b
Left a
x, b
c) | (a
x,b
c) <- (a :-> b) -> [(a, b)]
forall a b. (a :-> b) -> [(a, b)]
toTable a :-> b
p ]
                   [(a, b)] -> [(a, b)] -> [(a, b)]
forall a. [a] -> [a] -> [a]
++ [ (b -> Either a b
forall a b. b -> Either a b
Right b
y,b
c) | (b
y,b
c) <- (b :-> b) -> [(b, b)]
forall a b. (a :-> b) -> [(a, b)]
toTable b :-> b
q ]
toTable (Table Tree (a, Maybe b)
xys) = ((a, Maybe b) -> Maybe (a, b)) -> [(a, Maybe b)] -> [(a, b)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\(a
a, Maybe b
b) -> (a
a,) (b -> (a, b)) -> Maybe b -> Maybe (a, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe b
b) ([(a, Maybe b)] -> [(a, b)]) -> [(a, Maybe b)] -> [(a, b)]
forall a b. (a -> b) -> a -> b
$ Tree (a, Maybe b) -> [(a, Maybe b)]
forall a. Tree a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Tree (a, Maybe b)
xys
toTable (Map a -> a
_ a -> a
h a :-> b
p) = [ (a -> a
h a
x, b
c) | (a
x,b
c) <- (a :-> b) -> [(a, b)]
forall a b. (a :-> b) -> [(a, b)]
toTable a :-> b
p ]