{-# 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,
  evalApp,
  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.Functor (($>))
import Data.List (find)
import qualified Data.List.Infinite as InfList
import qualified Data.Map as M
import Data.Maybe (isJust)
import Data.Ratio
import qualified Data.Text as T
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.Effects.Fresh
import Disco.Effects.Input
import Disco.Enumerate
import Disco.Error
import Disco.Names
import Disco.Property
import Disco.Syntax.Operators (BOp (..))
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 (
  SearchStatus (SubSeq),
  extendSeq,
  lookupSeq,
  number,
 )
import Polysemy
import Polysemy.Error
import Polysemy.Random
import Polysemy.State
import qualified System.Random as R

------------------------------------------------------------
-- 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
  | -- | Given the index of a memory cell and a function's arguments,
    --   memoize the results of a function.
    FMemo Int SimpleValue
  deriving (Int -> Frame -> ShowS
[Frame] -> ShowS
Frame -> String
(Int -> Frame -> ShowS)
-> (Frame -> String) -> ([Frame] -> ShowS) -> Show Frame
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Frame -> ShowS
showsPrec :: Int -> Frame -> ShowS
$cshow :: Frame -> String
show :: Frame -> String
$cshowList :: [Frame] -> ShowS
showList :: [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
(Int -> CESK -> ShowS)
-> (CESK -> String) -> ([CESK] -> ShowS) -> Show CESK
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CESK -> ShowS
showsPrec :: Int -> CESK -> ShowS
$cshow :: CESK -> String
show :: CESK -> String
$cshowList :: [CESK] -> ShowS
showList :: [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 []) = Either EvalError Value -> Maybe (Either EvalError Value)
forall a. a -> Maybe a
Just (EvalError -> Either EvalError Value
forall a b. a -> Either a b
Left EvalError
e)
isFinal (Out Value
v []) = Either EvalError Value -> Maybe (Either EvalError Value)
forall a. a -> Maybe a
Just (Value -> Either EvalError Value
forall a b. b -> Either a b
Right Value
v)
isFinal CESK
_ = Maybe (Either EvalError Value)
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 -> Either EvalError Value -> Sem r (Either EvalError Value)
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return Either EvalError Value
res
  Maybe (Either EvalError Value)
Nothing -> CESK -> Sem r CESK
forall (r :: EffectRow).
Members '[Fresh, Random, State Mem] r =>
CESK -> Sem r CESK
step CESK
cesk Sem r CESK
-> (CESK -> Sem r (Either EvalError Value))
-> Sem r (Either EvalError Value)
forall a b. Sem r a -> (a -> Sem r b) -> Sem r b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= CESK -> Sem r (Either EvalError Value)
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 QName Core -> Env -> Maybe Value
forall a b. QName a -> Ctx a b -> Maybe b
Ctx.lookup' QName Core
x Env
e of
    Maybe Value
Nothing -> CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ EvalError -> [Frame] -> CESK
Up (QName Core -> EvalError
forall core. QName core -> EvalError
UnboundError QName Core
x) [Frame]
k
    Just Value
v -> CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Value -> [Frame] -> CESK
Out Value
v [Frame]
k
  (In (CNum Rational
r) Env
_ [Frame]
k) -> CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Value -> [Frame] -> CESK
Out (Rational -> Value
VNum Rational
r) [Frame]
k
  (In (CConst Op
OMatchErr) Env
_ [Frame]
k) -> CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ EvalError -> [Frame] -> CESK
Up EvalError
NonExhaustive [Frame]
k
  (In (CConst Op
OEmptyGraph) Env
_ [Frame]
k) -> CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Value -> [Frame] -> CESK
Out (Graph SimpleValue -> Value
VGraph Graph SimpleValue
forall a. Graph a
empty) [Frame]
k
  (In (CConst Op
op) Env
_ [Frame]
k) -> CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
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) -> CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Core -> Env -> [Frame] -> CESK
In Core
c Env
e (Side -> Frame
FInj Side
s Frame -> [Frame] -> [Frame]
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) -> CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
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 Frame -> [Frame] -> [Frame]
forall a. a -> [a] -> [a]
: [Frame]
k)
  (In Core
CUnit Env
_ [Frame]
k) -> CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
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) -> CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Core -> Env -> [Frame] -> CESK
In Core
c1 Env
e (Env -> Core -> Frame
FPairR Env
e Core
c2 Frame -> [Frame] -> [Frame]
forall a. a -> [a] -> [a]
: [Frame]
k)
  (In (CProj Side
s Core
c) Env
e [Frame]
k) -> CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Core -> Env -> [Frame] -> CESK
In Core
c Env
e (Side -> Frame
FProj Side
s Frame -> [Frame] -> [Frame]
forall a. a -> [a] -> [a]
: [Frame]
k)
  (In (CAbs ShouldMemo
mem Bind [Name Core] Core
b) Env
e [Frame]
k) -> do
    ([Name Core]
xs, Core
body) <- Bind [Name Core] Core -> Sem r ([Name Core], Core)
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
    case ShouldMemo
mem of
      ShouldMemo
Memo -> do
        Int
cell <- Value -> Sem r Int
forall (r :: EffectRow).
Members '[State Mem] r =>
Value -> Sem r Int
allocateValue (Map SimpleValue Value -> Value
VMap Map SimpleValue Value
forall k a. Map k a
M.empty)
        CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Value -> [Frame] -> CESK
Out (Maybe (Int, [Value]) -> Env -> [Name Core] -> Core -> Value
VClo ((Int, [Value]) -> Maybe (Int, [Value])
forall a. a -> Maybe a
Just (Int
cell, [])) Env
e [Name Core]
xs Core
body) [Frame]
k
      ShouldMemo
NoMemo -> CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Value -> [Frame] -> CESK
Out (Maybe (Int, [Value]) -> Env -> [Name Core] -> Core -> Value
VClo Maybe (Int, [Value])
forall a. Maybe a
Nothing Env
e [Name Core]
xs Core
body) [Frame]
k
  (In (CApp Core
c1 Core
c2) Env
e [Frame]
k) -> CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Core -> Env -> [Frame] -> CESK
In Core
c1 Env
e (Env -> Core -> Frame
FArg Env
e Core
c2 Frame -> [Frame] -> [Frame]
forall a. a -> [a] -> [a]
: [Frame]
k)
  (In (CType Type
ty) Env
_ [Frame]
k) -> CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
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) <- Bind [Name Core] [Core] -> Sem r ([Name Core], [Core])
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 <- Env -> [(QName Core, Core)] -> Sem r [Int]
forall (r :: EffectRow).
Members '[State Mem] r =>
Env -> [(QName Core, Core)] -> Sem r [Int]
allocateRec Env
e ([QName Core] -> [Core] -> [(QName Core, Core)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((Name Core -> QName Core) -> [Name Core] -> [QName Core]
forall a b. (a -> b) -> [a] -> [b]
map Name Core -> QName Core
forall a. Name a -> QName a
localName [Name Core]
xs) [Core]
cs)
    CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Value -> [Frame] -> CESK
Out ((Int -> Value -> Value) -> Value -> [Int] -> Value
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Value -> Value -> Value
VPair (Value -> Value -> Value)
-> (Int -> Value) -> Int -> Value -> Value
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) -> CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Core -> Env -> [Frame] -> CESK
In Core
c Env
e (Frame
FForce Frame -> [Frame] -> [Frame]
forall a. a -> [a] -> [a]
: [Frame]
k)
  (In (CTest [(String, Type, Name Core)]
vars Core
c) Env
e [Frame]
k) -> CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
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 Frame -> [Frame] -> [Frame]
forall a. a -> [a] -> [a]
: [Frame]
k)
  (Out Value
v (FInj Side
s : [Frame]
k)) -> CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
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) <- Bind (Name Core) Core -> Sem r (Name Core, Core)
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
    CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Core -> Env -> [Frame] -> CESK
In Core
c1 (QName Core -> Value -> Env -> Env
forall a b. QName a -> b -> Ctx a b -> Ctx a b
Ctx.insert (Name Core -> QName Core
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) <- Bind (Name Core) Core -> Sem r (Name Core, Core)
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
    CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Core -> Env -> [Frame] -> CESK
In Core
c2 (QName Core -> Value -> Env -> Env
forall a b. QName a -> b -> Ctx a b -> Ctx a b
Ctx.insert (Name Core -> QName Core
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)) -> CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Core -> Env -> [Frame] -> CESK
In Core
c2 Env
e (Value -> Frame
FPairL Value
v1 Frame -> [Frame] -> [Frame]
forall a. a -> [a] -> [a]
: [Frame]
k)
  (Out Value
v2 (FPairL Value
v1 : [Frame]
k)) -> CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
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)) -> CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Value -> [Frame] -> CESK
Out (Side -> Value -> Value -> Value
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)) -> CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Core -> Env -> [Frame] -> CESK
In Core
c2 Env
e (Value -> Frame
FApp Value
v Frame -> [Frame] -> [Frame]
forall a. a -> [a] -> [a]
: [Frame]
k)
  (Out Value
v (FMemo Int
n SimpleValue
sv : [Frame]
k)) -> Int -> SimpleValue -> Value -> Sem r ()
forall (r :: EffectRow).
Members '[State Mem] r =>
Int -> SimpleValue -> Value -> Sem r ()
memoSet Int
n SimpleValue
sv Value
v Sem r () -> CESK -> Sem r CESK
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Value -> [Frame] -> CESK
Out Value
v [Frame]
k
  (Out Value
v (FApp (VClo Maybe (Int, [Value])
mi Env
e [Name Core
x] Core
b) : [Frame]
k)) -> case Maybe (Int, [Value])
mi of
    Maybe (Int, [Value])
Nothing -> CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Core -> Env -> [Frame] -> CESK
In Core
b (QName Core -> Value -> Env -> Env
forall a b. QName a -> b -> Ctx a b -> Ctx a b
Ctx.insert (Name Core -> QName Core
forall a. Name a -> QName a
localName Name Core
x) Value
v Env
e) [Frame]
k
    Just (Int
n, [Value]
mem) -> do
      let sv :: SimpleValue
sv = Value -> SimpleValue
toSimpleValue (Value -> SimpleValue) -> Value -> SimpleValue
forall a b. (a -> b) -> a -> b
$ (Value -> Value -> Value) -> Value -> [Value] -> Value
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Value -> Value -> Value
VPair Value
VUnit (Value
v Value -> [Value] -> [Value]
forall a. a -> [a] -> [a]
: [Value]
mem)
      Maybe Value
mv <- Int -> SimpleValue -> Sem r (Maybe Value)
forall (r :: EffectRow).
Members '[State Mem] r =>
Int -> SimpleValue -> Sem r (Maybe Value)
memoLookup Int
n SimpleValue
sv
      case Maybe Value
mv of
        Maybe Value
Nothing -> CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Core -> Env -> [Frame] -> CESK
In Core
b (QName Core -> Value -> Env -> Env
forall a b. QName a -> b -> Ctx a b -> Ctx a b
Ctx.insert (Name Core -> QName Core
forall a. Name a -> QName a
localName Name Core
x) Value
v Env
e) (Int -> SimpleValue -> Frame
FMemo Int
n SimpleValue
sv Frame -> [Frame] -> [Frame]
forall a. a -> [a] -> [a]
: [Frame]
k)
        Just Value
v' -> CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Value -> [Frame] -> CESK
Out Value
v' [Frame]
k
  (Out Value
v (FApp (VClo Maybe (Int, [Value])
mi Env
e (Name Core
x : [Name Core]
xs) Core
b) : [Frame]
k)) -> CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Value -> [Frame] -> CESK
Out (Maybe (Int, [Value]) -> Env -> [Name Core] -> Core -> Value
VClo (([Value] -> [Value]) -> (Int, [Value]) -> (Int, [Value])
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 (Value
v Value -> [Value] -> [Value]
forall a. a -> [a] -> [a]
:) ((Int, [Value]) -> (Int, [Value]))
-> Maybe (Int, [Value]) -> Maybe (Int, [Value])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Int, [Value])
mi) (QName Core -> Value -> Env -> Env
forall a b. QName a -> b -> Ctx a b -> Ctx a b
Ctx.insert (Name Core -> QName Core
forall a. Name a -> QName a
localName Name Core
x) Value
v Env
e) [Name Core]
xs Core
b) [Frame]
k
  (Out Value
v2 (FApp (VConst Op
op) : [Frame]
k)) -> [Frame] -> Op -> Value -> Sem r CESK
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)) -> CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
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 Maybe (Int, [Value])
_ Env
e [Name Core
x] Core
b) (FArgV Value
v : [Frame]
k)) -> CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Core -> Env -> [Frame] -> CESK
In Core
b (QName Core -> Value -> Env -> Env
forall a b. QName a -> b -> Ctx a b -> Ctx a b
Ctx.insert (Name Core -> QName Core
forall a. Name a -> QName a
localName Name Core
x) Value
v Env
e) [Frame]
k
  (Out (VClo Maybe (Int, [Value])
mi Env
e (Name Core
x : [Name Core]
xs) Core
b) (FArgV Value
v : [Frame]
k)) -> CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Value -> [Frame] -> CESK
Out (Maybe (Int, [Value]) -> Env -> [Name Core] -> Core -> Value
VClo Maybe (Int, [Value])
mi (QName Core -> Value -> Env -> Env
forall a b. QName a -> b -> Ctx a b -> Ctx a b
Ctx.insert (Name Core -> QName Core
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)) -> [Frame] -> Op -> Value -> Sem r CESK
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)) -> CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
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 <- Int -> Sem r (Maybe Cell)
forall (r :: EffectRow).
Members '[State Mem] r =>
Int -> Sem r (Maybe Cell)
lkup Int
n
    case Maybe Cell
