Add viper highlighting

chapters/2-Background.typ

@@ -302,7 +302,7 @@ In Viper, methods can be seen as an abstraction over a sequence of operations. T
 
 #figure(
   caption: "Viper method example",
-  ```java
+  ```vpr
   method multiply(x: Int, y: Int) returns (res: Int)
   requires x >= 0 && y >= 0
   ensures res == x * y
@@ -330,7 +330,7 @@ Field permissions, which define the heap areas that an expression, a statement,
 
 #figure(
   caption: "Viper permissions example",
-  ```java
+  ```vpr
   field b: Bool
 
   method negate(this: Ref)
@@ -347,7 +347,7 @@ As well as being declared in preconditions and postconditions, field permissions
 
 #figure(
   caption: "Viper exclusivity example",
-  ```java
+  ```vpr
   field b: Bool
 
   method exclusivity(x: Ref, y: Ref)
@@ -366,7 +366,7 @@ The wildcard permission amount provides a convenient way to implement duplicable
 
 #figure(
   caption: "Viper fractional permissions example",
-  ```java
+  ```vpr
   field b: Bool
   
   method fractional(x: Ref, y: Ref, z: Ref)
@@ -392,7 +392,7 @@ Similar to predicates, functions in Viper are used to define parameterized and p
 
 #figure(
   caption: "Viper predicate example",
-  ```java
+  ```vpr
   field value: Int
   field next: Ref
 
@@ -432,7 +432,7 @@ Domain axioms are also global and define properties that are assumed to be true
 
 #figure(
   caption: "Viper domain example",
-  ```java
+  ```vpr
   domain Fraction {
     function nominator(f: Fraction): Int
     function denominator(f: Fraction): Int

chapters/6-Encoding.typ

@@ -113,7 +113,7 @@ Finally, @stack-vpr shows how the example from @cap:kt-stack is encoded in Viper
 
 #figure(
   caption: "Stack encoding in Viper",
-  ```java
+  ```vpr
   field value: Ref, next: Ref, root: Ref
 
   predicate UniqueAny(this: Ref)

config/thesis-config.typ

@@ -17,6 +17,55 @@
   image("../images/cpp-logo.svg", width: .8em), " C++",
 )
 
+#let vpr-show() = r => {
+  // Types:
+  show regex("\b(Ref)\b"): set text(rgb("#4b69c6"))
+  show regex("\b(Bool)\b"): set text(rgb("#4b69c6"))
+  show regex("\b(Int)\b"): set text(rgb("#4b69c6"))
+
+  // Keywords:
+  show regex("\b(inhale)\b"): set text(rgb("#d73a49"))
+  show regex("\b(exhale)\b"): set text(rgb("#d73a49"))
+  show regex("\b(method)\b"): set text(rgb("#d73a49"))
+  show regex("\b(function)\b"): set text(rgb("#d73a49"))
+  show regex("\b(predicate)\b"): set text(rgb("#d73a49"))
+  show regex("\b(field)\b"): set text(rgb("#d73a49"))
+  show regex("\b(fold)\b"): set text(rgb("#d73a49"))
+  show regex("\b(unfold)\b"): set text(rgb("#d73a49"))
+  show regex("\b(unfolding)\b"): set text(rgb("#d73a49"))
+  show regex("\b(in)\b"): set text(rgb("#d73a49"))
+  show regex("\b(requires)\b"): set text(rgb("#d73a49"))
+  show regex("\b(ensures)\b"): set text(rgb("#d73a49"))
+  show regex("\b(returns)\b"): set text(rgb("#d73a49"))
+  show regex("\b(var)\b"): set text(rgb("#d73a49"))
+  show regex("\b(if)\b"): set text(rgb("#d73a49"))
+  show regex("\b(else)\b"): set text(rgb("#d73a49"))
+  show regex("\b(acc)\b"): set text(rgb("#d73a49"))
+  show regex("\b(while)\b"): set text(rgb("#d73a49"))
+  show regex("\b(forall)\b"): set text(rgb("#d73a49"))
+  show regex("\b(axiom)\b"): set text(rgb("#d73a49"))
+  show regex("\b(invariant)\b"): set text(rgb("#d73a49"))
+  show regex("\b(assert)\b"): set text(rgb("#d73a49"))
+  show regex("\b(wildcard)\b"): set text(rgb("#d73a49"))
+  show regex("\b(null)\b"): set text(rgb("#d73a49"))
+  show regex("\b(true)\b"): set text(rgb("#d73a49"))
+  show regex("\b(false)\b"): set text(rgb("#d73a49"))
+  show regex("\b(domain)\b"): set text(rgb("#d73a49"))
+  show regex("\b(write)\b"): set text(rgb("#d73a49"))
+  show "&&": set text(rgb("#d73a49"))
+  show "||": set text(rgb("#d73a49"))
+  show "=": set text(rgb("#d73a49"))
+  show "<": set text(rgb("#d73a49"))
+  show ">": set text(rgb("#d73a49"))
+  show ":": set text(rgb("#d73a49"))
+  show "!": set text(rgb("#d73a49"))
+  show "*": set text(rgb("#d73a49"))
+
+  show regex("//.*"): set text(rgb("#8a8a8a"))
+
+  r
+  }
+
 #let config(
     myAuthor: "Nome cognome",
     myTitle: "Titolo",
