Docs update

doc/spec/grammar/lexer.l

@@ -182,13 +182,17 @@ mask                      { return MASK; }
 override                  { return OVERRIDE; }
 named                     { return NAMED; }
 
+fip                       { return ID_FIP; }
+fbip                      { return ID_FBIP; }
+tail                      { return ID_TAIL; }
 rec                       { return ID_REC; }
 co                        { return ID_CO; }
 open                      { return ID_OPEN; }
 extend                    { return ID_EXTEND; }
 linear                    { return ID_LINEAR;  }
 value                     { return ID_VALUE;  }
 reference                 { return ID_REFERENCE;  }
+ref                       { return ID_REF; }
 
 inline                    { return ID_INLINE;  }
 noinline                  { return ID_NOINLINE;}

doc/spec/grammar/parser.y

@@ -62,7 +62,7 @@ void printDecl( const char* sort, const char* name );
 %token ALIAS CON
 %token FORALL EXISTS SOME
 
-%token IMPORT AS MODULE
+%token IMPORT AS MODULE MOD
 %token PUB ABSTRACT
 %token EXTERN
 %token INFIX INFIXL INFIXR
@@ -76,12 +76,13 @@ void printDecl( const char* sort, const char* name );
 %token CTL FINAL RAW
 %token IFACE UNSAFE BREAK CONTINUE
 
+%token ID_FBIP ID_FIP ID_TAIL
 %token ID_CO ID_REC
 %token ID_INLINE ID_NOINLINE
 %token ID_C ID_CS ID_JS ID_FILE
 %token ID_LINEAR ID_OPEN ID_EXTEND
 %token ID_BEHIND
-%token ID_VALUE ID_REFERENCE ID_SCOPED
+%token ID_VALUE ID_REFERENCE ID_REF ID_SCOPED
 %token ID_INITIALLY ID_FINALLY
 
 %type <Id>  varid conid qvarid qconid op
@@ -271,6 +272,7 @@ typemod     : structmod
 
 structmod   : ID_VALUE
             | ID_REFERENCE
+            | ID_REF
             | /* empty */
             ;
 
@@ -349,7 +351,18 @@ operation   : pub VAL identifier typeparams ':' tatomic
 -- Pure (top-level) Declarations
 ----------------------------------------------------------*/
 puredecl    : inlinemod VAL binder '=' blockexpr      { $$ = $3; }
-            | inlinemod FUN funid funbody             { $$ = $3; }
+            | inlinemod fipmod FUN funid funbody             { $$ = $4; }
+            ;
+
+fipalloc    : '(' INT ')'
+            | '(' 'n' ')'
+            | /* empty */
+            ;
+
+fipmod      : ID_FBIP fipalloc
+            | ID_FIP fipalloc
+            | ID_TAIL
+            | /* empty */
             ;
 
 inlinemod   : ID_INLINE
@@ -625,11 +638,15 @@ varid       : ID
             | ID_BEHIND       { $$ = "behind"; }
             | ID_VALUE        { $$ = "value"; }
             | ID_REFERENCE    { $$ = "reference"; }
+            | ID_REF          { $$ = "ref"; }
             | ID_SCOPED       { $$ = "scoped"; }
             | ID_INITIALLY    { $$ = "initially"; }
             | ID_FINALLY      { $$ = "finally"; }
             | ID_REC          { $$ = "rec"; }
             | ID_CO           { $$ = "co"; }
+            | ID_FBIP         { $$ = "fbip"; }
+            | ID_FIP          { $$ = "fip"; }
+            | ID_TAIL         { $$ = "tail"; }
             /* | ID_NAMED        { $$ = "named"; } */
             ;
 

doc/spec/spec.kk.md

@@ -108,11 +108,13 @@ grammar will draw it's lexemes from the _lex_ production.
 |              | &bar; | `match` &bar; `return` &bar; `with` &bar; `in`                                       |                         |
 |              | &bar; | `handle` &bar; `handler` &bar; `mask`                                                   |                         |
 |              | &bar; | `ctl` &bar; `final` &bar; `raw`                                     |                         |
-|              | &bar; | `override` &bar; `named`                                               |                         |
+|              | &bar; | `override` &bar; `named`                                        |                         |
 |              | &bar; | `interface` &bar; `break` &bar; `continue` &bar; `unsafe`        | (future reserved words) |
 |         |       |                                                                           |                         |
 | _specialid_  | ::=   | `co` &bar; `rec` &bar; `open` &bar; `extend` &bar; `behind`   |                         |