cell of
      Maybe Cell
Nothing -> String -> Sem r CESK
forall a. HasCallStack => String -> a
error (String -> Sem r CESK) -> String -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ String
"impossible: location " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" not found in memory"
      Just (V Value
v) -> CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Value -> [Frame] -> CESK
Out Value
v [Frame]
k
      Just (E Env
e Core
t) -> do
        Int -> Cell -> Sem r ()
forall (r :: EffectRow).
Members '[State Mem] r =>
Int -> Cell -> Sem r ()
set Int
n Cell
Blackhole
        CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Core -> Env -> [Frame] -> CESK
In Core
t Env
e (Int -> Frame
FUpdate Int
n Frame -> [Frame] -> [Frame]
forall a. a -> [a] -> [a]
: [Frame]
k)
      Just Cell
Blackhole -> CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ EvalError -> [Frame] -> CESK
Up EvalError
InfiniteLoop [Frame]
k
  (Out Value
v (FUpdate Int
n : [Frame]
k)) -> do
    Int -> Cell -> Sem r ()
forall (r :: EffectRow).
Members '[State Mem] r =>
Int -> Cell -> Sem r ()
set Int
n (Value -> Cell
V Value
v)
    CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Value -> [Frame] -> CESK
Out Value
v [Frame]
k
  (Up EvalError
err (f :: Frame
f@FTest {} : [Frame]
k)) ->
    CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Value -> [Frame] -> CESK
Out (ValProp -> Value
VProp (TestResult -> ValProp
VPDone (Bool -> TestReason -> TestEnv -> TestResult
TestResult Bool
False (EvalError -> TestReason
forall a. EvalError -> TestReason_ a
TestRuntimeError EvalError
err) TestEnv
emptyTestEnv))) (Frame
f Frame -> [Frame] -> [Frame]
forall a. a -> [a] -> [a]
: [Frame]
k)
  (Up EvalError
err (Frame
_ : [Frame]
ks)) -> CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
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 -> CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ EvalError -> [Frame] -> CESK
Up EvalError
err [Frame]
k
      Right TestEnv
e' -> CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Value -> [Frame] -> CESK
Out (ValProp -> Value
VProp (ValProp -> Value) -> ValProp -> Value
forall a b. (a -> b) -> a -> b
$ TestEnv -> ValProp -> ValProp
extendPropEnv TestEnv
e' ValProp
result) [Frame]
k
  CESK
_ -> String -> Sem r 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 = String -> a
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 = String -> a
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 (EvalError -> Sem r CESK)
-> (Value -> EvalError) -> Value -> Sem r CESK
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> EvalError
Crash (String -> EvalError) -> (Value -> String) -> Value -> EvalError
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Value -> Char) -> Value -> String
forall a. (Value -> a) -> Value -> [a]
vlist Value -> Char
vchar
  Op
OId -> Value -> Sem r CESK
out
  --------------------------------------------------
  -- Arithmetic

  Op
OAdd -> (Rational -> Rational -> Rational) -> Value -> Sem r Value
forall (r :: EffectRow).
(Rational -> Rational -> Rational) -> Value -> Sem r Value
numOp2 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
(+) (Value -> Sem r Value)
-> (Value -> Sem r CESK) -> Value -> Sem r CESK
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Value -> Sem r CESK
out
  Op
ONeg -> (Rational -> Rational) -> Value -> Sem r Value
forall (r :: EffectRow).
(Rational -> Rational) -> Value -> Sem r Value
numOp1 Rational -> Rational
forall a. Num a => a -> a
negate (Value -> Sem r Value)
-> (Value -> Sem r CESK) -> Value -> Sem r CESK
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Value -> Sem r CESK
out
  Op
OSqrt -> (Rational -> Rational) -> Value -> Sem r Value
forall (r :: EffectRow).
(Rational -> Rational) -> Value -> Sem r Value
numOp1 Rational -> Rational
integerSqrt (Value -> Sem r Value)
-> (Value -> Sem r CESK) -> Value -> Sem r CESK
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Value -> Sem r CESK
out
  Op
OFloor -> (Rational -> Rational) -> Value -> Sem r Value
forall (r :: EffectRow).
(Rational -> Rational) -> Value -> Sem r Value
numOp1 ((Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
1) (Integer -> Rational)
-> (Rational -> Integer) -> Rational -> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Integer
forall b. Integral b => Rational -> b
forall a b. (RealFrac a, Integral b) => a -> b
floor) (Value -> Sem r Value)
-> (Value -> Sem r CESK) -> Value -> Sem r CESK
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Value -> Sem r CESK
out
  Op
OCeil -> (Rational -> Rational) -> Value -> Sem r Value
forall (r :: EffectRow).
(Rational -> Rational) -> Value -> Sem r Value
numOp1 ((Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
1) (Integer -> Rational)
-> (Rational -> Integer) -> Rational -> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Integer
forall b. Integral b => Rational -> b
forall a b. (RealFrac a, Integral b) => a -> b
ceiling) (Value -> Sem r Value)
-> (Value -> Sem r CESK) -> Value -> Sem r CESK
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Value -> Sem r CESK
out
  Op
OAbs -> (Rational -> Rational) -> Value -> Sem r Value
forall (r :: EffectRow).
(Rational -> Rational) -> Value -> Sem r Value
numOp1 Rational -> Rational
forall a. Num a => a -> a
abs (Value -> Sem r Value)
-> (Value -> Sem r CESK) -> Value -> Sem r CESK
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Value -> Sem r CESK
out
  Op
OMul -> (Rational -> Rational -> Rational) -> Value -> Sem r Value
forall (r :: EffectRow).
(Rational -> Rational -> Rational) -> Value -> Sem r Value
numOp2 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
(*) (Value -> Sem r Value)
-> (Value -> Sem r CESK) -> Value -> Sem r CESK
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Value -> Sem r CESK
out
  Op
ODiv -> (Rational -> Rational -> Sem (Error EvalError : r) Value)
-> Value -> Sem (Error EvalError : r) Value
forall (r :: EffectRow).
(Rational -> Rational -> Sem r Value) -> Value -> Sem r Value
numOp2' Rational -> Rational -> Sem (Error EvalError : r) Value
forall (r :: EffectRow).
Member (Error EvalError) r =>
Rational -> Rational -> Sem r Value
divOp (Value -> Sem (Error EvalError : r) Value)
-> (Sem (Error EvalError : r) Value -> Sem r CESK)
-> Value
-> Sem r CESK
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> Sem (Error EvalError : r) Value -> Sem r CESK
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 = EvalError -> Sem r Value
forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw EvalError
DivByZero
    divOp Rational
m Rational
n = Value -> Sem r Value
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Sem r Value) -> Value -> Sem r Value
forall a b. (a -> b) -> a -> b
$ Rational -> Value
ratv (Rational
m Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ Rational
n)
  Op
OExp -> (Rational -> Rational -> Sem (Error EvalError : r) Value)
-> Value -> Sem (Error EvalError : r) Value
forall (r :: EffectRow).
(Rational -> Rational -> Sem r Value) -> Value -> Sem r Value
numOp2' Rational -> Rational -> Sem (Error EvalError : r) Value
forall (r :: EffectRow).
Member (Error EvalError) r =>
Rational -> Rational -> Sem r Value
expOp (Value -> Sem (Error EvalError : r) Value)
-> (Sem (Error EvalError : r) Value -> Sem r CESK)
-> Value
-> Sem r CESK
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> Sem (Error EvalError : r) Value -> Sem r CESK
forall (r :: EffectRow).
Sem (Error EvalError : r) Value -> Sem r CESK
outWithErr
   where
    expOp :: Member (Error EvalError) r => Rational -> Rational -> Sem r Value
    expOp :: forall (r :: EffectRow).
Member (Error EvalError) r =>
Rational -> Rational -> Sem r Value
expOp Rational
m Rational
n
      | Rational
m Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
== Rational
0 Bool -> Bool -> Bool
&& Rational
n Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
< Rational
0 = EvalError -> Sem r Value
forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw EvalError
DivByZero
      | Bool
otherwise = Value -> Sem r Value
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Sem r Value) -> Value -> Sem r Value
forall a b. (a -> b) -> a -> b
$ Rational -> Value
ratv (Rational
m Rational -> Integer -> Rational
forall a b. (Fractional a, Integral b) => a -> b -> a
^^ Rational -> Integer
forall a. Ratio a -> a
numerator Rational
n)
  Op
OMod -> (Rational -> Rational -> Sem (Error EvalError : r) Value)
-> Value -> Sem (Error EvalError : r) Value
forall (r :: EffectRow).
(Rational -> Rational -> Sem r Value) -> Value -> Sem r Value
numOp2' Rational -> Rational -> Sem (Error EvalError : r) Value
forall (r :: EffectRow).
Member (Error EvalError) r =>
Rational -> Rational -> Sem r Value
modOp (Value -> Sem (Error EvalError : r) Value)
-> (Sem (Error EvalError : r) Value -> Sem r CESK)
-> Value
-> Sem r CESK
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> Sem (Error EvalError : r) Value -> Sem r CESK
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 Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
== Rational
0 = EvalError -> Sem r Value
forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw EvalError
DivByZero
      | Bool
otherwise = Value -> Sem r Value
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Sem r Value) -> Value -> Sem r Value
forall a b. (a -> b) -> a -> b
$ Integer -> Value
intv (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
m Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Rational -> Integer
forall a. Ratio a -> a
numerator Rational
n)
  Op
ODivides -> (Rational -> Rational -> Sem r Value) -> Value -> Sem r Value
forall (r :: EffectRow).
(Rational -> Rational -> Sem r Value) -> Value -> Sem r Value
numOp2' (\Rational
m Rational
n -> Value -> Sem r Value
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Value
boolv (Bool -> Value) -> Bool -> Value
forall a b. (a -> b) -> a -> b
$ Rational -> Rational -> Bool
divides Rational
m Rational
n)) (Value -> Sem r Value)
-> (Value -> Sem r CESK) -> Value -> Sem r CESK
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Value -> Sem r CESK
out
  --------------------------------------------------
  -- Number theory

  Op
OIsPrime -> (Integer -> Value) -> Value -> Sem r Value
forall (r :: EffectRow). (Integer -> Value) -> Value -> Sem r Value
intOp1 (Bool -> Value
boolv (Bool -> Value) -> (Integer -> Bool) -> Integer -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Bool
isPrime) (Value -> Sem r Value)
-> (Value -> Sem r CESK) -> Value -> Sem r CESK
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Value -> Sem r CESK
out
  Op
OFactor -> (Integer -> Sem (Error EvalError : r) Value)
-> Value -> Sem (Error EvalError : r) Value
forall (r :: EffectRow).
(Integer -> Sem r Value) -> Value -> Sem r Value
intOp1' Integer -> Sem (Error EvalError : r) Value
forall (r :: EffectRow).
Member (Error EvalError) r =>
Integer -> Sem r Value
primFactor (Value -> Sem (Error EvalError : r) Value)
-> (Sem (Error EvalError : r) Value -> Sem r CESK)
-> Value
-> Sem r CESK
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> Sem (Error EvalError : r) Value -> Sem r CESK
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 = EvalError -> Sem r Value
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 = Value -> Sem r Value
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Sem r Value)
-> ([(Value, Integer)] -> Value)
-> [(Value, Integer)]
-> Sem r Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Value, Integer)] -> Value
VBag ([(Value, Integer)] -> Sem r Value)
-> [(Value, Integer)] -> Sem r Value
forall a b. (a -> b) -> a -> b
$ ((Prime Integer, Word) -> (Value, Integer))
-> [(Prime Integer, Word)] -> [(Value, Integer)]
forall a b. (a -> b) -> [a] -> [b]
map ((Integer -> Value
intv (Integer -> Value)
-> (Prime Integer -> Integer) -> Prime Integer -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Prime Integer -> Integer
forall a. Prime a -> a
unPrime) (Prime Integer -> Value)
-> (Word -> Integer) -> (Prime Integer, Word) -> (Value, Integer)
forall b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** Word -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral) (Integer -> [(Prime Integer, Word)]
forall a. UniqueFactorisation a => a -> [(Prime a, Word)]
factorise Integer
n)
  Op
