Beta support for Kappa (#744)

* Beta support for Kappa

Commit history below:

Experimental support for linear capabilities

This commit lets the programmer annotate traits with modes. An included
trait must have a mode, either given at inclusion time, or given in the
trait header (this works as a default). There are currently two modes;
`linear` whose references must be treated linearly, and `unsafe` which
works just like a regular type (no restrictions on aliasing). A value of
class type may be cast into a trait type (like in `master`) or
a (composite) capability type. All modes must match exactly. Here is a
small example program to show what is currently possible:

```
-- Foo defaults to unsafe
unsafe trait Foo<t>
  require f : t
  def foo() : void
    print "Foo!"

-- Inclusion of Bar requires specifying a mode
trait Bar

-- C can be aliased freely
passive class C<t> : Foo<t> + unsafe Bar
  f : t

-- D must be treated linearly unless upcast to Foo<int>
passive class D : Foo<int> + linear Bar
  f : int

class Main
  def main() : void
    let x = new D
        y = consume x : linear Bar + unsafe Foo<int>
        z = consume y : Foo<int>
        w = z
    in
      w.foo()
```

The checking that linearity is preserved is done using an additional
pass, implemented in the file `src/typechecker/Capturechecker.hs`. This
keeps the changes made to `Typechecker.hs` to a minimum, which is nice.
Basically, the capturechecker figures out where references are captured
and when a linear reference is safe to capture.

The linear references **should** be interoperable with all the features
currently in Encore, but testing is very welcome! It should be noted
that consumes are currently not atomic (the value is read and nullified
sequentially), but this shouldn't matter in a race-free program. Linear
streams are possible but not very useful, since both `get` and `getNext`
require you to consume the stream. For any useful patterns we would need
a way to `get` and move the stream forward in one go (maybe `consume s`
should be the way to do this?).

Experimental support for borrowing

This commit adds support for declaring parameters as
stackbound (`S(Foo)`). A linear reference can be passed as a stack bound
parameter without consuming, as the linear alias is buried for the
duration of the call (borrowing requires a synchronous call). A
stackbound may be locally aliased (but not returned from functions or
methods), but cannot be used in parallel (so far this means that it may
not be passed to an active object). The following program exemplifies
most uses of borrowing:

```
-- Stackbounds cannot be returned from functions or methods
-- def steal(x : S(Token)) : S(Token)
--   x

def borrow(x : S(Token)) : void{
  let thief = new Thief<Token>
      y = x -- Stackbounds can be locally aliased
  in{
    -- thief.steal(x); -- Stackbounds cannot be passed to active objects
    borrowAgain(y);  -- Stackbounds can be passed to other borrowing functions/methods
  }
}

def borrowAgain(x : S(Token)) : void{
  x.foo(); -- You can call methods and access fields on stackbound objects
}

class Main
  -- f : S(Foo<int>) -- Fields cannot be stackbound
  def borrow(x : S(Token)) : void
    borrow(x.f) -- Fields of linear objects can be borrowed as long as each node in the path is linear

  def main() : void
    let x = new Token
        thief = new Thief<Token>
    in{
       -- thief.steal(x); -- Linear values cannot be borrowed by active objects
       x.f = new Token;
       this.borrow(x); -- Synchronous method calls can borrow linear values
    }

trait Foo
 def foo() : void
   print "Foo!"

passive class Token : linear Foo
  f : Token

class Thief<t>
  def steal(x : S(t)) : void
    ()
```

Borrowing should interplay nicely with arrays and most other programming
constructs, but please do report anomalies of any kind.

made embeds free

Support for read mode

This was actually implemented before, but was lost in a git related
accident...

A trait with the `read` mode can only require `val` fields of safe
types. The safe types are active objects, primitives and passive objects
with a safe mode (currently only `read` itself).

Support for subordinate mode

Types containing a capability type with the `subord` mode cannot be
returned from its surrounding aggregate. This is checked by controlling
the target of a method call or field access and throwing an error unless
the target is `this` or is fully encapsulated itself (i.e. is a
capability type with *only* subordinate capabilities). Traits without
manifest modes are typechecked as if they were subordinate, but they
still need to be given an explicit mode at inclusion.

A known issue is that subordinate state can be leaked via closures.

Support for thread mode

Capabilities with the thread mode may not leave the active object that
created it. This is checked when calling methods on active objects; if
an argument is thread or the return type is thread, the target must
either be this, or itself be thread. This also means that fields with
the thread mode can only be declared in traits that are manifestly
thread.

Experimental splitting support

A let expression can now have several variables *per expression*, and
each variable can optionally have a type annotation:
```
let i, f : float = 42;
print i; -- 42
print f; -- 42.000000
```
If the types of the variables are linear, these are checked to be in
conjunction in the type of the right hand side:
```
let p = new Person();
let a : Aged, n : Named = consume p;
```
If the types are not linear any splitting is allowed. Not giving a type
to a variable defaults to the type of the right hand side (meaning any
splitting will fail).

Fix #451, parsing error with manifest modes

Since `read` is not a reserved keyword, the following code:
```
class T

read trait Get
```
was parsed as
```
class T
  read <Expecting ':'>

trait Get
```

This is fixed by adding a `try` that allows the parser to backtrack when
reading a field fails.

Read mode must be manifestly set

To simplify typechecking, the read mode must be manifestly set. It can
still be used on inclusion, but only if the included trait already is
manifestly read.

Fix #452, consider safe composite types safe

This commit considers `Maybe T`, `Stream T`, `Fut T` and `Par T` as safe
types iff `T` is a safe type. Tuples are safe if all the constituent
types are safe. Ranges are also safe.

Arrays are not safe since they can be written to. In the future one
could consider a type like `[val T]` to be safe (an array that can only
be read from). I'll leave that design up to @glundi.

Fixed upcasting bug

Before this commit, a composite type was only checked for subsumption of
operations, meaning that `T1 + T2` could be cast to `T1 * T2`. Now an
upcast must preserve the conjunctions of the subtype (i.e. not introduce
new ones). It is still safe to forget conjunctions by casting `T1 * T2`
into `T1 + T2`.

Fix #450, check conjunctiveness when splitting

Before this commit, there was a bug when checking of whether an unpack was
allowed that lead to code like `let read Get, linear Set = consume Cell`
compiling. This is now fixed so that all types in an unpack needs to be
separated by a conjunction in the capability being unpacked, unless all
the types can safely be (at least locally) aliased.

A known bug is that we also need to check that the modes are preserved
for all types in an upcast, meaning that the `read Get` above should
also be `linear` (assuming `Get` and `Set` are conjunctive in `Cell`).

Fixed capture bug when matching on tuples

This commit fixes a bug where matching on a tuple with a linear value
would not allow you to capture that value in a pattern:

```
let x = new LinearThing();
match (42, consume x) with
  (n, y) => () -- Cannot capture linear expression y
```

The solution is a bit clunky but works. It adds a boolean in the
meta-blob to mark which expressions are patterns. Patterns can then be
ignored by the capture checker.

Disallow sending borrowed values to constructors

Fix #604, a bug where borrowed values could be passed as (non-borrowed)
arguments to constructors. Constructors now work like normal method
calls.

Also moved all (both) tests regarding capabilities to a test-suite of
their own and added more tests regarding borrowing.

Prevent arrays of borrowed elements

Disallow the type `[borrowed T]`, since it can be used to duplicate
linear values (see the test `arrayBorrow.enc`).

Support for safe closures

A closure is now annotated when capturing a `thread`, `subord` or
`borrowed` capability, meaning you cannot cheat the type system by
capturing state in closures. See tests `capabilities/closure*` for
examples.

Check overriding of methods in read traits

This commit adapts method overriding and provision to consider read
traits. A required method in a read trait can only be provided by
another read trait. A read trait can only be extended with `val` fields
of safe type. See tests `readTrait*` for examples.

A current issue is that there is no way to consider passive classes
safe. Currently, there is a special case for the class `String`, but we
should come up with a way that makes it possible to consider classes
safe.

Thread mode => Local mode

Remove unsafe traits from tests

Check for clashing manifest modes

Read and subordinate are minor modes

Support for moded classes (NO TESTS)

Support for looking up marker trait (ignore mode)

Translated capability test suite

Translated basic tests to Kappa

Translated trait tests to Kappa

Translated concurrency tests

Translated the remaining tests, modulo shared

Support for shared mode (very imprecise...)

Only allow safe type arguments

Warnings for unsafe operations

Currently passing arrays and splitting conjunctions

Fixed bug in capability splitting

Support for strong updates (dropping linear capabilities)

Fix regression

Updated last bits of standard library

Allow local in active

Added tests and moved old tests around

* Remove comments and unused code

* Translated Savina benchmarks to Kappa

* Removed null-check hack from Savina

* Refactoring after Kiko's suggentions

* Fixed bug when giving mode to unmoded class

* Fixed bug with implicitly safe class

* Set formal arrow type

* Merged errors

* Merge capturechecking errors with typechecking errors

* Relax polymorphism to allow local type arguments

Instead, polymorphic values cannot be passed between
actors (currently this is only warned about).

* Improve error messages

* Removed unused Makefiles

Author: EliasC

emacs/encore-mode/encore-mode-expansions.el

@@ -462,14 +462,15 @@
   (let (p1 p2 (case-fold-search nil))
     (progn
       (move-end-of-line nil)
-      (re-search-backward "\\<class\\|trait\\>")
+      (re-search-backward "\\<class\\>\\|\\<\.+\>? *\\<trait\\>")
       (move-end-of-line nil)
       (skip-chars-forward " \t\n")
       (setq p1 (point))
 
       (while (and (not (eobp))
                   (not (string-match "^[ \t]*\\<end\\>" (current-line))))
-        (if (string-match encore-block-open-regex (current-line))
+        (if (and (not (string-match "\\<require\\>" (current-line)))
+                 (string-match encore-block-open-regex (current-line)))
             (encore-skip-block))
         (forward-line 1))
       (skip-chars-backward " \t\n")
@@ -493,7 +494,8 @@
       (forward-line 1)
       (while (and (not (eobp))
                   (not (string-match "^[ \t]*\\<end\\>" (current-line))))
-        (if (string-match encore-block-open-regex (current-line))
+        (if (and (not (string-match "\\<require\\>" (current-line)))
+                 (string-match encore-block-open-regex (current-line)))
             (encore-skip-block))
         (forward-line 1))
 

emacs/encore-mode/encore-mode.el

@@ -52,22 +52,24 @@
 ;; Please keep these lists sorted
 (setq encore-keywords
       '(
+        "active"
         "as"
         "and"
         "async"
         "await"
+        "borrowed"
         "break"
         "by"
         "case"
         "chain"
         "class"
+        "consume"
         "def"
         "do"
         "else"
         "end"
         "eos"
         "for"
-        "foreach"
         "fun"
         "get"
         "getNext"
@@ -79,18 +81,22 @@
         "let"
         "liftf"
         "liftv"
+        "linear"
+        "local"
         "match"
         "module"
         "new"
         "not"
         "or"
-        "passive"
         "print"
         "println"
         "qualified"
+        "read"
         "repeat"
         "require"
+        "shared"
         "stream"
+        "subord"
         "suspend"
         "then"
         "this"
@@ -111,6 +117,7 @@
         "BODY"
         "EMBED"
         "END"
+        "unsafe"
         ))
 (setq encore-constants
       '(
@@ -203,12 +210,10 @@
   (if (equal first "def")
       (if (string-match "\\<def\\>" line)
           (match-beginning 0)
-      (if (string-match "\\<passive\\>" line)
+      (if (string-match "\\(\\<.+\\>\\)? *\\<class\\>" line)
           (+ (match-beginning 0) encore-tab-width)
-      (if (string-match "\\<class\\>" line)
-          (+ (match-beginning 0) encore-tab-width)
-      (if (string-match "\\<trait\\>" line)
-          (+ (match-beginning 0) encore-tab-width)))))
+      (if (string-match "\\(\\<.+\\>\\)? *\\<trait\\>" line)
+          (+ (match-beginning 0) encore-tab-width))))
 
   (if (equal first "fun")
       (if (string-match "\\<where\\>" line)
@@ -230,7 +235,7 @@
           (match-beginning 1)
       (if (string-match "\\<class\\>" line)
           (match-beginning 0)
-      (if (string-match "\\<trait\\>" line)
+      (if (string-match "\\<.+\\>? *\\<trait\\>" line)
           (match-beginning 0)))))
 
   (if (equal first "else")
@@ -305,14 +310,14 @@
 
 (setq encore-block-open-regex
       (concat "\\<def\\>"    "\\|"
-              "\\<class\\>"  "\\|"
-              "\\<passive"   "\\|"
-              "\\<trait\\>"  "\\|"
+              "\\<fun\\>"    "\\|"
+              "\\(\\<.+\\>\\)? *\\<class\\>" "\\|"
+              "\\(\\<.+\\>\\)? *\\<trait\\>" "\\|"
               "\\<while\\>"  "\\|"
               "\\<for\\>"    "\\|"
               "\\<repeat\\>" "\\|"
               "\\<do\\>"     "\\|"
-              "\\<fun\\>[^=>\n]*\\($\\|--\\)" "\\|"
+              "\\<fun\\>" "\\|"
               "\\<let\\>" "\\|"
               "\\<if\\>" "\\|"
               "\\<unless\\>" "\\|"
@@ -420,7 +425,7 @@
 (defvar encore-imenu-generic-expression
   '(("passive class" "^\s*passive\s+class\s*\\(\\<\\w+\\>\\) *\\(\\[.*\\]\\)? *:?.*" 1)
     ("active class" "^\s*class\s*\\(\\<\\w+\\>\\)" 1)
-    ("trait" "^\s*trait\s*\\(\\<\\w+\\>\\)" 1)
+    ("trait" "^\\<.+\\>?\s*trait\s*\\(\\<\\w+\\>\\)" 1)
     ("method definition" "^\s*def\s*\\(.*\s+\\)*\\(\\<\\w+\\>\\) *\\(\\[.*\\]\\)?(" 2)
     ("function definition" "^\s*fun\s*\\(\\w+\\) *\\(\\[.*\\]\\)?(" 1))
   "Contains regexes to parse Encore with imenu")
@@ -466,6 +471,9 @@
      (error " *** Error during typechecking *** \n"
             "\"" (file-name) "\"" " (line " line ", column " column ")\n"
             (message))
+     (error " *** Error during capturechecking *** \n"
+            "\"" (file-name) "\"" " (line " line ", column " column ")\n"
+            (message))
      (info line-start "Importing module" (message) line-end)
      )
     :modes encore-mode)

emacs/encore-mode/snippets/encore-mode/main

@@ -3,7 +3,7 @@
 # key: main
 # expand-env: ((yas-also-auto-indent-first-line 't))
 # --
-class Main
+active class Main
   def main(args : [String]) : unit
     $0
   end

modules/standard/Active/Active.enc

@@ -1,7 +1,7 @@
 -- This file was automatically converted by encorec
 
 module Active
-class Active[inner]
+active class Active[inner]
   var state : inner
   def init(factory : () -> inner) : unit
     this.state = factory()

modules/standard/Active/ActiveTest.enc

@@ -4,6 +4,9 @@ import Active.Active
 fun getActiveInt() : Active[int]
   new Active[int](fun () => 1)
 end
+
+-- TODO: This won't compile until parametric types can be
+-- instantiated with local or linear types
 fun getActiveFoo() : Active[Foo]
   new Active[Foo](fun () => new Foo())
 end
@@ -29,7 +32,7 @@ fun testApply() : unit
     assertTrue(2 == (get(a.getState())).read())
   end
 end
-passive class Foo
+local class Foo
   var f : int
   def init() : unit
     this.f = 1
@@ -41,7 +44,7 @@ passive class Foo
     this.f
   end
 end
-class Main
+active class Main
   def main() : unit
     testInit()
     testMap()

modules/standard/Boxed/Bool.enc

@@ -2,8 +2,8 @@
 
 module Bool
 
-passive class Bool
-  var value : bool
+read class Bool
+  val value : bool
   def init(x : bool) : unit
     this.value = x
   end

modules/standard/Boxed/BoxedTest.enc

@@ -4,7 +4,7 @@ import Boxed.Real
 import Boxed.Bool
 import Boxed.Unit
 
-class Main
+active class Main
   def main() : unit
     val maxReal = EMBED (real) 1.7976931348623157E+308; END
     val minReal = EMBED (real) -1.7976931348623157E+308; END

modules/standard/Boxed/Char.enc

@@ -2,8 +2,8 @@
 
 module Char
 
-passive class Char
-  var value : char
+read class Char
+  val value : char
   def init(x : char) : unit
     this.value = x
   end

modules/standard/Boxed/Integer.enc

@@ -2,8 +2,8 @@
 
 module Integer
 
-passive class Integer
-  var value : int
+read class Integer
+  val value : int
   def init(x : int) : unit
     this.value = x
   end

modules/standard/Boxed/Real.enc

@@ -2,8 +2,8 @@
 
 module Real
 
-passive class Real
-  var value : real
+read class Real
+  val value : real
   def init(x : real) : unit
     this.value = x
   end

modules/standard/Boxed/Unit.enc

@@ -2,7 +2,7 @@
 
 module Unit
 
-passive class Unit
+read class Unit
   def show() : String
     "()"
   end

modules/standard/Data/Either.enc

@@ -7,7 +7,7 @@ end
 fun Right[a, b](x : b) : Either[a, b]
   new Right[a, b](x) : Either[a, b]
 end
-trait Either[a, b]
+read trait Either[a, b]
   require def Left() : Maybe[a]
   require def Right() : Maybe[b]
   def map(f : b -> b) : Either[a, b]
@@ -44,8 +44,8 @@ trait Either[a, b]
     end
   end
 end
-passive class Left[a, b] : Either[a, b](x)
-  var x : a
+class Left[a, b] : Either[a, b](x)
+  val x : a
   def init(x : a) : unit
     this.x = x
   end
@@ -56,8 +56,8 @@ passive class Left[a, b] : Either[a, b](x)
     Nothing
   end
 end
-passive class Right[a, b] : Either[a, b](x)
-  var x : b
+class Right[a, b] : Either[a, b](x)
+  val x : b
   def init(x : b) : unit
     this.x = x
   end

modules/standard/Random.enc

@@ -18,8 +18,8 @@ fun random(max : int) : int
 
   END
 end
-passive class Random
-  var seed : EMBED unsigned int END
+read class Random
+  val seed : EMBED unsigned int END
   def Random_trace() : unit
     ()
   end

modules/standard/Regex/Regex.enc

@@ -13,7 +13,7 @@ END
 
 typedef PMatch = EMBED regmatch_t* END
 typedef RegexT = EMBED regex_t END
-passive class Regex
+local class Regex
   var pattern : String
   var maxSize : int
   var flagICase : bool
@@ -23,7 +23,7 @@ passive class Regex
   var executed : EMBED char* END
   def Regex_trace() : unit
     EMBED (unit)
-      _enc__passive_String_t* _enc__field_pattern = _this->_enc__field_pattern;
+      _enc__read_String_t* _enc__field_pattern = _this->_enc__field_pattern;
       encore_trace_object((*_ctx), _enc__field_pattern, _enc__trace_String);
 
       regmatch_t* _enc__field_pMatch = _this->_enc__field_pMatch;

modules/standard/Regex/RegexTest.enc

@@ -1,7 +1,7 @@
 -- This file was automatically converted by encorec
 
 import Regex
-class Main
+active class Main
   def findRegex(regex : Regex, s : String) : unit
     match regex.exec(s) with
       case Just(true) =>

modules/standard/Set/OrderedSet.enc

@@ -1,7 +1,7 @@
 -- This file was automatically converted by encorec
 
 module OrderedSet
-passive class OrderedSet[t]
+local class OrderedSet[t]
   var root : Node[t]
   var size : int
   var cmp : (t, t) -> int
@@ -46,7 +46,7 @@ passive class OrderedSet[t]
     end
   end
 end
-passive class Node[t]
+local class Node[t] : Id
   var elem : t
   var left : Node[t]
   var right : Node[t]
@@ -150,7 +150,7 @@ passive class Node[t]
     end
   end
 end
-passive class OrderedSetIterator[t]
+local class OrderedSetIterator[t]
   var cur : Node[t]
   def init(n : Node[t]) : unit
     if n == null then

modules/standard/Set/OrderedSetTest.enc

@@ -178,7 +178,7 @@ fun testSetSemantics() : bool
     os.size() == 4
   end
 end
-class Main
+active class Main
   def main() : unit
     assertTrue(testInit())
     assertTrue(testAdd())

modules/standard/Std.enc

@@ -2,12 +2,12 @@ module Std
 
 -- This is currenly just a marker interface. In the future, id
 -- might contain the logic for giving objects ids.
-trait Id
+read trait Id
 end
 
 -- Equivalence is currently only supported on a given type. In
--- the future, other solutions are planned, possibly including a 
--- self type instead of this type parameter. 
-trait Eq[t]
+-- the future, other solutions are planned, possibly including a
+-- self type instead of this type parameter.
+read trait Eq[t]
   require def eq(other:t) : bool
 end