module Hermod.ReCon.LTL.Internal.IR.HomogeneousFormula.FinFree (
    FinFree(..)
  , Extended(..)
  , substInt
  , substText
  , lower
  , eval
  ) where

import           Hermod.ReCon.Common.Types (BinRel (..))
import           Hermod.ReCon.LTL.Formula (IntTerm (..), IntValue, TextTerm (..), VariableIdentifier)
import           Hermod.ReCon.LTL.Internal.Subst (substIntTerm)
import qualified Hermod.ReCon.Presburger.Decide as PD
import qualified Hermod.ReCon.Presburger.Formula as P

import           Data.Functor ((<&>))
import           Data.Set (Set)
import qualified Data.Set as Set
import           Data.Text (Text)

-- | An extended value: either a concrete value or a placeholder distinct from all concrete values.
data Extended a = Val a | Placeholder deriving (Int -> Extended a -> ShowS
[Extended a] -> ShowS
Extended a -> [Char]
(Int -> Extended a -> ShowS)
-> (Extended a -> [Char])
-> ([Extended a] -> ShowS)
-> Show (Extended a)
forall a. Show a => Int -> Extended a -> ShowS
forall a. Show a => [Extended a] -> ShowS
forall a. Show a => Extended a -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Extended a -> ShowS
showsPrec :: Int -> Extended a -> ShowS
$cshow :: forall a. Show a => Extended a -> [Char]
show :: Extended a -> [Char]
$cshowList :: forall a. Show a => [Extended a] -> ShowS
showList :: [Extended a] -> ShowS
Show, Eq (Extended a)
Eq (Extended a) =>
(Extended a -> Extended a -> Ordering)
-> (Extended a -> Extended a -> Bool)
-> (Extended a -> Extended a -> Bool)
-> (Extended a -> Extended a -> Bool)
-> (Extended a -> Extended a -> Bool)
-> (Extended a -> Extended a -> Extended a)
-> (Extended a -> Extended a -> Extended a)
-> Ord (Extended a)
Extended a -> Extended a -> Bool
Extended a -> Extended a -> Ordering
Extended a -> Extended a -> Extended a
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 a. Ord a => Eq (Extended a)
forall a. Ord a => Extended a -> Extended a -> Bool
forall a. Ord a => Extended a -> Extended a -> Ordering
forall a. Ord a => Extended a -> Extended a -> Extended a
$ccompare :: forall a. Ord a => Extended a -> Extended a -> Ordering
compare :: Extended a -> Extended a -> Ordering
$c< :: forall a. Ord a => Extended a -> Extended a -> Bool
< :: Extended a -> Extended a -> Bool
$c<= :: forall a. Ord a => Extended a -> Extended a -> Bool
<= :: Extended a -> Extended a -> Bool
$c> :: forall a. Ord a => Extended a -> Extended a -> Bool
> :: Extended a -> Extended a -> Bool
$c>= :: forall a. Ord a => Extended a -> Extended a -> Bool
>= :: Extended a -> Extended a -> Bool
$cmax :: forall a. Ord a => Extended a -> Extended a -> Extended a
max :: Extended a -> Extended a -> Extended a
$cmin :: forall a. Ord a => Extended a -> Extended a -> Extended a
min :: Extended a -> Extended a -> Extended a
Ord, Extended a -> Extended a -> Bool
(Extended a -> Extended a -> Bool)
-> (Extended a -> Extended a -> Bool) -> Eq (Extended a)
forall a. Eq a => Extended a -> Extended a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Extended a -> Extended a -> Bool
== :: Extended a -> Extended a -> Bool
$c/= :: forall a. Eq a => Extended a -> Extended a -> Bool
/= :: Extended a -> Extended a -> Bool
Eq)

