-- |
-- Module      : Test.Speculate.Engine
-- Copyright   : (c) 2016-2024 Rudy Matela
-- License     : 3-Clause BSD  (see the file LICENSE)
-- Maintainer  : Rudy Matela <rudy@matela.com.br>
--
-- This module is part of Speculate.
--
-- Main engine to process data.
module Test.Speculate.Engine
  ( expansions
  , expansionsOfType
  , expansionsWith

  , theoryAndRepresentativesFromAtoms
  , representativesFromAtoms
  , theoryFromAtoms
  , theoryAndRepresentativesFromAtomsKeeping
  , representativesFromAtomsKeeping
  , theoryFromAtomsKeeping
  , equivalencesBetween

  , consider
  , distinctFromSchemas
  , classesFromSchemas
  , classesFromSchemasAndVariables

  , semiTheoryFromThyAndReps

  , conditionalTheoryFromThyAndReps
  , conditionalEquivalences
  , subConsequence

  , psortBy

  , module Test.Speculate.Expr
  )
where

import Data.Dynamic
import Data.Maybe
import Data.List hiding (insert)
import Data.Function (on)

import Test.LeanCheck ((\/))
import Test.Speculate.Utils
import Test.Speculate.Expr
import Test.Speculate.Reason
import Test.Speculate.CondReason
import Test.Speculate.SemiReason
import Test.Speculate.Utils.Class (Class)
import Test.Speculate.Utils.List (none)
import qualified Test.Speculate.Utils.Class as C
import qualified Test.Speculate.Utils.Digraph as D

------------------------------
-- * Manipulating expressions