OFrac -> (Rational -> Sem r Value) -> Value -> Sem r Value
forall (r :: EffectRow).
(Rational -> Sem r Value) -> Value -> Sem r Value
numOp1' (Value -> Sem r Value
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Sem r Value)
-> (Rational -> Value) -> Rational -> Sem r Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Value
primFrac) (Value -> Sem r Value)
-> (Value -> Sem r CESK) -> Value -> Sem r CESK
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 (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
r)) (Integer -> Value
intv (Rational -> Integer
forall a. Ratio a -> a
denominator Rational
r))

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

  Op
OMultinom -> (Value -> Value -> Sem r Value) -> Value -> Sem r Value
forall a. (Value -> Value -> a) -> Value -> a
arity2 Value -> Value -> Sem r Value
forall (r :: EffectRow). Value -> Value -> Sem r Value
multinomOp (Value -> Sem r Value)
-> (Value -> Sem r CESK) -> Value -> Sem r CESK
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) ((Value -> Integer) -> Value -> [Integer]
forall a. (Value -> a) -> Value -> [a]
vlist Value -> Integer
vint -> [Integer]
ks0) = Value -> Sem r Value
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Sem r Value)
-> (Integer -> Value) -> Integer -> Sem r Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Value
intv (Integer -> Sem r Value) -> Integer -> Sem r Value
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' Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
n = Integer
0
        | Bool
otherwise = Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
choose Integer
n Integer
k' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer -> [Integer] -> Integer
multinomial (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
k') [Integer]
ks
  Op
OFact -> (Rational -> Sem (Error EvalError : r) Value)
-> Value -> Sem (Error EvalError : r) Value
forall (r :: EffectRow).
(Rational -> Sem r Value) -> Value -> Sem r Value
numOp1' Rational -> Sem (Error EvalError : r) Value
forall (r :: EffectRow).
Member (Error EvalError) r =>
Rational -> Sem r Value
factOp (Value -> Sem (Error EvalError : r) Value)
-> (Sem (Error EvalError : r) Value -> Sem r CESK)
-> Value
-> Sem r CESK
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> Sem (Error EvalError : r) Value -> Sem r CESK
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 (Rational -> Integer
forall a. Ratio a -> a
numerator -> Integer
n)
      | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
forall a. Bounded a => a
maxBound :: Int) = EvalError -> Sem r Value
forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw EvalError
Overflow
      | Bool
otherwise = Value -> Sem r Value
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Sem r Value)
-> (Integer -> Value) -> Integer -> Sem r Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Value
intv (Integer -> Sem r Value) -> Integer -> Sem r Value
forall a b. (a -> b) -> a -> b
$ Int -> Integer
forall a. (Integral a, Bits a) => Int -> a
factorial (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n)
  Op
OEnum -> Value -> Sem r CESK
out (Value -> Sem r CESK) -> (Value -> Value) -> Value -> Sem r CESK
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Value
enumOp
   where
    enumOp :: Value -> Value
    enumOp :: Value -> Value
enumOp (VType Type
ty) = (Value -> Value) -> [Value] -> Value
forall a. (a -> Value) -> [a] -> Value
listv Value -> Value
forall a. a -> a
id (Type -> [Value]
enumerateType Type
ty)
    enumOp Value
v = String -> Value
forall a. HasCallStack => String -> a
error (String -> Value) -> String -> Value
forall a b. (a -> b) -> a -> b
$ String
"Impossible! enumOp on non-type " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
forall a. Show a => a -> String
show Value
v
  Op
OCount -> Value -> Sem r CESK
out (Value -> Sem r CESK) -> (Value -> Value) -> Value -> Sem r CESK
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 = String -> Value
forall a. HasCallStack => String -> a
error (String -> Value) -> String -> Value
forall a b. (a -> b) -> a -> b
$ String
"Impossible! countOp on non-type " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
forall a. Show a => a -> String
show Value
v

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

  Op
OUntil -> (Value -> Value -> Sem r CESK) -> Value -> Sem r CESK
forall a. (Value -> Value -> a) -> Value -> a
arity2 ((Value -> Value -> Sem r CESK) -> Value -> Sem r CESK)
-> (Value -> Value -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ \Value
v1 -> Value -> Sem r CESK
out (Value -> Sem r CESK) -> (Value -> Value) -> Value -> Sem r CESK
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ellipsis Value -> Value -> Value
ellipsis (Value -> Ellipsis Value
forall t. t -> Ellipsis t
Until Value
v1)
  Op
OLookupSeq -> Value -> Sem r CESK
out (Value -> Sem r CESK) -> (Value -> Value) -> Value -> Sem r CESK
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Value
oeisLookup
  Op
OExtendSeq -> Value -> Sem r CESK
out (Value -> Sem r CESK) -> (Value -> Value) -> Value -> Sem r CESK
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Value
oeisExtend
  --------------------------------------------------
  -- Comparison

  Op
OEq -> (Value -> Value -> Sem r CESK) -> Value -> Sem r CESK
forall a. (Value -> Value -> a) -> Value -> a
arity2 ((Value -> Value -> Sem r CESK) -> Value -> Sem r CESK)
-> (Value -> Value -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ \Value
v1 Value
v2 -> Value -> Sem r CESK
out (Value -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Bool -> Value
boolv (Value -> Value -> Bool
valEq Value
v1 Value
v2)
  Op
OLt -> (Value -> Value -> Sem r CESK) -> Value -> Sem r CESK
forall a. (Value -> Value -> a) -> Value -> a
arity2 ((Value -> Value -> Sem r CESK) -> Value -> Sem r CESK)
-> (Value -> Value -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ \Value
v1 Value
v2 -> Value -> Sem r CESK
out (Value -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Bool -> Value
boolv (Value -> Value -> Bool
valLt Value
v1 Value
v2)
  --------------------------------------------------
  -- Container operations

  Op
OPower -> Op -> ([(Value, Integer)] -> Sem r CESK) -> Value -> Sem r CESK
forall (r :: EffectRow) a.
Op -> ([(Value, Integer)] -> Sem r a) -> Value -> Sem r a
withBag Op
OPower (([(Value, Integer)] -> Sem r CESK) -> Value -> Sem r CESK)
-> ([(Value, Integer)] -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Value -> Sem r CESK
out (Value -> Sem r CESK)
-> ([(Value, Integer)] -> Value)
-> [(Value, Integer)]
-> Sem r CESK
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Value, Integer)] -> Value
VBag ([(Value, Integer)] -> Value)
-> ([(Value, Integer)] -> [(Value, Integer)])
-> [(Value, Integer)]
-> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Value, Integer)] -> [(Value, Integer)]
sortNCount ([(Value, Integer)] -> [(Value, Integer)])
-> ([(Value, Integer)] -> [(Value, Integer)])
-> [(Value, Integer)]
-> [(Value, Integer)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (([(Value, Integer)], Integer) -> (Value, Integer))
-> [([(Value, Integer)], Integer)] -> [(Value, Integer)]
forall a b. (a -> b) -> [a] -> [b]
map (([(Value, Integer)] -> Value)
-> ([(Value, Integer)], Integer) -> (Value, Integer)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first [(Value, Integer)] -> Value
VBag) ([([(Value, Integer)], Integer)] -> [(Value, Integer)])
-> ([(Value, Integer)] -> [([(Value, Integer)], Integer)])
-> [(Value, Integer)]
-> [(Value, Integer)]
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' [([(Value, Integer)], Integer)]
-> [([(Value, Integer)], Integer)]
-> [([(Value, Integer)], Integer)]
forall a. [a] -> [a] -> [a]
++ (Integer -> [([(Value, Integer)], Integer)])
-> [Integer] -> [([(Value, Integer)], Integer)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\Integer
k' -> (([(Value, Integer)], Integer) -> ([(Value, Integer)], Integer))
-> [([(Value, Integer)], Integer)]
-> [([(Value, Integer)], Integer)]
forall a b. (a -> b) -> [a] -> [b]
map (Integer
-> (Value, Integer)
-> ([(Value, Integer)], Integer)
-> ([(Value, Integer)], Integer)
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') (a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
: [(a, b)]
zs, b -> b -> b
forall a. Integral a => a -> a -> a
choose b
n b
k' b -> b -> b
forall a. Num a => a -> a -> a
* b
m)
  Op
OBagElem -> (Value -> Value -> Sem r CESK) -> Value -> Sem r CESK
forall a. (Value -> Value -> a) -> Value -> a
arity2 ((Value -> Value -> Sem r CESK) -> Value -> Sem r CESK)
-> (Value -> Value -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ \Value
x ->
    Op -> ([(Value, Integer)] -> Sem r CESK) -> Value -> Sem r CESK
forall (r :: EffectRow) a.
Op -> ([(Value, Integer)] -> Sem r a) -> Value -> Sem r a
withBag Op
OBagElem (([(Value, Integer)] -> Sem r CESK) -> Value -> Sem r CESK)
-> ([(Value, Integer)] -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$
      Value -> Sem r CESK
out (Value -> Sem r CESK)
-> ([(Value, Integer)] -> Value)
-> [(Value, Integer)]
-> Sem r CESK
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Value
boolv (Bool -> Value)
-> ([(Value, Integer)] -> Bool) -> [(Value, Integer)] -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Value -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Value -> Bool)
-> ([(Value, Integer)] -> Maybe Value)
-> [(Value, Integer)]
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Value -> Bool) -> [Value] -> Maybe Value
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (Value -> Value -> Bool
valEq Value
x) ([Value] -> Maybe Value)
-> ([(Value, Integer)] -> [Value])
-> [(Value, Integer)]
-> Maybe Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Value, Integer) -> Value) -> [(Value, Integer)] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map (Value, Integer) -> Value
forall a b. (a, b) -> a
fst
  Op
OListElem -> (Value -> Value -> Sem r CESK) -> Value -> Sem r CESK
forall a. (Value -> Value -> a) -> Value -> a
arity2 ((Value -> Value -> Sem r CESK) -> Value -> Sem r CESK)
-> (Value -> Value -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ \Value
x -> Value -> Sem r CESK
out (Value -> Sem r CESK) -> (Value -> Value) -> Value -> Sem r CESK
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Value
boolv (Bool -> Value) -> (Value -> Bool) -> Value -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Value -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Value -> Bool) -> (Value -> Maybe Value) -> Value -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Value -> Bool) -> [Value] -> Maybe Value
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (Value -> Value -> Bool
valEq Value
x) ([Value] -> Maybe Value)
-> (Value -> [Value]) -> Value -> Maybe Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Value -> Value) -> Value -> [Value]
forall a. (Value -> a) -> Value -> [a]
vlist Value -> Value
forall a. a -> a
id
  Op
OEachSet -> (Value -> Value -> Sem r CESK) -> Value -> Sem r CESK
forall a. (Value -> Value -> a) -> Value -> a
arity2 ((Value -> Value -> Sem r CESK) -> Value -> Sem r CESK)
-> (Value -> Value -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ \Value
f ->
    Op -> ([(Value, Integer)] -> Sem r CESK) -> Value -> Sem r CESK
forall (r :: EffectRow) a.
Op -> ([(Value, Integer)] -> Sem r a) -> Value -> Sem r a
withBag Op
OEachSet (([(Value, Integer)] -> Sem r CESK) -> Value -> Sem r CESK)
-> ([(Value, Integer)] -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$
      Sem (Error EvalError : r) Value -> Sem r CESK
forall (r :: EffectRow).
Sem (Error EvalError : r) Value -> Sem r CESK
outWithErr (Sem (Error EvalError : r) Value -> Sem r CESK)
-> ([(Value, Integer)] -> Sem (Error EvalError : r) Value)
-> [(Value, Integer)]
-> Sem r CESK
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Value] -> Value)
-> Sem (Error EvalError : r) [Value]
-> Sem (Error EvalError : r) Value
forall a b.
(a -> b)
-> Sem (Error EvalError : r) a -> Sem (Error EvalError : r) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Value, Integer)] -> Value
VBag ([(Value, Integer)] -> Value)
-> ([Value] -> [(Value, Integer)]) -> [Value] -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Value] -> [(Value, Integer)]
countValues) (Sem (Error EvalError : r) [Value]
 -> Sem (Error EvalError : r) Value)
