Source file archive.ml

(*Generated by Lem from archive.lem.*)
open Lem_basic_classes
open Lem_bool
open Lem_list
open Lem_num
open Lem_maybe
open Lem_string
open Show
open Lem_assert_extra

open Missing_pervasives
open Byte_sequence
open Error

type archive_entry_header =
  { name      : string
   ; timestamp : Nat_big_num.num
   ; uid       : int
   ; gid       : int
   ; mode      : int
   ; size      : int (* 1GB should be enough *)
   }

type archive_global_header = char
  list

(*val read_archive_entry_header : natural -> byte_sequence -> error (archive_entry_header * natural * byte_sequence)*)
let read_archive_entry_header seq_length seq:(archive_entry_header*Nat_big_num.num*Byte_sequence_wrapper.byte_sequence)error=
   (let magic_bytes = ([Char.chr (Nat_big_num.to_int ( (Nat_big_num.of_int 96))) (* 0x60 *); Char.chr (Nat_big_num.to_int ( (Nat_big_num.of_int 10))) (* 0x0a *)]) in
        let header_length =( (Nat_big_num.of_int 60)) in bind (
        (* let _ = Missing_pervasives.errs ("Archive entry header? " ^ (show (take 16 bs)) ^ "? ") in *)partition_with_length header_length seq_length seq) (fun (header, rest) -> bind (offset_and_cut( (Nat_big_num.of_int 58))( (Nat_big_num.of_int 2)) header) (fun magic -> bind (offset_and_cut( (Nat_big_num.of_int 0))( (Nat_big_num.of_int 16)) header) (fun name1 -> bind (offset_and_cut( (Nat_big_num.of_int 16))( (Nat_big_num.of_int 12)) header) (fun timestamp_str -> bind (offset_and_cut( (Nat_big_num.of_int 28))( (Nat_big_num.of_int 6))  header) (fun uid_str -> bind (offset_and_cut( (Nat_big_num.of_int 34))( (Nat_big_num.of_int 6))  header) (fun gid_str -> bind (offset_and_cut( (Nat_big_num.of_int 40))( (Nat_big_num.of_int 8))  header) (fun mode_str -> bind (offset_and_cut( (Nat_big_num.of_int 48))( (Nat_big_num.of_int 10)) header) (fun size_str ->
        let size2 = (natural_of_decimal_string (string_of_byte_sequence size_str)) in
                (* let _ = Missing_pervasives.errln (": yes, size " ^ (show size)) in *)
        return ({ name = (string_of_byte_sequence name1); timestamp = (( (Nat_big_num.of_int 0) : Nat_big_num.num)) (* FIXME *);
          uid = 0 (* FIXME *) ; gid = 0 (* FIXME *) ; mode = 0 (* FIXME *);
            size = (Nat_big_num.to_int size2) (* FIXME *) }, Nat_big_num.sub_nat seq_length header_length, rest))))))))))

(*val read_archive_global_header : byte_sequence -> error (archive_global_header * byte_sequence)*)
let read_archive_global_header bs:((char)list*Byte_sequence_wrapper.byte_sequence)error=  (bind (
  (* let _ = Missing_pervasives.errs ("Archive? " ^ (show (take 16 bs)) ^ "? ")
  in*)takebytes( (Nat_big_num.of_int 8)) bs) (fun h ->
  if string_of_byte_sequence h = "!<arch>\n" then bind (
    (* let _ = Missing_pervasives.errln ": yes" in *)dropbytes( (Nat_big_num.of_int 8)) bs) (fun t ->
    return (char_list_of_byte_sequence h, t))
  else
    (* let _ = Missing_pervasives.errln ": no" in *)
    fail "read_archive_global_header: not an archive"))

