source: extracted/bitVector.ml @ 2601

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

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

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
35open Char
36
37open String
38
39type bitVector = Bool.bool Vector.vector
40
41type bit = Bool.bool
42
43type nibble = bitVector
44
45type byte7 = bitVector
46
47type byte = bitVector
48
49type word = bitVector
50
51type word11 = bitVector
52
53(** val zero : Nat.nat -> bitVector **)
54let zero n =
55  Vector.replicate n Bool.False
56
57(** val maximum : Nat.nat -> bitVector **)
58let maximum n =
59  Vector.replicate n Bool.True
60
61(** val pad : Nat.nat -> Nat.nat -> bitVector -> Bool.bool Vector.vector **)
62let pad m n b =
63  Vector.pad_vector Bool.False m n b
64
65(** val nat_to_bv : Nat.nat -> Nat.nat -> bitVector **)
66let rec nat_to_bv n k =
67  match n with
68  | Nat.O -> Vector.VEmpty
69  | Nat.S n' ->
70    Vector.VCons (n',
71      (Nat.eqb (Util.modulus k (Nat.S (Nat.S Nat.O))) (Nat.S Nat.O)),
72      (nat_to_bv n' (Util.division k (Nat.S (Nat.S Nat.O)))))
73
74(** val bv_to_nat : Nat.nat -> bitVector -> Nat.nat **)
75let rec bv_to_nat n = function
76| Vector.VEmpty -> Nat.O
77| Vector.VCons (n', x, b') ->
78  Nat.plus
79    (match x with
80     | Bool.True -> Nat.S Nat.O
81     | Bool.False -> Nat.O)
82    (Nat.times (bv_to_nat n' b') (Nat.S (Nat.S Nat.O)))
83
84(** val conjunction_bv : Nat.nat -> bitVector -> bitVector -> bitVector **)
85let conjunction_bv n b c =
86  Vector.zip_with n Bool.andb b c
87
88(** val inclusive_disjunction_bv :
89    Nat.nat -> bitVector -> bitVector -> Bool.bool Vector.vector **)
90let inclusive_disjunction_bv n b c =
91  Vector.zip_with n Bool.orb b c
92
93(** val exclusive_disjunction_bv :
94    Nat.nat -> bitVector -> bitVector -> Bool.bool Vector.vector **)
95let exclusive_disjunction_bv n b c =
96  Vector.zip_with n Bool.xorb b c
97
98(** val negation_bv : Nat.nat -> bitVector -> Bool.bool Vector.vector **)
99let negation_bv n b =
100  Vector.map0 n Bool.notb b
101
102(** val eq_b : Bool.bool -> Bool.bool -> Bool.bool **)
103let eq_b b c =
104  match b with
105  | Bool.True -> c
106  | Bool.False -> Bool.notb c
107
108(** val eq_bv : Nat.nat -> bitVector -> bitVector -> Bool.bool **)
109let eq_bv n b c =
110  Vector.eq_v n eq_b b c
111
112(** val eq_bv_elim :
113    Nat.nat -> bitVector -> bitVector -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
114let eq_bv_elim n x y ht hf =
115  Vector.eq_v_elim eq_b (fun _ clearme ->
116    match clearme with
117    | Bool.True ->
118      (fun clearme0 ->
119        match clearme0 with
120        | Bool.True -> (fun auto auto' -> auto __)
121        | Bool.False -> (fun auto auto' -> auto' __))
122    | Bool.False ->
123      (fun clearme0 ->
124        match clearme0 with
125        | Bool.True -> (fun auto auto' -> auto' __)
126        | Bool.False -> (fun auto auto' -> auto __))) n x y ht hf
Note: See TracBrowser for help on using the repository browser.