DEFINITION MODULE INT128 [ZTYPE];

(* 128-bit Integer Numbers *) 


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


(* INT128 type *)

TYPE
    INT128 = OPAQUE RECORD
        value : ARRAY 16 OF OCTET; (* 128 bits *)
    END; (* INT128 *)


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


(* Range *) 

CONST [TMIN] minValue =
    { 0FFH, 0FFH, 0FFH, 0FFH, 0FFH, 0FFH, 0FFH, 0FFH,
      0FFH, 0FFH, 0FFH, 0FFH, 0FFH, 0FFH, 0FFH, 0FFH };
(* Smallest value of type INT128.
   This value is bound to TMIN for type INT128. *) 

CONST [TMAX] maxValue =
    {    0,    0,    0,    0,    0,    0,    0,    0,
      0FFH, 0FFH, 0FFH, 0FFH, 0FFH, 0FFH, 0FFH, 0FFH };
(* Largest value of type INT128.
   This value is bound to TMAX for type INT128. *)


(* Literal assignment *)

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


(* Type conversions *)

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

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

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

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


(* Monadic arithmetic operations *) 

PROCEDURE [ABS] abs ( n : INT128 ) : INT128;
(* Returns the absolute value of INT128 value n.
   This function is bound to pervasive function ABS for type INT128. *)

PROCEDURE [NEG] neg ( n : INT128 ) : INT128;
(* Returns the sign reversed value of INT128 value n.
   This function is bound to the unary minus operator for type INT128. *)

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


(* Dyadic arithmetic operations *) 

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

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

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

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


(* Relational operations *) 

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

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

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


(* Scalar conversion primitives *)

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

PROCEDURE [TO] toSXF ( n : INT128; VAR s : ARRAY OF CHAR );
(* Converts INT128 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 : INT128; CONST s : ARRAY OF CHAR );
(* Converts a string in scalar exchange format to an INT128 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 : INT128 );
(* Reads the textual representation of an INT128 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 an INT128 argument. *)

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

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

END INT128.