summaryrefslogtreecommitdiff
path: root/docs/chapter06/lattice.gv
diff options
context:
space:
mode:
Diffstat (limited to 'docs/chapter06/lattice.gv')
-rw-r--r--docs/chapter06/lattice.gv97
1 files changed, 97 insertions, 0 deletions
diff --git a/docs/chapter06/lattice.gv b/docs/chapter06/lattice.gv
new file mode 100644
index 00000000..e5cc59be
--- /dev/null
+++ b/docs/chapter06/lattice.gv
@@ -0,0 +1,97 @@
+digraph Lattice {
+ // Define nodes
+ splines=false;
+ node [shape=circle, style=filled, fillcolor=lightblue];
+ nodesep=0.6;
+
+ TOP [label=<<B>⊤</B >>, fillcolor=black, fontcolor=white];
+ BOT [label=<<B>⊥</B>>, fillcolor=black, fontcolor=white];
+
+ // ----------------------
+ // Control
+ XCTRL [label=<<B>⊤</B >:ctrl>, fillcolor=yellow, shape=oval];
+ CTRL [label=<<B>⊥</B>:ctrl>, fillcolor=yellow, shape=oval];
+
+ TOP -> XCTRL;
+ XCTRL -> CTRL;
+ CTRL -> BOT;
+
+ // ----------------------
+ // 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];
+
+ // ----------------------
+ // Tuples
+
+ TUPLE_TOP [label=<<B>⊤</B >:tuple>, fillcolor=pink, shape=oval];
+ TUPLE_BOT [label=<<B>⊥</B>:tuple>, fillcolor=pink, shape=oval];
+
+ TUPLE1 [shape=none, fillcolor=none, label=<
+ <TABLE BORDER="0" CELLBORDER="1" CELLSPACING="0">
+ <TH><TD BGCOLOR="pink">tuple</TD></TH>
+ <TR><TD BGCOLOR="black" ><FONT color="white">type</FONT></TD></TR>
+ </TABLE>
+ >];
+ TUPLE2 [shape=none, fillcolor=none, label=<
+ <TABLE BORDER="0" CELLBORDER="1" CELLSPACING="0">
+ <TH><TD BGCOLOR="pink">tuple</TD></TH>
+ <TR><TD BGCOLOR="black" ><FONT color="white">type</FONT></TD></TR>
+ <TR><TD BGCOLOR="black" ><FONT color="white">type</FONT></TD></TR>
+ </TABLE>
+ >];
+ TUPLEN [shape=none, fillcolor=none, label=<
+ <TABLE BORDER="0" CELLBORDER="1" CELLSPACING="0">
+ <TH><TD BGCOLOR="pink">tuple</TD></TH>
+ <TR><TD BGCOLOR="black" ><FONT color="white">type</FONT></TD></TR>
+ <TR><TD BGCOLOR="black" ><FONT color="white">...</FONT></TD></TR>
+ <TR><TD BGCOLOR="black" ><FONT color="white">type</FONT></TD></TR>
+ </TABLE>
+ >];
+
+
+ TOP -> TUPLE_TOP;
+ TUPLE_TOP -> TUPLE1;
+ TUPLE_TOP -> TUPLE2;
+ TUPLE_TOP -> TUPLEN;
+ TUPLE1 -> TUPLE_BOT;
+ TUPLE2 -> TUPLE_BOT;
+ TUPLEN -> TUPLE_BOT;
+ TUPLE_BOT -> BOT;
+
+ // Additional customization
+ {rank=same; TOP}
+ {rank=same; XCTRL; INT_TOP; TUPLE_TOP}
+ {rank=same;
+ INT_MIN; INT_MINDOTS; INT_MINUS; INT_ZERO; INT_PLUS; INT_MAXDOTS; INT_MAX;
+ }
+ {rank=same; CTRL; INT_BOT, TUPLE_BOT}
+ {rank=same; BOT;}
+}