diff --git a/.gitignore b/.gitignore
index 87fe535..2837e2c 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,4 +1,5 @@
dist/
+dist-newstyle/
.toolchain/
*.o
*.hi
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..f650649
--- /dev/null
+++ b/README.md
@@ -0,0 +1 @@
+
diff --git a/artifacts/protocol-complete-tree.dot b/artifacts/protocol-complete-tree.dot
new file mode 100644
index 0000000..9466c3d
--- /dev/null
+++ b/artifacts/protocol-complete-tree.dot
@@ -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"];
+}
diff --git a/artifacts/protocol-complete-tree.png b/artifacts/protocol-complete-tree.png
new file mode 100644
index 0000000..9f04b5c
Binary files /dev/null and b/artifacts/protocol-complete-tree.png differ
diff --git a/artifacts/protocol-complete-tree.svg b/artifacts/protocol-complete-tree.svg
new file mode 100644
index 0000000..5e8d335
--- /dev/null
+++ b/artifacts/protocol-complete-tree.svg
@@ -0,0 +1,253 @@
+
+
+
+
+
diff --git a/artifacts/protocol-decision-tree.svg b/artifacts/protocol-decision-tree.svg
new file mode 100644
index 0000000..3cb5875
--- /dev/null
+++ b/artifacts/protocol-decision-tree.svg
@@ -0,0 +1,123 @@
+
+
+
+
+
diff --git a/artifacts/protocol-tree.dot b/artifacts/protocol-tree.dot
new file mode 100644
index 0000000..279aee8
--- /dev/null
+++ b/artifacts/protocol-tree.dot
@@ -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"];
+}
diff --git a/artifacts/tessera-demo.gif b/artifacts/tessera-demo.gif
new file mode 100644
index 0000000..e3f2c24
Binary files /dev/null and b/artifacts/tessera-demo.gif differ
diff --git a/benchmarks/Bench.hs b/benchmarks/Bench.hs
new file mode 100644
index 0000000..8b66030
--- /dev/null
+++ b/benchmarks/Bench.hs
@@ -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
diff --git a/scripts/setup b/scripts/setup
old mode 100644
new mode 100755
diff --git a/tests/Spec.hs b/tests/Spec.hs
new file mode 100644
index 0000000..49b9520
--- /dev/null
+++ b/tests/Spec.hs
@@ -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"