{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeOperators #-}
module Test.IOTasks.Internal.Specification (
Specification(..),
readInput, writeOutput, writeOptionalOutput, anyOptionalOutput,
branch, tillExit, exit, while, whileNot, repeatUntil, doWhile, nop,
runSpecification, runSpecification', AddLinebreaks,
readVars, hasIteration,
pPrintSpecification,
InputMode(..),
sem, semM, RecStruct(..),
accept, Action(..),
LoopBody(..),
) where
import Test.IOTasks.ValueSet
import Test.IOTasks.Internal.Term
import Test.IOTasks.Var (Var (..), SomeVar, varname, someVar)
import Test.IOTasks.Trace
import Test.IOTasks.Internal.OutputPattern hiding (text)
import Test.IOTasks.Overflow
import Test.IOTasks.ValueMap
import Test.IOTasks.Internal.SpecificationGenerator
import Data.Set (Set)
import qualified Data.Set as Set
import Data.List (nub,intersperse, intersect)
import Data.Functor.Identity (runIdentity,Identity(..))
import Data.Bifunctor (first, second)
import Data.Either (isLeft, isRight, lefts)
import Type.Reflection (Typeable)
import Test.QuickCheck (Arbitrary(..))
import Text.PrettyPrint hiding ((<>))
import Data.GADT.Compare
import Data.Functor.Classes (Ord1(liftCompare))
data Specification where
ReadInput :: (Typeable a,Read a,Show a) => Var a -> ValueSet a -> InputMode -> Specification -> Specification
WriteOutput :: OptFlag -> Set (OutputPattern k) -> Specification -> Specification
Branch :: Term 'Transparent Bool -> Specification -> Specification -> Specification -> Specification
TillE :: Specification -> Specification -> Specification
E :: Specification
Nop :: Specification
data InputMode = AssumeValid | UntilValid | ElseAbort deriving (InputMode -> InputMode -> Bool
(InputMode -> InputMode -> Bool)
-> (InputMode -> InputMode -> Bool) -> Eq InputMode
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: InputMode -> InputMode -> Bool
== :: InputMode -> InputMode -> Bool
$c/= :: InputMode -> InputMode -> Bool
/= :: InputMode -> InputMode -> Bool
Eq,Eq InputMode
Eq InputMode =>
(InputMode -> InputMode -> Ordering)
-> (InputMode -> InputMode -> Bool)
-> (InputMode -> InputMode -> Bool)
-> (InputMode -> InputMode -> Bool)
-> (InputMode -> InputMode -> Bool)
-> (InputMode -> InputMode -> InputMode)
-> (InputMode -> InputMode -> InputMode)
-> Ord InputMode
InputMode -> InputMode -> Bool
InputMode -> InputMode -> Ordering
InputMode -> InputMode -> InputMode
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: InputMode -> InputMode -> Ordering
compare :: InputMode -> InputMode -> Ordering
$c< :: InputMode -> InputMode -> Bool
< :: InputMode -> InputMode -> Bool
$c<= :: InputMode -> InputMode -> Bool
<= :: InputMode -> InputMode -> Bool
$c> :: InputMode -> InputMode -> Bool
> :: InputMode -> InputMode -> Bool
$c>= :: InputMode -> InputMode -> Bool
>= :: InputMode -> InputMode -> Bool
$cmax :: InputMode -> InputMode -> InputMode
max :: InputMode -> InputMode -> InputMode
$cmin :: InputMode -> InputMode -> InputMode
min :: InputMode -> InputMode -> InputMode
Ord,Int -> InputMode -> ShowS
[InputMode] -> ShowS
InputMode -> String
(Int -> InputMode -> ShowS)
-> (InputMode -> String)
-> ([InputMode] -> ShowS)
-> Show InputMode
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> InputMode -> ShowS
showsPrec :: Int -> InputMode -> ShowS
$cshow :: InputMode -> String
show :: InputMode -> String
$cshowList :: [InputMode] -> ShowS
showList :: [InputMode] -> ShowS
Show)
instance Eq Specification where
Specification
x == :: Specification -> Specification -> Bool
== Specification
y = Specification -> Specification -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Specification
x Specification
y Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ
instance Ord Specification where
compare :: Specification -> Specification -> Ordering
compare Specification
Nop Specification
Nop = Ordering
EQ
compare Specification
Nop Specification
_ = Ordering
LT
compare Specification
_ Specification
Nop = Ordering
GT
compare Specification
E Specification
E = Ordering
EQ
compare Specification
E Specification
_ = Ordering
LT
compare Specification
_ Specification
E = Ordering
GT
compare (TillE Specification
bx Specification
x) (TillE Specification
by Specification
y) = (Specification, Specification)
-> (Specification, Specification) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Specification
bx,Specification
x) (Specification
by,Specification
y)
compare TillE{} Specification
_ = Ordering
LT
compare Specification
_ TillE{} = Ordering
GT
compare (Branch Term 'Transparent Bool
cx Specification
tx Specification
ex Specification
sx) (Branch Term 'Transparent Bool
cy Specification
ty Specification
ey Specification
sy) = (Term 'Transparent Bool, Specification, Specification,
Specification)
-> (Term 'Transparent Bool, Specification, Specification,
Specification)
-> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Term 'Transparent Bool
cx,Specification
tx,Specification
ex,Specification
sx) (Term 'Transparent Bool
cy,Specification
ty,Specification
ey,Specification
sy)
compare Branch{} Specification
_ = Ordering
LT
compare Specification
_ Branch{} = Ordering
GT
compare (WriteOutput OptFlag
ox Set (OutputPattern k)
px Specification
sx) (WriteOutput OptFlag
oy Set (OutputPattern k)
py Specification
sy) =
case (OutputPattern k -> OutputPattern k -> Ordering)
-> Set (OutputPattern k) -> Set (OutputPattern k) -> Ordering
forall a b. (a -> b -> Ordering) -> Set a -> Set b -> Ordering
forall (f :: * -> *) a b.
Ord1 f =>
(a -> b -> Ordering) -> f a -> f b -> Ordering
liftCompare (\OutputPattern k
x OutputPattern k
y -> OutputPattern k -> OutputPattern 'SpecificationP
forall (k :: PatternKind).
OutputPattern k -> OutputPattern 'SpecificationP
convert OutputPattern k
x OutputPattern 'SpecificationP
-> OutputPattern 'SpecificationP -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` OutputPattern k -> OutputPattern 'SpecificationP
forall (k :: PatternKind).
OutputPattern k -> OutputPattern 'SpecificationP
convert OutputPattern k
y) Set (OutputPattern k)
px Set (OutputPattern k)
py of
Ordering
LT -> Ordering
LT
Ordering
EQ -> (OptFlag, Specification) -> (OptFlag, Specification) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (OptFlag
ox,Specification
sx) (OptFlag
oy,Specification
sy)
Ordering
GT -> Ordering
GT
compare WriteOutput{} Specification
_ = Ordering
LT
compare Specification
_ WriteOutput{} = Ordering
GT
compare (ReadInput Var a
x ValueSet a
xs InputMode
mx Specification
sx) (ReadInput Var a
y ValueSet a
ys InputMode
my Specification
sy) =
case Var a -> Var a -> GOrdering a a
forall a b. Var a -> Var b -> GOrdering a b
forall k (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
gcompare Var a
x Var a
y of
GOrdering a a
GLT -> Ordering
LT
GOrdering a a
GEQ -> (ValueSet a, InputMode, Specification)
-> (ValueSet a, InputMode, Specification) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (ValueSet a
xs,InputMode
mx,Specification
sx) (ValueSet a
ValueSet a
ys,InputMode
my,Specification
sy)
GOrdering a a
GGT -> Ordering
GT
instance Semigroup Specification where
Specification
s <> :: Specification -> Specification -> Specification
<> Specification
Nop = Specification
s
Specification
Nop <> Specification
s = Specification
s
(ReadInput Var a
x ValueSet a
vs InputMode
m Specification
s) <> Specification
s' = Var a -> ValueSet a -> InputMode -> Specification -> Specification
forall k.
(Typeable k, Read k, Show k) =>
Var k -> ValueSet k -> InputMode -> Specification -> Specification
ReadInput Var a
x ValueSet a
vs InputMode
m (Specification -> Specification) -> Specification -> Specification
forall a b. (a -> b) -> a -> b
$ Specification
s Specification -> Specification -> Specification
forall a. Semigroup a => a -> a -> a
<> Specification
s'
(WriteOutput OptFlag
o Set (OutputPattern k)
t Specification
s) <> Specification
s' = OptFlag -> Set (OutputPattern k) -> Specification -> Specification
forall (k :: PatternKind).
OptFlag -> Set (OutputPattern k) -> Specification -> Specification
WriteOutput OptFlag
o Set (OutputPattern k)
t (Specification -> Specification) -> Specification -> Specification
forall a b. (a -> b) -> a -> b
$ Specification
s Specification -> Specification -> Specification
forall a. Semigroup a => a -> a -> a
<> Specification
s'
(Branch Term 'Transparent Bool
c Specification
l Specification
r Specification
s) <> Specification
s' = Term 'Transparent Bool
-> Specification -> Specification -> Specification -> Specification
Branch Term 'Transparent Bool
c Specification
l Specification
r (Specification -> Specification) -> Specification -> Specification
forall a b. (a -> b) -> a -> b
$ Specification
s Specification -> Specification -> Specification
forall a. Semigroup a => a -> a -> a
<> Specification
s'
TillE Specification
bdy Specification
s <> Specification
s' = Specification -> Specification -> Specification
TillE Specification
bdy (Specification -> Specification) -> Specification -> Specification
forall a b. (a -> b) -> a -> b
$ Specification
s Specification -> Specification -> Specification
forall a. Semigroup a => a -> a -> a
<> Specification
s'
Specification
E <> Specification
_ = Specification
E
instance Monoid Specification where
mempty :: Specification
mempty = Specification
nop
readInput :: (Typeable a,Read a,Show a) => Var a -> ValueSet a -> InputMode -> Specification
readInput :: forall a.
(Typeable a, Read a, Show a) =>
Var a -> ValueSet a -> InputMode -> Specification
readInput = Var a -> ValueSet a -> InputMode -> Specification
forall a.
(Typeable a, Read a, Show a) =>
Var a -> ValueSet a -> InputMode -> Specification
readInput' where
readInput' :: forall a. (Typeable a,Read a,Show a) => Var a -> ValueSet a -> InputMode -> Specification
readInput' :: forall a.
(Typeable a, Read a, Show a) =>
Var a -> ValueSet a -> InputMode -> Specification
readInput' Var a
x ValueSet a
vs InputMode
m = Var a -> ValueSet a -> InputMode -> Specification -> Specification
forall k.
(Typeable k, Read k, Show k) =>
Var k -> ValueSet k -> InputMode -> Specification -> Specification
ReadInput Var a
x ValueSet a
vs InputMode
m Specification
nop
writeOutput :: [OutputPattern k] -> Specification
writeOutput :: forall (k :: PatternKind). [OutputPattern k] -> Specification
writeOutput [OutputPattern k]
ts = OptFlag -> Set (OutputPattern k) -> Specification -> Specification
forall (k :: PatternKind).
OptFlag -> Set (OutputPattern k) -> Specification -> Specification
WriteOutput OptFlag
Mandatory ([OutputPattern k] -> Set (OutputPattern k)
forall a. Ord a => [a] -> Set a
Set.fromList [OutputPattern k]
ts) Specification
nop
writeOptionalOutput :: [OutputPattern k] -> Specification
writeOptionalOutput :: forall (k :: PatternKind). [OutputPattern k] -> Specification
writeOptionalOutput [OutputPattern k]
ts = OptFlag -> Set (OutputPattern k) -> Specification -> Specification
forall (k :: PatternKind).
OptFlag -> Set (OutputPattern k) -> Specification -> Specification
WriteOutput OptFlag
Optional ([OutputPattern k] -> Set (OutputPattern k)
forall a. Ord a => [a] -> Set a
Set.fromList [OutputPattern k]
ts) Specification
nop
anyOptionalOutput :: Specification
anyOptionalOutput :: Specification
anyOptionalOutput = [OutputPattern Any] -> Specification
forall (k :: PatternKind). [OutputPattern k] -> Specification
writeOptionalOutput [OutputPattern Any
forall (k :: PatternKind). OutputPattern k
Wildcard]
branch :: Term 'Transparent Bool -> Specification -> Specification -> Specification
branch :: Term 'Transparent Bool
-> Specification -> Specification -> Specification
branch Term 'Transparent Bool
c Specification
t Specification
e = Term 'Transparent Bool
-> Specification -> Specification -> Specification -> Specification
Branch Term 'Transparent Bool
c Specification
t Specification
e Specification
nop
nop :: Specification
nop :: Specification
nop = Specification
Nop
tillExit :: Specification -> Specification
tillExit :: Specification -> Specification
tillExit Specification
bdy
| Bool
topLevelExitMarkerMissing = String -> Specification
forall a. HasCallStack => String -> a
error String
"tillExit: no top-level exit marker in body"
| Bool
hasDormantPath = String -> Specification
forall a. HasCallStack => String -> a
error String
"tillExit: body has dormant symbolic path (no input and not ending in 'exit')"
| Bool
otherwise = Specification -> Specification -> Specification
TillE Specification
bdy Specification
nop
where
loopPaths :: [[Either SomeVar ()]]
loopPaths = Specification -> [[Either SomeVar ()]]
pathProgress Specification
bdy
hasDormantPath :: Bool
hasDormantPath = [] [Either SomeVar ()] -> [[Either SomeVar ()]] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [[Either SomeVar ()]]
loopPaths
topLevelExitMarkerMissing :: Bool
topLevelExitMarkerMissing = ([Either SomeVar ()] -> Bool) -> [[Either SomeVar ()]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Either SomeVar () -> Bool) -> [Either SomeVar ()] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Either SomeVar () -> Bool
forall a b. Either a b -> Bool
isLeft) [[Either SomeVar ()]]
loopPaths
exit :: Specification
exit :: Specification
exit = Specification
E
whileNot :: Term 'Transparent Bool -> Specification -> Specification
whileNot :: Term 'Transparent Bool -> Specification -> Specification
whileNot Term 'Transparent Bool
c Specification
bdy =
Specification -> Specification
tillExit (Term 'Transparent Bool
-> Specification -> Specification -> Specification
branch Term 'Transparent Bool
c Specification
exit Specification
bdy) Specification -> Maybe String -> Specification
forall a. a -> Maybe String -> a
`orErrorFrom` String -> Term 'Transparent Bool -> Specification -> Maybe String
forall (k :: TermKind).
String -> Term k Bool -> Specification -> Maybe String
loopChecks String
"whileNot" Term 'Transparent Bool
c Specification
bdy
while :: Term 'Transparent Bool -> Specification -> Specification
while :: Term 'Transparent Bool -> Specification -> Specification
while Term 'Transparent Bool
c Specification
bdy = Specification -> Specification
tillExit (Term 'Transparent Bool
-> Specification -> Specification -> Specification
branch Term 'Transparent Bool
c Specification
bdy Specification
exit) Specification -> Maybe String -> Specification
forall a. a -> Maybe String -> a
`orErrorFrom` String -> Term 'Transparent Bool -> Specification -> Maybe String
forall (k :: TermKind).
String -> Term k Bool -> Specification -> Maybe String
loopChecks String
"while" Term 'Transparent Bool
c Specification
bdy
repeatUntil :: Specification -> Term 'Transparent Bool -> Specification
repeatUntil :: Specification -> Term 'Transparent Bool -> Specification
repeatUntil Specification
bdy Term 'Transparent Bool
c = Specification -> Specification
tillExit (Specification
bdy Specification -> Specification -> Specification
forall a. Semigroup a => a -> a -> a
<> Term 'Transparent Bool
-> Specification -> Specification -> Specification
branch Term 'Transparent Bool
c Specification
exit Specification
nop) Specification -> Maybe String -> Specification
forall a. a -> Maybe String -> a
`orErrorFrom` String -> Term 'Transparent Bool -> Specification -> Maybe String
forall (k :: TermKind).
String -> Term k Bool -> Specification -> Maybe String
loopChecks String
"repeatUntil" Term 'Transparent Bool
c Specification
bdy
doWhile :: Specification -> Term 'Transparent Bool -> Specification
doWhile :: Specification -> Term 'Transparent Bool -> Specification
doWhile Specification
bdy Term 'Transparent Bool
c = Specification -> Specification
tillExit (Specification
bdy Specification -> Specification -> Specification
forall a. Semigroup a => a -> a -> a
<> Term 'Transparent Bool
-> Specification -> Specification -> Specification
branch Term 'Transparent Bool
c Specification
nop Specification
exit) Specification -> Maybe String -> Specification
forall a. a -> Maybe String -> a
`orErrorFrom` String -> Term 'Transparent Bool -> Specification -> Maybe String
forall (k :: TermKind).
String -> Term k Bool -> Specification -> Maybe String
loopChecks String
"doWhile" Term 'Transparent Bool
c Specification
bdy
orErrorFrom :: a -> Maybe String -> a
orErrorFrom :: forall a. a -> Maybe String -> a
orErrorFrom = (a -> (String -> a) -> Maybe String -> a
forall b a. b -> (a -> b) -> Maybe a -> b
`maybe` String -> a
forall a. HasCallStack => String -> a
error )
loopChecks :: String -> Term k Bool -> Specification -> Maybe String
loopChecks :: forall (k :: TermKind).
String -> Term k Bool -> Specification -> Maybe String
loopChecks String
caller Term k Bool
c Specification
bdy
| String
caller String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [String]
expectedCallers = Maybe String
forall {a}. a
unexpectedCallerError
| Specification -> Bool
hasTopLevelExit Specification
bdy = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String
caller String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": top-level exit marker in body"
| [[SomeVar]] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[SomeVar]]
condVars = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String
caller String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": constant loop condition"
| ([Either SomeVar ()] -> Bool) -> [[Either SomeVar ()]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\[Either SomeVar ()]
p -> [SomeVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([SomeVar] -> Bool) -> [SomeVar] -> Bool
forall a b. (a -> b) -> a -> b
$ [[SomeVar]] -> [SomeVar]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[SomeVar]]
condVars [SomeVar] -> [SomeVar] -> [SomeVar]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [Either SomeVar ()] -> [SomeVar]
forall a b. [Either a b] -> [a]
lefts [Either SomeVar ()]
p) ([[Either SomeVar ()]] -> Bool) -> [[Either SomeVar ()]] -> Bool
forall a b. (a -> b) -> a -> b
$ Specification -> [[Either SomeVar ()]]
pathProgress Specification
bdy = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String
caller String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": body has dormant symbolic path (no input changes loop condition and it does not end in 'exit')"
| Bool
otherwise = Maybe String
forall a. Maybe a
Nothing
where
condVars :: [[SomeVar]]
condVars = Term k Bool -> [[SomeVar]]
forall a (k :: TermKind). Typeable a => Term k a -> [[SomeVar]]
termVarExps Term k Bool
c
expectedCallers :: [String]
expectedCallers = [String
"while", String
"whileNot", String
"repeatUntil", String
"doWhile"]
unexpectedCallerError :: a
unexpectedCallerError = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$
[String] -> String
unlines
[ String
"checks involving 'pathProgress' assume the caller of 'loopChecks' to be one of " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
expectedCallers
, String
"(if you see this message while using the public API, please contact the library authors)"
]
hasTopLevelExit :: Specification -> Bool
hasTopLevelExit :: Specification -> Bool
hasTopLevelExit (ReadInput Var a
_ ValueSet a
_ InputMode
_ Specification
s) = Specification -> Bool
hasTopLevelExit Specification
s
hasTopLevelExit (WriteOutput OptFlag
_ Set (OutputPattern k)
_ Specification
s) = Specification -> Bool
hasTopLevelExit Specification
s
hasTopLevelExit (Branch Term 'Transparent Bool
_ Specification
l Specification
r Specification
s) = Specification -> Bool
hasTopLevelExit Specification
l Bool -> Bool -> Bool
|| Specification -> Bool
hasTopLevelExit Specification
r Bool -> Bool -> Bool
|| Specification -> Bool
hasTopLevelExit Specification
s
hasTopLevelExit (TillE Specification
_ Specification
s) = Specification -> Bool
hasTopLevelExit Specification
s
hasTopLevelExit Specification
Nop = Bool
False
hasTopLevelExit Specification
E = Bool
True
pathProgress :: Specification -> [[Either SomeVar ()]]
pathProgress :: Specification -> [[Either SomeVar ()]]
pathProgress (ReadInput Var a
x ValueSet a
_ InputMode
_ Specification
s') = ((SomeVar -> Either SomeVar ()
forall a b. a -> Either a b
Left (SomeVar -> Either SomeVar ()) -> SomeVar -> Either SomeVar ()
forall a b. (a -> b) -> a -> b
$ Var a -> SomeVar
forall a. Typeable a => Var a -> SomeVar
someVar Var a
x):) ([Either SomeVar ()] -> [Either SomeVar ()])
-> [[Either SomeVar ()]] -> [[Either SomeVar ()]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Specification -> [[Either SomeVar ()]]
pathProgress Specification
s'
pathProgress (WriteOutput OptFlag
_ Set (OutputPattern k)
_ Specification
s') = Specification -> [[Either SomeVar ()]]
pathProgress Specification
s'
pathProgress (Branch Term 'Transparent Bool
_ Specification
s1 Specification
s2 Specification
s') = Specification -> [[Either SomeVar ()]]
pathProgress (Specification
s1 Specification -> Specification -> Specification
forall a. Semigroup a => a -> a -> a
<> Specification
s') [[Either SomeVar ()]]
-> [[Either SomeVar ()]] -> [[Either SomeVar ()]]
forall a. [a] -> [a] -> [a]
++ Specification -> [[Either SomeVar ()]]
pathProgress (Specification
s2 Specification -> Specification -> Specification
forall a. Semigroup a => a -> a -> a
<> Specification
s')
pathProgress (TillE Specification
s Specification
s') =
let directlyTerminatingPaths :: [[Either SomeVar ()]]
directlyTerminatingPaths = ([Either SomeVar ()] -> [Either SomeVar ()])
-> [[Either SomeVar ()]] -> [[Either SomeVar ()]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Either SomeVar ()] -> [Either SomeVar ()]
forall a. HasCallStack => [a] -> [a]
init ([[Either SomeVar ()]] -> [[Either SomeVar ()]])
-> ([[Either SomeVar ()]] -> [[Either SomeVar ()]])
-> [[Either SomeVar ()]]
-> [[Either SomeVar ()]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Either SomeVar ()] -> Bool)
-> [[Either SomeVar ()]] -> [[Either SomeVar ()]]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Either SomeVar () -> Bool) -> [Either SomeVar ()] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Either SomeVar () -> Bool
forall a b. Either a b -> Bool
isRight) ([[Either SomeVar ()]] -> [[Either SomeVar ()]])
-> [[Either SomeVar ()]] -> [[Either SomeVar ()]]
forall a b. (a -> b) -> a -> b
$ Specification -> [[Either SomeVar ()]]
pathProgress Specification
s
in [Either SomeVar ()] -> [Either SomeVar ()] -> [Either SomeVar ()]
forall a. [a] -> [a] -> [a]
(++) ([Either SomeVar ()] -> [Either SomeVar ()] -> [Either SomeVar ()])
-> [[Either SomeVar ()]]
-> [[Either SomeVar ()] -> [Either SomeVar ()]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[Either SomeVar ()]]
directlyTerminatingPaths [[Either SomeVar ()] -> [Either SomeVar ()]]
-> [[Either SomeVar ()]] -> [[Either SomeVar ()]]
forall a b. [a -> b] -> [a] -> [b]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Specification -> [[Either SomeVar ()]]
pathProgress Specification
s'
pathProgress Specification
Nop = [[]]
pathProgress Specification
E = [[() -> Either SomeVar ()
forall a b. b -> Either a b
Right ()]]
readVars :: Specification -> [SomeVar]
readVars :: Specification -> [SomeVar]
readVars = [SomeVar] -> [SomeVar]
forall a. Eq a => [a] -> [a]
nub ([SomeVar] -> [SomeVar])
-> (Specification -> [SomeVar]) -> Specification -> [SomeVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Specification -> [SomeVar]
go where
go :: Specification -> [SomeVar]
go (ReadInput Var a
x ValueSet a
_ InputMode
_ Specification
s') = Var a -> SomeVar
forall a. Typeable a => Var a -> SomeVar
someVar Var a
x SomeVar -> [SomeVar] -> [SomeVar]
forall a. a -> [a] -> [a]
: Specification -> [SomeVar]
go Specification
s'
go (WriteOutput OptFlag
_ Set (OutputPattern k)
_ Specification
s') = Specification -> [SomeVar]
go Specification
s'
go (Branch Term 'Transparent Bool
_ Specification
l Specification
r Specification
s') = Specification -> [SomeVar]
go Specification
l [SomeVar] -> [SomeVar] -> [SomeVar]
forall a. [a] -> [a] -> [a]
++ Specification -> [SomeVar]
go Specification
r [SomeVar] -> [SomeVar] -> [SomeVar]
forall a. [a] -> [a] -> [a]
++ Specification -> [SomeVar]
go Specification
s'
go Specification
Nop = []
go (TillE Specification
bdy Specification
s') = Specification -> [SomeVar]
go Specification
bdy [SomeVar] -> [SomeVar] -> [SomeVar]
forall a. [a] -> [a] -> [a]
++ Specification -> [SomeVar]
go Specification
s'
go Specification
E = []
hasIteration :: Specification -> Bool
hasIteration :: Specification -> Bool
hasIteration (ReadInput Var a
_ ValueSet a
_ InputMode
_ Specification
s') = Specification -> Bool
hasIteration Specification
s'
hasIteration (WriteOutput OptFlag
_ Set (OutputPattern k)
_ Specification
s') = Specification -> Bool
hasIteration Specification
s'
hasIteration (Branch Term 'Transparent Bool
_ Specification
l Specification
r Specification
s') = Specification -> Bool
hasIteration Specification
l Bool -> Bool -> Bool
|| Specification -> Bool
hasIteration Specification
r Bool -> Bool -> Bool
|| Specification -> Bool
hasIteration Specification
s'
hasIteration TillE{} = Bool
True
hasIteration Specification
Nop = Bool
False
hasIteration Specification
E = Bool
False
runSpecification :: Specification -> [String] -> (AbstractTrace,OverflowWarning)
runSpecification :: Specification -> [String] -> (AbstractTrace, OverflowWarning)
runSpecification = Bool
-> Specification -> [String] -> (AbstractTrace, OverflowWarning)
runSpecification' Bool
True
runSpecification' :: AddLinebreaks -> Specification -> [String] -> (AbstractTrace,OverflowWarning)
runSpecification' :: Bool
-> Specification -> [String] -> (AbstractTrace, OverflowWarning)
runSpecification' Bool
addLinebreaks Specification
spec [String]
inputs =
(forall v.
(Typeable v, Read v, Show v) =>
(ValueMap, [String])
-> Var v
-> ValueSet v
-> InputMode
-> RecStruct
String
((AbstractTrace, OverflowWarning)
-> (AbstractTrace, OverflowWarning))
(ValueMap, [String])
(AbstractTrace, OverflowWarning))
-> (RecStruct
String
()
(AbstractTrace, OverflowWarning)
(AbstractTrace, OverflowWarning)
-> (AbstractTrace, OverflowWarning))
-> (forall (k :: PatternKind).
(ValueMap, [String])
-> OptFlag
-> Set (OutputPattern k)
-> (AbstractTrace, OverflowWarning)
-> (AbstractTrace, OverflowWarning))
-> ((ValueMap, [String])
-> Term 'Transparent Bool
-> (AbstractTrace, OverflowWarning)
-> (AbstractTrace, OverflowWarning)
-> (AbstractTrace, OverflowWarning))
-> (Action
-> (AbstractTrace, OverflowWarning)
-> (AbstractTrace, OverflowWarning))
-> ((AbstractTrace, OverflowWarning)
-> (AbstractTrace, OverflowWarning))
-> (AbstractTrace, OverflowWarning)
-> (ValueMap, [String])
-> Specification
-> (AbstractTrace, OverflowWarning)
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
(\(ValueMap
e,[String]
ins) Var v
x (ValueSet v
vs :: ValueSet v) InputMode
mode ->
case [String]
ins of
[] -> (AbstractTrace, OverflowWarning)
-> RecStruct
String
((AbstractTrace, OverflowWarning)
-> (AbstractTrace, OverflowWarning))
(ValueMap, [String])
(AbstractTrace, OverflowWarning)
forall p x a r. r -> RecStruct p x a r
NoRec (AbstractTrace
outOfInputs,OverflowWarning
NoOverflow)
(String
i:[String]
is)
| Var v -> ValueMap -> ValueSet v -> v -> Bool
forall a. Var a -> ValueMap -> ValueSet a -> a -> Bool
containsValue Var v
x ValueMap
e ValueSet v
vs (Var v -> String -> v
forall a. Var a -> String -> a
readValue Var v
x String
i) -> String
-> ((AbstractTrace, OverflowWarning)
-> (AbstractTrace, OverflowWarning))
-> (ValueMap, [String])
-> RecStruct
String
((AbstractTrace, OverflowWarning)
-> (AbstractTrace, OverflowWarning))
(ValueMap, [String])
(AbstractTrace, OverflowWarning)
forall p x a r. p -> x -> a -> RecStruct p x a r
RecSub String
i (AbstractTrace, OverflowWarning)
-> (AbstractTrace, OverflowWarning)
forall a. a -> a
id (Value -> SomeVar -> ValueMap -> ValueMap
insertValue (v -> Value
forall a. Typeable a => a -> Value
wrapValue (v -> Value) -> v -> Value
forall a b. (a -> b) -> a -> b
$ Var v -> String -> v
forall a. Var a -> String -> a
readValue Var v
x String
i) (Var v -> SomeVar
forall a. Typeable a => Var a -> SomeVar
someVar Var v
x) ValueMap
e,[String]
is)
| Bool
otherwise -> case InputMode
mode of
InputMode
AssumeValid -> String
-> RecStruct
String
((AbstractTrace, OverflowWarning)
-> (AbstractTrace, OverflowWarning))
(ValueMap, [String])
(AbstractTrace, OverflowWarning)
forall a. HasCallStack => String -> a
error (String
-> RecStruct
String
((AbstractTrace, OverflowWarning)
-> (AbstractTrace, OverflowWarning))
(ValueMap, [String])
(AbstractTrace, OverflowWarning))
-> String
-> RecStruct
String
((AbstractTrace, OverflowWarning)
-> (AbstractTrace, OverflowWarning))
(ValueMap, [String])
(AbstractTrace, OverflowWarning)
forall a b. (a -> b) -> a -> b
$ String
"invalid value: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" is not an element of " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ValueSet v -> String
forall a. Typeable a => ValueSet a -> String
showValueSet ValueSet v
vs
InputMode
UntilValid -> String
-> ((AbstractTrace, OverflowWarning)
-> (AbstractTrace, OverflowWarning))
-> (ValueMap, [String])
-> RecStruct
String
((AbstractTrace, OverflowWarning)
-> (AbstractTrace, OverflowWarning))
(ValueMap, [String])
(AbstractTrace, OverflowWarning)
forall p x a r. p -> x -> a -> RecStruct p x a r
RecSame String
i ((AbstractTrace -> AbstractTrace)
-> (AbstractTrace, OverflowWarning)
-> (AbstractTrace, OverflowWarning)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (OptFlag -> Set (OutputPattern 'TraceP) -> AbstractTrace
progWrite OptFlag
Optional (OutputPattern 'TraceP -> Set (OutputPattern 'TraceP)
forall a. a -> Set a
Set.singleton OutputPattern 'TraceP
forall (k :: PatternKind). OutputPattern k
Wildcard) <>)) (ValueMap
e,[String]
is)
InputMode
ElseAbort -> (AbstractTrace, OverflowWarning)
-> RecStruct
String
((AbstractTrace, OverflowWarning)
-> (AbstractTrace, OverflowWarning))
(ValueMap, [String])
(AbstractTrace, OverflowWarning)
forall p x a r. r -> RecStruct p x a r
NoRec ((Char -> AbstractTrace -> AbstractTrace)
-> AbstractTrace -> String -> AbstractTrace
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (AbstractTrace -> AbstractTrace -> AbstractTrace
forall a. Semigroup a => a -> a -> a
(<>) (AbstractTrace -> AbstractTrace -> AbstractTrace)
-> (Char -> AbstractTrace)
-> Char
-> AbstractTrace
-> AbstractTrace
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> AbstractTrace
progRead) ((AbstractTrace -> AbstractTrace -> AbstractTrace
forall a. Semigroup a => a -> a -> a
(<>) (AbstractTrace -> AbstractTrace -> AbstractTrace)
-> (Char -> AbstractTrace)
-> Char
-> AbstractTrace
-> AbstractTrace
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> AbstractTrace
progRead) Char
'\n' (AbstractTrace -> AbstractTrace) -> AbstractTrace -> AbstractTrace
forall a b. (a -> b) -> a -> b
$ OptFlag -> Set (OutputPattern 'TraceP) -> AbstractTrace
progWrite OptFlag
Optional (OutputPattern 'TraceP -> Set (OutputPattern 'TraceP)
forall a. a -> Set a
Set.singleton OutputPattern 'TraceP
forall (k :: PatternKind). OutputPattern k
Wildcard)) String
i,OverflowWarning
NoOverflow)
)
(\case
NoRec (AbstractTrace, OverflowWarning)
r -> (AbstractTrace, OverflowWarning)
r
RecSub String
i () (AbstractTrace
t',OverflowWarning
w) -> ((Char -> AbstractTrace -> AbstractTrace)
-> AbstractTrace -> String -> AbstractTrace
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (AbstractTrace -> AbstractTrace -> AbstractTrace
forall a. Semigroup a => a -> a -> a
(<>) (AbstractTrace -> AbstractTrace -> AbstractTrace)
-> (Char -> AbstractTrace)
-> Char
-> AbstractTrace
-> AbstractTrace
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> AbstractTrace
progRead) ((AbstractTrace -> AbstractTrace -> AbstractTrace
forall a. Semigroup a => a -> a -> a
(<>) (AbstractTrace -> AbstractTrace -> AbstractTrace)
-> (Char -> AbstractTrace)
-> Char
-> AbstractTrace
-> AbstractTrace
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> AbstractTrace
progRead) Char
'\n' AbstractTrace
t') String
i,OverflowWarning
w)
RecSame String
i () (AbstractTrace
t',OverflowWarning
w) -> ((Char -> AbstractTrace -> AbstractTrace)
-> AbstractTrace -> String -> AbstractTrace
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (AbstractTrace -> AbstractTrace -> AbstractTrace
forall a. Semigroup a => a -> a -> a
(<>) (AbstractTrace -> AbstractTrace -> AbstractTrace)
-> (Char -> AbstractTrace)
-> Char
-> AbstractTrace
-> AbstractTrace
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> AbstractTrace
progRead) ((AbstractTrace -> AbstractTrace -> AbstractTrace
forall a. Semigroup a => a -> a -> a
(<>) (AbstractTrace -> AbstractTrace -> AbstractTrace)
-> (Char -> AbstractTrace)
-> Char
-> AbstractTrace
-> AbstractTrace
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> AbstractTrace
progRead) Char
'\n' AbstractTrace
t') String
i,OverflowWarning
w)
RecBoth{} -> String -> (AbstractTrace, OverflowWarning)
forall a. HasCallStack => String -> a
error String
"runSpecification: impossible"
)
(\(ValueMap
e,[String]
_) OptFlag
o Set (OutputPattern k)
ts (AbstractTrace
t',OverflowWarning
ww) ->
let (OverflowWarning
warn,Set (OutputPattern 'TraceP)
os) = Bool
-> ValueMap
-> Set (OutputPattern k)
-> (OverflowWarning, Set (OutputPattern 'TraceP))
forall (k :: PatternKind).
Bool
-> ValueMap
-> Set (OutputPattern k)
-> (OverflowWarning, Set (OutputPattern 'TraceP))
evalPatternSet' Bool
addLinebreaks ValueMap
e Set (OutputPattern k)
ts
in (OptFlag -> Set (OutputPattern 'TraceP) -> AbstractTrace
progWrite OptFlag
o Set (OutputPattern 'TraceP)
os AbstractTrace -> AbstractTrace -> AbstractTrace
forall a. Semigroup a => a -> a -> a
<> AbstractTrace
t', OverflowWarning
warn OverflowWarning -> OverflowWarning -> OverflowWarning
forall a. Semigroup a => a -> a -> a
<> OverflowWarning
ww)
)
(\(ValueMap
e,[String]
_) Term 'Transparent Bool
c (AbstractTrace, OverflowWarning)
l (AbstractTrace, OverflowWarning)
r ->
let (OverflowWarning
w,Bool
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
c
in if Bool
b
then (OverflowWarning -> OverflowWarning)
-> (AbstractTrace, OverflowWarning)
-> (AbstractTrace, OverflowWarning)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (OverflowWarning -> OverflowWarning -> OverflowWarning
forall a. Semigroup a => a -> a -> a
<> OverflowWarning
w) (AbstractTrace, OverflowWarning)
l
else (OverflowWarning -> OverflowWarning)
-> (AbstractTrace, OverflowWarning)
-> (AbstractTrace, OverflowWarning)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (OverflowWarning -> OverflowWarning -> OverflowWarning
forall a. Semigroup a => a -> a -> a
<> OverflowWarning
w) (AbstractTrace, OverflowWarning)
r
)
(((AbstractTrace, OverflowWarning)
-> (AbstractTrace, OverflowWarning))
-> Action
-> (AbstractTrace, OverflowWarning)
-> (AbstractTrace, OverflowWarning)
forall a b. a -> b -> a
const (AbstractTrace, OverflowWarning)
-> (AbstractTrace, OverflowWarning)
forall a. a -> a
id)
(AbstractTrace, OverflowWarning)
-> (AbstractTrace, OverflowWarning)
forall a. a -> a
id
(AbstractTrace
terminate,OverflowWarning
NoOverflow)
([SomeVar] -> ValueMap
emptyValueMap ([SomeVar] -> ValueMap) -> [SomeVar] -> ValueMap
forall a b. (a -> b) -> a -> b
$ Specification -> [SomeVar]
readVars Specification
spec,[String]
inputs)
Specification
spec
data RecStruct p x a r = NoRec r | RecSub p x a | RecSame p x a | RecBoth p x a a
sem :: 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. st -> OptFlag -> Set (OutputPattern k) -> a -> a) ->
(st -> Term 'Transparent Bool -> a -> a -> a) ->
(Action -> a -> a) ->
(a -> a) ->
a ->
st -> Specification -> a
sem :: 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 forall v.
(Typeable v, Read v, Show v) =>
st -> Var v -> ValueSet v -> InputMode -> RecStruct p (a -> a) st a
f RecStruct p () a a -> a
f' forall (k :: PatternKind).
st -> OptFlag -> Set (OutputPattern k) -> a -> a
g st -> Term 'Transparent Bool -> a -> a -> a
h Action -> a -> a
i a -> a
j a
z st
st Specification
s = Identity a -> a
forall a. Identity a -> a
runIdentity (Identity a -> a) -> Identity a -> a
forall a b. (a -> b) -> a -> b
$ (forall v.
(Typeable v, Read v, Show v) =>
st
-> Var v
-> ValueSet v
-> InputMode
-> Identity (RecStruct p (a -> a) st a))
-> (RecStruct p () a a -> Identity a)
-> (forall (k :: PatternKind).
st -> OptFlag -> Set (OutputPattern k) -> Identity a -> Identity a)
-> (st
-> Term 'Transparent Bool
-> Identity a
-> Identity a
-> Identity a)
-> (Action -> Identity a -> Identity a)
-> (Identity a -> Identity a)
-> Identity a
-> st
-> Specification
-> Identity a
forall (m :: * -> *) st p a.
Monad m =>
(forall v.
(Typeable v, Read v, Show v) =>
st
-> Var v
-> ValueSet v
-> InputMode
-> m (RecStruct p (a -> a) st a))
-> (RecStruct p () a a -> m a)
-> (forall (k :: PatternKind).
st -> OptFlag -> Set (OutputPattern k) -> m a -> m a)
-> (st -> Term 'Transparent Bool -> m a -> m a -> m a)
-> (Action -> m a -> m a)
-> (m a -> m a)
-> m a
-> st
-> Specification
-> m a
semM
(\st
a Var v
b ValueSet v
c InputMode
d -> RecStruct p (a -> a) st a -> Identity (RecStruct p (a -> a) st a)
forall a. a -> Identity a
Identity (RecStruct p (a -> a) st a -> Identity (RecStruct p (a -> a) st a))
-> RecStruct p (a -> a) st a
-> Identity (RecStruct p (a -> a) st a)
forall a b. (a -> b) -> a -> b
$ st -> Var v -> ValueSet v -> InputMode -> RecStruct p (a -> a) st a
forall v.
(Typeable v, Read v, Show v) =>
st -> Var v -> ValueSet v -> InputMode -> RecStruct p (a -> a) st a
f st
a Var v
b ValueSet v
c InputMode
d)
(a -> Identity a
forall a. a -> Identity a
Identity (a -> Identity a)
-> (RecStruct p () a a -> a) -> RecStruct p () a a -> Identity a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RecStruct p () a a -> a
f')
(\st
a OptFlag
b Set (OutputPattern k)
c -> a -> Identity a
forall a. a -> Identity a
Identity (a -> Identity a) -> (Identity a -> a) -> Identity a -> Identity a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. st -> OptFlag -> Set (OutputPattern k) -> a -> a
forall (k :: PatternKind).
st -> OptFlag -> Set (OutputPattern k) -> a -> a
g st
a OptFlag
b Set (OutputPattern k)
c (a -> a) -> (Identity a -> a) -> Identity a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity a -> a
forall a. Identity a -> a
runIdentity)
(\st
a Term 'Transparent Bool
b Identity a
c Identity a
d -> a -> Identity a
forall a. a -> Identity a
Identity (a -> Identity a) -> a -> Identity a
forall a b. (a -> b) -> a -> b
$ st -> Term 'Transparent Bool -> a -> a -> a
h st
a Term 'Transparent Bool
b (Identity a -> a
forall a. Identity a -> a
runIdentity Identity a
c) (Identity a -> a
forall a. Identity a -> a
runIdentity Identity a
d))
(\Action
a Identity a
b -> a -> Identity a
forall a. a -> Identity a
Identity (a -> Identity a) -> a -> Identity a
forall a b. (a -> b) -> a -> b
$ Action -> a -> a
i Action
a (Identity a -> a
forall a. Identity a -> a
runIdentity Identity a
b))
(a -> Identity a
forall a. a -> Identity a
Identity (a -> Identity a) -> (Identity a -> a) -> Identity a -> Identity a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
j (a -> a) -> (Identity a -> a) -> Identity a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity a -> a
forall a. Identity a -> a
runIdentity)
(a -> Identity a
forall a. a -> Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
z)
st
st
Specification
s
semM :: forall m st p a. Monad m =>
(forall v. (Typeable v,Read v,Show v) => st -> Var v -> ValueSet v -> InputMode -> m (RecStruct p (a->a) st a)) -> (RecStruct p () a a -> m a) ->
(forall k. st -> OptFlag -> Set (OutputPattern k) -> m a -> m a) ->
(st -> Term 'Transparent Bool -> m a -> m a -> m a) ->
(Action -> m a -> m a) ->
(m a -> m a) ->
m a ->
st -> Specification -> m a
semM :: forall (m :: * -> *) st p a.
Monad m =>
(forall v.
(Typeable v, Read v, Show v) =>
st
-> Var v
-> ValueSet v
-> InputMode
-> m (RecStruct p (a -> a) st a))
-> (RecStruct p () a a -> m a)
-> (forall (k :: PatternKind).
st -> OptFlag -> Set (OutputPattern k) -> m a -> m a)
-> (st -> Term 'Transparent Bool -> m a -> m a -> m a)
-> (Action -> m a -> m a)
-> (m a -> m a)
-> m a
-> st
-> Specification
-> m a
semM forall v.
(Typeable v, Read v, Show v) =>
st
-> Var v
-> ValueSet v
-> InputMode
-> m (RecStruct p (a -> a) st a)
f RecStruct p () a a -> m a
f' forall (k :: PatternKind).
st -> OptFlag -> Set (OutputPattern k) -> m a -> m a
g st -> Term 'Transparent Bool -> m a -> m a -> m a
h Action -> m a -> m a
i m a -> m a
j m a
z st
s_I Specification
spec = st -> Specification -> (Action -> st -> m a) -> m a
sem' st
s_I Specification
spec Action -> st -> m a
k_I where
sem' :: st -> Specification -> (Action -> st -> m a) -> m a
sem' :: st -> Specification -> (Action -> st -> m a) -> m a
sem' st
st s :: Specification
s@(ReadInput Var a
x ValueSet a
vs InputMode
mode Specification
s') Action -> st -> m a
k =
do
let mStruct :: m (RecStruct p (a -> a) st a)
mStruct = st
-> Var a
-> ValueSet a
-> InputMode
-> m (RecStruct p (a -> a) st a)
forall v.
(Typeable v, Read v, Show v) =>
st
-> Var v
-> ValueSet v
-> InputMode
-> m (RecStruct p (a -> a) st a)
f st
st Var a
x ValueSet a
vs InputMode
mode
RecStruct p (a -> a) st a
struct <- m (RecStruct p (a -> a) st a)
mStruct
RecStruct p () a a -> m a
f' (RecStruct p () a a -> m a) -> m (RecStruct p () a a) -> m a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< case RecStruct p (a -> a) st a
struct of
NoRec a
r -> RecStruct p () a a -> m (RecStruct p () a a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RecStruct p () a a -> m (RecStruct p () a a))
-> RecStruct p () a a -> m (RecStruct p () a a)
forall a b. (a -> b) -> a -> b
$ a -> RecStruct p () a a
forall p x a r. r -> RecStruct p x a r
NoRec a
r
RecSub p
p a -> a
r st
st' -> p -> () -> a -> RecStruct p () a a
forall p x a r. p -> x -> a -> RecStruct p x a r
RecSub p
p () (a -> RecStruct p () a a) -> (a -> a) -> a -> RecStruct p () a a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
r (a -> RecStruct p () a a) -> m a -> m (RecStruct p () a a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> st -> Specification -> (Action -> st -> m a) -> m a
sem' st
st' Specification
s' Action -> st -> m a
k
RecSame p
p a -> a
r st
st' -> p -> () -> a -> RecStruct p () a a
forall p x a r. p -> x -> a -> RecStruct p x a r
RecSame p
p () (a -> RecStruct p () a a) -> (a -> a) -> a -> RecStruct p () a a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
r (a -> RecStruct p () a a) -> m a -> m (RecStruct p () a a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> st -> Specification -> (Action -> st -> m a) -> m a
sem' st
st' Specification
s Action -> st -> m a
k
RecBoth p
p a -> a
r st
st' st
st'' -> p -> () -> a -> a -> RecStruct p () a a
forall p x a r. p -> x -> a -> a -> RecStruct p x a r
RecBoth p
p () (a -> a -> RecStruct p () a a)
-> (a -> a) -> a -> a -> RecStruct p () a a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
r (a -> a -> RecStruct p () a a)
-> m a -> m (a -> RecStruct p () a a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> st -> Specification -> (Action -> st -> m a) -> m a
sem' st
st' Specification
s' Action -> st -> m a
k m (a -> RecStruct p () a a) -> m a -> m (RecStruct p () a a)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> st -> Specification -> (Action -> st -> m a) -> m a
sem' st
st'' Specification
s Action -> st -> m a
k
sem' st
st (WriteOutput OptFlag
o Set (OutputPattern k)
ts Specification
s') Action -> st -> m a
k = st -> OptFlag -> Set (OutputPattern k) -> m a -> m a
forall (k :: PatternKind).
st -> OptFlag -> Set (OutputPattern k) -> m a -> m a
g st
st OptFlag
o Set (OutputPattern k)
ts (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ st -> Specification -> (Action -> st -> m a) -> m a
sem' st
st Specification
s' Action -> st -> m a
k
sem' st
st (Branch Term 'Transparent Bool
c Specification
l Specification
r Specification
s') Action -> st -> m a
k = st -> Term 'Transparent Bool -> m a -> m a -> m a
h st
st Term 'Transparent Bool
c (st -> Specification -> (Action -> st -> m a) -> m a
sem' st
st (Specification
l Specification -> Specification -> Specification
forall a. Semigroup a => a -> a -> a
<> Specification
s') Action -> st -> m a
k) (st -> Specification -> (Action -> st -> m a) -> m a
sem' st
st (Specification
r Specification -> Specification -> Specification
forall a. Semigroup a => a -> a -> a
<> Specification
s') Action -> st -> m a
k)
sem' st
st (TillE Specification
s Specification
s') Action -> st -> m a
k = m a -> m a
j (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ st -> Specification -> (Action -> st -> m a) -> m a
sem' st
st Specification
s Action -> st -> m a
k'
where
k' :: Action -> st -> m a
k' Action
End st
st = Action -> m a -> m a
i Action
End (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ st -> Specification -> (Action -> st -> m a) -> m a
sem' st
st Specification
s Action -> st -> m a
k'
k' Action
Exit st
st = Action -> m a -> m a
i Action
Exit (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ st -> Specification -> (Action -> st -> m a) -> m a
sem' st
st Specification
s' Action -> st -> m a
k
sem' st
st Specification
Nop Action -> st -> m a
k = Action -> st -> m a
k Action
End st
st
sem' st
st Specification
E Action -> st -> m a
k = Action -> st -> m a
k Action
Exit st
st
k_I :: Action -> st -> m a
k_I :: Action -> st -> m a
k_I Action
End st
_ = m a
z
k_I Action
Exit st
_ = String -> m a
forall a. HasCallStack => String -> a
error String
"ill-formed specification: exit marker at top-level"
data Action = End | Exit
pPrintSpecification :: Specification -> Doc
pPrintSpecification :: Specification -> Doc
pPrintSpecification (ReadInput Var a
x ValueSet a
vs InputMode
m Specification
s) = String -> Doc
text ([String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"[▷ ",Var a -> String
forall a. Var a -> String
varname Var a
x,String
" ∈ ", ValueSet a -> String
forall a. Typeable a => ValueSet a -> String
showValueSet ValueSet a
vs, String
"]",InputMode -> String
showInputMode InputMode
m]) Doc -> Doc -> Doc
$$ Specification -> Doc
pPrintSpecification Specification
s
pPrintSpecification (WriteOutput OptFlag
opt Set (OutputPattern k)
ts Specification
s) = String -> Doc
text ([String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [String
"[{",if OptFlag
opt OptFlag -> OptFlag -> Bool
forall a. Eq a => a -> a -> Bool
== OptFlag
Optional then String
"𝜀," else String
""] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ String -> [String] -> [String]
forall a. a -> [a] -> [a]
intersperse String
"," ((OutputPattern k -> String) -> [OutputPattern k] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map OutputPattern k -> String
forall (k :: PatternKind). OutputPattern k -> String
showPatternSimple (Set (OutputPattern k) -> [OutputPattern k]
forall a. Set a -> [a]
Set.toList Set (OutputPattern k)
ts)) [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"}▷ ]"]) Doc -> Doc -> Doc
$$ Specification -> Doc
pPrintSpecification Specification
s
pPrintSpecification (Branch Term 'Transparent Bool
c Specification
t Specification
e Specification
s) = String -> Doc
text ([String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"[",Term 'Transparent Bool -> String
forall a (k :: TermKind). Typeable a => Term k a -> String
showTerm Term 'Transparent Bool
c,String
"]⇒ ("]) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Specification -> Doc
pPrintSpecification Specification
t Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text String
"△ " Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Specification -> Doc
pPrintSpecification Specification
e Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text String
")" Doc -> Doc -> Doc
$$ Specification -> Doc
pPrintSpecification Specification
s
pPrintSpecification Specification
Nop = String -> Doc
text String
"0"
pPrintSpecification (TillE Specification
bdy Specification
s) = String -> Doc
text String
"(" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Specification -> Doc
pPrintSpecification Specification
bdy Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text String
")🠒ᴱ" Doc -> Doc -> Doc
$$ Specification -> Doc
pPrintSpecification Specification
s
pPrintSpecification Specification
E = String -> Doc
text String
"E"
showInputMode :: InputMode -> String
showInputMode :: InputMode -> String
showInputMode InputMode
AssumeValid = String
""
showInputMode InputMode
UntilValid = String
"↻"
showInputMode InputMode
ElseAbort = String
"↯"
accept :: Specification -> Trace -> Bool
accept :: Specification -> Trace -> Bool
accept Specification
s_ Trace
t_ = Specification
-> (Action -> Trace -> ValueMap -> Bool)
-> Trace
-> ValueMap
-> Bool
accept' Specification
s_ Action -> Trace -> ValueMap -> Bool
k_I Trace
t_ ValueMap
d_I
where
accept' :: Specification -> (Action -> Trace -> ValueMap -> Bool) -> Trace -> ValueMap -> Bool
accept' :: Specification
-> (Action -> Trace -> ValueMap -> Bool)
-> Trace
-> ValueMap
-> Bool
accept' (ReadInput Var a
x (ValueSet a
ty :: ValueSet a) InputMode
AssumeValid Specification
s') Action -> Trace -> ValueMap -> Bool
k Trace
t ValueMap
d = case Trace
t of
ProgReadString String
v Trace
t' | Var a -> ValueMap -> ValueSet a -> a -> Bool
forall a. Var a -> ValueMap -> ValueSet a -> a -> Bool
containsValue Var a
x ValueMap
d ValueSet a
ty a
val -> Specification
-> (Action -> Trace -> ValueMap -> Bool)
-> Trace
-> ValueMap
-> Bool
accept' Specification
s' Action -> Trace -> ValueMap -> Bool
k Trace
t' (Value -> SomeVar -> ValueMap -> ValueMap
insertValue (a -> Value
forall a. Typeable a => a -> Value
wrapValue a
val) (Var a -> SomeVar
forall a. Typeable a => Var a -> SomeVar
someVar Var a
x) ValueMap
d)
where val :: a
val = Var a -> String -> a
forall a. Var a -> String -> a
readValue Var a
x String
v
Trace
_ -> Bool
False
accept' (ReadInput Var a
x (ValueSet a
ty :: ValueSet a) InputMode
ElseAbort Specification
s') Action -> Trace -> ValueMap -> Bool
k Trace
t ValueMap
d = case Trace
t of
ProgReadString String
v Trace
t'| Var a -> ValueMap -> ValueSet a -> a -> Bool
forall a. Var a -> ValueMap -> ValueSet a -> a -> Bool
containsValue Var a
x ValueMap
d ValueSet a
ty a
val -> Specification
-> (Action -> Trace -> ValueMap -> Bool)
-> Trace
-> ValueMap
-> Bool
accept' Specification
s' Action -> Trace -> ValueMap -> Bool
k Trace
t' (Value -> SomeVar -> ValueMap -> ValueMap
insertValue (a -> Value
forall a. Typeable a => a -> Value
wrapValue a
val) (Var a -> SomeVar
forall a. Typeable a => Var a -> SomeVar
someVar Var a
x) ValueMap
d)
where val :: a
val = Var a -> String -> a
forall a. Var a -> String -> a
readValue Var a
x String
v
ProgReadString String
v Trace
Terminate | Bool -> Bool
not (Var a -> ValueMap -> ValueSet a -> a -> Bool
forall a. Var a -> ValueMap -> ValueSet a -> a -> Bool
containsValue Var a
x ValueMap
d ValueSet a
ty (Var a -> String -> a
forall a. Var a -> String -> a
readValue Var a
x String
v)) -> Bool
True
Trace
_ -> Bool
False
accept' s :: Specification
s@(ReadInput Var a
x (ValueSet a
ty :: ValueSet a) InputMode
UntilValid Specification
s') Action -> Trace -> ValueMap -> Bool
k Trace
t ValueMap
d = case Trace
t of
ProgReadString String
v Trace
t'
| Var a -> ValueMap -> ValueSet a -> a -> Bool
forall a. Var a -> ValueMap -> ValueSet a -> a -> Bool
containsValue Var a
x ValueMap
d ValueSet a
ty a
val -> Specification
-> (Action -> Trace -> ValueMap -> Bool)
-> Trace
-> ValueMap
-> Bool
accept' Specification
s' Action -> Trace -> ValueMap -> Bool
k Trace
t' (Value -> SomeVar -> ValueMap -> ValueMap
insertValue (a -> Value
forall a. Typeable a => a -> Value
wrapValue a
val) (Var a -> SomeVar
forall a. Typeable a => Var a -> SomeVar
someVar Var a
x) ValueMap
d)
| Bool -> Bool
not (Var a -> ValueMap -> ValueSet a -> a -> Bool
forall a. Var a -> ValueMap -> ValueSet a -> a -> Bool
containsValue Var a
x ValueMap
d ValueSet a
ty a
val) -> Specification
-> (Action -> Trace -> ValueMap -> Bool)
-> Trace
-> ValueMap
-> Bool
accept' Specification
s Action -> Trace -> ValueMap -> Bool
k Trace
t ValueMap
d
where val :: a
val = Var a -> String -> a
forall a. Var a -> String -> a
readValue Var a
x String
v
Trace
_ -> Bool
False
accept' (WriteOutput OptFlag
Optional Set (OutputPattern k)
os Specification
s') Action -> Trace -> ValueMap -> Bool
k Trace
t ValueMap
d = Specification
-> (Action -> Trace -> ValueMap -> Bool)
-> Trace
-> ValueMap
-> Bool
accept' (OptFlag -> Set (OutputPattern k) -> Specification -> Specification
forall (k :: PatternKind).
OptFlag -> Set (OutputPattern k) -> Specification -> Specification
WriteOutput OptFlag
Mandatory Set (OutputPattern k)
os Specification
s') Action -> Trace -> ValueMap -> Bool
k Trace
t ValueMap
d Bool -> Bool -> Bool
|| Specification
-> (Action -> Trace -> ValueMap -> Bool)
-> Trace
-> ValueMap
-> Bool
accept' Specification
s' Action -> Trace -> ValueMap -> Bool
k Trace
t ValueMap
d
accept' (WriteOutput OptFlag
Mandatory Set (OutputPattern k)
os Specification
s') Action -> Trace -> ValueMap -> Bool
k Trace
t ValueMap
d = case Trace
t of
ProgWrite OptFlag
Mandatory Set (OutputPattern 'TraceP)
vs Trace
t' | Set (OutputPattern 'TraceP)
vs Set (OutputPattern 'TraceP) -> Set (OutputPattern 'TraceP) -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` (OverflowWarning, Set (OutputPattern 'TraceP))
-> Set (OutputPattern 'TraceP)
forall a b. (a, b) -> b
snd (ValueMap
-> Set (OutputPattern k)
-> (OverflowWarning, Set (OutputPattern 'TraceP))
forall (k :: PatternKind).
ValueMap
-> Set (OutputPattern k)
-> (OverflowWarning, Set (OutputPattern 'TraceP))
evalPatternSet ValueMap
d Set (OutputPattern k)
os) -> Specification
-> (Action -> Trace -> ValueMap -> Bool)
-> Trace
-> ValueMap
-> Bool
accept' Specification
s' Action -> Trace -> ValueMap -> Bool
k Trace
t' ValueMap
d
Trace
_ -> Bool
False
accept' (Branch Term 'Transparent Bool
c Specification
s1 Specification
s2 Specification
s') Action -> Trace -> ValueMap -> Bool
k Trace
t ValueMap
d
| (OverflowWarning, Bool) -> Bool
forall a b. (a, b) -> b
snd (ValueMap -> Term 'Transparent Bool -> (OverflowWarning, Bool)
forall a (k :: TermKind).
Typeable a =>
ValueMap -> Term k a -> (OverflowWarning, a)
oEval ValueMap
d Term 'Transparent Bool
c) = Specification
-> (Action -> Trace -> ValueMap -> Bool)
-> Trace
-> ValueMap
-> Bool
accept' (Specification
s1 Specification -> Specification -> Specification
forall a. Semigroup a => a -> a -> a
<> Specification
s') Action -> Trace -> ValueMap -> Bool
k Trace
t ValueMap
d
| Bool
otherwise = Specification
-> (Action -> Trace -> ValueMap -> Bool)
-> Trace
-> ValueMap
-> Bool
accept' (Specification
s2 Specification -> Specification -> Specification
forall a. Semigroup a => a -> a -> a
<> Specification
s') Action -> Trace -> ValueMap -> Bool
k Trace
t ValueMap
d
accept' (TillE Specification
s Specification
s') Action -> Trace -> ValueMap -> Bool
k Trace
t ValueMap
d = Specification
-> (Action -> Trace -> ValueMap -> Bool)
-> Trace
-> ValueMap
-> Bool
accept' Specification
s Action -> Trace -> ValueMap -> Bool
k' Trace
t ValueMap
d
where
k' :: Action -> Trace -> ValueMap -> Bool
k' Action
End = Specification
-> (Action -> Trace -> ValueMap -> Bool)
-> Trace
-> ValueMap
-> Bool
accept' Specification
s Action -> Trace -> ValueMap -> Bool
k'
k' Action
Exit = Specification
-> (Action -> Trace -> ValueMap -> Bool)
-> Trace
-> ValueMap
-> Bool
accept' Specification
s' Action -> Trace -> ValueMap -> Bool
k
accept' Specification
E Action -> Trace -> ValueMap -> Bool
k Trace
t ValueMap
d = Action -> Trace -> ValueMap -> Bool
k Action
Exit Trace
t ValueMap
d
accept' Specification
Nop Action -> Trace -> ValueMap -> Bool
k Trace
t ValueMap
d = Action -> Trace -> ValueMap -> Bool
k Action
End Trace
t ValueMap
d
k_I :: Action -> Trace -> ValueMap -> Bool
k_I :: Action -> Trace -> ValueMap -> Bool
k_I Action
End Trace
Terminate ValueMap
_ = Bool
True
k_I Action
End Trace
_ ValueMap
_ = Bool
False
k_I Action
Exit Trace
_ ValueMap
_ = String -> Bool
forall a. HasCallStack => String -> a
error String
"ill-formed specification: exit marker at top-level"
d_I :: ValueMap
d_I :: ValueMap
d_I = [SomeVar] -> ValueMap
emptyValueMap ([SomeVar] -> ValueMap) -> [SomeVar] -> ValueMap
forall a b. (a -> b) -> a -> b
$ Specification -> [SomeVar]
readVars Specification
s_
instance Arbitrary Specification where
arbitrary :: Gen Specification
arbitrary = Gen Specification
specGen
shrink :: Specification -> [Specification]
shrink = Specification -> [Specification]
shrinkSpec
data LoopBody = LoopBody { LoopBody -> Specification
body :: Specification, LoopBody -> Specification
progress :: Specification}
instance Show LoopBody where
show :: LoopBody -> String
show (LoopBody Specification
b Specification
p) = [String] -> String
unlines
[ String
"LoopBody {"
, String
" body = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
render (Specification -> Doc
pPrintSpecification Specification
b) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
","
, String
" progress = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
render (Specification -> Doc
pPrintSpecification Specification
p)
, String
"}"
]
instance Arbitrary LoopBody where
arbitrary :: Gen LoopBody
arbitrary = (Specification -> Specification -> LoopBody)
-> (Specification, Specification) -> LoopBody
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Specification -> Specification -> LoopBody
LoopBody ((Specification, Specification) -> LoopBody)
-> Gen (Specification, Specification) -> Gen LoopBody
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Specification, Specification)
loopBodyGen