-- |
-- Module      : Test.Speculate.Reason
-- 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 of Speculate.
--
-- Equational reasoning for 'Expr's based on term rewriting.
module Test.Speculate.Reason
  ( Thy (..)
  , emptyThy
  , normalize
  , normalizeE
  , isNormal
  , isRootNormal
  , isRootNormalE
  , complete
  , equivalent
  , equivalentInstance
  , insert
  , showThy
  , printThy
  , keepUpToLength
  , keepMaxOf
  , (|==|)
  , theorize
  , theorizeBy
  , finalEquations
  , criticalPairs
  , normalizedCriticalPairs
  , append

  , okThy
  , canonicalEqn
  , canonicalRule
  , canonicalizeEqn
  , deduce
  , simplify
  , delete
  , orient
  , compose
  , collapse
  , updateRulesBy
  , updateEquationsBy
  , discardRedundantEquations
  , finalize
  , initialize
  , defaultKeep
  , doubleCheck

  , reductions1

  , dwoBy
  , (|>)
  )
where

import Test.Speculate.Expr
import Test.Speculate.Reason.Order
import Test.Speculate.Utils
import Data.Either
import Data.Function (on)
import Data.Functor ((<$>)) -- for GHC < 7.10
import Data.List (partition, (\\), sortBy, sort)
import Data.Maybe
import Data.Monoid ((<>))
import Data.Tuple (swap)
import qualified Data.List as L (insert)
import Control.Monad

type Rule = (Expr,Expr)
type Equation = (Expr,Expr)

data Thy = Thy
  { Thy -> [Rule]
rules :: [Rule]
  , Thy -> [Rule]
equations :: [Equation]
  , Thy -> Expr -> Expr -> Bool
canReduceTo :: Expr -> Expr -> Bool -- ^ should be compatible with compareE
  , Thy -> Expr -> Expr -> Ordering
compareE :: Expr -> Expr -> Ordering -- ^ total order used to "sort" equations
  , Thy -> Int
closureLimit :: Int
  , Thy -> Expr -> Bool
keepE :: Expr -> Bool
  , Thy -> [Rule]
invalid :: [Equation] -- ^ reserved for rules and equations that were later found to be invalid through testing
  }

compareEqn :: Thy -> Equation -> Equation -> Ordering
compareEqn :: Thy -> Rule -> Rule -> Ordering
compareEqn thy :: Thy
thy@Thy {compareE :: Thy -> Expr -> Expr -> Ordering
compareE = Expr -> Expr -> Ordering
cmp} (Expr
e1l,Expr
e1r) (Expr
e2l,Expr
e2r) =
  Expr
e1l Expr -> Expr -> Ordering
`cmp` Expr
e2l  Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<>  Expr
e1r Expr -> Expr -> Ordering
`cmp` Expr
e2r

-- data invariant
okThy :: Thy -> Bool
okThy :: Thy -> Bool
okThy thy :: Thy
thy@Thy {rules :: Thy -> [Rule]
rules = [Rule]
rs, equations :: Thy -> [Rule]
equations = [Rule]
eqs, canReduceTo :: Thy -> Expr -> Expr -> Bool
canReduceTo = Expr -> Expr -> Bool
(->-), keepE :: Thy -> Expr -> Bool
keepE = Expr -> Bool
keep, compareE :: Thy -> Expr -> Expr -> Ordering
compareE = Expr -> Expr -> Ordering
cmp} =
     (Rule -> Rule -> Bool) -> [Rule] -> Bool
forall a. (a -> a -> Bool) -> [a] -> Bool
orderedBy Rule -> Rule -> Bool
(<) [Rule]
rs
  Bool -> Bool -> Bool
&& (Rule -> Rule -> Bool) -> [Rule] -> Bool
forall a. (a -> a -> Bool) -> [a] -> Bool
orderedBy Rule -> Rule -> Bool
(<) [Rule]
eqs
  Bool -> Bool -> Bool
&& (Rule -> Bool) -> [Rule] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Expr -> Expr -> Bool) -> Rule -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Expr -> Expr -> Bool
(->-)) [Rule]
rs
  Bool -> Bool -> Bool
&& (Rule -> Bool) -> [Rule] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
/= Ordering
LT) (Ordering -> Bool) -> (Rule -> Ordering) -> Rule -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Expr -> Ordering) -> Rule -> Ordering
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Expr -> Expr -> Ordering
cmp) [Rule]
eqs
  Bool -> Bool -> Bool
&& (Rule -> Bool) -> [Rule] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Expr -> Expr -> Bool) -> Rule -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (TypeRep -> TypeRep -> Bool
forall a. Eq a => a -> a -> Bool
(==) (TypeRep -> TypeRep -> Bool)
-> (Expr -> TypeRep) -> Expr -> Expr -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Expr -> TypeRep
typ)) ([Rule]
rs[Rule] -> [Rule] -> [Rule]
forall a. [a] -> [a] -> [a]
++[Rule]
eqs)
  Bool -> Bool -> Bool
&& (Rule -> Bool) -> [Rule] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Thy -> Rule -> Bool
canonicalEqn Thy
thy) [Rule]
eqs
  Bool -> Bool -> Bool
&& (Rule -> Bool) -> [Rule] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Rule -> Bool
canonicalRule [Rule]
rs
-- && canonicalizeThy thy == thy -- (uneeded, follows from above)
  Bool -> Bool -> Bool
&& (Rule -> Bool) -> [Rule] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Rule -> Bool
keepEqn ([Rule]
rs[Rule] -> [Rule] -> [Rule]
forall a. [a] -> [a] -> [a]
++[Rule]
eqs)
  where
  Rule
e1 < :: Rule -> Rule -> Bool
< Rule
e2 = Thy -> Rule -> Rule -> Ordering
compareEqn Thy
thy Rule
e1 Rule
e2 Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
LT
  keepEqn :: Rule -> Bool
keepEqn (Expr
e1,Expr
e2) = Expr -> Bool
keep Expr
e1 Bool -> Bool -> Bool
&& Expr -> Bool
keep Expr
e2

updateRulesBy :: ([Rule] -> [Rule]) -> Thy -> Thy
updateRulesBy :: ([Rule] -> [Rule]) -> Thy -> Thy
updateRulesBy [Rule] -> [Rule]
f thy :: Thy
thy@Thy {rules :: Thy -> [Rule]
rules = [Rule]
rs} = Thy
thy {rules :: [Rule]
rules = [Rule] -> [Rule]
f [Rule]
rs}

updateEquationsBy :: ([Equation] -> [Equation]) -> Thy -> Thy
updateEquationsBy :: ([Rule] -> [Rule]) -> Thy -> Thy
updateEquationsBy [Rule] -> [Rule]
f thy :: Thy
thy@Thy {equations :: Thy -> [Rule]
equations = [Rule]
es} = Thy
thy {equations :: [Rule]
equations = [Rule] -> [Rule]
f [Rule]
es}

mapRules :: (Rule -> Rule) -> Thy -> Thy
mapRules :: (Rule -> Rule) -> Thy -> Thy
mapRules = ([Rule] -> [Rule]) -> Thy -> Thy
updateRulesBy (([Rule] -> [Rule]) -> Thy -> Thy)
-> ((Rule -> Rule) -> [Rule] -> [Rule])
-> (Rule -> Rule)
-> Thy
-> Thy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rule -> Rule) -> [Rule] -> [Rule]
forall a b. (a -> b) -> [a] -> [b]
map

mapEquations :: (Equation -> Equation) -> Thy -> Thy
mapEquations :: (Rule -> Rule) -> Thy -> Thy
mapEquations = ([Rule] -> [Rule]) -> Thy -> Thy
updateEquationsBy (([Rule] -> [Rule]) -> Thy -> Thy)
-> ((Rule -> Rule) -> [Rule] -> [Rule])
-> (Rule -> Rule)
-> Thy
-> Thy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rule -> Rule) -> [Rule] -> [Rule]
forall a b. (a -> b) -> [a] -> [b]
map

-- | This instance is as efficient as it gets, but, this function will not
--   detect equality when rules and equations are in a different order (or
--   repeated).  See '|==|'.
instance Eq Thy where
  Thy
