Source file missing_pervasives.ml

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

(*val naturalZero : natural*)
(*let naturalZero:natural=  0*)

(*val id : forall 'a. 'a -> 'a*)
let id0 x:'a=  x

(*type byte*)
(*val natural_of_byte : byte -> natural*)

let compare_byte b1 b2:int=  (Nat_big_num.compare (Nat_big_num.of_int (Char.code b1)) (Nat_big_num.of_int (Char.code b2)))

let instance_Basic_classes_Ord_Missing_pervasives_byte_dict:(char)ord_class= ({

  compare_method = compare_byte;

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

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

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

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

(*val char_of_byte : byte -> char*)

(*val byte_of_char : char -> byte*)

(* Define how to print a byte in hex *)
(*val hex_char_of_nibble : natural -> char*)
let hex_char_of_nibble n:char=
   (if Nat_big_num.equal n( (Nat_big_num.of_int 0)) then
    '0'
  else if Nat_big_num.equal n( (Nat_big_num.of_int 1)) then
    '1'
  else if Nat_big_num.equal n( (Nat_big_num.of_int 2)) then
    '2'
  else if Nat_big_num.equal n( (Nat_big_num.of_int 3)) then
    '3'
  else if Nat_big_num.equal n( (Nat_big_num.of_int 4)) then
    '4'
  else if Nat_big_num.equal n( (Nat_big_num.of_int 5)) then
    '5'
  else if Nat_big_num.equal n( (Nat_big_num.of_int 6)) then
    '6'
  else if Nat_big_num.equal n( (Nat_big_num.of_int 7)) then
    '7'
  else if Nat_big_num.equal n( (Nat_big_num.of_int 8)) then
    '8'
  else if Nat_big_num.equal n( (Nat_big_num.of_int 9)) then
    '9'
  else if Nat_big_num.equal n( (Nat_big_num.of_int 10)) then
    'a'
  else if Nat_big_num.equal n( (Nat_big_num.of_int 11)) then
    'b'
  else if Nat_big_num.equal n( (Nat_big_num.of_int 12)) then
    'c'
  else if Nat_big_num.equal n( (Nat_big_num.of_int 13)) then
    'd'
  else if Nat_big_num.equal n( (Nat_big_num.of_int 14)) then
    'e'
  else if Nat_big_num.equal n( (Nat_big_num.of_int 15)) then
    'f'
   else
     (assert false))

let hex_string_of_byte b:string=
     (Xstring.implode [ hex_char_of_nibble ( Nat_big_num.div(Nat_big_num.of_int (Char.code b))( (Nat_big_num.of_int 16)))
             ; hex_char_of_nibble ( Nat_big_num.modulus(Nat_big_num.of_int (Char.code b))( (Nat_big_num.of_int 16)))])

let instance_Show_Show_Missing_pervasives_byte_dict:(char)show_class= ({

  show_method = hex_string_of_byte})

(*val natural_of_decimal_digit : char -> maybe natural*)
let natural_of_decimal_digit c:(Nat_big_num.num)option=
   (if c = '0' then
    Some( (Nat_big_num.of_int 0))
  else if c = '1' then
    Some( (Nat_big_num.of_int 1))
  else if c = '2' then
    Some( (Nat_big_num.of_int 2))
  else if c = '3' then
    Some( (Nat_big_num.of_int 3))
  else if c = '4' then
    Some( (Nat_big_num.of_int 4))
  else if c = '5' then
    Some( (Nat_big_num.of_int 5))
  else if c = '6' then
    Some( (Nat_big_num.of_int 6))
  else if c = '7' then
    Some( (Nat_big_num.of_int 7))
  else if c = '8' then
    Some( (Nat_big_num.of_int 8))
  else if c = '9' then
    Some( (Nat_big_num.of_int 9))
  else
    None)

(*val natural_of_decimal_string_helper : natural -> list char -> natural*)
let rec natural_of_decimal_string_helper acc chars:Nat_big_num.num=
     ((match chars with
        [] -> acc
        | c :: cs -> (match natural_of_decimal_digit c with
            Some dig -> natural_of_decimal_string_helper ( Nat_big_num.add( Nat_big_num.mul( (Nat_big_num.of_int 10)) acc) dig) cs
            | None -> acc
        )
    ))

(*val natural_of_decimal_string : string -> natural*)
let natural_of_decimal_string s:Nat_big_num.num=
     (natural_of_decimal_string_helper( (Nat_big_num.of_int 0)) (Xstring.explode s))

(*val hex_string_of_natural : natural -> string*)
let rec hex_string_of_natural n:string=
     (if Nat_big_num.less n( (Nat_big_num.of_int 16)) then Xstring.implode [hex_char_of_nibble n]
    else (hex_string_of_natural ( Nat_big_num.div n( (Nat_big_num.of_int 16)))) ^ (Xstring.implode [hex_char_of_nibble ( Nat_big_num.modulus n( (Nat_big_num.of_int 16)))]))

(*val natural_of_bool : bool -> natural*)
let natural_of_bool b:Nat_big_num.num=
   ((match b with
    | true  -> (Nat_big_num.of_int 1)
    | false -> (Nat_big_num.of_int 0)
  ))

(*val unsafe_nat_of_natural : natural -> nat*)

(*val unsafe_int_of_natural   : natural -> int*)

(*val byte_of_natural : natural -> byte*)

(*val natural_ordering : natural -> natural -> ordering*)
(*let natural_ordering left right:ordering=
   if (Instance_Basic_classes_Eq_Num_natural.=) left right then
    EQ
  else if (Instance_Basic_classes_Ord_Num_natural.<) left right then
    LT
  else
    GT*)

(*val merge_by : forall 'a. ('a -> 'a -> ordering) -> list 'a -> list 'a -> list 'a*)
let rec merge_by comp xs ys:'a list=
   ((match (xs, ys) with
    | ([], ys)      -> ys
    | (xs, [])     -> xs
    | (x::xs, y::ys) ->
      if Lem.orderingEqual (comp x y) (-1) then
        x::(merge_by comp xs (y::ys))
      else
        y::(merge_by comp (x::xs) ys)
  ))

(*val sort_by : forall 'a. ('a -> 'a -> ordering) -> list 'a -> list 'a*)
(*let rec sort_by comp xs:list 'a=
   match xs with
    | [] -> []
    | [x] -> [x]
    | xs ->
      let ls = List.take (Instance_Num_NumIntegerDivision_nat.div List.length xs 2) xs in
      let rs = List.drop (Instance_Num_NumIntegerDivision_nat.div List.length xs 2) xs in
        merge_by comp (sort_by comp ls) (sort_by comp rs)
  end*)

(** [mapMaybei f xs] maps a function expecting an index (the position in the list
  * [xs] that it is currently viewing) and producing a [maybe] type across a list.
  * Elements that produce [Nothing] under [f] are discarded in the output, whilst
  * those producing [Just e] for some [e] are kept.
  *)
(*val mapMaybei' : forall 'a 'b. (natural -> 'a -> maybe 'b) -> natural -> list 'a -> list 'b*)
let rec mapMaybei' f idx1 xs:'b list=
   ((match xs with
  | []    -> []
  | x::xs ->
      (match f idx1 x with
      | None -> mapMaybei' f ( Nat_big_num.add( (Nat_big_num.of_int 1)) idx1) xs
      | Some e  -> e :: mapMaybei' f ( Nat_big_num.add( (Nat_big_num.of_int 1)) idx1) xs
      )
  ))

(*val mapMaybei : forall 'a 'b. (natural -> 'a -> maybe 'b) -> list 'a -> list 'b*)

let mapMaybei f xs:'b list=
   (mapMaybei' f( (Nat_big_num.of_int 0)) xs)

(** [partitionii is xs] returns a pair of lists: firstly those elements in [xs] that are
    at indices in [is], and secondly the remaining elements.
    It preserves the order of elements in xs. *)
(*val partitionii' : forall 'a. natural -> list natural -> list 'a
    -> list (natural * 'a) (* accumulates the 'in' partition *)
    -> list (natural * 'a) (* accumulates the 'out' partition *)
    -> (list (natural * 'a) * list (natural * 'a))*)
let rec partitionii' (offset : Nat_big_num.num) sorted_is xs reverse_accum reverse_accum_compl:(Nat_big_num.num*'a)list*(Nat_big_num.num*'a)list=
     (
    (* offset o means "xs begins at index o, as reckoned by the indices in sorted_is" *)(match sorted_is with
        [] -> (List.rev reverse_accum, List.rev reverse_accum_compl)
        | i :: more_is ->
            let (length_to_split_off : int) = (Nat_big_num.to_int ( Nat_big_num.sub_nat i offset))
            in
            let (left, right) = (Lem_list.split_at length_to_split_off xs) in
            let left_indices : Nat_big_num.num list = (Lem_list.genlist
                (fun j -> Nat_big_num.add (Nat_big_num.of_int j) offset)
                (List.length left))
            in
            let left_with_indices = (list_combine left_indices left) in
            (* left begins at offset, right begins at offset + i *)
            (match right with
                [] -> (* We got to the end of the list before the target index. *)
                    (List.rev reverse_accum,
                     List.rev_append reverse_accum_compl left_with_indices)
                | x :: more_xs ->
                    (* x is at index i by definition, so more_xs starts with index i + 1 *)
                    partitionii' (Nat_big_num.add i( (Nat_big_num.of_int 1))) more_is more_xs ((i, x) :: reverse_accum)
                        (List.rev_append left_with_indices reverse_accum_compl)
            )
    ))

(*val filteri : forall 'a. list natural -> list 'a -> list 'a*)
let filteri is xs:'a list=
     (let sorted_is = (List.sort Nat_big_num.compare is) in
    let (accum, accum_compl) = (partitionii'( (Nat_big_num.of_int 0)) sorted_is xs [] [])
    in
    let (just_indices, just_items) = (List.split accum)
    in
    just_items)

(*val filterii : forall 'a. list natural -> list 'a -> list (natural * 'a)*)
let filterii is xs:(Nat_big_num.num*'a)list=
     (let sorted_is = (List.sort Nat_big_num.compare is) in
    let (accum, accum_compl) = (partitionii'( (Nat_big_num.of_int 0)) sorted_is xs [] [])
    in
    accum)

(*val partitioni : forall 'a. list natural -> list 'a -> (list 'a * list 'a)*)
let partitioni is xs:'a list*'a list=
     (let sorted_is = (List.sort Nat_big_num.compare is) in
    let (accum, accum_compl) = (partitionii'( (Nat_big_num.of_int 0)) sorted_is xs [] [])
    in
    let (just_indices, just_items) = (List.split accum)
    in
    let (just_indices_compl, just_items_compl) = (List.split accum_compl)
    in
    (just_items, just_items_compl))

(*val partitionii : forall 'a. list natural -> list 'a -> (list (natural * 'a) * list (natural * 'a))*)
let partitionii is xs:(Nat_big_num.num*'a)list*(Nat_big_num.num*'a)list=
     (let sorted_is = (List.sort Nat_big_num.compare is) in
    partitionii'( (Nat_big_num.of_int 0)) sorted_is xs [] [])

(** [unzip3 ls] takes a list of triples and returns a triple of lists. *)
(*val unzip3: forall 'a 'b 'c. list ('a * 'b * 'c) -> (list 'a * list 'b * list 'c)*)
let rec unzip3 l:'a list*'b list*'c list=  ((match l with
  | [] -> ([], [], [])
  | (x, y, z) :: xyzs -> let (xs, ys, zs) = (unzip3 xyzs) in ((x :: xs), (y :: ys), (z :: zs))
))

(** [zip3 ls] takes a triple of lists and returns a list of triples. *)
(*val zip3: forall 'a 'b 'c. list 'a -> list 'b -> list 'c -> list ('a * 'b * 'c)*)
let rec zip3 alist blist clist:('a*'b*'c)list=  ((match (alist, blist, clist) with
  | ([], [], []) -> []
  | (x :: morex, y :: morey, z :: morez) -> let more_xyz = (zip3 morex morey morez) in (x, y, z) :: more_xyz
))

(** [null_byte] is the null character a a byte. *)
(*val null_byte : byte*)

(** [null_char] is the null character. *)
(*val null_char : char*)
let null_char:char=  ( '\000')

(** [println s] prints [s] to stdout, adding a trailing newline. *)
(* val println : string -> unit *)
(* declare ocaml target_rep function println = `print_endline` *)

(** [prints s] prints [s] to stdout, without adding a trailing newline. *)
(* val prints : string -> unit *)
(* declare ocaml target_rep function prints = `print_string` *)

(** [errln s] prints [s] to stderr, adding a trailing newline. *)
(*val errln : string -> unit*)

(** [errs s] prints [s] to stderr, without adding a trailing newline. *)
(*val errs : string -> unit*)

(** [outln s] prints [s] to stdout, adding a trailing newline. *)
(*val outln : string -> unit*)

(** [outs s] prints [s] to stdout, without adding a trailing newline. *)
(*val outs : string -> unit*)

(** [intercalate sep xs] places [sep] between all elements of [xs].
  * Made tail recursive and unrolled slightly to improve performance on large
  * lists.*)
(*val intercalate' : forall 'a. 'a -> list 'a -> list 'a -> list 'a*)
let rec intercalate' sep xs accum:'a list=
	 ((match xs with
		| []       -> List.rev accum
		| [x]      ->  List.rev_append (List.rev (List.rev accum)) [x]
		| [x; y]   ->  List.rev_append (List.rev (List.rev accum)) [x; sep; y]
		| x::y::xs -> intercalate' sep xs (sep::(y::(sep::(x::accum))))
	))

(*val intercalate : forall 'a. 'a -> list 'a -> list 'a*)
let intercalate sep xs:'a list=  (intercalate' sep xs [])

(** [unlines xs] concatenates a list of strings [xs], placing each entry
  * on a new line.
  *)
(*val unlines : list string -> string*)
let unlines xs:string=
   (List.fold_left (^) "" (intercalate "\n" xs))

(** [bracket xs] concatenates a list of strings [xs], separating each entry with a
  * space, and bracketing the resulting string.
  *)
(*val bracket : list string -> string*)
let bracket xs:string=
   ("(" ^ (List.fold_left (^) "" (intercalate " " xs) ^ ")"))

(** [string_of_list l] produces a string representation of list [l].
  *)
(*val string_of_list : forall 'a. Show 'a => list 'a -> string*)
let string_of_list dict_Show_Show_a l:string=
   (let result = (intercalate "," (Lem_list.map  
  dict_Show_Show_a.show_method l)) in
  let folded = (List.fold_left (^) "" result) in
    "[" ^ (folded ^ "]"))

let instance_Show_Show_list_dict dict_Show_Show_a:('a list)show_class= ({

  show_method = 
  (string_of_list dict_Show_Show_a)})

(** [split_string_on_char s c] splits a string [s] into a list of substrings
  * on character [c], otherwise returning the singleton list containing [s]
  * if [c] is not found in [s].
  *
  * NOTE: quirkily, this doesn't discard separators (e.g. because NUL characters
  * are significant when indexing into string tables). FIXME: given this, is this
  * function really reusable? I suspect not.
  *)
(*val split_string_on_char : string -> char -> list string*)

(* [find_substring sub s] returns the index at which *)
(*val find_substring : string -> string -> maybe natural*)

(*val string_contains : string -> string -> bool*)
let string_contains s substr:bool=  (not ((Lem.option_equal Nat_big_num.equal (Ml_bindings.find_substring substr s) None)))

(*val string_replace : string -> string -> string -> string*)

(** [string_of_nat m] produces a string representation of natural number [m]. *)
(*val string_of_nat : nat -> string*)

(** [string_suffix i s] returns all but the first [i] characters of [s].
  * Fails if the index is negative, or beyond the end of the string.
  *)
(*val string_suffix : natural -> string -> maybe string*)

(*val nat_length : forall 'a. list 'a -> nat*)

(*val length : forall 'a. list 'a -> natural*)
let length xs:Nat_big_num.num=  (Nat_big_num.of_int (List.length xs))

(*val takeRevAcc : forall 'a. natural -> list 'a -> list 'a -> list 'a*)
let rec takeRevAcc m xs rev_acc:'a list=
   ((match xs with
    | []    -> List.rev rev_acc
    | x::xs ->
      if Nat_big_num.equal m( (Nat_big_num.of_int 0)) then
        List.rev rev_acc
      else
        takeRevAcc ( Nat_big_num.sub_nat m( (Nat_big_num.of_int 1))) xs (x::rev_acc)
  ))

(** [take cnt xs] takes the first [cnt] elements of list [xs].  Returns a truncation
  * if [cnt] is greater than the length of [xs].
  *)
(*val take : forall 'a. natural -> list 'a -> list 'a*)
let rec take0 m xs:'a list=
   (takeRevAcc m xs [])

(** [drop cnt xs] returns all but the first [cnt] elements of list [xs].  Returns an empty list
  * if [cnt] is greater than the length of [xs].
  *)
(*val drop : forall 'a. natural -> list 'a -> list 'a*)
let rec drop0 m xs:'a list=
   ((match xs with
    | []    -> []
    | x::xs ->
      if Nat_big_num.equal m( (Nat_big_num.of_int 0)) then
        x::xs
      else
        drop0 ( Nat_big_num.sub_nat m( (Nat_big_num.of_int 1))) xs
  ))

(** [string_prefix i s] returns the first [i] characters of [s].
  * Fails if the index is negative, or beyond the end of the string.
  *)
(*val string_prefix : natural -> string -> maybe string*)
(*let string_prefix m s:maybe(string)=
   let cs = String.toCharList s in
    if (Instance_Basic_classes_Ord_Num_natural.>) m (length cs) then
      Nothing
    else
      Just (String.toString (take m cs))*)
(* FIXME: isabelle *)

(** [string_index_of c s] returns [Just(i)] where [i] is the index of the first
  * occurrence if [c] in [s], if it exists, otherwise returns [Nothing]. *)
(*val string_index_of' : char -> list char -> natural -> maybe natural*)
let rec string_index_of' e ss idx1:(Nat_big_num.num)option=
   ((match ss with
    | []    -> None
    | s::ss ->
      if s = e then
        Some idx1
      else
        string_index_of' e ss ( Nat_big_num.add( (Nat_big_num.of_int 1)) idx1)
  ))

(*val string_index_of : char -> string -> maybe natural*)
(*let string_index_of e s:maybe(natural)=  string_index_of' e (String.toCharList s) 0*)

(*val index : forall 'a. natural -> list 'a -> maybe 'a*)
(*let rec index m xs:maybe 'a=
   match xs with
    | []    -> Nothing
    | x::xs ->
        if (Instance_Basic_classes_Eq_Num_natural.=) m 0 then
          Just x
        else
          index ((Instance_Num_NumMinus_Num_natural.-) m 1) xs
  end*)

(*val find_index_helper : forall 'a. natural -> ('a -> bool) -> list 'a -> maybe natural*)
let rec find_index_helper count p xs:(Nat_big_num.num)option=
	 ((match xs with
		| []    -> None
		| y::ys ->
			if p y then
				Some count
			else
				find_index_helper ( Nat_big_num.add count( (Nat_big_num.of_int 1))) p ys
	))

(*val find_index : forall 'a. ('a -> bool) -> list 'a -> maybe natural*)
let find_index0 p xs:(Nat_big_num.num)option=  (find_index_helper( (Nat_big_num.of_int 0)) p xs)

(*val argv : list string*)

(*val replicate_revacc : forall 'a. list 'a -> natural -> 'a -> list 'a*)
let rec replicate_revacc revacc len e:'a list= 
  (
  if(Nat_big_num.equal len ( (Nat_big_num.of_int 0))) then (List.rev revacc)
  else
    (replicate_revacc (e :: revacc)
       ( Nat_big_num.sub_nat len ( (Nat_big_num.of_int 1))) e))

(*val replicate : forall 'a. natural -> 'a -> list 'a*)
let rec replicate0 len e:'a list=
	 (replicate_revacc [] len e)

(* We want a tail-recursive append. reverse_append l1 l2 appends l2 to the
 * reverse of l1. So we get [l1-backwards] [l2]. So just reverse l1. *)
(*val list_append : forall 'a. list 'a -> list 'a -> list 'a*)
let list_append l1 l2:'a list=
     (List.rev_append (List.rev l1) l2)

(*val list_concat : forall 'a. list (list 'a) -> list 'a*)
let list_concat ll:'a list=  (List.fold_left list_append [] ll)

(*val list_concat_map : forall 'a 'b. ('a -> list 'b) -> list 'a -> list 'b*)
let list_concat_map f l:'b list=
     (list_concat (Lem_list.map f l))

(*val list_reverse_concat_map_helper : forall 'a 'b. ('a -> list 'b) -> list 'b -> list 'a -> list 'b*)
let rec list_reverse_concat_map_helper f acc ll:'b list=
     (let lcons = (fun l -> (fun i -> i :: l))
    in
    (match ll with
      | []      -> acc
      | item :: items ->
            (* item is a thing that maps to a list. it needn't be a list yet *)
            let mapped_list = (f item)
            in
            (* let _ = Missing_pervasives.errln ("Map function gave us a list of " ^ (show (List.length mapped_list)) ^ " items") in *)
            list_reverse_concat_map_helper f (List.fold_left lcons acc (f item)) items
    ))

(*val list_reverse_concat_map : forall 'a 'b. ('a -> list 'b) -> list 'a -> list 'b*)
let list_reverse_concat_map f ll:'b list=  (list_reverse_concat_map_helper f [] ll)

(*val list_take_with_accum : forall 'a. nat -> list 'a -> list 'a -> list 'a*)
let rec list_take_with_accum n reverse_acc l:'a list=
    (
  (*  let _ = Missing_pervasives.errs ("Taking a byte; have accumulated " ^ (show (List.length acc) ^ " so far\n"))
   in *)(match n with
        0 -> List.rev reverse_acc
      | _ -> (match l with
            [] -> failwith "list_take_with_accum: not enough elements"
            | x :: xs -> list_take_with_accum (Nat_num.nat_monus n 1) (x :: reverse_acc) xs
        )
    ))

(*val unsafe_string_take : natural -> string -> string*)
let unsafe_string_take m str:string=
   (let m = (Nat_big_num.to_int m) in
    Xstring.implode (Lem_list.take m (Xstring.explode str)))

(** [padding_and_maybe_newline c w s] creates enough of char [c] to pad string [s] to [w] characters,
  * unless [s] is of length [w - 1] or greater, in which case it generates [w] copies preceded by a newline.
  * This style of formatting is used by the GNU linker in its link map output, so we
  * reproduce it using this function. Note that string [s] does not appear in the
  * output. *)
(*val padding_and_maybe_newline : char -> natural -> string -> string*)
let padding_and_maybe_newline c width str:string=
     (let padlen = (Nat_big_num.sub_nat width (Nat_big_num.of_int (String.length str))) in
    (if Nat_big_num.less_equal padlen( (Nat_big_num.of_int 1)) then "\n" else "")
     ^ (Xstring.implode (replicate0 (if Nat_big_num.less_equal padlen( (Nat_big_num.of_int 1)) then width else padlen) c)))

(** [space_padding_and_maybe_newline w s] creates enoughspaces to pad string [s] to [w] characters,
  * unless [s] is of length [w - 1] or greater, in which case it generates [w] copies preceded by a newline.
  * This style of formatting is used by the GNU linker in its link map output, so we
  * reproduce it using this function. Note that string [s] does not appear in the
  * output. *)
(*val space_padding_and_maybe_newline : natural -> string -> string*)
let space_padding_and_maybe_newline width str:string=
     (padding_and_maybe_newline ' ' width str)

(** [padded_and_maybe_newline w s] pads string [s] to [w] characters, using char [c]
  * unless [s] is of length [w - 1] or greater, in which case the padding consists of
  * [w] copies of [c] preceded by a newline.
  * This style of formatting is used by the GNU linker in its link map output, so we
  * reproduce it using this function. *)
(*val padded_and_maybe_newline : char -> natural -> string -> string*)
let padded_and_maybe_newline c width str:string=
     (str ^ (padding_and_maybe_newline c width str))

(** [padding_to c w s] creates enough copies of [c] to pad string [s] to [w] characters,
  * or 0 characters if [s] is of length [w] or greater. Note that string [s] does not appear in the
  * output. *)
(*val padding_to : char -> natural -> string -> string*)
let padding_to c width str:string=
     (let padlen = (Nat_big_num.sub_nat width (Nat_big_num.of_int (String.length str))) in
    if Nat_big_num.less_equal padlen( (Nat_big_num.of_int 0)) then "" else (Xstring.implode (replicate0 padlen c)))

(** [left_padded_to c w s] left-pads string [s] to [w] characters using [c],
  * returning it unchanged if [s] is of length [w] or greater. *)
(*val left_padded_to : char -> natural -> string -> string*)
let left_padded_to c width str:string=
     ((padding_to c width str) ^ str)

(** [right_padded_to c w s] right-pads string [s] to [w] characters using [c],
  * returning it unchanged if [s] is of length [w] or greater. *)
(*val right_padded_to : char -> natural -> string -> string*)
let right_padded_to c width str:string=
     (str ^ (padding_to c width str))

(** [space_padded_and_maybe_newline w s] pads string [s] to [w] characters, using spaces,
  * unless [s] is of length [w - 1] or greater, in which case the padding consists of
  * [w] spaces preceded by a newline.
  * This style of formatting is used by the GNU linker in its link map output, so we
  * reproduce it using this function. *)
(*val space_padded_and_maybe_newline : natural -> string -> string*)
let space_padded_and_maybe_newline width str:string=
     (str ^ (padding_and_maybe_newline ' ' width str))

(** [left_space_padded_to w s] left-pads string [s] to [w] characters using spaces,
  * returning it unchanged if [s] is of length [w] or greater. *)
(*val left_space_padded_to : natural -> string -> string*)
let left_space_padded_to width str:string=
     ((padding_to ' ' width str) ^ str)

(** [right_space_padded_to w s] right-pads string [s] to [w] characters using spaces,
  * returning it unchanged if [s] is of length [w] or greater. *)
(*val right_space_padded_to : natural -> string -> string*)
let right_space_padded_to width str:string=
     (str ^ (padding_to ' ' width str))

(** [left_zero_padded_to w s] left-pads string [s] to [w] characters using zeroes,
  * returning it unchanged if [s] is of length [w] or greater. *)
(*val left_zero_padded_to : natural -> string -> string*)
let left_zero_padded_to width str:string=
     ((padding_to '0' width str) ^ str)

(** hex parsing *)

(*val natural_of_char : char -> natural*)
let natural_of_char c:Nat_big_num.num=
   (let naturalOrd c'=  (Nat_big_num.of_int (Char.code c')) in
  let n = (naturalOrd c) in
  if Nat_big_num.greater_equal n (naturalOrd '0') && Nat_big_num.less_equal n (naturalOrd '9') then Nat_big_num.sub_nat n (naturalOrd '0')
  else if Nat_big_num.greater_equal n (naturalOrd 'A') && Nat_big_num.less_equal n (naturalOrd 'F') then Nat_big_num.add (Nat_big_num.sub_nat n (naturalOrd 'A'))( (Nat_big_num.of_int 10))
  else if Nat_big_num.greater_equal n (naturalOrd 'a') && Nat_big_num.less_equal n (naturalOrd 'f') then Nat_big_num.add (Nat_big_num.sub_nat n (naturalOrd 'a'))( (Nat_big_num.of_int 10))
  else failwith ("natural_of_char argument #'" ^ (Xstring.implode [c] ^ "' not in 0-9,A-F,a-f")))

(*val natural_of_hex' : list char -> natural*)
let rec natural_of_hex' cs:Nat_big_num.num=
   ((match cs with
  | c :: cs' -> Nat_big_num.add (natural_of_char c) (Nat_big_num.mul( (Nat_big_num.of_int 16)) (natural_of_hex' cs'))
  | [] -> (Nat_big_num.of_int 0)
  ))

(*val natural_of_hex : string -> natural*)
let natural_of_hex s:Nat_big_num.num=
   (let cs = (Xstring.explode s) in
  (match cs with
  | '0'::'x'::cs' ->
      (match cs' with
      | c :: _ -> natural_of_hex' (List.rev cs')
      | [] -> failwith ("natural_of_hex argument \"" ^ (s ^ "\" has no digits"))
      )
  | _ -> failwith ("natural_of_hex argument \"" ^ (s ^ "\" does not begin 0x"))
  ))

let assert_unwrap_maybe maybe1:'a=
   ((match maybe1 with
    | Some v -> v
    | None -> failwith "assert_unwrap_maybe: nothing"
  ))