(*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 string_of_byte_sequence : byte_sequence -> string*) let string_of_byte_sequence0 seq:string= ((match seq with | Sequence bs -> Xstring.implode (Lem_list.map (fun x-> x) bs) )) (*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)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 (* let _ = Missing_pervasives.errs ("Archive entry header? " ^ (show (take 16 bs)) ^ "? ") in *) partition_with_length header_length seq_length seq >>= (fun (header, rest) -> offset_and_cut(Nat_big_num.of_int 58)(Nat_big_num.of_int 2) header >>= (fun magic -> offset_and_cut(Nat_big_num.of_int 0)(Nat_big_num.of_int 16) header >>= (fun name1 -> offset_and_cut(Nat_big_num.of_int 16)(Nat_big_num.of_int 12) header >>= (fun timestamp_str -> offset_and_cut(Nat_big_num.of_int 28)(Nat_big_num.of_int 6) header >>= (fun uid_str -> offset_and_cut(Nat_big_num.of_int 34)(Nat_big_num.of_int 6) header >>= (fun gid_str -> offset_and_cut(Nat_big_num.of_int 40)(Nat_big_num.of_int 8) header >>= (fun mode_str -> 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_sequence0 size_str)) in (* let _ = Missing_pervasives.errln (": yes, size " ^ (show size)) in *) return ({ name = (string_of_byte_sequence0 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 seq:((char)list*byte_sequence)error= ((match seq with | Sequence bs -> (* let _ = Missing_pervasives.errs ("Archive? " ^ (show (take 16 bs)) ^ "? ") in*) let chars = (Lem_list.map (fun x-> x) (take0(Nat_big_num.of_int 8) bs)) in if Xstring.implode chars = "!\n" then (* let _ = Missing_pervasives.errln ": yes" in *) return (chars, Sequence(drop0(Nat_big_num.of_int 8) bs)) 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)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), seq) -> (match seq with | Sequence next_bs -> (* let _ = Missing_pervasives.errln ("yes; next_bs has length " ^ (show (List.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 (*let _ = Missing_pervasives.errln ("amount_to_drop is " ^ (show amount_to_drop)) in*) let chunk = (Sequence(Lem_list.take hdr.size next_bs)) in (*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_sequence0 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 seq) 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_sequence)list)error= (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 )))