{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -fmax-pmcheck-models=200 #-}
module Disco.Interpret.CESK (
CESK,
runCESK,
step,
eval,
runTest,
)
where
import Unbound.Generics.LocallyNameless (Bind, Name)
import Algebra.Graph
import qualified Algebra.Graph.AdjacencyMap as AdjMap
import Control.Arrow ((***), (>>>))
import Control.Monad ((>=>))
import Data.Bifunctor (first, second)
import Data.List (find)
import qualified Data.Map as M
import Data.Maybe (isJust)
import Data.Ratio
import Disco.AST.Core
import Disco.AST.Generic (
Ellipsis (..),
Side (..),
selectSide,
)
import Disco.AST.Typed (AProperty)
import Disco.Compile
import Disco.Context as Ctx
import Disco.Enumerate
import Disco.Error
import Disco.Names
import Disco.Property
import Disco.Types hiding (V)
import Disco.Value
import Math.Combinatorics.Exact.Binomial (choose)
import Math.Combinatorics.Exact.Factorial (factorial)
import Math.NumberTheory.Primes (factorise, unPrime)
import Math.NumberTheory.Primes.Testing (isPrime)
import Disco.Effects.Fresh
import Disco.Effects.Input
import Disco.Effects.Random
import Polysemy
import Polysemy.Error
import Polysemy.State
type Cont = [Frame]
data Frame
=
FInj Side
|
FCase Env (Bind (Name Core) Core) (Bind (Name Core) Core)
|
FPairR Env Core
|
FPairL Value
|
FProj Side
|
FArg Env Core
|
FArgV Value
|
FApp Value
|
FForce
|
FUpdate Int
|
FTest TestVars Env
deriving (Int -> Frame -> ShowS
[Frame] -> ShowS
Frame -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Frame] -> ShowS
$cshowList :: [Frame] -> ShowS
show :: Frame -> String
$cshow :: Frame -> String
showsPrec :: Int -> Frame -> ShowS
$cshowsPrec :: Int -> Frame -> ShowS
Show)
data CESK
=
In Core Env Cont
|
Out Value Cont
|
Up EvalError Cont
deriving (Int -> CESK -> ShowS
[CESK] -> ShowS
CESK -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CESK] -> ShowS
$cshowList :: [CESK] -> ShowS
show :: CESK -> String
$cshow :: CESK -> String
showsPrec :: Int -> CESK -> ShowS
$cshowsPrec :: Int -> CESK -> ShowS
Show)
isFinal :: CESK -> Maybe (Either EvalError Value)
isFinal :: CESK -> Maybe (Either EvalError Value)
isFinal (Up EvalError
e []) = forall a. a -> Maybe a
Just (forall a b. a -> Either a b
Left EvalError
e)
isFinal (Out Value
v []) = forall a. a -> Maybe a
Just (forall a b. b -> Either a b
Right Value
v)
isFinal CESK
_ = forall a. Maybe a
Nothing
runCESK :: Members '[Fresh, Random, State Mem] r => CESK -> Sem r (Either EvalError Value)
runCESK :: forall (r :: EffectRow).
Members '[Fresh, Random, State Mem] r =>
CESK -> Sem r (Either EvalError Value)
runCESK CESK
cesk = case CESK -> Maybe (Either EvalError Value)
isFinal CESK
cesk of
Just Either EvalError Value
res -> forall (m :: * -> *) a. Monad m => a -> m a
return Either EvalError Value
res
Maybe (Either EvalError Value)
Nothing -> forall (r :: EffectRow).
Members '[Fresh, Random, State Mem] r =>
CESK -> Sem r CESK
step CESK
cesk forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (r :: EffectRow).
Members '[Fresh, Random, State Mem] r =>
CESK -> Sem r (Either EvalError Value)
runCESK
step :: Members '[Fresh, Random, State Mem] r => CESK -> Sem r CESK
step :: forall (r :: EffectRow).
Members '[Fresh, Random, State Mem] r =>
CESK -> Sem r CESK
step CESK
cesk = case CESK
cesk of
(In (CVar QName Core
x) Env
e [Frame]
k) -> case forall a b. QName a -> Ctx a b -> Maybe b
Ctx.lookup' QName Core
x Env
e of
Maybe Value
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ EvalError -> [Frame] -> CESK
Up (forall core. QName core -> EvalError
UnboundError QName Core
x) [Frame]
k
Just Value
v -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Value -> [Frame] -> CESK
Out Value
v [Frame]
k
(In (CNum RationalDisplay
d Rational
r) Env
_ [Frame]
k) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Value -> [Frame] -> CESK
Out (RationalDisplay -> Rational -> Value
VNum RationalDisplay
d Rational
r) [Frame]
k
(In (CConst Op
OMatchErr) Env
_ [Frame]
k) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ EvalError -> [Frame] -> CESK
Up EvalError
NonExhaustive [Frame]
k
(In (CConst Op
OEmptyGraph) Env
_ [Frame]
k) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Value -> [Frame] -> CESK
Out (Graph SimpleValue -> Value
VGraph forall a. Graph a
empty) [Frame]
k
(In (CConst Op
op) Env
_ [Frame]
k) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Value -> [Frame] -> CESK
Out (Op -> Value
VConst Op
op) [Frame]
k
(In (CInj Side
s Core
c) Env
e [Frame]
k) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Core -> Env -> [Frame] -> CESK
In Core
c Env
e (Side -> Frame
FInj Side
s forall a. a -> [a] -> [a]
: [Frame]
k)
(In (CCase Core
c Bind (Name Core) Core
b1 Bind (Name Core) Core
b2) Env
e [Frame]
k) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Core -> Env -> [Frame] -> CESK
In Core
c Env
e (Env -> Bind (Name Core) Core -> Bind (Name Core) Core -> Frame
FCase Env
e Bind (Name Core) Core
b1 Bind (Name Core) Core
b2 forall a. a -> [a] -> [a]
: [Frame]
k)
(In Core
CUnit Env
_ [Frame]
k) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Value -> [Frame] -> CESK
Out Value
VUnit [Frame]
k
(In (CPair Core
c1 Core
c2) Env
e [Frame]
k) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Core -> Env -> [Frame] -> CESK
In Core
c1 Env
e (Env -> Core -> Frame
FPairR Env
e Core
c2 forall a. a -> [a] -> [a]
: [Frame]
k)
(In (CProj Side
s Core
c) Env
e [Frame]
k) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Core -> Env -> [Frame] -> CESK
In Core
c Env
e (Side -> Frame
FProj Side
s forall a. a -> [a] -> [a]
: [Frame]
k)
(In (CAbs Bind [Name Core] Core
b) Env
e [Frame]
k) -> do
([Name Core]
xs, Core
body) <- forall (r :: EffectRow) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind Bind [Name Core] Core
b
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Value -> [Frame] -> CESK
Out (Env -> [Name Core] -> Core -> Value
VClo Env
e [Name Core]
xs Core
body) [Frame]
k
(In (CApp Core
c1 Core
c2) Env
e [Frame]
k) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Core -> Env -> [Frame] -> CESK
In Core
c1 Env
e (Env -> Core -> Frame
FArg Env
e Core
c2 forall a. a -> [a] -> [a]
: [Frame]
k)
(In (CType Type
ty) Env
_ [Frame]
k) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Value -> [Frame] -> CESK
Out (Type -> Value
VType Type
ty) [Frame]
k
(In (CDelay Bind [Name Core] [Core]
b) Env
e [Frame]
k) -> do
([Name Core]
xs, [Core]
cs) <- forall (r :: EffectRow) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind Bind [Name Core] [Core]
b
[Int]
locs <- forall (r :: EffectRow).
Members '[State Mem] r =>
Env -> [(QName Core, Core)] -> Sem r [Int]
allocateRec Env
e (forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a -> b) -> [a] -> [b]
map forall a. Name a -> QName a
localName [Name Core]
xs) [Core]
cs)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Value -> [Frame] -> CESK
Out (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Value -> Value -> Value
VPair forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Value
VRef) Value
VUnit [Int]
locs) [Frame]
k
(In (CForce Core
c) Env
e [Frame]
k) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Core -> Env -> [Frame] -> CESK
In Core
c Env
e (Frame
FForce forall a. a -> [a] -> [a]
: [Frame]
k)
(In (CTest [(String, Type, Name Core)]
vars Core
c) Env
e [Frame]
k) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Core -> Env -> [Frame] -> CESK
In Core
c Env
e (TestVars -> Env -> Frame
FTest ([(String, Type, Name Core)] -> TestVars
TestVars [(String, Type, Name Core)]
vars) Env
e forall a. a -> [a] -> [a]
: [Frame]
k)
(Out Value
v (FInj Side
s : [Frame]
k)) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Value -> [Frame] -> CESK
Out (Side -> Value -> Value
VInj Side
s Value
v) [Frame]
k
(Out (VInj Side
L Value
v) (FCase Env
e Bind (Name Core) Core
b1 Bind (Name Core) Core
_ : [Frame]
k)) -> do
(Name Core
x, Core
c1) <- forall (r :: EffectRow) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind Bind (Name Core) Core
b1
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Core -> Env -> [Frame] -> CESK
In Core
c1 (forall a b. QName a -> b -> Ctx a b -> Ctx a b
Ctx.insert (forall a. Name a -> QName a
localName Name Core
x) Value
v Env
e) [Frame]
k
(Out (VInj Side
R Value
v) (FCase Env
e Bind (Name Core) Core
_ Bind (Name Core) Core
b2 : [Frame]
k)) -> do
(Name Core
x, Core
c2) <- forall (r :: EffectRow) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind Bind (Name Core) Core
b2
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Core -> Env -> [Frame] -> CESK
In Core
c2 (forall a b. QName a -> b -> Ctx a b -> Ctx a b
Ctx.insert (forall a. Name a -> QName a
localName Name Core
x) Value
v Env
e) [Frame]
k
(Out Value
v1 (FPairR Env
e Core
c2 : [Frame]
k)) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Core -> Env -> [Frame] -> CESK
In Core
c2 Env
e (Value -> Frame
FPairL Value
v1 forall a. a -> [a] -> [a]
: [Frame]
k)
(Out Value
v2 (FPairL Value
v1 : [Frame]
k)) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Value -> [Frame] -> CESK
Out (Value -> Value -> Value
VPair Value
v1 Value
v2) [Frame]
k
(Out (VPair Value
v1 Value
v2) (FProj Side
s : [Frame]
k)) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Value -> [Frame] -> CESK
Out (forall a. Side -> a -> a -> a
selectSide Side
s Value
v1 Value
v2) [Frame]
k
(Out Value
v (FArg Env
e Core
c2 : [Frame]
k)) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Core -> Env -> [Frame] -> CESK
In Core
c2 Env
e (Value -> Frame
FApp Value
v forall a. a -> [a] -> [a]
: [Frame]
k)
(Out Value
v2 (FApp (VClo Env
e [Name Core
x] Core
b) : [Frame]
k)) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Core -> Env -> [Frame] -> CESK
In Core
b (forall a b. QName a -> b -> Ctx a b -> Ctx a b
Ctx.insert (forall a. Name a -> QName a
localName Name Core
x) Value
v2 Env
e) [Frame]
k
(Out Value
v2 (FApp (VClo Env
e (Name Core
x : [Name Core]
xs) Core
b) : [Frame]
k)) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Value -> [Frame] -> CESK
Out (Env -> [Name Core] -> Core -> Value
VClo (forall a b. QName a -> b -> Ctx a b -> Ctx a b
Ctx.insert (forall a. Name a -> QName a
localName Name Core
x) Value
v2 Env
e) [Name Core]
xs Core
b) [Frame]
k
(Out Value
v2 (FApp (VConst Op
op) : [Frame]
k)) -> forall (r :: EffectRow).
Members '[Random, State Mem] r =>
[Frame] -> Op -> Value -> Sem r CESK
appConst [Frame]
k Op
op Value
v2
(Out Value
v2 (FApp (VFun Value -> Value
f) : [Frame]
k)) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Value -> [Frame] -> CESK
Out (Value -> Value
f Value
v2) [Frame]
k
(Out (VClo Env
e [Name Core
x] Core
b) (FArgV Value
v : [Frame]
k)) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Core -> Env -> [Frame] -> CESK
In Core
b (forall a b. QName a -> b -> Ctx a b -> Ctx a b
Ctx.insert (forall a. Name a -> QName a
localName Name Core
x) Value
v Env
e) [Frame]
k
(Out (VClo Env
e (Name Core
x : [Name Core]
xs) Core
b) (FArgV Value
v : [Frame]
k)) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Value -> [Frame] -> CESK
Out (Env -> [Name Core] -> Core -> Value
VClo (forall a b. QName a -> b -> Ctx a b -> Ctx a b
Ctx.insert (forall a. Name a -> QName a
localName Name Core
x) Value
v Env
e) [Name Core]
xs Core
b) [Frame]
k
(Out (VConst Op
op) (FArgV Value
v : [Frame]
k)) -> forall (r :: EffectRow).
Members '[Random, State Mem] r =>
[Frame] -> Op -> Value -> Sem r CESK
appConst [Frame]
k Op
op Value
v
(Out (VFun Value -> Value
f) (FArgV Value
v : [Frame]
k)) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Value -> [Frame] -> CESK
Out (Value -> Value
f Value
v) [Frame]
k
(Out (VRef Int
n) (Frame
FForce : [Frame]
k)) -> do
Maybe Cell
cell <- forall (r :: EffectRow).
Members '[State Mem] r =>
Int -> Sem r (Maybe Cell)
lkup Int
n
case Maybe Cell
cell of
Maybe Cell
Nothing -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"impossible: location " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n forall a. [a] -> [a] -> [a]
++ String
" not found in memory"
Just (V Value
v) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Value -> [Frame] -> CESK
Out Value
v [Frame]
k
Just (E Env
e Core
t) -> do
forall (r :: EffectRow).
Members '[State Mem] r =>
Int -> Cell -> Sem r ()
set Int
n Cell
Blackhole
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Core -> Env -> [Frame] -> CESK
In Core
t Env
e (Int -> Frame
FUpdate Int
n forall a. a -> [a] -> [a]
: [Frame]
k)
Just Cell
Blackhole -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ EvalError -> [Frame] -> CESK
Up EvalError
InfiniteLoop [Frame]
k
(Out Value
v (FUpdate Int
n : [Frame]
k)) -> do
forall (r :: EffectRow).
Members '[State Mem] r =>
Int -> Cell -> Sem r ()
set Int
n (Value -> Cell
V Value
v)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Value -> [Frame] -> CESK
Out Value
v [Frame]
k
(Up EvalError
err (f :: Frame
f@FTest {} : [Frame]
k)) ->
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Value -> [Frame] -> CESK
Out (ValProp -> Value
VProp (TestResult -> ValProp
VPDone (Bool -> TestReason -> TestEnv -> TestResult
TestResult Bool
False (forall a. EvalError -> TestReason_ a
TestRuntimeError EvalError
err) TestEnv
emptyTestEnv))) (Frame
f forall a. a -> [a] -> [a]
: [Frame]
k)
(Up EvalError
err (Frame
_ : [Frame]
ks)) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ EvalError -> [Frame] -> CESK
Up EvalError
err [Frame]
ks
(Out Value
v (FTest TestVars
vs Env
e : [Frame]
k)) -> do
let result :: ValProp
result = Value -> ValProp
ensureProp Value
v
res :: Either EvalError TestEnv
res = TestVars -> Env -> Either EvalError TestEnv
getTestEnv TestVars
vs Env
e
case Either EvalError TestEnv
res of
Left EvalError
err -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ EvalError -> [Frame] -> CESK
Up EvalError
err [Frame]
k
Right TestEnv
e' -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Value -> [Frame] -> CESK
Out (ValProp -> Value
VProp forall a b. (a -> b) -> a -> b
$ TestEnv -> ValProp -> ValProp
extendPropEnv TestEnv
e' ValProp
result) [Frame]
k
CESK
_ -> forall a. HasCallStack => String -> a
error String
"Impossible! Bad CESK machine state"
arity2 :: (Value -> Value -> a) -> Value -> a
arity2 :: forall a. (Value -> Value -> a) -> Value -> a
arity2 Value -> Value -> a
f (VPair Value
x Value
y) = Value -> Value -> a
f Value
x Value
y
arity2 Value -> Value -> a
_f Value
_v = forall a. HasCallStack => String -> a
error String
"arity2 on a non-pair!"
arity3 :: (Value -> Value -> Value -> a) -> Value -> a
arity3 :: forall a. (Value -> Value -> Value -> a) -> Value -> a
arity3 Value -> Value -> Value -> a
f (VPair Value
x (VPair Value
y Value
z)) = Value -> Value -> Value -> a
f Value
x Value
y Value
z
arity3 Value -> Value -> Value -> a
_f Value
_v = forall a. HasCallStack => String -> a
error String
"arity3 on a non-triple!"
appConst ::
Members '[Random, State Mem] r =>
Cont ->
Op ->
Value ->
Sem r CESK
appConst :: forall (r :: EffectRow).
Members '[Random, State Mem] r =>
[Frame] -> Op -> Value -> Sem r CESK
appConst [Frame]
k = \case
Op
OCrash -> EvalError -> Sem r CESK
up forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> EvalError
Crash forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (Value -> a) -> Value -> [a]
vlist Value -> Char
vchar
Op
OId -> Value -> Sem r CESK
out
Op
OAdd -> forall (r :: EffectRow).
(Rational -> Rational -> Rational) -> Value -> Sem r Value
numOp2 forall a. Num a => a -> a -> a
(+) forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Value -> Sem r CESK
out
Op
ONeg -> forall (r :: EffectRow).
(Rational -> Rational) -> Value -> Sem r Value
numOp1 forall a. Num a => a -> a
negate forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Value -> Sem r CESK
out
Op
OSqrt -> forall (r :: EffectRow).
(Rational -> Rational) -> Value -> Sem r Value
numOp1 Rational -> Rational
integerSqrt forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Value -> Sem r CESK
out
Op
OFloor -> forall (r :: EffectRow).
(Rational -> Rational) -> Value -> Sem r Value
numOp1 ((forall a. Integral a => a -> a -> Ratio a
% Integer
1) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (RealFrac a, Integral b) => a -> b
floor) forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Value -> Sem r CESK
out
Op
OCeil -> forall (r :: EffectRow).
(Rational -> Rational) -> Value -> Sem r Value
numOp1 ((forall a. Integral a => a -> a -> Ratio a
% Integer
1) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (RealFrac a, Integral b) => a -> b
ceiling) forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Value -> Sem r CESK
out
Op
OAbs -> forall (r :: EffectRow).
(Rational -> Rational) -> Value -> Sem r Value
numOp1 forall a. Num a => a -> a
abs forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Value -> Sem r CESK
out
Op
OMul -> forall (r :: EffectRow).
(Rational -> Rational -> Rational) -> Value -> Sem r Value
numOp2 forall a. Num a => a -> a -> a
(*) forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Value -> Sem r CESK
out
Op
ODiv -> forall (r :: EffectRow).
(Rational -> Rational -> Sem r Value) -> Value -> Sem r Value
numOp2' forall (r :: EffectRow).
Member (Error EvalError) r =>
Rational -> Rational -> Sem r Value
divOp forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (r :: EffectRow).
Sem (Error EvalError : r) Value -> Sem r CESK
outWithErr
where
divOp :: Member (Error EvalError) r => Rational -> Rational -> Sem r Value
divOp :: forall (r :: EffectRow).
Member (Error EvalError) r =>
Rational -> Rational -> Sem r Value
divOp Rational
_ Rational
0 = forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw EvalError
DivByZero
divOp Rational
m Rational
n = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Rational -> Value
ratv (Rational
m forall a. Fractional a => a -> a -> a
/ Rational
n)
Op
OExp -> forall (r :: EffectRow).
(Rational -> Rational -> Rational) -> Value -> Sem r Value
numOp2 (\Rational
m Rational
n -> Rational
m forall a b. (Fractional a, Integral b) => a -> b -> a
^^ forall a. Ratio a -> a
numerator Rational
n) forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Value -> Sem r CESK
out
Op
OMod -> forall (r :: EffectRow).
(Rational -> Rational -> Sem r Value) -> Value -> Sem r Value
numOp2' forall (r :: EffectRow).
Member (Error EvalError) r =>
Rational -> Rational -> Sem r Value
modOp forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (r :: EffectRow).
Sem (Error EvalError : r) Value -> Sem r CESK
outWithErr
where
modOp :: Member (Error EvalError) r => Rational -> Rational -> Sem r Value
modOp :: forall (r :: EffectRow).
Member (Error EvalError) r =>
Rational -> Rational -> Sem r Value
modOp Rational
m Rational
n
| Rational
n forall a. Eq a => a -> a -> Bool
== Rational
0 = forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw EvalError
DivByZero
| Bool
otherwise = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Integer -> Value
intv (forall a. Ratio a -> a
numerator Rational
m forall a. Integral a => a -> a -> a
`mod` forall a. Ratio a -> a
numerator Rational
n)
Op
ODivides -> forall (r :: EffectRow).
(Rational -> Rational -> Sem r Value) -> Value -> Sem r Value
numOp2' (\Rational
m Rational
n -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall e. Enum e => e -> Value
enumv forall a b. (a -> b) -> a -> b
$ forall {a}. Integral a => Ratio a -> Ratio a -> Bool
divides Rational
m Rational
n)) forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Value -> Sem r CESK
out
where
divides :: Ratio a -> Ratio a -> Bool
divides Ratio a
0 Ratio a
0 = Bool
True
divides Ratio a
0 Ratio a
_ = Bool
False
divides Ratio a
x Ratio a
y = forall a. Ratio a -> a
denominator (Ratio a
y forall a. Fractional a => a -> a -> a
/ Ratio a
x) forall a. Eq a => a -> a -> Bool
== a
1
Op
OIsPrime -> forall (r :: EffectRow). (Integer -> Value) -> Value -> Sem r Value
intOp1 (forall e. Enum e => e -> Value
enumv forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Bool
isPrime) forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Value -> Sem r CESK
out
Op
OFactor -> forall (r :: EffectRow).
(Integer -> Sem r Value) -> Value -> Sem r Value
intOp1' forall (r :: EffectRow).
Member (Error EvalError) r =>
Integer -> Sem r Value
primFactor forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (r :: EffectRow).
Sem (Error EvalError : r) Value -> Sem r CESK
outWithErr
where
primFactor :: Member (Error EvalError) r => Integer -> Sem r Value
primFactor :: forall (r :: EffectRow).
Member (Error EvalError) r =>
Integer -> Sem r Value
primFactor Integer
0 = forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw (String -> EvalError
Crash String
"0 has no prime factorization!")
primFactor Integer
n = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Value, Integer)] -> Value
VBag forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map ((Integer -> Value
intv forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Prime a -> a
unPrime) forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** forall a b. (Integral a, Num b) => a -> b
fromIntegral) (forall a. UniqueFactorisation a => a -> [(Prime a, Word)]
factorise Integer
n)
Op
OFrac -> forall (r :: EffectRow).
(Rational -> Sem r Value) -> Value -> Sem r Value
numOp1' (forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Value
primFrac) forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Value -> Sem r CESK
out
where
primFrac :: Rational -> Value
primFrac :: Rational -> Value
primFrac Rational
r = Value -> Value -> Value
VPair (Integer -> Value
intv (forall a. Ratio a -> a
numerator Rational
r)) (Integer -> Value
intv (forall a. Ratio a -> a
denominator Rational
r))
Op
OMultinom -> forall a. (Value -> Value -> a) -> Value -> a
arity2 forall (r :: EffectRow). Value -> Value -> Sem r Value
multinomOp forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Value -> Sem r CESK
out
where
multinomOp :: Value -> Value -> Sem r Value
multinomOp :: forall (r :: EffectRow). Value -> Value -> Sem r Value
multinomOp (Value -> Integer
vint -> Integer
n0) (forall a. (Value -> a) -> Value -> [a]
vlist Value -> Integer
vint -> [Integer]
ks0) = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Value
intv forall a b. (a -> b) -> a -> b
$ Integer -> [Integer] -> Integer
multinomial Integer
n0 [Integer]
ks0
where
multinomial :: Integer -> [Integer] -> Integer
multinomial :: Integer -> [Integer] -> Integer
multinomial Integer
_ [] = Integer
1
multinomial Integer
n (Integer
k' : [Integer]
ks)
| Integer
k' forall a. Ord a => a -> a -> Bool
> Integer
n = Integer
0
| Bool
otherwise = forall a. Integral a => a -> a -> a
choose Integer
n Integer
k' forall a. Num a => a -> a -> a
* Integer -> [Integer] -> Integer
multinomial (Integer
n forall a. Num a => a -> a -> a
- Integer
k') [Integer]
ks
Op
OFact -> forall (r :: EffectRow).
(Rational -> Sem r Value) -> Value -> Sem r Value
numOp1' forall (r :: EffectRow).
Member (Error EvalError) r =>
Rational -> Sem r Value
factOp forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (r :: EffectRow).
Sem (Error EvalError : r) Value -> Sem r CESK
outWithErr
where
factOp :: Member (Error EvalError) r => Rational -> Sem r Value
factOp :: forall (r :: EffectRow).
Member (Error EvalError) r =>
Rational -> Sem r Value
factOp (forall a. Ratio a -> a
numerator -> Integer
n)
| Integer
n forall a. Ord a => a -> a -> Bool
> forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Bounded a => a
maxBound :: Int) = forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw EvalError
Overflow
| Bool
otherwise = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Value
intv forall a b. (a -> b) -> a -> b
$ forall a. (Integral a, Bits a) => Int -> a
factorial (forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n)
Op
OEnum -> Value -> Sem r CESK
out forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Value
enumOp
where
enumOp :: Value -> Value
enumOp :: Value -> Value
enumOp (VType Type
ty) = forall a. (a -> Value) -> [a] -> Value
listv forall a. a -> a
id (Type -> [Value]
enumerateType Type
ty)
enumOp Value
v = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Impossible! enumOp on non-type " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Value
v
Op
OCount -> Value -> Sem r CESK
out forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Value
countOp
where
countOp :: Value -> Value
countOp :: Value -> Value
countOp (VType Type
ty) = case Type -> Maybe Integer
countType Type
ty of
Just Integer
num -> Side -> Value -> Value
VInj Side
R (Integer -> Value
intv Integer
num)
Maybe Integer
Nothing -> Value
VNil
countOp Value
v = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Impossible! countOp on non-type " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Value
v
Op
OUntil -> forall a. (Value -> Value -> a) -> Value -> a
arity2 forall a b. (a -> b) -> a -> b
$ \Value
v1 -> Value -> Sem r CESK
out forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ellipsis Value -> Value -> Value
ellipsis (forall t. t -> Ellipsis t
Until Value
v1)
Op
OEq -> forall a. (Value -> Value -> a) -> Value -> a
arity2 forall a b. (a -> b) -> a -> b
$ \Value
v1 Value
v2 -> Value -> Sem r CESK
out forall a b. (a -> b) -> a -> b
$ forall e. Enum e => e -> Value
enumv (Value -> Value -> Bool
valEq Value
v1 Value
v2)
Op
OLt -> forall a. (Value -> Value -> a) -> Value -> a
arity2 forall a b. (a -> b) -> a -> b
$ \Value
v1 Value
v2 -> Value -> Sem r CESK
out forall a b. (a -> b) -> a -> b
$ forall e. Enum e => e -> Value
enumv (Value -> Value -> Bool
valLt Value
v1 Value
v2)
Op
OPower -> forall (r :: EffectRow) a.
Op -> ([(Value, Integer)] -> Sem r a) -> Value -> Sem r a
withBag Op
OPower forall a b. (a -> b) -> a -> b
$ Value -> Sem r CESK
out forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Value, Integer)] -> Value
VBag forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Value, Integer)] -> [(Value, Integer)]
sortNCount forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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, Integer)] -> Value
VBag) forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Value, Integer)] -> [([(Value, Integer)], Integer)]
choices
where
choices :: [(Value, Integer)] -> [([(Value, Integer)], Integer)]
choices :: [(Value, Integer)] -> [([(Value, Integer)], Integer)]
choices [] = [([], Integer
1)]
choices ((Value
x, Integer
n) : [(Value, Integer)]
xs) = [([(Value, Integer)], Integer)]
xs' forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\Integer
k' -> forall a b. (a -> b) -> [a] -> [b]
map (forall {b} {a}.
Integral b =>
b -> (a, b) -> ([(a, b)], b) -> ([(a, b)], b)
cons Integer
n (Value
x, Integer
k')) [([(Value, Integer)], Integer)]
xs') [Integer
1 .. Integer
n]
where
xs' :: [([(Value, Integer)], Integer)]
xs' = [(Value, Integer)] -> [([(Value, Integer)], Integer)]
choices [(Value, Integer)]
xs
cons :: b -> (a, b) -> ([(a, b)], b) -> ([(a, b)], b)
cons b
n (a
x, b
k') ([(a, b)]
zs, b
m) = ((a
x, b
k') forall a. a -> [a] -> [a]
: [(a, b)]
zs, forall a. Integral a => a -> a -> a
choose b
n b
k' forall a. Num a => a -> a -> a
* b
m)
Op
OBagElem -> forall a. (Value -> Value -> a) -> Value -> a
arity2 forall a b. (a -> b) -> a -> b
$ \Value
x ->
forall (r :: EffectRow) a.
Op -> ([(Value, Integer)] -> Sem r a) -> Value -> Sem r a
withBag Op
OBagElem forall a b. (a -> b) -> a -> b
$
Value -> Sem r CESK
out forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Enum e => e -> Value
enumv forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Maybe a -> Bool
isJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (Value -> Value -> Bool
valEq Value
x) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst
Op
OListElem -> forall a. (Value -> Value -> a) -> Value -> a
arity2 forall a b. (a -> b) -> a -> b
$ \Value
x -> Value -> Sem r CESK
out forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Enum e => e -> Value
enumv forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Maybe a -> Bool
isJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (Value -> Value -> Bool
valEq Value
x) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (Value -> a) -> Value -> [a]
vlist forall a. a -> a
id
Op
OEachSet -> forall a. (Value -> Value -> a) -> Value -> a
arity2 forall a b. (a -> b) -> a -> b
$ \Value
f ->
forall (r :: EffectRow) a.
Op -> ([(Value, Integer)] -> Sem r a) -> Value -> Sem r a
withBag Op
OEachSet forall a b. (a -> b) -> a -> b
$
forall (r :: EffectRow).
Sem (Error EvalError : r) Value -> Sem r CESK
outWithErr forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Value, Integer)] -> Value
VBag forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Value] -> [(Value, Integer)]
countValues) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (r :: EffectRow).
Members '[Random, Error EvalError, State Mem] r =>
Value -> [Value] -> Sem r Value
evalApp Value
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. a -> [a] -> [a]
: []) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst)
Op
OEachBag -> forall a. (Value -> Value -> a) -> Value -> a
arity2 forall a b. (a -> b) -> a -> b
$ \Value
f ->
forall (r :: EffectRow) a.
Op -> ([(Value, Integer)] -> Sem r a) -> Value -> Sem r a
withBag Op
OEachBag forall a b. (a -> b) -> a -> b
$
forall (r :: EffectRow).
Sem (Error EvalError : r) Value -> Sem r CESK
outWithErr forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Value, Integer)] -> Value
VBag forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Value, Integer)] -> [(Value, Integer)]
sortNCount) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\(Value
x, Integer
n) -> (,Integer
n) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: EffectRow).
Members '[Random, Error EvalError, State Mem] r =>
Value -> [Value] -> Sem r Value
evalApp Value
f [Value
x])
Op
OFilterBag -> forall a. (Value -> Value -> a) -> Value -> a
arity2 forall a b. (a -> b) -> a -> b
$ \Value
f -> forall (r :: EffectRow) a.
Op -> ([(Value, Integer)] -> Sem r a) -> Value -> Sem r a
withBag Op
OFilterBag forall a b. (a -> b) -> a -> b
$ \[(Value, Integer)]
xs ->
forall (r :: EffectRow).
Sem (Error EvalError : r) Value -> Sem r CESK
outWithErr forall a b. (a -> b) -> a -> b
$ do
[Value]
bs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (r :: EffectRow).
Members '[Random, Error EvalError, State Mem] r =>
Value -> [Value] -> Sem r Value
evalApp Value
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. a -> [a] -> [a]
: []) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Value, Integer)]
xs
forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Value, Integer)] -> Value
VBag forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
Prelude.filter (Value -> Bool
isTrue forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [Value]
bs [(Value, Integer)]
xs
where
isTrue :: Value -> Bool
isTrue (VInj Side
R Value
VUnit) = Bool
True
isTrue Value
_ = Bool
False
Op
OMerge -> forall a. (Value -> Value -> Value -> a) -> Value -> a
arity3 forall a b. (a -> b) -> a -> b
$ \Value
f Value
bxs Value
bys ->
case (Value
bxs, Value
bys) of
(VBag [(Value, Integer)]
xs, VBag [(Value, Integer)]
ys) -> forall (r :: EffectRow).
Sem (Error EvalError : r) Value -> Sem r CESK
outWithErr ([(Value, Integer)] -> Value
VBag forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: EffectRow).
Members '[Random, Error EvalError, State Mem] r =>
Value
-> [(Value, Integer)]
-> [(Value, Integer)]
-> Sem r [(Value, Integer)]
mergeM Value
f [(Value, Integer)]
xs [(Value, Integer)]
ys)
(VBag [(Value, Integer)]
_, Value
_) -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Impossible! OMerge on non-VBag " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Value
bys
(Value, Value)
_ -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Impossible! OMerge on non-VBag " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Value
bxs
Op
OBagUnions -> forall (r :: EffectRow) a.
Op -> ([(Value, Integer)] -> Sem r a) -> Value -> Sem r a
withBag Op
OBagUnions forall a b. (a -> b) -> a -> b
$ \[(Value, Integer)]
cts ->
Value -> Sem r CESK
out forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Value, Integer)] -> Value
VBag forall a b. (a -> b) -> a -> b
$ [(Value, Integer)] -> [(Value, Integer)]
sortNCount [(Value
x, Integer
m forall a. Num a => a -> a -> a
* Integer
n) | (VBag [(Value, Integer)]
xs, Integer
n) <- [(Value, Integer)]
cts, (Value
x, Integer
m) <- [(Value, Integer)]
xs]
Op
OBagToSet -> forall (r :: EffectRow) a.
Op -> ([(Value, Integer)] -> Sem r a) -> Value -> Sem r a
withBag Op
OBagToSet forall a b. (a -> b) -> a -> b
$ Value -> Sem r CESK
out forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Value, Integer)] -> Value
VBag forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a b. (a -> b) -> [a] -> [b]
map forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second) (forall a b. a -> b -> a
const Integer
1)
Op
OSetToList -> forall (r :: EffectRow) a.
Op -> ([(Value, Integer)] -> Sem r a) -> Value -> Sem r a
withBag Op
OSetToList forall a b. (a -> b) -> a -> b
$ Value -> Sem r CESK
out forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Value) -> [a] -> Value
listv forall a. a -> a
id forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst
Op
OBagToList -> forall (r :: EffectRow) a.
Op -> ([(Value, Integer)] -> Sem r a) -> Value -> Sem r a
withBag Op
OBagToList forall a b. (a -> b) -> a -> b
$ Value -> Sem r CESK
out forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Value) -> [a] -> Value
listv forall a. a -> a
id forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall a. Int -> a -> [a]
replicate forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral)))
Op
OListToSet -> Value -> Sem r CESK
out forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Value, Integer)] -> Value
VBag forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a b. (a -> b) -> [a] -> [b]
map forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) (forall a b. a -> b -> a
const Integer
1) forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Value] -> [(Value, Integer)]
countValues forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (Value -> a) -> Value -> [a]
vlist forall a. a -> a
id
Op
OListToBag -> Value -> Sem r CESK
out forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Value, Integer)] -> Value
VBag forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Value] -> [(Value, Integer)]
countValues forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (Value -> a) -> Value -> [a]
vlist forall a. a -> a
id
Op
OBagToCounts -> forall (r :: EffectRow) a.
Op -> ([(Value, Integer)] -> Sem r a) -> Value -> Sem r a
withBag Op
OBagToCounts forall a b. (a -> b) -> a -> b
$ Value -> Sem r CESK
out forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Value, Integer)] -> Value
VBag forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map ((,Integer
1) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> Value) -> (b -> Value) -> (a, b) -> Value
pairv forall a. a -> a
id Integer -> Value
intv)
Op
OCountsToBag ->
forall (r :: EffectRow) a.
Op -> ([(Value, Integer)] -> Sem r a) -> Value -> Sem r a
withBag Op
OCountsToBag forall a b. (a -> b) -> a -> b
$
Value -> Sem r CESK
out forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Value, Integer)] -> Value
VBag forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Value, Integer)] -> [(Value, Integer)]
sortNCount forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a. Num a => a -> a -> a
(*)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a} {a} {b}. ((a, a), b) -> (a, (a, b))
assoc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (forall a b. (Value -> a) -> (Value -> b) -> Value -> (a, b)
vpair forall a. a -> a
id Value -> Integer
vint))
where
assoc :: ((a, a), b) -> (a, (a, b))
assoc ((a
a, a
b), b
c) = (a
a, (a
b, b
c))
Op
OUnsafeCountsToBag ->
forall (r :: EffectRow) a.
Op -> ([(Value, Integer)] -> Sem r a) -> Value -> Sem r a
withBag Op
OUnsafeCountsToBag forall a b. (a -> b) -> a -> b
$
Value -> Sem r CESK
out forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Value, Integer)] -> Value
VBag forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a. Num a => a -> a -> a
(*)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a} {a} {b}. ((a, a), b) -> (a, (a, b))
assoc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (forall a b. (Value -> a) -> (Value -> b) -> Value -> (a, b)
vpair forall a. a -> a
id Value -> Integer
vint))
where
assoc :: ((a, a), b) -> (a, (a, b))
assoc ((a
a, a
b), b
c) = (a
a, (a
b, b
c))
Op
OMapToSet ->
forall (r :: EffectRow) a.
Op -> (Map SimpleValue Value -> Sem r a) -> Value -> Sem r a
withMap Op
OMapToSet forall a b. (a -> b) -> a -> b
$
Value -> Sem r CESK
out forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Value, Integer)] -> Value
VBag forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (\(SimpleValue
k', Value
v) -> (Value -> Value -> Value
VPair (SimpleValue -> Value
fromSimpleValue SimpleValue
k') Value
v, Integer
1)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [(k, a)]
M.assocs
Op
OSetToMap ->
forall (r :: EffectRow) a.
Op -> ([(Value, Integer)] -> Sem r a) -> Value -> Sem r a
withBag Op
OSetToMap forall a b. (a -> b) -> a -> b
$
Value -> Sem r CESK
out forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map SimpleValue Value -> Value
VMap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (Value -> (SimpleValue, Value)
convertAssoc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst)
where
convertAssoc :: Value -> (SimpleValue, Value)
convertAssoc (VPair Value
k' Value
v) = (Value -> SimpleValue
toSimpleValue Value
k', Value
v)
convertAssoc Value
v = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Impossible! convertAssoc on non-VPair " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Value
v
Op
OInsert -> forall a. (Value -> Value -> Value -> a) -> Value -> a
arity3 forall a b. (a -> b) -> a -> b
$ \Value
k' Value
v ->
forall (r :: EffectRow) a.
Op -> (Map SimpleValue Value -> Sem r a) -> Value -> Sem r a
withMap Op
OInsert forall a b. (a -> b) -> a -> b
$
Value -> Sem r CESK
out forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map SimpleValue Value -> Value
VMap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (Value -> SimpleValue
toSimpleValue Value
k') Value
v
Op
OLookup -> forall a. (Value -> Value -> a) -> Value -> a
arity2 forall a b. (a -> b) -> a -> b
$ \Value
k' ->
forall (r :: EffectRow) a.
Op -> (Map SimpleValue Value -> Sem r a) -> Value -> Sem r a
withMap Op
OLookup forall a b. (a -> b) -> a -> b
$
Value -> Sem r CESK
out forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Value -> Value
toMaybe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Value -> SimpleValue
toSimpleValue Value
k')
where
toMaybe :: Maybe Value -> Value
toMaybe = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Side -> Value -> Value
VInj Side
L Value
VUnit) (Side -> Value -> Value
VInj Side
R)
Op
OVertex -> Value -> Sem r CESK
out forall b c a. (b -> c) -> (a -> b) -> a -> c
. Graph SimpleValue -> Value
VGraph forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Graph a
Vertex forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> SimpleValue
toSimpleValue
Op
OOverlay -> forall a. (Value -> Value -> a) -> Value -> a
arity2 forall a b. (a -> b) -> a -> b
$ forall (r :: EffectRow) a.
Op
-> (Graph SimpleValue -> Graph SimpleValue -> Sem r a)
-> Value
-> Value
-> Sem r a
withGraph2 Op
OOverlay forall a b. (a -> b) -> a -> b
$ \Graph SimpleValue
g1 Graph SimpleValue
g2 ->
Value -> Sem r CESK
out forall a b. (a -> b) -> a -> b
$ Graph SimpleValue -> Value
VGraph (forall a. Graph a -> Graph a -> Graph a
Overlay Graph SimpleValue
g1 Graph SimpleValue
g2)
Op
OConnect -> forall a. (Value -> Value -> a) -> Value -> a
arity2 forall a b. (a -> b) -> a -> b
$ forall (r :: EffectRow) a.
Op
-> (Graph SimpleValue -> Graph SimpleValue -> Sem r a)
-> Value
-> Value
-> Sem r a
withGraph2 Op
OConnect forall a b. (a -> b) -> a -> b
$ \Graph SimpleValue
g1 Graph SimpleValue
g2 ->
Value -> Sem r CESK
out forall a b. (a -> b) -> a -> b
$ Graph SimpleValue -> Value
VGraph (forall a. Graph a -> Graph a -> Graph a
Connect Graph SimpleValue
g1 Graph SimpleValue
g2)
Op
OSummary -> forall (r :: EffectRow) a.
Op -> (Graph SimpleValue -> Sem r a) -> Value -> Sem r a
withGraph Op
OSummary forall a b. (a -> b) -> a -> b
$ Value -> Sem r CESK
out forall b c a. (b -> c) -> (a -> b) -> a -> c
. Graph SimpleValue -> Value
graphSummary
OForall [Type]
tys -> Value -> Sem r CESK
out forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\Value
v -> ValProp -> Value
VProp (SearchMotive -> [Type] -> Value -> TestEnv -> ValProp
VPSearch SearchMotive
SMForall [Type]
tys Value
v TestEnv
emptyTestEnv))
OExists [Type]
tys -> Value -> Sem r CESK
out forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\Value
v -> ValProp -> Value
VProp (SearchMotive -> [Type] -> Value -> TestEnv -> ValProp
VPSearch SearchMotive
SMExists [Type]
tys Value
v TestEnv
emptyTestEnv))
Op
OHolds -> forall (r :: EffectRow).
Members '[Random, State Mem] r =>
SearchType -> Value -> Sem r TestResult
testProperty SearchType
Exhaustive forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> forall (r :: EffectRow).
Member (Error EvalError) r =>
TestResult -> Sem r Value
resultToBool forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (r :: EffectRow).
Sem (Error EvalError : r) Value -> Sem r CESK
outWithErr
Op
ONotProp -> Value -> Sem r CESK
out forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValProp -> Value
VProp forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValProp -> ValProp
notProp forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> ValProp
ensureProp
OShouldEq Type
ty -> forall a. (Value -> Value -> a) -> Value -> a
arity2 forall a b. (a -> b) -> a -> b
$ \Value
v1 Value
v2 ->
Value -> Sem r CESK
out forall a b. (a -> b) -> a -> b
$ ValProp -> Value
VProp (TestResult -> ValProp
VPDone (Bool -> TestReason -> TestEnv -> TestResult
TestResult (Value -> Value -> Bool
valEq Value
v1 Value
v2) (forall a. Type -> a -> a -> TestReason_ a
TestEqual Type
ty Value
v1 Value
v2) TestEnv
emptyTestEnv))
OShouldLt Type
ty -> forall a. (Value -> Value -> a) -> Value -> a
arity2 forall a b. (a -> b) -> a -> b
$ \Value
v1 Value
v2 ->
Value -> Sem r CESK
out forall a b. (a -> b) -> a -> b
$ ValProp -> Value
VProp (TestResult -> ValProp
VPDone (Bool -> TestReason -> TestEnv -> TestResult
TestResult (Value -> Value -> Bool
valLt Value
v1 Value
v2) (forall a. Type -> a -> a -> TestReason_ a
TestLt Type
ty Value
v1 Value
v2) TestEnv
emptyTestEnv))
Op
OAnd -> forall a. (Value -> Value -> a) -> Value -> a
arity2 forall a b. (a -> b) -> a -> b
$ \Value
p1 Value
p2 ->
Value -> Sem r CESK
out forall a b. (a -> b) -> a -> b
$ ValProp -> Value
VProp (LOp -> ValProp -> ValProp -> ValProp
VPBin LOp
LAnd (Value -> ValProp
ensureProp Value
p1) (Value -> ValProp
ensureProp Value
p2))
Op
OOr -> forall a. (Value -> Value -> a) -> Value -> a
arity2 forall a b. (a -> b) -> a -> b
$ \Value
p1 Value
p2 ->
Value -> Sem r CESK
out forall a b. (a -> b) -> a -> b
$ ValProp -> Value
VProp (LOp -> ValProp -> ValProp -> ValProp
VPBin LOp
LOr (Value -> ValProp
ensureProp Value
p1) (Value -> ValProp
ensureProp Value
p2))
Op
OImpl -> forall a. (Value -> Value -> a) -> Value -> a
arity2 forall a b. (a -> b) -> a -> b
$ \Value
p1 Value
p2 ->
Value -> Sem r CESK
out forall a b. (a -> b) -> a -> b
$ ValProp -> Value
VProp (LOp -> ValProp -> ValProp -> ValProp
VPBin LOp
LImpl (Value -> ValProp
ensureProp Value
p1) (Value -> ValProp
ensureProp Value
p2))
Op
c -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Unimplemented: appConst " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Op
c
where
outWithErr :: Sem (Error EvalError ': r) Value -> Sem r CESK
outWithErr :: forall (r :: EffectRow).
Sem (Error EvalError : r) Value -> Sem r CESK
outWithErr Sem (Error EvalError : r) Value
m = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (EvalError -> [Frame] -> CESK
`Up` [Frame]
k) (Value -> [Frame] -> CESK
`Out` [Frame]
k) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall e (r :: EffectRow) a.
Sem (Error e : r) a -> Sem r (Either e a)
runError Sem (Error EvalError : r) Value
m
out :: Value -> Sem r CESK
out Value
v = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Value -> [Frame] -> CESK
Out Value
v [Frame]
k
up :: EvalError -> Sem r CESK
up EvalError
e = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ EvalError -> [Frame] -> CESK
Up EvalError
e [Frame]
k
withBag :: Op -> ([(Value, Integer)] -> Sem r a) -> Value -> Sem r a
withBag :: forall (r :: EffectRow) a.
Op -> ([(Value, Integer)] -> Sem r a) -> Value -> Sem r a
withBag Op
op [(Value, Integer)] -> Sem r a
f = \case
VBag [(Value, Integer)]
xs -> [(Value, Integer)] -> Sem r a
f [(Value, Integer)]
xs
Value
v -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Impossible! " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Op
op forall a. [a] -> [a] -> [a]
++ String
" on non-VBag " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Value
v
withMap :: Op -> (M.Map SimpleValue Value -> Sem r a) -> Value -> Sem r a
withMap :: forall (r :: EffectRow) a.
Op -> (Map SimpleValue Value -> Sem r a) -> Value -> Sem r a
withMap Op
op Map SimpleValue Value -> Sem r a
f = \case
VMap Map SimpleValue Value
m -> Map SimpleValue Value -> Sem r a
f Map SimpleValue Value
m
Value
v -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Impossible! " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Op
op forall a. [a] -> [a] -> [a]
++ String
" on non-VMap " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Value
v
withGraph :: Op -> (Graph SimpleValue -> Sem r a) -> Value -> Sem r a
withGraph :: forall (r :: EffectRow) a.
Op -> (Graph SimpleValue -> Sem r a) -> Value -> Sem r a
withGraph Op
op Graph SimpleValue -> Sem r a
f = \case
VGraph Graph SimpleValue
g -> Graph SimpleValue -> Sem r a
f Graph SimpleValue
g
Value
v -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Impossible! " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Op
op forall a. [a] -> [a] -> [a]
++ String
" on non-VGraph " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Value
v
withGraph2 :: Op -> (Graph SimpleValue -> Graph SimpleValue -> Sem r a) -> Value -> Value -> Sem r a
withGraph2 :: forall (r :: EffectRow) a.
Op
-> (Graph SimpleValue -> Graph SimpleValue -> Sem r a)
-> Value
-> Value
-> Sem r a
withGraph2 Op
op Graph SimpleValue -> Graph SimpleValue -> Sem r a
f Value
v1 Value
v2 = case (Value
v1, Value
v2) of
(VGraph Graph SimpleValue
g1, VGraph Graph SimpleValue
g2) -> Graph SimpleValue -> Graph SimpleValue -> Sem r a
f Graph SimpleValue
g1 Graph SimpleValue
g2
(Value
_, VGraph Graph SimpleValue
_) -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Impossible! " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Op
op forall a. [a] -> [a] -> [a]
++ String
" on non-VGraph " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Value
v1
(Value, Value)
_ -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Impossible! " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Op
op forall a. [a] -> [a] -> [a]
++ String
" on non-VGraph " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Value
v2
intOp1 :: (Integer -> Value) -> Value -> Sem r Value
intOp1 :: forall (r :: EffectRow). (Integer -> Value) -> Value -> Sem r Value
intOp1 Integer -> Value
f = forall (r :: EffectRow).
(Integer -> Sem r Value) -> Value -> Sem r Value
intOp1' (forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Value
f)
intOp1' :: (Integer -> Sem r Value) -> Value -> Sem r Value
intOp1' :: forall (r :: EffectRow).
(Integer -> Sem r Value) -> Value -> Sem r Value
intOp1' Integer -> Sem r Value
f = Integer -> Sem r Value
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Integer
vint
numOp1 :: (Rational -> Rational) -> Value -> Sem r Value
numOp1 :: forall (r :: EffectRow).
(Rational -> Rational) -> Value -> Sem r Value
numOp1 Rational -> Rational
f = forall (r :: EffectRow).
(Rational -> Sem r Value) -> Value -> Sem r Value
numOp1' forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Value
ratv forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Rational
f
numOp1' :: (Rational -> Sem r Value) -> Value -> Sem r Value
numOp1' :: forall (r :: EffectRow).
(Rational -> Sem r Value) -> Value -> Sem r Value
numOp1' Rational -> Sem r Value
f (VNum RationalDisplay
_ Rational
m) = Rational -> Sem r Value
f Rational
m
numOp1' Rational -> Sem r Value
_ Value
v = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Impossible! numOp1' on non-VNum " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Value
v
numOp2 :: (Rational -> Rational -> Rational) -> Value -> Sem r Value
numOp2 :: forall (r :: EffectRow).
(Rational -> Rational -> Rational) -> Value -> Sem r Value
numOp2 Rational -> Rational -> Rational
(#) = forall (r :: EffectRow).
(Rational -> Rational -> Sem r Value) -> Value -> Sem r Value
numOp2' forall a b. (a -> b) -> a -> b
$ \Rational
m Rational
n -> forall (m :: * -> *) a. Monad m => a -> m a
return (Rational -> Value
ratv (Rational
m Rational -> Rational -> Rational
# Rational
n))
numOp2' :: (Rational -> Rational -> Sem r Value) -> Value -> Sem r Value
numOp2' :: forall (r :: EffectRow).
(Rational -> Rational -> Sem r Value) -> Value -> Sem r Value
numOp2' Rational -> Rational -> Sem r Value
(#) =
forall a. (Value -> Value -> a) -> Value -> a
arity2 forall a b. (a -> b) -> a -> b
$ \Value
v1 Value
v2 -> case (Value
v1, Value
v2) of
(VNum RationalDisplay
d1 Rational
n1, VNum RationalDisplay
d2 Rational
n2) -> do
Value
res <- Rational
n1 Rational -> Rational -> Sem r Value
# Rational
n2
case Value
res of
VNum RationalDisplay
_ Rational
r -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ RationalDisplay -> Rational -> Value
VNum (RationalDisplay
d1 forall a. Semigroup a => a -> a -> a
<> RationalDisplay
d2) Rational
r
Value
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Value
res
(VNum {}, Value
_) -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Impossible! numOp2' on non-VNum " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Value
v2
(Value, Value)
_ -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Impossible! numOp2' on non-VNum " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Value
v1
integerSqrt :: Rational -> Rational
integerSqrt :: Rational -> Rational
integerSqrt Rational
n = Integer -> Integer
integerSqrt' (forall a. Ratio a -> a
numerator Rational
n) forall a. Integral a => a -> a -> Ratio a
% Integer
1
integerSqrt' :: Integer -> Integer
integerSqrt' :: Integer -> Integer
integerSqrt' Integer
0 = Integer
0
integerSqrt' Integer
1 = Integer
1
integerSqrt' Integer
n =
let twopows :: [Integer]
twopows = forall a. (a -> a) -> a -> [a]
iterate (forall a. Num a => a -> Int -> a
^! Int
2) Integer
2
(Integer
lowerRoot, Integer
lowerN) =
forall a. [a] -> a
last forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
takeWhile ((Integer
n forall a. Ord a => a -> a -> Bool
>=) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip (Integer
1 forall a. a -> [a] -> [a]
: [Integer]
twopows) [Integer]
twopows
newtonStep :: Integer -> Integer
newtonStep Integer
x = forall a. Integral a => a -> a -> a
div (Integer
x forall a. Num a => a -> a -> a
+ forall a. Integral a => a -> a -> a
div Integer
n Integer
x) Integer
2
iters :: [Integer]
iters = forall a. (a -> a) -> a -> [a]
iterate Integer -> Integer
newtonStep (Integer -> Integer
integerSqrt' (forall a. Integral a => a -> a -> a
div Integer
n Integer
lowerN) forall a. Num a => a -> a -> a
* Integer
lowerRoot)
isRoot :: Integer -> Bool
isRoot Integer
r = Integer
r forall a. Num a => a -> Int -> a
^! Int
2 forall a. Ord a => a -> a -> Bool
<= Integer
n Bool -> Bool -> Bool
&& Integer
n forall a. Ord a => a -> a -> Bool
< (Integer
r forall a. Num a => a -> a -> a
+ Integer
1) forall a. Num a => a -> Int -> a
^! Int
2
in forall a. [a] -> a
head forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Bool
isRoot) [Integer]
iters
(^!) :: Num a => a -> Int -> a
^! :: forall a. Num a => a -> Int -> a
(^!) a
x Int
n = a
x forall a b. (Num a, Integral b) => a -> b -> a
^ Int
n
valEq :: Value -> Value -> Bool
valEq :: Value -> Value -> Bool
valEq Value
v1 Value
v2 = Value -> Value -> Ordering
valCmp Value
v1 Value
v2 forall a. Eq a => a -> a -> Bool
== Ordering
EQ
valLt :: Value -> Value -> Bool
valLt :: Value -> Value -> Bool
valLt Value
v1 Value
v2 = Value -> Value -> Ordering
valCmp Value
v1 Value
v2 forall a. Eq a => a -> a -> Bool
== Ordering
LT
valCmp :: Value -> Value -> Ordering
valCmp :: Value -> Value -> Ordering
valCmp (VNum RationalDisplay
_ Rational
r1) (VNum RationalDisplay
_ Rational
r2) = forall a. Ord a => a -> a -> Ordering
compare Rational
r1 Rational
r2
valCmp (VInj Side
L Value
_) (VInj Side
R Value
_) = Ordering
LT
valCmp (VInj Side
R Value
_) (VInj Side
L Value
_) = Ordering
GT
valCmp (VInj Side
L Value
v1) (VInj Side
L Value
v2) = Value -> Value -> Ordering
valCmp Value
v1 Value
v2
valCmp (VInj Side
R Value
v1) (VInj Side
R Value
v2) = Value -> Value -> Ordering
valCmp Value
v1 Value
v2
valCmp Value
VUnit Value
VUnit = Ordering
EQ
valCmp (VPair Value
v11 Value
v12) (VPair Value
v21 Value
v22) = Value -> Value -> Ordering
valCmp Value
v11 Value
v21 forall a. Semigroup a => a -> a -> a
<> Value -> Value -> Ordering
valCmp Value
v12 Value
v22
valCmp (VType Type
ty1) (VType Type
ty2) = forall a. Ord a => a -> a -> Ordering
compare Type
ty1 Type
ty2
valCmp (VBag [(Value, Integer)]
cs1) (VBag [(Value, Integer)]
cs2) = [(Value, Integer)] -> [(Value, Integer)] -> Ordering
compareBags [(Value, Integer)]
cs1 [(Value, Integer)]
cs2
valCmp (VMap Map SimpleValue Value
m1) (VMap Map SimpleValue Value
m2) = [(SimpleValue, Value)] -> [(SimpleValue, Value)] -> Ordering
compareMaps (forall k a. Map k a -> [(k, a)]
M.assocs Map SimpleValue Value
m1) (forall k a. Map k a -> [(k, a)]
M.assocs Map SimpleValue Value
m2)
valCmp (VGraph Graph SimpleValue
g1) (VGraph Graph SimpleValue
g2) = Value -> Value -> Ordering
valCmp (Graph SimpleValue -> Value
graphSummary Graph SimpleValue
g1) (Graph SimpleValue -> Value
graphSummary Graph SimpleValue
g2)
valCmp Value
v1 Value
v2 = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"valCmp\n " forall a. [a] -> [a] -> [a]
++ forall a. Int -> [a] -> [a]
take Int
100 (forall a. Show a => a -> String
show Value
v1) forall a. [a] -> [a] -> [a]
++ String
"...\n " forall a. [a] -> [a] -> [a]
++ forall a. Int -> [a] -> [a]
take Int
100 (forall a. Show a => a -> String
show Value
v2) forall a. [a] -> [a] -> [a]
++ String
"..."
compareBags :: [(Value, Integer)] -> [(Value, Integer)] -> Ordering
compareBags :: [(Value, Integer)] -> [(Value, Integer)] -> Ordering
compareBags [] [] = Ordering
EQ
compareBags [] [(Value, Integer)]
_ = Ordering
LT
compareBags [(Value, Integer)]
_ [] = Ordering
GT
compareBags ((Value
x, Integer
xn) : [(Value, Integer)]
xs) ((Value
y, Integer
yn) : [(Value, Integer)]
ys) =
Value -> Value -> Ordering
valCmp Value
x Value
y forall a. Semigroup a => a -> a -> a
<> forall a. Ord a => a -> a -> Ordering
compare Integer
xn Integer
yn forall a. Semigroup a => a -> a -> a
<> [(Value, Integer)] -> [(Value, Integer)] -> Ordering
compareBags [(Value, Integer)]
xs [(Value, Integer)]
ys
compareMaps :: [(SimpleValue, Value)] -> [(SimpleValue, Value)] -> Ordering
compareMaps :: [(SimpleValue, Value)] -> [(SimpleValue, Value)] -> Ordering
compareMaps [] [] = Ordering
EQ
compareMaps [] [(SimpleValue, Value)]
_ = Ordering
LT
compareMaps [(SimpleValue, Value)]
_ [] = Ordering
GT
compareMaps ((SimpleValue
k1, Value
v1) : [(SimpleValue, Value)]
as1) ((SimpleValue
k2, Value
v2) : [(SimpleValue, Value)]
as2) =
Value -> Value -> Ordering
valCmp (SimpleValue -> Value
fromSimpleValue SimpleValue
k1) (SimpleValue -> Value
fromSimpleValue SimpleValue
k2) forall a. Semigroup a => a -> a -> a
<> Value -> Value -> Ordering
valCmp Value
v1 Value
v2 forall a. Semigroup a => a -> a -> a
<> [(SimpleValue, Value)] -> [(SimpleValue, Value)] -> Ordering
compareMaps [(SimpleValue, Value)]
as1 [(SimpleValue, Value)]
as2
ellipsis :: Ellipsis Value -> Value -> Value
ellipsis :: Ellipsis Value -> Value -> Value
ellipsis (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Value -> Rational
vrat -> Ellipsis Rational
end) (forall a. (Value -> a) -> Value -> [a]
vlist Value -> Rational
vrat -> [Rational]
rs) = forall a. (a -> Value) -> [a] -> Value
listv Rational -> Value
ratv forall a b. (a -> b) -> a -> b
$ forall a. (Enum a, Num a, Ord a) => [a] -> Ellipsis a -> [a]
enumEllipsis [Rational]
rs Ellipsis Rational
end
enumEllipsis :: (Enum a, Num a, Ord a) => [a] -> Ellipsis a -> [a]
enumEllipsis :: forall a. (Enum a, Num a, Ord a) => [a] -> Ellipsis a -> [a]
enumEllipsis [] Ellipsis a
_ = forall a. HasCallStack => String -> a
error String
"Impossible! Disco.Interpret.CESK.enumEllipsis []"
enumEllipsis [a
x] (Until a
y)
| a
x forall a. Ord a => a -> a -> Bool
<= a
y = [a
x .. a
y]
| Bool
otherwise = [a
x, forall a. Enum a => a -> a
pred a
x .. a
y]
enumEllipsis [a]
xs (Until a
y)
| a
d forall a. Ord a => a -> a -> Bool
> a
0 = forall a. (a -> Bool) -> [a] -> [a]
takeWhile (forall a. Ord a => a -> a -> Bool
<= a
y) [a]
nums
| a
d forall a. Ord a => a -> a -> Bool
< a
0 = forall a. (a -> Bool) -> [a] -> [a]
takeWhile (forall a. Ord a => a -> a -> Bool
>= a
y) [a]
nums
| Bool
otherwise = [a]
nums
where
d :: a
d = forall a. (Eq a, Num a) => [a] -> a
constdiff [a]
xs
nums :: [a]
nums = forall a. Num a => [a] -> [a]
babbage [a]
xs
babbage :: Num a => [a] -> [a]
babbage :: forall a. Num a => [a] -> [a]
babbage [] = []
babbage [a
x] = forall a. a -> [a]
repeat a
x
babbage (a
x : [a]
xs) = forall b a. (b -> a -> b) -> b -> [a] -> [b]
scanl forall a. Num a => a -> a -> a
(+) a
x (forall a. Num a => [a] -> [a]
babbage (forall a. Num a => [a] -> [a]
diff (a
x forall a. a -> [a] -> [a]
: [a]
xs)))
diff :: Num a => [a] -> [a]
diff :: forall a. Num a => [a] -> [a]
diff [a]
xs = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (-) (forall a. [a] -> [a]
tail [a]
xs) [a]
xs
constdiff :: (Eq a, Num a) => [a] -> a
constdiff :: forall a. (Eq a, Num a) => [a] -> a
constdiff [] = forall a. HasCallStack => String -> a
error String
"Impossible! Disco.Interpret.Core.constdiff []"
constdiff (a
x : [a]
xs)
| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. Eq a => a -> a -> Bool
== a
x) [a]
xs = a
x
| Bool
otherwise = forall a. (Eq a, Num a) => [a] -> a
constdiff (forall a. Num a => [a] -> [a]
diff (a
x forall a. a -> [a] -> [a]
: [a]
xs))
countValues :: [Value] -> [(Value, Integer)]
countValues :: [Value] -> [(Value, Integer)]
countValues = [(Value, Integer)] -> [(Value, Integer)]
sortNCount forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (,Integer
1)
sortNCount :: [(Value, Integer)] -> [(Value, Integer)]
sortNCount :: [(Value, Integer)] -> [(Value, Integer)]
sortNCount [] = []
sortNCount [(Value, Integer)
x] = [(Value, Integer)
x]
sortNCount [(Value, Integer)]
xs = (Integer -> Integer -> Integer)
-> [(Value, Integer)] -> [(Value, Integer)] -> [(Value, Integer)]
merge forall a. Num a => a -> a -> a
(+) ([(Value, Integer)] -> [(Value, Integer)]
sortNCount [(Value, Integer)]
firstHalf) ([(Value, Integer)] -> [(Value, Integer)]
sortNCount [(Value, Integer)]
secondHalf)
where
([(Value, Integer)]
firstHalf, [(Value, Integer)]
secondHalf) = forall a. Int -> [a] -> ([a], [a])
splitAt (forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Value, Integer)]
xs forall a. Integral a => a -> a -> a
`div` Int
2) [(Value, Integer)]
xs
merge ::
(Integer -> Integer -> Integer) ->
[(Value, Integer)] ->
[(Value, Integer)] ->
[(Value, Integer)]
merge :: (Integer -> Integer -> Integer)
-> [(Value, Integer)] -> [(Value, Integer)] -> [(Value, Integer)]
merge Integer -> Integer -> Integer
g = [(Value, Integer)] -> [(Value, Integer)] -> [(Value, Integer)]
go
where
go :: [(Value, Integer)] -> [(Value, Integer)] -> [(Value, Integer)]
go [] [] = []
go [] ((Value
y, Integer
n) : [(Value, Integer)]
ys) = Value
-> Integer -> Integer -> [(Value, Integer)] -> [(Value, Integer)]
mergeCons Value
y Integer
0 Integer
n ([(Value, Integer)] -> [(Value, Integer)] -> [(Value, Integer)]
go [] [(Value, Integer)]
ys)
go ((Value
x, Integer
n) : [(Value, Integer)]
xs) [] = Value
-> Integer -> Integer -> [(Value, Integer)] -> [(Value, Integer)]
mergeCons Value
x Integer
n Integer
0 ([(Value, Integer)] -> [(Value, Integer)] -> [(Value, Integer)]
go [(Value, Integer)]
xs [])
go ((Value
x, Integer
n1) : [(Value, Integer)]
xs) ((Value
y, Integer
n2) : [(Value, Integer)]
ys) = case Value -> Value -> Ordering
valCmp Value
x Value
y of
Ordering
LT -> Value
-> Integer -> Integer -> [(Value, Integer)] -> [(Value, Integer)]
mergeCons Value
x Integer
n1 Integer
0 ([(Value, Integer)] -> [(Value, Integer)] -> [(Value, Integer)]
go [(Value, Integer)]
xs ((Value
y, Integer
n2) forall a. a -> [a] -> [a]
: [(Value, Integer)]
ys))
Ordering
EQ -> Value
-> Integer -> Integer -> [(Value, Integer)] -> [(Value, Integer)]
mergeCons Value
x Integer
n1 Integer
n2 ([(Value, Integer)] -> [(Value, Integer)] -> [(Value, Integer)]
go [(Value, Integer)]
xs [(Value, Integer)]
ys)
Ordering
GT -> Value
-> Integer -> Integer -> [(Value, Integer)] -> [(Value, Integer)]
mergeCons Value
y Integer
0 Integer
n2 ([(Value, Integer)] -> [(Value, Integer)] -> [(Value, Integer)]
go ((Value
x, Integer
n1) forall a. a -> [a] -> [a]
: [(Value, Integer)]
xs) [(Value, Integer)]
ys)
mergeCons :: Value
-> Integer -> Integer -> [(Value, Integer)] -> [(Value, Integer)]
mergeCons Value
a Integer
m1 Integer
m2 [(Value, Integer)]
zs = case Integer -> Integer -> Integer
g Integer
m1 Integer
m2 of
Integer
0 -> [(Value, Integer)]
zs
Integer
n -> (Value
a, Integer
n) forall a. a -> [a] -> [a]
: [(Value, Integer)]
zs
mergeM ::
Members '[Random, Error EvalError, State Mem] r =>
Value ->
[(Value, Integer)] ->
[(Value, Integer)] ->
Sem r [(Value, Integer)]
mergeM :: forall (r :: EffectRow).
Members '[Random, Error EvalError, State Mem] r =>
Value
-> [(Value, Integer)]
-> [(Value, Integer)]
-> Sem r [(Value, Integer)]
mergeM Value
g = [(Value, Integer)]
-> [(Value, Integer)] -> Sem r [(Value, Integer)]
go
where
go :: [(Value, Integer)]
-> [(Value, Integer)] -> Sem r [(Value, Integer)]
go [] [] = forall (m :: * -> *) a. Monad m => a -> m a
return []
go [] ((Value
y, Integer
n) : [(Value, Integer)]
ys) = Value
-> Integer
-> Integer
-> [(Value, Integer)]
-> Sem r [(Value, Integer)]
mergeCons Value
y Integer
0 Integer
n forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [(Value, Integer)]
-> [(Value, Integer)] -> Sem r [(Value, Integer)]
go [] [(Value, Integer)]
ys
go ((Value
x, Integer
n) : [(Value, Integer)]
xs) [] = Value
-> Integer
-> Integer
-> [(Value, Integer)]
-> Sem r [(Value, Integer)]
mergeCons Value
x Integer
n Integer
0 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [(Value, Integer)]
-> [(Value, Integer)] -> Sem r [(Value, Integer)]
go [(Value, Integer)]
xs []
go ((Value
x, Integer
n1) : [(Value, Integer)]
xs) ((Value
y, Integer
n2) : [(Value, Integer)]
ys) = case Value -> Value -> Ordering
valCmp Value
x Value
y of
Ordering
LT -> Value
-> Integer
-> Integer
-> [(Value, Integer)]
-> Sem r [(Value, Integer)]
mergeCons Value
x Integer
n1 Integer
0 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [(Value, Integer)]
-> [(Value, Integer)] -> Sem r [(Value, Integer)]
go [(Value, Integer)]
xs ((Value
y, Integer
n2) forall a. a -> [a] -> [a]
: [(Value, Integer)]
ys)
Ordering
EQ -> Value
-> Integer
-> Integer
-> [(Value, Integer)]
-> Sem r [(Value, Integer)]
mergeCons Value
x Integer
n1 Integer
n2 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [(Value, Integer)]
-> [(Value, Integer)] -> Sem r [(Value, Integer)]
go [(Value, Integer)]
xs [(Value, Integer)]
ys
Ordering
GT -> Value
-> Integer
-> Integer
-> [(Value, Integer)]
-> Sem r [(Value, Integer)]
mergeCons Value
y Integer
0 Integer
n2 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [(Value, Integer)]
-> [(Value, Integer)] -> Sem r [(Value, Integer)]
go ((Value
x, Integer
n1) forall a. a -> [a] -> [a]
: [(Value, Integer)]
xs) [(Value, Integer)]
ys
mergeCons :: Value
-> Integer
-> Integer
-> [(Value, Integer)]
-> Sem r [(Value, Integer)]
mergeCons Value
a Integer
m1 Integer
m2 [(Value, Integer)]
zs = do
Value
nm <- forall (r :: EffectRow).
Members '[Random, Error EvalError, State Mem] r =>
Value -> [Value] -> Sem r Value
evalApp Value
g [Value -> Value -> Value
VPair (Integer -> Value
intv Integer
m1) (Integer -> Value
intv Integer
m2)]
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case Value
nm of
VNum RationalDisplay
_ Rational
0 -> [(Value, Integer)]
zs
VNum RationalDisplay
_ Rational
n -> (Value
a, forall a. Ratio a -> a
numerator Rational
n) forall a. a -> [a] -> [a]
: [(Value, Integer)]
zs
Value
v -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Impossible! merge function in mergeM returned non-VNum " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Value
v
graphSummary :: Graph SimpleValue -> Value
graphSummary :: Graph SimpleValue -> Value
graphSummary = [(SimpleValue, [SimpleValue])] -> Value
toDiscoAdjMap forall b c a. (b -> c) -> (a -> b) -> a -> c
. Graph SimpleValue -> [(SimpleValue, [SimpleValue])]
reifyGraph
where
reifyGraph :: Graph SimpleValue -> [(SimpleValue, [SimpleValue])]
reifyGraph :: Graph SimpleValue -> [(SimpleValue, [SimpleValue])]
reifyGraph =
forall a. AdjacencyMap a -> [(a, [a])]
AdjMap.adjacencyList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a.
b -> (a -> b) -> (b -> b -> b) -> (b -> b -> b) -> Graph a -> b
foldg forall a. AdjacencyMap a
AdjMap.empty forall a. a -> AdjacencyMap a
AdjMap.vertex forall a.
Ord a =>
AdjacencyMap a -> AdjacencyMap a -> AdjacencyMap a
AdjMap.overlay forall a.
Ord a =>
AdjacencyMap a -> AdjacencyMap a -> AdjacencyMap a
AdjMap.connect
toDiscoAdjMap :: [(SimpleValue, [SimpleValue])] -> Value
toDiscoAdjMap :: [(SimpleValue, [SimpleValue])] -> Value
toDiscoAdjMap =
Map SimpleValue Value -> Value
VMap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ([(Value, Integer)] -> Value
VBag forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Value] -> [(Value, Integer)]
countValues forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map SimpleValue -> Value
fromSimpleValue))
resultToBool :: Member (Error EvalError) r => TestResult -> Sem r Value
resultToBool :: forall (r :: EffectRow).
Member (Error EvalError) r =>
TestResult -> Sem r Value
resultToBool (TestResult Bool
_ (TestRuntimeError EvalError
e) TestEnv
_) = forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw EvalError
e
resultToBool (TestResult Bool
b TestReason
_ TestEnv
_) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall e. Enum e => e -> Value
enumv Bool
b
notProp :: ValProp -> ValProp
notProp :: ValProp -> ValProp
notProp (VPDone TestResult
r) = TestResult -> ValProp
VPDone (TestResult -> TestResult
invertPropResult TestResult
r)
notProp (VPSearch SearchMotive
sm [Type]
tys Value
p TestEnv
e) = SearchMotive -> [Type] -> Value -> TestEnv -> ValProp
VPSearch (SearchMotive -> SearchMotive
invertMotive SearchMotive
sm) [Type]
tys Value
p TestEnv
e
notProp (VPBin LOp
LAnd ValProp
vp1 ValProp
vp2) = LOp -> ValProp -> ValProp -> ValProp
VPBin LOp
LOr (ValProp -> ValProp
notProp ValProp
vp1) (ValProp -> ValProp
notProp ValProp
vp2)
notProp (VPBin LOp
LOr ValProp
vp1 ValProp
vp2) = LOp -> ValProp -> ValProp -> ValProp
VPBin LOp
LAnd (ValProp -> ValProp
notProp ValProp
vp1) (ValProp -> ValProp
notProp ValProp
vp2)
notProp (VPBin LOp
LImpl ValProp
vp1 ValProp
vp2) = LOp -> ValProp -> ValProp -> ValProp
VPBin LOp
LAnd ValProp
vp1 (ValProp -> ValProp
notProp ValProp
vp2)
ensureProp :: Value -> ValProp
ensureProp :: Value -> ValProp
ensureProp (VProp ValProp
p) = ValProp
p
ensureProp (VInj Side
L Value
_) = TestResult -> ValProp
VPDone (Bool -> TestReason -> TestEnv -> TestResult
TestResult Bool
False forall a. TestReason_ a
TestBool TestEnv
emptyTestEnv)
ensureProp (VInj Side
R Value
_) = TestResult -> ValProp
VPDone (Bool -> TestReason -> TestEnv -> TestResult
TestResult Bool
True forall a. TestReason_ a
TestBool TestEnv
emptyTestEnv)
ensureProp Value
_ = forall a. HasCallStack => String -> a
error String
"ensureProp: non-prop value"
combineTestResultBool :: LOp -> TestResult -> TestResult -> Bool
combineTestResultBool :: LOp -> TestResult -> TestResult -> Bool
combineTestResultBool LOp
op (TestResult Bool
b1 TestReason
_ TestEnv
_) (TestResult Bool
b2 TestReason
_ TestEnv
_) = LOp -> Bool -> Bool -> Bool
interpLOp LOp
op Bool
b1 Bool
b2
testProperty ::
Members '[Random, State Mem] r =>
SearchType ->
Value ->
Sem r TestResult
testProperty :: forall (r :: EffectRow).
Members '[Random, State Mem] r =>
SearchType -> Value -> Sem r TestResult
testProperty SearchType
initialSt = forall (r :: EffectRow).
Members '[Random, State Mem] r =>
ValProp -> Sem r TestResult
checkProp forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> ValProp
ensureProp
where
checkProp ::
Members '[Random, State Mem] r =>
ValProp ->
Sem r TestResult
checkProp :: forall (r :: EffectRow).
Members '[Random, State Mem] r =>
ValProp -> Sem r TestResult
checkProp (VPDone TestResult
r) = forall (m :: * -> *) a. Monad m => a -> m a
return TestResult
r
checkProp (VPBin LOp
op ValProp
vp1 ValProp
vp2) = do
TestResult
tr1 <- forall (r :: EffectRow).
Members '[Random, State Mem] r =>
ValProp -> Sem r TestResult
checkProp ValProp
vp1
TestResult
tr2 <- forall (r :: EffectRow).
Members '[Random, State Mem] r =>
ValProp -> Sem r TestResult
checkProp ValProp
vp2
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> TestReason -> TestEnv -> TestResult
TestResult (LOp -> TestResult -> TestResult -> Bool
combineTestResultBool LOp
op TestResult
tr1 TestResult
tr2) (forall a. LOp -> TestResult -> TestResult -> TestReason_ a
TestBin LOp
op TestResult
tr1 TestResult
tr2) TestEnv
emptyTestEnv
checkProp (VPSearch SearchMotive
sm [Type]
tys Value
f TestEnv
e) =
TestEnv -> TestResult -> TestResult
extendResultEnv TestEnv
e forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (r :: EffectRow) a.
Member Random r =>
SearchType -> IEnumeration a -> Sem r ([a], SearchType)
generateSamples SearchType
initialSt IEnumeration [Value]
vals forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (r :: EffectRow).
Members '[Random, State Mem] r =>
([[Value]], SearchType) -> Sem r TestResult
go)
where
vals :: IEnumeration [Value]
vals = [Type] -> IEnumeration [Value]
enumTypes [Type]
tys
(SearchMotive (Bool
whenFound, Bool
wantsSuccess)) = SearchMotive
sm
go ::
Members '[Random, State Mem] r =>
([[Value]], SearchType) ->
Sem r TestResult
go :: forall (r :: EffectRow).
Members '[Random, State Mem] r =>
([[Value]], SearchType) -> Sem r TestResult
go ([], SearchType
st) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> TestReason -> TestEnv -> TestResult
TestResult (Bool -> Bool
not Bool
whenFound) (forall a. SearchType -> TestReason_ a
TestNotFound SearchType
st) TestEnv
emptyTestEnv
go ([Value]
x : [[Value]]
xs, SearchType
st) = do
Either EvalError ValProp
mprop <- forall e (r :: EffectRow) a.
Sem (Error e : r) a -> Sem r (Either e a)
runError (Value -> ValProp
ensureProp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: EffectRow).
Members '[Random, Error EvalError, State Mem] r =>
Value -> [Value] -> Sem r Value
evalApp Value
f [Value]
x)
case Either EvalError ValProp
mprop of
Left EvalError
err -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> TestReason -> TestEnv -> TestResult
TestResult Bool
False (forall a. EvalError -> TestReason_ a
TestRuntimeError EvalError
err) TestEnv
emptyTestEnv
Right (VPDone TestResult
r) -> forall (r :: EffectRow).
Members '[Random, State Mem] r =>
SearchType -> [[Value]] -> TestResult -> Sem r TestResult
continue SearchType
st [[Value]]
xs TestResult
r
Right ValProp
prop -> forall (r :: EffectRow).
Members '[Random, State Mem] r =>
ValProp -> Sem r TestResult
checkProp ValProp
prop forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (r :: EffectRow).
Members '[Random, State Mem] r =>
SearchType -> [[Value]] -> TestResult -> Sem r TestResult
continue SearchType
st [[Value]]
xs
continue ::
Members '[Random, State Mem] r =>
SearchType ->
[[Value]] ->
TestResult ->
Sem r TestResult
continue :: forall (r :: EffectRow).
Members '[Random, State Mem] r =>
SearchType -> [[Value]] -> TestResult -> Sem r TestResult
continue SearchType
st [[Value]]
xs r :: TestResult
r@(TestResult Bool
_ TestReason
_ TestEnv
e')
| TestResult -> Bool
testIsError TestResult
r = forall (m :: * -> *) a. Monad m => a -> m a
return TestResult
r
| TestResult -> Bool
testIsOk TestResult
r forall a. Eq a => a -> a -> Bool
== Bool
wantsSuccess =
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> TestReason -> TestEnv -> TestResult
TestResult Bool
whenFound (forall a. TestResult -> TestReason_ a
TestFound TestResult
r) TestEnv
e'
| Bool
otherwise = forall (r :: EffectRow).
Members '[Random, State Mem] r =>
([[Value]], SearchType) -> Sem r TestResult
go ([[Value]]
xs, SearchType
st)
evalApp ::
Members '[Random, Error EvalError, State Mem] r =>
Value ->
[Value] ->
Sem r Value
evalApp :: forall (r :: EffectRow).
Members '[Random, Error EvalError, State Mem] r =>
Value -> [Value] -> Sem r Value
evalApp Value
f [Value]
xs =
forall (r :: EffectRow) a. Sem (Fresh : r) a -> Sem r a
runFresh (forall (r :: EffectRow).
Members '[Fresh, Random, State Mem] r =>
CESK -> Sem r (Either EvalError Value)
runCESK (Value -> [Frame] -> CESK
Out Value
f (forall a b. (a -> b) -> [a] -> [b]
map Value -> Frame
FArgV [Value]
xs))) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw forall (m :: * -> *) a. Monad m => a -> m a
return
runTest ::
Members '[Random, Error EvalError, Input Env, State Mem] r =>
Int ->
AProperty ->
Sem r TestResult
runTest :: forall (r :: EffectRow).
Members '[Random, Error EvalError, Input Env, State Mem] r =>
Int -> AProperty -> Sem r TestResult
runTest Int
n AProperty
p = forall (r :: EffectRow).
Members '[Random, State Mem] r =>
SearchType -> Value -> Sem r TestResult
testProperty (Integer -> Integer -> SearchType
Randomized Integer
n' Integer
n') forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (r :: EffectRow).
Members '[Random, Error EvalError, Input Env, State Mem] r =>
Core -> Sem r Value
eval (AProperty -> Core
compileProperty AProperty
p)
where
n' :: Integer
n' = forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
n forall a. Integral a => a -> a -> a
`div` Int
2)
eval :: Members '[Random, Error EvalError, Input Env, State Mem] r => Core -> Sem r Value
eval :: forall (r :: EffectRow).
Members '[Random, Error EvalError, Input Env, State Mem] r =>
Core -> Sem r Value
eval Core
c = do
Env
e <- forall i (r :: EffectRow). Member (Input i) r => Sem r i
input @Env
forall (r :: EffectRow) a. Sem (Fresh : r) a -> Sem r a
runFresh (forall (r :: EffectRow).
Members '[Fresh, Random, State Mem] r =>
CESK -> Sem r (Either EvalError Value)
runCESK (Core -> Env -> [Frame] -> CESK
In Core
c Env
e [])) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw forall (m :: * -> *) a. Monad m => a -> m a
return