{-# LANGUAGE OverloadedStrings #-}
module Language.EFLINT.Spec where
import Data.Foldable (asum)
import Data.List (intercalate)
import qualified Data.Map as M
import qualified Data.Set as S
import Control.Monad (join)
import Data.Aeson hiding (String)
import qualified Data.Aeson as JSON
type DomId = String
type Tagged = (Elem, DomId)
data Var = Var DomId String
deriving (Eq Var
Var -> Var -> Bool
Var -> Var -> Ordering
Var -> Var -> Var
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Var -> Var -> Var
$cmin :: Var -> Var -> Var
max :: Var -> Var -> Var
$cmax :: Var -> Var -> Var
>= :: Var -> Var -> Bool
$c>= :: Var -> Var -> Bool
> :: Var -> Var -> Bool
$c> :: Var -> Var -> Bool
<= :: Var -> Var -> Bool
$c<= :: Var -> Var -> Bool
< :: Var -> Var -> Bool
$c< :: Var -> Var -> Bool
compare :: Var -> Var -> Ordering
$ccompare :: Var -> Var -> Ordering
Ord, Var -> Var -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Var -> Var -> Bool
$c/= :: Var -> Var -> Bool
== :: Var -> Var -> Bool
$c== :: Var -> Var -> Bool
Eq, Int -> Var -> ShowS
[Var] -> ShowS
Var -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Var] -> ShowS
$cshowList :: [Var] -> ShowS
show :: Var -> [Char]
$cshow :: Var -> [Char]
showsPrec :: Int -> Var -> ShowS
$cshowsPrec :: Int -> Var -> ShowS
Show, ReadPrec [Var]
ReadPrec Var
Int -> ReadS Var
ReadS [Var]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Var]
$creadListPrec :: ReadPrec [Var]
readPrec :: ReadPrec Var
$creadPrec :: ReadPrec Var
readList :: ReadS [Var]
$creadList :: ReadS [Var]
readsPrec :: Int -> ReadS Var
$creadsPrec :: Int -> ReadS Var
Read)
data Elem = String String
| Int Int
| Product [Tagged]
deriving (Eq Elem
Elem -> Elem -> Bool
Elem -> Elem -> Ordering
Elem -> Elem -> Elem
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Elem -> Elem -> Elem
$cmin :: Elem -> Elem -> Elem
max :: Elem -> Elem -> Elem
$cmax :: Elem -> Elem -> Elem
>= :: Elem -> Elem -> Bool
$c>= :: Elem -> Elem -> Bool
> :: Elem -> Elem -> Bool
$c> :: Elem -> Elem -> Bool
<= :: Elem -> Elem -> Bool
$c<= :: Elem -> Elem -> Bool
< :: Elem -> Elem -> Bool
$c< :: Elem -> Elem -> Bool
compare :: Elem -> Elem -> Ordering
$ccompare :: Elem -> Elem -> Ordering
Ord, Elem -> Elem -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Elem -> Elem -> Bool
$c/= :: Elem -> Elem -> Bool
== :: Elem -> Elem -> Bool
$c== :: Elem -> Elem -> Bool
Eq, Int -> Elem -> ShowS
[Elem] -> ShowS
Elem -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Elem] -> ShowS
$cshowList :: [Elem] -> ShowS
show :: Elem -> [Char]
$cshow :: Elem -> [Char]
showsPrec :: Int -> Elem -> ShowS
$cshowsPrec :: Int -> Elem -> ShowS
Show, ReadPrec [Elem]
ReadPrec Elem
Int -> ReadS Elem
ReadS [Elem]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Elem]
$creadListPrec :: ReadPrec [Elem]
readPrec :: ReadPrec Elem
$creadPrec :: ReadPrec Elem
readList :: ReadS [Elem]
$creadList :: ReadS [Elem]
readsPrec :: Int -> ReadS Elem
$creadsPrec :: Int -> ReadS Elem
Read)
data Domain = AnyString
| AnyInt
| Strings [String]
| Ints [Int]
| Products [Var]
| Time
deriving (Eq Domain
Domain -> Domain -> Bool
Domain -> Domain -> Ordering
Domain -> Domain -> Domain
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Domain -> Domain -> Domain
$cmin :: Domain -> Domain -> Domain
max :: Domain -> Domain -> Domain
$cmax :: Domain -> Domain -> Domain
>= :: Domain -> Domain -> Bool
$c>= :: Domain -> Domain -> Bool
> :: Domain -> Domain -> Bool
$c> :: Domain -> Domain -> Bool
<= :: Domain -> Domain -> Bool
$c<= :: Domain -> Domain -> Bool
< :: Domain -> Domain -> Bool
$c< :: Domain -> Domain -> Bool
compare :: Domain -> Domain -> Ordering
$ccompare :: Domain -> Domain -> Ordering
Ord, Domain -> Domain -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Domain -> Domain -> Bool
$c/= :: Domain -> Domain -> Bool
== :: Domain -> Domain -> Bool
$c== :: Domain -> Domain -> Bool
Eq, Int -> Domain -> ShowS
[Domain] -> ShowS
Domain -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Domain] -> ShowS
$cshowList :: [Domain] -> ShowS
show :: Domain -> [Char]
$cshow :: Domain -> [Char]
showsPrec :: Int -> Domain -> ShowS
$cshowsPrec :: Int -> Domain -> ShowS
Show, ReadPrec [Domain]
ReadPrec Domain
Int -> ReadS Domain
ReadS [Domain]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Domain]
$creadListPrec :: ReadPrec [Domain]
readPrec :: ReadPrec Domain
$creadPrec :: ReadPrec Domain
readList :: ReadS [Domain]
$creadList :: ReadS [Domain]
readsPrec :: Int -> ReadS Domain
$creadsPrec :: Int -> ReadS Domain
Read)
enumerable :: Spec -> Domain -> Bool
enumerable :: Spec -> Domain -> Bool
enumerable Spec
spec Domain
d = case Domain
d of
Strings [[Char]]
_ -> Bool
True
Ints [Int]
_ -> Bool
True
Products [Var]
vars -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Spec -> Var -> Bool
enumerable_var Spec
spec) [Var]
vars
Domain
AnyString -> Bool
False
Domain
AnyInt -> Bool
False
Domain
Time -> Bool
False
where enumerable_var :: Spec -> Var -> Bool
enumerable_var :: Spec -> Var -> Bool
enumerable_var Spec
spec Var
v = case forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TypeSpec -> Domain
domain (Spec -> [Char] -> Maybe TypeSpec
find_decl Spec
spec (Spec -> Var -> [Char]
remove_decoration Spec
spec Var
v)) of
Maybe Domain
Nothing -> Bool
False
Just Domain
dom -> Spec -> Domain -> Bool
enumerable Spec
spec Domain
dom
closed_type :: Spec -> DomId -> Maybe Bool
closed_type :: Spec -> [Char] -> Maybe Bool
closed_type Spec
spec [Char]
d = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TypeSpec -> Bool
closed (Spec -> [Char] -> Maybe TypeSpec
find_decl Spec
spec [Char]
d)
type Arguments = Either [Term] [Modifier]
data Modifier = Rename Var Term
deriving (Eq Modifier
Modifier -> Modifier -> Bool
Modifier -> Modifier -> Ordering
Modifier -> Modifier -> Modifier
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Modifier -> Modifier -> Modifier
$cmin :: Modifier -> Modifier -> Modifier
max :: Modifier -> Modifier -> Modifier
$cmax :: Modifier -> Modifier -> Modifier
>= :: Modifier -> Modifier -> Bool
$c>= :: Modifier -> Modifier -> Bool
> :: Modifier -> Modifier -> Bool
$c> :: Modifier -> Modifier -> Bool
<= :: Modifier -> Modifier -> Bool
$c<= :: Modifier -> Modifier -> Bool
< :: Modifier -> Modifier -> Bool
$c< :: Modifier -> Modifier -> Bool
compare :: Modifier -> Modifier -> Ordering
$ccompare :: Modifier -> Modifier -> Ordering
Ord, Modifier -> Modifier -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Modifier -> Modifier -> Bool
$c/= :: Modifier -> Modifier -> Bool
== :: Modifier -> Modifier -> Bool
$c== :: Modifier -> Modifier -> Bool
Eq, Int -> Modifier -> ShowS
[Modifier] -> ShowS
Modifier -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Modifier] -> ShowS
$cshowList :: [Modifier] -> ShowS
show :: Modifier -> [Char]
$cshow :: Modifier -> [Char]
showsPrec :: Int -> Modifier -> ShowS
$cshowsPrec :: Int -> Modifier -> ShowS
Show, ReadPrec [Modifier]
ReadPrec Modifier
Int -> ReadS Modifier
ReadS [Modifier]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Modifier]
$creadListPrec :: ReadPrec [Modifier]
readPrec :: ReadPrec Modifier
$creadPrec :: ReadPrec Modifier
readList :: ReadS [Modifier]
$creadList :: ReadS [Modifier]
readsPrec :: Int -> ReadS Modifier
$creadsPrec :: Int -> ReadS Modifier
Read)
data Kind = Fact FactSpec | Act ActSpec | Duty DutySpec | Event EventSpec
deriving (Eq Kind
Kind -> Kind -> Bool
Kind -> Kind -> Ordering
Kind -> Kind -> Kind
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Kind -> Kind -> Kind
$cmin :: Kind -> Kind -> Kind
max :: Kind -> Kind -> Kind
$cmax :: Kind -> Kind -> Kind
>= :: Kind -> Kind -> Bool
$c>= :: Kind -> Kind -> Bool
> :: Kind -> Kind -> Bool
$c> :: Kind -> Kind -> Bool
<= :: Kind -> Kind -> Bool
$c<= :: Kind -> Kind -> Bool
< :: Kind -> Kind -> Bool
$c< :: Kind -> Kind -> Bool
compare :: Kind -> Kind -> Ordering
$ccompare :: Kind -> Kind -> Ordering
Ord, Kind -> Kind -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Kind -> Kind -> Bool
$c/= :: Kind -> Kind -> Bool
== :: Kind -> Kind -> Bool
$c== :: Kind -> Kind -> Bool
Eq, Int -> Kind -> ShowS
[Kind] -> ShowS
Kind -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Kind] -> ShowS
$cshowList :: [Kind] -> ShowS
show :: Kind -> [Char]
$cshow :: Kind -> [Char]
showsPrec :: Int -> Kind -> ShowS
$cshowsPrec :: Int -> Kind -> ShowS
Show, ReadPrec [Kind]
ReadPrec Kind
Int -> ReadS Kind
ReadS [Kind]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Kind]
$creadListPrec :: ReadPrec [Kind]
readPrec :: ReadPrec Kind
$creadPrec :: ReadPrec Kind
readList :: ReadS [Kind]
$creadList :: ReadS [Kind]
readsPrec :: Int -> ReadS Kind
$creadsPrec :: Int -> ReadS Kind
Read)
data Restriction = VarRestriction | FunctionRestriction
deriving (Eq Restriction
Restriction -> Restriction -> Bool
Restriction -> Restriction -> Ordering
Restriction -> Restriction -> Restriction
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Restriction -> Restriction -> Restriction
$cmin :: Restriction -> Restriction -> Restriction
max :: Restriction -> Restriction -> Restriction
$cmax :: Restriction -> Restriction -> Restriction
>= :: Restriction -> Restriction -> Bool
$c>= :: Restriction -> Restriction -> Bool
> :: Restriction -> Restriction -> Bool
$c> :: Restriction -> Restriction -> Bool
<= :: Restriction -> Restriction -> Bool
$c<= :: Restriction -> Restriction -> Bool
< :: Restriction -> Restriction -> Bool
$c< :: Restriction -> Restriction -> Bool
compare :: Restriction -> Restriction -> Ordering
$ccompare :: Restriction -> Restriction -> Ordering
Ord, Restriction -> Restriction -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Restriction -> Restriction -> Bool
$c/= :: Restriction -> Restriction -> Bool
== :: Restriction -> Restriction -> Bool
$c== :: Restriction -> Restriction -> Bool
Eq, Int -> Restriction -> ShowS
[Restriction] -> ShowS
Restriction -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Restriction] -> ShowS
$cshowList :: [Restriction] -> ShowS
show :: Restriction -> [Char]
$cshow :: Restriction -> [Char]
showsPrec :: Int -> Restriction -> ShowS
$cshowsPrec :: Int -> Restriction -> ShowS
Show, ReadPrec [Restriction]
ReadPrec Restriction
Int -> ReadS Restriction
ReadS [Restriction]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Restriction]
$creadListPrec :: ReadPrec [Restriction]
readPrec :: ReadPrec Restriction
$creadPrec :: ReadPrec Restriction
readList :: ReadS [Restriction]
$creadList :: ReadS [Restriction]
readsPrec :: Int -> ReadS Restriction
$creadsPrec :: Int -> ReadS Restriction
Read, Int -> Restriction
Restriction -> Int
Restriction -> [Restriction]
Restriction -> Restriction
Restriction -> Restriction -> [Restriction]
Restriction -> Restriction -> Restriction -> [Restriction]
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: Restriction -> Restriction -> Restriction -> [Restriction]
$cenumFromThenTo :: Restriction -> Restriction -> Restriction -> [Restriction]
enumFromTo :: Restriction -> Restriction -> [Restriction]
$cenumFromTo :: Restriction -> Restriction -> [Restriction]
enumFromThen :: Restriction -> Restriction -> [Restriction]
$cenumFromThen :: Restriction -> Restriction -> [Restriction]
enumFrom :: Restriction -> [Restriction]
$cenumFrom :: Restriction -> [Restriction]
fromEnum :: Restriction -> Int
$cfromEnum :: Restriction -> Int
toEnum :: Int -> Restriction
$ctoEnum :: Int -> Restriction
pred :: Restriction -> Restriction
$cpred :: Restriction -> Restriction
succ :: Restriction -> Restriction
$csucc :: Restriction -> Restriction
Enum)
data TypeSpec = TypeSpec {
TypeSpec -> Kind
kind :: Kind
, TypeSpec -> Domain
domain :: Domain
, TypeSpec -> Term
domain_constraint :: Term
, TypeSpec -> Maybe Restriction
restriction :: Maybe Restriction
, TypeSpec -> [Derivation]
derivation :: [Derivation]
, TypeSpec -> Bool
closed :: Bool
, TypeSpec -> [Term]
conditions :: [Term]
} deriving (TypeSpec -> TypeSpec -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TypeSpec -> TypeSpec -> Bool
$c/= :: TypeSpec -> TypeSpec -> Bool
== :: TypeSpec -> TypeSpec -> Bool
$c== :: TypeSpec -> TypeSpec -> Bool
Eq, Int -> TypeSpec -> ShowS
[TypeSpec] -> ShowS
TypeSpec -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [TypeSpec] -> ShowS
$cshowList :: [TypeSpec] -> ShowS
show :: TypeSpec -> [Char]
$cshow :: TypeSpec -> [Char]
showsPrec :: Int -> TypeSpec -> ShowS
$cshowsPrec :: Int -> TypeSpec -> ShowS
Show, ReadPrec [TypeSpec]
ReadPrec TypeSpec
Int -> ReadS TypeSpec
ReadS [TypeSpec]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [TypeSpec]
$creadListPrec :: ReadPrec [TypeSpec]
readPrec :: ReadPrec TypeSpec
$creadPrec :: ReadPrec TypeSpec
readList :: ReadS [TypeSpec]
$creadList :: ReadS [TypeSpec]
readsPrec :: Int -> ReadS TypeSpec
$creadsPrec :: Int -> ReadS TypeSpec
Read)
data Derivation = Dv [Var] Term
| HoldsWhen Term
deriving (Eq Derivation
Derivation -> Derivation -> Bool
Derivation -> Derivation -> Ordering
Derivation -> Derivation -> Derivation
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Derivation -> Derivation -> Derivation
$cmin :: Derivation -> Derivation -> Derivation
max :: Derivation -> Derivation -> Derivation
$cmax :: Derivation -> Derivation -> Derivation
>= :: Derivation -> Derivation -> Bool
$c>= :: Derivation -> Derivation -> Bool
> :: Derivation -> Derivation -> Bool
$c> :: Derivation -> Derivation -> Bool
<= :: Derivation -> Derivation -> Bool
$c<= :: Derivation -> Derivation -> Bool
< :: Derivation -> Derivation -> Bool
$c< :: Derivation -> Derivation -> Bool
compare :: Derivation -> Derivation -> Ordering
$ccompare :: Derivation -> Derivation -> Ordering
Ord, Derivation -> Derivation -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Derivation -> Derivation -> Bool
$c/= :: Derivation -> Derivation -> Bool
== :: Derivation -> Derivation -> Bool
$c== :: Derivation -> Derivation -> Bool
Eq, Int -> Derivation -> ShowS
[Derivation] -> ShowS
Derivation -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Derivation] -> ShowS
$cshowList :: [Derivation] -> ShowS
show :: Derivation -> [Char]
$cshow :: Derivation -> [Char]
showsPrec :: Int -> Derivation -> ShowS
$cshowsPrec :: Int -> Derivation -> ShowS
Show, ReadPrec [Derivation]
ReadPrec Derivation
Int -> ReadS Derivation
ReadS [Derivation]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Derivation]
$creadListPrec :: ReadPrec [Derivation]
readPrec :: ReadPrec Derivation
$creadPrec :: ReadPrec Derivation
readList :: ReadS [Derivation]
$creadList :: ReadS [Derivation]
readsPrec :: Int -> ReadS Derivation
$creadsPrec :: Int -> ReadS Derivation
Read)
data FactSpec = FactSpec {
FactSpec -> Bool
invariant :: Bool
, FactSpec -> Bool
actor :: Bool
}
deriving (Eq FactSpec
FactSpec -> FactSpec -> Bool
FactSpec -> FactSpec -> Ordering
FactSpec -> FactSpec -> FactSpec
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: FactSpec -> FactSpec -> FactSpec
$cmin :: FactSpec -> FactSpec -> FactSpec
max :: FactSpec -> FactSpec -> FactSpec
$cmax :: FactSpec -> FactSpec -> FactSpec
>= :: FactSpec -> FactSpec -> Bool
$c>= :: FactSpec -> FactSpec -> Bool
> :: FactSpec -> FactSpec -> Bool
$c> :: FactSpec -> FactSpec -> Bool
<= :: FactSpec -> FactSpec -> Bool
$c<= :: FactSpec -> FactSpec -> Bool
< :: FactSpec -> FactSpec -> Bool
$c< :: FactSpec -> FactSpec -> Bool
compare :: FactSpec -> FactSpec -> Ordering
$ccompare :: FactSpec -> FactSpec -> Ordering
Ord, FactSpec -> FactSpec -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FactSpec -> FactSpec -> Bool
$c/= :: FactSpec -> FactSpec -> Bool
== :: FactSpec -> FactSpec -> Bool
$c== :: FactSpec -> FactSpec -> Bool
Eq, Int -> FactSpec -> ShowS
[FactSpec] -> ShowS
FactSpec -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [FactSpec] -> ShowS
$cshowList :: [FactSpec] -> ShowS
show :: FactSpec -> [Char]
$cshow :: FactSpec -> [Char]
showsPrec :: Int -> FactSpec -> ShowS
$cshowsPrec :: Int -> FactSpec -> ShowS
Show, ReadPrec [FactSpec]
ReadPrec FactSpec
Int -> ReadS FactSpec
ReadS [FactSpec]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [FactSpec]
$creadListPrec :: ReadPrec [FactSpec]
readPrec :: ReadPrec FactSpec
$creadPrec :: ReadPrec FactSpec
readList :: ReadS [FactSpec]
$creadList :: ReadS [FactSpec]
readsPrec :: Int -> ReadS FactSpec
$creadsPrec :: Int -> ReadS FactSpec
Read)
data DutySpec = DutySpec {
DutySpec -> [[Char]]
enforcing_acts :: [DomId]
, DutySpec -> [[Char]]
terminating_acts :: [DomId]
, DutySpec -> [[Char]]
creating_acts :: [DomId]
, DutySpec -> [Term]
violated_when :: [Term]
}
deriving (Eq DutySpec
DutySpec -> DutySpec -> Bool
DutySpec -> DutySpec -> Ordering
DutySpec -> DutySpec -> DutySpec
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: DutySpec -> DutySpec -> DutySpec
$cmin :: DutySpec -> DutySpec -> DutySpec
max :: DutySpec -> DutySpec -> DutySpec
$cmax :: DutySpec -> DutySpec -> DutySpec
>= :: DutySpec -> DutySpec -> Bool
$c>= :: DutySpec -> DutySpec -> Bool
> :: DutySpec -> DutySpec -> Bool
$c> :: DutySpec -> DutySpec -> Bool
<= :: DutySpec -> DutySpec -> Bool
$c<= :: DutySpec -> DutySpec -> Bool
< :: DutySpec -> DutySpec -> Bool
$c< :: DutySpec -> DutySpec -> Bool
compare :: DutySpec -> DutySpec -> Ordering
$ccompare :: DutySpec -> DutySpec -> Ordering
Ord, DutySpec -> DutySpec -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DutySpec -> DutySpec -> Bool
$c/= :: DutySpec -> DutySpec -> Bool
== :: DutySpec -> DutySpec -> Bool
$c== :: DutySpec -> DutySpec -> Bool
Eq, Int -> DutySpec -> ShowS
[DutySpec] -> ShowS
DutySpec -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [DutySpec] -> ShowS
$cshowList :: [DutySpec] -> ShowS
show :: DutySpec -> [Char]
$cshow :: DutySpec -> [Char]
showsPrec :: Int -> DutySpec -> ShowS
$cshowsPrec :: Int -> DutySpec -> ShowS
Show, ReadPrec [DutySpec]
ReadPrec DutySpec
Int -> ReadS DutySpec
ReadS [DutySpec]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [DutySpec]
$creadListPrec :: ReadPrec [DutySpec]
readPrec :: ReadPrec DutySpec
$creadPrec :: ReadPrec DutySpec
readList :: ReadS [DutySpec]
$creadList :: ReadS [DutySpec]
readsPrec :: Int -> ReadS DutySpec
$creadsPrec :: Int -> ReadS DutySpec
Read)
data ActSpec = ActSpec {
ActSpec -> [Effect]
effects :: [Effect]
, ActSpec -> [Sync]
syncs :: [Sync]
, ActSpec -> Bool
physical :: Bool
}
deriving (Eq ActSpec
ActSpec -> ActSpec -> Bool
ActSpec -> ActSpec -> Ordering
ActSpec -> ActSpec -> ActSpec
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ActSpec -> ActSpec -> ActSpec
$cmin :: ActSpec -> ActSpec -> ActSpec
max :: ActSpec -> ActSpec -> ActSpec
$cmax :: ActSpec -> ActSpec -> ActSpec
>= :: ActSpec -> ActSpec -> Bool
$c>= :: ActSpec -> ActSpec -> Bool
> :: ActSpec -> ActSpec -> Bool
$c> :: ActSpec -> ActSpec -> Bool
<= :: ActSpec -> ActSpec -> Bool
$c<= :: ActSpec -> ActSpec -> Bool
< :: ActSpec -> ActSpec -> Bool
$c< :: ActSpec -> ActSpec -> Bool
compare :: ActSpec -> ActSpec -> Ordering
$ccompare :: ActSpec -> ActSpec -> Ordering
Ord, ActSpec -> ActSpec -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ActSpec -> ActSpec -> Bool
$c/= :: ActSpec -> ActSpec -> Bool
== :: ActSpec -> ActSpec -> Bool
$c== :: ActSpec -> ActSpec -> Bool
Eq, Int -> ActSpec -> ShowS
[ActSpec] -> ShowS
ActSpec -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [ActSpec] -> ShowS
$cshowList :: [ActSpec] -> ShowS
show :: ActSpec -> [Char]
$cshow :: ActSpec -> [Char]
showsPrec :: Int -> ActSpec -> ShowS
$cshowsPrec :: Int -> ActSpec -> ShowS
Show, ReadPrec [ActSpec]
ReadPrec ActSpec
Int -> ReadS ActSpec
ReadS [ActSpec]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [ActSpec]
$creadListPrec :: ReadPrec [ActSpec]
readPrec :: ReadPrec ActSpec
$creadPrec :: ReadPrec ActSpec
readList :: ReadS [ActSpec]
$creadList :: ReadS [ActSpec]
readsPrec :: Int -> ReadS ActSpec
$creadsPrec :: Int -> ReadS ActSpec
Read)
data Effect = CAll [Var] Term
| TAll [Var] Term
| OAll [Var] Term
deriving (Eq Effect
Effect -> Effect -> Bool
Effect -> Effect -> Ordering
Effect -> Effect -> Effect
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Effect -> Effect -> Effect
$cmin :: Effect -> Effect -> Effect
max :: Effect -> Effect -> Effect
$cmax :: Effect -> Effect -> Effect
>= :: Effect -> Effect -> Bool
$c>= :: Effect -> Effect -> Bool
> :: Effect -> Effect -> Bool
$c> :: Effect -> Effect -> Bool
<= :: Effect -> Effect -> Bool
$c<= :: Effect -> Effect -> Bool
< :: Effect -> Effect -> Bool
$c< :: Effect -> Effect -> Bool
compare :: Effect -> Effect -> Ordering
$ccompare :: Effect -> Effect -> Ordering
Ord, Effect -> Effect -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Effect -> Effect -> Bool
$c/= :: Effect -> Effect -> Bool
== :: Effect -> Effect -> Bool
$c== :: Effect -> Effect -> Bool
Eq, Int -> Effect -> ShowS
[Effect] -> ShowS
Effect -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Effect] -> ShowS
$cshowList :: [Effect] -> ShowS
show :: Effect -> [Char]
$cshow :: Effect -> [Char]
showsPrec :: Int -> Effect -> ShowS
$cshowsPrec :: Int -> Effect -> ShowS
Show, ReadPrec [Effect]
ReadPrec Effect
Int -> ReadS Effect
ReadS [Effect]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Effect]
$creadListPrec :: ReadPrec [Effect]
readPrec :: ReadPrec Effect
$creadPrec :: ReadPrec Effect
readList :: ReadS [Effect]
$creadList :: ReadS [Effect]
readsPrec :: Int -> ReadS Effect
$creadsPrec :: Int -> ReadS Effect
Read)
data Sync = Sync [Var] Term
deriving (Eq Sync
Sync -> Sync -> Bool
Sync -> Sync -> Ordering
Sync -> Sync -> Sync
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Sync -> Sync -> Sync
$cmin :: Sync -> Sync -> Sync
max :: Sync -> Sync -> Sync
$cmax :: Sync -> Sync -> Sync
>= :: Sync -> Sync -> Bool
$c>= :: Sync -> Sync -> Bool
> :: Sync -> Sync -> Bool
$c> :: Sync -> Sync -> Bool
<= :: Sync -> Sync -> Bool
$c<= :: Sync -> Sync -> Bool
< :: Sync -> Sync -> Bool
$c< :: Sync -> Sync -> Bool
compare :: Sync -> Sync -> Ordering
$ccompare :: Sync -> Sync -> Ordering
Ord, Sync -> Sync -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Sync -> Sync -> Bool
$c/= :: Sync -> Sync -> Bool
== :: Sync -> Sync -> Bool
$c== :: Sync -> Sync -> Bool
Eq, Int -> Sync -> ShowS
[Sync] -> ShowS
Sync -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Sync] -> ShowS
$cshowList :: [Sync] -> ShowS
show :: Sync -> [Char]
$cshow :: Sync -> [Char]
showsPrec :: Int -> Sync -> ShowS
$cshowsPrec :: Int -> Sync -> ShowS
Show, ReadPrec [Sync]
ReadPrec Sync
Int -> ReadS Sync
ReadS [Sync]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Sync]
$creadListPrec :: ReadPrec [Sync]
readPrec :: ReadPrec Sync
$creadPrec :: ReadPrec Sync
readList :: ReadS [Sync]
$creadList :: ReadS [Sync]
readsPrec :: Int -> ReadS Sync
$creadsPrec :: Int -> ReadS Sync
Read)
data EventSpec = EventSpec {
EventSpec -> [Effect]
event_effects :: [Effect]
, EventSpec -> [Sync]
event_syncs :: [Sync]
}
deriving (Eq EventSpec
EventSpec -> EventSpec -> Bool
EventSpec -> EventSpec -> Ordering
EventSpec -> EventSpec -> EventSpec
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: EventSpec -> EventSpec -> EventSpec
$cmin :: EventSpec -> EventSpec -> EventSpec
max :: EventSpec -> EventSpec -> EventSpec
$cmax :: EventSpec -> EventSpec -> EventSpec
>= :: EventSpec -> EventSpec -> Bool
$c>= :: EventSpec -> EventSpec -> Bool
> :: EventSpec -> EventSpec -> Bool
$c> :: EventSpec -> EventSpec -> Bool
<= :: EventSpec -> EventSpec -> Bool
$c<= :: EventSpec -> EventSpec -> Bool
< :: EventSpec -> EventSpec -> Bool
$c< :: EventSpec -> EventSpec -> Bool
compare :: EventSpec -> EventSpec -> Ordering
$ccompare :: EventSpec -> EventSpec -> Ordering
Ord, EventSpec -> EventSpec -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: EventSpec -> EventSpec -> Bool
$c/= :: EventSpec -> EventSpec -> Bool
== :: EventSpec -> EventSpec -> Bool
$c== :: EventSpec -> EventSpec -> Bool
Eq, Int -> EventSpec -> ShowS
[EventSpec] -> ShowS
EventSpec -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [EventSpec] -> ShowS
$cshowList :: [EventSpec] -> ShowS
show :: EventSpec -> [Char]
$cshow :: EventSpec -> [Char]
showsPrec :: Int -> EventSpec -> ShowS
$cshowsPrec :: Int -> EventSpec -> ShowS
Show, ReadPrec [EventSpec]
ReadPrec EventSpec
Int -> ReadS EventSpec
ReadS [EventSpec]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [EventSpec]
$creadListPrec :: ReadPrec [EventSpec]
readPrec :: ReadPrec EventSpec
$creadPrec :: ReadPrec EventSpec
readList :: ReadS [EventSpec]
$creadList :: ReadS [EventSpec]
readsPrec :: Int -> ReadS EventSpec
$creadsPrec :: Int -> ReadS EventSpec
Read)
data Spec = Spec {
Spec -> Map [Char] TypeSpec
decls :: M.Map DomId TypeSpec
, Spec -> Map [Char] [Char]
aliases :: M.Map DomId DomId
}
deriving (Spec -> Spec -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Spec -> Spec -> Bool
$c/= :: Spec -> Spec -> Bool
== :: Spec -> Spec -> Bool
$c== :: Spec -> Spec -> Bool
Eq, Int -> Spec -> ShowS
[Spec] -> ShowS
Spec -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Spec] -> ShowS
$cshowList :: [Spec] -> ShowS
show :: Spec -> [Char]
$cshow :: Spec -> [Char]
showsPrec :: Int -> Spec -> ShowS
$cshowsPrec :: Int -> Spec -> ShowS
Show, ReadPrec [Spec]
ReadPrec Spec
Int -> ReadS Spec
ReadS [Spec]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Spec]
$creadListPrec :: ReadPrec [Spec]
readPrec :: ReadPrec Spec
$creadPrec :: ReadPrec Spec
readList :: ReadS [Spec]
$creadList :: ReadS [Spec]
readsPrec :: Int -> ReadS Spec
$creadsPrec :: Int -> ReadS Spec
Read)
spec_union :: Spec -> Spec -> Spec
spec_union :: Spec -> Spec -> Spec
spec_union Spec
old_spec Spec
new_spec =
Spec {decls :: Map [Char] TypeSpec
decls = Map [Char] TypeSpec -> Map [Char] TypeSpec -> Map [Char] TypeSpec
decls_union (Spec -> Map [Char] TypeSpec
decls Spec
old_spec) (Spec -> Map [Char] TypeSpec
decls Spec
new_spec)
,aliases :: Map [Char] [Char]
aliases = Map [Char] [Char] -> Map [Char] [Char] -> Map [Char] [Char]
aliases_union (Spec -> Map [Char] [Char]
aliases Spec
old_spec) (Spec -> Map [Char] [Char]
aliases Spec
new_spec)
}
decls_union :: M.Map DomId TypeSpec -> M.Map DomId TypeSpec -> M.Map DomId TypeSpec
decls_union :: Map [Char] TypeSpec -> Map [Char] TypeSpec -> Map [Char] TypeSpec
decls_union Map [Char] TypeSpec
old Map [Char] TypeSpec
new = forall k a. Ord k => Map k a -> Map k a -> Map k a
M.union Map [Char] TypeSpec
new Map [Char] TypeSpec
old
aliases_union :: M.Map DomId DomId -> M.Map DomId DomId -> M.Map DomId DomId
aliases_union :: Map [Char] [Char] -> Map [Char] [Char] -> Map [Char] [Char]
aliases_union Map [Char] [Char]
old Map [Char] [Char]
new = forall k a. Ord k => Map k a -> Map k a -> Map k a
M.union Map [Char] [Char]
new Map [Char] [Char]
old
actor_ref_address :: String
actor_ref_address :: [Char]
actor_ref_address = [Char]
"ref"
emptySpec :: Spec
emptySpec :: Spec
emptySpec = Spec { decls :: Map [Char] TypeSpec
decls = Map [Char] TypeSpec
built_in_decls, aliases :: Map [Char] [Char]
aliases = forall k a. Map k a
M.empty}
where built_in_decls :: Map [Char] TypeSpec
built_in_decls = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [
([Char]
"int", TypeSpec
int_decl)
, ([Char]
"string", TypeSpec
string_decl)
, ([Char]
actor_ref_address, TypeSpec
string_decl)
, ([Char]
"actor", TypeSpec
actor_decl)
]
basic :: Spec -> S.Set DomId
basic :: Spec -> Set [Char]
basic Spec
spec = forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
M.foldrWithKey forall {a}. Ord a => a -> TypeSpec -> Set a -> Set a
op forall a. Set a
S.empty (Spec -> Map [Char] TypeSpec
decls Spec
spec)
where op :: a -> TypeSpec -> Set a -> Set a
op a
d TypeSpec
tspec Set a
res | forall (t :: * -> *) a. Foldable t => t a -> Bool
null (TypeSpec -> [Derivation]
derivation TypeSpec
tspec) = forall a. Ord a => a -> Set a -> Set a
S.insert a
d Set a
res
| Bool
otherwise = Set a
res
derived :: Spec -> S.Set DomId
derived :: Spec -> Set [Char]
derived Spec
spec = forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
M.foldrWithKey forall {a}. Ord a => a -> TypeSpec -> Set a -> Set a
op forall a. Set a
S.empty (Spec -> Map [Char] TypeSpec
decls Spec
spec)
where op :: a -> TypeSpec -> Set a -> Set a
op a
d TypeSpec
tspec Set a
res | forall (t :: * -> *) a. Foldable t => t a -> Bool
null (TypeSpec -> [Derivation]
derivation TypeSpec
tspec) = Set a
res
| Bool
otherwise = forall a. Ord a => a -> Set a -> Set a
S.insert a
d Set a
res
is_var :: Spec -> DomId -> Bool
is_var :: Spec -> [Char] -> Bool
is_var Spec
spec [Char]
d = case forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TypeSpec -> Maybe Restriction
restriction (forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup [Char]
d (Spec -> Map [Char] TypeSpec
decls Spec
spec)) of
Just Restriction
VarRestriction -> Bool
True
Maybe Restriction
_ -> Bool
False
is_function :: Spec -> DomId -> Bool
is_function :: Spec -> [Char] -> Bool
is_function Spec
spec [Char]
d = case forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TypeSpec -> Maybe Restriction
restriction (forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup [Char]
d (Spec -> Map [Char] TypeSpec
decls Spec
spec)) of
Just Restriction
FunctionRestriction -> Bool
True
Maybe Restriction
_ -> Bool
False
type Initialiser= [Effect]
emptyInitialiser :: Initialiser
emptyInitialiser :: [Effect]
emptyInitialiser = []
data Statement = Trans [Var] TransType (Either Term (DomId, Arguments))
| Query Term
data TransType = Trigger | AddEvent | RemEvent | ObfEvent
deriving (Eq TransType
TransType -> TransType -> Bool
TransType -> TransType -> Ordering
TransType -> TransType -> TransType
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: TransType -> TransType -> TransType
$cmin :: TransType -> TransType -> TransType
max :: TransType -> TransType -> TransType
$cmax :: TransType -> TransType -> TransType
>= :: TransType -> TransType -> Bool
$c>= :: TransType -> TransType -> Bool
> :: TransType -> TransType -> Bool
$c> :: TransType -> TransType -> Bool
<= :: TransType -> TransType -> Bool
$c<= :: TransType -> TransType -> Bool
< :: TransType -> TransType -> Bool
$c< :: TransType -> TransType -> Bool
compare :: TransType -> TransType -> Ordering
$ccompare :: TransType -> TransType -> Ordering
Ord, TransType -> TransType -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TransType -> TransType -> Bool
$c/= :: TransType -> TransType -> Bool
== :: TransType -> TransType -> Bool
$c== :: TransType -> TransType -> Bool
Eq, Int -> TransType
TransType -> Int
TransType -> [TransType]
TransType -> TransType
TransType -> TransType -> [TransType]
TransType -> TransType -> TransType -> [TransType]
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: TransType -> TransType -> TransType -> [TransType]
$cenumFromThenTo :: TransType -> TransType -> TransType -> [TransType]
enumFromTo :: TransType -> TransType -> [TransType]
$cenumFromTo :: TransType -> TransType -> [TransType]
enumFromThen :: TransType -> TransType -> [TransType]
$cenumFromThen :: TransType -> TransType -> [TransType]
enumFrom :: TransType -> [TransType]
$cenumFrom :: TransType -> [TransType]
fromEnum :: TransType -> Int
$cfromEnum :: TransType -> Int
toEnum :: Int -> TransType
$ctoEnum :: Int -> TransType
pred :: TransType -> TransType
$cpred :: TransType -> TransType
succ :: TransType -> TransType
$csucc :: TransType -> TransType
Enum)
type Scenario = [Statement]
data Directive = Include FilePath
| Require FilePath
data Phrase = PDo Tagged
| PTrigger [Var] Term
| Create [Var] Term
| Terminate [Var] Term
| Obfuscate [Var] Term
| PQuery Term
| PInstQuery Bool [Var] Term
| PDeclBlock [Decl]
| PSkip
deriving (Phrase -> Phrase -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Phrase -> Phrase -> Bool
$c/= :: Phrase -> Phrase -> Bool
== :: Phrase -> Phrase -> Bool
$c== :: Phrase -> Phrase -> Bool
Eq, Int -> Phrase -> ShowS
[Phrase] -> ShowS
Phrase -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Phrase] -> ShowS
$cshowList :: [Phrase] -> ShowS
show :: Phrase -> [Char]
$cshow :: Phrase -> [Char]
showsPrec :: Int -> Phrase -> ShowS
$cshowsPrec :: Int -> Phrase -> ShowS
Show, ReadPrec [Phrase]
ReadPrec Phrase
Int -> ReadS Phrase
ReadS [Phrase]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Phrase]
$creadListPrec :: ReadPrec [Phrase]
readPrec :: ReadPrec Phrase
$creadPrec :: ReadPrec Phrase
readList :: ReadS [Phrase]
$creadList :: ReadS [Phrase]
readsPrec :: Int -> ReadS Phrase
$creadsPrec :: Int -> ReadS Phrase
Read)
data Decl = TypeDecl DomId TypeSpec
| TypeExt DomId [ModClause]
| PlaceholderDecl DomId DomId
deriving (Decl -> Decl -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Decl -> Decl -> Bool
$c/= :: Decl -> Decl -> Bool
== :: Decl -> Decl -> Bool
$c== :: Decl -> Decl -> Bool
Eq, Int -> Decl -> ShowS
[Decl] -> ShowS
Decl -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Decl] -> ShowS
$cshowList :: [Decl] -> ShowS
show :: Decl -> [Char]
$cshow :: Decl -> [Char]
showsPrec :: Int -> Decl -> ShowS
$cshowsPrec :: Int -> Decl -> ShowS
Show, ReadPrec [Decl]
ReadPrec Decl
Int -> ReadS Decl
ReadS [Decl]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Decl]
$creadListPrec :: ReadPrec [Decl]
readPrec :: ReadPrec Decl
$creadPrec :: ReadPrec Decl
readList :: ReadS [Decl]
$creadList :: ReadS [Decl]
readsPrec :: Int -> ReadS Decl
$creadsPrec :: Int -> ReadS Decl
Read)
data CDecl = CTypeDecl DomId TypeSpec
| CTypeExt DomId [CModClause]
| CPlaceholderDecl DomId DomId
deriving (CDecl -> CDecl -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CDecl -> CDecl -> Bool
$c/= :: CDecl -> CDecl -> Bool
== :: CDecl -> CDecl -> Bool
$c== :: CDecl -> CDecl -> Bool
Eq, Int -> CDecl -> ShowS
[CDecl] -> ShowS
CDecl -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [CDecl] -> ShowS
$cshowList :: [CDecl] -> ShowS
show :: CDecl -> [Char]
$cshow :: CDecl -> [Char]
showsPrec :: Int -> CDecl -> ShowS
$cshowsPrec :: Int -> CDecl -> ShowS
Show, ReadPrec [CDecl]
ReadPrec CDecl
Int -> ReadS CDecl
ReadS [CDecl]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [CDecl]
$creadListPrec :: ReadPrec [CDecl]
readPrec :: ReadPrec CDecl
$creadPrec :: ReadPrec CDecl
readList :: ReadS [CDecl]
$creadList :: ReadS [CDecl]
readsPrec :: Int -> ReadS CDecl
$creadsPrec :: Int -> ReadS CDecl
Read)
isInitialTypeDecl :: Decl -> Bool
isInitialTypeDecl :: Decl -> Bool
isInitialTypeDecl (TypeDecl [Char]
_ TypeSpec
_) = Bool
True
isInitialTypeDecl (TypeExt [Char]
_ [ModClause]
_) = Bool
False
isInitialTypeDecl (PlaceholderDecl [Char]
_ [Char]
_) = Bool
False
extend_spec :: [Decl] -> Spec -> Spec
extend_spec :: [Decl] -> Spec -> Spec
extend_spec = forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Decl -> Spec -> Spec
op)
where op :: Decl -> Spec -> Spec
op (TypeDecl [Char]
ty TypeSpec
tyspec) Spec
spec = Spec
spec { decls :: Map [Char] TypeSpec
decls = forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert [Char]
ty TypeSpec
tyspec (Spec -> Map [Char] TypeSpec
decls Spec
spec) }
op (PlaceholderDecl [Char]
f [Char]
t) Spec
spec = Spec
spec { aliases :: Map [Char] [Char]
aliases = forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert [Char]
f [Char]
t (Spec -> Map [Char] [Char]
aliases Spec
spec) }
op Decl
_ Spec
spec = Spec
spec
data ModClause = ConditionedByCl [Term]
| DerivationCl [Derivation]
| PostCondCl [Effect]
| SyncCl [Sync]
| ViolationCl [Term]
| EnforcingActsCl [DomId]
| TerminatedByCl [DomId]
| CreatedByCl [DomId]
deriving (ModClause -> ModClause -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ModClause -> ModClause -> Bool
$c/= :: ModClause -> ModClause -> Bool
== :: ModClause -> ModClause -> Bool
$c== :: ModClause -> ModClause -> Bool
Eq, Int -> ModClause -> ShowS
[ModClause] -> ShowS
ModClause -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [ModClause] -> ShowS
$cshowList :: [ModClause] -> ShowS
show :: ModClause -> [Char]
$cshow :: ModClause -> [Char]
showsPrec :: Int -> ModClause -> ShowS
$cshowsPrec :: Int -> ModClause -> ShowS
Show, ReadPrec [ModClause]
ReadPrec ModClause
Int -> ReadS ModClause
ReadS [ModClause]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [ModClause]
$creadListPrec :: ReadPrec [ModClause]
readPrec :: ReadPrec ModClause
$creadPrec :: ReadPrec ModClause
readList :: ReadS [ModClause]
$creadList :: ReadS [ModClause]
readsPrec :: Int -> ReadS ModClause
$creadsPrec :: Int -> ReadS ModClause
Read)
data CModClause = CConditionedByCl [Term]
| CDerivationCl [Derivation]
| CPostCondCl [Effect]
| CSyncCl [Sync]
| CViolationCl [Term]
| CEnforcingActsCl [DomId]
| CTerminatedByCl [DomId]
| CCreatedByCl [DomId]
deriving (CModClause -> CModClause -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CModClause -> CModClause -> Bool
$c/= :: CModClause -> CModClause -> Bool
== :: CModClause -> CModClause -> Bool
$c== :: CModClause -> CModClause -> Bool
Eq, Int -> CModClause -> ShowS
[CModClause] -> ShowS
CModClause -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [CModClause] -> ShowS
$cshowList :: [CModClause] -> ShowS
show :: CModClause -> [Char]
$cshow :: CModClause -> [Char]
showsPrec :: Int -> CModClause -> ShowS
$cshowsPrec :: Int -> CModClause -> ShowS
Show, ReadPrec [CModClause]
ReadPrec CModClause
Int -> ReadS CModClause
ReadS [CModClause]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [CModClause]
$creadListPrec :: ReadPrec [CModClause]
readPrec :: ReadPrec CModClause
$creadPrec :: ReadPrec CModClause
readList :: ReadS [CModClause]
$creadList :: ReadS [CModClause]
readsPrec :: Int -> ReadS CModClause
$creadsPrec :: Int -> ReadS CModClause
Read)
enforcing_act_condition :: DomId -> Term
enforcing_act_condition :: [Char] -> Term
enforcing_act_condition [Char]
a = Term -> Term
Enabled ([Char] -> Arguments -> Term
App [Char]
a (forall a b. b -> Either a b
Right []))
terminated_by_condition :: DomId -> DomId -> Term
terminated_by_condition :: [Char] -> [Char] -> Term
terminated_by_condition [Char]
d [Char]
a = [Char] -> Arguments -> Term
App [Char]
d (forall a b. b -> Either a b
Right [])
terminated_by_precondition :: DomId -> DomId -> Term
terminated_by_precondition :: [Char] -> [Char] -> Term
terminated_by_precondition [Char]
d [Char]
a = Term -> Term
Present ([Char] -> Arguments -> Term
App [Char]
d (forall a b. b -> Either a b
Right []))
created_by_condition :: DomId -> DomId -> Term
created_by_condition :: [Char] -> [Char] -> Term
created_by_condition [Char]
d [Char]
a = [Char] -> Arguments -> Term
App [Char]
d (forall a b. b -> Either a b
Right [])
apply_type_ext :: DomId -> [CModClause] -> TypeSpec -> TypeSpec
apply_type_ext :: [Char] -> [CModClause] -> TypeSpec -> TypeSpec
apply_type_ext [Char]
ty [CModClause]
clauses TypeSpec
tspec = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr CModClause -> TypeSpec -> TypeSpec
apply_clause TypeSpec
tspec [CModClause]
clauses
where apply_clause :: CModClause -> TypeSpec -> TypeSpec
apply_clause CModClause
clause TypeSpec
tspec = case CModClause
clause of
CConditionedByCl [Term]
conds -> TypeSpec
tspec { conditions :: [Term]
conditions = [Term]
conds forall a. [a] -> [a] -> [a]
++ TypeSpec -> [Term]
conditions TypeSpec
tspec }
CDerivationCl [Derivation]
dvs -> TypeSpec
tspec { derivation :: [Derivation]
derivation = [Derivation]
dvs forall a. [a] -> [a] -> [a]
++ TypeSpec -> [Derivation]
derivation TypeSpec
tspec }
CPostCondCl [Effect]
effs -> TypeSpec
tspec { kind :: Kind
kind = Kind -> Kind
add_effects (TypeSpec -> Kind
kind TypeSpec
tspec) }
where add_effects :: Kind -> Kind
add_effects (Act ActSpec
aspec) = ActSpec -> Kind
Act (ActSpec
aspec { effects :: [Effect]
effects = [Effect]
effs forall a. [a] -> [a] -> [a]
++ ActSpec -> [Effect]
effects ActSpec
aspec})
add_effects (Event EventSpec
espec)= EventSpec -> Kind
Event (EventSpec
espec { event_effects :: [Effect]
event_effects = [Effect]
effs forall a. [a] -> [a] -> [a]
++ EventSpec -> [Effect]
event_effects EventSpec
espec })
add_effects Kind
s = Kind
s
CSyncCl [Sync]
ss -> TypeSpec
tspec { kind :: Kind
kind = Kind -> Kind
add_syncs (TypeSpec -> Kind
kind TypeSpec
tspec) }
where add_syncs :: Kind -> Kind
add_syncs (Act ActSpec
aspec) = ActSpec -> Kind
Act forall a b. (a -> b) -> a -> b
$ ActSpec
aspec { syncs :: [Sync]
syncs = [Sync]
ss forall a. [a] -> [a] -> [a]
++ ActSpec -> [Sync]
syncs ActSpec
aspec}
add_syncs (Event EventSpec
espec) = EventSpec -> Kind
Event forall a b. (a -> b) -> a -> b
$ EventSpec
espec { event_syncs :: [Sync]
event_syncs = [Sync]
ss forall a. [a] -> [a] -> [a]
++ EventSpec -> [Sync]
event_syncs EventSpec
espec}
add_syncs Kind
s = Kind
s
CViolationCl [Term]
vs -> TypeSpec
tspec { kind :: Kind
kind = Kind -> Kind
add_viol_conds (TypeSpec -> Kind
kind TypeSpec
tspec) }
where add_viol_conds :: Kind -> Kind
add_viol_conds (Duty DutySpec
dspec) = DutySpec -> Kind
Duty forall a b. (a -> b) -> a -> b
$ DutySpec
dspec { violated_when :: [Term]
violated_when = [Term]
vs forall a. [a] -> [a] -> [a]
++ DutySpec -> [Term]
violated_when DutySpec
dspec }
add_viol_conds Kind
s = Kind
s
CEnforcingActsCl [[Char]]
ds -> TypeSpec
tspec { kind :: Kind
kind = Kind -> Kind
add_enf_acts (TypeSpec -> Kind
kind TypeSpec
tspec) }
where add_enf_acts :: Kind -> Kind
add_enf_acts (Duty DutySpec
dspec) = DutySpec -> Kind
Duty forall a b. (a -> b) -> a -> b
$ DutySpec
dspec { enforcing_acts :: [[Char]]
enforcing_acts = [[Char]]
ds forall a. [a] -> [a] -> [a]
++ DutySpec -> [[Char]]
enforcing_acts DutySpec
dspec }
add_enf_acts Kind
s = Kind
s
CTerminatedByCl [[Char]]
as -> TypeSpec
tspec { kind :: Kind
kind = Kind -> Kind
add_terms_acts (TypeSpec -> Kind
kind TypeSpec
tspec) }
where add_terms_acts :: Kind -> Kind
add_terms_acts (Duty DutySpec
dspec) = DutySpec -> Kind
Duty forall a b. (a -> b) -> a -> b
$ DutySpec
dspec { terminating_acts :: [[Char]]
terminating_acts = [[Char]]
as forall a. [a] -> [a] -> [a]
++ DutySpec -> [[Char]]
terminating_acts DutySpec
dspec }
add_terms_acts Kind
s = Kind
s
CCreatedByCl [[Char]]
as -> TypeSpec
tspec { kind :: Kind
kind = Kind -> Kind
add_create_acts (TypeSpec -> Kind
kind TypeSpec
tspec) }
where add_create_acts :: Kind -> Kind
add_create_acts (Duty DutySpec
dspec) = DutySpec -> Kind
Duty forall a b. (a -> b) -> a -> b
$ DutySpec
dspec { creating_acts :: [[Char]]
creating_acts = [[Char]]
as forall a. [a] -> [a] -> [a]
++ DutySpec -> [[Char]]
creating_acts DutySpec
dspec }
add_create_acts Kind
s = Kind
s
data CPhrase = CDo Tagged
| CTrigger [Var] Term
| CCreate [Var] Term
| CTerminate [Var] Term
| CObfuscate [Var] Term
| CQuery Term
| CInstQuery Bool [Var] Term
| CPOnlyDecls
| CPDir CDirective
| CSeq CPhrase CPhrase
| CPSkip
data CDirective = DirInv DomId
process_directives :: [CDirective] -> Spec -> Spec
process_directives :: [CDirective] -> Spec -> Spec
process_directives = forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr CDirective -> Spec -> Spec
op)
where op :: CDirective -> Spec -> Spec
op (DirInv [Char]
ty) Spec
spec = Spec
spec { decls :: Map [Char] TypeSpec
decls = forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
M.adjust TypeSpec -> TypeSpec
mod [Char]
ty (Spec -> Map [Char] TypeSpec
decls Spec
spec) }
where mod :: TypeSpec -> TypeSpec
mod TypeSpec
tspec = case TypeSpec -> Kind
kind TypeSpec
tspec of
Fact FactSpec
fspec -> TypeSpec
tspec { kind :: Kind
kind = FactSpec -> Kind
Fact (FactSpec
fspec {invariant :: Bool
invariant = Bool
True}) }
Kind
_ -> TypeSpec
tspec
invariants :: Spec -> S.Set DomId
invariants :: Spec -> Set [Char]
invariants Spec
spec = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall {a}. Ord a => (a, TypeSpec) -> Set a -> Set a
op forall a. Set a
S.empty (forall k a. Map k a -> [(k, a)]
M.assocs (Spec -> Map [Char] TypeSpec
decls Spec
spec))
where op :: (a, TypeSpec) -> Set a -> Set a
op (a
ty,TypeSpec
tspec) Set a
acc = case TypeSpec -> Kind
kind TypeSpec
tspec of
Fact FactSpec
fspec | FactSpec -> Bool
invariant FactSpec
fspec -> forall a. Ord a => a -> Set a -> Set a
S.insert a
ty Set a
acc
Kind
_ -> Set a
acc
actors :: Spec -> S.Set DomId
actors :: Spec -> Set [Char]
actors Spec
spec = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall {a}. Ord a => (a, TypeSpec) -> Set a -> Set a
op forall a. Set a
S.empty (forall k a. Map k a -> [(k, a)]
M.assocs (Spec -> Map [Char] TypeSpec
decls Spec
spec))
where op :: (a, TypeSpec) -> Set a -> Set a
op (a
ty,TypeSpec
tspec) Set a
acc = case TypeSpec -> Kind
kind TypeSpec
tspec of
Fact FactSpec
fspec | FactSpec -> Bool
actor FactSpec
fspec -> forall a. Ord a => a -> Set a -> Set a
S.insert a
ty Set a
acc
Kind
_ -> Set a
acc
type Subs = M.Map Var Tagged
data Term = Not Term
| And Term Term
| Or Term Term
| BoolLit Bool
| Leq Term Term
| Geq Term Term
| Ge Term Term
| Le Term Term
| Sub Term Term
| Add Term Term
| Mult Term Term
| Mod Term Term
| Div Term Term
| IntLit Int
| StringLit String
| Eq Term Term
| Neq Term Term
| Exists [Var] Term
| Forall [Var] Term
| Count [Var] Term
| Sum [Var] Term
| Max [Var] Term
| Min [Var] Term
| When Term Term
| Present Term
| Violated Term
| Enabled Term
| Project Term Var
| Tag Term DomId
| Untag Term
| Ref Var
| App DomId Arguments
| CurrentTime
deriving (Int -> Term -> ShowS
[Term] -> ShowS
Term -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Term] -> ShowS
$cshowList :: [Term] -> ShowS
show :: Term -> [Char]
$cshow :: Term -> [Char]
showsPrec :: Int -> Term -> ShowS
$cshowsPrec :: Int -> Term -> ShowS
Show, Eq Term
Term -> Term -> Bool
Term -> Term -> Ordering
Term -> Term -> Term
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Term -> Term -> Term
$cmin :: Term -> Term -> Term
max :: Term -> Term -> Term
$cmax :: Term -> Term -> Term
>= :: Term -> Term -> Bool
$c>= :: Term -> Term -> Bool
> :: Term -> Term -> Bool
$c> :: Term -> Term -> Bool
<= :: Term -> Term -> Bool
$c<= :: Term -> Term -> Bool
< :: Term -> Term -> Bool
$c< :: Term -> Term -> Bool
compare :: Term -> Term -> Ordering
$ccompare :: Term -> Term -> Ordering
Ord, Term -> Term -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Term -> Term -> Bool
$c/= :: Term -> Term -> Bool
== :: Term -> Term -> Bool
$c== :: Term -> Term -> Bool
Eq, ReadPrec [Term]
ReadPrec Term
Int -> ReadS Term
ReadS [Term]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Term]
$creadListPrec :: ReadPrec [Term]
readPrec :: ReadPrec Term
$creadPrec :: ReadPrec Term
readList :: ReadS [Term]
$creadList :: ReadS [Term]
readsPrec :: Int -> ReadS Term
$creadsPrec :: Int -> ReadS Term
Read)
data Value = ResBool Bool
| ResString String
| ResInt Int
| ResTagged Tagged
deriving (Value -> Value -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Value -> Value -> Bool
$c/= :: Value -> Value -> Bool
== :: Value -> Value -> Bool
$c== :: Value -> Value -> Bool
Eq, Int -> Value -> ShowS
[Value] -> ShowS
Value -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Value] -> ShowS
$cshowList :: [Value] -> ShowS
show :: Value -> [Char]
$cshow :: Value -> [Char]
showsPrec :: Int -> Value -> ShowS
$cshowsPrec :: Int -> Value -> ShowS
Show)
data Type = TyStrings
| TyInts
| TyBool
| TyTagged DomId
deriving (Type -> Type -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Type -> Type -> Bool
$c/= :: Type -> Type -> Bool
== :: Type -> Type -> Bool
$c== :: Type -> Type -> Bool
Eq, Int -> Type -> ShowS
[Type] -> ShowS
Type -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Type] -> ShowS
$cshowList :: [Type] -> ShowS
show :: Type -> [Char]
$cshow :: Type -> [Char]
showsPrec :: Int -> Type -> ShowS
$cshowsPrec :: Int -> Type -> ShowS
Show)
instance Show TransType where
show :: TransType -> [Char]
show TransType
Trigger = [Char]
""
show TransType
AddEvent = [Char]
"+"
show TransType
RemEvent = [Char]
"-"
show TransType
ObfEvent = [Char]
"~"
no_decoration :: DomId -> Var
no_decoration :: [Char] -> Var
no_decoration [Char]
ty = [Char] -> [Char] -> Var
Var [Char]
ty [Char]
""
remove_decoration :: Spec -> Var -> DomId
remove_decoration :: Spec -> Var -> [Char]
remove_decoration Spec
spec (Var [Char]
dom [Char]
_) = Spec -> ShowS
chase_alias Spec
spec [Char]
dom
duty_decls :: Spec -> [(DomId, DutySpec)]
duty_decls :: Spec -> [([Char], DutySpec)]
duty_decls Spec
spec = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall {a}. (a, TypeSpec) -> [(a, DutySpec)]
op forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
M.assocs (Spec -> Map [Char] TypeSpec
decls Spec
spec)
where op :: (a, TypeSpec) -> [(a, DutySpec)]
op (a
d,TypeSpec
tspec) = case TypeSpec -> Kind
kind TypeSpec
tspec of
Duty DutySpec
ds -> [(a
d,DutySpec
ds)]
Kind
_ -> []
trigger_decls :: Spec -> [(DomId, Either EventSpec ActSpec)]
trigger_decls :: Spec -> [([Char], Either EventSpec ActSpec)]
trigger_decls Spec
spec = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall {a}. (a, TypeSpec) -> [(a, Either EventSpec ActSpec)]
op forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
M.assocs (Spec -> Map [Char] TypeSpec
decls Spec
spec)
where op :: (a, TypeSpec) -> [(a, Either EventSpec ActSpec)]
op (a
d,TypeSpec
tspec) = case TypeSpec -> Kind
kind TypeSpec
tspec of
Event EventSpec
e -> [(a
d,forall a b. a -> Either a b
Left EventSpec
e)]
Act ActSpec
a -> [(a
d,forall a b. b -> Either a b
Right ActSpec
a)]
Kind
_ -> []
triggerable :: Spec -> DomId -> Bool
triggerable :: Spec -> [Char] -> Bool
triggerable Spec
spec [Char]
d = case forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TypeSpec -> Kind
kind (Spec -> [Char] -> Maybe TypeSpec
find_decl Spec
spec [Char]
d) of
Maybe Kind
Nothing -> Bool
False
Just (Act ActSpec
_) -> Bool
True
Just (Event EventSpec
_) -> Bool
True
Just Kind
_ -> Bool
False
find_decl :: Spec -> DomId -> Maybe TypeSpec
find_decl :: Spec -> [Char] -> Maybe TypeSpec
find_decl Spec
spec [Char]
d = forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Spec -> ShowS
chase_alias Spec
spec [Char]
d) (Spec -> Map [Char] TypeSpec
decls Spec
spec)
find_violation_cond :: Spec -> DomId -> Maybe [Term]
find_violation_cond :: Spec -> [Char] -> Maybe [Term]
find_violation_cond Spec
spec [Char]
d = case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Spec -> ShowS
chase_alias Spec
spec [Char]
d) (Spec -> Map [Char] TypeSpec
decls Spec
spec) of
Maybe TypeSpec
Nothing -> forall a. Maybe a
Nothing
Just TypeSpec
ts -> case TypeSpec -> Kind
kind TypeSpec
ts of
Duty DutySpec
ds -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ DutySpec -> [Term]
violated_when DutySpec
ds
Kind
_ -> forall a. Maybe a
Nothing
chase_alias :: Spec -> DomId -> DomId
chase_alias :: Spec -> ShowS
chase_alias Spec
spec [Char]
d = Set [Char] -> ShowS
chase_alias' forall a. Set a
S.empty [Char]
d
where chase_alias' :: Set [Char] -> ShowS
chase_alias' Set [Char]
tried [Char]
d
| [Char]
d forall a. Ord a => a -> Set a -> Bool
`S.member` Set [Char]
tried = [Char]
d
| Bool
otherwise = forall b a. b -> (a -> b) -> Maybe a -> b
maybe [Char]
d (Set [Char] -> ShowS
chase_alias' (forall a. Ord a => a -> Set a -> Set a
S.insert [Char]
d Set [Char]
tried)) (forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup [Char]
d (Spec -> Map [Char] [Char]
aliases Spec
spec))
show_arguments :: Arguments -> String
show_arguments :: Arguments -> [Char]
show_arguments (Right [Modifier]
mods) = [Modifier] -> [Char]
show_modifiers [Modifier]
mods
show_arguments (Left [Term]
xs) = [Char]
"(" forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"," (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> [Char]
show [Term]
xs) forall a. [a] -> [a] -> [a]
++ [Char]
")"
show_modifiers :: [Modifier] -> String
show_modifiers :: [Modifier] -> [Char]
show_modifiers [] = [Char]
"()"
show_modifiers [Modifier]
cs = [Char]
"(" forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"," (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> [Char]
show [Modifier]
cs) forall a. [a] -> [a] -> [a]
++ [Char]
")"
show_projections :: [Var] -> String
show_projections :: [Var] -> [Char]
show_projections [] = [Char]
""
show_projections [Var]
ds = [Char]
"[" forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"," (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> [Char]
show [Var]
ds) forall a. [a] -> [a] -> [a]
++ [Char]
"]"
show_component :: Tagged -> String
show_component :: Tagged -> [Char]
show_component = Tagged -> [Char]
ppTagged
ppTagged :: Tagged -> String
ppTagged :: Tagged -> [Char]
ppTagged (Elem
v,[Char]
t) = case Elem
v of
String [Char]
s -> [Char]
t forall a. [a] -> [a] -> [a]
++ [Char]
"(" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show [Char]
s forall a. [a] -> [a] -> [a]
++ [Char]
")"
Int Int
i -> [Char]
t forall a. [a] -> [a] -> [a]
++ [Char]
"(" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
i forall a. [a] -> [a] -> [a]
++ [Char]
")"
Product [Tagged]
tes -> [Char]
t forall a. [a] -> [a] -> [a]
++ [Char]
"(" forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"," (forall a b. (a -> b) -> [a] -> [b]
map Tagged -> [Char]
ppTagged [Tagged]
tes) forall a. [a] -> [a] -> [a]
++ [Char]
")"
show_stmt :: Statement -> String
show_stmt :: Statement -> [Char]
show_stmt (Query Term
t) = [Char]
"?" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term
t
show_stmt (Trans [Var]
xs TransType
atype Either Term ([Char], Arguments)
etm) = case [Var]
xs of
[] -> case Either Term ([Char], Arguments)
etm of Left Term
t -> forall a. Show a => a -> [Char]
show TransType
atype forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term
t
Right ([Char]
d,Arguments
mods) -> forall a. Show a => a -> [Char]
show TransType
atype forall a. [a] -> [a] -> [a]
++ [Char]
d forall a. [a] -> [a] -> [a]
++ Arguments -> [Char]
show_arguments Arguments
mods
[Var]
_ -> [Char]
"(" forall a. [a] -> [a] -> [a]
++ [Char]
"Foreach " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"," (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> [Char]
show [Var]
xs) forall a. [a] -> [a] -> [a]
++ [Char]
" : " forall a. [a] -> [a] -> [a]
++ Statement -> [Char]
show_stmt ([Var] -> TransType -> Either Term ([Char], Arguments) -> Statement
Trans [] TransType
atype Either Term ([Char], Arguments)
etm) forall a. [a] -> [a] -> [a]
++ [Char]
")"
valOf :: Tagged -> Elem
valOf :: Tagged -> Elem
valOf (Elem
c,[Char]
t) = Elem
c
tagOf :: Tagged -> DomId
tagOf :: Tagged -> [Char]
tagOf (Elem
c,[Char]
t) = [Char]
t
substitutions_of :: [Modifier] -> [(Var, Term)]
substitutions_of :: [Modifier] -> [(Var, Term)]
substitutions_of = forall a b. (a -> b) -> [a] -> [b]
map (\(Rename Var
x Term
y) -> (Var
x,Term
y))
make_substitutions_of :: [Var] -> Arguments -> [(Var, Term)]
make_substitutions_of :: [Var] -> Arguments -> [(Var, Term)]
make_substitutions_of [Var]
_ (Right [Modifier]
mods) = [Modifier] -> [(Var, Term)]
substitutions_of [Modifier]
mods
make_substitutions_of [Var]
xs (Left [Term]
args) = forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
xs [Term]
args
project :: Tagged -> DomId -> Maybe Tagged
project :: Tagged -> [Char] -> Maybe Tagged
project (Product [Tagged]
tvs,[Char]
_) [Char]
ty = forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
asum (forall a b. (a -> b) -> [a] -> [b]
map forall {a}. (a, [Char]) -> Maybe (a, [Char])
try [Tagged]
tvs)
where try :: (a, [Char]) -> Maybe (a, [Char])
try tv :: (a, [Char])
tv@(a
v,[Char]
ty') | [Char]
ty forall a. Eq a => a -> a -> Bool
== [Char]
ty' = forall a. a -> Maybe a
Just (a, [Char])
tv
try (a, [Char])
_ = forall a. Maybe a
Nothing
project Tagged
_ [Char]
_ = forall a. Maybe a
Nothing
emptySubs :: Subs
emptySubs :: Subs
emptySubs = forall k a. Map k a
M.empty
subsUnion :: Subs -> Subs -> Subs
subsUnion :: Subs -> Subs -> Subs
subsUnion = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall k a. Ord k => Map k a -> Map k a -> Map k a
M.union
subsUnions :: [Subs] -> Subs
subsUnions :: [Subs] -> Subs
subsUnions = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Subs -> Subs -> Subs
subsUnion forall k a. Map k a
M.empty
type Refiner = M.Map DomId Domain
emptyRefiner :: Refiner
emptyRefiner :: Refiner
emptyRefiner = forall k a. Map k a
M.empty
refine_specification :: Spec -> Refiner -> Spec
refine_specification :: Spec -> Refiner -> Spec
refine_specification Spec
spec Refiner
rm =
Spec
spec { decls :: Map [Char] TypeSpec
decls = forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
M.foldrWithKey [Char] -> TypeSpec -> Map [Char] TypeSpec -> Map [Char] TypeSpec
reinserter (Spec -> Map [Char] TypeSpec
decls Spec
spec) (Spec -> Map [Char] TypeSpec
decls Spec
spec) }
where reinserter :: [Char] -> TypeSpec -> Map [Char] TypeSpec -> Map [Char] TypeSpec
reinserter [Char]
k TypeSpec
tspec Map [Char] TypeSpec
sm' = case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup [Char]
k Refiner
rm of
Maybe Domain
Nothing -> Map [Char] TypeSpec
sm'
Just Domain
d -> case (Domain
d, TypeSpec -> Domain
domain TypeSpec
tspec) of
(Strings [[Char]]
ss, Domain
AnyString) -> Map [Char] TypeSpec
sm''
(Strings [[Char]]
ss, Strings [[Char]]
ss')
| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [[Char]]
ss') [[Char]]
ss -> Map [Char] TypeSpec
sm''
(Ints [Int]
is, Domain
AnyInt) -> Map [Char] TypeSpec
sm''
(Ints [Int]
is, Ints [Int]
is')
| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
is') [Int]
is -> Map [Char] TypeSpec
sm''
(Domain, Domain)
_ -> Map [Char] TypeSpec
sm'
where sm'' :: Map [Char] TypeSpec
sm'' = forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert [Char]
k (TypeSpec
tspec {domain :: Domain
domain = Domain
d}) Map [Char] TypeSpec
sm'
actor_decl :: TypeSpec
actor_decl :: TypeSpec
actor_decl = TypeSpec { kind :: Kind
kind = FactSpec -> Kind
Fact (Bool -> Bool -> FactSpec
FactSpec Bool
False Bool
True)
, domain :: Domain
domain = Domain
AnyString
, domain_constraint :: Term
domain_constraint = Bool -> Term
BoolLit Bool
True
, restriction :: Maybe Restriction
restriction = forall a. Maybe a
Nothing
, derivation :: [Derivation]
derivation = []
, conditions :: [Term]
conditions = []
, closed :: Bool
closed = Bool
True
}
int_decl :: TypeSpec
int_decl :: TypeSpec
int_decl = TypeSpec { kind :: Kind
kind = FactSpec -> Kind
Fact (Bool -> Bool -> FactSpec
FactSpec Bool
False Bool
False)
, domain :: Domain
domain = Domain
AnyInt
, domain_constraint :: Term
domain_constraint = Bool -> Term
BoolLit Bool
True
, restriction :: Maybe Restriction
restriction = forall a. Maybe a
Nothing
, derivation :: [Derivation]
derivation = []
, closed :: Bool
closed = Bool
True
, conditions :: [Term]
conditions = [] }
ints_decl :: [Int] -> TypeSpec
ints_decl :: [Int] -> TypeSpec
ints_decl [Int]
is = TypeSpec
int_decl { domain :: Domain
domain = [Int] -> Domain
Ints [Int]
is }
string_decl :: TypeSpec
string_decl :: TypeSpec
string_decl = TypeSpec { kind :: Kind
kind = FactSpec -> Kind
Fact (Bool -> Bool -> FactSpec
FactSpec Bool
False Bool
False)
, domain :: Domain
domain = Domain
AnyString
, domain_constraint :: Term
domain_constraint = Bool -> Term
BoolLit Bool
True
, restriction :: Maybe Restriction
restriction = forall a. Maybe a
Nothing
, derivation :: [Derivation]
derivation = []
, closed :: Bool
closed = Bool
True
, conditions :: [Term]
conditions = [] }
strings_decl :: [String] -> TypeSpec
strings_decl :: [[Char]] -> TypeSpec
strings_decl [[Char]]
ss =
TypeSpec { kind :: Kind
kind = FactSpec -> Kind
Fact (Bool -> Bool -> FactSpec
FactSpec Bool
False Bool
False)
, domain :: Domain
domain = [[Char]] -> Domain
Strings [[Char]]
ss
, domain_constraint :: Term
domain_constraint = Bool -> Term
BoolLit Bool
True
, restriction :: Maybe Restriction
restriction = forall a. Maybe a
Nothing
, derivation :: [Derivation]
derivation = []
, closed :: Bool
closed = Bool
True
, conditions :: [Term]
conditions = [] }
newtype TaggedJSON = TaggedJSON Tagged
instance ToJSON TaggedJSON where
toJSON :: TaggedJSON -> Value
toJSON (TaggedJSON te :: Tagged
te@(Elem
v,[Char]
d)) = case Elem
v of
String [Char]
s -> [Pair] -> Value
object [ Key
"tagged-type" forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
.= Text -> Value
JSON.String Text
"string", Key
"fact-type" forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
.= forall a. ToJSON a => a -> Value
toJSON [Char]
d, Key
"value" forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
.= forall a. ToJSON a => a -> Value
toJSON [Char]
s, Key
"textual" forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
.= forall a. ToJSON a => a -> Value
toJSON (Tagged -> [Char]
ppTagged Tagged
te) ]
Int Int
i -> [Pair] -> Value
object [ Key
"tagged-type" forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
.= Text -> Value
JSON.String Text
"int", Key
"fact-type" forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
.= forall a. ToJSON a => a -> Value
toJSON [Char]
d, Key
"value" forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
.= forall a. ToJSON a => a -> Value
toJSON Int
i, Key
"textual" forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
.= forall a. ToJSON a => a -> Value
toJSON (Tagged -> [Char]
ppTagged Tagged
te) ]
Product [Tagged]
tes -> [Pair] -> Value
object [ Key
"tagged-type" forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
.= Text -> Value
JSON.String Text
"product", Key
"fact-type" forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
.= forall a. ToJSON a => a -> Value
toJSON [Char]
d, Key
"arguments" forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
.= forall a. ToJSON a => a -> Value
toJSON (forall a b. (a -> b) -> [a] -> [b]
map Tagged -> TaggedJSON
TaggedJSON [Tagged]
tes), Key
"textual" forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
.= forall a. ToJSON a => a -> Value
toJSON (Tagged -> [Char]
ppTagged Tagged
te) ]