-- | `HomogeneousFormula` with all finite-domain quantifiers already eliminated.
--   Only infinite-domain (unbounded) quantifiers remain.
data FinFree =
   ------------ Connective -------------
     Or FinFree FinFree
   | And FinFree FinFree
   | Not FinFree
   | Implies FinFree FinFree
   | Top
   | Bottom
   -------------------------------------

   ----------- Event property ----------
   | PropIntForall  VariableIdentifier FinFree
   | PropTextForall VariableIdentifier FinFree
   | PropIntExists  VariableIdentifier FinFree
   | PropTextExists VariableIdentifier FinFree
   | PropIntBinRel BinRel IntTerm  IntTerm
   | PropTextEq    TextTerm  Text
   deriving (Int -> FinFree -> ShowS
[FinFree] -> ShowS
FinFree -> [Char]
(Int -> FinFree -> ShowS)
-> (FinFree -> [Char]) -> ([FinFree] -> ShowS) -> Show FinFree
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> FinFree -> ShowS
showsPrec :: Int -> FinFree -> ShowS
$cshow :: FinFree -> [Char]
show :: FinFree -> [Char]
$cshowList :: [FinFree] -> ShowS
showList :: [FinFree] -> ShowS
Show, FinFree -> FinFree -> Bool
(FinFree -> FinFree -> Bool)
-> (FinFree -> FinFree -> Bool) -> Eq FinFree
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FinFree -> FinFree -> Bool
== :: FinFree -> FinFree -> Bool
$c/= :: FinFree -> FinFree -> Bool
/= :: FinFree -> FinFree -> Bool
Eq, Eq FinFree
Eq FinFree =>
(FinFree -> FinFree -> Ordering)
-> (FinFree -> FinFree -> Bool)
-> (FinFree -> FinFree -> Bool)
-> (FinFree -> FinFree -> Bool)
-> (FinFree -> FinFree -> Bool)
-> (FinFree -> FinFree -> FinFree)
-> (FinFree -> FinFree -> FinFree)
-> Ord FinFree
FinFree -> FinFree -> Bool
FinFree -> FinFree -> Ordering
FinFree -> FinFree -> FinFree
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
$ccompare :: FinFree -> FinFree -> Ordering
compare :: FinFree -> FinFree -> Ordering
$c< :: FinFree -> FinFree -> Bool
< :: FinFree -> FinFree -> Bool
$c<= :: FinFree -> FinFree -> Bool
<= :: FinFree -> FinFree -> Bool
$c> :: FinFree -> FinFree -> Bool
> :: FinFree -> FinFree -> Bool
$c>= :: FinFree -> FinFree -> Bool
>= :: FinFree -> FinFree -> Bool
$cmax :: FinFree -> FinFree -> FinFree
max :: FinFree -> FinFree -> FinFree
$cmin :: FinFree -> FinFree -> FinFree
min :: FinFree -> FinFree -> FinFree
Ord)
   -------------------------------------

-- ---------------------------------------------------------------------------
-- Value accumulation (used by lower to eliminate text quantifiers)
-- ---------------------------------------------------------------------------

