module Hermod.ReCon.LTL.Formula.Pretty (
    Prec(..)
  , prettyIntTerm
  , prettyTextTerm
  , prettyBinRel
  , prettyPropConstraint
  , prettyPropConstraints
  , prettyFormula) where

import           Cardano.Logging (showT)
import           Hermod.ReCon.LTL.Formula
import           Hermod.ReCon.LTL.Formula.Prec (Prec)
import qualified Hermod.ReCon.LTL.Formula.Prec as Prec

import qualified Data.Set as Set
import           Data.Text (Text, intercalate)

-- | Add parentheses when an inner precedence exceeds the outer one.
surround :: Prec -> Prec -> Text -> Text
surround :: Prec -> Prec -> Text -> Text
surround Prec
outer Prec
inner Text
str | Prec
outer Prec -> Prec -> Bool
forall a. Ord a => a -> a -> Bool
<= Prec
inner = Text
str
surround Prec
_ Prec
_ Text
str = Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
str Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"

-- | Render an integer term.
prettyIntTerm :: IntTerm -> Text
prettyIntTerm :: IntTerm -> Text
prettyIntTerm (IntVar IntValue
1 Text
x) = Text
x
prettyIntTerm (IntVar IntValue
k Text
x) = IntValue -> Text
forall a. Show a => a -> Text
showT IntValue
k Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"·" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
x
prettyIntTerm (IntConst IntValue
n) = IntValue -> Text
forall a. Show a => a -> Text
showT IntValue
n
prettyIntTerm (IntSum IntTerm
a IntTerm
b) = IntTerm -> Text
prettyIntTerm IntTerm
a Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" + " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> IntTerm -> Text
prettyIntTerm IntTerm
b

-- | Render a text term.
prettyTextTerm :: TextTerm -> Text
prettyTextTerm :: TextTerm -> Text
prettyTextTerm (TextVar Text
x)   = Text
x
prettyTextTerm (TextConst Text
s) = Text -> Text
forall a. Show a => a -> Text
showT Text
s

-- | Render a binary relation symbol.
prettyBinRel :: BinRel -> Text
prettyBinRel :: BinRel -> Text
prettyBinRel BinRel
Eq  = Text
"="
prettyBinRel BinRel
Lt  = Text
"<"
prettyBinRel BinRel
Lte = Text
"≤"
prettyBinRel BinRel
Gt  = Text
">"
prettyBinRel BinRel
Gte = Text
"≥"

-- | Render a single property constraint.
prettyPropConstraint :: PropConstraint -> Text
prettyPropConstraint :: PropConstraint -> Text
prettyPropConstraint (IntPropConstraint  Text
k IntTerm
t) = Text -> Text
forall a. Show a => a -> Text
showT Text
k Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" = " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> IntTerm -> Text
prettyIntTerm IntTerm
t
prettyPropConstraint (TextPropConstraint Text
k TextTerm
t) = Text -> Text
forall a. Show a => a -> Text
showT Text
k Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" = " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> TextTerm -> Text
prettyTextTerm TextTerm
t

-- | Render a list of property constraints.
prettyPropConstraints :: [PropConstraint] -> Text
prettyPropConstraints :: [PropConstraint] -> Text
prettyPropConstraints = Text -> [Text] -> Text
intercalate Text
", " ([Text] -> Text)
-> ([PropConstraint] -> [Text]) -> [PropConstraint] -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PropConstraint -> Text) -> [PropConstraint] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PropConstraint -> Text
prettyPropConstraint

wordToXscript :: (Word -> Text) -> Word -> Text
wordToXscript :: (Word -> Text) -> Word -> Text
wordToXscript Word -> Text
f Word
x =
  let (Word
d, Word
m) = Word
x Word -> Word -> (Word, Word)
forall a. Integral a => a -> a -> (a, a)
`divMod` Word
10
      ch :: Text
ch = Word -> Text
f Word
m in
  if Word
d Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
0
  then
    Text
ch
  else
    (Word -> Text) -> Word -> Text
wordToXscript Word -> Text
f Word
d Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
ch

wordToSuperscript :: Word -> Text
wordToSuperscript :: Word -> Text
wordToSuperscript = (Word -> Text) -> Word -> Text
wordToXscript Word -> Text
superscript0to9 where
  superscript0to9 :: Word -> Text
  superscript0to9 :: Word -> Text
