{-# 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,
  boolv,
  vbool,
  pairv,
  vpair,
  listv,
  vlist,
  genv,
  vgen,

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

  -- * Environments
  Env,

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

  -- * Pretty-printing
  prettyValue',
  prettyValue,
) where

import Algebra.Graph (Graph, foldg)
import Control.Monad (forM)
import Data.Bifunctor (first)
import Data.Char (chr, ord)
import Data.Foldable (Foldable (..))
import Data.Function (on)
import Data.IntMap (IntMap)
import qualified Data.IntMap as IM
import Data.List (nubBy)
import Data.Map (Map)
import qualified Data.Map as M
import Data.Ratio
import Disco.AST.Core
import Disco.AST.Generic (Side (..))
import Disco.Context as Ctx
import Disco.Effects.LFresh
import Disco.Error
import Disco.Names
import Disco.Pretty
import Disco.Syntax.Operators (BOp (Add, Mul))
import Disco.Types
import Polysemy
import Polysemy.Input
import Polysemy.Reader
import Polysemy.State
import System.Random (StdGen)
import Unbound.Generics.LocallyNameless (Name)
import Prelude hiding (Foldable (..), (<>))
import qualified Prelude as P

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

-- | Different types of values which can result from the evaluation
--   process.
data Value where
  -- | A numeric value.
  VNum :: 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 :: Maybe (Int, [Value]) -> 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
  VGen :: StdGen -> 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
$cshowsPrec :: Int -> Value -> ShowS
showsPrec :: Int -> Value -> ShowS
$cshow :: Value -> String
show :: Value -> String
$cshowList :: [Value] -> ShowS
showList :: [Value] -> ShowS
Show)

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