textValuesAccum :: Set Text -> VariableIdentifier -> FinFree -> Set Text
textValuesAccum :: Set VariableIdentifier
-> VariableIdentifier -> FinFree -> Set VariableIdentifier
textValuesAccum Set VariableIdentifier
acc VariableIdentifier
x (Or FinFree
phi FinFree
psi)      = Set VariableIdentifier
-> VariableIdentifier -> FinFree -> Set VariableIdentifier
textValuesAccum (Set VariableIdentifier
-> VariableIdentifier -> FinFree -> Set VariableIdentifier
textValuesAccum Set VariableIdentifier
acc VariableIdentifier
x FinFree
phi) VariableIdentifier
x FinFree
psi
textValuesAccum Set VariableIdentifier
acc VariableIdentifier
x (And FinFree
phi FinFree
psi)     = Set VariableIdentifier
-> VariableIdentifier -> FinFree -> Set VariableIdentifier
textValuesAccum (Set VariableIdentifier
-> VariableIdentifier -> FinFree -> Set VariableIdentifier
textValuesAccum Set VariableIdentifier
acc VariableIdentifier
x FinFree
phi) VariableIdentifier
x FinFree
psi
textValuesAccum Set VariableIdentifier
acc VariableIdentifier
x (Not FinFree
phi)         = Set VariableIdentifier
-> VariableIdentifier -> FinFree -> Set VariableIdentifier
textValuesAccum Set VariableIdentifier
acc VariableIdentifier
x FinFree
phi
textValuesAccum Set VariableIdentifier
acc VariableIdentifier
x (Implies FinFree
phi FinFree
psi) = Set VariableIdentifier
-> VariableIdentifier -> FinFree -> Set VariableIdentifier
textValuesAccum (Set VariableIdentifier
-> VariableIdentifier -> FinFree -> Set VariableIdentifier
textValuesAccum Set VariableIdentifier
acc VariableIdentifier
x FinFree
phi) VariableIdentifier
x FinFree
psi
textValuesAccum Set VariableIdentifier
acc VariableIdentifier
_ FinFree
Top               = Set VariableIdentifier
acc
textValuesAccum Set VariableIdentifier
acc VariableIdentifier
_ FinFree
Bottom            = Set VariableIdentifier
acc
textValuesAccum Set VariableIdentifier
acc VariableIdentifier
_ (PropIntBinRel {})                    = Set VariableIdentifier
acc
textValuesAccum Set VariableIdentifier
acc VariableIdentifier
_ (PropTextEq (TextConst VariableIdentifier
_) VariableIdentifier
_)         = Set VariableIdentifier
acc
textValuesAccum Set VariableIdentifier
acc VariableIdentifier
x (PropTextEq (TextVar VariableIdentifier
x') VariableIdentifier
v) | VariableIdentifier
x VariableIdentifier -> VariableIdentifier -> Bool
forall a. Eq a => a -> a -> Bool
== VariableIdentifier
x' = VariableIdentifier
-> Set VariableIdentifier -> Set VariableIdentifier
forall a. Ord a => a -> Set a -> Set a
Set.insert VariableIdentifier
v Set VariableIdentifier
acc
textValuesAccum Set VariableIdentifier
acc VariableIdentifier
_ (PropTextEq (TextVar VariableIdentifier
_) VariableIdentifier
_)           = Set VariableIdentifier
acc
textValuesAccum Set VariableIdentifier
acc VariableIdentifier
x (PropIntForall  VariableIdentifier
x' FinFree
phi) | VariableIdentifier
x VariableIdentifier -> VariableIdentifier -> Bool
forall a. Eq a => a -> a -> Bool
/= VariableIdentifier
x' = Set VariableIdentifier
-> VariableIdentifier -> FinFree -> Set VariableIdentifier
textValuesAccum Set VariableIdentifier
acc VariableIdentifier
x FinFree
phi
textValuesAccum Set VariableIdentifier
acc VariableIdentifier
_ (PropIntForall  VariableIdentifier
_ FinFree
_)               = Set VariableIdentifier
acc
textValuesAccum Set VariableIdentifier
acc VariableIdentifier
x (PropTextForall VariableIdentifier
x' FinFree
phi) | VariableIdentifier
x VariableIdentifier -> VariableIdentifier -> Bool
forall a. Eq a => a -> a -> Bool
/= VariableIdentifier
x' = Set VariableIdentifier
-> VariableIdentifier -> FinFree -> Set VariableIdentifier
textValuesAccum Set VariableIdentifier
acc VariableIdentifier
x FinFree
phi
textValuesAccum Set VariableIdentifier
acc VariableIdentifier
_ (PropTextForall VariableIdentifier
_ FinFree
_)               = Set VariableIdentifier
acc
textValuesAccum Set VariableIdentifier
acc VariableIdentifier
x (PropIntExists  VariableIdentifier
x' FinFree
phi) | VariableIdentifier
x VariableIdentifier -> VariableIdentifier -> Bool
forall a. Eq a => a -> a -> Bool
/= VariableIdentifier
x' = Set VariableIdentifier
-> VariableIdentifier -> FinFree -> Set VariableIdentifier
textValuesAccum Set VariableIdentifier
acc VariableIdentifier
x FinFree
phi
textValuesAccum Set VariableIdentifier
acc VariableIdentifier
_ (PropIntExists  VariableIdentifier
_ FinFree
_)               = Set VariableIdentifier
acc
textValuesAccum Set VariableIdentifier
acc VariableIdentifier
x (PropTextExists VariableIdentifier
x' FinFree
phi) | VariableIdentifier
x VariableIdentifier -> VariableIdentifier -> Bool
forall a. Eq a => a -> a -> Bool
/= VariableIdentifier
x' = Set VariableIdentifier
-> VariableIdentifier -> FinFree -> Set VariableIdentifier
textValuesAccum Set VariableIdentifier
acc VariableIdentifier
x FinFree
phi
textValuesAccum Set VariableIdentifier
acc VariableIdentifier
_ (PropTextExists VariableIdentifier
_ FinFree
_)               = Set VariableIdentifier
acc

textValues :: VariableIdentifier -> FinFree -> Set Text
textValues :: VariableIdentifier -> FinFree -> Set VariableIdentifier
textValues = Set VariableIdentifier
-> VariableIdentifier -> FinFree -> Set VariableIdentifier
textValuesAccum Set VariableIdentifier
forall a. Set a
Set.empty

-- ---------------------------------------------------------------------------
-- Capture-avoiding substitution
-- ---------------------------------------------------------------------------

-- | φ[v / x]  (integer substitution)
substInt :: IntValue -> VariableIdentifier -> FinFree -> FinFree
substInt :: IntValue -> VariableIdentifier -> FinFree -> FinFree
substInt IntValue
v VariableIdentifier
x (And FinFree
phi FinFree
psi)     = FinFree -> FinFree -> FinFree
And (IntValue -> VariableIdentifier -> FinFree -> FinFree
substInt IntValue
v VariableIdentifier
x FinFree
phi) (IntValue -> VariableIdentifier -> FinFree -> FinFree
substInt IntValue
v VariableIdentifier
x FinFree
psi)
substInt IntValue
v VariableIdentifier
x (Or FinFree
phi FinFree
psi)      = FinFree -> FinFree -> FinFree
Or (IntValue -> VariableIdentifier -> FinFree -> FinFree
substInt IntValue
v VariableIdentifier
x FinFree
phi) (IntValue -> VariableIdentifier -> FinFree -> FinFree
substInt IntValue
v VariableIdentifier
x FinFree
psi)
substInt IntValue
v VariableIdentifier
x (Implies FinFree
phi FinFree
psi) = FinFree -> FinFree -> FinFree
Implies (IntValue -> VariableIdentifier -> FinFree -> FinFree
substInt IntValue
v VariableIdentifier
x FinFree
phi) (IntValue -> VariableIdentifier -> FinFree -> FinFree
substInt IntValue
v VariableIdentifier
x FinFree
psi)
substInt IntValue
v VariableIdentifier
x (Not FinFree
phi)         = FinFree -> FinFree
Not (IntValue -> VariableIdentifier -> FinFree -> FinFree
substInt IntValue
v VariableIdentifier
x FinFree
phi)
substInt IntValue
_ VariableIdentifier
_ FinFree
Bottom            = FinFree
Bottom
substInt IntValue
_ VariableIdentifier
_ FinFree
Top               = FinFree
Top
substInt IntValue
v VariableIdentifier
x (PropIntBinRel BinRel
rel IntTerm
lhs IntTerm
rhs) = BinRel -> IntTerm -> IntTerm -> FinFree
PropIntBinRel BinRel
rel (IntValue -> VariableIdentifier -> IntTerm -> IntTerm
substIntTerm IntValue
v VariableIdentifier
x IntTerm
lhs) (IntValue -> VariableIdentifier -> IntTerm -> IntTerm
substIntTerm IntValue
v VariableIdentifier
x IntTerm
rhs)
substInt IntValue
_ VariableIdentifier
_ (PropTextEq TextTerm
t VariableIdentifier
rhs)          = TextTerm -> VariableIdentifier -> FinFree
PropTextEq TextTerm
t VariableIdentifier
rhs
substInt IntValue
v VariableIdentifier
x (PropIntForall  VariableIdentifier
x' FinFree
phi) | VariableIdentifier
x VariableIdentifier -> VariableIdentifier -> Bool
forall a. Eq a => a -> a -> Bool
/= VariableIdentifier
x' = VariableIdentifier -> FinFree -> FinFree
PropIntForall  VariableIdentifier
x' (IntValue -> VariableIdentifier -> FinFree -> FinFree
substInt IntValue
v VariableIdentifier
x FinFree
phi)
substInt IntValue
_ VariableIdentifier
_ (PropIntForall  VariableIdentifier
x' FinFree
phi)            = VariableIdentifier -> FinFree -> FinFree
PropIntForall  VariableIdentifier
x' FinFree
phi
substInt IntValue
v VariableIdentifier
x (PropTextForall VariableIdentifier
x' FinFree
phi) | VariableIdentifier
x VariableIdentifier -> VariableIdentifier -> Bool
forall a. Eq a => a -> a -> Bool
/= VariableIdentifier
x' = VariableIdentifier -> FinFree -> FinFree
PropTextForall VariableIdentifier
x' (IntValue -> VariableIdentifier -> FinFree -> FinFree
substInt IntValue
v VariableIdentifier
x FinFree
phi)
substInt IntValue
_ VariableIdentifier
_ (PropTextForall VariableIdentifier
x' FinFree
phi)            = VariableIdentifier -> FinFree -> FinFree
PropTextForall VariableIdentifier
x' FinFree
phi
substInt IntValue
v VariableIdentifier
x (PropIntExists  VariableIdentifier
x' FinFree
phi) | VariableIdentifier
x VariableIdentifier -> VariableIdentifier -> Bool
forall a. Eq a => a -> a -> Bool
/= VariableIdentifier
x' = VariableIdentifier -> FinFree -> FinFree
PropIntExists  VariableIdentifier
x' (IntValue -> VariableIdentifier -> FinFree -> FinFree
substInt IntValue
v VariableIdentifier
x FinFree
phi)
substInt IntValue
_ VariableIdentifier
_ (PropIntExists  VariableIdentifier
x' FinFree
phi)            = VariableIdentifier -> FinFree -> FinFree
PropIntExists  VariableIdentifier
x' FinFree
phi
substInt IntValue
v VariableIdentifier
x (PropTextExists VariableIdentifier
x' FinFree
phi) | VariableIdentifier
x VariableIdentifier -> VariableIdentifier -> Bool
forall a. Eq a => a -> a -> Bool
/= VariableIdentifier
x' = VariableIdentifier -> FinFree -> FinFree
PropTextExists VariableIdentifier
x' (IntValue -> VariableIdentifier -> FinFree -> FinFree
substInt IntValue
v VariableIdentifier
x FinFree
phi)
substInt IntValue
_ VariableIdentifier
_ (PropTextExists VariableIdentifier
x' FinFree
phi)            = VariableIdentifier -> FinFree -> FinFree
PropTextExists VariableIdentifier
x' FinFree
phi

