{-# LANGUAGE DeriveTraversable          #-}
{-# LANGUAGE DerivingStrategies         #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE OverloadedStrings          #-}
{-# LANGUAGE PatternSynonyms            #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Disco.Value
-- Copyright   :  disco team and contributors
-- Maintainer  :  byorgey@gmail.com
--
-- SPDX-License-Identifier: BSD-3-Clause
--
-- Disco runtime values and environments.
--
-----------------------------------------------------------------------------

module Disco.Value
  ( -- * Values

    Value(.., VNil, VCons, VFun)
  , SimpleValue(..)
  , toSimpleValue, fromSimpleValue

    -- ** Conversion

  , ratv, vrat
  , intv, vint
  , charv, vchar
  , enumv
  , pairv, vpair
  , listv, vlist

    -- * Props & testing
  , ValProp(..), TestResult(..), TestReason_(..), TestReason
  , SearchType(..), SearchMotive(.., SMExists, SMForall)
  , TestVars(..), TestEnv(..), emptyTestEnv, getTestEnv, extendPropEnv, extendResultEnv
  , testIsOk, testIsError, testReason, testEnv

  -- * Environments

  , Env

  -- * Memory
  , Cell(..), Mem, emptyMem, allocate, allocateRec, lkup, set

  -- * Pretty-printing

  , prettyValue', prettyValue, prettyTestFailure, prettyTestResult
  ) where

import           Prelude                          hiding ((<>))
import qualified Prelude                          as P

import           Control.Monad                    (forM)
import           Data.Bifunctor                   (first)
import           Data.Char                        (chr, ord, toLower)
import           Data.IntMap                      (IntMap)
import qualified Data.IntMap                      as IM
import           Data.List                        (foldl')
import           Data.Map                         (Map)
import qualified Data.Map                         as M
import           Data.Ratio

import           Algebra.Graph                    (Graph, foldg)

import           Disco.AST.Core
import           Disco.AST.Generic                (Side (..))
import           Disco.AST.Typed                  (AProperty)
import           Disco.Context                    as Ctx
import           Disco.Error
import           Disco.Names
import           Disco.Pretty
import           Disco.Syntax.Operators           (BOp (Add, Mul))
import           Disco.Typecheck.Erase            (eraseProperty)
import           Disco.Types

import           Disco.Effects.LFresh
import           Polysemy
import           Polysemy.Input
import           Polysemy.Reader
import           Polysemy.State
import           Unbound.Generics.LocallyNameless (Name)

------------------------------------------------------------
-- Value type
------------------------------------------------------------

-- | Different types of values which can result from the evaluation
--   process.
data Value where

  -- | A numeric value, which also carries a flag saying how
  --   fractional values should be diplayed.
  VNum     :: RationalDisplay -> Rational -> Value

  -- | A built-in function constant.
  VConst   :: Op -> Value

  -- | An injection into a sum type.
  VInj     :: Side -> Value -> Value

  -- | The unit value.
  VUnit    :: Value

  -- | A pair of values.
  VPair    :: Value -> Value -> Value

  -- | A closure, i.e. a function body together with its
  --   environment.
  VClo     :: Env -> [Name Core] -> Core -> Value

  -- | A disco type can be a value.  For now, there are only a very
  --   limited number of places this could ever show up (in
  --   particular, as an argument to @enumerate@ or @count@).
  VType    :: Type -> Value

  -- | A reference, i.e. a pointer to a memory cell.  This is used to
  --   implement (optional, user-requested) laziness as well as
  --   recursion.
  VRef     :: Int -> Value

  -- | A literal function value.  @VFun@ is only used when
  --   enumerating function values in order to decide comparisons at
  --   higher-order function types.  For example, in order to
  --   compare two values of type @(Bool -> Bool) -> Bool@ for
  --   equality, we have to enumerate all functions of type @Bool ->
  --   Bool@ as @VFun@ values.
  --
  --   We assume that all @VFun@ values are /strict/, that is, their
  --   arguments should be fully evaluated to RNF before being
  --   passed to the function.
  VFun_   :: ValFun -> Value

  -- | A proposition.
  VProp   :: ValProp -> Value

  -- | A literal bag, containing a finite list of (perhaps only
  --   partially evaluated) values, each paired with a count.  This is
  --   also used to represent sets (with the invariant that all counts
  --   are equal to 1).
  VBag :: [(Value, Integer)] -> Value

  -- | A graph, stored using an algebraic repesentation.
  VGraph :: Graph SimpleValue -> Value

  -- | A map from keys to values. Differs from functions because we can
  --   actually construct the set of entries, while functions only have this
  --   property when the key type is finite.
  VMap :: Map SimpleValue Value -> Value

  deriving Int -> Value -> ShowS
[Value] -> ShowS
Value -> String
(Int -> Value -> ShowS)
-> (Value -> String) -> ([Value] -> ShowS) -> Show Value
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Value] -> ShowS
$cshowList :: [Value] -> ShowS
show :: Value -> String
$cshow :: Value -> String
showsPrec :: Int -> Value -> ShowS
$cshowsPrec :: Int -> Value -> ShowS
Show

-- | Convenient pattern for the empty list.
pattern VNil :: Value
pattern $bVNil :: Value
$mVNil :: forall r. Value -> (Void# -> r) -> (Void# -> r) -> r
VNil      = VInj L VUnit

-- | Convenient pattern for list cons.
pattern VCons :: Value -> Value -> Value
pattern $bVCons :: Value -> Value -> Value
$mVCons :: forall r. Value -> (Value -> Value -> r) -> (Void# -> r) -> r
VCons h t = VInj R (VPair h t)

-- | Values which can be used as keys in a map, i.e. those for which a
--   Haskell Ord instance can be easily created.  These should always
--   be of a type for which the QSimple qualifier can be constructed.
--   At the moment these are always fully evaluated (containing no
--   indirections) and thus don't need memory management.  At some
--   point in the future constructors for simple graphs and simple
--   maps could be created, if the value type is also QSimple.  The
--   only reason for actually doing this would be constructing graphs
--   of graphs or maps of maps, or the like.
data SimpleValue where
  SNum   :: RationalDisplay -> Rational -> SimpleValue
  SUnit  :: SimpleValue
  SInj   :: Side -> SimpleValue -> SimpleValue
  SPair  :: SimpleValue -> SimpleValue -> SimpleValue
  SBag   :: [(SimpleValue, Integer)] -> SimpleValue
  SType  :: Type -> SimpleValue
  deriving (Int -> SimpleValue -> ShowS
[SimpleValue] -> ShowS
SimpleValue -> String
(Int -> SimpleValue -> ShowS)
-> (SimpleValue -> String)
-> ([SimpleValue] -> ShowS)
-> Show SimpleValue
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SimpleValue] -> ShowS
$cshowList :: [SimpleValue] -> ShowS
show :: SimpleValue -> String
$cshow :: SimpleValue -> String
showsPrec :: Int -> SimpleValue -> ShowS
$cshowsPrec :: Int -> SimpleValue -> ShowS
Show, SimpleValue -> SimpleValue -> Bool
(SimpleValue -> SimpleValue -> Bool)
-> (SimpleValue -> SimpleValue -> Bool) -> Eq SimpleValue
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SimpleValue -> SimpleValue -> Bool
$c/= :: SimpleValue -> SimpleValue -> Bool
== :: SimpleValue -> SimpleValue -> Bool
$c== :: SimpleValue -> SimpleValue -> Bool
Eq, Eq SimpleValue
Eq SimpleValue
-> (SimpleValue -> SimpleValue -> Ordering)
-> (SimpleValue -> SimpleValue -> Bool)
-> (SimpleValue -> SimpleValue -> Bool)
-> (SimpleValue -> SimpleValue -> Bool)
-> (SimpleValue -> SimpleValue -> Bool)
-> (SimpleValue -> SimpleValue -> SimpleValue)
-> (SimpleValue -> SimpleValue -> SimpleValue)
-> Ord SimpleValue
SimpleValue -> SimpleValue -> Bool
SimpleValue -> SimpleValue -> Ordering
SimpleValue -> SimpleValue -> SimpleValue
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: SimpleValue -> SimpleValue -> SimpleValue
$cmin :: SimpleValue -> SimpleValue -> SimpleValue
max :: SimpleValue -> SimpleValue -> SimpleValue
$cmax :: SimpleValue -> SimpleValue -> SimpleValue
>= :: SimpleValue -> SimpleValue -> Bool
$c>= :: SimpleValue -> SimpleValue -> Bool
> :: SimpleValue -> SimpleValue -> Bool
$c> :: SimpleValue -> SimpleValue -> Bool
<= :: SimpleValue -> SimpleValue -> Bool
$c<= :: SimpleValue -> SimpleValue -> Bool
< :: SimpleValue -> SimpleValue -> Bool
$c< :: SimpleValue -> SimpleValue -> Bool
compare :: SimpleValue -> SimpleValue -> Ordering
$ccompare :: SimpleValue -> SimpleValue -> Ordering
$cp1Ord :: Eq SimpleValue
Ord)

toSimpleValue :: Value -> SimpleValue
toSimpleValue :: Value -> SimpleValue
toSimpleValue = \case
  VNum RationalDisplay
d Rational
n    -> RationalDisplay -> Rational -> SimpleValue
SNum RationalDisplay
d Rational
n
  Value
VUnit       -> SimpleValue
SUnit
  VInj Side
s Value
v1   -> Side -> SimpleValue -> SimpleValue
SInj Side
s (Value -> SimpleValue
toSimpleValue Value
v1)
  VPair Value
v1 Value
v2 -> SimpleValue -> SimpleValue -> SimpleValue
SPair (Value -> SimpleValue
toSimpleValue Value
v1) (Value -> SimpleValue
toSimpleValue Value
v2)
  VBag [(Value, Integer)]
bs     -> [(SimpleValue, Integer)] -> SimpleValue
SBag (((Value, Integer) -> (SimpleValue, Integer))
-> [(Value, Integer)] -> [(SimpleValue, Integer)]
forall a b. (a -> b) -> [a] -> [b]
map ((Value -> SimpleValue)
-> (Value, Integer) -> (SimpleValue, Integer)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Value -> SimpleValue
toSimpleValue) [(Value, Integer)]
bs)
  VType Type
t     -> Type -> SimpleValue
SType Type
t
  Value
t           -> String -> SimpleValue
forall a. HasCallStack => String -> a
error (String -> SimpleValue) -> String -> SimpleValue
forall a b. (a -> b) -> a -> b
$ String
"A non-simple value was passed as simple: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
forall a. Show a => a -> String
show Value
t

fromSimpleValue :: SimpleValue -> Value
fromSimpleValue :: SimpleValue -> Value
fromSimpleValue (SNum RationalDisplay
d Rational
n)    = RationalDisplay -> Rational -> Value
VNum RationalDisplay
d Rational
n
fromSimpleValue SimpleValue
SUnit         = Value
VUnit
fromSimpleValue (SInj Side
s SimpleValue
v)    = Side -> Value -> Value
VInj Side
s (SimpleValue -> Value
fromSimpleValue SimpleValue
v)
fromSimpleValue (SPair SimpleValue
v1 SimpleValue
v2) = Value -> Value -> Value
VPair (SimpleValue -> Value
fromSimpleValue SimpleValue
v1) (SimpleValue -> Value
fromSimpleValue SimpleValue
v2)
fromSimpleValue (SBag [(SimpleValue, Integer)]
bs)     = [(Value, Integer)] -> Value
VBag ([(Value, Integer)] -> Value) -> [(Value, Integer)] -> Value
forall a b. (a -> b) -> a -> b
$ ((SimpleValue, Integer) -> (Value, Integer))
-> [(SimpleValue, Integer)] -> [(Value, Integer)]
forall a b. (a -> b) -> [a] -> [b]
map ((SimpleValue -> Value)
-> (SimpleValue, Integer) -> (Value, Integer)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first SimpleValue -> Value
fromSimpleValue) [(SimpleValue, Integer)]
bs
fromSimpleValue (SType Type
t)     = Type -> Value
VType Type
t

-- | A @ValFun@ is just a Haskell function @Value -> Value@.  It is a
--   @newtype@ just so we can have a custom @Show@ instance for it and
--   then derive a @Show@ instance for the rest of the @Value@ type.
newtype ValFun = ValFun (Value -> Value)

instance Show ValFun where
  show :: ValFun -> String
show ValFun
_ = String
"<fun>"

pattern VFun :: (Value -> Value) -> Value
pattern $bVFun :: (Value -> Value) -> Value
$mVFun :: forall r. Value -> ((Value -> Value) -> r) -> (Void# -> r) -> r
VFun f = VFun_ (ValFun f)

------------------------------------------------------------
-- Converting to and from Value
------------------------------------------------------------

-- XXX write some comments about partiality

-- | A convenience function for creating a default @VNum@ value with a
--   default (@Fractional@) flag.
ratv :: Rational -> Value
ratv :: Rational -> Value
ratv = RationalDisplay -> Rational -> Value
VNum RationalDisplay
forall a. Monoid a => a
mempty

vrat :: Value -> Rational
vrat :: Value -> Rational
vrat (VNum RationalDisplay
_ Rational
r) = Rational
r
vrat Value
v          = String -> Rational
forall a. HasCallStack => String -> a
error (String -> Rational) -> String -> Rational
forall a b. (a -> b) -> a -> b
$ String
"vrat " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
forall a. Show a => a -> String
show Value
v

-- | A convenience function for creating a default @VNum@ value with a
--   default (@Fractional@) flag.
intv :: Integer -> Value
intv :: Integer -> Value
intv = Rational -> Value
ratv (Rational -> Value) -> (Integer -> Rational) -> Integer -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
1)

vint :: Value -> Integer
vint :: Value -> Integer
vint (VNum RationalDisplay
_ Rational
n) = Rational -> Integer
forall a. Ratio a -> a
numerator Rational
n
vint Value
v          = String -> Integer
forall a. HasCallStack => String -> a
error (String -> Integer) -> String -> Integer
forall a b. (a -> b) -> a -> b
$ String
"vint " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
forall a. Show a => a -> String
show Value
v

vchar :: Value -> Char
vchar :: Value -> Char
vchar = Int -> Char
chr (Int -> Char) -> (Value -> Int) -> Value -> Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Int) -> (Value -> Integer) -> Value -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Integer
vint

charv :: Char -> Value
charv :: Char -> Value
charv = Integer -> Value
intv (Integer -> Value) -> (Char -> Integer) -> Char -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Integer) -> (Char -> Int) -> Char -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Int
ord

-- | Turn any instance of @Enum@ into a @Value@, by creating a
--   constructor with an index corresponding to the enum value.
enumv :: Enum e => e -> Value
enumv :: e -> Value
enumv e
e = Side -> Value -> Value
VInj (Int -> Side
forall a. Enum a => Int -> a
toEnum (Int -> Side) -> Int -> Side
forall a b. (a -> b) -> a -> b
$ e -> Int
forall a. Enum a => a -> Int
fromEnum e
e) Value
VUnit

pairv :: (a -> Value) -> (b -> Value) -> (a,b) -> Value
pairv :: (a -> Value) -> (b -> Value) -> (a, b) -> Value
pairv a -> Value
av b -> Value
bv (a
a,b
b) = Value -> Value -> Value
VPair (a -> Value
av a
a) (b -> Value
bv b
b)

vpair :: (Value -> a) -> (Value -> b) -> Value -> (a,b)
vpair :: (Value -> a) -> (Value -> b) -> Value -> (a, b)
vpair Value -> a
va Value -> b
vb (VPair Value
a Value
b) = (Value -> a
va Value
a, Value -> b
vb Value
b)
vpair Value -> a
_ Value -> b
_ Value
v             = String -> (a, b)
forall a. HasCallStack => String -> a
error (String -> (a, b)) -> String -> (a, b)
forall a b. (a -> b) -> a -> b
$ String
"vpair " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
forall a. Show a => a -> String
show Value
v

listv :: (a -> Value) -> [a] -> Value
listv :: (a -> Value) -> [a] -> Value
listv a -> Value
_ []        = Value
VNil
listv a -> Value
eltv (a
a:[a]
as) = Value -> Value -> Value
VCons (a -> Value
eltv a
a) ((a -> Value) -> [a] -> Value
forall a. (a -> Value) -> [a] -> Value
listv a -> Value
eltv [a]
as)

vlist :: (Value -> a) -> Value -> [a]
vlist :: (Value -> a) -> Value -> [a]
vlist Value -> a
_ Value
VNil            = []
vlist Value -> a
velt (VCons Value
v Value
vs) = Value -> a
velt Value
v a -> [a] -> [a]
forall a. a -> [a] -> [a]
: (Value -> a) -> Value -> [a]
forall a. (Value -> a) -> Value -> [a]
vlist Value -> a
velt Value
vs
vlist Value -> a
_ Value
v               = String -> [a]
forall a. HasCallStack => String -> a
error (String -> [a]) -> String -> [a]
forall a b. (a -> b) -> a -> b
$ String
"vlist " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
forall a. Show a => a -> String
show Value
v


------------------------------------------------------------
-- Propositions
------------------------------------------------------------

data SearchType
  = Exhaustive
    -- ^ All possibilities were checked.
  | Randomized Integer Integer
    -- ^ A number of small cases were checked exhaustively and
    --   then a number of additional cases were checked at random.
  deriving Int -> SearchType -> ShowS
[SearchType] -> ShowS
SearchType -> String
(Int -> SearchType -> ShowS)
-> (SearchType -> String)
-> ([SearchType] -> ShowS)
-> Show SearchType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SearchType] -> ShowS
$cshowList :: [SearchType] -> ShowS
show :: SearchType -> String
$cshow :: SearchType -> String
showsPrec :: Int -> SearchType -> ShowS
$cshowsPrec :: Int -> SearchType -> ShowS
Show

-- | The answer (success or failure) we're searching for, and
--   the result (success or failure) we return when we find it.
--   The motive @(False, False)@ corresponds to a "forall" quantifier
--   (look for a counterexample, fail if you find it) and the motive
--   @(True, True)@ corresponds to "exists". The other values
--   arise from negations.
newtype SearchMotive = SearchMotive (Bool, Bool)
  deriving Int -> SearchMotive -> ShowS
[SearchMotive] -> ShowS
SearchMotive -> String
(Int -> SearchMotive -> ShowS)
-> (SearchMotive -> String)
-> ([SearchMotive] -> ShowS)
-> Show SearchMotive
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SearchMotive] -> ShowS
$cshowList :: [SearchMotive] -> ShowS
show :: SearchMotive -> String
$cshow :: SearchMotive -> String
showsPrec :: Int -> SearchMotive -> ShowS
$cshowsPrec :: Int -> SearchMotive -> ShowS
Show

