250 lines
9.8 KiB
Haskell
250 lines
9.8 KiB
Haskell
module Main where
|
|
|
|
import Data.List (isInfixOf)
|
|
import qualified Data.Map.Strict as Map
|
|
import System.Exit (exitFailure, exitSuccess)
|
|
|
|
import Tessera.Analyze
|
|
import Tessera.Check (checkProgram)
|
|
import Tessera.Env
|
|
import Tessera.Eval
|
|
import Tessera.Matrix
|
|
import Tessera.Parser (parseExpression, parseProgram)
|
|
import Tessera.Serialize
|
|
import Tessera.Syntax
|
|
import Tessera.Tree
|
|
|
|
type Result = (String, Bool)
|
|
|
|
parseOk :: String -> Program
|
|
parseOk source = case parseProgram source of
|
|
Left diagnostic -> error ("parse failed: " ++ show diagnostic)
|
|
Right program -> program
|
|
|
|
envOk :: Program -> Env
|
|
envOk program = case checkProgram program of
|
|
Left diagnostic -> error ("check failed: " ++ show diagnostic)
|
|
Right env -> env
|
|
|
|
envSource :: String -> Env
|
|
envSource = envOk . parseOk
|
|
|
|
aritiesOf :: Env -> [(String, Int)]
|
|
aritiesOf env = Map.toList (Map.map (length . snd) (envConstructorTypes env))
|
|
|
|
valueOf :: Env -> String -> Value
|
|
valueOf env text = case parseExpression (aritiesOf env) text of
|
|
Left diagnostic -> error ("value parse failed: " ++ show diagnostic)
|
|
Right expression -> case evalExpr env Map.empty expression of
|
|
Left message -> error ("value eval failed: " ++ message)
|
|
Right value -> value
|
|
|
|
matchOf :: String -> Program -> Declaration
|
|
matchOf name program = case [m | m@(MatchDeclaration n _ _ _) <- program, n == name] of
|
|
(m : _) -> m
|
|
[] -> error ("no match " ++ name)
|
|
|
|
treeOf :: Env -> Strategy -> Declaration -> Tree
|
|
treeOf env strategy (MatchDeclaration _ arguments _ clauses) =
|
|
compileMatch env strategy (map snd arguments) (zip (map clausePatterns clauses) [0 .. length clauses - 1]) (initialOccurrences (length arguments))
|
|
treeOf _ _ _ = Failure
|
|
|
|
boolType :: Type
|
|
boolType = TName "Bool" []
|
|
|
|
intType :: Type
|
|
intType = TName "Int" []
|
|
|
|
listProgram :: Program
|
|
listProgram = parseOk "data List a = Nil | Cons a (List a)\n"
|
|
|
|
main :: IO ()
|
|
main = do
|
|
let results = tests
|
|
failures = [name | (name, ok) <- results, not ok]
|
|
mapM_ (\(name, ok) -> putStrLn ((if ok then "ok " else "FAIL ") ++ name)) results
|
|
putStrLn (show (length results - length failures) ++ "/" ++ show (length results) ++ " tests passed")
|
|
if null failures then exitSuccess else exitFailure
|
|
|
|
tests :: [Result]
|
|
tests =
|
|
[ ("specialise expands constructor and wildcard rows", testSpecialise)
|
|
, ("default matrix keeps wildcard rows only", testDefault)
|
|
, ("boolean witness is the missing constructor", testBooleanWitness)
|
|
, ("boolean coverage is exhaustive", testBooleanCoverage)
|
|
, ("integer witness escapes the covered literals", testIntegerWitness)
|
|
, ("multiple arguments detect cross column gaps", testMultipleArguments)
|
|
, ("recursive list coverage is exhaustive", testRecursiveList)
|
|
, ("uninhabited recursive type is vacuously exhaustive", testUninhabited)
|
|
, ("variable binding and shadowing", testBinding)
|
|
, ("source matcher agrees with compiled trees", testAgreement)
|
|
, ("serialisation round trip preserves the tree", testRoundTrip)
|
|
, ("malformed tree encoding is rejected", testMalformedTree)
|
|
, ("unknown constructor in tree is rejected", testUnknownConstructor)
|
|
, ("redundant clause is detected", testRedundant)
|
|
, ("useful clause example selects its clause", testExample)
|
|
, ("overlapping nested patterns", testOverlapping)
|
|
, ("deterministic generated matches agree", testGenerated)
|
|
]
|
|
|
|
testSpecialise :: Bool
|
|
testSpecialise =
|
|
let env = envOk listProgram
|
|
listInt = TName "List" [intType]
|
|
matrix = [[PCon "Cons" [PVar "x", PVar "xs"]], [PWild]]
|
|
specialised = specialize env (KeyCon "Cons") matrix
|
|
in length specialised == 2 && all ((== 2) . length) specialised
|
|
|
|
testDefault :: Bool
|
|
testDefault =
|
|
let env = envOk listProgram
|
|
matrix = [[PCon "Cons" [PVar "x", PVar "xs"]], [PWild]]
|
|
in defaultMatrix matrix == [[]] && Map.size (envConstructorTypes env) > 0
|
|
|
|
testBooleanWitness :: Bool
|
|
testBooleanWitness =
|
|
let env = envSource "data Flag = On | Off\n"
|
|
outcome = witness env 100 [TName "Flag" []] [[PCon "On" []]]
|
|
in case outcome of
|
|
NotCovered [PCon "Off" []] -> True
|
|
_ -> False
|
|
|
|
testBooleanCoverage :: Bool
|
|
testBooleanCoverage =
|
|
let env = envSource "data Flag = On | Off\n"
|
|
outcome = witness env 100 [TName "Flag" []] [[PCon "On" []], [PCon "Off" []]]
|
|
in outcome == Covered
|
|
|
|
testIntegerWitness :: Bool
|
|
testIntegerWitness =
|
|
let env = envSource "data Flag = On | Off\n"
|
|
outcome = witness env 100 [intType] [[PInt 0], [PInt 1]]
|
|
in case outcome of
|
|
NotCovered [PInt n] -> n == 2
|
|
_ -> False
|
|
|
|
testMultipleArguments :: Bool
|
|
testMultipleArguments =
|
|
let env = envSource "data Flag = On | Off\n"
|
|
matrix = [[PCon "On" [], PCon "On" []], [PCon "On" [], PCon "Off" []], [PCon "Off" [], PCon "On" []]]
|
|
outcome = witness env 200 [TName "Flag" [], TName "Flag" []] matrix
|
|
in case outcome of
|
|
NotCovered [PCon "Off" [], PCon "Off" []] -> True
|
|
_ -> False
|
|
|
|
testRecursiveList :: Bool
|
|
testRecursiveList =
|
|
let env = envOk listProgram
|
|
matrix = [[PCon "Nil" []], [PCon "Cons" [PWild, PWild]]]
|
|
outcome = witness env 200 [TName "List" [intType]] matrix
|
|
in outcome == Covered
|
|
|
|
testUninhabited :: Bool
|
|
testUninhabited =
|
|
let program = parseOk "data Loop = Loop Loop\n\nmatch spin (x : Loop) : Int =\n | Loop y -> 0\n"
|
|
env = envOk program
|
|
matrix = [[PCon "Loop" [PVar "y"]]]
|
|
outcome = witness env 200 [TName "Loop" []] matrix
|
|
inhabitants = finiteInhabitants env
|
|
in outcome == Covered && Map.findWithDefault True "Loop" inhabitants == False
|
|
|
|
testBinding :: Bool
|
|
testBinding =
|
|
let program = parseOk "data Pair a b = MkPair a b\n\nmatch first (p : Pair Int Int) : Int =\n | MkPair x y -> x + y\n"
|
|
env = envOk program
|
|
match' = matchOf "first" program
|
|
tree = treeOf env Leftmost match'
|
|
value = valueOf env "MkPair 4 5"
|
|
in evaluateCompiled env (matchClauses match') tree [value] == Right (VInt 9)
|
|
&& evaluateSource env (matchClauses match') [value] == Right (VInt 9)
|
|
|
|
testAgreement :: Bool
|
|
testAgreement =
|
|
let program = parseOk "data Flag = On | Off\n\nmatch both (a : Flag) (b : Flag) : Int =\n | On On -> 1\n | On Off -> 2\n | Off On -> 3\n | Off Off -> 4\n"
|
|
env = envOk program
|
|
match' = matchOf "both" program
|
|
clauses = matchClauses match'
|
|
values = [ [valueOf env "On", valueOf env "On"]
|
|
, [valueOf env "On", valueOf env "Off"]
|
|
, [valueOf env "Off", valueOf env "On"]
|
|
, [valueOf env "Off", valueOf env "Off"]
|
|
]
|
|
leftmost = treeOf env Leftmost match'
|
|
heuristic = treeOf env Heuristic match'
|
|
in all (\v -> evaluateSource env clauses v == evaluateCompiled env clauses leftmost v
|
|
&& evaluateSource env clauses v == evaluateCompiled env clauses heuristic v) values
|
|
|
|
testRoundTrip :: Bool
|
|
testRoundTrip =
|
|
let source = "data Flag = On | Off\n\nmatch flag (f : Flag) : Int =\n | On -> 1\n | Off -> 0\n"
|
|
program = parseOk source
|
|
env = envOk program
|
|
match' = matchOf "flag" program
|
|
tree = treeOf env Heuristic match'
|
|
encoded = encodeArtifact "flag" source Heuristic tree
|
|
in case decodeArtifact encoded of
|
|
Left _ -> False
|
|
Right artifact -> artifactTree artifact == tree
|
|
|
|
testMalformedTree :: Bool
|
|
testMalformedTree =
|
|
case decodeArtifact "tessera-tree 1\nfunction x\ntree W[\nsource-begin\nsource-end\n" of
|
|
Left _ -> True
|
|
Right _ -> False
|
|
|
|
testUnknownConstructor :: Bool
|
|
testUnknownConstructor =
|
|
let source = "data Flag = On | Off\n\nmatch flag (f : Flag) : Int =\n | On -> 1\n | Off -> 0\n"
|
|
encoded = "tessera-tree 1\nfunction flag\nstrategy leftmost\ntree W[0]{cNope:L0;}[X]\nsource-begin\n" ++ source ++ "source-end\n"
|
|
in case decodeArtifact encoded of
|
|
Left message -> "unknown constructor" `isInfixOf` message
|
|
Right _ -> False
|
|
|
|
testRedundant :: Bool
|
|
testRedundant =
|
|
let program = parseOk "data Flag = On | Off\n\nmatch flag (f : Flag) : Int =\n | On -> 1\n | _ -> 0\n | Off -> 2\n"
|
|
env = envOk program
|
|
report = case analyzeMatch env (matchOf "flag" program) of
|
|
Just r -> r
|
|
Nothing -> error "no report"
|
|
statuses = map reportClauseStatus (reportClauseReports report)
|
|
in statuses == [ClauseUseful, ClauseUseful, ClauseRedundant]
|
|
|
|
testExample :: Bool
|
|
testExample =
|
|
let program = parseOk "data Flag = On | Off\n\nmatch flag (f : Flag) : Int =\n | On -> 1\n | Off -> 0\n"
|
|
env = envOk program
|
|
report = case analyzeMatch env (matchOf "flag" program) of
|
|
Just r -> r
|
|
Nothing -> error "no report"
|
|
examples = [example | ClauseReport _ ClauseUseful (Just example) <- reportClauseReports report]
|
|
in length examples == 2
|
|
|
|
testOverlapping :: Bool
|
|
testOverlapping =
|
|
let program = parseOk "data Option a = None | Some a\n\nmatch pick (o : Option Int) : Int =\n | Some x -> x\n | Some 0 -> 1\n | None -> 0\n"
|
|
env = envOk program
|
|
report = case analyzeMatch env (matchOf "pick" program) of
|
|
Just r -> r
|
|
Nothing -> error "no report"
|
|
statuses = map reportClauseStatus (reportClauseReports report)
|
|
in statuses == [ClauseUseful, ClauseRedundant, ClauseUseful]
|
|
|
|
testGenerated :: Bool
|
|
testGenerated =
|
|
let generated = [ "match f (a : Flag) (b : Flag) : Int =\n | " ++ renderPattern a ++ " " ++ renderPattern b ++ " -> 0\n"
|
|
| (a, b) <- [(True, True), (True, False), (False, True)]
|
|
]
|
|
source = "data Flag = On | Off\n\n" ++ concat generated
|
|
program = parseOk source
|
|
env = envOk program
|
|
match' = matchOf "f" program
|
|
leftmost = treeOf env Leftmost match'
|
|
heuristic = treeOf env Heuristic match'
|
|
values = [[valueOf env "On", valueOf env "On"], [valueOf env "On", valueOf env "Off"], [valueOf env "Off", valueOf env "On"], [valueOf env "Off", valueOf env "Off"]]
|
|
in all (\v -> evaluateCompiled env (matchClauses match') leftmost v == evaluateCompiled env (matchClauses match') heuristic v) values
|
|
|
|
renderPattern :: Bool -> String
|
|
renderPattern True = "On"
|
|
renderPattern False = "Off"
|