module Hermod.ReCon.LTL.ContinuousFormula (
    ContinuousFormula(..)
  , retract
  , interp
  , eval) where

import           Hermod.ReCon.Common.Types (BinRel (..), IntValue, VariableIdentifier)
import           Hermod.ReCon.Integer.Polynomial.Term (IntTerm (..))
import           Hermod.ReCon.LTL.Formula (Event (..), Formula, OnMissingKey (..), PropConstraint (..),
                   TextTerm, TextValue)
import qualified Hermod.ReCon.LTL.Formula as F
import           Hermod.ReCon.LTL.Internal.IR.HomogeneousFormula (HomogeneousFormula)
import qualified Hermod.ReCon.LTL.Internal.IR.HomogeneousFormula as H

import           Control.Monad.Reader (Reader, asks)
import           Data.Map.Strict (lookup)
import           Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.Text as Text
import           Prelude hiding (lookup)

-- | Default name: φ.
--
--   The continuous counterpart of 'Formula': all temporal connectives are
--   absent.  A 'ContinuousFormula' is evaluated against a /single/ event
--   (or time unit) rather than a sequence, making it a purely propositional /
--   first-order assertion about the present moment.
data ContinuousFormula ty =

   -------------- Atomic ---------------
     -- | ty c̄
     Atom ty (Set PropConstraint)
   -------------------------------------

   ------------ Connective -------------
     -- | φ ∨ ψ
   | Or (ContinuousFormula ty) (ContinuousFormula ty)
     -- | φ ∧ ψ
   | And (ContinuousFormula ty) (ContinuousFormula ty)
     -- | ¬ φ
   | Not (ContinuousFormula ty)
     -- | φ ⇒ ψ
   | Implies (ContinuousFormula ty) (ContinuousFormula ty)
     -- | ⊤
   | Top
     -- | ⊥
   | Bottom
   -------------------------------------

   ----------- Event property ----------
     -- | ∀x ∈ ℤ. φ  —  x ranges over all integers
   | PropIntForall  VariableIdentifier (ContinuousFormula ty)
     -- | ∀x ∈ Text. φ  —  x ranges over all strings
   | PropTextForall VariableIdentifier (ContinuousFormula ty)
     -- | ∀x ∈ v̄. φ  —  x ranges over the given integers
   | PropIntForallN  VariableIdentifier (Set IntValue)  (ContinuousFormula ty)
     -- | ∀x ∈ v̄. φ  —  x ranges over the given strings
   | PropTextForallN VariableIdentifier (Set TextValue) (ContinuousFormula ty)
     -- | ∃x ∈ ℤ. φ  —  x ranges over all integers
   | PropIntExists  VariableIdentifier (ContinuousFormula ty)
     -- | ∃x ∈ Text. φ  —  x ranges over all strings
   | PropTextExists VariableIdentifier (ContinuousFormula ty)
     -- | ∃x ∈ v̄. φ  —  x ranges over the given integers
   | PropIntExistsN  VariableIdentifier (Set IntValue)  (ContinuousFormula ty)
     -- | ∃x ∈ v̄. φ  —  x ranges over the given strings
   | PropTextExistsN VariableIdentifier (Set TextValue) (ContinuousFormula ty)
     -- | t rel t  (integer)
   | PropIntBinRel BinRel IntTerm IntTerm
     -- | t = v  (text)
   | PropTextEq TextTerm TextValue
   -------------------------------------
   deriving (Int -> ContinuousFormula ty -> ShowS
[ContinuousFormula ty] -> ShowS
ContinuousFormula ty -> String
(Int -> ContinuousFormula ty -> ShowS)
-> (ContinuousFormula ty -> String)
-> ([ContinuousFormula ty] -> ShowS)
-> Show (ContinuousFormula ty)
forall ty. Show ty => Int -> ContinuousFormula ty -> ShowS
forall ty. Show ty => [ContinuousFormula ty] -> ShowS
forall ty. Show ty => ContinuousFormula ty -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall ty. Show ty => Int -> ContinuousFormula ty -> ShowS
showsPrec :: Int -> ContinuousFormula ty -> ShowS
$cshow :: forall ty. Show ty => ContinuousFormula ty -> String
show :: ContinuousFormula ty -> String
$cshowList :: forall ty. Show ty => [ContinuousFormula ty] -> ShowS
showList :: [ContinuousFormula ty] -> ShowS
Show, ContinuousFormula ty -> ContinuousFormula ty -> Bool
(ContinuousFormula ty -> ContinuousFormula ty -> Bool)
-> (ContinuousFormula ty -> ContinuousFormula ty -> Bool)
-> Eq (ContinuousFormula ty)
forall ty.
Eq ty =>
ContinuousFormula ty -> ContinuousFormula ty -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall ty.
Eq ty =>
ContinuousFormula ty -> ContinuousFormula ty -> Bool
== :: ContinuousFormula ty -> ContinuousFormula ty -> Bool
$c/= :: forall ty.
Eq ty =>
ContinuousFormula ty -> ContinuousFormula ty -> Bool
/= :: ContinuousFormula ty -> ContinuousFormula ty -> Bool
Eq, Eq (ContinuousFormula ty)
Eq (ContinuousFormula ty) =>
(ContinuousFormula ty -> ContinuousFormula ty -> Ordering)
-> (ContinuousFormula ty -> ContinuousFormula ty -> Bool)
-> (ContinuousFormula ty -> ContinuousFormula ty -> Bool)
-> (ContinuousFormula ty -> ContinuousFormula ty -> Bool)
-> (ContinuousFormula ty -> ContinuousFormula ty -> Bool)
-> (ContinuousFormula ty
    -> ContinuousFormula ty -> ContinuousFormula ty)
-> (ContinuousFormula ty
    -> ContinuousFormula ty -> ContinuousFormula ty)
-> Ord (ContinuousFormula ty)
ContinuousFormula ty -> ContinuousFormula ty -> Bool
ContinuousFormula ty -> ContinuousFormula ty -> Ordering
ContinuousFormula ty
-> ContinuousFormula ty -> ContinuousFormula ty
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
forall ty. Ord ty => Eq (ContinuousFormula ty)
forall ty.
Ord ty =>
ContinuousFormula ty -> ContinuousFormula ty -> Bool
forall ty.
Ord ty =>
ContinuousFormula ty -> ContinuousFormula ty -> Ordering
forall ty.
Ord ty =>
ContinuousFormula ty
-> ContinuousFormula ty -> ContinuousFormula ty
$ccompare :: forall ty.
Ord ty =>
ContinuousFormula ty -> ContinuousFormula ty -> Ordering
compare :: ContinuousFormula ty -> ContinuousFormula ty -> Ordering
$c< :: forall ty.
Ord ty =>
ContinuousFormula ty -> ContinuousFormula ty -> Bool
< :: ContinuousFormula ty -> ContinuousFormula ty -> Bool
$c<= :: forall ty.
Ord ty =>
ContinuousFormula ty -> ContinuousFormula ty -> Bool
<= :: ContinuousFormula ty -> ContinuousFormula ty -> Bool
$c> :: forall ty.
Ord ty =>
ContinuousFormula ty -> ContinuousFormula ty -> Bool
> :: ContinuousFormula ty -> ContinuousFormula ty -> Bool
$c>= :: forall ty.
Ord ty =>
ContinuousFormula ty -> ContinuousFormula ty -> Bool
>= :: ContinuousFormula ty -> ContinuousFormula ty -> Bool
$cmax :: forall ty.
Ord ty =>
ContinuousFormula ty
-> ContinuousFormula ty -> ContinuousFormula ty
max :: ContinuousFormula ty
-> ContinuousFormula ty -> ContinuousFormula ty
$cmin :: forall ty.
Ord ty =>
ContinuousFormula ty
-> ContinuousFormula ty -> ContinuousFormula ty
min :: ContinuousFormula ty
-> ContinuousFormula ty -> ContinuousFormula ty
Ord)

