From 80c32e224153b9aa76b43d3010c0ac9deb1987b9 Mon Sep 17 00:00:00 2001
From: francescoo22 <francesco.protopapa22@gmail.com>
Date: Fri, 5 Jul 2024 13:52:31 +0200
Subject: [PATCH] Fix trees length

---
 chapters/4-Annotation-System.typ | 21 ++++++++++++---------
 chapters/rules/statements.typ    | 25 ++++++++++++++-----------
 2 files changed, 26 insertions(+), 20 deletions(-)

diff --git a/chapters/4-Annotation-System.typ b/chapters/4-Annotation-System.typ
index 851cf83..628df79 100644
--- a/chapters/4-Annotation-System.typ
+++ b/chapters/4-Annotation-System.typ
@@ -5,6 +5,7 @@
 #import "rules/statements.typ": *
 
 #pagebreak(to:"odd")
+// TODO: coerenza nei nomi delle regole (nel modo in cui abbrevio unique, shared e borrowed)
 = Annotation System
 
 This chapter describes an annotation system for controlling aliasing within a subset of the Kotlin language.
@@ -220,6 +221,9 @@ $ f(){begin_f; var x; ...} $
 
 === Assigning null
 
+// TODO: precondizione per p in context???
+// basta essere coerenti, o sempre o mai
+
 #display-rules(Assign-Null, "")
 
 The definition of unique tells us that a reference is unique when it is `null` or is the sole accessible reference pointing to the object that is pointing. Given that, we can safely consider unique a path $p$ after assigning `null` to it. Moreover, all sup-paths of $p$ are removed from the context after the assignment.
@@ -253,24 +257,23 @@ These rules are straightforward, but necessary to define how to type a sequence
 
 === Call
 
-#display-rules(Call)
+#display-rules(Call, "")
+
+=== Assign call
+
+#display-rules(Assign-Call, "")
 
 === Assign unique
 
-#display-rules(Assign-Unique)
+#display-rules(Assign-Unique, "")
 
 === Assign shared
 
-#display-rules(Assign-Shared)
+#display-rules(Assign-Shared, "")
 
 === Assign boorowed field
 
-#display-rules(Assign-Borrowed-Field)
-
-=== Assign call
-
-#display-rules(Assign-Call)
-// regola per la call prima di assign call?
+#display-rules(Assign-Borrowed-Field, "")
 
 === If
 
diff --git a/chapters/rules/statements.typ b/chapters/rules/statements.typ
index acf8b6c..00047dd 100644
--- a/chapters/rules/statements.typ
+++ b/chapters/rules/statements.typ
@@ -57,11 +57,10 @@
   
   prooftree(
     stacked-axiom(
-      (a0, a1, a2, a3, a4),
-      (a5, a6, a7)
+      (a0, a1, a2), (a3, a4, a5), (a6, a7)
     ),
     rule(
-      label: "Assign-Borrowed-Field",
+      label: $"Assign-"borrowed"-Field"$,
       $mid(p = p'.f)', p.overline(f_0) : alpha_0 beta_0, ..., p.overline(f_n) : alpha_n beta_n$
     )
   )
@@ -96,13 +95,17 @@
   )
 }
 
-#let Assign-Call = prooftree(
-  axiom($Delta(p) = alpha' beta'$),
-  axiom($Delta tr m(overline(p)) tl Delta_1$),
-  axiom($mtype(m) = alpha_0 beta_0, ..., alpha_n beta_n -> alpha$),
-  axiom($Delta_1[p |-> alpha] = Delta'$),
-  rule(n:4, label: "Assign-Call", $mid(p = m(overline(p)))'$)
-)
+#let Assign-Call = {
+  let a1 = $Delta(p) = alpha' beta'$
+  let a2 = $Delta tr m(overline(p)) tl Delta_1$
+  let a3 = $mtype(m) = alpha_0 beta_0, ..., alpha_n beta_n -> alpha$
+  let a4 = $Delta_1[p |-> alpha] = Delta'$
+  prooftree(
+    stacked-axiom((a1, a2), (a3, a4)),
+    rule(label: "Assign-Call", $mid(p = m(overline(p)))'$)
+  )
+}
+
 
 #let Call = {
   let a0 = $forall 0 <= i <= n : Delta(p_i) = alpha_i beta_i$
@@ -116,7 +119,7 @@
   let a7 = $norm(p_0 : alpha'_0 beta'_0, ..., p_n : alpha'_n beta'_n) = p'_0 : alpha''_0 beta''_0, ..., p'_m : alpha''_m beta''_m$
   prooftree(
     stacked-axiom(
-      (a0, a1), (a2, a3), (a4, a5), (a6, a7)
+      (a0,), (a1,), (a2,), (a3,), (a4,), (a5, a6), (a7,)
     ),
     rule(label: "Call", $mid(m(p_0, ..., p_n))', p'_0 : alpha''_0 beta''_0, ..., p'_m : alpha''_m beta''_m$)
   )