-> ([(Value, Integer)] -> Sem (Error EvalError : r) [Value])
-> [(Value, Integer)]
-> Sem (Error EvalError : r) Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Value, Integer) -> Sem (Error EvalError : r) Value)
-> [(Value, Integer)] -> Sem (Error EvalError : r) [Value]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Value -> [Value] -> Sem (Error EvalError : r) Value
forall (r :: EffectRow).
Members '[Random, Error EvalError, State Mem] r =>
Value -> [Value] -> Sem r Value
evalApp Value
f ([Value] -> Sem (Error EvalError : r) Value)
-> ((Value, Integer) -> [Value])
-> (Value, Integer)
-> Sem (Error EvalError : r) Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Value -> [Value] -> [Value]
forall a. a -> [a] -> [a]
: []) (Value -> [Value])
-> ((Value, Integer) -> Value) -> (Value, Integer) -> [Value]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Value, Integer) -> Value
forall a b. (a, b) -> a
fst)
  Op
OEachBag -> (Value -> Value -> Sem r CESK) -> Value -> Sem r CESK
forall a. (Value -> Value -> a) -> Value -> a
arity2 ((Value -> Value -> Sem r CESK) -> Value -> Sem r CESK)
-> (Value -> Value -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ \Value
f ->
    Op -> ([(Value, Integer)] -> Sem r CESK) -> Value -> Sem r CESK
forall (r :: EffectRow) a.
Op -> ([(Value, Integer)] -> Sem r a) -> Value -> Sem r a
withBag Op
OEachBag (([(Value, Integer)] -> Sem r CESK) -> Value -> Sem r CESK)
-> ([(Value, Integer)] -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$
      Sem (Error EvalError : r) Value -> Sem r CESK
forall (r :: EffectRow).
Sem (Error EvalError : r) Value -> Sem r CESK
outWithErr (Sem (Error EvalError : r) Value -> Sem r CESK)
-> ([(Value, Integer)] -> Sem (Error EvalError : r) Value)
-> [(Value, Integer)]
-> Sem r CESK
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([(Value, Integer)] -> Value)
-> Sem (Error EvalError : r) [(Value, Integer)]
-> Sem (Error EvalError : r) Value
forall a b.
(a -> b)
-> Sem (Error EvalError : r) a -> Sem (Error EvalError : r) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Value, Integer)] -> Value
VBag ([(Value, Integer)] -> Value)
-> ([(Value, Integer)] -> [(Value, Integer)])
-> [(Value, Integer)]
-> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Value, Integer)] -> [(Value, Integer)]
sortNCount) (Sem (Error EvalError : r) [(Value, Integer)]
 -> Sem (Error EvalError : r) Value)
-> ([(Value, Integer)]
    -> Sem (Error EvalError : r) [(Value, Integer)])
-> [(Value, Integer)]
-> Sem (Error EvalError : r) Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Value, Integer) -> Sem (Error EvalError : r) (Value, Integer))
-> [(Value, Integer)]
-> Sem (Error EvalError : r) [(Value, Integer)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\(Value
x, Integer
n) -> (,Integer
n) (Value -> (Value, Integer))
-> Sem (Error EvalError : r) Value
-> Sem (Error EvalError : r) (Value, Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value -> [Value] -> Sem (Error EvalError : r) Value
forall (r :: EffectRow).
Members '[Random, Error EvalError, State Mem] r =>
Value -> [Value] -> Sem r Value
evalApp Value
f [Value
x])
  Op
OFilterBag -> (Value -> Value -> Sem r CESK) -> Value -> Sem r CESK
forall a. (Value -> Value -> a) -> Value -> a
arity2 ((Value -> Value -> Sem r CESK) -> Value -> Sem r CESK)
-> (Value -> Value -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ \Value
f -> Op -> ([(Value, Integer)] -> Sem r CESK) -> Value -> Sem r CESK
forall (r :: EffectRow) a.
Op -> ([(Value, Integer)] -> Sem r a) -> Value -> Sem r a
withBag Op
OFilterBag (([(Value, Integer)] -> Sem r CESK) -> Value -> Sem r CESK)
-> ([(Value, Integer)] -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ \[(Value, Integer)]
xs ->
    Sem (Error EvalError : r) Value -> Sem r CESK
forall (r :: EffectRow).
Sem (Error EvalError : r) Value -> Sem r CESK
outWithErr (Sem (Error EvalError : r) Value -> Sem r CESK)
-> Sem (Error EvalError : r) Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ do
      [Value]
bs <- ((Value, Integer) -> Sem (Error EvalError : r) Value)
-> [(Value, Integer)] -> Sem (Error EvalError : r) [Value]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Value -> [Value] -> Sem (Error EvalError : r) Value
forall (r :: EffectRow).
Members '[Random, Error EvalError, State Mem] r =>
Value -> [Value] -> Sem r Value
evalApp Value
f ([Value] -> Sem (Error EvalError : r) Value)
-> ((Value, Integer) -> [Value])
-> (Value, Integer)
-> Sem (Error EvalError : r) Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Value -> [Value] -> [Value]
forall a. a -> [a] -> [a]
: []) (Value -> [Value])
-> ((Value, Integer) -> Value) -> (Value, Integer) -> [Value]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Value, Integer) -> Value
forall a b. (a, b) -> a
fst) [(Value, Integer)]
xs
      Value -> Sem (Error EvalError : r) Value
forall a. a -> Sem (Error EvalError : r) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Sem (Error EvalError : r) Value)
-> ([(Value, (Value, Integer))] -> Value)
-> [(Value, (Value, Integer))]
-> Sem (Error EvalError : r) Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Value, Integer)] -> Value
VBag ([(Value, Integer)] -> Value)
-> ([(Value, (Value, Integer))] -> [(Value, Integer)])
-> [(Value, (Value, Integer))]
-> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Value, (Value, Integer)) -> (Value, Integer))
-> [(Value, (Value, Integer))] -> [(Value, Integer)]
forall a b. (a -> b) -> [a] -> [b]
map (Value, (Value, Integer)) -> (Value, Integer)
forall a b. (a, b) -> b
snd ([(Value, (Value, Integer))] -> [(Value, Integer)])
-> ([(Value, (Value, Integer))] -> [(Value, (Value, Integer))])
-> [(Value, (Value, Integer))]
-> [(Value, Integer)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Value, (Value, Integer)) -> Bool)
-> [(Value, (Value, Integer))] -> [(Value, (Value, Integer))]
forall a. (a -> Bool) -> [a] -> [a]
Prelude.filter (Value -> Bool
isTrue (Value -> Bool)
-> ((Value, (Value, Integer)) -> Value)
-> (Value, (Value, Integer))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Value, (Value, Integer)) -> Value
forall a b. (a, b) -> a
fst) ([(Value, (Value, Integer))] -> Sem (Error EvalError : r) Value)
-> [(Value, (Value, Integer))] -> Sem (Error EvalError : r) Value
forall a b. (a -> b) -> a -> b
$ [Value] -> [(Value, Integer)] -> [(Value, (Value, Integer))]
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 -> (Value -> Value -> Value -> Sem r CESK) -> Value -> Sem r CESK
forall a. (Value -> Value -> Value -> a) -> Value -> a
arity3 ((Value -> Value -> Value -> Sem r CESK) -> Value -> Sem r CESK)
-> (Value -> Value -> Value -> Sem r CESK) -> Value -> Sem r CESK
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) -> Sem (Error EvalError : r) Value -> Sem r CESK
forall (r :: EffectRow).
Sem (Error EvalError : r) Value -> Sem r CESK
outWithErr ([(Value, Integer)] -> Value
VBag ([(Value, Integer)] -> Value)
-> Sem (Error EvalError : r) [(Value, Integer)]
-> Sem (Error EvalError : r) Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value
-> [(Value, Integer)]
-> [(Value, Integer)]
-> Sem (Error EvalError : r) [(Value, Integer)]
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
_) -> String -> Sem r CESK
forall a. HasCallStack => String -> a
error (String -> Sem r CESK) -> String -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ String
"Impossible! OMerge on non-VBag " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
forall a. Show a => a -> String
show Value
bys
      (Value, Value)
_ -> String -> Sem r CESK
forall a. HasCallStack => String -> a
error (String -> Sem r CESK) -> String -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ String
"Impossible! OMerge on non-VBag " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
forall a. Show a => a -> String
show Value
bxs
  Op
OBagUnions -> Op -> ([(Value, Integer)] -> Sem r CESK) -> Value -> Sem r CESK
forall (r :: EffectRow) a.
Op -> ([(Value, Integer)] -> Sem r a) -> Value -> Sem r a
withBag Op
OBagUnions (([(Value, Integer)] -> Sem r CESK) -> Value -> Sem r CESK)
-> ([(Value, Integer)] -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ \[(Value, Integer)]
cts ->
    Value -> Sem r CESK
out (Value -> Sem r CESK)
-> ([(Value, Integer)] -> Value)
-> [(Value, Integer)]
-> Sem r CESK
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Value, Integer)] -> Value
VBag ([(Value, Integer)] -> Sem r CESK)
-> [(Value, Integer)] -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ [(Value, Integer)] -> [(Value, Integer)]
sortNCount [(Value
x, Integer
m Integer -> Integer -> Integer
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 -> Op -> ([(Value, Integer)] -> Sem r CESK) -> Value -> Sem r CESK
forall (r :: EffectRow) a.
Op -> ([(Value, Integer)] -> Sem r a) -> Value -> Sem r a
withBag Op
OBagToSet (([(Value, Integer)] -> Sem r CESK) -> Value -> Sem r CESK)
-> ([(Value, Integer)] -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Value -> Sem r CESK
out (Value -> Sem r CESK)
-> ([(Value, Integer)] -> Value)
-> [(Value, Integer)]
-> Sem r CESK
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Value, Integer)] -> Value
VBag ([(Value, Integer)] -> Value)
-> ([(Value, Integer)] -> [(Value, Integer)])
-> [(Value, Integer)]
-> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((Value, Integer) -> (Value, Integer))
-> [(Value, Integer)] -> [(Value, Integer)]
forall a b. (a -> b) -> [a] -> [b]
map (((Value, Integer) -> (Value, Integer))
 -> [(Value, Integer)] -> [(Value, Integer)])
-> ((Integer -> Integer) -> (Value, Integer) -> (Value, Integer))
-> (Integer -> Integer)
-> [(Value, Integer)]
-> [(Value, Integer)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer -> Integer) -> (Value, Integer) -> (Value, Integer)
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) (Integer -> Integer -> Integer
forall a b. a -> b -> a
const Integer
1)
  Op
OSetToList -> Op -> ([(Value, Integer)] -> Sem r CESK) -> Value -> Sem r CESK
forall (r :: EffectRow) a.
Op -> ([(Value, Integer)] -> Sem r a) -> Value -> Sem r a
withBag Op
OSetToList (([(Value, Integer)] -> Sem r CESK) -> Value -> Sem r CESK)
-> ([(Value, Integer)] -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Value -> Sem r CESK
out (Value -> Sem r CESK)
-> ([(Value, Integer)] -> Value)
-> [(Value, Integer)]
-> Sem r CESK
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Value -> Value) -> [Value] -> Value
forall a. (a -> Value) -> [a] -> Value
listv Value -> Value
forall a. a -> a
id ([Value] -> Value)
-> ([(Value, Integer)] -> [Value]) -> [(Value, Integer)] -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Value, Integer) -> Value) -> [(Value, Integer)] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map (Value, Integer) -> Value
forall a b. (a, b) -> a
fst
  Op
OBagToList -> Op -> ([(Value, Integer)] -> Sem r CESK) -> Value -> Sem r CESK
forall (r :: EffectRow) a.
Op -> ([(Value, Integer)] -> Sem r a) -> Value -> Sem r a
withBag Op
OBagToList (([(Value, Integer)] -> Sem r CESK) -> Value -> Sem r CESK)
-> ([(Value, Integer)] -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Value -> Sem r CESK
out (Value -> Sem r CESK)
-> ([(Value, Integer)] -> Value)
-> [(Value, Integer)]
-> Sem r CESK
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Value -> Value) -> [Value] -> Value
forall a. (a -> Value) -> [a] -> Value
listv Value -> Value
forall a. a -> a
id ([Value] -> Value)
-> ([(Value, Integer)] -> [Value]) -> [(Value, Integer)] -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Value, Integer) -> [Value]) -> [(Value, Integer)] -> [Value]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((Value -> Integer -> [Value]) -> (Value, Integer) -> [Value]
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((Integer -> Value -> [Value]) -> Value -> Integer -> [Value]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Int -> Value -> [Value]
forall a. Int -> a -> [a]
replicate (Int -> Value -> [Value])
-> (Integer -> Int) -> Integer -> Value -> [Value]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral)))
  Op
OListToSet -> Value -> Sem r CESK
out (Value -> Sem r CESK) -> (Value -> Value) -> Value -> Sem r CESK
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Value, Integer)] -> Value
VBag ([(Value, Integer)] -> Value)
-> (Value -> [(Value, Integer)]) -> Value -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((Value, Integer) -> (Value, Integer))
-> [(Value, Integer)] -> [(Value, Integer)]
forall a b. (a -> b) -> [a] -> [b]
map (((Value, Integer) -> (Value, Integer))
 -> [(Value, Integer)] -> [(Value, Integer)])