-- | Retract a 'Formula' into a 'ContinuousFormula', returning 'Nothing' if
--   the formula contains any temporal connective.
retract :: Formula event ty -> Maybe (ContinuousFormula ty)
retract :: forall event ty. Formula event ty -> Maybe (ContinuousFormula ty)
retract (F.Forall {})            = Maybe (ContinuousFormula ty)
forall a. Maybe a
Nothing
retract (F.ForallN {})           = Maybe (ContinuousFormula ty)
forall a. Maybe a
Nothing
retract (F.ExistsN {})           = Maybe (ContinuousFormula ty)
forall a. Maybe a
Nothing
retract (F.Next {})              = Maybe (ContinuousFormula ty)
forall a. Maybe a
Nothing
retract (F.NextN {})             = Maybe (ContinuousFormula ty)
forall a. Maybe a
Nothing
retract (F.UntilN {})            = Maybe (ContinuousFormula ty)
forall a. Maybe a
Nothing
retract (F.Atom ty
ty Set PropConstraint
cs)           = ContinuousFormula ty -> Maybe (ContinuousFormula ty)
forall a. a -> Maybe a
Just (ty -> Set PropConstraint -> ContinuousFormula ty
forall ty. ty -> Set PropConstraint -> ContinuousFormula ty
Atom ty
ty Set PropConstraint
cs)
retract (F.Or Formula event ty
phi Formula event ty
psi)           = ContinuousFormula ty
-> ContinuousFormula ty -> ContinuousFormula ty
forall ty.
ContinuousFormula ty
-> ContinuousFormula ty -> ContinuousFormula ty
Or      (ContinuousFormula ty
 -> ContinuousFormula ty -> ContinuousFormula ty)