pattern SMForall :: SearchMotive
pattern $bSMForall :: SearchMotive
$mSMForall :: forall r. SearchMotive -> (Void# -> r) -> (Void# -> r) -> r
SMForall = SearchMotive (False, False)

pattern SMExists :: SearchMotive
pattern $bSMExists :: SearchMotive
$mSMExists :: forall r. SearchMotive -> (Void# -> r) -> (Void# -> r) -> r
SMExists = SearchMotive (True, True)

-- | A collection of variables that might need to be reported for
--   a test, along with their types and user-legible names.
newtype TestVars = TestVars [(String, Type, Name Core)]
  deriving newtype (Int -> TestVars -> ShowS
[TestVars] -> ShowS
TestVars -> String
(Int -> TestVars -> ShowS)
-> (TestVars -> String) -> ([TestVars] -> ShowS) -> Show TestVars
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TestVars] -> ShowS
$cshowList :: [TestVars] -> ShowS
show :: TestVars -> String
$cshow :: TestVars -> String
showsPrec :: Int -> TestVars -> ShowS
$cshowsPrec :: Int -> TestVars -> ShowS
Show, b -> TestVars -> TestVars
NonEmpty TestVars -> TestVars
TestVars -> TestVars -> TestVars
(TestVars -> TestVars -> TestVars)
-> (NonEmpty TestVars -> TestVars)
-> (forall b. Integral b => b -> TestVars -> TestVars)
-> Semigroup TestVars
forall b. Integral b => b -> TestVars -> TestVars
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
stimes :: b -> TestVars -> TestVars
$cstimes :: forall b. Integral b => b -> TestVars -> TestVars
sconcat :: NonEmpty TestVars -> TestVars
$csconcat :: NonEmpty TestVars -> TestVars
<> :: TestVars -> TestVars -> TestVars
$c<> :: TestVars -> TestVars -> TestVars
Semigroup, Semigroup TestVars
TestVars
Semigroup TestVars
-> TestVars
-> (TestVars -> TestVars -> TestVars)
-> ([TestVars] -> TestVars)
-> Monoid TestVars
[TestVars] -> TestVars
TestVars -> TestVars -> TestVars
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
mconcat :: [TestVars] -> TestVars
$cmconcat :: [TestVars] -> TestVars
mappend :: TestVars -> TestVars -> TestVars
$cmappend :: TestVars -> TestVars -> TestVars
mempty :: TestVars
$cmempty :: TestVars
$cp1Monoid :: Semigroup TestVars
Monoid)

-- | A variable assignment found during a test.
newtype TestEnv = TestEnv [(String, Type, Value)]
  deriving newtype (Int -> TestEnv -> ShowS
[TestEnv] -> ShowS
TestEnv -> String
(Int -> TestEnv -> ShowS)
-> (TestEnv -> String) -> ([TestEnv] -> ShowS) -> Show TestEnv
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TestEnv] -> ShowS
$cshowList :: [TestEnv] -> ShowS
show :: TestEnv -> String
$cshow :: TestEnv -> String
showsPrec :: Int -> TestEnv -> ShowS
$cshowsPrec :: Int -> TestEnv -> ShowS
Show, b -> TestEnv -> TestEnv
NonEmpty TestEnv -> TestEnv
TestEnv -> TestEnv -> TestEnv
(TestEnv -> TestEnv -> TestEnv)
-> (NonEmpty TestEnv -> TestEnv)
-> (forall b. Integral b => b -> TestEnv -> TestEnv)
-> Semigroup TestEnv
forall b. Integral b => b -> TestEnv -> TestEnv
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
stimes :: b -> TestEnv -> TestEnv
$cstimes :: forall b. Integral b => b -> TestEnv -> TestEnv
sconcat :: NonEmpty TestEnv -> TestEnv
$csconcat :: NonEmpty TestEnv -> TestEnv
<> :: TestEnv -> TestEnv -> TestEnv
$c<> :: TestEnv -> TestEnv -> TestEnv
Semigroup, Semigroup TestEnv
TestEnv
Semigroup TestEnv
-> TestEnv
-> (TestEnv -> TestEnv -> TestEnv)
-> ([TestEnv] -> TestEnv)
-> Monoid TestEnv
[TestEnv] -> TestEnv
TestEnv -> TestEnv -> TestEnv
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
mconcat :: [TestEnv] -> TestEnv
$cmconcat :: [TestEnv] -> TestEnv
mappend :: TestEnv -> TestEnv -> TestEnv
$cmappend :: TestEnv -> TestEnv -> TestEnv
mempty :: TestEnv
$cmempty :: TestEnv
$cp1Monoid :: Semigroup TestEnv
Monoid)

