DEFINITION MODULE ExampleVector [VTYPE];

(* Example definition of a vector ADT *)


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


(* component type *)

TYPE ComponentType IS REAL; (* arbitrary numeric type *)


(* ExampleVector type *)

TYPE
    ExampleVector = RECORD
        v1, v2, v3, v4, v5 : ComponentType;
    END;


(* monadic arithmetic operations *) 

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

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


(* dyadic arithmetic operations *) 

PROCEDURE [+] add ( v1, v2 : ExampleVector ) : ExampleVector; 
(* Adds vectors v1 and v2 and returns the result.
   This function is bound to the + operator for type ExampleVector. *)

PROCEDURE [-] sub ( v1, v2 : ExampleVector ) : ExampleVector; 
(* Subtracts vectors v2 from v1 and returns the result.
   This function is bound to the - operator for type ExampleVector. *)

PROCEDURE dot ( v1, v2 : ExampleVector ) : ComponentType;
(* Calculates the dot product of vectors v1 and v2 and returns the result. *)

PROCEDURE scalar ( a : ComponentType; v : ExampleVector ) : ExampleVector; 
(* Performs a scalar division of vector v and component a,
   returns the resulting vector. *)


(* relational operations *) 

PROCEDURE [=] isEqual ( v1, v2 : ExampleVector ) : BOOLEAN;
(* Returns TRUE is vectors v1 and v2 are equal, otherwise FALSE.
   This function is bound to operators = and # for type ExampleVector. *)


(* IO operations *)

PROCEDURE Read( infile : File; VAR v : ExampleVector );
(* Reads the textual representation of an ExampleVector value from 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 v
   - the file status is set to any of:
     success, outOfRange, wrongFormat, endOfLine, or endOfInput.
   This procedure is substituted for invocations of READ with an argument of
   type ExampleVector. *)

PROCEDURE Write( outfile : File; CONST v : ExampleVector );
(* Writes the textual representation of vector v to outfile. This procedure
   is substituted for invocations of WRITE with an ExampleVector argument. *)

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

END ExampleVector.