source: extracted/bitVectorZ.ml @ 2601

Last change on this file since 2601 was 2601, checked in by sacerdot, 8 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.6 KB
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
49(** val z_of_unsigned_bitvector : Nat.nat -> BitVector.bitVector -> Z.z **)
50let rec z_of_unsigned_bitvector n = function
51| Vector.VEmpty -> Z.OZ
52| Vector.VCons (n', h, t) ->
53  (match h with
54   | Bool.True ->
55     Z.Pos
56       (Vector.fold_left n' (fun acc b ->
57         match b with
58         | Bool.True -> Positive.P1 acc
59         | Bool.False -> Positive.P0 acc) Positive.One t)
60   | Bool.False -> z_of_unsigned_bitvector n' t)
61
62(** val z_of_signed_bitvector : Nat.nat -> BitVector.bitVector -> Z.z **)
63let z_of_signed_bitvector n = function
64| Vector.VEmpty -> Z.OZ
65| Vector.VCons (n', h, t) ->
66  (match h with
67   | Bool.True ->
68     Z.zopp
69       (Z.zsucc (z_of_unsigned_bitvector n' (BitVector.negation_bv n' t)))
70   | Bool.False -> z_of_unsigned_bitvector n' t)
71
72(** val bits_of_pos : Positive.pos -> Bool.bool List.list **)
73let rec bits_of_pos = function
74| Positive.One -> List.Cons (Bool.True, List.Nil)
75| Positive.P1 p' -> List.Cons (Bool.True, (bits_of_pos p'))
76| Positive.P0 p' -> List.Cons (Bool.False, (bits_of_pos p'))
77
78(** val zeroext_reversed :
79    Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
80let rec zeroext_reversed n m bv =
81  match m with
82  | Nat.O -> Vector.VEmpty
83  | Nat.S m' ->
84    (match bv with
85     | Vector.VEmpty -> BitVector.zero (Nat.S m')
86     | Vector.VCons (n', h, t) ->
87       Vector.VCons (m', h, (zeroext_reversed n' m' t)))
88
89(** val bitvector_of_Z : Nat.nat -> Z.z -> BitVector.bitVector **)
90let rec bitvector_of_Z n = function
91| Z.OZ -> BitVector.zero n
92| Z.Pos p ->
93  let bits = bits_of_pos p in
94  Vector.reverse0 n
95    (zeroext_reversed (List.length bits) n (Vector.vector_of_list bits))
96| Z.Neg p ->
97  (match p with
98   | Positive.One -> BitVector.maximum n
99   | Positive.P1 x ->
100     let bits = bits_of_pos (Positive.pred0 p) in
101     let pz =
102       Vector.reverse0 n
103         (zeroext_reversed (List.length bits) n (Vector.vector_of_list bits))
104     in
105     BitVector.negation_bv n pz
106   | Positive.P0 x ->
107     let bits = bits_of_pos (Positive.pred0 p) in
108     let pz =
109       Vector.reverse0 n
110         (zeroext_reversed (List.length bits) n (Vector.vector_of_list bits))
111     in
112     BitVector.negation_bv n pz)
113
114(** val pos_length : Positive.pos -> Nat.nat **)
115let rec pos_length = function
116| Positive.One -> Nat.O
117| Positive.P1 q -> Nat.S (pos_length q)
118| Positive.P0 q -> Nat.S (pos_length q)
119
Note: See TracBrowser for help on using the repository browser.