class interface KL_PLATFORM

feature(s) from GENERAL
   --  Access :

   generating_type: STRING
      --  Name of current object's generating type (type of 
      --  which it is a direct instance).


   generator: STRING
      --  Name of current object's generating class (base class
      --  of the type of which it is a direct instance).


   stripped (other: GENERAL): like other
      --  Newly created object with fields copied from current object,
      --  but limited to attributes of type of other.

      require
         conformance: conforms_to(other)
      ensure
         stripped_to_other: Result.same_type(other)

feature(s) from GENERAL
   --  Status report :

   conforms_to (other: GENERAL): BOOLEAN
      --  Is dynamic type of Current a descendant of dynamic type of
      --  other ?
      --  
      --  Note: because of automatic conversion from expanded to reference
      --  type when passing argument other, do not expect a correct  
      --  behavior with  expanded types.

      require
         not is_expanded_type;
         other_not_void: other /= Void

   same_type (other: GENERAL): BOOLEAN
      --  Is type of current object identical to type of other ?

      require
         not is_expanded_type;
         other_not_void: other /= Void
      ensure
         definition: Result = (conforms_to(other) and other.conforms_to(Current))

feature(s) from GENERAL
   --  Comparison :

   equal (some: ANY; other: like some): BOOLEAN
      --  Are some and other both Void or attached to
      --  objects considered equal ?

      ensure
         definition: Result = (some = Void and other = Void) or else some /= Void and other /= Void and then some.is_equal(other)

   is_equal (other: like Current): BOOLEAN
      --  Is other attached to an object considered equal to 
      --  current object ?

      require
         other_not_void: other /= Void
      ensure
         consistent: standard_is_equal(other) implies Result;
         symmetric: Result implies other.is_equal(Current)

   standard_equal (some: ANY; other: like some): BOOLEAN
      --  Are some and other both Void or attached to
      --  field-by-field objects of the same type ?
      --  Always use the default object comparison criterion.

      ensure
         definition: Result = (some = Void and other = Void) or else some /= Void and other /= Void and then some.standard_is_equal(other)

   standard_is_equal (other: like Current): BOOLEAN
      --  Are Current and other field-by-field identical?

      require
         other /= Void
      ensure
         symmetric: Result implies other.standard_is_equal(Current)

feature(s) from GENERAL
   --  Deep Comparison :

   deep_equal (some: ANY; other: like some): BOOLEAN
      --  Are some and other either both Void or attached to 
      --  recursively isomorphic object structures ?

      ensure
         shallow_implies_deep: standard_equal(some,other) implies Result;
         same_type: Result implies some.same_type(other);
         symmetric: Result implies deep_equal(other,some)

feature(s) from GENERAL
   --  Deep Comparison :

   standard_deep_equal (some: ANY; other: like some): BOOLEAN
      --  Are some and other either both Void or attached to 
      --  recursively isomorphic object structures ?

      ensure
         shallow_implies_deep: standard_equal(some,other) implies Result;
         same_type: Result implies some.same_type(other);
         symmetric: Result implies deep_equal(other,some)

   is_deep_equal (other: like Current): BOOLEAN
      --  Is Current recursively isomorph with other ?

      require
         other_not_void: other /= Void
      ensure
         symmetric: Result implies other.is_deep_equal(Current)

feature(s) from GENERAL
   --  Duplication :

   clone (other: ANY): like other
      --  When argument other is Void, return Void
      --  otherwise return other.twin.

      ensure
         equal: equal(Result,other)

   twin: like Current
      --  Return a new object with the dynamic type of Current.
      --  Before being returned, the new object is initialized using
      --  feature copy (Current is passed as the argument).
      --  Thus, when feature copy of GENERAL is not redefined, 
      --  twin has exactly the same behaviour as standard_twin.

      ensure
         equal: Result.is_equal(Current)

   copy (other: like Current)
      --  Update current object using fields of object attached
      --  to other, so as to yield equal objects.

      require
         other_not_void: other /= Void
      ensure
         is_equal: is_equal(other)

   standard_clone (other: ANY): like other
      --  Void if other is Void; otherwise new object 
      --  field-by-field identical to other. 
      --  Always use the default copying semantics.

      ensure
         equal: standard_equal(Result,other)

   standard_twin: like Current
      --  Return a new object with the dynamic type of Current.
      --  Before being returned, the new object is initialized using
      --  feature standard_copy (Current is passed as the argument).


   standard_copy (other: like Current)
      --  Copy every field of other onto corresponding field of 
      --  current object.

      require
         other_not_void: other /= Void
      ensure
         standard_is_equal(other)