-- | φ[v / x]  (text substitution)
substText :: Extended Text -> VariableIdentifier -> FinFree -> FinFree
substText :: Extended VariableIdentifier
-> VariableIdentifier -> FinFree -> FinFree
substText Extended VariableIdentifier
v VariableIdentifier
x (And FinFree
phi FinFree
psi)     = FinFree -> FinFree -> FinFree
And (Extended VariableIdentifier
-> VariableIdentifier -> FinFree -> FinFree
substText Extended VariableIdentifier
v VariableIdentifier
x FinFree
phi) (Extended VariableIdentifier
-> VariableIdentifier -> FinFree -> FinFree
substText Extended VariableIdentifier
v VariableIdentifier
x FinFree
psi)
substText Extended VariableIdentifier
v VariableIdentifier
x (Or FinFree
phi FinFree
psi)      = FinFree -> FinFree -> FinFree
Or (Extended VariableIdentifier
-> VariableIdentifier -> FinFree -> FinFree
substText Extended VariableIdentifier
v VariableIdentifier
x FinFree
phi) (Extended VariableIdentifier
-> VariableIdentifier -> FinFree -> FinFree
substText Extended VariableIdentifier
v VariableIdentifier
x FinFree
psi)
substText Extended VariableIdentifier
v VariableIdentifier
x (Implies FinFree
phi FinFree
psi) = FinFree -> FinFree -> FinFree
Implies (Extended VariableIdentifier
-> VariableIdentifier -> FinFree -> FinFree
substText Extended VariableIdentifier
v VariableIdentifier
x FinFree
phi) (Extended VariableIdentifier
-> VariableIdentifier -> FinFree -> FinFree
substText Extended VariableIdentifier
v VariableIdentifier
x FinFree
psi)
substText Extended VariableIdentifier
v VariableIdentifier
x (Not FinFree
phi)         = FinFree -> FinFree
Not (Extended VariableIdentifier
-> VariableIdentifier -> FinFree -> FinFree
substText Extended VariableIdentifier
v VariableIdentifier
x FinFree
phi)
substText Extended VariableIdentifier
_ VariableIdentifier
_ FinFree
Bottom            = FinFree
Bottom
substText Extended VariableIdentifier
_ VariableIdentifier
_ FinFree
Top               = FinFree
Top
substText Extended VariableIdentifier
_ VariableIdentifier
_ (PropIntBinRel BinRel
rel IntTerm
lhs IntTerm
rhs)    = BinRel -> IntTerm -> IntTerm -> FinFree
PropIntBinRel BinRel
rel IntTerm
lhs IntTerm
rhs
substText Extended VariableIdentifier
_ VariableIdentifier
_ (PropTextEq (TextConst VariableIdentifier
c) VariableIdentifier
rhs) = TextTerm -> VariableIdentifier -> FinFree
PropTextEq (VariableIdentifier -> TextTerm
TextConst VariableIdentifier
c) VariableIdentifier
rhs
-- (x = v)[☐ / x] = ⊥ — placeholder is distinct from all strings
substText Extended VariableIdentifier
Placeholder VariableIdentifier
x (PropTextEq (TextVar VariableIdentifier
x') VariableIdentifier
_) | VariableIdentifier
x VariableIdentifier -> VariableIdentifier -> Bool
forall a. Eq a => a -> a -> Bool
== VariableIdentifier
x' = FinFree
Bottom
substText (Val VariableIdentifier
v) VariableIdentifier
x (PropTextEq (TextVar VariableIdentifier
x') VariableIdentifier
rhs)   | VariableIdentifier
x VariableIdentifier -> VariableIdentifier -> Bool
forall a. Eq a => a -> a -> Bool
== VariableIdentifier
x' = TextTerm -> VariableIdentifier -> FinFree
PropTextEq (VariableIdentifier -> TextTerm
TextConst VariableIdentifier
v) VariableIdentifier
rhs
substText Extended VariableIdentifier
_ VariableIdentifier
_ (PropTextEq (TextVar VariableIdentifier
x') VariableIdentifier
rhs)                    = TextTerm -> VariableIdentifier -> FinFree
PropTextEq (VariableIdentifier -> TextTerm
TextVar VariableIdentifier
x') VariableIdentifier
rhs
substText Extended VariableIdentifier
v VariableIdentifier
x (PropIntForall  VariableIdentifier
x' FinFree
phi) | VariableIdentifier
x VariableIdentifier -> VariableIdentifier -> Bool
forall a. Eq a => a -> a -> Bool
/= VariableIdentifier
x' = VariableIdentifier -> FinFree -> FinFree
PropIntForall  VariableIdentifier
x' (Extended VariableIdentifier
-> VariableIdentifier -> FinFree -> FinFree
substText Extended VariableIdentifier
v VariableIdentifier
x FinFree
phi)
substText Extended VariableIdentifier
_ VariableIdentifier
_ (PropIntForall  VariableIdentifier
x' FinFree
phi)            = VariableIdentifier -> FinFree -> FinFree
PropIntForall  VariableIdentifier
x' FinFree
phi
substText Extended VariableIdentifier
v VariableIdentifier
x (PropTextForall VariableIdentifier
x' FinFree
phi) | VariableIdentifier
x VariableIdentifier -> VariableIdentifier -> Bool
forall a. Eq a => a -> a -> Bool
/= VariableIdentifier
x' = VariableIdentifier -> FinFree -> FinFree
PropTextForall VariableIdentifier
x' (Extended VariableIdentifier
-> VariableIdentifier -> FinFree -> FinFree
substText Extended VariableIdentifier
v VariableIdentifier
x FinFree
phi)
substText Extended VariableIdentifier
_ VariableIdentifier
_ (PropTextForall VariableIdentifier
x' FinFree
phi)            = VariableIdentifier -> FinFree -> FinFree
PropTextForall VariableIdentifier
x' FinFree
phi
substText Extended VariableIdentifier
v VariableIdentifier
x (PropIntExists  VariableIdentifier
x' FinFree
phi) | VariableIdentifier
x VariableIdentifier -> VariableIdentifier -> Bool
forall a. Eq a => a -> a -> Bool
/= VariableIdentifier
x' = VariableIdentifier -> FinFree -> FinFree
PropIntExists  VariableIdentifier
x' (Extended VariableIdentifier
-> VariableIdentifier -> FinFree -> FinFree
substText Extended VariableIdentifier
v VariableIdentifier
x FinFree
phi)
substText Extended VariableIdentifier
_ VariableIdentifier
_ (PropIntExists  VariableIdentifier
x' FinFree
phi)            = VariableIdentifier -> FinFree -> FinFree
PropIntExists  VariableIdentifier
x' FinFree
phi
substText Extended VariableIdentifier
v VariableIdentifier
x (PropTextExists VariableIdentifier
x' FinFree
phi) | VariableIdentifier
x VariableIdentifier -> VariableIdentifier -> Bool
forall a. Eq a => a -> a -> Bool
/= VariableIdentifier
x' = VariableIdentifier -> FinFree -> FinFree
PropTextExists VariableIdentifier
x' (Extended VariableIdentifier
-> VariableIdentifier -> FinFree -> FinFree
substText Extended VariableIdentifier
v VariableIdentifier
x FinFree
phi)
substText Extended VariableIdentifier
_ VariableIdentifier
_ (PropTextExists VariableIdentifier
x' FinFree
phi)            = VariableIdentifier -> FinFree -> FinFree
PropTextExists VariableIdentifier
x' FinFree
phi