-|              | &bar; | `linear` &bar; `value` &bar; `reference`                            |                         |
+|              | &bar; | `linear` &bar; `scoped` &bar;                                 |                     |
+|              | &bar  | `value` &bar; `reference` &bar; `ref`           |                         |
+|              | &bar; | `fip` &bar; `fbip` &bar; `tail`                                                   |                         |
 |              | &bar; | `inline` &bar; `noinline` &bar; `initially` &bar; `finally`      |                         |
 |              | &bar; | `js` &bar; `c` &bar; `cs` &bar; `file`                           |                         |
 {.grammar .lex}
@@ -540,8 +542,10 @@ ignored.
 
 | ~~~~~~~~~~~~~~~| ~~~~~~| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~| ~~~~~~~~~~~~~~~~~~~~~|
 | _puredecl_     | ::=   | [_inlinemod_]{.opt} `val` _valdecl_                                                   |                      |
-|                | &bar; | [_inlinemod_]{.opt} `fun` _fundecl_                                                   |                      |
+|                | &bar; | [_inlinemod_]{.opt} [_fipmod_]{.opt} `fun` _fundecl_                                                   |                      |
 | _inlinemod_    | ::=   | `inline` &bar; `noinline`                                                  |                      |
+| _fipalloc_     | ::=   | `(` _integer_ `)` &bar;  `(` `n` `)`                                          | (n means finitely)     |
+| _fipmod_       | ::=   | `fip` [_fipalloc_]{.opt} &bar; `fbip` [_fipalloc_]{.opt} &bar; `tail`         |                      |
 |           |       |                                                                               |                      |
 | _valdecl_      | ::=   | _binder_ `=` _blockexpr_                                                           |                      |
 | _binder_       | ::=   | _identifier_ [``:`` _type_]{.opt}                                             |                      |

doc/spec/tour.kk.md

@@ -1909,9 +1909,59 @@ can make code that uses only linear effects more compact and efficient.
 
 ### Named and Scoped Handlers { #sec-namedh; }
 
-~ Todo
-See `samples/named-handlers`.
-~
+Named handlers allow us to define multiple handlers for the same effect that are lexically distinct from one another. For example, to define a handler for managing a file, we can write:
+```unchecked
+named effect file
+  fun read-line() : string   // `:(file)   -> <exn> a`
+
+// a (named) handler instance for files
+fun file(fname, action) 
+  var content := read-text-file(fname.path).lines
+  with f <- named handler 
+    fun read-line() 
+      match content  
+        Nil -> "" 
+        Cons(x,xx) -> { content := xx; x }
+  action(f)
+
+pub fun main() 
+  with f1 <- file("package.yaml")
+  with f2 <- file("stack.yaml")
+  println( f1.read-line() ++ "\n" ++ f2.read-line() )
+```
+This allows us to have two separate handlers for the same effect, and to use them in the same scope. The `named` keyword is used to define a handler instance, and the `with` statement is used to bind a handler instance to a variable. The handler instance can then be used as a regular handler, and it can be passed to other functions. 
+
+When used with handlers that involve multiple resumptions, you must be careful to ensure that the handler instance does not escape the scope of the resumption. For example, the following code is incorrect, and will fail at runtime:
+
+```unchecked
+fun wrong-escape1() 
+  with f <- file("stack.yaml")
+  f
+
+pub fun test() 
+  val f = wrong-escape1()
+  f.read-line.println
+```
+
+To ensure that the handler instance does not escape, you can mark the effect as a scoped effect. 
+
+```unchecked
+named scoped effect file<s::S> 
+  fun read-line() : string  // `: (f : file<s>) -> scope<s> string`
+
+// a handler instance for files
+fun file(fname : string, action : forall<s> file<s> -> <scope<s>|e> a ) : e a 
+  var i := 0
+  with f <- named handler 
+    fun read-line()
+      i := i + 1
+      (fname ++ ": line " ++ i.show)
+  action(f)
+``` 
+
+When creating the file the function `file` quantifies the `action` function by a polymorphic scope `s`, and connects that to the scope of the `file` instance passed to the `action`. Each action is guaranteed to not escape the scope of the action method due to the scope polymorphism. Scope types which are recognized by the `::S` kind annotation are not limited to just effect handlers, and can be used with other variables. See the [``samples/named-handlers``][named-handlers] directory on github or in your Koka installation for more complex examples of both named handlers and scoped effects and types.
+
+[named-handlers]: https://github.com/koka-lang/koka/tree/master/samples/named-handlers {target='_top'}
 
 ## FBIP: Functional but In-Place { #sec-fbip; }
 
@@ -1927,15 +1977,27 @@ describe loops in terms of regular function calls, reuse analysis lets us
 describe in-place mutating imperative algorithms in a purely functional
 way (and get persistence as well).
 
