From d5ee3259dbd122c7db92be64cc2a377024d8d98e Mon Sep 17 00:00:00 2001
From: Benjamin Canou <benjamin@canou.fr>
Date: Mon, 18 Jun 2018 13:24:51 +0200
Subject: [PATCH] Michelson: update documentation

---
 docs/whitedoc/michelson.rst | 55 ++++++++++++++++++++++++++++++++++---
 1 file changed, 51 insertions(+), 4 deletions(-)

diff --git a/docs/whitedoc/michelson.rst b/docs/whitedoc/michelson.rst
index 4f4036daa..79f2dbbec 100644
--- a/docs/whitedoc/michelson.rst
+++ b/docs/whitedoc/michelson.rst
@@ -776,16 +776,37 @@ Operations on strings
 ~~~~~~~~~~~~~~~~~~~~~
 
 Strings are mostly used for naming things without having to rely on
-external ID databases. So what can be done is basically use string
-constants as is, concatenate them and use them as keys.
+external ID databases. They are restricted to the printable subset of
+7-bit ASCII, plus some escaped characters (see section on
+constants). So what can be done is basically use string constants as
+is, concatenate or splice them, and use them as keys.
+
 
 -  ``CONCAT``: String concatenation.
 
 ::
 
-    :: string : string : 'S   -> string : 'S
+    :: string list : 'S   -> string : 'S
 
-    > CONCAT / s : t : S  =>  (s ^ t) : S
+    > CONCAT / {} : S  =>  "" : S
+    > CONCAT / { s ; <ss> } : S  =>  (s ^ r) : S
+       where CONCAT / { <ss> } : S  =>  r : S
+
+-  ``SIZE``: number of characters in a string.
+
+::
+
+     :: string : 'S   ->   nat : 'S
+
+-  ``SLICE``: String access.
+
+    :: nat : nat : string : 'S   ->  option string : 'S
+
+    > SLICE / offset : length : s : S  =>  Some ss : S
+       where ss is the substring of s at the given offset and of the given length
+         iff offset and (offset + length) are in bounds
+    > SLICE / offset : length : s : S  =>  None  : S
+         iff offset or (offset + length) are out of bounds
 
 -  ``COMPARE``: Lexicographic comparison.
 
@@ -1462,6 +1483,32 @@ the wild and untyped outside world.
 
      :: bytes : 'S   ->   option 'a : 'S
 
+-  ``CONCAT``: Byte sequence concatenation.
+
+::
+
+    :: bytes list : 'S   -> bytes : 'S
+
+    > CONCAT / {} : S  =>  0x : S
+    > CONCAT / { s ; <ss> } : S  =>  (s ^ r) : S
+       where CONCAT / { <ss> } : S  =>  r : S
+
+-  ``SIZE``: size of a sequence of bytes.
+
+::
+
+     :: bytes : 'S   ->   nat : 'S
+
+-  ``SLICE``: Bytes access.
+
+    :: nat : nat : bytes : 'S   -> option string : 'S
+
+    > SLICE / offset : length : s : S  =>  Some ss : S
+       where ss is the substring of s at the given offset and of the given length
+         iff offset and (offset + length) are in bounds
+    > SLICE / offset : length : s : S  =>  None : S
+         iff offset or (offset + length) are out of bounds
+
 -  ``COMPARE``: Lexicographic comparison.
 
 ::