diff options
| author | Dibyendu Majumdar <dibyendumajumdar@users.noreply.github.com> | 2024-05-02 22:08:06 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2024-05-02 14:08:06 -0700 |
| commit | 0caf37adc5f8c1600f13d80aaf77361f407c9694 (patch) | |
| tree | 30498744a348cbefb727d680b13793fdd10463ca /chapter04/docs | |
| parent | e31c37890a86aedfb209cf543baf05b1b60a27d2 (diff) | |
| download | Simple-0caf37adc5f8c1600f13d80aaf77361f407c9694.tar.gz Simple-0caf37adc5f8c1600f13d80aaf77361f407c9694.zip | |
Documentation updates (#76)
* More clearly explain why we do not have an AST in the implementation
* Improve the description of type lattice.
Cross reference to future chapters.
* Minor update
* Add lattice visual
Revise the text describing meet.
* minor update
* Add a lattice visual to the text
* Update the lattice visual.
Add description of the new edges in the SoN graph
Diffstat (limited to 'chapter04/docs')
| -rw-r--r-- | chapter04/docs/build-graphs.sh | 2 | ||||
| -rw-r--r-- | chapter04/docs/lattice.gv | 63 | ||||
| -rw-r--r-- | chapter04/docs/lattice.svg | 195 |
3 files changed, 260 insertions, 0 deletions
diff --git a/chapter04/docs/build-graphs.sh b/chapter04/docs/build-graphs.sh new file mode 100644 index 00000000..d8038602 --- /dev/null +++ b/chapter04/docs/build-graphs.sh @@ -0,0 +1,2 @@ +dot -Tsvg lattice.gv > lattice.svg + diff --git a/chapter04/docs/lattice.gv b/chapter04/docs/lattice.gv new file mode 100644 index 00000000..2644448e --- /dev/null +++ b/chapter04/docs/lattice.gv @@ -0,0 +1,63 @@ +digraph Lattice { + // Define nodes + splines=false; + node [shape=circle, style=filled, fillcolor=lightblue]; + nodesep=0.6; + + TOP [label="⊤"]; + BOT [label="⊥"]; + + CTRL [label="Ctrl"]; + + INT_TOP [label="IntTop"]; + INT_BOT [label="IntBot"]; + + INT_MIN [label="-n"]; + INT_MINDOTS [label="..." shape=none style=none]; + INT_MINUS [label="-1"]; + INT_ZERO [label="0"]; + INT_PLUS [label="1"]; + INT_MAXDOTS [label="..." shape=none style=none]; + INT_MAX [label="+n"]; + + TUPLE [label="TUPLE"]; + + // Define edges + edge [arrowhead=none]; + + TOP -> INT_TOP; + INT_TOP -> INT_MIN; + INT_TOP -> INT_MINDOTS; + INT_TOP -> INT_MINUS; + INT_TOP -> INT_ZERO; + INT_TOP -> INT_PLUS; + INT_TOP -> INT_MAXDOTS; + INT_TOP -> INT_MAX; + INT_MIN -> INT_BOT; + INT_MINDOTS -> INT_BOT; + INT_MINUS -> INT_BOT; + INT_ZERO -> INT_BOT; + INT_PLUS -> INT_BOT; + INT_MAXDOTS -> INT_BOT; + INT_MAX -> INT_BOT; + INT_BOT -> BOT; + + INT_MIN -> INT_MINDOTS -> INT_MINUS -> INT_ZERO -> INT_PLUS -> INT_MAXDOTS -> INT_MAX [style=invis]; + + TOP -> TUPLE; + TUPLE -> BOT; + + TOP -> CTRL; + CTRL -> BOT; + + + // Additional customization + {rank=same; TOP} + {rank=same; INT_TOP} + {rank=same; CTRL; INT_MIN; INT_MINDOTS; + INT_MINUS; INT_ZERO; + INT_PLUS; INT_MAXDOTS; + INT_MAX; TUPLE} + {rank=same; INT_BOT} + {rank=same; BOT;} +}
\ No newline at end of file diff --git a/chapter04/docs/lattice.svg b/chapter04/docs/lattice.svg new file mode 100644 index 00000000..0d403c20 --- /dev/null +++ b/chapter04/docs/lattice.svg @@ -0,0 +1,195 @@ +<?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 2.43.0 (0) + --> +<!-- Title: Lattice Pages: 1 --> +<svg width="802pt" height="478pt" + viewBox="0.00 0.00 802.14 478.27" 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 474.27)"> +<title>Lattice</title> +<polygon fill="white" stroke="transparent" points="-4,4 -4,-474.27 798.14,-474.27 798.14,4 -4,4"/> +<!-- TOP --> +<g id="node1" class="node"> +<title>TOP</title> +<ellipse fill="lightblue" stroke="black" cx="377.6" cy="-450.77" rx="19.5" ry="19.5"/> +<text text-anchor="middle" x="377.6" y="-447.07" font-family="Times,serif" font-size="14.00">⊤</text> +</g> +<!-- CTRL --> +<g id="node3" class="node"> +<title>CTRL</title> +<ellipse fill="lightblue" stroke="black" cx="28.6" cy="-235.14" rx="28.7" ry="28.7"/> +<text text-anchor="middle" x="28.6" y="-231.44" font-family="Times,serif" font-size="14.00">Ctrl</text> +</g> +<!-- TOP->CTRL --> +<g id="edge25" class="edge"> +<title>TOP->CTRL</title> +<path fill="none" stroke="black" d="M360.76,-440.37C304.12,-405.37 120.24,-291.76 53.28,-250.38"/> +</g> +<!-- INT_TOP --> +<g id="node4" class="node"> +<title>INT_TOP</title> +<ellipse fill="lightblue" stroke="black" cx="377.6" cy="-354.98" rx="40.09" ry="40.09"/> +<text text-anchor="middle" x="377.6" y="-351.28" font-family="Times,serif" font-size="14.00">IntTop</text> +</g> +<!-- TOP->INT_TOP --> +<g id="edge1" class="edge"> +<title>TOP->INT_TOP</title> +<path fill="none" stroke="black" d="M377.6,-431.24C377.6,-420.99 377.6,-407.84 377.6,-395.42"/> +</g> +<!-- TUPLE --> +<g id="node13" class="node"> +<title>TUPLE</title> +<ellipse fill="lightblue" stroke="black" cx="750.6" cy="-235.14" rx="43.59" ry="43.59"/> +<text text-anchor="middle" x="750.6" y="-231.44" font-family="Times,serif" font-size="14.00">TUPLE</text> +</g> +<!-- TOP->TUPLE --> +<g id="edge23" class="edge"> +<title>TOP->TUPLE</title> +<path fill="none" stroke="black" d="M394.59,-440.95C451.03,-408.32 633.13,-303.05 712.75,-257.02"/> +</g> +<!-- BOT --> +<g id="node2" class="node"> +<title>BOT</title> +<ellipse fill="lightblue" stroke="black" cx="377.6" cy="-19.5" rx="19.5" ry="19.5"/> +<text text-anchor="middle" x="377.6" y="-15.8" font-family="Times,serif" font-size="14.00">⊥</text> +</g> +<!-- CTRL->BOT --> +<g id="edge26" class="edge"> +<title>CTRL->BOT</title> +<path fill="none" stroke="black" d="M53.14,-219.97C120.01,-178.65 304.22,-64.84 360.83,-29.86"/> +</g> +<!-- INT_MIN --> +<g id="node6" class="node"> +<title>INT_MIN</title> +<ellipse fill="lightblue" stroke="black" cx="119.6" cy="-235.14" rx="19.5" ry="19.5"/> +<text text-anchor="middle" x="119.6" y="-231.44" font-family="Times,serif" font-size="14.00">-n</text> +</g> +<!-- INT_TOP->INT_MIN --> +<g id="edge2" class="edge"> +<title>INT_TOP->INT_MIN</title> +<path fill="none" stroke="black" d="M341.18,-337.34C284.92,-311.65 179.02,-263.28 137.21,-244.18"/> +</g> +<!-- INT_MINDOTS --> +<g id="node7" class="node"> +<title>INT_MINDOTS</title> +<text text-anchor="middle" x="208.6" y="-231.44" font-family="Times,serif" font-size="14.00">...</text> +</g> +<!-- INT_TOP->INT_MINDOTS --> +<g id="edge3" class="edge"> +<title>INT_TOP->INT_MINDOTS</title> +<path fill="none" stroke="black" d="M345.01,-331.26C312.3,-308.45 262.65,-273.83 233.14,-253.25"/> +</g> +<!-- INT_MINUS --> +<g id="node8" class="node"> +<title>INT_MINUS</title> +<ellipse fill="lightblue" stroke="black" cx="297.6" cy="-235.14" rx="19.5" ry="19.5"/> +<text text-anchor="middle" x="297.6" y="-231.44" font-family="Times,serif" font-size="14.00">-1</text> +</g> +<!-- INT_TOP->INT_MINUS --> +<g id="edge4" class="edge"> +<title>INT_TOP->INT_MINUS</title> +<path fill="none" stroke="black" d="M355.31,-321.15C339.96,-298.54 320.25,-269.51 308.29,-251.89"/> +</g> +<!-- INT_ZERO --> +<g id="node9" class="node"> +<title>INT_ZERO</title> +<ellipse fill="lightblue" stroke="black" cx="377.6" cy="-235.14" rx="18" ry="18"/> +<text text-anchor="middle" x="377.6" y="-231.44" font-family="Times,serif" font-size="14.00">0</text> +</g> +<!-- INT_TOP->INT_ZERO --> +<g id="edge5" class="edge"> +<title>INT_TOP->INT_ZERO</title> +<path fill="none" stroke="black" d="M377.6,-314.41C377.6,-293.68 377.6,-269.36 377.6,-253.39"/> +</g> +<!-- INT_PLUS --> +<g id="node10" class="node"> +<title>INT_PLUS</title> +<ellipse fill="lightblue" stroke="black" cx="456.6" cy="-235.14" rx="18" ry="18"/> +<text text-anchor="middle" x="456.6" y="-231.44" font-family="Times,serif" font-size="14.00">1</text> +</g> +<!-- INT_TOP->INT_PLUS --> +<g id="edge6" class="edge"> +<title>INT_TOP->INT_PLUS</title> +<path fill="none" stroke="black" d="M399.6,-321.15C415.13,-298 435.17,-268.1 446.88,-250.63"/> +</g> +<!-- INT_MAXDOTS --> +<g id="node11" class="node"> +<title>INT_MAXDOTS</title> +<text text-anchor="middle" x="544.6" y="-231.44" font-family="Times,serif" font-size="14.00">...</text> +</g> +<!-- INT_TOP->INT_MAXDOTS --> +<g id="edge7" class="edge"> +<title>INT_TOP->INT_MAXDOTS</title> +<path fill="none" stroke="black" d="M410.19,-330.98C442.56,-308.14 491.43,-273.65 520.47,-253.16"/> +</g> +<!-- INT_MAX --> +<g id="node12" class="node"> +<title>INT_MAX</title> +<ellipse fill="lightblue" stroke="black" cx="639.6" cy="-235.14" rx="24.9" ry="24.9"/> +<text text-anchor="middle" x="639.6" y="-231.44" font-family="Times,serif" font-size="14.00">+n</text> +</g> +<!-- INT_TOP->INT_MAX --> +<g id="edge8" class="edge"> +<title>INT_TOP->INT_MAX</title> +<path fill="none" stroke="black" d="M414.03,-337.59C469.15,-312.8 572.09,-266.5 617.32,-246.16"/> +</g> +<!-- INT_BOT --> +<g id="node5" class="node"> +<title>INT_BOT</title> +<ellipse fill="lightblue" stroke="black" cx="377.6" cy="-115.29" rx="40.09" ry="40.09"/> +<text text-anchor="middle" x="377.6" y="-111.59" font-family="Times,serif" font-size="14.00">IntBot</text> +</g> +<!-- INT_BOT->BOT --> +<g id="edge16" class="edge"> +<title>INT_BOT->BOT</title> +<path fill="none" stroke="black" d="M377.6,-74.79C377.6,-62.37 377.6,-49.25 377.6,-39.01"/> +</g> +<!-- INT_MIN->INT_BOT --> +<g id="edge9" class="edge"> +<title>INT_MIN->INT_BOT</title> +<path fill="none" stroke="black" d="M137.33,-226.04C179.23,-206.9 285.02,-158.58 341.21,-132.91"/> +</g> +<!-- INT_MIN->INT_MINDOTS --> +<!-- INT_MINDOTS->INT_BOT --> +<g id="edge10" class="edge"> +<title>INT_MINDOTS->INT_BOT</title> +<path fill="none" stroke="black" d="M233.17,-217C262.65,-196.45 312.17,-161.91 344.87,-139.11"/> +</g> +<!-- INT_MINDOTS->INT_MINUS --> +<!-- INT_MINUS->INT_BOT --> +<g id="edge11" class="edge"> +<title>INT_MINUS->INT_BOT</title> +<path fill="none" stroke="black" d="M308.39,-218.24C320.33,-200.65 339.91,-171.81 355.2,-149.29"/> +</g> +<!-- INT_MINUS->INT_ZERO --> +<!-- INT_ZERO->INT_BOT --> +<g id="edge12" class="edge"> +<title>INT_ZERO->INT_BOT</title> +<path fill="none" stroke="black" d="M377.6,-217C377.6,-201.04 377.6,-176.66 377.6,-155.88"/> +</g> +<!-- INT_ZERO->INT_PLUS --> +<!-- INT_PLUS->INT_BOT --> +<g id="edge13" class="edge"> +<title>INT_PLUS->INT_BOT</title> +<path fill="none" stroke="black" d="M446.91,-219.69C435.21,-202.23 415.16,-172.33 399.63,-149.16"/> +</g> +<!-- INT_PLUS->INT_MAXDOTS --> +<!-- INT_MAXDOTS->INT_BOT --> +<g id="edge14" class="edge"> +<title>INT_MAXDOTS->INT_BOT</title> +<path fill="none" stroke="black" d="M520.31,-217C491.28,-196.51 442.55,-162.13 410.24,-139.33"/> +</g> +<!-- INT_MAXDOTS->INT_MAX --> +<!-- INT_MAX->INT_BOT --> +<g id="edge15" class="edge"> +<title>INT_MAX->INT_BOT</title> +<path fill="none" stroke="black" d="M617.26,-224.09C572.09,-203.77 469.52,-157.64 414.35,-132.82"/> +</g> +<!-- TUPLE->BOT --> +<g id="edge24" class="edge"> +<title>TUPLE->BOT</title> +<path fill="none" stroke="black" d="M712.78,-213.27C633.14,-167.23 450.85,-61.85 394.51,-29.27"/> +</g> +</g> +</svg> |
