From 3ba6686fc991998a0a420709dfb0012bbddf77ab Mon Sep 17 00:00:00 2001 From: Cliff Click Date: Tue, 29 Sep 2026 12:21:46 -0700 Subject: Backport lazy memory splits to ch10, split into ch10a and b --- chapter10a/docs/lattice.svg | 726 +++++++++++++++++++++++++------------------- 1 file changed, 415 insertions(+), 311 deletions(-) (limited to 'chapter10a/docs/lattice.svg') diff --git a/chapter10a/docs/lattice.svg b/chapter10a/docs/lattice.svg index aa296366..24c0de8c 100644 --- a/chapter10a/docs/lattice.svg +++ b/chapter10a/docs/lattice.svg @@ -4,463 +4,567 @@ - - + + Lattice - + + +cluster_control + +Control + + +cluster_integer + +Integer + + +cluster_pointer + +Pointer = nullability × struct type + + +cluster_struct + +Struct +named collection of named scalar types + + +cluster_memory + +Memory + + +cluster_tuple + +Tuple +collection of types + TOP - -⊤ + +⊤ XCTRL - -⊤ -:ctrl + +⊤:ctrl - + TOP->XCTRL - - + + INT_TOP - -⊤ -:int + +⊤:int - + TOP->INT_TOP - - + + - + -PTR - - - -*ptr - - -struct - - - -TOP->PTR - - +PTR_TOP + +⊤:ptr +[*⊤:struct] + + + +TOP->PTR_TOP + + - + STRUCT_TOP - -⊤ -:struct + +⊤:struct +[struct top] - + TOP->STRUCT_TOP - - + + - + MEM_TOP - -⊤ -:mem + +⊤:mem - + TOP->MEM_TOP - - + + - + TUPLE_TOP - -⊤ -:tuple + +⊤:tuple - + TOP->TUPLE_TOP - - + + BOT - -⊥ + +⊥ CTRL - -⊥ -:ctrl + +⊥:ctrl - + XCTRL->CTRL - - + + + - + CTRL->BOT - - + + - + -INT_MINDOTS - -... +INT_NEG + +… −2, −1 - - -INT_TOP->INT_MINDOTS - - + + +INT_TOP->INT_NEG + + INT_ZERO - -0 + +0 - + INT_TOP->INT_ZERO - - + + - + -INT_MAXDOTS - -... +INT_POS + +1, 2, … - - -INT_TOP->INT_MAXDOTS - - + + +INT_TOP->INT_POS + + + INT_BOT - -⊥ -:int + +⊥:int - + INT_BOT->BOT - - + + - - -INT_MINDOTS->INT_BOT - - + + +INT_NEG->INT_BOT + + - + - + INT_ZERO->INT_BOT - - + + + + + + +INT_POS->INT_BOT + + - - - -INT_MAXDOTS->INT_BOT - - + + +PTR_NULL + +null +[*⊤:struct?] - - -PTR0 - - - -*ptr? - - -struct - - - -PTR->PTR0 - - - - + -PTR0->BOT - - +PTR_TOP->PTR_NULL + + - + +PTR_PERSON + +*Person + + + +PTR_TOP->PTR_PERSON + + + + + +PTR_S1 + +*s1 + + + +PTR_TOP->PTR_S1 + + + + + +PTR_MORE + +*s2, … + + + +PTR_TOP->PTR_MORE + + + + + + +PTR_BOT + +⊥:ptr +[*⊥:struct?] + + + +PTR_BOT->BOT + + + + + +PTR_PERSON_NIL + +*Person? + + + +PTR_NULL->PTR_PERSON_NIL + + + + + +PTR_S1_NIL + +*s1? + + + +PTR_NULL->PTR_S1_NIL + + + + + +PTR_MORE_NIL + +*s2?, … + + + +PTR_NULL->PTR_MORE_NIL + + + + + +PTR_ANY + +*⊥:struct +[ptr any struct] + + + +PTR_ANY->PTR_BOT + + + + + + +PTR_PERSON->PTR_ANY + + + + + + +PTR_PERSON->PTR_PERSON_NIL + + + + + +PTR_S1->PTR_ANY + + + + + + +PTR_S1->PTR_S1_NIL + + + + + + +PTR_MORE->PTR_ANY + + + + + +PTR_MORE->PTR_MORE_NIL + + + + + +PTR_PERSON_NIL->PTR_BOT + + + + + + +PTR_S1_NIL->PTR_BOT + + + + + + +PTR_MORE_NIL->PTR_BOT + + + + + +STRUCT_PERSON + +Person +age: int + + + +STRUCT_TOP->STRUCT_PERSON + + + + + STRUCT_S1 - - - -field - - - - - - - - -int/ptr + +s1 +x: int - + STRUCT_TOP->STRUCT_S1 - - + + - + STRUCT_S2 - - - -field - - - - - - - - -int/ptr - - -field - - - - - - - - -int/ptr + +s2 +x: int, y: int - + STRUCT_TOP->STRUCT_S2 - - - - - -STRUCT_SN - - - -field - - - - - - - - -int/ptr - - -...   - - - - - - - - -int/ptr - - -field - - - - - - - - -int/ptr - - - -STRUCT_TOP->STRUCT_SN - - - + + + + + +STRUCT_MORE + +… + + + +STRUCT_TOP->STRUCT_MORE + + + + - + STRUCT_BOT - -⊥ -:struct + +⊥:struct +[struct bottom] - + STRUCT_BOT->BOT - - + + + + +STRUCT_PERSON->STRUCT_BOT + + + + - + STRUCT_S1->STRUCT_BOT - - + + - + STRUCT_S2->STRUCT_BOT - - + + - - - -STRUCT_SN->STRUCT_BOT - - + + + +STRUCT_MORE->STRUCT_BOT + + - + MEM_BOT - -⊥ -:mem + +⊥:mem - + MEM_TOP->MEM_BOT - - + + + - + MEM_BOT->BOT - - + + - + TUPLE1 - - - -Tuple - - -type + +(type) - + TUPLE_TOP->TUPLE1 - - + + - + TUPLE2 - - - -Tuple - - -type - - -type + +(type, type) - + TUPLE_TOP->TUPLE2 - - + + - + TUPLEN - - - -Tuple - - -type - - -... - - -type + +(type, …) - + TUPLE_TOP->TUPLEN - - + + - + TUPLE_BOT - -⊥ -:tuple + +⊥:tuple - + TUPLE_BOT->BOT - - + + - + TUPLE1->TUPLE_BOT - - + + + - + TUPLE2->TUPLE_BOT - - + + + - + TUPLEN->TUPLE_BOT - - + + -- cgit v1.2.3