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

differentially validate coverage witnesses and compiled dispatch

Browse Source
This commit is contained in:
milner committed 2020-03-25 12:00:00 +00:00
1 parent 819e78225c
commit 9317226bb3
11 files changed
+737
Download Patch File Download Diff File Expand all files Collapse all files

No files matched your search

.gitignore
+1
View File
@@ -1,4 +1,5 @@
dist/
dist-newstyle/
.toolchain/
*.o
*.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>
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
scripts/setup
Regular → Executable
View File
File mode changed.
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"