emptyTestEnv :: TestEnv
emptyTestEnv :: TestEnv
emptyTestEnv = [(String, Type, Value)] -> TestEnv
TestEnv []

getTestEnv :: TestVars -> Env -> Either EvalError TestEnv
getTestEnv :: TestVars -> Env -> Either EvalError TestEnv
getTestEnv (TestVars [(String, Type, Name Core)]
tvs) Env
e = ([(String, Type, Value)] -> TestEnv)
-> Either EvalError [(String, Type, Value)]
-> Either EvalError TestEnv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(String, Type, Value)] -> TestEnv
TestEnv (Either EvalError [(String, Type, Value)]
 -> Either EvalError TestEnv)
-> (((String, Type, Name Core)
     -> Either EvalError (String, Type, Value))
    -> Either EvalError [(String, Type, Value)])
-> ((String, Type, Name Core)
    -> Either EvalError (String, Type, Value))
-> Either EvalError TestEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(String, Type, Name Core)]
-> ((String, Type, Name Core)
    -> Either EvalError (String, Type, Value))
-> Either EvalError [(String, Type, Value)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(String, Type, Name Core)]
tvs (((String, Type, Name Core)
  -> Either EvalError (String, Type, Value))
 -> Either EvalError TestEnv)
-> ((String, Type, Name Core)
    -> Either EvalError (String, Type, Value))
-> Either EvalError TestEnv
forall a b. (a -> b) -> a -> b
$ \(String
s, Type
ty, Name Core
name) -> do
  let value :: Maybe Value
value = QName Core -> Env -> Maybe Value
forall a b. QName a -> Ctx a b -> Maybe b
Ctx.lookup' (Name Core -> QName Core
forall a. Name a -> QName a
localName Name Core
name) Env
e
  case Maybe Value
