diff options
| -rw-r--r-- | TypeAnalysis.md | bin | 5852 -> 6680 bytes | |||
| -rw-r--r-- | chapter12/docs/lattice.gv | 2 | ||||
| -rw-r--r-- | docs/Makefile | 12 | ||||
| -rw-r--r-- | docs/lattice_i.gv | 40 | ||||
| -rw-r--r-- | docs/lattice_i.svg | 159 | ||||
| -rw-r--r-- | docs/lattice_if.gv | 71 | ||||
| -rw-r--r-- | docs/lattice_if.svg | 265 |
7 files changed, 548 insertions, 1 deletions
diff --git a/TypeAnalysis.md b/TypeAnalysis.md Binary files differindex 3a857d88..a260710b 100644 --- a/TypeAnalysis.md +++ b/TypeAnalysis.md diff --git a/chapter12/docs/lattice.gv b/chapter12/docs/lattice.gv index eec7cc1d..23b3f7a7 100644 --- a/chapter12/docs/lattice.gv +++ b/chapter12/docs/lattice.gv @@ -38,7 +38,7 @@ digraph Lattice { INT_MINDOTS -> INT_ZERO -> INT_MAXDOTS [style=invis]; // ---------------------- - // Integers + // Floats FLT_TOP [label=<<B>⊤</B >:flt>, fillcolor=aqua, shape=oval]; FLT_BOT [label=<<B>⊥</B>:flt>, fillcolor=aqua, shape=oval]; diff --git a/docs/Makefile b/docs/Makefile new file mode 100644 index 00000000..12659b8f --- /dev/null +++ b/docs/Makefile @@ -0,0 +1,12 @@ +GV := $(wildcard *.gv) +SVG := $(patsubst %.gv,%.svg,$(GV)) + +.PHONY: all +all: $(SVG) + +%.svg: %.gv + dot -Tsvg $< > $@ + +.PHONY: clean +clean: + @rm -f $(SVG) diff --git a/docs/lattice_i.gv b/docs/lattice_i.gv new file mode 100644 index 00000000..fe8df136 --- /dev/null +++ b/docs/lattice_i.gv @@ -0,0 +1,40 @@ +digraph Lattice { + compound = true; + // Define nodes + splines=false; + node [shape=circle, style=filled]; + nodesep=0.6; + + // ---------------------- + // Integers + INT_TOP [label=<<B>⊤</B >:int>, fillcolor=lightblue, shape=oval]; + INT_BOT [label=<<B>⊥</B>:int>, fillcolor=lightblue, shape=oval]; + + INT_MIN [label="-n" , fillcolor=lightblue]; + INT_MINDOTS [label="...", fillcolor=lightblue shape=oval]; + INT_MINUS [label="-1" , fillcolor=lightblue]; + INT_ZERO [label="0" , fillcolor=lightblue]; + INT_PLUS [label="1" , fillcolor=lightblue]; + INT_MAXDOTS [label="...", fillcolor=lightblue, shape=oval]; + INT_MAX [label="+n" , fillcolor=lightblue]; + + 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_MIN -> INT_MINDOTS -> INT_MINUS -> INT_ZERO -> INT_PLUS -> INT_MAXDOTS -> INT_MAX [style=invis]; + + // Additional customization + {rank=same; INT_MIN; INT_MINDOTS; INT_MINUS; INT_ZERO; INT_PLUS; INT_MAXDOTS; INT_MAX; } +} diff --git a/docs/lattice_i.svg b/docs/lattice_i.svg new file mode 100644 index 00000000..b11d57aa --- /dev/null +++ b/docs/lattice_i.svg @@ -0,0 +1,159 @@ +<?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="564pt" height="194pt"
+ viewBox="0.00 0.00 563.75 194.31" 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 190.31)">
+<title>Lattice</title>
+<polygon fill="white" stroke="none" points="-4,4 -4,-190.31 559.75,-190.31 559.75,4 -4,4"/>
+<!-- INT_TOP -->
+<g id="node1" class="node">
+<title>INT_TOP</title>
+<ellipse fill="lightblue" stroke="black" cx="276.6" cy="-168.31" rx="33.95" ry="18"/>
+<text text-anchor="start" x="259.72" y="-164.26" font-family="Times New Roman,serif" font-weight="bold" font-size="14.00">⊤</text>
+<text text-anchor="start" x="275.47" y="-164.26" font-family="Times New Roman,serif" font-size="14.00">:int</text>
+</g>
+<!-- INT_MIN -->
+<g id="node3" class="node">
+<title>INT_MIN</title>
+<ellipse fill="lightblue" stroke="black" cx="18.6" cy="-93.15" rx="18.6" ry="18.6"/>
+<text text-anchor="middle" x="18.6" y="-88.1" font-family="Times New Roman,serif" font-size="14.00">-n</text>
+</g>
+<!-- INT_TOP->INT_MIN -->
+<g id="edge1" class="edge">
+<title>INT_TOP->INT_MIN</title>
+<path fill="none" stroke="black" d="M247,-158.92C197.13,-144.78 96.96,-116.37 47.53,-102.36"/>
+<polygon fill="black" stroke="black" points="48.71,-99.06 38.13,-99.69 46.8,-105.79 48.71,-99.06"/>
+</g>
+<!-- INT_MINDOTS -->
+<g id="node4" class="node">
+<title>INT_MINDOTS</title>
+<ellipse fill="lightblue" stroke="black" cx="107.6" cy="-93.15" rx="27" ry="18"/>
+<text text-anchor="middle" x="107.6" y="-88.1" font-family="Times New Roman,serif" font-size="14.00">...</text>
+</g>
+<!-- INT_TOP->INT_MINDOTS -->
+<g id="edge2" class="edge">
+<title>INT_TOP->INT_MINDOTS</title>
+<path fill="none" stroke="black" d="M250.93,-156.2C221.31,-143.38 172.55,-122.27 140.26,-108.29"/>
+<polygon fill="black" stroke="black" points="141.94,-105.21 131.38,-104.45 139.16,-111.63 141.94,-105.21"/>
+</g>
+<!-- INT_MINUS -->
+<g id="node5" class="node">
+<title>INT_MINUS</title>
+<ellipse fill="lightblue" stroke="black" cx="196.6" cy="-93.15" rx="18.6" ry="18.6"/>
+<text text-anchor="middle" x="196.6" y="-88.1" font-family="Times New Roman,serif" font-size="14.00">-1</text>
+</g>
+<!-- INT_TOP->INT_MINUS -->
+<g id="edge3" class="edge">
+<title>INT_TOP->INT_MINUS</title>
+<path fill="none" stroke="black" d="M260.02,-152.15C247.97,-141.13 231.55,-126.11 218.43,-114.12"/>
+<polygon fill="black" stroke="black" points="220.83,-111.57 211.09,-107.41 216.11,-116.74 220.83,-111.57"/>
+</g>
+<!-- INT_ZERO -->
+<g id="node6" class="node">
+<title>INT_ZERO</title>
+<ellipse fill="lightblue" stroke="black" cx="276.6" cy="-93.15" rx="18" ry="18"/>
+<text text-anchor="middle" x="276.6" y="-88.1" font-family="Times New Roman,serif" font-size="14.00">0</text>
+</g>
+<!-- INT_TOP->INT_ZERO -->
+<g id="edge4" class="edge">
+<title>INT_TOP->INT_ZERO</title>
+<path fill="none" stroke="black" d="M276.6,-149.97C276.6,-141.92 276.6,-132.14 276.6,-123.02"/>
+<polygon fill="black" stroke="black" points="280.1,-123.13 276.6,-113.13 273.1,-123.13 280.1,-123.13"/>
+</g>
+<!-- INT_PLUS -->
+<g id="node7" class="node">
+<title>INT_PLUS</title>
+<ellipse fill="lightblue" stroke="black" cx="355.6" cy="-93.15" rx="18" ry="18"/>
+<text text-anchor="middle" x="355.6" y="-88.1" font-family="Times New Roman,serif" font-size="14.00">1</text>
+</g>
+<!-- INT_TOP->INT_PLUS -->
+<g id="edge5" class="edge">
+<title>INT_TOP->INT_PLUS</title>
+<path fill="none" stroke="black" d="M292.96,-152.15C305.01,-141 321.48,-125.74 334.51,-113.68"/>
+<polygon fill="black" stroke="black" points="336.82,-116.31 341.78,-106.95 332.06,-111.18 336.82,-116.31"/>
+</g>
+<!-- INT_MAXDOTS -->
+<g id="node8" class="node">
+<title>INT_MAXDOTS</title>
+<ellipse fill="lightblue" stroke="black" cx="443.6" cy="-93.15" rx="27" ry="18"/>
+<text text-anchor="middle" x="443.6" y="-88.1" font-family="Times New Roman,serif" font-size="14.00">...</text>
+</g>
+<!-- INT_TOP->INT_MAXDOTS -->
+<g id="edge6" class="edge">
+<title>INT_TOP->INT_MAXDOTS</title>
+<path fill="none" stroke="black" d="M302.32,-156.04C331.46,-143.28 379,-122.45 410.79,-108.53"/>
+<polygon fill="black" stroke="black" points="412.17,-111.74 419.93,-104.52 409.36,-105.33 412.17,-111.74"/>
+</g>
+<!-- INT_MAX -->
+<g id="node9" class="node">
+<title>INT_MAX</title>
+<ellipse fill="lightblue" stroke="black" cx="534.6" cy="-93.15" rx="21.15" ry="21.15"/>
+<text text-anchor="middle" x="534.6" y="-88.1" font-family="Times New Roman,serif" font-size="14.00">+n</text>
+</g>
+<!-- INT_TOP->INT_MAX -->
+<g id="edge7" class="edge">
+<title>INT_TOP->INT_MAX</title>
+<path fill="none" stroke="black" d="M306.19,-158.92C355.31,-144.99 453.21,-117.23 503.38,-103.01"/>
+<polygon fill="black" stroke="black" points="504.07,-106.45 512.73,-100.35 502.16,-99.71 504.07,-106.45"/>
+</g>
+<!-- INT_BOT -->
+<g id="node2" class="node">
+<title>INT_BOT</title>
+<ellipse fill="lightblue" stroke="black" cx="276.6" cy="-18" rx="33.95" ry="18"/>
+<text text-anchor="start" x="259.72" y="-13.95" font-family="Times New Roman,serif" font-weight="bold" font-size="14.00">⊥</text>
+<text text-anchor="start" x="275.47" y="-13.95" font-family="Times New Roman,serif" font-size="14.00">:int</text>
+</g>
+<!-- INT_MIN->INT_BOT -->
+<g id="edge8" class="edge">
+<title>INT_MIN->INT_BOT</title>
+<path fill="none" stroke="black" d="M36.33,-87.13C77.31,-75.51 179.45,-46.55 236.48,-30.38"/>
+<polygon fill="black" stroke="black" points="237.13,-33.83 245.79,-27.73 235.22,-27.09 237.13,-33.83"/>
+</g>
+<!-- INT_MIN->INT_MINDOTS -->
+<!-- INT_MINDOTS->INT_BOT -->
+<g id="edge9" class="edge">
+<title>INT_MINDOTS->INT_BOT</title>
+<path fill="none" stroke="black" d="M129.69,-82.59C157.87,-70.39 206.96,-49.14 240.58,-34.59"/>
+<polygon fill="black" stroke="black" points="241.73,-37.91 249.51,-30.72 238.95,-31.48 241.73,-37.91"/>
+</g>
+<!-- INT_MINDOTS->INT_MINUS -->
+<!-- INT_MINUS->INT_BOT -->
+<g id="edge10" class="edge">
+<title>INT_MINUS->INT_BOT</title>
+<path fill="none" stroke="black" d="M210.17,-79.75C221.61,-69.28 238.28,-54.04 252.06,-41.44"/>
+<polygon fill="black" stroke="black" points="254.05,-44.36 259.07,-35.03 249.33,-39.19 254.05,-44.36"/>
+</g>
+<!-- INT_MINUS->INT_ZERO -->
+<!-- INT_ZERO->INT_BOT -->
+<g id="edge11" class="edge">
+<title>INT_ZERO->INT_BOT</title>
+<path fill="none" stroke="black" d="M276.6,-74.82C276.6,-66.77 276.6,-56.98 276.6,-47.86"/>
+<polygon fill="black" stroke="black" points="280.1,-47.98 276.6,-37.98 273.1,-47.98 280.1,-47.98"/>
+</g>
+<!-- INT_ZERO->INT_PLUS -->
+<!-- INT_PLUS->INT_BOT -->
+<g id="edge12" class="edge">
+<title>INT_PLUS->INT_BOT</title>
+<path fill="none" stroke="black" d="M342.55,-80.07C331.3,-69.66 314.75,-54.33 301.04,-41.64"/>
+<polygon fill="black" stroke="black" points="303.78,-39.4 294.06,-35.17 299.02,-44.53 303.78,-39.4"/>
+</g>
+<!-- INT_PLUS->INT_MAXDOTS -->
+<!-- INT_MAXDOTS->INT_BOT -->
+<g id="edge13" class="edge">
+<title>INT_MAXDOTS->INT_BOT</title>
+<path fill="none" stroke="black" d="M421.42,-82.44C393.56,-70.24 345.4,-49.14 312.32,-34.65"/>
+<polygon fill="black" stroke="black" points="314.1,-31.61 303.54,-30.8 311.29,-38.02 314.1,-31.61"/>
+</g>
+<!-- INT_MAXDOTS->INT_MAX -->
+<!-- INT_MAX->INT_BOT -->
+<g id="edge14" class="edge">
+<title>INT_MAX->INT_BOT</title>
+<path fill="none" stroke="black" d="M514.35,-86.41C471.9,-74.38 372.87,-46.3 316.93,-30.44"/>
+<polygon fill="black" stroke="black" points="318.05,-27.12 307.47,-27.76 316.14,-33.85 318.05,-27.12"/>
+</g>
+</g>
+</svg>
diff --git a/docs/lattice_if.gv b/docs/lattice_if.gv new file mode 100644 index 00000000..feb53dfe --- /dev/null +++ b/docs/lattice_if.gv @@ -0,0 +1,71 @@ +digraph Lattice { + compound = true; + // Define nodes + splines=false; + node [shape=circle, style=filled]; + nodesep=0.6; + + TOP [label=<<B>⊤</B >>, fillcolor=black, fontcolor=white]; + BOT [label=<<B>⊥</B>>, fillcolor=black, fontcolor=white]; + + // ---------------------- + // Integers + INT_TOP [label=<<B>⊤</B >:int>, fillcolor=lightblue, shape=oval]; + INT_BOT [label=<<B>⊥</B>:int>, fillcolor=lightblue, shape=oval]; + + INT_MIN [label="-n" , fillcolor=lightblue]; + INT_MINDOTS [label="...", fillcolor=lightblue shape=oval]; + INT_MINUS [label="-1" , fillcolor=lightblue]; + INT_ZERO [label="0" , fillcolor=lightblue]; + INT_PLUS [label="1" , fillcolor=lightblue]; + INT_MAXDOTS [label="...", fillcolor=lightblue, shape=oval]; + INT_MAX [label="+n" , fillcolor=lightblue]; + + 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]; + + // ---------------------- + // Floats + FLT_TOP [label=<<B>⊤</B >:flt>, fillcolor=aqua, shape=oval]; + FLT_BOT [label=<<B>⊥</B>:flt>, fillcolor=aqua, shape=oval]; + + FLT_MINDOTS [label="...", fillcolor=aqua, shape=oval]; + FLT_ZERO [label="0" , fillcolor=aqua]; + FLT_MAXDOTS [label="...", fillcolor=aqua, shape=oval]; + + TOP -> FLT_TOP; + FLT_TOP -> FLT_MINDOTS; + FLT_TOP -> FLT_ZERO; + FLT_TOP -> FLT_MAXDOTS; + FLT_MINDOTS -> FLT_BOT; + FLT_ZERO -> FLT_BOT; + FLT_MAXDOTS -> FLT_BOT; + FLT_BOT -> BOT; + + FLT_MINDOTS -> FLT_ZERO -> FLT_MAXDOTS [style=invis]; + + // Additional customization + {rank=same; TOP} + {rank=same; INT_TOP; FLT_TOP; } + {rank=same; INT_MIN; INT_MINDOTS; INT_MINUS; INT_ZERO; INT_PLUS; INT_MAXDOTS; INT_MAX; + FLT_MINDOTS; FLT_ZERO; FLT_MAXDOTS; + } + {rank=same; INT_BOT; FLT_BOT; } + {rank=same; BOT;} +} diff --git a/docs/lattice_if.svg b/docs/lattice_if.svg new file mode 100644 index 00000000..1f6af94a --- /dev/null +++ b/docs/lattice_if.svg @@ -0,0 +1,265 @@ +<?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="837pt" height="351pt"
+ viewBox="0.00 0.00 836.60 350.81" 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 346.81)">
+<title>Lattice</title>
+<polygon fill="white" stroke="none" points="-4,4 -4,-346.81 832.6,-346.81 832.6,4 -4,4"/>
+<!-- TOP -->
+<g id="node1" class="node">
+<title>TOP</title>
+<ellipse fill="black" stroke="black" cx="451.6" cy="-321.68" rx="21.12" ry="21.12"/>
+<text text-anchor="start" x="443.72" y="-317.26" font-family="Times New Roman,serif" font-weight="bold" font-size="14.00" fill="white">⊤</text>
+</g>
+<!-- INT_TOP -->
+<g id="node3" class="node">
+<title>INT_TOP</title>
+<ellipse fill="lightblue" stroke="black" cx="316.6" cy="-246.56" rx="33.95" ry="18"/>
+<text text-anchor="start" x="299.72" y="-242.51" font-family="Times New Roman,serif" font-weight="bold" font-size="14.00">⊤</text>
+<text text-anchor="start" x="315.47" y="-242.51" font-family="Times New Roman,serif" font-size="14.00">:int</text>
+</g>
+<!-- TOP->INT_TOP -->
+<g id="edge1" class="edge">
+<title>TOP->INT_TOP</title>
+<path fill="none" stroke="black" d="M433.11,-310.67C411.69,-299.07 375.98,-279.72 349.73,-265.51"/>
+<polygon fill="black" stroke="black" points="351.62,-262.55 341.16,-260.86 348.29,-268.71 351.62,-262.55"/>
+</g>
+<!-- FLT_TOP -->
+<g id="node12" class="node">
+<title>FLT_TOP</title>
+<ellipse fill="aqua" stroke="black" cx="669.6" cy="-246.56" rx="32.41" ry="18"/>
+<text text-anchor="start" x="653.85" y="-242.51" font-family="Times New Roman,serif" font-weight="bold" font-size="14.00">⊤</text>
+<text text-anchor="start" x="669.6" y="-242.51" font-family="Times New Roman,serif" font-size="14.00">:flt</text>
+</g>
+<!-- TOP->FLT_TOP -->
+<g id="edge23" class="edge">
+<title>TOP->FLT_TOP</title>
+<path fill="none" stroke="black" d="M471.71,-313.93C508.04,-301.75 585.1,-275.9 631.61,-260.3"/>
+<polygon fill="black" stroke="black" points="632.65,-263.64 641.02,-257.14 630.43,-257.01 632.65,-263.64"/>
+</g>
+<!-- BOT -->
+<g id="node2" class="node">
+<title>BOT</title>
+<ellipse fill="black" stroke="black" cx="451.6" cy="-21.12" rx="21.12" ry="21.12"/>
+<text text-anchor="start" x="443.72" y="-16.7" font-family="Times New Roman,serif" font-weight="bold" font-size="14.00" fill="white">⊥</text>
+</g>
+<!-- INT_MIN -->
+<g id="node5" class="node">
+<title>INT_MIN</title>
+<ellipse fill="lightblue" stroke="black" cx="18.6" cy="-171.4" rx="18.6" ry="18.6"/>
+<text text-anchor="middle" x="18.6" y="-166.35" font-family="Times New Roman,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="M286.1,-238.07C228.49,-223.93 104.36,-193.46 47.78,-179.57"/>
+<polygon fill="black" stroke="black" points="48.79,-176.21 38.24,-177.23 47.12,-183.01 48.79,-176.21"/>
+</g>
+<!-- INT_MINDOTS -->
+<g id="node6" class="node">
+<title>INT_MINDOTS</title>
+<ellipse fill="lightblue" stroke="black" cx="107.6" cy="-171.4" rx="27" ry="18"/>
+<text text-anchor="middle" x="107.6" y="-166.35" font-family="Times New Roman,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="M288.84,-235.84C250.98,-222.59 183.17,-198.86 142.09,-184.48"/>
+<polygon fill="black" stroke="black" points="143.28,-181.19 132.69,-181.19 140.97,-187.79 143.28,-181.19"/>
+</g>
+<!-- INT_MINUS -->
+<g id="node7" class="node">
+<title>INT_MINUS</title>
+<ellipse fill="lightblue" stroke="black" cx="196.6" cy="-171.4" rx="18.6" ry="18.6"/>
+<text text-anchor="middle" x="196.6" y="-166.35" font-family="Times New Roman,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="M294.86,-232.31C274.43,-219.85 243.84,-201.21 222.23,-188.03"/>
+<polygon fill="black" stroke="black" points="224.08,-185.06 213.71,-182.84 220.43,-191.03 224.08,-185.06"/>
+</g>
+<!-- INT_ZERO -->
+<g id="node8" class="node">
+<title>INT_ZERO</title>
+<ellipse fill="lightblue" stroke="black" cx="276.6" cy="-171.4" rx="18" ry="18"/>
+<text text-anchor="middle" x="276.6" y="-166.35" font-family="Times New Roman,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="M307.52,-228.96C302.4,-219.6 295.91,-207.72 290.19,-197.27"/>
+<polygon fill="black" stroke="black" points="293.41,-195.87 285.55,-188.77 287.27,-199.23 293.41,-195.87"/>
+</g>
+<!-- INT_PLUS -->
+<g id="node9" class="node">
+<title>INT_PLUS</title>
+<ellipse fill="lightblue" stroke="black" cx="355.6" cy="-171.4" rx="18" ry="18"/>
+<text text-anchor="middle" x="355.6" y="-166.35" font-family="Times New Roman,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="M325.45,-228.96C330.32,-219.82 336.47,-208.29 341.94,-198.02"/>
+<polygon fill="black" stroke="black" points="344.99,-199.74 346.6,-189.27 338.81,-196.45 344.99,-199.74"/>
+</g>
+<!-- INT_MAXDOTS -->
+<g id="node10" class="node">
+<title>INT_MAXDOTS</title>
+<ellipse fill="lightblue" stroke="black" cx="443.6" cy="-171.4" rx="27" ry="18"/>
+<text text-anchor="middle" x="443.6" y="-166.35" font-family="Times New Roman,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="M339.01,-232.65C359.76,-220.7 390.76,-202.84 413.63,-189.66"/>
+<polygon fill="black" stroke="black" points="415.27,-192.76 422.19,-184.73 411.77,-186.69 415.27,-192.76"/>
+</g>
+<!-- INT_MAX -->
+<g id="node11" class="node">
+<title>INT_MAX</title>
+<ellipse fill="lightblue" stroke="black" cx="534.6" cy="-171.4" rx="21.15" ry="21.15"/>
+<text text-anchor="middle" x="534.6" y="-166.35" font-family="Times New Roman,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="M344.65,-236.14C385.52,-222.43 461.18,-197.04 503.63,-182.79"/>
+<polygon fill="black" stroke="black" points="504.62,-186.15 512.98,-179.66 502.39,-179.52 504.62,-186.15"/>
+</g>
+<!-- INT_BOT -->
+<g id="node4" class="node">
+<title>INT_BOT</title>
+<ellipse fill="lightblue" stroke="black" cx="316.6" cy="-96.25" rx="33.95" ry="18"/>
+<text text-anchor="start" x="299.72" y="-92.2" font-family="Times New Roman,serif" font-weight="bold" font-size="14.00">⊥</text>
+<text text-anchor="start" x="315.47" y="-92.2" font-family="Times New Roman,serif" font-size="14.00">:int</text>
+</g>
+<!-- INT_BOT->BOT -->
+<g id="edge16" class="edge">
+<title>INT_BOT->BOT</title>
+<path fill="none" stroke="black" d="M339.8,-82.68C362.89,-70.17 398.36,-50.96 423.13,-37.54"/>
+<polygon fill="black" stroke="black" points="424.57,-40.74 431.7,-32.9 421.24,-34.59 424.57,-40.74"/>
+</g>
+<!-- INT_MIN->INT_BOT -->
+<g id="edge9" class="edge">
+<title>INT_MIN->INT_BOT</title>
+<path fill="none" stroke="black" d="M36.79,-165.94C83.64,-154.44 209.35,-123.58 275.15,-107.42"/>
+<polygon fill="black" stroke="black" points="275.98,-110.82 284.85,-105.04 274.31,-104.03 275.98,-110.82"/>
+</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="M131.16,-162.15C166.91,-149.64 235.21,-125.73 278.2,-110.69"/>
+<polygon fill="black" stroke="black" points="279.1,-114.08 287.38,-107.47 276.79,-107.47 279.1,-114.08"/>
+</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="M212.28,-160.84C230.74,-149.59 261.83,-130.63 285.28,-116.34"/>
+<polygon fill="black" stroke="black" points="286.79,-119.51 293.51,-111.32 283.15,-113.54 286.79,-119.51"/>
+</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="M284.88,-155.25C289.83,-146.21 296.24,-134.47 302.01,-123.92"/>
+<polygon fill="black" stroke="black" points="305.03,-125.7 306.76,-115.24 298.89,-122.34 305.03,-125.7"/>
+</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="M347.32,-154.89C342.53,-145.89 336.36,-134.32 330.81,-123.9"/>
+<polygon fill="black" stroke="black" points="334.04,-122.53 326.25,-115.35 327.86,-125.82 334.04,-122.53"/>
+</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="M423.47,-158.81C403.37,-147.23 372.15,-129.25 348.63,-115.7"/>
+<polygon fill="black" stroke="black" points="350.48,-112.73 340.07,-110.77 346.99,-118.79 350.48,-112.73"/>
+</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="M514.48,-163.65C478.45,-151.56 402.33,-126.02 355.71,-110.37"/>
+<polygon fill="black" stroke="black" points="356.84,-107.06 346.25,-107.2 354.62,-113.7 356.84,-107.06"/>
+</g>
+<!-- FLT_MINDOTS -->
+<g id="node14" class="node">
+<title>FLT_MINDOTS</title>
+<ellipse fill="aqua" stroke="black" cx="625.6" cy="-171.4" rx="27" ry="18"/>
+<text text-anchor="middle" x="625.6" y="-166.35" font-family="Times New Roman,serif" font-size="14.00">...</text>
+</g>
+<!-- FLT_TOP->FLT_MINDOTS -->
+<g id="edge24" class="edge">
+<title>FLT_TOP->FLT_MINDOTS</title>
+<path fill="none" stroke="black" d="M659.61,-228.96C654.17,-219.92 647.32,-208.52 641.19,-198.34"/>
+<polygon fill="black" stroke="black" points="644.32,-196.75 636.17,-189.98 638.32,-200.36 644.32,-196.75"/>
+</g>
+<!-- FLT_ZERO -->
+<g id="node15" class="node">
+<title>FLT_ZERO</title>
+<ellipse fill="aqua" stroke="black" cx="713.6" cy="-171.4" rx="18" ry="18"/>
+<text text-anchor="middle" x="713.6" y="-166.35" font-family="Times New Roman,serif" font-size="14.00">0</text>
+</g>
+<!-- FLT_TOP->FLT_ZERO -->
+<g id="edge25" class="edge">
+<title>FLT_TOP->FLT_ZERO</title>
+<path fill="none" stroke="black" d="M679.58,-228.96C685.21,-219.6 692.35,-207.72 698.64,-197.27"/>
+<polygon fill="black" stroke="black" points="701.61,-199.11 703.77,-188.74 695.62,-195.51 701.61,-199.11"/>
+</g>
+<!-- FLT_MAXDOTS -->
+<g id="node16" class="node">
+<title>FLT_MAXDOTS</title>
+<ellipse fill="aqua" stroke="black" cx="801.6" cy="-171.4" rx="27" ry="18"/>
+<text text-anchor="middle" x="801.6" y="-166.35" font-family="Times New Roman,serif" font-size="14.00">...</text>
+</g>
+<!-- FLT_TOP->FLT_MAXDOTS -->
+<g id="edge26" class="edge">
+<title>FLT_TOP->FLT_MAXDOTS</title>
+<path fill="none" stroke="black" d="M691.99,-233.15C713.77,-221.07 747.03,-202.64 771.2,-189.25"/>
+<polygon fill="black" stroke="black" points="772.89,-192.31 779.94,-184.4 769.5,-186.19 772.89,-192.31"/>
+</g>
+<!-- FLT_BOT -->
+<g id="node13" class="node">
+<title>FLT_BOT</title>
+<ellipse fill="aqua" stroke="black" cx="669.6" cy="-96.25" rx="32.41" ry="18"/>
+<text text-anchor="start" x="653.85" y="-92.2" font-family="Times New Roman,serif" font-weight="bold" font-size="14.00">⊥</text>
+<text text-anchor="start" x="669.6" y="-92.2" font-family="Times New Roman,serif" font-size="14.00">:flt</text>
+</g>
+<!-- FLT_BOT->BOT -->
+<g id="edge30" class="edge">
+<title>FLT_BOT->BOT</title>
+<path fill="none" stroke="black" d="M642.43,-86.13C601.76,-72.49 525.27,-46.84 482.51,-32.49"/>
+<polygon fill="black" stroke="black" points="483.69,-29.2 473.09,-29.33 481.46,-35.83 483.69,-29.2"/>
+</g>
+<!-- FLT_MINDOTS->FLT_BOT -->
+<g id="edge27" class="edge">
+<title>FLT_MINDOTS->FLT_BOT</title>
+<path fill="none" stroke="black" d="M635.36,-154.17C640.79,-145.14 647.68,-133.68 653.85,-123.42"/>
+<polygon fill="black" stroke="black" points="656.77,-125.36 658.93,-114.99 650.77,-121.75 656.77,-125.36"/>
+</g>
+<!-- FLT_MINDOTS->FLT_ZERO -->
+<!-- FLT_ZERO->FLT_BOT -->
+<g id="edge28" class="edge">
+<title>FLT_ZERO->FLT_BOT</title>
+<path fill="none" stroke="black" d="M704.69,-155.6C699.17,-146.42 691.93,-134.37 685.45,-123.61"/>
+<polygon fill="black" stroke="black" points="688.49,-121.88 680.34,-115.11 682.5,-125.49 688.49,-121.88"/>
+</g>
+<!-- FLT_ZERO->FLT_MAXDOTS -->
+<!-- FLT_MAXDOTS->FLT_BOT -->
+<g id="edge29" class="edge">
+<title>FLT_MAXDOTS->FLT_BOT</title>
+<path fill="none" stroke="black" d="M781.26,-159.13C760.12,-147.42 726.74,-128.92 701.97,-115.19"/>
+<polygon fill="black" stroke="black" points="703.71,-112.15 693.27,-110.37 700.32,-118.28 703.71,-112.15"/>
+</g>
+</g>
+</svg>
|
