From 34766f1a2e9e60626eb1bd5a08140fc41a3770c8 Mon Sep 17 00:00:00 2001
From: Cliff Click <cliffc@acm.org>
Date: Tue, 26 Nov 2024 17:00:45 -0800
Subject: Upgrades to the Type lattice diagrams

---
 chapter06/docs/lattice.gv  |  29 ++--
 chapter06/docs/lattice.svg | 412 ++++++++++++++++++++++-----------------------
 2 files changed, 219 insertions(+), 222 deletions(-)

(limited to 'chapter06/docs')

diff --git a/chapter06/docs/lattice.gv b/chapter06/docs/lattice.gv
index e533ad4a..782c2253 100644
--- a/chapter06/docs/lattice.gv
+++ b/chapter06/docs/lattice.gv
@@ -4,24 +4,24 @@ digraph Lattice {
     node [shape=circle, style=filled, fillcolor=lightblue];
     nodesep=0.6;
 
-    TOP [label="⊤"];
-    BOT [label="⊥"];
+    TOP [label="⊤" , fillcolor=black, fontcolor=white];
+    BOT [label="⊥", fillcolor=black, fontcolor=white];
 
-    XCTRL [label="~Ctrl"];
-    CTRL [label="Ctrl"];
+    XCTRL [label="⊤ :Ctrl", fillcolor=yellow];
+    CTRL  [label="⊥ :Ctrl", fillcolor=yellow];
 
-    INT_TOP [label="IntTop"];
-    INT_BOT [label="IntBot"];
+    INT_TOP [label="⊤ :Int"];
+    INT_BOT [label="⊥ :Int"];
 
     INT_MIN [label="-n"];
-    INT_MINDOTS [label="..." shape=none style=none];
     INT_MINUS [label="-1"];
+    INT_MINDOTS [label="..." shape=none style=none];
     INT_ZERO [label="0"];
     INT_PLUS [label="1"];
     INT_MAXDOTS [label="..." shape=none style=none];
     INT_MAX [label="+n"];
 
-    TUPLE [label="TUPLE"];
+    TUPLE [label="TUPLE", fillcolor=pink];
 
     // Define edges
     edge [arrowhead=none];
@@ -45,20 +45,17 @@ digraph Lattice {
 
     INT_MIN -> INT_MINDOTS -> INT_MINUS -> INT_ZERO -> INT_PLUS -> INT_MAXDOTS -> INT_MAX [style=invis];
 
-    TOP          -> TUPLE;
-    TUPLE        -> BOT;
+    TOP   -> TUPLE;
+    TUPLE -> BOT;
 
-    TOP -> XCTRL;
+    TOP   -> XCTRL;
     XCTRL -> CTRL;
-    CTRL -> BOT;
+    CTRL  -> BOT;
 
     // Additional customization
     {rank=same; TOP}
     {rank=same; INT_TOP; XCTRL}
-    {rank=same; INT_MIN; INT_MINDOTS;
-                INT_MINUS; INT_ZERO;
-                INT_PLUS; INT_MAXDOTS;
-                INT_MAX; TUPLE}
+    {rank=same; INT_MIN; INT_MINDOTS; INT_MINUS; INT_ZERO; INT_PLUS; INT_MAXDOTS; INT_MAX; TUPLE }
     {rank=same; INT_BOT; CTRL}
     {rank=same; BOT;}
 }
diff --git a/chapter06/docs/lattice.svg b/chapter06/docs/lattice.svg
index 713b54c1..f4929b41 100644
--- a/chapter06/docs/lattice.svg
+++ b/chapter06/docs/lattice.svg
@@ -1,206 +1,206 @@
-<?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="702pt" height="478pt"
- viewBox="0.00 0.00 702.04 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 698.04,-474.27 698.04,4 -4,4"/>
-<!-- TOP -->
-<g id="node1" class="node">
-<title>TOP</title>
-<ellipse fill="lightblue" stroke="black" cx="277.5" cy="-450.77" rx="19.5" ry="19.5"/>
-<text text-anchor="middle" x="277.5" y="-447.07" font-family="Times,serif" font-size="14.00">⊤</text>
-</g>
-<!-- XCTRL -->
-<g id="node3" class="node">
-<title>XCTRL</title>
-<ellipse fill="lightblue" stroke="black" cx="46.5" cy="-354.98" rx="36.29" ry="36.29"/>
-<text text-anchor="middle" x="46.5" y="-351.28" font-family="Times,serif" font-size="14.00">~Ctrl</text>
-</g>
-<!-- TOP&#45;&gt;XCTRL -->
-<g id="edge25" class="edge">
-<title>TOP&#45;&gt;XCTRL</title>
-<path fill="none" stroke="black" d="M259.76,-442.57C221.3,-426.95 129.74,-389.78 80.01,-369.59"/>
-</g>
-<!-- INT_TOP -->
-<g id="node5" class="node">
-<title>INT_TOP</title>
-<ellipse fill="lightblue" stroke="black" cx="277.5" cy="-354.98" rx="40.09" ry="40.09"/>
-<text text-anchor="middle" x="277.5" y="-351.28" font-family="Times,serif" font-size="14.00">IntTop</text>
-</g>
-<!-- TOP&#45;&gt;INT_TOP -->
-<g id="edge1" class="edge">
-<title>TOP&#45;&gt;INT_TOP</title>
-<path fill="none" stroke="black" d="M277.5,-431.24C277.5,-420.99 277.5,-407.84 277.5,-395.42"/>
-</g>
-<!-- TUPLE -->
-<g id="node14" class="node">
-<title>TUPLE</title>
-<ellipse fill="lightblue" stroke="black" cx="650.5" cy="-235.14" rx="43.59" ry="43.59"/>
-<text text-anchor="middle" x="650.5" y="-231.44" font-family="Times,serif" font-size="14.00">TUPLE</text>
-</g>
-<!-- TOP&#45;&gt;TUPLE -->
-<g id="edge23" class="edge">
-<title>TOP&#45;&gt;TUPLE</title>
-<path fill="none" stroke="black" d="M294.49,-440.95C350.93,-408.32 533.03,-303.05 612.65,-257.02"/>
-</g>
-<!-- BOT -->
-<g id="node2" class="node">
-<title>BOT</title>
-<ellipse fill="lightblue" stroke="black" cx="277.5" cy="-19.5" rx="19.5" ry="19.5"/>
-<text text-anchor="middle" x="277.5" y="-15.8" font-family="Times,serif" font-size="14.00">⊥</text>
-</g>
-<!-- CTRL -->
-<g id="node4" class="node">
-<title>CTRL</title>
-<ellipse fill="lightblue" stroke="black" cx="50.5" cy="-115.29" rx="28.7" ry="28.7"/>
-<text text-anchor="middle" x="50.5" y="-111.59" font-family="Times,serif" font-size="14.00">Ctrl</text>
-</g>
-<!-- XCTRL&#45;&gt;CTRL -->
-<g id="edge26" class="edge">
-<title>XCTRL&#45;&gt;CTRL</title>
-<path fill="none" stroke="black" d="M47.11,-318.58C47.9,-270.77 49.29,-187.82 50.02,-144.12"/>
-</g>
-<!-- CTRL&#45;&gt;BOT -->
-<g id="edge27" class="edge">
-<title>CTRL&#45;&gt;BOT</title>
-<path fill="none" stroke="black" d="M76.98,-103.35C123.76,-84.02 219.83,-44.32 259.63,-27.88"/>
-</g>
-<!-- INT_MIN -->
-<g id="node7" class="node">
-<title>INT_MIN</title>
-<ellipse fill="lightblue" stroke="black" cx="19.5" cy="-235.14" rx="19.5" ry="19.5"/>
-<text text-anchor="middle" x="19.5" y="-231.44" font-family="Times,serif" font-size="14.00">&#45;n</text>
-</g>
-<!-- INT_TOP&#45;&gt;INT_MIN -->
-<g id="edge2" class="edge">
-<title>INT_TOP&#45;&gt;INT_MIN</title>
-<path fill="none" stroke="black" d="M241.08,-337.34C184.83,-311.65 78.92,-263.28 37.12,-244.18"/>
-</g>
-<!-- INT_MINDOTS -->
-<g id="node8" class="node">
-<title>INT_MINDOTS</title>
-<text text-anchor="middle" x="108.5" y="-231.44" font-family="Times,serif" font-size="14.00">...</text>
-</g>
-<!-- INT_TOP&#45;&gt;INT_MINDOTS -->
-<g id="edge3" class="edge">
-<title>INT_TOP&#45;&gt;INT_MINDOTS</title>
-<path fill="none" stroke="black" d="M244.91,-331.26C212.21,-308.45 162.56,-273.83 133.04,-253.25"/>
-</g>
-<!-- INT_MINUS -->
-<g id="node9" class="node">
-<title>INT_MINUS</title>
-<ellipse fill="lightblue" stroke="black" cx="197.5" cy="-235.14" rx="19.5" ry="19.5"/>
-<text text-anchor="middle" x="197.5" y="-231.44" font-family="Times,serif" font-size="14.00">&#45;1</text>
-</g>
-<!-- INT_TOP&#45;&gt;INT_MINUS -->
-<g id="edge4" class="edge">
-<title>INT_TOP&#45;&gt;INT_MINUS</title>
-<path fill="none" stroke="black" d="M255.21,-321.15C239.86,-298.54 220.15,-269.51 208.19,-251.89"/>
-</g>
-<!-- INT_ZERO -->
-<g id="node10" class="node">
-<title>INT_ZERO</title>
-<ellipse fill="lightblue" stroke="black" cx="277.5" cy="-235.14" rx="18" ry="18"/>
-<text text-anchor="middle" x="277.5" y="-231.44" font-family="Times,serif" font-size="14.00">0</text>
-</g>
-<!-- INT_TOP&#45;&gt;INT_ZERO -->
-<g id="edge5" class="edge">
-<title>INT_TOP&#45;&gt;INT_ZERO</title>
-<path fill="none" stroke="black" d="M277.5,-314.41C277.5,-293.68 277.5,-269.36 277.5,-253.39"/>
-</g>
-<!-- INT_PLUS -->
-<g id="node11" class="node">
-<title>INT_PLUS</title>
-<ellipse fill="lightblue" stroke="black" cx="356.5" cy="-235.14" rx="18" ry="18"/>
-<text text-anchor="middle" x="356.5" y="-231.44" font-family="Times,serif" font-size="14.00">1</text>
-</g>
-<!-- INT_TOP&#45;&gt;INT_PLUS -->
-<g id="edge6" class="edge">
-<title>INT_TOP&#45;&gt;INT_PLUS</title>
-<path fill="none" stroke="black" d="M299.5,-321.15C315.03,-298 335.07,-268.1 346.78,-250.63"/>
-</g>
-<!-- INT_MAXDOTS -->
-<g id="node12" class="node">
-<title>INT_MAXDOTS</title>
-<text text-anchor="middle" x="444.5" y="-231.44" font-family="Times,serif" font-size="14.00">...</text>
-</g>
-<!-- INT_TOP&#45;&gt;INT_MAXDOTS -->
-<g id="edge7" class="edge">
-<title>INT_TOP&#45;&gt;INT_MAXDOTS</title>
-<path fill="none" stroke="black" d="M310.09,-330.98C342.46,-308.14 391.33,-273.65 420.37,-253.16"/>
-</g>
-<!-- INT_MAX -->
-<g id="node13" class="node">
-<title>INT_MAX</title>
-<ellipse fill="lightblue" stroke="black" cx="539.5" cy="-235.14" rx="24.9" ry="24.9"/>
-<text text-anchor="middle" x="539.5" y="-231.44" font-family="Times,serif" font-size="14.00">+n</text>
-</g>
-<!-- INT_TOP&#45;&gt;INT_MAX -->
-<g id="edge8" class="edge">
-<title>INT_TOP&#45;&gt;INT_MAX</title>
-<path fill="none" stroke="black" d="M313.93,-337.59C369.05,-312.8 471.99,-266.5 517.22,-246.16"/>
-</g>
-<!-- INT_BOT -->
-<g id="node6" class="node">
-<title>INT_BOT</title>
-<ellipse fill="lightblue" stroke="black" cx="277.5" cy="-115.29" rx="40.09" ry="40.09"/>
-<text text-anchor="middle" x="277.5" y="-111.59" font-family="Times,serif" font-size="14.00">IntBot</text>
-</g>
-<!-- INT_BOT&#45;&gt;BOT -->
-<g id="edge16" class="edge">
-<title>INT_BOT&#45;&gt;BOT</title>
-<path fill="none" stroke="black" d="M277.5,-74.79C277.5,-62.37 277.5,-49.25 277.5,-39.01"/>
-</g>
-<!-- INT_MIN&#45;&gt;INT_BOT -->
-<g id="edge9" class="edge">
-<title>INT_MIN&#45;&gt;INT_BOT</title>
-<path fill="none" stroke="black" d="M37.23,-226.04C79.13,-206.9 184.92,-158.58 241.11,-132.91"/>
-</g>
-<!-- INT_MIN&#45;&gt;INT_MINDOTS -->
-<!-- INT_MINDOTS&#45;&gt;INT_BOT -->
-<g id="edge10" class="edge">
-<title>INT_MINDOTS&#45;&gt;INT_BOT</title>
-<path fill="none" stroke="black" d="M133.07,-217C162.55,-196.45 212.07,-161.91 244.77,-139.11"/>
-</g>
-<!-- INT_MINDOTS&#45;&gt;INT_MINUS -->
-<!-- INT_MINUS&#45;&gt;INT_BOT -->
-<g id="edge11" class="edge">
-<title>INT_MINUS&#45;&gt;INT_BOT</title>
-<path fill="none" stroke="black" d="M208.29,-218.24C220.23,-200.65 239.81,-171.81 255.1,-149.29"/>
-</g>
-<!-- INT_MINUS&#45;&gt;INT_ZERO -->
-<!-- INT_ZERO&#45;&gt;INT_BOT -->
-<g id="edge12" class="edge">
-<title>INT_ZERO&#45;&gt;INT_BOT</title>
-<path fill="none" stroke="black" d="M277.5,-217C277.5,-201.04 277.5,-176.66 277.5,-155.88"/>
-</g>
-<!-- INT_ZERO&#45;&gt;INT_PLUS -->
-<!-- INT_PLUS&#45;&gt;INT_BOT -->
-<g id="edge13" class="edge">
-<title>INT_PLUS&#45;&gt;INT_BOT</title>
-<path fill="none" stroke="black" d="M346.81,-219.69C335.11,-202.23 315.06,-172.33 299.53,-149.16"/>
-</g>
-<!-- INT_PLUS&#45;&gt;INT_MAXDOTS -->
-<!-- INT_MAXDOTS&#45;&gt;INT_BOT -->
-<g id="edge14" class="edge">
-<title>INT_MAXDOTS&#45;&gt;INT_BOT</title>
-<path fill="none" stroke="black" d="M420.22,-217C391.18,-196.51 342.45,-162.13 310.14,-139.33"/>
-</g>
-<!-- INT_MAXDOTS&#45;&gt;INT_MAX -->
-<!-- INT_MAX&#45;&gt;INT_BOT -->
-<g id="edge15" class="edge">
-<title>INT_MAX&#45;&gt;INT_BOT</title>
-<path fill="none" stroke="black" d="M517.16,-224.09C471.99,-203.77 369.42,-157.64 314.25,-132.82"/>
-</g>
-<!-- TUPLE&#45;&gt;BOT -->
-<g id="edge24" class="edge">
-<title>TUPLE&#45;&gt;BOT</title>
-<path fill="none" stroke="black" d="M612.68,-213.27C533.04,-167.23 350.75,-61.85 294.41,-29.27"/>
-</g>
-</g>
-</svg>
+<?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 12.2.0 (20241103.1931)
+ -->
+<!-- Title: Lattice Pages: 1 -->
+<svg width="686pt" height="485pt"
+ viewBox="0.00 0.00 686.18 484.71" 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 480.71)">
+<title>Lattice</title>
+<polygon fill="white" stroke="none" points="-4,4 -4,-480.71 682.18,-480.71 682.18,4 -4,4"/>
+<!-- TOP -->
+<g id="node1" class="node">
+<title>TOP</title>
+<ellipse fill="black" stroke="black" cx="276.6" cy="-455.59" rx="21.12" ry="21.12"/>
+<text text-anchor="middle" x="276.6" y="-450.16" font-family="Times New Roman,serif" font-size="14.00" fill="white">⊤</text>
+</g>
+<!-- XCTRL -->
+<g id="node3" class="node">
+<title>XCTRL</title>
+<ellipse fill="yellow" stroke="black" cx="44.6" cy="-356.2" rx="42.26" ry="42.26"/>
+<text text-anchor="middle" x="44.6" y="-351.53" font-family="Times New Roman,serif" font-size="14.00">⊤ :Ctrl</text>
+</g>
+<!-- TOP&#45;&gt;XCTRL -->
+<g id="edge25" class="edge">
+<title>TOP&#45;&gt;XCTRL</title>
+<path fill="none" stroke="black" d="M257.21,-446.45C219.1,-430.45 133.74,-394.62 83.54,-373.55"/>
+</g>
+<!-- INT_TOP -->
+<g id="node5" class="node">
+<title>INT_TOP</title>
+<ellipse fill="lightblue" stroke="black" cx="276.6" cy="-356.2" rx="38.06" ry="38.06"/>
+<text text-anchor="middle" x="276.6" y="-351.53" font-family="Times New Roman,serif" font-size="14.00">⊤ :Int</text>
+</g>
+<!-- TOP&#45;&gt;INT_TOP -->
+<g id="edge1" class="edge">
+<title>TOP&#45;&gt;INT_TOP</title>
+<path fill="none" stroke="black" d="M276.6,-434.41C276.6,-422.93 276.6,-408.19 276.6,-394.67"/>
+</g>
+<!-- TUPLE -->
+<g id="node14" class="node">
+<title>TUPLE</title>
+<ellipse fill="pink" stroke="black" cx="638.6" cy="-238.36" rx="39.58" ry="39.58"/>
+<text text-anchor="middle" x="638.6" y="-233.31" font-family="Times New Roman,serif" font-size="14.00">TUPLE</text>
+</g>
+<!-- TOP&#45;&gt;TUPLE -->
+<g id="edge23" class="edge">
+<title>TOP&#45;&gt;TUPLE</title>
+<path fill="none" stroke="black" d="M295.05,-444.52C352.6,-409.98 529.5,-303.82 604.46,-258.84"/>
+</g>
+<!-- BOT -->
+<g id="node2" class="node">
+<title>BOT</title>
+<ellipse fill="black" stroke="black" cx="276.6" cy="-21.12" rx="21.12" ry="21.12"/>
+<text text-anchor="middle" x="276.6" y="-15.7" font-family="Times New Roman,serif" font-size="14.00" fill="white">⊥</text>
+</g>
+<!-- CTRL -->
+<g id="node4" class="node">
+<title>CTRL</title>
+<ellipse fill="yellow" stroke="black" cx="44.6" cy="-120.51" rx="42.26" ry="42.26"/>
+<text text-anchor="middle" x="44.6" y="-115.84" font-family="Times New Roman,serif" font-size="14.00">⊥ :Ctrl</text>
+</g>
+<!-- XCTRL&#45;&gt;CTRL -->
+<g id="edge26" class="edge">
+<title>XCTRL&#45;&gt;CTRL</title>
+<path fill="none" stroke="black" d="M44.6,-313.52C44.6,-270.94 44.6,-205.88 44.6,-163.27"/>
+</g>
+<!-- CTRL&#45;&gt;BOT -->
+<g id="edge27" class="edge">
+<title>CTRL&#45;&gt;BOT</title>
+<path fill="none" stroke="black" d="M83.43,-103.21C133.61,-82.15 219.04,-46.28 257.2,-30.27"/>
+</g>
+<!-- INT_MIN -->
+<g id="node7" class="node">
+<title>INT_MIN</title>
+<ellipse fill="lightblue" stroke="black" cx="18.6" cy="-238.36" rx="18.6" ry="18.6"/>
+<text text-anchor="middle" x="18.6" y="-233.31" font-family="Times New Roman,serif" font-size="14.00">&#45;n</text>
+</g>
+<!-- INT_TOP&#45;&gt;INT_MIN -->
+<g id="edge2" class="edge">
+<title>INT_TOP&#45;&gt;INT_MIN</title>
+<path fill="none" stroke="black" d="M242.07,-339.7C186.05,-314.54 77.4,-265.76 35.58,-246.98"/>
+</g>
+<!-- INT_MINUS -->
+<g id="node8" class="node">
+<title>INT_MINUS</title>
+<ellipse fill="lightblue" stroke="black" cx="196.6" cy="-238.36" rx="18.6" ry="18.6"/>
+<text text-anchor="middle" x="196.6" y="-233.31" font-family="Times New Roman,serif" font-size="14.00">&#45;1</text>
+</g>
+<!-- INT_TOP&#45;&gt;INT_MINUS -->
+<g id="edge4" class="edge">
+<title>INT_TOP&#45;&gt;INT_MINUS</title>
+<path fill="none" stroke="black" d="M255.16,-324.16C239.51,-301.5 219,-271.8 206.87,-254.23"/>
+</g>
+<!-- INT_MINDOTS -->
+<g id="node9" class="node">
+<title>INT_MINDOTS</title>
+<text text-anchor="middle" x="107.6" y="-233.31" font-family="Times New Roman,serif" font-size="14.00">...</text>
+</g>
+<!-- INT_TOP&#45;&gt;INT_MINDOTS -->
+<g id="edge3" class="edge">
+<title>INT_TOP&#45;&gt;INT_MINDOTS</title>
+<path fill="none" stroke="black" d="M245.6,-333.95C213.01,-311.61 162.38,-276.91 132.36,-256.33"/>
+</g>
+<!-- INT_ZERO -->
+<g id="node10" class="node">
+<title>INT_ZERO</title>
+<ellipse fill="lightblue" stroke="black" cx="276.6" cy="-238.36" rx="18" ry="18"/>
+<text text-anchor="middle" x="276.6" y="-233.31" font-family="Times New Roman,serif" font-size="14.00">0</text>
+</g>
+<!-- INT_TOP&#45;&gt;INT_ZERO -->
+<g id="edge5" class="edge">
+<title>INT_TOP&#45;&gt;INT_ZERO</title>
+<path fill="none" stroke="black" d="M276.6,-317.91C276.6,-297.4 276.6,-272.93 276.6,-256.82"/>
+</g>
+<!-- INT_PLUS -->
+<g id="node11" class="node">
+<title>INT_PLUS</title>
+<ellipse fill="lightblue" stroke="black" cx="355.6" cy="-238.36" rx="18" ry="18"/>
+<text text-anchor="middle" x="355.6" y="-233.31" font-family="Times New Roman,serif" font-size="14.00">1</text>
+</g>
+<!-- INT_TOP&#45;&gt;INT_PLUS -->
+<g id="edge6" class="edge">
+<title>INT_TOP&#45;&gt;INT_PLUS</title>
+<path fill="none" stroke="black" d="M297.77,-324.16C313.31,-301.37 333.71,-271.45 345.66,-253.92"/>
+</g>
+<!-- INT_MAXDOTS -->
+<g id="node12" class="node">
+<title>INT_MAXDOTS</title>
+<text text-anchor="middle" x="443.6" y="-233.31" font-family="Times New Roman,serif" font-size="14.00">...</text>
+</g>
+<!-- INT_TOP&#45;&gt;INT_MAXDOTS -->
+<g id="edge7" class="edge">
+<title>INT_TOP&#45;&gt;INT_MAXDOTS</title>
+<path fill="none" stroke="black" d="M307.62,-333.68C339.88,-311.3 389.71,-276.74 419.25,-256.25"/>
+</g>
+<!-- INT_MAX -->
+<g id="node13" class="node">
+<title>INT_MAX</title>
+<ellipse fill="lightblue" stroke="black" cx="534.6" cy="-238.36" rx="21.15" ry="21.15"/>
+<text text-anchor="middle" x="534.6" y="-233.31" font-family="Times New Roman,serif" font-size="14.00">+n</text>
+</g>
+<!-- INT_TOP&#45;&gt;INT_MAX -->
+<g id="edge8" class="edge">
+<title>INT_TOP&#45;&gt;INT_MAX</title>
+<path fill="none" stroke="black" d="M311.12,-339.7C366.18,-314.97 472.08,-267.43 515.4,-247.97"/>
+</g>
+<!-- INT_BOT -->
+<g id="node6" class="node">
+<title>INT_BOT</title>
+<ellipse fill="lightblue" stroke="black" cx="276.6" cy="-120.51" rx="38.06" ry="38.06"/>
+<text text-anchor="middle" x="276.6" y="-115.84" font-family="Times New Roman,serif" font-size="14.00">⊥ :Int</text>
+</g>
+<!-- INT_BOT&#45;&gt;BOT -->
+<g id="edge16" class="edge">
+<title>INT_BOT&#45;&gt;BOT</title>
+<path fill="none" stroke="black" d="M276.6,-82.14C276.6,-68.73 276.6,-54.11 276.6,-42.65"/>
+</g>
+<!-- INT_MIN&#45;&gt;INT_BOT -->
+<g id="edge9" class="edge">
+<title>INT_MIN&#45;&gt;INT_BOT</title>
+<path fill="none" stroke="black" d="M35.52,-229.76C77.34,-210.98 186.17,-162.11 242.19,-136.96"/>
+</g>
+<!-- INT_MIN&#45;&gt;INT_MINDOTS -->
+<!-- INT_MINUS&#45;&gt;INT_BOT -->
+<g id="edge11" class="edge">
+<title>INT_MINUS&#45;&gt;INT_BOT</title>
+<path fill="none" stroke="black" d="M206.73,-222.68C218.92,-205.03 239.72,-174.92 255.46,-152.12"/>
+</g>
+<!-- INT_MINUS&#45;&gt;INT_ZERO -->
+<!-- INT_MINDOTS&#45;&gt;INT_BOT -->
+<g id="edge10" class="edge">
+<title>INT_MINDOTS&#45;&gt;INT_BOT</title>
+<path fill="none" stroke="black" d="M132.17,-220.51C162.11,-199.99 212.71,-165.3 245.38,-142.91"/>
+</g>
+<!-- INT_MINDOTS&#45;&gt;INT_MINUS -->
+<!-- INT_ZERO&#45;&gt;INT_BOT -->
+<g id="edge12" class="edge">
+<title>INT_ZERO&#45;&gt;INT_BOT</title>
+<path fill="none" stroke="black" d="M276.6,-220.01C276.6,-203.86 276.6,-179.23 276.6,-158.64"/>
+</g>
+<!-- INT_ZERO&#45;&gt;INT_PLUS -->
+<!-- INT_PLUS&#45;&gt;INT_BOT -->
+<g id="edge13" class="edge">
+<title>INT_PLUS&#45;&gt;INT_BOT</title>
+<path fill="none" stroke="black" d="M345.91,-223.15C333.96,-205.63 313.31,-175.35 297.65,-152.39"/>
+</g>
+<!-- INT_PLUS&#45;&gt;INT_MAXDOTS -->
+<!-- INT_MAXDOTS&#45;&gt;INT_BOT -->
+<g id="edge14" class="edge">
+<title>INT_MAXDOTS&#45;&gt;INT_BOT</title>
+<path fill="none" stroke="black" d="M419.31,-220.51C389.82,-200.05 340.03,-165.51 307.74,-143.12"/>
+</g>
+<!-- INT_MAXDOTS&#45;&gt;INT_MAX -->
+<!-- INT_MAX&#45;&gt;INT_BOT -->
+<g id="edge15" class="edge">
+<title>INT_MAX&#45;&gt;INT_BOT</title>
+<path fill="none" stroke="black" d="M515.62,-228.84C472.45,-209.45 366.34,-161.81 311.17,-137.04"/>
+</g>
+<!-- TUPLE&#45;&gt;BOT -->
+<g id="edge24" class="edge">
+<title>TUPLE&#45;&gt;BOT</title>
+<path fill="none" stroke="black" d="M604.54,-217.92C529.56,-172.93 352.32,-66.57 294.9,-32.11"/>
+</g>
+</g>
+</svg>
-- 
cgit v1.2.3