-- |
-- Module      : Test.Speculate.CondReason
-- Copyright   : (c) 2016-2019 Rudy Matela
-- License     : 3-Clause BSD  (see the file LICENSE)
-- Maintainer  : Rudy Matela <rudy@matela.com.br>
--
-- This module is part o Speculate.
--
-- Conditional equational reasoning.
module Test.Speculate.CondReason where

import Test.Speculate.Expr
import Test.Speculate.Reason
import qualified Test.Speculate.Utils.Digraph as D
import Test.Speculate.Utils.Digraph (Digraph)
import Data.Maybe (maybeToList,fromMaybe)
import Data.List (lookup, sortBy)
import Data.Function (on)
import Data.Functor ((<$>)) -- for GHC < 7.10
import qualified Data.List as L
import Test.Speculate.Utils

-- Chy = Conditional Thy = Conditional Theory
data Chy = Chy
  { Chy -> [(Expr, Expr, Expr)]
cequations :: [(Expr,Expr,Expr)]
  , Chy -> Digraph Expr
cimplications :: Digraph Expr
  , Chy -> Digraph Expr
cclasses :: [(Expr,[Expr])]
  , Chy -> Thy
unThy :: Thy
  }

emptyChy :: Chy
emptyChy :: Chy
emptyChy = Chy :: [(Expr, Expr, Expr)] -> Digraph Expr -> Digraph Expr -> Thy -> Chy
Chy
  { cequations :: [(Expr, Expr, Expr)]
cequations = []
  , cimplications :: Digraph Expr
cimplications = Digraph Expr
forall a. Digraph a
D.empty
  , cclasses :: Digraph Expr
cclasses = []
  , unThy :: Thy
unThy = Thy
emptyThy
  }

updateCEquationsBy :: ([(Expr,Expr,Expr)] -> [(Expr,Expr,Expr)]) -> Chy -> Chy
updateCEquationsBy :: ([(Expr, Expr, Expr)] -> [(Expr, Expr, Expr)]) -> Chy -> Chy
updateCEquationsBy [(Expr, Expr, Expr)] -> [(Expr, Expr, Expr)]
f chy :: Chy
chy@Chy{cequations :: Chy -> [(Expr, Expr, Expr)]
cequations = [(Expr, Expr, Expr)]
ceqs} = Chy
chy{cequations :: [(Expr, Expr, Expr)]
cequations = [(Expr, Expr, Expr)] -> [(Expr, Expr, Expr)]
f [(Expr, Expr, Expr)]
ceqs}

listImplied :: Chy -> Expr -> [Expr]
listImplied :: Chy -> Expr -> [Expr]
listImplied Chy{cimplications :: Chy -> Digraph Expr
cimplications = Digraph Expr
ccss} Expr
ce = Expr -> Digraph Expr -> [Expr]
forall a. Eq a => a -> Digraph a -> [a]
D.succs Expr
ce Digraph Expr
ccss

listImplies :: Chy -> Expr -> [Expr]
listImplies :: Chy -> Expr -> [Expr]
listImplies Chy{cimplications :: Chy -> Digraph Expr
cimplications = Digraph Expr
ccss} Expr
ce = Expr -> Digraph Expr -> [Expr]
forall a. Eq a => a -> Digraph a -> [a]
D.preds Expr
ce Digraph Expr
ccss

