From 88e52b066d954f3c83a0d9c5dcbb5a83c981e67f Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Wed, 15 May 2024 19:09:12 -0500 Subject: [PATCH] Add history types user doc --- doc/usr/source/2_input/6_history_type.rst | 25 +++++++++++++++++++++++ doc/usr/source/index.rst | 1 + 2 files changed, 26 insertions(+) create mode 100644 doc/usr/source/2_input/6_history_type.rst diff --git a/doc/usr/source/2_input/6_history_type.rst b/doc/usr/source/2_input/6_history_type.rst new file mode 100644 index 000000000..39d72a290 --- /dev/null +++ b/doc/usr/source/2_input/6_history_type.rst @@ -0,0 +1,25 @@ + +History Types +============= + +In order to improve the expressivity of Kind 2's specification language, +the tool provides a built-in type constructor that allows users to +refer to an `unbounded` number of previous values of a stream. +Specifically, the unary type constructor ``history(x)``, that +takes a stream ``x`` of arbitrary type ``T`` as its single argument, +represents the set of all streams ``z`` of values of type ``T`` such that +at any time ``t >= 0``, there exists a ``k`` in the interval ``[0, t]`` such that +``z(t) = x(k)``. + +For instance, given a node with an input stream ``x`` and an output +stream ``y``, both with the same type, the property `the current value of stream y +equals the current value or a previous value of a stream x plus one` +can't be expressed in Lustre. However, using the type constructor +``history``, one can easily express the property as +``exists (z: history(x)) y=z+1``. + +Notice that ``history(x)`` denotes a refinement type, +suggesting its applicability wherever a type is expected in the model. +However, at present, the implementation restricts the use of the +type constructor ``history`` to the type of a quantified variable. +We plan to lift this restriction in future versions of Kind 2. diff --git a/doc/usr/source/index.rst b/doc/usr/source/index.rst index 8dce909bd..4f8f9a4d0 100644 --- a/doc/usr/source/index.rst +++ b/doc/usr/source/index.rst @@ -26,6 +26,7 @@ Table of Contents 2_input/3_machine_ints 2_input/4_refinement_types 2_input/5_enums + 2_input/6_history_type 3_output/2_machine_readable 3_output/3_exit_codes