eflint-3.0.0.1: Simulation interpreter for FLINT policy descriptions
Safe HaskellNone
LanguageHaskell2010

Language.EFLINT.Spec

Synopsis

Documentation

data Var Source #

Constructors

Var DomId String 

Instances

Instances details
Eq Var Source # 
Instance details

Defined in Language.EFLINT.Spec

Methods

(==) :: Var -> Var -> Bool #

(/=) :: Var -> Var -> Bool #

Ord Var Source # 
Instance details

Defined in Language.EFLINT.Spec

Methods

compare :: Var -> Var -> Ordering #

(<) :: Var -> Var -> Bool #

(<=) :: Var -> Var -> Bool #

(>) :: Var -> Var -> Bool #

(>=) :: Var -> Var -> Bool #

max :: Var -> Var -> Var #

min :: Var -> Var -> Var #

Read Var Source # 
Instance details

Defined in Language.EFLINT.Spec

Show Var Source # 
Instance details

Defined in Language.EFLINT.Spec

Methods

showsPrec :: Int -> Var -> ShowS #

show :: Var -> String #

showList :: [Var] -> ShowS #

data Elem Source #

Constructors

String String 
Int Int 
Product [Tagged] 

Instances

Instances details
Eq Elem Source # 
Instance details

Defined in Language.EFLINT.Spec

Methods

(==) :: Elem -> Elem -> Bool #

(/=) :: Elem -> Elem -> Bool #

Ord Elem Source # 
Instance details

Defined in Language.EFLINT.Spec

Methods

compare :: Elem -> Elem -> Ordering #

(<) :: Elem -> Elem -> Bool #

(<=) :: Elem -> Elem -> Bool #

(>) :: Elem -> Elem -> Bool #

(>=) :: Elem -> Elem -> Bool #

max :: Elem -> Elem -> Elem #

min :: Elem -> Elem -> Elem #

Read Elem Source # 
Instance details

Defined in Language.EFLINT.Spec

Show Elem Source # 
Instance details

Defined in Language.EFLINT.Spec

Methods

showsPrec :: Int -> Elem -> ShowS #

show :: Elem -> String #

showList :: [Elem] -> ShowS #

data Domain Source #

Instances

Instances details
Eq Domain Source # 
Instance details

Defined in Language.EFLINT.Spec

Methods

(==) :: Domain -> Domain -> Bool #

(/=) :: Domain -> Domain -> Bool #

Ord Domain Source # 
Instance details

Defined in Language.EFLINT.Spec

Read Domain Source # 
Instance details

Defined in Language.EFLINT.Spec

Show Domain Source # 
Instance details

Defined in Language.EFLINT.Spec

data Modifier Source #

Constructors

Rename Var Term 

Instances

Instances details
Eq Modifier Source # 
Instance details

Defined in Language.EFLINT.Spec

Ord Modifier Source # 
Instance details

Defined in Language.EFLINT.Spec

Read Modifier Source # 
Instance details

Defined in Language.EFLINT.Spec

Show Modifier Source # 
Instance details

Defined in Language.EFLINT.Spec

data Kind Source #

Instances

Instances details
Eq Kind Source # 
Instance details

Defined in Language.EFLINT.Spec

Methods

(==) :: Kind -> Kind -> Bool #

(/=) :: Kind -> Kind -> Bool #

Ord Kind Source # 
Instance details

Defined in Language.EFLINT.Spec

Methods

compare :: Kind -> Kind -> Ordering #

(<) :: Kind -> Kind -> Bool #

(<=) :: Kind -> Kind -> Bool #

(>) :: Kind -> Kind -> Bool #

(>=) :: Kind -> Kind -> Bool #

max :: Kind -> Kind -> Kind #

min :: Kind -> Kind -> Kind #

Read Kind Source # 
Instance details

Defined in Language.EFLINT.Spec

Show Kind Source # 
Instance details

Defined in Language.EFLINT.Spec

Methods

showsPrec :: Int -> Kind -> ShowS #

show :: Kind -> String #

showList :: [Kind] -> ShowS #

data TypeSpec Source #

Instances

Instances details
Eq TypeSpec Source # 
Instance details

Defined in Language.EFLINT.Spec

Read TypeSpec Source # 
Instance details

Defined in Language.EFLINT.Spec

Show TypeSpec Source # 
Instance details

Defined in Language.EFLINT.Spec

data FactSpec Source #

Constructors

FactSpec 

Fields

Instances

Instances details
Eq FactSpec Source # 
Instance details

Defined in Language.EFLINT.Spec

Ord FactSpec Source # 
Instance details

Defined in Language.EFLINT.Spec

Read FactSpec Source # 
Instance details

Defined in Language.EFLINT.Spec

Show FactSpec Source # 
Instance details

Defined in Language.EFLINT.Spec

data DutySpec Source #

Constructors

DutySpec 

Instances

Instances details
Eq DutySpec Source # 
Instance details

Defined in Language.EFLINT.Spec

Ord DutySpec Source # 
Instance details

Defined in Language.EFLINT.Spec

Read DutySpec Source # 
Instance details

Defined in Language.EFLINT.Spec

Show DutySpec Source # 
Instance details

Defined in Language.EFLINT.Spec

data ActSpec Source #