-> ((Integer -> Integer) -> (Value, Integer) -> (Value, Integer))
-> (Integer -> Integer)
-> [(Value, Integer)]
-> [(Value, Integer)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer -> Integer) -> (Value, Integer) -> (Value, Integer)
forall a b. (a -> b) -> (Value, a) -> (Value, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) (Integer -> Integer -> Integer
forall a b. a -> b -> a
const Integer
1) ([(Value, Integer)] -> [(Value, Integer)])
-> (Value -> [(Value, Integer)]) -> Value -> [(Value, Integer)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Value] -> [(Value, Integer)]
countValues ([Value] -> [(Value, Integer)])
-> (Value -> [Value]) -> Value -> [(Value, Integer)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Value -> Value) -> Value -> [Value]
forall a. (Value -> a) -> Value -> [a]
vlist Value -> Value
forall a. a -> a
id
  Op
OListToBag -> Value -> Sem r CESK
out (Value -> Sem r CESK) -> (Value -> Value) -> Value -> Sem r CESK
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Value, Integer)] -> Value
VBag ([(Value, Integer)] -> Value)
-> (Value -> [(Value, Integer)]) -> Value -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Value] -> [(Value, Integer)]
countValues ([Value] -> [(Value, Integer)])
-> (Value -> [Value]) -> Value -> [(Value, Integer)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Value -> Value) -> Value -> [Value]
forall a. (Value -> a) -> Value -> [a]
vlist Value -> Value
forall a. a -> a
id
  Op
OBagToCounts -> Op -> ([(Value, Integer)] -> Sem r CESK) -> Value -> Sem r CESK
forall (r :: EffectRow) a.
Op -> ([(Value, Integer)] -> Sem r a) -> Value -> Sem r a
withBag Op
OBagToCounts (([(Value, Integer)] -> Sem r CESK) -> Value -> Sem r CESK)
-> ([(Value, Integer)] -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Value -> Sem r CESK
out (Value -> Sem r CESK)
-> ([(Value, Integer)] -> Value)
-> [(Value, Integer)]
-> Sem r CESK
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Value, Integer)] -> Value
VBag ([(Value, Integer)] -> Value)
-> ([(Value, Integer)] -> [(Value, Integer)])
-> [(Value, Integer)]
-> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Value, Integer) -> (Value, Integer))
-> [(Value, Integer)] -> [(Value, Integer)]
forall a b. (a -> b) -> [a] -> [b]
map ((,Integer
1) (Value -> (Value, Integer))
-> ((Value, Integer) -> Value)
-> (Value, Integer)
-> (Value, Integer)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Value -> Value) -> (Integer -> Value) -> (Value, Integer) -> Value
forall a b. (a -> Value) -> (b -> Value) -> (a, b) -> Value
pairv Value -> Value
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 ->
    Op -> ([(Value, Integer)] -> Sem r CESK) -> Value -> Sem r CESK
forall (r :: EffectRow) a.
Op -> ([(Value, Integer)] -> Sem r a) -> Value -> Sem r a
withBag Op
OCountsToBag (([(Value, Integer)] -> Sem r CESK) -> Value -> Sem r CESK)
-> ([(Value, Integer)] -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$
      Value -> Sem r CESK
out (Value -> Sem r CESK)
-> ([(Value, Integer)] -> Value)
-> [(Value, Integer)]
-> Sem r CESK
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Value, Integer)] -> Value
VBag ([(Value, Integer)] -> Value)
-> ([(Value, Integer)] -> [(Value, Integer)])
-> [(Value, Integer)]
-> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Value, Integer)] -> [(Value, Integer)]
sortNCount ([(Value, Integer)] -> [(Value, Integer)])
-> ([(Value, Integer)] -> [(Value, Integer)])
-> [(Value, Integer)]
-> [(Value, Integer)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Value, Integer) -> (Value, Integer))
-> [(Value, Integer)] -> [(Value, Integer)]
forall a b. (a -> b) -> [a] -> [b]
map (((Integer, Integer) -> Integer)
-> (Value, (Integer, Integer)) -> (Value, Integer)
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 ((Integer -> Integer -> Integer) -> (Integer, Integer) -> Integer
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(*)) ((Value, (Integer, Integer)) -> (Value, Integer))
-> ((Value, Integer) -> (Value, (Integer, Integer)))
-> (Value, Integer)
-> (Value, Integer)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Value, Integer), Integer) -> (Value, (Integer, Integer))
forall {a} {a} {b}. ((a, a), b) -> (a, (a, b))
assoc (((Value, Integer), Integer) -> (Value, (Integer, Integer)))
-> ((Value, Integer) -> ((Value, Integer), Integer))
-> (Value, Integer)
-> (Value, (Integer, Integer))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Value -> (Value, Integer))
-> (Value, Integer) -> ((Value, Integer), Integer)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ((Value -> Value) -> (Value -> Integer) -> Value -> (Value, Integer)
forall a b. (Value -> a) -> (Value -> b) -> Value -> (a, b)
vpair Value -> Value
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 ->
    Op -> ([(Value, Integer)] -> Sem r CESK) -> Value -> Sem r CESK
forall (r :: EffectRow) a.
Op -> ([(Value, Integer)] -> Sem r a) -> Value -> Sem r a
withBag Op
OUnsafeCountsToBag (([(Value, Integer)] -> Sem r CESK) -> Value -> Sem r CESK)
-> ([(Value, Integer)] -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$
      Value -> Sem r CESK
out (Value -> Sem r CESK)
-> ([(Value, Integer)] -> Value)
-> [(Value, Integer)]
-> Sem r CESK
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Value, Integer)] -> Value
VBag ([(Value, Integer)] -> Value)
-> ([(Value, Integer)] -> [(Value, Integer)])
-> [(Value, Integer)]
-> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Value, Integer) -> (Value, Integer))
-> [(Value, Integer)] -> [(Value, Integer)]
forall a b. (a -> b) -> [a] -> [b]
map (((Integer, Integer) -> Integer)
-> (Value, (Integer, Integer)) -> (Value, Integer)
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 ((Integer -> Integer -> Integer) -> (Integer, Integer) -> Integer
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(*)) ((Value, (Integer, Integer)) -> (Value, Integer))
-> ((Value, Integer) -> (Value, (Integer, Integer)))
-> (Value, Integer)
-> (Value, Integer)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Value, Integer), Integer) -> (Value, (Integer, Integer))
forall {a} {a} {b}. ((a, a), b) -> (a, (a, b))
assoc (((Value, Integer), Integer) -> (Value, (Integer, Integer)))
-> ((Value, Integer) -> ((Value, Integer), Integer))
-> (Value, Integer)
-> (Value, (Integer, Integer))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Value -> (Value, Integer))
-> (Value, Integer) -> ((Value, Integer), Integer)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ((Value -> Value) -> (Value -> Integer) -> Value -> (Value, Integer)
forall a b. (Value -> a) -> (Value -> b) -> Value -> (a, b)
vpair Value -> Value
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 ->
    Op -> (Map SimpleValue Value -> Sem r CESK) -> Value -> Sem r CESK
forall (r :: EffectRow) a.
Op -> (Map SimpleValue Value -> Sem r a) -> Value -> Sem r a
withMap Op
OMapToSet ((Map SimpleValue Value -> Sem r CESK) -> Value -> Sem r CESK)
-> (Map SimpleValue Value -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$
      Value -> Sem r CESK
out (Value -> Sem r CESK)
-> (Map SimpleValue Value -> Value)
-> Map SimpleValue Value
-> Sem r CESK
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Value, Integer)] -> Value
VBag ([(Value, Integer)] -> Value)
-> (Map SimpleValue Value -> [(Value, Integer)])
-> Map SimpleValue Value
-> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((SimpleValue, Value) -> (Value, Integer))
-> [(SimpleValue, Value)] -> [(Value, Integer)]
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)) ([(SimpleValue, Value)] -> [(Value, Integer)])
-> (Map SimpleValue Value -> [(SimpleValue, Value)])
-> Map SimpleValue Value
-> [(Value, Integer)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map SimpleValue Value -> [(SimpleValue, Value)]
forall k a. Map k a -> [(k, a)]
M.assocs
  Op
OSetToMap ->
    Op -> ([(Value, Integer)] -> Sem r CESK) -> Value -> Sem r CESK
forall (r :: EffectRow) a.
Op -> ([(Value, Integer)] -> Sem r a) -> Value -> Sem r a
withBag Op
OSetToMap (([(Value, Integer)] -> Sem r CESK) -> Value -> Sem r CESK)
-> ([(Value, Integer)] -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$
      Value -> Sem r CESK
out (Value -> Sem r CESK)
-> ([(Value, Integer)] -> Value)
-> [(Value, Integer)]
-> Sem r CESK
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map SimpleValue Value -> Value
VMap (Map SimpleValue Value -> Value)
-> ([(Value, Integer)] -> Map SimpleValue Value)
-> [(Value, Integer)]
-> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(SimpleValue, Value)] -> Map SimpleValue Value
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(SimpleValue, Value)] -> Map SimpleValue Value)
-> ([(Value, Integer)] -> [(SimpleValue, Value)])
-> [(Value, Integer)]
-> Map SimpleValue Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Value, Integer) -> (SimpleValue, Value))
-> [(Value, Integer)] -> [(SimpleValue, Value)]
forall a b. (a -> b) -> [a] -> [b]
map (Value -> (SimpleValue, Value)
convertAssoc (Value -> (SimpleValue, Value))
-> ((Value, Integer) -> Value)
-> (Value, Integer)
-> (SimpleValue, Value)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Value, Integer) -> Value
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 = String -> (SimpleValue, Value)
forall a. HasCallStack => String -> a
error (String -> (SimpleValue, Value)) -> String -> (SimpleValue, Value)
forall a b. (a -> b) -> a -> b
$ String
"Impossible! convertAssoc on non-VPair " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
forall a. Show a => a -> String
show Value
v
  Op