(*val accum_archive_contents : (list (string * byte_sequence)) -> maybe string -> natural -> byte_sequence -> error (list (string * byte_sequence))*)
let rec accum_archive_contents accum extended_filenames whole_seq_length whole_seq:((string*Byte_sequence_wrapper.byte_sequence)list)error=
   (
  (* let _ = Missing_pervasives.errs "Can read a header? " in *)if not (Nat_big_num.equal (Byte_sequence.length0 whole_seq) whole_seq_length) then
    (assert false) (* invariant: whole_seq_length always equal to length of whole_seq, so the length is only
      computed one.  This "fail" needed for Isabelle termination proofs... *)
  else
  (match (read_archive_entry_header whole_seq_length whole_seq) with
    | Fail _ -> return accum
    | Success (hdr, (seq_length : Nat_big_num.num), next_bs) ->
        (* let _ = Missing_pervasives.errln ("yes; next_bs has length " ^ (show (Byte_sequence.length next_bs))) in *)
        let amount_to_drop =
          (if (hdr.size mod 2) = 0 then
            (Nat_big_num.of_int hdr.size)
          else Nat_big_num.add
            (Nat_big_num.of_int hdr.size)( (Nat_big_num.of_int 1)))
        in
        if Nat_big_num.equal amount_to_drop( (Nat_big_num.of_int 0)) then
          fail "accum_archive_contents: amount to drop from byte sequence is 0"
        else bind (
        (*let _ = Missing_pervasives.errln ("amount_to_drop is " ^ (show amount_to_drop)) in*)takebytes (Nat_big_num.of_int hdr.size) next_bs) (fun chunk ->
        (*let _ = Missing_pervasives.errs ("Processing archive header named " ^ hdr.name)
        in*)
        let (new_accum, (new_extended_filenames :  string option)) =
          (let name1 = (Xstring.explode hdr.name) in
            if (listEqualBy (=) name1 ['/'; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' ']) then
              (* SystemV symbol lookup table; we skip this *) (accum, extended_filenames)
            else
              (match name1 with
                | x::xs ->
                  if x = '/' then
                    (match xs with
                      | y::ys ->
                        if y = '/' then
                          (accum, Some (string_of_byte_sequence chunk))
                        else
                          let index = (natural_of_decimal_string (Xstring.implode xs)) in
                            (match extended_filenames with
                              | None -> failwith "corrupt archive: reference to non-existent extended filenames"
                              | Some s ->
                                let table_suffix = ((match Ml_bindings.string_suffix index s with Some x -> x | None -> "" )) in
                                let index = ((match Ml_bindings.string_index_of '/' table_suffix with Some x -> x | None -> (Nat_big_num.of_int (String.length table_suffix)) )) in
                                let ext_name = ((match Ml_bindings.string_prefix index table_suffix with Some x -> x | None -> "" )) in
                                  (*let _ = Missing_pervasives.errln ("Got ext_name " ^ ext_name) in*)
                                  (((ext_name, chunk) :: accum), extended_filenames)
                           )
                      | [] ->
                        let index = (natural_of_decimal_string (Xstring.implode xs)) in
                          (match extended_filenames with
                            | None -> failwith "corrupt archive: reference to non-existent extended filenames"
                            | Some s ->
                              let table_suffix = ((match Ml_bindings.string_suffix index s with Some x -> x | None -> "" )) in
                              let index = ((match Ml_bindings.string_index_of '/' table_suffix with Some x -> x | None -> (Nat_big_num.of_int (String.length table_suffix)) )) in
                              let ext_name = ((match Ml_bindings.string_prefix index table_suffix with Some x -> x | None -> "" )) in
                                (*let _ = Missing_pervasives.errln ("Got ext_name " ^ ext_name) in*)
                                (((ext_name, chunk) :: accum), extended_filenames)
                         )
                    )
                  else
                    (((hdr.name, chunk) :: accum), extended_filenames)
                | [] -> (((hdr.name, chunk) :: accum), extended_filenames)
              ))
        in
          (match (Byte_sequence.dropbytes amount_to_drop next_bs) with
            | Fail _ -> return accum
            | Success new_seq ->
              accum_archive_contents new_accum new_extended_filenames ( Nat_big_num.sub_nat seq_length amount_to_drop) new_seq
          ))
  ))

(*val read_archive : byte_sequence -> error (list (string * byte_sequence))*)
let read_archive bs:((string*byte_sequence0)list)error=  (bind (read_archive_global_header bs) (fun (hdr, seq) ->
    let result = (accum_archive_contents [] None (Byte_sequence.length0 seq) seq)  in
    (* let _ = Missing_pervasives.errln "Finished reading archive" in *)
    (match result with
        Success r -> Success (List.rev r)
        | Fail x -> Fail x
    )))