Add annotation example

appendix/bibliography/bibliography.bib

@@ -165,25 +165,6 @@ @book{Aliasing-OOP
 address = {Berlin, Heidelberg}
 }
 
-@article{Featherweight-Java,
-author = {Igarashi, Atsushi and Pierce, Benjamin C. and Wadler, Philip},
-title = {Featherweight Java: a minimal core calculus for Java and GJ},
-year = {2001},
-issue_date = {May 2001},
-publisher = {Association for Computing Machinery},
-address = {New York, NY, USA},
-volume = {23},
-number = {3},
-issn = {0164-0925},
-url = {https://doi.org/10.1145/503502.503505},
-doi = {10.1145/503502.503505},
-abstract = {Several recent studies have introduced lightweight versions of Java: reduced languages in which complex features like threads and reflection are dropped to enable rigorous arguments about key properties such as type safety. We carry this process a step further, omitting almost all features of the full language (including interfaces and even assignment) to obtain a small calculus, Featherweight Java, for which rigorous proofs are not only possible but easy. Featherweight Java bears a similar relation to Java as the lambda-calculus does to languages such as ML and Haskell. It offers a similar computational "feel," providing classes, methods, fields, inheritance, and dynamic typecasts with a semantics closely following Java's. A proof of type safety for Featherweight Java thus illustrates many of the interesting features of a safety proof for the full language, while remaining pleasingly compact. The minimal syntax, typing rules, and operational semantics of Featherweight Java make it a handy tool for studying the consequences of extensions and variations. As an illustration of its utility in this regard, we extend Featherweight Java with generic classes in the style of GJ (Bracha, Odersky, Stoutamire, and Wadler) and give a detailed proof of type safety. The extended system formalizes for the first time some of the key features of GJ.},
-journal = {ACM Trans. Program. Lang. Syst.},
-month = {may},
-pages = {396–450},
-numpages = {55},
-keywords = {Compilation, Java, generic classes, language design, language semantics}
-}
 
 TO BE ADDED PROBABLY
 - reachability types

chapters/4-Annotation-System.typ

@@ -28,14 +28,14 @@ How the annotation system looks like in Kotlin
 
 == Grammar
 
-In order to define the rules of this annotation system, a grammar representing a substet of the Kotlin language is used. The grammar uses a notation similar to Featherweight Java @Featherweight-Java.
+In order to define the rules of this annotation system, a grammar representing a substet of the Kotlin language is used.
 
 #figure(
   caption: "TODO",
   frame-box(
     $
       CL &::= class C(overline(f\: alpha_f)) \
-      M &::= m(overline(af beta space x)): af {begin_m; overline(s); ret_m e} \
+      M &::= m(overline(x\: af beta)): af {begin_m; overline(s); ret_m e} \
       af &::= unique | shared \
       beta &::= dot | borrowed \
       p &::= x | p.f \
@@ -57,10 +57,76 @@ In order to define the rules of this annotation system, a grammar representing a
 - `T` is an annotation that can only be inferred and means that the reference is *not accessible*.
 - $borrowed$ (borrowed) indicates that the function receiving the reference won't create extra aliases to it, and on return, its fields will maintain at least the permissions stated in the class declaration.
 - Annotations on fields indicate only the default permissions, in order to understand the real permissions of a fields it is necessary to look at the context. This concept is formalized by rules in /*@cap:paths*/ and shown in /*@field-annotations.*/
+
+#let grammar_annotations = ```
+class C(
+  f1: unique,
+  f2: shared
+)
+
+m1() : unique { 
+  ... 
+}
+
+
+m2(this: unique) : shared {
+  ... 
+}
+
+m3(
+  x1: unique,
+  x2: unique borrowed,
+  x3: shared,
+  x4: shared borrowed
+) {
+  ...
+}
+```
+
+#let kt_annotations = ```kt
+class C(
+    @Unique var f1: Any,
+    var f2: Any
+)
+
+@Unique
+fun m1(): Any {
+    /* ... */
+}
+
+fun @receiver:Unique Any.m2() {
+    /* ... */
+}
+
+fun m3(
+    @Unique x1: Any,
+    @Unique @Borrowed x2: Any,
+    x3: Any,
+    @Borrowed x4: Any
+) {
+    /* ... */
+}
+```
+
+#grid(
+  columns: (auto, auto),
+  column-gutter: 2em,
+  row-gutter: 1em,
+  [*Grammar*],[*Kotlin*],
+  grammar_annotations, kt_annotations
+)
+
 === Expressions
 === Statements
 - Since it is not too relevant for the purposes of the system, the guard of an if statement is kept as simple as possible.
 
+== General
+
+#display-rules(
+  M-Type, "",
+  M-Args, "",
+)
+
 == Context
 
 #frame-box(
@@ -71,15 +137,6 @@ In order to define the rules of this annotation system, a grammar representing a
   $
 )
 
-== General
-
-#display-rules(
-  M-Type, "",
-  M-Args, "",
-)
-
-== Context
-
 - The same variable/field cannot appear more than once in a context.
 - Contexts are always *finite*
 - If not present in the context, fields have a default annotation that is the one written in the class declaration
@@ -219,7 +276,7 @@ fun @receiver:Unique C.f(
 
 // TODO: derivation?
 
-$ f(unique this, unique borrowed space x, shared borrowed space y, shared z){begin_f; ...} $
+$ f(this: unique, x: unique borrowed, y: shared borrowed, z: shared){begin_f; ...} $
 
 === Variable Declaration
 
@@ -530,12 +587,6 @@ Where _fresh_ is a variable that has not been declared before.
   Return-p, "",
 )
 
-*Note:* Since they can be easily desugared, there are no rules for returnning `null` or a method call.
-
-The same can be done for the guard of if statements:
-- `if (p1 == null) ...` $equiv$ `var p2 ; p2 = null ; if(p1 == p2) ...`
-- `if (p1 == m(...)) ...` $equiv$ `var p2 ; p2 = m(...) ; if(p1 == p2) ...`
-
 // TODO: Stack example + DERIVATION
 
 // TODO: put this in a separate chapter

chapters/rules/base.typ

@@ -4,12 +4,12 @@
 // ****************** General ******************
 
 #let M-Type = prooftree(
-  axiom($m(alpha_0 beta_0 x_0, ..., alpha_n beta_n x_n): alpha {begin_m; overline(s); ret_m e}$),
+  axiom($m(x_0: alpha_0 beta_0, ..., x_n: alpha_n beta_n): alpha {begin_m; overline(s); ret_m e}$),
   rule(label: "M-Type", $mtype(m) = alpha_0 beta_0, ..., alpha_n beta_n -> alpha$),
 )
 
 #let M-Args = prooftree(
-  axiom($m(alpha_0 beta_0 x_0, ..., alpha_n beta_n x_n): alpha {begin_m; overline(s); ret_m e}$),
+  axiom($m(x_0: alpha_0 beta_0, ..., x_n: alpha_n beta_n): alpha {begin_m; overline(s); ret_m e}$),
   rule(label: "M-Args", $args(m) = x_0, ..., x_n$),
 )