-~ Note
-FBIP is still active research. In particular we'd like to add ways to add
-annotations to ensure reuse is taking place.
-~
+Koka has a few keywords for guaranteeing that a function is optimized by the compiler.
+
+The `fip` keyword is the most restrictive and guarantees that a function is fully optimized by the compiler to use in-place mutation when possible.
+Higher order functions, or other variables used multiple times in a `fip` function must be marked as borrowed using the `^` prefix on their name (eg. `^f`). 
+Borrowed parameters cannot be passed as owned parameters to functions or constructors, cannot be matched destructively, and cannot be returned. 
+
+The `tail` keyword guarantees that a function is tail-recursive. These functions will not use stack space.
+
+The `fbip` keyword guarantees that a function is optimized by the compiler to use in-place mutation when possible.
+However, unlike `fip`, `fbip` allows for deallocation, and also allows for non tail calls, which means these functions can use non-constant stack space.
+
+Both `fip` and `fbip` can allow for a constant amount of allocation using `fip(n)` or `fbip(n)` where `n` is the number of constructor allocations allowed.
+This allows them to be used in insertion functions for datastructures, where at least one constructor for the inserted element is necessary.
+
+Following are a few examples of the techniques of FBIP in action. 
+For more information about the restrictions for `fip` and the new keywords, see
+the recent papers: [@Lorenzen:fip;@Lorenzen:fip-t]
 
 ### Tree Rebalancing
 
-As an example, we consider
-insertion into a red-black tree [@guibas1978dichromatic].
+As an example, consider insertion into a red-black tree [@guibas1978dichromatic]. 
 A polymorphic version of this example is part of the [``samples``][samples] directory when you have
 installed &koka; and can be loaded as ``:l`` [``samples/basic/rbtree``][rbtree].
 We define red-black trees as:
@@ -1955,13 +2017,13 @@ balanced. When inserting nodes, the invariants need to be maintained by
 rebalancing the nodes when needed. Okasaki's algorithm [@Okasaki:rbtree]
 implements this elegantly and functionally:
 ```unchecked
-fun balance-left( l : tree, k : int, v : bool, r : tree ): tree
+fbip(1) fun balance-left( l : tree, k : int, v : bool, r : tree ): tree
   match l
     Node(_, Node(Red, lx, kx, vx, rx), ky, vy, ry)
       -> Node(Red, Node(Black, lx, kx, vx, rx), ky, vy, Node(Black, ry, k, v, r))
     ...
 
-fun ins( t : tree, k : int, v : bool ): tree
+fbip(1) fun ins( t : tree, k : int, v : bool ): tree  
   match t
     Leaf -> Node(Red, Leaf, k, v, Leaf)
     Node(Red, l, kx, vx, r)
@@ -2000,7 +2062,7 @@ type tree
   Tip
   Bin( left: tree, value : int, right: tree )
 
-fun tmap-inorder( t : tree, f : int -> int ) : tree
+fbip fun tmap-inorder( t : tree, f : int -> int ) : tree
   match t
     Bin(l,x,r) -> Bin( l.tmap-inorder(f), f(x), r.tmap-inorder(f) )
     Tip        -> Tip
@@ -2090,7 +2152,7 @@ We start our traversal by going downward into the tree with an empty
 visitor, expressed as `tmap(f, t, Done, Down)`:
 
 ```
-fun tmap( f : int -> int, t : tree, visit : visitor, d : direction )
+fip fun tmap( f : int -> int, t : tree, visit : visitor, d : direction )
   match d
     Down -> match t     // going down a left spine
       Bin(l,x,r) -> tmap(f,l,BinR(r,x,visit),Down) // A

support/pygments/koka.py

@@ -26,18 +26,18 @@ class KokaLexer(RegexLexer):
     keywords = [
         'infix', 'infixr', 'infixl',
         'module', 'import', 'as',
-        'pub', 'abstract',
+        'pub', 'abstract', 'ctx'
         'type', 'struct', 'alias', 'effect', 'con',
         'forall', 'exists', 'some',
         'fun', 'fn', 'val', 'var', 'extern',
         'if', 'then', 'else', 'elif', 
         'match', 'return', 'with', 'in',
         'handle', 'handler', 'mask',
         'ctl', 'final', 'raw',
-        'override', 'named',
+        'override', 'named', 'scoped',
         'interface', 'break', 'continue', 'unsafe',
         'co', 'rec', 'open', 'extend', 'behind',
-        'linear', 'value', 'reference', 
+        'linear', 'value', 'reference',
         'inline', 'noinline'
     ]