value of
    Just Value
v  -> (String, Type, Value) -> Either EvalError (String, Type, Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (String
s, Type
ty, Value
v)
    Maybe Value
Nothing -> EvalError -> Either EvalError (String, Type, Value)
forall a b. a -> Either a b
Left (Name Core -> EvalError
forall core. Name core -> EvalError
UnboundError Name Core
name)

-- | The possible outcomes of a property test, parametrized over
--   the type of values. A @TestReason@ explains why a proposition
--   succeeded or failed.
data TestReason_ a
  = TestBool
    -- ^ The prop evaluated to a boolean.
  | TestEqual Type a a
    -- ^ The test was an equality test. Records the values being
    --   compared and also their type (which is needed for printing).
  | TestNotFound SearchType
    -- ^ The search didn't find any examples/counterexamples.
  | TestFound TestResult
    -- ^ The search found an example/counterexample.
  | TestRuntimeError EvalError
    -- ^ The prop failed at runtime. This is always a failure, no
    --   matter which quantifiers or negations it's under.
  deriving (Int -> TestReason_ a -> ShowS
[TestReason_ a] -> ShowS
TestReason_ a -> String
(Int -> TestReason_ a -> ShowS)
-> (TestReason_ a -> String)
-> ([TestReason_ a] -> ShowS)
-> Show (TestReason_ a)
forall a. Show a => Int -> TestReason_ a -> ShowS
forall a. Show a => [TestReason_ a] -> ShowS
forall a. Show a => TestReason_ a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TestReason_ a] -> ShowS
$cshowList :: forall a. Show a => [TestReason_ a] -> ShowS
show :: TestReason_ a -> String
$cshow :: forall a. Show a => TestReason_ a -> String
showsPrec :: Int -> TestReason_ a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> TestReason_ a -> ShowS
Show, a -> TestReason_ b -> TestReason_ a
(a -> b) -> TestReason_ a -> TestReason_ b
(forall a b. (a -> b) -> TestReason_ a -> TestReason_ b)
-> (forall a b. a -> TestReason_ b -> TestReason_ a)
-> Functor TestReason_
forall a b. a -> TestReason_ b -> TestReason_ a
forall a b. (a -> b) -> TestReason_ a -> TestReason_ b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> TestReason_ b -> TestReason_ a
$c<$ :: forall a b. a -> TestReason_ b -> TestReason_ a
fmap :: (a -> b) -> TestReason_ a -> TestReason_ b
$cfmap :: forall a b. (a -> b) -> TestReason_ a -> TestReason_ b
Functor, TestReason_ a -> Bool
(a -> m) -> TestReason_ a -> m
(a -> b -> b) -> b -> TestReason_ a -> b
(forall m. Monoid m => TestReason_ m -> m)
-> (forall m a. Monoid m => (a -> m) -> TestReason_ a -> m)
-> (forall m a. Monoid m => (a -> m) -> TestReason_ a -> m)
-> (forall a b. (a -> b -> b) -> b -> TestReason_ a -> b)
-> (forall a b. (a -> b -> b) -> b -> TestReason_ a -> b)
-> (forall b a. (b -> a -> b) -> b -> TestReason_ a -> b)
-> (forall b a. (b -> a -> b) -> b -> TestReason_ a -> b)
-> (forall a. (a -> a -> a) -> TestReason_ a -> a)
-> (forall a. (a -> a -> a) -> TestReason_ a -> a)
-> (forall a. TestReason_ a -> [a])
-> (forall a. TestReason_ a -> Bool)
-> (forall a. TestReason_ a -> Int)
-> (forall a. Eq a => a -> TestReason_ a -> Bool)
-> (forall a. Ord a => TestReason_ a -> a)
-> (forall a. Ord a => TestReason_ a -> a)
-> (forall a. Num a => TestReason_ a -> a)
-> (forall a. Num a => TestReason_ a -> a)
-> Foldable TestReason_
forall a. Eq a => a -> TestReason_ a -> Bool
forall a. Num a => TestReason_ a -> a
forall a. Ord a => TestReason_ a -> a
forall m. Monoid m => TestReason_ m -> m
forall a. TestReason_ a -> Bool
forall a. TestReason_ a -> Int
forall a. TestReason_ a -> [a]
forall a. (a -> a -> a) -> TestReason_ a -> a
forall m a. Monoid m => (a -> m) -> TestReason_ a -> m
forall b a. (b -> a -> b) -> b -> TestReason_ a -> b
forall a b. (a -> b -> b) -> b -> TestReason_ a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: TestReason_ a -> a
$cproduct :: forall a. Num a => TestReason_ a -> a
sum :: TestReason_ a -> a
$csum :: forall a. Num a => TestReason_ a -> a
minimum :: TestReason_ a -> a
$cminimum :: forall a. Ord a => TestReason_ a -> a
maximum :: TestReason_ a -> a
$cmaximum :: forall a. Ord a => TestReason_ a -> a
elem :: a -> TestReason_ a -> Bool
$celem :: forall a. Eq a => a -> TestReason_ a -> Bool
length :: TestReason_ a -> Int
$clength :: forall a. TestReason_ a -> Int
null :: TestReason_ a -> Bool
$cnull :: forall a. TestReason_ a -> Bool
toList :: TestReason_ a -> [a]
$ctoList :: forall a. TestReason_ a -> [a]
foldl1 :: (a -> a -> a) -> TestReason_ a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> TestReason_ a -> a
foldr1 :: (a -> a -> a) -> TestReason_ a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> TestReason_ a -> a
foldl' :: (b -> a -> b) -> b -> TestReason_ a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> TestReason_ a -> b
foldl :: (b -> a -> b) -> b -> TestReason_ a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> TestReason_ a -> b
foldr' :: (a -> b -> b) -> b -> TestReason_ a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> TestReason_ a -> b
foldr :: (a -> b -> b) -> b -> TestReason_ a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> TestReason_ a -> b
foldMap' :: (a -> m) -> TestReason_ a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> TestReason_ a -> m
foldMap :: (a -> m) -> TestReason_ a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> TestReason_ a -> m
fold :: TestReason_ m -> m
$cfold :: forall m. Monoid m => TestReason_ m -> m
Foldable, Functor TestReason_
Foldable TestReason_
Functor TestReason_
-> Foldable TestReason_
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> TestReason_ a -> f (TestReason_ b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    TestReason_ (f a) -> f (TestReason_ a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> TestReason_ a -> m (TestReason_ b))
-> (forall (m :: * -> *) a.
    Monad m =>
    TestReason_ (m a) -> m (TestReason_ a))
-> Traversable TestReason_
(a -> f b) -> TestReason_ a -> f (TestReason_ b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
TestReason_ (m a) -> m (TestReason_ a)
forall (f :: * -> *) a.
Applicative f =>
TestReason_ (f a) -> f (TestReason_ a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TestReason_ a -> m (TestReason_ b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TestReason_ a -> f (TestReason_ b)
sequence :: TestReason_ (m a) -> m (TestReason_ a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
TestReason_ (m a) -> m (TestReason_ a)
mapM :: (a -> m b) -> TestReason_ a -> m (TestReason_ b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TestReason_ a -> m (TestReason_ b)
sequenceA :: TestReason_ (f a) -> f (TestReason_ a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
TestReason_ (f a) -> f (TestReason_ a)
traverse :: (a -> f b) -> TestReason_ a -> f (TestReason_ b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TestReason_ a -> f (TestReason_ b)
$cp2Traversable :: Foldable TestReason_
$cp1Traversable :: Functor TestReason_
Traversable)

type TestReason = TestReason_ Value

-- | The possible outcomes of a proposition.
data TestResult = TestResult Bool TestReason TestEnv
  deriving Int -> TestResult -> ShowS
[TestResult] -> ShowS
TestResult -> String
(Int -> TestResult -> ShowS)
-> (TestResult -> String)
-> ([TestResult] -> ShowS)
-> Show TestResult
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TestResult] -> ShowS
$cshowList :: [TestResult] -> ShowS
show :: TestResult -> String
$cshow :: TestResult -> String
showsPrec :: Int -> TestResult -> ShowS
$cshowsPrec :: Int -> TestResult -> ShowS
Show

-- | Whether the property test resulted in a runtime error.
testIsError :: TestResult -> Bool
testIsError :: TestResult -> Bool
testIsError (TestResult Bool
_ (TestRuntimeError EvalError
_) TestEnv
_) = Bool
True
testIsError TestResult
_                                     = Bool
False

-- | Whether the property test resulted in success.
testIsOk :: TestResult -> Bool
testIsOk :: TestResult -> Bool
testIsOk (TestResult Bool
b TestReason_ Value
_ TestEnv
_) = Bool
b

-- | The reason the property test had this result.
testReason :: TestResult -> TestReason
testReason :: TestResult -> TestReason_ Value
testReason (TestResult Bool
_ TestReason_ Value
r TestEnv
_) = TestReason_ Value
r

testEnv :: TestResult -> TestEnv
testEnv :: TestResult -> TestEnv
testEnv (TestResult Bool
_ TestReason_ Value
_ TestEnv
e) = TestEnv
e

-- | A @ValProp@ is the normal form of a Disco value of type @Prop@.
data ValProp
  = VPDone TestResult
    -- ^ A prop that has already either succeeded or failed.
  | VPSearch SearchMotive [Type] Value TestEnv
    -- ^ A pending search.
  deriving Int -> ValProp -> ShowS
[ValProp] -> ShowS
ValProp -> String
(Int -> ValProp -> ShowS)
-> (ValProp -> String) -> ([ValProp] -> ShowS) -> Show ValProp
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ValProp] -> ShowS
$cshowList :: [ValProp] -> ShowS
show :: ValProp -> String
$cshow :: ValProp -> String
showsPrec :: Int -> ValProp -> ShowS
$cshowsPrec :: Int -> ValProp -> ShowS
Show

extendPropEnv :: TestEnv -> ValProp -> ValProp
extendPropEnv :: TestEnv -> ValProp -> ValProp
extendPropEnv TestEnv
g (VPDone (TestResult Bool
b TestReason_ Value
r TestEnv
e)) = TestResult -> ValProp
VPDone (Bool -> TestReason_ Value -> TestEnv -> TestResult
TestResult Bool
b TestReason_ Value
r (TestEnv
g TestEnv -> TestEnv -> TestEnv
forall a. Semigroup a => a -> a -> a
P.<> TestEnv
e))
extendPropEnv TestEnv
g (VPSearch SearchMotive
sm [Type]
tys Value
v TestEnv
e)       = SearchMotive -> [Type] -> Value -> TestEnv -> ValProp
VPSearch SearchMotive
sm [Type]
tys Value
v (TestEnv
g TestEnv -> TestEnv -> TestEnv
forall a. Semigroup a => a -> a -> a
P.<> TestEnv
e)

extendResultEnv :: TestEnv -> TestResult -> TestResult
extendResultEnv :: TestEnv -> TestResult -> TestResult
extendResultEnv TestEnv
g (TestResult Bool
b TestReason_ Value
r TestEnv
e) = Bool -> TestReason_ Value -> TestEnv -> TestResult
TestResult Bool
b TestReason_ Value
r (TestEnv
g TestEnv -> TestEnv -> TestEnv
forall a. Semigroup a => a -> a -> a
P.<> TestEnv
e)

------------------------------------------------------------
-- Environments
------------------------------------------------------------

-- | An environment is a mapping from names to values.
type Env  = Ctx Core Value

------------------------------------------------------------
-- Memory
------------------------------------------------------------

-- | 'Mem' represents a memory, containing 'Cell's
data Mem = Mem { Mem -> Int
next :: Int, Mem -> IntMap Cell
mu :: IntMap Cell } deriving Int -> Mem -> ShowS
[Mem] -> ShowS
Mem -> String
(Int -> Mem -> ShowS)
-> (Mem -> String) -> ([Mem] -> ShowS) -> Show Mem
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Mem] -> ShowS
$cshowList :: [Mem] -> ShowS
show :: Mem -> String
$cshow :: Mem -> String
showsPrec :: Int -> Mem -> ShowS
$cshowsPrec :: Int -> Mem -> ShowS
Show
data Cell = Blackhole | E Env Core | V Value deriving Int -> Cell -> ShowS
[Cell] -> ShowS
Cell -> String
(Int -> Cell -> ShowS)
-> (Cell -> String) -> ([Cell] -> ShowS) -> Show Cell
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Cell] -> ShowS
$cshowList :: [Cell] -> ShowS
show :: Cell -> String
$cshow :: Cell -> String
showsPrec :: Int -> Cell -> ShowS
$cshowsPrec :: Int -> Cell -> ShowS
Show

emptyMem :: Mem
emptyMem :: Mem
emptyMem = Int -> IntMap Cell -> Mem
Mem Int
0 IntMap Cell
forall a. IntMap a
IM.empty

-- | Allocate a new memory cell containing an unevaluated expression
--   with the current environment.  Return the index of the allocated
--   cell.
allocate :: Members '[State Mem] r => Env -> Core -> Sem r Int
allocate :: Env -> Core -> Sem r Int
allocate Env
e Core
t = do
  Mem Int
n IntMap Cell
m <- Sem r Mem
forall s (r :: EffectRow). Member (State s) r => Sem r s
get
  Mem -> Sem r ()
forall s (r :: EffectRow). Member (State s) r => s -> Sem r ()
put (Mem -> Sem r ()) -> Mem -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Int -> IntMap Cell -> Mem
Mem (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (Int -> Cell -> IntMap Cell -> IntMap Cell
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
n (Env -> Core -> Cell
E Env
e Core
t) IntMap Cell
m)
  Int -> Sem r Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
n

-- | Allocate new memory cells for a group of mutually recursive
--   bindings, and return the indices of the allocate cells.
allocateRec :: Members '[State Mem] r => Env -> [(QName Core, Core)] -> Sem r [Int]
allocateRec :: Env -> [(QName Core, Core)] -> Sem r [Int]
allocateRec Env
e [(QName Core, Core)]
bs = do
  Mem Int
n IntMap Cell
m <- Sem r Mem
forall s (r :: EffectRow). Member (State s) r => Sem r s
get
  let newRefs :: [(Int, (QName Core, Core))]
newRefs = [Int] -> [(QName Core, Core)] -> [(Int, (QName Core, Core))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
n ..] [(QName Core, Core)]
bs
      e' :: Env
e' = (Env -> (Int, (QName Core, Core)) -> Env)
-> Env -> [(Int, (QName Core, Core))] -> Env
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (((Int, (QName Core, Core)) -> Env -> Env)
-> Env -> (Int, (QName Core, Core)) -> Env
forall a b c. (a -> b -> c) -> b -> a -> c
flip (\(Int
i,(QName Core
x,Core
_)) -> QName Core -> Value -> Env -> Env
forall a b. QName a -> b -> Ctx a b -> Ctx a b
Ctx.insert QName Core
x (Int -> Value
VRef Int
i))) Env
e [(Int, (QName Core, Core))]
newRefs
      m' :: IntMap Cell
m' = (IntMap Cell -> (Int, (QName Core, Core)) -> IntMap Cell)
-> IntMap Cell -> [(Int, (QName Core, Core))] -> IntMap Cell
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (((Int, (QName Core, Core)) -> IntMap Cell -> IntMap Cell)
-> IntMap Cell -> (Int, (QName Core, Core)) -> IntMap Cell
forall a b c. (a -> b -> c) -> b -> a -> c
flip (\(Int
i,(QName Core
_,Core
c)) -> Int -> Cell -> IntMap Cell -> IntMap Cell
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
i (Env -> Core -> Cell
E Env
e' Core
c))) IntMap Cell
m [(Int, (QName Core, Core))]
newRefs
      n' :: Int
n' = Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [(QName Core, Core)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(QName Core, Core)]
bs
  Mem -> Sem r ()
forall s (r :: EffectRow). Member (State s) r => s -> Sem r ()
put (Mem -> Sem r ()) -> Mem -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Int -> IntMap Cell -> Mem
Mem Int
n' IntMap Cell
m'
  [Int] -> Sem r [Int]
forall (m :: * -> *) a. Monad m => a -> m a
return [Int
n .. Int
n'Int -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1]

-- | Look up the cell at a given index.
lkup :: Members '[State Mem] r => Int -> Sem r (Maybe Cell)
lkup :: Int -> Sem r (Maybe Cell)
lkup Int
n = (Mem -> Maybe Cell) -> Sem r (Maybe Cell)
forall s a (r :: EffectRow).
Member (State s) r =>
(s -> a) -> Sem r a
gets (Int -> IntMap Cell -> Maybe Cell
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
n (IntMap Cell -> Maybe Cell)
-> (Mem -> IntMap Cell) -> Mem -> Maybe Cell
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mem -> IntMap Cell
mu)

-- | Set the cell at a given index.
set :: Members '[State Mem] r => Int -> Cell -> Sem r ()
set :: Int -> Cell -> Sem r ()
set Int
n Cell
c = (Mem -> Mem) -> Sem r ()
forall s (r :: EffectRow).
Member (State s) r =>
(s -> s) -> Sem r ()
modify ((Mem -> Mem) -> Sem r ()) -> (Mem -> Mem) -> Sem r ()
forall a b. (a -> b) -> a -> b
$ \(Mem Int
nxt IntMap Cell
m) -> Int -> IntMap Cell -> Mem
Mem Int
nxt (Int -> Cell -> IntMap Cell -> IntMap Cell
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
n Cell
c IntMap Cell
m)

------------------------------------------------------------
-- Pretty-printing values
------------------------------------------------------------

prettyValue' :: Member (Input TyDefCtx) r => Type -> Value -> Sem r Doc
prettyValue' :: Type -> Value -> Sem r Doc
prettyValue' Type
ty Value
v = Sem (LFresh : r) Doc -> Sem r Doc
forall (r :: EffectRow) a. Sem (LFresh : r) a -> Sem r a
runLFresh (Sem (LFresh : r) Doc -> Sem r Doc)
-> (Sem (Reader PA : LFresh : r) Doc -> Sem (LFresh : r) Doc)
-> Sem (Reader PA : LFresh : r) Doc
-> Sem r Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PA -> Sem (Reader PA : LFresh : r) Doc -> Sem (LFresh : r) Doc
forall i (r :: EffectRow) a. i -> Sem (Reader i : r) a -> Sem r a
runReader PA
initPA (Sem (Reader PA : LFresh : r) Doc -> Sem r Doc)
-> Sem (Reader PA : LFresh : r) Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ Type -> Value -> Sem (Reader PA : LFresh : r) Doc
forall (r :: EffectRow).
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r Doc
prettyValue Type
ty Value
v

prettyValue :: Members '[Input TyDefCtx, LFresh, Reader PA] r => Type -> Value -> Sem r Doc

-- Lazily expand any user-defined types
prettyValue :: Type -> Value -> Sem r Doc
prettyValue (TyUser String
x [Type]
args) Value
v = do
  TyDefCtx
tydefs <- Sem r TyDefCtx
forall i (r :: EffectRow). Member (Input i) r => Sem r i
input
  let (TyDefBody [String]
_ [Type] -> Type
body) = TyDefCtx
tydefs TyDefCtx -> String -> TyDefBody
forall k a. Ord k => Map k a -> k -> a
M.! String
x   -- This can't fail if typechecking succeeded
  Type -> Value -> Sem r Doc
forall (r :: EffectRow).
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r Doc
prettyValue ([Type] -> Type
body [Type]
args) Value
v

prettyValue Type
_      Value
VUnit                     = Sem r Doc
"■"
prettyValue Type
TyProp Value
_                         = Type -> Sem r Doc
forall (r :: EffectRow).
Members '[Reader PA, LFresh] r =>
Type -> Sem r Doc
prettyPlaceholder Type
TyProp
prettyValue Type
TyBool (VInj Side
s Value
_)                = String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> Sem r Doc) -> String -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ (Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (Bool -> String
forall a. Show a => a -> String
show (Side
s Side -> Side -> Bool
forall a. Eq a => a -> a -> Bool
== Side
R))
prettyValue Type
TyBool Value
v =
  String -> Sem r Doc
forall a. HasCallStack => String -> a
error (String -> Sem r Doc) -> String -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ String
"Non-VInj passed with Bool type to prettyValue: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
forall a. Show a => a -> String
show Value
v
prettyValue Type
TyC (Value -> Char
vchar -> Char
c)                 = String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Char -> String
forall a. Show a => a -> String
show Char
c)
prettyValue (TyList Type
TyC) ((Value -> Char) -> Value -> String
forall a. (Value -> a) -> Value -> [a]
vlist Value -> Char
vchar -> String
cs) = Sem r Doc -> Sem r Doc
forall (f :: * -> *). Functor f => f Doc -> f Doc
doubleQuotes (Sem r Doc -> Sem r Doc)
-> (String -> Sem r Doc) -> String -> Sem r Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> Sem r Doc) -> ShowS -> String -> Sem r Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> String) -> ShowS
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Char -> String
prettyChar (String -> Sem r Doc) -> String -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ String
cs
  where
    prettyChar :: Char -> String
prettyChar = Int -> ShowS
forall a. Int -> [a] -> [a]
drop Int
1 ShowS -> (Char -> String) -> Char -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
forall a. [a] -> [a]
reverse ShowS -> (Char -> String) -> Char -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ShowS
forall a. Int -> [a] -> [a]
drop Int
1 ShowS -> (Char -> String) -> Char -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
forall a. [a] -> [a]
reverse ShowS -> (Char -> String) -> Char -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
forall a. Show a => a -> String
show ShowS -> (Char -> String) -> Char -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> ShowS
forall a. a -> [a] -> [a]
:[])
prettyValue (TyList Type
ty) ((Value -> Value) -> Value -> [Value]
forall a. (Value -> a) -> Value -> [a]
vlist Value -> Value
forall a. a -> a
id -> [Value]
xs)     = do
  [Sem r Doc]
ds <- Sem r Doc -> [Sem r Doc] -> Sem r [Sem r Doc]
forall (f :: * -> *).
Applicative f =>
f Doc -> [f Doc] -> f [f Doc]
punctuate (String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
",") ((Value -> Sem r Doc) -> [Value] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Type -> Value -> Sem r Doc
forall (r :: EffectRow).
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r Doc
prettyValue Type
ty) [Value]
xs)
  Sem r Doc -> Sem r Doc
forall (f :: * -> *). Functor f => f Doc -> f Doc
brackets ([Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep [Sem r Doc]
ds)

prettyValue ty :: Type
ty@(Type
_ :*: Type
_) Value
v                   = Sem r Doc -> Sem r Doc
forall (f :: * -> *). Functor f => f Doc -> f Doc
parens (Type -> Value -> Sem r Doc
forall (r :: EffectRow).
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r Doc
prettyTuple Type
ty Value
v)

prettyValue (Type
ty1 :+: Type
_) (VInj Side
L Value
v)           = Sem r Doc
"left"  Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> Type -> Value -> Sem r Doc
forall (r :: EffectRow).
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r Doc
prettyVP Type
ty1 Value
v
prettyValue (Type
_ :+: Type
ty2) (VInj Side
R Value
v)           = Sem r Doc
"right" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> Type -> Value -> Sem r Doc
forall (r :: EffectRow).
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r Doc
prettyVP Type
ty2 Value
v
prettyValue (Type
_ :+: Type
_) Value
v =
  String -> Sem r Doc
forall a. HasCallStack => String -> a
error (String -> Sem r Doc) -> String -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ String
"Non-VInj passed with sum type to prettyValue: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
forall a. Show a => a -> String
show Value
v

prettyValue Type
_ (VNum RationalDisplay
d Rational
r)
  | Rational -> Integer
forall a. Ratio a -> a
denominator Rational
r Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1                       = String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> Sem r Doc) -> String -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ Integer -> String
forall a. Show a => a -> String
show (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
r)
  | Bool
otherwise                                = String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> Sem r Doc) -> String -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ case RationalDisplay
d of
      RationalDisplay
