{-# 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 identifiers
type Tagged     = (Elem, DomId)

data Var        = Var DomId String {- decoration -}
                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 -- with var instantiated instead as the value of expr
                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 {- whether closed world assumption is made for this type -}
                    , 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 -- TODO move to outer AST
                    , 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] -- for record-keeping only, semantics in static-eval
                    , DutySpec -> [[Char]]
terminating_acts  :: [DomId] -- for record-keeping only, semantics in static-eval
                    , DutySpec -> [[Char]]
creating_acts     :: [DomId] -- for record-keeping only, semantics in static-eval
                    , 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)

-- | Union of specifications with overrides/replacements, not concretizations
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)
       }

-- | Right-based union over type declarations, only replacement, no concretization
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) -- used for actor identifiers
                          , ([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-environment pairs, restricting either:
-- * the components of the initial state (all instantiations of <TYPE> restricted by <ENV>)
--    (can be thought of as the Genesis transition, constructing the Garden of Eden)
-- * the possible actions performed in a state, only the actions <TYPE> are enabled 
--    if they are consistent with <ENV>
type Initialiser= [Effect] 

emptyInitialiser :: Initialiser
emptyInitialiser :: [Effect]
emptyInitialiser = []

data Statement  = Trans [Var] TransType (Either Term (DomId, Arguments)) -- foreach-application that should evaluate to exactly one act
                | 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 {- whether requested instances must hold true -} [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  {- act id -}-> 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 {- duty id -} -> DomId {- act id -} -> 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 {- duty id -} -> DomId {- act id -} -> 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 {- duty id -} -> DomId {- act id -} -> 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            -- execute computed instance
             | CTrigger [Var] Term   -- execute instance to be computed
             | CCreate [Var] Term
             | CTerminate [Var] Term
             | CObfuscate [Var] Term
             | CQuery Term
             | CInstQuery Bool {- whether generated instances must be present -} [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 -- should perhaps not be exposed to the user, auxiliary
                | Untag Term     -- auxiliary
                | 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]
"~"

-- instance Show Elem where
--   show v = case v of
--     String s    -> show s
--     Int i       -> show i
--     Product cs  -> "(" ++ intercalate "," (map show_component cs) ++ ")"

-- instance Show Domain where
--   show r = case r of
--     Time          -> "<TIME>"
--     AnyString     -> "<STRING>" 
--     Strings ss    -> "<STRING:" ++ intercalate "," (map show ss) ++ ">"
--     AnyInt        -> "<INT>"
--     Ints is       -> "<INT:" ++ intercalate "," (map show is) ++ ">"
--     Products rs   -> "(" ++ intercalate " * " (map show rs) ++ ")"

-- instance Show Modifier where
--   show (Rename dt1 dt2) = show dt1 ++ " = " ++ show dt2

-- instance Show Var where
--   show (Var ty dec) = ty ++ dec

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

-- environments

emptySubs :: Subs
emptySubs :: Subs
emptySubs = forall k a. Map k a
M.empty

-- | right-biased
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

{-
subsUnify :: Subs -> Subs -> Bool 
subsUnify e1 = M.foldrWithKey op True 
  where op k v res | Just v' <- M.lookup k e1, v /= v' = False
                   | otherwise                         = res
-}

-- functions related to partial instantiation (refinement)

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) ]