From cbbadb81207199f340ff408485bb37cd1bbeb0c6 Mon Sep 17 00:00:00 2001 From: Cliff Click Date: Tue, 12 Aug 2025 15:54:26 -0700 Subject: More lattices for main --- TypeAnalysis.md | Bin 5852 -> 6680 bytes chapter12/docs/lattice.gv | 2 +- docs/Makefile | 12 +++ docs/lattice_i.gv | 40 +++++++ docs/lattice_i.svg | 159 ++++++++++++++++++++++++++++ docs/lattice_if.gv | 71 +++++++++++++ docs/lattice_if.svg | 265 ++++++++++++++++++++++++++++++++++++++++++++++ 7 files changed, 548 insertions(+), 1 deletion(-) create mode 100644 docs/Makefile create mode 100644 docs/lattice_i.gv create mode 100644 docs/lattice_i.svg create mode 100644 docs/lattice_if.gv create mode 100644 docs/lattice_if.svg diff --git a/TypeAnalysis.md b/TypeAnalysis.md index 3a857d88..a260710b 100644 Binary files a/TypeAnalysis.md and b/TypeAnalysis.md differ 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=<⊤:flt>, fillcolor=aqua, shape=oval]; FLT_BOT [label=<⊥: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=<⊤:int>, fillcolor=lightblue, shape=oval]; + INT_BOT [label=<⊥: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 @@ + + + + + + +Lattice + + + +INT_TOP + +⊤ +:int + + + +INT_MIN + +-n + + + +INT_TOP->INT_MIN + + + + + +INT_MINDOTS + +... + + + +INT_TOP->INT_MINDOTS + + + + + +INT_MINUS + +-1 + + + +INT_TOP->INT_MINUS + + + + + +INT_ZERO + +0 + + + +INT_TOP->INT_ZERO + + + + + +INT_PLUS + +1 + + + +INT_TOP->INT_PLUS + + + + + +INT_MAXDOTS + +... + + + +INT_TOP->INT_MAXDOTS + + + + + +INT_MAX + ++n + + + +INT_TOP->INT_MAX + + + + + +INT_BOT + +⊥ +:int + + + +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 + + + + + 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=<⊤>, fillcolor=black, fontcolor=white]; + BOT [label=<⊥>, fillcolor=black, fontcolor=white]; + + // ---------------------- + // Integers + INT_TOP [label=<⊤:int>, fillcolor=lightblue, shape=oval]; + INT_BOT [label=<⊥: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=<⊤:flt>, fillcolor=aqua, shape=oval]; + FLT_BOT [label=<⊥: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 @@ + + + + + + +Lattice + + + +TOP + +⊤ + + + +INT_TOP + +⊤ +:int + + + +TOP->INT_TOP + + + + + +FLT_TOP + +⊤ +:flt + + + +TOP->FLT_TOP + + + + + +BOT + +⊥ + + + +INT_MIN + +-n + + + +INT_TOP->INT_MIN + + + + + +INT_MINDOTS + +... + + + +INT_TOP->INT_MINDOTS + + + + + +INT_MINUS + +-1 + + + +INT_TOP->INT_MINUS + + + + + +INT_ZERO + +0 + + + +INT_TOP->INT_ZERO + + + + + +INT_PLUS + +1 + + + +INT_TOP->INT_PLUS + + + + + +INT_MAXDOTS + +... + + + +INT_TOP->INT_MAXDOTS + + + + + +INT_MAX + ++n + + + +INT_TOP->INT_MAX + + + + + +INT_BOT + +⊥ +:int + + + +INT_BOT->BOT + + + + + +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 + + + + + +FLT_MINDOTS + +... + + + +FLT_TOP->FLT_MINDOTS + + + + + +FLT_ZERO + +0 + + + +FLT_TOP->FLT_ZERO + + + + + +FLT_MAXDOTS + +... + + + +FLT_TOP->FLT_MAXDOTS + + + + + +FLT_BOT + +⊥ +:flt + + + +FLT_BOT->BOT + + + + + +FLT_MINDOTS->FLT_BOT + + + + + + +FLT_ZERO->FLT_BOT + + + + + + +FLT_MAXDOTS->FLT_BOT + + + + + -- cgit v1.2.3