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

-----------------------------------------------------------------------------
-- |
-- Module      :  Disco.Interpret.CESK
-- Copyright   :  disco team and contributors
-- Maintainer  :  byorgey@gmail.com
--
-- SPDX-License-Identifier: BSD-3-Clause
--
-- CESK machine interpreter for Disco.
-----------------------------------------------------------------------------

module Disco.Interpret.CESK
  ( CESK,
    runCESK,
    step,
    eval,
    runTest,
  )
where

import           Unbound.Generics.LocallyNameless   (Bind, Name)

import           Algebra.Graph
import qualified Algebra.Graph.AdjacencyMap         as AdjMap
import           Control.Arrow                      ((***), (>>>))
import           Control.Monad                      ((>=>))
import           Data.Bifunctor                     (first, second)
import           Data.List                          (find)
import qualified Data.Map                           as M
import           Data.Maybe                         (isJust)
import           Data.Ratio
import           Disco.AST.Core
import           Disco.AST.Generic                  (Ellipsis (..), Side (..),
                                                     selectSide)
import           Disco.AST.Typed                    (AProperty)
import           Disco.Compile
import           Disco.Context                      as Ctx
import           Disco.Enumerate
import           Disco.Error
import           Disco.Names
import           Disco.Property
import           Disco.Types                        hiding (V)
import           Disco.Value
import           Math.Combinatorics.Exact.Binomial  (choose)
import           Math.Combinatorics.Exact.Factorial (factorial)
import           Math.NumberTheory.Primes           (factorise, unPrime)
import           Math.NumberTheory.Primes.Testing   (isPrime)
import           Math.OEIS                          (catalogNums,
                                                     extendSequence,
                                                     lookupSequence)

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

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

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

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

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

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

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

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

