Adjust structure

chapters/4-Annotation-System.typ

@@ -258,46 +258,85 @@ However, these rules are not sufficient to type a method call statement since pa
 == Paths
 <cap:paths>
 
+=== Root
+
+#display-rules(
+  Root-Base, Root-Rec,
+)
+
+*TODO: Spiega*
+
+=== Get
+
+#display-rules(
+  Get-Var, Get-Path,
+)
+
 - $Lub{alpha_0 beta_0, ..., alpha_n beta_n}$ identifies the least upper bound of the annotations based on the lattice in @annotation-lattice.
 - Note that even if $p.f$ is annotated as unique in the class declaration, $Delta(p.f)$ can be shared (or $top$) if $Delta(p) = shared$ (or $top$)
 - Note that fields of a borrowed parameter are borrowed too and they need to be treated carefully in order to avoid unsoundness. Specifically, borrowed fields:
   - Can be passed as arguments to other functions (if relation rules are respected).
   - Have to become `T` after being read (even if shared).
   - Can only be reassigned with a `unique`.
 - Note that $(Delta(p) = alpha beta) => (Delta inangle(root(p)) = alpha' beta')$ i.e. the root is present in the context.
-- $Delta tr std(p, alpha beta)$ means that paths rooted in $p$ have the right permissions when passing $p$ where $alpha beta$ is expected. To understand better why these rules are necessary look at the example in /*@path-permissions*/.
-- Note that in the rule "Std-Rec-2" the premise $(x : alpha beta) (p') = alpha'' beta''$ means that the evaluation of $p'$ in a context in which there is only $x : alpha beta$ is $alpha'' beta''$
+
+*TODO: Spiega e riorganizza*
+
+=== Standard Form
 
 #display-rules(
-  Root-Base, Root-Rec,
-  Get-Var, Get-Path,
   Std-Empty, Std-Rec-1,
   Std-Rec-2, "",
 )
 
+*TODO:* fondamentale per method-modularity
+
+- $Delta tr std(p, alpha beta)$ means that paths rooted in $p$ have the right permissions when passing $p$ where $alpha beta$ is expected. To understand better why these rules are necessary look at the example in
+- Note that in the rule "Std-Rec-2" the premise $(x : alpha beta) (p') = alpha'' beta''$ means that the evaluation of $p'$ in a context in which there is only $x : alpha beta$ is $alpha'' beta''$
+
+
+
 == Unification
 
+=== Pointwise LUB
+
+#display-rules(
+  Ctx-Lub-Empty, Ctx-Lub-Sym,
+  Ctx-Lub-1, "",
+  Ctx-Lub-2, "",
+  Ctx-Lub-3, "",
+)
+
+*TODO: sistema descrizione*
 - $Delta_1 lub Delta_2$ is the pointwise lub of $Delta_1$ and $Delta_2$.
   - If a variable $x$ is present in only one context, it will be annotated with $top$ in $Delta_1 lub Delta_2$.
   - If a path $p.f$ is missing in one of the two contexts, we can just consider the annotation in the class declaration.
+
+=== Local declarations removal
+
+#display-rules(
+  Remove-Locals-Base, "",
+  Remove-Locals-Keep, "",
+  Remove-Locals-Discard, "",
+)
+
+*TODO: sistema descrizione*
 - $Delta triangle.filled.small.l Delta_1$ is used to maintain the correct context when exiting a scope.
   - $Delta$ represents the resulting context of the inner scope.
   - $Delta_1$ represents the context at the beginning of the scope.
   - The result of the operation is a context where paths rooted in variable locally declared inside the scope are removed.
-- $unify(Delta, Delta_1, Delta_2)$ means that we want to unify $Delta_1$ and $Delta_2$ starting from a parent environment $Delta$.
-  - A path $p$ contained in $Delta_1$ or $Delta_2$ such that $root(p) = x$ is not contained $Delta$ will not be included in the unfication.
-  - The annotation of variables contained in the unfication is the least upper bound of the annotation in $Delta_1$ and $Delta_2$.
+
+=== Unify
 
 #display-rules(
-  Ctx-Lub-Empty, Ctx-Lub-Sym,
-  Ctx-Lub-1, "",
-  Ctx-Lub-2, "",
-  Ctx-Lub-3, "",
-  Remove-Locals-Base, Remove-Locals-Keep,
-  Remove-Locals-Discard, "",
   Unify, ""
 )
 
+*TODO: sistema descrizione*
+- $unify(Delta, Delta_1, Delta_2)$ means that we want to unify $Delta_1$ and $Delta_2$ starting from a parent environment $Delta$.
+  - A path $p$ contained in $Delta_1$ or $Delta_2$ such that $root(p) = x$ is not contained $Delta$ will not be included in the unfication.
+  - The annotation of variables contained in the unfication is the least upper bound of the annotation in $Delta_1$ and $Delta_2$.
+
 == Normalization
 
 - Normalization takes a list of annotated $p$ and retruns a list in which duplicates are substituted with the least upper bound.
