extracted/bitVectorZ.ml

   1 open Preamble
   2
   3 open Types
   4
   5 open Bool
   6
   7 open Relations
   8
   9 open Nat
  10
  11 open Hints_declaration
  12
  13 open Core_notation
  14
  15 open Pts
  16
  17 open Logic
  18
  19 open Positive
  20
  21 open Z
  22
  23 open Setoids
  24
  25 open Monad
  26
  27 open Option
  28
  29 open Extranat
  30
  31 open Vector
  32
  33 open Div_and_mod
  34
  35 open Jmeq
  36
  37 open Russell
  38
  39 open List
  40
  41 open Util
  42
  43 open FoldStuff
  44
  45 open BitVector
  46
  47 open Exp
  48
  49 open Arithmetic
  50
  51 open Division
  52
  53 (** val z_of_unsigned_bitvector : Nat.nat -> BitVector.bitVector -> Z.z **)
  54 let rec z_of_unsigned_bitvector n = function
  55 | Vector.VEmpty -> Z.OZ
  56 | Vector.VCons (n', h, t) ->
  57   (match h with
  58    | Bool.True ->
  59      Z.Pos
  60        (Vector.fold_left n' (fun acc b ->
  61          match b with
  62          | Bool.True -> Positive.P1 acc
  63          | Bool.False -> Positive.P0 acc) Positive.One t)
  64    | Bool.False -> z_of_unsigned_bitvector n' t)
  65
  66 (** val z_of_signed_bitvector : Nat.nat -> BitVector.bitVector -> Z.z **)
  67 let z_of_signed_bitvector n = function
  68 | Vector.VEmpty -> Z.OZ
  69 | Vector.VCons (n', h, t) ->
  70   (match h with
  71    | Bool.True ->
  72      Z.zopp
  73        (Z.zsucc (z_of_unsigned_bitvector n' (BitVector.negation_bv n' t)))
  74    | Bool.False -> z_of_unsigned_bitvector n' t)
  75
  76 (** val bits_of_pos : Positive.pos -> Bool.bool List.list **)
  77 let rec bits_of_pos = function
  78 | Positive.One -> List.Cons (Bool.True, List.Nil)
  79 | Positive.P1 p' -> List.Cons (Bool.True, (bits_of_pos p'))
  80 | Positive.P0 p' -> List.Cons (Bool.False, (bits_of_pos p'))
  81
  82 (** val zeroext_reversed :
  83     Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
  84 let rec zeroext_reversed n m bv =
  85   match m with
  86   | Nat.O -> Vector.VEmpty
  87   | Nat.S m' ->
  88     (match bv with
  89      | Vector.VEmpty -> BitVector.zero (Nat.S m')
  90      | Vector.VCons (n', h, t) ->
  91        Vector.VCons (m', h, (zeroext_reversed n' m' t)))
  92
  93 (** val bitvector_of_Z : Nat.nat -> Z.z -> BitVector.bitVector **)
  94 let rec bitvector_of_Z n = function
  95 | Z.OZ -> BitVector.zero n
  96 | Z.Pos p ->
  97   let bits = bits_of_pos p in
  98   Vector.reverse n
  99     (zeroext_reversed (List.length bits) n (Vector.vector_of_list bits))
 100 | Z.Neg p ->
 101   (match p with
 102    | Positive.One -> BitVector.maximum n
 103    | Positive.P1 x ->
 104      let bits = bits_of_pos (Positive.pred p) in
 105      let pz =
 106        Vector.reverse n
 107          (zeroext_reversed (List.length bits) n (Vector.vector_of_list bits))
 108      in
 109      BitVector.negation_bv n pz
 110    | Positive.P0 x ->
 111      let bits = bits_of_pos (Positive.pred p) in
 112      let pz =
 113        Vector.reverse n
 114          (zeroext_reversed (List.length bits) n (Vector.vector_of_list bits))
 115      in
 116      BitVector.negation_bv n pz)
 117
 118 (** val pos_length : Positive.pos -> Nat.nat **)
 119 let rec pos_length = function
 120 | Positive.One -> Nat.O
 121 | Positive.P1 q -> Nat.S (pos_length q)
 122 | Positive.P0 q -> Nat.S (pos_length q)
 123