{-# LANGUAGE BangPatterns, OverloadedStrings, PartialTypeSignatures, ScopedTypeVariables, TypeSynonymInstances, FlexibleInstances, FlexibleContexts #-}
module Main where
import Data.Aeson
import qualified Data.ByteString as B
import qualified Data.ByteString.Lazy as LB
import Data.Char
import Data.List
import Data.Maybe
import qualified Data.Sequence as Seq
import qualified Data.Stringable as S
import qualified Data.String as DS
import Data.String.Utils
import Data.Text.Encoding
import Data.Typeable
import qualified Language.Haskell.Exts.Parser as HSE.Parser
import qualified Language.Haskell.Exts.Syntax as HSE.Syntax
import Algebra.Equation.Internal
import Algebra.Equation.Reduce
import Numeric.Natural
import System.Directory
import System.IO.Unsafe
import Test.QuickCheck
import Test.QuickCheck.Monadic
import qualified Test.QuickSpec.Equation
import qualified Test.QuickSpec.Generate
import qualified Test.QuickSpec.Main
import qualified Test.QuickSpec.Reasoning.CongruenceClosure
import qualified Test.QuickSpec.Reasoning.NaiveEquationalReasoning
import qualified Test.QuickSpec.Signature
import qualified Test.QuickSpec.TestTree
import qualified Test.QuickSpec.Utils.Typeable
import qualified Test.QuickSpec.Utils.Typed
import qualified Test.QuickSpec.Utils.TypeMap
import qualified Test.QuickSpec.Term
import Test.Tasty (defaultMain, testGroup, localOption)
import Test.Tasty.QuickCheck
main = defaultMain $ testGroup "All tests" [
testProperty "Can parse equations" canParseEquations
, testProperty "Can parse terms" canParseTerms
, testProperty "Can parse variables" canParseVars
, testProperty "Can parse constants" canParseConsts
, testProperty "Can parse examples" canParseExamples
, testProperty "Can evaluate examples" canEvalExamples
, testProperty "Can make example signature" canMakeSignature
, testProperty "Constants added" constantsAdded
, testProperty "Variables added" variablesAdded
, testProperty "Sigs render" sigsRender
, testProperty "Sigs have constants" sigsHaveConsts
, testProperty "Sigs have variables" sigsHaveVars
, testProperty "Constants are distinct" sigConstsUniqueIndices
, testProperty "Variables are distinct" sigVarsUniqueIndices
, testProperty "Can find closure of term" canFindClosure
, testProperty "No classes without equations" noClassesFromEmptyEqs
, testProperty "Equation induces a class" getClassFromEq
, testProperty "Classes contain given terms" classesHaveTerms
, testProperty "Equal terms in same class" eqPartsAppearInSameClass
, testProperty "Terms appear in one class" classesHaveNoDupes
, testProperty "Class elements are equal" classElementsAreEqual
, testProperty "Non-equal elements separate" nonEqualElementsSeparate
, testProperty "Classes have one arity" classHasSameArity
, testProperty "Class length more than one" classesNotSingletons
, testProperty "Can get classes from sig" canGetClassesFromEqs
, testProperty "Can get sig from equations" canGetSigFromEqs
, testProperty "Sig has equation variables" eqSigHasVars
, testProperty "Sig has equation constants" eqSigHasConsts
, testProperty "Equations have one arity" equationsHaveSameArity
, testProperty "Can get type of terms" canGetTermType
, testProperty "No trivial terms" noTrivialTerms
, testProperty "Equations are consistent" eqsAreConsistent
, testProperty "Switch function types" switchFunctionTypes
, testProperty "Can prune equations" canPruneEqs
, testProperty "Type parsing regression" regressionTypeParse
, testProperty "Nat example has eqs" natHasEqs
, testProperty "Nat example outputs eqs" natKeepsEqs
, testProperty "Nat classes are nontrivial" natClassesNontrivial
, testProperty "Commutativity is nontrivial" commClassesNontrivial
, testProperty "Nat equations are pruned" natEqsPruned
, testProperty "Reduction matches QuickSpec" natEqsMatchQS
, testProperty "Replacement types unique" extractedTypesUnique
, testProperty "QuickSpec conversions invert" convertTypesIso
, testProperty "Symmetric equations equal" eqsSymmetric
, testProperty "Spot symmetric equations" eqsSetEq
, testProperty "Can generate eq variables" canMakeVars
, testProperty "Can generate var QS sigs" canMakeQSSigs
, testProperty "Can find vars in sig" lookupVars
, testProperty "Can prune" justPrune
, testProperty "New reduce" newReduce
, testProperty "Reduce is idempotent" reduceIdem
, testProperty "Redundant transitivity" transStripped
, testProperty "Generated terms have type" termsHaveType
, testProperty "Manual Nat finds eqs" manualNatFindsEqs
, testProperty "Fresh sig + parsed eqs works" manualNatAllowsGiven
, testProperty "Fresh classes match parsed" manualNatClassesMatch
, testProperty "Fresh classes have parsed terms" topNatTermsFound
, testProperty "Parsed classes have fresh terms" qsNatTermsFound
, testProperty "Singleton classes generated" natClassesIncludeSingletons
, testProperty "Class contents match exactly" exactClassMatch
, testProperty "Pruned eqs match" parsedEqsPrune
, testProperty "Fresh Nat reduces own eqs" manualNatReducesSelf
]
-- Tests
canParseEquations = all try [
"{\"relation\":\"~=\",\"lhs\":{\"role\":\"application\",\"lhs\":{\"role\":\"application\",\"lhs\":{\"role\":\"constant\",\"type\":\"[Integer] -> [Integer] -> Ordering\",\"symbol\":\"lengthCompare\"},\"rhs\":{\"role\":\"variable\",\"type\":\"[Integer]\",\"id\":7}},\"rhs\":{\"role\":\"variable\",\"type\":\"[Integer]\",\"id\":7}},\"rhs\":{\"role\":\"application\",\"lhs\":{\"role\":\"application\",\"lhs\":{\"role\":\"constant\",\"type\":\"[Integer] -> [Integer] -> Ordering\",\"symbol\":\"lengthCompare\"},\"rhs\":{\"role\":\"variable\",\"type\":\"[Integer]\",\"id\":6}},\"rhs\":{\"role\":\"variable\",\"type\":\"[Integer]\",\"id\":6}}}",
"{\"relation\":\"~=\",\"lhs\":{\"role\":\"application\",\"lhs\":{\"role\":\"application\",\"lhs\":{\"role\":\"constant\",\"type\":\"[Integer] -> [Integer] -> Ordering\",\"symbol\":\"lengthCompare\"},\"rhs\":{\"role\":\"variable\",\"type\":\"[Integer]\",\"id\":8}},\"rhs\":{\"role\":\"variable\",\"type\":\"[Integer]\",\"id\":8}},\"rhs\":{\"role\":\"application\",\"lhs\":{\"role\":\"application\",\"lhs\":{\"role\":\"constant\",\"type\":\"[Integer] -> [Integer] -> Ordering\",\"symbol\":\"lengthCompare\"},\"rhs\":{\"role\":\"variable\",\"type\":\"[Integer]\",\"id\":6}},\"rhs\":{\"role\":\"variable\",\"type\":\"[Integer]\",\"id\":6}}}"
]
where try x = case decode x of
Nothing -> False
Just (Eq l r) -> True
canParseTerms = all try [
"{\"role\":\"constant\",\"type\":\"[Integer] -> [Integer] -> Ordering\",\"symbol\":\"lengthCompare\"}",
"{\"role\":\"variable\",\"type\":\"[Integer]\",\"id\":7}",
"{\"role\":\"variable\",\"type\":\"[Integer]\",\"id\":6}",
"{\"role\":\"variable\",\"type\":\"[Integer]\",\"id\":8}",
"{\"role\":\"application\",\"lhs\":{\"role\":\"constant\",\"type\":\"[Integer] -> [Integer] -> Ordering\",\"symbol\":\"lengthCompare\"},\"rhs\":{\"role\":\"variable\",\"type\":\"[Integer]\",\"id\":7}}",
"{\"role\":\"application\",\"lhs\":{\"role\":\"constant\",\"type\":\"[Integer] -> [Integer] -> Ordering\",\"symbol\":\"lengthCompare\"},\"rhs\":{\"role\":\"variable\",\"type\":\"[Integer]\",\"id\":6}}",
"{\"role\":\"application\",\"lhs\":{\"role\":\"constant\",\"type\":\"[Integer] -> [Integer] -> Ordering\",\"symbol\":\"lengthCompare\"},\"rhs\":{\"role\":\"variable\",\"type\":\"[Integer]\",\"id\":8}}",
"{\"role\":\"application\",\"lhs\":{\"role\":\"constant\",\"type\":\"[Integer] -> [Integer] -> Ordering\",\"symbol\":\"lengthCompare\"},\"rhs\":{\"role\":\"variable\",\"type\":\"[Integer]\",\"id\":6}}",
"{\"role\":\"application\",\"lhs\":{\"role\":\"application\",\"lhs\":{\"role\":\"constant\",\"type\":\"[Integer] -> [Integer] -> Ordering\",\"symbol\":\"lengthCompare\"},\"rhs\":{\"role\":\"variable\",\"type\":\"[Integer]\",\"id\":7}},\"rhs\":{\"role\":\"variable\",\"type\":\"[Integer]\",\"id\":7}}",
"{\"role\":\"application\",\"lhs\":{\"role\":\"application\",\"lhs\":{\"role\":\"constant\",\"type\":\"[Integer] -> [Integer] -> Ordering\",\"symbol\":\"lengthCompare\"},\"rhs\":{\"role\":\"variable\",\"type\":\"[Integer]\",\"id\":6}},\"rhs\":{\"role\":\"variable\",\"type\":\"[Integer]\",\"id\":6}}",
"{\"role\":\"application\",\"lhs\":{\"role\":\"application\",\"lhs\":{\"role\":\"constant\",\"type\":\"[Integer] -> [Integer] -> Ordering\",\"symbol\":\"lengthCompare\"},\"rhs\":{\"role\":\"variable\",\"type\":\"[Integer]\",\"id\":8}},\"rhs\":{\"role\":\"variable\",\"type\":\"[Integer]\",\"id\":8}}"
]
where try x = case decode x :: Maybe Term of
Nothing -> error ("Couldn't decode " ++ S.toString x)
Just _ -> True
canParseVars = all try [
"{\"role\":\"variable\",\"type\":\"[Integer]\",\"id\":7}",
"{\"role\":\"variable\",\"type\":\"[Integer]\",\"id\":6}"
]
where try x = case decode x :: Maybe Var of
Nothing -> error ("Couldn't decode " ++ S.toString x)
Just _ -> True
canParseConsts = all try [
"{\"role\":\"constant\",\"type\":\"[Integer] -> [Integer] -> Ordering\",\"symbol\":\"lengthCompare\"}"
]
where try x = case decode x :: Maybe Const of
Nothing -> error ("Couldn't decode " ++ S.toString x)
Just _ -> True
canParseExamples = not (null exampleEqs)
canEvalExamples = withExamples allStrict
where allStrict = foldr ((&&) . strict) True
strict (Eq !l !r) = True
canMakeSignature = withExamples makeSig
where makeSig xs = case sigFromEqs xs of
Sig !cs !vs -> True
constantsAdded cs s = case withConsts cs s of
Sig cs' _ -> all (`elem` cs') cs
variablesAdded vs s = case withVars vs s of
Sig _ vs' -> all (`elem` vs') vs
sigsRender = once $ do
eqs <- resize 20 genNormalisedEqs
let sig = sigFromEqs eqs
s = show (renderN sig :: Test.QuickSpec.Signature.Sig)
return (length s >= 0)
sigsHaveConsts = once $ do
eqs <- resize 42 genNormalisedEqs
let s@(Sig cs vs) = sigFromEqs eqs
rendered = renderN s
consts = Test.QuickSpec.Signature.constantSymbols rendered
names = map constName cs
return (checkNames names consts)
sigsHaveVars = once (forAll (resize 42 genNormalisedEqs) sigsHaveVars')
sigsHaveVars' eqs =
let s@(Sig _ vs) = sigFromEqs eqs
rendered = renderN s
variables = Test.QuickSpec.Signature.variableSymbols rendered
hasVars :: Bool
hasVars = checkVars variables
checkVars = checkNames names
names = map varName vs
foundNames = map Test.QuickSpec.Term.name variables
dbg = show (("expect names", names),
("found names", foundNames))
in counterexample dbg (return hasVars :: Gen Bool)
sigConstsUniqueIndices = once . resize 20 $ do
s <- genNormalisedSig
c <- genNormalisedConst
return (sigConstsUniqueIndices' s c)
-- Use `c` to generate a bunch of similar constants `consts`, add them to `s` to
-- get `sig`. Render `sig` to a QuickSpec signature, then print out its constant
-- symbols and compare with those of `sig`.
sigConstsUniqueIndices' s (Const a (Name n) t) = hasConsts
where syms = Test.QuickSpec.Signature.constantSymbols (renderN sig)
names = map Test.QuickSpec.Term.name syms
hasConsts = setEq (map Name names)
(map constName (sigConsts sig))
consts = [Const a (Name (n ++ show i)) t | i <- [0..10]]
sig = withConsts consts s
sigVarsUniqueIndices :: Property
sigVarsUniqueIndices = once $ resize 20 $ do
s <- genNormalisedSig
v <- genNormalisedVar
return (sigVarsUniqueIndices' s v)
-- Use `v` to generate a bunch of `Var`s of the same type, `vars`, add them to
-- `s` to get `sig`. Render `sig` to a QuickSpec signature, then print out its
-- variable symbols and compare with those of `sig`.
sigVarsUniqueIndices' :: Sig -> Var -> Bool
sigVarsUniqueIndices' s (Var t _ a) = hasVars
where syms = Test.QuickSpec.Signature.variableSymbols (renderN sig)
names = map Test.QuickSpec.Term.name syms
hasVars = setEq (map Name names)
(map varName (sigVars sig))
vars = [Var t i a | i <- [0..10]]
sig = withVars vars s
-- Some vars get split over multiple lines
readVars s = accumulate [] (lines s)
where accumulate (v:vs) (l@(' ':_):ls) = accumulate ((v ++ l):vs) ls
accumulate vs (l :ls) = accumulate (l :vs) ls
accumulate vs [] = vs
noClassesFromEmptyEqs = null (classesFromEqs [])
-- Sub-terms are added, which can make more than one class
getClassFromEq eq = length (classesFromEqs [eq]) >= 1
classesHaveTerms eqs = found `all` terms
where terms = concatMap termsOf eqs
termsOf (Eq l r) = [l, r]
found t = (t `elem`) `any` classes
classes = classesFromEqs eqs
eqPartsAppearInSameClass eqs = counterexample (show debug) test
where test = all eqPartsInSameClass eqs
classes = classesFromEqs eqs
matchingClass t = head $ filter (t `elem`) classes
eqPartsInSameClass (Eq l r) = r `elem` matchingClass l &&
l `elem` matchingClass r
debug = (("eqs", eqs), ("classes", classes))
classesHaveNoDupes eqs = counterexample (show debug) test
where test = all appearOnce terms
classes = classesFromEqs eqs
terms = concat classes
appearOnce t = length (filter (t `elem`) classes) == 1
debug = (("eqs", eqs), ("classes", classes), ("terms", terms))
classHasSameArity eqs = all oneArity classes
where classes = classesFromEqs eqs
oneArity ts = length (nub (map termArity ts)) == 1
equationsHaveSameArity (Eqs eqs) = all sameArity eqs
where sameArity (Eq l r) = termArity l == termArity r
nonEqualElementsSeparate ty = forAll (iterable ty) nonEqualElementsSeparate'
nonEqualElementsSeparate' (t, v) = all found expected
where (a:b:c:d:e:f:_) = map extend [0..]
extend 0 = t
extend n = app v (extend (n-1))
eqs = [Eq a b, Eq b c, Eq d e, Eq e f]
classes = classesFromEqs eqs
expected = [[a, b, c], [d, e, f]]
found xs = any (setEq xs) classes
match xs ys = all (\x -> any (setEq x) ys) xs
classElementsAreEqual = once (forAll (resize 42 arbitrary) classElementsAreEqual')
classElementsAreEqual' (Eqs eqs) = all elementsAreEqual classes
where classes :: [[Term]]
classes = classesFromEqs eqs
terms = nub $ concatMap termsOf eqs
termsOf (Eq x y) = [x, y]
elementsAreEqual :: [Term] -> Bool
elementsAreEqual cls = all (equalToAll cls) cls
equalToAll :: [Term] -> Term -> Bool
equalToAll xs y = all (equal y) xs
equal :: Term -> Term -> Bool
equal x y = y `isElem` eqClosure eqs x
classesNotSingletons (Eqs eqs) = all nonSingle classes'
where nonSingle c = length (nub c) > 1
classes = classesFromEqs eqs -- All classes, even subterms
classes' = filter (\c -> any (`elem` c) terms) classes -- Top-level
terms = getTerms [] eqs
getTerms acc [] = acc
getTerms acc (Eq l r:es) = getTerms (l:r:acc) es
canFindClosure ty = forAll (iterable ty) canFindClosure'
canFindClosure' (t, v) = all match expected
where -- Generate unique terms by wrapping in "app c"
(a:b:c:d:e:f:g:h:_) = map extend [0..]
extend 0 = t
extend n = app v (extend (n-1))
match (x, xs) = setEq (eqClosure eqs x) xs
eqs = [Eq a b, Eq a c, Eq b d, Eq b b, Eq f g, Eq f h]
abcd = [a, b, c, d]
fgh = [f, g, h]
expected = [(a, abcd), (b, abcd), (c, abcd), (d, abcd),
(e, [e]),
(f, fgh), (g, fgh), (h, fgh)]
canGetClassesFromEqs (Eqs eqs) = True
where typeCheck = classesFromEqs eqs
canGetSigFromEqs eqs = case sigFromEqs eqs of
Sig _ _ -> True
eqSigHasVars eqs = counterexample debug test
where sig = sigFromEqs eqs
sigvars = sigVars sig
eqvars = concatMap eqVars eqs
test = setEq sigvars eqvars
debug = show (("eqs", eqs),
("sigvars", sigvars),
("eqvars", eqvars),
("sig", sig))
eqSigHasConsts eqs = counterexample debug test
where sig = sigFromEqs eqs
test = setEq sigconsts eqconsts
sigconsts = sigConsts sig
eqconsts = concatMap eqConsts eqs
debug = show (("eqs", eqs),
("sig", sig),
("sigconsts", sigconsts),
("eqconsts", eqconsts))
canPruneEqs = once (forAll (resize 20 arbitrary) canPruneEqs')
canPruneEqs' (Eqs eqs) = counterexample (show (("eqs", eqs), ("eqs'", eqs')))
(expected eqs')
where expected [] = null eqs -- No output when no eqs
expected (x:xs) = not (null eqs)
eqs' = reduction eqs
canGetTermType input output = expected (termType' term)
where term = app (C (Const undefined undefined func))
(C (Const undefined undefined input))
func = tyFun input output
strip = filter (/= ' ')
expected t = strip (typeName t) === strip (typeName output)
noTrivialTerms t = forAll (termOfType t) (not . trivial)
eqsAreConsistent (Eqs eqs) = consistentEqs eqs
-- Given 'i' and 'o', we should be able to replace 'i -> o'
switchFunctionTypes i1 i2 o1 o2 = check <$> termOfType (HSE.Syntax.TyFun () i1 o1)
where db = [(i1, i2), (o1, o2)]
check f = let [Eq lhs rhs] = restoreTypes db [replaceEqTypes db (Eq f f)]
in termType lhs == termType rhs
regressionTypeParse = LB.length (encode result) > 0
where ex = "[{\"relation\":\"~=\",\"lhs\":{\"role\":\"application\",\"lhs\":{\"role\":\"constant\",\"type\":\"List Integer -> List Integer\",\"symbol\":\"reverse\"},\"rhs\":{\"role\":\"application\",\"lhs\":{\"role\":\"application\",\"lhs\":{\"role\":\"constant\",\"type\":\"Integer -> List Integer -> List Integer\",\"symbol\":\"cCons\"},\"rhs\":{\"role\":\"variable\",\"type\":\"Integer\",\"id\":3}},\"rhs\":{\"role\":\"constant\",\"type\":\"List Integer\",\"symbol\":\"cNil\"}}},\"rhs\":{\"role\":\"application\",\"lhs\":{\"role\":\"application\",\"lhs\":{\"role\":\"constant\",\"type\":\"Integer -> List Integer -> List Integer\",\"symbol\":\"cCons\"},\"rhs\":{\"role\":\"variable\",\"type\":\"Integer\",\"id\":3}},\"rhs\":{\"role\":\"constant\",\"type\":\"List Integer\",\"symbol\":\"cNil\"}}}]"
result = parseAndReduce ex
natHasEqs = case eitherDecode rawNatEqs :: Either String [Equation] of
Left err -> error err
Right [] -> error "No equations found"
Right eqs -> True
natKeepsEqs = case parseAndReduce rawNatEqs of
[] -> error "No equations found"
_ -> True
natClassesNontrivial =
let raw = rawNatEqs
rawEqs = parsedNatEqs
(_, rawEqs') = replaceTypes rawEqs
classes = classesFromEqs rawEqs'
in counterexample (show classes)
(any (\c -> length c > 2) classes)
commClassesNontrivial n1 n2 i o = once $
counterexample (show (("eqs", eqs),
("clss", clss),
("comm", comm)))
(all ((> 1) . length . nub) clss')
where f = C $ Const (Arity 2) n1 (HSE.Syntax.TyFun () i (HSE.Syntax.TyFun () i o))
q = C $ Const (Arity 1) n2 (HSE.Syntax.TyFun () o o)
x = V $ Var i 0 (Arity iArity)
y = V $ Var i 1 (Arity iArity)
iArity = countArity i
(cl, cr) = (App (App f x Nothing) y Nothing, App (App f y Nothing) x Nothing)
(ql, qr) = (App q (App (App f x Nothing) y Nothing) Nothing,
App q (App (App f y Nothing) x Nothing) Nothing)
comm = Eq cl cr
eqs = [comm, Eq ql qr]
clss = classesFromEqs eqs
clss' = filter topLevel clss
topLevel c = any (`elem` c) [cl, cr, ql, qr]
natEqsPruned = length pruned < length rawEqs'
where (_, rawEqs') = replaceTypes parsedNatEqs
pruned = pruneEqsN rawEqs'
natEqsMatchQS = once $ monadicIO $ do
expect <- run $ LB.readFile "test/data/nat-simple-expect.json"
let Right expectEqs = eitherDecode expect :: Either String [Equation]
foundEqs = parseAndReduce rawNatEqs
fLen = length foundEqs
eLen = length expectEqs
monitor . counterexample $ show (("foundEqs", foundEqs),
("expectEqs", expectEqs),
("length foundEqs", length foundEqs),
("length expectEqs", length expectEqs))
assert (length foundEqs == length expectEqs)
extractedTypesUnique (Eqs eqs) = counterexample (show types)
(nub types == types)
where types = allTypes eqs
convertTypesIso =
(forAll (resize 20 arbitrary)
(\x -> case convertTypesIso' x of
([], []) -> property True
(extraEqs', extraConv) ->
counterexample (show (("extraEqs'", extraEqs'),
("extraConv", extraConv)))
(property False)))
convertTypesIso' (Eqs eqs) =
let (_, eqs') = replaceTypes eqs
qsEqs = Test.QuickSpec.Equation.equations qsClss
sig = renderN (sigFromEqs eqs')
qsClss = unSomeClassesN2 eqs' sig
conv = map (qsEqToEq . Test.QuickSpec.Utils.Typed.some Test.QuickSpec.Equation.eraseEquation) qsEqs
conv' = map (Test.QuickSpec.Utils.Typed.several
(map (qsTermToTerm . Test.QuickSpec.Term.term)))
qsClss
clss = classesFromEqs eqs'
result = setEq clss conv'
cmp (Eq l1 r1) (Eq l2 r2) = (show l1 == show l2 && show r1 == show r2) ||
(show l1 == show r2 && show r1 == show l2)
in setDiffBy setEq clss conv'
eqsSymmetric [] = return True
eqsSymmetric eqs = do
Eq l r <- elements eqs
return (Eq r l `elem` eqs)
eqsSetEq eqs = setEq eqs (map swap eqs)
where swap (Eq l r) = Eq r l
canMakeVars = do
v <- genNormalisedVar
return True
canMakeQSSigs = do
v <- genNormalisedVar
let sig = renderQSVars [v]
return (length (show sig) > 0)
lookupVars = once $ do
eqs <- resize 42 genEqsWithVars
let Sig _ vs = sigFromEqs eqs'
(_, eqs') = replaceTypes eqs
v <- elements vs
let expectName = unName (varName v)
sig = renderQSVars [v]
symbol = sigToSymN (V v) sig
foundName = Test.QuickSpec.Term.name symbol
return (expectName == foundName)
justPrune = once $ do
eqs <- resize 20 arbitrary
let (_, eqs') = replaceTypes eqs
o = pruneEqsN eqs'
return (length o >= 0)
newReduce = once (forAll (resize 20 arbitrary) newReduce')
newReduce' (Eqs eqs) = counterexample (show (("eqs", eqs),
("result", result)))
(length (show result) > 0)
where result = reduction eqs
reduceIdem = once (forAll (resize 20 arbitrary) reduceIdem')
reduceIdem' (Eqs eqs) = setEq eqs' eqs''
where eqs' = reduction eqs
eqs'' = reduction eqs'
transStripped = once . resize 10 $ do
Eqs eqs <- arbitrary
t <- arbitrary
a <- termOfType t
b <- termOfType t
c <- termOfType t
ds <- listOf (termOfType t)
-- Add a bunch of redundant equations
eqs' <- renameEqs (eqs ++ [Eq x y | x <- b:c:ds, y <- b:c:ds])
let (_, eqs'') = replaceTypes eqs'
pruned = reduction eqs''
-- Check if (at least) our redundant equations got stripped out
return (length pruned <= length eqs + 2 + length ds)
termsHaveType ty = forAll (termOfType ty) checkType
where checkType trm = termType (setForTerm trm) == Just ty
manualNatFindsEqs = once . monadicIO $ do
-- Our raw equations, for comparison
let rawEqs = parsedNatEqs
clss = rawNatClasses
eqs = Test.QuickSpec.Equation.equations clss
eqs' = dbgEqs eqs
monitor . counterexample . show $ ("eqs'", eqs')
-- Our golden input should match these
assert (length eqs == length rawEqs)
manualNatAllowsGiven = counterexample (show eqs')
((length eqs' > 0) &&
(length eqs' <= length parsedNatEqs))
where clss = classesFromEqs naturalEqs
clss' = sort (map (sort . mkUnSomeClassN natSig) clss)
eqs' = unSomePruneN clss' natSig
naturalEqs = map (replaceEqTypes db) parsedNatEqs
db = [(tyCon "Nat", tyCon "Natural")]
manualNatClassesMatch = counterexample dbg result
where ourClss = classesFromEqs eqs'
ourClss' = sort (map (sort . mkUnSomeClassN natSig) ourClss)
ourClss'' = map (map Test.QuickSpec.Term.term) ourClss'
eqs' = map (replaceEqTypes db) parsedNatEqs
db = [(tyCon "Nat", tyCon "Natural")]
result = setEq natNonTrivial ourClss''
natNonTrivial = filter ((> 1) . length) natClasses
dbg = show (("qs non-trivial", length natNonTrivial),
("our classes", length ourClss''))
topNatTermsFound = all termInClasses (termsOf [] eqs')
where termsOf acc [] = acc
termsOf acc (Eq l r:xs) = termsOf (l:r:acc) xs
termInClasses t = let qs = any (renderTermN t natSig `elem`) natClasses
us = any (t `elem`) clss
in case (qs, us) of
(False, False) -> error $ show t ++ " not found in either"
(False, _) -> error $ show t ++ " not in QS"
(_, False) -> error $ show t ++ " not in ours"
_ -> True
clss = classesFromEqs eqs'
eqs' = map (replaceEqTypes db) parsedNatEqs
db = [(tyCon "Nat", tyCon "Natural")]
qsNatTermsFound = case unfoundInOurs of
[] -> True
us -> error (show ("unfound", us))
where allTerms = concat (filter ((> 1) . length) natClasses)
clss = classesFromEqs eqs'
inOurs t = any (t `elem`) (map (map (`renderTermN` natSig)) clss)
unfoundInOurs = filter (not . inOurs) allTerms
db = [(tyCon "Nat", tyCon "Natural")]
eqs' = map (replaceEqTypes db) parsedNatEqs
natClassesIncludeSingletons = any ((== 1) . length) natClasses
-- We compare the "show" output, to avoid irrelevant details like symbol indices
exactClassMatch = counterexample (show (("ourClasses", ourClasses),
("qsClasses'", qsClasses')))
(ourClasses == qsClasses')
where ourClasses = map (Test.QuickSpec.Utils.Typed.several (map term))
(unSomeClassesN2 parsedNatEqs' natSig')
qsClasses = filter ((> 1) . length) natClasses
qsClasses' = replaceQSTypes naturalDb qsClasses
convertPrunes = length (doPrune qsClasses natSig') == 10
where qsClasses = filter (Test.QuickSpec.Utils.Typed.several ((> 1) . length))
rawNatClasses'
db = [(tyCon "Natural", tyCon "Z")]
-- We don't compare equations directly, since they may differ slightly e.g. due
-- to commutativity
parsedEqsPrune = nub [length ourPrune, length qsPrune] == [10]
where (db, eqs') = replaceTypes parsedNatEqs
ourPrune = doPrune classes sig
classes = unSomeClassesN2 eqs' sig
sig = let sig' = renderN (sigFromEqs eqs')
sig'' = Test.QuickSpec.Signature.signature sig'
in sig'' `mappend` Test.QuickSpec.Main.undefinedsSig sig''
qsPrune = doPrune rawNatClasses natSig
manualNatReducesSelf = counterexample (show ("pruned", pruned))
((length pruned < 20) &&
(length pruned > 1))
where pruned = doPrune rawNatClasses natSig
-- Helpers
natSig = mconcat [
Test.QuickSpec.Signature.fun0 "cZ" (0 :: Natural),
Test.QuickSpec.Signature.fun1 "cS" ((+1) :: Natural -> Natural),
Test.QuickSpec.Signature.fun2 "plus" ((+) :: Natural -> Natural -> Natural),
Test.QuickSpec.Signature.fun2 "times" ((*) :: Natural -> Natural -> Natural),
Test.QuickSpec.Signature.gvars (map (\n -> "(var, Natural, " ++ show n ++ ")")
[0, 1, 2])
(((fromInteger . abs) <$> arbitrary) :: Gen Natural)]
natSig' = mconcat [
Test.QuickSpec.Signature.fun0 "cZ" (undefined :: Z),
Test.QuickSpec.Signature.fun1 "cS" (undefined :: Z -> Z),
Test.QuickSpec.Signature.fun2 "plus" (undefined :: Z -> Z -> Z),
Test.QuickSpec.Signature.fun2 "times" (undefined :: Z -> Z -> Z),
Test.QuickSpec.Signature.gvars (map (\n -> "(var, Z, " ++ show n ++ ")")
[0, 1, 2])
(return undefined :: Gen Z)]
genEqsWithVars = arbitrary `suchThat` hasVars
where hasVars eqs = case sigFromEqs eqs of
Sig _ [] -> False
_ -> True
genNormalisedVar = do
eqs' <- genNormalisedEqs
case sigFromEqs eqs' of
Sig _ [] -> scale (+1) genNormalisedVar
Sig _ (v:_) -> return v
genNormalisedConst = do
eqs' <- genNormalisedEqs
case sigFromEqs eqs' of
Sig [] _ -> scale (+1) genNormalisedConst
Sig (c:_) _ -> return c
genNormalisedEqs = do
eqs <- arbitrary
let (_, eqs') = replaceTypes eqs
return eqs'
genNormalisedSig = sigFromEqs <$> genNormalisedEqs
setEq :: (Foldable t1, Foldable t2, Eq a) => t1 a -> t2 a -> Bool
setEq = setEqBy (==)
setEqBy :: (Foldable t1, Foldable t2) => (a -> b -> Bool) -> t1 a -> t2 b -> Bool
setEqBy f xs ys = all (\y -> any (`f` y) xs) ys &&
all (\x -> any (x `f`) ys) xs
setDiff :: Eq a => [a] -> [a] -> ([a], [a])
setDiff = setDiffBy (==)
setDiffBy :: (a -> b -> Bool)
-> [a]
-> [b]
-> ([a], [b])
setDiffBy f xs ys = (xs', ys')
where xs' = filter (\x -> not (any (x `f`) ys)) xs
ys' = filter (\y -> not (any (`f` y) xs)) ys
-- Data generators
-- Example input from files
exampleEqs :: [[Equation]]
exampleEqs = map (fromJust . decode) exampleJson
exampleJson :: [LB.ByteString]
{-# NOINLINE exampleJson #-}
exampleJson = unsafePerformIO $ exampleFiles >>= mapM LB.readFile
exampleDir = "test/data"
exampleFiles = do
fs <- getDirectoryContents exampleDir
return (prefix (json fs))
where prefix = map ((exampleDir ++ "/") ++)
json = filter isJson
isJson :: String -> Bool
isJson x = reverse ".json" == take 5 (reverse x)
withExamples = forAll (elements exampleEqs)
-- Random input generators
newtype Equations = Eqs [Equation] deriving (Show, Eq)
instance Arbitrary Equations where
shrink (Eqs []) = []
shrink (Eqs eqs) = [Eqs eqs' | eqs' <- shrink eqs, consistentEqs eqs']
arbitrary = do
-- Make a bunch of terms and declare them equal
classEqs <- scale (\s -> min 5 (s `div` 2)) (listOf mkClass)
let eqs = concat classEqs
-- Pad out with filler
pre <- scale (\s -> min 5 (s `div` 2)) arbitrary
post <- scale (\s -> min 5 (s `div` 2)) arbitrary
-- Make sure it's consistent
eqs' <- renameEqs (pre ++ eqs ++ post)
return (Eqs eqs')
where mkClass = do
t <- arbitrary
ts <- scale (`div` 2) (listOf (termOfType t))
return $ case ts of
[] -> []
(x:xs) -> [Eq x y | y <- xs]
-- | Keep renaming constants until each name only refers to one type
renameEqs eqs = if consistentEqs eqs
then return eqs
else mapM renameEq eqs >>= renameEqs
where renameEq (Eq l r) = Eq <$> renameTerm l <*> renameTerm r
renameTerm (C (Const a _ t)) = C <$> (Const a <$> arbitrary <*> pure t)
renameTerm (V v) = pure (V v)
renameTerm (App l r _) = app <$> renameTerm l <*> renameTerm r
consistentEqs eqs = let nts = concatMap eqNames eqs
in consistentNames nts
instance Arbitrary Equation where
arbitrary = do t <- arbitrary
l <- termOfType t
r <- termOfType t
if trivial l && trivial r || l == r || allVar l || allVar r
then discard
else return $ Eq l r
shrink (Eq l r) = [Eq l' r' | (l', r') <- shrink (l, r),
not (trivial l' && trivial r'),
not (allVar l'),
not (allVar r'),
termType' l' == termType' r']
-- | Generate a "non-trivial" Term, i.e. containing at least one App, one Const
-- and one Var, with the given Type
termOfType :: Type -> Gen Term
termOfType t = do
-- Generate a random Term of the correct type, of the form `app l r`
term <- appOfTypeArity 0 t
-- Force one branch to contain a Var and the other to contain a Const
giveVarConst term
-- | Force one branch of an `App` to contain a Const and the other to contain a
-- Var
giveVarConst (App l r _) = do
which <- arbitrary
l' <- if which then giveVar l else giveConst l
r' <- if not which then giveVar r else giveConst r
return (app l' r')
-- | Randomly replace part of the given Term with a Var
giveVar :: Term -> Gen Term
-- If the Term is already a Var, there is no work to do
giveVar (V v) = return (V v)
-- Turn Consts into Vars. Since Consts may have higher arity (up to 5) than Vars
-- (up to 2), we rely on the App cases to prevent hitting high-arity Terms
giveVar (C c) = V <$> varOfTypeArity (constArity c) (constType c)
-- Don't recurse any further if we reach an arity of 2, since we might reach a
-- sub-Term with an arity above 2, which cannot be turned into a Var
giveVar t | termArity t >= 2 = V <$> varOfTypeArity (termArity t)
(termType' t)
-- If it's safe to recurse, choose a branch at random to force a Var into
giveVar (App l r _) = do
which <- arbitrary
l' <- if which then giveVar l else return l
r' <- if not which then giveVar r else return r
return (app l' r')
-- | Randomly replace part of a Term with a Const
giveConst :: Term -> Gen Term
-- Constants can just be returned as-is
giveConst (C c) = return (C c)
-- Variable arity should always be lower than 3, which a Const should have no
-- problem with
giveConst (V v) = C <$> constOfTypeArity (varArity v) (varType v)
-- Don't recurse into Terms with arity 5, since we might hit a Term with a
-- higher arity which we can't replace with a Const
giveConst t | termArity t >= 5 = C <$> constOfTypeArity (termArity t)
(termType' t)
-- It's safe to recurse into low-arity Apps. We pick a branch randomly to put a
-- Const into
giveConst (App l r _) = do
which <- arbitrary
l' <- if which then giveConst l else return l
r' <- if not which then giveConst r else return r
return (app l' r')
constOfTypeArity :: Arity -> Type -> Gen Const
constOfTypeArity a t = if a > 5
then error ("Can't make Const of type " ++ show t ++ " and arity " ++ show a)
else Const a <$> arbitrary <*> pure t
varOfTypeArity :: Arity -> Type -> Gen Var
varOfTypeArity a t = if a > 2
then error ("Can't make Var of type " ++ show t ++ " and arity " ++ show a)
else Var t <$> choose (0, 4) <*> pure a
appOfTypeArity :: Arity -> Type -> Gen Term
appOfTypeArity a t = do
arg <- arbitrary
r <- termOfTypeArity 0 arg
l <- termOfTypeArity (a+1) (tyFun arg t)
return $ app l r
termOfTypeArity :: Arity -> Type -> Gen Term
termOfTypeArity a t = oneof (mkConst ++ mkVar ++ mkApp)
where -- We can only generate constants up to arity 5
mkConst = if a > 5
then error ("Can't gen Term of arity " ++ show a)
else [C <$> constOfTypeArity a t]
-- We can only generate variables up to arity 2
mkVar = if a > 2
then []
else [V <$> varOfTypeArity a t]
mkApp = if a > 4
then []
else [appOfTypeArity a t]
-- "Trivial" equations will be pruned, so we need to avoid generating (or
-- shrinking down to) equations where both sides only have one symbol, or which
-- don't contain any variables
trivial (C _) = True
trivial (V _) = True
trivial x | not (hasVar x) = True
trivial x | not (hasConst x) = True
trivial x = False
hasConst (V _) = False
hasConst (C _) = True
hasConst (App l r _) = hasConst l || hasConst r
hasVar (V _) = True
hasVar (C _) = False
hasVar (App l r _) = hasVar l || hasVar r
allVar (V _) = True
allVar (C _) = False
allVar (App l r _) = allVar l && allVar r
-- | Make sure no name is used for constants of two types
termNames :: Term -> [(Name, Type)]
termNames (C (Const _ n t)) = [(n, t)]
termNames (V _) = []
termNames (App l r _) = nub (termNames l ++ termNames r)
eqNames :: Equation -> [(Name, Type)]
eqNames (Eq l r) = termNames l ++ termNames r
consistentNames nts = all hasOneType names
where names = map fst nts
hasOneType n = length (typesOf n) == 1
typesOf n = nub (map snd (entriesOf n))
entriesOf n = filter ((== n) . fst) nts
instance Arbitrary Term where
arbitrary = do
t <- arbitrary
termOfType t
shrink (C c) = C <$> shrink c
shrink (V v) = V <$> shrink v
shrink t@(App l r _) = C (Const (termArity t) (termName t) (termType' t)) :
[app l' r' | (l', r') <- shrink (l, r)]
termName (C c) = constName c
termName (V v) = Name (filter isAlpha (show (varType v) ++ show (varArity v)))
termName (App l r _) = let Name l' = termName l
Name r' = termName r
in Name ("app" ++ l' ++ r')
instance Arbitrary Var where
arbitrary = sized $ \n -> do
arity <- elements [0, 1, 2]
typ <- naryType arity n
index <- elements [0, 1, 2]
return $ Var typ index (Arity arity)
shrink (Var t i a) = if i == 0
then []
else [Var t 0 a]
instance Arbitrary Const where
arbitrary = sized $ \n -> do
arity <- elements [0..5]
name <- arbitrary
typ <- naryType arity n
return $ Const (Arity arity) name typ
shrink (Const a n t) = do n' <- shrink n
return (Const a n' t)
instance Arbitrary Sig where
arbitrary = Sig <$> listOf arbitrary <*> listOf arbitrary
shrink (Sig [] []) = []
shrink (Sig cs vs) = Sig [] [] : [Sig cs' vs' | (cs', vs') <- shrink (cs, vs)]
instance Arbitrary Type where
arbitrary = sized sizedType
instance Arbitrary Name where
arbitrary = Name <$> listOf1 (arbitrary `suchThat` isAlpha `suchThat` isAscii) `suchThat` valid
where valid s = let t = S.fromString s
b = S.fromString s
in s == S.toString b &&
s == S.toString t &&
b == S.fromString s &&
b == encodeUtf8 t &&
t == S.fromString s &&
t == decodeUtf8 b
shrink (Name x) = let suffices = tail (tails x)
nonEmpty = filter (not . null) suffices
names = map Name nonEmpty
in reverse names -- Try shortest first
sizedType :: Int -> Gen Type
sizedType 0 = elements [tyCon "Int", tyCon "Bool", tyCon "Float"]
sizedType n = oneof [
sizedType 0,
do x <- sizedType (n - 1)
return $ tyCon ("[" ++ typeName x ++ "]"),
do n' <- choose (0, n - 1)
l <- sizedType n'
r <- sizedType (n - n')
return $ tyCon ("(" ++ typeName l ++ ", " ++ typeName r ++ ")")
]
naryType 0 n = sizedType n
naryType a n = do
arg <- sizedType n
ret <- naryType (a-1) n
return $ tyFun arg ret
dbg :: (Show a, Monad m) => a -> PropertyM m ()
dbg = monitor . counterexample . show
doOnce :: (Show a, Arbitrary a, Testable prop) => (a -> prop) -> Property
doOnce = once . forAll (resize 42 arbitrary)
-- | The list of all terms equal to `x`, according to `eqs`
eqClosure :: [Equation] -> Term -> Seq.Seq Term
eqClosure eqs x = indirect eqs Seq.empty (directEq eqs x)
indirect :: [Equation] -> Seq.Seq Term -> Seq.Seq Term -> Seq.Seq Term
indirect eqs seen xs | null xs = seen
indirect eqs seen xs = indirect eqs (nub' $ seen Seq.>< unseen) unseen
where new = xs >>= directEq eqs
unseen = nub' $ Seq.filter notSeen new
notSeen a = not (a `isElem` seen)
nub' = foldl f Seq.empty
where f acc x = if x `isElem` acc
then acc
else x Seq.<| acc
isElem x xs = isJust (Seq.elemIndexL x xs)
-- | The list of terms equal to `x` by definition, according to `eqs`
directEq :: [Equation] -> Term -> Seq.Seq Term
directEq eqs x = x Seq.<| Seq.filter direct terms
where terms = Seq.fromList . nub . concatMap termsOf $ eqs
termsOf (Eq a b) = [a, b]
direct a = Eq x a `elem` eqs || Eq a x `elem` eqs
app l r = case termType l of
Just (HSE.Syntax.TyFun _ _ o) -> App l r (Just o)
_ -> x
where [Eq x _] = setAllTypes [Eq (App l r Nothing)
(App l r Nothing)]
iterable ty = do t <- termOfType ty
v <- termOfType (tyFun ty ty)
return (t, v)
tyFun = HSE.Syntax.TyFun ()
instance Show Test.QuickSpec.Reasoning.NaiveEquationalReasoning.Context where
show cxt = concat ["(context\n (universe ",
show (Test.QuickSpec.Reasoning.NaiveEquationalReasoning.universe cxt),
")\n (maxDepth ",
show (Test.QuickSpec.Reasoning.NaiveEquationalReasoning.maxDepth cxt),
")\n (rel ",
show (Test.QuickSpec.Reasoning.NaiveEquationalReasoning.rel cxt),
")\n)"]
instance Show Test.QuickSpec.Reasoning.CongruenceClosure.S where
show s = concat ["(S\n (funUse ",
show (Test.QuickSpec.Reasoning.CongruenceClosure.funUse s),
")\n (argUse ",
show (Test.QuickSpec.Reasoning.CongruenceClosure.argUse s),
")\n (lookup ",
show (Test.QuickSpec.Reasoning.CongruenceClosure.lookup s)
]
dbgEqs = map (Test.QuickSpec.Utils.Typed.some
(Test.QuickSpec.Equation.showTypedEquation natSig))
rawNatEqs = unsafePerformIO (LB.readFile "test/data/nat-simple-raw.json")
Right parsedNatEqs = eitherDecode rawNatEqs :: Either String [Equation]
(typeDb, parsedNatEqs') = replaceTypes parsedNatEqs
doReps clss = map (Test.QuickSpec.Utils.Typed.some2
(Test.QuickSpec.Utils.Typed.tagged term . head))
clss
natClasses = map (Test.QuickSpec.Utils.Typed.several
(map Test.QuickSpec.Term.term))
rawNatClasses
rawNatClasses' = swapTypes' naturalDb rawNatClasses
swapTypes' db = map (Test.QuickSpec.Utils.Typed.several
(\xs -> let trep = head (typeRepArgs (typeRep xs)) -- Strip off [] and Expr
typ = case HSE.Parser.parseType (show trep) of
HSE.Parser.ParseOk x -> unwrapParens (fmap (const ()) x)
typ' = replaceInType db typ
in case getVal (getRep typ') of
MkHT x -> Test.QuickSpec.Utils.Typed.Some
(Test.QuickSpec.Utils.Typed.O
(map (\e -> let trm = replaceQSType db (Test.QuickSpec.Term.term e)
in e {
Test.QuickSpec.Term.term = trm,
Test.QuickSpec.Term.eval = \env -> case trm of
Test.QuickSpec.Term.Var s -> Test.QuickSpec.Term.unValuation env (Test.QuickSpec.Term.Variable (Test.QuickSpec.Term.Atom s (Test.QuickSpec.Term.pgen (return x))))
Test.QuickSpec.Term.Const s -> x
Test.QuickSpec.Term.App l r -> x
})
xs))))
rawNatClasses :: [Test.QuickSpec.Utils.Typed.Several Test.QuickSpec.Term.Expr]
rawNatClasses = concatMap (Test.QuickSpec.Utils.Typed.some2
(map (Test.QuickSpec.Utils.Typed.Some .
Test.QuickSpec.Utils.Typed.O) .
Test.QuickSpec.TestTree.classes))
(Test.QuickSpec.Utils.TypeMap.toList r)
where r = unsafePerformIO $ Test.QuickSpec.Generate.generate
False
(const Test.QuickSpec.Term.partialGen)
natSig
tType (Test.QuickSpec.Term.Var s) = Test.QuickSpec.Utils.Typeable.unTypeRep (Test.QuickSpec.Term.symbolType s)
tType (Test.QuickSpec.Term.Const s) = Test.QuickSpec.Utils.Typeable.unTypeRep (Test.QuickSpec.Term.symbolType s)
tType (Test.QuickSpec.Term.App l r) = case funResultTy (tType l) (tType r) of
Nothing -> error ("Incompatible types (" ++ show (tType l) ++ ") (" ++ show (tType r) ++ ")")
Just t -> t
replaceQSTypes :: [(Type, Type)] -> [[Test.QuickSpec.Term.Term]] -> [[Test.QuickSpec.Term.Term]]
replaceQSTypes db = map rep
where rep = map (replaceQSType db)
replaceQSType db t =
case t of
Test.QuickSpec.Term.Var s -> Test.QuickSpec.Term.Var (
let ty = prnt (Test.QuickSpec.Utils.Typeable.unTypeRep
(Test.QuickSpec.Term.symbolType s))
tr = repToQSRep (getRep ty)
n = let suf = reverse
(takeWhile (/= ',')
(reverse (Test.QuickSpec.Term.name s)))
idx = read (init suf) :: Int
in unName (varName (Var
ty
idx
(Arity (Test.QuickSpec.Term.symbolArity s))))
in s {
Test.QuickSpec.Term.symbolType = tr,
Test.QuickSpec.Term.name = n
})
Test.QuickSpec.Term.Const s -> Test.QuickSpec.Term.Const (s {
Test.QuickSpec.Term.symbolType =
repToQSRep
(getRep
(prnt (Test.QuickSpec.Utils.Typeable.unTypeRep
(Test.QuickSpec.Term.symbolType s))))
})
Test.QuickSpec.Term.App l r -> Test.QuickSpec.Term.App
(replaceQSType db l)
(replaceQSType db r)
where prs x = case HSE.Parser.parseType (show x) of
HSE.Parser.ParseOk typ -> unwrapParens (fmap (const ()) typ)
HSE.Parser.ParseFailed _ e -> error (concat [
"Failed to replace QuickSpec type '",
show t,
"'. Error is: ",
e])
prnt = replaceInType db . prs
naturalDb = [(tyCon "Natural", tyCon "Z")]