canonicalVariationsEqn :: (Expr,Expr) -> [(Expr,Expr)]
canonicalVariationsEqn :: (Expr, Expr) -> [(Expr, Expr)]
canonicalVariationsEqn = ((Expr, Expr) -> Bool) -> [(Expr, Expr)] -> [(Expr, Expr)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Expr -> Expr -> Bool) -> (Expr, Expr) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
(/=))
                       ([(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 b. (a -> b) -> [a] -> [b]
map Expr -> (Expr, Expr)
unfoldPair
                       ([Expr] -> [(Expr, Expr)])
-> ((Expr, Expr) -> [Expr]) -> (Expr, Expr) -> [(Expr, Expr)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
fastCanonicalVariations
                       (Expr -> [Expr])
-> ((Expr, Expr) -> Expr) -> (Expr, Expr) -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr, Expr) -> Expr
foldPair

-- | List all variable assignments for a given type and list of variables.
expansionsOfType :: Expr -> [String] -> Expr -> [Expr]
expansionsOfType :: Expr -> [String] -> Expr -> [Expr]
expansionsOfType Expr
ht [String]
vs Expr
e = [ Expr -> [Expr] -> Expr
fill Expr
e [String
v String -> Expr -> Expr
`varAsTypeOf` Expr
ht | String
v <- [String]
vs']
                           | [String]
vs' <- Int -> [String] -> [[String]]
forall a. Int -> [a] -> [[a]]
placements (Expr -> Expr -> Int
countHoles Expr
ht Expr
e) [String]
vs ]
  where
  placements :: Int -> [a] -> [[a]]
  placements :: forall a. Int -> [a] -> [[a]]
placements Int
0 [a]
xs = [[]]
  placements Int
n [a]
xs = [a
ya -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
ys | a
y <- [a]
xs, [a]
ys <- Int -> [a] -> [[a]]
forall a. Int -> [a] -> [[a]]
placements (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) [a]
xs]
  countHoles :: Expr -> Expr -> Int
  countHoles :: Expr -> Expr -> Int
countHoles Expr
ht Expr
e = [()] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [() | Expr
h <- Expr -> [Expr]
holes Expr
e, Expr -> TypeRep
typ Expr
h TypeRep -> TypeRep -> Bool
forall a. Eq a => a -> a -> Bool
== Expr -> TypeRep
typ Expr
ht]
-- change first argument of expansionsOfType to just [Expr] with the list of
-- possible variables?

expansionsWith :: [Expr] -> Expr -> [Expr]
expansionsWith :: [Expr] -> Expr -> [Expr]
expansionsWith [Expr]
es = [[Expr]] -> Expr -> [Expr]
ew ((Expr -> TypeRep) -> [Expr] -> [[Expr]]
forall b a. Ord b => (a -> b) -> [a] -> [[a]]
classifyOn Expr -> TypeRep
typ [Expr]
es)
  where
  nam :: Expr -> String
nam (Value (Char
'_':String
s) Dynamic
_) = String
s
  nam Expr
_ = String
"expansionsWith: argument list must only contain vars."
  ew :: [[Expr]] -> Expr -> [Expr]
  ew :: [[Expr]] -> Expr -> [Expr]
ew []        Expr
e = [Expr
e]
  ew ([Expr]
es:[[Expr]]
tnss) Expr
e = [[Expr]] -> Expr -> [Expr]
ew [[Expr]]
tnss
           (Expr -> [Expr]) -> [Expr] -> [Expr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
`concatMap` Expr -> [String] -> Expr -> [Expr]
expansionsOfType ([Expr] -> Expr
forall a. HasCallStack => [a] -> a
head [Expr]
es) ((Expr -> String) -> [Expr] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> String
nam [Expr]
es) Expr
e

-- | List all variable assignments for a given number of variables.
--   It only assign variables to holes (variables with "" as its name).
--
-- > > expansions preludeInstances 2 '(_ + _ + ord _)
-- > [ (x + x) + ord c :: Int
-- > , (x + x) + ord d :: Int
-- > , (x + y) + ord c :: Int
-- > , (x + y) + ord d :: Int
-- > , (y + x) + ord c :: Int
-- > , (y + x) + ord d :: Int
-- > , (y + y) + ord c :: Int
-- > , (y + y) + ord d :: Int ]
expansions :: Instances -> Int -> Expr -> [Expr]
expansions :: [Expr] -> Int -> Expr -> [Expr]
expansions [Expr]
is Int
n Expr
e =
  case [Expr] -> [(Expr, Int)]
forall a. Eq a => [a] -> [(a, Int)]
counts (Expr -> [Expr]
holes Expr
e) of
    []      -> [Expr
e]
    (Expr
h,Int
c):[(Expr, Int)]
_ -> [Expr] -> Int -> Expr -> [Expr]
expansions [Expr]
is Int
n (Expr -> [Expr]) -> [Expr] -> [Expr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
`concatMap`
               Expr -> [String] -> Expr -> [Expr]
expansionsOfType Expr
h (Int -> [String] -> [String]
forall a. Int -> [a] -> [a]
take Int
n ([Expr] -> Expr -> [String]
lookupNames [Expr]
is Expr
h)) Expr
e

rehole :: Expr -> Expr
rehole :: Expr -> Expr
rehole (Expr
e1 :$ Expr
e2)    = Expr -> Expr
rehole Expr
e1 Expr -> Expr -> Expr
:$ Expr -> Expr
rehole Expr
e2
rehole Expr
e | Expr -> Bool
isVar Expr
e   = String
"" String -> Expr -> Expr
`varAsTypeOf` Expr
e
         | Bool
otherwise = Expr
e

----------------------------
-- * Enumerating expressions

-- | Computes a theory from atomic expressions.  Example:
--
-- > > theoryFromAtoms 5 (const True) (equal preludeInstances 100)
-- > >   [hole (undefined :: Int),constant "+" ((+) :: Int -> Int -> Int)]
-- > Thy { rules = [ (x + y) + z == x + (y + z) ]
-- >     , equations = [ y + x == x + y
-- >                   , y + (x + z) == x + (y + z)
-- >                   , z + (x + y) == x + (y + z)
-- >                   , z + (y + x) == x + (y + z) ]
-- >     , canReduceTo = (|>)
-- >     , closureLimit = 2
-- >     , keepE = keepUpToLength 5
-- >     }
theoryFromAtoms :: (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> Thy
theoryFromAtoms :: (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> Thy
theoryFromAtoms  =  (Expr -> Bool) -> (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> Thy
theoryFromAtomsKeeping (Bool -> Expr -> Bool
forall a b. a -> b -> a
const Bool
True)

representativesFromAtoms :: (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> [[Expr]]
representativesFromAtoms :: (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> [[Expr]]
representativesFromAtoms  =  (Expr -> Bool)
-> (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> [[Expr]]
representativesFromAtomsKeeping (Bool -> Expr -> Bool
forall a b. a -> b -> a
const Bool
True)

theoryAndRepresentativesFromAtoms :: (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> (Thy,[[Expr]])
theoryAndRepresentativesFromAtoms :: (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> (Thy, [[Expr]])
theoryAndRepresentativesFromAtoms  =  (Expr -> Bool)
-> (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> (Thy, [[Expr]])
theoryAndRepresentativesFromAtomsKeeping (Bool -> Expr -> Bool
forall a b. a -> b -> a
const Bool
True)

theoryFromAtomsKeeping :: (Expr -> Bool) -> (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> Thy
theoryFromAtomsKeeping :: (Expr -> Bool) -> (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> Thy
theoryFromAtomsKeeping Expr -> Bool
keep Expr -> Expr -> Bool
(===) Int
sz  =  (Thy, [[Expr]]) -> Thy
forall a b. (a, b) -> a
fst ((Thy, [[Expr]]) -> Thy)
-> ([[Expr]] -> (Thy, [[Expr]])) -> [[Expr]] -> Thy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Bool)
-> (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> (Thy, [[Expr]])
theoryAndRepresentativesFromAtomsKeeping Expr -> Bool
keep Expr -> Expr -> Bool
(===) Int
sz

representativesFromAtomsKeeping :: (Expr -> Bool) -> (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> [[Expr]]
representativesFromAtomsKeeping :: (Expr -> Bool)
-> (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> [[Expr]]
representativesFromAtomsKeeping Expr -> Bool
keep Expr -> Expr -> Bool
(===) Int
sz  =  (Thy, [[Expr]]) -> [[Expr]]
forall a b. (a, b) -> b
snd ((Thy, [[Expr]]) -> [[Expr]])
-> ([[Expr]] -> (Thy, [[Expr]])) -> [[Expr]] -> [[Expr]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Bool)
-> (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> (Thy, [[Expr]])
theoryAndRepresentativesFromAtomsKeeping Expr -> Bool
keep Expr -> Expr -> Bool
(===) Int
sz

expand :: (Expr -> Bool) -> (Expr -> Expr -> Bool) -> Int -> [Expr] -> (Thy,[[Expr]]) -> (Thy,[[Expr]])
expand :: (Expr -> Bool)
-> (Expr -> Expr -> Bool)
-> Int
-> [Expr]
-> (Thy, [[Expr]])
-> (Thy, [[Expr]])
expand Expr -> Bool
keep Expr -> Expr -> Bool
(===) Int
sz [Expr]
ss (Thy
thy,[[Expr]]
sss) = (Thy -> Thy) -> (Thy, [[Expr]]) -> (Thy, [[Expr]])
forall a a' b. (a -> a') -> (a, b) -> (a', b)
first Thy -> Thy
complete
                                  ((Thy, [[Expr]]) -> (Thy, [[Expr]]))
-> ([[Expr]] -> (Thy, [[Expr]])) -> [[Expr]] -> (Thy, [[Expr]])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Thy, [[Expr]]) -> Expr -> (Thy, [[Expr]]))
-> (Thy, [[Expr]]) -> [Expr] -> (Thy, [[Expr]])
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((Expr -> (Thy, [[Expr]]) -> (Thy, [[Expr]]))
-> (Thy, [[Expr]]) -> Expr -> (Thy, [[Expr]])
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Expr -> (Thy, [[Expr]]) -> (Thy, [[Expr]]))
 -> (Thy, [[Expr]]) -> Expr -> (Thy, [[Expr]]))
-> (Expr -> (Thy, [[Expr]]) -> (Thy, [[Expr]]))
-> (Thy, [[Expr]])
-> Expr
-> (Thy, [[Expr]])
forall a b. (a -> b) -> a -> b
$ (Expr -> Expr -> Bool)
-> Int -> Expr -> (Thy, [[Expr]]) -> (Thy, [[Expr]])
consider Expr -> Expr -> Bool
(===) Int
sz) (Thy
thy,[[Expr]]
sss)
                                  ([Expr] -> (Thy, [[Expr]]))
-> ([[Expr]] -> [Expr]) -> [[Expr]] -> (Thy, [[Expr]])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Expr]] -> [Expr]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
                                  ([[Expr]] -> [Expr])
-> ([[Expr]] -> [[Expr]]) -> [[Expr]] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Expr]
ss[Expr] -> [[Expr]] -> [[Expr]]
forall a. a -> [a] -> [a]
:)
                                  ([[Expr]] -> [[Expr]])
-> ([[Expr]] -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Expr] -> [Expr] -> [Expr]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> a -> b) -> [a] -> [b]
zipWithReverse [Expr] -> [Expr] -> [Expr]
(*$*)
                                  ([[Expr]] -> (Thy, [[Expr]])) -> [[Expr]] -> (Thy, [[Expr]])
forall a b. (a -> b) -> a -> b
$ Int -> [[Expr]] -> [[Expr]]
forall a. Int -> [a] -> [a]
take Int
sz [[Expr]]
sss
  where
  [Expr]
fes *$* :: [Expr] -> [Expr] -> [Expr]
*$* [Expr]
xes = (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
filter Expr -> Bool
keep ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$ [Maybe Expr] -> [Expr]
forall a. [Maybe a] -> [a]
catMaybes [Expr
fe Expr -> Expr -> Maybe Expr
$$ Expr
xe | Expr
fe <- [Expr]
fes, Expr
xe <- [Expr]
xes]

-- | Given atomic expressions, compute theory and representative schema
--   expressions.  (cf. 'theoryFromAtoms')
theoryAndRepresentativesFromAtomsKeeping :: (Expr -> Bool) -> (Expr -> Expr -> Bool)
                                         -> Int -> [[Expr]] -> (Thy,[[Expr]])
theoryAndRepresentativesFromAtomsKeeping :: (Expr -> Bool)
-> (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> (Thy, [[Expr]])
theoryAndRepresentativesFromAtomsKeeping Expr -> Bool
keep Expr -> Expr -> Bool
(===) Int
sz [[Expr]]
dss  =
  [(Thy, [[Expr]]) -> (Thy, [[Expr]])]
-> (Thy, [[Expr]]) -> (Thy, [[Expr]])
forall a. [a -> a] -> a -> a
chain [(Expr -> Bool)
-> (Expr -> Expr -> Bool)
-> Int
-> [Expr]
-> (Thy, [[Expr]])
-> (Thy, [[Expr]])
expand Expr -> Bool
keep Expr -> Expr -> Bool
(===) Int
sz' ([[Expr]]
dss [[Expr]] -> Int -> [Expr]
forall a. [[a]] -> Int -> [a]
! (Int
sz'Int -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)) | Int
sz' <- [Int] -> [Int]
forall a. [a] -> [a]
reverse [Int
1..Int
sz]] (Thy
iniThy,[])
  where
  iniThy :: Thy
iniThy = Thy
emptyThy { keepE = keepUpToLength sz
                    , closureLimit = 2
                    , canReduceTo = dwoBy (\Expr
e1 Expr
e2 -> Expr
e1 Expr -> Expr -> Ordering
`cmp` Expr
e2 Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
GT)
                    , compareE = cmp
                    }
  cmp :: Expr -> Expr -> Ordering
cmp  =  [Expr] -> Expr -> Expr -> Ordering
compareComplexityThenIndex ([[Expr]] -> [Expr]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Expr]]
dss)
  -- NOTE: "concat dss" may be an infinite list.  This function assumes that
  -- the symbols will appear on the list eventually for termination.  If I am
  -- correct, this invariant is assured by the rest of the code.

-- considers a schema
consider :: (Expr -> Expr -> Bool) -> Int -> Expr -> (Thy,[[Expr]]) -> (Thy,[[Expr]])
consider :: (Expr -> Expr -> Bool)
-> Int -> Expr -> (Thy, [[Expr]]) -> (Thy, [[Expr]])
consider Expr -> Expr -> Bool
(===) Int
sz Expr
s (Thy
thy,[[Expr]]
sss)
  | Expr
ns Expr -> [Expr] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Expr]
ss = (Thy
thy,[[Expr]]
sss)
  | Bool -> Bool
not (Expr
ns Expr -> Expr -> Bool
=== Expr
ns) = (Thy
thy,[[Expr]]
sssWs)  -- uncomparable type
  | Bool
otherwise =
    ( Thy -> [(Expr, Expr)] -> Thy
append Thy
thy ([(Expr, Expr)] -> Thy) -> [(Expr, Expr)] -> Thy
forall a b. (a -> b) -> a -> b
$ (Expr -> Expr -> Bool) -> Expr -> Expr -> [(Expr, Expr)]
equivalencesBetween Expr -> Expr -> Bool
(-===-) Expr
ms Expr
ms [(Expr, Expr)] -> [(Expr, Expr)] -> [(Expr, Expr)]
forall a. [a] -> [a] -> [a]
++ [(Expr, Expr)]
eqs
    , if ((Expr, Expr) -> Bool) -> [(Expr, Expr)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\(Expr
e1,Expr
e2) -> Expr -> Bool
unrepeatedVars Expr
e1 Bool -> Bool -> Bool
&& Expr -> Bool
unrepeatedVars Expr
e2) [(Expr, Expr)]
eqs
      then [[Expr]]
sss
      else [[Expr]]
sssWs )
  where
  ns :: Expr
ns = Expr -> Expr
rehole (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Thy -> Expr -> Expr
normalizeE Thy
thy (Expr -> Expr
fastMostGeneralVariation Expr
s)
  -- between s and ns, choose the one with less holes to call equivalencesBetween
  ms :: Expr
ms | [Expr] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Expr -> [Expr]
holes Expr
s) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [Expr] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Expr -> [Expr]
holes Expr
ns) = Expr
s
     | Bool
otherwise = Expr
ns -- favour ns only if it reduces the number of variables
  Expr
e1 -===- :: Expr -> Expr -> Bool
-===- Expr
e2  =  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 Bool -> Bool -> Bool
|| Expr
e1 Expr -> Expr -> Bool
=== Expr
e2
  ss :: [Expr]
ss = Int -> [[Expr]] -> [Expr]
forall a. Int -> [[a]] -> [a]
uptoT Int
sz [[Expr]]
sss
  sssWs :: [[Expr]]
sssWs = [[Expr]]
sss [[Expr]] -> [[Expr]] -> [[Expr]]
forall a. [[a]] -> [[a]] -> [[a]]
\/ Int -> Expr -> [[Expr]]
forall a. Int -> a -> [[a]]
wcons0 Int
sz Expr
s
  eqs :: [(Expr, Expr)]
eqs = (Expr -> [(Expr, Expr)]) -> [Expr] -> [(Expr, Expr)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((Expr -> Expr -> Bool) -> Expr -> Expr -> [(Expr, Expr)]
equivalencesBetween Expr -> Expr -> Bool
(-===-) Expr
ms) ([Expr] -> [(Expr, Expr)]) -> [Expr] -> [(Expr, Expr)]
forall a b. (a -> b) -> a -> b
$ (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
filter (Expr
ms Expr -> Expr -> Bool
===) [Expr]
ss
  wcons0 :: Int -> a -> [[a]]
  wcons0 :: forall a. Int -> a -> [[a]]
wcons0 Int
n a
s = Int -> [a] -> [[a]]
forall a. Int -> a -> [a]
replicate (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) [] [[a]] -> [[a]] -> [[a]]
forall a. [a] -> [a] -> [a]
++ [[a
s]]

distinctFromSchemas :: Instances -> Int -> Int -> Thy -> [Expr] -> [Expr]
distinctFromSchemas :: [Expr] -> Int -> Int -> Thy -> [Expr] -> [Expr]
distinctFromSchemas [Expr]
ti Int
nt Int
nv Thy
thy = (Class Expr -> Expr) -> [Class Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Class Expr -> Expr
forall a. Class a -> a
C.rep ([Class Expr] -> [Expr])
-> ([Expr] -> [Class Expr]) -> [Expr] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> Int -> Int -> Thy -> [Expr] -> [Class Expr]
classesFromSchemas [Expr]
ti Int
nt Int
nv Thy
thy

-- > > classesFromSchemas preludeInstances 500 2 thy [_ + _, _ + (_ + _)]
-- > [ (x + x :: Int,[])
-- > , (x + y :: Int,[y + x :: Int])
-- > , (y + y :: Int,[])
-- > , (x + (x + x) :: Int,[])
-- > , (x + (x + y) :: Int,[x + (y + x) :: Int,y + (x + x) :: Int])
-- > , (x + (y + y) :: Int,[y + (x + y) :: Int,y + (y + x) :: Int])
-- > , (y + (y + y) :: Int,[]) ]
classesFromSchemas :: Instances -> Int -> Int -> Thy -> [Expr] -> [Class Expr]
classesFromSchemas :: [Expr] -> Int -> Int -> Thy -> [Expr] -> [Class Expr]
classesFromSchemas [Expr]
ti Int
nt Int
nv Thy
thy = (Expr -> Expr -> Bool) -> [Class Expr] -> [Class Expr]
forall a. (a -> a -> Bool) -> [Class a] -> [Class a]
C.mergesThat ([Expr] -> Int -> Expr -> Expr -> Bool
equal [Expr]
ti Int
nt)
                                ([Class Expr] -> [Class Expr])
-> ([Expr] -> [Class Expr]) -> [Expr] -> [Class Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Expr) -> [Class Expr] -> [Class Expr]
forall b a. Eq b => (a -> b) -> [Class a] -> [Class a]
C.mergesOn (Thy -> Expr -> Expr
normalizeE Thy
thy)
                                ([Class Expr] -> [Class Expr])
-> ([Expr] -> [Class Expr]) -> [Expr] -> [Class Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> [Class Expr]) -> [Expr] -> [Class Expr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Expr] -> Thy -> Int -> Expr -> [Class Expr]
classesFromSchema [Expr]
ti Thy
thy Int
nv)
-- the "mergesThat (equal ...)" above is necesary because "equivalent thy"
-- won't detect all equivalences.  here we test the few remaining
-- there shouldn't be that much overhead

-- | Returns all classes of expressions that can be build from expression
--   schemas (single variable expressions).  Examples:
--
-- > > classesFromSchema preludeInstances thy 2 (i_ -+- i_)
-- > [ (x + x :: Int,[])
-- > , (x + y :: Int,[])
-- > , (y + x :: Int,[])
-- > , (y + y :: Int,[]) ]
classesFromSchema :: Instances -> Thy -> Int -> Expr -> [Class Expr]
classesFromSchema :: [Expr] -> Thy -> Int -> Expr -> [Class Expr]
classesFromSchema [Expr]
ti Thy
thy Int
n = (Expr -> Expr) -> [Class Expr] -> [Class Expr]
forall b a. Eq b => (a -> b) -> [Class a] -> [Class a]
C.mergesOn (Thy -> Expr -> Expr
normalizeE Thy
thy)
                           ([Class Expr] -> [Class Expr])
-> (Expr -> [Class Expr]) -> Expr -> [Class Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Class Expr) -> [Expr] -> [Class Expr]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> Class Expr
forall a. a -> Class a
C.fromRep
                           ([Expr] -> [Class Expr])
-> (Expr -> [Expr]) -> Expr -> [Class Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> Int -> Expr -> [Expr]
expansions [Expr]
ti Int
n

classesFromSchemasAndVariables :: Thy -> [Expr] -> [Expr] -> [Class Expr]
classesFromSchemasAndVariables :: Thy -> [Expr] -> [Expr] -> [Class Expr]
classesFromSchemasAndVariables Thy
thy [Expr]
vs = (Expr -> Expr) -> [Class Expr] -> [Class Expr]
forall b a. Eq b => (a -> b) -> [Class a] -> [Class a]
C.mergesOn (Thy -> Expr -> Expr
normalizeE Thy
thy)
                                      ([Class Expr] -> [Class Expr])
-> ([Expr] -> [Class Expr]) -> [Expr] -> [Class Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> [Class Expr]) -> [Expr] -> [Class Expr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Thy -> [Expr] -> Expr -> [Class Expr]
classesFromSchemaAndVariables Thy
thy [Expr]
vs)

classesFromSchemaAndVariables :: Thy -> [Expr] -> Expr -> [Class Expr]
classesFromSchemaAndVariables :: Thy -> [Expr] -> Expr -> [Class Expr]
classesFromSchemaAndVariables Thy
thy [Expr]
vs = (Expr -> Expr) -> [Class Expr] -> [Class Expr]
forall b a. Eq b => (a -> b) -> [Class a] -> [Class a]
C.mergesOn (Thy -> Expr -> Expr
normalizeE Thy
thy)
                                     ([Class Expr] -> [Class Expr])
-> (Expr -> [Class Expr]) -> Expr -> [Class Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Class Expr) -> [Expr] -> [Class Expr]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> Class Expr
forall a. a -> Class a
C.fromRep
                                     ([Expr] -> [Class Expr])
-> (Expr -> [Expr]) -> Expr -> [Class Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
filter ([Expr] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Expr] -> Bool) -> (Expr -> [Expr]) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
holes)
                                     ([Expr] -> [Expr]) -> (Expr -> [Expr]) -> Expr -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> Expr -> [Expr]
expansionsWith [Expr]
vs

-- Return relevant equivalences between holed expressions:
--
-- > equivalencesBetween basicInstances 500 (_ + _) (_ + _) =
-- >   [i + j == j + i]
equivalencesBetween :: (Expr -> Expr -> Bool) -> Expr -> Expr -> [(Expr,Expr)]
equivalencesBetween :: (Expr -> Expr -> Bool) -> Expr -> Expr -> [(Expr, Expr)]
equivalencesBetween Expr -> Expr -> Bool
(===) Expr
e1 Expr
e2 = [(Expr, Expr)] -> [(Expr, Expr)]
filterRelevant ([(Expr, Expr)] -> [(Expr, Expr)])
-> [(Expr, Expr)] -> [(Expr, Expr)]
forall a b. (a -> b) -> a -> b
$ (Expr, Expr) -> [(Expr, Expr)]
canonicalVariationsEqn (Expr
e1,Expr
e2)
  where
  isInstanceOf' :: (Expr, Expr) -> (Expr, Expr) -> Bool
isInstanceOf'  =  Expr -> Expr -> Bool
isInstanceOf (Expr -> Expr -> Bool)
-> ((Expr, Expr) -> Expr) -> (Expr, Expr) -> (Expr, Expr) -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Expr, Expr) -> Expr
foldPair
  filterRelevant :: [(Expr, Expr)] -> [(Expr, Expr)]
filterRelevant []      =  []
  filterRelevant ((Expr, Expr)
e:[(Expr, Expr)]
es)
    | (Expr -> Expr -> Bool) -> (Expr, Expr) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Expr -> Expr -> Bool
(===) (Expr, Expr)
e    =  (Expr, Expr)
e (Expr, Expr) -> [(Expr, Expr)] -> [(Expr, Expr)]
forall a. a -> [a] -> [a]
: [(Expr, Expr)] -> [(Expr, Expr)]
filterRelevant (((Expr, Expr) -> Bool) -> [(Expr, Expr)] -> [(Expr, Expr)]
forall a. (a -> Bool) -> [a] -> [a]
discard ((Expr, Expr) -> (Expr, Expr) -> Bool
`isInstanceOf'` (Expr, Expr)
e) [(Expr, Expr)]
es)
    | Bool
otherwise          =  [(Expr, Expr)] -> [(Expr, Expr)]
filterRelevant [(Expr, Expr)]
es

semiTheoryFromThyAndReps :: Instances -> Int -> Int
                         -> Thy -> [Expr] -> Shy
semiTheoryFromThyAndReps :: [Expr] -> Int -> Int -> Thy -> [Expr] -> Shy
semiTheoryFromThyAndReps [Expr]
ti Int
nt Int
nv Thy
thy =
    Thy -> [(Expr, Expr)] -> Shy
stheorize Thy
thy
  ([(Expr, Expr)] -> Shy)
-> ([Expr] -> [(Expr, Expr)]) -> [Expr] -> Shy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Expr -> Bool) -> [Expr] -> [(Expr, Expr)]
forall a. (a -> a -> Bool) -> [a] -> [(a, a)]
pairsThat (\Expr
e1 Expr
e2 -> Expr
e1 Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
/= Expr
e2
                      Bool -> Bool -> Bool
&& Expr -> TypeRep
typ Expr
e1 TypeRep -> TypeRep -> Bool
forall a. Eq a => a -> a -> Bool
== Expr -> TypeRep
typ Expr
e2
                      Bool -> Bool -> Bool
&& [Expr] -> Int -> Expr -> Expr -> Bool
lessOrEqual [Expr]
ti Int
nt Expr
e1 Expr
e2)
  ([Expr] -> [(Expr, Expr)])
-> ([Expr] -> [Expr]) -> [Expr] -> [(Expr, Expr)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> Int -> Int -> Thy -> [Expr] -> [Expr]
distinctFromSchemas [Expr]
ti Int
nt Int
nv Thy
thy
  ([Expr] -> [Expr]) -> ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
filter ([Expr] -> Expr -> Bool
isOrd [Expr]
ti)

conditionalTheoryFromThyAndReps :: Instances
                                -> Int -> Int -> Int
                                -> Thy -> [Expr] -> Chy
conditionalTheoryFromThyAndReps :: [Expr] -> Int -> Int -> Int -> Thy -> [Expr] -> Chy
conditionalTheoryFromThyAndReps [Expr]
ti Int
nt Int
nv Int
csz Thy
thy [Expr]
es' =
  ((Expr, Expr, Expr) -> Bool)
-> (Expr -> Expr -> Expr -> Bool)
-> (Expr -> Expr -> Bool)
-> Int
-> Thy
-> [Class Expr]
-> [Class Expr]
-> Chy
conditionalEquivalences
    ((Expr -> Expr -> Ordering) -> [Expr] -> (Expr, Expr, Expr) -> Bool
canonicalCEqnBy (Thy -> Expr -> Expr -> Ordering
compareE Thy
thy) [Expr]
ti)
    ([Expr] -> Int -> Expr -> Expr -> Expr -> Bool
condEqual [Expr]
ti Int
nt)
    ([Expr] -> Int -> Expr -> Expr -> Bool
lessOrEqual [Expr]
ti Int
nt)
    Int
csz Thy
thy [Class Expr]
clpres [Class Expr]
cles
  where
  ([Class Expr]
cles,[Class Expr]
clpres) = ([Class Expr] -> [Class Expr])
-> ([Class Expr], [Class Expr]) -> ([Class Expr], [Class Expr])
forall b b' a. (b -> b') -> (a, b) -> (a, b')
second ((Class Expr -> Bool) -> [Class Expr] -> [Class Expr]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Expr
e,[Expr]
_) -> Expr -> Int
size Expr
e Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
csz))
                (([Class Expr], [Class Expr]) -> ([Class Expr], [Class Expr]))
-> ([Class Expr] -> ([Class Expr], [Class Expr]))
-> [Class Expr]
-> ([Class Expr], [Class Expr])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Class Expr -> Bool)
-> [Class Expr] -> ([Class Expr], [Class Expr])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\(Expr
e,[Expr]
_) -> Expr -> TypeRep
typ Expr
e TypeRep -> TypeRep -> Bool
forall a. Eq a => a -> a -> Bool
/= TypeRep
boolTy)
                ([Class Expr] -> ([Class Expr], [Class Expr]))
-> ([Class Expr] -> [Class Expr])
-> [Class Expr]
-> ([Class Expr], [Class Expr])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Class Expr -> Bool) -> [Class Expr] -> [Class Expr]
forall a. (a -> Bool) -> [a] -> [a]
filter ([Expr] -> Expr -> Bool
isEq [Expr]
ti (Expr -> Bool) -> (Class Expr -> Expr) -> Class Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Class Expr -> Expr
forall a b. (a, b) -> a
fst)
                ([Class Expr] -> ([Class Expr], [Class Expr]))
-> [Class Expr] -> ([Class Expr], [Class Expr])
forall a b. (a -> b) -> a -> b
$ [Expr] -> Int -> Int -> Thy -> [Expr] -> [Class Expr]
classesFromSchemas [Expr]
ti Int
nt Int
nv Thy
thy [Expr]
es'

conditionalEquivalences :: ((Expr,Expr,Expr) -> Bool)
                        -> (Expr -> Expr -> Expr -> Bool)
                        -> (Expr -> Expr -> Bool)
                        -> Int -> Thy -> [Class Expr] -> [Class Expr] -> Chy
conditionalEquivalences :: ((Expr, Expr, Expr) -> Bool)
-> (Expr -> Expr -> Expr -> Bool)
-> (Expr -> Expr -> Bool)
-> Int
-> Thy
-> [Class Expr]
-> [Class Expr]
-> Chy
conditionalEquivalences (Expr, Expr, Expr) -> Bool
canon Expr -> Expr -> Expr -> Bool
cequal Expr -> Expr -> Bool
(==>) Int
csz Thy
thy [Class Expr]
clpres [Class Expr]
cles =
    ((Expr, Expr, Expr) -> Bool) -> Chy -> Chy
cdiscard (\(Expr
ce,Expr
e1,Expr
e2) -> Thy -> [Class Expr] -> Expr -> Expr -> Expr -> Bool
subConsequence Thy
thy [Class Expr]
clpres Expr
ce Expr
e1 Expr
e2)
  (Chy -> Chy)
-> ([(Expr, Expr, Expr)] -> Chy) -> [(Expr, Expr, Expr)] -> Chy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Chy -> (Expr, Expr, Expr) -> Chy)
-> Chy -> [(Expr, Expr, Expr)] -> Chy
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (((Expr, Expr, Expr) -> Chy -> Chy)
-> Chy -> (Expr, Expr, Expr) -> Chy
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Expr, Expr, Expr) -> Chy -> Chy
cinsert) ([(Expr, Expr, Expr)] -> [Class Expr] -> [Class Expr] -> Thy -> Chy
Chy [] [Class Expr]
cdg [Class Expr]
clpres Thy
thy)
  ([(Expr, Expr, Expr)] -> Chy)
-> ([(Expr, Expr, Expr)] -> [(Expr, Expr, Expr)])
-> [(Expr, Expr, Expr)]
-> Chy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Expr, Expr, Expr) -> (Expr, Expr, Expr) -> Ordering)
-> [(Expr, Expr, Expr)] -> [(Expr, Expr, Expr)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Thy -> Expr -> Expr -> Ordering
compareE Thy
thy (Expr -> Expr -> Ordering)
-> ((Expr, Expr, Expr) -> Expr)
-> (Expr, Expr, Expr)
-> (Expr, Expr, Expr)
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Expr, Expr, Expr) -> Expr
foldTrio)
  ([(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) -> Bool)
-> [(Expr, Expr, Expr)] -> [(Expr, Expr, Expr)]
forall a. (a -> Bool) -> [a] -> [a]
discard (\(Expr
pre,Expr
e1,Expr
e2) -> Expr
pre Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Expr
forall a. (Typeable a, Show a) => a -> Expr
val Bool
False
                          Bool -> Bool -> Bool
|| Bool -> Bool
not ([Expr] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Expr -> [Expr]
nubVars Expr
pre [Expr] -> [Expr] -> [Expr]
forall a. Eq a => [a] -> [a] -> [a]
\\ (Expr -> [Expr]
nubVars Expr
e1 [Expr] -> [Expr] -> [Expr]
forall a. Ord a => [a] -> [a] -> [a]
+++ Expr -> [Expr]
nubVars Expr
e2)))
                          Bool -> Bool -> Bool
|| Thy -> [Class Expr] -> Expr -> Expr -> Expr -> Bool
subConsequence Thy
thy [] Expr
pre Expr
e1 Expr
e2)
  ([(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) -> Bool)
-> [(Expr, Expr, Expr)] -> [(Expr, Expr, Expr)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Expr, Expr, Expr) -> Bool
canon
  ([(Expr, Expr, Expr)] -> Chy) -> [(Expr, Expr, Expr)] -> Chy
forall a b. (a -> b) -> a -> b
$ [ (Expr
ce, Expr
e1, Expr
e2)
    | Expr
e1 <- [Expr]
es, Expr
e2 <- [Expr]
es, Expr
e1 Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
/= Expr
e2, (Expr, Expr, Expr) -> Bool
canon (Bool -> Expr
forall a. (Typeable a, Show a) => a -> Expr
val Bool
False,Expr
e1,Expr
e2)
    , Expr -> TypeRep
typ Expr
e1 TypeRep -> TypeRep -> Bool
forall a. Eq a => a -> a -> Bool
== Expr -> TypeRep
typ Expr
e2, Expr -> TypeRep
typ Expr
e1 TypeRep -> TypeRep -> Bool
forall a. Eq a => a -> a -> Bool
/= TypeRep
boolTy
    , Expr
ce <- Expr -> Expr -> [Expr]
explain Expr
e1 Expr
e2
    ]
  where
  ([Expr]
es,[Expr]
pres) = ((Class Expr -> Expr) -> [Class Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Class Expr -> Expr
forall a. Class a -> a
C.rep [Class Expr]
cles, (Class Expr -> Expr) -> [Class Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Class Expr -> Expr
forall a. Class a -> a
C.rep [Class Expr]
clpres)
  explain :: Expr -> Expr -> [Expr]
explain Expr
e1 Expr
e2 = (Expr -> Bool) -> [Class Expr] -> [Expr]
forall a. Eq a => (a -> Bool) -> Digraph a -> [a]
D.narrow (\Expr
ep -> Expr -> Expr -> Expr -> Bool
cequal Expr
ep Expr
e1 Expr
e2) [Class Expr]
cdg
  cdg :: [Class Expr]
cdg = [(Expr, Expr)] -> [Class Expr]
forall a. Ord a => [(a, a)] -> Digraph a
D.fromEdges
      ([(Expr, Expr)] -> [Class Expr])
-> ([Expr] -> [(Expr, Expr)]) -> [Expr] -> [Class Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Expr -> Bool) -> [Expr] -> [(Expr, Expr)]
forall a. (a -> a -> Bool) -> [a] -> [(a, a)]
pairsThat Expr -> Expr -> Bool
(==>)
      ([Expr] -> [Class Expr]) -> [Expr] -> [Class Expr]
forall a b. (a -> b) -> a -> b
$ (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
filter (\Expr
e -> Expr -> TypeRep
typ Expr
e TypeRep -> TypeRep -> Bool
forall a. Eq a => a -> a -> Bool
== TypeRep
boolTy Bool -> Bool -> Bool
&& Bool -> Bool
not (Expr -> Bool
isAssignment Expr
e)) [Expr]
pres

-- | Is the equation a consequence of substitution?
-- > subConsequence (x == y) (x + y) (x + x) == True
-- > subConsequence (x <= y) (x + y) (x + x) == False -- not sub
-- > subConsequence (abs x == abs y) (abs x) (abs y) == True
-- > subConsequence (abs x == 1) (x + abs x) (20) == False (artificial)
subConsequence :: Thy -> [Class Expr] -> Expr -> Expr -> Expr -> Bool
subConsequence :: Thy -> [Class Expr] -> Expr -> Expr -> Expr -> Bool
subConsequence Thy
thy [Class Expr]
clpres ((Value String
"==" Dynamic
_ :$ Expr
ea) :$ Expr
eb) Expr
e1 Expr
e2
  -- NOTE: the first 4 are uneeded, but make it a bit faster...
  | Expr
ea Expr -> Expr -> Bool
`isSubexprOf` Expr
e1 Bool -> Bool -> Bool
&& Thy -> Expr -> Expr -> Bool
equivalent Thy
thy{closureLimit=1} (Expr
e1 Expr -> (Expr, Expr) -> Expr
/ (Expr
ea,Expr
eb)) Expr
e2 = Bool
True
  | Expr
eb Expr -> Expr -> Bool
`isSubexprOf` Expr
e1 Bool -> Bool -> Bool
&& Thy -> Expr -> Expr -> Bool
equivalent Thy
thy{closureLimit=1} (Expr
e1 Expr -> (Expr, Expr) -> Expr
/ (Expr
eb,Expr
ea)) Expr
e2 = Bool
True
  | Expr
ea Expr -> Expr -> Bool
`isSubexprOf` Expr
e2 Bool -> Bool -> Bool
&& Thy -> Expr -> Expr -> Bool
equivalent Thy
thy{closureLimit=1} (Expr
e2 Expr -> (Expr, Expr) -> Expr
/ (Expr
ea,Expr
eb)) Expr
e1 = Bool
True
  | Expr
eb Expr -> Expr -> Bool
`isSubexprOf` Expr
e2 Bool -> Bool -> Bool
&& Thy -> Expr -> Expr -> Bool
equivalent Thy
thy{closureLimit=1} (Expr
e2 Expr -> (Expr, Expr) -> Expr
/ (Expr
eb,Expr
ea)) Expr
e1 = Bool
True
  | Thy -> Expr -> Expr -> Bool
equivalent ((Expr
ea,Expr
eb) (Expr, Expr) -> Thy -> Thy
`insert` Thy
thy){closureLimit=1} Expr
e1 Expr
e2 = Bool
True
  where
  Expr
e / :: Expr -> (Expr, Expr) -> Expr
/ (Expr
e1,Expr
e2)  =  Expr
e Expr -> [(Expr, Expr)] -> Expr
// [(Expr
e1,Expr
e2)]
subConsequence Thy
thy [Class Expr]
clpres Expr
ce Expr
e1 Expr
e2 = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or
  [ Thy -> [Class Expr] -> Expr -> Expr -> Expr -> Bool
subConsequence Thy
thy [Class Expr]
clpres Expr
ce' Expr
e1 Expr
e2
  | (Expr
rce,[Expr]
ces) <- [Class Expr]
clpres, Expr
ce Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
rce, Expr
ce' <- [Expr]
ces ]

psortBy :: (a -> a -> Bool) -> [a] -> [(a,a)]
psortBy :: forall a. (a -> a -> Bool) -> [a] -> [(a, a)]
psortBy a -> a -> Bool
(<) [a]
xs = [(a
x,a
y) | a
x <- [a]
xs, a
y <- [a]
xs, a
x a -> a -> Bool
< a
y, (a -> Bool) -> [a] -> Bool
forall a. (a -> Bool) -> [a] -> Bool
none (\a
z -> a
x a -> a -> Bool
< a
z Bool -> Bool -> Bool
&& a
z a -> a -> Bool
< a
y) [a]
xs]