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


-- parsing frame specifications
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"

-- parsing refiner specifications
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

-- parsing initial state specifications
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