superscript0to9 Word
0 = Text
"⁰"
  superscript0to9 Word
1 = Text
"¹"
  superscript0to9 Word
2 = Text
"²"
  superscript0to9 Word
3 = Text
"³"
  superscript0to9 Word
4 = Text
"⁴"
  superscript0to9 Word
5 = Text
"⁵"
  superscript0to9 Word
6 = Text
"⁶"
  superscript0to9 Word
7 = Text
"⁷"
  superscript0to9 Word
8 = Text
"⁸"
  superscript0to9 Word
9 = Text
"⁹"
  superscript0to9 Word
_ = Text
"" -- Unexpected input

wordToSubscript :: Word -> Text
wordToSubscript :: Word -> Text
wordToSubscript = (Word -> Text) -> Word -> Text
wordToXscript Word -> Text
subscript0to9 where
  subscript0to9 :: Word -> Text
  subscript0to9 :: Word -> Text
subscript0to9 Word
0 = Text
"₀"
  subscript0to9 Word
1 = Text
"₁"
  subscript0to9 Word
2 = Text
"₂"
  subscript0to9 Word
3 = Text
"₃"
  subscript0to9 Word
4 = Text
"₄"
  subscript0to9 Word
5 = Text
"₅"
  subscript0to9 Word
6 = Text
"₆"
  subscript0to9 Word
7 = Text
"₇"
  subscript0to9 Word
8 = Text
"₈"
  subscript0to9 Word
9 = Text
"₉"
  subscript0to9 Word
_ = Text
"" -- Unexpected input