-- ---------------------------------------------------------------------------
-- Lowering to Presburger.Formula
-- ---------------------------------------------------------------------------

-- | Lower a `FinFree` to 'P.Formula' by eliminating all text quantifiers and
--   evaluating ground `PropTextEq` atoms.
--
--   Text universals unfold to a conjunction (⊤ for empty domain);
--   text existentials unfold to a disjunction (⊥ for empty domain).
--
--   @'eval' = 'PD.eval' . 'lower'@
lower :: FinFree -> P.Formula
lower :: FinFree -> Formula
lower (Or FinFree
phi FinFree
psi)      = Formula -> Formula -> Formula
P.Or (FinFree -> Formula
lower FinFree
phi) (FinFree -> Formula
lower FinFree
psi)
lower (And FinFree
phi FinFree
psi)     = Formula -> Formula -> Formula
P.And (FinFree -> Formula
lower FinFree
phi) (FinFree -> Formula
lower FinFree
psi)
lower (Not FinFree
phi)         = Formula -> Formula
P.Not (FinFree -> Formula
lower FinFree
phi)
lower (Implies FinFree
phi FinFree
psi) = Formula -> Formula -> Formula
P.Implies (FinFree -> Formula
lower FinFree
phi) (FinFree -> Formula
lower FinFree
psi)
lower FinFree
Top               = Formula
P.Top
lower FinFree
Bottom            = Formula
P.Bottom
lower (PropIntForall VariableIdentifier
x FinFree
phi) = VariableIdentifier -> Formula -> Formula
P.IntForall VariableIdentifier
x (FinFree -> Formula
lower FinFree
phi)
lower (PropIntExists VariableIdentifier
x FinFree
phi) = VariableIdentifier -> Formula -> Formula
P.IntExists VariableIdentifier
x (FinFree -> Formula
lower FinFree
phi)
lower (PropIntBinRel BinRel
rel IntTerm
lhs IntTerm
rhs) = BinRel -> IntTerm -> IntTerm -> Formula
P.IntBinRel BinRel
rel IntTerm
lhs IntTerm
rhs
-- Ground text equations are folded directly to ⊤/⊥:
lower (PropTextEq (TextConst VariableIdentifier
lhs) VariableIdentifier
rhs)
  | VariableIdentifier
