-- |
-- Module      : Test.Speculate.Misc
-- 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.
--
-- Inequational (or semi-equational) reasoning.
module Test.Speculate.SemiReason where

import Test.Speculate.Expr
import Test.Speculate.Reason
import Test.Speculate.Utils
import Data.List as L (sortBy, delete)
import Data.Function (on)

type Equation = (Expr, Expr)
-- Maybe (Bool, Expr, Expr)?  where bool tells if it is strict

data Shy = Shy
  { Shy -> [Equation]
sequations  :: [Equation] -- <='s
--, ssequations :: [Equation] -- <'s -- LATER!
  , Shy -> Thy
sthy :: Thy
  }

emptyShy :: Shy
emptyShy :: Shy
emptyShy = Shy :: [Equation] -> Thy -> Shy
Shy
  { sequations :: [Equation]
sequations = []
  , sthy :: Thy
sthy = Thy
emptyThy
  }

updateSemiEquationsBy :: ([Equation] -> [Equation]) -> Shy -> Shy
updateSemiEquationsBy :: ([Equation] -> [Equation]) -> Shy -> Shy
updateSemiEquationsBy [Equation] -> [Equation]
f shy :: Shy
shy@Shy {sequations :: Shy -> [Equation]
sequations = [Equation]
es} = Shy
shy {sequations :: [Equation]
sequations = [Equation] -> [Equation]
f [Equation]
es}

mapSemiEquations :: (Equation -> Equation) -> Shy -> Shy
mapSemiEquations :: (Equation -> Equation) -> Shy -> Shy
mapSemiEquations = ([Equation] -> [Equation]) -> Shy -> Shy
updateSemiEquationsBy (([Equation] -> [Equation]) -> Shy -> Shy)
-> ((Equation -> Equation) -> [Equation] -> [Equation])
-> (Equation -> Equation)
-> Shy
-> Shy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Equation -> Equation) -> [Equation] -> [Equation]
forall a b. (a -> b) -> [a] -> [b]
map

scompareE :: Shy -> (Expr -> Expr -> Ordering)
scompareE :: Shy -> Expr -> Expr -> Ordering
scompareE = Thy -> Expr -> Expr -> Ordering
compareE (Thy -> Expr -> Expr -> Ordering)
-> (Shy -> Thy) -> Shy -> Expr -> Expr -> Ordering
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Shy -> Thy
sthy

lesser  :: Shy -> Expr -> [Expr]
lesser :: Shy -> Expr -> [Expr]
lesser  Shy
shy Expr
e = [ Expr
e1 | (Expr
e1,Expr
e2) <- Shy -> [Equation]
sequations Shy
shy, Expr
e Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
e2 ]

greater :: Shy -> Expr -> [Expr]
greater :: Shy -> Expr -> [Expr]
greater Shy
shy Expr
e = [ Expr
e2 | (Expr
e1,Expr
e2) <- Shy -> [Equation]
sequations Shy
shy, Expr
e Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
e1 ]

-- | given a semi-equation (inequality),
--   simplerThan restricts the Shy (SemiTheory)
--   into only equations simpler
--   than the given semi-equation
--   or that are instances of simpler equations.
--
-- half-baked example:
--
-- @x + 1@ is simpler than @x + y@ and it is returned.
-- @(1 + 1) + 1@ is more complex than @x + y@
-- but it is returned as well as it is an instance of @x + 1@.
simplerThan :: Equation -> Shy -> Shy
simplerThan :: Equation -> Shy -> Shy
simplerThan Equation
seq = ([Equation] -> [Equation]) -> Shy -> Shy
updateSEquationsBy [Equation] -> [Equation]
upd
  where
  isSEInstanceOf :: Equation -> Equation -> Bool
isSEInstanceOf = Expr -> Expr -> Bool
isInstanceOf (Expr -> Expr -> Bool)
-> (Equation -> Expr) -> Equation -> Equation -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Equation -> Expr
foldPair
  upd :: [Equation] -> [Equation]
upd [Equation]
eqs = [Equation]
r [Equation] -> [Equation] -> [Equation]
forall a. [a] -> [a] -> [a]
++ [Equation
seq' | Equation
seq' <- [Equation]
r'
                       , (Equation -> Bool) -> [Equation] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Equation
seq' Equation -> Equation -> Bool
`isSEInstanceOf`) [Equation]
r ]
    where
    r :: [Equation]
r  =          (Equation -> Bool) -> [Equation] -> [Equation]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Equation -> Equation -> Bool
forall a. Eq a => a -> a -> Bool
/= Equation
seq) [Equation]
eqs
    r' :: [Equation]
r' = Int -> [Equation] -> [Equation]
forall a. Int -> [a] -> [a]
drop Int
1 ([Equation] -> [Equation]) -> [Equation] -> [Equation]
forall a b. (a -> b) -> a -> b
$ (Equation -> Bool) -> [Equation] -> [Equation]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Equation -> Equation -> Bool
forall a. Eq a => a -> a -> Bool
/= Equation
seq) [Equation]
eqs
-- simplerThan used to be just:
-- simplerThan seq = updateSEquationsBy (takeWhile (/= seq))

transConsequence :: Shy -> Equation -> Bool
transConsequence :: Shy -> Equation -> Bool
transConsequence Shy
shy (Expr
e1,Expr
e2) = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [ Expr
e1' Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
e2'
                                  | Expr
e1' <- Expr -> [Expr] -> [Expr]
forall a. Eq a => a -> [a] -> [a]
L.delete Expr
e2 ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$ Shy -> Expr -> [Expr]
greater Shy
shy' Expr
e1
                                  , Expr
e2' <- Expr -> [Expr] -> [Expr]
forall a. Eq a => a -> [a] -> [a]
L.delete Expr
e1 ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$ Shy -> Expr -> [Expr]
lesser  Shy
shy' Expr
e2
                                  ]
  where
  shy' :: Shy
