source: extracted/bitVector.mli @ 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: 1.2 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
53val zero : Nat.nat -> bitVector
54
55val maximum : Nat.nat -> bitVector
56
57val pad : Nat.nat -> Nat.nat -> bitVector -> Bool.bool Vector.vector
58
59val nat_to_bv : Nat.nat -> Nat.nat -> bitVector
60
61val bv_to_nat : Nat.nat -> bitVector -> Nat.nat
62
63val conjunction_bv : Nat.nat -> bitVector -> bitVector -> bitVector
64
65val inclusive_disjunction_bv :
66  Nat.nat -> bitVector -> bitVector -> Bool.bool Vector.vector
67
68val exclusive_disjunction_bv :
69  Nat.nat -> bitVector -> bitVector -> Bool.bool Vector.vector
70
71val negation_bv : Nat.nat -> bitVector -> Bool.bool Vector.vector
72
73val eq_b : Bool.bool -> Bool.bool -> Bool.bool
74
75val eq_bv : Nat.nat -> bitVector -> bitVector -> Bool.bool
76
77val eq_bv_elim :
78  Nat.nat -> bitVector -> bitVector -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
Note: See TracBrowser for help on using the repository browser.