lhs VariableIdentifier -> VariableIdentifier -> Bool
forall a. Eq a => a -> a -> Bool
== VariableIdentifier
rhs = Formula
P.Top
  | Bool
otherwise  = Formula
P.Bottom
lower (PropTextEq (TextVar VariableIdentifier
x) VariableIdentifier
_) = [Char] -> Formula
forall a. HasCallStack => [Char] -> a
error ([Char] -> Formula) -> [Char] -> Formula
forall a b. (a -> b) -> a -> b
$ [Char]
"lower: free text variable " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> VariableIdentifier -> [Char]
forall a. Show a => a -> [Char]
show VariableIdentifier
x
-- ⟦∀x ∈ Text. φ⟧ ≡ φ[☐/x] ∧ φ[v₁/x] ∧ ...  (⊤ when dom is empty)
lower (PropTextForall VariableIdentifier
x FinFree
phi) =
  let vals :: [VariableIdentifier]
vals = Set VariableIdentifier -> [VariableIdentifier]
forall a. Set a -> [a]
Set.toList (VariableIdentifier -> FinFree -> Set VariableIdentifier
textValues VariableIdentifier
x FinFree
phi)
  in (Formula -> Formula -> Formula) -> Formula -> [Formula] -> Formula
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Formula -> Formula -> Formula
P.And Formula
P.Top
       (FinFree -> Formula
lower (Extended VariableIdentifier
-> VariableIdentifier -> FinFree -> FinFree
substText Extended VariableIdentifier
forall a. Extended a
Placeholder VariableIdentifier
x FinFree
phi) Formula -> [Formula] -> [Formula]
forall a. a -> [a] -> [a]
: ([VariableIdentifier]
vals [VariableIdentifier]
-> (VariableIdentifier -> Formula) -> [Formula]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \VariableIdentifier
v -> FinFree -> Formula
lower (Extended VariableIdentifier
-> VariableIdentifier -> FinFree -> FinFree
substText (VariableIdentifier -> Extended VariableIdentifier
forall a. a -> Extended a
Val VariableIdentifier
v) VariableIdentifier
x FinFree
phi)))
-- ⟦∃x ∈ Text. φ⟧ ≡ φ[☐/x] ∨ φ[v₁/x] ∨ ...  (⊥ when dom is empty)
lower (PropTextExists VariableIdentifier
x FinFree
phi) =
  let vals :: [VariableIdentifier]
