with Ada.Unchecked_Conversion;

package body FILO.FS.VFS is

   State : T := Initial;

   Path_Max : constant := 4096;
   Max_Link_Depth : constant := 32;

   subtype Path_Length is Natural range 0 .. Path_Max;
   subtype Path_Index_Plus is Positive range 1 .. Path_Max + 1;
   subtype Path_Index is Path_Index_Plus range 1 .. Path_Max;

   subtype Path_Buffer is Buffer_Type (Path_Index)
   with
      Object_Size => Path_Max * 8;
   Path_Buf : Path_Buffer;

   subtype Path_String is String (Path_Index)
   with
      Object_Size => Path_Max * 8;
   Path : Path_String;

   function C_Mount return int
   with
      SPARK_Mode => Off
   is
      Success : Boolean;
   begin
      if not Is_Mounted (State) then
         State := Initial; -- Work around not having an unmount in FILO.
      end if;
      Mount (State, Part_Len, Success);
      return (if Success then 1 else 0);
   end C_Mount;

   procedure Open (File_Path : System.Address; Ret : out int)
   is
      function Str_Len (S : System.Address) return Natural;
      function Str_Len (S : System.Address) return Natural
      with
         SPARK_Mode => Off
      is
         Buf : Buffer_Type (1 .. Path_Max + 1)
         with
            Convention => C,
            Address => S;
      begin
         for I in Buf'Range loop
            if Buf (I) = 16#00# then
               return I - 1;
            end if;
         end loop;
         return Path_Max + 1;
      end Str_Len;

      procedure Str_Cpy (Dst : out String; Src : in System.Address);
      procedure Str_Cpy (Dst : out String; Src : in System.Address)
      with
         SPARK_Mode => Off
      is
         Src_String : String (Dst'Range)
         with
            Convention => C,
            Address => Src;
      begin
         Dst := Src_String;
      end Str_Cpy;

      function Component_Start (Path : Path_String; Pos : Positive) return Path_Index_Plus is
      begin
         for I in Pos .. Path'Last loop
            if Path (I) /= '/' then
               return I;
            end if;
         end loop;
         return Path'Last + 1;
      end Component_Start;

      function Component_End (Path : Path_String; Start : Path_Index_Plus; Limit : Path_Index) return Path_Length
      with
         Post => Component_End'Result <= Limit
      is
      begin
         for I in Start .. Limit loop
            if Path (I) = '/' or Is_Space (Path (I)) then
               return I - 1;
            end if;
         end loop;
         return Limit;
      end Component_End;

      function Path_End (Path : Path_String; Start : Path_Index) return Path_Length is
      begin
         for I in Start .. Path'Last loop
            if Is_Space (Path (I)) then
               return I - 1;
            end if;
         end loop;
         return Path'Last;
      end Path_End;

      procedure Read_Link
        (Path        : in out Path_String;
         Rest_First  : in     Path_Index_Plus;
         Rest_Last   : in     Path_Index;
         Link_Len    : in     Positive;
         Success     :    out Boolean)
      with
         Pre =>
            Is_Open (State) and
            Rest_First - 1 <= Rest_Last,
         Post =>
            Is_Open (State)
      is
         function As_String is new Ada.Unchecked_Conversion (Path_Buffer, Path_String);

         Rest_Len : constant Natural := Rest_Last - Rest_First + 1;
         File_Pos : File_Offset := 0;
         Read_Len : Natural;
      begin
         if Path_Max - Rest_Len < Link_Len then
            Success := False;
            return;
         end if;

         pragma Warnings
           (GNATprove, Off, """File_Pos"" is set*but not used",
            Reason => "We only read the link at once, during path walks.");
         Read
           (State    => State,
            File_Pos => File_Pos,
            Buf      => Path_Buf (1 .. Link_Len),
            Len      => Read_Len);
         pragma Warnings (GNATprove, On, """File_Pos"" is set*but not used");
         Success := Read_Len = Link_Len;

         if Success then
            Path (Link_Len + 1 .. Link_Len + Rest_Len) := Path (Rest_First .. Rest_Last);
            Path (Link_Len + Rest_Len + 1 .. Path'Last) := (others => ' ');
            Path (1 .. Link_Len) := As_String (Path_Buf) (1 .. Link_Len);
         end if;
      end Read_Link;

      Path_Len : constant Natural := Str_Len (File_Path);
      Root_Dir : Boolean := True;
   begin
      Ret := 0;

      if not Is_Mounted (State) or Path_Len > Path_Max then
         return;
      end if;

      if Is_Open (State) then
         Close (State);
      end if;

      Str_Cpy (Path (1 .. Path_Len), File_Path);
      Path (Path_Len + 1 .. Path'Last) := (others => ' ');

      Link_Loop :
      for I in 1 .. Max_Link_Depth loop
         pragma Loop_Invariant (Is_Mounted (State));
         declare
            Path_Pos : Path_Index_Plus := Path'First;
            Path_Last : constant Path_Length := Path_End (Path, Path_Pos);
         begin
            if Path_Last < Path'First then
               return;
            end if;

            Path_Loop :
            loop
               pragma Loop_Invariant
                 (Is_Mounted (State) and
                  Path_Last in Path'Range);
               declare
                  Comp_First : constant Path_Index_Plus := Component_Start (Path, Path_Pos);
                  Comp_Last : constant Path_Length := Component_End (Path, Comp_First, Path_Last);
                  File_Type : FS.File_Type;
                  File_Len : File_Length;
                  Success : Boolean;
               begin
                  if Comp_First > Comp_Last then
                     return;
                  end if;

                  Open
                    (State       => State,
                     File_Len    => File_Len,
                     File_Type   => File_Type,
                     File_Name   => Path (Comp_First .. Comp_Last),
                     In_Root     => Root_Dir,
                     Success     => Success);
                  if not Success then
                     return;
                  end if;
                  Root_Dir := False;

                  case File_Type is
                     when Dir =>
                        if Comp_Last = Path_Last then
                           Close (State);
                           return;
                        end if;
                        Path_Pos := Comp_Last + 1;
                     when Regular =>
                        if Comp_Last = Path_Last then
                           Set_File_Max (File_Len);
                           Ret := 1;
                           return;
                        else
                           Close (State);
                           return;
                        end if;
                     when Link =>
                        if File_Len = 0 or File_Len > Path_Max then
                           Success := False;
                        else
                           Read_Link
                             (Path        => Path,
                              Rest_First  => Comp_Last + 1,
                              Rest_Last   => Path_Last,
                              Link_Len    => Positive (File_Len),
                              Success     => Success);
                        end if;
                        Close (State);
                        if not Success then
                           return;
                        end if;
                        Root_Dir := Path (1) = '/';
                        exit Path_Loop; -- continue in Link_Loop
                  end case;
               end;
            end loop Path_Loop;
         end;
      end loop Link_Loop;
   end Open;

   function C_Open (File_Path : System.Address) return int
   with
      SPARK_Mode => Off
   is
      Ret : int;
   begin
      if Is_Mounted (State) then
         Open (File_Path, Ret);
      else
         Ret := 0;
      end if;
      return Ret;
   end C_Open;

   procedure C_Close is
   begin
      if Is_Open (State) then
         Close (State);
      end if;
   end C_Close;
   
   function C_Read (Buf : System.Address; Len : int) return int
   with
      SPARK_Mode => Off
   is
      subtype Buffer_Range is Natural range 0 .. Integer (Len) - 1;
      Buffer : Buffer_Type (Buffer_Range)
      with
         Convention => C,
         Address => Buf;

      File_Pos : File_Offset := FILO.FS.File_Pos;
      Read_Len : Natural;
   begin
      if Is_Open (State) then
         Read (State, File_Pos, Buffer, Read_Len);
         Set_File_Pos (File_Pos);
      else
         Read_Len := 0;
      end if;
      return int (Read_Len);
   end C_Read;

end FILO.FS.VFS;