-- | Pretty-print a `Formula` using unicode operators.
prettyFormula :: Show a => Formula event a -> Prec -> Text
prettyFormula :: forall a event. Show a => Formula event a -> Prec -> Text
prettyFormula (Forall Word
k Formula event a
phi) Prec
lvl = Prec -> Prec -> Text -> Text
surround Prec
lvl Prec
Prec.Prefix (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$
  Text
"☐ ᪲" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> (if Word
k Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
0 then Text
"" else Word -> Text
wordToSubscript Word
k) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Formula event a -> Prec -> Text
forall a event. Show a => Formula event a -> Prec -> Text
prettyFormula Formula event a
phi Prec
Prec.Atom
prettyFormula (ForallN Word
k Formula event a
phi) Prec
lvl = Prec -> Prec -> Text -> Text
surround Prec
lvl Prec
Prec.Prefix (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$
  Text
"☐" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Word -> Text
wordToSuperscript Word
k Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Formula event a -> Prec -> Text
forall a event. Show a => Formula event a -> Prec -> Text
prettyFormula Formula event a
phi Prec
Prec.Atom
prettyFormula (ExistsN Word
k Formula event a
phi) Prec
lvl = Prec -> Prec -> Text -> Text
surround Prec
lvl Prec
Prec.Prefix (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$
  Text
"♢" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Word -> Text
wordToSuperscript Word
k Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Formula event a -> Prec -> Text
forall a event. Show a => Formula event a -> Prec -> Text
prettyFormula Formula event a
phi Prec
Prec.Atom
prettyFormula (Next Formula event a
phi) Prec
lvl = Prec -> Prec -> Text -> Text
surround Prec
lvl Prec
Prec.Prefix (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$
  Text
"◯" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Formula event a -> Prec -> Text
forall a event. Show a => Formula event a -> Prec -> Text
prettyFormula Formula event a
phi Prec
Prec.Atom
prettyFormula (NextN Word
k Formula event a
phi) Prec
lvl = Prec -> Prec -> Text -> Text
surround Prec
lvl Prec
Prec.Prefix (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$
  Text
"◯" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Word -> Text
wordToSuperscript Word
k Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Formula event a -> Prec -> Text
forall a event. Show a => Formula event a -> Prec -> Text
prettyFormula Formula event a
phi Prec
Prec.Atom
prettyFormula (UntilN Word
k Formula event a
phi Formula event a
psi) Prec
lvl = Prec -> Prec -> Text -> Text
surround Prec
lvl Prec
Prec.Universe (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$
  Formula event a -> Prec -> Text
forall a event. Show a => Formula event a -> Prec -> Text
prettyFormula Formula event a
phi Prec
Prec.Implies Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"|" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Word -> Text
wordToSuperscript Word
k Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Formula event a -> Prec -> Text
forall a event. Show a => Formula event a -> Prec -> Text
prettyFormula Formula event a
psi Prec
Prec.Implies
prettyFormula (Implies Formula event a
phi Formula event a
psi) Prec
lvl = Prec -> Prec -> Text -> Text
surround Prec
lvl Prec
Prec.Implies (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$
  Formula event a -> Prec -> Text
forall a event. Show a => Formula event a -> Prec -> Text
prettyFormula Formula event a
phi Prec
Prec.Or Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"⇒" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Formula event a -> Prec -> Text
forall a event. Show a => Formula event a -> Prec -> Text
prettyFormula Formula event a
psi Prec
Prec.Implies
prettyFormula (Or Formula event a
phi Formula event a
psi) Prec
lvl = Prec -> Prec -> Text -> Text
surround Prec
lvl Prec
Prec.Or (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$
  Formula event a -> Prec -> Text
forall a event. Show a => Formula event a -> Prec -> Text
prettyFormula Formula event a
phi Prec
Prec.Or Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"∨" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Formula event a -> Prec -> Text
forall a event. Show a => Formula event a -> Prec -> Text
prettyFormula Formula event a
psi Prec
Prec.Or
prettyFormula (And Formula event a
phi Formula event a
psi) Prec
lvl = Prec -> Prec -> Text -> Text
surround Prec
lvl Prec
Prec.And (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$
  Formula event a -> Prec -> Text
forall a event. Show a => Formula event a -> Prec -> Text
prettyFormula Formula event a
phi Prec
Prec.And Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"∧" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Formula event a -> Prec -> Text
forall a event. Show a => Formula event a -> Prec -> Text
prettyFormula Formula event a
psi Prec
Prec.And
prettyFormula (Not Formula event a
phi) Prec
lvl = Prec -> Prec -> Text -> Text
surround Prec
lvl Prec
Prec.Prefix (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$
  Text
"¬ " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Formula event a -> Prec -> Text
forall a event. Show a => Formula event a -> Prec -> Text
prettyFormula Formula event a
phi Prec
Prec.Atom
prettyFormula Formula event a
Top Prec
lvl = Prec -> Prec -> Text -> Text
surround Prec
lvl Prec
Prec.Atom Text
"⊤"
prettyFormula Formula event a
Bottom Prec
lvl = Prec -> Prec -> Text -> Text
surround Prec
lvl Prec
Prec.Atom Text
"⊥"
prettyFormula (PropIntForall Text
x Formula event a
phi) Prec
lvl = Prec -> Prec -> Text -> Text
surround Prec
lvl Prec
Prec.Universe (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$
  Text
"∀" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
x Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" ∈ ℤ. " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Formula event a -> Prec -> Text
forall a event. Show a => Formula event a -> Prec -> Text
prettyFormula Formula event a
phi Prec
Prec.Universe
prettyFormula (PropTextForall Text
x Formula event a
phi) Prec
lvl = Prec -> Prec -> Text -> Text
surround Prec
lvl Prec
Prec.Universe (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$
  Text
"∀" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
x Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" ∈ Text. " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Formula event a -> Prec -> Text
forall a event. Show a => Formula event a -> Prec -> Text
prettyFormula Formula event a
phi Prec
Prec.Universe
prettyFormula (PropIntForallN Text
x Set IntValue
dom Formula event a
phi) Prec
lvl = Prec -> Prec -> Text -> Text
surround Prec
lvl Prec
Prec.Universe (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$
  Text
"∀" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
x Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" ∈ "
      Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"{" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> [Text] -> Text
intercalate Text
", " ((IntValue -> Text) -> [IntValue] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap IntValue -> Text
forall a. Show a => a -> Text
showT (Set IntValue -> [IntValue]
forall a. Set a -> [a]
Set.toList Set IntValue
dom)) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"}"
      Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
". " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Formula event a -> Prec -> Text
forall a event. Show a => Formula event a -> Prec -> Text
prettyFormula Formula event a
phi Prec
Prec.Universe
prettyFormula (PropTextForallN Text
x Set Text
dom Formula event a
phi) Prec
lvl = Prec -> Prec -> Text -> Text
surround Prec
lvl Prec
Prec.Universe (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$
  Text
"∀" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
x Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" ∈ "
      Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"{" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> [Text] -> Text
intercalate Text
", " ((Text -> Text) -> [Text] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Text -> Text
forall a. Show a => a -> Text
showT (Set Text -> [Text]
forall a. Set a -> [a]
Set.toList Set Text
dom)) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"}"
      Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
". " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Formula event a -> Prec -> Text
forall a event. Show a => Formula event a -> Prec -> Text
prettyFormula Formula event a
phi Prec
Prec.Universe
prettyFormula (PropIntExists Text
x Formula event a
phi) Prec
lvl = Prec -> Prec -> Text -> Text
surround Prec
lvl Prec
Prec.Universe (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$
  Text
"∃" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
x Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" ∈ ℤ. " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Formula event a -> Prec -> Text
forall a event. Show a => Formula event a -> Prec -> Text
prettyFormula Formula event a
phi Prec
Prec.Universe
prettyFormula (PropTextExists Text
x Formula event a
phi) Prec
lvl = Prec -> Prec -> Text -> Text
surround Prec
lvl Prec
Prec.Universe (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$
  Text
"∃" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
x Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" ∈ Text. " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Formula event a -> Prec -> Text
forall a event. Show a => Formula event a -> Prec -> Text
prettyFormula Formula event a
phi Prec
Prec.Universe
prettyFormula (PropIntExistsN Text
x Set IntValue
dom Formula event a
phi) Prec
lvl = Prec -> Prec -> Text -> Text
surround Prec
lvl Prec
Prec.Universe (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$
  Text
"∃" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
x Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" ∈ "
      Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"{" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> [Text] -> Text
intercalate Text
", " ((IntValue -> Text) -> [IntValue] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap IntValue -> Text
forall a. Show a => a -> Text
showT (Set IntValue -> [IntValue]
forall a. Set a -> [a]
Set.toList Set IntValue
dom)) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"}"
      Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
". " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Formula event a -> Prec -> Text
forall a event. Show a => Formula event a -> Prec -> Text
prettyFormula Formula event a
phi Prec
Prec.Universe
prettyFormula (PropTextExistsN Text
x Set Text
dom Formula event a
phi) Prec
lvl = Prec -> Prec -> Text -> Text
surround Prec
lvl Prec
Prec.Universe (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$
  Text
"∃" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
x Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" ∈ "
      Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"{" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> [Text] -> Text
intercalate Text
", " ((Text -> Text) -> [Text] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Text -> Text
forall a. Show a => a -> Text
showT (Set Text -> [Text]
forall a. Set a -> [a]
Set.toList Set Text
dom)) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"}"
      Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
". " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Formula event a -> Prec -> Text
forall a event. Show a => Formula event a -> Prec -> Text
prettyFormula Formula event a
phi Prec
Prec.Universe
prettyFormula (Atom a
c Set PropConstraint
is) Prec
lvl = Prec -> Prec -> Text -> Text
surround Prec
lvl Prec
Prec.Atom (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$
  a -> Text
forall a. Show a => a -> Text
showT a
c Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [PropConstraint] -> Text
prettyPropConstraints (Set PropConstraint -> [PropConstraint]
forall a. Set a -> [a]
Set.toList Set PropConstraint
is) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
prettyFormula (PropIntBinRel BinRel
rel Relevance event a
_ IntTerm
lhs IntTerm
rhs) Prec
lvl = Prec -> Prec -> Text -> Text
surround Prec
lvl Prec
Prec.Eq (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$
  IntTerm -> Text
prettyIntTerm IntTerm
lhs Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> BinRel -> Text
prettyBinRel BinRel
rel Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> IntTerm -> Text
prettyIntTerm IntTerm
rhs
prettyFormula (PropTextEq Relevance event a
_ TextTerm
t Text
v) Prec
lvl = Prec -> Prec -> Text -> Text
surround Prec
lvl Prec
Prec.Eq (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$
  TextTerm -> Text
prettyTextTerm TextTerm
t Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" = " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> Text
forall a. Show a => a -> Text
showT Text
v