Fraction -> Integer -> String
forall a. Show a => a -> String
show (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
r) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"/" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (Rational -> Integer
forall a. Ratio a -> a
denominator Rational
r)
      RationalDisplay
Decimal  -> Rational -> String
prettyDecimal Rational
r

prettyValue ty :: Type
ty@(Type
_ :->: Type
_) Value
_                  = Type -> Sem r Doc
forall (r :: EffectRow).
Members '[Reader PA, LFresh] r =>
Type -> Sem r Doc
prettyPlaceholder Type
ty

prettyValue (TySet Type
ty) (VBag [(Value, Integer)]
xs)             = Sem r Doc -> Sem r Doc
forall (f :: * -> *). Functor f => f Doc -> f Doc
braces (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ Type -> Doc -> [Value] -> Sem r Doc
forall (r :: EffectRow).
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Doc -> [Value] -> Sem r Doc
prettySequence Type
ty Doc
"," (((Value, Integer) -> Value) -> [(Value, Integer)] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map (Value, Integer) -> Value
forall a b. (a, b) -> a
fst [(Value, Integer)]
xs)
prettyValue (TySet Type
_) Value
v =
  String -> Sem r Doc
forall a. HasCallStack => String -> a
error (String -> Sem r Doc) -> String -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ String
"Non-VBag passed with Set type to prettyValue: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
forall a. Show a => a -> String
show Value
v
prettyValue (TyBag Type
ty) (VBag [(Value, Integer)]
xs)             = Type -> [(Value, Integer)] -> Sem r Doc
forall (r :: EffectRow).
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> [(Value, Integer)] -> Sem r Doc
prettyBag Type
ty [(Value, Integer)]
xs
prettyValue (TyBag Type
_) Value
v =
  String -> Sem r Doc
forall a. HasCallStack => String -> a
error (String -> Sem r Doc) -> String -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ String
"Non-VBag passed with Bag type to prettyValue: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
forall a. Show a => a -> String
show Value
v

prettyValue (TyMap Type
tyK Type
tyV) (VMap Map SimpleValue Value
m)         =
  Sem r Doc
"map" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Functor f => f Doc -> f Doc
parens (Sem r Doc -> Sem r Doc
forall (f :: * -> *). Functor f => f Doc -> f Doc
braces (Type -> Doc -> [Value] -> Sem r Doc
forall (r :: EffectRow).
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Doc -> [Value] -> Sem r Doc
prettySequence (Type
tyK Type -> Type -> Type
:*: Type
tyV) Doc
"," (Map SimpleValue Value -> [Value]
assocsToValues Map SimpleValue Value
m)))
  where
    assocsToValues :: Map SimpleValue Value -> [Value]
assocsToValues = ((SimpleValue, Value) -> Value)
-> [(SimpleValue, Value)] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map (\(SimpleValue
k,Value
v) -> Value -> Value -> Value
VPair (SimpleValue -> Value
fromSimpleValue SimpleValue
k) Value
v) ([(SimpleValue, Value)] -> [Value])
-> (Map SimpleValue Value -> [(SimpleValue, Value)])
-> Map SimpleValue Value
-> [Value]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map SimpleValue Value -> [(SimpleValue, Value)]
forall k a. Map k a -> [(k, a)]
M.assocs
prettyValue (TyMap Type
_ Type
_) Value
v =
  String -> Sem r Doc
forall a. HasCallStack => String -> a
error (String -> Sem r Doc) -> String -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ String
"Non-map value with map type passed to prettyValue: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
forall a. Show a => a -> String
show Value
v

prettyValue (TyGraph Type
ty) (VGraph Graph SimpleValue
g)          =
  Sem r Doc
-> (SimpleValue -> Sem r Doc)
-> (Sem r Doc -> Sem r Doc -> Sem r Doc)
-> (Sem r Doc -> Sem r Doc -> Sem r Doc)
-> Graph SimpleValue
-> Sem r Doc
forall b a.
b -> (a -> b) -> (b -> b -> b) -> (b -> b -> b) -> Graph a -> b
foldg
    Sem r Doc
"emptyGraph"
    ((Sem r Doc
"vertex" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<>) (Sem r Doc -> Sem r Doc)
-> (SimpleValue -> Sem r Doc) -> SimpleValue -> Sem r Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Value -> Sem r Doc
forall (r :: EffectRow).
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r Doc
prettyVP Type
ty (Value -> Sem r Doc)
-> (SimpleValue -> Value) -> SimpleValue -> Sem r Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleValue -> Value
fromSimpleValue)
    (\Sem r Doc
l Sem r Doc
r -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA (BOp -> PA
getPA BOp
Add) (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt Sem r Doc
l Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc
"+" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt Sem r Doc
r)
    (\Sem r Doc
l Sem r Doc
r -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA (BOp -> PA
getPA BOp
Mul) (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt Sem r Doc
l Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc
"*" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt Sem r Doc
r)
    Graph SimpleValue
g
prettyValue (TyGraph Type
_) Value
v =
  String -> Sem r Doc
forall a. HasCallStack => String -> a
error (String -> Sem r Doc) -> String -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ String
"Non-graph value with graph type passed to prettyValue: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
forall a. Show a => a -> String
show Value
v

prettyValue ty :: Type
ty@TyAtom{} Value
v =
  String -> Sem r Doc
forall a. HasCallStack => String -> a
error (String -> Sem r Doc) -> String -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ String
"Invalid atomic type passed to prettyValue: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
ty String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
forall a. Show a => a -> String
show Value
v

prettyValue ty :: Type
ty@TyCon{} Value
v =
  String -> Sem r Doc
forall a. HasCallStack => String -> a
error (String -> Sem r Doc) -> String -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ String
"Invalid type constructor passed to prettyValue: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
ty String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
forall a. Show a => a -> String
show Value
v

-- | Pretty-print a value with guaranteed parentheses.  Do nothing for
--   tuples; add an extra set of parens for other values.
prettyVP :: Members '[Input TyDefCtx, LFresh, Reader PA] r => Type -> Value -> Sem r Doc
prettyVP :: Type -> Value -> Sem r Doc
prettyVP ty :: Type
ty@(Type
_ :*: Type
_) = Type -> Value -> Sem r Doc
forall (r :: EffectRow).
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r Doc
prettyValue Type
ty
prettyVP Type
ty           = Sem r Doc -> Sem r Doc
forall (f :: * -> *). Functor f => f Doc -> f Doc
parens (Sem r Doc -> Sem r Doc)
-> (Value -> Sem r Doc) -> Value -> Sem r Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Value -> Sem r Doc
forall (r :: EffectRow).
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r Doc
prettyValue Type
ty

prettyPlaceholder :: Members '[Reader PA, LFresh] r => Type -> Sem r Doc
prettyPlaceholder :: Type -> Sem r Doc
prettyPlaceholder Type
ty = Sem r Doc
"<" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Type
ty Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> Sem r Doc
">"

prettyTuple :: Members '[Input TyDefCtx, LFresh, Reader PA] r => Type -> Value -> Sem r Doc
prettyTuple :: Type -> Value -> Sem r Doc
prettyTuple (Type
ty1 :*: Type
ty2) (VPair Value
v1 Value
v2) = Type -> Value -> Sem r Doc
forall (r :: EffectRow).
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r Doc
prettyValue Type
ty1 Value
v1 Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> Sem r Doc
"," Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Type -> Value -> Sem r Doc
forall (r :: EffectRow).
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r Doc
prettyTuple Type
ty2 Value
v2
prettyTuple Type
ty Value
v                        = Type -> Value -> Sem r Doc
forall (r :: EffectRow).
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r Doc
prettyValue Type
ty Value
v

-- | 'prettySequence' pretty-prints a lists of values separated by a delimiter.
prettySequence :: Members '[Input TyDefCtx, LFresh, Reader PA] r => Type -> Doc -> [Value] -> Sem r Doc
prettySequence :: Type -> Doc -> [Value] -> Sem r Doc
prettySequence Type
ty Doc
del [Value]
vs = [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep ([Sem r Doc] -> Sem r Doc) -> Sem r [Sem r Doc] -> Sem r Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Sem r Doc -> [Sem r Doc] -> Sem r [Sem r Doc]
forall (f :: * -> *).
Applicative f =>
f Doc -> [f Doc] -> f [f Doc]
punctuate (Doc -> Sem r Doc
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
del) ((Value -> Sem r Doc) -> [Value] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Type -> Value -> Sem r Doc
forall (r :: EffectRow).
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r Doc
prettyValue Type
ty) [Value]
vs)

-- | Pretty-print a literal bag value.
prettyBag :: Members '[Input TyDefCtx, LFresh, Reader PA] r => Type -> [(Value,Integer)] -> Sem r Doc
prettyBag :: Type -> [(Value, Integer)] -> Sem r Doc
prettyBag Type
_ [] = Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc
bag Sem r Doc
forall (m :: * -> *). Applicative m => m Doc
empty
prettyBag Type
ty [(Value, Integer)]
vs
  | ((Value, Integer) -> Bool) -> [(Value, Integer)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
==Integer
1) (Integer -> Bool)
-> ((Value, Integer) -> Integer) -> (Value, Integer) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Value, Integer) -> Integer
forall a b. (a, b) -> b
snd) [(Value, Integer)]
vs = Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc
bag (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ Type -> Doc -> [Value] -> Sem r Doc
forall (r :: EffectRow).
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Doc -> [Value] -> Sem r Doc
prettySequence Type
ty Doc
"," (((Value, Integer) -> Value) -> [(Value, Integer)] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map (Value, Integer) -> Value
forall a b. (a, b) -> a
fst [(Value, Integer)]
vs)
  | Bool
otherwise            = Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc
bag (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep ([Sem r Doc] -> Sem r Doc) -> Sem r [Sem r Doc] -> Sem r Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Sem r Doc -> [Sem r Doc] -> Sem r [Sem r Doc]
forall (f :: * -> *).
Applicative f =>
f Doc -> [f Doc] -> f [f Doc]
punctuate (Doc -> Sem r Doc
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
",") (((Value, Integer) -> Sem r Doc)
-> [(Value, Integer)] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Value, Integer) -> Sem r Doc
prettyCount [(Value, Integer)]
vs)
  where
    prettyCount :: (Value, Integer) -> Sem r Doc
prettyCount (Value
v,Integer
1) = Type -> Value -> Sem r Doc
forall (r :: EffectRow).
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r Doc
prettyValue Type
ty Value
v
    prettyCount (Value
v,Integer
n) = Type -> Value -> Sem r Doc
forall (r :: EffectRow).
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r Doc
prettyValue Type
ty Value
v Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc
"#" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Integer -> String
forall a. Show a => a -> String
show Integer
n)

------------------------------------------------------------
-- Pretty-printing for test results
------------------------------------------------------------

prettyTestFailure
  :: Members '[Input TyDefCtx, LFresh, Reader PA] r
  => AProperty -> TestResult -> Sem r Doc
prettyTestFailure :: AProperty -> TestResult -> Sem r Doc
prettyTestFailure AProperty
_    (TestResult Bool
True TestReason_ Value
_ TestEnv
_)    = Sem r Doc
forall (m :: * -> *). Applicative m => m Doc
empty
prettyTestFailure AProperty
prop (TestResult Bool
False TestReason_ Value
r TestEnv
env) =
  AProperty -> TestReason_ Value -> Sem r Doc
forall (r :: EffectRow).
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
AProperty -> TestReason_ Value -> Sem r Doc
prettyFailureReason AProperty
prop TestReason_ Value
r
  Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
$+$
  String -> TestEnv -> Sem r Doc
forall (r :: EffectRow).
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
String -> TestEnv -> Sem r Doc
prettyTestEnv String
"Counterexample:" TestEnv
env

prettyTestResult
  :: Members '[Input TyDefCtx, LFresh, Reader PA] r
  => AProperty -> TestResult -> Sem r Doc
prettyTestResult :: AProperty -> TestResult -> Sem r Doc
prettyTestResult AProperty
prop TestResult
r | Bool -> Bool
not (TestResult -> Bool
testIsOk TestResult
r) = AProperty -> TestResult -> Sem r Doc
forall (r :: EffectRow).
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
AProperty -> TestResult -> Sem r Doc
prettyTestFailure AProperty
prop TestResult
r
prettyTestResult AProperty
prop (TestResult Bool
_ TestReason_ Value
r TestEnv
_)   =
  (Sem r Doc
"Test passed:" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Property -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty (AProperty -> Property
eraseProperty AProperty
prop))
  Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
$+$
  TestReason_ Value -> Sem r Doc
forall (r :: EffectRow).
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
TestReason_ Value -> Sem r Doc
prettySuccessReason TestReason_ Value
r

prettySuccessReason
  :: Members '[Input TyDefCtx, LFresh, Reader PA] r
  => TestReason -> Sem r Doc
prettySuccessReason :: TestReason_ Value -> Sem r Doc
prettySuccessReason (TestFound (TestResult Bool
_ TestReason_ Value
_ TestEnv
vs)) = String -> TestEnv -> Sem r Doc
forall (r :: EffectRow).
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
String -> TestEnv -> Sem r Doc
prettyTestEnv String
"Found example:" TestEnv
vs
prettySuccessReason (TestNotFound SearchType
Exhaustive) = Sem r Doc
"No counterexamples exist."
prettySuccessReason (TestNotFound (Randomized Integer
n Integer
m)) =
  Sem r Doc
"Checked" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Integer -> String
forall a. Show a => a -> String
show (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
m)) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc
"possibilities without finding a counterexample."
prettySuccessReason TestReason_ Value
_ = Sem r Doc
forall (m :: * -> *). Applicative m => m Doc
empty