@@ -45,13 +94,16 @@
         enabled: true,
         languages: (
           kt: (name: kt-name, color: purple),
-          java: (name: vpr-name, color: orange),
+          vpr: (name: vpr-name, color: orange),
           cpp: (name: cpp-name, color: blue)
         )
       )
       it
       codly-disable()
     }
+
+    show raw.where(lang: "vpr"): vpr-show()
+
     show par: set block(spacing: 0.55em)
     show heading: set block(above: 1.4em, below: 1em)
 

vars/kt-to-vpr-examples.typ

@@ -13,7 +13,7 @@ fun use_f(x: A) {
 }
 ```
 
-#let intro-vpr = ```java
+#let intro-vpr = ```vpr
 field n: Int
 
 method f(x: Ref, y: Ref)
@@ -59,7 +59,7 @@ class C(
 ) : A(0, 0)
 ```
 
-#let classes-vpr = ```java
+#let classes-vpr = ```vpr
 field x: Int
 field y: Int
 field a1: Ref
@@ -94,7 +94,7 @@ fun returnShared(): T {
 }
 ```
 
-#let return-vpr = ```java
+#let return-vpr = ```vpr
 method returnUnique()
 returns(ret: Ref)
 ensures acc(SharedT(ret), wildcard)
@@ -127,7 +127,7 @@ fun arg_shared_b(
 }
 ```
 
-#let param-vpr = ```java
+#let param-vpr = ```vpr
 method arg_unique(t: Ref)
 requires acc(UniqueT(t))
 requires acc(SharedT(t), wildcard)
@@ -168,7 +168,7 @@ class C(
 ) : A(0, 0)
 ```
 
-#let classes-unique-vpr = ```java
+#let classes-unique-vpr = ```vpr
 predicate UniqueA(this: Ref) {
   acc(this.x, wildcard) &&
   acc(this.y, write)
@@ -192,7 +192,7 @@ predicate UniqueC(this: Ref) {
 }
 ```
 
-#let full-encoding = ```java
+#let full-encoding = ```vpr
 field bf$a1: Ref
 field bf$a2: Ref
 field bf$b: Ref
@@ -238,7 +238,7 @@ fun @receiver:Unique T.uniqueReceiver() {}
 fun @receiver:Unique @receiver:Borrowed T.uniqueBorrowedReceiver() {}
 ```
 
-#let receiver-vpr = ```java
+#let receiver-vpr = ```vpr
 method uniqueReceiver(this: Ref)
 requires acc(SharedT(this), wildcard)
 requires acc(UniqueT(this), write)
@@ -272,7 +272,7 @@ fun call(
 }
 ```
 
-#let unique-call-vpr = ```java
+#let unique-call-vpr = ```vpr
 method uniqueParam(t: Ref)
 requires acc(UniqueT(t), write) && acc(SharedT(t), wildcard)
 ensures acc(SharedT(t), wildcard)
@@ -310,7 +310,7 @@ fun call(@Unique t: T) {
 }
 ```
 
-#let shared-call-vpr = ```java
+#let shared-call-vpr = ```vpr
 method sharedParam(t: Ref)
 requires acc(SharedT(t), wildcard)
 ensures acc(SharedT(t), wildcard)
@@ -338,7 +338,7 @@ class A(val x: Int, var y: Int)
 class B(@property:Unique var a1: A, var a2: A)
 ```
 
-#let constructor-vpr = ```java
+#let constructor-vpr = ```vpr
 method constructorA(p1: Int, p2: Int) returns (ret: Ref)
   ensures acc(SharedA(ret), wildcard)
   ensures acc(UniqueA(ret), write)