source: extracted/bitVectorZ.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: 718 bytes
Line 
1open Preamble
2
3open Types
4
5open Bool
6
7open Relations
8
9open Nat
10
11open Hints_declaration
12
13open Core_notation
14
15open Pts
16
17open Logic
18
19open Positive
20
21open Z
22
23open Char
24
25open String
26
27open Extranat
28
29open Vector
30
31open Div_and_mod
32
33open Jmeq
34
35open Russell
36
37open List
38
39open Util
40
41open FoldStuff
42
43open BitVector
44
45open Arithmetic
46
47open Division
48
49val z_of_unsigned_bitvector : Nat.nat -> BitVector.bitVector -> Z.z
50
51val z_of_signed_bitvector : Nat.nat -> BitVector.bitVector -> Z.z
52
53val bits_of_pos : Positive.pos -> Bool.bool List.list
54
55val zeroext_reversed :
56  Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector
57
58val bitvector_of_Z : Nat.nat -> Z.z -> BitVector.bitVector
59
60val pos_length : Positive.pos -> Nat.nat
61
Note: See TracBrowser for help on using the repository browser.