t == :: Thy -> Thy -> Bool
== Thy
u = Thy -> [Rule]
rules Thy
t [Rule] -> [Rule] -> Bool
forall a. Eq a => a -> a -> Bool
== Thy -> [Rule]
rules Thy
u
        Bool -> Bool -> Bool
&& Thy -> [Rule]
equations Thy
t [Rule] -> [Rule] -> Bool
forall a. Eq a => a -> a -> Bool
== Thy -> [Rule]
equations Thy
u
        Bool -> Bool -> Bool
&& Thy -> Int
closureLimit Thy
t Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Thy -> Int
closureLimit Thy
u -- useful when self-speculating

(|==|) :: Thy -> Thy -> Bool
|==| :: Thy -> Thy -> Bool
(|==|) Thy
t Thy
u = Thy -> [Rule]
rules Thy
t [Rule] -> [Rule] -> Bool
forall a. Ord a => [a] -> [a] -> Bool
=|= Thy -> [Rule]
rules Thy
u
          Bool -> Bool -> Bool
&& (Rule -> Rule) -> [Rule] -> [Rule]
forall a b. (a -> b) -> [a] -> [b]
map Rule -> Rule
forall b. Ord b => (b, b) -> (b, b)
orient (Thy -> [Rule]
equations Thy
t) [Rule] -> [Rule] -> Bool
forall a. Ord a => [a] -> [a] -> Bool
=|= (Rule -> Rule) -> [Rule] -> [Rule]
forall a b. (a -> b) -> [a] -> [b]
map Rule -> Rule
forall b. Ord b => (b, b) -> (b, b)
orient (Thy -> [Rule]
equations Thy
u)
  where
  [a]
xs =|= :: [a] -> [a] -> Bool
=|= [a]
ys = [a] -> [a]
forall a. Ord a => [a] -> [a]
nubSort [a]
xs [a] -> [a] -> Bool
forall a. Eq a => a -> a -> Bool
== [a] -> [a]
forall a. Ord a => [a] -> [a]
nubSort [a]
ys
  orient :: (b, b) -> (b, b)
orient (b
e1,b
e2) | b
e1 b -> b -> Bool
forall a. Ord a => a -> a -> Bool
< b
e2   = (b
e2,b
e1)
                 | Bool
otherwise = (b
e1,b
e2)
infix 4 |==|

emptyThy :: Thy
emptyThy :: Thy
emptyThy = Thy :: [Rule]
-> [Rule]
-> (Expr -> Expr -> Bool)
-> (Expr -> Expr -> Ordering)
-> Int
-> (Expr -> Bool)
-> [Rule]
-> Thy
Thy
         { rules :: [Rule]
rules = []
         , equations :: [Rule]
equations = []
         , canReduceTo :: Expr -> Expr -> Bool
canReduceTo = Expr -> Expr -> Bool
(|>)
         , compareE :: Expr -> Expr -> Ordering
compareE = Expr -> Expr -> Ordering
forall a. Ord a => a -> a -> Ordering
compare
         , closureLimit :: Int
closureLimit = Int
0
         , keepE :: Expr -> Bool
keepE = Bool -> Expr -> Bool
forall a b. a -> b -> a
const Bool
True
         , invalid :: [Rule]
invalid = []
         }

ruleFilter :: Thy -> [Rule] -> [Rule]
ruleFilter :: Thy -> [Rule] -> [Rule]
ruleFilter Thy {keepE :: Thy -> Expr -> Bool
keepE = Expr -> Bool
keep} = (Rule -> Bool) -> [Rule] -> [Rule]
forall a. (a -> Bool) -> [a] -> [a]
filter Rule -> Bool
keepR
  where
  keepR :: Rule -> Bool
keepR (Expr
e1,Expr
e2) = Expr -> Bool
keep Expr
e1 Bool -> Bool -> Bool
&& Expr -> Bool
keep Expr
e2

keepUpToLength :: Int -> Expr -> Bool
keepUpToLength :: Int -> Expr -> Bool
keepUpToLength Int
limit Expr
e = Expr -> Int
size Expr
e Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
limit

keepMaxOf :: [Equation] -> Expr -> Bool
keepMaxOf :: [Rule] -> Expr -> Bool
keepMaxOf = Int -> Expr -> Bool
keepUpToLength (Int -> Expr -> Bool) -> ([Rule] -> Int) -> [Rule] -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (Int -> Int) -> ([Rule] -> Int) -> [Rule] -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Int] -> Int) -> ([Rule] -> [Int]) -> [Rule] -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int
0Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
:) ([Int] -> [Int]) -> ([Rule] -> [Int]) -> [Rule] -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Int) -> [Expr] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> Int
size ([Expr] -> [Int]) -> ([Rule] -> [Expr]) -> [Rule] -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Rule] -> [Expr]
forall a. [(a, a)] -> [a]
catPairs

normalize :: Thy -> Expr -> Expr
normalize :: Thy -> Expr -> Expr
normalize Thy {rules :: Thy -> [Rule]
rules = [Rule]
rs} = Expr -> Expr
n
  where
  n :: Expr -> Expr
n Expr
e = case (Rule -> [Expr]) -> [Rule] -> [Expr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Expr
e Expr -> Rule -> [Expr]
`reductions1`) [Rule]
rs of
          []     -> Expr
e -- already normalized
          (Expr
e':[Expr]
_) -> Expr -> Expr
n Expr
e'

-- normalize by rules and equations
normalizeE :: Thy -> Expr -> Expr
normalizeE :: Thy -> Expr -> Expr
normalizeE thy :: Thy
thy@(Thy {equations :: Thy -> [Rule]
equations = [Rule]
eqs, canReduceTo :: Thy -> Expr -> Expr -> Bool
canReduceTo = Expr -> Expr -> Bool
(->-)})  =  Expr -> Expr
n1
  where
  n1 :: Expr -> Expr
n1  =  Expr -> Expr
n2 (Expr -> Expr) -> (Expr -> Expr) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Thy -> Expr -> Expr
normalize Thy
thy
  n2 :: Expr -> Expr