feature(s) from GENERAL
   --  Deep Duplication :

   deep_clone (other: GENERAL): like other
      --  Void if other is Void: otherwise, new object structure 
      --  recursively duplicated from the one attached to other.

      ensure
         deep_equal: deep_equal(other,Result)

feature(s) from GENERAL
   --  Basic operations :

   default: like Current
      --  Default value of current type.


   default_pointer: POINTER
      --  Default value of type POINTER (avoid the need to
      --  write p.default for some p of type POINTER).

      ensure
         Result = Result.default

   default_rescue
      --  Handle exception if no Rescue clause.
      --  (Default: do nothing.)   


   do_nothing
      --  Execute a null action.


feature(s) from GENERAL
   --  Input and Output :

   io: STD_INPUT_OUTPUT
      --  Handle to standard file setup.
      --  To use the standard input/output file.
      --  Has type STD_FILES in ELKS 95.

      ensure
         Result /= Void

   std_input: STD_INPUT
      --  To use the standard input file.


   std_output: STD_OUTPUT
      --  To use the standard output file.


   std_error: STD_ERROR
      --  To use the standard error file.


feature(s) from GENERAL
   --  Object Printing :

   print (some: GENERAL)
      --  Write terse external representation of some on
      --  standard_output.
      --  To customize printing, one may redefine 
      --  fill_tagged_out_memory or out_in_tagged_out_memory (see 
      --  for example how it works in class COLLECTION).
      --  Not frozen in ELKS 95.


   print_on (file: OUTPUT_STREAM)
      --  Default printing of current object on a file.
      --  One may redefine fill_tagged_out_memory or 
      --  out_in_tagged_out_memory to adapt the behavior of 
      --  print_on.
      -- 


   tagged_out: STRING
      --  New string containing printable representation of current 
      --  object, each field preceded by its attribute name, a 
      --  colon and a space.


   out: STRING
      --  Create a new string containing terse printable 
      --  representation of current object.


   out_in_tagged_out_memory
      --  Append terse printable represention of current object
      --  in tagged_out_memory.


   tagged_out_memory: STRING

   fill_tagged_out_memory
      --  Append a viewable information in tagged_out_memory in 
      --  order to affect the behavior of out, tagged_out, etc.


feature(s) from GENERAL
   --  Basic named file handling :

   file_tools: FILE_TOOLS

   file_exists (path: STRING): BOOLEAN
      --  True if path is an existing readable file.

      require
         path /= Void

   remove_file (path: STRING)
      require
         path /= Void

   rename_file (old_path, new_path: STRING)
      require
         old_path /= Void;
         new_path /= Void

feature(s) from GENERAL
   --  Access to command-line arguments :

   argument_count: INTEGER
      --  Number of arguments given to command that started
      --  system execution (command name does not count).

      ensure
         Result >= 0

   argument (i: INTEGER): STRING
      --  i th argument of command that started system execution 
      --  Gives the command name if i is 0.

      require
         i >= 0;
         i <= argument_count
      ensure
         Result /= Void

   command_arguments: FIXED_ARRAY[STRING]
      --  Give acces to arguments command line including the
      --  command name at index 0.

      ensure
         not Result.empty

   get_environment_variable (name: STRING): STRING
      --  To get the value of a system environment variable
      --  (like "PATH" on Unix for example).
      --  Gives Void when system variable name is undefined.

      require
         name /= Void

feature(s) from GENERAL
   --  System calls and crashs :

   crash
      --  Print Run Time Stack and then exit with exit_failure_code.


   trace_switch (flag: BOOLEAN)
      --  May be used in combination with option "-trace" of
      --  command compile_to_c (see compile_to_c.hlp for
      --  details).


   system (system_command_line: STRING)
      --  To execute a system_command_line as for example, "ls -l" on UNIX.


   die_with_code (code: INTEGER)
      --  Terminate execution with exit status code code.
      --  Do not print any message.
      --  Note: you can use predefined exit_success_code or
      --  exit_failure_code as well as another code you need.


   exit_success_code: INTEGER

   exit_failure_code: INTEGER

feature(s) from GENERAL
   --  Maths constants :

   Pi: DOUBLE

   Evalue: DOUBLE

   Deg: DOUBLE
      --  Degrees/Radian


   Phi: DOUBLE
      --  Golden Ratio


