Language.EFLINT.Parse

Documentation

flint_lexer :: String -> Either String [Token]

lexer_settings :: LexerSettings

value_expr :: BNF Token Term

keyword_when :: BNF Token String

var :: BNF Token Var

atom :: BNF Token String

decoration :: BNF Token String

arguments :: BNF Token Arguments

modifier :: BNF Token Modifier

type_expr :: BNF Token Domain

parse_component :: BNF Token a -> String -> Either String a

flint :: BNF Token (Spec, Refiner, Initialiser, Scenario)

parse_flint :: String -> Either String (Spec, Refiner, Initialiser, Scenario)

declarations :: BNF Token [Decl]

placeholder :: BNF Token Decl

frame :: BNF Token [Decl]

syn_fact_decl :: (Bool -> Maybe Restriction -> DomId -> Domain -> Term -> [ModClause] -> a) -> BNF Token a

fact_restriction_by_keyword :: BNF Token (Maybe Restriction)

syn_bool_fact_decl :: (Bool -> DomId -> [ModClause] -> a) -> BNF Token a

syn_ext :: BNF Token Decl

syn_is_closed :: BNF Token Bool

syn_fact_ext :: BNF Token Decl

syn_actor_decl :: (Bool -> DomId -> Domain -> Term -> [ModClause] -> a) -> BNF Token a

syn_pred_decl :: (DomId -> Term -> a) -> BNF Token a

syn_inv_decl :: (DomId -> Term -> a) -> BNF Token a

syn_domain_constraint :: SymbExpr Token Term

syn_duty_decl :: (Bool -> DomId -> Var -> Var -> [Var] -> Term -> [ModClause] -> a) -> BNF Token a

syn_act_decl :: (Bool -> DomId -> Maybe Var -> Maybe Var -> [Var] -> Term -> [ModClause] -> a) -> BNF Token a

syn_physical_decl :: (DomId -> Maybe Var -> [Var] -> Term -> [ModClause] -> a) -> BNF Token a

syn_act_ext :: BNF Token Decl

syn_physical_ext :: SymbExpr Token Decl

syn_event_ext :: BNF Token Decl

syn_duty_ext :: BNF Token Decl

syn_event_decl :: (Bool -> DomId -> [Var] -> Term -> [ModClause] -> a) -> BNF Token a

syn_fact_clauses :: BNF Token [ModClause]

syn_physical_clauses :: BNF Token [ModClause]

syn_event_clauses :: BNF Token [ModClause]

syn_duty_clauses :: BNF Token [ModClause]

objects :: BNF Token [Var]

enforcing_acts_clauses :: BNF Token [DomId]

terminated_by_clauses :: BNF Token [DomId]

created_by_clauses :: BNF Token [DomId]

violation_condition :: BNF Token [Term]

precondition :: BNF Token [Term]

precondition' :: AltExpr Token [Term]

creating_post :: BNF Token [Effect]

creating_post' :: AltExpr Token [Effect]

terminating_post :: BNF Token [Effect]

terminating_post' :: AltExpr Token [Effect]

obfuscating_post :: BNF Token [Effect]

obfuscating_post' :: AltExpr Token [Effect]

postconditions :: BNF Token [Effect]

effect :: BNF Token ([Var], Term)

synchronisations :: BNF Token [Sync]

application :: (DomId -> Arguments -> a) -> BNF Token a

foreach :: ([Var] -> Term -> a) -> BNF Token a

opt_foreach :: ([Var] -> Term -> a) -> BNF Token a

derivation_from :: BNF Token [Derivation]

keyword_present_when :: BNF Token String

parse_refiner :: String -> Either String Refiner

refiner :: BNF Token Refiner

refine :: BNF Token (DomId, Domain)

parse_initialiser :: String -> Either String Initialiser

initialiser :: BNF Token Initialiser

scenario :: BNF Token Scenario

statement :: BNF Token Statement

phrase_scenario :: BNF Token [Phrase]

syn_directives_phrases :: BNF Token [Either Directive Phrase]

syn_directive :: BNF Token Directive

syn_phrases :: BNF Token [Phrase]

syn_phrase :: BNF Token Phrase