n2 Expr
e = case (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
filter (Expr
e Expr -> Expr -> Bool
->-) ((Rule -> [Expr]) -> [Rule] -> [Expr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Expr
e Expr -> Rule -> [Expr]
`reductions1`) ([Rule] -> [Expr]) -> [Rule] -> [Expr]
forall a b. (a -> b) -> a -> b
$ [Rule]
eqs [Rule] -> [Rule] -> [Rule]
forall a. [a] -> [a] -> [a]
++ (Rule -> Rule) -> [Rule] -> [Rule]
forall a b. (a -> b) -> [a] -> [b]
map Rule -> Rule
forall a b. (a, b) -> (b, a)
swap [Rule]
eqs) of
         []     -> Expr
e -- already normalized
         (Expr
e':[Expr]
_) -> Expr -> Expr
n1 Expr
e'

isNormal :: Thy -> Expr -> Bool
isNormal :: Thy -> Expr -> Bool
isNormal Thy
thy Expr
e = Thy -> Expr -> Expr
normalizeE Thy
thy Expr
e Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
e

isRootNormal :: Thy -> Expr -> Bool
isRootNormal :: Thy -> Expr -> Bool
isRootNormal Thy
thy Expr
e  =  (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
none (Expr
e Expr -> Expr -> Bool
`isInstanceOf`) ([Expr] -> Bool) -> [Expr] -> Bool
forall a b. (a -> b) -> a -> b
$ (Rule -> Expr) -> [Rule] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Rule -> Expr
forall a b. (a, b) -> a
fst (Thy -> [Rule]
rules Thy
thy)
  where
  none :: (a -> Bool) -> t a -> Bool
none a -> Bool
p  =  Bool -> Bool
not (Bool -> Bool) -> (t a -> Bool) -> t a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Bool) -> t a -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any a -> Bool
p

isRootNormalE :: Thy -> Expr -> Bool
isRootNormalE :: Thy -> Expr -> Bool
isRootNormalE Thy
thy Expr
e  =  Thy -> Expr -> Bool
isRootNormal Thy
thy Expr
e
                    Bool -> Bool -> Bool
&&  [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ((Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
filter (Expr
e Expr -> Expr -> Bool
->-) ([Expr] -> [Expr]) -> ([Rule] -> [Expr]) -> [Rule] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rule -> Maybe Expr) -> [Rule] -> [Expr]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Expr -> Rule -> Maybe Expr
reduceRoot Expr
e) ([Rule] -> [Expr]) -> [Rule] -> [Expr]
forall a b. (a -> b) -> a -> b
$ Thy -> [Rule]
equations Thy
thy [Rule] -> [Rule] -> [Rule]
forall a. [a] -> [a] -> [a]
++ (Rule -> Rule) -> [Rule] -> [Rule]
forall a b. (a -> b) -> [a] -> [b]
map Rule -> Rule
forall a b. (a, b) -> (b, a)
swap (Thy -> [Rule]
equations Thy
thy))
  where
  ->- :: Expr -> Expr -> Bool
(->-)  =  Thy -> Expr -> Expr -> Bool
canReduceTo Thy
thy
  reduceRoot :: Expr -> Rule -> Maybe Expr
reduceRoot Expr
e (Expr
e1,Expr
e2) = (Expr
e2 Expr -> [Rule] -> Expr
//-) ([Rule] -> Expr) -> Maybe [Rule] -> Maybe Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr
e Expr -> Expr -> Maybe [Rule]
`match` Expr
e1)

reduceRoot :: Expr -> Rule -> Maybe Expr
reduceRoot :: Expr -> Rule -> Maybe Expr
reduceRoot Expr
e (Expr
e1,Expr
e2) = (Expr
e2 Expr -> [Rule] -> Expr
//-) ([Rule] -> Expr) -> Maybe [Rule] -> Maybe Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr
e Expr -> Expr -> Maybe [Rule]
`match` Expr
e1)

-- Lists all reductions by one rule, note that reductions may be repeated.
reductions1 :: Expr -> Rule -> [Expr]
reductions1 :: Expr -> Rule -> [Expr]
reductions1 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
reductions1 e :: Expr
e@(Expr
e1 :$ Expr
e2) Rule
r = Maybe Expr -> [Expr]
forall a. Maybe a -> [a]
maybeToList (Expr
e Expr -> Rule -> Maybe Expr
`reduceRoot` Rule
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) (Expr -> Rule -> [Expr]
reductions1 Expr
e1 Rule
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
:$) (Expr -> Rule -> [Expr]
reductions1 Expr
e2 Rule
r)
reductions1 Expr
e Rule
r = Maybe Expr -> [Expr]
forall a. Maybe a -> [a]
maybeToList (Expr
e Expr -> Rule -> Maybe Expr
`reduceRoot` Rule
r)

-- as defined by Martin & Nipkow in "Ordered Rewriting and Confluence" on 1990
-- this definition is sound, but incomplete (some groundJoinable pairs won't be
-- detected).
groundJoinable :: Thy -> Expr -> Expr -> Bool
groundJoinable :: Thy -> Expr -> Expr -> Bool
groundJoinable thy :: Thy
thy@Thy{equations :: Thy -> [Rule]
equations = [Rule]
eqs} Expr
e1 Expr
e2 =
     Expr
e1 Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
e2
  Bool -> Bool -> Bool
|| (Rule -> Bool) -> [Rule] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\(Expr
el,Expr
er) -> Bool
-> ([Rule] -> [Rule] -> Bool)
-> Maybe [Rule]
-> Maybe [Rule]
-> Bool
forall c a b. c -> (a -> b -> c) -> Maybe a -> Maybe b -> c
maybe2 Bool
False ([Rule] -> [Rule] -> Bool
forall a. Eq a => a -> a -> Bool
(==) ([Rule] -> [Rule] -> Bool)
-> ([Rule] -> [Rule]) -> [Rule] -> [Rule] -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` [Rule] -> [Rule]
forall a. Ord a => [a] -> [a]
sort) (Expr
e1 Expr -> Expr -> Maybe [Rule]
`match` Expr
el) (Expr
e2 Expr -> Expr -> Maybe [Rule]
`match` Expr
er)) ([Rule]
eqs [Rule] -> [Rule] -> [Rule]
forall a. [a] -> [a] -> [a]
++ (Rule -> Rule) -> [Rule] -> [Rule]
forall a b. (a -> b) -> [a] -> [b]
map Rule -> Rule
forall a b. (a, b) -> (b, a)
swap [Rule]
eqs)
  Bool -> Bool -> Bool
|| (Expr
f Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
g Bool -> Bool -> Bool
&& [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((Expr -> Expr -> Bool) -> [Expr] -> [Expr] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Thy -> Expr -> Expr -> Bool
groundJoinable Thy
thy) [Expr]
xs [Expr]
ys))
  where
  (Expr
f:[Expr]
xs) = Expr -> [Expr]
unfoldApp Expr
e1
  (Expr
g:[Expr]
ys) = Expr -> [Expr]
unfoldApp Expr
e2
-- TODO: one case missing on groundJoinable
-- I need a function f, such that:
-- f (x) = [x]
-- f (xy) = [xx, xy, yx]
-- f (xyz) = [xxx, xxy, xyx, xyy, xyz, xzy, yxx, yxy, yyx, yzx, zxy, zyx]
-- f (xyzw) = [ xxxx, xxxy, xxyx, xxyy, xxyz, xxzy
--            , xyxx, xyxy, xyyx, xyyy, xyyz, xyzx, xyzy, xyzz, xyzw, xywz
--            , xzxy, xzyx, xzyy, xzyz, xzyw, xzzy, xzwx, xzwy,
--            , xwyz, ... ]

normalizedCriticalPairs :: Thy -> [(Expr,Expr)]
normalizedCriticalPairs :: Thy -> [Rule]
normalizedCriticalPairs Thy
thy = (Rule -> Rule -> Ordering) -> [Rule] -> [Rule]
forall a. (a -> a -> Ordering) -> [a] -> [a]
nubSortBy (Thy -> Rule -> Rule -> Ordering
compareEqn Thy
thy)
                            ([Rule] -> [Rule]) -> ([Rule] -> [Rule]) -> [Rule] -> [Rule]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rule -> Rule) -> [Rule] -> [Rule]
forall a b. (a -> b) -> [a] -> [b]
map (Thy -> Rule -> Rule
canonicalizeEqn Thy
thy)
                            ([Rule] -> [Rule]) -> ([Rule] -> [Rule]) -> [Rule] -> [Rule]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rule -> Bool) -> [Rule] -> [Rule]
forall a. (a -> Bool) -> [a] -> [a]
discard ((Expr -> Expr -> Bool) -> Rule -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((Expr -> Expr -> Bool) -> Rule -> Bool)
-> (Expr -> Expr -> Bool) -> Rule -> Bool
forall a b. (a -> b) -> a -> b
$ Thy -> Expr -> Expr -> Bool
groundJoinable Thy
thy)
                            ([Rule] -> [Rule]) -> ([Rule] -> [Rule]) -> [Rule] -> [Rule]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rule -> Bool) -> [Rule] -> [Rule]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Expr -> Expr -> Bool) -> Rule -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
(/=))
                            ([Rule] -> [Rule]) -> ([Rule] -> [Rule]) -> [Rule] -> [Rule]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rule -> Rule) -> [Rule] -> [Rule]
forall a b. (a -> b) -> [a] -> [b]
map (Thy -> Expr -> Expr
normalize Thy
thy (Expr -> Expr) -> (Expr -> Expr) -> Rule -> Rule
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
*** Thy -> Expr -> Expr
normalize Thy
thy)
                            ([Rule] -> [Rule]) -> [Rule] -> [Rule]
forall a b. (a -> b) -> a -> b
$ Thy -> [Rule]
criticalPairs Thy
thy

criticalPairs :: Thy -> [(Expr,Expr)]
criticalPairs :: Thy -> [Rule]
criticalPairs thy :: Thy
thy@Thy{rules :: Thy -> [Rule]
rules = [Rule]
rs}  =
  (Rule -> Rule -> Ordering) -> [[Rule]] -> [Rule]
forall a. Ord a => (a -> a -> Ordering) -> [[a]] -> [a]
nubMergesBy Rule -> Rule -> Ordering
compareEqnQuickly [Rule
r Rule -> Rule -> [Rule]
`criticalPairsWith` Rule
s | Rule
r <- [Rule]
rs, Rule
s <- [Rule]
rs]
  where
  criticalPairsWith :: Rule -> Rule -> [(Expr,Expr)]
  r1 :: Rule
r1@(Expr
e1,Expr
_) criticalPairsWith :: Rule -> Rule -> [Rule]
`criticalPairsWith` r2 :: Rule
r2@(Expr
e2,Expr
_) =
      (Rule -> Rule -> Ordering) -> [Rule] -> [Rule]
forall a. (a -> a -> Ordering) -> [a] -> [a]
nubSortBy Rule -> Rule -> Ordering
compareEqnQuickly
    ([Rule] -> [Rule]) -> ([Expr] -> [Rule]) -> [Expr] -> [Rule]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rule -> Rule) -> [Rule] -> [Rule]
forall a b. (a -> b) -> [a] -> [b]
map Rule -> Rule
sortuple
    ([Rule] -> [Rule]) -> ([Expr] -> [Rule]) -> [Expr] -> [Rule]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rule -> Bool) -> [Rule] -> [Rule]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Expr -> Expr -> Bool) -> Rule -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
(/=))
    ([Rule] -> [Rule]) -> ([Expr] -> [Rule]) -> [Expr] -> [Rule]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> [Rule]) -> [Expr] -> [Rule]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\Expr
e -> (Expr
e Expr -> Rule -> [Expr]
`reductions1` Rule
r1) [Expr] -> [Expr] -> [Rule]
forall a b. [a] -> [b] -> [(a, b)]
** (Expr
e Expr -> Rule -> [Expr]
`reductions1` Rule
r2))
    ([Expr] -> [Rule]) -> ([Expr] -> [Expr]) -> [Expr] -> [Rule]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Expr -> Ordering) -> [Expr] -> [Expr]
forall a. (a -> a -> Ordering) -> [a] -> [a]
nubSortBy Expr -> Expr -> Ordering
compareQuickly
    ([Expr] -> [Rule]) -> [Expr] -> [Rule]
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> [Expr]
overlaps Expr
e1 Expr
e2
  [a]
xs ** :: [a] -> [b] -> [(a, b)]
** [b]
ys = [(a
x,b
y) | a
x <- [a]
xs, b
y <- [b]
ys]
  sortuple :: Rule -> Rule
sortuple (Expr
x,Expr
y) | Expr
x Expr -> Expr -> Bool
< Expr
y     = (Expr
y,Expr
x)
                 | Bool
otherwise = (Expr
x,Expr
y)
  compareEqnQuickly :: Rule -> Rule -> Ordering
compareEqnQuickly = Expr -> Expr -> Ordering
compareQuickly (Expr -> Expr -> Ordering)
-> (Rule -> Expr) -> Rule -> Rule -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Rule -> Expr
foldPair
  (<) :: Expr -> Expr -> Bool
  Expr
e1 < :: Expr -> Expr -> Bool
< Expr
e2 = Expr
e1 Expr -> Expr -> Ordering
`compareQuickly` Expr
e2 Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
LT

-- Warning: will have to also be applied in reverse to get all overlaps.
--
-- canonicalization here is needed for the nub
overlaps :: Expr -> Expr -> [Expr]
overlaps :: Expr -> Expr -> [Expr]
overlaps Expr
e1 Expr
e2 = [Expr] -> [Expr]
forall a. a -> a
id -- nubSort
               ([Expr] -> [Expr]) -> ([[Rule]] -> [Expr]) -> [[Rule]] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Rule] -> Expr) -> [[Rule]] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Expr -> Expr
canonicalize (Expr -> Expr) -> ([Rule] -> Expr) -> [Rule] -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr
e2' Expr -> [Rule] -> Expr
//-))
               ([[Rule]] -> [Expr]) -> [[Rule]] -> [Expr]
forall a b. (a -> b) -> a -> b
$ (Expr
e1' Expr -> Expr -> Maybe [Rule]
`unification`) (Expr -> Maybe [Rule]) -> [Expr] -> [[Rule]]
forall a b. (a -> Maybe b) -> [a] -> [b]
`mapMaybe` Expr -> [Expr]
nonVarSubexprs Expr
e2'
  where
  nonVarSubexprs :: Expr -> [Expr]
nonVarSubexprs = (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
discard Expr -> Bool
isVar ([Expr] -> [Expr]) -> (Expr -> [Expr]) -> Expr -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
nubSubexprs
  e1' :: Expr
e1' = (String -> String) -> Expr -> Expr
renameVarsBy (String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"1") Expr
e1
  e2' :: Expr
e2' = (String -> String) -> Expr -> Expr
renameVarsBy (String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"2") Expr
e2

equivalent :: Thy -> Expr -> Expr -> Bool
equivalent :: Thy -> Expr -> Expr -> Bool
equivalent Thy
thy Expr
e1 Expr
e2 = Expr
e1' Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
e2'
                    Bool -> Bool -> Bool
|| [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [ Thy -> Expr -> Expr
normalizeE Thy
thy Expr
e1'' Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Thy -> Expr -> Expr
normalizeE Thy
thy Expr
e2''
                          | Expr
e1'' <- Thy -> Expr -> [Expr]
closure Thy
thy Expr
e1'
                          , Expr
e2'' <- Thy -> Expr -> [Expr]
closure Thy
thy Expr
e2'
                          ]
  where
  e1' :: Expr
e1' = Thy -> Expr -> Expr
normalizeE Thy
thy Expr
e1
  e2' :: Expr
e2' = Thy -> Expr -> Expr
normalizeE Thy
thy Expr
e2

equivalentInstance :: Thy -> Expr -> Expr -> Bool
equivalentInstance :: Thy -> Expr -> Expr -> Bool
equivalentInstance Thy
thy Expr
e1 Expr
e2 = Expr
e1' Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
e2'
                            Bool -> Bool -> Bool
|| [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [ Thy -> Expr -> Expr
normalizeE Thy
thy Expr
e1'' Expr -> Expr -> Bool
`isInstanceOf` Thy -> Expr -> Expr
normalizeE Thy
thy Expr
e2''
                                  | Expr
e1'' <- Thy -> Expr -> [Expr]
closure Thy
thy Expr
e1'
                                  , Expr
e2'' <- Thy -> Expr -> [Expr]
closure Thy
thy Expr
e2'
                                  ]
  where
  e1' :: Expr
e1' = Thy -> Expr -> Expr
normalizeE Thy
thy Expr
e1
  e2' :: Expr
e2' = Thy -> Expr -> Expr
normalizeE Thy
thy Expr
e2

closure :: Thy -> Expr -> [Expr]
closure :: Thy -> Expr -> [Expr]
closure Thy
thy Expr
e = Int
-> ([Expr] -> [Expr] -> Bool)
-> ([Expr] -> [Expr])
-> [Expr]
-> [Expr]
forall a. Int -> (a -> a -> Bool) -> (a -> a) -> a -> a
iterateUntilLimit (Thy -> Int
closureLimit Thy
thy) [Expr] -> [Expr] -> Bool
forall a. Eq a => a -> a -> Bool
(==) [Expr] -> [Expr]
step [Thy -> Expr -> Expr
normalizeE Thy
thy Expr
e]
  where
  eqs :: [Rule]
eqs = Thy -> [Rule]
equations Thy
thy
  step :: [Expr] -> [Expr]
step = (Expr -> [Expr]) -> [Expr] -> [Expr]
forall b a. Ord b => (a -> [b]) -> [a] -> [b]
nubMergeMap Expr -> [Expr]
reductionsEqs1
  reductionsEqs1 :: Expr -> [Expr]
reductionsEqs1 Expr
e = Expr
e Expr -> [Expr] -> [Expr]
forall a. Ord a => a -> [a] -> [a]
`L.insert` (Rule -> [Expr]) -> [Rule] -> [Expr]
forall b a. Ord b => (a -> [b]) -> [a] -> [b]
nubMergeMap (Expr -> Rule -> [Expr]
reductions1 Expr
e) ([Rule]
eqs [Rule] -> [Rule] -> [Rule]
forall a. [a] -> [a] -> [a]
++ (Rule -> Rule) -> [Rule] -> [Rule]
forall a b. (a -> b) -> [a] -> [b]
map Rule -> Rule
forall a b. (a, b) -> (b, a)
swap [Rule]
eqs)

insert :: Equation -> Thy -> Thy
insert :: Rule -> Thy -> Thy
insert (Expr
e1,Expr
e2) Thy
thy
  | Thy -> Expr -> Expr
normalize Thy
thy Expr
e1 Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Thy -> Expr -> Expr
normalize Thy
thy Expr
e2 = Thy
thy
  | Bool
otherwise = Thy -> Thy
complete (Thy -> Thy) -> Thy -> Thy
forall a b. (a -> b) -> a -> b
$ ([Rule] -> [Rule]) -> Thy -> Thy
updateEquationsBy (Thy -> Rule -> Rule
canonicalizeEqn Thy
thy (Expr
e1,Expr
e2) Rule -> [Rule] -> [Rule]
forall a. Ord a => a -> [a] -> [a]
`L.insert`) Thy
thy

append :: Thy -> [Equation] -> Thy
append :: Thy -> [Rule] -> Thy
append Thy
thy [Rule]
eqs = ([Rule] -> [Rule]) -> Thy -> Thy
updateEquationsBy ([Rule] -> [Rule]
forall a. Ord a => [a] -> [a]
nubSort ([Rule] -> [Rule]) -> ([Rule] -> [Rule]) -> [Rule] -> [Rule]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Rule] -> [Rule] -> [Rule]
forall a. [a] -> [a] -> [a]
++ [Rule]
eqs')) Thy
thy
  where
  eqs' :: [Rule]
eqs' = [ Thy -> Rule -> Rule
canonicalizeEqn Thy
thy (Expr
e1',Expr
e2')
         | (Expr
e1,Expr
e2) <- [Rule]
eqs
         , let e1' :: Expr
e1' = Thy -> Expr -> Expr
normalize Thy
thy Expr
e1
         , let e2' :: Expr
e2' = Thy -> Expr -> Expr
normalize Thy
thy Expr
e2
         , Expr
e1' Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
/= Expr
e2'
         ]

complete :: Thy -> Thy
complete :: Thy -> Thy
complete = (Thy -> Thy -> Bool) -> (Thy -> Thy) -> Thy -> Thy
forall a. (a -> a -> Bool) -> (a -> a) -> a -> a
iterateUntil Thy -> Thy -> Bool
forall a. Eq a => a -> a -> Bool
(==)
         ((Thy -> Thy) -> Thy -> Thy) -> (Thy -> Thy) -> Thy -> Thy
forall a b. (a -> b) -> a -> b
$ Thy -> Thy
deduce
         (Thy -> Thy) -> (Thy -> Thy) -> Thy -> Thy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Thy -> Thy
collapse
         (Thy -> Thy) -> (Thy -> Thy) -> Thy -> Thy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Thy -> Thy
compose
         (Thy -> Thy) -> (Thy -> Thy) -> Thy -> Thy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Thy -> Thy
orient
         (Thy -> Thy) -> (Thy -> Thy) -> Thy -> Thy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Thy -> Thy
deleteGroundJoinable
         (Thy -> Thy) -> (Thy -> Thy) -> Thy -> Thy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Thy -> Thy
delete
         (Thy -> Thy) -> (Thy -> Thy) -> Thy -> Thy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Thy -> Thy
simplify
-- TODO: (?) on complete, each step should also return a boolean indicating
--           whether the rule was applied succesfully.  (low priority)

completeVerbose :: Thy -> IO Thy
completeVerbose :: Thy -> IO Thy
completeVerbose Thy
thy0 = do
  let {thy1 :: Thy
thy1 = Thy -> Thy
canonicalizeThy Thy
thy0}; Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Thy
thy1 Thy -> Thy -> Bool
forall a. Eq a => a -> a -> Bool
== Thy
thy0) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Thy -> IO ()
pr String
"canonThy" Thy
thy1
  let {thy2 :: Thy
thy2 = Thy -> Thy
deduce          Thy
thy1}; Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Thy
thy2 Thy -> Thy -> Bool
forall a. Eq a => a -> a -> Bool
== Thy
thy1) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Thy -> IO ()
pr String
"deduce"   Thy
thy2
  let {thy3 :: Thy
thy3 = Thy -> Thy
simplify        Thy
thy2}; Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Thy
thy3 Thy -> Thy -> Bool
forall a. Eq a => a -> a -> Bool
== Thy
thy2) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Thy -> IO ()
pr String
"simplify" Thy
thy3
  let {thy4 :: Thy
thy4 = Thy -> Thy
delete          Thy
thy3}; Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Thy
thy4 Thy -> Thy -> Bool
forall a. Eq a => a -> a -> Bool
== Thy
thy3) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Thy -> IO ()
pr String
"delete"   Thy
thy4
  let {thy5 :: Thy
thy5 = Thy -> Thy
orient          Thy
thy4}; Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Thy
thy5 Thy -> Thy -> Bool
forall a. Eq a => a -> a -> Bool
== Thy
thy4) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Thy -> IO ()
pr String
"orient"   Thy
thy5
  let {thy6 :: Thy
thy6 = Thy -> Thy
compose         Thy
thy5}; Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Thy
thy6 Thy -> Thy -> Bool
forall a. Eq a => a -> a -> Bool
== Thy
thy5) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Thy -> IO ()
pr String
"compose"  Thy
thy6
  let {thy7 :: Thy
thy7 = Thy -> Thy
collapse        Thy
thy6}; Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Thy
thy7 Thy -> Thy -> Bool
forall a. Eq a => a -> a -> Bool
== Thy
thy6) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Thy -> IO ()
pr String
"collapse" Thy
thy7
  -- threadDelay $ 100 * 1000 -- 100 milisecond delay
  if Thy
thy7 Thy -> Thy -> Bool
forall a. Eq a => a -> a -> Bool
/= Thy
thy0  then Thy -> IO Thy
completeVerbose Thy
thy7
                   else Thy -> IO Thy
forall (m :: * -> *) a. Monad m => a -> m a
return          Thy
thy7
  where
  pr :: String -> Thy -> IO ()
pr String
n = (String -> IO ()
putStrLn (String
":: After " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
":") IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>)
       (IO () -> IO ()) -> (Thy -> IO ()) -> Thy -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn (String -> IO ()) -> (Thy -> String) -> Thy -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Thy -> String
showThy


deduce :: Thy -> Thy
deduce :: Thy -> Thy
deduce Thy
thy = ([Rule] -> [Rule]) -> Thy -> Thy
updateEquationsBy ([Rule] -> [Rule] -> [Rule]
forall a. Ord a => [a] -> [a] -> [a]
+++ Thy -> [Rule] -> [Rule]
ruleFilter Thy
thy (Thy -> [Rule]
normalizedCriticalPairs Thy
thy)) Thy
thy

orient :: Thy -> Thy
orient :: Thy -> Thy
orient thy :: Thy
thy@Thy {equations :: Thy -> [Rule]
equations = [Rule]
eqs, rules :: Thy -> [Rule]
rules = [Rule]
rs, canReduceTo :: Thy -> Expr -> Expr -> Bool
canReduceTo = Expr -> Expr -> Bool
(>)} =
  Thy
thy {equations :: [Rule]
equations = [Rule]
eqs', rules :: [Rule]
rules = [Rule]
rs [Rule] -> [Rule] -> [Rule]
forall a. Ord a => [a] -> [a] -> [a]
+++ [Rule] -> [Rule]
forall a. Ord a => [a] -> [a]
nubSort ((Rule -> Rule) -> [Rule] -> [Rule]
forall a b. (a -> b) -> [a] -> [b]
map Rule -> Rule
canonicalizeRule [Rule]
rs')}
  where
  ([Rule]
eqs',[Rule]
rs') = [Either Rule Rule] -> ([Rule], [Rule])
forall a b. [Either a b] -> ([a], [b])
partitionEithers ([Either Rule Rule] -> ([Rule], [Rule]))
-> ([Rule] -> [Either Rule Rule]) -> [Rule] -> ([Rule], [Rule])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rule -> Either Rule Rule) -> [Rule] -> [Either Rule Rule]
forall a b. (a -> b) -> [a] -> [b]
map Rule -> Either Rule Rule
o ([Rule] -> ([Rule], [Rule])) -> [Rule] -> ([Rule], [Rule])
forall a b. (a -> b) -> a -> b
$ Thy -> [Rule] -> [Rule]
ruleFilter Thy
thy [Rule]
eqs
  o :: Rule -> Either Rule Rule
o (Expr
e1,Expr
e2) | Expr
e1 Expr -> Expr -> Bool
> Expr
e2 = Rule -> Either Rule Rule
forall a b. b -> Either a b
Right (Expr
e1,Expr
e2)
            | Expr
e2 Expr -> Expr -> Bool
> Expr
e1 = Rule -> Either Rule Rule
forall a b. b -> Either a b
Right (Expr
e2,Expr
e1)
            | Bool
otherwise = Rule -> Either Rule Rule
forall a b. a -> Either a b
Left (Expr
e1,Expr
e2)

delete :: Thy -> Thy
delete :: Thy -> Thy
delete = ([Rule] -> [Rule]) -> Thy -> Thy
updateEquationsBy (([Rule] -> [Rule]) -> Thy -> Thy)
-> ([Rule] -> [Rule]) -> Thy -> Thy
forall a b. (a -> b) -> a -> b
$ (Rule -> Bool) -> [Rule] -> [Rule]
forall a. (a -> Bool) -> [a] -> [a]
discard ((Expr -> Expr -> Bool) -> Rule -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
(==))

deleteEquivalent :: Thy -> Thy
deleteEquivalent :: Thy -> Thy
deleteEquivalent Thy
thy =
  ([Rule] -> [Rule]) -> Thy -> Thy
updateEquationsBy ((Rule -> Bool) -> [Rule] -> [Rule]
forall a. (a -> Bool) -> [a] -> [a]
discard (\(Expr
e1,Expr
e2) -> Thy -> Expr -> Expr -> Bool
equivalent (([Rule] -> [Rule]) -> Thy -> Thy
updateEquationsBy ((Rule -> Bool) -> [Rule] -> [Rule]
forall a. (a -> Bool) -> [a] -> [a]
filter (Rule -> Rule -> Bool
forall a. Eq a => a -> a -> Bool
/= (Expr
e1,Expr
e2))) Thy
thy{closureLimit :: Int
closureLimit=Int
1}) Expr
e1 Expr
e2)) Thy
thy

deleteGroundJoinable :: Thy -> Thy
deleteGroundJoinable :: Thy -> Thy
deleteGroundJoinable Thy
thy =
  ([Rule] -> [Rule]) -> Thy -> Thy
updateEquationsBy ((Rule -> Bool) -> [Rule] -> [Rule]
forall a. (a -> Bool) -> [a] -> [a]
discard (\(Expr
e1,Expr
e2) -> Thy -> Expr -> Expr -> Bool
groundJoinable (([Rule] -> [Rule]) -> Thy -> Thy
updateEquationsBy ((Rule -> Bool) -> [Rule] -> [Rule]
forall a. (a -> Bool) -> [a] -> [a]
filter (Rule -> Rule -> Bool
forall a. Eq a => a -> a -> Bool
/= (Expr
e1,Expr
e2))) Thy
thy) Expr
e1 Expr
e2)) Thy
thy
-- TODO: make deleteGroundJoinable more efficient (it is *very* inneficient right now)

-- a.k.a. Simplify-identity
simplify :: Thy -> Thy
simplify :: Thy -> Thy
simplify Thy
thy = ([Rule] -> [Rule]) -> Thy -> Thy
updateEquationsBy ([Rule] -> [Rule]
forall a. Ord a => [a] -> [a]
nubSort ([Rule] -> [Rule]) -> ([Rule] -> [Rule]) -> [Rule] -> [Rule]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rule -> Rule) -> [Rule] -> [Rule]
forall a b. (a -> b) -> [a] -> [b]
map (Thy -> Rule -> Rule
canonicalizeEqn Thy
thy))
             (Thy -> Thy) -> Thy -> Thy
forall a b. (a -> b) -> a -> b
$ (Rule -> Rule) -> Thy -> Thy
mapEquations (Thy -> Expr -> Expr
normalize Thy
thy (Expr -> Expr) -> (Expr -> Expr) -> Rule -> Rule
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
*** Thy -> Expr -> Expr
normalize Thy
thy) Thy
thy

-- a.k.a. R-Simplify-rule
compose :: Thy -> Thy
compose :: Thy -> Thy
compose Thy
thy = ([Rule] -> [Rule]) -> Thy -> Thy
updateRulesBy ([Rule] -> [Rule]
forall a. Ord a => [a] -> [a]
nubSort ([Rule] -> [Rule]) -> ([Rule] -> [Rule]) -> [Rule] -> [Rule]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rule -> Rule) -> [Rule] -> [Rule]
forall a b. (a -> b) -> [a] -> [b]
map Rule -> Rule
canonicalizeRule)
            (Thy -> Thy) -> Thy -> Thy
forall a b. (a -> b) -> a -> b
$ (Rule -> Rule) -> Thy -> Thy
mapRules (Expr -> Expr
forall a. a -> a
id (Expr -> Expr) -> (Expr -> Expr) -> Rule -> Rule
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
*** Thy -> Expr -> Expr
normalize Thy
thy) Thy
thy

-- a.k.a. L-Simplify-rule
collapse :: Thy -> Thy
collapse :: Thy -> Thy
collapse thy :: Thy
thy@Thy {equations :: Thy -> [Rule]
equations = [Rule]
eqs, rules :: Thy -> [Rule]
rules = [Rule]
rs} =
  Thy
thy {equations :: [Rule]
equations = [Rule]
eqs [Rule] -> [Rule] -> [Rule]
forall a. Ord a => [a] -> [a] -> [a]
+++ ([Rule] -> [Rule] -> [Rule]) -> [Rule] -> [[Rule]] -> [Rule]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr [Rule] -> [Rule] -> [Rule]
forall a. Ord a => [a] -> [a] -> [a]
(+++) [] ((Rule -> [Rule]) -> [Rule] -> [[Rule]]
forall a b. (a -> b) -> [a] -> [b]
map Rule -> [Rule]
collapse [Rule]
eqs'), rules :: [Rule]
rules = [Rule]
rs'}
  where
  ([Rule]
eqs',[Rule]
rs') = (Rule -> Bool) -> [Rule] -> ([Rule], [Rule])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Rule -> Bool
collapsable [Rule]
rs
  collapsable :: Rule -> Bool
collapsable = Bool -> Bool
not (Bool -> Bool) -> (Rule -> Bool) -> Rule -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Rule] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Rule] -> Bool) -> (Rule -> [Rule]) -> Rule -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rule -> [Rule]
collapse
  collapse :: Rule -> [Equation]
  collapse :: Rule -> [Rule]
collapse (Expr
e1,Expr
e2) = ([Rule] -> [Rule] -> [Rule]) -> [Rule] -> [[Rule]] -> [Rule]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr [Rule] -> [Rule] -> [Rule]
forall a. Ord a => [a] -> [a] -> [a]
(+++) []
    [ [Rule] -> [Rule]
forall a. Ord a => [a] -> [a]
nubSort [ Thy -> Rule -> Rule
canonicalizeEqn Thy
thy (Expr
e,Expr
e2) | Expr
e <- Expr -> Rule -> [Expr]
reductions1 Expr
e1 (Expr
e1',Expr
e2') ]
    | (Expr
e1',Expr
e2') <- [Rule]
rs
    , (Expr
e1',Expr
e2') Rule -> Rule -> Bool
forall a. Eq a => a -> a -> Bool
/= (Expr
e1,Expr
e2)
    , Expr
e1 Expr -> Expr -> Bool
=| Expr
e1' ]
  -- emcompasses or ">" or specialization ordering or duck beak
  (=|) :: Expr -> Expr -> Bool
  Expr
e1 =| :: Expr -> Expr -> Bool
=| Expr
e2 = Expr
e1 Expr -> Expr -> Bool
`hasInstanceOf` Expr
e2
     Bool -> Bool -> Bool
&& Bool -> Bool
not (Expr
e2 Expr -> Expr -> Bool
`hasInstanceOf` Expr
e1)

canonicalizeThy :: Thy -> Thy
canonicalizeThy :: Thy -> Thy
canonicalizeThy = [Expr] -> Thy -> Thy
canonicalizeThyWith [Expr]
preludeInstances

canonicalizeThyWith :: Instances -> Thy -> Thy
canonicalizeThyWith :: [Expr] -> Thy -> Thy
canonicalizeThyWith [Expr]
ti Thy
thy = (Rule -> Rule) -> Thy -> Thy
mapRules ([Expr] -> Rule -> Rule
canonicalizeRuleWith [Expr]
ti)
                           (Thy -> Thy) -> (Thy -> Thy) -> Thy -> Thy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rule -> Rule) -> Thy -> Thy
mapEquations (Thy -> [Expr] -> Rule -> Rule
canonicalizeEqnWith Thy
thy [Expr]
ti)
                           (Thy -> Thy) -> Thy -> Thy
forall a b. (a -> b) -> a -> b
$ Thy
thy

canonicalizeEqn :: Thy -> Equation -> Equation
canonicalizeEqn :: Thy -> Rule -> Rule
canonicalizeEqn Thy
thy = Thy -> [Expr] -> Rule -> Rule
canonicalizeEqnWith Thy
thy [Expr]
preludeInstances

canonicalEqn :: Thy -> Equation -> Bool
canonicalEqn :: Thy -> Rule -> Bool
canonicalEqn Thy
thy Rule
eq = Thy -> Rule -> Rule
canonicalizeEqn Thy
thy Rule
eq Rule -> Rule -> Bool
forall a. Eq a => a -> a -> Bool
== Rule
eq

canonicalizeEqnWith :: Thy -> Instances -> Equation -> Equation
canonicalizeEqnWith :: Thy -> [Expr] -> Rule -> Rule
canonicalizeEqnWith Thy
thy [Expr]
ti = Rule -> Rule
forall a b. (a, b) -> (b, a)
swap (Rule -> Rule) -> (Rule -> Rule) -> Rule -> Rule
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> Rule -> Rule
canonicalizeRuleWith [Expr]
ti (Rule -> Rule) -> (Rule -> Rule) -> Rule -> Rule
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rule -> Rule
forall a b. (a, b) -> (b, a)
swap (Rule -> Rule) -> (Rule -> Rule) -> Rule -> Rule
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rule -> Rule
o
  where
  cmp :: Expr -> Expr -> Ordering
cmp = Thy -> Expr -> Expr -> Ordering
compareE Thy
thy
  o :: Rule -> Rule
o (Expr
e1,Expr
e2) | Expr
e1 Expr -> Expr -> Ordering
`cmp` Expr
e2 Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
LT = (Expr
e2,Expr
e1)
            | Bool
otherwise         = (Expr
e1,Expr
e2)


canonicalizeRule :: Rule -> Rule
canonicalizeRule :: Rule -> Rule
canonicalizeRule = [Expr] -> Rule -> Rule
canonicalizeRuleWith [Expr]
preludeInstances

canonicalRule :: Rule -> Bool
canonicalRule :: Rule -> Bool
canonicalRule Rule
r = Rule -> Rule
canonicalizeRule Rule
r Rule -> Rule -> Bool
forall a. Eq a => a -> a -> Bool
== Rule
r

canonicalizeRuleWith :: Instances -> Rule -> Rule
canonicalizeRuleWith :: [Expr] -> Rule -> Rule
canonicalizeRuleWith [Expr]
ti (Expr
e1,Expr
e2) =
  case (Expr -> [String]) -> Expr -> Expr
canonicalizeWith ([Expr] -> Expr -> [String]
lookupNames [Expr]
ti) (Expr
e1 Expr -> Expr -> Expr
:$ Expr
e2) of
    Expr
e1' :$ Expr
e2' -> (Expr
e1',Expr
e2')
    Expr
_ -> String -> Rule
forall a. HasCallStack => String -> a
error (String -> Rule) -> String -> Rule
forall a b. (a -> b) -> a -> b
$ String
"canonicalizeRuleWith: the impossible happened,"
              String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"this is definitely a bug, see source!"

printThy :: Thy -> IO ()
printThy :: Thy -> IO ()
printThy = String -> IO ()
putStrLn (String -> IO ()) -> (Thy -> String) -> Thy -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Thy -> String
showThy

showThy :: Thy -> String
showThy :: Thy -> String
showThy Thy
thy = (if [Rule] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Rule]
rs
                 then String
"no rules.\n"
                 else String
"rules:\n"     String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Rule] -> String
showEquations [Rule]
rs)
           String -> String -> String
forall a. [a] -> [a] -> [a]
++ (if [Rule] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Rule]
eqs
                 then String
""
                 else String
"equations:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Rule] -> String
showEquations [Rule]
eqs)
  where
  thy' :: Thy
thy' = Thy -> Thy
canonicalizeThy Thy
thy
  rs :: [Rule]
rs = Thy -> [Rule]
rules Thy
thy'
  eqs :: [Rule]
eqs = Thy -> [Rule]
equations Thy
thy'
  showEquations :: [Rule] -> String
showEquations = [String] -> String
unlines ([String] -> String) -> ([Rule] -> [String]) -> [Rule] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rule -> String) -> [Rule] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Rule -> String
showEquation
  showEquation :: Rule -> String
showEquation (Expr
e1,Expr
e2) = Expr -> String
showExpr Expr
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" == " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
showExpr Expr
e2

finalEquations :: (Equation -> Bool) -> Instances -> Thy -> [Equation]
finalEquations :: (Rule -> Bool) -> [Expr] -> Thy -> [Rule]
finalEquations Rule -> Bool
shouldShow [Expr]
ti Thy
thy =
    (Rule -> Rule -> Ordering) -> [Rule] -> [Rule]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (TypeRep -> TypeRep -> Ordering
compareTy (TypeRep -> TypeRep -> Ordering)
-> (Rule -> TypeRep) -> Rule -> Rule -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Expr -> TypeRep
typ (Expr -> TypeRep) -> (Rule -> Expr) -> Rule -> TypeRep
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rule -> Expr
forall a b. (a, b) -> a
fst))
  ([Rule] -> [Rule]) -> ([Rule] -> [Rule]) -> [Rule] -> [Rule]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rule -> Rule -> Ordering) -> [Rule] -> [Rule]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Thy -> Expr -> Expr -> Ordering
compareE Thy
thy (Expr -> Expr -> Ordering)
-> (Rule -> Expr) -> Rule -> Rule -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Rule -> Expr
foldPair)
  ([Rule] -> [Rule]) -> ([Rule] -> [Rule]) -> [Rule] -> [Rule]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rule -> Bool) -> [Rule] -> [Rule]
forall a. (a -> Bool) -> [a] -> [a]
filter Rule -> Bool
shouldShow
  ([Rule] -> [Rule]) -> [Rule] -> [Rule]
forall a b. (a -> b) -> a -> b
$ Thy -> [Rule]
rules Thy
thy' [Rule] -> [Rule] -> [Rule]
forall a. [a] -> [a] -> [a]
++ (Rule -> Rule) -> [Rule] -> [Rule]
forall a b. (a -> b) -> [a] -> [b]
map Rule -> Rule
forall a b. (a, b) -> (b, a)
swap (Thy -> [Rule]
equations Thy
thy')
  where
  thy' :: Thy
thy' = [Expr] -> Thy -> Thy
canonicalizeThyWith [Expr]
ti (Thy -> Thy) -> (Thy -> Thy) -> Thy -> Thy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Thy -> Thy
discardRedundantRulesByEquations (Thy -> Thy) -> Thy -> Thy
forall a b. (a -> b) -> a -> b
$ Thy -> Thy
finalize Thy
thy

-- | Finalize a theory by discarding redundant equations.  If after finalizing
--   you 'complete', redundant equations might pop-up again.
finalize :: Thy -> Thy
finalize :: Thy -> Thy
finalize = Thy -> Thy
discardRedundantEquations

-- | Double-checks a resulting theory moving untrue rules and equations to the
--   invalid list.
--
-- As a side-effect of using testing to conjecturing equations,
-- we may get smaller equations that are obviously incorrect
-- when we consider a bigger (harder-to-test) equation that is incorrect.
--
-- For example, given an incorrect large equation, it may follow that
-- False=True.
--
-- This function can be used to double-check the generated theory.
-- If any equation or rule is discarded, that means the number of tests
-- should probably be increased.
doubleCheck :: (Expr -> Expr -> Bool) -> Thy -> Thy
doubleCheck :: (Expr -> Expr -> Bool) -> Thy -> Thy
doubleCheck Expr -> Expr -> Bool
(===) Thy
thy  =  Thy
thy
                       {  rules :: [Rule]
rules     = (Rule -> Bool) -> [Rule] -> [Rule]
forall a. (a -> Bool) -> [a] -> [a]
filter Rule -> Bool
correct (Thy -> [Rule]
rules Thy
thy)
                       ,  equations :: [Rule]
equations = (Rule -> Bool) -> [Rule] -> [Rule]
forall a. (a -> Bool) -> [a] -> [a]
filter Rule -> Bool
correct (Thy -> [Rule]
equations Thy
thy)
                       ,  invalid :: [Rule]
invalid   = (Rule -> Bool) -> [Rule] -> [Rule]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Rule -> Bool) -> Rule -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rule -> Bool
correct) (Thy -> [Rule]
rules Thy
thy [Rule] -> [Rule] -> [Rule]
forall a. [a] -> [a] -> [a]
++ Thy -> [Rule]
equations Thy
thy)
                       }
  where
  correct :: Rule -> Bool
correct  =  (Expr -> Expr -> Bool) -> Rule -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Expr -> Expr -> Bool
(===)

theorize :: [Equation] -> Thy
theorize :: [Rule] -> Thy
theorize = (Expr -> Expr -> Bool) -> [Rule] -> Thy
theorizeBy (Thy -> Expr -> Expr -> Bool
canReduceTo Thy
emptyThy)

theorizeBy :: (Expr -> Expr -> Bool) -> [Equation] -> Thy
theorizeBy :: (Expr -> Expr -> Bool) -> [Rule] -> Thy
theorizeBy Expr -> Expr -> Bool
(>) = Thy -> Thy
finalize
               (Thy -> Thy) -> ([Rule] -> Thy) -> [Rule] -> Thy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Thy -> Thy
canonicalizeThy
               (Thy -> Thy) -> ([Rule] -> Thy) -> [Rule] -> Thy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Thy -> Thy
complete
               (Thy -> Thy) -> ([Rule] -> Thy) -> [Rule] -> Thy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> (Expr -> Expr -> Bool) -> [Rule] -> Thy
initialize Int
3 Expr -> Expr -> Bool
(>)

initialize :: Int -> (Expr -> Expr -> Bool) -> [Equation] -> Thy
initialize :: Int -> (Expr -> Expr -> Bool) -> [Rule] -> Thy
initialize Int
n Expr -> Expr -> Bool
(>) [Rule]
eqs = Thy
thy
  where
  thy :: Thy
thy = Thy
emptyThy
      { equations :: [Rule]
equations = [Rule] -> [Rule]
forall a. Ord a => [a] -> [a]
nubSort ([Rule] -> [Rule]) -> [Rule] -> [Rule]
forall a b. (a -> b) -> a -> b
$ (Rule -> Rule) -> [Rule] -> [Rule]
forall a b. (a -> b) -> [a] -> [b]
map (Thy -> Rule -> Rule
canonicalizeEqn Thy
thy) [Rule]
eqs
      , keepE :: Expr -> Bool
keepE = [Rule] -> Expr -> Bool
keepMaxOf [Rule]
eqs
      , canReduceTo :: Expr -> Expr -> Bool
canReduceTo = Expr -> Expr -> Bool
(>)
      , closureLimit :: Int
closureLimit = Int
n
      }

defaultKeep :: Thy -> Thy
defaultKeep :: Thy -> Thy
defaultKeep thy :: Thy
thy@Thy {equations :: Thy -> [Rule]
equations = [Rule]
eqs, rules :: Thy -> [Rule]
rules = [Rule]
rs} =
  Thy
thy { keepE :: Expr -> Bool
keepE = [Rule] -> Expr -> Bool
keepMaxOf ([Rule]
eqs[Rule] -> [Rule] -> [Rule]
forall a. [a] -> [a] -> [a]
++[Rule]
rs) }

discardRedundantEquations :: Thy -> Thy
discardRedundantEquations :: Thy -> Thy
discardRedundantEquations Thy
thy =
  ([Rule] -> [Rule]) -> Thy -> Thy
updateEquationsBy [Rule] -> [Rule]
discardRedundant Thy
thy
  where
  discardRedundant :: [Rule] -> [Rule]
discardRedundant = [Rule] -> [Rule] -> [Rule]
d []
                   ([Rule] -> [Rule]) -> ([Rule] -> [Rule]) -> [Rule] -> [Rule]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rule -> Rule -> Bool) -> [Rule] -> [Rule]
forall a. (a -> a -> Bool) -> [a] -> [a]
discardLater Rule -> Rule -> Bool
eqnInstanceOf
                   ([Rule] -> [Rule]) -> ([Rule] -> [Rule]) -> [Rule] -> [Rule]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Rule] -> [Rule]
forall a. [a] -> [a]
reverse
                   ([Rule] -> [Rule]) -> ([Rule] -> [Rule]) -> [Rule] -> [Rule]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rule -> Int) -> [Rule] -> [Rule]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn ((Int -> Int -> Int) -> (Int, Int) -> Int
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) ((Int, Int) -> Int) -> (Rule -> (Int, Int)) -> Rule -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Int
size (Expr -> Int) -> (Expr -> Int) -> Rule -> (Int, Int)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
*** Expr -> Int
size))
  (Expr
e1l,Expr
e1r) eqnInstanceOf :: Rule -> Rule -> Bool
`eqnInstanceOf` (Expr
e0l,Expr
e0r) = Expr
e1l Expr -> Expr -> Bool
`hasCanonInstanceOf` Expr
e0l
                                     Bool -> Bool -> Bool
&& Expr
e1r Expr -> Expr -> Bool
`hasCanonInstanceOf` Expr
e0r
                                     Bool -> Bool -> Bool
|| Expr
e1l Expr -> Expr -> Bool
`hasCanonInstanceOf` Expr
e0r
                                     Bool -> Bool -> Bool
&& Expr
e1r Expr -> Expr -> Bool
`hasCanonInstanceOf` Expr
e0l
  d :: [Rule] -> [Rule] -> [Rule]
d [Rule]
ks [] = [Rule]
ks
  d [Rule]
ks ((Expr
e1,Expr
e2):[Rule]
eqs)
    | Thy -> Expr -> Expr -> Bool
equivalent Thy
thy {equations :: [Rule]
equations = [Rule]
eqs} Expr
e1 Expr
e2 = [Rule] -> [Rule] -> [Rule]
d          [Rule]
ks  [Rule]
eqs
    | Bool
otherwise                              = [Rule] -> [Rule] -> [Rule]
d ((Expr
e1,Expr
e2)Rule -> [Rule] -> [Rule]
forall a. a -> [a] -> [a]
:[Rule]
ks) [Rule]
eqs

discardRedundantRulesByEquations :: Thy -> Thy
discardRedundantRulesByEquations :: Thy -> Thy
discardRedundantRulesByEquations Thy
thy = ([Rule] -> [Rule]) -> Thy -> Thy
updateRulesBy ([Rule] -> [Rule] -> [Rule]
d [] ([Rule] -> [Rule]) -> ([Rule] -> [Rule]) -> [Rule] -> [Rule]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Rule] -> [Rule]
forall a. [a] -> [a]
reverse) Thy
thy
  where
  d :: [Rule] -> [Rule] -> [Rule]
d [Rule]
ks [] = [Rule]
ks
  d [Rule]
ks ((Expr
e1,Expr
e2):[Rule]
rs)
    | Thy -> Expr -> Expr -> Bool
equivalent Thy
thy {rules :: [Rule]
rules = [Rule]
ks[Rule] -> [Rule] -> [Rule]
forall a. [a] -> [a] -> [a]
++[Rule]
rs} Expr
e1 Expr
e2 = [Rule] -> [Rule] -> [Rule]
d          [Rule]
ks  [Rule]
rs
    | Bool
otherwise                             = [Rule] -> [Rule] -> [Rule]
d ((Expr
e1,Expr
e2)Rule -> [Rule] -> [Rule]
forall a. a -> [a] -> [a]
:[Rule]
ks) [Rule]
rs