vals = Set VariableIdentifier -> [VariableIdentifier]
forall a. Set a -> [a]
Set.toList (VariableIdentifier -> FinFree -> Set VariableIdentifier
textValues VariableIdentifier
x FinFree
phi)
  in (Formula -> Formula -> Formula) -> Formula -> [Formula] -> Formula
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Formula -> Formula -> Formula
P.Or Formula
P.Bottom
       (FinFree -> Formula
lower (Extended VariableIdentifier
-> VariableIdentifier -> FinFree -> FinFree
substText Extended VariableIdentifier
forall a. Extended a
Placeholder VariableIdentifier
x FinFree
phi) Formula -> [Formula] -> [Formula]
forall a. a -> [a] -> [a]
: ([VariableIdentifier]
vals [VariableIdentifier]
-> (VariableIdentifier -> Formula) -> [Formula]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \VariableIdentifier
v -> FinFree -> Formula
lower (Extended VariableIdentifier
-> VariableIdentifier -> FinFree -> FinFree
substText (VariableIdentifier -> Extended VariableIdentifier
forall a. a -> Extended a
Val VariableIdentifier
v) VariableIdentifier
x FinFree
phi)))

-- | Evaluate the `FinFree` onto `Bool`.
eval :: FinFree -> Bool
eval :: FinFree -> Bool
eval = Formula -> Bool
PD.eval (Formula -> Bool) -> (FinFree -> Formula) -> FinFree -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FinFree -> Formula
lower