@@ -319,7 +358,8 @@ fun use_f(x: unique) {
 
 == Statements Typing
 
-TODO: How to read typing rules
+*TODO: How to read typing rules*
+*TODO: adjust program definition*
 
 $"Program" ::= overline(CL) times overline(M)$
 where:

chapters/rules/base.typ

@@ -174,11 +174,14 @@
   rule(n:2, label: "Std-Rec-1", $p' : alpha beta, Delta tr std(p, alpha beta)$),
 )
 
-#let Std-Rec-2 = prooftree(
-  axiom($p subset.sq p'$),
-  axiom($root(p) = x$),
-  axiom($(x : alpha beta) (p') = alpha'' beta''$),
-  axiom($alpha' beta' rel alpha'' beta''$),
-  axiom($Delta tr std(p, alpha beta)$),
-  rule(n:5, label: "Std-Rec-2", $p' : alpha' beta', Delta tr std(p, alpha beta)$),
-)
+#let Std-Rec-2 = {
+  let a1 = $p subset.sq p'$
+  let a2 = $root(p) = x$
+  let a3 = $(x : alpha beta) (p') = alpha'' beta''$
+  let a4 = $alpha' beta' rel alpha'' beta''$
+  let a5 = $Delta tr std(p, alpha beta)$
+  prooftree(
+    stacked-axiom((a1, a2), (a3, a4, a5)),
+    rule(label: "Std-Rec-2", $p' : alpha' beta', Delta tr std(p, alpha beta)$),
+  )
+}

chapters/rules/unification.typ

@@ -57,27 +57,34 @@
   rule(label: "Ctx-Lub-Sym", $Delta_1 lub Delta_2 = Delta_2 lub Delta_1$),
 )
 
-#let Ctx-Lub-1 = prooftree(
-  axiom($Delta_2 inangle(p.f) = alpha'' beta''$),
-  axiom($Delta_2 without p.f = Delta'_2$),
-  axiom($Delta_1 lub Delta'_2 = Delta'$),
-  axiom($Lub{alpha beta, alpha'' beta''} = alpha' beta'$),
-  rule(n:4, label: "Ctx-Lub-1", $(p.f : alpha beta, Delta_1) lub Delta_2 = p.f : alpha' beta', Delta'$),
-)
+#let Ctx-Lub-1 = {
+  let a1 = $Delta_2 inangle(p.f) = alpha'' beta''$
+  let a2 = $Delta_2 without p.f = Delta'_2$
+  let a3 = $Delta_1 lub Delta'_2 = Delta'$
+  let a4 = $Lub{alpha beta, alpha'' beta''} = alpha' beta'$
+  prooftree(
+    stacked-axiom((a1, a2), (a3, a4)),
+    rule(label: "Ctx-Lub-1", $(p.f : alpha beta, Delta_1) lub Delta_2 = p.f : alpha' beta', Delta'$),
+  )
+}
 
 #let Ctx-Lub-2 = prooftree(
   axiom($x in.not Delta_2$),
   axiom($Delta_1 lub Delta_2 = Delta'$),
   rule(n:2, label: "Ctx-Lub-2", $(x : alpha beta, Delta_1) lub Delta_2 = x : top, Delta'$),
 )
 
-#let Ctx-Lub-3 = prooftree(
-  axiom($Delta_2 inangle(x) = alpha'' beta''$),
-  axiom($Delta_2 without x = Delta'_2$),
-  axiom($Delta_1 lub Delta'_2 = Delta'$),
-  axiom($Lub{alpha beta, alpha'' beta''} = alpha' beta'$),
-  rule(n:4, label: "Ctx-Lub-3", $(x : alpha beta, Delta_1) lub Delta_2 = x : alpha' beta', Delta'$),
-)
+#let Ctx-Lub-3 = {
+  let a1 = $Delta_2 inangle(x) = alpha'' beta''$
+  let a2 = $Delta_2 without x = Delta'_2$
+  let a3 = $Delta_1 lub Delta'_2 = Delta'$
+  let a4 = $Lub{alpha beta, alpha'' beta''} = alpha' beta'$
+  prooftree(
+    stacked-axiom((a1, a2), (a3, a4)),
+    rule(label: "Ctx-Lub-3", $(x : alpha beta, Delta_1) lub Delta_2 = x : alpha' beta', Delta'$),
+  )
+}
+
 
 #let Remove-Locals-Base = prooftree(
   axiom($$),
@@ -111,8 +118,11 @@
   rule(label: "N-Empty", $norm(dot) = dot$)
 )
 
-#let N-Rec = prooftree(
-  axiom($Lub(alpha_i beta_i | p_i = p_0 and 0 <= i <= n) = ablub$),
-  axiom($norm(p_i: alpha_i beta_i | p_i != p_0 and 0 <= i <= n) = p'_0 : alpha'_0 beta'_0, ..., p'_m : alpha'_m beta'_m$),
-  rule(n:2, label: "N-rec", $norm(p_0\: alpha_0 beta_0, ..., p_n\: alpha_n beta_n) = p_0 : ablub, p'_0 : alpha'_0 beta'_0, ..., p'_m : alpha'_m beta'_m$)
-)
+#let N-Rec = {
+  let a1 = $Lub(alpha_i beta_i | p_i = p_0 and 0 <= i <= n) = ablub$
+  let a2 = $norm(p_i: alpha_i beta_i | p_i != p_0 and 0 <= i <= n) = p'_0 : alpha'_0 beta'_0, ..., p'_m : alpha'_m beta'_m$
+  prooftree(
+    stacked-axiom((a1,), (a2,)),
+    rule(label: "N-rec", $norm(p_0\: alpha_0 beta_0, ..., p_n\: alpha_n beta_n) = p_0 : ablub, p'_0 : alpha'_0 beta'_0, ..., p'_m : alpha'_m beta'_m$)
+  )
+}