OInsert -> (Value -> Value -> Value -> Sem r CESK) -> Value -> Sem r CESK
forall a. (Value -> Value -> Value -> a) -> Value -> a
arity3 ((Value -> Value -> Value -> Sem r CESK) -> Value -> Sem r CESK)
-> (Value -> Value -> Value -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ \Value
k' Value
v ->
    Op -> (Map SimpleValue Value -> Sem r CESK) -> Value -> Sem r CESK
forall (r :: EffectRow) a.
Op -> (Map SimpleValue Value -> Sem r a) -> Value -> Sem r a
withMap Op
OInsert ((Map SimpleValue Value -> Sem r CESK) -> Value -> Sem r CESK)
-> (Map SimpleValue Value -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$
      Value -> Sem r CESK
out (Value -> Sem r CESK)
-> (Map SimpleValue Value -> Value)
-> Map SimpleValue Value
-> Sem r CESK
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map SimpleValue Value -> Value
VMap (Map SimpleValue Value -> Value)
-> (Map SimpleValue Value -> Map SimpleValue Value)
-> Map SimpleValue Value
-> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleValue
-> Value -> Map SimpleValue Value -> Map SimpleValue Value
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (Value -> SimpleValue
toSimpleValue Value
k') Value
v
  Op
OLookup -> (Value -> Value -> Sem r CESK) -> Value -> Sem r CESK
forall a. (Value -> Value -> a) -> Value -> a
arity2 ((Value -> Value -> Sem r CESK) -> Value -> Sem r CESK)
-> (Value -> Value -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ \Value
k' ->
    Op -> (Map SimpleValue Value -> Sem r CESK) -> Value -> Sem r CESK
forall (r :: EffectRow) a.
Op -> (Map SimpleValue Value -> Sem r a) -> Value -> Sem r a
withMap Op
OLookup ((Map SimpleValue Value -> Sem r CESK) -> Value -> Sem r CESK)
-> (Map SimpleValue Value -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$
      Value -> Sem r CESK
out (Value -> Sem r CESK)
-> (Map SimpleValue Value -> Value)
-> Map SimpleValue Value
-> Sem r CESK
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Value -> Value
toMaybe (Maybe Value -> Value)
-> (Map SimpleValue Value -> Maybe Value)
-> Map SimpleValue Value
-> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleValue -> Map SimpleValue Value -> Maybe Value
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Value -> SimpleValue
toSimpleValue Value
k')
   where
    toMaybe :: Maybe Value -> Value
toMaybe = Value -> (Value -> Value) -> Maybe Value -> Value
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Side -> Value -> Value
VInj Side
L Value
VUnit) (Side -> Value -> Value
VInj Side
R)
  --------------------------------------------------
  -- Randomness

  Op
ORandom -> (Value -> Value -> Sem r CESK) -> Value -> Sem r CESK
forall a. (Value -> Value -> a) -> Value -> a
arity2 ((Value -> Value -> Sem r CESK) -> Value -> Sem r CESK)
-> ((Value -> Value -> Sem r CESK) -> Value -> Value -> Sem r CESK)
-> (Value -> Value -> Sem r CESK)
-> Value
-> Sem r CESK
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Value -> Value -> Sem r CESK) -> Value -> Value -> Sem r CESK
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Value -> Value -> Sem r CESK) -> Value -> Sem r CESK)
-> (Value -> Value -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ \Value
g -> (Value -> Value -> Sem r CESK) -> Value -> Sem r CESK
forall a. (Value -> Value -> a) -> Value -> a
arity2 ((Value -> Value -> Sem r CESK) -> Value -> Sem r CESK)
-> (Value -> Value -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ \Value
v1 Value
v2 ->
    let (Integer
a, StdGen
g') = (Integer, Integer) -> StdGen -> (Integer, StdGen)
forall g. RandomGen g => (Integer, Integer) -> g -> (Integer, g)
forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
R.randomR (Value -> Integer
vint Value
v1, Value -> Integer
vint Value
v2) (Value -> StdGen
vgen Value
g)
     in Value -> Sem r CESK
out (Value -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Value -> Value -> Value
VPair (Integer -> Value
intv Integer
a) (StdGen -> Value
genv StdGen
g')
  Op
OSeed -> Value -> Sem r CESK
out (Value -> Sem r CESK) -> (Value -> Value) -> Value -> Sem r CESK
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StdGen -> Value
VGen (StdGen -> Value) -> (Value -> StdGen) -> Value -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> StdGen
R.mkStdGen (Int -> StdGen) -> (Value -> Int) -> Value -> StdGen
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Int) -> (Value -> Integer) -> Value -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Integer
vint)
  --------------------------------------------------
  -- Graph operations

  Op
OVertex -> Value -> Sem r CESK
out (Value -> Sem r CESK) -> (Value -> Value) -> Value -> Sem r CESK
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Graph SimpleValue -> Value
VGraph (Graph SimpleValue -> Value)
-> (Value -> Graph SimpleValue) -> Value -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleValue -> Graph SimpleValue
forall a. a -> Graph a
Vertex (SimpleValue -> Graph SimpleValue)
-> (Value -> SimpleValue) -> Value -> Graph SimpleValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> SimpleValue
toSimpleValue
  Op
OOverlay -> (Value -> Value -> Sem r CESK) -> Value -> Sem r CESK
forall a. (Value -> Value -> a) -> Value -> a
arity2 ((Value -> Value -> Sem r CESK) -> Value -> Sem r CESK)
-> (Value -> Value -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Op
-> (Graph SimpleValue -> Graph SimpleValue -> Sem r CESK)
-> Value
-> Value
-> Sem r CESK
forall (r :: EffectRow) a.
Op
-> (Graph SimpleValue -> Graph SimpleValue -> Sem r a)
-> Value
-> Value
-> Sem r a
withGraph2 Op
OOverlay ((Graph SimpleValue -> Graph SimpleValue -> Sem r CESK)
 -> Value -> Value -> Sem r CESK)
-> (Graph SimpleValue -> Graph SimpleValue -> Sem r CESK)
-> Value
-> Value
-> Sem r CESK
forall a b. (a -> b) -> a -> b
$ \Graph SimpleValue
g1 Graph SimpleValue
g2 ->
    Value -> Sem r CESK
out (Value -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Graph SimpleValue -> Value
VGraph (Graph SimpleValue -> Graph SimpleValue -> Graph SimpleValue
forall a. Graph a -> Graph a -> Graph a
Overlay Graph SimpleValue
g1 Graph SimpleValue
g2)
  Op
OConnect -> (Value -> Value -> Sem r CESK) -> Value -> Sem r CESK
forall a. (Value -> Value -> a) -> Value -> a
arity2 ((Value -> Value -> Sem r CESK) -> Value -> Sem r CESK)
-> (Value -> Value -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Op
-> (Graph SimpleValue -> Graph SimpleValue -> Sem r CESK)
-> Value
-> Value
-> Sem r CESK
forall (r :: EffectRow) a.
Op
-> (Graph SimpleValue -> Graph SimpleValue -> Sem r a)
-> Value
-> Value
-> Sem r a
withGraph2 Op
OConnect ((Graph SimpleValue -> Graph SimpleValue -> Sem r CESK)
 -> Value -> Value -> Sem r CESK)
-> (Graph SimpleValue -> Graph SimpleValue -> Sem r CESK)
-> Value
-> Value
-> Sem r CESK
forall a b. (a -> b) -> a -> b
$ \Graph SimpleValue
g1 Graph SimpleValue
g2 ->
    Value -> Sem r CESK
out (Value -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Graph SimpleValue -> Value
VGraph (Graph SimpleValue -> Graph SimpleValue -> Graph SimpleValue
forall a. Graph a -> Graph a -> Graph a
Connect Graph SimpleValue
g1 Graph SimpleValue
g2)
  Op
OSummary -> Op -> (Graph SimpleValue -> Sem r CESK) -> Value -> Sem r CESK
forall (r :: EffectRow) a.
Op -> (Graph SimpleValue -> Sem r a) -> Value -> Sem r a
withGraph Op
OSummary ((Graph SimpleValue -> Sem r CESK) -> Value -> Sem r CESK)
-> (Graph SimpleValue -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Value -> Sem r CESK
out (Value -> Sem r CESK)
-> (Graph SimpleValue -> Value) -> Graph SimpleValue -> Sem r CESK
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Graph SimpleValue -> Value
graphSummary
  --------------------------------------------------
  -- Propositions

  OForall [Type]
tys -> Value -> Sem r CESK
out (Value -> Sem r CESK) -> (Value -> Value) -> Value -> Sem r CESK
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 (Value -> Sem r CESK) -> (Value -> Value) -> Value -> Sem r CESK
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 -> SearchType -> Value -> Sem r TestResult
forall (r :: EffectRow).
Members '[Random, State Mem] r =>
SearchType -> Value -> Sem r TestResult
testProperty SearchType
Exhaustive (Value -> Sem r TestResult)
-> (TestResult -> Sem r CESK) -> Value -> Sem r CESK
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> TestResult -> Sem (Error EvalError : r) Value
forall (r :: EffectRow).
Member (Error EvalError) r =>
TestResult -> Sem r Value
resultToBool (TestResult -> Sem (Error EvalError : r) Value)
-> (Sem (Error EvalError : r) Value -> Sem r CESK)
-> TestResult
-> Sem r CESK
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> Sem (Error EvalError : r) Value -> Sem r CESK
forall (r :: EffectRow).
Sem (Error EvalError : r) Value -> Sem r CESK
outWithErr
  Op
ONotProp -> Value -> Sem r CESK
out (Value -> Sem r CESK) -> (Value -> Value) -> Value -> Sem r CESK
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValProp -> Value
VProp (ValProp -> Value) -> (Value -> ValProp) -> Value -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValProp -> ValProp
notProp (ValProp -> ValProp) -> (Value -> ValProp) -> Value -> ValProp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> ValProp
ensureProp
  OShould BOp
op Type
ty -> (Value -> Value -> Sem r CESK) -> Value -> Sem r CESK
forall a. (Value -> Value -> a) -> Value -> a
arity2 ((Value -> Value -> Sem r CESK) -> Value -> Sem r CESK)
-> (Value -> Value -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ \Value
v1 Value
v2 ->
    Value -> Sem r CESK
out (Value -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ ValProp -> Value
VProp (TestResult -> ValProp
VPDone (Bool -> TestReason -> TestEnv -> TestResult
TestResult (BOp -> Value -> Value -> Bool
valOp BOp
op Value
v1 Value
v2) (BOp -> Type -> Value -> Value -> TestReason
forall a. BOp -> Type -> a -> a -> TestReason_ a
TestCmp BOp
op Type
ty Value
v1 Value
v2) TestEnv
emptyTestEnv))
  Op
OAnd -> (Value -> Value -> Sem r CESK) -> Value -> Sem r CESK
forall a. (Value -> Value -> a) -> Value -> a
arity2 ((Value -> Value -> Sem r CESK) -> Value -> Sem r CESK)
-> (Value -> Value -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ \Value
p1 Value
p2 ->
    Value -> Sem r CESK
out (Value -> Sem r CESK) -> Value -> Sem r CESK
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 -> (Value -> Value -> Sem r CESK) -> Value -> Sem r CESK
forall a. (Value -> Value -> a) -> Value -> a
arity2 ((Value -> Value -> Sem r CESK) -> Value -> Sem r CESK)
-> (Value -> Value -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ \Value
p1 Value
p2 ->
    Value -> Sem r CESK
out (Value -> Sem r CESK) -> Value -> Sem r CESK
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 -> (Value -> Value -> Sem r CESK) -> Value -> Sem r CESK
forall a. (Value -> Value -> a) -> Value -> a
arity2 ((Value -> Value -> Sem r CESK) -> Value -> Sem r CESK)
-> (Value -> Value -> Sem r CESK) -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ \Value
p1 Value
p2 ->
    Value -> Sem r CESK
out (Value -> Sem r CESK) -> Value -> Sem r CESK
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 -> String -> Value -> Sem r CESK
forall a. HasCallStack => String -> a
error (String -> Value -> Sem r CESK) -> String -> Value -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ String
"Unimplemented: appConst " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Op -> String
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 = (EvalError -> CESK)
-> (Value -> CESK) -> Either EvalError Value -> CESK
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) (Either EvalError Value -> CESK)
-> Sem r (Either EvalError Value) -> Sem r CESK
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sem (Error EvalError : r) Value -> Sem r (Either EvalError Value)
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 = CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
forall a b. (a -> b) -> a -> b
$ Value -> [Frame] -> CESK
Out Value
v [Frame]
k
  up :: EvalError -> Sem r CESK
up EvalError
e = CESK -> Sem r CESK
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (CESK -> Sem r CESK) -> CESK -> Sem r CESK
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 -> String -> Sem r a
forall a. HasCallStack => String -> a
error (String -> Sem r a) -> String -> Sem r a
forall a b. (a -> b) -> a -> b
$ String
"Impossible! " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Op -> String
forall a. Show a => a -> String
show Op
op String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" on non-VBag " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
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 -> String -> Sem r a
forall a. HasCallStack => String -> a
error (String -> Sem r a) -> String -> Sem r a
forall a b. (a -> b) -> a -> b
$ String
"Impossible! " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Op -> String
forall a. Show a => a -> String
show Op
op String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" on non-VMap " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
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 -> String -> Sem r a
forall a. HasCallStack => String -> a
error (String -> Sem r a) -> String -> Sem r a
forall a b. (a -> b) -> a -> b
$ String
"Impossible! " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Op -> String
forall a. Show a => a -> String
show Op
op String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" on non-VGraph " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
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
_) -> String -> Sem r a
forall a. HasCallStack => String -> a
error (String -> Sem r a) -> String -> Sem r a
forall a b. (a -> b) -> a -> b
$ String
"Impossible! " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Op -> String
forall a. Show a => a -> String
show Op
op String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" on non-VGraph " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
forall a. Show a => a -> String
show Value
v1
    (Value, Value)
_ -> String -> Sem r a
forall a. HasCallStack => String -> a
error (String -> Sem r a) -> String -> Sem r a
forall a b. (a -> b) -> a -> b
$ String
"Impossible! " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Op -> String
forall a. Show a => a -> String
show Op
op String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" on non-VGraph " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
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 = (Integer -> Sem r Value) -> Value -> Sem r Value
forall (r :: EffectRow).
(Integer -> Sem r Value) -> Value -> Sem r Value
intOp1' (Value -> Sem r Value
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Sem r Value)
-> (Integer -> Value) -> Integer -> Sem r Value
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 (Integer -> Sem r Value)
-> (Value -> Integer) -> Value -> Sem r Value
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 = (Rational -> Sem r Value) -> Value -> Sem r Value
forall (r :: EffectRow).
(Rational -> Sem r Value) -> Value -> Sem r Value
numOp1' ((Rational -> Sem r Value) -> Value -> Sem r Value)
-> (Rational -> Sem r Value) -> Value -> Sem r Value
forall a b. (a -> b) -> a -> b
$ Value -> Sem r Value
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Sem r Value)
-> (Rational -> Value) -> Rational -> Sem r Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Value
ratv (Rational -> Value) -> (Rational -> Rational) -> Rational -> Value
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 Rational
m) = Rational -> Sem r Value
f Rational
m
numOp1' Rational -> Sem r Value
_ Value
v = String -> Sem r Value
forall a. HasCallStack => String -> a
error (String -> Sem r Value) -> String -> Sem r Value
forall a b. (a -> b) -> a -> b
$ String
"Impossible! numOp1' on non-VNum " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
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
(#) = (Rational -> Rational -> Sem r Value) -> Value -> Sem r Value
forall (r :: EffectRow).
(Rational -> Rational -> Sem r Value) -> Value -> Sem r Value
numOp2' ((Rational -> Rational -> Sem r Value) -> Value -> Sem r Value)
-> (Rational -> Rational -> Sem r Value) -> Value -> Sem r Value
forall a b. (a -> b) -> a -> b
$ \Rational
m Rational
n -> Value -> Sem r Value
forall a. a -> Sem r a
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
(#) =
  (Value -> Value -> Sem r Value) -> Value -> Sem r Value
forall a. (Value -> Value -> a) -> Value -> a
arity2 ((Value -> Value -> Sem r Value) -> Value -> Sem r Value)
-> (Value -> Value -> Sem r Value) -> Value -> Sem r Value
forall a b. (a -> b) -> a -> b
$ \Value
v1 Value
v2 -> case (Value
v1, Value
v2) of
    (VNum Rational
n1, VNum Rational
n2) -> Rational
n1 Rational -> Rational -> Sem r Value
# Rational
n2
    (VNum {}, Value
_) -> String -> Sem r Value
forall a. HasCallStack => String -> a
error (String -> Sem r Value) -> String -> Sem r Value
forall a b. (a -> b) -> a -> b
$ String
"Impossible! numOp2' on non-VNum " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
forall a. Show a => a -> String
show Value
v2
    (Value, Value)
_ -> String -> Sem r Value
forall a. HasCallStack => String -> a
error (String -> Sem r Value) -> String -> Sem r Value
forall a b. (a -> b) -> a -> b
$ String
"Impossible! numOp2' on non-VNum " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
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' (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
n) Integer -> Integer -> Rational
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 = (Integer -> Integer) -> Integer -> [Integer]
forall a. (a -> a) -> a -> [a]
iterate (Integer -> Int -> Integer
forall a. Num a => a -> Int -> a
^! Int
2) Integer
2
      (Integer
lowerRoot, Integer
lowerN) =
        [(Integer, Integer)] -> (Integer, Integer)
forall a. HasCallStack => [a] -> a
last ([(Integer, Integer)] -> (Integer, Integer))
-> [(Integer, Integer)] -> (Integer, Integer)
forall a b. (a -> b) -> a -> b
$ ((Integer, Integer) -> Bool)
-> [(Integer, Integer)] -> [(Integer, Integer)]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile ((Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>=) (Integer -> Bool)
-> ((Integer, Integer) -> Integer) -> (Integer, Integer) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer, Integer) -> Integer
forall a b. (a, b) -> b
snd) ([(Integer, Integer)] -> [(Integer, Integer)])
-> [(Integer, Integer)] -> [(Integer, Integer)]
forall a b. (a -> b) -> a -> b
$ [Integer] -> [Integer] -> [(Integer, Integer)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Integer
1 Integer -> [Integer] -> [Integer]
forall a. a -> [a] -> [a]
: [Integer]
twopows) [Integer]
twopows
      newtonStep :: Integer -> Integer
newtonStep Integer
x = Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div Integer
n Integer
x) Integer
2
      iters :: Infinite Integer
iters = (Integer -> Integer) -> Integer -> Infinite Integer
forall a. (a -> a) -> a -> Infinite a
InfList.iterate' Integer -> Integer
newtonStep (Integer -> Integer
integerSqrt' (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div Integer
n Integer
lowerN) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
lowerRoot)
      isRoot :: Integer -> Bool
isRoot Integer
r = Integer
r Integer -> Int -> Integer
forall a. Num a => a -> Int -> a
^! Int
2 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
n Bool -> Bool -> Bool
&& Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< (Integer
r Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Integer -> Int -> Integer
forall a. Num a => a -> Int -> a
^! Int
2
   in Infinite Integer -> Integer
forall a. Infinite a -> a
InfList.head (Infinite Integer -> Integer) -> Infinite Integer -> Integer
forall a b. (a -> b) -> a -> b
$ (Integer -> Bool) -> Infinite Integer -> Infinite Integer
forall a. (a -> Bool) -> Infinite a -> Infinite a
InfList.dropWhile (Bool -> Bool
not (Bool -> Bool) -> (Integer -> Bool) -> Integer -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Bool
isRoot) Infinite 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 a -> Int -> a
forall a b. (Num a, Integral b) => a -> b -> a
^ Int
n

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

valEq, valLt :: Value -> Value -> Bool
valEq :: Value -> Value -> Bool
valEq = BOp -> Value -> Value -> Bool
valOp BOp
Eq
valLt :: Value -> Value -> Bool
valLt = BOp -> Value -> Value -> Bool
valOp BOp
Lt

valOp :: BOp -> Value -> Value -> Bool
valOp :: BOp -> Value -> Value -> Bool
valOp BOp
op Value
v1 Value
v2 = case BOp
op of
  BOp
Eq -> Value -> Value -> Ordering
valCmp Value
v1 Value
v2 Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ
  BOp
Neq -> Value -> Value -> Ordering
valCmp Value
v1 Value
v2 Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
/= Ordering
EQ
  BOp
Lt -> Value -> Value -> Ordering
valCmp Value
v1 Value
v2 Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
LT
  BOp
Gt -> Value -> Value -> Ordering
valCmp Value
v1 Value
v2 Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
GT
  BOp
Leq -> Value -> Value -> Ordering
valCmp Value
v1 Value
v2 Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
/= Ordering
GT
  BOp
Geq -> Value -> Value -> Ordering
valCmp Value
v1 Value
v2 Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
/= Ordering
LT
  BOp
Divides -> Value -> Value -> Bool
valDivides Value
v1 Value
v2
  BOp
_ -> Bool
False

valDivides :: Value -> Value -> Bool
valDivides :: Value -> Value -> Bool
valDivides (VNum Rational
r1) (VNum Rational
r2) = Rational -> Rational -> Bool
divides Rational
r1 Rational
r2
valDivides Value
_ Value
_ = Bool
False

divides :: Rational -> Rational -> Bool
divides :: Rational -> Rational -> Bool
divides Rational
0 Rational
0 = Bool
True
divides Rational
0 Rational
_ = Bool
False
divides Rational
x Rational
y = Rational -> Integer
forall a. Ratio a -> a
denominator (Rational
y Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ Rational
x) Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1

valCmp :: Value -> Value -> Ordering
valCmp :: Value -> Value -> Ordering
valCmp (VNum Rational
r1) (VNum Rational
r2) = Rational -> Rational -> Ordering
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 Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> Value -> Value -> Ordering
valCmp Value
v12 Value
v22
valCmp (VType Type
ty1) (VType Type
ty2) = Type -> Type -> Ordering
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 (Map SimpleValue Value -> [(SimpleValue, Value)]
forall k a. Map k a -> [(k, a)]
M.assocs Map SimpleValue Value
m1) (Map SimpleValue Value -> [(SimpleValue, Value)]
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 = String -> Ordering
forall a. HasCallStack => String -> a
error (String -> Ordering) -> String -> Ordering
forall a b. (a -> b) -> a -> b
$ String
"valCmp\n  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> ShowS
forall a. Int -> [a] -> [a]
take Int
100 (Value -> String
forall a. Show a => a -> String
show Value
v1) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"...\n  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> ShowS
forall a. Int -> [a] -> [a]
take Int
100 (Value -> String
forall a. Show a => a -> String
show Value
v2) String -> ShowS
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 Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Integer
xn Integer
yn Ordering -> Ordering -> Ordering
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) Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> Value -> Value -> Ordering
valCmp Value
v1 Value
v2 Ordering -> Ordering -> Ordering
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 ((Value -> Rational) -> Ellipsis Value -> Ellipsis Rational
forall a b. (a -> b) -> Ellipsis a -> Ellipsis b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Value -> Rational
vrat -> Ellipsis Rational
end) ((Value -> Rational) -> Value -> [Rational]
forall a. (Value -> a) -> Value -> [a]
vlist Value -> Rational
vrat -> [Rational]
rs) = (Rational -> Value) -> [Rational] -> Value
forall a. (a -> Value) -> [a] -> Value
listv Rational -> Value
ratv ([Rational] -> Value) -> [Rational] -> Value
forall a b. (a -> b) -> a -> b
$ [Rational] -> Ellipsis Rational -> [Rational]
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
_ = String -> [a]
forall a. HasCallStack => String -> a
error String
"Impossible! Disco.Interpret.CESK.enumEllipsis []"
enumEllipsis [a
x] (Until a
y)
  | a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
y = [a
x .. a
y]
  | Bool
otherwise = [a
x, a -> a
forall a. Enum a => a -> a
pred a
x .. a
y]
enumEllipsis [a]
xs (Until a
y)
  | a
d a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
0 = (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
y) [a]
nums
  | a
d a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
0 = (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
y) [a]
nums
  | Bool
otherwise = [a]
nums
 where
  d :: a
d = [a] -> a
forall a. (Eq a, Num a) => [a] -> a
constdiff [a]
xs
  nums :: [a]
nums = [a] -> [a]
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] = a -> [a]
forall a. a -> [a]
repeat a
x
babbage (a
x : [a]
xs) = (a -> a -> a) -> a -> [a] -> [a]
forall b a. (b -> a -> b) -> b -> [a] -> [b]
scanl a -> a -> a
forall a. Num a => a -> a -> a
(+) a
x ([a] -> [a]
forall a. Num a => [a] -> [a]
babbage ([a] -> [a]
forall a. Num a => [a] -> [a]
diff (a
x a -> [a] -> [a]
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 = (a -> a -> a) -> [a] -> [a] -> [a]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (-) (Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
drop Int
1 [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 [] = String -> a
forall a. HasCallStack => String -> a
error String
"Impossible! Disco.Interpret.Core.constdiff []"
constdiff (a
x : [a]
xs)
  | (a -> Bool) -> [a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x) [a]
xs = a
x
  | Bool
otherwise = [a] -> a
forall a. (Eq a, Num a) => [a] -> a
constdiff ([a] -> [a]
forall a. Num a => [a] -> [a]
diff (a
x a -> [a] -> [a]
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 :: Value -> Value
oeisLookup ((Value -> Integer) -> Value -> [Integer]
forall a. (Value -> a) -> Value -> [a]
vlist Value -> Integer
vint -> [Integer]
ns) = Value -> (OEISSeq -> Value) -> Maybe OEISSeq -> Value
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Value
VNil OEISSeq -> Value
parseResult (SearchStatus -> Maybe OEISSeq
lookupSeq ([Integer] -> SearchStatus
SubSeq [Integer]
ns))
 where
  parseResult :: OEISSeq -> Value
parseResult OEISSeq
r = Side -> Value -> Value
VInj Side
R ((Char -> Value) -> String -> Value
forall a. (a -> Value) -> [a] -> Value
listv Char -> Value
charv (String
"https://oeis.org/" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Text -> String
T.unpack (OEISSeq -> Text
number OEISSeq
r)))

-- | 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 :: Value -> Value
oeisExtend = (Integer -> Value) -> [Integer] -> Value
forall a. (a -> Value) -> [a] -> Value
listv Integer -> Value
intv ([Integer] -> Value) -> (Value -> [Integer]) -> Value -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Integer] -> [Integer]
extendSeq ([Integer] -> [Integer])
-> (Value -> [Integer]) -> Value -> [Integer]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Value -> Integer) -> Value -> [Integer]
forall a. (Value -> a) -> Value -> [a]
vlist Value -> Integer
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 ([(Value, Integer)] -> [(Value, Integer)])
-> ([Value] -> [(Value, Integer)]) -> [Value] -> [(Value, Integer)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Value -> (Value, Integer)) -> [Value] -> [(Value, Integer)]
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 Integer -> Integer -> Integer
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) = Int
-> [(Value, Integer)] -> ([(Value, Integer)], [(Value, Integer)])
forall a. Int -> [a] -> ([a], [a])
splitAt ([(Value, Integer)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Value, Integer)]
xs Int -> Int -> Int
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) (Value, Integer) -> [(Value, Integer)] -> [(Value, Integer)]
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) (Value, Integer) -> [(Value, Integer)] -> [(Value, Integer)]
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) (Value, Integer) -> [(Value, Integer)] -> [(Value, Integer)]
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 [] [] = [(Value, Integer)] -> Sem r [(Value, Integer)]
forall a. a -> Sem r a
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 ([(Value, Integer)] -> Sem r [(Value, Integer)])
-> Sem r [(Value, Integer)] -> Sem r [(Value, Integer)]
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 ([(Value, Integer)] -> Sem r [(Value, Integer)])
-> Sem r [(Value, Integer)] -> Sem r [(Value, Integer)]
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 ([(Value, Integer)] -> Sem r [(Value, Integer)])
-> Sem r [(Value, Integer)] -> Sem r [(Value, Integer)]
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) (Value, Integer) -> [(Value, Integer)] -> [(Value, Integer)]
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 ([(Value, Integer)] -> Sem r [(Value, Integer)])
-> Sem r [(Value, Integer)] -> Sem r [(Value, Integer)]
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 ([(Value, Integer)] -> Sem r [(Value, Integer)])
-> Sem r [(Value, Integer)] -> Sem r [(Value, Integer)]
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) (Value, Integer) -> [(Value, Integer)] -> [(Value, Integer)]
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 <- Value -> [Value] -> Sem r Value
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)]
    [(Value, Integer)] -> Sem r [(Value, Integer)]
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Value, Integer)] -> Sem r [(Value, Integer)])
-> [(Value, Integer)] -> Sem r [(Value, Integer)]
forall a b. (a -> b) -> a -> b
$ case Value
nm of
      VNum Rational
