Fix stack in grammar + proof

appendix/stack-proof.typ

@@ -0,0 +1,13 @@
+#import "../config/utils.typ": *
+#import "../vars/proofs/push.typ": *
+#pagebreak(to:"odd")
+
+= Stack Typing Proof
+
+#display-rules(
+  push-1, "",
+  push-2, "",
+  push-3, "",
+)
+
+*TODO: CONTINUE*

chapters/5-Annotation-System.typ

@@ -747,40 +747,41 @@ Where _fresh_ is a variable that has not been declared before.
 - decide whether to put it in chapter 4 the kt example and here with the grammar. Or just one of them
 
 #figure(
-  caption: "TODO",
-  ```kt
-  class Node(
-      @property:Unique var value: Any?,
-      @property:Unique var next: Node?,
-  )
-
-  class Stack(@property:Unique var root: Node?)
-
-  fun @receiver:Borrowed @receiver:Unique Stack.push(@Unique value: Any?) {
-      // Δ = this: borrowed unique, value: unique
-      val r = this.root
-      // Δ = this: borrowed unique, value: unique, r: unique, this.root: T
-      this.root = Node(value, r)
-      // Δ = this: borrowed unique, value: T, r: T, this.root: unique
+  caption: "Typing for a Stack implementation",
+  ```
+  class Node(value: unique, next: unique)
+
+  class Stack(root: unique)
+
+  fun push(this: unique ♭, value: unique): shared {
+    begin_push;
+    // Δ = this: unique ♭, value: unique
+    var r;
+    // Δ = this: unique ♭, value: unique, r: T
+    r = this.root;
+    // Δ = this: unique ♭, value: unique, r: unique, this.root: T
+    this.root = Node(value, r);
+    // Δ = this: unique ♭, value: T, r: T, this.root: unique
+    return Unit();
   }
 
-  @Unique
-  fun @receiver:Borrowed @receiver:Unique Stack.pop(): Any? {
-      // Δ = this: borrowed unique
-      val value: Any?
-      // Δ = this: borrowed unique, value: T
-      if (this.root == null) {
-          value = null
-          // Δ = this: borrowed unique, value: unique
-      } else {
-          value = this.root!!.value
-          // Δ = this: borrowed unique, value: unique, this.root.value: T
-          this.root = this.root!!.next
-          // Δ = this: borrowed unique, value: unique, this.root: unique
-      }
-      // Unification...
-      // Δ = this: borrowed unique, value: unique, this.root: unique
-      return value
+  fun pop(this: unique ♭): unique {
+    begin_pop;
+    // Δ = this: unique ♭
+    var value;
+    // Δ = this: unique ♭, value: T
+    if (this.root == null) {
+        value = null;
+        // Δ = this: unique ♭, value: unique
+    } else {
+        value = this.root.value;
+        // Δ = this: unique ♭, value: unique, this.root.value: T
+        this.root = this.root.next;
+        // Δ = this: unique ♭, value: unique, this.root: unique
+    }
+    // Unification...
+    // Δ = this: unique ♭, value: unique, this.root: unique
+    return value;
   }
   ```
 )

config/utils.typ

@@ -26,6 +26,8 @@
 #let std = "std"
 #let loop = "while"
 #let do = "do"
+#let value = "value"
+#let push = "push"
 #let ablub = $alpha_union.sq beta_union.sq$
 #let tl = $tack.l$
 #let tr = $tack.r$

structure.typ

@@ -28,4 +28,5 @@
 #set heading(numbering: "A.1", supplement: "Appendix")
 #counter(heading).update(0)
 
-#include("./appendix/full-rules-set.typ")
+#include("./appendix/full-rules-set.typ")
+#include("./appendix/stack-proof.typ")

vars/proofs/push.typ

@@ -0,0 +1,39 @@
+#import "../../config/proof-tree.typ": *
+#import "../../config/utils.typ": *
+
+#let template = prooftree(
+  axiom($$),
+  rule(label: "", $$),
+)
+
+#let push-1 = prooftree(
+  axiom($push(this\: unique borrowed, value: unique): shared {...}$),
+  rule(label: "M-type", $mtype(push) = unique borrowed, unique -> shared$),
+  axiom($push(this\: unique borrowed, value: unique): shared {...}$),
+  rule(label: "M-args", $args(push) = this, value$),
+  rule(n:2, label: "Begin", $dot tr begin_push tl this: unique borrowed, value: unique$),
+)
+
+#let push-2 = prooftree(
+  axiom($r != this$),
+  axiom($r != value$),
+  axiom($r in.not dot$),
+  rule(n:2, label: "Not-In-Rec", $r in.not value: unique$),
+  rule(n:2, label: "Not-In-Rec", $r in.not this: unique borrowed, value: unique$),
+  rule(label: "Decl", $this: unique borrowed, value: unique tr var r tl  this: unique borrowed, value: unique, r: top$),
+)
+
+#let push-3 = {
+  let a1 = $this."root" subset.sq.eq.not r$
+  let a2 = $Delta(r) = top$
+  let a3 = $Delta(this."root") = unique borrowed$
+  let a4 = $unique != top$
+  let a5 = $(dot = borrowed) => (unique = unique)$
+  let a6 = $Delta[this."root" |-> top] = Delta, this."root": top equiv Delta_1$
+  let a7 = $Delta tr sp(this."root") = dot$
+  let a8 = $Delta_1 [r |-> unique] = Delta'$
+  prooftree(
+    stacked-axiom((a1,a2,a3,a4, a5), (a6, a7, a8)),
+    rule(label: "", $Delta equiv this: unique borrowed, value: unique, r: top tr r = this."root" tl this: unique borrowed, value: unique, r: unique, this."root": top equiv Delta'$),
+  )
+}