Source file byte_sequence_impl.ml

(*Generated by Lem from byte_sequence_impl.lem.*)
(** [byte_sequence_ocaml.lem], a list of bytes used for ELF I/O and other basic
  * tasks in the ELF model.
  *)

open Lem_basic_classes
open Lem_bool
open Lem_list
open Lem_num
open Lem_string
open Lem_assert_extra

open Error
open Lem_maybe
open Missing_pervasives
open Show

(** A [byte_sequence], [bs], denotes a consecutive list of bytes.  Can be read
  * from or written to a binary file.  Most basic type in the ELF formalisation.
  * This is a faster OCaml byte sequence implementation.
  *)
(*type byte_sequence*)

(*val compare_byte_sequence : byte_sequence -> byte_sequence -> ordering*)

let instance_Basic_classes_Ord_Byte_sequence_impl_byte_sequence_dict:(Byte_sequence_wrapper.byte_sequence)ord_class= ({

  compare_method = Byte_sequence_wrapper.compare;

  isLess_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(Byte_sequence_wrapper.compare f1 f2) (-1))));

  isLessEqual_method = (fun f1 -> (fun f2 -> let result = (Byte_sequence_wrapper.compare f1 f2) in Lem.orderingEqual result (-1) || Lem.orderingEqual result 0));

  isGreater_method = (fun f1 -> (fun f2 -> ( Lem.orderingEqual(Byte_sequence_wrapper.compare f1 f2) 1)));

  isGreaterEqual_method = (fun f1 -> (fun f2 -> let result = (Byte_sequence_wrapper.compare f1 f2) in Lem.orderingEqual result 1 || Lem.orderingEqual result 0))})

(*val string_of_byte_sequence : byte_sequence -> string*)

let instance_Show_Show_Byte_sequence_impl_byte_sequence_dict:(Byte_sequence_wrapper.byte_sequence)show_class= ({

  show_method = Byte_sequence_wrapper.to_string})

(*val equal : byte_sequence -> byte_sequence -> bool*)

let instance_Basic_classes_Eq_Byte_sequence_impl_byte_sequence_dict:(Byte_sequence_wrapper.byte_sequence)eq_class= ({

  isEqual_method = Byte_sequence_wrapper.equal;

  isInequal_method = (fun l r->not (Byte_sequence_wrapper.equal l r))})

(* See byte_sequence_generic.lem for a description of these functions *)

(*val empty : byte_sequence*)

(*val acquire : string -> error byte_sequence*)

(*val serialise : string -> byte_sequence -> error unit*)

(*val read_char : byte_sequence -> error (byte * byte_sequence)*)

(*val find_byte : byte_sequence -> byte -> maybe natural*)

(*val create : natural -> byte -> byte_sequence*)

(*val length : byte_sequence -> natural*)

(*val concat : list byte_sequence -> byte_sequence*)

(*val zero_pad_to_length : natural -> byte_sequence -> byte_sequence*)

(*val byte_sequence_of_byte_list : list byte -> byte_sequence*)

(*val char_list_of_byte_sequence : byte_sequence -> list char*)

(*val byte_list_of_byte_sequence : byte_sequence -> list byte*)

(*val dropbytes : natural -> byte_sequence -> error byte_sequence*)

(*val takebytes : natural -> byte_sequence -> error (byte_sequence)*)

(*val takebytes_with_length : natural -> natural -> byte_sequence -> error byte_sequence*)
let takebytes_with_length count ts_length ts:(Byte_sequence_wrapper.byte_sequence)error=
   (if not (Nat_big_num.equal (Byte_sequence_wrapper.big_num_length ts) ts_length) then fail "takebytes_with_length: invalid length"
  else Byte_sequence_wrapper.big_num_takebytes count ts)