source: extracted/bitVectorZ.ml @ 2746

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

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 Extranat
24
25open Vector
26
27open Div_and_mod
28
29open Jmeq
30
31open Russell
32
33open List
34
35open Util
36
37open FoldStuff
38
39open BitVector
40
41open Exp
42
43open Arithmetic
44
45open Division
46
47(** val z_of_unsigned_bitvector : Nat.nat -> BitVector.bitVector -> Z.z **)
48let rec z_of_unsigned_bitvector n = function
49| Vector.VEmpty -> Z.OZ
50| Vector.VCons (n', h, t) ->
51  (match h with
52   | Bool.True ->
53     Z.Pos
54       (Vector.fold_left n' (fun acc b ->
55         match b with
56         | Bool.True -> Positive.P1 acc
57         | Bool.False -> Positive.P0 acc) Positive.One t)
58   | Bool.False -> z_of_unsigned_bitvector n' t)
59
60(** val z_of_signed_bitvector : Nat.nat -> BitVector.bitVector -> Z.z **)
61let z_of_signed_bitvector n = function
62| Vector.VEmpty -> Z.OZ
63| Vector.VCons (n', h, t) ->
64  (match h with
65   | Bool.True ->
66     Z.zopp
67       (Z.zsucc (z_of_unsigned_bitvector n' (BitVector.negation_bv n' t)))
68   | Bool.False -> z_of_unsigned_bitvector n' t)
69
70(** val bits_of_pos : Positive.pos -> Bool.bool List.list **)
71let rec bits_of_pos = function
72| Positive.One -> List.Cons (Bool.True, List.Nil)
73| Positive.P1 p' -> List.Cons (Bool.True, (bits_of_pos p'))
74| Positive.P0 p' -> List.Cons (Bool.False, (bits_of_pos p'))
75
76(** val zeroext_reversed :
77    Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
78let rec zeroext_reversed n m bv =
79  match m with
80  | Nat.O -> Vector.VEmpty
81  | Nat.S m' ->
82    (match bv with
83     | Vector.VEmpty -> BitVector.zero (Nat.S m')
84     | Vector.VCons (n', h, t) ->
85       Vector.VCons (m', h, (zeroext_reversed n' m' t)))
86
87(** val bitvector_of_Z : Nat.nat -> Z.z -> BitVector.bitVector **)
88let rec bitvector_of_Z n = function
89| Z.OZ -> BitVector.zero n
90| Z.Pos p ->
91  let bits = bits_of_pos p in
92  Vector.reverse0 n
93    (zeroext_reversed (List.length bits) n (Vector.vector_of_list bits))
94| Z.Neg p ->
95  (match p with
96   | Positive.One -> BitVector.maximum n
97   | Positive.P1 x ->
98     let bits = bits_of_pos (Positive.pred0 p) in
99     let pz =
100       Vector.reverse0 n
101         (zeroext_reversed (List.length bits) n (Vector.vector_of_list bits))
102     in
103     BitVector.negation_bv n pz
104   | Positive.P0 x ->
105     let bits = bits_of_pos (Positive.pred0 p) in
106     let pz =
107       Vector.reverse0 n
108         (zeroext_reversed (List.length bits) n (Vector.vector_of_list bits))
109     in
110     BitVector.negation_bv n pz)
111
112(** val pos_length : Positive.pos -> Nat.nat **)
113let rec pos_length = function
114| Positive.One -> Nat.O
115| Positive.P1 q -> Nat.S (pos_length q)
116| Positive.P0 q -> Nat.S (pos_length q)
117
Note: See TracBrowser for help on using the repository browser.