creusot_std/std/
ops.rs

1use crate::prelude::*;
2#[cfg(creusot)]
3use core::convert::Infallible;
4#[cfg(feature = "nightly")]
5use core::marker::Tuple;
6use core::ops::*;
7
8// Note: we should NOT give a generic extern spec for Deref::deref, since this
9// method is an exception being used both as a logic function and as a program
10// function. See #1235.
11
12/// `FnOnceExt` is an extension trait for the `FnOnce` trait, used for
13/// adding a specification to closures. It should not be used directly.
14#[cfg(feature = "nightly")]
15pub trait FnOnceExt<Args: Tuple> {
16    type Output;
17
18    #[logic(prophetic)]
19    fn precondition(self, a: Args) -> bool;
20
21    #[logic(prophetic)]
22    fn postcondition_once(self, a: Args, res: Self::Output) -> bool;
23}
24
25#[cfg(not(feature = "nightly"))]
26pub trait FnOnceExt<Args> {
27    type Output;
28}
29
30/// `FnMutExt` is an extension trait for the `FnMut` trait, used for
31/// adding a specification to closures. It should not be used directly.
32#[cfg(feature = "nightly")]
33pub trait FnMutExt<Args: Tuple>: FnOnceExt<Args> {
34    #[logic(prophetic)]
35    fn postcondition_mut(self, _: Args, _: Self, _: Self::Output) -> bool;
36
37    #[logic(prophetic)]
38    fn hist_inv(self, _: Self) -> bool;
39
40    #[logic(law)]
41    #[requires(self.postcondition_mut(args, res_state, res))]
42    #[ensures(self.hist_inv(res_state))]
43    fn postcondition_mut_hist_inv(self, args: Args, res_state: Self, res: Self::Output);
44
45    #[logic(law)]
46    #[ensures(self.hist_inv(self))]
47    fn hist_inv_refl(self);
48
49    #[logic(law)]
50    #[requires(self.hist_inv(b))]
51    #[requires(b.hist_inv(c))]
52    #[ensures(self.hist_inv(c))]
53    fn hist_inv_trans(self, b: Self, c: Self);
54
55    #[logic(law)]
56    #[ensures(self.postcondition_once(args, res) ==
57              exists<res_state: Self> self.postcondition_mut(args, res_state, res) && resolve(res_state))]
58    fn fn_mut_once(self, args: Args, res: Self::Output);
59}
60
61#[cfg(not(feature = "nightly"))]
62pub trait FnMutExt<Args>: FnOnceExt<Args> {}
63
64/// `FnExt` is an extension trait for the `Fn` trait, used for
65/// adding a specification to closures. It should not be used directly.
66#[cfg(feature = "nightly")]
67pub trait FnExt<Args: Tuple>: FnMutExt<Args> {
68    #[logic(prophetic)]
69    fn postcondition(self, _: Args, _: Self::Output) -> bool;
70
71    #[logic(law)]
72    #[ensures(self.postcondition_mut(args, res_state, res) == (self.postcondition(args, res) && self == res_state))]
73    fn fn_mut(self, args: Args, res_state: Self, res: Self::Output);
74
75    #[logic(law)]
76    #[ensures(self.postcondition_once(args, res) == (self.postcondition(args, res) && resolve(self)))]
77    fn fn_once(self, args: Args, res: Self::Output);
78
79    #[logic(law)]
80    #[ensures(self.hist_inv(res_state) == (self == res_state))]
81    fn fn_hist_inv(self, res_state: Self);
82}
83
84/// `FnExt` is an extension trait for the `Fn` trait, used for
85/// adding a specification to closures. It should not be used directly.
86#[cfg(not(feature = "nightly"))]
87pub trait FnExt<Args>: FnMutExt<Args> {}
88
89#[cfg(feature = "nightly")]
90impl<Args: Tuple, F: ?Sized + FnOnce<Args>> FnOnceExt<Args> for F {
91    type Output = <Self as FnOnce<Args>>::Output;
92
93    #[logic(open, prophetic, inline)]
94    #[allow(unused_variables)]
95    #[intrinsic("precondition")]
96    fn precondition(self, args: Args) -> bool {
97        dead
98    }
99
100    #[logic(open, prophetic, inline)]
101    #[allow(unused_variables)]
102    #[intrinsic("postcondition_once")]
103    fn postcondition_once(self, args: Args, result: Self::Output) -> bool {
104        dead
105    }
106}
107
108#[cfg(feature = "nightly")]
109impl<Args: Tuple, F: ?Sized + FnMut<Args>> FnMutExt<Args> for F {
110    #[logic(open, prophetic, inline)]
111    #[allow(unused_variables)]
112    #[intrinsic("postcondition_mut")]
113    fn postcondition_mut(self, args: Args, result_state: Self, result: Self::Output) -> bool {
114        dead
115    }
116
117    #[logic(open, prophetic, inline)]
118    #[allow(unused_variables)]
119    #[intrinsic("hist_inv")]
120    fn hist_inv(self, result_state: Self) -> bool {
121        dead
122    }
123
124    #[trusted]
125    #[logic(law)]
126    #[requires(self.postcondition_mut(args, res_state, res))]
127    #[ensures(self.hist_inv(res_state))]
128    fn postcondition_mut_hist_inv(self, args: Args, res_state: Self, res: Self::Output) {}
129
130    #[trusted]
131    #[logic(law)]
132    #[ensures(self.hist_inv(self))]
133    fn hist_inv_refl(self) {}
134
135    #[trusted]
136    #[logic(law)]
137    #[requires(self.hist_inv(b))]
138    #[requires(b.hist_inv(c))]
139    #[ensures(self.hist_inv(c))]
140    fn hist_inv_trans(self, b: Self, c: Self) {}
141
142    #[logic(law)]
143    #[trusted]
144    #[ensures(self.postcondition_once(args, res) ==
145              exists<res_state: Self> self.postcondition_mut(args, res_state, res) && resolve(res_state))]
146    fn fn_mut_once(self, args: Args, res: Self::Output) {}
147}
148
149#[cfg(feature = "nightly")]
150impl<Args: Tuple, F: ?Sized + Fn<Args>> FnExt<Args> for F {
151    #[logic(open, inline)]
152    #[allow(unused_variables)]
153    #[intrinsic("postcondition")]
154    fn postcondition(self, args: Args, result: Self::Output) -> bool {
155        dead
156    }
157
158    #[logic(law)]
159    #[trusted]
160    #[ensures(self.postcondition_mut(args, res_state, res) == (self.postcondition(args, res) && self == res_state))]
161    fn fn_mut(self, args: Args, res_state: Self, res: Self::Output) {}
162
163    #[logic(law)]
164    #[trusted]
165    #[ensures(self.postcondition_once(args, res) == (self.postcondition(args, res) && resolve(self)))]
166    fn fn_once(self, args: Args, res: Self::Output) {}
167
168    #[logic(law)]
169    #[trusted]
170    #[ensures(self.hist_inv(res_state) == (self == res_state))]
171    fn fn_hist_inv(self, res_state: Self) {}
172}
173
174extern_spec! {
175    mod core {
176        mod ops {
177            trait FnOnce<Args> where Args: Tuple {
178                #[requires(self.precondition(arg))]
179                #[ensures(self.postcondition_once(arg, result))]
180                fn call_once(self, arg: Args) -> Self::Output;
181            }
182
183            trait FnMut<Args> where Args: Tuple {
184                #[requires((*self).precondition(arg))]
185                #[ensures((*self).postcondition_mut(arg, ^self, result))]
186                fn call_mut(&mut self, arg: Args) -> Self::Output;
187            }
188
189            trait Fn<Args> where Args: Tuple {
190                #[requires((*self).precondition(arg))]
191                #[ensures((*self).postcondition(arg, result))]
192                fn call(&self, arg: Args) -> Self::Output;
193            }
194
195            trait Deref {
196                #[check(ghost)]
197                #[requires(false)]
198                fn deref(&self) -> &Self::Target;
199            }
200
201            trait DerefMut {
202                #[check(ghost)]
203                #[requires(false)]
204                fn deref_mut(&mut self) -> &mut Self::Target;
205            }
206        }
207    }
208
209    impl<'a, T> Deref for &'a T {
210        #[check(ghost)]
211        #[ensures(*result == **self)]
212        fn deref<'b>(&'b self) -> &'b T {
213            *self
214        }
215    }
216
217    impl<'a, T> Deref for &'a mut T {
218        #[check(ghost)]
219        #[ensures(*result == **self)]
220        fn deref<'b>(&'b self) -> &'b T {
221            *self
222        }
223    }
224
225    impl<'a, T> DerefMut for &'a mut T {
226        #[check(ghost)]
227        #[ensures(*result == **self)]
228        #[ensures(^result == *^self)]
229        #[ensures(^*self == ^^self)]
230        fn deref_mut<'b>(&'b mut self) -> &'b mut T {
231            *self
232        }
233    }
234}
235
236impl<T: DeepModel> DeepModel for Bound<T> {
237    type DeepModelTy = Bound<T::DeepModelTy>;
238
239    #[logic(open)]
240    fn deep_model(self) -> Self::DeepModelTy {
241        match self {
242            Bound::Included(b) => Bound::Included(b.deep_model()),
243            Bound::Excluded(b) => Bound::Excluded(b.deep_model()),
244            Bound::Unbounded => Bound::Unbounded,
245        }
246    }
247}
248
249/// Methods for the specification of [`std::ops::RangeBounds`].
250pub trait RangeBounds<T: ?Sized + DeepModel<DeepModelTy: OrdLogic>>:
251    core::ops::RangeBounds<T>
252{
253    #[logic]
254    fn start_bound_logic(&self) -> Bound<&T>;
255
256    #[logic]
257    fn end_bound_logic(&self) -> Bound<&T>;
258}
259
260/// Membership to an interval `(Bound<T>, Bound<T>)`.
261#[logic(open)]
262pub fn between<T: OrdLogic>(lo: Bound<T>, item: T, hi: Bound<T>) -> bool {
263    lower_bound(lo, item) && upper_bound(item, hi)
264}
265
266/// Comparison with a lower bound.
267#[logic(open)]
268pub fn lower_bound<T: OrdLogic>(lo: Bound<T>, item: T) -> bool {
269    pearlite! {
270        match lo {
271            Bound::Included(lo) => lo <= item,
272            Bound::Excluded(lo) => lo < item,
273            Bound::Unbounded => true,
274        }
275    }
276}
277
278/// Comparison with an upper bound.
279#[logic(open)]
280pub fn upper_bound<T: OrdLogic>(item: T, hi: Bound<T>) -> bool {
281    pearlite! {
282        match hi {
283            Bound::Included(hi) => item <= hi,
284            Bound::Excluded(lo) => lo < item,
285            Bound::Unbounded => true,
286        }
287    }
288}
289
290extern_spec! {
291    mod core {
292        mod ops {
293            trait RangeBounds<T>
294            where
295                Self: RangeBounds<T>,
296                T: ?Sized + DeepModel,
297                T::DeepModelTy: OrdLogic,
298            {
299                #[ensures(result == self.start_bound_logic())]
300                fn start_bound(&self) -> Bound<&T>;
301
302                #[ensures(result == self.end_bound_logic())]
303                fn end_bound(&self) -> Bound<&T>;
304
305                #[ensures(result == between(self.start_bound_logic().deep_model(), item.deep_model(), self.end_bound_logic().deep_model()))]
306                fn contains<U>(&self, item: &U) -> bool
307                where
308                    T: PartialOrd<U>,
309                    U: ?Sized + PartialOrd<T> + DeepModel<DeepModelTy = T::DeepModelTy>;
310
311                #[ensures(result == !exists<item: T::DeepModelTy> between(self.start_bound_logic().deep_model(), item, self.end_bound_logic().deep_model()))]
312                fn is_empty(&self) -> bool
313                where T: PartialOrd;
314            }
315        }
316    }
317
318    impl<T: Copy> Bound<&T> {
319        #[erasure]
320        #[ensures(result == match self {
321            Bound::Unbounded => Bound::Unbounded,
322            Bound::Included(x) => Bound::Included(*x),
323            Bound::Excluded(x) => Bound::Excluded(*x),
324        })]
325        fn copied(self) -> Bound<T> {
326            match self {
327                Bound::Unbounded => Bound::Unbounded,
328                Bound::Included(x) => Bound::Included(*x),
329                Bound::Excluded(x) => Bound::Excluded(*x),
330            }
331        }
332    }
333}
334
335impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for RangeFull {
336    #[logic(open)]
337    fn start_bound_logic(&self) -> Bound<&T> {
338        Bound::Unbounded
339    }
340
341    #[logic(open)]
342    fn end_bound_logic(&self) -> Bound<&T> {
343        Bound::Unbounded
344    }
345}
346
347impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for RangeFrom<T> {
348    #[logic(open)]
349    fn start_bound_logic(&self) -> Bound<&T> {
350        Bound::Included(&self.start)
351    }
352
353    #[logic(open)]
354    fn end_bound_logic(&self) -> Bound<&T> {
355        Bound::Unbounded
356    }
357}
358
359impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for RangeTo<T> {
360    #[logic(open)]
361    fn start_bound_logic(&self) -> Bound<&T> {
362        Bound::Unbounded
363    }
364
365    #[logic(open)]
366    fn end_bound_logic(&self) -> Bound<&T> {
367        Bound::Excluded(&self.end)
368    }
369}
370
371impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for Range<T> {
372    #[logic(open)]
373    fn start_bound_logic(&self) -> Bound<&T> {
374        Bound::Included(&self.start)
375    }
376
377    #[logic(open)]
378    fn end_bound_logic(&self) -> Bound<&T> {
379        Bound::Excluded(&self.end)
380    }
381}
382
383impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for RangeInclusive<T> {
384    #[logic(open)]
385    fn start_bound_logic(&self) -> Bound<&T> {
386        Bound::Included(&self.start_log())
387    }
388
389    #[logic(opaque)]
390    fn end_bound_logic(&self) -> Bound<&T> {
391        dead
392    }
393}
394
395impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for RangeToInclusive<T> {
396    #[logic(open)]
397    fn start_bound_logic(&self) -> Bound<&T> {
398        Bound::Unbounded
399    }
400
401    #[logic(open)]
402    fn end_bound_logic(&self) -> Bound<&T> {
403        Bound::Included(&self.end)
404    }
405}
406
407impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for (Bound<T>, Bound<T>) {
408    #[logic(open)]
409    fn start_bound_logic(&self) -> Bound<&T> {
410        match *self {
411            (Bound::Included(ref start), _) => Bound::Included(start),
412            (Bound::Excluded(ref start), _) => Bound::Excluded(start),
413            (Bound::Unbounded, _) => Bound::Unbounded,
414        }
415    }
416
417    #[logic(open)]
418    fn end_bound_logic(&self) -> Bound<&T> {
419        match *self {
420            (_, Bound::Included(ref end)) => Bound::Included(end),
421            (_, Bound::Excluded(ref end)) => Bound::Excluded(end),
422            (_, Bound::Unbounded) => Bound::Unbounded,
423        }
424    }
425}
426
427impl<'a, T: ?Sized + 'a + DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T>
428    for (Bound<&'a T>, Bound<&'a T>)
429{
430    #[logic(open)]
431    fn start_bound_logic(&self) -> Bound<&T> {
432        self.0
433    }
434
435    #[logic(open)]
436    fn end_bound_logic(&self) -> Bound<&T> {
437        self.1
438    }
439}
440
441impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for RangeFrom<&T> {
442    #[logic(open)]
443    fn start_bound_logic(&self) -> Bound<&T> {
444        Bound::Included(self.start)
445    }
446
447    #[logic(open)]
448    fn end_bound_logic(&self) -> Bound<&T> {
449        Bound::Unbounded
450    }
451}
452
453impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for RangeTo<&T> {
454    #[logic(open)]
455    fn start_bound_logic(&self) -> Bound<&T> {
456        Bound::Unbounded
457    }
458
459    #[logic(open)]
460    fn end_bound_logic(&self) -> Bound<&T> {
461        Bound::Excluded(self.end)
462    }
463}
464
465impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for Range<&T> {
466    #[logic(open)]
467    fn start_bound_logic(&self) -> Bound<&T> {
468        Bound::Included(self.start)
469    }
470
471    #[logic(open)]
472    fn end_bound_logic(&self) -> Bound<&T> {
473        Bound::Excluded(self.end)
474    }
475}
476
477// I don't know why this impl is different from the one for `RangeInclusive<T>`.
478impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for RangeInclusive<&T> {
479    #[logic(open)]
480    fn start_bound_logic(&self) -> Bound<&T> {
481        Bound::Included(&self.start_log())
482    }
483
484    #[logic(open)]
485    fn end_bound_logic(&self) -> Bound<&T> {
486        Bound::Included(&self.end_log())
487    }
488}
489
490impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for RangeToInclusive<&T> {
491    #[logic(open)]
492    fn start_bound_logic(&self) -> Bound<&T> {
493        Bound::Unbounded
494    }
495
496    #[logic(open)]
497    fn end_bound_logic(&self) -> Bound<&T> {
498        Bound::Included(self.end)
499    }
500}
501
502#[cfg(feature = "nightly")]
503impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for core::range::Range<T> {
504    #[logic(open)]
505    fn start_bound_logic(&self) -> Bound<&T> {
506        Bound::Included(&self.start)
507    }
508
509    #[logic(open)]
510    fn end_bound_logic(&self) -> Bound<&T> {
511        Bound::Excluded(&self.end)
512    }
513}
514
515#[cfg(feature = "nightly")]
516impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for core::range::Range<&T> {
517    #[logic(open)]
518    fn start_bound_logic(&self) -> Bound<&T> {
519        Bound::Included(self.start)
520    }
521
522    #[logic(open)]
523    fn end_bound_logic(&self) -> Bound<&T> {
524        Bound::Excluded(self.end)
525    }
526}
527
528#[cfg(feature = "nightly")]
529impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for core::range::RangeFrom<T> {
530    #[logic(open)]
531    fn start_bound_logic(&self) -> Bound<&T> {
532        Bound::Included(&self.start)
533    }
534
535    #[logic(open)]
536    fn end_bound_logic(&self) -> Bound<&T> {
537        Bound::Unbounded
538    }
539}
540
541#[cfg(feature = "nightly")]
542impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for core::range::RangeFrom<&T> {
543    #[logic(open)]
544    fn start_bound_logic(&self) -> Bound<&T> {
545        Bound::Included(self.start)
546    }
547
548    #[logic(open)]
549    fn end_bound_logic(&self) -> Bound<&T> {
550        Bound::Unbounded
551    }
552}
553
554#[cfg(feature = "nightly")]
555impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for core::range::RangeInclusive<T> {
556    #[logic(open)]
557    fn start_bound_logic(&self) -> Bound<&T> {
558        Bound::Included(&self.start)
559    }
560
561    #[logic(open)]
562    fn end_bound_logic(&self) -> Bound<&T> {
563        Bound::Included(&self.last)
564    }
565}
566
567#[cfg(feature = "nightly")]
568impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for core::range::RangeInclusive<&T> {
569    #[logic(open)]
570    fn start_bound_logic(&self) -> Bound<&T> {
571        Bound::Included(self.start)
572    }
573
574    #[logic(open)]
575    fn end_bound_logic(&self) -> Bound<&T> {
576        Bound::Included(self.last)
577    }
578}
579
580pub trait RangeInclusiveExt<Idx> {
581    #[logic]
582    fn new_log(start: Idx, end: Idx) -> Self;
583
584    #[logic]
585    fn start_log(self) -> Idx;
586
587    #[logic]
588    fn end_log(self) -> Idx;
589
590    #[logic]
591    fn is_empty_log(self) -> bool
592    where
593        Idx: DeepModel,
594        Idx::DeepModelTy: OrdLogic;
595}
596
597impl<Idx> RangeInclusiveExt<Idx> for RangeInclusive<Idx> {
598    #[logic(opaque)]
599    #[trusted]
600    #[ensures(start == result.start_log() && end == result.end_log())]
601    fn new_log(start: Idx, end: Idx) -> Self {
602        dead
603    }
604
605    #[logic(opaque)]
606    fn start_log(self) -> Idx {
607        dead
608    }
609
610    #[logic(opaque)]
611    fn end_log(self) -> Idx {
612        dead
613    }
614
615    #[logic(opaque)]
616    #[trusted]
617    #[ensures(!result ==> self.start_log().deep_model() <= self.end_log().deep_model())]
618    fn is_empty_log(self) -> bool
619    where
620        Idx: DeepModel,
621        Idx::DeepModelTy: OrdLogic,
622    {
623        dead
624    }
625}
626
627extern_spec! {
628    impl<Idx> RangeInclusive<Idx> {
629        #[ensures(result.start_log() == start)]
630        #[ensures(result.end_log() == end)]
631        #[ensures(start.deep_model() <= end.deep_model() ==> !result.is_empty_log())]
632        fn new(start: Idx, end: Idx) -> Self
633            where Idx: DeepModel, Idx::DeepModelTy: OrdLogic;
634
635        #[ensures(*result == self.start_log())]
636        fn start(&self) -> &Idx;
637
638        #[ensures(*result == self.end_log())]
639        fn end(&self) -> &Idx;
640    }
641
642    impl<Idx: PartialOrd<Idx> + DeepModel> RangeInclusive<Idx>
643    where Idx::DeepModelTy: OrdLogic
644    {
645        #[ensures(result == self.is_empty_log())]
646        fn is_empty(&self) -> bool;
647    }
648}
649
650extern_spec! {
651    impl<T> Try for Option<T> {
652        #[ensures(result == Some(output))]
653        fn from_output(output: T) -> Self {
654            Some(output)
655        }
656
657        #[ensures(match self {
658            Some(v) => result == ControlFlow::Continue(v),
659            None => result == ControlFlow::Break(None)
660        })]
661        fn branch(self) -> ControlFlow<Option<Infallible>, T> {
662            match self {
663                Some(v) => ControlFlow::Continue(v),
664                None => ControlFlow::Break(None),
665            }
666        }
667    }
668
669    impl<T> FromResidual<Option<Infallible>> for Option<T> {
670        #[ensures(result == None)]
671        fn from_residual(residual: Option<Infallible>) -> Self {
672            match residual {
673                None => None,
674            }
675        }
676    }
677
678    impl<T, E> Try for Result<T, E> {
679        #[ensures(result == Ok(output))]
680        fn from_output(output: T) -> Self {
681            Ok(output)
682        }
683
684        #[ensures(match self {
685            Ok(v) => result == ControlFlow::Continue(v),
686            Err(e) => result == ControlFlow::Break(Err(e))
687        })]
688        fn branch(self) -> ControlFlow<Result<Infallible, E>, T> {
689            match self {
690                Ok(v) => ControlFlow::Continue(v),
691                Err(e) => ControlFlow::Break(Err(e)),
692            }
693        }
694    }
695
696    impl<T, E, F: From<E>> FromResidual<Result<Infallible, E>> for Result<T, F> {
697        #[ensures(match (result, residual) {
698            (Err(result), Err(residual)) => F::from.postcondition((residual,), result),
699            _ => false,
700        })]
701        fn from_residual(residual: Result<Infallible, E>) -> Self {
702            match residual {
703                Err(e) => Err(core::convert::From::from(e)),
704            }
705        }
706    }
707}
708
709/// Dummy impls that don't use the unstable traits Tuple, FnOnce<Args>, FnMut<Args>, Fn<Args>
710#[cfg(not(feature = "nightly"))]
711mod impls {
712    use crate::std::ops::*;
713
714    impl<O, F: FnOnce() -> O> FnOnceExt<()> for F {
715        type Output = O;
716    }
717    impl<O, F: FnMut() -> O> FnMutExt<()> for F {}
718    impl<O, F: Fn() -> O> FnExt<()> for F {}
719
720    macro_rules! impl_fn {
721        ( $( $tuple:tt ),+ ) => {
722            impl<$($tuple),+, O, F: FnOnce($($tuple),+) -> O> FnOnceExt<($($tuple),+,)> for F {
723                type Output = O;
724            }
725            impl<$($tuple),+, O, F: FnMut($($tuple),+) -> O> FnMutExt<($($tuple),+,)> for F {}
726            impl<$($tuple),+, O, F: Fn($($tuple),+) -> O> FnExt<($($tuple),+,)> for F {}
727        };
728    }
729
730    impl_fn! { A1 }
731    impl_fn! { A1, A2 }
732    impl_fn! { A1, A2, A3 }
733    impl_fn! { A1, A2, A3, A4 }
734    impl_fn! { A1, A2, A3, A4, A5 }
735    impl_fn! { A1, A2, A3, A4, A5, A6 }
736    impl_fn! { A1, A2, A3, A4, A5, A6, A7 }
737    impl_fn! { A1, A2, A3, A4, A5, A6, A7, A8 }
738    impl_fn! { A1, A2, A3, A4, A5, A6, A7, A8, A9 }
739}
creusot_std/std/ops.rs

creusot_std/std/
ops.rs