0 -> [(Value, Integer)]
zs
      VNum Rational
n -> (Value
a, Rational -> Integer
forall a. Ratio a -> a
numerator Rational
n) (Value, Integer) -> [(Value, Integer)] -> [(Value, Integer)]
forall a. a -> [a] -> [a]
: [(Value, Integer)]
zs
      Value
v -> String -> [(Value, Integer)]
forall a. HasCallStack => String -> a
error (String -> [(Value, Integer)]) -> String -> [(Value, Integer)]
forall a b. (a -> b) -> a -> b
$ String
"Impossible! merge function in mergeM returned non-VNum " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
forall a. Show a => a -> String
show Value
v

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

graphSummary :: Graph SimpleValue -> Value
graphSummary :: Graph SimpleValue -> Value
graphSummary = [(SimpleValue, [SimpleValue])] -> Value
toDiscoAdjMap ([(SimpleValue, [SimpleValue])] -> Value)
-> (Graph SimpleValue -> [(SimpleValue, [SimpleValue])])
-> Graph SimpleValue
-> Value
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 =
    AdjacencyMap SimpleValue -> [(SimpleValue, [SimpleValue])]
forall a. AdjacencyMap a -> [(a, [a])]
AdjMap.adjacencyList (AdjacencyMap SimpleValue -> [(SimpleValue, [SimpleValue])])
-> (Graph SimpleValue -> AdjacencyMap SimpleValue)
-> Graph SimpleValue
-> [(SimpleValue, [SimpleValue])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AdjacencyMap SimpleValue
-> (SimpleValue -> AdjacencyMap SimpleValue)
-> (AdjacencyMap SimpleValue
    -> AdjacencyMap SimpleValue -> AdjacencyMap SimpleValue)
-> (AdjacencyMap SimpleValue
    -> AdjacencyMap SimpleValue -> AdjacencyMap SimpleValue)
-> Graph SimpleValue
-> AdjacencyMap SimpleValue
forall b a.
b -> (a -> b) -> (b -> b -> b) -> (b -> b -> b) -> Graph a -> b
foldg AdjacencyMap SimpleValue
forall a. AdjacencyMap a
AdjMap.empty SimpleValue -> AdjacencyMap SimpleValue
forall a. a -> AdjacencyMap a
AdjMap.vertex AdjacencyMap SimpleValue
-> AdjacencyMap SimpleValue -> AdjacencyMap SimpleValue
forall a.
Ord a =>
AdjacencyMap a -> AdjacencyMap a -> AdjacencyMap a
AdjMap.overlay AdjacencyMap SimpleValue
-> AdjacencyMap SimpleValue -> AdjacencyMap SimpleValue
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 (Map SimpleValue Value -> Value)
-> ([(SimpleValue, [SimpleValue])] -> Map SimpleValue Value)
-> [(SimpleValue, [SimpleValue])]
-> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(SimpleValue, Value)] -> Map SimpleValue Value
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(SimpleValue, Value)] -> Map SimpleValue Value)
-> ([(SimpleValue, [SimpleValue])] -> [(SimpleValue, Value)])
-> [(SimpleValue, [SimpleValue])]
-> Map SimpleValue Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((SimpleValue, [SimpleValue]) -> (SimpleValue, Value))
-> [(SimpleValue, [SimpleValue])] -> [(SimpleValue, Value)]
forall a b. (a -> b) -> [a] -> [b]
map (([SimpleValue] -> Value)
-> (SimpleValue, [SimpleValue]) -> (SimpleValue, Value)
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 ([(Value, Integer)] -> Value
VBag ([(Value, Integer)] -> Value)
-> ([SimpleValue] -> [(Value, Integer)]) -> [SimpleValue] -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Value] -> [(Value, Integer)]
countValues ([Value] -> [(Value, Integer)])
-> ([SimpleValue] -> [Value])
-> [SimpleValue]
-> [(Value, Integer)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SimpleValue -> Value) -> [SimpleValue] -> [Value]
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
_) = EvalError -> Sem r Value
forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw EvalError
e
resultToBool (TestResult Bool
b TestReason
_ TestEnv
_) = Value -> Sem r Value
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Sem r Value) -> Value -> Sem r Value
forall a b. (a -> b) -> a -> b
$ Bool -> Value
boolv 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 TestReason
forall a. TestReason_ a
TestBool TestEnv
emptyTestEnv)
ensureProp (VInj Side
R Value
_) = TestResult -> ValProp
VPDone (Bool -> TestReason -> TestEnv -> TestResult
TestResult Bool
True TestReason
forall a. TestReason_ a
TestBool TestEnv
emptyTestEnv)
ensureProp Value
_ = String -> ValProp
forall a. HasCallStack => String -> a
error String
"ensureProp: non-prop value"