Constructors

ActSpec 

Fields

Instances

Instances details
Eq ActSpec Source # 
Instance details

Defined in Language.EFLINT.Spec

Methods

(==) :: ActSpec -> ActSpec -> Bool #

(/=) :: ActSpec -> ActSpec -> Bool #

Ord ActSpec Source # 
Instance details

Defined in Language.EFLINT.Spec

Read ActSpec Source # 
Instance details

Defined in Language.EFLINT.Spec

Show ActSpec Source # 
Instance details

Defined in Language.EFLINT.Spec

data Effect Source #

Constructors

CAll [Var] Term 
TAll [Var] Term 
OAll [Var] Term 

Instances

Instances details
Eq Effect Source # 
Instance details

Defined in Language.EFLINT.Spec

Methods

(==) :: Effect -> Effect -> Bool #

(/=) :: Effect -> Effect -> Bool #

Ord Effect Source # 
Instance details

Defined in Language.EFLINT.Spec

Read Effect Source # 
Instance details

Defined in Language.EFLINT.Spec

Show Effect Source # 
Instance details

Defined in Language.EFLINT.Spec

data Sync Source #

Constructors

Sync [Var] Term 

Instances

Instances details
Eq Sync Source # 
Instance details

Defined in Language.EFLINT.Spec

Methods

(==) :: Sync -> Sync -> Bool #

(/=) :: Sync -> Sync -> Bool #

Ord Sync Source # 
Instance details

Defined in Language.EFLINT.Spec

Methods

compare :: Sync -> Sync -> Ordering #

(<) :: Sync -> Sync -> Bool #

(<=) :: Sync -> Sync -> Bool #

(>) :: Sync -> Sync -> Bool #

(>=) :: Sync -> Sync -> Bool #

max :: Sync -> Sync -> Sync #

min :: Sync -> Sync -> Sync #

Read Sync Source # 
Instance details

Defined in Language.EFLINT.Spec

Show Sync Source # 
Instance details

Defined in Language.EFLINT.Spec

Methods

showsPrec :: Int -> Sync -> ShowS #

show :: Sync -> String #

showList :: [Sync] -> ShowS #

data Spec Source #

Constructors

Spec 

Instances

Instances details
Eq Spec Source # 
Instance details

Defined in Language.EFLINT.Spec

Methods

(==) :: Spec -> Spec -> Bool #

(/=) :: Spec -> Spec -> Bool #

Read Spec Source # 
Instance details

Defined in Language.EFLINT.Spec

Show Spec Source # 
Instance details

Defined in Language.EFLINT.Spec

Methods

showsPrec :: Int -> Spec -> ShowS #

show :: Spec -> String #

showList :: [Spec] -> ShowS #

spec_union :: Spec -> Spec -> Spec Source #

Union of specifications with overrides/replacements, not concretizations

decls_union :: Map DomId TypeSpec -> Map DomId TypeSpec -> Map DomId TypeSpec Source #

Right-based union over type declarations, only replacement, no concretization

the components of the initial state (all instantiations of TYPE restricted by ENV)

the possible actions performed in a state, only the actions TYPE are enabled

data Phrase Source #

Instances

Instances details
Eq Phrase Source # 
Instance details

Defined in Language.EFLINT.Spec

Methods

(==) :: Phrase -> Phrase -> Bool #

(/=) :: Phrase -> Phrase -> Bool #

Read Phrase Source # 
Instance details

Defined in Language.EFLINT.Spec

Show Phrase Source # 
Instance details

Defined in Language.EFLINT.Spec

data Decl Source #

Instances

Instances details
Eq Decl Source # 
Instance details

Defined in Language.EFLINT.Spec

Methods

(==) :: Decl -> Decl -> Bool #

(/=) :: Decl -> Decl -> Bool #

Read Decl Source # 
Instance details

Defined in Language.EFLINT.Spec

Show Decl Source # 
Instance details

Defined in Language.EFLINT.Spec

Methods

showsPrec :: Int -> Decl -> ShowS #

show :: Decl -> String #

showList :: [Decl] -> ShowS #

data CDirective Source #

Constructors

DirInv DomId 

data Value Source #

Instances

Instances details
Eq Value Source # 
Instance details

Defined in Language.EFLINT.Spec

Methods

(==) :: Value -> Value -> Bool #

(/=) :: Value -> Value -> Bool #

Show Value Source # 
Instance details

Defined in Language.EFLINT.Spec

Methods

showsPrec :: Int -> Value -> ShowS #

show :: Value -> String #

showList :: [Value] -> ShowS #

data Type Source #

Instances

Instances details
Eq Type Source # 
Instance details

Defined in Language.EFLINT.Spec

Methods

(==) :: Type -> Type -> Bool #

(/=) :: Type -> Type -> Bool #

Show Type Source # 
Instance details

Defined in Language.EFLINT.Spec

Methods

showsPrec :: Int -> Type -> ShowS #

show :: Type -> String #

showList :: [Type] -> ShowS #

subsUnion :: Subs -> Subs -> Subs Source #

right-biased

newtype TaggedJSON Source #

Constructors

TaggedJSON Tagged 

Instances

Instances details
ToJSON TaggedJSON Source # 
Instance details

Defined in Language.EFLINT.Spec