{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}

-- | A tutorial for how to use "Logic.Ltl" with higher-order effects.
-- The explanations here assume you've understood the simple tutorial in
-- "Examples.Ltl.Simple".
module Examples.Ltl.HigherOrder where

import Control.Applicative
import Control.Monad
import Control.Monad.Except
import Control.Monad.Identity
import Control.Monad.State
import Control.Monad.Writer
import Effect.Error
import Effect.Error.Passthrough ()
import Effect.TH
import Logic.Ltl
import Logic.SingleStep

-- * Example domain specification

-- $doc
-- Our domain will be a low level, Turing-complete, abstract machine
-- called 'MonadMiniLang' which is based on a stack of integers and
-- booleans and can raise three different errors. Values can be popped
-- and pushed, arbitrary text can be printed, and two control
-- structures are present: 'if_' and 'while_'.
--
-- These two latter operations are what makes 'MonadMiniLang' a
-- /higher order domain/: There are /nesting/ operations, that is,
-- operations that have sequences of operations in the same monad as
-- parameters.
--
-- In Graft, nested operations must occur in /positive position/ for
-- conceptual and technical reasons. As a reminder, @x@ is in
-- /positive/ position in @t@ if it stands before an even number of
-- @->@s, otherwise it is in /negative/ position. A few examples:
--
-- - In @a -> b@, @a@ is in negative position, @b@ in positive
-- - position.
--
-- - In @(a -> b) -> c@, @a@ and @c@ are in positive position, and @b@
--   is in negative position.
--
-- - In @Maybe ((a -> [b]) -> c) -> d@, @d@ and @b@ are in positive
--   position, and @a@ and @c@ are in negative position.

data MiniLangValue
  = MiniLangInteger Integer
  | MiniLangBoolean Bool
  deriving (Int -> MiniLangValue -> ShowS
[MiniLangValue] -> ShowS
MiniLangValue -> String
(Int -> MiniLangValue -> ShowS)
-> (MiniLangValue -> String)
-> ([MiniLangValue] -> ShowS)
-> Show MiniLangValue
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> MiniLangValue -> ShowS
showsPrec :: Int -> MiniLangValue -> ShowS
$cshow :: MiniLangValue -> String
show :: MiniLangValue -> String
$cshowList :: [MiniLangValue] -> ShowS
showList :: [MiniLangValue] -> ShowS
Show, MiniLangValue -> MiniLangValue -> Bool
(MiniLangValue -> MiniLangValue -> Bool)
-> (MiniLangValue -> MiniLangValue -> Bool) -> Eq MiniLangValue
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MiniLangValue -> MiniLangValue -> Bool
== :: MiniLangValue -> MiniLangValue -> Bool
$c/= :: MiniLangValue -> MiniLangValue -> Bool
/= :: MiniLangValue -> MiniLangValue -> Bool
Eq)

data MiniLangError
  = StackUnderflow
  | ExpectedBoolean
  | ExpectedInteger
  deriving (Int -> MiniLangError -> ShowS
[MiniLangError] -> ShowS
MiniLangError -> String
(Int -> MiniLangError -> ShowS)
-> (MiniLangError -> String)
-> ([MiniLangError] -> ShowS)
-> Show MiniLangError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> MiniLangError -> ShowS
showsPrec :: Int -> MiniLangError -> ShowS
$cshow :: MiniLangError -> String
show :: MiniLangError -> String
$cshowList :: [MiniLangError] -> ShowS
showList :: [MiniLangError] -> ShowS
Show, MiniLangError -> MiniLangError -> Bool
(MiniLangError -> MiniLangError -> Bool)
-> (MiniLangError -> MiniLangError -> Bool) -> Eq MiniLangError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MiniLangError -> MiniLangError -> Bool
== :: MiniLangError -> MiniLangError -> Bool
$c/= :: MiniLangError -> MiniLangError -> Bool
/= :: MiniLangError -> MiniLangError -> Bool
Eq)

class (Monad m) => MonadMiniLang m where
  push :: MiniLangValue -> m ()
  pop :: m MiniLangValue
  echo :: String -> m ()
  if_ :: m a -> m a -> m a
  while_ :: m () -> m ()

-- $doc
-- A concrete implementation for our domain: we use
--
-- - a list of values as inner state to account for the stack
--
-- - a writer to allow printing strings using 'echo'
--
-- - an exception to cover possible errors

type MiniLangT m = ExceptT MiniLangError (WriterT String (StateT [MiniLangValue] m))