prettyFailureReason
  :: Members '[Input TyDefCtx, LFresh, Reader PA] r
  => AProperty -> TestReason -> Sem r Doc
prettyFailureReason :: AProperty -> TestReason_ Value -> Sem r Doc
prettyFailureReason AProperty
prop TestReason_ Value
TestBool = Sem r Doc
"Test is false:" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Property -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty (AProperty -> Property
eraseProperty AProperty
prop)
prettyFailureReason AProperty
prop (TestEqual Type
ty Value
v1 Value
v2) =
  Sem r Doc
"Test result mismatch for:" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Property -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty (AProperty -> Property
eraseProperty AProperty
prop)
  Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
$+$
  Sem r Doc -> [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> [f Doc] -> f Doc
bulletList Sem r Doc
"-"
  [ Sem r Doc
"Left side:  " Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> Type -> Value -> Sem r Doc
forall (r :: EffectRow).
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r Doc
prettyValue Type
ty Value
v1
  , Sem r Doc
"Right side: " Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> Type -> Value -> Sem r Doc
forall (r :: EffectRow).
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r Doc
prettyValue Type
ty Value
v2
  ]
prettyFailureReason AProperty
prop (TestRuntimeError EvalError
e) =
  Sem r Doc
"Test failed:" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Property -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty (AProperty -> Property
eraseProperty AProperty
prop)
  Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
$+$
  DiscoError -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty (EvalError -> DiscoError
EvalErr EvalError
e)
prettyFailureReason AProperty
prop (TestFound (TestResult Bool
_ TestReason_ Value
r TestEnv
_)) = AProperty -> TestReason_ Value -> Sem r Doc
forall (r :: EffectRow).
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
AProperty -> TestReason_ Value -> Sem r Doc
prettyFailureReason AProperty
prop TestReason_ Value
r
prettyFailureReason AProperty
prop (TestNotFound SearchType
Exhaustive) =
  Sem r Doc
"No example exists:" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Property -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty (AProperty -> Property
eraseProperty AProperty
prop)
  Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
$+$
  Sem r Doc
"All possible values were checked."
prettyFailureReason AProperty
prop (TestNotFound (Randomized Integer
n Integer
m)) = do
  Sem r Doc
"No example was found:" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Property -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty (AProperty -> Property
eraseProperty AProperty
prop)
  Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
$+$
  (Sem r Doc
"Checked" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Integer -> String
forall a. Show a => a -> String
show (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
m)) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc
"possibilities.")