feature(s) from GENERAL
   --  Character names :

   Ctrl_a: CHARACTER

   Ctrl_b: CHARACTER

   Ctrl_c: CHARACTER

   Ctrl_d: CHARACTER

   Ctrl_e: CHARACTER

   Ctrl_f: CHARACTER

   Ctrl_g: CHARACTER

   Ch_bs: CHARACTER

   Ch_tab: CHARACTER

   Ctrl_j: CHARACTER

   Ctrl_k: CHARACTER

   Ctrl_l: CHARACTER

   Ctrl_m: CHARACTER

   Ctrl_n: CHARACTER

   Ctrl_o: CHARACTER

   Ctrl_p: CHARACTER

   Ctrl_q: CHARACTER

   Ctrl_r: CHARACTER

   Ctrl_s: CHARACTER

   Ctrl_t: CHARACTER

   Ctrl_u: CHARACTER

   Ctrl_v: CHARACTER

   Ctrl_w: CHARACTER

   Ctrl_x: CHARACTER

   Ctrl_y: CHARACTER

   Ctrl_z: CHARACTER

   Ch_del: CHARACTER

feature(s) from GENERAL
   --  Should not exist :

   not_yet_implemented

feature(s) from GENERAL
   --  For ELS Compatibility :

   id_object (id: INTEGER): ANY
      --  Object for which object_id has returned id;
      --  Void if none.

      require
         id /= 0

   object_id: INTEGER
      --  Value identifying current reference object.

      require
         not is_expanded_type

feature(s) from GENERAL
   --  The Guru section :

   to_pointer: POINTER
      --  Explicit conversion of a reference into POINTER type.

      require
         not is_expanded_type

   is_expanded_type: BOOLEAN
      --  Target is not evaluated (Statically computed).
      --  Result is true if target static type is an expanded type.
      --  Useful for formal generic type.


   is_basic_expanded_type: BOOLEAN
      --  Target is not evaluated (Statically computed).
      --  Result is true if target static type is one of the 
      --  following types: BOOLEAN, CHARACTER, INTEGER, REAL,
      --  DOUBLE or POINTER.

      ensure
         Result implies is_expanded_type

   object_size: INTEGER
      --  Gives the size of the current object at first level 
      --  only (pointed-to sub-object are not concerned).  
      --  The result is given in number of CHARACTER.


feature(s) from GENERAL
   --  Implementation of GENERAL (do not use directly) :

   se_assigned_from (other: GENERAL): BOOLEAN
      --  To implement conforms_to (must only be called inside
      --  conforms_to because of VJRV rule).

      require
         not is_expanded_type

feature(s) from PLATFORM
   --  Maximum :

   Maximum_character_code: INTEGER
      --  Smallest and largest supported codes for CHARACTER values


   Maximum_integer: INTEGER
      --  Largest supported value of type INTEGER.

      ensure
         meaningful: Result >= 0

   Maximum_real: REAL
      --  Largest supported value of type REAL.

      ensure
         meaningful: Result >= 0.0

   Maximum_double: DOUBLE
      --  Largest supported value of type DOUBLE.

      ensure
         meaningful: Result >= Maximum_real

feature(s) from PLATFORM
   --  Minimum :

   Minimum_character_code: INTEGER
      --  Smallest supported code for CHARACTER values.


   Minimum_integer: INTEGER
      --  Smallest supported value of type INTEGER.

      ensure
         meaningful: Result <= 0

   Minimum_double: DOUBLE
      --  Smallest supported value of type DOUBLE.

      ensure
         meaningful: Result <= 0.0

   Minimum_real: REAL
      --  Smallest supported value of type REAL.

      ensure
         meaningful: Result <= 0.0

feature(s) from PLATFORM
   --  Bits :

   Boolean_bits: INTEGER
      --  Number of bits in a value of type BOOLEAN.

      ensure
         meaningful: Result >= 1

   Character_bits: INTEGER
      --  Number of bits in a value of type CHARACTER.

      ensure
         meaningful: Result >= 1;
         large_enough: 2 ^ Result >= Maximum_character_code

   Integer_bits: INTEGER
      --  Number of bits in a value of type INTEGER.

      ensure
         meaningful: Result >= 1

   Real_bits: INTEGER
      --  Number of bits in a value of type REAL.

      ensure
         meaningful: Result >= 1

   Double_bits: INTEGER
      --  Number of bits in a value of type DOUBLE.

      ensure
         meaningful: Result >= 1;
         meaningful: Result >= Real_bits

   Pointer_bits: INTEGER
      --  Number of bits in a value of type POINTER.



end of KL_PLATFORM