First pass on polymorphic contracts and user types documentation

kind2-mc · Jan 21, 2025 · 03b7311 · 03b7311
1 parent 33d6499
commit 03b7311
Show file tree

Hide file tree

Showing 4 changed files with 97 additions and 3 deletions.
diff --git a/doc/usr/source/2_input/1_lustre.rst b/doc/usr/source/2_input/1_lustre.rst
@@ -1206,7 +1206,7 @@ For a polymorphic node to be well-typed, it must be meaningful for *any* type in
 This type of polymorphism is called *parametric polymorphism*, and is also sometimes referred to as 
 *generics* in general-purpose programming languages.
 
-To illustrate these semantics, even though the ``+`` operator is overloaded between 
+To illustrate these semantics, even though the ``+`` operator is overloaded between types
 ``int -> int -> int`` and ``real -> real -> real``, 
 the following polymorphic node will give a type error, as it cannot be instantiated with any type.
 
@@ -1220,4 +1220,69 @@ the following polymorphic node will give a type error, as it cannot be instantia
 
 Note that polymorphic nodes can have ``check(.)`` statements just as non-polymorphic nodes.
 When checking properties of polymorphic nodes at the top level, the type parameters are interpreted 
-as abstract types.
+as abstract types.
+
+Polymorphic contracts
+---------------------
+In addition to polymorphic nodes, Kind 2 also supports polymorphic contracts. 
+The first way of accomplishing this is by using a polymorphic contract definition,
+such as ``Stutter``, which states that the output ``y`` must either be equal to the input
+``x`` or the previous value of ``x``.
+
+.. code-block:: none
+
+   contract Stutter<<T>> (x: T) returns (y: T) ;
+   let
+      guarantee 
+        (y = x) or
+        (true -> (y = pre x));
+   tel
+
+Then, the polymorphic contract can be included in a node using an import statement, where
+the type arguments are provided (analogously to a polymorphic node declaration and 
+node call).
+
+.. code-block:: none
+
+   contract Stutter<<T>> (x: T) returns (y: T) ;
+   let
+      guarantee 
+        (y = x) or
+        (true -> (y = pre x));
+   tel
+
+   node N (x: int) returns (y: int);
+   (*@contract 
+      import Stutter<<int>>(x) returns (y);
+   *)
+   let
+      y = pre x;
+   tel
+
+
+   node P<<T>>(x: T) returns (y: T);
+   (*@contract 
+      import Stutter<<T>>(x) returns (y);
+   *)
+   let
+      y = pre x;
+   tel
+
+Above, node ``N`` instantiates the contract ``Stutter`` with type ``int``. 
+Node ``P`` demonstrates using a polymorphic contract declaration with a polymorphic 
+node. 
+
+Another way of specifying a polymorphic contract is by including it in the 
+node declaration with the ``(*@contract ... *)`` syntax.
+
+.. code-block:: none
+
+   node M<<T>>(x: int) returns (y: int);
+   (*@contract
+      guarantee 
+         (y = x) or
+         (true -> (y = pre x));
+   *)
+   let
+      y = pre x;
+   tel
diff --git a/doc/usr/source/2_input/7_abstract_types.rst b/doc/usr/source/2_input/7_abstract_types.rst
@@ -27,7 +27,7 @@ type ``T`` to have a finite domain.
     type T;
     function id_T (x: T) returns (y: T);
     (*@contract
-    assume forall (x:T) (forall (y: T) x = y);
+    assume forall (x: T) (forall (y: T) x = y);
     *)
     let
         y = x;

diff --git a/doc/usr/source/2_input/8_polymorphic_types.rst b/doc/usr/source/2_input/8_polymorphic_types.rst
@@ -0,0 +1,28 @@
+Polymorphic User Types
+======================
+
+Kind 2 supports **polymorphic user types**, 
+which are user-defined types that contain type parameters. 
+An example is a polymorphic user-defined ``Pair`` type, 
+shown below, declared as ``type Pair<<T; U>> = [T, U];``.
+
+A polymorphic user-defined type ``T`` is instantiated with ``T<<...>>``
+syntax (analogous to polymorphic nodes and node calls) 
+as in the following examples.
+
+.. code-block:: none
+    type Pair<<T; U>> = [T, U];
+
+    node SwapIntBool(x: Pair<<int; bool>>) returns (y: Pair <<bool; int>>)
+    let
+        y = {x.%1, x.%0};
+    tel
+
+    node SwapGeneric<<T; U>>(x: Pair<<T; U>>) returns (y: Pair <<U; T>>)
+    let
+        y = {x.%1, x.%0};
+    tel
+
+In other words, ``Pair`` (or any other user-defined polymorphic type) can 
+be viewed as as a ``type constructor`` which takes types as inputs 
+and returns a type.
diff --git a/doc/usr/source/index.rst b/doc/usr/source/index.rst
@@ -28,6 +28,7 @@ Table of Contents
     2_input/5_enums
     2_input/6_history_type
     2_input/7_abstract_types
+    2_input/8_polymorphic_types
     3_output/2_machine_readable
     3_output/3_exit_codes