source: driver/extracted/bitVectorZ.ml @ 3106

Last change on this file since 3106 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 2.7 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 Setoids
24
25open Monad
26
27open Option
28
29open Extranat
30
31open Vector
32
33open Div_and_mod
34
35open Jmeq
36
37open Russell
38
39open List
40
41open Util
42
43open FoldStuff
44
45open BitVector
46
47open Exp
48
49open Arithmetic
50
51open Division
52
53(** val z_of_unsigned_bitvector : Nat.nat -> BitVector.bitVector -> Z.z **)
54let rec z_of_unsigned_bitvector n = function
55| Vector.VEmpty -> Z.OZ
56| Vector.VCons (n', h, t) ->
57  (match h with
58   | Bool.True ->
59     Z.Pos
60       (Vector.fold_left n' (fun acc b ->
61         match b with
62         | Bool.True -> Positive.P1 acc
63         | Bool.False -> Positive.P0 acc) Positive.One t)
64   | Bool.False -> z_of_unsigned_bitvector n' t)
65
66(** val z_of_signed_bitvector : Nat.nat -> BitVector.bitVector -> Z.z **)
67let z_of_signed_bitvector n = function
68| Vector.VEmpty -> Z.OZ
69| Vector.VCons (n', h, t) ->
70  (match h with
71   | Bool.True ->
72     Z.zopp
73       (Z.zsucc (z_of_unsigned_bitvector n' (BitVector.negation_bv n' t)))
74   | Bool.False -> z_of_unsigned_bitvector n' t)
75
76(** val bits_of_pos : Positive.pos -> Bool.bool List.list **)
77let rec bits_of_pos = function
78| Positive.One -> List.Cons (Bool.True, List.Nil)
79| Positive.P1 p' -> List.Cons (Bool.True, (bits_of_pos p'))
80| Positive.P0 p' -> List.Cons (Bool.False, (bits_of_pos p'))
81
82(** val zeroext_reversed :
83    Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
84let rec zeroext_reversed n m bv =
85  match m with
86  | Nat.O -> Vector.VEmpty
87  | Nat.S m' ->
88    (match bv with
89     | Vector.VEmpty -> BitVector.zero (Nat.S m')
90     | Vector.VCons (n', h, t) ->
91       Vector.VCons (m', h, (zeroext_reversed n' m' t)))
92
93(** val bitvector_of_Z : Nat.nat -> Z.z -> BitVector.bitVector **)
94let rec bitvector_of_Z n = function
95| Z.OZ -> BitVector.zero n
96| Z.Pos p ->
97  let bits = bits_of_pos p in
98  Vector.reverse n
99    (zeroext_reversed (List.length bits) n (Vector.vector_of_list bits))
100| Z.Neg p ->
101  (match p with
102   | Positive.One -> BitVector.maximum n
103   | Positive.P1 x ->
104     let bits = bits_of_pos (Positive.pred p) in
105     let pz =
106       Vector.reverse n
107         (zeroext_reversed (List.length bits) n (Vector.vector_of_list bits))
108     in
109     BitVector.negation_bv n pz
110   | Positive.P0 x ->
111     let bits = bits_of_pos (Positive.pred p) in
112     let pz =
113       Vector.reverse n
114         (zeroext_reversed (List.length bits) n (Vector.vector_of_list bits))
115     in
116     BitVector.negation_bv n pz)
117
118(** val pos_length : Positive.pos -> Nat.nat **)
119let rec pos_length = function
120| Positive.One -> Nat.O
121| Positive.P1 q -> Nat.S (pos_length q)
122| Positive.P0 q -> Nat.S (pos_length q)
123
Note: See TracBrowser for help on using the repository browser.