sneeker/tessera
1
10 Fork 2
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Compare commits

base: sneeker/tessera:2cbbe7bb4966ad549cf9949790acc3e85a9d7fc1
sneeker/tessera:master
..
compare: sneeker/tessera:9317226bb37195a63cc1a2eb241281480f14c506
sneeker/tessera:master
10 Commits
2cbbe7bb49 .. 9317226bb3
Author SHA1 Message Date
milner 9317226bb3 differentially validate coverage witnesses and compiled dispatch 2020-03-25 12:00:00 +00:00
milner 819e78225c implement protocol ast and instruction-selection examples 2020-03-18 12:00:00 +00:00
milner d38ebcf1b5 render labelled decision trees as graphviz diagrams 2020-03-13 12:00:00 +00:00
milner b61a0893a3 persist trees and expose execution and diagnostic commands 2020-03-09 12:00:00 +00:00
milner d543c82e41 select decision columns using inspection-cost heuristics 2020-03-04 12:00:00 +00:00
milner d584e97680 compile matches into executable decision trees 2020-02-28 12:00:00 +00:00
milner a37d3975ed analyse finite inhabitants of recursive type declarations 2020-02-24 12:00:00 +00:00
milner 41291e8405 construct missing-case witnesses for finite and integer domains 2020-02-19 12:00:00 +00:00
milner 536ecdf0cf check match coverage across multiple arguments 2020-02-14 12:00:00 +00:00
milner 7e1d712e85 detect redundant clauses through usefulness analysis 2020-02-10 12:00:00 +00:00
23 changed files with 1419 additions and 0 deletions
Expand all files Collapse all files

No files matched your search