shy' = Equation -> Shy -> Shy
simplerThan (Expr
e1,Expr
e2) Shy
shy

updateSEquationsBy :: ([Equation] -> [Equation]) -> Shy -> Shy
updateSEquationsBy :: ([Equation] -> [Equation]) -> Shy -> Shy
updateSEquationsBy [Equation] -> [Equation]
f shy :: Shy
shy@Shy{sequations :: Shy -> [Equation]
sequations = [Equation]
seqs} = Shy
shy{sequations :: [Equation]
sequations = [Equation] -> [Equation]
f [Equation]
seqs}

stheorize :: Thy -> [Equation] -> Shy
stheorize :: Thy -> [Equation] -> Shy
stheorize Thy
thy [Equation]
seqs =
  Shy :: [Equation] -> Thy -> Shy
Shy{ sequations :: [Equation]
sequations = (Equation -> Equation -> Ordering) -> [Equation] -> [Equation]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Thy -> Expr -> Expr -> Ordering
compareE Thy
thy (Expr -> Expr -> Ordering)
-> (Equation -> Expr) -> Equation -> Equation -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Equation -> Expr
foldPair) [Equation]
seqs
     , sthy :: Thy
sthy = Thy
thy
     }

-- list all equation sides in a Shy
sides :: Shy -> [Expr]
sides :: Shy -> [Expr]
sides Shy
shy = (Expr -> Expr -> Ordering) -> [Expr] -> [Expr]
forall a. (a -> a -> Ordering) -> [a] -> [a]
nubSortBy (Shy -> Expr -> Expr -> Ordering
scompareE Shy
shy)
          ([Expr] -> [Expr])
-> ([Equation] -> [Expr]) -> [Equation] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Equation -> [Expr]) -> [Equation] -> [Expr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(Expr
e1,Expr
e2) -> [Expr
e1,Expr
e2])
          ([Equation] -> [Expr]) -> [Equation] -> [Expr]
forall a b. (a -> b) -> a -> b
$ Shy -> [Equation]
sequations Shy
shy

finalSemiEquations :: (Equation -> Bool) -> Instances -> (Expr -> Expr -> Bool) -> Shy -> [Equation]
finalSemiEquations :: (Equation -> Bool)
-> [Expr] -> (Expr -> Expr -> Bool) -> Shy -> [Equation]
finalSemiEquations Equation -> Bool
shouldShow [Expr]
insts Expr -> Expr -> Bool
equivalentInstanceOf Shy
shy =
    (Equation -> Equation -> Ordering) -> [Equation] -> [Equation]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (TypeRep -> TypeRep -> Ordering
compareTy (TypeRep -> TypeRep -> Ordering)
-> (Equation -> TypeRep) -> Equation -> Equation -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Expr -> TypeRep
typ (Expr -> TypeRep) -> (Equation -> Expr) -> Equation -> TypeRep
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Equation -> Expr
forall a b. (a, b) -> a
fst))
  ([Equation] -> [Equation])
-> (Shy -> [Equation]) -> Shy -> [Equation]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Equation -> Bool) -> [Equation] -> [Equation]
forall a. (a -> Bool) -> [a] -> [a]
filter Equation -> Bool
shouldShow
  ([Equation] -> [Equation])
-> (Shy -> [Equation]) -> Shy -> [Equation]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Equation -> Equation -> Bool) -> [Equation] -> [Equation]
forall a. (a -> a -> Bool) -> [a] -> [a]
discardLater (Expr -> Expr -> Bool
equivalentInstanceOf (Expr -> Expr -> Bool)
-> (Equation -> Expr) -> Equation -> Equation -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Equation -> Expr
foldPair)
  ([Equation] -> [Equation])
-> (Shy -> [Equation]) -> Shy -> [Equation]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Equation -> Bool) -> [Equation] -> [Equation]
forall a. (a -> Bool) -> [a] -> [a]
discard (Shy -> Equation -> Bool
transConsequence Shy
shy)
  ([Equation] -> [Equation])
-> (Shy -> [Equation]) -> Shy -> [Equation]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Equation -> Equation -> Bool) -> [Equation] -> [Equation]
forall a. (a -> a -> Bool) -> [a] -> [a]
discardLater (Expr -> Expr -> Bool
isInstanceOf (Expr -> Expr -> Bool)
-> (Equation -> Expr) -> Equation -> Equation -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Equation -> Expr
foldPair)
  ([Equation] -> [Equation])
-> (Shy -> [Equation]) -> Shy -> [Equation]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Shy -> [Equation]
sequations
  (Shy -> [Equation]) -> Shy -> [Equation]
forall a b. (a -> b) -> a -> b
$ [Expr] -> Shy -> Shy
canonicalizeShyWith [Expr]
insts Shy
shy

canonicalizeShyWith :: Instances -> Shy -> Shy
canonicalizeShyWith :: [Expr] -> Shy -> Shy
canonicalizeShyWith = (Equation -> Equation) -> Shy -> Shy
mapSemiEquations ((Equation -> Equation) -> Shy -> Shy)
-> ([Expr] -> Equation -> Equation) -> [Expr] -> Shy -> Shy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> Equation -> Equation
canonicalizeSemiEquationWith

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