{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -fmax-pmcheck-models=200 #-}

-----------------------------------------------------------------------------

-----------------------------------------------------------------------------

-- |
-- Module      :  Disco.Interpret.CESK
-- Copyright   :  disco team and contributors
-- Maintainer  :  byorgey@gmail.com
--
-- SPDX-License-Identifier: BSD-3-Clause
--
-- CESK machine interpreter for Disco.
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 Math.OEIS (
--   catalogNums,
--   extendSequence,
--   lookupSequence,
--  )

import Disco.Effects.Fresh
import Disco.Effects.Input
import Disco.Effects.Random
import Polysemy
import Polysemy.Error
import Polysemy.State

------------------------------------------------------------
-- Utilities
------------------------------------------------------------

------------------------------------------------------------
-- Frames and continuations
------------------------------------------------------------

-- The CESK machine carries a current continuation explaining what to
-- do with the value of the currently focused expression, once it has
-- been fully evaluated.

-- | A continuation is just a stack of frames.
type Cont = [Frame]

-- | A frame represents a single step of the context, explaining what
--   to do with a value in that context (ultimately transforming it
--   into another value, which may in turn be handed to the next frame
--   in the continuation stack, and so on).
--
--   As an invariant, any 'Frame' containing unevaluated 'Core'
--   expressions must also carry an 'Env' in which to evaluate them.
data Frame
  = -- | Inject the value into a sum type.
    FInj Side
  | -- | Do a case analysis on the value.
    FCase Env (Bind (Name Core) Core) (Bind (Name Core) Core)
  | -- | Evaluate the right-hand value of a pair once we have finished
    --   evaluating the left-hand side.
    FPairR Env Core
  | -- | Put the value into the right-hand side of a pair together with
    --   this previously evaluated left-hand side.
    FPairL Value
  | -- | Project one or the other side of a pair.
    FProj Side
  | -- | Evaluate the argument of an application once we have finished
    --   evaluating the function.
    FArg Env Core
  | -- | Apply an evaluated function to this already-evaluated argument.
    FArgV Value
  | -- | Apply a previously evaluated function to the value.
    FApp Value
  | -- | Force evaluation of the contents of a memory cell.
    FForce
  | -- | Update the contents of a memory cell with its evaluation.
    FUpdate Int
  | -- | Record the results of a test.
    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)

------------------------------------------------------------
-- The CESK machine
------------------------------------------------------------

-- | The CESK machine has two basic kinds of states.
data CESK
  = -- | The 'In' constructor represents the state when we are recursing
    --   "into" a term.  There is a currently focused expression which
    --   is to be evaluated in the given context.  Generally, evaluation
    --   proceeds by pattern-matching on the focused expression and
    --   either immediately turning it into a value (if it is simple),
    --   or focusing on a subexpression and pushing a new frame on the
    --   continuation stack indicating how to continue evaluating the
    --   whole expression once finished with the subexpression.
    In Core Env Cont
  | -- | The 'Out' constructor represents the state when we have
    --   completed evaluating an expression and are now on our way back
    --   "out" of the recursion.  Generally, evaluation proceeds by
    --   pattern-matching on the top frame of the continuation stack
    --   (and sometimes on the value as well), to see what is to be done
    --   with the value.
    Out Value Cont
  | -- | There is also an 'Up' constructor representing an exception
    --   that is propagating up the continuation stack.  Disco does
    --   not have user-level exceptions or try/catch blocks etc., but
    --   exceptions may be caught by test frames and turned into a
    --   test result rather than crashing the entire computation.
    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)

-- | Is the CESK machine in a final state?
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

-- | Run a CESK machine to completion.
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

