package body FILO.FS.NullFS is

   Global_NullFS : NullFS_Type := (
      State => Unmounted
   );

   procedure Mount
      (Item : in out NullFS_Type;
       Success : out Boolean)
   is
   begin
      Success := True;
      Item.State := Mounted;
   end Mount;

   procedure Open
      (Item    : in out NullFS_Type;
       Path    : in     String;
       Success : out    Boolean)
   is
   begin
      Success := True;
      Item.State := File_Open;
   end Open;

   procedure Read
      (Item    : in out NullFS_Type;
       Buffer  : in out Buffer_Type;
       Offset  : in     Natural;
       Success : out    Boolean)
   is
   begin
      Success := True;
      null;
   end Read;

   procedure Close 
      (Item : in out NullFS_Type;
       Success : out Boolean)
   is
   begin
      Success := True;
      Item.State := Mounted;
   end Close;

   ---------------------------------------------------------------------A

   function To_Int (Success : Boolean) return Interfaces.C.int is
      (if Success then 1 else 0);

   function C_Mount return Interfaces.C.int
   is
      Success : Boolean;
   begin
      Mount(Global_NullFS, Success);
      return To_Int (Success);
   end C_Mount;

   function C_Read 
      (buf : System.Address;
       len : Interfaces.C.int)
   return Interfaces.C.int
      with SPARK_Mode => Off
   is
      use FILO.FS;
      Buffer : Buffer_Type (0 .. Integer(len) - 1) with Address => buf;
      Offset : constant Natural := Natural(File_Pos);
      Success : Boolean;
   begin
      Read (Global_NullFS, Buffer, Offset, Success);
      if Success then
         Set_File_Pos (File_Length (Offset + Buffer'Length));
      end if;
      return To_Int (Success);
      
   end C_Read;

   function C_Dir
      (Path : Interfaces.C.Strings.chars_ptr)
   return Interfaces.C.int
      with SPARK_Mode => Off
   is
      use Interfaces.C.Strings;
      Success : Boolean;
   begin
      Open (Global_NullFS, Value (Path), Success);
      return To_Int (Success);
   end C_Dir;

   function C_Close return Interfaces.C.int
      with SPARK_Mode => Off
   is
      Success : Boolean;
   begin
      Close (Global_NullFS, Success);
      return To_Int (Success);
   end C_Close;

end FILO.FS.NullFS;