runMiniLangT :: (Functor m) => MiniLangT m a -> m ((Either MiniLangError a, String), [MiniLangValue])
runMiniLangT :: forall (m :: * -> *) a.
Functor m =>
MiniLangT m a
-> m ((Either MiniLangError a, String), [MiniLangValue])
runMiniLangT MiniLangT m a
m = StateT [MiniLangValue] m (Either MiniLangError a, String)
-> [MiniLangValue]
-> m ((Either MiniLangError a, String), [MiniLangValue])
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (WriterT String (StateT [MiniLangValue] m) (Either MiniLangError a)
-> StateT [MiniLangValue] m (Either MiniLangError a, String)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (MiniLangT m a
-> WriterT
     String (StateT [MiniLangValue] m) (Either MiniLangError a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT MiniLangT m a
m)) []

instance (Monad m) => MonadMiniLang (MiniLangT m) where
  push :: MiniLangValue -> MiniLangT m ()
push MiniLangValue
v = do
    [MiniLangValue]
vs <- ExceptT
  MiniLangError
  (WriterT String (StateT [MiniLangValue] m))
  [MiniLangValue]
forall s (m :: * -> *). MonadState s m => m s
get
    [MiniLangValue] -> MiniLangT m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (MiniLangValue
v MiniLangValue -> [MiniLangValue] -> [MiniLangValue]
forall a. a -> [a] -> [a]
: [MiniLangValue]
vs)
  pop :: MiniLangT m MiniLangValue
pop = do
    [MiniLangValue]
vs <- ExceptT
  MiniLangError
  (WriterT String (StateT [MiniLangValue] m))
  [MiniLangValue]
forall s (m :: * -> *). MonadState s m => m s
get
    case [MiniLangValue]
vs of
      [] -> MiniLangError -> MiniLangT m MiniLangValue
forall a.
MiniLangError
-> ExceptT
     MiniLangError (WriterT String (StateT [MiniLangValue] m)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError MiniLangError
StackUnderflow
      (MiniLangValue
v : [MiniLangValue]
vs') -> [MiniLangValue] -> MiniLangT m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put [MiniLangValue]
vs' MiniLangT m ()
-> MiniLangT m MiniLangValue -> MiniLangT m MiniLangValue
forall a b.
ExceptT MiniLangError (WriterT String (StateT [MiniLangValue] m)) a
-> ExceptT
     MiniLangError (WriterT String (StateT [MiniLangValue] m)) b
-> ExceptT
     MiniLangError (WriterT String (StateT [MiniLangValue] m)) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> MiniLangValue -> MiniLangT m MiniLangValue
forall a.
a
-> ExceptT
     MiniLangError (WriterT String (StateT [MiniLangValue] m)) a
forall (m :: * -> *) a. Monad m => a -> m a
return MiniLangValue
v
  echo :: String -> MiniLangT m ()
echo = String -> MiniLangT m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell
  if_ :: forall a. MiniLangT m a -> MiniLangT m a -> MiniLangT m a
if_ MiniLangT m a
m1 MiniLangT m a
m2 = do
    MiniLangValue
v <- MiniLangT m MiniLangValue
forall (m :: * -> *). MonadMiniLang m => m MiniLangValue
pop
    case MiniLangValue
v of
      MiniLangBoolean Bool
True -> MiniLangT m a
m1
      MiniLangBoolean Bool
False -> MiniLangT m a
m2
      MiniLangValue
_ -> MiniLangError -> MiniLangT m a
forall a.
MiniLangError
-> ExceptT
     MiniLangError (WriterT String (StateT [MiniLangValue] m)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError MiniLangError
ExpectedBoolean
  while_ :: MiniLangT m () -> MiniLangT m ()
while_ MiniLangT m ()
m = do
    MiniLangValue
v <- MiniLangT m MiniLangValue
forall (m :: * -> *). MonadMiniLang m => m MiniLangValue
pop
    case MiniLangValue
v of
      MiniLangBoolean Bool
True -> MiniLangT m ()
m MiniLangT m () -> MiniLangT m () -> MiniLangT m ()
forall a b.
ExceptT MiniLangError (WriterT String (StateT [MiniLangValue] m)) a
-> ExceptT
     MiniLangError (WriterT String (StateT [MiniLangValue] m)) b
-> ExceptT
     MiniLangError (WriterT String (StateT [MiniLangValue] m)) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> MiniLangT m () -> MiniLangT m ()
forall (m :: * -> *). MonadMiniLang m => m () -> m ()
while_ MiniLangT m ()
m
      MiniLangBoolean Bool
False -> () -> MiniLangT m ()
forall a.
a
-> ExceptT
     MiniLangError (WriterT String (StateT [MiniLangValue] m)) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      MiniLangValue
_ -> MiniLangError -> MiniLangT m ()
forall a.
MiniLangError
-> ExceptT
     MiniLangError (WriterT String (StateT [MiniLangValue] m)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError MiniLangError
ExpectedBoolean

-- $doc
-- As in the simple tutorial, the 'MonadPlus' instance is necessary
-- boilerplate for the interpretation of 'Ltl' formulas, since there
-- might be several ways to satisfy one formula, and we want to try
-- them all.

instance {-# OVERLAPPING #-} (MonadPlus m) => Alternative (MiniLangT m) where
  empty :: forall a. MiniLangT m a
empty = WriterT String (StateT [MiniLangValue] m) a
-> ExceptT
     MiniLangError (WriterT String (StateT [MiniLangValue] m)) a
forall (m :: * -> *) a. Monad m => m a -> ExceptT MiniLangError m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (WriterT String (StateT [MiniLangValue] m) a
 -> ExceptT
      MiniLangError (WriterT String (StateT [MiniLangValue] m)) a)
-> WriterT String (StateT [MiniLangValue] m) a
-> ExceptT
     MiniLangError (WriterT String (StateT [MiniLangValue] m)) a
forall a b. (a -> b) -> a -> b
$ StateT [MiniLangValue] m a
-> WriterT String (StateT [MiniLangValue] m) a
forall (m :: * -> *) a. Monad m => m a -> WriterT String m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift StateT [MiniLangValue] m a
forall a. StateT [MiniLangValue] m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  ExceptT (WriterT (StateT [MiniLangValue]
-> m ((Either MiniLangError a, String), [MiniLangValue])
f)) <|> :: forall a. MiniLangT m a -> MiniLangT m a -> MiniLangT m a
<|> ExceptT (WriterT (StateT [MiniLangValue]
-> m ((Either MiniLangError a, String), [MiniLangValue])
g)) =
    WriterT String (StateT [MiniLangValue] m) (Either MiniLangError a)
-> ExceptT
     MiniLangError (WriterT String (StateT [MiniLangValue] m)) a
forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (WriterT String (StateT [MiniLangValue] m) (Either MiniLangError a)
 -> ExceptT
      MiniLangError (WriterT String (StateT [MiniLangValue] m)) a)
-> (([MiniLangValue]
     -> m ((Either MiniLangError a, String), [MiniLangValue]))
    -> WriterT
         String (StateT [MiniLangValue] m) (Either MiniLangError a))
-> ([MiniLangValue]
    -> m ((Either MiniLangError a, String), [MiniLangValue]))
-> ExceptT
     MiniLangError (WriterT String (StateT [MiniLangValue] m)) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT [MiniLangValue] m (Either MiniLangError a, String)
-> WriterT
     String (StateT [MiniLangValue] m) (Either MiniLangError a)
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterT (StateT [MiniLangValue] m (Either MiniLangError a, String)
 -> WriterT
      String (StateT [MiniLangValue] m) (Either MiniLangError a))
-> (([MiniLangValue]
     -> m ((Either MiniLangError a, String), [MiniLangValue]))
    -> StateT [MiniLangValue] m (Either MiniLangError a, String))
-> ([MiniLangValue]
    -> m ((Either MiniLangError a, String), [MiniLangValue]))
-> WriterT
     String (StateT [MiniLangValue] m) (Either MiniLangError a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([MiniLangValue]
 -> m ((Either MiniLangError a, String), [MiniLangValue]))
-> StateT [MiniLangValue] m (Either MiniLangError a, String)
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT (([MiniLangValue]
  -> m ((Either MiniLangError a, String), [MiniLangValue]))
 -> ExceptT
      MiniLangError (WriterT String (StateT [MiniLangValue] m)) a)
-> ([MiniLangValue]
    -> m ((Either MiniLangError a, String), [MiniLangValue]))
-> ExceptT
     MiniLangError (WriterT String (StateT [MiniLangValue] m)) a
forall a b. (a -> b) -> a -> b
$ \[MiniLangValue]
s -> [MiniLangValue]
-> m ((Either MiniLangError a, String), [MiniLangValue])
f [MiniLangValue]
s m ((Either MiniLangError a, String), [MiniLangValue])
-> m ((Either MiniLangError a, String), [MiniLangValue])
-> m ((Either MiniLangError a, String), [MiniLangValue])
forall a. m a -> m a -> m a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` [MiniLangValue]
-> m ((Either MiniLangError a, String), [MiniLangValue])
g [MiniLangValue]
s

instance {-# OVERLAPPING #-} (MonadPlus m) => MonadPlus (MiniLangT m)

-- * Using the effect system

-- $doc
-- To obtain the effects associated with "MiniLang" for free, we call
-- the same macros as in "Examples.Ltl.Simple" which also work in
-- higher order settings.

defineEffectType ''MonadMiniLang
makeEffect ''MonadMiniLang ''MonadMiniLangEffect

-- * Example programs in 'MonadMiniLang'

-- | A program that computes the nth Fibonacci number.
fibonacciExample :: (MonadError MiniLangError m, MonadMiniLang m) => Integer -> m Integer
fibonacciExample :: forall (m :: * -> *).
(MonadError MiniLangError m, MonadMiniLang m) =>
Integer -> m Integer
fibonacciExample Integer
n = do
  Integer -> m ()
forall (m :: * -> *). MonadMiniLang m => Integer -> m ()
pushInteger Integer
1
  Integer -> m ()
forall (m :: * -> *). MonadMiniLang m => Integer -> m ()
pushInteger Integer
0
  Integer -> m ()
forall (m :: * -> *). MonadMiniLang m => Integer -> m ()
pushInteger Integer
n
  Bool -> m ()
forall (m :: * -> *). MonadMiniLang m => Bool -> m ()
pushBoolean (Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0)
  m () -> m ()
forall (m :: * -> *). MonadMiniLang m => m () -> m ()
while_ (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
    Integer
n' <- m Integer
forall (m :: * -> *).
(MonadError MiniLangError m, MonadMiniLang m) =>
m Integer
popInteger
    Integer
b <- m Integer
forall (m :: * -> *).
(MonadError MiniLangError m, MonadMiniLang m) =>
m Integer
popInteger
    Integer
a <- m Integer
forall (m :: * -> *).
(MonadError MiniLangError m, MonadMiniLang m) =>
m Integer
popInteger
    String -> m ()
forall (m :: * -> *). MonadMiniLang m => String -> m ()
echo (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ Integer -> String
forall a. Show a => a -> String
show Integer
n' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
b String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n"
    Integer -> m ()
forall (m :: * -> *). MonadMiniLang m => Integer -> m ()
pushInteger (Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
b)
    Integer -> m ()
forall (m :: * -> *). MonadMiniLang m => Integer -> m ()
pushInteger Integer
a
    Integer -> m ()
forall (m :: * -> *). MonadMiniLang m => Integer -> m ()
pushInteger (Integer
n' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
    Bool -> m ()
forall (m :: * -> *). MonadMiniLang m => Bool -> m ()
pushBoolean (Integer
n' Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
1)
  Integer
_ <- m Integer
forall (m :: * -> *).
(MonadError MiniLangError m, MonadMiniLang m) =>
m Integer
popInteger
  m Integer
forall (m :: * -> *).
(MonadError MiniLangError m, MonadMiniLang m) =>
m Integer
popInteger

-- | A program that computes the greatest common divisor of two numbers.
gcdExample :: (MonadError MiniLangError m, MonadMiniLang m) => Integer -> Integer -> m Integer
gcdExample :: forall (m :: * -> *).
(MonadError MiniLangError m, MonadMiniLang m) =>
Integer -> Integer -> m Integer
gcdExample Integer
a Integer
b = do
  Integer -> m ()
forall (m :: * -> *). MonadMiniLang m => Integer -> m ()
pushInteger Integer
a
  Integer -> m ()
forall (m :: * -> *). MonadMiniLang m => Integer -> m ()
pushInteger Integer
b
  Bool -> m ()
forall (m :: * -> *). MonadMiniLang m => Bool -> m ()
pushBoolean (Integer
0 Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
b)
  m () -> m ()
forall (m :: * -> *). MonadMiniLang m => m () -> m ()
while_ (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
    Integer
b' <- m Integer
forall (m :: * -> *).
(MonadError MiniLangError m, MonadMiniLang m) =>
m Integer
popInteger
    Integer
a' <- m Integer
forall (m :: * -> *).
(MonadError MiniLangError m, MonadMiniLang m) =>
m Integer
popInteger
    Integer -> m ()
forall (m :: * -> *). MonadMiniLang m => Integer -> m ()
pushInteger Integer
b'
    Integer -> m ()
forall (m :: * -> *). MonadMiniLang m => Integer -> m ()
pushInteger (Integer
a' Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
b')
    Bool -> m ()
forall (m :: * -> *). MonadMiniLang m => Bool -> m ()
pushBoolean (Integer
0 Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
a' Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
b')
  Integer
_ <- m Integer
forall (m :: * -> *).
(MonadError MiniLangError m, MonadMiniLang m) =>
m Integer
popInteger
  m Integer
forall (m :: * -> *).
(MonadError MiniLangError m, MonadMiniLang m) =>
m Integer
popInteger

-- ** Helper functions used in the example programs

popInteger :: (MonadError MiniLangError m, MonadMiniLang m) => m Integer
popInteger :: forall (m :: * -> *).
(MonadError MiniLangError m, MonadMiniLang m) =>
m Integer
popInteger =
  m MiniLangValue
forall (m :: * -> *). MonadMiniLang m => m MiniLangValue
pop m MiniLangValue -> (MiniLangValue -> m Integer) -> m Integer
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    MiniLangInteger Integer
n -> Integer -> m Integer
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
n
    MiniLangValue
_ -> MiniLangError -> m Integer
forall a. MiniLangError -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError MiniLangError
ExpectedInteger

pushInteger :: (MonadMiniLang m) => Integer -> m ()
pushInteger :: forall (m :: * -> *). MonadMiniLang m => Integer -> m ()
pushInteger = MiniLangValue -> m ()
forall (m :: * -> *). MonadMiniLang m => MiniLangValue -> m ()
push (MiniLangValue -> m ())
-> (Integer -> MiniLangValue) -> Integer -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> MiniLangValue
MiniLangInteger

popBoolean :: (MonadError MiniLangError m, MonadMiniLang m) => m Bool
popBoolean :: forall (m :: * -> *).
(MonadError MiniLangError m, MonadMiniLang m) =>
m Bool
popBoolean =
  m MiniLangValue
forall (m :: * -> *). MonadMiniLang m => m MiniLangValue
pop m MiniLangValue -> (MiniLangValue -> m Bool) -> m Bool
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    MiniLangBoolean Bool
b -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
b
    MiniLangValue
_ -> MiniLangError -> m Bool
forall a. MiniLangError -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError MiniLangError
ExpectedBoolean

pushBoolean :: (MonadMiniLang m) => Bool -> m ()
pushBoolean :: forall (m :: * -> *). MonadMiniLang m => Bool -> m ()
pushBoolean = MiniLangValue -> m ()
forall (m :: * -> *). MonadMiniLang m => MiniLangValue -> m ()
push (MiniLangValue -> m ()) -> (Bool -> MiniLangValue) -> Bool -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> MiniLangValue
MiniLangBoolean

-- * Defining single step modifications

-- $doc
-- Our type of modifications is a conjunction of a function to be
-- applied before pushing a value, and a function to be applied after
-- poping a value. To combine those within a Semigroup instance, we
-- compose them while accounting for the fact that they can return
-- 'Nothing'.
--
-- Again, as explained in the simple tutorial, the
-- 'Semigroup' instance is necessary because evaluation of 'Ltl'
-- formulas might sometimes make it necessary to apply more than one
-- modification on the same operation.

data MiniLangMod = MiniLangMod
  { MiniLangMod -> MiniLangValue -> Maybe MiniLangValue
onPop :: MiniLangValue -> Maybe MiniLangValue,
    MiniLangMod -> MiniLangValue -> Maybe MiniLangValue
onPush :: MiniLangValue -> Maybe MiniLangValue
  }

instance Semigroup MiniLangMod where
  MiniLangMod MiniLangValue -> Maybe MiniLangValue
fPop MiniLangValue -> Maybe MiniLangValue
fPush <> :: MiniLangMod -> MiniLangMod -> MiniLangMod
<> MiniLangMod MiniLangValue -> Maybe MiniLangValue
gPop MiniLangValue -> Maybe MiniLangValue
gPush =
    (MiniLangValue -> Maybe MiniLangValue)
-> (MiniLangValue -> Maybe MiniLangValue) -> MiniLangMod
MiniLangMod
      (\MiniLangValue
x -> (MiniLangValue -> Maybe MiniLangValue
fPop (MiniLangValue -> Maybe MiniLangValue)
-> (MiniLangValue -> Maybe MiniLangValue)
-> MiniLangValue
-> Maybe MiniLangValue
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< MiniLangValue -> Maybe MiniLangValue
gPop) MiniLangValue
x Maybe MiniLangValue -> Maybe MiniLangValue -> Maybe MiniLangValue
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> MiniLangValue -> Maybe MiniLangValue
fPop MiniLangValue
x Maybe MiniLangValue -> Maybe MiniLangValue -> Maybe MiniLangValue
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> MiniLangValue -> Maybe MiniLangValue
gPop MiniLangValue
x)
      (\MiniLangValue
x -> (MiniLangValue -> Maybe MiniLangValue
fPush (MiniLangValue -> Maybe MiniLangValue)
-> (MiniLangValue -> Maybe MiniLangValue)
-> MiniLangValue
-> Maybe MiniLangValue
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< MiniLangValue -> Maybe MiniLangValue
gPush) MiniLangValue
x Maybe MiniLangValue -> Maybe MiniLangValue -> Maybe MiniLangValue
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> MiniLangValue -> Maybe MiniLangValue
fPush MiniLangValue
x Maybe MiniLangValue -> Maybe MiniLangValue -> Maybe MiniLangValue
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> MiniLangValue -> Maybe MiniLangValue
gPush MiniLangValue
x)

-- $doc
-- Meaning is given to the single step modifications through their
-- interpretation over our domain. This is what the class
-- 'InterpretLtlHigherOrder' is for. There are two main differences
-- with the first order case:
--
-- - The interpretation function directly handles 'Ltl'
--   formulas. (Remember that the 'InterpretMod' instance in the
--   simple tutorial only has to handle single-step modifications.)
--   This is because the approach based on applying atomic
--   modifications to single operations breaks down for higher-order
--   operations: a single higher-order operation may contain sequences
--   ('AST's) of operations.
--
-- - An explicit distinction needs to be made between first-order and
--   higher-order effect constructors, by using 'Direct' and 'Nested'
--   respectively.
--
-- Considering the second difference:
--
-- - Using 'Direct' signals that the operation at hand is first order,
--   and you can proceed as if writing an 'InterpretMod' instance, as
--   explained in the simple tutorial.
--
-- - Using 'Nested' means the operation is of higher order. This case
--   is detailed below.
--
-- Handling higher order operations:
--
-- In the first order setting, we have the convenient class
-- 'InterpretMod' which allows us to specify how single-step
-- modifications should be applied on operations. In the higher order
-- setting the question is different: applying a single step
-- modification on a nested operation makes no sense because it will
-- likely contain several such operations, thus we provide the whole
-- set of formulas to be applied currently and leave it to the user as
-- to how they should be handling those. While it seems complicated,
-- it is actually pretty straighforward in most cases as the user has
-- sufficient domain knowledge to know how and when the nested blocks
-- will be executed.
--
-- In the example:
--
-- Let's explain 'if_' here. The typical behaviour of 'if_' will be to
-- evaluate the condition and pass the formula that modifies the
-- remainder of the computation to either of the two branches,
-- depending on whether the condition was true or false. In the case
-- of our example, evaluation the condition is itself an operation,
-- namely a 'pop'. So, we will first consume the next single step
-- modification and apply it to that 'pop'. If that was successful,
-- we'll pass on the remaining formulas to the correct block depending
-- on the result of the (possibly modified) result of evaluating the
-- condition.
--
-- Note how we use the function 'nowLaterList' which, from a list of
-- Ltl formulas, creates a list of pairs of a modification to be
-- applied now and the remaining formulas. This function will likely
-- often be called in higher order operations.

instance
  (MonadPlus m, MonadError MiniLangError m, MonadMiniLang m) =>
  InterpretLtlHigherOrder MiniLangMod m MonadMiniLangEffect
  where
  interpretLtlHigherOrder :: forall (ops :: [(* -> *) -> * -> *]) a.
MonadMiniLangEffect (AST ops) a
-> LtlInterpHigherOrder MiniLangMod m ops a
interpretLtlHigherOrder (Push MiniLangValue
v) = ModInterp MiniLangMod m a
-> LtlInterpHigherOrder MiniLangMod m ops a
forall mod (m :: * -> *) a (ops :: [(* -> *) -> * -> *]).
ModInterp mod m a -> LtlInterpHigherOrder mod m ops a
Direct (ModInterp MiniLangMod m a
 -> LtlInterpHigherOrder MiniLangMod m ops a)
-> ModInterp MiniLangMod m a
-> LtlInterpHigherOrder MiniLangMod m ops a
forall a b. (a -> b) -> a -> b
$ (MiniLangMod -> m (Maybe a)) -> ModInterp MiniLangMod m a
forall mod (m :: * -> *) a.
(mod -> m (Maybe a)) -> ModInterp mod m a
Visible ((MiniLangMod -> m (Maybe a)) -> ModInterp MiniLangMod m a)
-> (MiniLangMod -> m (Maybe a)) -> ModInterp MiniLangMod m a
forall a b. (a -> b) -> a -> b
$ \MiniLangMod
modif ->
    case MiniLangMod -> MiniLangValue -> Maybe MiniLangValue
onPush MiniLangMod
modif MiniLangValue
v of
      Just MiniLangValue
v' -> a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> m a -> m (Maybe a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MiniLangValue -> m ()
forall (m :: * -> *). MonadMiniLang m => MiniLangValue -> m ()
push MiniLangValue
v'
      Maybe MiniLangValue
Nothing -> Maybe a -> m (Maybe a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing
  interpretLtlHigherOrder MonadMiniLangEffect (AST ops) a
Pop = ModInterp MiniLangMod m a
-> LtlInterpHigherOrder MiniLangMod m ops a
forall mod (m :: * -> *) a (ops :: [(* -> *) -> * -> *]).
ModInterp mod m a -> LtlInterpHigherOrder mod m ops a
Direct (ModInterp MiniLangMod m a
 -> LtlInterpHigherOrder MiniLangMod m ops a)
-> ModInterp MiniLangMod m a
-> LtlInterpHigherOrder MiniLangMod m ops a
forall a b. (a -> b) -> a -> b
$ (MiniLangMod -> m (Maybe a)) -> ModInterp MiniLangMod m a
forall mod (m :: * -> *) a.
(mod -> m (Maybe a)) -> ModInterp mod m a
Visible ((MiniLangMod -> m (Maybe a)) -> ModInterp MiniLangMod m a)
-> (MiniLangMod -> m (Maybe a)) -> ModInterp MiniLangMod m a
forall a b. (a -> b) -> a -> b
$ \MiniLangMod
modif -> MiniLangMod -> MiniLangValue -> Maybe MiniLangValue
onPop MiniLangMod
modif (MiniLangValue -> Maybe a) -> m MiniLangValue -> m (Maybe a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m MiniLangValue
forall (m :: * -> *). MonadMiniLang m => m MiniLangValue
pop
  interpretLtlHigherOrder Echo {} = ModInterp MiniLangMod m a
-> LtlInterpHigherOrder MiniLangMod m ops a
forall mod (m :: * -> *) a (ops :: [(* -> *) -> * -> *]).
ModInterp mod m a -> LtlInterpHigherOrder mod m ops a
Direct ModInterp MiniLangMod m a
forall mod (m :: * -> *) a. ModInterp mod m a
Invisible
  interpretLtlHigherOrder (If_ AST ops a
m1 AST ops a
m2) = ((forall b.
  [Ltl MiniLangMod] -> AST ops b -> m (b, [Ltl MiniLangMod]))
 -> [Ltl MiniLangMod] -> m (Maybe (a, [Ltl MiniLangMod])))
-> LtlInterpHigherOrder MiniLangMod m ops a
forall mod (ops :: [(* -> *) -> * -> *]) (m :: * -> *) a.
((forall b. [Ltl mod] -> AST ops b -> m (b, [Ltl mod]))
 -> [Ltl mod] -> m (Maybe (a, [Ltl mod])))
-> LtlInterpHigherOrder mod m ops a
Nested (((forall b.
   [Ltl MiniLangMod] -> AST ops b -> m (b, [Ltl MiniLangMod]))
  -> [Ltl MiniLangMod] -> m (Maybe (a, [Ltl MiniLangMod])))
 -> LtlInterpHigherOrder MiniLangMod m ops a)
-> ((forall b.
     [Ltl MiniLangMod] -> AST ops b -> m (b, [Ltl MiniLangMod]))
    -> [Ltl MiniLangMod] -> m (Maybe (a, [Ltl MiniLangMod])))
-> LtlInterpHigherOrder MiniLangMod m ops a
forall a b. (a -> b) -> a -> b
$ \forall b.
[Ltl MiniLangMod] -> AST ops b -> m (b, [Ltl MiniLangMod])
evalAST [Ltl MiniLangMod]
ltls -> do
    MiniLangValue
v <- m MiniLangValue
forall (m :: * -> *). MonadMiniLang m => m MiniLangValue
pop
    [m (Maybe (a, [Ltl MiniLangMod]))]
-> m (Maybe (a, [Ltl MiniLangMod]))
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([m (Maybe (a, [Ltl MiniLangMod]))]
 -> m (Maybe (a, [Ltl MiniLangMod])))
-> [m (Maybe (a, [Ltl MiniLangMod]))]
-> m (Maybe (a, [Ltl MiniLangMod]))
forall a b. (a -> b) -> a -> b
$
      ((Maybe MiniLangMod, [Ltl MiniLangMod])
 -> m (Maybe (a, [Ltl MiniLangMod])))
-> [(Maybe MiniLangMod, [Ltl MiniLangMod])]
-> [m (Maybe (a, [Ltl MiniLangMod]))]
forall a b. (a -> b) -> [a] -> [b]
map
        ( \(Maybe MiniLangMod
now, [Ltl MiniLangMod]
later) ->
            let vMiniLangModed :: Maybe MiniLangValue
vMiniLangModed = case Maybe MiniLangMod
now of
                  Just MiniLangMod
x -> MiniLangMod -> MiniLangValue -> Maybe MiniLangValue
onPop MiniLangMod
x MiniLangValue
v
                  Maybe MiniLangMod
Nothing -> MiniLangValue -> Maybe MiniLangValue
forall a. a -> Maybe a
Just MiniLangValue
v
             in case Maybe MiniLangValue
vMiniLangModed of
                  Just (MiniLangBoolean Bool
True) -> (a, [Ltl MiniLangMod]) -> Maybe (a, [Ltl MiniLangMod])
forall a. a -> Maybe a
Just ((a, [Ltl MiniLangMod]) -> Maybe (a, [Ltl MiniLangMod]))
-> m (a, [Ltl MiniLangMod]) -> m (Maybe (a, [Ltl MiniLangMod]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Ltl MiniLangMod] -> AST ops a -> m (a, [Ltl MiniLangMod])
forall b.
[Ltl MiniLangMod] -> AST ops b -> m (b, [Ltl MiniLangMod])
evalAST [Ltl MiniLangMod]
later AST ops a
m1
                  Just (MiniLangBoolean Bool
False) -> (a, [Ltl MiniLangMod]) -> Maybe (a, [Ltl MiniLangMod])
forall a. a -> Maybe a
Just ((a, [Ltl MiniLangMod]) -> Maybe (a, [Ltl MiniLangMod]))
-> m (a, [Ltl MiniLangMod]) -> m (Maybe (a, [Ltl MiniLangMod]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Ltl MiniLangMod] -> AST ops a -> m (a, [Ltl MiniLangMod])
forall b.
[Ltl MiniLangMod] -> AST ops b -> m (b, [Ltl MiniLangMod])
evalAST [Ltl MiniLangMod]
later AST ops a
m2
                  Maybe MiniLangValue
Nothing -> Maybe (a, [Ltl MiniLangMod]) -> m (Maybe (a, [Ltl MiniLangMod]))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (a, [Ltl MiniLangMod])
forall a. Maybe a
Nothing
                  Maybe MiniLangValue
_ -> MiniLangError -> m (Maybe (a, [Ltl MiniLangMod]))
forall a. MiniLangError -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError MiniLangError
ExpectedBoolean
        )
        ([Ltl MiniLangMod] -> [(Maybe MiniLangMod, [Ltl MiniLangMod])]
forall a. Semigroup a => [Ltl a] -> [(Maybe a, [Ltl a])]
nowLaterList [Ltl MiniLangMod]
ltls)
  interpretLtlHigherOrder (While_ AST ops ()
m) = ((forall b.
  [Ltl MiniLangMod] -> AST ops b -> m (b, [Ltl MiniLangMod]))
 -> [Ltl MiniLangMod] -> m (Maybe (a, [Ltl MiniLangMod])))
-> LtlInterpHigherOrder MiniLangMod m ops a
forall mod (ops :: [(* -> *) -> * -> *]) (m :: * -> *) a.
((forall b. [Ltl mod] -> AST ops b -> m (b, [Ltl mod]))
 -> [Ltl mod] -> m (Maybe (a, [Ltl mod])))
-> LtlInterpHigherOrder mod m ops a
Nested (((forall b.
   [Ltl MiniLangMod] -> AST ops b -> m (b, [Ltl MiniLangMod]))
  -> [Ltl MiniLangMod] -> m (Maybe (a, [Ltl MiniLangMod])))
 -> LtlInterpHigherOrder MiniLangMod m ops a)
-> ((forall b.
     [Ltl MiniLangMod] -> AST ops b -> m (b, [Ltl MiniLangMod]))
    -> [Ltl MiniLangMod] -> m (Maybe (a, [Ltl MiniLangMod])))
-> LtlInterpHigherOrder MiniLangMod m ops a
forall a b. (a -> b) -> a -> b
$ \forall b.
[Ltl MiniLangMod] -> AST ops b -> m (b, [Ltl MiniLangMod])
evalAST [Ltl MiniLangMod]
ltls -> do
    MiniLangValue
v <- m MiniLangValue
forall (m :: * -> *). MonadMiniLang m => m MiniLangValue
pop
    [m (Maybe (a, [Ltl MiniLangMod]))]
-> m (Maybe (a, [Ltl MiniLangMod]))
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([m (Maybe (a, [Ltl MiniLangMod]))]
 -> m (Maybe (a, [Ltl MiniLangMod])))
-> [m (Maybe (a, [Ltl MiniLangMod]))]
-> m (Maybe (a, [Ltl MiniLangMod]))
forall a b. (a -> b) -> a -> b
$
      ((Maybe MiniLangMod, [Ltl MiniLangMod])
 -> m (Maybe (a, [Ltl MiniLangMod])))
-> [(Maybe MiniLangMod, [Ltl MiniLangMod])]
-> [m (Maybe (a, [Ltl MiniLangMod]))]
forall a b. (a -> b) -> [a] -> [b]
map
        ( \(Maybe MiniLangMod
now, [Ltl MiniLangMod]
later) ->
            let vMiniLangModed :: Maybe MiniLangValue
vMiniLangModed = case Maybe MiniLangMod
now of
                  Just MiniLangMod
x -> MiniLangMod -> MiniLangValue -> Maybe MiniLangValue
onPop MiniLangMod
x MiniLangValue
v
                  Maybe MiniLangMod
Nothing -> MiniLangValue -> Maybe MiniLangValue
forall a. a -> Maybe a
Just MiniLangValue
v
             in case Maybe MiniLangValue
vMiniLangModed of
                  Just (MiniLangBoolean Bool
True) -> do
                    ((), [Ltl MiniLangMod]
later') <- [Ltl MiniLangMod] -> AST ops () -> m ((), [Ltl MiniLangMod])
forall b.
[Ltl MiniLangMod] -> AST ops b -> m (b, [Ltl MiniLangMod])
evalAST [Ltl MiniLangMod]
later AST ops ()
m
                    case MonadMiniLangEffect (AST ops) ()
-> LtlInterpHigherOrder MiniLangMod m ops ()
forall (ops :: [(* -> *) -> * -> *]) a.
MonadMiniLangEffect (AST ops) a
-> LtlInterpHigherOrder MiniLangMod m ops a
forall mod (m :: * -> *) (op :: (* -> *) -> * -> *)
       (ops :: [(* -> *) -> * -> *]) a.
InterpretLtlHigherOrder mod m op =>
op (AST ops) a -> LtlInterpHigherOrder mod m ops a
interpretLtlHigherOrder (AST ops () -> MonadMiniLangEffect (AST ops) ()
forall (m :: * -> *). m () -> MonadMiniLangEffect m ()
While_ AST ops ()
m) of
                      Nested (forall b.
 [Ltl MiniLangMod] -> AST ops b -> m (b, [Ltl MiniLangMod]))
-> [Ltl MiniLangMod] -> m (Maybe ((), [Ltl MiniLangMod]))
f -> (forall b.
 [Ltl MiniLangMod] -> AST ops b -> m (b, [Ltl MiniLangMod]))
-> [Ltl MiniLangMod] -> m (Maybe ((), [Ltl MiniLangMod]))
f [Ltl MiniLangMod] -> AST ops b -> m (b, [Ltl MiniLangMod])
forall b.
[Ltl MiniLangMod] -> AST ops b -> m (b, [Ltl MiniLangMod])
evalAST [Ltl MiniLangMod]
later'
                      LtlInterpHigherOrder MiniLangMod m ops ()
_ -> String -> m (Maybe (a, [Ltl MiniLangMod]))
forall a. HasCallStack => String -> a
error String
"impossible"
                  Just (MiniLangBoolean Bool
False) -> Maybe (a, [Ltl MiniLangMod]) -> m (Maybe (a, [Ltl MiniLangMod]))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (a, [Ltl MiniLangMod]) -> m (Maybe (a, [Ltl MiniLangMod])))
-> Maybe (a, [Ltl MiniLangMod]) -> m (Maybe (a, [Ltl MiniLangMod]))
forall a b. (a -> b) -> a -> b
$ (a, [Ltl MiniLangMod]) -> Maybe (a, [Ltl MiniLangMod])
forall a. a -> Maybe a
Just ((), [Ltl MiniLangMod]
later)
                  Maybe MiniLangValue
Nothing -> Maybe (a, [Ltl MiniLangMod]) -> m (Maybe (a, [Ltl MiniLangMod]))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (a, [Ltl MiniLangMod])
forall a. Maybe a
Nothing
                  Maybe MiniLangValue
_ -> MiniLangError -> m (Maybe (a, [Ltl MiniLangMod]))
forall a. MiniLangError -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError MiniLangError
ExpectedBoolean
        )
        ([Ltl MiniLangMod] -> [(Maybe MiniLangMod, [Ltl MiniLangMod])]
forall a. Semigroup a => [Ltl a] -> [(Maybe a, [Ltl a])]
nowLaterList [Ltl MiniLangMod]
ltls)

-- * Smart constructors of modifications

-- | Modify boolean values on pop
popBoolMiniLangMod :: (Bool -> Maybe Bool) -> MiniLangMod
popBoolMiniLangMod :: (Bool -> Maybe Bool) -> MiniLangMod
popBoolMiniLangMod Bool -> Maybe Bool
f =
  MiniLangMod
    { onPop :: MiniLangValue -> Maybe MiniLangValue
onPop = \case
        MiniLangBoolean Bool
b -> Bool -> MiniLangValue
MiniLangBoolean (Bool -> MiniLangValue) -> Maybe Bool -> Maybe MiniLangValue
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> Maybe Bool
f Bool
b
        MiniLangValue
_ -> Maybe MiniLangValue
forall a. Maybe a
Nothing,
      onPush :: MiniLangValue -> Maybe MiniLangValue
onPush = Maybe MiniLangValue -> MiniLangValue -> Maybe MiniLangValue
forall a b. a -> b -> a
const Maybe MiniLangValue
forall a. Maybe a
Nothing
    }

-- | Modify integer values on pop
popIntegerMiniLangMod :: (Integer -> Maybe Integer) -> MiniLangMod
popIntegerMiniLangMod :: (Integer -> Maybe Integer) -> MiniLangMod
popIntegerMiniLangMod Integer -> Maybe Integer
f =
  MiniLangMod
    { onPop :: MiniLangValue -> Maybe MiniLangValue
onPop = \case
        MiniLangInteger Integer
n -> Integer -> MiniLangValue
MiniLangInteger (Integer -> MiniLangValue) -> Maybe Integer -> Maybe MiniLangValue
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Integer -> Maybe Integer
f Integer
n
        MiniLangValue
_ -> Maybe MiniLangValue
forall a. Maybe a
Nothing,
      onPush :: MiniLangValue -> Maybe MiniLangValue
onPush = Maybe MiniLangValue -> MiniLangValue -> Maybe MiniLangValue
forall a b. a -> b -> a
const Maybe MiniLangValue
forall a. Maybe a
Nothing
    }

-- | Modify all values on pop
popMiniLangMod :: (Bool -> Maybe Bool) -> (Integer -> Maybe Integer) -> MiniLangMod
popMiniLangMod :: (Bool -> Maybe Bool) -> (Integer -> Maybe Integer) -> MiniLangMod
popMiniLangMod Bool -> Maybe Bool
fBool Integer -> Maybe Integer
fInteger = (Bool -> Maybe Bool) -> MiniLangMod
popBoolMiniLangMod Bool -> Maybe Bool
fBool MiniLangMod -> MiniLangMod -> MiniLangMod
forall a. Semigroup a => a -> a -> a
<> (Integer -> Maybe Integer) -> MiniLangMod
popIntegerMiniLangMod Integer -> Maybe Integer
fInteger

-- | Modify booleans on push
pushBoolMiniLangMod :: (Bool -> Maybe Bool) -> MiniLangMod
pushBoolMiniLangMod :: (Bool -> Maybe Bool) -> MiniLangMod
pushBoolMiniLangMod Bool -> Maybe Bool
f =
  MiniLangMod
    { onPop :: MiniLangValue -> Maybe MiniLangValue
onPop = Maybe MiniLangValue -> MiniLangValue -> Maybe MiniLangValue
forall a b. a -> b -> a
const Maybe MiniLangValue
forall a. Maybe a
Nothing,
      onPush :: MiniLangValue -> Maybe MiniLangValue
onPush = \case
        MiniLangBoolean Bool
b -> Bool -> MiniLangValue
MiniLangBoolean (Bool -> MiniLangValue) -> Maybe Bool -> Maybe MiniLangValue
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> Maybe Bool
f Bool
b
        MiniLangValue
_ -> Maybe MiniLangValue
forall a. Maybe a
Nothing
    }

-- | Modify integers on push
pushIntegerMiniLangMod :: (Integer -> Maybe Integer) -> MiniLangMod
pushIntegerMiniLangMod :: (Integer -> Maybe Integer) -> MiniLangMod
pushIntegerMiniLangMod Integer -> Maybe Integer
f =
  MiniLangMod
    { onPop :: MiniLangValue -> Maybe MiniLangValue
onPop = Maybe MiniLangValue -> MiniLangValue -> Maybe MiniLangValue
forall a b. a -> b -> a
const Maybe MiniLangValue
forall a. Maybe a
Nothing,
      onPush :: MiniLangValue -> Maybe MiniLangValue
onPush = \case
        MiniLangInteger Integer
n -> Integer -> MiniLangValue
MiniLangInteger (Integer -> MiniLangValue) -> Maybe Integer -> Maybe MiniLangValue
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Integer -> Maybe Integer
f Integer
n
        MiniLangValue
_ -> Maybe MiniLangValue
forall a. Maybe a
Nothing
    }

-- | Modify all values on push
pushMiniLangMod :: (Bool -> Maybe Bool) -> (Integer -> Maybe Integer) -> MiniLangMod
pushMiniLangMod :: (Bool -> Maybe Bool) -> (Integer -> Maybe Integer) -> MiniLangMod
pushMiniLangMod Bool -> Maybe Bool
fBool Integer -> Maybe Integer
fInteger = (Bool -> Maybe Bool) -> MiniLangMod
pushBoolMiniLangMod Bool -> Maybe Bool
fBool MiniLangMod -> MiniLangMod -> MiniLangMod
forall a. Semigroup a => a -> a -> a
<> (Integer -> Maybe Integer) -> MiniLangMod
pushIntegerMiniLangMod Integer -> Maybe Integer
fInteger

-- | Negate booleans on pop and push
flipBools :: MiniLangMod
flipBools :: MiniLangMod
flipBools = (Bool -> Maybe Bool) -> MiniLangMod
popBoolMiniLangMod (Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool -> Maybe Bool) -> (Bool -> Bool) -> Bool -> Maybe Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
not) MiniLangMod -> MiniLangMod -> MiniLangMod
forall a. Semigroup a => a -> a -> a
<> (Bool -> Maybe Bool) -> MiniLangMod
pushBoolMiniLangMod (Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool -> Maybe Bool) -> (Bool -> Bool) -> Bool -> Maybe Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
not)

-- | Negate integers on pop and push
flipIntegers :: MiniLangMod
flipIntegers :: MiniLangMod
flipIntegers = (Integer -> Maybe Integer) -> MiniLangMod
popIntegerMiniLangMod (Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Maybe Integer)
-> (Integer -> Integer) -> Integer -> Maybe Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer
forall a. Num a => a -> a
negate) MiniLangMod -> MiniLangMod -> MiniLangMod
forall a. Semigroup a => a -> a -> a
<> (Integer -> Maybe Integer) -> MiniLangMod
pushIntegerMiniLangMod (Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Maybe Integer)
-> (Integer -> Integer) -> Integer -> Maybe Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer
forall a. Num a => a -> a
negate)

-- | Negate all values on pop and push
flipBoth :: MiniLangMod
flipBoth :: MiniLangMod
flipBoth = MiniLangMod
flipBools MiniLangMod -> MiniLangMod -> MiniLangMod
forall a. Semigroup a => a -> a -> a
<> MiniLangMod
flipIntegers

-- | Apply the modulo operation on pop and push for integers
moduloMiniLangMod :: Integer -> MiniLangMod
moduloMiniLangMod :: Integer -> MiniLangMod
moduloMiniLangMod Integer
n = (Integer -> Maybe Integer) -> MiniLangMod
popIntegerMiniLangMod (Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Maybe Integer)
-> (Integer -> Integer) -> Integer -> Maybe Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
n)) MiniLangMod -> MiniLangMod -> MiniLangMod
forall a. Semigroup a => a -> a -> a
<> (Integer -> Maybe Integer) -> MiniLangMod
pushIntegerMiniLangMod (Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Maybe Integer)
-> (Integer -> Integer) -> Integer -> Maybe Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
n))

-- * Running modified MiniLang programs

-- $doc
-- As in the simple tutorial, we can use the function
-- 'interpretLtlAST' to obtain a function that will interpret an
-- 'LtlAST' of 'MonadMiniLangEffect' and 'MonadErrorEffect'.
--
-- Note that the 'LtlInstanceKind' for the 'MonadMiniLangEffect' is
-- 'InterpretLtlHigherOrderTag', since that's the instance that we
-- implemented above: @InterpretLtlHigherOrder MiniLangMod m
-- MonadMiniLangEffect@.
--
-- Again, the 'InterpretEffectStateful' instance for @MonadErrorEffect
-- MiniLangError@ is the \"passthrough\" instance imported from
-- "Effect.Error.Passthtrough", which ignores all modifications: We're
-- only interested in modifying 'MonadMiniLang' operations in the
-- program, not its generic error handling.

interpretAndRunMiniLang ::
  LtlAST MiniLangMod '[MonadMiniLangEffect, MonadErrorEffect MiniLangError] a ->
  [((Either MiniLangError a, String), [MiniLangValue])]
interpretAndRunMiniLang :: forall a.
LtlAST
  MiniLangMod
  '[MonadMiniLangEffect, MonadErrorEffect MiniLangError]
  a
-> [((Either MiniLangError a, String), [MiniLangValue])]
interpretAndRunMiniLang =
  MiniLangT [] a
-> [((Either MiniLangError a, String), [MiniLangValue])]
forall (m :: * -> *) a.
Functor m =>
MiniLangT m a
-> m ((Either MiniLangError a, String), [MiniLangValue])
runMiniLangT
    (MiniLangT [] a
 -> [((Either MiniLangError a, String), [MiniLangValue])])
-> (LtlAST
      MiniLangMod
      '[MonadMiniLangEffect, MonadErrorEffect MiniLangError]
      a
    -> MiniLangT [] a)
-> LtlAST
     MiniLangMod
     '[MonadMiniLangEffect, MonadErrorEffect MiniLangError]
     a
-> [((Either MiniLangError a, String), [MiniLangValue])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (tags :: [LtlInstanceKind]) mod (m :: * -> *)
       (ops :: [(* -> *) -> * -> *]) a.
(Semigroup mod, MonadPlus m, InterpretEffectsLtl mod m tags ops) =>
LtlAST mod ops a -> m a
interpretLtlAST
      @'[ InterpretLtlHigherOrderTag,
          InterpretEffectStatefulTag
        ]

-- $doc
-- As in the simple simple tutorial, we can apply the 'modifyLtl'
-- function to modify the 'MonadMiniLang' operations in the program.

exampleSomewhere :: [((Either MiniLangError Integer, String), [MiniLangValue])]
exampleSomewhere :: [((Either MiniLangError Integer, String), [MiniLangValue])]
exampleSomewhere = LtlAST
  MiniLangMod
  '[MonadMiniLangEffect, MonadErrorEffect MiniLangError]
  Integer
-> [((Either MiniLangError Integer, String), [MiniLangValue])]
forall a.
LtlAST
  MiniLangMod
  '[MonadMiniLangEffect, MonadErrorEffect MiniLangError]
  a
-> [((Either MiniLangError a, String), [MiniLangValue])]
interpretAndRunMiniLang (LtlAST
   MiniLangMod
   '[MonadMiniLangEffect, MonadErrorEffect MiniLangError]
   Integer
 -> [((Either MiniLangError Integer, String), [MiniLangValue])])
-> LtlAST
     MiniLangMod
     '[MonadMiniLangEffect, MonadErrorEffect MiniLangError]
     Integer
-> [((Either MiniLangError Integer, String), [MiniLangValue])]
forall a b. (a -> b) -> a -> b
$
  Ltl MiniLangMod
-> LtlAST
     MiniLangMod
     '[MonadMiniLangEffect, MonadErrorEffect MiniLangError]
     Integer
-> LtlAST
     MiniLangMod
     '[MonadMiniLangEffect, MonadErrorEffect MiniLangError]
     Integer
forall mod (ops :: [(* -> *) -> * -> *]) a.
Ltl mod -> LtlAST mod ops a -> LtlAST mod ops a
modifyLtl (MiniLangMod -> Ltl MiniLangMod
forall a. a -> Ltl a
somewhere MiniLangMod
flipIntegers) (LtlAST
   MiniLangMod
   '[MonadMiniLangEffect, MonadErrorEffect MiniLangError]
   Integer
 -> LtlAST
      MiniLangMod
      '[MonadMiniLangEffect, MonadErrorEffect MiniLangError]
      Integer)
-> LtlAST
     MiniLangMod
     '[MonadMiniLangEffect, MonadErrorEffect MiniLangError]
     Integer
-> LtlAST
     MiniLangMod
     '[MonadMiniLangEffect, MonadErrorEffect MiniLangError]
     Integer
forall a b. (a -> b) -> a -> b
$ do
    String
-> Fixpoint
     Freer
     (JoinedEffects
        '[LtlEffect MiniLangMod, MonadMiniLangEffect,
          MonadErrorEffect MiniLangError])
     ()
forall (m :: * -> *). MonadMiniLang m => String -> m ()
echo String
"Pushing 42"
    Integer
-> Fixpoint
     Freer
     (JoinedEffects
        '[LtlEffect MiniLangMod, MonadMiniLangEffect,
          MonadErrorEffect MiniLangError])
     ()
forall (m :: * -> *). MonadMiniLang m => Integer -> m ()
pushInteger Integer
42
    LtlAST
  MiniLangMod
  '[MonadMiniLangEffect, MonadErrorEffect MiniLangError]
  Integer
forall (m :: * -> *).
(MonadError MiniLangError m, MonadMiniLang m) =>
m Integer
popInteger

-- $doc
-- >>> exampleSomewhere
-- [((Right -42,"Pushing 42"),[]),
--  ((Right -42,"Pushing 42"),[])]

-- $doc
-- Let's look at a more interesting example with a higher-order
-- operation, 'if_'.

exampleIf :: MiniLangMod -> Bool -> [((Either MiniLangError (), String), [MiniLangValue])]
exampleIf :: MiniLangMod
-> Bool -> [((Either MiniLangError (), String), [MiniLangValue])]
exampleIf MiniLangMod
modif Bool
intOrBool = Fixpoint
  Freer
  (JoinedEffects
     '[LtlEffect MiniLangMod, MonadMiniLangEffect,
       MonadErrorEffect MiniLangError])
  ()
-> [((Either MiniLangError (), String), [MiniLangValue])]
forall a.
LtlAST
  MiniLangMod
  '[MonadMiniLangEffect, MonadErrorEffect MiniLangError]
  a
-> [((Either MiniLangError a, String), [MiniLangValue])]
interpretAndRunMiniLang (Fixpoint
   Freer
   (JoinedEffects
      '[LtlEffect MiniLangMod, MonadMiniLangEffect,
        MonadErrorEffect MiniLangError])
   ()
 -> [((Either MiniLangError (), String), [MiniLangValue])])
-> Fixpoint
     Freer
     (JoinedEffects
        '[LtlEffect MiniLangMod, MonadMiniLangEffect,
          MonadErrorEffect MiniLangError])
     ()
-> [((Either MiniLangError (), String), [MiniLangValue])]
forall a b. (a -> b) -> a -> b
$
  Ltl MiniLangMod
-> Fixpoint
     Freer
     (JoinedEffects
        '[LtlEffect MiniLangMod, MonadMiniLangEffect,
          MonadErrorEffect MiniLangError])
     ()
-> Fixpoint
     Freer
     (JoinedEffects
        '[LtlEffect MiniLangMod, MonadMiniLangEffect,
          MonadErrorEffect MiniLangError])
     ()
forall mod (ops :: [(* -> *) -> * -> *]) a.
Ltl mod -> LtlAST mod ops a -> LtlAST mod ops a
modifyLtl (MiniLangMod -> Ltl MiniLangMod
forall a. a -> Ltl a
somewhere MiniLangMod
modif) (Fixpoint
   Freer
   (JoinedEffects
      '[LtlEffect MiniLangMod, MonadMiniLangEffect,
        MonadErrorEffect MiniLangError])
   ()
 -> Fixpoint
      Freer
      (JoinedEffects
         '[LtlEffect MiniLangMod, MonadMiniLangEffect,
           MonadErrorEffect MiniLangError])
      ())
-> Fixpoint
     Freer
     (JoinedEffects
        '[LtlEffect MiniLangMod, MonadMiniLangEffect,
          MonadErrorEffect MiniLangError])
     ()
-> Fixpoint
     Freer
     (JoinedEffects
        '[LtlEffect MiniLangMod, MonadMiniLangEffect,
          MonadErrorEffect MiniLangError])
     ()
forall a b. (a -> b) -> a -> b
$ do
    Bool
-> Fixpoint
     Freer
     (JoinedEffects
        '[LtlEffect MiniLangMod, MonadMiniLangEffect,
          MonadErrorEffect MiniLangError])
     ()
forall (m :: * -> *). MonadMiniLang m => Bool -> m ()
pushBoolean Bool
intOrBool
    Fixpoint
  Freer
  (JoinedEffects
     '[LtlEffect MiniLangMod, MonadMiniLangEffect,
       MonadErrorEffect MiniLangError])
  ()
-> Fixpoint
     Freer
     (JoinedEffects
        '[LtlEffect MiniLangMod, MonadMiniLangEffect,
          MonadErrorEffect MiniLangError])
     ()
-> Fixpoint
     Freer
     (JoinedEffects
        '[LtlEffect MiniLangMod, MonadMiniLangEffect,
          MonadErrorEffect MiniLangError])
     ()
forall a.
Fixpoint
  Freer
  (JoinedEffects
     '[LtlEffect MiniLangMod, MonadMiniLangEffect,
       MonadErrorEffect MiniLangError])
  a
-> Fixpoint
     Freer
     (JoinedEffects
        '[LtlEffect MiniLangMod, MonadMiniLangEffect,
          MonadErrorEffect MiniLangError])
     a
-> Fixpoint
     Freer
     (JoinedEffects
        '[LtlEffect MiniLangMod, MonadMiniLangEffect,
          MonadErrorEffect MiniLangError])
     a
forall (m :: * -> *) a. MonadMiniLang m => m a -> m a -> m a
if_
      (Integer
-> Fixpoint
     Freer
     (JoinedEffects
        '[LtlEffect MiniLangMod, MonadMiniLangEffect,
          MonadErrorEffect MiniLangError])
     ()
forall (m :: * -> *). MonadMiniLang m => Integer -> m ()
pushInteger Integer
42)
      (Bool
-> Fixpoint
     Freer
     (JoinedEffects
        '[LtlEffect MiniLangMod, MonadMiniLangEffect,
          MonadErrorEffect MiniLangError])
     ()
forall (m :: * -> *). MonadMiniLang m => Bool -> m ()
pushBoolean Bool
True)

-- $doc
-- >>> exampleIf flipIntegers True
-- [((Right (),""),[MiniLangInteger (-42)]]
--
-- >>> exampleIf flipIntegers False
-- []
--
-- The two runs above show that we only modify the \"else\" branch of
-- the 'if_' when it is executed: in the second run, no modification
-- is applied, because no push or pop involving an integer happens.
--
-- The next two runs are more involved, because we modify booleans,
-- which are intrinsically very relevant for 'if_'s. Let's mark the
-- places that are potentially modified:
--
-- > do
-- >   pushBoolean intOrBool    -- (1) because we push a boolean
-- >   if_                      -- (2) because 'if_' pushes a boolean
-- >     (pushInteger 42)
-- >     (pushBoolean True)     -- (3) because we push a boolean
--
-- The modality 'somewhere' requires that we either modify the
-- 'pushBoolean' at (1), or modify some later 'push' or 'pop' of a
-- boolean. If 'intOrBool' is initially 'True', that means we have two
-- options:
--
-- - modify at (1), which means that the we'll 'pop' a 'False' at
--   (2). In this scenario, we'll execute the 'else' branch, which
--   will 'push' a 'True' at (3).
--
-- - modify at (2), which also means that we'll 'pop' a 'False' at
--   (2). We'll consequently also execute the execute the 'else'
--   branch, which will 'push' a 'True' at (3).
--
-- Note that we'll never apply a modification at (3), because in both
-- cases, the requirements of 'somewhere' are already satisfied.
--
-- >>> exampleIf flipBools True
-- [((Right (), ""), [MiniLangBoolean True]),
--  ((Right (), ""), [MiniLangBoolean True])]
--
-- For our last run, let's look at the case where 'intOrBool' is
-- 'False'. In that case, the following three scenarios are possible:
--
-- - modify at (1), which means that we'll 'pop' a 'True' at (2). So,
--   we'll execute the 'then' branch, which will 'push' a '42'.
--
-- - modify at (2), which means that we'll 'pop' a 'True' at (2). So,
--   we'll execute the 'then' branch, which will 'push' a '42'.
--
-- - If we don't modify at (1) or (2), we'll execute the 'else'
--   branch, which will 'push' a 'False' (modified from 'True') at
--   (3).
--
-- >>> exampleIf flipBools False
-- [((Right (),""),[MiniLangInteger 42]),
--  ((Right (),""),[MiniLangInteger 42]),
--  ((Right (),""),[MiniLangBoolean False])]

-- $doc
-- Finally, for a more testing-flavoured example, we can check the
-- property that the programs only interact with the stack through the
-- 'push' and 'pop' operations, by applying @everywhere
-- flipBoth@. Effectively, this modification means that the entries on
-- the stack will always be the inverse of their "actual" values, and
-- that the meaning of 'push' and 'pop' also contains reversing this
-- polarity.

exampleFlipFibonacci :: Bool
exampleFlipFibonacci :: Bool
exampleFlipFibonacci =
  (Integer -> Bool) -> [Integer] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all
    ( \Integer
n ->
        (((Either MiniLangError Integer, String), [MiniLangValue])
 -> Either MiniLangError Integer)
-> [((Either MiniLangError Integer, String), [MiniLangValue])]
-> [Either MiniLangError Integer]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap
          ((Either MiniLangError Integer, String), [MiniLangValue])
-> Either MiniLangError Integer
getResult
          ( LtlAST
  MiniLangMod
  '[MonadMiniLangEffect, MonadErrorEffect MiniLangError]
  Integer
-> [((Either MiniLangError Integer, String), [MiniLangValue])]
forall a.
LtlAST
  MiniLangMod
  '[MonadMiniLangEffect, MonadErrorEffect MiniLangError]
  a
-> [((Either MiniLangError a, String), [MiniLangValue])]
interpretAndRunMiniLang
              (Ltl MiniLangMod
-> LtlAST
     MiniLangMod
     '[MonadMiniLangEffect, MonadErrorEffect MiniLangError]
     Integer
-> LtlAST
     MiniLangMod
     '[MonadMiniLangEffect, MonadErrorEffect MiniLangError]
     Integer
forall mod (ops :: [(* -> *) -> * -> *]) a.
Ltl mod -> LtlAST mod ops a -> LtlAST mod ops a
modifyLtl (MiniLangMod -> Ltl MiniLangMod
forall a. a -> Ltl a
everywhere MiniLangMod
flipBoth) (Integer
-> LtlAST
     MiniLangMod
     '[MonadMiniLangEffect, MonadErrorEffect MiniLangError]
     Integer
forall (m :: * -> *).
(MonadError MiniLangError m, MonadMiniLang m) =>
Integer -> m Integer
fibonacciExample Integer
n))
          )
          [Either MiniLangError Integer]
-> [Either MiniLangError Integer] -> Bool
forall a. Eq a => a -> a -> Bool
== [((Either MiniLangError Integer, String), [MiniLangValue])
-> Either MiniLangError Integer
getResult (((Either MiniLangError Integer, String), [MiniLangValue])
 -> Either MiniLangError Integer)
-> (Identity
      ((Either MiniLangError Integer, String), [MiniLangValue])
    -> ((Either MiniLangError Integer, String), [MiniLangValue]))
-> Identity
     ((Either MiniLangError Integer, String), [MiniLangValue])
-> Either MiniLangError Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity ((Either MiniLangError Integer, String), [MiniLangValue])
-> ((Either MiniLangError Integer, String), [MiniLangValue])
forall a. Identity a -> a
runIdentity (Identity ((Either MiniLangError Integer, String), [MiniLangValue])
 -> Either MiniLangError Integer)
-> Identity
     ((Either MiniLangError Integer, String), [MiniLangValue])
-> Either MiniLangError Integer
forall a b. (a -> b) -> a -> b
$ MiniLangT Identity Integer
-> Identity
     ((Either MiniLangError Integer, String), [MiniLangValue])
forall (m :: * -> *) a.
Functor m =>
MiniLangT m a
-> m ((Either MiniLangError a, String), [MiniLangValue])
runMiniLangT (Integer -> MiniLangT Identity Integer
forall (m :: * -> *).
(MonadError MiniLangError m, MonadMiniLang m) =>
Integer -> m Integer
fibonacciExample Integer
n)]
    )
    [Integer
0 .. Integer
10]
  where
    getResult :: ((Either MiniLangError Integer, String), [MiniLangValue]) -> Either MiniLangError Integer
    getResult :: ((Either MiniLangError Integer, String), [MiniLangValue])
-> Either MiniLangError Integer
getResult = (Either MiniLangError Integer, String)
-> Either MiniLangError Integer
forall a b. (a, b) -> a
fst ((Either MiniLangError Integer, String)
 -> Either MiniLangError Integer)
-> (((Either MiniLangError Integer, String), [MiniLangValue])
    -> (Either MiniLangError Integer, String))
-> ((Either MiniLangError Integer, String), [MiniLangValue])
-> Either MiniLangError Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Either MiniLangError Integer, String), [MiniLangValue])
-> (Either MiniLangError Integer, String)
forall a b. (a, b) -> a
fst

-- $doc
-- >>> exampleFlipFibonacci
-- True