-- | Convenient pattern for list cons.
pattern VCons :: Value -> Value -> Value
pattern $mVCons :: forall {r}. Value -> (Value -> Value -> r) -> ((# #) -> r) -> r
$bVCons :: Value -> Value -> Value
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 :: 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
$cshowsPrec :: Int -> SimpleValue -> ShowS
showsPrec :: Int -> SimpleValue -> ShowS
$cshow :: SimpleValue -> String
show :: SimpleValue -> String
$cshowList :: [SimpleValue] -> ShowS
showList :: [SimpleValue] -> ShowS
Show, SimpleValue -> SimpleValue -> Bool
(SimpleValue -> SimpleValue -> Bool)
-> (SimpleValue -> SimpleValue -> Bool) -> Eq SimpleValue
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SimpleValue -> SimpleValue -> Bool
== :: SimpleValue -> SimpleValue -> Bool
$c/= :: SimpleValue -> SimpleValue -> Bool
/= :: 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
$ccompare :: SimpleValue -> SimpleValue -> Ordering
compare :: SimpleValue -> SimpleValue -> Ordering
$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
>= :: SimpleValue -> SimpleValue -> Bool
$cmax :: SimpleValue -> SimpleValue -> SimpleValue
max :: SimpleValue -> SimpleValue -> SimpleValue
$cmin :: SimpleValue -> SimpleValue -> SimpleValue
min :: SimpleValue -> SimpleValue -> SimpleValue
Ord)

toSimpleValue :: Value -> SimpleValue
toSimpleValue :: Value -> SimpleValue
toSimpleValue = \case
  VNum Rational
n -> Rational -> SimpleValue
SNum 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 a b c. (a -> b) -> (a, c) -> (b, c)
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 Rational
n) = Rational -> Value
VNum 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 a b c. (a -> b) -> (a, c) -> (b, c)
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 $mVFun :: forall {r}. Value -> ((Value -> Value) -> r) -> ((# #) -> r) -> r
$bVFun :: (Value -> Value) -> Value
VFun f = VFun_ (ValFun f)

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

-- XXX write some comments about partiality

ratv :: Rational -> Value
ratv :: Rational -> Value
ratv = Rational -> Value
VNum

vrat :: Value -> Rational
vrat :: Value -> Rational
vrat (VNum 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 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

boolv :: Bool -> Value
boolv :: Bool -> Value
boolv Bool
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
$ Bool -> Int
forall a. Enum a => a -> Int
fromEnum Bool
e) Value
VUnit

vbool :: Value -> Bool
vbool :: Value -> Bool
vbool (VInj Side
s Value
VUnit) = Int -> Bool
forall a. Enum a => Int -> a
toEnum (Int -> Bool) -> Int -> Bool
forall a b. (a -> b) -> a -> b
$ Side -> Int
forall a. Enum a => a -> Int
fromEnum Side
s
vbool Value
v = String -> Bool
forall a. HasCallStack => String -> a
error (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ String
"vbool " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
forall a. Show a => a -> String
show Value
v

pairv :: (a -> Value) -> (b -> Value) -> (a, b) -> Value
pairv :: forall a b. (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 :: forall a b. (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 :: forall a. (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 :: forall a. (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

vgen :: Value -> StdGen
vgen :: Value -> StdGen
vgen (VGen StdGen
v) = StdGen
v
vgen Value
v = String -> StdGen
forall a. HasCallStack => String -> a
error (String -> StdGen) -> String -> StdGen
forall a b. (a -> b) -> a -> b
$ String
"vgen " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
forall a. Show a => a -> String
show Value
v

genv :: StdGen -> Value
genv :: StdGen -> Value
genv = StdGen -> Value
VGen

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

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

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

pattern SMExists :: SearchMotive
pattern $mSMExists :: forall {r}. SearchMotive -> ((# #) -> r) -> ((# #) -> r) -> r
$bSMExists :: SearchMotive
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
$cshowsPrec :: Int -> TestVars -> ShowS
showsPrec :: Int -> TestVars -> ShowS
$cshow :: TestVars -> String
show :: TestVars -> String
$cshowList :: [TestVars] -> ShowS
showList :: [TestVars] -> ShowS
Show, 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
$c<> :: TestVars -> TestVars -> TestVars
<> :: TestVars -> TestVars -> TestVars
$csconcat :: NonEmpty TestVars -> TestVars
sconcat :: NonEmpty TestVars -> TestVars
$cstimes :: forall b. Integral b => b -> TestVars -> TestVars
stimes :: forall b. Integral b => b -> 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
$cmempty :: TestVars
mempty :: TestVars
$cmappend :: TestVars -> TestVars -> TestVars
mappend :: TestVars -> TestVars -> TestVars
$cmconcat :: [TestVars] -> TestVars
mconcat :: [TestVars] -> 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
$cshowsPrec :: Int -> TestEnv -> ShowS
showsPrec :: Int -> TestEnv -> ShowS
$cshow :: TestEnv -> String
show :: TestEnv -> String
$cshowList :: [TestEnv] -> ShowS
showList :: [TestEnv] -> ShowS
Show, 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
$c<> :: TestEnv -> TestEnv -> TestEnv
<> :: TestEnv -> TestEnv -> TestEnv
$csconcat :: NonEmpty TestEnv -> TestEnv
sconcat :: NonEmpty TestEnv -> TestEnv
$cstimes :: forall b. Integral b => b -> TestEnv -> TestEnv
stimes :: forall b. Integral b => b -> 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
$cmempty :: TestEnv
mempty :: TestEnv
$cmappend :: TestEnv -> TestEnv -> TestEnv
mappend :: TestEnv -> TestEnv -> TestEnv
$cmconcat :: [TestEnv] -> TestEnv
mconcat :: [TestEnv] -> TestEnv
Monoid)

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

mergeTestEnv :: TestEnv -> TestEnv -> TestEnv
mergeTestEnv :: TestEnv -> TestEnv -> TestEnv
mergeTestEnv (TestEnv [(String, Type, Value)]
e1) (TestEnv [(String, Type, Value)]
e2) = [(String, Type, Value)] -> TestEnv
TestEnv (((String, Type, Value) -> (String, Type, Value) -> Bool)
-> [(String, Type, Value)] -> [(String, Type, Value)]
forall a. (a -> a -> Bool) -> [a] -> [a]
nubBy (String -> String -> Bool
forall a. Eq a => a -> a -> Bool
(==) (String -> String -> Bool)
-> ((String, Type, Value) -> String)
-> (String, Type, Value)
-> (String, Type, Value)
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (String, Type, Value) -> String
forall {a} {b} {c}. (a, b, c) -> a
fst3) ([(String, Type, Value)]
e1 [(String, Type, Value)]
-> [(String, Type, Value)] -> [(String, Type, Value)]
forall a. Semigroup a => a -> a -> a
P.<> [(String, Type, Value)]
e2))
 where
  fst3 :: (a, b, c) -> a
fst3 (a
a, b
_, c
_) = a
a

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 a b. (a -> b) -> Either EvalError a -> Either EvalError b
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 a. a -> Either EvalError a
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
UnboundPanic Name Core
name)

-- | Binary logical operators.
data LOp = LAnd | LOr | LImpl deriving (LOp -> LOp -> Bool
(LOp -> LOp -> Bool) -> (LOp -> LOp -> Bool) -> Eq LOp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LOp -> LOp -> Bool
== :: LOp -> LOp -> Bool
$c/= :: LOp -> LOp -> Bool
/= :: LOp -> LOp -> Bool
Eq, Eq LOp
Eq LOp =>
(LOp -> LOp -> Ordering)
-> (LOp -> LOp -> Bool)
-> (LOp -> LOp -> Bool)
-> (LOp -> LOp -> Bool)
-> (LOp -> LOp -> Bool)
-> (LOp -> LOp -> LOp)
-> (LOp -> LOp -> LOp)
-> Ord LOp
LOp -> LOp -> Bool
LOp -> LOp -> Ordering
LOp -> LOp -> LOp
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
$ccompare :: LOp -> LOp -> Ordering
compare :: LOp -> LOp -> Ordering
$c< :: LOp -> LOp -> Bool
< :: LOp -> LOp -> Bool
$c<= :: LOp -> LOp -> Bool
<= :: LOp -> LOp -> Bool
$c> :: LOp -> LOp -> Bool
> :: LOp -> LOp -> Bool
$c>= :: LOp -> LOp -> Bool
>= :: LOp -> LOp -> Bool
$cmax :: LOp -> LOp -> LOp
max :: LOp -> LOp -> LOp
$cmin :: LOp -> LOp -> LOp
min :: LOp -> LOp -> LOp
Ord, Int -> LOp -> ShowS
[LOp] -> ShowS
LOp -> String
(Int -> LOp -> ShowS)
-> (LOp -> String) -> ([LOp] -> ShowS) -> Show LOp
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> LOp -> ShowS
showsPrec :: Int -> LOp -> ShowS
$cshow :: LOp -> String
show :: LOp -> String
$cshowList :: [LOp] -> ShowS
showList :: [LOp] -> ShowS
Show, Int -> LOp
LOp -> Int
LOp -> [LOp]
LOp -> LOp
LOp -> LOp -> [LOp]
LOp -> LOp -> LOp -> [LOp]
(LOp -> LOp)
-> (LOp -> LOp)
-> (Int -> LOp)
-> (LOp -> Int)
-> (LOp -> [LOp])
-> (LOp -> LOp -> [LOp])
-> (LOp -> LOp -> [LOp])
-> (LOp -> LOp -> LOp -> [LOp])
-> Enum LOp
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: LOp -> LOp
succ :: LOp -> LOp
$cpred :: LOp -> LOp
pred :: LOp -> LOp
$ctoEnum :: Int -> LOp
toEnum :: Int -> LOp
$cfromEnum :: LOp -> Int
fromEnum :: LOp -> Int
$cenumFrom :: LOp -> [LOp]
enumFrom :: LOp -> [LOp]
$cenumFromThen :: LOp -> LOp -> [LOp]
enumFromThen :: LOp -> LOp -> [LOp]
$cenumFromTo :: LOp -> LOp -> [LOp]
enumFromTo :: LOp -> LOp -> [LOp]
$cenumFromThenTo :: LOp -> LOp -> LOp -> [LOp]
enumFromThenTo :: LOp -> LOp -> LOp -> [LOp]
Enum, LOp
LOp -> LOp -> Bounded LOp
forall a. a -> a -> Bounded a
$cminBound :: LOp
minBound :: LOp
$cmaxBound :: LOp
maxBound :: LOp
Bounded)

interpLOp :: LOp -> Bool -> Bool -> Bool
interpLOp :: LOp -> Bool -> Bool -> Bool
interpLOp LOp
LAnd = Bool -> Bool -> Bool
(&&)
interpLOp LOp
LOr = Bool -> Bool -> Bool
(||)
interpLOp LOp
LImpl = Bool -> Bool -> Bool
(==>)
 where
  Bool
True ==> :: Bool -> Bool -> Bool
==> Bool
False = Bool
False
  Bool
_ ==> Bool
_ = Bool
True

-- | 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
  = -- | The prop evaluated to a boolean.
    TestBool
  | -- | The test was a comparison. Records the comparison operator,
    --   the values being compared, and also their type (which is
    --   needed for printing).
    TestCmp BOp Type a a
  | -- | The search didn't find any examples/counterexamples.
    TestNotFound SearchType
  | -- | The search found an example/counterexample.
    TestFound TestResult
  | -- | A binary logical operator was used to combine the given two results.
    TestBin LOp TestResult TestResult
  | -- | The prop failed at runtime. This is always a failure, no
    --   matter which quantifiers or negations it's under.
    TestRuntimeError EvalError
  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
$cshowsPrec :: forall a. Show a => Int -> TestReason_ a -> ShowS
showsPrec :: Int -> TestReason_ a -> ShowS
$cshow :: forall a. Show a => TestReason_ a -> String
show :: TestReason_ a -> String
$cshowList :: forall a. Show a => [TestReason_ a] -> ShowS
showList :: [TestReason_ a] -> ShowS
Show, (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
$cfmap :: forall a b. (a -> b) -> TestReason_ a -> TestReason_ b
fmap :: forall a b. (a -> b) -> TestReason_ a -> TestReason_ b
$c<$ :: forall a b. a -> TestReason_ b -> TestReason_ a
<$ :: forall a b. a -> TestReason_ b -> TestReason_ a
Functor, (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
$cfold :: forall m. Monoid m => TestReason_ m -> m
fold :: forall m. Monoid m => TestReason_ m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> TestReason_ a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> TestReason_ a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> TestReason_ a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> TestReason_ a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> TestReason_ a -> b
foldr :: forall a b. (a -> b -> b) -> b -> TestReason_ a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> TestReason_ a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> TestReason_ a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> TestReason_ a -> b
foldl :: forall b a. (b -> a -> b) -> b -> TestReason_ a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> TestReason_ a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> TestReason_ a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> TestReason_ a -> a
foldr1 :: forall a. (a -> a -> a) -> TestReason_ a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> TestReason_ a -> a
foldl1 :: forall a. (a -> a -> a) -> TestReason_ a -> a
$ctoList :: forall a. TestReason_ a -> [a]
toList :: forall a. TestReason_ a -> [a]
$cnull :: forall a. TestReason_ a -> Bool
null :: forall a. TestReason_ a -> Bool
$clength :: forall a. TestReason_ a -> Int
length :: forall a. TestReason_ a -> Int
$celem :: forall a. Eq a => a -> TestReason_ a -> Bool
elem :: forall a. Eq a => a -> TestReason_ a -> Bool
$cmaximum :: forall a. Ord a => TestReason_ a -> a
maximum :: forall a. Ord a => TestReason_ a -> a
$cminimum :: forall a. Ord a => TestReason_ a -> a
minimum :: forall a. Ord a => TestReason_ a -> a
$csum :: forall a. Num a => TestReason_ a -> a
sum :: forall a. Num a => TestReason_ a -> a
$cproduct :: forall a. Num a => TestReason_ a -> a
product :: forall a. Num a => TestReason_ a -> a
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_
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)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TestReason_ a -> f (TestReason_ b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TestReason_ a -> f (TestReason_ b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
TestReason_ (f a) -> f (TestReason_ a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
TestReason_ (f a) -> f (TestReason_ a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TestReason_ a -> m (TestReason_ b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TestReason_ a -> m (TestReason_ b)
$csequence :: forall (m :: * -> *) a.
Monad m =>
TestReason_ (m a) -> m (TestReason_ a)
sequence :: forall (m :: * -> *) a.
Monad m =>
TestReason_ (m a) -> m (TestReason_ a)
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
$cshowsPrec :: Int -> TestResult -> ShowS
showsPrec :: Int -> TestResult -> ShowS
$cshow :: TestResult -> String
show :: TestResult -> String
$cshowList :: [TestResult] -> ShowS
showList :: [TestResult] -> ShowS
Show)

-- | Whether the property test resulted in a runtime error.
testIsError :: TestResult -> Bool
testIsError :: TestResult -> Bool
testIsError (TestResult Bool
_ (TestRuntimeError {}) 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
_ TestEnv
_) = Bool
b

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

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

testIsCertain :: TestResult -> Bool
testIsCertain :: TestResult -> Bool
testIsCertain (TestResult Bool
_ TestReason
r TestEnv
_) = TestReason -> Bool
resultIsCertain TestReason
r

resultIsCertain :: TestReason -> Bool
resultIsCertain :: TestReason -> Bool
resultIsCertain TestReason
TestBool = Bool
True
resultIsCertain TestCmp {} = Bool
True
resultIsCertain (TestNotFound SearchType
Exhaustive) = Bool
True
resultIsCertain (TestNotFound (Randomized Integer
_ Integer
_)) = Bool
False
resultIsCertain (TestFound TestResult
r) = TestResult -> Bool
testIsCertain TestResult
r
resultIsCertain (TestRuntimeError {}) = Bool
True
resultIsCertain (TestBin LOp
op TestResult
tr1 TestResult
tr2)
  | Bool
c1 Bool -> Bool -> Bool
&& Bool
c2 = Bool
True
  | Bool
c1 Bool -> Bool -> Bool
&& ((LOp
op LOp -> LOp -> Bool
forall a. Eq a => a -> a -> Bool
== LOp
LOr) Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
ok1) = Bool
True
  | Bool
c2 Bool -> Bool -> Bool
&& ((LOp
op LOp -> LOp -> Bool
forall a. Eq a => a -> a -> Bool
/= LOp
LAnd) Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
ok2) = Bool
True
  | Bool
otherwise = Bool
False
 where
  c1 :: Bool
c1 = TestResult -> Bool
testIsCertain TestResult
tr1
  c2 :: Bool
c2 = TestResult -> Bool
testIsCertain TestResult
tr2
  ok1 :: Bool
ok1 = TestResult -> Bool
testIsOk TestResult
tr1
  ok2 :: Bool
ok2 = TestResult -> Bool
testIsOk TestResult
tr2

-- | A @ValProp@ is the normal form of a Disco value of type @Prop@.
data ValProp
  = -- | A prop that has already either succeeded or failed.
    VPDone TestResult
  | -- | A pending search.
    VPSearch SearchMotive [Type] Value TestEnv
  | -- | A binary logical operator combining two prop values.
    VPBin LOp ValProp ValProp
  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
$cshowsPrec :: Int -> ValProp -> ShowS
showsPrec :: Int -> ValProp -> ShowS
$cshow :: ValProp -> String
show :: ValProp -> String
$cshowList :: [ValProp] -> ShowS
showList :: [ValProp] -> ShowS
Show)

extendPropEnv :: TestEnv -> ValProp -> ValProp
extendPropEnv :: TestEnv -> ValProp -> ValProp
extendPropEnv TestEnv
g (VPDone TestResult
res) = TestResult -> ValProp
VPDone (TestEnv -> TestResult -> TestResult
extendResultEnv TestEnv
g TestResult
res)
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)
extendPropEnv TestEnv
g (VPBin LOp
op ValProp
vp1 ValProp
vp2) = LOp -> ValProp -> ValProp -> ValProp
VPBin LOp
op (TestEnv -> ValProp -> ValProp
extendPropEnv TestEnv
g ValProp
vp1) (TestEnv -> ValProp -> ValProp
extendPropEnv TestEnv
g ValProp
vp2)

extendResultEnv :: TestEnv -> TestResult -> TestResult
extendResultEnv :: TestEnv -> TestResult -> TestResult
extendResultEnv TestEnv
g (TestResult Bool
b TestReason
r TestEnv
e) = Bool -> TestReason -> TestEnv -> TestResult
TestResult Bool
b TestReason
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
$cshowsPrec :: Int -> Mem -> ShowS
showsPrec :: Int -> Mem -> ShowS
$cshow :: Mem -> String
show :: Mem -> String
$cshowList :: [Mem] -> ShowS
showList :: [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
$cshowsPrec :: Int -> Cell -> ShowS
showsPrec :: Int -> Cell -> ShowS
$cshow :: Cell -> String
show :: Cell -> String
$cshowList :: [Cell] -> ShowS
showList :: [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 :: forall (r :: EffectRow).
Members '[State Mem] r =>
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
n Int -> 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 a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
n

allocateValue :: Members '[State Mem] r => Value -> Sem r Int
allocateValue :: forall (r :: EffectRow).
Members '[State Mem] r =>
Value -> Sem r Int
allocateValue Value
v = 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
n Int -> 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 (Value -> Cell
Disco.Value.V Value
v) IntMap Cell
m)
  Int -> Sem r Int
forall a. a -> Sem r a
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 :: forall (r :: EffectRow).
Members '[State Mem] r =>
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 b a. (b -> a -> b) -> b -> [a] -> b
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 b a. (b -> a -> b) -> b -> [a] -> b
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 a. [a] -> 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 a. a -> Sem r a
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 :: forall (r :: EffectRow).
Members '[State Mem] r =>
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 :: forall (r :: EffectRow).
Members '[State Mem] r =>
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)

memoLookup :: Members '[State Mem] r => Int -> SimpleValue -> Sem r (Maybe Value)
memoLookup :: forall (r :: EffectRow).
Members '[State Mem] r =>
Int -> SimpleValue -> Sem r (Maybe Value)
memoLookup Int
n SimpleValue
sv = (Mem -> Maybe Value) -> Sem r (Maybe Value)
forall s a (r :: EffectRow).
Member (State s) r =>
(s -> a) -> Sem r a
gets (Maybe Cell -> Maybe Value
mLookup (Maybe Cell -> Maybe Value)
-> (Mem -> Maybe Cell) -> Mem -> Maybe Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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)
 where
  mLookup :: Maybe Cell -> Maybe Value
mLookup (Just (Disco.Value.V (VMap Map SimpleValue Value
vmap))) = SimpleValue -> Map SimpleValue Value -> Maybe Value
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup SimpleValue
sv Map SimpleValue Value
vmap
  mLookup Maybe Cell
_ = Maybe Value
forall a. Maybe a
Nothing

memoSet :: Members '[State Mem] r => Int -> SimpleValue -> Value -> Sem r ()
memoSet :: forall (r :: EffectRow).
Members '[State Mem] r =>
Int -> SimpleValue -> Value -> Sem r ()
memoSet Int
n SimpleValue
sv Value
v = do
  Maybe Cell
mc <- Int -> Sem r (Maybe Cell)
forall (r :: EffectRow).
Members '[State Mem] r =>
Int -> Sem r (Maybe Cell)
lkup Int
n
  case Maybe Cell
mc of
    Just (Disco.Value.V (VMap Map SimpleValue Value
vmap)) -> Int -> Cell -> Sem r ()
forall (r :: EffectRow).
Members '[State Mem] r =>
Int -> Cell -> Sem r ()
set Int
n (Value -> Cell
Disco.Value.V (Map SimpleValue Value -> Value
VMap (SimpleValue
-> Value -> Map SimpleValue Value -> Map SimpleValue Value
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert SimpleValue
sv Value
v Map SimpleValue Value
vmap)))
    Maybe Cell
_ -> () -> Sem r ()
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

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

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

prettyValue :: Members '[Input TyDefCtx, LFresh, Reader PA] r => Type -> Value -> Sem r (Doc ann)
-- Lazily expand any user-defined types
prettyValue :: forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r (Doc ann)
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 ann)
forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r (Doc ann)
prettyValue ([Type] -> Type
body [Type]
args) Value
v
prettyValue Type
_ Value
VUnit = Sem r (Doc ann)
"■"
prettyValue Type
TyProp Value
_ = Type -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Type -> Sem r (Doc ann)
prettyPlaceholder Type
TyProp
prettyValue Type
TyBool (VInj Side
s Value
_) = String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (String -> Sem r (Doc ann)) -> String -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ Int -> ShowS
forall a. Int -> [a] -> [a]
take Int
1 (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 ann)
forall a. HasCallStack => String -> a
error (String -> Sem r (Doc ann)) -> String -> Sem r (Doc ann)
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 ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
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 ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
doubleQuotes (Sem r (Doc ann) -> Sem r (Doc ann))
-> (String -> Sem r (Doc ann)) -> String -> Sem r (Doc ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (String -> Sem r (Doc ann)) -> ShowS -> String -> Sem r (Doc ann)
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 ann)) -> String -> Sem r (Doc ann)
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 ann)]
ds <- Sem r (Doc ann) -> [Sem r (Doc ann)] -> Sem r [Sem r (Doc ann)]
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> [f (Doc ann)] -> f [f (Doc ann)]
punctuate (String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
",") ((Value -> Sem r (Doc ann)) -> [Value] -> [Sem r (Doc ann)]
forall a b. (a -> b) -> [a] -> [b]
map (Type -> Value -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r (Doc ann)
prettyValue Type
ty) [Value]
xs)
  Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
brackets ([Sem r (Doc ann)] -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep [Sem r (Doc ann)]
ds)
prettyValue ty :: Type
ty@(Type
_ :*: Type
_) Value
v = Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
parens (Type -> Value -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r (Doc ann)
prettyTuple Type
ty Value
v)
prettyValue (Type
ty1 :+: Type
_) (VInj Side
L Value
v) = Sem r (Doc ann)
"left" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Type -> Value -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r (Doc ann)
prettyVP Type
ty1 Value
v
prettyValue (Type
_ :+: Type
ty2) (VInj Side
R Value
v) = Sem r (Doc ann)
"right" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Type -> Value -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r (Doc ann)
prettyVP Type
ty2 Value
v
prettyValue (Type
_ :+: Type
_) Value
v =
  String -> Sem r (Doc ann)
forall a. HasCallStack => String -> a
error (String -> Sem r (Doc ann)) -> String -> Sem r (Doc ann)
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 Rational
r) = String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (String -> Sem r (Doc ann)) -> String -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ Rational -> String
prettyRational Rational
r
prettyValue Type
_ (VGen StdGen
_) = Type -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Type -> Sem r (Doc ann)
prettyPlaceholder Type
TyGen
prettyValue ty :: Type
ty@(Type
_ :->: Type
_) Value
_ = Type -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Type -> Sem r (Doc ann)
prettyPlaceholder Type
ty
prettyValue (TySet Type
ty) (VBag [(Value, Integer)]
xs) = Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
braces (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ Type -> Doc ann -> [Value] -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Doc ann -> [Value] -> Sem r (Doc ann)
prettySequence Type
ty Doc ann
"," (((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 ann)
forall a. HasCallStack => String -> a
error (String -> Sem r (Doc ann)) -> String -> Sem r (Doc ann)
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 ann)
forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> [(Value, Integer)] -> Sem r (Doc ann)
prettyBag Type
ty [(Value, Integer)]
xs
prettyValue (TyBag Type
_) Value
v =
  String -> Sem r (Doc ann)
forall a. HasCallStack => String -> a
error (String -> Sem r (Doc ann)) -> String -> Sem r (Doc ann)
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 ann)
"map" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
parens (Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
braces (Type -> Doc ann -> [Value] -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Doc ann -> [Value] -> Sem r (Doc ann)
prettySequence (Type
tyK Type -> Type -> Type
:*: Type
tyV) Doc ann
"," (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 ann)
forall a. HasCallStack => String -> a
error (String -> Sem r (Doc ann)) -> String -> Sem r (Doc ann)
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 ann)
-> (SimpleValue -> Sem r (Doc ann))
-> (Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann))
-> (Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann))
-> Graph SimpleValue
-> Sem r (Doc ann)
forall b a.
b -> (a -> b) -> (b -> b -> b) -> (b -> b -> b) -> Graph a -> b
foldg
    Sem r (Doc ann)
"emptyGraph"
    ((Sem r (Doc ann)
"vertex" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<>) (Sem r (Doc ann) -> Sem r (Doc ann))
-> (SimpleValue -> Sem r (Doc ann))
-> SimpleValue
-> Sem r (Doc ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Value -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r (Doc ann)
prettyVP Type
ty (Value -> Sem r (Doc ann))
-> (SimpleValue -> Value) -> SimpleValue -> Sem r (Doc ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleValue -> Value
fromSimpleValue)
    (\Sem r (Doc ann)
l Sem r (Doc ann)
r -> PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA (BOp -> PA
getPA BOp
Add) (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt Sem r (Doc ann)
l Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"+" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt Sem r (Doc ann)
r)
    (\Sem r (Doc ann)
l Sem r (Doc ann)
r -> PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA (BOp -> PA
getPA BOp
Mul) (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt Sem r (Doc ann)
l Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"*" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt Sem r (Doc ann)
r)
    Graph SimpleValue
g
prettyValue (TyGraph Type
_) Value
v =
  String -> Sem r (Doc ann)
forall a. HasCallStack => String -> a
error (String -> Sem r (Doc ann)) -> String -> Sem r (Doc ann)
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 ann)
forall a. HasCallStack => String -> a
error (String -> Sem r (Doc ann)) -> String -> Sem r (Doc ann)
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 ann)
forall a. HasCallStack => String -> a
error (String -> Sem r (Doc ann)) -> String -> Sem r (Doc ann)
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 ann)
prettyVP :: forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r (Doc ann)
prettyVP ty :: Type
ty@(Type
_ :*: Type
_) = Type -> Value -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r (Doc ann)
prettyValue Type
ty
prettyVP Type
ty = Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
parens (Sem r (Doc ann) -> Sem r (Doc ann))
-> (Value -> Sem r (Doc ann)) -> Value -> Sem r (Doc ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Value -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r (Doc ann)
prettyValue Type
ty

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

prettyTuple :: Members '[Input TyDefCtx, LFresh, Reader PA] r => Type -> Value -> Sem r (Doc ann)
prettyTuple :: forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r (Doc ann)
prettyTuple (Type
ty1 :*: Type
ty2) (VPair Value
v1 Value
v2) = Type -> Value -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r (Doc ann)
prettyValue Type
ty1 Value
v1 Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
"," Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Type -> Value -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r (Doc ann)
prettyTuple Type
ty2 Value
v2
prettyTuple Type
ty Value
v = Type -> Value -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r (Doc ann)
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 ann -> [Value] -> Sem r (Doc ann)
prettySequence :: forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Doc ann -> [Value] -> Sem r (Doc ann)
prettySequence Type
ty Doc ann
del [Value]
vs = [Sem r (Doc ann)] -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep ([Sem r (Doc ann)] -> Sem r (Doc ann))
-> Sem r [Sem r (Doc ann)] -> Sem r (Doc ann)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Sem r (Doc ann) -> [Sem r (Doc ann)] -> Sem r [Sem r (Doc ann)]
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> [f (Doc ann)] -> f [f (Doc ann)]
punctuate (Doc ann -> Sem r (Doc ann)
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc ann
del) ((Value -> Sem r (Doc ann)) -> [Value] -> [Sem r (Doc ann)]
forall a b. (a -> b) -> [a] -> [b]
map (Type -> Value -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r (Doc ann)
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 ann)
prettyBag :: forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> [(Value, Integer)] -> Sem r (Doc ann)
prettyBag Type
_ [] = Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann)
bag Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => m (Doc ann)
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 ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann)
bag (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ Type -> Doc ann -> [Value] -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Doc ann -> [Value] -> Sem r (Doc ann)
prettySequence Type
ty Doc ann
"," (((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 ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann)
bag (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ [Sem r (Doc ann)] -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep ([Sem r (Doc ann)] -> Sem r (Doc ann))
-> Sem r [Sem r (Doc ann)] -> Sem r (Doc ann)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Sem r (Doc ann) -> [Sem r (Doc ann)] -> Sem r [Sem r (Doc ann)]
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> [f (Doc ann)] -> f [f (Doc ann)]
punctuate (Doc ann -> Sem r (Doc ann)
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc ann
",") (((Value, Integer) -> Sem r (Doc ann))
-> [(Value, Integer)] -> [Sem r (Doc ann)]
forall a b. (a -> b) -> [a] -> [b]
map (Value, Integer) -> Sem r (Doc ann)
prettyCount [(Value, Integer)]
vs)
 where
  prettyCount :: (Value, Integer) -> Sem r (Doc ann)
prettyCount (Value
v, Integer
1) = Type -> Value -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r (Doc ann)
prettyValue Type
ty Value
v
  prettyCount (Value
v, Integer
n) = Type -> Value -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r (Doc ann)
prettyValue Type
ty Value
v Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"#" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (Integer -> String
forall a. Show a => a -> String
show Integer
n)