package FILO.FS.Ext2 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_Path   : in     String;
      Success     : out    Boolean)
   with
      Pre => Is_Mounted (State) and not Is_Open (State),
      Post => Success = Is_Open (State);

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

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

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

   -- maximum block size is 64KiB (2^16):
   subtype Log_Block_Size is Positive range 10 .. 16;
   subtype Max_Block_Index is Index_Type range 0 .. 2 ** Log_Block_Size'Last - 1;

   -- Minimum ext2 block size is 1KiB (two 512B blocks)
   type FSBlock_Offset is new Block_Offset range 0 .. Block_Offset'Last / 2;
   type FSBlock_Logical is new Block_Offset range 0 .. Block_Offset'Last / 2;

   -- We use a 64KiB cache which fits at least one ext2 block. If a lower
   -- block size is encountered (likely), we partition the cache into up
   -- to 64 1KiB blocks.
   -- Cache entries can be used for blocks that map logical block offets
   -- to physical ones. Then we note the first logical block offset mapped
   -- by the cached block. Otherwise, we use their physical offset.
   type Cache_Label is new Unsigned_64;
   subtype Block_Cache_Index is Natural range 0 .. 63;
   type Cache_Label_Logical is array (Block_Cache_Index) of Boolean;
   type Cache_Label_Array is array (Block_Cache_Index) of Cache_Label;

   -- Same as the 12 direct + 3 indirect blocks times 4B:
   subtype Inode_Extents_Index is Natural range 0 .. 59;
   subtype Inode_Extents is Buffer_Type (Inode_Extents_Index);

   type Inode_Index is new Unsigned_32 range 1 .. Unsigned_32'Last;
   subtype Inode_Size is Positive range 128 .. Positive (Unsigned_16'Last);
   subtype Desc_Size  is Positive range  32 .. 2 ** 15; -- power-of-2 that fits in 16 bits

   type Inode_Type is (Dir, Regular, Link, Fast_Link);
   type Inode_Length is range 0 .. 2 ** 46;

   type Inode_Info is record
      Mode        : Inode_Type := Inode_Type'First;
      Size        : Inode_Length := 0;
      Use_Extents : Boolean := False;
      Inline      : Buffer_Type (Inode_Extents_Index) := (others => 16#00#);
   end record;

   type T is record
      S : State;
      Part_Len             : Partition_Length := 0;
      First_Data_Block     : FSBlock_Offset := 0;
      Block_Size_Bits      : Log_Block_Size := 10;
      Inodes_Per_Group     : Inode_Index := 1;
      Inode_Size           : Ext2.Inode_Size := Ext2.Inode_Size'First;
      Desc_Size            : Ext2.Desc_Size := Ext2.Desc_Size'First;
      Feature_Extents      : Boolean := False;
      Feature_64Bit        : Boolean := False;
      Inode                : Inode_Info := (others => <>);
      Block_Cache_Logical  : Cache_Label_Logical := (others => False);
      Block_Cache_Label    : Cache_Label_Array := (others => 0);
      Block_Cache          : Buffer_Type (Max_Block_Index) := (others => 16#00#);
   end record;

end FILO.FS.Ext2;