Abstract Types

Kind 2 supports Lustre’s abstract types, which are user-declared types without definitions. Abstract types are declared with the syntax type <name>. Below is a simple Lustre file that declares an identity node that takes an input of (abstract) type T and returns an output of type T equal to the input.

type T;
function id_T (x: T) returns (y: T);
let
    y = x;
tel

In Kind 2, all abstract types have infinite domains. As a result, assumptions that constrain an abstract type to a finite domain are inconsistent (such an example is shown in the following code block).

type T;
function id_T (x: T) returns (y: T);
con
    assume forall (x: T) (forall (y: T) x = y);
noc
let
    y = x;
tel

Thus, users should exercise caution with assumptions involving quantification over variables with abstract types.