source: driver/extracted/bitVector.ml @ 3106

Last change on this file since 3106 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
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 Setoids
32
33open Monad
34
35open Option
36
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 =
83  Vector.map n Bool.notb b
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
110
Note: See TracBrowser for help on using the repository browser.