with System;
with Interfaces.C;
with Interfaces.C.Strings;

use Interfaces.C;

generic

   type T (<>) is private;

   with function Is_Mounted (State : T) return Boolean is <>;
   with function Is_Open (State : T) return Boolean is <>
   with
      Post => (if Is_Open'Result then Is_Mounted (State));

   Initial : T;

   with procedure Mount
     (State    : in out T;
      Part_Len : in     Partition_Length;
      Success  :    out Boolean)
   is <>
   with
      Pre => not Is_Mounted (State),
      Post => Success = Is_Mounted (State);

   with procedure Open
     (State       : in out T;
      File_Len    :    out File_Length;
      File_Path   : in     String;
      Success     : out    Boolean)
   is <>
   with
      Pre => Is_Mounted (State) and not Is_Open (State),
      Post => Success = Is_Open (State);

   with procedure Close (State : in out T)
   is <>
   with
      Pre => Is_Open (State),
      Post => Is_Mounted (State);

   with procedure Read
     (State    : in out T;
      File_Pos : in out File_Offset;
      Buf      :    out Buffer_Type;
      Len      :    out Natural)
   is <>
   with
      Pre => Is_Open (State),
      Post => Is_Open (State);

package FILO.FS.VFS
with
   Convention => C
is

   function C_Mount return int;

   function C_Open (File_Path : Strings.chars_ptr) return int;
   procedure C_Close;
   
   function C_Read (Buf : System.Address; Len : int) return int;

end FILO.FS.VFS;