source: extracted/bitVector.ml @ 2746

Last change on this file since 2746 was 2649, checked in by sacerdot, 7 years ago

...

File size: 2.7 KB
Line 
1open Preamble
2
3open Bool
4
5open Hints_declaration
6
7open Core_notation
8
9open Pts
10
11open Logic
12
13open Relations
14
15open Nat
16
17open Div_and_mod
18
19open Jmeq
20
21open Russell
22
23open Types
24
25open List
26
27open Util
28
29open FoldStuff
30
31open Extranat
32
33open Vector
34
35type bitVector = Bool.bool Vector.vector
36
37type bit = Bool.bool
38
39type nibble = bitVector
40
41type byte7 = bitVector
42
43type byte = bitVector
44
45type word = bitVector
46
47type word11 = bitVector
48
49(** val zero : Nat.nat -> bitVector **)
50let zero n =
51  Vector.replicate n Bool.False
52
53(** val maximum : Nat.nat -> bitVector **)
54let maximum n =
55  Vector.replicate n Bool.True
56
57(** val pad : Nat.nat -> Nat.nat -> bitVector -> Bool.bool Vector.vector **)
58let pad m n b =
59  Vector.pad_vector Bool.False m n b
60
61(** val nat_to_bv : Nat.nat -> Nat.nat -> bitVector **)
62let rec nat_to_bv n k =
63  match n with
64  | Nat.O -> Vector.VEmpty
65  | Nat.S n' ->
66    Vector.VCons (n',
67      (Nat.eqb (Util.modulus k (Nat.S (Nat.S Nat.O))) (Nat.S Nat.O)),
68      (nat_to_bv n' (Util.division k (Nat.S (Nat.S Nat.O)))))
69
70(** val bv_to_nat : Nat.nat -> bitVector -> Nat.nat **)
71let rec bv_to_nat n = function
72| Vector.VEmpty -> Nat.O
73| Vector.VCons (n', x, b') ->
74  Nat.plus
75    (match x with
76     | Bool.True -> Nat.S Nat.O
77     | Bool.False -> Nat.O)
78    (Nat.times (bv_to_nat n' b') (Nat.S (Nat.S Nat.O)))
79
80(** val conjunction_bv : Nat.nat -> bitVector -> bitVector -> bitVector **)
81let conjunction_bv n b c =
82  Vector.zip_with n Bool.andb b c
83
84(** val inclusive_disjunction_bv :
85    Nat.nat -> bitVector -> bitVector -> Bool.bool Vector.vector **)
86let inclusive_disjunction_bv n b c =
87  Vector.zip_with n Bool.orb b c
88
89(** val exclusive_disjunction_bv :
90    Nat.nat -> bitVector -> bitVector -> Bool.bool Vector.vector **)
91let exclusive_disjunction_bv n b c =
92  Vector.zip_with n Bool.xorb b c
93
94(** val negation_bv : Nat.nat -> bitVector -> Bool.bool Vector.vector **)
95let negation_bv n b =
96  Vector.map0 n Bool.notb b
97
98(** val eq_b : Bool.bool -> Bool.bool -> Bool.bool **)
99let eq_b b c =
100  match b with
101  | Bool.True -> c
102  | Bool.False -> Bool.notb c
103
104(** val eq_bv : Nat.nat -> bitVector -> bitVector -> Bool.bool **)
105let eq_bv n b c =
106  Vector.eq_v n eq_b b c
107
108(** val eq_bv_elim :
109    Nat.nat -> bitVector -> bitVector -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
110let eq_bv_elim n x y ht hf =
111  Vector.eq_v_elim eq_b (fun _ clearme ->
112    match clearme with
113    | Bool.True ->
114      (fun clearme0 ->
115        match clearme0 with
116        | Bool.True -> (fun auto auto' -> auto __)
117        | Bool.False -> (fun auto auto' -> auto' __))
118    | Bool.False ->
119      (fun clearme0 ->
120        match clearme0 with
121        | Bool.True -> (fun auto auto' -> auto' __)
122        | Bool.False -> (fun auto auto' -> auto __))) n x y ht hf
123
Note: See TracBrowser for help on using the repository browser.