{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
module Disco.Value (
Value (.., VNil, VCons, VFun),
SimpleValue (..),
toSimpleValue,
fromSimpleValue,
ratv,
vrat,
intv,
vint,
charv,
vchar,
enumv,
pairv,
vpair,
listv,
vlist,
ValProp (..),
TestResult (..),
TestReason_ (..),
TestReason,
SearchType (..),
SearchMotive (.., SMExists, SMForall),
TestVars (..),
TestEnv (..),
emptyTestEnv,
getTestEnv,
extendPropEnv,
extendResultEnv,
testIsOk,
testIsError,
testReason,
testEnv,
resultIsCertain,
LOp (..),
interpLOp,
Env,
Cell (..),
Mem,
emptyMem,
allocate,
allocateRec,
lkup,
set,
prettyValue',
prettyValue,
) 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.Context as Ctx
import Disco.Error
import Disco.Names
import Disco.Pretty
import Disco.Syntax.Operators (BOp (Add, Mul))
import Disco.Types
import Disco.Effects.LFresh
import Polysemy
import Polysemy.Input
import Polysemy.Reader
import Polysemy.State
import Unbound.Generics.LocallyNameless (Name)
data Value where
VNum :: RationalDisplay -> Rational -> Value
VConst :: Op -> Value
VInj :: Side -> Value -> Value
VUnit :: Value
VPair :: Value -> Value -> Value
VClo :: Env -> [Name Core] -> Core -> Value
VType :: Type -> Value
VRef :: Int -> Value
VFun_ :: ValFun -> Value
VProp :: ValProp -> Value
VBag :: [(Value, Integer)] -> Value
VGraph :: Graph SimpleValue -> Value
VMap :: Map SimpleValue Value -> Value
deriving (Int -> Value -> ShowS
[Value] -> ShowS
Value -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Value] -> ShowS
$cshowList :: [Value] -> ShowS
show :: Value -> [Char]
$cshow :: Value -> [Char]
showsPrec :: Int -> Value -> ShowS
$cshowsPrec :: Int -> Value -> ShowS
Show)
pattern VNil :: Value
pattern $bVNil :: Value
$mVNil :: forall {r}. Value -> ((# #) -> r) -> ((# #) -> r) -> r
VNil = VInj L VUnit
pattern VCons :: Value -> Value -> Value
pattern $bVCons :: Value -> Value -> Value
$mVCons :: forall {r}. Value -> (Value -> Value -> r) -> ((# #) -> r) -> r
VCons h t = VInj R (VPair h t)
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 -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [SimpleValue] -> ShowS
$cshowList :: [SimpleValue] -> ShowS
show :: SimpleValue -> [Char]
$cshow :: SimpleValue -> [Char]
showsPrec :: Int -> SimpleValue -> ShowS
$cshowsPrec :: Int -> SimpleValue -> ShowS
Show, SimpleValue -> SimpleValue -> Bool
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
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
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 (forall a b. (a -> b) -> [a] -> [b]
map (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 -> forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"A non-simple value was passed as simple: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
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 forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (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
newtype ValFun = ValFun (Value -> Value)
instance Show ValFun where
show :: ValFun -> [Char]
show ValFun
_ = [Char]
"<fun>"
pattern VFun :: (Value -> Value) -> Value
pattern $bVFun :: (Value -> Value) -> Value
$mVFun :: forall {r}. Value -> ((Value -> Value) -> r) -> ((# #) -> r) -> r
VFun f = VFun_ (ValFun f)
ratv :: Rational -> Value
ratv :: Rational -> Value
ratv = RationalDisplay -> Rational -> Value
VNum forall a. Monoid a => a
mempty
vrat :: Value -> Rational
vrat :: Value -> Rational
vrat (VNum RationalDisplay
_ Rational
r) = Rational
r
vrat Value
v = forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"vrat " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Value
v
intv :: Integer -> Value
intv :: Integer -> Value
intv = Rational -> Value
ratv forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Integral a => a -> a -> Ratio a
% Integer
1)
vint :: Value -> Integer
vint :: Value -> Integer
vint (VNum RationalDisplay
_ Rational
n) = forall a. Ratio a -> a
numerator Rational
n
vint Value
v = forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"vint " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Value
v
vchar :: Value -> Char
vchar :: Value -> Char
vchar = Int -> Char
chr forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Integer
vint
charv :: Char -> Value
charv :: Char -> Value
charv = Integer -> Value
intv forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Int
ord
enumv :: Enum e => e -> Value
enumv :: forall e. Enum e => e -> Value
enumv e
e = Side -> Value -> Value
VInj (forall a. Enum a => Int -> a
toEnum forall a b. (a -> b) -> a -> b
$ forall a. Enum a => a -> Int
fromEnum e
e) Value
VUnit
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 = forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"vpair " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
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) (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 forall a. a -> [a] -> [a]
: forall a. (Value -> a) -> Value -> [a]
vlist Value -> a
velt Value
vs
vlist Value -> a
_ Value
v = forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"vlist " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Value
v
data SearchType
=
Exhaustive
|
Randomized Integer Integer
deriving (Int -> SearchType -> ShowS
[SearchType] -> ShowS
SearchType -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [SearchType] -> ShowS
$cshowList :: [SearchType] -> ShowS
show :: SearchType -> [Char]
$cshow :: SearchType -> [Char]
showsPrec :: Int -> SearchType -> ShowS
$cshowsPrec :: Int -> SearchType -> ShowS
Show)
newtype SearchMotive = SearchMotive (Bool, Bool)
deriving (Int -> SearchMotive -> ShowS
[SearchMotive] -> ShowS
SearchMotive -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [SearchMotive] -> ShowS
$cshowList :: [SearchMotive] -> ShowS
show :: SearchMotive -> [Char]
$cshow :: SearchMotive -> [Char]
showsPrec :: Int -> SearchMotive -> ShowS
$cshowsPrec :: Int -> SearchMotive -> ShowS
Show)
pattern SMForall :: SearchMotive
pattern $bSMForall :: SearchMotive
$mSMForall :: forall {r}. SearchMotive -> ((# #) -> r) -> ((# #) -> r) -> r
SMForall = SearchMotive (False, False)
pattern SMExists :: SearchMotive
pattern $bSMExists :: SearchMotive
$mSMExists :: forall {r}. SearchMotive -> ((# #) -> r) -> ((# #) -> r) -> r
SMExists = SearchMotive (True, True)
newtype TestVars = TestVars [(String, Type, Name Core)]
deriving newtype (Int -> TestVars -> ShowS
[TestVars] -> ShowS
TestVars -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [TestVars] -> ShowS
$cshowList :: [TestVars] -> ShowS
show :: TestVars -> [Char]
$cshow :: TestVars -> [Char]
showsPrec :: Int -> TestVars -> ShowS
$cshowsPrec :: Int -> TestVars -> ShowS
Show, NonEmpty TestVars -> TestVars
TestVars -> TestVars -> 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 :: forall b. Integral b => 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
[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
Monoid)
newtype TestEnv = TestEnv [(String, Type, Value)]
deriving newtype (Int -> TestEnv -> ShowS
[TestEnv] -> ShowS
TestEnv -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [TestEnv] -> ShowS
$cshowList :: [TestEnv] -> ShowS
show :: TestEnv -> [Char]
$cshow :: TestEnv -> [Char]
showsPrec :: Int -> TestEnv -> ShowS
$cshowsPrec :: Int -> TestEnv -> ShowS
Show, NonEmpty TestEnv -> TestEnv
TestEnv -> TestEnv -> 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 :: forall b. Integral b => 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
[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
Monoid)
emptyTestEnv :: TestEnv
emptyTestEnv :: TestEnv
emptyTestEnv = [([Char], Type, Value)] -> TestEnv
TestEnv []
getTestEnv :: TestVars -> Env -> Either EvalError TestEnv
getTestEnv :: TestVars -> Env -> Either EvalError TestEnv
getTestEnv (TestVars [([Char], Type, Name Core)]
tvs) Env
e = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [([Char], Type, Value)] -> TestEnv
TestEnv forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [([Char], Type, Name Core)]
tvs forall a b. (a -> b) -> a -> b
$ \([Char]
s, Type
ty, Name Core
name) -> do
let value :: Maybe Value
value = forall a b. QName a -> Ctx a b -> Maybe b
Ctx.lookup' (forall a. Name a -> QName a
localName Name Core
name) Env
e
case Maybe Value
value of
Just Value
v -> forall (m :: * -> *) a. Monad m => a -> m a
return ([Char]
s, Type
ty, Value
v)
Maybe Value
Nothing -> forall a b. a -> Either a b
Left (forall core. Name core -> EvalError
UnboundPanic Name Core
name)
data LOp = LAnd | LOr | LImpl deriving (LOp -> LOp -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LOp -> LOp -> Bool
$c/= :: LOp -> LOp -> Bool
== :: LOp -> LOp -> Bool
$c== :: LOp -> LOp -> Bool
Eq, Eq 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
min :: LOp -> LOp -> LOp
$cmin :: LOp -> LOp -> LOp
max :: LOp -> LOp -> LOp
$cmax :: LOp -> LOp -> LOp
>= :: LOp -> LOp -> Bool
$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
compare :: LOp -> LOp -> Ordering
$ccompare :: LOp -> LOp -> Ordering
Ord, Int -> LOp -> ShowS
[LOp] -> ShowS
LOp -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [LOp] -> ShowS
$cshowList :: [LOp] -> ShowS
show :: LOp -> [Char]
$cshow :: LOp -> [Char]
showsPrec :: Int -> LOp -> ShowS
$cshowsPrec :: Int -> LOp -> ShowS
Show, Int -> LOp
LOp -> Int
LOp -> [LOp]
LOp -> LOp
LOp -> LOp -> [LOp]
LOp -> LOp -> LOp -> [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
enumFromThenTo :: LOp -> LOp -> LOp -> [LOp]
$cenumFromThenTo :: LOp -> LOp -> LOp -> [LOp]
enumFromTo :: LOp -> LOp -> [LOp]
$cenumFromTo :: LOp -> LOp -> [LOp]
enumFromThen :: LOp -> LOp -> [LOp]
$cenumFromThen :: LOp -> LOp -> [LOp]
enumFrom :: LOp -> [LOp]
$cenumFrom :: LOp -> [LOp]
fromEnum :: LOp -> Int
$cfromEnum :: LOp -> Int
toEnum :: Int -> LOp
$ctoEnum :: Int -> LOp
pred :: LOp -> LOp
$cpred :: LOp -> LOp
succ :: LOp -> LOp
$csucc :: LOp -> LOp
Enum, LOp
forall a. a -> a -> Bounded a
maxBound :: LOp
$cmaxBound :: LOp
minBound :: LOp
$cminBound :: 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
data TestReason_ a
=
TestBool
|
TestEqual Type a a
|
TestLt Type a a
|
TestNotFound SearchType
|
TestFound TestResult
|
TestBin LOp TestResult TestResult
|
TestRuntimeError EvalError
deriving (Int -> TestReason_ a -> ShowS
forall a. Show a => Int -> TestReason_ a -> ShowS
forall a. Show a => [TestReason_ a] -> ShowS
forall a. Show a => TestReason_ a -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [TestReason_ a] -> ShowS
$cshowList :: forall a. Show a => [TestReason_ a] -> ShowS
show :: TestReason_ a -> [Char]
$cshow :: forall a. Show a => TestReason_ a -> [Char]
showsPrec :: Int -> TestReason_ a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> TestReason_ a -> ShowS
Show, 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
<$ :: forall a b. a -> TestReason_ b -> TestReason_ a
$c<$ :: forall a b. a -> TestReason_ b -> TestReason_ a
fmap :: forall a b. (a -> b) -> TestReason_ a -> TestReason_ b
$cfmap :: forall a b. (a -> b) -> TestReason_ a -> TestReason_ b
Functor, 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 :: forall a. Num a => TestReason_ a -> a
$cproduct :: forall a. Num a => TestReason_ a -> a
sum :: forall a. Num a => TestReason_ a -> a
$csum :: forall a. Num a => TestReason_ a -> a
minimum :: forall a. Ord a => TestReason_ a -> a
$cminimum :: forall a. Ord a => TestReason_ a -> a
maximum :: forall a. Ord a => TestReason_ a -> a
$cmaximum :: forall a. Ord a => TestReason_ a -> a
elem :: forall a. Eq a => a -> TestReason_ a -> Bool
$celem :: forall a. Eq a => a -> TestReason_ a -> Bool
length :: forall a. TestReason_ a -> Int
$clength :: forall a. TestReason_ a -> Int
null :: forall a. TestReason_ a -> Bool
$cnull :: forall a. TestReason_ a -> Bool
toList :: forall a. TestReason_ a -> [a]
$ctoList :: forall a. TestReason_ a -> [a]
foldl1 :: forall a. (a -> a -> a) -> TestReason_ a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> TestReason_ a -> a
foldr1 :: forall a. (a -> a -> a) -> TestReason_ a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> TestReason_ a -> a
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
$cfoldl :: forall b a. (b -> a -> 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
$cfoldr :: forall a b. (a -> b -> b) -> b -> TestReason_ a -> b
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
$cfoldMap :: forall m a. Monoid m => (a -> m) -> TestReason_ a -> m
fold :: forall m. Monoid m => TestReason_ m -> m
$cfold :: forall m. Monoid m => TestReason_ m -> m
Foldable, Functor TestReason_
Foldable 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)
sequence :: forall (m :: * -> *) a.
Monad m =>
TestReason_ (m a) -> m (TestReason_ a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
TestReason_ (m a) -> m (TestReason_ a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TestReason_ a -> m (TestReason_ b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TestReason_ a -> m (TestReason_ b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
TestReason_ (f a) -> f (TestReason_ a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
TestReason_ (f a) -> f (TestReason_ a)
traverse :: 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)
Traversable)
type TestReason = TestReason_ Value
data TestResult = TestResult Bool TestReason TestEnv
deriving (Int -> TestResult -> ShowS
[TestResult] -> ShowS
TestResult -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [TestResult] -> ShowS
$cshowList :: [TestResult] -> ShowS
show :: TestResult -> [Char]
$cshow :: TestResult -> [Char]
showsPrec :: Int -> TestResult -> ShowS
$cshowsPrec :: Int -> TestResult -> ShowS
Show)
testIsError :: TestResult -> Bool
testIsError :: TestResult -> Bool
testIsError (TestResult Bool
_ (TestRuntimeError EvalError
_) TestEnv
_) = Bool
True
testIsError TestResult
_ = Bool
False
testIsOk :: TestResult -> Bool
testIsOk :: TestResult -> Bool
testIsOk (TestResult Bool
b TestReason
_ TestEnv
_) = Bool
b
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 TestEqual {} = Bool
True
resultIsCertain TestLt {} = 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 EvalError
_) = 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 forall a. Eq a => a -> a -> Bool
== LOp
LOr) forall a. Eq a => a -> a -> Bool
== Bool
ok1) = Bool
True
| Bool
c2 Bool -> Bool -> Bool
&& ((LOp
op forall a. Eq a => a -> a -> Bool
/= LOp
LAnd) 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
data ValProp
=
VPDone TestResult
|
VPSearch SearchMotive [Type] Value TestEnv
|
VPBin LOp ValProp ValProp
deriving (Int -> ValProp -> ShowS
[ValProp] -> ShowS
ValProp -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [ValProp] -> ShowS
$cshowList :: [ValProp] -> ShowS
show :: ValProp -> [Char]
$cshow :: ValProp -> [Char]
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
r TestEnv
e)) = TestResult -> ValProp
VPDone (Bool -> TestReason -> TestEnv -> TestResult
TestResult Bool
b TestReason
r (TestEnv
g 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 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 forall a. Semigroup a => a -> a -> a
P.<> TestEnv
e)
type Env = Ctx Core Value
data Mem = Mem {Mem -> Int
next :: Int, Mem -> IntMap Cell
mu :: IntMap Cell} deriving (Int -> Mem -> ShowS
[Mem] -> ShowS
Mem -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Mem] -> ShowS
$cshowList :: [Mem] -> ShowS
show :: Mem -> [Char]
$cshow :: Mem -> [Char]
showsPrec :: Int -> Mem -> ShowS
$cshowsPrec :: Int -> Mem -> ShowS
Show)
data Cell = Blackhole | E Env Core | V Value deriving (Int -> Cell -> ShowS
[Cell] -> ShowS
Cell -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Cell] -> ShowS
$cshowList :: [Cell] -> ShowS
show :: Cell -> [Char]
$cshow :: Cell -> [Char]
showsPrec :: Int -> Cell -> ShowS
$cshowsPrec :: Int -> Cell -> ShowS
Show)
emptyMem :: Mem
emptyMem :: Mem
emptyMem = Int -> IntMap Cell -> Mem
Mem Int
0 forall a. IntMap a
IM.empty
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 <- forall s (r :: EffectRow). Member (State s) r => Sem r s
get
forall s (r :: EffectRow). Member (State s) r => s -> Sem r ()
put forall a b. (a -> b) -> a -> b
$ Int -> IntMap Cell -> Mem
Mem (Int
n forall a. Num a => a -> a -> a
+ Int
1) (forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
n (Env -> Core -> Cell
E Env
e Core
t) IntMap Cell
m)
forall (m :: * -> *) a. Monad m => a -> m a
return Int
n
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 <- forall s (r :: EffectRow). Member (State s) r => Sem r s
get
let newRefs :: [(Int, (QName Core, Core))]
newRefs = forall a b. [a] -> [b] -> [(a, b)]
zip [Int
n ..] [(QName Core, Core)]
bs
e' :: Env
e' = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (forall a b c. (a -> b -> c) -> b -> a -> c
flip (\(Int
i, (QName Core
x, Core
_)) -> 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' = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (forall a b c. (a -> b -> c) -> b -> a -> c
flip (\(Int
i, (QName Core
_, Core
c)) -> 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 forall a. Num a => a -> a -> a
+ forall (t :: * -> *) a. Foldable t => t a -> Int
length [(QName Core, Core)]
bs
forall s (r :: EffectRow). Member (State s) r => s -> Sem r ()
put forall a b. (a -> b) -> a -> b
$ Int -> IntMap Cell -> Mem
Mem Int
n' IntMap Cell
m'
forall (m :: * -> *) a. Monad m => a -> m a
return [Int
n .. Int
n' forall a. Num a => a -> a -> a
- Int
1]
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 = forall s a (r :: EffectRow).
Member (State s) r =>
(s -> a) -> Sem r a
gets (forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mem -> IntMap Cell
mu)
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 = forall s (r :: EffectRow).
Member (State s) r =>
(s -> s) -> Sem r ()
modify forall a b. (a -> b) -> a -> b
$ \(Mem Int
nxt IntMap Cell
m) -> Int -> IntMap Cell -> Mem
Mem Int
nxt (forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
n Cell
c IntMap Cell
m)
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 = forall (r :: EffectRow) a. Sem (LFresh : r) a -> Sem r a
runLFresh forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall i (r :: EffectRow) a. i -> Sem (Reader i : r) a -> Sem r a
runReader PA
initPA forall a b. (a -> b) -> a -> b
$ 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)
prettyValue :: forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r (Doc ann)
prettyValue (TyUser [Char]
x [Type]
args) Value
v = do
TyDefCtx
tydefs <- forall i (r :: EffectRow). Member (Input i) r => Sem r i
input
let (TyDefBody [[Char]]
_ [Type] -> Type
body) = TyDefCtx
tydefs forall k a. Ord k => Map k a -> k -> a
M.! [Char]
x
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
_ = forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Type -> Sem r (Doc ann)
prettyPlaceholder Type
TyProp
prettyValue Type
TyBool (VInj Side
s Value
_) = forall (m :: * -> *) ann. Applicative m => [Char] -> m (Doc ann)
text forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (forall a. Show a => a -> [Char]
show (Side
s forall a. Eq a => a -> a -> Bool
== Side
R))
prettyValue Type
TyBool Value
v =
forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"Non-VInj passed with Bool type to prettyValue: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Value
v
prettyValue Type
TyC (Value -> Char
vchar -> Char
c) = forall (m :: * -> *) ann. Applicative m => [Char] -> m (Doc ann)
text (forall a. Show a => a -> [Char]
show Char
c)
prettyValue (TyList Type
TyC) (forall a. (Value -> a) -> Value -> [a]
vlist Value -> Char
vchar -> [Char]
cs) = forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
doubleQuotes forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) ann. Applicative m => [Char] -> m (Doc ann)
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Char -> [Char]
prettyChar forall a b. (a -> b) -> a -> b
$ [Char]
cs
where
prettyChar :: Char -> [Char]
prettyChar = forall a. Int -> [a] -> [a]
drop Int
1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
reverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Int -> [a] -> [a]
drop Int
1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
reverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. a -> [a] -> [a]
: [])
prettyValue (TyList Type
ty) (forall a. (Value -> a) -> Value -> [a]
vlist forall a. a -> a
id -> [Value]
xs) = do
[Sem r (Doc ann)]
ds <- forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> [f (Doc ann)] -> f [f (Doc ann)]
punctuate (forall (m :: * -> *) ann. Applicative m => [Char] -> m (Doc ann)
text [Char]
",") (forall a b. (a -> b) -> [a] -> [b]
map (forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r (Doc ann)
prettyValue Type
ty) [Value]
xs)
forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
brackets (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 = forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
parens (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" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (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" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (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 =
forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"Non-VInj passed with sum type to prettyValue: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Value
v
prettyValue Type
_ (VNum RationalDisplay
d Rational
r)
| forall a. Ratio a -> a
denominator Rational
r forall a. Eq a => a -> a -> Bool
== Integer
1 = forall (m :: * -> *) ann. Applicative m => [Char] -> m (Doc ann)
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> [Char]
show (forall a. Ratio a -> a
numerator Rational
r)
| Bool
otherwise = forall (m :: * -> *) ann. Applicative m => [Char] -> m (Doc ann)
text forall a b. (a -> b) -> a -> b
$ case RationalDisplay
d of
RationalDisplay
Fraction -> forall a. Show a => a -> [Char]
show (forall a. Ratio a -> a
numerator Rational
r) forall a. [a] -> [a] -> [a]
++ [Char]
"/" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall a. Ratio a -> a
denominator Rational
r)
RationalDisplay
Decimal -> Rational -> [Char]
prettyDecimal Rational
r
prettyValue ty :: Type
ty@(Type
_ :->: Type
_) Value
_ = 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) = forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
braces forall a b. (a -> b) -> a -> b
$ forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Doc ann -> [Value] -> Sem r (Doc ann)
prettySequence Type
ty Doc ann
"," (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Value, Integer)]
xs)
prettyValue (TySet Type
_) Value
v =
forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"Non-VBag passed with Set type to prettyValue: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Value
v
prettyValue (TyBag Type
ty) (VBag [(Value, Integer)]
xs) = 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 =
forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"Non-VBag passed with Bag type to prettyValue: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Value
v
prettyValue (TyMap Type
tyK Type
tyV) (VMap Map SimpleValue Value
m) =
Sem r (Doc ann)
"map" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
parens (forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
braces (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 = forall a b. (a -> b) -> [a] -> [b]
map (\(SimpleValue
k, Value
v) -> Value -> Value -> Value
VPair (SimpleValue -> Value
fromSimpleValue SimpleValue
k) Value
v) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [(k, a)]
M.assocs
prettyValue (TyMap Type
_ Type
_) Value
v =
forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"Non-map value with map type passed to prettyValue: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Value
v
prettyValue (TyGraph Type
ty) (VGraph Graph SimpleValue
g) =
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" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r (Doc ann)
prettyVP Type
ty forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleValue -> Value
fromSimpleValue)
(\Sem r (Doc ann)
l Sem r (Doc ann)
r -> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA (BOp -> PA
getPA BOp
Add) forall a b. (a -> b) -> a -> b
$ forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt Sem r (Doc ann)
l forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"+" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (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 -> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA (BOp -> PA
getPA BOp
Mul) forall a b. (a -> b) -> a -> b
$ forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt Sem r (Doc ann)
l forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"*" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (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 =
forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"Non-graph value with graph type passed to prettyValue: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Value
v
prettyValue ty :: Type
ty@TyAtom {} Value
v =
forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"Invalid atomic type passed to prettyValue: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Type
ty forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Value
v
prettyValue ty :: Type
ty@TyCon {} Value
v =
forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"Invalid type constructor passed to prettyValue: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Type
ty forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Value
v
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
_) = forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r (Doc ann)
prettyValue Type
ty
prettyVP Type
ty = forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
parens forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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)
"<" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Type
ty 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) = forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r (Doc ann)
prettyValue Type
ty1 Value
v1 forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
"," forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (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 = forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r (Doc ann)
prettyValue Type
ty Value
v
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 = forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> [f (Doc ann)] -> f [f (Doc ann)]
punctuate (forall (m :: * -> *) a. Monad m => a -> m a
return Doc ann
del) (forall a b. (a -> b) -> [a] -> [b]
map (forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r (Doc ann)
prettyValue Type
ty) [Value]
vs)
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
_ [] = forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann)
bag forall (m :: * -> *) ann. Applicative m => m (Doc ann)
empty
prettyBag Type
ty [(Value, Integer)]
vs
| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((forall a. Eq a => a -> a -> Bool
== Integer
1) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(Value, Integer)]
vs = forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann)
bag forall a b. (a -> b) -> a -> b
$ forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Doc ann -> [Value] -> Sem r (Doc ann)
prettySequence Type
ty Doc ann
"," (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Value, Integer)]
vs)
| Bool
otherwise = forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann)
bag forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> [f (Doc ann)] -> f [f (Doc ann)]
punctuate (forall (m :: * -> *) a. Monad m => a -> m a
return 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) = 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) = forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r (Doc ann)
prettyValue Type
ty Value
v forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"#" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (m :: * -> *) ann. Applicative m => [Char] -> m (Doc ann)
text (forall a. Show a => a -> [Char]
show Integer
n)