{- HLINT ignore "Use newtype instead of data" -}
module Hermod.ReCon.LTL.Check(
    checkIntTerm
  , checkTextTerm
  , checkParamConstraint
  , checkFormula
  , Error(..)
  , prettyError
  ) where

import           Hermod.ReCon.LTL.Formula

import           Prelude hiding (Foldable (..))

import           Data.Foldable (foldl')
import           Data.Set (Set, insert, member)
import qualified Data.Set as Set
import           Data.Text (Text)

-- The file concerns checking syntactic correctness of formulas.

data Error = UnboundVariableIdentifier VariableIdentifier deriving (Int -> Error -> ShowS
[Error] -> ShowS
Error -> String
(Int -> Error -> ShowS)
-> (Error -> String) -> ([Error] -> ShowS) -> Show Error
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Error -> ShowS
showsPrec :: Int -> Error -> ShowS
$cshow :: Error -> String
show :: Error -> String
$cshowList :: [Error] -> ShowS
showList :: [Error] -> ShowS
Show, Error -> Error -> Bool
(Error -> Error -> Bool) -> (Error -> Error -> Bool) -> Eq Error
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Error -> Error -> Bool
== :: Error -> Error -> Bool
$c/= :: Error -> Error -> Bool
/= :: Error -> Error -> Bool
Eq)

prettyError :: Error -> Text
prettyError :: Error -> Text
prettyError (UnboundVariableIdentifier Text
x) = Text
"Unbound variable: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
x

-- | Verify the given parameter variable is bound in the current context.
checkParamVar :: Set VariableIdentifier -> Text -> [Error]
checkParamVar :: Set Text -> Text -> [Error]
checkParamVar Set Text
bound Text
x | Text -> Set Text -> Bool
forall a. Ord a => a -> Set a -> Bool
member Text
x Set Text
bound  = []
checkParamVar Set Text
_ Text
x  = [Text -> Error
UnboundVariableIdentifier Text
x]

-- | Validate an integer term by checking all of its free variables are bound.
checkIntTerm :: Set VariableIdentifier -> IntTerm -> [Error]
checkIntTerm :: Set Text -> IntTerm -> [Error]
checkIntTerm Set Text
bound (IntVar IntValue
_ Text
x) = Set Text -> Text -> [Error]
checkParamVar Set Text
bound Text
x
checkIntTerm Set Text
_ (IntConst IntValue
_)     = []
checkIntTerm Set Text
bound (IntSum IntTerm
a IntTerm
b) = Set Text -> IntTerm -> [Error]
checkIntTerm Set Text
bound IntTerm
a [Error] -> [Error] -> [Error]
forall a. [a] -> [a] -> [a]
++ Set Text -> IntTerm -> [Error]
checkIntTerm Set Text
bound IntTerm
b

-- | Validate a text term by checking all of its free variables are bound.
checkTextTerm :: Set VariableIdentifier -> TextTerm -> [Error]
checkTextTerm :: Set Text -> TextTerm -> [Error]
checkTextTerm Set Text
bound (TextVar Text
x) = Set Text -> Text -> [Error]
checkParamVar Set Text
bound Text
x
checkTextTerm Set Text
_ (TextConst Text
_)   = []

-- | Validate a constraint by ensuring its term is well-scoped.
checkParamConstraint :: Set VariableIdentifier -> PropConstraint -> [Error]
checkParamConstraint :: Set Text -> PropConstraint -> [Error]
checkParamConstraint Set Text
bound (IntPropConstraint  Text
_ IntTerm
t) = Set Text -> IntTerm -> [Error]
checkIntTerm  Set Text
bound IntTerm
t
checkParamConstraint Set Text
bound (TextPropConstraint Text
_ TextTerm
t) = Set Text -> TextTerm -> [Error]
checkTextTerm Set Text
bound TextTerm
t

-- | Check whether the formula is syntactically valid.
checkFormula :: Set VariableIdentifier -> Formula event ty -> [Error]
checkFormula :: forall event ty. Set Text -> Formula event ty -> [Error]
checkFormula Set Text
bound (Forall Word
_ Formula event ty
phi) = Set Text -> Formula event ty -> [Error]
forall event ty. Set Text -> Formula event ty -> [Error]
checkFormula Set Text
bound Formula event ty
phi
checkFormula Set Text
bound (ForallN Word
_ Formula event ty
phi) = Set Text -> Formula event ty -> [Error]
forall event ty. Set Text -> Formula event ty -> [Error]
checkFormula Set Text
bound Formula event ty
phi
checkFormula Set Text
bound (ExistsN Word
_ Formula event ty
phi) = Set Text -> Formula event ty -> [Error]
forall event ty. Set Text -> Formula event ty -> [Error]
checkFormula Set Text
bound Formula event ty
phi
checkFormula Set Text
bound (And Formula event ty
phi Formula event ty
psi) = Set Text -> Formula event ty -> [Error]
forall event ty. Set Text -> Formula event ty -> [Error]
checkFormula Set Text
bound Formula event ty
phi [Error] -> [Error] -> [Error]
forall a. [a] -> [a] -> [a]
++ Set Text -> Formula event ty -> [Error]
forall event ty. Set Text -> Formula event ty -> [Error]
checkFormula Set Text
bound Formula event ty
psi
checkFormula Set Text
bound (Or Formula event ty
phi Formula event ty
psi) = Set Text -> Formula event ty -> [Error]
forall event ty. Set Text -> Formula event ty -> [Error]
checkFormula Set Text
bound Formula event ty
phi [Error] -> [Error] -> [Error]
forall a. [a] -> [a] -> [a]
++ Set Text -> Formula event ty -> [Error]
forall event ty. Set Text -> Formula event ty -> [Error]
checkFormula Set Text
bound Formula event ty
psi
checkFormula Set Text
bound (Not Formula event ty
phi) = Set Text -> Formula event ty -> [Error]
forall event ty. Set Text -> Formula event ty -> [Error]
checkFormula Set Text
bound Formula event ty
phi
checkFormula Set Text
_ Formula event ty
Bottom = []
checkFormula Set Text
_ Formula event ty
Top = []
checkFormula Set Text
bound (Next Formula event ty
phi) = Set Text -> Formula event ty -> [Error]
forall event ty. Set Text -> Formula event ty -> [Error]
checkFormula Set Text
bound Formula event ty
phi
checkFormula Set Text
bound (NextN Word
_ Formula event ty
phi) = Set Text -> Formula event ty -> [Error]
forall event ty. Set Text -> Formula event ty -> [Error]
checkFormula Set Text
bound Formula event ty
phi
checkFormula Set Text
bound (Implies Formula event ty
phi Formula event ty
psi) = Set Text -> Formula event ty -> [Error]
forall event ty. Set Text -> Formula event ty -> [Error]
checkFormula Set Text
bound Formula event ty
phi [Error] -> [Error] -> [Error]
forall a. [a] -> [a] -> [a]
++ Set Text -> Formula event ty -> [Error]
forall event ty. Set Text -> Formula event ty -> [Error]
checkFormula Set Text
bound Formula event ty
psi
checkFormula Set Text
bound (UntilN Word
_ Formula event ty
phi Formula event ty
psi) = Set Text -> Formula event ty -> [Error]
forall event ty. Set Text -> Formula event ty -> [Error]
checkFormula Set Text
bound Formula event ty
phi [Error] -> [Error] -> [Error]
forall a. [a] -> [a] -> [a]
++ Set Text -> Formula event ty -> [Error]
forall event ty. Set Text -> Formula event ty -> [Error]
checkFormula Set Text
bound Formula event ty
psi
checkFormula Set Text
bound (PropIntForall  Text
x Formula event ty
phi) = Set Text -> Formula event ty -> [Error]
forall event ty. Set Text -> Formula event ty -> [Error]
checkFormula (Text -> Set Text -> Set Text
forall a. Ord a => a -> Set a -> Set a
insert Text
x Set Text
bound) Formula event ty
phi
checkFormula Set Text
bound (PropTextForall Text
x Formula event ty
phi) = Set Text -> Formula event ty -> [Error]
forall event ty. Set Text -> Formula event ty -> [Error]
checkFormula (Text -> Set Text -> Set Text
forall a. Ord a => a -> Set a -> Set a
insert Text
x Set Text
bound) Formula event ty
phi
checkFormula Set Text
bound (PropIntForallN  Text
x Set IntValue
_ Formula event ty
phi) = Set Text -> Formula event ty -> [Error]
forall event ty. Set Text -> Formula event ty -> [Error]
checkFormula (Text -> Set Text -> Set Text
forall a. Ord a => a -> Set a -> Set a
insert Text
x Set Text
bound) Formula event ty
phi
checkFormula Set Text
bound (PropTextForallN Text
x Set Text
_ Formula event ty
phi) = Set Text -> Formula event ty -> [Error]
forall event ty. Set Text -> Formula event ty -> [Error]
checkFormula (Text -> Set Text -> Set Text
forall a. Ord a => a -> Set a -> Set a
insert Text
x Set Text
bound) Formula event ty
phi
checkFormula Set Text
bound (PropIntExists  Text
x Formula event ty
phi) = Set Text -> Formula event ty -> [Error]
forall event ty. Set Text -> Formula event ty -> [Error]
checkFormula (Text -> Set Text -> Set Text
forall a. Ord a => a -> Set a -> Set a
insert Text
x Set Text
bound) Formula event ty
phi
checkFormula Set Text
bound (PropTextExists Text
x Formula event ty
phi) = Set Text -> Formula event ty -> [Error]
forall event ty. Set Text -> Formula event ty -> [Error]
checkFormula (Text -> Set Text -> Set Text
forall a. Ord a => a -> Set a -> Set a
insert Text
x Set Text
bound) Formula event ty
phi
checkFormula Set Text
bound (PropIntExistsN  Text
x Set IntValue
_ Formula event ty
phi) = Set Text -> Formula event ty -> [Error]
forall event ty. Set Text -> Formula event ty -> [Error]
checkFormula (Text -> Set Text -> Set Text
forall a. Ord a => a -> Set a -> Set a
insert Text
x Set Text
bound) Formula event ty
phi
checkFormula Set Text
bound (PropTextExistsN Text
x Set Text
_ Formula event ty
phi) = Set Text -> Formula event ty -> [Error]
forall event ty. Set Text -> Formula event ty -> [Error]
checkFormula (Text -> Set Text -> Set Text
forall a. Ord a => a -> Set a -> Set a
insert Text
x Set Text
bound) Formula event ty
phi
checkFormula Set Text
bound (PropIntBinRel BinRel
_ Relevance event ty
_ IntTerm
lhs IntTerm
rhs) = Set Text -> IntTerm -> [Error]
checkIntTerm Set Text
bound IntTerm
lhs [Error] -> [Error] -> [Error]
forall a. [a] -> [a] -> [a]
++ Set Text -> IntTerm -> [Error]
checkIntTerm Set Text
bound IntTerm
rhs
checkFormula Set Text
bound (PropTextEq Relevance event ty
_ TextTerm
t Text
_) = Set Text -> TextTerm -> [Error]
checkTextTerm Set Text
bound TextTerm
t
checkFormula Set Text
bound (Atom ty
_ Set PropConstraint
cs) = ([Error] -> [Error] -> [Error]) -> [Error] -> [[Error]] -> [Error]
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' [Error] -> [Error] -> [Error]
forall a. [a] -> [a] -> [a]
(++) [] ((PropConstraint -> [Error]) -> [PropConstraint] -> [[Error]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Set Text -> PropConstraint -> [Error]
checkParamConstraint Set Text
bound) (Set PropConstraint -> [PropConstraint]
forall a. Set a -> [a]
Set.toList Set PropConstraint
cs))