extracted/bitVector.ml

   1 open Preamble
   2
   3 open Bool
   4
   5 open Hints_declaration
   6
   7 open Core_notation
   8
   9 open Pts
  10
  11 open Logic
  12
  13 open Relations
  14
  15 open Nat
  16
  17 open Div_and_mod
  18
  19 open Jmeq
  20
  21 open Russell
  22
  23 open Types
  24
  25 open List
  26
  27 open Util
  28
  29 open FoldStuff
  30
  31 open Setoids
  32
  33 open Monad
  34
  35 open Option
  36
  37 open Extranat
  38
  39 open Vector
  40
  41 type bitVector = Bool.bool Vector.vector
  42
  43 type bit = Bool.bool
  44
  45 type nibble = bitVector
  46
  47 type byte7 = bitVector
  48
  49 type byte = bitVector
  50
  51 type word = bitVector
  52
  53 type word11 = bitVector
  54
  55 (** val zero : Nat.nat -> bitVector **)
  56 let zero n =
  57   Vector.replicate n Bool.False
  58
  59 (** val maximum : Nat.nat -> bitVector **)
  60 let maximum n =
  61   Vector.replicate n Bool.True
  62
  63 (** val pad : Nat.nat -> Nat.nat -> bitVector -> Bool.bool Vector.vector **)
  64 let pad m n b =
  65   Vector.pad_vector Bool.False m n b
  66
  67 (** val conjunction_bv : Nat.nat -> bitVector -> bitVector -> bitVector **)
  68 let conjunction_bv n b c =
  69   Vector.zip_with n Bool.andb b c
  70
  71 (** val inclusive_disjunction_bv :
  72     Nat.nat -> bitVector -> bitVector -> Bool.bool Vector.vector **)
  73 let inclusive_disjunction_bv n b c =
  74   Vector.zip_with n Bool.orb b c
  75
  76 (** val exclusive_disjunction_bv :
  77     Nat.nat -> bitVector -> bitVector -> Bool.bool Vector.vector **)
  78 let exclusive_disjunction_bv n b c =
  79   Vector.zip_with n Bool.xorb b c
  80
  81 (** val negation_bv : Nat.nat -> bitVector -> Bool.bool Vector.vector **)
  82 let negation_bv n b =
  83   Vector.map n Bool.notb b
  84
  85 (** val eq_b : Bool.bool -> Bool.bool -> Bool.bool **)
  86 let eq_b b c =
  87   match b with
  88   | Bool.True -> c
  89   | Bool.False -> Bool.notb c
  90
  91 (** val eq_bv : Nat.nat -> bitVector -> bitVector -> Bool.bool **)
  92 let eq_bv n b c =
  93   Vector.eq_v n eq_b b c
  94
  95 (** val eq_bv_elim :
  96     Nat.nat -> bitVector -> bitVector -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
  97 let eq_bv_elim n x y ht hf =
  98   Vector.eq_v_elim eq_b (fun _ clearme ->
  99     match clearme with
 100     | Bool.True ->
 101       (fun clearme0 ->
 102         match clearme0 with
 103         | Bool.True -> (fun auto auto' -> auto __)
 104         | Bool.False -> (fun auto auto' -> auto' __))
 105     | Bool.False ->
 106       (fun clearme0 ->
 107         match clearme0 with
 108         | Bool.True -> (fun auto auto' -> auto' __)
 109         | Bool.False -> (fun auto auto' -> auto __))) n x y ht hf
 110