-- | Advance the CESK machine by one step.
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
  -- Annoying to repeat this code, not sure of a better way.
  -- The usual evaluation order (function then argument) doesn't work when
  -- we're applying a test function to randomly generated values.
  (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"

------------------------------------------------------------
-- Interpreting constants
------------------------------------------------------------

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
  --------------------------------------------------
  -- Basics

  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
  --------------------------------------------------
  -- Arithmetic

  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

  --------------------------------------------------
  -- Number theory

  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
    -- Semantics of the @$factor@ prim: turn a natural number into its
    -- bag of prime factors.  Crash if called on 0, which does not have
    -- a prime factorization.
    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
    -- Semantics of the @$frac@ prim: turn a rational number into a pair
    -- of its numerator and denominator.
    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))

  --------------------------------------------------
  -- Combinatorics

  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

  --------------------------------------------------
  -- Sequences

  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)
  -- OLookupSeq -> out . oeisLookup
  -- OExtendSeq -> out . oeisExtend
  --------------------------------------------------
  -- Comparison

  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)
  --------------------------------------------------
  -- Container operations

  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]
  --------------------------------------------------
  -- Container conversions

  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)
  -- Bag (a, N) -> Bag a
  --   Notionally this takes a set of pairs instead of a bag, but operationally we need to
  --   be prepared for a bag, because of the way literal bags desugar, e.g.
  --
  --   Disco> :desugar let x = 3 in ⟅ 'a' # (2 + x), 'b', 'b' ⟆
  --   (λx. bagFromCounts(bag(('a', 2 + x) :: ('b', 1) :: ('b', 1) :: [])))(3)

  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))

  --------------------------------------------------
  -- Maps

  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)

  --------------------------------------------------
  -- Graph operations

  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
  --------------------------------------------------
  -- Propositions

  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

--------------------------------------------------
-- Arithmetic

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

-- | Perform a square root operation. If the program typechecks,
--   then the argument and output will really be Natural.
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

-- | implementation of `integerSqrt'` taken from the Haskell wiki:
--   https://wiki.haskell.org/Generic_number_type#squareRoot
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

-- this operator is used for `integerSqrt'`
(^!) :: 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

------------------------------------------------------------
-- Comparison
------------------------------------------------------------

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

------------------------------------------------------------
-- Polynomial sequences [a,b,c,d .. e]
------------------------------------------------------------

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

-- | Extend a sequence infinitely by interpolating it as a polynomial
--   sequence, via forward differences.  Essentially the same
--   algorithm used by Babbage's famous Difference Engine.
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)))

-- | Compute the forward difference of the given sequence, that is,
--   differences of consecutive pairs of elements.
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

-- | Take forward differences until the result is constant, and return
--   the constant.  The sign of the constant difference tells us the
--   limiting behavior of the sequence.
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))

------------------------------------------------------------
-- OEIS
------------------------------------------------------------

-- -- | Looks up a sequence of integers in OEIS.
-- --   Returns 'left()' if the sequence is unknown in OEIS,
-- --   otherwise 'right "https://oeis.org/<oeis_sequence_id>"'
-- oeisLookup :: Value -> Value
-- oeisLookup (vlist vint -> ns) = maybe VNil parseResult (lookupSequence ns)
--  where
--   parseResult r = VInj R (listv charv ("https://oeis.org/" ++ seqNum r))
--   seqNum = getCatalogNum . catalogNums

--   getCatalogNum [] = error "No catalog info"
--   getCatalogNum (n : _) = n

-- -- | Extends a Disco integer list with data from a known OEIS
-- --   sequence.  Returns a list of integers upon success, otherwise the
-- --   original list (unmodified).
-- oeisExtend :: Value -> Value
-- oeisExtend = listv intv . extendSequence . vlist vint

------------------------------------------------------------
-- Normalizing bags/sets
------------------------------------------------------------

-- | Given a list of disco values, sort and collate them into a list
--   pairing each unique value with its count.  Used to
--   construct/normalize bags and sets.  Prerequisite: the values must
--   be comparable.
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)

-- | Normalize a list of values where each value is paired with a
--   count, but there could be duplicate values.  This function uses
--   merge sort to sort the values, adding the counts of multiple
--   instances of the same value.  Prerequisite: the values must be
--   comparable.
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

-- | Generic function for merging two sorted, count-annotated lists of
--   type @[(a,Integer)]@ a la merge sort, using the given comparison
--   function, and using the provided count combining function to
--   decide what count to assign to each element of the output.  For
--   example, @(+)@ corresponds to bag union; @min@ corresponds to
--   intersection; and so on.
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

------------------------------------------------------------
-- Graphs
------------------------------------------------------------

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))

------------------------------------------------------------
-- Propositions / tests
------------------------------------------------------------

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)

-- | Convert a @Value@ to a @ValProp@, embedding booleans if necessary.
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)

------------------------------------------------------------
-- Top-level evaluation
------------------------------------------------------------

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