source: src/ASM/new-matita-development/Arithmetic.ma @ 688

Last change on this file since 688 was 475, checked in by mulligan, 10 years ago

Matita interpreter ported to latest version of matita (the one with the tabs). To use, this directory must be copied into the /lib directory in the matita directory.

File size: 6.8 KB
Line 
1include "cerco/BitVector.ma".
2include "cerco/Util.ma".
3
4definition nat_of_bool ≝
5  λb: bool.
6    match b with
7      [ false ⇒ O
8      | true ⇒ S O
9      ].
10   
11definition add_n_with_carry:
12      ∀n: nat. ∀b, c: BitVector n. ∀carry: bool. (BitVector n) × (BitVector 3) ≝
13  λn: nat.
14  λb: BitVector n.
15  λc: BitVector n.
16  λcarry: bool.
17    let b_as_nat ≝ nat_of_bitvector n b in
18    let c_as_nat ≝ nat_of_bitvector n c in
19    let carry_as_nat ≝ nat_of_bool carry in
20    let result_old ≝ b_as_nat + c_as_nat + carry_as_nat in
21    let ac_flag ≝ geb ((modulus b_as_nat (2 * n)) +
22                  (modulus c_as_nat (2 * n)) +
23                  c_as_nat) (2 * n) in
24    let bit_xxx ≝ geb ((modulus b_as_nat (2^(n - 1))) +
25                  (modulus c_as_nat (2^(n - 1))) +
26                  c_as_nat) (2^(n - 1)) in
27    let result ≝ modulus result_old (2^n) in
28    let cy_flag ≝ geb result_old (2^n) in
29    let ov_flag ≝ exclusive_disjunction cy_flag bit_xxx in
30      mk_pair ? ? (bitvector_of_nat n result)
31                       ([[ cy_flag ; ac_flag ; ov_flag ]]).
32
33definition sub_n_with_carry: ∀n: nat. ∀b,c: BitVector n. ∀carry: bool. (BitVector n) × (BitVector 3) ≝
34  λn: nat.
35  λb: BitVector n.
36  λc: BitVector n.
37  λcarry: bool.
38     let b_as_nat ≝ nat_of_bitvector n b in
39     let c_as_nat ≝ nat_of_bitvector n c in
40     let carry_as_nat ≝ nat_of_bool carry in
41     let temporary ≝ (b_as_nat mod (2 * n)) - (c_as_nat mod (2 * n)) in
42     let ac_flag ≝ ltb (b_as_nat mod (2 * n)) ((c_as_nat mod (2 * n)) + carry_as_nat) in
43     let bit_six ≝ ltb (b_as_nat mod (2^(n - 1))) ((c_as_nat mod (2^(n - 1))) + carry_as_nat) in
44     let 〈b',cy_flag〉 ≝
45       if geb b_as_nat (c_as_nat + carry_as_nat) then
46         〈b_as_nat, false〉
47       else
48         〈b_as_nat + (2^n), true〉
49     in
50       let ov_flag ≝ exclusive_disjunction cy_flag bit_six in
51         〈bitvector_of_nat n ((b' - c_as_nat) - carry_as_nat), [[ cy_flag; ac_flag; ov_flag ]]〉.         
52         
53definition add_8_with_carry ≝ add_n_with_carry 8.
54definition add_16_with_carry ≝ add_n_with_carry 16.
55definition sub_8_with_carry ≝ sub_n_with_carry 8.
56definition sub_16_with_carry ≝ sub_n_with_carry 16.
57
58definition increment ≝
59  λn: nat.
60  λb: BitVector n.
61    let b_as_nat ≝ (nat_of_bitvector n b) + 1 in
62    let overflow ≝ geb b_as_nat 2^n in
63      match overflow with
64        [ false ⇒ bitvector_of_nat n b_as_nat
65        | true ⇒ zero n
66        ].
67       
68definition decrement ≝
69  λn: nat.
70  λb: BitVector n.
71    let b_as_nat ≝ nat_of_bitvector n b in
72      match b_as_nat with
73        [ O ⇒ maximum n
74        | S o ⇒ bitvector_of_nat n o
75        ].
76   
77definition two_complement_negation ≝
78  λn: nat.
79  λb: BitVector n.
80    let new_b ≝ negation_bv n b in
81      increment n new_b.
82   
83definition addition_n ≝
84  λn: nat.
85  λb, c: BitVector n.
86    let 〈res,flags〉 ≝ add_n_with_carry n b c false in
87      res.
88   
89definition subtraction ≝
90  λn: nat.
91  λb, c: BitVector n.
92    addition_n n b (two_complement_negation n c).
93   
94definition multiplication ≝
95  λn: nat.
96  λb, c: BitVector n.
97    let b_nat ≝ nat_of_bitvector ? b in
98    let c_nat ≝ nat_of_bitvector ? c in
99    let result ≝ b_nat * c_nat in
100      bitvector_of_nat (n + n) result.
101     
102definition division_u ≝
103  λn: nat.
104  λb, c: BitVector n.
105    let b_nat ≝ nat_of_bitvector ? b in
106    let c_nat ≝ nat_of_bitvector ? c in
107    match c_nat with
108    [ O ⇒ None ?
109    | _ ⇒
110      let result ≝ b_nat ÷ c_nat in
111        Some ? (bitvector_of_nat n result)
112    ].
113   
114alias id "option1" = "cic:/matita/basics/sums/option.ind(1,0,1)".
115     
116definition division_s: ∀n. ∀b, c: BitVector n. option1 (BitVector n) ≝
117  λn.
118    match n with
119    [ O ⇒ λb, c. None ?
120    | S p ⇒ λb, c: BitVector (S p).
121        let b_sign_bit ≝ get_index_v ? ? b O ? in
122        let c_sign_bit ≝ get_index_v ? ? c O ? in
123        let b_as_nat ≝ nat_of_bitvector ? b in
124        let c_as_nat ≝ nat_of_bitvector ? c in
125        match c_as_nat with
126        [ O ⇒ None ?
127        | S o ⇒
128          match b_sign_bit with
129          [ true ⇒
130            let temp_b ≝ b_as_nat - (2^p) in
131            match c_sign_bit with
132            [ true ⇒
133              let temp_c ≝ c_as_nat - (2^p) in
134                Some ? (bitvector_of_nat ? (temp_b ÷ temp_c))
135            | false ⇒
136              let result ≝ (temp_b ÷ c_as_nat) + (2^p) in
137                Some ? (bitvector_of_nat ? result)
138            ]
139          | false ⇒
140            match c_sign_bit with
141            [ true ⇒
142              let temp_c ≝ c_as_nat - (2^p) in
143              let result ≝ (b_as_nat ÷ temp_c) + (2^p) in
144                Some ? (bitvector_of_nat ? result)
145            | false ⇒ Some ? (bitvector_of_nat ? (b_as_nat ÷ c_as_nat))
146            ]
147          ]
148        ]
149    ].
150    //
151qed.
152
153definition modulus_u ≝
154  λn.
155  λb, c: BitVector n.
156    let b_nat ≝ nat_of_bitvector ? b in
157    let c_nat ≝ nat_of_bitvector ? c in
158    let result ≝ modulus b_nat c_nat in
159      bitvector_of_nat (n + n) result.
160           
161definition modulus_s ≝
162  λn.
163  λb, c: BitVector n.
164    match division_s n b c with
165      [ None ⇒ None ?
166      | Some result ⇒
167          let 〈high_bits, low_bits〉 ≝ split bool ? n (multiplication n result c) in
168            Some ? (subtraction n b low_bits)
169      ].
170     
171definition lt_u ≝
172  λn.
173  λb, c: BitVector n.
174    let b_nat ≝ nat_of_bitvector ? b in
175    let c_nat ≝ nat_of_bitvector ? c in
176      ltb b_nat c_nat.
177     
178definition gt_u ≝ λn, b, c. lt_u n c b.
179
180definition lte_u ≝ λn, b, c. ¬(gt_u n b c).
181
182definition gte_u ≝ λn, b, c. ¬(lt_u n b c).
183     
184definition lt_s ≝
185  λn.
186  λb, c: BitVector n.
187    let 〈result, flags〉 ≝ sub_n_with_carry n b c false in
188    let ov_flag ≝ get_index_v ? ? flags 2 ? in
189     if ov_flag then
190       true
191     else
192       ((match n return λn'.BitVector n' → bool with
193       [ O ⇒ λ_.false
194       | S o ⇒
195         λresult'.(get_index_v ? ? result' O ?)
196       ]) result).
197  //
198qed.
199
200definition gt_s ≝ λn,b,c. lt_s n c b.
201
202definition lte_s ≝ λn,b,c. ¬(gt_s n b c).
203
204definition gte_s ≝ λn. λb, c. ¬(lt_s n b c).
205     
206alias symbol "greater_than_or_equal" (instance 1) = "nat greater than or equal prop".
207
208definition bitvector_of_bool:
209      ∀n: nat. ∀b: bool. BitVector (S n) ≝
210  λn: nat.
211  λb: bool.
212   (pad n 1 [[b]])⌈n + 1 ↦ S n⌉.
213  //
214qed.
215
216definition full_add ≝
217  λn: nat.
218  λb, c: BitVector n.
219  λd: Bit.
220    fold_right2_i ? ? ? (
221      λn.
222       λb1, b2: bool.
223        λd: Bit × (BitVector n).
224        let 〈c1,r〉 ≝ d in
225          〈(b1 ∧ b2) ∨ (c1 ∧ (b1 ∨ b2)),
226           (exclusive_disjunction (exclusive_disjunction b1 b2) c1) ::: r〉)
227     〈d, [[ ]]〉 ? b c.
228   
229definition half_add ≝
230  λn: nat.
231  λb, c: BitVector n.
232    full_add n b c false.
Note: See TracBrowser for help on using the repository browser.