DEFINITION MODULE BS128 [SetType];

(* 128-bit Bitset *)

FROM FileIO IMPORT File; (* required for IO *)


(* BS128 type *)

TYPE
    BS128 = OPAQUE RECORD
        ARRAY 16 OF OCTET; (* 128 bits *)
    END; (* BS128 *)


(* Literal assignment *)

PROCEDURE [:=] assign ( VAR assignTo : BS128;
                        elements     : VARIADIC OF CARDINAL );
(* Assigns a variadic list of values of type CARDINAL to BS128 assignTo.
   This procedure is bound to the := operator for literal assignment. *)


(* accessor *)

PROCEDURE [.] isElement ( CONST set : BS128; element : CARDINAL ) : BOOLEAN;
(* Returns TRUE if element is an element of BS128 set, otherwise FALSE.
   This function is bound to the array operator [ ] and the IN operator
   for rvalues of type BS128. *)


(* mutator *)

PROCEDURE [!] storeValue ( CONST set : BS128;
                           element   : CARDINAL;
                           value     : BOOLEAN );
(* Includes character element in BS128 set if value is TRUE, otherwise
   removes it from set. This procedure is bound to the array operator [ ]
   for lvalues of type BS128. *)


(* counter *)

PROCEDURE [COUNT] elementCount ( CONST set : BS128 ) : CARDINAL;
(* Returns the number of elements in BS128 set. This function is bound
   to pervasive function COUNT for type BS128. *)


(* Dyadic set operations *) 

PROCEDURE [+] union ( CONST set1, set2 : BS128 ) : BS128;
(* Returns the union of BS128 values set1 and set2.
   This function is bound to the + operator for type BS128. *)

PROCEDURE [-] diff ( CONST set1, set2 : BS128 ) : BS128;
(* Returns the set difference of BS128 values set1 and set2.
   This function is bound to the - operator for type BS128. *)

PROCEDURE [*] intersection ( set1, set2 : BS128 ) : BS128;
(* Returns the intersection of BS128 values set1 and set2.
   This function it bound to the * operator for type BS128. *)

PROCEDURE [/] symdiff ( set1, set2 : BS128 ) : BS128;
(* Returns the symmetric set difference of BS128 values set1 and set2.
   This function is bound to the / operator for type BS128. *)


(* Relational operations *)

PROCEDURE [=] isEqual ( set1, set2 : BS128 ) : BOOLEAN;
(* Returns TRUE if BS128 values set1 and set2 are equal, otherwise FALSE.
   This function is bound to operators = and # for type BS128. *)

PROCEDURE [<] isSubset ( set1, set2 : BS128 ) : BOOLEAN;
(* Returns TRUE if BS128 set1 is a true subset of set2, otherwise FALSE.
   This function is bound to operators < and >= for type BS128. *)

PROCEDURE [>] isSuperset ( set1, set2 : BS128 ) : BOOLEAN;
(* Returns TRUE if BS128 set1 is a true superset of set2, otherwise FALSE.
   This function is bound to operators > and <= for type BS128. *)


(* IO operations *)

(* The EBNF for the textual representation of BS128 values is:
    bitsetValue : simpleFormat | compactFormat | bitGroupFormat ;
    simpleFormat : bit+ ;
    compactFormat : base16Digit+ ;
    bitGroupFormat : "{" bit+ ( groupSeparator? bit+ )* "}" ;
    groupSeparator : " " | "." ;
    bit  : "0" | "1" ;
    base16Digit : "0" .. "9" | "A" .. "F" ;
   The number of bits shown is equal to the bitwidth of the BS128 type. *)

PROCEDURE Read ( infile : File; VAR set : BS128 );
(* Reads the textual representation of a BS128 value from stream infile
   - any leading whitespace is skipped
   - any remaining characters that are part of the value being read are
     removed from infile
   - the textual representation of the value read is assigned to set
   - the file status is set to any of:
     success, outOfRange, wrongFormat, endOfLine, or endOfInput. This
   procedure is substituted for invocations of READ with a BS128 argument. *)

PROCEDURE Write ( outfile : File; CONST set : BS128 );
(* Writes the value of CHARSET set in simple format to stream outfile. This
   procedure is substituted for invocations of WRITE with a BS128 argument.*)

PROCEDURE WriteF ( outfile      : File;
                   CONST fmtStr : ARRAY OF CHAR;
                   items        : VARIADIC OF CONST BS128 );
(* Writes a formatted textual representation of one or more BS128 values to
   output stream outfile. The output format is determined by fmtStr. This
   procedure is substituted for invocations of WRITEF with one or more
   BS128 arguments. *)

END BS128.