DEFINITION MODULE Unsigned31 [ZTYPE];

(* Unsigned Integer Subrange Type With Values from 1 to 31 *) 


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


(* Unsigned31 type *)

TYPE
    Unsigned31 = OPAQUE RECORD
        value : OCTET; (* 8 bits *)
    END; (* Unsigned31 *)


(* Z-Type bindings to operators, pervasives and primitives: *)


(* Range *) 

CONST [TMIN] minValue = 1;
(* Smallest value of type Unsigned31.
   This value is bound to TMIN for type Unsigned31. *) 

CONST [TMAX] maxValue = 31;
(* Largest value of type Unsigned31.
   This value is bound to TMAX for type Unsigned31. *)


(* Literal assignment *)

PROCEDURE [:=] assign ( VAR assignTo : Unsigned31; literal : ARRAY OF CHAR );
(* Converts string literal to a Unsigned31 value and assigns it to assignTo.
   This procedure is bound to the := operator for literal assignment. *)


(* Type conversions *)

PROCEDURE [::] toCARD  ( n : Unsigned31 ) : CARDINAL;
(* Converts Unsigned31 value n to a CARDINAL value and returns it.
   This function is bound to the :: operator for Unsigned31 to CARDINAL
   conversion. *)

PROCEDURE [::] toINT ( n : Unsigned31 ) : INTEGER; 
(* Converts Unsigned31 value n to an INTEGER value and returns it.
   This function is bound to the :: operator for Unsigned31 to INTEGER
   conversion. *)

PROCEDURE [::] fromCARD  ( n : CARDINAL ) : Unsigned31;
(* Converts CARDINAL value n to a Unsigned31 value and returns it.
   This function is bound to the :: operator for CARDINAL to Unsigned31
   conversion. *)

PROCEDURE [::] fromINT  ( n : INTEGER ) : Unsigned31;
(* Converts INTEGER value n to a Unsigned31 value and returns it.
   This function is bound to the :: operator for INTEGER to Unsigned31
   conversion. *)


(* Monadic arithmetic operations *)

PROCEDURE [ODD] odd ( n : Unsigned31 ) : BOOLEAN;
(* Returns TRUE if Unsigned31 value n is odd, otherwise FALSE.
   This function is bound to pervasive function ODD for type Unsigned31. *)


(* Dyadic arithmetic operations *) 

PROCEDURE [+] add ( n1, n2 : Unsigned31 ) : Unsigned31;
(* Adds Unsigned31 values n1 and n2 and returns the result.
   This function is bound to the + operator for type Unsigned31. *)

PROCEDURE [-] sub ( n1, n2 : Unsigned31 ) : Unsigned31;
(* Subtracts Unsigned31 value n2 from n1 and returns the result.
   This function is bound to the - operator for type Unsigned31. *)

PROCEDURE [*] multiply ( n1, n2 : Unsigned31 ) : Unsigned31;
(* Multiplies Unsigned31 values n1 and n2 and returns the result.
   This function it bound to the * operator for type Unsigned31. *)

PROCEDURE [/] divide ( n1, n2 : Unsigned31 ) : Unsigned31;
(* Divives Unsigned31 value n1 by n2 and returns the result.
   This function is bound to the / operator for type Unsigned31. *)


(* Relational operations *) 

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

PROCEDURE [<] isLess ( n1, n2 : Unsigned31 ) : BOOLEAN;
(* Returns TRUE if Unsigned31 value n1 is less than n2, otherwise FASLE.
   This function is bound to operators < and >= for type Unsigned31. *)

PROCEDURE [>] isGreater ( n1, n2 : Unsigned31 ) : BOOLEAN;
(* Returns TRUE if Unsigned31 value n1 is greater than n2, otherwise FALSE.
   This function is bound to operators > and <= for type Unsigned31. *)


(* Scalar conversion primitives *)

CONST digitCapacity = 2; (* maximum digits in native format *)

PROCEDURE [TO] toSXF ( n : Unsigned31; VAR s : ARRAY OF CHAR );
(* Converts Unsigned31 value n to a string in scalar exchange format.
   This procedure is used to synthesise conversions to other scalar types
   when no direct conversion path exists. *)

PROCEDURE [FROM] fromSXF ( VAR n : Unsigned31; CONST s : ARRAY OF CHAR );
(* Converts a string in scalar exchange format to a Unsigned31 value.
   This procedure is used to synthesise conversions from other scalar types
   when no direct conversion path exists. *)


(* IO operations *)

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

PROCEDURE Write( outfile : File; n : Unsigned31 );
(* Writes the textual representation of value n to stream outfile.
   This procedure is substituted for invocations of WRITE with a Unsigned31
   argument. *)

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

END Unsigned31.