diff options
| author | Cliff Click <cliffc@acm.org> | 2025-08-12 15:54:26 -0700 |
|---|---|---|
| committer | Cliff Click <cliffc@acm.org> | 2025-08-12 15:54:26 -0700 |
| commit | cbbadb81207199f340ff408485bb37cd1bbeb0c6 (patch) | |
| tree | fac96691cc99d127bf6c78f15c763656a8798274 /docs/lattice_if.gv | |
| parent | 6aa254dd46bede60db3350ecdb9173171f110a12 (diff) | |
| download | Simple-cbbadb81207199f340ff408485bb37cd1bbeb0c6.tar.gz Simple-cbbadb81207199f340ff408485bb37cd1bbeb0c6.zip | |
More lattices for main
Diffstat (limited to 'docs/lattice_if.gv')
| -rw-r--r-- | docs/lattice_if.gv | 71 |
1 files changed, 71 insertions, 0 deletions
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;} +} |