-- | Is the CESK machine in a final state?
isFinal :: CESK -> Maybe (Either EvalError Value)
isFinal :: CESK -> Maybe (Either EvalError Value)
isFinal (Up EvalError
e [])  = 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 :: 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 (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 (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 :: 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 (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 (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 RationalDisplay
d Rational
r) Env
_ [Frame]
k) -> CESK -> Sem r CESK
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 (RationalDisplay -> Rational -> Value
VNum RationalDisplay
d Rational
r) [Frame]
k
  (In (CConst Op
OMatchErr) Env
_ [Frame]
k) -> CESK -> Sem r CESK
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 (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 (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 (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 (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 (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 (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 (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 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
    CESK -> Sem r CESK
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 (Env -> [Name Core] -> Core -> Value
VClo Env
e [Name Core]
xs Core
body) [Frame]
k
  (In (CApp Core
c1 Core
c2) Env
e [Frame]
k) -> CESK -> Sem r CESK
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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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
v2 (FApp (VClo Env
e [Name Core
x] Core
b) : [Frame]
k)) -> CESK -> Sem r CESK
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
v2 Env
e) [Frame]
k
  (Out Value
v2 (FApp (VClo Env
e (Name Core
x : [Name Core]
xs) Core
b) : [Frame]
k)) -> CESK -> Sem r CESK
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 (Env -> [Name Core] -> Core -> Value
VClo (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
v2 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 (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 Env
e [Name Core
x] Core
b) (FArgV Value
v : [Frame]
k)) -> CESK -> Sem r CESK
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 Env
e (Name Core
x : [Name Core]
xs) Core
b) (FArgV Value
v : [Frame]
k)) -> CESK -> Sem r CESK
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 (Env -> [Name Core] -> Core -> Value
VClo (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 :: (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 :: (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 :: [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 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 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 :: 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 (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 -> Rational) -> Value -> Sem r Value
forall (r :: EffectRow).
(Rational -> Rational -> Rational) -> Value -> Sem r Value
numOp2 (\Rational
m Rational
n -> 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) (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
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 :: 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 (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 (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Value
forall e. Enum e => e -> Value
enumv (Bool -> Value) -> Bool -> Value
forall a b. (a -> b) -> a -> b
$ Rational -> Rational -> Bool
forall a. Integral a => Ratio a -> Ratio a -> 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
    where
      divides :: Ratio a -> Ratio a -> Bool
divides Ratio a
0 Ratio a
0 = Bool
True
      divides Ratio a
0 Ratio a
_ = Bool
False
      divides Ratio a
x Ratio a
y = Ratio a -> a
forall a. Ratio a -> a
denominator (Ratio a
y Ratio a -> Ratio a -> Ratio a
forall a. Fractional a => a -> a -> a
/ Ratio a
x) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
1

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

  Op
OIsPrime -> (Integer -> Value) -> Value -> Sem r Value
forall (r :: EffectRow). (Integer -> Value) -> Value -> Sem r Value
intOp1 (Bool -> Value
forall e. Enum e => e -> Value
enumv (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 :: 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 (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 (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 (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 :: 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 (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 :: 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 (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
forall e. Enum e => e -> Value
enumv (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
forall e. Enum e => e -> Value
enumv (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 (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
forall e. Enum e => e -> Value
enumv (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
forall e. Enum e => e -> Value
enumv (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 (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)
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 (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)
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)
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 (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
mInteger -> 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 (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 (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 (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 (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 (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 (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)

  --------------------------------------------------
  -- 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
  OShouldEq 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 (Value -> Value -> Bool
valEq Value
v1 Value
v2) (Type -> Value -> Value -> TestReason
forall a. Type -> a -> a -> TestReason_ a
TestEqual Type
ty Value
v1 Value
v2) TestEnv
emptyTestEnv))

  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 :: 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 (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 (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 :: 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 :: 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 :: 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 :: 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 :: (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 (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' :: (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 :: (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 (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' :: (Rational -> Sem r Value) -> Value -> Sem r Value
numOp1' Rational -> Sem r Value
f (VNum RationalDisplay
_ Rational
m) = Rational -> Sem r Value
f Rational
m
numOp1' Rational -> Sem r Value
_ Value
v          = 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 :: (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 (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' :: (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 RationalDisplay
d1 Rational
n1, VNum RationalDisplay
d2 Rational
n2) -> do
      Value
res <- Rational
n1 Rational -> Rational -> Sem r Value
# Rational
n2
      case Value
res of
        VNum RationalDisplay
_ Rational
r -> Value -> Sem r Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Sem r Value) -> Value -> Sem r Value
forall a b. (a -> b) -> a -> b
$ RationalDisplay -> Rational -> Value
VNum (RationalDisplay
d1 RationalDisplay -> RationalDisplay -> RationalDisplay
forall a. Semigroup a => a -> a -> a
<> RationalDisplay
d2) Rational
r
        Value
_        -> Value -> Sem r Value
forall (m :: * -> *) a. Monad m => a -> m a
return Value
res
    (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. [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 :: [Integer]
iters = (Integer -> Integer) -> Integer -> [Integer]
forall a. (a -> a) -> a -> [a]
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 [Integer] -> Integer
forall a. [a] -> a
head ([Integer] -> Integer) -> [Integer] -> Integer
forall a b. (a -> b) -> a -> b
$ (Integer -> Bool) -> [Integer] -> [Integer]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Bool -> Bool
not (Bool -> Bool) -> (Integer -> Bool) -> Integer -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Bool
isRoot) [Integer]
iters

-- this operator is used for `integerSqrt'`
(^!) :: Num a => a -> Int -> a
^! :: 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 :: Value -> Value -> Bool
valEq :: Value -> Value -> Bool
valEq Value
v1 Value
v2 = Value -> Value -> Ordering
valCmp Value
v1 Value
v2 Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ

valLt :: Value -> Value -> Bool
valLt :: Value -> Value -> Bool
valLt Value
v1 Value
v2 = Value -> Value -> Ordering
valCmp Value
v1 Value
v2 Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
LT

valCmp :: Value -> Value -> Ordering
valCmp :: Value -> Value -> Ordering
valCmp (VNum RationalDisplay
_ Rational
r1) (VNum RationalDisplay
_ Rational
r2) = 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 (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 :: [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 :: [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 :: [a] -> [a]
diff [a]
xs = (a -> a -> a) -> [a] -> [a] -> [a]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (-) ([a] -> [a]
forall a. [a] -> [a]
tail [a]
xs) [a]
xs

-- | Take forward differences until the result is constant, and return
--   the constant.  The sign of the constant difference tells us the
--   limiting behavior of the sequence.
constdiff :: (Eq a, Num a) => [a] -> a
constdiff :: [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 -> (OEISSequence -> Value) -> Maybe OEISSequence -> Value
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Value
VNil OEISSequence -> Value
parseResult ([Integer] -> Maybe OEISSequence
lookupSequence [Integer]
ns)
  where
    parseResult :: OEISSequence -> Value
parseResult OEISSequence
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]
++ OEISSequence -> String
seqNum OEISSequence
r))
    seqNum :: OEISSequence -> String
seqNum = [String] -> String
forall a. [a] -> a
getCatalogNum ([String] -> String)
-> (OEISSequence -> [String]) -> OEISSequence -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OEISSequence -> [String]
catalogNums

    getCatalogNum :: [p] -> p
getCatalogNum []      = String -> p
forall a. HasCallStack => String -> a
error String
"No catalog info"
    getCatalogNum (p
n : [p]
_) = p
n

-- | Extends a Disco integer list with data from a known OEIS
--   sequence.  Returns a list of integers upon success, otherwise the
--   original list (unmodified).
oeisExtend :: Value -> Value
oeisExtend :: 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]
extendSequence ([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 (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 :: 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 (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 (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 RationalDisplay
_ Rational
0 -> [(Value, Integer)]
zs
        VNum RationalDisplay
_ 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 (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 :: 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 (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
forall e. Enum e => e -> Value
enumv Bool
b

notProp :: ValProp -> ValProp
notProp :: ValProp -> ValProp
notProp (VPDone TestResult
r)            = TestResult -> ValProp
VPDone (TestResult -> TestResult
invertPropResult TestResult
r)
notProp (VPSearch SearchMotive
sm [Type]
tys Value
p TestEnv
e) = SearchMotive -> [Type] -> Value -> TestEnv -> ValProp
VPSearch (SearchMotive -> SearchMotive
invertMotive SearchMotive
sm) [Type]
tys Value
p TestEnv
e

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

testProperty
  :: Members '[Random, State Mem] r
  => SearchType -> Value -> Sem r TestResult
testProperty :: 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 :: ValProp -> Sem r TestResult
checkProp (VPDone TestResult
r) = TestResult -> Sem r TestResult
forall (m :: * -> *) a. Monad m => a -> m a
return TestResult
r
    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 (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 :: ([[Value]], SearchType) -> Sem r TestResult
go ([], SearchType
st)   = TestResult -> Sem r TestResult
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 (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 (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 :: 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 (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 (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 :: 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 (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 (m :: * -> *) a. Monad m => a -> m a
return

runTest
  :: Members '[Random, Error EvalError, Input Env, State Mem] r
  => Int -> AProperty -> Sem r TestResult
runTest :: 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 :: Core -> Sem r Value
eval Core
c = do
  Env
e <- forall (r :: EffectRow). Member (Input Env) r => Sem r Env
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 (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 (m :: * -> *) a. Monad m => a -> m a
return