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)
data Shy = Shy
{ sequations :: [Equation]
, sthy :: Thy
}
emptyShy :: Shy
emptyShy = Shy
{ sequations = []
, sthy = emptyThy
}
updateSemiEquationsBy :: ([Equation] -> [Equation]) -> Shy -> Shy
updateSemiEquationsBy f shy@Shy {sequations = es} = shy {sequations = f es}
mapSemiEquations :: (Equation -> Equation) -> Shy -> Shy
mapSemiEquations = updateSemiEquationsBy . map
scompareE :: Shy -> (Expr -> Expr -> Ordering)
scompareE = compareE . sthy
lesser :: Shy -> Expr -> [Expr]
lesser shy e = [ e1 | (e1,e2) <- sequations shy, e == e2 ]
greater :: Shy -> Expr -> [Expr]
greater shy e = [ e2 | (e1,e2) <- sequations shy, e == e1 ]
simplerThan :: Equation -> Shy -> Shy
simplerThan seq = updateSEquationsBy upd
where
isSEInstanceOf = isInstanceOf `on` foldPair
upd eqs = r ++ [seq' | seq' <- r'
, any (seq' `isSEInstanceOf`) r ]
where
r = takeWhile (/= seq) eqs
r' = drop 1 $ dropWhile (/= seq) eqs
transConsequence :: Shy -> Equation -> Bool
transConsequence shy (e1,e2) = or [ e1' == e2'
| e1' <- L.delete e2 $ greater shy' e1
, e2' <- L.delete e1 $ lesser shy' e2
]
where
shy' = simplerThan (e1,e2) shy
updateSEquationsBy :: ([Equation] -> [Equation]) -> Shy -> Shy
updateSEquationsBy f shy@Shy{sequations = seqs} = shy{sequations = f seqs}
stheorize :: Thy -> [Equation] -> Shy
stheorize thy seqs =
Shy{ sequations = sortBy (compareE thy `on` foldPair) seqs
, sthy = thy
}
sides :: Shy -> [Expr]
sides shy = nubSortBy (scompareE shy)
. concatMap (\(e1,e2) -> [e1,e2])
$ sequations shy
finalSemiEquations :: (Equation -> Bool) -> Instances -> (Expr -> Expr -> Bool) -> Shy -> [Equation]
finalSemiEquations shouldShow insts equivalentInstanceOf shy =
sortBy (compareTy `on` (typ . fst))
. filter shouldShow
. discardLater (equivalentInstanceOf `on` foldPair)
. discard (transConsequence shy)
. discardLater (isInstanceOf `on` foldPair)
. sequations
$ canonicalizeShyWith insts shy
canonicalizeShyWith :: Instances -> Shy -> Shy
canonicalizeShyWith = mapSemiEquations . canonicalizeSemiEquationWith
canonicalizeSemiEquationWith :: Instances -> Equation -> Equation
canonicalizeSemiEquationWith is (e1,e2) =
case canonicalizeWith (lookupNames is) (e1 :$ e2) of
e1' :$ e2' -> (e1',e2')
_ -> error $ "canonicalizeShyWith: the impossible happened,"
++ "this is definitely a bug, see source!"