listEquivalent :: Chy -> Expr -> [Expr]
listEquivalent :: Chy -> Expr -> [Expr]
listEquivalent Chy{cclasses :: Chy -> Digraph Expr
cclasses = Digraph Expr
ccss} Expr
ce = [Expr] -> Maybe [Expr] -> [Expr]
forall a. a -> Maybe a -> a
fromMaybe [] (Maybe [Expr] -> [Expr]) -> Maybe [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$ Expr -> Digraph Expr -> Maybe [Expr]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Expr
ce Digraph Expr
ccss

reduceRootWith :: Binds -> Expr -> (Expr,Expr) -> Maybe Expr
reduceRootWith :: Binds -> Expr -> (Expr, Expr) -> Maybe Expr
reduceRootWith Binds
bs Expr
e (Expr
e1,Expr
e2) = (Expr
e2 Expr -> Binds -> Expr
//-) (Binds -> Expr) -> Maybe Binds -> Maybe Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Binds -> Expr -> Expr -> Maybe Binds
matchWith Binds
bs Expr
e Expr
e1

reductions1With :: Binds -> Expr -> (Expr,Expr) -> [Expr]
reductions1With :: Binds -> Expr -> (Expr, Expr) -> [Expr]
reductions1With Binds
bs Expr
e (Expr
l,Expr
_) | Expr -> Int
size Expr
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Expr -> Int
size Expr
e = [] -- optional optimization
reductions1With Binds
bs e :: Expr
e@(Expr
e1 :$ Expr
e2) (Expr, Expr)
r = Maybe Expr -> [Expr]
forall a. Maybe a -> [a]
maybeToList (Binds -> Expr -> (Expr, Expr) -> Maybe Expr
reduceRootWith Binds
bs Expr
e (Expr, Expr)
r)
                                 [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ (Expr -> Expr) -> [Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Expr -> Expr -> Expr
:$ Expr
e2) (Binds -> Expr -> (Expr, Expr) -> [Expr]
reductions1With Binds
bs Expr
e1 (Expr, Expr)
r)
                                 [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ (Expr -> Expr) -> [Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Expr
e1 Expr -> Expr -> Expr
:$) (Binds -> Expr -> (Expr, Expr) -> [Expr]
reductions1With Binds
bs Expr
e2 (Expr, Expr)
r)
reductions1With Binds
bs Expr
e (Expr, Expr)
r = Maybe Expr -> [Expr]
forall a. Maybe a -> [a]
maybeToList (Binds -> Expr -> (Expr, Expr) -> Maybe Expr
reduceRootWith Binds
bs Expr
e (Expr, Expr)
r)

creductions1 :: Expr -> Expr -> (Expr,Expr,Expr) -> [Expr]
creductions1 :: Expr -> Expr -> (Expr, Expr, Expr) -> [Expr]
creductions1 Expr
ce Expr
e (Expr
ceq,Expr
el,Expr
er) =
  case Expr
ce Expr -> Expr -> Maybe Binds
`match` Expr
ceq of
    Maybe Binds
Nothing -> []
    Just Binds
bs -> Binds -> Expr -> (Expr, Expr) -> [Expr]
reductions1With Binds
bs Expr
e (Expr
el,Expr
er)

-- normalize is maybe a misnomer.  not necessarily convergent.
cnormalize :: Chy -> Expr -> Expr -> Expr
cnormalize :: Chy -> Expr -> Expr -> Expr
cnormalize chy :: Chy
chy@Chy{cequations :: Chy -> [(Expr, Expr, Expr)]
cequations = [(Expr, Expr, Expr)]
ceqs, unThy :: Chy -> Thy
unThy = Thy
thy} Expr
ce = Expr -> Expr
n
  where
  n :: Expr -> Expr
n Expr
e = case (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
filter (Thy -> Expr -> Expr -> Bool
canReduceTo Thy
thy Expr
e)
           ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$ ((Expr, Expr, Expr) -> [Expr]) -> [(Expr, Expr, Expr)] -> [Expr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Expr -> Expr -> (Expr, Expr, Expr) -> [Expr]
creductions1 Expr
ce Expr
e) [(Expr, Expr, Expr)]
ceqs
          [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ (Expr -> [Expr]) -> [Expr] -> [Expr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\Expr
ce' -> ((Expr, Expr, Expr) -> [Expr]) -> [(Expr, Expr, Expr)] -> [Expr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Expr -> Expr -> (Expr, Expr, Expr) -> [Expr]
creductions1 Expr
ce' Expr
e) [(Expr, Expr, Expr)]
ceqs) (Chy -> Expr -> [Expr]
listEquivalent Chy
chy Expr
ce)
          [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ (Expr -> [Expr]) -> [Expr] -> [Expr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\Expr
ce' -> ((Expr, Expr, Expr) -> [Expr]) -> [(Expr, Expr, Expr)] -> [Expr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Expr -> Expr -> (Expr, Expr, Expr) -> [Expr]
creductions1 Expr
ce' Expr
e) [(Expr, Expr, Expr)]
ceqs) (Chy -> Expr -> [Expr]
listImplied Chy
chy Expr
ce)
          [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ (Expr -> [Expr]) -> [Expr] -> [Expr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\Expr
ce' -> ((Expr, Expr, Expr) -> [Expr]) -> [(Expr, Expr, Expr)] -> [Expr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Expr -> Expr -> (Expr, Expr, Expr) -> [Expr]
creductions1 Expr
ce' Expr
e) [(Expr, Expr, Expr)]
ceqs) ((Expr -> [Expr]) -> [Expr] -> [Expr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Chy -> Expr -> [Expr]
listEquivalent Chy
chy) (Chy -> Expr -> [Expr]
listImplied Chy
chy Expr
ce)) of
          [] -> Expr
e -- already normalized
          (Expr
e':[Expr]
_) -> Expr -> Expr
n (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Thy -> Expr -> Expr
normalize Thy
thy Expr
e'
-- TODO: fix silly code structure in cnormalize!

-- Checks if two expressions are equivalent under a condition
-- using the conditional theory.
cequivalent :: Chy -> Expr -> Expr -> Expr -> Bool
cequivalent :: Chy -> Expr -> Expr -> Expr -> Bool
cequivalent Chy
chy Expr
ce Expr
e1 Expr
e2 =
  Thy -> Expr -> Expr -> Bool
equivalent (Chy -> Thy
unThy Chy
chy) (Chy -> Expr -> Expr -> Expr
cnormalize Chy
chy Expr
ce Expr
e1) (Chy -> Expr -> Expr -> Expr
cnormalize Chy
chy Expr
ce Expr
e2)

cIsInstanceOf :: Chy -> (Expr,Expr,Expr) -> (Expr,Expr,Expr) -> Bool
cIsInstanceOf :: Chy -> (Expr, Expr, Expr) -> (Expr, Expr, Expr) -> Bool
cIsInstanceOf Chy
chy (Expr
ce2,Expr
le2,Expr
re2) (Expr
ce1,Expr
le1,Expr
re1) =
  case (Expr, Expr) -> Expr
foldPair (Expr
le2,Expr
re2) Expr -> Expr -> Maybe Binds
`match` (Expr, Expr) -> Expr
foldPair (Expr
le1,Expr
re1) of
    Maybe Binds
Nothing -> Bool
False
    Just Binds
bs -> Thy -> Expr -> Expr -> Bool
equivalent (Chy -> Thy
unThy Chy
chy) (Expr
ce1 Expr -> Binds -> Expr
//- Binds
bs) Expr
ce2

-- TODO: make cinsert result independent of insertion order
cinsert :: (Expr,Expr,Expr) -> Chy -> Chy
cinsert :: (Expr, Expr, Expr) -> Chy -> Chy
cinsert ceq :: (Expr, Expr, Expr)
ceq@(Expr
ce,Expr
e1,Expr
e2) chy :: Chy
chy@Chy{cequations :: Chy -> [(Expr, Expr, Expr)]
cequations = [(Expr, Expr, Expr)]
eqs}
  | Chy -> Expr -> Expr -> Expr -> Bool
cequivalent Chy
chy Expr
ce Expr
e1 Expr
e2 = Chy
chy
  | Bool
otherwise = Chy -> Chy
cdelete (Chy -> Chy) -> Chy -> Chy
forall a b. (a -> b) -> a -> b
$ Chy
chy {cequations :: [(Expr, Expr, Expr)]
cequations = [(Expr, Expr, Expr)]
eqs [(Expr, Expr, Expr)]
-> [(Expr, Expr, Expr)] -> [(Expr, Expr, Expr)]
forall a. [a] -> [a] -> [a]
++ [(Expr, Expr, Expr)
ceq]}

cfilter :: ((Expr,Expr,Expr) -> Bool) -> Chy -> Chy
cfilter :: ((Expr, Expr, Expr) -> Bool) -> Chy -> Chy
cfilter (Expr, Expr, Expr) -> Bool
p = ([(Expr, Expr, Expr)] -> [(Expr, Expr, Expr)]) -> Chy -> Chy
updateCEquationsBy (((Expr, Expr, Expr) -> Bool)
-> [(Expr, Expr, Expr)] -> [(Expr, Expr, Expr)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Expr, Expr, Expr) -> Bool
p)

cdiscard :: ((Expr,Expr,Expr) -> Bool) -> Chy -> Chy
cdiscard :: ((Expr, Expr, Expr) -> Bool) -> Chy -> Chy
cdiscard (Expr, Expr, Expr) -> Bool
p = ((Expr, Expr, Expr) -> Bool) -> Chy -> Chy
cfilter (Bool -> Bool
not (Bool -> Bool)
-> ((Expr, Expr, Expr) -> Bool) -> (Expr, Expr, Expr) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr, Expr, Expr) -> Bool
p)

cdelete :: Chy -> Chy
cdelete :: Chy -> Chy
cdelete Chy
chy = ([(Expr, Expr, Expr)] -> [(Expr, Expr, Expr)]) -> Chy -> Chy
updateCEquationsBy [(Expr, Expr, Expr)] -> [(Expr, Expr, Expr)]
upd Chy
chy
  where
  upd :: [(Expr, Expr, Expr)] -> [(Expr, Expr, Expr)]
upd = ((Expr, Expr, Expr) -> (Expr, Expr, Expr) -> Bool)
-> [(Expr, Expr, Expr)] -> [(Expr, Expr, Expr)]
forall a. (a -> a -> Bool) -> [a] -> [a]
discardLater (Chy -> (Expr, Expr, Expr) -> (Expr, Expr, Expr) -> Bool
cIsInstanceOf Chy
chy)
      ([(Expr, Expr, Expr)] -> [(Expr, Expr, Expr)])
-> ([(Expr, Expr, Expr)] -> [(Expr, Expr, Expr)])
-> [(Expr, Expr, Expr)]
-> [(Expr, Expr, Expr)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Expr, Expr, Expr) -> [(Expr, Expr, Expr)] -> Bool)
-> [(Expr, Expr, Expr)] -> [(Expr, Expr, Expr)]
forall a. (a -> [a] -> Bool) -> [a] -> [a]
discardByOthers (\(Expr
ce,Expr
e1,Expr
e2) [(Expr, Expr, Expr)]
eqs -> Chy -> Expr -> Expr -> Expr -> Bool
cequivalent Chy
chy{cequations :: [(Expr, Expr, Expr)]
cequations = [(Expr, Expr, Expr)]
eqs} Expr
ce Expr
e1 Expr
e2)

cfinalize :: Chy -> Chy
cfinalize :: Chy -> Chy
cfinalize chy :: Chy
chy@Chy{cequations :: Chy -> [(Expr, Expr, Expr)]
cequations = [(Expr, Expr, Expr)]
ceqs} =
  ([(Expr, Expr, Expr)] -> [(Expr, Expr, Expr)]) -> Chy -> Chy
updateCEquationsBy (((Expr, Expr, Expr) -> [(Expr, Expr, Expr)])
-> [(Expr, Expr, Expr)] -> [(Expr, Expr, Expr)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Expr, Expr, Expr) -> [(Expr, Expr, Expr)]
expandSmallerConditions) Chy
chy
  where
  expandSmallerConditions :: (Expr, Expr, Expr) -> [(Expr, Expr, Expr)]
expandSmallerConditions ceq :: (Expr, Expr, Expr)
ceq@(Expr
ce,Expr
e1,Expr
e2) =
    (Expr
ce,Expr
e1,Expr
e2) (Expr, Expr, Expr) -> [(Expr, Expr, Expr)] -> [(Expr, Expr, Expr)]
forall a. a -> [a] -> [a]
: [ (Expr
ce',Chy -> Expr -> Expr -> Expr
cnormalize Chy
chy' Expr
ce' Expr
e1,Chy -> Expr -> Expr -> Expr
cnormalize Chy
chy' Expr
ce' Expr
e2)
                 | Expr
ce' <- Chy -> Expr -> [Expr]
listImplies Chy
chy Expr
ce
                 , Expr -> Int
size Expr
ce' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Expr -> Int
size Expr
ce
                 , Expr
ce' Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
/= Bool -> Expr
forall a. (Typeable a, Show a) => a -> Expr
val Bool
False
                 , let chy' :: Chy
chy' = Chy
chy{cequations :: [(Expr, Expr, Expr)]
cequations = (Expr, Expr, Expr) -> [(Expr, Expr, Expr)] -> [(Expr, Expr, Expr)]
forall a. Eq a => a -> [a] -> [a]
L.delete (Expr, Expr, Expr)
ceq [(Expr, Expr, Expr)]
ceqs}
                 , Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Chy -> Expr -> Expr -> Expr -> Bool
cequivalent Chy
chy' Expr
ce' Expr
e1 Expr
e2
                 ]

canonicalizeCEqn :: (Expr -> Expr -> Ordering) -> (Expr,Expr,Expr) -> (Expr,Expr,Expr)
canonicalizeCEqn :: (Expr -> Expr -> Ordering)
-> (Expr, Expr, Expr) -> (Expr, Expr, Expr)
canonicalizeCEqn Expr -> Expr -> Ordering
cmp = (Expr -> Expr -> Ordering)
-> [Expr] -> (Expr, Expr, Expr) -> (Expr, Expr, Expr)
canonicalizeCEqnWith Expr -> Expr -> Ordering
cmp [Expr]
preludeInstances

canonicalizeCEqnWith :: (Expr -> Expr -> Ordering) -> Instances -> (Expr,Expr,Expr) -> (Expr,Expr,Expr)
canonicalizeCEqnWith :: (Expr -> Expr -> Ordering)
-> [Expr] -> (Expr, Expr, Expr) -> (Expr, Expr, Expr)
canonicalizeCEqnWith Expr -> Expr -> Ordering
cmp [Expr]
ti = (Expr, Expr, Expr) -> (Expr, Expr, Expr)
c ((Expr, Expr, Expr) -> (Expr, Expr, Expr))
-> ((Expr, Expr, Expr) -> (Expr, Expr, Expr))
-> (Expr, Expr, Expr)
-> (Expr, Expr, Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr, Expr, Expr) -> (Expr, Expr, Expr)
forall a. (a, Expr, Expr) -> (a, Expr, Expr)
o
  where
  c :: (Expr, Expr, Expr) -> (Expr, Expr, Expr)
c (Expr
ce,Expr
e1,Expr
e2) = case (Expr -> [String]) -> Expr -> Expr
canonicalizeWith ([Expr] -> Expr -> [String]
lookupNames [Expr]
ti) (Expr
e2 Expr -> Expr -> Expr
:$ (Expr
e1 Expr -> Expr -> Expr
:$ Expr
ce)) of
                   (Expr
e2' :$ (Expr
e1' :$ Expr
ce')) -> (Expr
ce',Expr
e1',Expr
e2')
                   Expr
_ -> String -> (Expr, Expr, Expr)
forall a. HasCallStack => String -> a
error (String -> (Expr, Expr, Expr)) -> String -> (Expr, Expr, Expr)
forall a b. (a -> b) -> a -> b
$ String
"canonicalizeCEqnWith: the impossible happened,"
                             String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"this is definitely a bug, see source!"
  o :: (a, Expr, Expr) -> (a, Expr, Expr)
o (a
ce,Expr
e1,Expr
e2) | Expr
e1 Expr -> Expr -> Ordering
`cmp` Expr
e2 Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
LT = (a
ce,Expr
e2,Expr
e1)
               | Bool
otherwise         = (a
ce,Expr
e1,Expr
e2)

canonicalCEqnBy :: (Expr -> Expr -> Ordering) -> Instances -> (Expr,Expr,Expr) -> Bool
canonicalCEqnBy :: (Expr -> Expr -> Ordering) -> [Expr] -> (Expr, Expr, Expr) -> Bool
canonicalCEqnBy Expr -> Expr -> Ordering
cmp [Expr]
ti (Expr, Expr, Expr)
ceqn = (Expr -> Expr -> Ordering)
-> [Expr] -> (Expr, Expr, Expr) -> (Expr, Expr, Expr)
canonicalizeCEqnWith Expr -> Expr -> Ordering
cmp [Expr]
ti (Expr, Expr, Expr)
ceqn (Expr, Expr, Expr) -> (Expr, Expr, Expr) -> Bool
forall a. Eq a => a -> a -> Bool
== (Expr, Expr, Expr)
ceqn

canonicalCEqn :: (Expr -> Expr -> Ordering) -> (Expr,Expr,Expr) -> Bool
canonicalCEqn :: (Expr -> Expr -> Ordering) -> (Expr, Expr, Expr) -> Bool
canonicalCEqn Expr -> Expr -> Ordering
cmp = (Expr -> Expr -> Ordering) -> [Expr] -> (Expr, Expr, Expr) -> Bool
canonicalCEqnBy Expr -> Expr -> Ordering
cmp [Expr]
preludeInstances

finalCondEquations :: ((Expr,Expr,Expr) -> Bool) -> Chy -> [(Expr,Expr,Expr)]
finalCondEquations :: ((Expr, Expr, Expr) -> Bool) -> Chy -> [(Expr, Expr, Expr)]
finalCondEquations (Expr, Expr, Expr) -> Bool
shouldShow =
    ((Expr, Expr, Expr) -> (Expr, Expr, Expr) -> Ordering)
-> [(Expr, Expr, Expr)] -> [(Expr, Expr, Expr)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (TypeRep -> TypeRep -> Ordering
compareTy (TypeRep -> TypeRep -> Ordering)
-> ((Expr, Expr, Expr) -> TypeRep)
-> (Expr, Expr, Expr)
-> (Expr, Expr, Expr)
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (\(Expr
c,Expr
x,Expr
y) -> Expr -> TypeRep
typ Expr
x))
  ([(Expr, Expr, Expr)] -> [(Expr, Expr, Expr)])
-> (Chy -> [(Expr, Expr, Expr)]) -> Chy -> [(Expr, Expr, Expr)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Expr, Expr, Expr) -> Bool)
-> [(Expr, Expr, Expr)] -> [(Expr, Expr, Expr)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Expr, Expr, Expr) -> Bool
shouldShow
  ([(Expr, Expr, Expr)] -> [(Expr, Expr, Expr)])
-> (Chy -> [(Expr, Expr, Expr)]) -> Chy -> [(Expr, Expr, Expr)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Chy -> [(Expr, Expr, Expr)]
cequations
  (Chy -> [(Expr, Expr, Expr)])
-> (Chy -> Chy) -> Chy -> [(Expr, Expr, Expr)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Chy -> Chy
cfinalize