prettyTestEnv
  :: Members '[Input TyDefCtx, LFresh, Reader PA] r
  => String -> TestEnv -> Sem r Doc
prettyTestEnv :: String -> TestEnv -> Sem r Doc
prettyTestEnv String
_ (TestEnv []) = Sem r Doc
forall (m :: * -> *). Applicative m => m Doc
empty
prettyTestEnv String
s (TestEnv [(String, Type, Value)]
vs) = String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
s Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
$+$ Int -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Functor f => Int -> f Doc -> f Doc
nest Int
2 ([Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
vcat (((String, Type, Value) -> Sem r Doc)
-> [(String, Type, Value)] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String, Type, Value) -> Sem r Doc
prettyBind [(String, Type, Value)]
vs))
  where
    maxNameLen :: Int
maxNameLen = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Int] -> Int)
-> ([(String, Type, Value)] -> [Int])
-> [(String, Type, Value)]
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((String, Type, Value) -> Int) -> [(String, Type, Value)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (\(String
n, Type
_, Value
_) -> String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
n) ([(String, Type, Value)] -> Int) -> [(String, Type, Value)] -> Int
forall a b. (a -> b) -> a -> b
$ [(String, Type, Value)]
vs
    prettyBind :: (String, Type, Value) -> Sem r Doc
prettyBind (String
x, Type
ty, Value
v) =
      String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
x Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int
maxNameLen Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
x) Char
' ') Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc
"=" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Type -> Value -> Sem r Doc
forall (r :: EffectRow).
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r Doc
prettyValue Type
ty Value
v