source: extracted/bitVector.ml @ 2773

Last change on this file since 2773 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
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 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 nat_to_bv : Nat.nat -> Nat.nat -> bitVector **)
68let rec nat_to_bv n k =
69  match n with
70  | Nat.O -> Vector.VEmpty
71  | Nat.S n' ->
72    Vector.VCons (n',
73      (Nat.eqb (Util.modulus k (Nat.S (Nat.S Nat.O))) (Nat.S Nat.O)),
74      (nat_to_bv n' (Util.division k (Nat.S (Nat.S Nat.O)))))
75
76(** val bv_to_nat : Nat.nat -> bitVector -> Nat.nat **)
77let rec bv_to_nat n = function
78| Vector.VEmpty -> Nat.O
79| Vector.VCons (n', x, b') ->
80  Nat.plus
81    (match x with
82     | Bool.True -> Nat.S Nat.O
83     | Bool.False -> Nat.O)
84    (Nat.times (bv_to_nat n' b') (Nat.S (Nat.S Nat.O)))
85
86(** val conjunction_bv : Nat.nat -> bitVector -> bitVector -> bitVector **)
87let conjunction_bv n b c =
88  Vector.zip_with n Bool.andb b c
89
90(** val inclusive_disjunction_bv :
91    Nat.nat -> bitVector -> bitVector -> Bool.bool Vector.vector **)
92let inclusive_disjunction_bv n b c =
93  Vector.zip_with n Bool.orb b c
94
95(** val exclusive_disjunction_bv :
96    Nat.nat -> bitVector -> bitVector -> Bool.bool Vector.vector **)
97let exclusive_disjunction_bv n b c =
98  Vector.zip_with n Bool.xorb b c
99
100(** val negation_bv : Nat.nat -> bitVector -> Bool.bool Vector.vector **)
101let negation_bv n b =
102  Vector.map n Bool.notb b
103
104(** val eq_b : Bool.bool -> Bool.bool -> Bool.bool **)
105let eq_b b c =
106  match b with
107  | Bool.True -> c
108  | Bool.False -> Bool.notb c
109
110(** val eq_bv : Nat.nat -> bitVector -> bitVector -> Bool.bool **)
111let eq_bv n b c =
112  Vector.eq_v n eq_b b c
113
114(** val eq_bv_elim :
115    Nat.nat -> bitVector -> bitVector -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
116let eq_bv_elim n x y ht hf =
117  Vector.eq_v_elim eq_b (fun _ clearme ->
118    match clearme with
119    | Bool.True ->
120      (fun clearme0 ->
121        match clearme0 with
122        | Bool.True -> (fun auto auto' -> auto __)
123        | Bool.False -> (fun auto auto' -> auto' __))
124    | Bool.False ->
125      (fun clearme0 ->
126        match clearme0 with
127        | Bool.True -> (fun auto auto' -> auto' __)
128        | Bool.False -> (fun auto auto' -> auto __))) n x y ht hf
129
Note: See TracBrowser for help on using the repository browser.