dafny_runtime/
big_int.rs

1use crate::DafnyPrint;
2use crate::Rc;
3use num::bigint::BigInt;
4use num::rational::BigRational;
5use num::FromPrimitive;
6use num::ToPrimitive;
7use num::{bigint::ParseBigIntError, Integer, Num, One, Signed, Zero};
8use std::{
9    clone::Clone,
10    cmp::Ordering,
11    convert::From,
12    fmt::Formatter,
13    hash::Hash,
14    ops::{Add, Div, Mul, Neg, Rem, Sub},
15};
16
17// Zero-cost abstraction over a Rc<BigInt>
18
19#[derive(Clone)]
20pub struct DafnyInt {
21    data: Rc<BigInt>,
22}
23
24impl DafnyInt {
25    pub fn new(data: Rc<BigInt>) -> DafnyInt {
26        DafnyInt { data }
27    }
28    pub fn strong_count(&self) -> usize {
29        Rc::strong_count(&self.data)
30    }
31}
32
33impl AsRef<BigInt> for DafnyInt {
34    fn as_ref(&self) -> &BigInt {
35        &self.data
36    }
37}
38
39impl Default for DafnyInt {
40    fn default() -> Self {
41        DafnyInt::new(Rc::new(BigInt::zero()))
42    }
43}
44
45pub fn dafny_int_to_bigint(i: &DafnyInt) -> BigInt {
46    i.data.as_ref().clone()
47}
48pub fn bigint_to_dafny_int(i: &BigInt) -> DafnyInt {
49    DafnyInt {
50        data: Rc::new(i.clone()),
51    }
52}
53
54impl Zero for DafnyInt {
55    #[inline]
56    fn zero() -> Self {
57        DafnyInt {
58            data: Rc::new(BigInt::zero()),
59        }
60    }
61    #[inline]
62    fn is_zero(&self) -> bool {
63        self.data.is_zero()
64    }
65}
66impl One for DafnyInt {
67    #[inline]
68    fn one() -> Self {
69        DafnyInt {
70            data: Rc::new(BigInt::one()),
71        }
72    }
73}
74impl Num for DafnyInt {
75    type FromStrRadixErr = ParseBigIntError;
76
77    #[inline]
78    fn from_str_radix(s: &str, radix: u32) -> Result<Self, Self::FromStrRadixErr> {
79        Ok(DafnyInt {
80            data: Rc::new(BigInt::from_str_radix(s, radix)?),
81        })
82    }
83}
84impl Ord for DafnyInt {
85    #[inline]
86    fn cmp(&self, other: &Self) -> Ordering {
87        self.data.cmp(&other.data)
88    }
89}
90impl Signed for DafnyInt {
91    #[inline]
92    fn abs(&self) -> Self {
93        DafnyInt {
94            data: Rc::new(self.data.as_ref().abs()),
95        }
96    }
97
98    #[inline]
99    fn abs_sub(&self, other: &Self) -> Self {
100        DafnyInt {
101            data: Rc::new(self.data.as_ref().abs_sub(other.data.as_ref())),
102        }
103    }
104
105    #[inline]
106    fn signum(&self) -> Self {
107        DafnyInt {
108            data: Rc::new(self.data.as_ref().signum()),
109        }
110    }
111
112    #[inline]
113    fn is_positive(&self) -> bool {
114        self.data.as_ref().is_positive()
115    }
116
117    #[inline]
118    fn is_negative(&self) -> bool {
119        self.data.as_ref().is_negative()
120    }
121}
122
123// Comparison
124impl PartialOrd<DafnyInt> for DafnyInt {
125    #[inline]
126    fn partial_cmp(&self, other: &DafnyInt) -> Option<Ordering> {
127        Some(self.cmp(other))
128    }
129}
130
131impl DafnyInt {
132    #[inline]
133    pub fn parse_bytes(number: &[u8], radix: u32) -> DafnyInt {
134        DafnyInt {
135            data: Rc::new(BigInt::parse_bytes(number, radix).unwrap()),
136        }
137    }
138    pub fn from_usize(usize: usize) -> DafnyInt {
139        DafnyInt {
140            data: Rc::new(BigInt::from(usize)),
141        }
142    }
143    pub fn from_i32(i: i32) -> DafnyInt {
144        DafnyInt {
145            data: Rc::new(BigInt::from(i)),
146        }
147    }
148}
149
150// fn dafny_rational_to_int(r: &BigRational) -> BigInt {
151//     euclidian_division(r.numer().clone(), r.denom().clone())
152// }
153
154impl DafnyPrint for BigInt {
155    fn fmt_print(&self, f: &mut Formatter<'_>, _in_seq: bool) -> std::fmt::Result {
156        write!(f, "{}", self)
157    }
158}
159
160fn divides_a_power_of_10(mut i: BigInt) -> (bool, BigInt, usize) {
161    let one: BigInt = One::one();
162
163    let mut factor = one.clone();
164    let mut log10 = 0;
165
166    let zero = Zero::zero();
167    let ten = BigInt::from_i32(10).unwrap();
168
169    if i <= zero {
170        return (false, factor, log10);
171    }
172
173    while i.is_multiple_of(&ten) {
174        i /= BigInt::from_i32(10).unwrap();
175        log10 += 1;
176    }
177
178    let two = BigInt::from_i32(2).unwrap();
179    let five = BigInt::from_i32(5).unwrap();
180
181    while i.is_multiple_of(&five) {
182        i /= &five;
183        factor *= &two;
184        log10 += 1;
185    }
186
187    while i.is_multiple_of(&two) {
188        i /= &two;
189        factor *= &two;
190        log10 += 1;
191    }
192
193    (i == one, factor, log10)
194}
195
196impl DafnyPrint for BigRational {
197    fn fmt_print(&self, f: &mut Formatter<'_>, _in_seq: bool) -> std::fmt::Result {
198        if self.denom() == &One::one() || self.numer() == &Zero::zero() {
199            write!(f, "{}.0", self.numer())
200        } else {
201            let (divides, factor, log10) = divides_a_power_of_10(self.denom().clone());
202            if divides {
203                let mut num = self.numer().clone();
204                num *= factor;
205
206                if num.is_negative() {
207                    write!(f, "-")?;
208                    num = -num;
209                }
210
211                let digits = num.to_string();
212
213                if log10 < digits.len() {
214                    let digit_count = digits.len() - log10;
215                    write!(f, "{}", &digits[..digit_count])?;
216                    write!(f, ".")?;
217                    write!(f, "{}", &digits[digit_count..])
218                } else {
219                    let z = log10 - digits.len();
220                    write!(f, "0.")?;
221                    for _ in 0..z {
222                        write!(f, "0")?;
223                    }
224                    write!(f, "{}", digits)
225                }
226            } else {
227                write!(f, "({}.0 / {}.0)", self.numer(), self.denom())
228            }
229        }
230    }
231}
232
233impl From<DafnyInt> for u8 {
234    fn from(val: DafnyInt) -> Self {
235        val.data.to_u8().unwrap()
236    }
237}
238impl From<DafnyInt> for u16 {
239    fn from(val: DafnyInt) -> Self {
240        val.data.to_u16().unwrap()
241    }
242}
243impl From<DafnyInt> for u32 {
244    fn from(val: DafnyInt) -> Self {
245        val.data.to_u32().unwrap()
246    }
247}
248impl From<DafnyInt> for u64 {
249    fn from(val: DafnyInt) -> Self {
250        val.data.to_u64().unwrap()
251    }
252}
253impl From<DafnyInt> for u128 {
254    fn from(val: DafnyInt) -> Self {
255        val.data.to_u128().unwrap()
256    }
257}
258impl From<DafnyInt> for i8 {
259    fn from(val: DafnyInt) -> Self {
260        val.data.to_i8().unwrap()
261    }
262}
263impl From<DafnyInt> for i16 {
264    fn from(val: DafnyInt) -> Self {
265        val.data.to_i16().unwrap()
266    }
267}
268impl From<DafnyInt> for i32 {
269    fn from(val: DafnyInt) -> Self {
270        val.data.to_i32().unwrap()
271    }
272}
273impl From<DafnyInt> for i64 {
274    fn from(val: DafnyInt) -> Self {
275        val.data.to_i64().unwrap()
276    }
277}
278impl From<DafnyInt> for i128 {
279    fn from(val: DafnyInt) -> Self {
280        val.data.to_i128().unwrap()
281    }
282}
283impl From<DafnyInt> for usize {
284    fn from(val: DafnyInt) -> Self {
285        val.data.to_usize().unwrap()
286    }
287}
288
289impl ToPrimitive for DafnyInt {
290    fn to_i64(&self) -> Option<i64> {
291        self.data.to_i64()
292    }
293
294    fn to_u64(&self) -> Option<u64> {
295        self.data.to_u64()
296    }
297
298    // Override of functions
299    fn to_u128(&self) -> Option<u128> {
300        self.data.to_u128()
301    }
302
303    fn to_i128(&self) -> Option<i128> {
304        self.data.to_i128()
305    }
306}
307
308impl PartialEq<DafnyInt> for DafnyInt {
309    fn eq(&self, other: &DafnyInt) -> bool {
310        self.data.eq(&other.data)
311    }
312}
313impl Eq for DafnyInt {}
314impl Hash for DafnyInt {
315    fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
316        self.data.hash(state);
317    }
318}
319
320impl DafnyPrint for DafnyInt {
321    fn fmt_print(&self, f: &mut Formatter<'_>, _in_seq: bool) -> std::fmt::Result {
322        write!(f, "{}", self.data)
323    }
324}
325
326impl ::std::fmt::Debug for DafnyInt {
327    fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
328        write!(f, "{}", self.data)
329    }
330}
331
332impl Add<DafnyInt> for DafnyInt {
333    type Output = DafnyInt;
334
335    fn add(self, rhs: DafnyInt) -> Self::Output {
336        DafnyInt {
337            data: Rc::new(self.data.as_ref() + rhs.data.as_ref()),
338        }
339    }
340}
341
342impl Mul<DafnyInt> for DafnyInt {
343    type Output = DafnyInt;
344
345    fn mul(self, rhs: DafnyInt) -> Self::Output {
346        DafnyInt {
347            data: Rc::new(self.data.as_ref() * rhs.data.as_ref()),
348        }
349    }
350}
351
352impl Div<DafnyInt> for DafnyInt {
353    type Output = DafnyInt;
354
355    fn div(self, rhs: DafnyInt) -> Self::Output {
356        DafnyInt {
357            data: Rc::new(self.data.as_ref() / rhs.data.as_ref()),
358        }
359    }
360}
361
362impl Sub<DafnyInt> for DafnyInt {
363    type Output = DafnyInt;
364
365    fn sub(self, rhs: DafnyInt) -> Self::Output {
366        DafnyInt {
367            data: Rc::new(self.data.as_ref() - rhs.data.as_ref()),
368        }
369    }
370}
371impl Rem<DafnyInt> for DafnyInt {
372    type Output = DafnyInt;
373
374    fn rem(self, rhs: DafnyInt) -> Self::Output {
375        DafnyInt {
376            data: Rc::new(self.data.as_ref() % rhs.data.as_ref()),
377        }
378    }
379}
380impl Neg for DafnyInt {
381    type Output = DafnyInt;
382
383    #[inline]
384    fn neg(self) -> Self::Output {
385        DafnyInt {
386            data: Rc::new(-self.data.as_ref()),
387        }
388    }
389}
390
391macro_rules! impl_dafnyint_from {
392    () => {};
393    ($type:ident) => {
394        impl ::std::convert::From<$type> for $crate::DafnyInt {
395            fn from(n: $type) -> Self {
396                $crate::DafnyInt {
397                    data: $crate::Rc::new(n.into()),
398                }
399            }
400        }
401        #[allow(trivial_numeric_casts)]
402        impl $crate::DafnyUsize for $type {
403            fn into_usize(self) -> usize {
404                self as usize
405            }
406        }
407    };
408}
409
410impl_dafnyint_from! { u8 }
411impl_dafnyint_from! { u16 }
412impl_dafnyint_from! { u32 }
413impl_dafnyint_from! { u64 }
414impl_dafnyint_from! { u128 }
415impl_dafnyint_from! { i8 }
416impl_dafnyint_from! { i16 }
417impl_dafnyint_from! { i32 }
418impl_dafnyint_from! { i64 }
419impl_dafnyint_from! { i128 }
420impl_dafnyint_from! { usize }
dafny_runtime/big_int.rs

dafny_runtime/
big_int.rs
