extracted/untrusted/glue.ml

   1 let int_of_bitvector v =
   2   let rec aux pow v =
   3     match v with
   4       Vector.VEmpty -> 0
   5     | Vector.VCons (_,hd,tl) ->
   6         if hd = Bool.True then
   7           pow + (aux (pow * 2) tl)
   8         else
   9           aux (pow * 2) tl
  10   in
  11     aux 1 (Vector.reverse Nat.O v)
  12
  13 let rec int_of_matitapos =
  14  function
  15    Positive.One -> 1
  16  | Positive.P0 v -> int_of_matitapos v * 2
  17  | Positive.P1 v -> int_of_matitapos v * 2 + 1
  18
  19 let int_of_matitaZ =
  20  function
  21    Z.OZ -> 0
  22  | Z.Pos p -> int_of_matitapos p
  23  | Z.Neg p -> -(int_of_matitapos p)
  24
  25 let option_of_matitaoption =
  26  function
  27     Types.None -> None
  28   | Types.Some v -> Some v
  29
  30 let rec matitanat_of_int n =
  31  if n = 0 then Nat.O
  32  else if n < 0 then assert false
  33  else Nat.S (matitanat_of_int (n-1))
  34
  35 let rec int_of_matitanat =
  36  function
  37     Nat.O -> 0
  38   | Nat.S n -> int_of_matitanat n + 1
  39
  40 let int_pair_of_pointer { Pointers.pblock = bl ; Pointers.poff = off } =
  41   (int_of_matitaZ bl, int_of_bitvector off)