[motoko-san] upd README

src/viper/README.md

@@ -26,7 +26,11 @@ _Motoko-san_ is a prototype code-level verifier for Motoko. The project started
   | [Testing](#Testing)
   | [File structure](#Struct)
 
-**[Currently supported features](#Subset)**
+**[Currently supported features](#Subset) -**
+    [Types and operations](#SupportedTypes)
+  | [Declarations](#SupportedDecls)
+  | [Expressions](#SupportedExprs)
+  | [Static code specification](#SupportedSpec)
 
 **[Further information](#Further)**
 
@@ -147,7 +151,7 @@ The implementation of _Motoko-san_ consists of the following source files:
 * `src/viper/pretty.ml` — the Viper pretty printer. Used for serializing Viper AST into text.
 * `src/viper/trans.ml` — the Motoko-to-Viper translation. Implements the logic of _Motoko-san_.
 * `src/viper/prep.ml` —  the Motoko-to-Motoko pass that prepares the unit for translation.
-
+* `src/viper/prelude.ml` - the Viper prelude generation. Creates common types and functions.
 
 Currently supported language features
 -------------------------------------
@@ -164,7 +168,7 @@ Below, we summarize the language features that _Motoko-san_ currently supports.
     Extending to actor classes and modules is _simple_.
 
 * **Types and operations**
-
+<a name="SupportedTypes"></a>
     * Type `Bool`
         * Literals: `true`, `false`
         * Operations: `not`, `or`, `and`, `implies` (short circuiting semantics)
@@ -269,7 +273,7 @@ Below, we summarize the language features that _Motoko-san_ currently supports.
           let x = #Con(p)          // not supported
           ```
 
-    Supporting `Text`, `Int32`, tuples, record, and variants is _simple_.
+    Supporting `Int32` is _simple_.
 
     Supporting `async` types is _hard_.
 
@@ -280,7 +284,7 @@ Below, we summarize the language features that _Motoko-san_ currently supports.
     Supporting other element types in arrays and tuples is _simple_.
 
 * **Declarations**
-  
+<a name="SupportedDecls"></a>
     * **Actor fields**
         * Mutable: `var x = ...`
         * Immutable: `let y = ...`
@@ -350,7 +354,22 @@ Below, we summarize the language features that _Motoko-san_ currently supports.
 
     * `if-[else]` statements
 
-        Supporting pattern-matching is conceptually _simple_.
+    * Pattern-matching: `swtich(e)`
+
+      ```motoko
+      switch (x) {
+          case null { .. };
+          case (?a) {
+            switch(a) {
+              case 1: { .. };
+              case 2: { .. };
+              case _: { .. };
+            }
+          };
+      };
+      ```
+
+      Nested matching is _not_ supported yet (simplifying Motoko-Motoko pass is missed).
 
     * Return statements `return e;`
 
@@ -404,7 +423,17 @@ Below, we summarize the language features that _Motoko-san_ currently supports.
 
         Supporting async function calls is _simple_.
 
+* **Expressions**
+<a name="SupportedExprs"></a>
+    * `x` -- local variables, function arguments, actor fields.
+    * `e2 <op> e2` -- binary operations.
+    * access to elements of an array `a[i]`, tuple `t.0` or record `a.f`.
+    * method call is _simple_ since could be boiled down to statement via simple Motoko-Motoko pass.
+    * `if`-expression is _simple_.
+    * `switch`-expression is _simple_ since boiled down to series of `if`.
+
 * **Static code specifications** — Note that the syntax is provisional:
+<a name="SupportedSpec"></a>
 
     * `assert:invariant` — Canister-level invariants
     
@@ -417,8 +446,14 @@ Below, we summarize the language features that _Motoko-san_ currently supports.
     * `assert:func` — Function preconditions
     
     * `assert:return` — Function postconditions. 
+
+    * `assert:system` — Compile-time assertions
+    
+    * `assert:loop:invariant` — Loop invariants
     
-        * These may refer to variables in the _initial_ state of the function call using the syntax `(old <exp>)`, for example:
+    **Expressions in assertions**
+
+    * `old(e)` - refers to value of the expression `e` in the _initial_ state of the function call. Could be used in postconditions or loop invariants to show changes that are made. For example:
 
             ```motoko
             var x : Int;
@@ -438,20 +473,17 @@ Below, we summarize the language features that _Motoko-san_ currently supports.
                 assert:return x < old_x;
             };
             ```
-        * To refer to the result value of a function in a postcondition, use the `var:return` syntax:
 
-            ```motoko
-            private func f(): [var Nat] {
-                assert:return (var:return).size() == xarray.size();
-                ...
-            }
-            ```
-    
-    * `assert:system` — Compile-time assertions
-    
-    * `assert:loop:invariant` — Loop invariants
-    
-    **Pure functions** — The tool could be easily extended with a keyword, e.g., `@pure`, to specify functions that are verifier to be side-effect free; such functions could be used inside other code specifications, e.g., `assert:invariant is_okay()` for some `@pure func is_okay() : Bool`.
+    * **Pure functions** — The tool could be easily extended with a keyword, e.g., `@pure`, to specify functions that are verifier to be side-effect free; such functions could be used inside other code specifications, e.g., `assert:invariant is_okay()` for some `@pure func is_okay() : Bool`.
+
+   * `Prim.Ret<T>()` - refers to the result value of a function. It's temporal syntax and requires manually annotate type of the value. Example:
+
+     ```motoko
+     private func create_array(n: Nat): [var Nat] {
+        assert:return (Prim.Ret<[var Nat]>).size() == n;
+        ...
+    }
+    ```
 
 Further information
 -------------------