{-# 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

-- | The 'anyOptionalOutput' function represents a specification for writing
-- arbitrary optional output. The output can be anything, as indicated by the
-- use of the 'wildcard' pattern in its definition:
--
-- > anyOptionalOutput = writeOptionalOutput [wildcard]
anyOptionalOutput :: Specification
anyOptionalOutput :: Specification
anyOptionalOutput = [OutputPattern Any] -> Specification
forall (k :: PatternKind). [OutputPattern k] -> Specification
writeOptionalOutput [OutputPattern Any
forall (k :: PatternKind). OutputPattern k
Wildcard]

-- | Represents a branching structure in a specification.
--
-- * The first 'Specification' argument is the "then-case".
-- * The second 'Specification' argument is the "else-case".
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

-- | Represents a loop structure in a specification, performing the body while the condition does not hold.
--
-- The 'whileNot' function takes a condition and a body specification, and constructs a loop structure where:
--
-- * The 'Term' @'@'Transparent' 'Bool' argument is the condition to be evaluated at the beginning of each iteration. The loop continues as long as the condition is 'False'.
-- * The 'Specification' argument is the body of the loop, executed while the condition is 'False'.
--
-- The function assumes that the body specification does not contain a top-level 'exit' marker.
--
-- > whileNot c bdy = tillExit (branch c exit bdy)
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

-- | Represents a loop structure in a specification, performing the body while the condition holds.
--
-- The 'while' function takes a condition and a body specification, and constructs a loop structure where:
--
-- * The 'Term' @'@'Transparent' 'Bool' argument is the condition to be evaluated at the beginning of each iteration. The loop continues as long as the condition is 'True'.
-- * The 'Specification' argument is the body of the loop, executed while the condition is 'True'.
--
-- The function assumes that the body specification does not contain a top-level 'exit' marker.
--
-- > while c bdy = tillExit (branch c bdy exit)
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

-- | Represents a loop structure in a specification, performing the body at least once and then further while the condition does not hold.
--
-- The 'repeatUntil' function takes a body specification and a condition, and constructs a loop structure where:
--
-- * The 'Specification' argument is the body of the loop, executed at least once and then further times while the condition is 'False'.
-- * The 'Term' @'@'Transparent' 'Bool' argument is the condition to be evaluated at the end of each iteration. The loop continues until the condition becomes 'True'.
--
-- The function assumes that the body specification does not contain a top-level 'exit' marker.
--
-- > repeatUntil bdy c = tillExit (bdy <> branch c exit nop)
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

-- | Represents a loop structure in a specification, performing the body at least once and then further while the condition holds.
--
-- The 'doWhile' function takes a body specification and a condition, and constructs a loop structure where:
--
-- * The 'Specification' argument is the body of the loop, executed at least once and then further times while the condition is 'True'.
-- * The 'Term' @'@'Transparent' 'Bool' argument is the condition to be evaluated at the end of each iteration. The loop continues until the condition becomes 'False'.
--
-- The function assumes that the body specification does not contain a top-level 'exit' marker.
--
-- > doWhile bdy c = tillExit (bdy <> branch c nop exit)
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)"
        ]

  -- the next case works without context information for the four loop constructors currently defined ()
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

-- using () as a stand-in for E
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_

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