combineTestResults :: LOp -> TestResult -> TestResult -> TestResult
combineTestResults :: LOp -> TestResult -> TestResult -> TestResult
combineTestResults LOp
op tr1 :: TestResult
tr1@(TestResult Bool
b1 TestReason
_ TestEnv
e1) tr2 :: TestResult
tr2@(TestResult Bool
b2 TestReason
_ TestEnv
e2) =
  Bool -> TestReason -> TestEnv -> TestResult
TestResult (LOp -> Bool -> Bool -> Bool
interpLOp LOp
op Bool
b1 Bool
b2) (LOp -> TestResult -> TestResult -> TestReason
forall a. LOp -> TestResult -> TestResult -> TestReason_ a
TestBin LOp
op TestResult
tr1 TestResult
tr2) (TestEnv -> TestEnv -> TestEnv
mergeTestEnv TestEnv
e1 TestEnv
e2)

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 = ValProp -> Sem r TestResult
forall (r :: EffectRow).
Members '[Random, State Mem] r =>
ValProp -> Sem r TestResult
checkProp (ValProp -> Sem r TestResult)
-> (Value -> ValProp) -> Value -> Sem r TestResult
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) = TestResult -> Sem r TestResult
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return TestResult
r
  checkProp (VPBin LOp
op ValProp
vp1 ValProp
vp2) = do
    TestResult
tr1 <- ValProp -> Sem r TestResult
forall (r :: EffectRow).
Members '[Random, State Mem] r =>
ValProp -> Sem r TestResult
checkProp ValProp
vp1
    TestResult
tr2 <- ValProp -> Sem r TestResult
forall (r :: EffectRow).
Members '[Random, State Mem] r =>
ValProp -> Sem r TestResult
checkProp ValProp
vp2
    TestResult -> Sem r TestResult
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (TestResult -> Sem r TestResult) -> TestResult -> Sem r TestResult
forall a b. (a -> b) -> a -> b
$ LOp -> TestResult -> TestResult -> TestResult
combineTestResults LOp
op TestResult
tr1 TestResult
tr2
  checkProp (VPSearch SearchMotive
sm [Type]
tys Value
f TestEnv
e) =
    TestEnv -> TestResult -> TestResult
extendResultEnv TestEnv
e (TestResult -> TestResult) -> Sem r TestResult -> Sem r TestResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SearchType -> IEnumeration [Value] -> Sem r ([[Value]], SearchType)
forall (r :: EffectRow) a.
Member Random r =>
SearchType -> IEnumeration a -> Sem r ([a], SearchType)
generateSamples SearchType
initialSt IEnumeration [Value]
vals Sem r ([[Value]], SearchType)
-> (([[Value]], SearchType) -> Sem r TestResult)
-> Sem r TestResult
forall a b. Sem r a -> (a -> Sem r b) -> Sem r b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ([[Value]], SearchType) -> Sem r TestResult
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) = TestResult -> Sem r TestResult
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (TestResult -> Sem r TestResult) -> TestResult -> Sem r TestResult
forall a b. (a -> b) -> a -> b
$ Bool -> TestReason -> TestEnv -> TestResult
TestResult (Bool -> Bool
not Bool
whenFound) (SearchType -> TestReason
forall a. SearchType -> TestReason_ a
TestNotFound SearchType
st) TestEnv
emptyTestEnv
    go ([Value]
x : [[Value]]
xs, SearchType
st) = do
      Either EvalError ValProp
mprop <- Sem (Error EvalError : r) ValProp
-> Sem r (Either EvalError ValProp)
forall e (r :: EffectRow) a.
Sem (Error e : r) a -> Sem r (Either e a)
runError (Value -> ValProp
ensureProp (Value -> ValProp)
-> Sem (Error EvalError : r) Value
-> Sem (Error EvalError : r) ValProp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value -> [Value] -> Sem (Error EvalError : r) Value
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 -> TestResult -> Sem r TestResult
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (TestResult -> Sem r TestResult) -> TestResult -> Sem r TestResult
forall a b. (a -> b) -> a -> b
$ Bool -> TestReason -> TestEnv -> TestResult
TestResult Bool
False (EvalError -> TestReason
forall a. EvalError -> TestReason_ a
TestRuntimeError EvalError
err) TestEnv
emptyTestEnv
        Right (VPDone TestResult
r) -> SearchType -> [[Value]] -> TestResult -> Sem r TestResult
forall (r :: EffectRow).
Members '[Random, State Mem] r =>
SearchType -> [[Value]] -> TestResult -> Sem r TestResult
continue SearchType
st [[Value]]
xs TestResult
r
        Right ValProp
prop -> ValProp -> Sem r TestResult
forall (r :: EffectRow).
Members '[Random, State Mem] r =>
ValProp -> Sem r TestResult
checkProp ValProp
prop Sem r TestResult
-> (TestResult -> Sem r TestResult) -> Sem r TestResult
forall a b. Sem r a -> (a -> Sem r b) -> Sem r b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SearchType -> [[Value]] -> TestResult -> Sem r TestResult
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 = TestResult -> Sem r TestResult
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return TestResult
r
      | TestResult -> Bool
testIsOk TestResult
r Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
wantsSuccess =
          TestResult -> Sem r TestResult
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (TestResult -> Sem r TestResult) -> TestResult -> Sem r TestResult
forall a b. (a -> b) -> a -> b
$ Bool -> TestReason -> TestEnv -> TestResult
TestResult Bool
whenFound (TestResult -> TestReason
forall a. TestResult -> TestReason_ a
TestFound TestResult
r) TestEnv
e'
      | Bool
otherwise = ([[Value]], SearchType) -> Sem r TestResult
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 =
  Sem (Fresh : r) (Either EvalError Value)
-> Sem r (Either EvalError Value)
forall (r :: EffectRow) a. Sem (Fresh : r) a -> Sem r a
runFresh (CESK -> Sem (Fresh : r) (Either EvalError Value)
forall (r :: EffectRow).
Members '[Fresh, Random, State Mem] r =>
CESK -> Sem r (Either EvalError Value)
runCESK (Value -> [Frame] -> CESK
Out Value
f ((Value -> Frame) -> [Value] -> [Frame]
forall a b. (a -> b) -> [a] -> [b]
map Value -> Frame
FArgV [Value]
xs))) Sem r (Either EvalError Value)
-> (Either EvalError Value -> Sem r Value) -> Sem r Value
forall a b. Sem r a -> (a -> Sem r b) -> Sem r b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (EvalError -> Sem r Value)
-> (Value -> Sem r Value) -> Either EvalError Value -> Sem r Value
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either EvalError -> Sem r Value
forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw Value -> Sem r Value
forall a. a -> Sem r a
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 = SearchType -> Value -> Sem r TestResult
forall (r :: EffectRow).
Members '[Random, State Mem] r =>
SearchType -> Value -> Sem r TestResult
testProperty (Integer -> Integer -> SearchType
Randomized Integer
n' Integer
n') (Value -> Sem r TestResult) -> Sem r Value -> Sem r TestResult
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Core -> Sem r Value
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' = Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
n Int -> Int -> Int
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
  Sem (Fresh : r) (Either EvalError Value)
-> Sem r (Either EvalError Value)
forall (r :: EffectRow) a. Sem (Fresh : r) a -> Sem r a
runFresh (CESK -> Sem (Fresh : r) (Either EvalError Value)
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 [])) Sem r (Either EvalError Value)
-> (Either EvalError Value -> Sem r Value) -> Sem r Value
forall a b. Sem r a -> (a -> Sem r b) -> Sem r b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (EvalError -> Sem r Value)
-> (Value -> Sem r Value) -> Either EvalError Value -> Sem r Value
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either EvalError -> Sem r Value
forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw Value -> Sem r Value
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return