{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Test.IOTasks.Interpreter (interpret) where

import Prelude hiding (readLn,putStrLn)

import Control.Monad.State

import qualified Data.Set as Set

import Test.IOTasks.Internal.Specification
import Test.IOTasks.MonadTeletype as MTT
import Test.IOTasks.Internal.Term
import Test.IOTasks.Var (someVar)
import Test.IOTasks.ValueSet
import Test.IOTasks.Trace
import Test.IOTasks.OutputPattern
import Test.IOTasks.ValueMap

-- | Interpret a specification as a program in 'Monad' m.
--
--   Returns a list containing all possible ways of resolving optionality, e.g.
--
-- >>> length (interpret $ writeOptionalOutput [x,y])
-- 3
interpret :: MonadTeletype m => Specification -> [m ()]
interpret :: forall (m :: * -> *). MonadTeletype m => Specification -> [m ()]
interpret Specification
s = do
  Specification
collapsed <- Specification -> [Specification]
collapseChoice Specification
s
  m () -> [m ()]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (m () -> [m ()]) -> m () -> [m ()]
forall a b. (a -> b) -> a -> b
$ (StateT ValueMap m () -> ValueMap -> m ())
-> ValueMap -> StateT ValueMap m () -> m ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT ValueMap m () -> ValueMap -> m ()
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT ([SomeVar] -> ValueMap
emptyValueMap [] :: ValueMap) (StateT ValueMap m () -> m ()) -> StateT ValueMap m () -> m ()
forall a b. (a -> b) -> a -> b
$
    (forall v.
 (Typeable v, Read v, Show v) =>
 ()
 -> Var v
 -> ValueSet v
 -> InputMode
 -> RecStruct
      (SomeVar, String -> Value, ValueMap -> Value -> Bool, InputMode)
      (StateT ValueMap m () -> StateT ValueMap m ())
      ()
      (StateT ValueMap m ()))
-> (RecStruct
      (SomeVar, String -> Value, ValueMap -> Value -> Bool, InputMode)
      ()
      (StateT ValueMap m ())
      (StateT ValueMap m ())
    -> StateT ValueMap m ())
-> (forall (k :: PatternKind).
    ()
    -> OptFlag
    -> Set (OutputPattern k)
    -> StateT ValueMap m ()
    -> StateT ValueMap m ())
-> (()
    -> Term 'Transparent Bool
    -> StateT ValueMap m ()
    -> StateT ValueMap m ()
    -> StateT ValueMap m ())
-> (Action -> StateT ValueMap m () -> StateT ValueMap m ())
-> (StateT ValueMap m () -> StateT ValueMap m ())
-> StateT ValueMap m ()
-> ()
-> Specification
-> StateT ValueMap m ()
forall st p a.
(forall v.
 (Typeable v, Read v, Show v) =>
 st
 -> Var v -> ValueSet v -> InputMode -> RecStruct p (a -> a) st a)
-> (RecStruct p () a a -> a)
-> (forall (k :: PatternKind).
    st -> OptFlag -> Set (OutputPattern k) -> a -> a)
-> (st -> Term 'Transparent Bool -> a -> a -> a)
-> (Action -> a -> a)
-> (a -> a)
-> a
-> st
-> Specification
-> a
sem
      -- (\() x (vs :: ValueSet v) m -> RecSub (someVar x,wrapValue . readValue @v, \var m -> (containsValue var m vs . unwrapValue),m) id ())
      (\() Var v
x (ValueSet v
vs :: ValueSet v) InputMode
m -> (SomeVar, String -> Value, ValueMap -> Value -> Bool, InputMode)
-> (StateT ValueMap m () -> StateT ValueMap m ())
-> ()
-> RecStruct
     (SomeVar, String -> Value, ValueMap -> Value -> Bool, InputMode)
     (StateT ValueMap m () -> StateT ValueMap m ())
     ()
     (StateT ValueMap m ())
forall p x a r. p -> x -> a -> RecStruct p x a r
RecSub (Var v -> SomeVar
forall a. Typeable a => Var a -> SomeVar
someVar Var v
x,v -> Value
forall a. Typeable a => a -> Value
wrapValue (v -> Value) -> (String -> v) -> String -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var v -> String -> v
forall a. Var a -> String -> a
readValue Var v
x, \ValueMap
vMap -> Var v -> ValueMap -> ValueSet v -> v -> Bool
forall a. Var a -> ValueMap -> ValueSet a -> a -> Bool
containsValue Var v
x ValueMap
vMap ValueSet v
vs (v -> Bool) -> (Value -> v) -> Value -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var v -> Value -> v
forall a. Var a -> Value -> a
unwrapValue Var v
x,InputMode
m) StateT ValueMap m () -> StateT ValueMap m ()
forall a. a -> a
id ())
      (\case
        RecSub (SomeVar
x,String -> Value
readF,ValueMap -> Value -> Bool
_,InputMode
AssumeValid) () StateT ValueMap m ()
p' -> do
          Value
v <- m Value -> StateT ValueMap m Value
forall (m :: * -> *) a. Monad m => m a -> StateT ValueMap m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (String -> Value
readF (String -> Value) -> m String -> m Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m String
forall (m :: * -> *). MonadTeletype m => m String
MTT.getLine)
          (ValueMap -> ValueMap) -> StateT ValueMap m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((ValueMap -> ValueMap) -> StateT ValueMap m ())
-> (ValueMap -> ValueMap) -> StateT ValueMap m ()
forall a b. (a -> b) -> a -> b
$ Value -> SomeVar -> ValueMap -> ValueMap
insertValue Value
v SomeVar
x
          StateT ValueMap m ()
p'
        RecSub (SomeVar
x,String -> Value
readF,ValueMap -> Value -> Bool
vsContains,InputMode
ElseAbort) () StateT ValueMap m ()
p' -> do
          Value
v <- m Value -> StateT ValueMap m Value
forall (m :: * -> *) a. Monad m => m a -> StateT ValueMap m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (String -> Value
readF (String -> Value) -> m String -> m Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m String
forall (m :: * -> *). MonadTeletype m => m String
MTT.getLine)
          ValueMap
vMap <- StateT ValueMap m ValueMap
forall s (m :: * -> *). MonadState s m => m s
get
          if ValueMap -> Value -> Bool
vsContains ValueMap
vMap Value
v
            then do
              (ValueMap -> ValueMap) -> StateT ValueMap m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((ValueMap -> ValueMap) -> StateT ValueMap m ())
-> (ValueMap -> ValueMap) -> StateT ValueMap m ()
forall a b. (a -> b) -> a -> b
$ Value -> SomeVar -> ValueMap -> ValueMap
insertValue Value
v SomeVar
x
              StateT ValueMap m ()
p'
            else m () -> StateT ValueMap m ()
forall (m :: * -> *) a. Monad m => m a -> StateT ValueMap m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> StateT ValueMap m ()) -> m () -> StateT ValueMap m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
forall (m :: * -> *). MonadTeletype m => String -> m ()
MTT.putStrLn String
"abort: invalid input value"
        RecSub (SomeVar
x,String -> Value
readF,ValueMap -> Value -> Bool
vsContains,InputMode
UntilValid) () StateT ValueMap m ()
p' -> do
          let readLoop :: StateT ValueMap m Value
readLoop = do
                Value
v <- m Value -> StateT ValueMap m Value
forall (m :: * -> *) a. Monad m => m a -> StateT ValueMap m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (String -> Value
readF (String -> Value) -> m String -> m Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m String
forall (m :: * -> *). MonadTeletype m => m String
MTT.getLine)
                ValueMap
vMap <- StateT ValueMap m ValueMap
forall s (m :: * -> *). MonadState s m => m s
get
                if ValueMap -> Value -> Bool
vsContains ValueMap
vMap Value
v then Value -> StateT ValueMap m Value
forall a. a -> StateT ValueMap m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value
v else m () -> StateT ValueMap m ()
forall (m :: * -> *) a. Monad m => m a -> StateT ValueMap m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (String -> m ()
forall (m :: * -> *). MonadTeletype m => String -> m ()
putStrLn String
"invalid value, try again") StateT ValueMap m ()
-> StateT ValueMap m Value -> StateT ValueMap m Value
forall a b.
StateT ValueMap m a -> StateT ValueMap m b -> StateT ValueMap m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT ValueMap m Value
readLoop
          Value
v <- StateT ValueMap m Value
readLoop
          (ValueMap -> ValueMap) -> StateT ValueMap m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((ValueMap -> ValueMap) -> StateT ValueMap m ())
-> (ValueMap -> ValueMap) -> StateT ValueMap m ()
forall a b. (a -> b) -> a -> b
$ Value -> SomeVar -> ValueMap -> ValueMap
insertValue Value
v SomeVar
x
          StateT ValueMap m ()
p'
        NoRec{} -> String -> StateT ValueMap m ()
forall a. HasCallStack => String -> a
error String
"interpret: impossible"
        RecSame{} -> String -> StateT ValueMap m ()
forall a. HasCallStack => String -> a
error String
"interpret: impossible"
        RecBoth{} -> String -> StateT ValueMap m ()
forall a. HasCallStack => String -> a
error String
"interpret: impossible")
      (\()
_ OptFlag
opt Set (OutputPattern k)
ts StateT ValueMap m ()
p' -> case OptFlag
opt of
        OptFlag
Mandatory -> do
          if Set (OutputPattern k) -> Int
forall a. Set a -> Int
Set.size Set (OutputPattern k)
ts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1
            then do
              ValueMap
e <- StateT ValueMap m ValueMap
forall s (m :: * -> *). MonadState s m => m s
get
              m () -> StateT ValueMap m ()
forall (m :: * -> *) a. Monad m => m a -> StateT ValueMap m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> StateT ValueMap m ()) -> m () -> StateT ValueMap m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
forall (m :: * -> *). MonadTeletype m => String -> m ()
putStrLn (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ OutputPattern 'TraceP -> String
forall (k :: PatternKind). OutputPattern k -> String
showPattern (OutputPattern 'TraceP -> String)
-> OutputPattern 'TraceP -> String
forall a b. (a -> b) -> a -> b
$ (OverflowWarning, OutputPattern 'TraceP) -> OutputPattern 'TraceP
forall a b. (a, b) -> b
snd ((OverflowWarning, OutputPattern 'TraceP) -> OutputPattern 'TraceP)
-> (OverflowWarning, OutputPattern 'TraceP)
-> OutputPattern 'TraceP
forall a b. (a -> b) -> a -> b
$ ValueMap
-> OutputPattern k -> (OverflowWarning, OutputPattern 'TraceP)
forall (k :: PatternKind).
ValueMap
-> OutputPattern k -> (OverflowWarning, OutputPattern 'TraceP)
evalPattern ValueMap
e (Int -> Set (OutputPattern k) -> OutputPattern k
forall a. Int -> Set a -> a
Set.elemAt Int
0 Set (OutputPattern k)
ts)
              StateT ValueMap m ()
p'
            else String -> StateT ValueMap m ()
forall a. HasCallStack => String -> a
error String
"interpret: impossible (due to collapseChoice)"
        OptFlag
Optional -> String -> StateT ValueMap m ()
forall a. HasCallStack => String -> a
error String
"interpret: impossible (due to collapseChoice)"
      )
      (\()
_ Term 'Transparent Bool
cond StateT ValueMap m ()
pl StateT ValueMap m ()
pr -> do
        ValueMap
e <- StateT ValueMap m ValueMap
forall s (m :: * -> *). MonadState s m => m s
get
        if (OverflowWarning, Bool) -> Bool
forall a b. (a, b) -> b
snd ((OverflowWarning, Bool) -> Bool)
-> (OverflowWarning, Bool) -> Bool
forall a b. (a -> b) -> a -> b
$ ValueMap -> Term 'Transparent Bool -> (OverflowWarning, Bool)
forall a (k :: TermKind).
Typeable a =>
ValueMap -> Term k a -> (OverflowWarning, a)
oEval ValueMap
e Term 'Transparent Bool
cond
          then StateT ValueMap m ()
pl
          else StateT ValueMap m ()
pr
      )
      ((StateT ValueMap m () -> StateT ValueMap m ())
-> Action -> StateT ValueMap m () -> StateT ValueMap m ()
forall a b. a -> b -> a
const StateT ValueMap m () -> StateT ValueMap m ()
forall a. a -> a
id)
      StateT ValueMap m () -> StateT ValueMap m ()
forall a. a -> a
id
      (() -> StateT ValueMap m ()
forall a. a -> StateT ValueMap m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
      ()
      Specification
collapsed

collapseChoice :: Specification -> [Specification]
collapseChoice :: Specification -> [Specification]
collapseChoice (ReadInput Var a
x ValueSet a
vs InputMode
m Specification
s') = Var a -> ValueSet a -> InputMode -> Specification -> Specification
forall a.
(Typeable a, Read a, Show a) =>
Var a -> ValueSet a -> InputMode -> Specification -> Specification
ReadInput Var a
x ValueSet a
vs InputMode
m (Specification -> Specification)
-> [Specification] -> [Specification]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Specification -> [Specification]
collapseChoice Specification
s'
collapseChoice (WriteOutput OptFlag
o Set (OutputPattern k)
ts Specification
s') = do
  OptFlag -> Set (OutputPattern k) -> Specification -> Specification
forall (k :: PatternKind).
OptFlag -> Set (OutputPattern k) -> Specification -> Specification
WriteOutput OptFlag
Mandatory (Set (OutputPattern k) -> Specification -> Specification)
-> [Set (OutputPattern k)] -> [Specification -> Specification]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (OutputPattern k -> Set (OutputPattern k)
forall a. a -> Set a
Set.singleton (OutputPattern k -> Set (OutputPattern k))
-> [OutputPattern k] -> [Set (OutputPattern k)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set (OutputPattern k) -> [OutputPattern k]
forall a. Set a -> [a]
Set.toList Set (OutputPattern k)
ts) [Specification -> Specification]
-> [Specification] -> [Specification]
forall a b. [a -> b] -> [a] -> [b]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Specification -> [Specification]
collapseChoice Specification
s' [Specification] -> [Specification] -> [Specification]
forall a. [a] -> [a] -> [a]
++ if OptFlag
o OptFlag -> OptFlag -> Bool
forall a. Eq a => a -> a -> Bool
== OptFlag
Optional then Specification -> [Specification]
collapseChoice Specification
s' else []
collapseChoice (Branch Term 'Transparent Bool
p Specification
l Specification
r Specification
s') = Term 'Transparent Bool
-> Specification -> Specification -> Specification -> Specification
Branch Term 'Transparent Bool
p (Specification -> Specification -> Specification -> Specification)
-> [Specification]
-> [Specification -> Specification -> Specification]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Specification -> [Specification]
collapseChoice Specification
l [Specification -> Specification -> Specification]
-> [Specification] -> [Specification -> Specification]
forall a b. [a -> b] -> [a] -> [b]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Specification -> [Specification]
collapseChoice Specification
r [Specification -> Specification]
-> [Specification] -> [Specification]
forall a b. [a -> b] -> [a] -> [b]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Specification -> [Specification]
collapseChoice Specification
s'
collapseChoice (TillE Specification
bdy Specification
s') = Specification -> Specification -> Specification
TillE (Specification -> Specification -> Specification)
-> [Specification] -> [Specification -> Specification]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Specification -> [Specification]
collapseChoice Specification
bdy [Specification -> Specification]
-> [Specification] -> [Specification]
forall a b. [a -> b] -> [a] -> [b]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Specification -> [Specification]
collapseChoice Specification
s'
collapseChoice Specification
Nop = Specification -> [Specification]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure Specification
Nop
collapseChoice Specification
E = Specification -> [Specification]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure Specification
E