package FILO.FS.ISO9660 is

   type T is private;

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

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

   procedure Open
     (State       : in out T;
      File_Len    :    out File_Length;
      File_Type   :    out FS.File_Type;
      File_Name   : in     String;
      In_Root     : in     Boolean;
      Success     : out    Boolean)
   with
      Pre => Is_Mounted (State) and File_Name'Length <= Natural'Last - 3,
      Post => (if Success then Is_Open (State) else Is_Mounted (State));

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

   pragma Warnings
     (GNATprove, Off, """State"" is not modified*",
      Reason => "It's `in out' to fulfill common interface.");
   procedure Read
     (State    : in out T;
      File_Pos : in out File_Offset;
      Buf      :    out Buffer_Type;
      Len      :    out Natural)
   with
      Relaxed_Initialization => Buf,
      Pre => Is_Open (State) and Buf'Length > 0,
      Post => Is_Open (State) and Buf'Initialized;
   pragma Warnings (GNATprove, On, """State"" is not modified*");

private
   type State is (Unmounted, Mounted, File_Opened);

   FSBlock_Size : constant := 2048;
   subtype FSBlock_Length is Index_Type range 0 .. FSBlock_Size;
   subtype FSBlock_Index is Index_Type range 0 .. FSBlock_Size - 1;

   type FSBlock_Count is range 0 .. 2 ** 32 - 1;
   subtype FSBlock is FSBlock_Count range 0 .. FSBlock_Count'Last - 1;
   type FSBlock_Logical is new FSBlock;

   type FS_Record is record
      Block    : FSBlock := 0;
      Offset   : FSBlock_Length := 0;
      Size     : FSBlock_Length := 0;
   end record
   with
      Dynamic_Predicate =>
         Size <= FSBlock_Size - Offset;

   subtype Directory_Record_Range is Index_Type range 0 .. 32;
   subtype Directory_Record is Buffer_Type (Directory_Record_Range);
   subtype Directory_Record_Offset is FSBlock_Index
      range 0 .. FSBlock_Size - Directory_Record'Length;

   -- We'll use the absolute position of the dir record
   subtype Inode_Index is FS_Record
   with
      Dynamic_Predicate =>
         Inode_Index.Size >= Directory_Record'Length;
   type Inode_Length is range 0 .. FSBlock_Count'Last * FSBlock_Size;

   type Mount_State is record
      Part_Len    : Partition_Length := 0;
      Root_Inode  : Inode_Index := (Size => Directory_Record'Length, others => <>);
   end record;

   type Extent is record
      Start : FSBlock := 0;
      Count : FSBlock_Count := 0;
   end record
   with
      Dynamic_Predicate =>
         Start <= FSBlock_Count'Last - Count;

   type Extent_Range is range 0 .. 0; -- Linux allows 100 "file sections"
   type Extents is array (Extent_Range) of Extent;

   type Inode_Info is record
      I        : Inode_Index := (Size => Directory_Record'Length, others => <>);
      Mode     : File_Type := File_Type'First;
      Size     : Inode_Length := 0;
      Extents  : ISO9660.Extents := (Extent_Range => (others => <>));
   end record;

   type T is record
      Static   : Mount_State  := (others => <>);
      S        : State;
      Inode    : Inode_Info := (others => <>);
      Cur_Dir  : Inode_Index := (Size => Directory_Record'Length, others => <>);
   end record;

end FILO.FS.ISO9660;