.gitignore
+1
View File
@@ -1,4 +1,5 @@
dist/ dist/
dist-newstyle/
.toolchain/ .toolchain/
*.o *.o
*.hi *.hi
README.md
+1
View File
@@ -0,0 +1 @@
<p align="center"><img src="artifacts/tessera-demo.gif" alt="a light theme vim session showing a missing case witness, the fix, the recheck, the compiled run and the strategy comparison"></p>
app/Main.hs
+265
View File
@@ -0,0 +1,265 @@
module Main where
import Control.Exception (SomeException, try)
import Data.List (foldl', intercalate, isSuffixOf)
import Data.Maybe (fromMaybe, mapMaybe)
import qualified Data.Map.Strict as Map
import Data.Time.Clock (diffUTCTime, getCurrentTime)
import System.Directory (doesDirectoryExist, listDirectory)
import System.Environment (getArgs, getProgName)
import System.Exit (exitFailure, exitSuccess)
import System.IO (hPutStrLn, stderr)
import Tessera.Analyze
import Tessera.Check (checkProgram)
import Tessera.Env (Env, envConstructorTypes)
import Tessera.Eval
import Tessera.Graph (renderDot)
import Tessera.Parser (parseExpression, parseProgram)
import Tessera.Serialize hiding (renderDiagnostic)
import Tessera.Syntax
import Tessera.Tree
main :: IO ()
main = do
arguments <- getArgs
case arguments of
("check" : file : rest) -> commandCheck file rest
("explain" : file : rest) -> commandExplain file rest
("compile" : file : rest) -> commandCompile file rest
("run" : file : rest) -> commandRun file rest
("graph" : file : rest) -> commandGraph file rest
("bench" : directory : rest) -> commandBench directory rest
_ -> usage
usage :: IO ()
usage = do
name <- getProgName
hPutStrLn stderr ("usage: " ++ name ++ " <check|explain|compile|run|graph|bench> ...")
exitFailure
optionValue :: String -> [String] -> Maybe String
optionValue name arguments = case dropWhile (/= name) arguments of
(_ : value : _) -> Just value
_ -> Nothing
strategyFrom :: [String] -> Strategy
strategyFrom arguments = case optionValue "--strategy" arguments of
Just "heuristic" -> Heuristic
_ -> Leftmost
loadProgram :: FilePath -> IO Program
loadProgram file = do
source <- readFile file
case parseProgram source of
Left diagnostic -> do
hPutStrLn stderr (renderDiagnostic diagnostic)
exitFailure
Right program -> return program
loadEnv :: Program -> IO Env
loadEnv program = case checkProgram program of
Left diagnostic -> do
hPutStrLn stderr (renderDiagnostic diagnostic)
exitFailure
Right env -> return env
renderDiagnostic :: Diagnostic -> String
renderDiagnostic (Diagnostic span' message) =
"line " ++ show (spanLine span') ++ " column " ++ show (spanColumn span') ++ ": " ++ message
renderType :: Type -> String
renderType ty = case ty of
TVar name -> name
TName name [] -> name
TName name arguments -> name ++ " " ++ unwords (map renderType arguments)
TTuple elements -> "(" ++ intercalate ", " (map renderType elements) ++ ")"
renderMatchReport :: MatchReport -> [String]
renderMatchReport report =
[ "match " ++ reportMatchName report
, if reportInconclusive report
then " coverage: inconclusive within the configured budget"
else if reportExhaustive report
then " coverage: exhaustive"
else " coverage: missing " ++ maybe "" (intercalate ", " . map renderValue) (reportMissingCase report)
]
++ concatMap renderClause (reportClauseReports report)
where
renderClause clause =
let status = case reportClauseStatus clause of
ClauseUseful -> "useful"
ClauseRedundant -> "redundant"
example = case reportClauseExample clause of
Just values -> " example " ++ intercalate ", " (map renderValue values)
Nothing -> ""
in [" clause " ++ show (reportClauseIndex clause) ++ ": " ++ status ++ example]
commandCheck :: FilePath -> [String] -> IO ()
commandCheck file _ = do
program <- loadProgram file
env <- loadEnv program
let reports = mapMaybe (analyzeMatch env) program
failures = [report | report <- reports, not (reportExhaustive report) || hasRedundant report]
output = concatMap renderMatchReport reports
mapM_ putStrLn output
if null failures then exitSuccess else exitFailure
where
hasRedundant report = any ((== ClauseRedundant) . reportClauseStatus) (reportClauseReports report)
commandExplain :: FilePath -> [String] -> IO ()
commandExplain file arguments = do
program <- loadProgram file
env <- loadEnv program
case optionValue "--function" arguments of
Nothing -> do
hPutStrLn stderr "explain requires --function"
exitFailure
Just name -> case mapMaybe (analyzeMatch env) program of
reports -> case filter ((== name) . reportMatchName) reports of
(report : _) -> do
mapM_ putStrLn (renderMatchReport report)
putStrLn "inhabited types"
mapM_ (\(typeName, flag) -> putStrLn (" " ++ typeName ++ ": " ++ if flag then "inhabited" else "uninhabited")) (Map.toList (reportInhabitedTypes report))
exitSuccess
[] -> do
hPutStrLn stderr ("unknown function " ++ name)
exitFailure
commandCompile :: FilePath -> [String] -> IO ()
commandCompile file arguments = do
source <- readFile file
program <- case parseProgram source of
Left diagnostic -> hPutStrLn stderr (renderDiagnostic diagnostic) >> exitFailure
Right p -> return p
env <- loadEnv program
case optionValue "--function" arguments of
Nothing -> hPutStrLn stderr "compile requires --function" >> exitFailure
Just name -> case findMatch name program of
Nothing -> hPutStrLn stderr ("unknown function " ++ name) >> exitFailure
Just match' -> do
let strategy = strategyFrom arguments
tree = compileMatchFor env strategy match'
output = fromMaybe (name ++ ".tree") (optionValue "-o" arguments)
writeFile output (encodeArtifact name source strategy tree)
putStrLn ("wrote " ++ output ++ " with " ++ strategyName strategy ++ " strategy, " ++ show (treeSize tree) ++ " nodes")
commandRun :: FilePath -> [String] -> IO ()
commandRun file arguments = do
content <- readFile file
artifact <- case decodeArtifact content of
Left message -> hPutStrLn stderr message >> exitFailure
Right a -> return a
case optionValue "--function" arguments of
Nothing -> hPutStrLn stderr "run requires --function" >> exitFailure
Just name -> case findMatch name (artifactProgram artifact) of
Nothing -> hPutStrLn stderr ("unknown function " ++ name) >> exitFailure
Just match' -> case optionValue "--input" arguments of
Nothing -> hPutStrLn stderr "run requires --input" >> exitFailure
Just inputFile -> do
inputText <- readFile inputFile
let arities = Map.toList (Map.map (length . snd) (envConstructorTypes (artifactEnv artifact)))
values <- case parseInputs (artifactEnv artifact) arities inputText of
Left message -> hPutStrLn stderr message >> exitFailure
Right v -> return v
results <- mapM (runOne (artifactEnv artifact) match' (artifactTree artifact)) values
if and results then exitSuccess else exitFailure
where
runOne env match' tree values = do
let compiled = evaluateCompiled env (matchClauses match') tree values
sourceResult = evaluateSource env (matchClauses match') values
case (compiled, sourceResult) of
(Right a, Right b) -> do
putStrLn (intercalate ", " (map renderValue values) ++ " => " ++ renderValue a ++ (if a == b then "" else " (source disagrees: " ++ renderValue b ++ ")"))
return (a == b)
(Left message, _) -> do
putStrLn (intercalate ", " (map renderValue values) ++ " => error " ++ message)
return False
(_, Left message) -> do
putStrLn (intercalate ", " (map renderValue values) ++ " => source error " ++ message)
return False
commandGraph :: FilePath -> [String] -> IO ()
commandGraph file arguments = do
content <- readFile file
artifact <- case decodeArtifact content of
Left message -> hPutStrLn stderr message >> exitFailure
Right a -> return a
let output = fromMaybe "tree.dot" (optionValue "-o" arguments)
writeFile output (renderDot (artifactTree artifact))
putStrLn ("wrote " ++ output)
commandBench :: FilePath -> [String] -> IO ()
commandBench directory arguments = do
exists <- doesDirectoryExist directory
if not exists
then hPutStrLn stderr ("not a directory: " ++ directory) >> exitFailure
else do
entries <- listDirectory directory
let files = [directory ++ "/" ++ entry | entry <- entries, ".tess" `isSuffixOf` entry]
mapM_ benchFile files
where
benchFile file = do
program <- loadProgram file
env <- loadEnv program
let matches = [match' | match' <- program, isMatch match']
mapM_ (benchMatch env) matches
benchMatch env match' = do
leftmostStart <- getCurrentTime
let leftmostTree = compileMatchFor env Leftmost match'
leftmostEnd <- getCurrentTime
heuristicStart <- getCurrentTime
let heuristicTree = compileMatchFor env Heuristic match'
heuristicEnd <- getCurrentTime
putStrLn (matchNameOf match')
putStrLn (" leftmost nodes " ++ show (treeSize leftmostTree) ++ " depth " ++ show (treeDepth leftmostTree) ++ " time " ++ show (diffUTCTime leftmostEnd leftmostStart))
putStrLn (" heuristic nodes " ++ show (treeSize heuristicTree) ++ " depth " ++ show (treeDepth heuristicTree) ++ " time " ++ show (diffUTCTime heuristicEnd heuristicStart))
isMatch :: Declaration -> Bool
isMatch (MatchDeclaration _ _ _ _) = True
isMatch _ = False
matchNameOf :: Declaration -> String
matchNameOf (MatchDeclaration name _ _ _) = name
matchNameOf _ = ""
findMatch :: String -> Program -> Maybe Declaration
findMatch name program = case [match' | match' <- program, matchNameOf match' == name, isMatch match'] of
(match' : _) -> Just match'
[] -> Nothing
compileMatchFor :: Env -> Strategy -> Declaration -> Tree
compileMatchFor env strategy (MatchDeclaration _ arguments _ clauses) =
let types = map snd arguments
rows = zip (map clausePatterns clauses) [0 .. length clauses - 1]
in compileMatch env strategy types rows (initialOccurrences (length arguments))
compileMatchFor _ _ _ = Failure
parseInputs :: Env -> [(String, Int)] -> String -> Either String [[Value]]
parseInputs env arities text = go (filter (not . null) (lines text)) []
where
go [] acc = Right (reverse acc)
go (line : rest) acc = case parseInputLine env arities line of
Left message -> Left message
Right values -> go rest (values : acc)
parseInputLine :: Env -> [(String, Int)] -> String -> Either String [Value]
parseInputLine env arities line =
let pieces = map trim (splitSemicolon line)
in mapM parsePiece pieces
where
parsePiece piece = case parseExpression arities piece of
Left diagnostic -> Left ("input parse error: " ++ renderDiagnostic diagnostic)
Right expression -> case evalExpr env Map.empty expression of
Left message -> Left message
Right value -> Right value
trim :: String -> String
trim = reverse . dropWhile (== ' ') . reverse . dropWhile (== ' ')
splitSemicolon :: String -> [String]
splitSemicolon [] = [""]
splitSemicolon text = case break (== ';') text of
(piece, []) -> [piece]
(piece, _ : rest) -> piece : splitSemicolon rest
artifacts/protocol-complete-tree.dot
+42
View File
@@ -0,0 +1,42 @@
digraph tessera {
graph [bgcolor="white", rankdir=TB, nodesep=0.35, ranksep=0.5];
node [shape=box, style="rounded,filled", color="#444444", fontcolor="#1c1c1a", fillcolor="#ffffff", fontname="Helvetica", fontsize=11];
edge [color="#666666", fontcolor="#333333", fontname="Helvetica", fontsize=10];
n0 [label="switch 0", fillcolor="#f7f7f5"];
n1 [label="switch 1", fillcolor="#f7f7f5"];
n2 [label="bind 1.0 n"];
n3 [label="clause 0", fillcolor="#e7efe4"];
n4 [label="bind 1.0 n"];
n5 [label="clause 1", fillcolor="#e7efe4"];
n6 [label="clause 2", fillcolor="#e7efe4"];
n7 [label="switch 1", fillcolor="#f7f7f5"];
n8 [label="bind 1.0 n"];
n9 [label="clause 3", fillcolor="#e7efe4"];
n10 [label="bind 1.0 n"];
n11 [label="clause 4", fillcolor="#e7efe4"];
n12 [label="clause 5", fillcolor="#e7efe4"];
n13 [label="switch 1", fillcolor="#f7f7f5"];
n14 [label="bind 1.0 n"];
n15 [label="clause 6", fillcolor="#e7efe4"];
n16 [label="bind 1.0 n"];
n17 [label="clause 7", fillcolor="#e7efe4"];
n18 [label="clause 8", fillcolor="#e7efe4"];
n0 -> n1 [label="Idle"];
n0 -> n7 [label="Waiting"];
n0 -> n13 [label="Connected"];
n1 -> n2 [label="Hello"];
n1 -> n4 [label="Data"];
n1 -> n6 [label="Close"];
n2 -> n3 [label="bind"];
n4 -> n5 [label="bind"];
n7 -> n8 [label="Hello"];
n7 -> n10 [label="Data"];
n7 -> n12 [label="Close"];
n8 -> n9 [label="bind"];
n10 -> n11 [label="bind"];
n13 -> n14 [label="Hello"];
n13 -> n16 [label="Data"];
n13 -> n18 [label="Close"];
n14 -> n15 [label="bind"];
n16 -> n17 [label="bind"];
}
artifacts/protocol-complete-tree.png
BIN
View File
Binary file not shown.
Side by Side

After

Width:  |  Height:  |  Size: 47 KiB

artifacts/protocol-complete-tree.svg
+253
View File
@@ -0,0 +1,253 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN"
"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
<!-- Generated by graphviz version 16.0.0 (0)
-->
<!-- Title: tessera Pages: 1 -->
<svg width="757pt" height="296pt"
viewBox="0.00 0.00 757.00 296.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
<g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 292)">
<title>tessera</title>
<polygon fill="white" stroke="none" points="-4,4 -4,-292 752.5,-292 752.5,4 -4,4"/>
<!-- n0 -->
<g id="node1" class="node">
<title>n0</title>
<path fill="#f7f7f5" stroke="#444444" d="M393.12,-288C393.12,-288 362.12,-288 362.12,-288 356.12,-288 350.12,-282 350.12,-276 350.12,-276 350.12,-264 350.12,-264 350.12,-258 356.12,-252 362.12,-252 362.12,-252 393.12,-252 393.12,-252 399.12,-252 405.12,-258 405.12,-264 405.12,-264 405.12,-276 405.12,-276 405.12,-282 399.12,-288 393.12,-288"/>
<text xml:space="preserve" text-anchor="middle" x="377.62" y="-266.3" font-family="Helvetica,sans-Serif" font-size="11.00" fill="#1c1c1a">switch 0</text>
</g>
<!-- n1 -->
<g id="node2" class="node">
<title>n1</title>
<path fill="#f7f7f5" stroke="#444444" d="M186.12,-204C186.12,-204 155.12,-204 155.12,-204 149.12,-204 143.12,-198 143.12,-192 143.12,-192 143.12,-180 143.12,-180 143.12,-174 149.12,-168 155.12,-168 155.12,-168 186.12,-168 186.12,-168 192.12,-168 198.12,-174 198.12,-180 198.12,-180 198.12,-192 198.12,-192 198.12,-198 192.12,-204 186.12,-204"/>
<text xml:space="preserve" text-anchor="middle" x="170.62" y="-182.3" font-family="Helvetica,sans-Serif" font-size="11.00" fill="#1c1c1a">switch 1</text>
</g>
<!-- n0&#45;&gt;n1 -->
<g id="edge1" class="edge">
<title>n0&#45;&gt;n1</title>
<path fill="none" stroke="#666666" d="M349.71,-257.94C313.42,-243.57 249.87,-218.39 209.05,-202.22"/>
<polygon fill="#666666" stroke="#666666" points="210.42,-199 199.84,-198.57 207.84,-205.51 210.42,-199"/>
<text xml:space="preserve" text-anchor="middle" x="294.39" y="-224.5" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#333333">Idle</text>
</g>
<!-- n7 -->
<g id="node8" class="node">
<title>n7</title>
<path fill="#f7f7f5" stroke="#444444" d="M393.12,-204C393.12,-204 362.12,-204 362.12,-204 356.12,-204 350.12,-198 350.12,-192 350.12,-192 350.12,-180 350.12,-180 350.12,-174 356.12,-168 362.12,-168 362.12,-168 393.12,-168 393.12,-168 399.12,-168 405.12,-174 405.12,-180 405.12,-180 405.12,-192 405.12,-192 405.12,-198 399.12,-204 393.12,-204"/>
<text xml:space="preserve" text-anchor="middle" x="377.62" y="-182.3" font-family="Helvetica,sans-Serif" font-size="11.00" fill="#1c1c1a">switch 1</text>
</g>
<!-- n0&#45;&gt;n7 -->
<g id="edge2" class="edge">
<title>n0&#45;&gt;n7</title>
<path fill="none" stroke="#666666" d="M377.62,-251.61C377.62,-241.17 377.62,-227.64 377.62,-215.66"/>
<polygon fill="#666666" stroke="#666666" points="381.13,-215.88 377.63,-205.88 374.13,-215.88 381.13,-215.88"/>
<text xml:space="preserve" text-anchor="middle" x="393.75" y="-224.5" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#333333">Waiting</text>
</g>
<!-- n13 -->
<g id="node14" class="node">
<title>n13</title>
<path fill="#f7f7f5" stroke="#444444" d="M607.12,-204C607.12,-204 576.12,-204 576.12,-204 570.12,-204 564.12,-198 564.12,-192 564.12,-192 564.12,-180 564.12,-180 564.12,-174 570.12,-168 576.12,-168 576.12,-168 607.12,-168 607.12,-168 613.12,-168 619.12,-174 619.12,-180 619.12,-180 619.12,-192 619.12,-192 619.12,-198 613.12,-204 607.12,-204"/>
<text xml:space="preserve" text-anchor="middle" x="591.62" y="-182.3" font-family="Helvetica,sans-Serif" font-size="11.00" fill="#1c1c1a">switch 1</text>
</g>
<!-- n0&#45;&gt;n13 -->
<g id="edge3" class="edge">
<title>n0&#45;&gt;n13</title>
<path fill="none" stroke="#666666" d="M405.6,-258.28C443.33,-243.82 510.68,-218.02 553.15,-201.74"/>
<polygon fill="#666666" stroke="#666666" points="554.14,-205.11 562.23,-198.26 551.64,-198.57 554.14,-205.11"/>
<text xml:space="preserve" text-anchor="middle" x="521.06" y="-224.5" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#333333">Connected</text>
</g>
<!-- n2 -->
<g id="node3" class="node">
<title>n2</title>
<path fill="#ffffff" stroke="#444444" d="M51.25,-120C51.25,-120 12,-120 12,-120 6,-120 0,-114 0,-108 0,-108 0,-96 0,-96 0,-90 6,-84 12,-84 12,-84 51.25,-84 51.25,-84 57.25,-84 63.25,-90 63.25,-96 63.25,-96 63.25,-108 63.25,-108 63.25,-114 57.25,-120 51.25,-120"/>
<text xml:space="preserve" text-anchor="middle" x="31.62" y="-98.3" font-family="Helvetica,sans-Serif" font-size="11.00" fill="#1c1c1a">bind 1.0 n</text>
</g>
<!-- n1&#45;&gt;n2 -->
<g id="edge4" class="edge">
<title>n1&#45;&gt;n2</title>
<path fill="none" stroke="#666666" d="M142.83,-168.6C122.13,-156.39 93.59,-139.55 70.6,-125.99"/>
<polygon fill="#666666" stroke="#666666" points="72.5,-123.05 62.11,-120.99 68.95,-129.08 72.5,-123.05"/>
<text xml:space="preserve" text-anchor="middle" x="120.7" y="-140.5" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#333333">Hello</text>
</g>
<!-- n4 -->
<g id="node5" class="node">
<title>n4</title>
<path fill="#ffffff" stroke="#444444" d="M139.25,-120C139.25,-120 100,-120 100,-120 94,-120 88,-114 88,-108 88,-108 88,-96 88,-96 88,-90 94,-84 100,-84 100,-84 139.25,-84 139.25,-84 145.25,-84 151.25,-90 151.25,-96 151.25,-96 151.25,-108 151.25,-108 151.25,-114 145.25,-120 139.25,-120"/>
<text xml:space="preserve" text-anchor="middle" x="119.62" y="-98.3" font-family="Helvetica,sans-Serif" font-size="11.00" fill="#1c1c1a">bind 1.0 n</text>
</g>
<!-- n1&#45;&gt;n4 -->
<g id="edge5" class="edge">
<title>n1&#45;&gt;n4</title>
<path fill="none" stroke="#666666" d="M159.81,-167.61C152.98,-156.63 144.02,-142.22 136.29,-129.8"/>
<polygon fill="#666666" stroke="#666666" points="139.48,-128.29 131.22,-121.65 133.53,-131.99 139.48,-128.29"/>
<text xml:space="preserve" text-anchor="middle" x="158.68" y="-140.5" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#333333">Data</text>
</g>
<!-- n6 -->
<g id="node7" class="node">
<title>n6</title>
<path fill="#e7efe4" stroke="#444444" d="M220.5,-120C220.5,-120 188.75,-120 188.75,-120 182.75,-120 176.75,-114 176.75,-108 176.75,-108 176.75,-96 176.75,-96 176.75,-90 182.75,-84 188.75,-84 188.75,-84 220.5,-84 220.5,-84 226.5,-84 232.5,-90 232.5,-96 232.5,-96 232.5,-108 232.5,-108 232.5,-114 226.5,-120 220.5,-120"/>
<text xml:space="preserve" text-anchor="middle" x="204.62" y="-98.3" font-family="Helvetica,sans-Serif" font-size="11.00" fill="#1c1c1a">clause 2</text>
</g>
<!-- n1&#45;&gt;n6 -->
<g id="edge6" class="edge">
<title>n1&#45;&gt;n6</title>
<path fill="none" stroke="#666666" d="M177.84,-167.61C182.25,-156.96 188.01,-143.07 193.05,-130.91"/>
<polygon fill="#666666" stroke="#666666" points="196.25,-132.34 196.85,-121.76 189.78,-129.66 196.25,-132.34"/>
<text xml:space="preserve" text-anchor="middle" x="202.41" y="-140.5" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#333333">Close</text>
</g>
<!-- n3 -->
<g id="node4" class="node">
<title>n3</title>
<path fill="#e7efe4" stroke="#444444" d="M47.5,-36C47.5,-36 15.75,-36 15.75,-36 9.75,-36 3.75,-30 3.75,-24 3.75,-24 3.75,-12 3.75,-12 3.75,-6 9.75,0 15.75,0 15.75,0 47.5,0 47.5,0 53.5,0 59.5,-6 59.5,-12 59.5,-12 59.5,-24 59.5,-24 59.5,-30 53.5,-36 47.5,-36"/>
<text xml:space="preserve" text-anchor="middle" x="31.62" y="-14.3" font-family="Helvetica,sans-Serif" font-size="11.00" fill="#1c1c1a">clause 0</text>
</g>
<!-- n2&#45;&gt;n3 -->
<g id="edge7" class="edge">
<title>n2&#45;&gt;n3</title>
<path fill="none" stroke="#666666" d="M31.62,-83.61C31.62,-73.17 31.62,-59.64 31.62,-47.66"/>
<polygon fill="#666666" stroke="#666666" points="35.13,-47.88 31.63,-37.88 28.13,-47.88 35.13,-47.88"/>
<text xml:space="preserve" text-anchor="middle" x="40.62" y="-56.5" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#333333">bind</text>
</g>
<!-- n5 -->
<g id="node6" class="node">
<title>n5</title>
<path fill="#e7efe4" stroke="#444444" d="M135.5,-36C135.5,-36 103.75,-36 103.75,-36 97.75,-36 91.75,-30 91.75,-24 91.75,-24 91.75,-12 91.75,-12 91.75,-6 97.75,0 103.75,0 103.75,0 135.5,0 135.5,0 141.5,0 147.5,-6 147.5,-12 147.5,-12 147.5,-24 147.5,-24 147.5,-30 141.5,-36 135.5,-36"/>
<text xml:space="preserve" text-anchor="middle" x="119.62" y="-14.3" font-family="Helvetica,sans-Serif" font-size="11.00" fill="#1c1c1a">clause 1</text>
</g>
<!-- n4&#45;&gt;n5 -->
<g id="edge8" class="edge">
<title>n4&#45;&gt;n5</title>
<path fill="none" stroke="#666666" d="M119.62,-83.61C119.62,-73.17 119.62,-59.64 119.62,-47.66"/>
<polygon fill="#666666" stroke="#666666" points="123.13,-47.88 119.63,-37.88 116.13,-47.88 123.13,-47.88"/>
<text xml:space="preserve" text-anchor="middle" x="128.62" y="-56.5" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#333333">bind</text>
</g>
<!-- n8 -->
<g id="node9" class="node">
<title>n8</title>
<path fill="#ffffff" stroke="#444444" d="M309.25,-120C309.25,-120 270,-120 270,-120 264,-120 258,-114 258,-108 258,-108 258,-96 258,-96 258,-90 264,-84 270,-84 270,-84 309.25,-84 309.25,-84 315.25,-84 321.25,-90 321.25,-96 321.25,-96 321.25,-108 321.25,-108 321.25,-114 315.25,-120 309.25,-120"/>
<text xml:space="preserve" text-anchor="middle" x="289.62" y="-98.3" font-family="Helvetica,sans-Serif" font-size="11.00" fill="#1c1c1a">bind 1.0 n</text>
</g>
<!-- n7&#45;&gt;n8 -->
<g id="edge9" class="edge">
<title>n7&#45;&gt;n8</title>
<path fill="none" stroke="#666666" d="M358.96,-167.61C346.6,-156.09 330.18,-140.79 316.42,-127.97"/>
<polygon fill="#666666" stroke="#666666" points="319.07,-125.65 309.37,-121.4 314.3,-130.77 319.07,-125.65"/>
<text xml:space="preserve" text-anchor="middle" x="350.14" y="-140.5" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#333333">Hello</text>
</g>
<!-- n10 -->
<g id="node11" class="node">
<title>n10</title>
<path fill="#ffffff" stroke="#444444" d="M397.25,-120C397.25,-120 358,-120 358,-120 352,-120 346,-114 346,-108 346,-108 346,-96 346,-96 346,-90 352,-84 358,-84 358,-84 397.25,-84 397.25,-84 403.25,-84 409.25,-90 409.25,-96 409.25,-96 409.25,-108 409.25,-108 409.25,-114 403.25,-120 397.25,-120"/>
<text xml:space="preserve" text-anchor="middle" x="377.62" y="-98.3" font-family="Helvetica,sans-Serif" font-size="11.00" fill="#1c1c1a">bind 1.0 n</text>
</g>
<!-- n7&#45;&gt;n10 -->
<g id="edge10" class="edge">
<title>n7&#45;&gt;n10</title>
<path fill="none" stroke="#666666" d="M377.62,-167.61C377.62,-157.17 377.62,-143.64 377.62,-131.66"/>
<polygon fill="#666666" stroke="#666666" points="381.13,-131.88 377.63,-121.88 374.13,-131.88 381.13,-131.88"/>
<text xml:space="preserve" text-anchor="middle" x="388.12" y="-140.5" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#333333">Data</text>
</g>
<!-- n12 -->
<g id="node13" class="node">
<title>n12</title>
<path fill="#e7efe4" stroke="#444444" d="M478.5,-120C478.5,-120 446.75,-120 446.75,-120 440.75,-120 434.75,-114 434.75,-108 434.75,-108 434.75,-96 434.75,-96 434.75,-90 440.75,-84 446.75,-84 446.75,-84 478.5,-84 478.5,-84 484.5,-84 490.5,-90 490.5,-96 490.5,-96 490.5,-108 490.5,-108 490.5,-114 484.5,-120 478.5,-120"/>
<text xml:space="preserve" text-anchor="middle" x="462.62" y="-98.3" font-family="Helvetica,sans-Serif" font-size="11.00" fill="#1c1c1a">clause 5</text>
</g>
<!-- n7&#45;&gt;n12 -->
<g id="edge11" class="edge">
<title>n7&#45;&gt;n12</title>
<path fill="none" stroke="#666666" d="M395.65,-167.61C407.48,-156.19 423.16,-141.08 436.37,-128.33"/>
<polygon fill="#666666" stroke="#666666" points="438.77,-130.88 443.54,-121.42 433.91,-125.84 438.77,-130.88"/>
<text xml:space="preserve" text-anchor="middle" x="437.96" y="-140.5" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#333333">Close</text>
</g>
<!-- n9 -->
<g id="node10" class="node">
<title>n9</title>
<path fill="#e7efe4" stroke="#444444" d="M305.5,-36C305.5,-36 273.75,-36 273.75,-36 267.75,-36 261.75,-30 261.75,-24 261.75,-24 261.75,-12 261.75,-12 261.75,-6 267.75,0 273.75,0 273.75,0 305.5,0 305.5,0 311.5,0 317.5,-6 317.5,-12 317.5,-12 317.5,-24 317.5,-24 317.5,-30 311.5,-36 305.5,-36"/>
<text xml:space="preserve" text-anchor="middle" x="289.62" y="-14.3" font-family="Helvetica,sans-Serif" font-size="11.00" fill="#1c1c1a">clause 3</text>
</g>
<!-- n8&#45;&gt;n9 -->
<g id="edge12" class="edge">
<title>n8&#45;&gt;n9</title>
<path fill="none" stroke="#666666" d="M289.62,-83.61C289.62,-73.17 289.62,-59.64 289.62,-47.66"/>
<polygon fill="#666666" stroke="#666666" points="293.13,-47.88 289.63,-37.88 286.13,-47.88 293.13,-47.88"/>
<text xml:space="preserve" text-anchor="middle" x="298.62" y="-56.5" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#333333">bind</text>
</g>
<!-- n11 -->
<g id="node12" class="node">
<title>n11</title>
<path fill="#e7efe4" stroke="#444444" d="M393.5,-36C393.5,-36 361.75,-36 361.75,-36 355.75,-36 349.75,-30 349.75,-24 349.75,-24 349.75,-12 349.75,-12 349.75,-6 355.75,0 361.75,0 361.75,0 393.5,0 393.5,0 399.5,0 405.5,-6 405.5,-12 405.5,-12 405.5,-24 405.5,-24 405.5,-30 399.5,-36 393.5,-36"/>
<text xml:space="preserve" text-anchor="middle" x="377.62" y="-14.3" font-family="Helvetica,sans-Serif" font-size="11.00" fill="#1c1c1a">clause 4</text>
</g>
<!-- n10&#45;&gt;n11 -->
<g id="edge13" class="edge">
<title>n10&#45;&gt;n11</title>
<path fill="none" stroke="#666666" d="M377.62,-83.61C377.62,-73.17 377.62,-59.64 377.62,-47.66"/>
<polygon fill="#666666" stroke="#666666" points="381.13,-47.88 377.63,-37.88 374.13,-47.88 381.13,-47.88"/>
<text xml:space="preserve" text-anchor="middle" x="386.62" y="-56.5" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#333333">bind</text>
</g>
<!-- n14 -->
<g id="node15" class="node">
<title>n14</title>
<path fill="#ffffff" stroke="#444444" d="M567.25,-120C567.25,-120 528,-120 528,-120 522,-120 516,-114 516,-108 516,-108 516,-96 516,-96 516,-90 522,-84 528,-84 528,-84 567.25,-84 567.25,-84 573.25,-84 579.25,-90 579.25,-96 579.25,-96 579.25,-108 579.25,-108 579.25,-114 573.25,-120 567.25,-120"/>
<text xml:space="preserve" text-anchor="middle" x="547.62" y="-98.3" font-family="Helvetica,sans-Serif" font-size="11.00" fill="#1c1c1a">bind 1.0 n</text>
</g>
<!-- n13&#45;&gt;n14 -->
<g id="edge14" class="edge">
<title>n13&#45;&gt;n14</title>
<path fill="none" stroke="#666666" d="M576.81,-167.52C572.68,-162.12 568.43,-156.01 565.12,-150 561.85,-144.04 558.94,-137.33 556.48,-130.9"/>
<polygon fill="#666666" stroke="#666666" points="559.94,-130.17 553.29,-121.92 553.35,-132.52 559.94,-130.17"/>
<text xml:space="preserve" text-anchor="middle" x="576.38" y="-140.5" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#333333">Hello</text>
</g>
<!-- n16 -->
<g id="node17" class="node">
<title>n16</title>
<path fill="#ffffff" stroke="#444444" d="M655.25,-120C655.25,-120 616,-120 616,-120 610,-120 604,-114 604,-108 604,-108 604,-96 604,-96 604,-90 610,-84 616,-84 616,-84 655.25,-84 655.25,-84 661.25,-84 667.25,-90 667.25,-96 667.25,-96 667.25,-108 667.25,-108 667.25,-114 661.25,-120 655.25,-120"/>
<text xml:space="preserve" text-anchor="middle" x="635.62" y="-98.3" font-family="Helvetica,sans-Serif" font-size="11.00" fill="#1c1c1a">bind 1.0 n</text>
</g>
<!-- n13&#45;&gt;n16 -->
<g id="edge15" class="edge">
<title>n13&#45;&gt;n16</title>
<path fill="none" stroke="#666666" d="M600.96,-167.61C606.79,-156.74 614.43,-142.51 621.05,-130.17"/>
<polygon fill="#666666" stroke="#666666" points="623.95,-132.17 625.59,-121.7 617.78,-128.86 623.95,-132.17"/>
<text xml:space="preserve" text-anchor="middle" x="626.76" y="-140.5" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#333333">Data</text>
</g>
<!-- n18 -->
<g id="node19" class="node">
<title>n18</title>
<path fill="#e7efe4" stroke="#444444" d="M736.5,-120C736.5,-120 704.75,-120 704.75,-120 698.75,-120 692.75,-114 692.75,-108 692.75,-108 692.75,-96 692.75,-96 692.75,-90 698.75,-84 704.75,-84 704.75,-84 736.5,-84 736.5,-84 742.5,-84 748.5,-90 748.5,-96 748.5,-96 748.5,-108 748.5,-108 748.5,-114 742.5,-120 736.5,-120"/>
<text xml:space="preserve" text-anchor="middle" x="720.62" y="-98.3" font-family="Helvetica,sans-Serif" font-size="11.00" fill="#1c1c1a">clause 8</text>
</g>
<!-- n13&#45;&gt;n18 -->
<g id="edge16" class="edge">
<title>n13&#45;&gt;n18</title>
<path fill="none" stroke="#666666" d="M618.98,-167.61C637.8,-155.65 663,-139.63 683.61,-126.53"/>
<polygon fill="#666666" stroke="#666666" points="685.47,-129.5 692.03,-121.18 681.71,-123.59 685.47,-129.5"/>
<text xml:space="preserve" text-anchor="middle" x="676.6" y="-140.5" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#333333">Close</text>
</g>
<!-- n15 -->
<g id="node16" class="node">
<title>n15</title>
<path fill="#e7efe4" stroke="#444444" d="M563.5,-36C563.5,-36 531.75,-36 531.75,-36 525.75,-36 519.75,-30 519.75,-24 519.75,-24 519.75,-12 519.75,-12 519.75,-6 525.75,0 531.75,0 531.75,0 563.5,0 563.5,0 569.5,0 575.5,-6 575.5,-12 575.5,-12 575.5,-24 575.5,-24 575.5,-30 569.5,-36 563.5,-36"/>
<text xml:space="preserve" text-anchor="middle" x="547.62" y="-14.3" font-family="Helvetica,sans-Serif" font-size="11.00" fill="#1c1c1a">clause 6</text>
</g>
<!-- n14&#45;&gt;n15 -->
<g id="edge17" class="edge">
<title>n14&#45;&gt;n15</title>
<path fill="none" stroke="#666666" d="M547.62,-83.61C547.62,-73.17 547.62,-59.64 547.62,-47.66"/>
<polygon fill="#666666" stroke="#666666" points="551.13,-47.88 547.63,-37.88 544.13,-47.88 551.13,-47.88"/>
<text xml:space="preserve" text-anchor="middle" x="556.62" y="-56.5" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#333333">bind</text>
</g>
<!-- n17 -->
<g id="node18" class="node">
<title>n17</title>
<path fill="#e7efe4" stroke="#444444" d="M651.5,-36C651.5,-36 619.75,-36 619.75,-36 613.75,-36 607.75,-30 607.75,-24 607.75,-24 607.75,-12 607.75,-12 607.75,-6 613.75,0 619.75,0 619.75,0 651.5,0 651.5,0 657.5,0 663.5,-6 663.5,-12 663.5,-12 663.5,-24 663.5,-24 663.5,-30 657.5,-36 651.5,-36"/>
<text xml:space="preserve" text-anchor="middle" x="635.62" y="-14.3" font-family="Helvetica,sans-Serif" font-size="11.00" fill="#1c1c1a">clause 7</text>
</g>
<!-- n16&#45;&gt;n17 -->
<g id="edge18" class="edge">
<title>n16&#45;&gt;n17</title>
<path fill="none" stroke="#666666" d="M635.62,-83.61C635.62,-73.17 635.62,-59.64 635.62,-47.66"/>
<polygon fill="#666666" stroke="#666666" points="639.13,-47.88 635.63,-37.88 632.13,-47.88 639.13,-47.88"/>
<text xml:space="preserve" text-anchor="middle" x="644.62" y="-56.5" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#333333">bind</text>
</g>
</g>
</svg>
Side by Side

After

Width:  |  Height:  |  Size: 18 KiB

artifacts/protocol-decision-tree.svg
+123
View File
@@ -0,0 +1,123 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN"
"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
<!-- Generated by graphviz version 16.0.0 (0)
-->
<!-- Title: tessera Pages: 1 -->
<svg width="241pt" height="296pt"
viewBox="0.00 0.00 241.00 296.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
<g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 292)">
<title>tessera</title>
<polygon fill="white" stroke="none" points="-4,4 -4,-292 236.5,-292 236.5,4 -4,4"/>
<!-- n0 -->
<g id="node1" class="node">
<title>n0</title>
<path fill="#f7f7f5" stroke="#444444" d="M135.12,-288C135.12,-288 104.12,-288 104.12,-288 98.12,-288 92.12,-282 92.12,-276 92.12,-276 92.12,-264 92.12,-264 92.12,-258 98.12,-252 104.12,-252 104.12,-252 135.12,-252 135.12,-252 141.12,-252 147.12,-258 147.12,-264 147.12,-264 147.12,-276 147.12,-276 147.12,-282 141.12,-288 135.12,-288"/>
<text xml:space="preserve" text-anchor="middle" x="119.62" y="-266.3" font-family="Helvetica,sans-Serif" font-size="11.00" fill="#1c1c1a">switch 0</text>
</g>
<!-- n1 -->
<g id="node2" class="node">
<title>n1</title>
<path fill="#f7f7f5" stroke="#444444" d="M53.12,-204C53.12,-204 22.12,-204 22.12,-204 16.12,-204 10.12,-198 10.12,-192 10.12,-192 10.12,-180 10.12,-180 10.12,-174 16.12,-168 22.12,-168 22.12,-168 53.12,-168 53.12,-168 59.12,-168 65.12,-174 65.12,-180 65.12,-180 65.12,-192 65.12,-192 65.12,-198 59.12,-204 53.12,-204"/>
<text xml:space="preserve" text-anchor="middle" x="37.62" y="-182.3" font-family="Helvetica,sans-Serif" font-size="11.00" fill="#1c1c1a">switch 1</text>
</g>
<!-- n0&#45;&gt;n1 -->
<g id="edge1" class="edge">
<title>n0&#45;&gt;n1</title>
<path fill="none" stroke="#666666" d="M102.23,-251.61C90.82,-240.19 75.7,-225.08 62.96,-212.33"/>
<polygon fill="#666666" stroke="#666666" points="65.61,-210.03 56.06,-205.44 60.66,-214.98 65.61,-210.03"/>
<text xml:space="preserve" text-anchor="middle" x="91.41" y="-224.5" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#333333">Idle</text>
</g>
<!-- n4 -->
<g id="node5" class="node">
<title>n4</title>
<path fill="#f7f7f5" stroke="#444444" d="M135.12,-204C135.12,-204 104.12,-204 104.12,-204 98.12,-204 92.12,-198 92.12,-192 92.12,-192 92.12,-180 92.12,-180 92.12,-174 98.12,-168 104.12,-168 104.12,-168 135.12,-168 135.12,-168 141.12,-168 147.12,-174 147.12,-180 147.12,-180 147.12,-192 147.12,-192 147.12,-198 141.12,-204 135.12,-204"/>
<text xml:space="preserve" text-anchor="middle" x="119.62" y="-182.3" font-family="Helvetica,sans-Serif" font-size="11.00" fill="#1c1c1a">switch 1</text>
</g>
<!-- n0&#45;&gt;n4 -->
<g id="edge2" class="edge">
<title>n0&#45;&gt;n4</title>
<path fill="none" stroke="#666666" d="M119.62,-251.61C119.62,-241.17 119.62,-227.64 119.62,-215.66"/>
<polygon fill="#666666" stroke="#666666" points="123.13,-215.88 119.63,-205.88 116.13,-215.88 123.13,-215.88"/>
<text xml:space="preserve" text-anchor="middle" x="135.75" y="-224.5" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#333333">Waiting</text>
</g>
<!-- n7 -->
<g id="node8" class="node">
<title>n7</title>
<path fill="#f7f7f5" stroke="#444444" d="M218.12,-204C218.12,-204 187.12,-204 187.12,-204 181.12,-204 175.12,-198 175.12,-192 175.12,-192 175.12,-180 175.12,-180 175.12,-174 181.12,-168 187.12,-168 187.12,-168 218.12,-168 218.12,-168 224.12,-168 230.12,-174 230.12,-180 230.12,-180 230.12,-192 230.12,-192 230.12,-198 224.12,-204 218.12,-204"/>
<text xml:space="preserve" text-anchor="middle" x="202.62" y="-182.3" font-family="Helvetica,sans-Serif" font-size="11.00" fill="#1c1c1a">switch 1</text>
</g>
<!-- n0&#45;&gt;n7 -->
<g id="edge3" class="edge">
<title>n0&#45;&gt;n7</title>
<path fill="none" stroke="#666666" d="M138.79,-251.78C144.88,-246.19 151.61,-239.9 157.62,-234 164.7,-227.06 172.2,-219.36 179.02,-212.24"/>
<polygon fill="#666666" stroke="#666666" points="181.24,-214.98 185.59,-205.32 176.17,-210.16 181.24,-214.98"/>
<text xml:space="preserve" text-anchor="middle" x="192.6" y="-224.5" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#333333">Connected</text>
</g>
<!-- n2 -->
<g id="node3" class="node">
<title>n2</title>
<path fill="#ffffff" stroke="#444444" d="M51.25,-120C51.25,-120 12,-120 12,-120 6,-120 0,-114 0,-108 0,-108 0,-96 0,-96 0,-90 6,-84 12,-84 12,-84 51.25,-84 51.25,-84 57.25,-84 63.25,-90 63.25,-96 63.25,-96 63.25,-108 63.25,-108 63.25,-114 57.25,-120 51.25,-120"/>
<text xml:space="preserve" text-anchor="middle" x="31.62" y="-98.3" font-family="Helvetica,sans-Serif" font-size="11.00" fill="#1c1c1a">bind 1.0 n</text>
</g>
<!-- n1&#45;&gt;n2 -->
<g id="edge4" class="edge">
<title>n1&#45;&gt;n2</title>
<path fill="none" stroke="#666666" d="M36.35,-167.61C35.59,-157.17 34.6,-143.64 33.72,-131.66"/>
<polygon fill="#666666" stroke="#666666" points="37.23,-131.59 33.01,-121.87 30.25,-132.1 37.23,-131.59"/>
<text xml:space="preserve" text-anchor="middle" x="46.23" y="-140.5" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#333333">Hello</text>
</g>
<!-- n3 -->
<g id="node4" class="node">
<title>n3</title>
<path fill="#e7efe4" stroke="#444444" d="M47.5,-36C47.5,-36 15.75,-36 15.75,-36 9.75,-36 3.75,-30 3.75,-24 3.75,-24 3.75,-12 3.75,-12 3.75,-6 9.75,0 15.75,0 15.75,0 47.5,0 47.5,0 53.5,0 59.5,-6 59.5,-12 59.5,-12 59.5,-24 59.5,-24 59.5,-30 53.5,-36 47.5,-36"/>
<text xml:space="preserve" text-anchor="middle" x="31.62" y="-14.3" font-family="Helvetica,sans-Serif" font-size="11.00" fill="#1c1c1a">clause 0</text>
</g>
<!-- n2&#45;&gt;n3 -->
<g id="edge5" class="edge">
<title>n2&#45;&gt;n3</title>
<path fill="none" stroke="#666666" d="M31.62,-83.61C31.62,-73.17 31.62,-59.64 31.62,-47.66"/>
<polygon fill="#666666" stroke="#666666" points="35.13,-47.88 31.63,-37.88 28.13,-47.88 35.13,-47.88"/>
<text xml:space="preserve" text-anchor="middle" x="40.62" y="-56.5" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#333333">bind</text>
</g>
<!-- n5 -->
<g id="node6" class="node">
<title>n5</title>
<path fill="#ffffff" stroke="#444444" d="M139.25,-120C139.25,-120 100,-120 100,-120 94,-120 88,-114 88,-108 88,-108 88,-96 88,-96 88,-90 94,-84 100,-84 100,-84 139.25,-84 139.25,-84 145.25,-84 151.25,-90 151.25,-96 151.25,-96 151.25,-108 151.25,-108 151.25,-114 145.25,-120 139.25,-120"/>
<text xml:space="preserve" text-anchor="middle" x="119.62" y="-98.3" font-family="Helvetica,sans-Serif" font-size="11.00" fill="#1c1c1a">bind 1.0 n</text>
</g>
<!-- n4&#45;&gt;n5 -->
<g id="edge6" class="edge">
<title>n4&#45;&gt;n5</title>
<path fill="none" stroke="#666666" d="M119.62,-167.61C119.62,-157.17 119.62,-143.64 119.62,-131.66"/>
<polygon fill="#666666" stroke="#666666" points="123.13,-131.88 119.63,-121.88 116.13,-131.88 123.13,-131.88"/>
<text xml:space="preserve" text-anchor="middle" x="130.12" y="-140.5" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#333333">Data</text>
</g>
<!-- n6 -->
<g id="node7" class="node">
<title>n6</title>
<path fill="#e7efe4" stroke="#444444" d="M135.5,-36C135.5,-36 103.75,-36 103.75,-36 97.75,-36 91.75,-30 91.75,-24 91.75,-24 91.75,-12 91.75,-12 91.75,-6 97.75,0 103.75,0 103.75,0 135.5,0 135.5,0 141.5,0 147.5,-6 147.5,-12 147.5,-12 147.5,-24 147.5,-24 147.5,-30 141.5,-36 135.5,-36"/>
<text xml:space="preserve" text-anchor="middle" x="119.62" y="-14.3" font-family="Helvetica,sans-Serif" font-size="11.00" fill="#1c1c1a">clause 1</text>
</g>
<!-- n5&#45;&gt;n6 -->
<g id="edge7" class="edge">
<title>n5&#45;&gt;n6</title>
<path fill="none" stroke="#666666" d="M119.62,-83.61C119.62,-73.17 119.62,-59.64 119.62,-47.66"/>
<polygon fill="#666666" stroke="#666666" points="123.13,-47.88 119.63,-37.88 116.13,-47.88 123.13,-47.88"/>
<text xml:space="preserve" text-anchor="middle" x="128.62" y="-56.5" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#333333">bind</text>
</g>
<!-- n8 -->
<g id="node9" class="node">
<title>n8</title>
<path fill="#e7efe4" stroke="#444444" d="M220.5,-120C220.5,-120 188.75,-120 188.75,-120 182.75,-120 176.75,-114 176.75,-108 176.75,-108 176.75,-96 176.75,-96 176.75,-90 182.75,-84 188.75,-84 188.75,-84 220.5,-84 220.5,-84 226.5,-84 232.5,-90 232.5,-96 232.5,-96 232.5,-108 232.5,-108 232.5,-114 226.5,-120 220.5,-120"/>
<text xml:space="preserve" text-anchor="middle" x="204.62" y="-98.3" font-family="Helvetica,sans-Serif" font-size="11.00" fill="#1c1c1a">clause 2</text>
</g>
<!-- n7&#45;&gt;n8 -->
<g id="edge8" class="edge">
<title>n7&#45;&gt;n8</title>
<path fill="none" stroke="#666666" d="M203.05,-167.61C203.3,-157.17 203.63,-143.64 203.93,-131.66"/>
<polygon fill="#666666" stroke="#666666" points="207.42,-131.96 204.16,-121.88 200.42,-131.79 207.42,-131.96"/>
<text xml:space="preserve" text-anchor="middle" x="216.49" y="-140.5" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#333333">Close</text>
</g>
</g>
</svg>
Side by Side

After

Width:  |  Height:  |  Size: 8.7 KiB

artifacts/protocol-tree.dot
+22
View File
@@ -0,0 +1,22 @@
digraph tessera {
graph [bgcolor="white", rankdir=TB, nodesep=0.35, ranksep=0.5];
node [shape=box, style="rounded,filled", color="#444444", fontcolor="#1c1c1a", fillcolor="#ffffff", fontname="Helvetica", fontsize=11];
edge [color="#666666", fontcolor="#333333", fontname="Helvetica", fontsize=10];
n0 [label="switch 0", fillcolor="#f7f7f5"];
n1 [label="switch 1", fillcolor="#f7f7f5"];
n2 [label="bind 1.0 n"];
n3 [label="clause 0", fillcolor="#e7efe4"];
n4 [label="switch 1", fillcolor="#f7f7f5"];
n5 [label="bind 1.0 n"];
n6 [label="clause 1", fillcolor="#e7efe4"];
n7 [label="switch 1", fillcolor="#f7f7f5"];
n8 [label="clause 2", fillcolor="#e7efe4"];
n0 -> n1 [label="Idle"];
n0 -> n4 [label="Waiting"];
n0 -> n7 [label="Connected"];
n1 -> n2 [label="Hello"];
n2 -> n3 [label="bind"];
n4 -> n5 [label="Data"];
n5 -> n6 [label="bind"];
n7 -> n8 [label="Close"];
}
artifacts/tessera-demo.gif
BIN
View File
Binary file not shown.
Side by Side

After

Width:  |  Height:  |  Size: 875 KiB

benchmarks/Bench.hs
+46
View File
@@ -0,0 +1,46 @@
module Main where
import Data.List (intercalate)
import qualified Data.Map.Strict as Map
import Data.Time.Clock (diffUTCTime, getCurrentTime)
import Tessera.Check (checkProgram)
import Tessera.Env
import Tessera.Eval
import Tessera.Matrix (witness, Outcome (..))
import Tessera.Parser (parseProgram)
import Tessera.Syntax
import Tessera.Tree
main :: IO ()
main = do
putStrLn "strategy,nodes,depth,witness_ms"
mapM_ runSize [4, 6, 8, 10]
runSize :: Int -> IO ()
runSize size = do
let source = declaration size
program = either (error . show) id (parseProgram source)
env = either (error . show) id (checkProgram program)
match' = head [m | m@(MatchDeclaration _ _ _ _) <- program]
clauses = matchClauses match'
rows = zip (map clausePatterns clauses) [0 .. length clauses - 1]
types = map snd (matchArgumentsOf match')
leftmost = compileMatch env Leftmost types rows (initialOccurrences (length types))
heuristic = compileMatch env Heuristic types rows (initialOccurrences (length types))
start <- getCurrentTime
let outcome = witness env 2000 types (map clausePatterns clauses)
end <- getCurrentTime
putStrLn (intercalate "," [ "leftmost", show (treeSize leftmost), show (treeDepth leftmost), show (diffUTCTime end start)])
putStrLn (intercalate "," [ "heuristic", show (treeSize heuristic), show (treeDepth heuristic), show (diffUTCTime end start)])
putStrLn (intercalate "," [ "outcome", show (outcome == Covered), "", ""])
matchArgumentsOf :: Declaration -> [(String, Type)]
matchArgumentsOf (MatchDeclaration _ arguments _ _) = arguments
matchArgumentsOf _ = []
declaration :: Int -> String
declaration size =
let constructors = intercalate " | " ["C" ++ show i ++ " Int" | i <- [1 .. size]]
patterns = concat [" | C" ++ show i ++ " n -> n\n" | i <- [1 .. size]]
in "data T = " ++ constructors ++ "\n\nmatch classify (t : T) : Int =\n" ++ patterns
examples/instructions-incomplete.tess
+9
View File
@@ -0,0 +1,9 @@
data Exp = Const Int | Reg Int | Plus Exp Exp | Times Exp Exp
data Instr = LoadImm Int | LoadReg Int | AddInstr | MulInstr
match select (e : Exp) : Instr =
| Plus (Reg a) (Reg b) -> AddInstr
| Times (Reg a) (Reg b) -> MulInstr
| Const n -> LoadImm n
| Reg n -> LoadReg n
examples/instructions.tess
+10
View File
@@ -0,0 +1,10 @@
data Exp = Const Int | Reg Int | Plus Exp Exp | Times Exp Exp
data Instr = LoadImm Int | LoadReg Int | AddInstr | MulInstr
match select (e : Exp) : Instr =
| Plus (Reg a) (Reg b) -> AddInstr
| Times (Reg a) (Reg b) -> MulInstr
| Const n -> LoadImm n
| Reg n -> LoadReg n
| _ -> LoadImm 0
examples/protocol-complete.tess
+14
View File
@@ -0,0 +1,14 @@
data State = Idle | Waiting | Connected
data Message = Hello Int | Data Int | Close
match classify (s : State) (m : Message) : Int =
| Idle (Hello n) -> n
| Idle (Data n) -> n
| Idle Close -> 0
| Waiting (Hello n) -> n
| Waiting (Data n) -> n
| Waiting Close -> 0
| Connected (Hello n) -> n
| Connected (Data n) -> n
| Connected Close -> 0
examples/protocol-redundant.tess
+15
View File
@@ -0,0 +1,15 @@
data State = Idle | Waiting | Connected
data Message = Hello Int | Data Int | Close
match classify (s : State) (m : Message) : Int =
| Idle (Hello n) -> n
| Idle (Data n) -> n
| Idle Close -> 0
| Waiting (Hello n) -> n
| Waiting (Data n) -> n
| Waiting Close -> 0
| Connected (Hello n) -> n
| Connected (Data n) -> n
| Connected Close -> 0
| _ Close -> 0
examples/protocol-values.txt
+4
View File
@@ -0,0 +1,4 @@
Idle; Hello 5
Waiting; Data 3
Connected; Close
Idle; Data 7
examples/protocol.tess
+8
View File
@@ -0,0 +1,8 @@
data State = Idle | Waiting | Connected
data Message = Hello Int | Data Int | Close
match classify (s : State) (m : Message) : Int =
| Idle (Hello n) -> n
| Waiting (Data n) -> n
| Connected Close -> 0
examples/simplify-redundant.tess
+12
View File
@@ -0,0 +1,12 @@
data Expr = Lit Int | Add Expr Expr | Mul Expr Expr | Neg Expr
match simplify (e : Expr) : Expr =
| Add (Lit 0) x -> x
| Add x (Lit 0) -> x
| Mul (Lit 0) x -> Lit 0
| Mul x (Lit 0) -> Lit 0
| Mul (Lit 0) (Lit 1) -> Lit 0
| Mul (Lit 1) x -> x
| Mul x (Lit 1) -> x
| Neg (Neg x) -> x
| e -> e
examples/simplify.tess
+11
View File
@@ -0,0 +1,11 @@
data Expr = Lit Int | Add Expr Expr | Mul Expr Expr | Neg Expr
match simplify (e : Expr) : Expr =
| Add (Lit 0) x -> x
| Add x (Lit 0) -> x
| Mul (Lit 0) x -> Lit 0
| Mul x (Lit 0) -> Lit 0
| Mul (Lit 1) x -> x
| Mul x (Lit 1) -> x
| Neg (Neg x) -> x
| e -> e
scripts/setup
Regular → Executable
View File
File mode changed.
src/Tessera/Graph.hs
+81
View File
@@ -0,0 +1,81 @@
module Tessera.Graph where
import Tessera.Matrix (Key (..))
import Tessera.Tree
data Rendered = Rendered
{ renderedNext :: Int
, renderedRoot :: Int
, renderedNodes :: [(Int, String, String)]
, renderedEdges :: [(Int, Int, String)]
}
buildGraph :: Tree -> Rendered
buildGraph tree =
let (next, root, nodes, edges) = go tree 0
in Rendered next root nodes edges
where
go node next = case node of
Success index ->
(next + 1, next, [(next, "clause " ++ show index, "success")], [])
Failure ->
(next + 1, next, [(next, "fail", "failure")], [])
Bind occurrence name inner ->
let (next', root', nodes', edges') = go inner (next + 1)
in (next', next, (next, "bind " ++ renderPath (occurrencePath occurrence) ++ " " ++ name, "bind") : nodes', (next, root', "bind") : edges')
Switch occurrence branches fallback ->
let (afterBranches, branchRoots, branchNodes, branchEdges) = goBranches branches (next + 1) [] [] []
(afterFallback, fallbackRoots, fallbackNodes, fallbackEdges) = case fallback of
Nothing -> (afterBranches, [], [], [])
Just defaultTree ->
let (finalNext, root', nodes', edges') = go defaultTree afterBranches
in (finalNext, [(root', "default")], nodes', edges')
node = (next, "switch " ++ renderPath (occurrencePath occurrence), "switch")
edges = [(next, r, l) | (r, l) <- branchRoots] ++ [(next, r, l) | (r, l) <- fallbackRoots]
in (afterFallback, next, node : branchNodes ++ fallbackNodes, edges ++ branchEdges ++ fallbackEdges)
goBranches [] next roots nodes edges = (next, reverse roots, nodes, edges)
goBranches ((key, subtree) : rest) next roots nodes edges =
let (next', root', nodes', edges') = go subtree next
in goBranches rest next' ((root', renderKey key) : roots) (nodes ++ nodes') (edges ++ edges')
renderPath :: [Int] -> String
renderPath [] = "root"
renderPath [x] = show x
renderPath (x : rest) = show x ++ "." ++ renderPath rest
renderKey :: Key -> String
renderKey key = case key of
KeyCon name -> name
KeyInt n -> show n
KeyBool b -> if b then "True" else "False"
KeyTuple n -> "tuple/" ++ show n
renderDot :: Tree -> String
renderDot tree = unlines (header ++ map renderNode (renderedNodes graph) ++ map renderEdge (renderedEdges graph) ++ ["}"])
where
graph = buildGraph tree
header =
[ "digraph tessera {"
, " graph [bgcolor=\"white\", rankdir=TB, nodesep=0.35, ranksep=0.5];"
, " node [shape=box, style=\"rounded,filled\", color=\"#444444\", fontcolor=\"#1c1c1a\", fillcolor=\"#ffffff\", fontname=\"Helvetica\", fontsize=11];"
, " edge [color=\"#666666\", fontcolor=\"#333333\", fontname=\"Helvetica\", fontsize=10];"
]
renderNode (identifier, label, kind) =
" n" ++ show identifier ++ " [label=\"" ++ escape label ++ "\"" ++ fillFor kind ++ "];"
renderEdge (from, to, label) =
" n" ++ show from ++ " -> n" ++ show to ++ " [label=\"" ++ escape label ++ "\"];"
fillFor kind = case kind of
"success" -> ", fillcolor=\"#e7efe4\""
"failure" -> ", fillcolor=\"#f4e6e4\""
"switch" -> ", fillcolor=\"#f7f7f5\""
_ -> ""
escape :: String -> String
escape = concatMap escapeChar
where
escapeChar c = case c of
'"' -> "\\\""
'\\' -> "\\\\"
'\n' -> "\\n"
_ -> [c]
src/Tessera/Serialize.hs
+190
View File
@@ -0,0 +1,190 @@
module Tessera.Serialize where
import Data.Char (isAlphaNum, isDigit)
import Data.List (isPrefixOf)
import Tessera.Check (checkProgram)
import Tessera.Env (Env, lookupConstructor)
import Tessera.Matrix (Key (..))
import Tessera.Parser (parseProgram)
import Tessera.Syntax
import Tessera.Tree
data Artifact = Artifact
{ artifactFunction :: String
, artifactStrategy :: Strategy
, artifactTree :: Tree
, artifactSource :: String
, artifactProgram :: Program
, artifactEnv :: Env
}
formatVersion :: String
formatVersion = "1"
encodeArtifact :: String -> String -> Strategy -> Tree -> String
encodeArtifact function source strategy tree = unlines
[ "tessera-tree " ++ formatVersion
, "function " ++ function
, "strategy " ++ strategyName strategy
, "tree " ++ encodeTree tree
, "source-begin"
, source
, "source-end"
]
encodeTree :: Tree -> String
encodeTree tree = case tree of
Success index -> "L" ++ show index
Failure -> "X"
Bind (Occurrence path) name inner -> "B[" ++ joinIntegers path ++ "|" ++ name ++ "]" ++ encodeTree inner
Switch (Occurrence path) branches fallback ->
"W[" ++ joinIntegers path ++ "]{"
++ concatMap encodeBranch branches
++ "}[" ++ maybe "" encodeTree fallback ++ "]"
encodeBranch :: (Key, Tree) -> String
encodeBranch (key, tree) = encodeKey key ++ ":" ++ encodeTree tree ++ ";"
encodeKey :: Key -> String
encodeKey key = case key of
KeyCon name -> "c" ++ name
KeyInt n -> "i" ++ show n
KeyBool b -> if b then "bT" else "bF"
KeyTuple n -> "t" ++ show n
joinIntegers :: [Int] -> String
joinIntegers [] = ""
joinIntegers [x] = show x
joinIntegers (x : rest) = show x ++ "," ++ joinIntegers rest
decodeArtifact :: String -> Either String Artifact
decodeArtifact input = do
let numbered = zip [1 ..] (lines input)
version <- lookupHeader "tessera-tree" numbered
if version /= formatVersion then Left ("unsupported tree format version " ++ version) else Right ()
function <- lookupHeader "function" numbered
strategyText <- lookupHeader "strategy" numbered
strategy <- case strategyText of
"leftmost" -> Right Leftmost
"heuristic" -> Right Heuristic
_ -> Left ("unknown strategy " ++ strategyText)
treeText <- lookupHeader "tree" numbered
tree <- decodeTree treeText
source <- extractSource numbered
program <- either (Left . renderDiagnostic) Right (parseProgram source)
env <- either (Left . renderDiagnostic) Right (checkProgram program)
if function `elem` [name | MatchDeclaration name _ _ _ <- program]
then Right ()
else Left ("function " ++ function ++ " is not declared in the embedded source")
validateTree env tree
return (Artifact function strategy tree source program env)
lookupHeader :: String -> [(Int, String)] -> Either String String
lookupHeader key numbered =
case [drop (length key + 1) line | (_, line) <- numbered, (key ++ " ") `isPrefixOf` line] of
(value : _) -> Right value
[] -> Left ("missing " ++ key ++ " header")
extractSource :: [(Int, String)] -> Either String String
extractSource numbered = case break (\(_, line) -> line == "source-begin") numbered of
(_, _ : rest) -> case break (\(_, line) -> line == "source-end") rest of
(body, _ : _) -> Right (unlines (map snd body))
_ -> Left "missing source-end marker"
_ -> Left "missing source-begin marker"
renderDiagnostic :: Diagnostic -> String
renderDiagnostic (Diagnostic span' message) =
"line " ++ show (spanLine span') ++ " column " ++ show (spanColumn span') ++ ": " ++ message
decodeTree :: String -> Either String Tree
decodeTree input = do
(tree, rest) <- parseTree input
if null rest then Right tree else Left ("trailing characters in tree encoding " ++ take 20 rest)
parseTree :: String -> Either String (Tree, String)
parseTree ('L' : rest) =
let (digits, remaining) = span isDigit rest
in if null digits then Left "malformed success node" else Right (Success (read digits), remaining)
parseTree ('X' : rest) = Right (Failure, rest)
parseTree ('B' : '[' : rest) = do
let (inside, afterInside) = break (== ']') rest
(path, name) <- case break (== '|') inside of
(p, '|' : n) -> Right (p, n)
_ -> Left "malformed bind node"
(inner, remaining) <- parseTree (drop 1 afterInside)
Right (Bind (Occurrence (parseIntegers path)) name inner, remaining)
parseTree ('W' : '[' : rest) = do
let (path, afterPath) = break (== ']') rest
afterPath' <- expect ']' afterPath
afterBrace <- expect '{' afterPath'
(branches, afterBranches) <- parseBranches afterBrace
afterBranches' <- expect '}' afterBranches
afterBracket <- expect '[' afterBranches'
let (fallbackText, afterFallback) = break (== ']') afterBracket
fallback <- if null fallbackText then Right Nothing else do
(tree, _) <- parseTree fallbackText
Right (Just tree)
afterFallback' <- expect ']' afterFallback
Right (Switch (Occurrence (parseIntegers path)) branches fallback, afterFallback')
parseTree _ = Left "malformed tree encoding"
expect :: Char -> String -> Either String String
expect c (x : rest) | x == c = Right rest
expect c _ = Left ("expected " ++ [c])
parseBranches :: String -> Either String ([(Key, Tree)], String)
parseBranches input = go input []
where
go ('}' : rest) acc = Right (reverse acc, '}' : rest)
go (c : rest) acc = do
(key, rest1) <- parseKey c rest
rest2 <- expect ':' rest1
(tree, rest3) <- parseTree rest2
rest4 <- expect ';' rest3
go rest4 ((key, tree) : acc)
go [] _ = Left "unterminated branch list"
parseKey :: Char -> String -> Either String (Key, String)
parseKey 'c' rest = let (name, remaining) = span (\c -> isAlphaNum c || c == '_') rest in Right (KeyCon name, remaining)
parseKey 'i' rest = let (digits, remaining) = span isDigit rest in Right (KeyInt (read digits), remaining)
parseKey 'b' rest = case rest of
('T' : remaining) -> Right (KeyBool True, remaining)
('F' : remaining) -> Right (KeyBool False, remaining)
_ -> Left "malformed boolean key"
parseKey 't' rest = let (digits, remaining) = span isDigit rest in Right (KeyTuple (read digits), remaining)
parseKey _ _ = Left "malformed branch key"
parseIntegers :: String -> [Int]
parseIntegers [] = []
parseIntegers text = map read (splitOn ',' text)
splitOn :: Char -> String -> [String]
splitOn _ [] = []
splitOn c text = case break (== c) text of
(piece, []) -> [piece]
(piece, _ : rest) -> piece : splitOn c rest
validateTree :: Env -> Tree -> Either String ()
validateTree env = go
where
go tree = case tree of
Success _ -> Right ()
Failure -> Right ()
Bind (Occurrence path) _ inner -> validatePath path >> go inner
Switch (Occurrence path) branches fallback -> do
validatePath path
mapM_ (validateKey env) (map fst branches)
mapM_ (go . snd) branches
mapM_ go fallback
validatePath path = if all (>= 0) path then Right () else Left "negative occurrence path"
validateKey :: Env -> Key -> Either String ()
validateKey env key = case key of
KeyCon name -> case lookupConstructor env name of
Just _ -> Right ()
Nothing -> Left ("unknown constructor in tree " ++ name)
KeyInt _ -> Right ()
KeyBool _ -> Right ()
KeyTuple _ -> Right ()
tessera.cabal
+63
View File
@@ -0,0 +1,63 @@
cabal-version: 2.4
name: tessera
version: 0.1.0.0
synopsis: pattern-match compiler with exhaustiveness checking and counterexample generation
description:
A pattern-match compiler for algebraic data types with usefulness analysis,
missing-case witness generation, decision-tree compilation and execution.
license: BSD-3-Clause
author: james
maintainer: james
category: Compilers
build-type: Simple
library
hs-source-dirs: src
exposed-modules:
Tessera.Syntax
Tessera.Parser
Tessera.Env
Tessera.Check
Tessera.Matrix
Tessera.Analyze
Tessera.Tree
Tessera.Eval
Tessera.Serialize
Tessera.Graph
build-depends:
base >=4.12 && <4.13
, containers >=0.6 && <0.7
, time >=1.8 && <1.10
default-language: Haskell2010
executable tessera
hs-source-dirs: app
main-is: Main.hs
build-depends:
base
, containers
, time
, directory
, tessera
default-language: Haskell2010
test-suite spec
type: exitcode-stdio-1.0
hs-source-dirs: tests
main-is: Spec.hs
build-depends:
base
, containers
, tessera
default-language: Haskell2010
benchmark matrix-bench
type: exitcode-stdio-1.0
hs-source-dirs: benchmarks
main-is: Bench.hs
build-depends:
base
, containers
, time
, tessera
default-language: Haskell2010
tests/Spec.hs
+249
View File
@@ -0,0 +1,249 @@
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"