[2601] | 1 | open Preamble |
---|
| 2 | |
---|
| 3 | open Types |
---|
| 4 | |
---|
| 5 | open Bool |
---|
| 6 | |
---|
| 7 | open Relations |
---|
| 8 | |
---|
| 9 | open Nat |
---|
| 10 | |
---|
| 11 | open Hints_declaration |
---|
| 12 | |
---|
| 13 | open Core_notation |
---|
| 14 | |
---|
| 15 | open Pts |
---|
| 16 | |
---|
| 17 | open Logic |
---|
| 18 | |
---|
| 19 | open Positive |
---|
| 20 | |
---|
| 21 | open Z |
---|
| 22 | |
---|
| 23 | open Extranat |
---|
| 24 | |
---|
| 25 | open Vector |
---|
| 26 | |
---|
| 27 | open Div_and_mod |
---|
| 28 | |
---|
| 29 | open Jmeq |
---|
| 30 | |
---|
| 31 | open Russell |
---|
| 32 | |
---|
| 33 | open List |
---|
| 34 | |
---|
| 35 | open Util |
---|
| 36 | |
---|
| 37 | open FoldStuff |
---|
| 38 | |
---|
| 39 | open BitVector |
---|
| 40 | |
---|
| 41 | open Arithmetic |
---|
| 42 | |
---|
| 43 | open Division |
---|
| 44 | |
---|
| 45 | (** val z_of_unsigned_bitvector : Nat.nat -> BitVector.bitVector -> Z.z **) |
---|
| 46 | let rec z_of_unsigned_bitvector n = function |
---|
| 47 | | Vector.VEmpty -> Z.OZ |
---|
| 48 | | Vector.VCons (n', h, t) -> |
---|
| 49 | (match h with |
---|
| 50 | | Bool.True -> |
---|
| 51 | Z.Pos |
---|
| 52 | (Vector.fold_left n' (fun acc b -> |
---|
| 53 | match b with |
---|
| 54 | | Bool.True -> Positive.P1 acc |
---|
| 55 | | Bool.False -> Positive.P0 acc) Positive.One t) |
---|
| 56 | | Bool.False -> z_of_unsigned_bitvector n' t) |
---|
| 57 | |
---|
| 58 | (** val z_of_signed_bitvector : Nat.nat -> BitVector.bitVector -> Z.z **) |
---|
| 59 | let z_of_signed_bitvector n = function |
---|
| 60 | | Vector.VEmpty -> Z.OZ |
---|
| 61 | | Vector.VCons (n', h, t) -> |
---|
| 62 | (match h with |
---|
| 63 | | Bool.True -> |
---|
| 64 | Z.zopp |
---|
| 65 | (Z.zsucc (z_of_unsigned_bitvector n' (BitVector.negation_bv n' t))) |
---|
| 66 | | Bool.False -> z_of_unsigned_bitvector n' t) |
---|
| 67 | |
---|
| 68 | (** val bits_of_pos : Positive.pos -> Bool.bool List.list **) |
---|
| 69 | let rec bits_of_pos = function |
---|
| 70 | | Positive.One -> List.Cons (Bool.True, List.Nil) |
---|
| 71 | | Positive.P1 p' -> List.Cons (Bool.True, (bits_of_pos p')) |
---|
| 72 | | Positive.P0 p' -> List.Cons (Bool.False, (bits_of_pos p')) |
---|
| 73 | |
---|
| 74 | (** val zeroext_reversed : |
---|
| 75 | Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector **) |
---|
| 76 | let rec zeroext_reversed n m bv = |
---|
| 77 | match m with |
---|
| 78 | | Nat.O -> Vector.VEmpty |
---|
| 79 | | Nat.S m' -> |
---|
| 80 | (match bv with |
---|
| 81 | | Vector.VEmpty -> BitVector.zero (Nat.S m') |
---|
| 82 | | Vector.VCons (n', h, t) -> |
---|
| 83 | Vector.VCons (m', h, (zeroext_reversed n' m' t))) |
---|
| 84 | |
---|
| 85 | (** val bitvector_of_Z : Nat.nat -> Z.z -> BitVector.bitVector **) |
---|
| 86 | let rec bitvector_of_Z n = function |
---|
| 87 | | Z.OZ -> BitVector.zero n |
---|
| 88 | | Z.Pos p -> |
---|
| 89 | let bits = bits_of_pos p in |
---|
| 90 | Vector.reverse0 n |
---|
| 91 | (zeroext_reversed (List.length bits) n (Vector.vector_of_list bits)) |
---|
| 92 | | Z.Neg p -> |
---|
| 93 | (match p with |
---|
| 94 | | Positive.One -> BitVector.maximum n |
---|
| 95 | | Positive.P1 x -> |
---|
| 96 | let bits = bits_of_pos (Positive.pred0 p) in |
---|
| 97 | let pz = |
---|
| 98 | Vector.reverse0 n |
---|
| 99 | (zeroext_reversed (List.length bits) n (Vector.vector_of_list bits)) |
---|
| 100 | in |
---|
| 101 | BitVector.negation_bv n pz |
---|
| 102 | | Positive.P0 x -> |
---|
| 103 | let bits = bits_of_pos (Positive.pred0 p) in |
---|
| 104 | let pz = |
---|
| 105 | Vector.reverse0 n |
---|
| 106 | (zeroext_reversed (List.length bits) n (Vector.vector_of_list bits)) |
---|
| 107 | in |
---|
| 108 | BitVector.negation_bv n pz) |
---|
| 109 | |
---|
| 110 | (** val pos_length : Positive.pos -> Nat.nat **) |
---|
| 111 | let rec pos_length = function |
---|
| 112 | | Positive.One -> Nat.O |
---|
| 113 | | Positive.P1 q -> Nat.S (pos_length q) |
---|
| 114 | | Positive.P0 q -> Nat.S (pos_length q) |
---|
| 115 | |
---|