source: extracted/bitVector.ml @ 2890

Last change on this file since 2890 was 2780, checked in by sacerdot, 7 years ago

Bug fixed: in BitVector?.ma the functions bv_to_nat and nat_to_bv were
using the wrong indianess. They were also redundant with the good
(but inefficient) ones in Arithmetic.ma.

On a simple test the compiled code runs (I have not checked the
result).

File size: 2.1 KB
RevLine 
[2601]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
[2773]31open Setoids
32
33open Monad
34
35open Option
36
[2601]37open Extranat
38
39open Vector
40
41type bitVector = Bool.bool Vector.vector
42
43type bit = Bool.bool
44
45type nibble = bitVector
46
47type byte7 = bitVector
48
49type byte = bitVector
50
51type word = bitVector
52
53type word11 = bitVector
54
55(** val zero : Nat.nat -> bitVector **)
56let zero n =
57  Vector.replicate n Bool.False
58
59(** val maximum : Nat.nat -> bitVector **)
60let maximum n =
61  Vector.replicate n Bool.True
62
63(** val pad : Nat.nat -> Nat.nat -> bitVector -> Bool.bool Vector.vector **)
64let pad m n b =
65  Vector.pad_vector Bool.False m n b
66
67(** val conjunction_bv : Nat.nat -> bitVector -> bitVector -> bitVector **)
68let 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 **)
73let 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 **)
78let 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 **)
82let negation_bv n b =
[2773]83  Vector.map n Bool.notb b
[2601]84
85(** val eq_b : Bool.bool -> Bool.bool -> Bool.bool **)
86let 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 **)
92let 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 **)
97let 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
[2649]110
Note: See TracBrowser for help on using the repository browser.