{-# LANGUAGE TupleSections #-}
module Language.EFLINT.Parse where
import Language.EFLINT.Spec
import GLL.Combinators hiding (many, some, IntLit, BoolLit, StringLit)
import Text.Regex.Applicative hiding ((<**>), optional)
import Data.Char (isLower)
import qualified Data.Map as M
flint_lexer :: String -> Either String [Token]
flint_lexer :: DomId -> Either DomId [Token]
flint_lexer = forall t.
SubsumesToken t =>
LexerSettings -> DomId -> Either DomId [t]
lexerEither LexerSettings
lexer_settings
lexer_settings :: LexerSettings
lexer_settings :: LexerSettings
lexer_settings = LexerSettings
emptyLanguage {
identifiers :: RE Char DomId
identifiers = RE Char DomId
types
, keywords :: [DomId]
keywords = [DomId
"!?",DomId
"||", DomId
"&&", DomId
"<=", DomId
">=", DomId
"..", DomId
"True", DomId
"False", DomId
"Sum", DomId
"==", DomId
"!=", DomId
"When", DomId
"Where",DomId
"Holds when", DomId
"Holds", DomId
"Present when", DomId
"Present", DomId
"Max", DomId
"Min", DomId
"Count", DomId
"Union", DomId
"Enabled", DomId
"Violated when", DomId
"Violated"
, DomId
"Atom", DomId
"String", DomId
"Int", DomId
"Time", DomId
"Current Time"
, DomId
"Exists", DomId
"Forall", DomId
"Foreach", DomId
"Force"
, DomId
"Extend", DomId
"Event", DomId
"Act", DomId
"Fact", DomId
"Physical", DomId
"Bool", DomId
"Var", DomId
"Function", DomId
"Invariant", DomId
"Predicate", DomId
"Duty", DomId
"Actor", DomId
"Holder", DomId
"Claimant", DomId
"Recipient", DomId
"Related to", DomId
"Conditioned by", DomId
"Creates", DomId
"Terminates", DomId
"Obfuscates", DomId
"Terminated by", DomId
"Created by", DomId
"With" , DomId
"Identified by", DomId
"Derived from", DomId
"Derived externally", DomId
"Enforced by", DomId
"Syncs with"
, DomId
"Do", DomId
"Placeholder", DomId
"For", DomId
"Not", DomId
"Open", DomId
"Closed", DomId
"?-", DomId
"?--"
, DomId
"#", DomId
"##", DomId
"###", DomId
"####"
, DomId
"#include", DomId
"#require"
]
, keychars :: DomId
keychars = [Char
'[', Char
']', Char
'(', Char
')', Char
'!', Char
',', Char
'\'', Char
'+', Char
'-', Char
'*', Char
'/', Char
'.', Char
'=', Char
'>', Char
'<', Char
':', Char
'?', Char
'{', Char
'}', Char
'%', Char
'~']
}
where types :: RE Char DomId
types = (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
RE Char DomId
word forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (forall a. [a] -> [a] -> [a]
(++) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (f :: * -> *) a. Alternative f => f a -> f [a]
some ((forall a. a -> [a] -> [a]
:[]) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s. (s -> Bool) -> RE s s
psym (forall a. Eq a => a -> a -> Bool
== Char
' '))) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RE Char DomId
word) forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
(\DomId
id -> DomId
"[" forall a. [a] -> [a] -> [a]
++ DomId
id forall a. [a] -> [a] -> [a]
++ DomId
"]") forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall s. Eq s => s -> RE s s
sym Char
'[' forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Alternative f => f a -> f [a]
many RE Char Char
internal forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* forall s. Eq s => s -> RE s s
sym Char
']' forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
(\DomId
id -> DomId
"<" forall a. [a] -> [a] -> [a]
++ DomId
id forall a. [a] -> [a] -> [a]
++ DomId
">") forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall s. Eq s => s -> RE s s
sym Char
'<' forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RE Char DomId
act_or_duty forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* forall s. Eq s => s -> RE s s
sym Char
'>'
where word :: RE Char DomId
word = (\Char
c [DomId]
ss -> Char
cforall a. a -> [a] -> [a]
:forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [DomId]
ss) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s. (s -> Bool) -> RE s s
psym Char -> Bool
isLower forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Alternative f => f a -> f [a]
many ((forall a. a -> [a] -> [a]
:[]) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s. (s -> Bool) -> RE s s
psym Char -> Bool
isLower forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> RE Char DomId
hyphen forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ((forall a. a -> [a] -> [a]
:[]) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s. Eq s => s -> RE s s
sym Char
'_'))
where hyphen :: RE Char DomId
hyphen = (\Char
c1 Char
c2 -> [Char
c1,Char
c2]) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s. Eq s => s -> RE s s
sym Char
'-' forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall s. (s -> Bool) -> RE s s
psym Char -> Bool
isLower
act_or_duty :: RE Char DomId
act_or_duty = (\DomId
id -> DomId
"<" forall a. [a] -> [a] -> [a]
++ DomId
id forall a. [a] -> [a] -> [a]
++ DomId
">") forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall s. Eq s => s -> RE s s
sym Char
'<' forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Alternative f => f a -> f [a]
many RE Char Char
internal forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* forall s. Eq s => s -> RE s s
sym Char
'>'
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s. (s -> Bool) -> RE s s
psym (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem DomId
"< =") forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Alternative f => f a -> f [a]
many RE Char Char
internal
internal :: RE Char Char
internal = forall s. (s -> Bool) -> RE s s
psym (\Char
c -> Bool -> Bool
not (Char
c forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` DomId
"]>+="))
value_expr :: BNF Token Term
value_expr :: BNF Token Term
value_expr = DomId
"value-expr"
forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<::= Bool -> Term
BoolLit Bool
True forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"True"
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Bool -> Term
BoolLit Bool
False forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"False"
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Term -> Term -> Term
When forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token Term
value_expr forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** BNF Token DomId
keyword_when forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> BNF Token Term
value_expr
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Term -> Term -> Term
Or forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token Term
value_expr forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"||" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<<<**> BNF Token Term
value_expr
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Term -> Term -> Term
And forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token Term
value_expr forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"&&" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<<<**> BNF Token Term
value_expr
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Term -> Term -> Term
Eq forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token Term
value_expr forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"==" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> BNF Token Term
value_expr
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Term -> Term -> Term
Neq forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token Term
value_expr forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"!=" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> BNF Token Term
value_expr
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Term -> Term -> Term
Leq forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token Term
value_expr forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"<=" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<<<**> BNF Token Term
value_expr
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Term -> Term -> Term
Geq forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token Term
value_expr forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
">=" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<<<**> BNF Token Term
value_expr
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Term -> Term -> Term
Le forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token Term
value_expr forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
'<' forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<<<**> BNF Token Term
value_expr
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Term -> Term -> Term
Ge forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token Term
value_expr forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
'>' forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<<<**> BNF Token Term
value_expr
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Term -> Term -> Term
Sub forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token Term
value_expr forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
'-' forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**>>> BNF Token Term
value_expr
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Term -> Term -> Term
Add forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token Term
value_expr forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
'+' forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**>>> BNF Token Term
value_expr
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Term -> Term -> Term
Mult forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token Term
value_expr forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
'*' forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**>>> BNF Token Term
value_expr
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Term -> Term -> Term
Mod forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token Term
value_expr forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
'%' forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**>>> BNF Token Term
value_expr
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Term -> Term -> Term
Div forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token Term
value_expr forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
'/' forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**>>> BNF Token Term
value_expr
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Term -> Term
Not forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
'!' forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> BNF Token Term
value_expr
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Term -> Term
Not forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Not" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> BNF Token Term
value_expr
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Sum" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t b
**> forall a. ([Var] -> Term -> a) -> BNF Token a
foreach [Var] -> Term -> Term
Sum
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Count" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t b
**> forall a. ([Var] -> Term -> a) -> BNF Token a
foreach [Var] -> Term -> Term
Count
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Max" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t b
**> forall a. ([Var] -> Term -> a) -> BNF Token a
foreach [Var] -> Term -> Term
Max
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Min" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t b
**> forall a. ([Var] -> Term -> a) -> BNF Token a
foreach [Var] -> Term -> Term
Min
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Int -> Term
IntLit forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> forall t. SubsumesToken t => SymbExpr t Int
int_lit
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> DomId -> Term
StringLit forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token DomId
atom
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Var -> Term
Ref forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token Var
var
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> forall a. (DomId -> Arguments -> a) -> BNF Token a
application DomId -> Arguments -> Term
App
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Term -> Var -> Term
Project forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token Term
value_expr forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
'.' forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> (BNF Token Var
var forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> forall {t} {s :: * -> * -> *} {b}.
(Show t, Ord t, IsSymbExpr s, SubsumesToken t) =>
s t b -> BNF t b
parens BNF Token Var
var)
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Term -> DomId -> Term
Tag forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token Term
value_expr forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
':' forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> forall t. SubsumesToken t => SymbExpr t DomId
id_lit
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> forall {t} {s :: * -> * -> *} {b}.
(Show t, Ord t, IsSymbExpr s, SubsumesToken t) =>
s t b -> BNF t b
parens ([Var] -> Term -> Term
Exists forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Exists" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> forall t (s :: * -> * -> *) (s2 :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s, IsSymbExpr s2, IsAltExpr s2) =>
s t a -> s2 t b -> SymbExpr t [a]
multipleSepBy1 BNF Token Var
var (forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
',') forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
':' forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> BNF Token Term
value_expr)
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> forall {t} {s :: * -> * -> *} {b}.
(Show t, Ord t, IsSymbExpr s, SubsumesToken t) =>
s t b -> BNF t b
parens ([Var] -> Term -> Term
Forall forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Forall" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> forall t (s :: * -> * -> *) (s2 :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s, IsSymbExpr s2, IsAltExpr s2) =>
s t a -> s2 t b -> SymbExpr t [a]
multipleSepBy1 BNF Token Var
var (forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
',') forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
':' forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> BNF Token Term
value_expr)
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Term -> Term
Present forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Present" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> BNF Token Term
value_expr
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Term -> Term
Present forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Holds" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> BNF Token Term
value_expr
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Term -> Term
Violated forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Violated" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> BNF Token Term
value_expr
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Term -> Term
Enabled forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Enabled" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> BNF Token Term
value_expr
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> forall {t} {s :: * -> * -> *} {b}.
(Show t, Ord t, IsSymbExpr s, SubsumesToken t) =>
s t b -> BNF t b
parens BNF Token Term
value_expr
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Term
CurrentTime forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Current Time"
keyword_when :: BNF Token String
keyword_when :: BNF Token DomId
keyword_when = DomId
"when-or-where" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Where" forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"When"
var :: BNF Token Var
var :: BNF Token Var
var = DomId
"decorated-type-lit"
forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> DomId -> DomId -> Var
Var forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> forall t. SubsumesToken t => SymbExpr t DomId
id_lit forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> BNF Token DomId
decoration
atom :: BNF Token String
atom :: BNF Token DomId
atom = DomId
"atom" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> forall t. SubsumesToken t => SymbExpr t DomId
string_lit forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> forall t. SubsumesToken t => SymbExpr t DomId
alt_id_lit
decoration :: BNF Token String
decoration :: BNF Token DomId
decoration = DomId
"decoration"
forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> forall {a}. Show a => Maybe a -> DomId -> DomId
make_f forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> forall t (s :: * -> * -> *) a.
(Show t, Ord t, IsSymbExpr s) =>
s t a -> SymbExpr t (Maybe a)
optional forall t. SubsumesToken t => SymbExpr t Int
int_lit forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> forall t (s :: * -> * -> *) a.
(Show t, Ord t, IsSymbExpr s) =>
s t a -> SymbExpr t [a]
multiple (forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
'\'')
where make_f :: Maybe a -> DomId -> DomId
make_f Maybe a
mi DomId
str = forall b a. b -> (a -> b) -> Maybe a -> b
maybe DomId
"" forall a. Show a => a -> DomId
show Maybe a
mi forall a. [a] -> [a] -> [a]
++ DomId
str
arguments :: BNF Token Arguments
arguments :: BNF Token Arguments
arguments = DomId
"arguments"
forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> forall {t} {s :: * -> * -> *} {b}.
(Show t, Ord t, IsSymbExpr s, SubsumesToken t) =>
s t b -> BNF t b
parens ( forall a b. b -> Either a b
Right forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> forall t (s :: * -> * -> *) (s2 :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s, IsSymbExpr s2, IsAltExpr s2) =>
s t a -> s2 t b -> SymbExpr t [a]
multipleSepBy BNF Token Modifier
modifier (forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
',')
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> forall a b. a -> Either a b
Left forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> forall t (s :: * -> * -> *) (s2 :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s, IsSymbExpr s2, IsAltExpr s2) =>
s t a -> s2 t b -> SymbExpr t [a]
multipleSepBy1 BNF Token Term
value_expr (forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
',') )
modifier :: BNF Token Modifier
modifier :: BNF Token Modifier
modifier = DomId
"modifier"
forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> Var -> Term -> Modifier
Rename forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token Var
var forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
'=' forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> BNF Token Term
value_expr
type_expr :: BNF Token Domain
type_expr :: BNF Token Domain
type_expr = DomId
"type-expr"
forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<::= [Var] -> Domain
Products forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. a -> [a] -> [a]
:[]) forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token Var
var
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> [DomId] -> Domain
Strings forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> forall {t} {s2 :: * -> * -> *} {s :: * -> * -> *} {a} {b}.
(Show t, Ord t, IsSymbExpr s2, IsSymbExpr s, IsAltExpr s2) =>
s t a -> s2 t b -> BNF t [a]
manySepBy2 BNF Token DomId
atom (forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
'+' forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
',')
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> [Int] -> Domain
Ints forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> forall {t} {s2 :: * -> * -> *} {s :: * -> * -> *} {a} {b}.
(Show t, Ord t, IsSymbExpr s2, IsSymbExpr s, IsAltExpr s2) =>
s t a -> s2 t b -> BNF t [a]
manySepBy2 forall t. SubsumesToken t => SymbExpr t Int
int_lit (forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
'+' forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
',')
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> [Var] -> Domain
Products forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> forall {t} {s2 :: * -> * -> *} {s :: * -> * -> *} {a} {b}.
(Show t, Ord t, IsSymbExpr s2, IsSymbExpr s, IsAltExpr s2) =>
s t a -> s2 t b -> BNF t [a]
manySepBy2 BNF Token Var
var (forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
'*')
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> forall {t} {s :: * -> * -> *} {b}.
(Show t, Ord t, IsSymbExpr s, SubsumesToken t) =>
s t b -> BNF t b
parens ([Var] -> Domain
Products forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> forall {t} {s2 :: * -> * -> *} {s :: * -> * -> *} {a} {b}.
(Show t, Ord t, IsSymbExpr s2, IsSymbExpr s, IsAltExpr s2) =>
s t a -> s2 t b -> BNF t [a]
manySepBy2 BNF Token Var
var (forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
'*'))
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> [Int] -> Domain
Ints forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. a -> [a] -> [a]
:[]) forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> forall t. SubsumesToken t => SymbExpr t Int
int_lit
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Int -> Int -> Domain
ints_from_domain forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> forall t. SubsumesToken t => SymbExpr t Int
int_lit forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
".." forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> forall t. SubsumesToken t => SymbExpr t Int
int_lit
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> [DomId] -> Domain
Strings forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. a -> [a] -> [a]
:[]) forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token DomId
atom
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Char -> Char -> Domain
strings_from_domain forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> forall t. SubsumesToken t => SymbExpr t Char
char_lit forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
".." forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> forall t. SubsumesToken t => SymbExpr t Char
char_lit
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Domain
AnyString forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"String"
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Domain
AnyString forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Atom"
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Domain
AnyInt forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Int"
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Domain
Time forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Time"
where ints_from_domain :: Int -> Int -> Domain
ints_from_domain :: Int -> Int -> Domain
ints_from_domain Int
min Int
max = [Int] -> Domain
Ints forall a b. (a -> b) -> a -> b
$ [Int
min..Int
max]
strings_from_domain :: Char -> Char -> Domain
strings_from_domain :: Char -> Char -> Domain
strings_from_domain Char
min Char
max = [DomId] -> Domain
Strings forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. a -> [a] -> [a]
:[]) [Char
min..Char
max]
parse_component :: BNF Token a -> String -> Either String a
parse_component :: forall a. BNF Token a -> DomId -> Either DomId a
parse_component BNF Token a
p DomId
str = case DomId -> Either DomId [Token]
flint_lexer DomId
str of
Left DomId
err -> forall a b. a -> Either a b
Left DomId
err
Right [Token]
ts -> case forall t (s :: * -> * -> *) a.
(Show t, Parseable t, IsSymbExpr s) =>
CombinatorOptions -> s t a -> [t] -> Either DomId [a]
parseWithOptionsAndError [Int -> CombinatorOption
maximumErrors Int
1] BNF Token a
p [Token]
ts of
Left DomId
err -> forall a b. a -> Either a b
Left DomId
err
Right [a]
as -> forall a b. b -> Either a b
Right (forall a. [a] -> a
head [a]
as)
flint :: BNF Token (Spec, Refiner, Initialiser, Scenario)
flint :: BNF Token (Spec, Refiner, Initialiser, Scenario)
flint = DomId
"flint" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> forall {b} {c} {d}. [Decl] -> b -> c -> d -> (Spec, b, c, d)
cons forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$
forall t (s :: * -> * -> *) a.
(Show t, Ord t, IsSymbExpr s) =>
s t a -> SymbExpr t (Maybe a)
optional (forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"#") forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> BNF Token [Decl]
declarations forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**>
forall t (s :: * -> * -> *) a.
(Show t, Ord t, IsSymbExpr s) =>
s t a -> a -> SymbExpr t a
optionalWithDef (forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"##" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t b
**> BNF Token Refiner
refiner) forall k a. Map k a
M.empty forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**>
forall t (s :: * -> * -> *) a.
(Show t, Ord t, IsSymbExpr s) =>
s t a -> a -> SymbExpr t a
optionalWithDef (forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"###" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t b
**> BNF Token Initialiser
initialiser) [] forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**>
forall t (s :: * -> * -> *) a.
(Show t, Ord t, IsSymbExpr s) =>
s t a -> a -> SymbExpr t a
optionalWithDef (forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"####" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t b
**> BNF Token Scenario
scenario) []
where cons :: [Decl] -> b -> c -> d -> (Spec, b, c, d)
cons [Decl]
ds b
r c
i d
s = ([Decl] -> Spec -> Spec
extend_spec [Decl]
ds Spec
emptySpec, b
r, c
i, d
s)
parse_flint :: DomId -> Either DomId (Spec, Refiner, Initialiser, Scenario)
parse_flint = forall a. BNF Token a -> DomId -> Either DomId a
parse_component BNF Token (Spec, Refiner, Initialiser, Scenario)
flint
declarations :: BNF Token [Decl]
declarations :: BNF Token [Decl]
declarations = DomId
"declarations" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> forall t (s :: * -> * -> *) a.
(Show t, Ord t, IsSymbExpr s) =>
s t a -> SymbExpr t [a]
multiple1 BNF Token [Decl]
frame
placeholder :: BNF Token Decl
placeholder :: BNF Token Decl
placeholder = DomId
"placeholder-decl" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> DomId -> DomId -> Decl
PlaceholderDecl forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Placeholder" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> forall t. SubsumesToken t => SymbExpr t DomId
id_lit forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"For" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> forall t. SubsumesToken t => SymbExpr t DomId
id_lit
frame :: BNF Token [Decl]
frame :: BNF Token [Decl]
frame = DomId
"frame" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> AltExprs Token [Decl]
fact
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> BNF Token [Decl]
duty
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> BNF Token [Decl]
act
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> BNF Token [Decl]
physical
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> BNF Token [Decl]
event
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> (forall a. a -> [a] -> [a]
:[]) forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token Decl
syn_ext
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> (forall a. a -> [a] -> [a]
:[]) forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token Decl
placeholder
where fact :: AltExprs Token [Decl]
fact = forall a.
(Bool
-> Maybe Restriction
-> DomId
-> Domain
-> Term
-> [ModClause]
-> a)
-> BNF Token a
syn_fact_decl (Bool
-> Bool
-> Bool
-> Maybe Restriction
-> DomId
-> Domain
-> Term
-> [ModClause]
-> [Decl]
make_fact Bool
False Bool
False)
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> forall a. (Bool -> DomId -> [ModClause] -> a) -> BNF Token a
syn_bool_fact_decl Bool -> DomId -> [ModClause] -> [Decl]
make_bool_fact
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> forall a.
(Bool -> DomId -> Domain -> Term -> [ModClause] -> a)
-> BNF Token a
syn_actor_decl (\Bool
d -> Bool
-> Bool
-> Bool
-> Maybe Restriction
-> DomId
-> Domain
-> Term
-> [ModClause]
-> [Decl]
make_fact Bool
False Bool
True Bool
d forall a. Maybe a
Nothing)
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> forall a. (DomId -> Term -> a) -> BNF Token a
syn_pred_decl (Bool -> DomId -> Term -> [Decl]
make_pred Bool
False)
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> forall a. (DomId -> Term -> a) -> BNF Token a
syn_inv_decl DomId -> Term -> [Decl]
make_inv
where make_fact :: Bool -> Bool -> Bool -> Maybe Restriction -> DomId -> Domain -> Term -> [ModClause] -> [Decl]
make_fact :: Bool
-> Bool
-> Bool
-> Maybe Restriction
-> DomId
-> Domain
-> Term
-> [ModClause]
-> [Decl]
make_fact Bool
inv Bool
is_actor Bool
is_closed Maybe Restriction
restr DomId
ty Domain
dom Term
dom_filter [ModClause]
clauses =
[DomId -> TypeSpec -> Decl
TypeDecl DomId
ty TypeSpec
tspec, DomId -> [ModClause] -> Decl
TypeExt DomId
ty [ModClause]
clauses]
where tspec :: TypeSpec
tspec = TypeSpec { kind :: Kind
kind = FactSpec -> Kind
Fact (Bool -> Bool -> FactSpec
FactSpec Bool
inv Bool
is_actor)
, domain :: Domain
domain = Domain
dom
, domain_constraint :: Term
domain_constraint = Term
dom_filter
, restriction :: Maybe Restriction
restriction = Maybe Restriction
restr
, derivation :: [Derivation]
derivation = []
, closed :: Bool
closed = Bool
is_closed
, conditions :: [Term]
conditions = [] }
make_pred :: Bool -> DomId -> Term -> [Decl]
make_pred Bool
inv DomId
ty Term
t = Bool
-> Bool
-> Bool
-> Maybe Restriction
-> DomId
-> Domain
-> Term
-> [ModClause]
-> [Decl]
make_fact Bool
inv Bool
False Bool
True forall a. Maybe a
Nothing DomId
ty ([Var] -> Domain
Products []) (Bool -> Term
BoolLit Bool
True) [[Derivation] -> ModClause
DerivationCl [Term -> Derivation
HoldsWhen Term
t]]
make_inv :: DomId -> Term -> [Decl]
make_inv DomId
ty Term
t = Bool -> DomId -> Term -> [Decl]
make_pred Bool
True DomId
ty Term
t
make_bool_fact :: Bool -> DomId -> [ModClause] -> [Decl]
make_bool_fact Bool
is_closed DomId
ty [ModClause]
clauses =
Bool
-> Bool
-> Bool
-> Maybe Restriction
-> DomId
-> Domain
-> Term
-> [ModClause]
-> [Decl]
make_fact Bool
False Bool
False Bool
is_closed forall a. Maybe a
Nothing DomId
ty ([Var] -> Domain
Products []) (Bool -> Term
BoolLit Bool
True) [ModClause]
clauses
act :: BNF Token [Decl]
act = forall a.
(Bool
-> DomId
-> Maybe Var
-> Maybe Var
-> [Var]
-> Term
-> [ModClause]
-> a)
-> BNF Token a
syn_act_decl Bool
-> DomId
-> Maybe Var
-> Maybe Var
-> [Var]
-> Term
-> [ModClause]
-> [Decl]
make_act
where make_act :: Bool
-> DomId
-> Maybe Var
-> Maybe Var
-> [Var]
-> Term
-> [ModClause]
-> [Decl]
make_act Bool
is_closed DomId
ty Maybe Var
mact Maybe Var
mrec [Var]
attrs Term
dom_filter [ModClause]
clauses =
[DomId -> TypeSpec -> Decl
TypeDecl DomId
ty TypeSpec
tspec, DomId -> [ModClause] -> Decl
TypeExt DomId
ty [ModClause]
clauses]
where tspec :: TypeSpec
tspec = TypeSpec {
kind :: Kind
kind = ActSpec -> Kind
Act (ActSpec {effects :: Initialiser
effects = [], syncs :: [Sync]
syncs = [], physical :: Bool
physical = Bool
False } ),
domain :: Domain
domain = [Var] -> Domain
Products (Var
actorforall a. a -> [a] -> [a]
:(forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (forall a. a -> [a] -> [a]
:[]) Maybe Var
mrec forall a. [a] -> [a] -> [a]
++ [Var]
attrs)),
domain_constraint :: Term
domain_constraint = Term
dom_filter,
restriction :: Maybe Restriction
restriction = forall a. Maybe a
Nothing,
derivation :: [Derivation]
derivation = [],
closed :: Bool
closed = Bool
is_closed,
conditions :: [Term]
conditions = [] }
actor :: Var
actor = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (DomId -> Var
no_decoration DomId
"actor") forall a. a -> a
id Maybe Var
mact
physical :: BNF Token [Decl]
physical = forall a.
(DomId -> Maybe Var -> [Var] -> Term -> [ModClause] -> a)
-> BNF Token a
syn_physical_decl DomId -> Maybe Var -> [Var] -> Term -> [ModClause] -> [Decl]
make_physical
where make_physical :: DomId -> Maybe Var -> [Var] -> Term -> [ModClause] -> [Decl]
make_physical DomId
ty Maybe Var
mact [Var]
attrs Term
dom_filter [ModClause]
clauses =
[DomId -> TypeSpec -> Decl
TypeDecl DomId
ty TypeSpec
tspec, DomId -> [ModClause] -> Decl
TypeExt DomId
ty (ModClause
holds_trueforall a. a -> [a] -> [a]
:[ModClause]
clauses)]
where tspec :: TypeSpec
tspec = TypeSpec {
kind :: Kind
kind = ActSpec -> Kind
Act (ActSpec { effects :: Initialiser
effects = [], syncs :: [Sync]
syncs = [], physical :: Bool
physical = Bool
True }),
domain :: Domain
domain = [Var] -> Domain
Products (Var
actorforall a. a -> [a] -> [a]
:[Var]
attrs),
domain_constraint :: Term
domain_constraint = Term
dom_filter,
restriction :: Maybe Restriction
restriction = forall a. Maybe a
Nothing,
derivation :: [Derivation]
derivation = [],
closed :: Bool
closed = Bool
True,
conditions :: [Term]
conditions = [] }
actor :: Var
actor = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (DomId -> Var
no_decoration DomId
"actor") forall a. a -> a
id Maybe Var
mact
holds_true :: ModClause
holds_true = [Derivation] -> ModClause
DerivationCl [Term -> Derivation
HoldsWhen (Bool -> Term
BoolLit Bool
True)]
event :: BNF Token [Decl]
event = forall a.
(Bool -> DomId -> [Var] -> Term -> [ModClause] -> a) -> BNF Token a
syn_event_decl Bool -> DomId -> [Var] -> Term -> [ModClause] -> [Decl]
make_event
where make_event :: Bool -> DomId -> [Var] -> Term -> [ModClause] -> [Decl]
make_event Bool
is_closed DomId
ty [Var]
attrs Term
dom_filter [ModClause]
clauses =
[DomId -> TypeSpec -> Decl
TypeDecl DomId
ty TypeSpec
tspec, DomId -> [ModClause] -> Decl
TypeExt DomId
ty [ModClause]
clauses]
where tspec :: TypeSpec
tspec = TypeSpec {
kind :: Kind
kind = EventSpec -> Kind
Event (EventSpec { event_effects :: Initialiser
event_effects = [], event_syncs :: [Sync]
event_syncs = [] })
, domain :: Domain
domain = [Var] -> Domain
Products [Var]
attrs
, domain_constraint :: Term
domain_constraint = Term
dom_filter
, restriction :: Maybe Restriction
restriction = forall a. Maybe a
Nothing
, derivation :: [Derivation]
derivation = []
, closed :: Bool
closed = Bool
is_closed
, conditions :: [Term]
conditions = []
}
duty :: BNF Token [Decl]
duty = forall a.
(Bool -> DomId -> Var -> Var -> [Var] -> Term -> [ModClause] -> a)
-> BNF Token a
syn_duty_decl Bool
-> DomId -> Var -> Var -> [Var] -> Term -> [ModClause] -> [Decl]
make_duty
where make_duty :: Bool
-> DomId -> Var -> Var -> [Var] -> Term -> [ModClause] -> [Decl]
make_duty Bool
is_closed DomId
ty Var
hold Var
claim [Var]
attrs Term
dom_filter [ModClause]
clauses =
[DomId -> TypeSpec -> Decl
TypeDecl DomId
ty TypeSpec
tspec, DomId -> [ModClause] -> Decl
TypeExt DomId
ty [ModClause]
clauses]
where tspec :: TypeSpec
tspec = TypeSpec {
domain :: Domain
domain = [Var] -> Domain
Products (Var
holdforall a. a -> [a] -> [a]
:Var
claimforall a. a -> [a] -> [a]
:[Var]
attrs),
domain_constraint :: Term
domain_constraint = Term
dom_filter,
restriction :: Maybe Restriction
restriction = forall a. Maybe a
Nothing,
kind :: Kind
kind = DutySpec -> Kind
Duty (DutySpec { violated_when :: [Term]
violated_when = [], enforcing_acts :: [DomId]
enforcing_acts = []
, terminating_acts :: [DomId]
terminating_acts = [], creating_acts :: [DomId]
creating_acts = [] }),
derivation :: [Derivation]
derivation = [],
closed :: Bool
closed = Bool
is_closed,
conditions :: [Term]
conditions = []}
syn_fact_decl :: (Bool -> Maybe Restriction -> DomId -> Domain -> Term -> [ModClause] -> a) -> BNF Token a
syn_fact_decl :: forall a.
(Bool
-> Maybe Restriction
-> DomId
-> Domain
-> Term
-> [ModClause]
-> a)
-> BNF Token a
syn_fact_decl Bool
-> Maybe Restriction -> DomId -> Domain -> Term -> [ModClause] -> a
cons = DomId
"fact-type-decl" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> Bool
-> Maybe Restriction -> DomId -> Domain -> Term -> [ModClause] -> a
cons forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$>
BNF Token Bool
syn_is_closed forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> BNF Token (Maybe Restriction)
fact_restriction_by_keyword forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> forall t. SubsumesToken t => SymbExpr t DomId
id_lit forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**>
forall t (s :: * -> * -> *) a.
(Show t, Ord t, IsSymbExpr s) =>
s t a -> a -> SymbExpr t a
optionalWithDef (forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Identified by" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t b
**> BNF Token Domain
type_expr) Domain
AnyString forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**>
BNF Token Term
syn_domain_constraint forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**>
BNF Token [ModClause]
syn_fact_clauses
fact_restriction_by_keyword :: BNF Token (Maybe Restriction)
fact_restriction_by_keyword :: BNF Token (Maybe Restriction)
fact_restriction_by_keyword = DomId
"restricted-fact" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=>
forall a. Maybe a
Nothing forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Fact"
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> forall a. a -> Maybe a
Just Restriction
VarRestriction forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Var"
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> forall a. a -> Maybe a
Just Restriction
FunctionRestriction forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Function"
syn_bool_fact_decl :: (Bool -> DomId -> [ModClause] -> a) -> BNF Token a
syn_bool_fact_decl :: forall a. (Bool -> DomId -> [ModClause] -> a) -> BNF Token a
syn_bool_fact_decl Bool -> DomId -> [ModClause] -> a
cons = DomId
"bool-fact-type-decl" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> Bool -> DomId -> [ModClause] -> a
cons forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$>
BNF Token Bool
syn_is_closed forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Bool" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> forall t. SubsumesToken t => SymbExpr t DomId
id_lit forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> BNF Token [ModClause]
syn_fact_clauses
syn_ext :: BNF Token Decl
syn_ext :: BNF Token Decl
syn_ext = DomId
"type-ext" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=>
forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Extend" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t b
**> ( BNF Token Decl
syn_fact_ext
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> BNF Token Decl
syn_act_ext
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> BNF Token Decl
syn_duty_ext
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> BNF Token Decl
syn_event_ext )
syn_is_closed :: BNF Token Bool
syn_is_closed :: BNF Token Bool
syn_is_closed = DomId
"is-type-closed-modifier" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> forall t (s :: * -> * -> *) a.
(Show t, Ord t, IsSymbExpr s) =>
s t a -> a -> SymbExpr t a
optionalWithDef AltExprs Token Bool
alts Bool
True
where alts :: AltExprs Token Bool
alts = Bool
True forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Closed"
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Bool
False forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Open"
syn_fact_ext :: BNF Token Decl
syn_fact_ext :: BNF Token Decl
syn_fact_ext = DomId
"fact-type-ext" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> DomId -> [ModClause] -> Decl
TypeExt forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Fact" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> forall t. SubsumesToken t => SymbExpr t DomId
id_lit forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> BNF Token [ModClause]
syn_fact_clauses
syn_actor_decl :: (Bool -> DomId -> Domain -> Term -> [ModClause] -> a) -> BNF Token a
syn_actor_decl :: forall a.
(Bool -> DomId -> Domain -> Term -> [ModClause] -> a)
-> BNF Token a
syn_actor_decl Bool -> DomId -> Domain -> Term -> [ModClause] -> a
cons = DomId
"actor-type-decl" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> Bool -> DomId -> [Var] -> Term -> [ModClause] -> a
cons' forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$>
BNF Token Bool
syn_is_closed forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Actor" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> forall t. SubsumesToken t => SymbExpr t DomId
id_lit forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**>
forall t (s :: * -> * -> *) a.
(Show t, Ord t, IsSymbExpr s) =>
s t a -> a -> SymbExpr t a
optionalWithDef (forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"With" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t b
**> forall t (s :: * -> * -> *) (s2 :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s, IsSymbExpr s2, IsAltExpr s2) =>
s t a -> s2 t b -> SymbExpr t [a]
manySepBy1 BNF Token Var
var (forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
'*')) [] forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**>
BNF Token Term
syn_domain_constraint forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**>
BNF Token [ModClause]
syn_fact_clauses
where cons' :: Bool -> DomId -> [Var] -> Term -> [ModClause] -> a
cons' Bool
isc DomId
d [Var]
vars Term
t = Bool -> DomId -> Domain -> Term -> [ModClause] -> a
cons Bool
isc DomId
d ([Var] -> Domain
Products (DomId -> DomId -> Var
Var DomId
actor_ref_address DomId
"" forall a. a -> [a] -> [a]
: [Var]
vars)) Term
t
syn_pred_decl :: (DomId -> Term -> a) -> BNF Token a
syn_pred_decl :: forall a. (DomId -> Term -> a) -> BNF Token a
syn_pred_decl DomId -> Term -> a
cons = DomId
"pred-type-decl" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> DomId -> Term -> a
cons forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$
forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Predicate" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> forall t. SubsumesToken t => SymbExpr t DomId
id_lit forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** BNF Token DomId
keyword_when forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> BNF Token Term
value_expr
syn_inv_decl :: (DomId -> Term -> a) -> BNF Token a
syn_inv_decl :: forall a. (DomId -> Term -> a) -> BNF Token a
syn_inv_decl DomId -> Term -> a
cons = DomId
"inv-type-decl" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> DomId -> Term -> a
cons forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$
forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Invariant" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> forall t. SubsumesToken t => SymbExpr t DomId
id_lit forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** BNF Token DomId
keyword_when forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> BNF Token Term
value_expr
syn_domain_constraint :: BNF Token Term
syn_domain_constraint = forall t (s :: * -> * -> *) a.
(Show t, Ord t, IsSymbExpr s) =>
s t a -> a -> SymbExpr t a
optionalWithDef (BNF Token DomId
keyword_when forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t b
**> BNF Token Term
value_expr) (Bool -> Term
BoolLit Bool
True)
syn_duty_decl :: (Bool -> DomId -> Var -> Var -> [Var] -> Term -> [ModClause] -> a) -> BNF Token a
syn_duty_decl :: forall a.
(Bool -> DomId -> Var -> Var -> [Var] -> Term -> [ModClause] -> a)
-> BNF Token a
syn_duty_decl Bool -> DomId -> Var -> Var -> [Var] -> Term -> [ModClause] -> a
cons = DomId
"duty-type-decl" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> Bool -> DomId -> Var -> Var -> [Var] -> Term -> [ModClause] -> a
cons forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$>
BNF Token Bool
syn_is_closed forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Duty" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> forall t. SubsumesToken t => SymbExpr t DomId
id_lit forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t (s :: * -> * -> *) a.
(Show t, Ord t, IsSymbExpr s) =>
s t a -> SymbExpr t (Maybe a)
optional (forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"With") forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<**
forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Holder" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> BNF Token Var
var forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<**
forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Claimant" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> BNF Token Var
var forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**>
BNF Token [Var]
objects forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> BNF Token Term
syn_domain_constraint forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**>
BNF Token [ModClause]
syn_duty_clauses
syn_act_decl :: (Bool -> DomId -> Maybe Var -> Maybe Var -> [Var] -> Term -> [ModClause] -> a) -> BNF Token a
syn_act_decl :: forall a.
(Bool
-> DomId
-> Maybe Var
-> Maybe Var
-> [Var]
-> Term
-> [ModClause]
-> a)
-> BNF Token a
syn_act_decl Bool
-> DomId
-> Maybe Var
-> Maybe Var
-> [Var]
-> Term
-> [ModClause]
-> a
cons = DomId
"act-type-decl" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> Bool
-> DomId
-> Maybe Var
-> Maybe Var
-> [Var]
-> Term
-> [ModClause]
-> a
cons forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$>
BNF Token Bool
syn_is_closed forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Act" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> forall t. SubsumesToken t => SymbExpr t DomId
id_lit forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t (s :: * -> * -> *) a.
(Show t, Ord t, IsSymbExpr s) =>
s t a -> SymbExpr t (Maybe a)
optional (forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"With") forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**>
forall t (s :: * -> * -> *) a.
(Show t, Ord t, IsSymbExpr s) =>
s t a -> SymbExpr t (Maybe a)
optional (forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Actor" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t b
**> BNF Token Var
var) forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**>
forall t (s :: * -> * -> *) a.
(Show t, Ord t, IsSymbExpr s) =>
s t a -> SymbExpr t (Maybe a)
optional (forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Recipient" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t b
**> BNF Token Var
var) forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**>
BNF Token [Var]
objects forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> BNF Token Term
syn_domain_constraint forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**>
BNF Token [ModClause]
syn_event_clauses
syn_physical_decl :: (DomId -> Maybe Var -> [Var] -> Term -> [ModClause] -> a) -> BNF Token a
syn_physical_decl :: forall a.
(DomId -> Maybe Var -> [Var] -> Term -> [ModClause] -> a)
-> BNF Token a
syn_physical_decl DomId -> Maybe Var -> [Var] -> Term -> [ModClause] -> a
cons = DomId
"physical-type-decl" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> DomId -> Maybe Var -> [Var] -> Term -> [ModClause] -> a
cons forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$
forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Physical" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> forall t. SubsumesToken t => SymbExpr t DomId
id_lit forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t (s :: * -> * -> *) a.
(Show t, Ord t, IsSymbExpr s) =>
s t a -> SymbExpr t (Maybe a)
optional (forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"With") forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**>
forall t (s :: * -> * -> *) a.
(Show t, Ord t, IsSymbExpr s) =>
s t a -> SymbExpr t (Maybe a)
optional (forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Actor" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t b
**> BNF Token Var
var) forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**>
BNF Token [Var]
objects forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> BNF Token Term
syn_domain_constraint forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**>
BNF Token [ModClause]
syn_event_clauses
syn_act_ext :: BNF Token Decl
syn_act_ext :: BNF Token Decl
syn_act_ext = DomId
"act-type-ext" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> DomId -> [ModClause] -> Decl
TypeExt forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Act" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> forall t. SubsumesToken t => SymbExpr t DomId
id_lit forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> BNF Token [ModClause]
syn_event_clauses
syn_physical_ext :: BNF Token Decl
syn_physical_ext = DomId
"physical-type-ext" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> DomId -> [ModClause] -> Decl
TypeExt forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Physical" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> forall t. SubsumesToken t => SymbExpr t DomId
id_lit forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> BNF Token [ModClause]
syn_physical_clauses
syn_event_ext :: BNF Token Decl
syn_event_ext :: BNF Token Decl
syn_event_ext = DomId
"event-type-ext" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> DomId -> [ModClause] -> Decl
TypeExt forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Event" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> forall t. SubsumesToken t => SymbExpr t DomId
id_lit forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> BNF Token [ModClause]
syn_event_clauses
syn_duty_ext :: BNF Token Decl
syn_duty_ext :: BNF Token Decl
syn_duty_ext = DomId
"duty-type-ext" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> DomId -> [ModClause] -> Decl
TypeExt forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Duty" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> forall t. SubsumesToken t => SymbExpr t DomId
id_lit forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> BNF Token [ModClause]
syn_duty_clauses
syn_event_decl :: (Bool -> DomId -> [Var] -> Term -> [ModClause] -> a) -> BNF Token a
syn_event_decl :: forall a.
(Bool -> DomId -> [Var] -> Term -> [ModClause] -> a) -> BNF Token a
syn_event_decl Bool -> DomId -> [Var] -> Term -> [ModClause] -> a
cons = DomId
"event-type-decl" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> Bool -> DomId -> [Var] -> Term -> [ModClause] -> a
cons forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$>
BNF Token Bool
syn_is_closed forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Event" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> forall t. SubsumesToken t => SymbExpr t DomId
id_lit forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t (s :: * -> * -> *) a.
(Show t, Ord t, IsSymbExpr s) =>
s t a -> SymbExpr t (Maybe a)
optional (forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"With") forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**>
BNF Token [Var]
objects forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> BNF Token Term
syn_domain_constraint forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**>
BNF Token [ModClause]
syn_event_clauses
syn_fact_clauses :: BNF Token [ModClause]
syn_fact_clauses :: BNF Token [ModClause]
syn_fact_clauses = forall t (s :: * -> * -> *) a.
(Show t, Ord t, IsSymbExpr s) =>
s t a -> SymbExpr t [a]
multiple SymbExpr Token ModClause
syn_fact_clause
where syn_fact_clause :: SymbExpr Token ModClause
syn_fact_clause = DomId
"fact-clause" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> [Term] -> ModClause
ConditionedByCl forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> AltExpr Token [Term]
precondition'
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> [Derivation] -> ModClause
DerivationCl forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token [Derivation]
derivation_from
syn_physical_clauses :: BNF Token [ModClause]
syn_physical_clauses :: BNF Token [ModClause]
syn_physical_clauses = forall t (s :: * -> * -> *) a.
(Show t, Ord t, IsSymbExpr s) =>
s t a -> SymbExpr t [a]
multiple SymbExpr Token ModClause
syn_physical_clause
where syn_physical_clause :: SymbExpr Token ModClause
syn_physical_clause = DomId
"physical-clause" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> [Term] -> ModClause
ConditionedByCl forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> AltExpr Token [Term]
precondition'
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Initialiser -> ModClause
PostCondCl forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> AltExpr Token Initialiser
creating_post'
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Initialiser -> ModClause
PostCondCl forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> AltExpr Token Initialiser
terminating_post'
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Initialiser -> ModClause
PostCondCl forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> AltExpr Token Initialiser
obfuscating_post'
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> [Sync] -> ModClause
SyncCl forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token [Sync]
synchronisations
syn_event_clauses :: BNF Token [ModClause]
syn_event_clauses :: BNF Token [ModClause]
syn_event_clauses = forall t (s :: * -> * -> *) a.
(Show t, Ord t, IsSymbExpr s) =>
s t a -> SymbExpr t [a]
multiple SymbExpr Token ModClause
syn_event_clause
where syn_event_clause :: SymbExpr Token ModClause
syn_event_clause = DomId
"event-clause" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> [Term] -> ModClause
ConditionedByCl forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> AltExpr Token [Term]
precondition'
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> [Derivation] -> ModClause
DerivationCl forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token [Derivation]
derivation_from
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Initialiser -> ModClause
PostCondCl forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> AltExpr Token Initialiser
creating_post'
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Initialiser -> ModClause
PostCondCl forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> AltExpr Token Initialiser
terminating_post'
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Initialiser -> ModClause
PostCondCl forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> AltExpr Token Initialiser
obfuscating_post'
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> [Sync] -> ModClause
SyncCl forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token [Sync]
synchronisations
syn_duty_clauses :: BNF Token [ModClause]
syn_duty_clauses :: BNF Token [ModClause]
syn_duty_clauses = forall t (s :: * -> * -> *) a.
(Show t, Ord t, IsSymbExpr s) =>
s t a -> SymbExpr t [a]
multiple SymbExpr Token ModClause
syn_duty_clause
where syn_duty_clause :: SymbExpr Token ModClause
syn_duty_clause = DomId
"duty-clause" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> [Term] -> ModClause
ConditionedByCl forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> AltExpr Token [Term]
precondition'
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> [Derivation] -> ModClause
DerivationCl forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token [Derivation]
derivation_from
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> [Term] -> ModClause
ViolationCl forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token [Term]
violation_condition
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> [DomId] -> ModClause
EnforcingActsCl forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token [DomId]
enforcing_acts_clauses
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> [DomId] -> ModClause
TerminatedByCl forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token [DomId]
terminated_by_clauses
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> [DomId] -> ModClause
CreatedByCl forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token [DomId]
created_by_clauses
objects :: BNF Token [Var]
objects :: BNF Token [Var]
objects = DomId
"related-to" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> forall t (s :: * -> * -> *) a.
(Show t, Ord t, IsSymbExpr s) =>
s t a -> a -> SymbExpr t a
optionalWithDef (forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Related to" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t b
**> forall t (s :: * -> * -> *) (s2 :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s, IsSymbExpr s2, IsAltExpr s2) =>
s t a -> s2 t b -> SymbExpr t [a]
multipleSepBy1 BNF Token Var
var (forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
',')) []
enforcing_acts_clauses :: BNF Token [DomId]
enforcing_acts_clauses :: BNF Token [DomId]
enforcing_acts_clauses = DomId
"enforcing-act-clauses"
forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Enforced by" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t b
**> forall t (s :: * -> * -> *) (s2 :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s, IsSymbExpr s2, IsAltExpr s2) =>
s t a -> s2 t b -> SymbExpr t [a]
multipleSepBy1 forall t. SubsumesToken t => SymbExpr t DomId
id_lit (forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
',')
terminated_by_clauses :: BNF Token [DomId]
terminated_by_clauses :: BNF Token [DomId]
terminated_by_clauses = DomId
"terminated-by-clauses"
forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Terminated by" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t b
**> forall t (s :: * -> * -> *) (s2 :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s, IsSymbExpr s2, IsAltExpr s2) =>
s t a -> s2 t b -> SymbExpr t [a]
multipleSepBy1 forall t. SubsumesToken t => SymbExpr t DomId
id_lit (forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
',')
created_by_clauses :: BNF Token [DomId]
created_by_clauses :: BNF Token [DomId]
created_by_clauses = DomId
"created-by-clauses"
forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Created by" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t b
**> forall t (s :: * -> * -> *) (s2 :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s, IsSymbExpr s2, IsAltExpr s2) =>
s t a -> s2 t b -> SymbExpr t [a]
multipleSepBy1 forall t. SubsumesToken t => SymbExpr t DomId
id_lit (forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
',')
violation_condition :: BNF Token [Term]
violation_condition :: BNF Token [Term]
violation_condition = DomId
"violation-conditions"
forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Violated when" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t b
**> forall t (s :: * -> * -> *) (s2 :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s, IsSymbExpr s2, IsAltExpr s2) =>
s t a -> s2 t b -> SymbExpr t [a]
multipleSepBy1 BNF Token Term
value_expr (forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
',')
precondition :: BNF Token [Term]
precondition :: BNF Token [Term]
precondition = DomId
"preconditions" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=>
forall t (s :: * -> * -> *) a.
(Show t, Ord t, IsSymbExpr s) =>
s t a -> a -> SymbExpr t a
optionalWithDef AltExpr Token [Term]
precondition' []
precondition' :: AltExpr Token [Term]
precondition' = forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Conditioned by" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t b
**> forall t (s :: * -> * -> *) (s2 :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s, IsSymbExpr s2, IsAltExpr s2) =>
s t a -> s2 t b -> SymbExpr t [a]
multipleSepBy BNF Token Term
value_expr (forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
',')
creating_post :: BNF Token [Effect]
creating_post :: BNF Token Initialiser
creating_post = DomId
"creating-postcondition" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=>
forall t (s :: * -> * -> *) a.
(Show t, Ord t, IsSymbExpr s) =>
s t a -> a -> SymbExpr t a
optionalWithDef AltExpr Token Initialiser
creating_post' []
creating_post' :: AltExpr Token Initialiser
creating_post' = forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Creates" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t b
**> (forall a b. (a -> b) -> [a] -> [b]
map (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [Var] -> Term -> Effect
CAll) forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> forall t (s :: * -> * -> *) (s2 :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s, IsSymbExpr s2, IsAltExpr s2) =>
s t a -> s2 t b -> SymbExpr t [a]
multipleSepBy1 BNF Token ([Var], Term)
effect (forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
','))
terminating_post :: BNF Token [Effect]
terminating_post :: BNF Token Initialiser
terminating_post = DomId
"terminating-postcondition" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=>
forall t (s :: * -> * -> *) a.
(Show t, Ord t, IsSymbExpr s) =>
s t a -> a -> SymbExpr t a
optionalWithDef AltExpr Token Initialiser
terminating_post' []
terminating_post' :: AltExpr Token Initialiser
terminating_post' = forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Terminates" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t b
**> (forall a b. (a -> b) -> [a] -> [b]
map (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [Var] -> Term -> Effect
TAll) forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> forall t (s :: * -> * -> *) (s2 :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s, IsSymbExpr s2, IsAltExpr s2) =>
s t a -> s2 t b -> SymbExpr t [a]
multipleSepBy1 BNF Token ([Var], Term)
effect (forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
','))
obfuscating_post :: BNF Token [Effect]
obfuscating_post :: BNF Token Initialiser
obfuscating_post = DomId
"obfuscating-postcondition" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=>
forall t (s :: * -> * -> *) a.
(Show t, Ord t, IsSymbExpr s) =>
s t a -> a -> SymbExpr t a
optionalWithDef AltExpr Token Initialiser
obfuscating_post' []
obfuscating_post' :: AltExpr Token Initialiser
obfuscating_post' = forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Obfuscates" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t b
**> (forall a b. (a -> b) -> [a] -> [b]
map (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [Var] -> Term -> Effect
OAll) forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> forall t (s :: * -> * -> *) (s2 :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s, IsSymbExpr s2, IsAltExpr s2) =>
s t a -> s2 t b -> SymbExpr t [a]
multipleSepBy1 BNF Token ([Var], Term)
effect (forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
','))
postconditions :: BNF Token [Effect]
postconditions :: BNF Token Initialiser
postconditions = DomId
"postconditions"
forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> forall a. [a] -> [a] -> [a]
(++) forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token Initialiser
creating_post forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> BNF Token Initialiser
terminating_post
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> forall a. [a] -> [a] -> [a]
(++) forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token Initialiser
terminating_post forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> BNF Token Initialiser
creating_post
effect :: BNF Token ([Var], Term)
effect :: BNF Token ([Var], Term)
effect = DomId
"effect-foreach"
forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> ([],) forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token Term
value_expr
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> forall a. ([Var] -> Term -> a) -> BNF Token a
foreach (,)
synchronisations :: BNF Token [Sync]
synchronisations :: BNF Token [Sync]
synchronisations = DomId
"synchronisations"
forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Syncs with" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t b
**> forall t (s :: * -> * -> *) (s2 :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s, IsSymbExpr s2, IsAltExpr s2) =>
s t a -> s2 t b -> SymbExpr t [a]
multipleSepBy1 (forall a. ([Var] -> Term -> a) -> BNF Token a
opt_foreach [Var] -> Term -> Sync
Sync) (forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
',')
application :: (DomId -> Arguments -> a) -> BNF Token a
application :: forall a. (DomId -> Arguments -> a) -> BNF Token a
application DomId -> Arguments -> a
cons = DomId
"application" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> DomId -> Arguments -> a
cons forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> forall t. SubsumesToken t => SymbExpr t DomId
id_lit forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> BNF Token Arguments
arguments
foreach :: ([Var] -> Term -> a) -> BNF Token a
foreach :: forall a. ([Var] -> Term -> a) -> BNF Token a
foreach [Var] -> Term -> a
cons = DomId
"foreach"
forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> forall {t} {s :: * -> * -> *} {b}.
(Show t, Ord t, IsSymbExpr s, SubsumesToken t) =>
s t b -> BNF t b
parens ([Var] -> Term -> a
cons forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Foreach" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> forall t (s :: * -> * -> *) (s2 :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s, IsSymbExpr s2, IsAltExpr s2) =>
s t a -> s2 t b -> SymbExpr t [a]
multipleSepBy1 BNF Token Var
var (forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
',')
forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
':' forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> BNF Token Term
value_expr )
opt_foreach :: ([Var] -> Term -> a) -> BNF Token a
opt_foreach :: forall a. ([Var] -> Term -> a) -> BNF Token a
opt_foreach [Var] -> Term -> a
cons = DomId
"optional-foreach"
forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> [Var] -> Term -> a
cons [] forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token Term
value_expr
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> forall a. ([Var] -> Term -> a) -> BNF Token a
foreach [Var] -> Term -> a
cons
derivation_from :: BNF Token [Derivation]
derivation_from :: BNF Token [Derivation]
derivation_from = DomId
"derivation"
forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Derived from" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t b
**> forall t (s :: * -> * -> *) (s2 :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s, IsSymbExpr s2, IsAltExpr s2) =>
s t a -> s2 t b -> SymbExpr t [a]
multipleSepBy1 SymbExpr Token Derivation
term_deriv (forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
',')
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> forall a b. (a -> b) -> [a] -> [b]
map Term -> Derivation
HoldsWhen forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ BNF Token DomId
keyword_present_when forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> forall t (s :: * -> * -> *) (s2 :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s, IsSymbExpr s2, IsAltExpr s2) =>
s t a -> s2 t b -> SymbExpr t [a]
multipleSepBy1 BNF Token Term
value_expr (forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
',')
where term_deriv :: SymbExpr Token Derivation
term_deriv = DomId
"term-derivation" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> [Var] -> Term -> Derivation
Dv [] forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token Term
value_expr forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> forall a. ([Var] -> Term -> a) -> BNF Token a
foreach [Var] -> Term -> Derivation
Dv
keyword_present_when :: BNF Token String
keyword_present_when :: BNF Token DomId
keyword_present_when = DomId
"present-when"
forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> DomId
"Holds when" forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Present" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"When"
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> DomId
"Holds when" forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Holds" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"When"
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> DomId
"Holds when" forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Present when"
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Holds when"
parse_refiner :: String -> Either String Refiner
parse_refiner :: DomId -> Either DomId Refiner
parse_refiner = forall a. BNF Token a -> DomId -> Either DomId a
parse_component BNF Token Refiner
refiner
refiner :: BNF Token Refiner
refiner :: BNF Token Refiner
refiner = DomId
"refinement" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> forall t (s :: * -> * -> *) a.
(Show t, Ord t, IsSymbExpr s) =>
s t a -> SymbExpr t [a]
multiple BNF Token (DomId, Domain)
refine
refine :: BNF Token (DomId, Domain)
refine :: BNF Token (DomId, Domain)
refine = DomId
"refine" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> (,) forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Fact" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> forall t. SubsumesToken t => SymbExpr t DomId
id_lit forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Identified by" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> BNF Token Domain
type_expr
parse_initialiser :: String -> Either String Initialiser
parse_initialiser :: DomId -> Either DomId Initialiser
parse_initialiser = forall a. BNF Token a -> DomId -> Either DomId a
parse_component BNF Token Initialiser
initialiser
initialiser :: BNF Token Initialiser
initialiser :: BNF Token Initialiser
initialiser = DomId
"initial state" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> forall t (s :: * -> * -> *) a.
(Show t, Ord t, IsSymbExpr s) =>
s t a -> SymbExpr t [a]
multiple (SymbExpr Token Effect
initial forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
'.')
where initial :: SymbExpr Token Effect
initial = DomId
"initial-statement"
forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> forall a. ([Var] -> Term -> a) -> BNF Token a
foreach [Var] -> Term -> Effect
CAll
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> [Var] -> Term -> Effect
CAll [] forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token Term
value_expr
scenario :: BNF Token Scenario
scenario :: BNF Token Scenario
scenario = DomId
"scenario" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> forall t (s :: * -> * -> *) a.
(Show t, Ord t, IsSymbExpr s) =>
s t a -> SymbExpr t [a]
multiple BNF Token Statement
statement
statement :: BNF Token Statement
statement :: BNF Token Statement
statement = DomId
"statement"
forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> forall a b. (a -> b) -> a -> b
($) forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> SymbExpr Token (([Var], DomId, Arguments) -> Statement)
actioner forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> SymbExpr Token ([Var], DomId, Arguments)
maybe_action forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
'.'
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Term -> Statement
Query forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
'?' forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> BNF Token Term
value_expr forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
'.'
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Term -> Statement
Query forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Term
Not forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"!?" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> BNF Token Term
value_expr forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
'.'
where actioner :: SymbExpr Token (([Var], DomId, Arguments) -> Statement)
actioner = DomId
"actioner"
forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> (\([Var]
xs, DomId
d, Arguments
ms) -> [Var] -> TransType -> Either Term (DomId, Arguments) -> Statement
Trans [Var]
xs TransType
Trigger (forall a b. b -> Either a b
Right (DomId
d,Arguments
ms))) forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t (s :: * -> * -> *) a.
(Show t, Ord t, IsSymbExpr s) =>
s t a -> SymbExpr t (Maybe a)
optional (forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
'!')
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> (\([Var]
xs, DomId
d, Arguments
ms) -> [Var] -> TransType -> Either Term (DomId, Arguments) -> Statement
Trans [Var]
xs TransType
AddEvent (forall a b. b -> Either a b
Right (DomId
d,Arguments
ms))) forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
'+'
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> (\([Var]
xs, DomId
d, Arguments
ms) -> [Var] -> TransType -> Either Term (DomId, Arguments) -> Statement
Trans [Var]
xs TransType
RemEvent (forall a b. b -> Either a b
Right (DomId
d,Arguments
ms))) forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
'-'
maybe_action :: SymbExpr Token ([Var], DomId, Arguments)
maybe_action = DomId
"action-statement"
forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> forall a. (DomId -> Arguments -> a) -> BNF Token a
application ([],,)
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> forall {t} {s :: * -> * -> *} {b}.
(Show t, Ord t, IsSymbExpr s, SubsumesToken t) =>
s t b -> BNF t b
parens ((\[Var]
xs (DomId
d,Arguments
args) -> ([Var]
xs,DomId
d,Arguments
args)) forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"Foreach" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> (forall t (s :: * -> * -> *) (s2 :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s, IsSymbExpr s2, IsAltExpr s2) =>
s t a -> s2 t b -> SymbExpr t [a]
multipleSepBy1 BNF Token Var
var (forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
',')) forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
':' forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> forall a. (DomId -> Arguments -> a) -> BNF Token a
application (,))
phrase_scenario :: BNF Token [Phrase]
phrase_scenario :: BNF Token [Phrase]
phrase_scenario = DomId
"phrase-scenario" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> forall t (s :: * -> * -> *) a.
(Show t, Ord t, IsSymbExpr s) =>
s t a -> SymbExpr t [a]
multiple (BNF Token Phrase
syn_phrase forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
'.')
syn_directives_phrases :: BNF Token [Either Directive Phrase]
syn_directives_phrases :: BNF Token [Either Directive Phrase]
syn_directives_phrases = DomId
"opt.directives.phrases" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> forall t (s :: * -> * -> *) a.
(Show t, Ord t, IsSymbExpr s) =>
s t a -> a -> SymbExpr t a
optionalWithDef
(forall t (s :: * -> * -> *) (s2 :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s, IsSymbExpr s2, IsAltExpr s2) =>
s t a -> s2 t b -> SymbExpr t [a]
someSepBy1 (forall a b. a -> Either a b
Left forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token Directive
syn_directive forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> forall a b. b -> Either a b
Right forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token Phrase
syn_phrase) (forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
'.')
forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t (s :: * -> * -> *) a.
(Show t, Ord t, IsSymbExpr s) =>
s t a -> SymbExpr t (Maybe a)
optional (forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
'.')) []
syn_directive :: BNF Token Directive
syn_directive :: BNF Token Directive
syn_directive = DomId
"directive" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=>
DomId -> Directive
Include forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"#include" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> forall t. SubsumesToken t => SymbExpr t DomId
string_lit
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> DomId -> Directive
Require forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"#require" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> forall t. SubsumesToken t => SymbExpr t DomId
string_lit
syn_phrases :: BNF Token [Phrase]
syn_phrases :: BNF Token [Phrase]
syn_phrases = DomId
"opt.phrase" forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> forall t (s :: * -> * -> *) a.
(Show t, Ord t, IsSymbExpr s) =>
s t a -> a -> SymbExpr t a
optionalWithDef
(forall t (s :: * -> * -> *) (s2 :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s, IsSymbExpr s2, IsAltExpr s2) =>
s t a -> s2 t b -> SymbExpr t [a]
someSepBy1 BNF Token Phrase
syn_phrase (forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
'.') forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t a
<** forall t (s :: * -> * -> *) a.
(Show t, Ord t, IsSymbExpr s) =>
s t a -> SymbExpr t (Maybe a)
optional (forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
'.')) []
syn_phrase :: BNF Token Phrase
syn_phrase :: BNF Token Phrase
syn_phrase = DomId
"phrase"
forall {t} {b :: * -> * -> *} {a}.
(Show t, Ord t, HasAlts b) =>
DomId -> b t a -> SymbExpr t a
<:=> forall t (s :: * -> * -> *) a.
(Show t, Ord t, IsSymbExpr s) =>
s t a -> SymbExpr t (Maybe a)
optional (forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
'!') forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t b
**> forall a. ([Var] -> Term -> a) -> BNF Token a
opt_foreach [Var] -> Term -> Phrase
PTrigger
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
'+' forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t b
**> forall a. ([Var] -> Term -> a) -> BNF Token a
opt_foreach [Var] -> Term -> Phrase
Create
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
'-' forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t b
**> forall a. ([Var] -> Term -> a) -> BNF Token a
opt_foreach [Var] -> Term -> Phrase
Terminate
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
'~' forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t b
**> forall a. ([Var] -> Term -> a) -> BNF Token a
opt_foreach [Var] -> Term -> Phrase
Obfuscate
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Term -> Phrase
PQuery forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => Char -> SymbExpr t Char
keychar Char
'?' forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> BNF Token Term
value_expr
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> Term -> Phrase
PQuery forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Term
Not forall t (s :: * -> * -> *) b a.
(Show t, Ord t, IsSymbExpr s) =>
b -> s t a -> AltExpr t b
<$$ forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"!?" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t (a -> b) -> s t a -> AltExpr t b
<**> BNF Token Term
value_expr
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"?-" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t b
**> forall a. ([Var] -> Term -> a) -> BNF Token a
opt_foreach (Bool -> [Var] -> Term -> Phrase
PInstQuery Bool
False)
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> forall t. SubsumesToken t => DomId -> SymbExpr t DomId
keyword DomId
"?--" forall t (i :: * -> * -> *) (s :: * -> * -> *) a b.
(Show t, Ord t, IsAltExpr i, IsSymbExpr s) =>
i t a -> s t b -> AltExpr t b
**> forall a. ([Var] -> Term -> a) -> BNF Token a
opt_foreach (Bool -> [Var] -> Term -> Phrase
PInstQuery Bool
True)
forall t (i :: * -> * -> *) (b :: * -> * -> *) a.
(Show t, Ord t, IsAltExpr i, HasAlts b) =>
i t a -> b t a -> AltExprs t a
<||> [Decl] -> Phrase
PDeclBlock forall t (s :: * -> * -> *) a b.
(Show t, Ord t, IsSymbExpr s) =>
(a -> b) -> s t a -> AltExpr t b
<$$> BNF Token [Decl]
declarations