-> Maybe (ContinuousFormula ty)
-> Maybe (ContinuousFormula ty -> ContinuousFormula ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula event ty -> Maybe (ContinuousFormula ty)
forall event ty. Formula event ty -> Maybe (ContinuousFormula ty)
retract Formula event ty
phi Maybe (ContinuousFormula ty -> ContinuousFormula ty)
-> Maybe (ContinuousFormula ty) -> Maybe (ContinuousFormula ty)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Formula event ty -> Maybe (ContinuousFormula ty)
forall event ty. Formula event ty -> Maybe (ContinuousFormula ty)
retract Formula event ty
psi
retract (F.And Formula event ty
phi Formula event ty
psi)          = ContinuousFormula ty
-> ContinuousFormula ty -> ContinuousFormula ty
forall ty.
ContinuousFormula ty
-> ContinuousFormula ty -> ContinuousFormula ty
And     (ContinuousFormula ty
 -> ContinuousFormula ty -> ContinuousFormula ty)
-> Maybe (ContinuousFormula ty)
-> Maybe (ContinuousFormula ty -> ContinuousFormula ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula event ty -> Maybe (ContinuousFormula ty)
forall event ty. Formula event ty -> Maybe (ContinuousFormula ty)
retract Formula event ty
phi Maybe (ContinuousFormula ty -> ContinuousFormula ty)
-> Maybe (ContinuousFormula ty) -> Maybe (ContinuousFormula ty)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Formula event ty -> Maybe (ContinuousFormula ty)
forall event ty. Formula event ty -> Maybe (ContinuousFormula ty)
retract Formula event ty
psi
retract (F.Not Formula event ty
phi)              = ContinuousFormula ty -> ContinuousFormula ty
forall ty. ContinuousFormula ty -> ContinuousFormula ty
Not     (ContinuousFormula ty -> ContinuousFormula ty)
-> Maybe (ContinuousFormula ty) -> Maybe (ContinuousFormula ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula event ty -> Maybe (ContinuousFormula ty)
forall event ty. Formula event ty -> Maybe (ContinuousFormula ty)
retract Formula event ty
phi
retract (F.Implies Formula event ty
phi Formula event ty
psi)      = ContinuousFormula ty
-> ContinuousFormula ty -> ContinuousFormula ty
forall ty.
ContinuousFormula ty
-> ContinuousFormula ty -> ContinuousFormula ty
Implies (ContinuousFormula ty
 -> ContinuousFormula ty -> ContinuousFormula ty)
-> Maybe (ContinuousFormula ty)
-> Maybe (ContinuousFormula ty -> ContinuousFormula ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula event ty -> Maybe (ContinuousFormula ty)
forall event ty. Formula event ty -> Maybe (ContinuousFormula ty)
retract Formula event ty
phi Maybe (ContinuousFormula ty -> ContinuousFormula ty)
-> Maybe (ContinuousFormula ty) -> Maybe (ContinuousFormula ty)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Formula event ty -> Maybe (ContinuousFormula ty)
forall event ty. Formula event ty -> Maybe (ContinuousFormula ty)
retract Formula event ty
psi
retract Formula event ty
F.Top                    = ContinuousFormula ty -> Maybe (ContinuousFormula ty)
forall a. a -> Maybe a
Just ContinuousFormula ty
forall ty. ContinuousFormula ty
Top
retract Formula event ty
F.Bottom                 = ContinuousFormula ty -> Maybe (ContinuousFormula ty)
forall a. a -> Maybe a
Just ContinuousFormula ty
forall ty. ContinuousFormula ty
Bottom
retract (F.PropIntForall  VariableIdentifier
x Formula event ty
phi)        = VariableIdentifier -> ContinuousFormula ty -> ContinuousFormula ty
forall ty.
VariableIdentifier -> ContinuousFormula ty -> ContinuousFormula ty
PropIntForall  VariableIdentifier
x     (ContinuousFormula ty -> ContinuousFormula ty)
-> Maybe (ContinuousFormula ty) -> Maybe (ContinuousFormula ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula event ty -> Maybe (ContinuousFormula ty)
forall event ty. Formula event ty -> Maybe (ContinuousFormula ty)
retract Formula event ty
phi
retract (F.PropTextForall VariableIdentifier
x Formula event ty
phi)        = VariableIdentifier -> ContinuousFormula ty -> ContinuousFormula ty
forall ty.
VariableIdentifier -> ContinuousFormula ty -> ContinuousFormula ty
PropTextForall VariableIdentifier
x     (ContinuousFormula ty -> ContinuousFormula ty)
-> Maybe (ContinuousFormula ty) -> Maybe (ContinuousFormula ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula event ty -> Maybe (ContinuousFormula ty)
forall event ty. Formula event ty -> Maybe (ContinuousFormula ty)
retract Formula event ty
phi
retract (F.PropIntForallN  VariableIdentifier
x Set IntValue
dom Formula event ty
phi)   = VariableIdentifier
-> Set IntValue -> ContinuousFormula ty -> ContinuousFormula ty
forall ty.
VariableIdentifier
-> Set IntValue -> ContinuousFormula ty -> ContinuousFormula ty
PropIntForallN  VariableIdentifier
x Set IntValue
dom (ContinuousFormula ty -> ContinuousFormula ty)
-> Maybe (ContinuousFormula ty) -> Maybe (ContinuousFormula ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula event ty -> Maybe (ContinuousFormula ty)
forall event ty. Formula event ty -> Maybe (ContinuousFormula ty)
retract Formula event ty
phi
retract (F.PropTextForallN VariableIdentifier
x Set VariableIdentifier
dom Formula event ty
phi)   = VariableIdentifier
-> Set VariableIdentifier
-> ContinuousFormula ty
-> ContinuousFormula ty
forall ty.
VariableIdentifier
-> Set VariableIdentifier
-> ContinuousFormula ty
-> ContinuousFormula ty
PropTextForallN VariableIdentifier
x Set VariableIdentifier
dom (ContinuousFormula ty -> ContinuousFormula ty)
-> Maybe (ContinuousFormula ty) -> Maybe (ContinuousFormula ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula event ty -> Maybe (ContinuousFormula ty)
forall event ty. Formula event ty -> Maybe (ContinuousFormula ty)
retract Formula event ty
phi
retract (F.PropIntExists  VariableIdentifier
x Formula event ty
phi)        = VariableIdentifier -> ContinuousFormula ty -> ContinuousFormula ty
forall ty.
VariableIdentifier -> ContinuousFormula ty -> ContinuousFormula ty
PropIntExists  VariableIdentifier
x     (ContinuousFormula ty -> ContinuousFormula ty)
-> Maybe (ContinuousFormula ty) -> Maybe (ContinuousFormula ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula event ty -> Maybe (ContinuousFormula ty)
forall event ty. Formula event ty -> Maybe (ContinuousFormula ty)
retract Formula event ty
phi
retract (F.PropTextExists VariableIdentifier
x Formula event ty
phi)        = VariableIdentifier -> ContinuousFormula ty -> ContinuousFormula ty
forall ty.
VariableIdentifier -> ContinuousFormula ty -> ContinuousFormula ty
PropTextExists VariableIdentifier
x     (ContinuousFormula ty -> ContinuousFormula ty)
-> Maybe (ContinuousFormula ty) -> Maybe (ContinuousFormula ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula event ty -> Maybe (ContinuousFormula ty)
forall event ty. Formula event ty -> Maybe (ContinuousFormula ty)
retract Formula event ty
phi
retract (F.PropIntExistsN  VariableIdentifier
x Set IntValue
dom Formula event ty
phi)   = VariableIdentifier
-> Set IntValue -> ContinuousFormula ty -> ContinuousFormula ty
forall ty.
VariableIdentifier
-> Set IntValue -> ContinuousFormula ty -> ContinuousFormula ty
PropIntExistsN  VariableIdentifier
x Set IntValue
dom (ContinuousFormula ty -> ContinuousFormula ty)
-> Maybe (ContinuousFormula ty) -> Maybe (ContinuousFormula ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula event ty -> Maybe (ContinuousFormula ty)
forall event ty. Formula event ty -> Maybe (ContinuousFormula ty)
retract Formula event ty
phi
retract (F.PropTextExistsN VariableIdentifier
x Set VariableIdentifier
dom Formula event ty
phi)   = VariableIdentifier
-> Set VariableIdentifier
-> ContinuousFormula ty
-> ContinuousFormula ty
forall ty.
VariableIdentifier
-> Set VariableIdentifier
-> ContinuousFormula ty
-> ContinuousFormula ty
PropTextExistsN VariableIdentifier
x Set VariableIdentifier
dom (ContinuousFormula ty -> ContinuousFormula ty)
-> Maybe (ContinuousFormula ty) -> Maybe (ContinuousFormula ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula event ty -> Maybe (ContinuousFormula ty)
forall event ty. Formula event ty -> Maybe (ContinuousFormula ty)
retract Formula event ty
phi
retract (F.PropIntBinRel BinRel
rel Relevance event ty
_ IntTerm
t1 IntTerm
t2)   = ContinuousFormula ty -> Maybe (ContinuousFormula ty)
forall a. a -> Maybe a
Just (BinRel -> IntTerm -> IntTerm -> ContinuousFormula ty
forall ty. BinRel -> IntTerm -> IntTerm -> ContinuousFormula ty
PropIntBinRel BinRel
rel IntTerm
t1 IntTerm
t2)
retract (F.PropTextEq Relevance event ty
_ TextTerm
t VariableIdentifier
v)            = ContinuousFormula ty -> Maybe (ContinuousFormula ty)
forall a. a -> Maybe a
Just (TextTerm -> VariableIdentifier -> ContinuousFormula ty
forall ty. TextTerm -> VariableIdentifier -> ContinuousFormula ty
PropTextEq TextTerm
t VariableIdentifier
v)

-- | Decide (e ⊧ φ).
eval :: (Event event ty, Eq ty) => ContinuousFormula ty -> event -> Reader OnMissingKey Bool
eval :: forall event ty.
(Event event ty, Eq ty) =>
ContinuousFormula ty -> event -> Reader OnMissingKey Bool
eval ContinuousFormula ty
phi event
e = HomogeneousFormula -> Bool
H.eval (HomogeneousFormula -> Bool)
-> ReaderT OnMissingKey Identity HomogeneousFormula
-> Reader OnMissingKey Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ContinuousFormula ty
-> event -> ReaderT OnMissingKey Identity HomogeneousFormula
forall event ty.
(Event event ty, Eq ty) =>
ContinuousFormula ty
-> event -> ReaderT OnMissingKey Identity HomogeneousFormula
interp ContinuousFormula ty
phi event
e

-- | Algorithm for (e ⊧ φ): checks each 'Atom' against the event type and
--   substitutes property constraints with the event's concrete values,
--   yielding a 'HomogeneousFormula' ready for decision.
interp :: (Event event ty, Eq ty) => ContinuousFormula ty -> event -> Reader OnMissingKey HomogeneousFormula
interp :: forall event ty.
(Event event ty, Eq ty) =>
ContinuousFormula ty
-> event -> ReaderT OnMissingKey Identity HomogeneousFormula
interp ContinuousFormula ty
phi event
e = ContinuousFormula ty
-> ReaderT OnMissingKey Identity HomogeneousFormula
forall {f :: * -> *}.
MonadReader OnMissingKey f =>
ContinuousFormula ty -> f HomogeneousFormula
go ContinuousFormula ty
phi
  where
    go :: ContinuousFormula ty -> f HomogeneousFormula
go (Atom ty
ty Set PropConstraint
cs)
      | event -> ty -> Bool
forall a ty. Event a ty => a -> ty -> Bool
ofTy event
e ty
ty = (HomogeneousFormula -> HomogeneousFormula -> HomogeneousFormula)
-> HomogeneousFormula -> [HomogeneousFormula] -> HomogeneousFormula
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr HomogeneousFormula -> HomogeneousFormula -> HomogeneousFormula
H.And HomogeneousFormula
H.Top ([HomogeneousFormula] -> HomogeneousFormula)
-> f [HomogeneousFormula] -> f HomogeneousFormula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (PropConstraint -> f HomogeneousFormula)
-> [PropConstraint] -> f [HomogeneousFormula]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (ty -> PropConstraint -> f HomogeneousFormula
forall {f :: * -> *}.
MonadReader OnMissingKey f =>
ty -> PropConstraint -> f HomogeneousFormula
evalConstraint ty
ty) (Set PropConstraint -> [PropConstraint]
forall a. Set a -> [a]
Set.toList Set PropConstraint
cs)
      | Bool
otherwise = HomogeneousFormula -> f HomogeneousFormula
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure HomogeneousFormula
H.Bottom
    go (Or ContinuousFormula ty
phi' ContinuousFormula ty
psi)      = HomogeneousFormula -> HomogeneousFormula -> HomogeneousFormula
H.Or      (HomogeneousFormula -> HomogeneousFormula -> HomogeneousFormula)
-> f HomogeneousFormula
-> f (HomogeneousFormula -> HomogeneousFormula)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ContinuousFormula ty -> f HomogeneousFormula
go ContinuousFormula ty
phi' f (HomogeneousFormula -> HomogeneousFormula)
-> f HomogeneousFormula -> f HomogeneousFormula
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ContinuousFormula ty -> f HomogeneousFormula
go ContinuousFormula ty
psi
    go (And ContinuousFormula ty
phi' ContinuousFormula ty
psi)     = HomogeneousFormula -> HomogeneousFormula -> HomogeneousFormula
H.And     (HomogeneousFormula -> HomogeneousFormula -> HomogeneousFormula)
-> f HomogeneousFormula
-> f (HomogeneousFormula -> HomogeneousFormula)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ContinuousFormula ty -> f HomogeneousFormula
go ContinuousFormula ty
phi' f (HomogeneousFormula -> HomogeneousFormula)
-> f HomogeneousFormula -> f HomogeneousFormula
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ContinuousFormula ty -> f HomogeneousFormula
go ContinuousFormula ty
psi
    go (Not ContinuousFormula ty
phi')         = HomogeneousFormula -> HomogeneousFormula
H.Not     (HomogeneousFormula -> HomogeneousFormula)
-> f HomogeneousFormula -> f HomogeneousFormula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ContinuousFormula ty -> f HomogeneousFormula
go ContinuousFormula ty
phi'
    go (Implies ContinuousFormula ty
phi' ContinuousFormula ty
psi) = HomogeneousFormula -> HomogeneousFormula -> HomogeneousFormula
H.Implies (HomogeneousFormula -> HomogeneousFormula -> HomogeneousFormula)
-> f HomogeneousFormula
-> f (HomogeneousFormula -> HomogeneousFormula)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ContinuousFormula ty -> f HomogeneousFormula
go ContinuousFormula ty
phi' f (HomogeneousFormula -> HomogeneousFormula)
-> f HomogeneousFormula -> f HomogeneousFormula
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ContinuousFormula ty -> f HomogeneousFormula
go ContinuousFormula ty
psi
    go ContinuousFormula ty
Top                = HomogeneousFormula -> f HomogeneousFormula
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure HomogeneousFormula
H.Top
    go ContinuousFormula ty
Bottom             = HomogeneousFormula -> f HomogeneousFormula
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure HomogeneousFormula
H.Bottom
    go (PropIntForall  VariableIdentifier
x ContinuousFormula ty
phi')       = VariableIdentifier -> HomogeneousFormula -> HomogeneousFormula
H.PropIntForall  VariableIdentifier
x (HomogeneousFormula -> HomogeneousFormula)
-> f HomogeneousFormula -> f HomogeneousFormula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ContinuousFormula ty -> f HomogeneousFormula
go ContinuousFormula ty
phi'
    go (PropTextForall VariableIdentifier
x ContinuousFormula ty
phi')       = VariableIdentifier -> HomogeneousFormula -> HomogeneousFormula
H.PropTextForall VariableIdentifier
x (HomogeneousFormula -> HomogeneousFormula)
-> f HomogeneousFormula -> f HomogeneousFormula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ContinuousFormula ty -> f HomogeneousFormula
go ContinuousFormula ty
phi'
    go (PropIntForallN  VariableIdentifier
x Set IntValue
dom ContinuousFormula ty
phi')  = VariableIdentifier
-> Set IntValue -> HomogeneousFormula -> HomogeneousFormula
H.PropIntForallN  VariableIdentifier
x Set IntValue
dom (HomogeneousFormula -> HomogeneousFormula)
-> f HomogeneousFormula -> f HomogeneousFormula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ContinuousFormula ty -> f HomogeneousFormula
go ContinuousFormula ty
phi'
    go (PropTextForallN VariableIdentifier
x Set VariableIdentifier
dom ContinuousFormula ty
phi')  = VariableIdentifier
-> Set VariableIdentifier
-> HomogeneousFormula
-> HomogeneousFormula
H.PropTextForallN VariableIdentifier
x Set VariableIdentifier
dom (HomogeneousFormula -> HomogeneousFormula)
-> f HomogeneousFormula -> f HomogeneousFormula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ContinuousFormula ty -> f HomogeneousFormula
go ContinuousFormula ty
phi'
    go (PropIntExists  VariableIdentifier
x ContinuousFormula ty
phi')       = VariableIdentifier -> HomogeneousFormula -> HomogeneousFormula
H.PropIntExists  VariableIdentifier
x (HomogeneousFormula -> HomogeneousFormula)
-> f HomogeneousFormula -> f HomogeneousFormula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ContinuousFormula ty -> f HomogeneousFormula
go ContinuousFormula ty
phi'
    go (PropTextExists VariableIdentifier
x ContinuousFormula ty
phi')       = VariableIdentifier -> HomogeneousFormula -> HomogeneousFormula
H.PropTextExists VariableIdentifier
x (HomogeneousFormula -> HomogeneousFormula)
-> f HomogeneousFormula -> f HomogeneousFormula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ContinuousFormula ty -> f HomogeneousFormula
go ContinuousFormula ty
phi'
    go (PropIntExistsN  VariableIdentifier
x Set IntValue
dom ContinuousFormula ty
phi')  = VariableIdentifier
-> Set IntValue -> HomogeneousFormula -> HomogeneousFormula
H.PropIntExistsN  VariableIdentifier
x Set IntValue
dom (HomogeneousFormula -> HomogeneousFormula)
-> f HomogeneousFormula -> f HomogeneousFormula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ContinuousFormula ty -> f HomogeneousFormula
go ContinuousFormula ty
phi'
    go (PropTextExistsN VariableIdentifier
x Set VariableIdentifier
dom ContinuousFormula ty
phi')  = VariableIdentifier
-> Set VariableIdentifier
-> HomogeneousFormula
-> HomogeneousFormula
H.PropTextExistsN VariableIdentifier
x Set VariableIdentifier
dom (HomogeneousFormula -> HomogeneousFormula)
-> f HomogeneousFormula -> f HomogeneousFormula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ContinuousFormula ty -> f HomogeneousFormula
go ContinuousFormula ty
phi'
    go (PropIntBinRel BinRel
rel IntTerm
t1 IntTerm
t2)     = HomogeneousFormula -> f HomogeneousFormula
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HomogeneousFormula -> f HomogeneousFormula)
-> HomogeneousFormula -> f HomogeneousFormula
forall a b. (a -> b) -> a -> b
$ BinRel -> IntTerm -> IntTerm -> HomogeneousFormula
H.PropIntBinRel BinRel
rel IntTerm
t1 IntTerm
t2
    go (PropTextEq TextTerm
t VariableIdentifier
v)              = HomogeneousFormula -> f HomogeneousFormula
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HomogeneousFormula -> f HomogeneousFormula)
-> HomogeneousFormula -> f HomogeneousFormula
forall a b. (a -> b) -> a -> b
$ TextTerm -> VariableIdentifier -> HomogeneousFormula
H.PropTextEq TextTerm
t VariableIdentifier
v

    evalConstraint :: ty -> PropConstraint -> f HomogeneousFormula
evalConstraint ty
ty (IntPropConstraint VariableIdentifier
key IntTerm
t) =
      case VariableIdentifier
-> Map VariableIdentifier IntValue -> Maybe IntValue
forall k a. Ord k => k -> Map k a -> Maybe a
lookup VariableIdentifier
key (event -> ty -> Map VariableIdentifier IntValue
forall a ty.
Event a ty =>
a -> ty -> Map VariableIdentifier IntValue
intProps event
e ty
ty) of
        Just IntValue
v  -> HomogeneousFormula -> f HomogeneousFormula
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HomogeneousFormula -> f HomogeneousFormula)
-> HomogeneousFormula -> f HomogeneousFormula
forall a b. (a -> b) -> a -> b
$ BinRel -> IntTerm -> IntTerm -> HomogeneousFormula
H.PropIntBinRel BinRel
Eq IntTerm
t (IntValue -> IntTerm
IntConst IntValue
v)
        Maybe IntValue
Nothing -> VariableIdentifier -> f HomogeneousFormula
forall {m :: * -> *}.
MonadReader OnMissingKey m =>
VariableIdentifier -> m HomogeneousFormula
missingKey VariableIdentifier
key
    evalConstraint ty
ty (TextPropConstraint VariableIdentifier
key TextTerm
t) =
      case VariableIdentifier
-> Map VariableIdentifier VariableIdentifier
-> Maybe VariableIdentifier
forall k a. Ord k => k -> Map k a -> Maybe a
lookup VariableIdentifier
key (event -> ty -> Map VariableIdentifier VariableIdentifier
forall a ty.
Event a ty =>
a -> ty -> Map VariableIdentifier VariableIdentifier
textProps event
e ty
ty) of
        Just VariableIdentifier
v  -> HomogeneousFormula -> f HomogeneousFormula
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HomogeneousFormula -> f HomogeneousFormula)
-> HomogeneousFormula -> f HomogeneousFormula
forall a b. (a -> b) -> a -> b
$ TextTerm -> VariableIdentifier -> HomogeneousFormula
H.PropTextEq TextTerm
t VariableIdentifier
v
        Maybe VariableIdentifier
Nothing -> VariableIdentifier -> f HomogeneousFormula
forall {m :: * -> *}.
MonadReader OnMissingKey m =>
VariableIdentifier -> m HomogeneousFormula
missingKey VariableIdentifier
key

    missingKey :: VariableIdentifier -> m HomogeneousFormula
missingKey VariableIdentifier
key = (OnMissingKey -> HomogeneousFormula) -> m HomogeneousFormula
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((OnMissingKey -> HomogeneousFormula) -> m HomogeneousFormula)
-> (OnMissingKey -> HomogeneousFormula) -> m HomogeneousFormula
forall a b. (a -> b) -> a -> b
$ \case
      OnMissingKey
BottomOnMissingKey -> HomogeneousFormula
H.Bottom
      OnMissingKey
CrashOnMissingKey  -> String -> HomogeneousFormula
forall a. HasCallStack => String -> a
error (String -> HomogeneousFormula) -> String -> HomogeneousFormula
forall a b. (a -> b) -> a -> b
$ String
"Missing key: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> VariableIdentifier -> String
Text.unpack VariableIdentifier
key