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

data Var        = Var DomId String {- decoration -}
                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 -- with var instantiated instead as the value of expr
                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 {- whether closed world assumption is made for this type -}
                    , 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 -- TODO move to outer AST
                    , 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] --TODO consider moving to outer ast
                    , 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)

-- | 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 :: 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)
       }

-- | 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 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) -- used for actor identifiers
                          , (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-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
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            -- execute computed instance
             | CTrigger [Var] Term   -- execute instance to be computed
             | 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 -- 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 -> 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
"~"

-- 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 :: 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

-- environments

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

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

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