{-# 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 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
Eq Var
-> (Var -> Var -> Ordering)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Var)
-> (Var -> Var -> Var)
-> Ord 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
$cp1Ord :: Eq Var
Ord, Var -> Var -> Bool
(Var -> Var -> Bool) -> (Var -> Var -> Bool) -> Eq Var
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 -> String
(Int -> Var -> ShowS)
-> (Var -> String) -> ([Var] -> ShowS) -> Show Var
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Var] -> ShowS
$cshowList :: [Var] -> ShowS
show :: Var -> String
$cshow :: Var -> String
showsPrec :: Int -> Var -> ShowS
$cshowsPrec :: Int -> Var -> ShowS
Show, ReadPrec [Var]
ReadPrec Var
Int -> ReadS Var
ReadS [Var]
(Int -> ReadS Var)
-> ReadS [Var] -> ReadPrec Var -> ReadPrec [Var] -> Read 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
Eq Elem
-> (Elem -> Elem -> Ordering)
-> (Elem -> Elem -> Bool)
-> (Elem -> Elem -> Bool)
-> (Elem -> Elem -> Bool)
-> (Elem -> Elem -> Bool)
-> (Elem -> Elem -> Elem)
-> (Elem -> Elem -> Elem)
-> Ord 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
$cp1Ord :: Eq Elem
Ord, Elem -> Elem -> Bool
(Elem -> Elem -> Bool) -> (Elem -> Elem -> Bool) -> Eq Elem
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 -> String
(Int -> Elem -> ShowS)
-> (Elem -> String) -> ([Elem] -> ShowS) -> Show Elem
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Elem] -> ShowS
$cshowList :: [Elem] -> ShowS
show :: Elem -> String
$cshow :: Elem -> String
showsPrec :: Int -> Elem -> ShowS
$cshowsPrec :: Int -> Elem -> ShowS
Show, ReadPrec [Elem]
ReadPrec Elem
Int -> ReadS Elem
ReadS [Elem]
(Int -> ReadS Elem)
-> ReadS [Elem] -> ReadPrec Elem -> ReadPrec [Elem] -> Read 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
Eq Domain
-> (Domain -> Domain -> Ordering)
-> (Domain -> Domain -> Bool)
-> (Domain -> Domain -> Bool)
-> (Domain -> Domain -> Bool)
-> (Domain -> Domain -> Bool)
-> (Domain -> Domain -> Domain)
-> (Domain -> Domain -> Domain)
-> Ord 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
$cp1Ord :: Eq Domain
Ord, Domain -> Domain -> Bool
(Domain -> Domain -> Bool)
-> (Domain -> Domain -> Bool) -> Eq Domain
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 -> String
(Int -> Domain -> ShowS)
-> (Domain -> String) -> ([Domain] -> ShowS) -> Show Domain
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Domain] -> ShowS
$cshowList :: [Domain] -> ShowS
show :: Domain -> String
$cshow :: Domain -> String
showsPrec :: Int -> Domain -> ShowS
$cshowsPrec :: Int -> Domain -> ShowS
Show, ReadPrec [Domain]
ReadPrec Domain
Int -> ReadS Domain
ReadS [Domain]
(Int -> ReadS Domain)
-> ReadS [Domain]
-> ReadPrec Domain
-> ReadPrec [Domain]
-> Read 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 [String]
_ -> Bool
True
Ints [Int]
_ -> Bool
True
Products [Var]
vars -> (Var -> Bool) -> [Var] -> Bool
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 (TypeSpec -> Domain) -> Maybe TypeSpec -> Maybe Domain
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TypeSpec -> Domain
domain (Spec -> String -> Maybe TypeSpec
find_decl Spec
spec (Spec -> Var -> String
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 -> String -> Maybe Bool
closed_type Spec
spec String
d = (TypeSpec -> Bool) -> Maybe TypeSpec -> Maybe Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TypeSpec -> Bool
closed (Spec -> String -> Maybe TypeSpec
find_decl Spec
spec String
d)
type Arguments = Either [Term] [Modifier]
data Modifier = Rename Var Term
deriving (Eq Modifier
Eq Modifier
-> (Modifier -> Modifier -> Ordering)
-> (Modifier -> Modifier -> Bool)
-> (Modifier -> Modifier -> Bool)
-> (Modifier -> Modifier -> Bool)
-> (Modifier -> Modifier -> Bool)
-> (Modifier -> Modifier -> Modifier)
-> (Modifier -> Modifier -> Modifier)
-> Ord 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
$cp1Ord :: Eq Modifier
Ord, Modifier -> Modifier -> Bool
(Modifier -> Modifier -> Bool)
-> (Modifier -> Modifier -> Bool) -> Eq Modifier
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 -> String
(Int -> Modifier -> ShowS)
-> (Modifier -> String) -> ([Modifier] -> ShowS) -> Show Modifier
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Modifier] -> ShowS
$cshowList :: [Modifier] -> ShowS
show :: Modifier -> String
$cshow :: Modifier -> String
showsPrec :: Int -> Modifier -> ShowS
$cshowsPrec :: Int -> Modifier -> ShowS
Show, ReadPrec [Modifier]
ReadPrec Modifier
Int -> ReadS Modifier
ReadS [Modifier]
(Int -> ReadS Modifier)
-> ReadS [Modifier]
-> ReadPrec Modifier
-> ReadPrec [Modifier]
-> Read 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
Eq Kind
-> (Kind -> Kind -> Ordering)
-> (Kind -> Kind -> Bool)
-> (Kind -> Kind -> Bool)
-> (Kind -> Kind -> Bool)
-> (Kind -> Kind -> Bool)
-> (Kind -> Kind -> Kind)
-> (Kind -> Kind -> Kind)
-> Ord 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
$cp1Ord :: Eq Kind
Ord, Kind -> Kind -> Bool
(Kind -> Kind -> Bool) -> (Kind -> Kind -> Bool) -> Eq Kind
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 -> String
(Int -> Kind -> ShowS)
-> (Kind -> String) -> ([Kind] -> ShowS) -> Show Kind
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Kind] -> ShowS
$cshowList :: [Kind] -> ShowS
show :: Kind -> String
$cshow :: Kind -> String
showsPrec :: Int -> Kind -> ShowS
$cshowsPrec :: Int -> Kind -> ShowS
Show, ReadPrec [Kind]
ReadPrec Kind
Int -> ReadS Kind
ReadS [Kind]
(Int -> ReadS Kind)
-> ReadS [Kind] -> ReadPrec Kind -> ReadPrec [Kind] -> Read 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 TypeSpec = TypeSpec {
TypeSpec -> Kind
kind :: Kind
, TypeSpec -> Domain
domain :: Domain
, TypeSpec -> Term
domain_constraint :: Term
, TypeSpec -> [Derivation]
derivation :: [Derivation]
, TypeSpec -> Bool
closed :: Bool
, TypeSpec -> [Term]
conditions :: [Term]
} deriving (TypeSpec -> TypeSpec -> Bool
(TypeSpec -> TypeSpec -> Bool)
-> (TypeSpec -> TypeSpec -> Bool) -> Eq TypeSpec
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 -> String
(Int -> TypeSpec -> ShowS)
-> (TypeSpec -> String) -> ([TypeSpec] -> ShowS) -> Show TypeSpec
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TypeSpec] -> ShowS
$cshowList :: [TypeSpec] -> ShowS
show :: TypeSpec -> String
$cshow :: TypeSpec -> String
showsPrec :: Int -> TypeSpec -> ShowS
$cshowsPrec :: Int -> TypeSpec -> ShowS
Show, ReadPrec [TypeSpec]
ReadPrec TypeSpec
Int -> ReadS TypeSpec
ReadS [TypeSpec]
(Int -> ReadS TypeSpec)
-> ReadS [TypeSpec]
-> ReadPrec TypeSpec
-> ReadPrec [TypeSpec]
-> Read 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
Eq Derivation
-> (Derivation -> Derivation -> Ordering)
-> (Derivation -> Derivation -> Bool)
-> (Derivation -> Derivation -> Bool)
-> (Derivation -> Derivation -> Bool)
-> (Derivation -> Derivation -> Bool)
-> (Derivation -> Derivation -> Derivation)
-> (Derivation -> Derivation -> Derivation)
-> Ord 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
$cp1Ord :: Eq Derivation
Ord, Derivation -> Derivation -> Bool
(Derivation -> Derivation -> Bool)
-> (Derivation -> Derivation -> Bool) -> Eq Derivation
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 -> String
(Int -> Derivation -> ShowS)
-> (Derivation -> String)
-> ([Derivation] -> ShowS)
-> Show Derivation
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Derivation] -> ShowS
$cshowList :: [Derivation] -> ShowS
show :: Derivation -> String
$cshow :: Derivation -> String
showsPrec :: Int -> Derivation -> ShowS
$cshowsPrec :: Int -> Derivation -> ShowS
Show, ReadPrec [Derivation]
ReadPrec Derivation
Int -> ReadS Derivation
ReadS [Derivation]
(Int -> ReadS Derivation)
-> ReadS [Derivation]
-> ReadPrec Derivation
-> ReadPrec [Derivation]
-> Read 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
Eq FactSpec
-> (FactSpec -> FactSpec -> Ordering)
-> (FactSpec -> FactSpec -> Bool)
-> (FactSpec -> FactSpec -> Bool)
-> (FactSpec -> FactSpec -> Bool)
-> (FactSpec -> FactSpec -> Bool)
-> (FactSpec -> FactSpec -> FactSpec)
-> (FactSpec -> FactSpec -> FactSpec)
-> Ord 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
$cp1Ord :: Eq FactSpec
Ord, FactSpec -> FactSpec -> Bool
(FactSpec -> FactSpec -> Bool)
-> (FactSpec -> FactSpec -> Bool) -> Eq FactSpec
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 -> String
(Int -> FactSpec -> ShowS)
-> (FactSpec -> String) -> ([FactSpec] -> ShowS) -> Show FactSpec
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FactSpec] -> ShowS
$cshowList :: [FactSpec] -> ShowS
show :: FactSpec -> String
$cshow :: FactSpec -> String
showsPrec :: Int -> FactSpec -> ShowS
$cshowsPrec :: Int -> FactSpec -> ShowS
Show, ReadPrec [FactSpec]
ReadPrec FactSpec
Int -> ReadS FactSpec
ReadS [FactSpec]
(Int -> ReadS FactSpec)
-> ReadS [FactSpec]
-> ReadPrec FactSpec
-> ReadPrec [FactSpec]
-> Read 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 -> [String]
enforcing_acts :: [DomId]
, DutySpec -> [Term]
violated_when :: [Term]
}
deriving (Eq DutySpec
Eq DutySpec
-> (DutySpec -> DutySpec -> Ordering)
-> (DutySpec -> DutySpec -> Bool)
-> (DutySpec -> DutySpec -> Bool)
-> (DutySpec -> DutySpec -> Bool)
-> (DutySpec -> DutySpec -> Bool)
-> (DutySpec -> DutySpec -> DutySpec)
-> (DutySpec -> DutySpec -> DutySpec)
-> Ord 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
$cp1Ord :: Eq DutySpec
Ord, DutySpec -> DutySpec -> Bool
(DutySpec -> DutySpec -> Bool)
-> (DutySpec -> DutySpec -> Bool) -> Eq DutySpec
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 -> String
(Int -> DutySpec -> ShowS)
-> (DutySpec -> String) -> ([DutySpec] -> ShowS) -> Show DutySpec
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DutySpec] -> ShowS
$cshowList :: [DutySpec] -> ShowS
show :: DutySpec -> String
$cshow :: DutySpec -> String
showsPrec :: Int -> DutySpec -> ShowS
$cshowsPrec :: Int -> DutySpec -> ShowS
Show, ReadPrec [DutySpec]
ReadPrec DutySpec
Int -> ReadS DutySpec
ReadS [DutySpec]
(Int -> ReadS DutySpec)
-> ReadS [DutySpec]
-> ReadPrec DutySpec
-> ReadPrec [DutySpec]
-> Read 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]
}
deriving (Eq ActSpec
Eq ActSpec
-> (ActSpec -> ActSpec -> Ordering)
-> (ActSpec -> ActSpec -> Bool)
-> (ActSpec -> ActSpec -> Bool)
-> (ActSpec -> ActSpec -> Bool)
-> (ActSpec -> ActSpec -> Bool)
-> (ActSpec -> ActSpec -> ActSpec)
-> (ActSpec -> ActSpec -> ActSpec)
-> Ord 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
$cp1Ord :: Eq ActSpec
Ord, ActSpec -> ActSpec -> Bool
(ActSpec -> ActSpec -> Bool)
-> (ActSpec -> ActSpec -> Bool) -> Eq ActSpec
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 -> String
(Int -> ActSpec -> ShowS)
-> (ActSpec -> String) -> ([ActSpec] -> ShowS) -> Show ActSpec
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ActSpec] -> ShowS
$cshowList :: [ActSpec] -> ShowS
show :: ActSpec -> String
$cshow :: ActSpec -> String
showsPrec :: Int -> ActSpec -> ShowS
$cshowsPrec :: Int -> ActSpec -> ShowS
Show, ReadPrec [ActSpec]
ReadPrec ActSpec
Int -> ReadS ActSpec
ReadS [ActSpec]
(Int -> ReadS ActSpec)
-> ReadS [ActSpec]
-> ReadPrec ActSpec
-> ReadPrec [ActSpec]
-> Read 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
Eq Effect
-> (Effect -> Effect -> Ordering)
-> (Effect -> Effect -> Bool)
-> (Effect -> Effect -> Bool)
-> (Effect -> Effect -> Bool)
-> (Effect -> Effect -> Bool)
-> (Effect -> Effect -> Effect)
-> (Effect -> Effect -> Effect)
-> Ord 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
$cp1Ord :: Eq Effect
Ord, Effect -> Effect -> Bool
(Effect -> Effect -> Bool)
-> (Effect -> Effect -> Bool) -> Eq Effect
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 -> String
(Int -> Effect -> ShowS)
-> (Effect -> String) -> ([Effect] -> ShowS) -> Show Effect
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Effect] -> ShowS
$cshowList :: [Effect] -> ShowS
show :: Effect -> String
$cshow :: Effect -> String
showsPrec :: Int -> Effect -> ShowS
$cshowsPrec :: Int -> Effect -> ShowS
Show, ReadPrec [Effect]
ReadPrec Effect
Int -> ReadS Effect
ReadS [Effect]
(Int -> ReadS Effect)
-> ReadS [Effect]
-> ReadPrec Effect
-> ReadPrec [Effect]
-> Read 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
Eq Sync
-> (Sync -> Sync -> Ordering)
-> (Sync -> Sync -> Bool)
-> (Sync -> Sync -> Bool)
-> (Sync -> Sync -> Bool)
-> (Sync -> Sync -> Bool)
-> (Sync -> Sync -> Sync)
-> (Sync -> Sync -> Sync)
-> Ord 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
$cp1Ord :: Eq Sync
Ord, Sync -> Sync -> Bool
(Sync -> Sync -> Bool) -> (Sync -> Sync -> Bool) -> Eq Sync
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 -> String
(Int -> Sync -> ShowS)
-> (Sync -> String) -> ([Sync] -> ShowS) -> Show Sync
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Sync] -> ShowS
$cshowList :: [Sync] -> ShowS
show :: Sync -> String
$cshow :: Sync -> String
showsPrec :: Int -> Sync -> ShowS
$cshowsPrec :: Int -> Sync -> ShowS
Show, ReadPrec [Sync]
ReadPrec Sync
Int -> ReadS Sync
ReadS [Sync]
(Int -> ReadS Sync)
-> ReadS [Sync] -> ReadPrec Sync -> ReadPrec [Sync] -> Read 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]
}
deriving (Eq EventSpec
Eq EventSpec
-> (EventSpec -> EventSpec -> Ordering)
-> (EventSpec -> EventSpec -> Bool)
-> (EventSpec -> EventSpec -> Bool)
-> (EventSpec -> EventSpec -> Bool)
-> (EventSpec -> EventSpec -> Bool)
-> (EventSpec -> EventSpec -> EventSpec)
-> (EventSpec -> EventSpec -> EventSpec)
-> Ord 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
$cp1Ord :: Eq EventSpec
Ord, EventSpec -> EventSpec -> Bool
(EventSpec -> EventSpec -> Bool)
-> (EventSpec -> EventSpec -> Bool) -> Eq EventSpec
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 -> String
(Int -> EventSpec -> ShowS)
-> (EventSpec -> String)
-> ([EventSpec] -> ShowS)
-> Show EventSpec
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [EventSpec] -> ShowS
$cshowList :: [EventSpec] -> ShowS
show :: EventSpec -> String
$cshow :: EventSpec -> String
showsPrec :: Int -> EventSpec -> ShowS
$cshowsPrec :: Int -> EventSpec -> ShowS
Show, ReadPrec [EventSpec]
ReadPrec EventSpec
Int -> ReadS EventSpec
ReadS [EventSpec]
(Int -> ReadS EventSpec)
-> ReadS [EventSpec]
-> ReadPrec EventSpec
-> ReadPrec [EventSpec]
-> Read 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 String TypeSpec
decls :: M.Map DomId TypeSpec
, Spec -> Map String String
aliases :: M.Map DomId DomId
}
deriving (Spec -> Spec -> Bool
(Spec -> Spec -> Bool) -> (Spec -> Spec -> Bool) -> Eq Spec
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 -> String
(Int -> Spec -> ShowS)
-> (Spec -> String) -> ([Spec] -> ShowS) -> Show Spec
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Spec] -> ShowS
$cshowList :: [Spec] -> ShowS
show :: Spec -> String
$cshow :: Spec -> String
showsPrec :: Int -> Spec -> ShowS
$cshowsPrec :: Int -> Spec -> ShowS
Show, ReadPrec [Spec]
ReadPrec Spec
Int -> ReadS Spec
ReadS [Spec]
(Int -> ReadS Spec)
-> ReadS [Spec] -> ReadPrec Spec -> ReadPrec [Spec] -> Read 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 :: Map String TypeSpec -> Map String String -> Spec
Spec {decls :: Map String TypeSpec
decls = Map String TypeSpec -> Map String TypeSpec -> Map String TypeSpec
decls_union (Spec -> Map String TypeSpec
decls Spec
old_spec) (Spec -> Map String TypeSpec
decls Spec
new_spec)
,aliases :: Map String String
aliases = Map String String -> Map String String -> Map String String
aliases_union (Spec -> Map String String
aliases Spec
old_spec) (Spec -> Map String String
aliases Spec
new_spec)
}
decls_union :: M.Map DomId TypeSpec -> M.Map DomId TypeSpec -> M.Map DomId TypeSpec
decls_union :: Map String TypeSpec -> Map String TypeSpec -> Map String TypeSpec
decls_union Map String TypeSpec
old Map String TypeSpec
new = Map String TypeSpec -> Map String TypeSpec -> Map String TypeSpec
forall k a. Ord k => Map k a -> Map k a -> Map k a
M.union Map String TypeSpec
new Map String TypeSpec
old
aliases_union :: M.Map DomId DomId -> M.Map DomId DomId -> M.Map DomId DomId
aliases_union :: Map String String -> Map String String -> Map String String
aliases_union Map String String
old Map String String
new = Map String String -> Map String String -> Map String String
forall k a. Ord k => Map k a -> Map k a -> Map k a
M.union Map String String
new Map String String
old
actor_ref_address :: String
actor_ref_address :: String
actor_ref_address = String
"ref"
emptySpec :: Spec
emptySpec :: Spec
emptySpec = Spec :: Map String TypeSpec -> Map String String -> Spec
Spec { decls :: Map String TypeSpec
decls = Map String TypeSpec
built_in_decls, aliases :: Map String String
aliases = Map String String
forall k a. Map k a
M.empty}
where built_in_decls :: Map String TypeSpec
built_in_decls = [(String, TypeSpec)] -> Map String TypeSpec
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [
(String
"int", TypeSpec
int_decl)
, (String
actor_ref_address, TypeSpec
string_decl)
, (String
"actor", TypeSpec
actor_decl)
]
basic :: Spec -> S.Set DomId
basic :: Spec -> Set String
basic Spec
spec = (String -> TypeSpec -> Set String -> Set String)
-> Set String -> Map String TypeSpec -> Set String
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
M.foldrWithKey String -> TypeSpec -> Set String -> Set String
forall a. Ord a => a -> TypeSpec -> Set a -> Set a
op Set String
forall a. Set a
S.empty (Spec -> Map String TypeSpec
decls Spec
spec)
where op :: a -> TypeSpec -> Set a -> Set a
op a
d TypeSpec
tspec Set a
res | [Derivation] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (TypeSpec -> [Derivation]
derivation TypeSpec
tspec) = a -> Set a -> Set a
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 String
derived Spec
spec = (String -> TypeSpec -> Set String -> Set String)
-> Set String -> Map String TypeSpec -> Set String
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
M.foldrWithKey String -> TypeSpec -> Set String -> Set String
forall a. Ord a => a -> TypeSpec -> Set a -> Set a
op Set String
forall a. Set a
S.empty (Spec -> Map String TypeSpec
decls Spec
spec)
where op :: a -> TypeSpec -> Set a -> Set a
op a
d TypeSpec
tspec Set a
res | [Derivation] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (TypeSpec -> [Derivation]
derivation TypeSpec
tspec) = Set a
res
| Bool
otherwise = a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
S.insert a
d Set a
res
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
Eq TransType
-> (TransType -> TransType -> Ordering)
-> (TransType -> TransType -> Bool)
-> (TransType -> TransType -> Bool)
-> (TransType -> TransType -> Bool)
-> (TransType -> TransType -> Bool)
-> (TransType -> TransType -> TransType)
-> (TransType -> TransType -> TransType)
-> Ord 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
$cp1Ord :: Eq TransType
Ord, TransType -> TransType -> Bool
(TransType -> TransType -> Bool)
-> (TransType -> TransType -> Bool) -> Eq TransType
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]
(TransType -> TransType)
-> (TransType -> TransType)
-> (Int -> TransType)
-> (TransType -> Int)
-> (TransType -> [TransType])
-> (TransType -> TransType -> [TransType])
-> (TransType -> TransType -> [TransType])
-> (TransType -> TransType -> TransType -> [TransType])
-> Enum 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
| PDeclBlock [Decl]
| PSkip
deriving (Phrase -> Phrase -> Bool
(Phrase -> Phrase -> Bool)
-> (Phrase -> Phrase -> Bool) -> Eq Phrase
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 -> String
(Int -> Phrase -> ShowS)
-> (Phrase -> String) -> ([Phrase] -> ShowS) -> Show Phrase
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Phrase] -> ShowS
$cshowList :: [Phrase] -> ShowS
show :: Phrase -> String
$cshow :: Phrase -> String
showsPrec :: Int -> Phrase -> ShowS
$cshowsPrec :: Int -> Phrase -> ShowS
Show, ReadPrec [Phrase]
ReadPrec Phrase
Int -> ReadS Phrase
ReadS [Phrase]
(Int -> ReadS Phrase)
-> ReadS [Phrase]
-> ReadPrec Phrase
-> ReadPrec [Phrase]
-> Read 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
(Decl -> Decl -> Bool) -> (Decl -> Decl -> Bool) -> Eq Decl
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 -> String
(Int -> Decl -> ShowS)
-> (Decl -> String) -> ([Decl] -> ShowS) -> Show Decl
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Decl] -> ShowS
$cshowList :: [Decl] -> ShowS
show :: Decl -> String
$cshow :: Decl -> String
showsPrec :: Int -> Decl -> ShowS
$cshowsPrec :: Int -> Decl -> ShowS
Show, ReadPrec [Decl]
ReadPrec Decl
Int -> ReadS Decl
ReadS [Decl]
(Int -> ReadS Decl)
-> ReadS [Decl] -> ReadPrec Decl -> ReadPrec [Decl] -> Read 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)
introducesName :: Decl -> Bool
introducesName :: Decl -> Bool
introducesName (TypeDecl String
_ TypeSpec
_) = Bool
True
introducesName (TypeExt String
_ [ModClause]
_) = Bool
False
introducesName (PlaceholderDecl String
_ String
_) = Bool
True
extend_spec :: [Decl] -> Spec -> Spec
extend_spec :: [Decl] -> Spec -> Spec
extend_spec = (Spec -> [Decl] -> Spec) -> [Decl] -> Spec -> Spec
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Decl -> Spec -> Spec) -> Spec -> [Decl] -> Spec
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 String
ty TypeSpec
tyspec) Spec
spec = Spec
spec { decls :: Map String TypeSpec
decls = String -> TypeSpec -> Map String TypeSpec -> Map String TypeSpec
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert String
ty TypeSpec
tyspec (Spec -> Map String TypeSpec
decls Spec
spec) }
op (PlaceholderDecl String
f String
t) Spec
spec = Spec
spec { aliases :: Map String String
aliases = String -> String -> Map String String -> Map String String
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert String
f String
t (Spec -> Map String String
aliases Spec
spec) }
op Decl
_ Spec
spec = Spec
spec
data ModClause = ConditionedByCl [Term]
| DerivationCl [Derivation]
| PostCondCl [Effect]
| SyncCl [Sync]
| ViolationCl [Term]
| EnforcingActsCl [DomId]
deriving (ModClause -> ModClause -> Bool
(ModClause -> ModClause -> Bool)
-> (ModClause -> ModClause -> Bool) -> Eq ModClause
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 -> String
(Int -> ModClause -> ShowS)
-> (ModClause -> String)
-> ([ModClause] -> ShowS)
-> Show ModClause
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ModClause] -> ShowS
$cshowList :: [ModClause] -> ShowS
show :: ModClause -> String
$cshow :: ModClause -> String
showsPrec :: Int -> ModClause -> ShowS
$cshowsPrec :: Int -> ModClause -> ShowS
Show, ReadPrec [ModClause]
ReadPrec ModClause
Int -> ReadS ModClause
ReadS [ModClause]
(Int -> ReadS ModClause)
-> ReadS [ModClause]
-> ReadPrec ModClause
-> ReadPrec [ModClause]
-> Read 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)
apply_ext :: DomId -> [ModClause] -> Spec -> Spec
apply_ext :: String -> [ModClause] -> Spec -> Spec
apply_ext String
ty [ModClause]
clauses Spec
spec = case Spec -> String -> Maybe TypeSpec
find_decl Spec
spec String
ty of
Maybe TypeSpec
Nothing -> Spec
spec
Just TypeSpec
tspec -> Spec
spec { decls :: Map String TypeSpec
decls = String -> TypeSpec -> Map String TypeSpec -> Map String TypeSpec
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert String
ty (String -> [ModClause] -> TypeSpec -> TypeSpec
apply_type_ext String
ty [ModClause]
clauses TypeSpec
tspec) (Spec -> Map String TypeSpec
decls Spec
spec) }
apply_type_ext :: DomId -> [ModClause] -> TypeSpec -> TypeSpec
apply_type_ext :: String -> [ModClause] -> TypeSpec -> TypeSpec
apply_type_ext String
ty [ModClause]
clauses TypeSpec
tspec = (ModClause -> TypeSpec -> TypeSpec)
-> TypeSpec -> [ModClause] -> TypeSpec
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ModClause -> TypeSpec -> TypeSpec
apply_clause TypeSpec
tspec [ModClause]
clauses
where apply_clause :: ModClause -> TypeSpec -> TypeSpec
apply_clause ModClause
clause TypeSpec
tspec = case ModClause
clause of
ConditionedByCl [Term]
conds -> TypeSpec
tspec { conditions :: [Term]
conditions = [Term]
conds [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ TypeSpec -> [Term]
conditions TypeSpec
tspec }
DerivationCl [Derivation]
dvs -> TypeSpec
tspec { derivation :: [Derivation]
derivation = [Derivation]
dvs [Derivation] -> [Derivation] -> [Derivation]
forall a. [a] -> [a] -> [a]
++ TypeSpec -> [Derivation]
derivation TypeSpec
tspec }
PostCondCl [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 [Effect] -> [Effect] -> [Effect]
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 [Effect] -> [Effect] -> [Effect]
forall a. [a] -> [a] -> [a]
++ EventSpec -> [Effect]
event_effects EventSpec
espec })
add_effects Kind
s = Kind
s
SyncCl [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 (ActSpec -> Kind) -> ActSpec -> Kind
forall a b. (a -> b) -> a -> b
$ ActSpec
aspec { syncs :: [Sync]
syncs = [Sync]
ss [Sync] -> [Sync] -> [Sync]
forall a. [a] -> [a] -> [a]
++ ActSpec -> [Sync]
syncs ActSpec
aspec}
add_syncs Kind
s = Kind
s
ViolationCl [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 (DutySpec -> Kind) -> DutySpec -> Kind
forall a b. (a -> b) -> a -> b
$ DutySpec
dspec { violated_when :: [Term]
violated_when = [Term]
vs [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ DutySpec -> [Term]
violated_when DutySpec
dspec }
add_viol_conds Kind
s = Kind
s
EnforcingActsCl [String]
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 (DutySpec -> Kind) -> DutySpec -> Kind
forall a b. (a -> b) -> a -> b
$ DutySpec
dspec { enforcing_acts :: [String]
enforcing_acts = [String]
ds [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ DutySpec -> [String]
enforcing_acts DutySpec
dspec }
add_enf_acts Kind
s = Kind
s
data CPhrase = CDo Tagged
| CTrigger [Var] Term
| CCreate [Var] Term
| CTerminate [Var] Term
| CObfuscate [Var] Term
| CQuery Term
| CPOnlyDecls
| CPDir CDirective
| CSeq CPhrase CPhrase
| CPSkip
data CDirective = DirInv DomId
process_directives :: [CDirective] -> Spec -> Spec
process_directives :: [CDirective] -> Spec -> Spec
process_directives = (Spec -> [CDirective] -> Spec) -> [CDirective] -> Spec -> Spec
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((CDirective -> Spec -> Spec) -> Spec -> [CDirective] -> Spec
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 String
ty) Spec
spec = Spec
spec { decls :: Map String TypeSpec
decls = (TypeSpec -> TypeSpec)
-> String -> Map String TypeSpec -> Map String TypeSpec
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
M.adjust TypeSpec -> TypeSpec
mod String
ty (Spec -> Map String 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 String
invariants Spec
spec = ((String, TypeSpec) -> Set String -> Set String)
-> Set String -> [(String, TypeSpec)] -> Set String
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (String, TypeSpec) -> Set String -> Set String
forall a. Ord a => (a, TypeSpec) -> Set a -> Set a
op Set String
forall a. Set a
S.empty (Map String TypeSpec -> [(String, TypeSpec)]
forall k a. Map k a -> [(k, a)]
M.assocs (Spec -> Map String 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 -> a -> Set a -> Set a
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 String
actors Spec
spec = ((String, TypeSpec) -> Set String -> Set String)
-> Set String -> [(String, TypeSpec)] -> Set String
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (String, TypeSpec) -> Set String -> Set String
forall a. Ord a => (a, TypeSpec) -> Set a -> Set a
op Set String
forall a. Set a
S.empty (Map String TypeSpec -> [(String, TypeSpec)]
forall k a. Map k a -> [(k, a)]
M.assocs (Spec -> Map String 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 -> a -> Set a -> Set a
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 -> String
(Int -> Term -> ShowS)
-> (Term -> String) -> ([Term] -> ShowS) -> Show Term
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Term] -> ShowS
$cshowList :: [Term] -> ShowS
show :: Term -> String
$cshow :: Term -> String
showsPrec :: Int -> Term -> ShowS
$cshowsPrec :: Int -> Term -> ShowS
Show, Eq Term
Eq Term
-> (Term -> Term -> Ordering)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Term)
-> (Term -> Term -> Term)
-> Ord 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
$cp1Ord :: Eq Term
Ord, Term -> Term -> Bool
(Term -> Term -> Bool) -> (Term -> Term -> Bool) -> Eq Term
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]
(Int -> ReadS Term)
-> ReadS [Term] -> ReadPrec Term -> ReadPrec [Term] -> Read 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
(Value -> Value -> Bool) -> (Value -> Value -> Bool) -> Eq Value
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 -> String
(Int -> Value -> ShowS)
-> (Value -> String) -> ([Value] -> ShowS) -> Show Value
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Value] -> ShowS
$cshowList :: [Value] -> ShowS
show :: Value -> String
$cshow :: Value -> String
showsPrec :: Int -> Value -> ShowS
$cshowsPrec :: Int -> Value -> ShowS
Show)
data Type = TyStrings
| TyInts
| TyBool
| TyTagged DomId
deriving (Type -> Type -> Bool
(Type -> Type -> Bool) -> (Type -> Type -> Bool) -> Eq Type
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 -> String
(Int -> Type -> ShowS)
-> (Type -> String) -> ([Type] -> ShowS) -> Show Type
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Type] -> ShowS
$cshowList :: [Type] -> ShowS
show :: Type -> String
$cshow :: Type -> String
showsPrec :: Int -> Type -> ShowS
$cshowsPrec :: Int -> Type -> ShowS
Show)
instance Show TransType where
show :: TransType -> String
show TransType
Trigger = String
""
show TransType
AddEvent = String
"+"
show TransType
RemEvent = String
"-"
show TransType
ObfEvent = String
"~"
no_decoration :: DomId -> Var
no_decoration :: String -> Var
no_decoration String
ty = String -> String -> Var
Var String
ty String
""
remove_decoration :: Spec -> Var -> DomId
remove_decoration :: Spec -> Var -> String
remove_decoration Spec
spec (Var String
dom String
_) = Spec -> ShowS
chase_alias Spec
spec String
dom
duty_decls :: Spec -> [(DomId, DutySpec)]
duty_decls :: Spec -> [(String, DutySpec)]
duty_decls Spec
spec = ((String, TypeSpec) -> [(String, DutySpec)])
-> [(String, TypeSpec)] -> [(String, DutySpec)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (String, TypeSpec) -> [(String, DutySpec)]
forall a. (a, TypeSpec) -> [(a, DutySpec)]
op ([(String, TypeSpec)] -> [(String, DutySpec)])
-> [(String, TypeSpec)] -> [(String, DutySpec)]
forall a b. (a -> b) -> a -> b
$ Map String TypeSpec -> [(String, TypeSpec)]
forall k a. Map k a -> [(k, a)]
M.assocs (Spec -> Map String 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 -> [(String, Either EventSpec ActSpec)]
trigger_decls Spec
spec = ((String, TypeSpec) -> [(String, Either EventSpec ActSpec)])
-> [(String, TypeSpec)] -> [(String, Either EventSpec ActSpec)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (String, TypeSpec) -> [(String, Either EventSpec ActSpec)]
forall a. (a, TypeSpec) -> [(a, Either EventSpec ActSpec)]
op ([(String, TypeSpec)] -> [(String, Either EventSpec ActSpec)])
-> [(String, TypeSpec)] -> [(String, Either EventSpec ActSpec)]
forall a b. (a -> b) -> a -> b
$ Map String TypeSpec -> [(String, TypeSpec)]
forall k a. Map k a -> [(k, a)]
M.assocs (Spec -> Map String 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,EventSpec -> Either EventSpec ActSpec
forall a b. a -> Either a b
Left EventSpec
e)]
Act ActSpec
a -> [(a
d,ActSpec -> Either EventSpec ActSpec
forall a b. b -> Either a b
Right ActSpec
a)]
Kind
_ -> []
triggerable :: Spec -> DomId -> Bool
triggerable :: Spec -> String -> Bool
triggerable Spec
spec String
d = case (TypeSpec -> Kind) -> Maybe TypeSpec -> Maybe Kind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TypeSpec -> Kind
kind (Spec -> String -> Maybe TypeSpec
find_decl Spec
spec String
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 -> String -> Maybe TypeSpec
find_decl Spec
spec String
d = String -> Map String TypeSpec -> Maybe TypeSpec
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Spec -> ShowS
chase_alias Spec
spec String
d) (Spec -> Map String TypeSpec
decls Spec
spec)
find_violation_cond :: Spec -> DomId -> Maybe [Term]
find_violation_cond :: Spec -> String -> Maybe [Term]
find_violation_cond Spec
spec String
d = case String -> Map String TypeSpec -> Maybe TypeSpec
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Spec -> ShowS
chase_alias Spec
spec String
d) (Spec -> Map String TypeSpec
decls Spec
spec) of
Maybe TypeSpec
Nothing -> Maybe [Term]
forall a. Maybe a
Nothing
Just TypeSpec
ts -> case TypeSpec -> Kind
kind TypeSpec
ts of
Duty DutySpec
ds -> [Term] -> Maybe [Term]
forall a. a -> Maybe a
Just ([Term] -> Maybe [Term]) -> [Term] -> Maybe [Term]
forall a b. (a -> b) -> a -> b
$ DutySpec -> [Term]
violated_when DutySpec
ds
Kind
_ -> Maybe [Term]
forall a. Maybe a
Nothing
chase_alias :: Spec -> DomId -> DomId
chase_alias :: Spec -> ShowS
chase_alias Spec
spec String
d = Set String -> ShowS
chase_alias' Set String
forall a. Set a
S.empty String
d
where chase_alias' :: Set String -> ShowS
chase_alias' Set String
tried String
d
| String
d String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set String
tried = String
d
| Bool
otherwise = String -> ShowS -> Maybe String -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
d (Set String -> ShowS
chase_alias' (String -> Set String -> Set String
forall a. Ord a => a -> Set a -> Set a
S.insert String
d Set String
tried)) (String -> Map String String -> Maybe String
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
d (Spec -> Map String String
aliases Spec
spec))
show_arguments :: Arguments -> String
show_arguments :: Arguments -> String
show_arguments (Right [Modifier]
mods) = [Modifier] -> String
show_modifiers [Modifier]
mods
show_arguments (Left [Term]
xs) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ((Term -> String) -> [Term] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Term -> String
forall a. Show a => a -> String
show [Term]
xs) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show_modifiers :: [Modifier] -> String
show_modifiers :: [Modifier] -> String
show_modifiers [] = String
"()"
show_modifiers [Modifier]
cs = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ((Modifier -> String) -> [Modifier] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Modifier -> String
forall a. Show a => a -> String
show [Modifier]
cs) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show_projections :: [Var] -> String
show_projections :: [Var] -> String
show_projections [] = String
""
show_projections [Var]
ds = String
"[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ((Var -> String) -> [Var] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Var -> String
forall a. Show a => a -> String
show [Var]
ds) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]"
show_component :: Tagged -> String
show_component :: Tagged -> String
show_component = Tagged -> String
ppTagged
ppTagged :: Tagged -> String
ppTagged :: Tagged -> String
ppTagged (Elem
v,String
t) = case Elem
v of
String String
s -> String
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
Int Int
i -> String
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
Product [Tagged]
tes -> String
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ((Tagged -> String) -> [Tagged] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Tagged -> String
ppTagged [Tagged]
tes) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show_stmt :: Statement -> String
show_stmt :: Statement -> String
show_stmt (Query Term
t) = String
"?" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
t
show_stmt (Trans [Var]
xs TransType
atype Either Term (String, Arguments)
etm) = case [Var]
xs of
[] -> case Either Term (String, Arguments)
etm of Left Term
t -> TransType -> String
forall a. Show a => a -> String
show TransType
atype String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
t
Right (String
d,Arguments
mods) -> TransType -> String
forall a. Show a => a -> String
show TransType
atype String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
d String -> ShowS
forall a. [a] -> [a] -> [a]
++ Arguments -> String
show_arguments Arguments
mods
[Var]
_ -> String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"Foreach " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ((Var -> String) -> [Var] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Var -> String
forall a. Show a => a -> String
show [Var]
xs) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Statement -> String
show_stmt ([Var] -> TransType -> Either Term (String, Arguments) -> Statement
Trans [] TransType
atype Either Term (String, Arguments)
etm) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
valOf :: Tagged -> Elem
valOf :: Tagged -> Elem
valOf (Elem
c,String
t) = Elem
c
tagOf :: Tagged -> DomId
tagOf :: Tagged -> String
tagOf (Elem
c,String
t) = String
t
substitutions_of :: [Modifier] -> [(Var, Term)]
substitutions_of :: [Modifier] -> [(Var, Term)]
substitutions_of = (Modifier -> (Var, Term)) -> [Modifier] -> [(Var, Term)]
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) = [Var] -> [Term] -> [(Var, Term)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
xs [Term]
args
project :: Tagged -> DomId -> Maybe Tagged
project :: Tagged -> String -> Maybe Tagged
project (Product [Tagged]
tvs,String
_) String
ty = [Maybe Tagged] -> Maybe Tagged
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
asum ((Tagged -> Maybe Tagged) -> [Tagged] -> [Maybe Tagged]
forall a b. (a -> b) -> [a] -> [b]
map Tagged -> Maybe Tagged
forall a. (a, String) -> Maybe (a, String)
try [Tagged]
tvs)
where try :: (a, String) -> Maybe (a, String)
try tv :: (a, String)
tv@(a
v,String
ty') | String
ty String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
ty' = (a, String) -> Maybe (a, String)
forall a. a -> Maybe a
Just (a, String)
tv
try (a, String)
_ = Maybe (a, String)
forall a. Maybe a
Nothing
project Tagged
_ String
_ = Maybe Tagged
forall a. Maybe a
Nothing
emptySubs :: Subs
emptySubs :: Subs
emptySubs = Subs
forall k a. Map k a
M.empty
subsUnion :: Subs -> Subs -> Subs
subsUnion :: Subs -> Subs -> Subs
subsUnion = (Subs -> Subs -> Subs) -> Subs -> Subs -> Subs
forall a b c. (a -> b -> c) -> b -> a -> c
flip Subs -> Subs -> Subs
forall k a. Ord k => Map k a -> Map k a -> Map k a
M.union
subsUnions :: [Subs] -> Subs
subsUnions :: [Subs] -> Subs
subsUnions = (Subs -> Subs -> Subs) -> Subs -> [Subs] -> Subs
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Subs -> Subs -> Subs
subsUnion Subs
forall k a. Map k a
M.empty
type Refiner = M.Map DomId Domain
emptyRefiner :: Refiner
emptyRefiner :: Refiner
emptyRefiner = Refiner
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 String TypeSpec
decls = (String -> TypeSpec -> Map String TypeSpec -> Map String TypeSpec)
-> Map String TypeSpec
-> Map String TypeSpec
-> Map String TypeSpec
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
M.foldrWithKey String -> TypeSpec -> Map String TypeSpec -> Map String TypeSpec
reinserter (Spec -> Map String TypeSpec
decls Spec
spec) (Spec -> Map String TypeSpec
decls Spec
spec) }
where reinserter :: String -> TypeSpec -> Map String TypeSpec -> Map String TypeSpec
reinserter String
k TypeSpec
tspec Map String TypeSpec
sm' = case String -> Refiner -> Maybe Domain
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
k Refiner
rm of
Maybe Domain
Nothing -> Map String TypeSpec
sm'
Just Domain
d -> case (Domain
d, TypeSpec -> Domain
domain TypeSpec
tspec) of
(Strings [String]
ss, Domain
AnyString) -> Map String TypeSpec
sm''
(Strings [String]
ss, Strings [String]
ss')
| (String -> Bool) -> [String] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
ss') [String]
ss -> Map String TypeSpec
sm''
(Ints [Int]
is, Domain
AnyInt) -> Map String TypeSpec
sm''
(Ints [Int]
is, Ints [Int]
is')
| (Int -> Bool) -> [Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
is') [Int]
is -> Map String TypeSpec
sm''
(Domain, Domain)
_ -> Map String TypeSpec
sm'
where sm'' :: Map String TypeSpec
sm'' = String -> TypeSpec -> Map String TypeSpec -> Map String TypeSpec
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert String
k (TypeSpec
tspec {domain :: Domain
domain = Domain
d}) Map String TypeSpec
sm'
actor_decl :: TypeSpec
actor_decl :: TypeSpec
actor_decl = TypeSpec :: Kind
-> Domain -> Term -> [Derivation] -> Bool -> [Term] -> TypeSpec
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
, derivation :: [Derivation]
derivation = []
, conditions :: [Term]
conditions = []
, closed :: Bool
closed = Bool
True
}
int_decl :: TypeSpec
int_decl :: TypeSpec
int_decl = TypeSpec :: Kind
-> Domain -> Term -> [Derivation] -> Bool -> [Term] -> TypeSpec
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
, 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
-> Domain -> Term -> [Derivation] -> Bool -> [Term] -> TypeSpec
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
, derivation :: [Derivation]
derivation = []
, closed :: Bool
closed = Bool
True
, conditions :: [Term]
conditions = [] }
strings_decl :: [String] -> TypeSpec
strings_decl :: [String] -> TypeSpec
strings_decl [String]
ss =
TypeSpec :: Kind
-> Domain -> Term -> [Derivation] -> Bool -> [Term] -> TypeSpec
TypeSpec { kind :: Kind
kind = FactSpec -> Kind
Fact (Bool -> Bool -> FactSpec
FactSpec Bool
False Bool
False)
, domain :: Domain
domain = [String] -> Domain
Strings [String]
ss
, domain_constraint :: Term
domain_constraint = Bool -> Term
BoolLit Bool
True
, 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,String
d)) = case Elem
v of
String String
s -> [Pair] -> Value
object [ Text
"tagged-type" Text -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= Text -> Value
JSON.String Text
"string", Text
"fact-type" Text -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= String -> Value
forall a. ToJSON a => a -> Value
toJSON String
d, Text
"value" Text -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= String -> Value
forall a. ToJSON a => a -> Value
toJSON String
s, Text
"textual" Text -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= String -> Value
forall a. ToJSON a => a -> Value
toJSON (Tagged -> String
ppTagged Tagged
te) ]
Int Int
i -> [Pair] -> Value
object [ Text
"tagged-type" Text -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= Text -> Value
JSON.String Text
"int", Text
"fact-type" Text -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= String -> Value
forall a. ToJSON a => a -> Value
toJSON String
d, Text
"value" Text -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= Int -> Value
forall a. ToJSON a => a -> Value
toJSON Int
i, Text
"textual" Text -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= String -> Value
forall a. ToJSON a => a -> Value
toJSON (Tagged -> String
ppTagged Tagged
te) ]
Product [Tagged]
tes -> [Pair] -> Value
object [ Text
"tagged-type" Text -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= Text -> Value
JSON.String Text
"product", Text
"fact-type" Text -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= String -> Value
forall a. ToJSON a => a -> Value
toJSON String
d, Text
"arguments" Text -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= [TaggedJSON] -> Value
forall a. ToJSON a => a -> Value
toJSON ((Tagged -> TaggedJSON) -> [Tagged] -> [TaggedJSON]
forall a b. (a -> b) -> [a] -> [b]
map Tagged -> TaggedJSON
TaggedJSON [Tagged]
tes), Text
"textual" Text -> Value -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= String -> Value
forall a. ToJSON a => a -> Value
toJSON (Tagged -> String
ppTagged Tagged
te) ]