flux_middle/rty/
expr.rs

1use std::{fmt, iter, ops::ControlFlow, sync::OnceLock};
2
3use flux_arc_interner::{Interned, List, impl_internable, impl_slice_internable};
4use flux_common::bug;
5use flux_macros::{TypeFoldable, TypeVisitable};
6use flux_rustc_bridge::{
7    ToRustc,
8    const_eval::{scalar_to_bits, scalar_to_int, scalar_to_uint},
9    ty::{Const, ConstKind, ValTree, VariantIdx},
10};
11use itertools::Itertools;
12use rustc_abi::{FIRST_VARIANT, FieldIdx};
13use rustc_data_structures::snapshot_map::SnapshotMap;
14use rustc_hir::def_id::DefId;
15use rustc_index::newtype_index;
16use rustc_macros::{Decodable, Encodable, TyDecodable, TyEncodable};
17use rustc_middle::{
18    mir::Local,
19    ty::{ParamConst, ScalarInt, TyCtxt},
20};
21use rustc_span::{Span, Symbol};
22use rustc_type_ir::{BoundVar, DebruijnIndex, INNERMOST};
23
24use super::{
25    BaseTy, Binder, BoundReftKind, BoundVariableKinds, FuncSort, GenericArgs, GenericArgsExt as _,
26    IntTy, Sort, UintTy,
27};
28use crate::{
29    big_int::BigInt,
30    def_id::FluxDefId,
31    fhir::{self},
32    global_env::GlobalEnv,
33    pretty::*,
34    queries::QueryResult,
35    rty::{
36        BoundVariableKind, SortArg,
37        fold::{
38            TypeFoldable, TypeFolder, TypeSuperFoldable, TypeSuperVisitable, TypeVisitable as _,
39            TypeVisitor,
40        },
41    },
42};
43
44/// A lambda abstraction with an elaborated output sort. We need the output sort of lambdas for
45/// encoding into fixpoint
46#[derive(Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable)]
47pub struct Lambda {
48    body: Binder<Expr>,
49    output: Sort,
50}
51
52impl Lambda {
53    pub fn bind_with_vars(body: Expr, inputs: BoundVariableKinds, output: Sort) -> Self {
54        debug_assert!(inputs.iter().all(BoundVariableKind::is_refine));
55        Self { body: Binder::bind_with_vars(body, inputs), output }
56    }
57
58    pub fn bind_with_fsort(body: Expr, fsort: FuncSort) -> Self {
59        Self { body: Binder::bind_with_sorts(body, fsort.inputs()), output: fsort.output().clone() }
60    }
61
62    pub fn apply(&self, args: &[Expr]) -> Expr {
63        self.body.replace_bound_refts(args)
64    }
65
66    pub fn vars(&self) -> &BoundVariableKinds {
67        self.body.vars()
68    }
69
70    pub fn output(&self) -> Sort {
71        self.output.clone()
72    }
73
74    pub fn fsort(&self) -> FuncSort {
75        let inputs_and_output = self
76            .vars()
77            .iter()
78            .map(|kind| kind.expect_sort().clone())
79            .chain(iter::once(self.output()))
80            .collect();
81        FuncSort { inputs_and_output }
82    }
83}
84
85#[derive(Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable)]
86pub struct AliasReft {
87    /// Id of the associated refinement in the trait
88    pub assoc_id: FluxDefId,
89    pub args: GenericArgs,
90}
91
92impl AliasReft {
93    pub fn to_rustc_trait_ref<'tcx>(&self, tcx: TyCtxt<'tcx>) -> rustc_middle::ty::TraitRef<'tcx> {
94        let trait_def_id = self.assoc_id.parent();
95        let args = self
96            .args
97            .to_rustc(tcx)
98            .truncate_to(tcx, tcx.generics_of(trait_def_id));
99        rustc_middle::ty::TraitRef::new(tcx, trait_def_id, args)
100    }
101}
102
103#[derive(Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable)]
104pub struct Expr {
105    kind: Interned<ExprKind>,
106    espan: Option<ESpan>,
107}
108
109impl Expr {
110    pub fn at_opt(self, espan: Option<ESpan>) -> Expr {
111        Expr { kind: self.kind, espan }
112    }
113
114    pub fn at(self, espan: ESpan) -> Expr {
115        self.at_opt(Some(espan))
116    }
117
118    pub fn at_base(self, base: ESpan) -> Expr {
119        if let Some(espan) = self.espan { self.at(espan.with_base(base)) } else { self }
120    }
121
122    pub fn span(&self) -> Option<ESpan> {
123        self.espan
124    }
125
126    pub fn tt() -> Expr {
127        static TRUE: OnceLock<Expr> = OnceLock::new();
128        TRUE.get_or_init(|| ExprKind::Constant(Constant::Bool(true)).intern())
129            .clone()
130    }
131
132    pub fn ff() -> Expr {
133        static FALSE: OnceLock<Expr> = OnceLock::new();
134        FALSE
135            .get_or_init(|| ExprKind::Constant(Constant::Bool(false)).intern())
136            .clone()
137    }
138
139    pub fn and_from_iter(exprs: impl IntoIterator<Item = Expr>) -> Expr {
140        exprs
141            .into_iter()
142            .reduce(|acc, e| Expr::binary_op(BinOp::And, acc, e))
143            .unwrap_or_else(Expr::tt)
144    }
145
146    pub fn or_from_iter(exprs: impl IntoIterator<Item = Expr>) -> Expr {
147        exprs
148            .into_iter()
149            .reduce(|acc, e| Expr::binary_op(BinOp::Or, acc, e))
150            .unwrap_or_else(Expr::ff)
151    }
152
153    pub fn and(e1: impl Into<Expr>, e2: impl Into<Expr>) -> Expr {
154        Expr::and_from_iter([e1.into(), e2.into()])
155    }
156
157    pub fn or(e1: impl Into<Expr>, e2: impl Into<Expr>) -> Expr {
158        Expr::or_from_iter([e1.into(), e2.into()])
159    }
160
161    pub fn zero() -> Expr {
162        static ZERO: OnceLock<Expr> = OnceLock::new();
163        ZERO.get_or_init(|| ExprKind::Constant(Constant::ZERO).intern())
164            .clone()
165    }
166
167    pub fn int_max(int_ty: IntTy) -> Expr {
168        let bit_width: u64 = int_ty
169            .bit_width()
170            .unwrap_or(flux_config::pointer_width().bits());
171        Expr::constant(Constant::int_max(bit_width.try_into().unwrap()))
172    }
173
174    pub fn int_min(int_ty: IntTy) -> Expr {
175        let bit_width: u64 = int_ty
176            .bit_width()
177            .unwrap_or(flux_config::pointer_width().bits());
178        Expr::constant(Constant::int_min(bit_width.try_into().unwrap()))
179    }
180
181    pub fn uint_max(uint_ty: UintTy) -> Expr {
182        let bit_width: u64 = uint_ty
183            .bit_width()
184            .unwrap_or(flux_config::pointer_width().bits());
185        Expr::constant(Constant::uint_max(bit_width.try_into().unwrap()))
186    }
187
188    pub fn nu() -> Expr {
189        Expr::bvar(INNERMOST, BoundVar::ZERO, BoundReftKind::Anon)
190    }
191
192    pub fn is_nu(&self) -> bool {
193        if let ExprKind::Var(Var::Bound(INNERMOST, var)) = self.kind()
194            && var.var == BoundVar::ZERO
195        {
196            true
197        } else {
198            false
199        }
200    }
201
202    pub fn unit() -> Expr {
203        Expr::tuple(List::empty())
204    }
205
206    pub fn var(var: Var) -> Expr {
207        ExprKind::Var(var).intern()
208    }
209
210    pub fn fvar(name: Name) -> Expr {
211        Var::Free(name).to_expr()
212    }
213
214    pub fn evar(evid: EVid) -> Expr {
215        Var::EVar(evid).to_expr()
216    }
217
218    pub fn bvar(debruijn: DebruijnIndex, var: BoundVar, kind: BoundReftKind) -> Expr {
219        Var::Bound(debruijn, BoundReft { var, kind }).to_expr()
220    }
221
222    pub fn early_param(index: u32, name: Symbol) -> Expr {
223        Var::EarlyParam(EarlyReftParam { index, name }).to_expr()
224    }
225
226    pub fn local(local: Local) -> Expr {
227        ExprKind::Local(local).intern()
228    }
229
230    pub fn constant(c: Constant) -> Expr {
231        ExprKind::Constant(c).intern()
232    }
233
234    pub fn const_def_id(c: DefId) -> Expr {
235        ExprKind::ConstDefId(c).intern()
236    }
237
238    pub fn const_generic(param: ParamConst) -> Expr {
239        ExprKind::Var(Var::ConstGeneric(param)).intern()
240    }
241
242    pub fn tuple(flds: List<Expr>) -> Expr {
243        ExprKind::Tuple(flds).intern()
244    }
245
246    pub fn ctor_struct(def_id: DefId, flds: List<Expr>) -> Expr {
247        ExprKind::Ctor(Ctor::Struct(def_id), flds).intern()
248    }
249
250    pub fn ctor_enum(def_id: DefId, idx: VariantIdx) -> Expr {
251        ExprKind::Ctor(Ctor::Enum(def_id, idx), List::empty()).intern()
252    }
253
254    pub fn ctor(ctor: Ctor, flds: List<Expr>) -> Expr {
255        ExprKind::Ctor(ctor, flds).intern()
256    }
257
258    pub fn is_ctor(def_id: DefId, variant_idx: VariantIdx, idx: impl Into<Expr>) -> Expr {
259        ExprKind::IsCtor(def_id, variant_idx, idx.into()).intern()
260    }
261
262    pub fn from_bits(bty: &BaseTy, bits: u128) -> Expr {
263        // FIXME: We are assuming the higher bits are not set. check this assumption
264        match bty {
265            BaseTy::Int(_) => {
266                let bits = bits as i128;
267                ExprKind::Constant(Constant::from(bits)).intern()
268            }
269            BaseTy::Uint(_) => ExprKind::Constant(Constant::from(bits)).intern(),
270            BaseTy::Bool => ExprKind::Constant(Constant::Bool(bits != 0)).intern(),
271            BaseTy::Char => {
272                let c = char::from_u32(bits.try_into().unwrap()).unwrap();
273                ExprKind::Constant(Constant::Char(c)).intern()
274            }
275            _ => bug!(),
276        }
277    }
278
279    pub fn ite(p: impl Into<Expr>, e1: impl Into<Expr>, e2: impl Into<Expr>) -> Expr {
280        ExprKind::IfThenElse(p.into(), e1.into(), e2.into()).intern()
281    }
282
283    pub fn abs(lam: Lambda) -> Expr {
284        ExprKind::Abs(lam).intern()
285    }
286
287    pub fn let_(init: Expr, body: Binder<Expr>) -> Expr {
288        ExprKind::Let(init, body).intern()
289    }
290
291    pub fn bounded_quant(kind: fhir::QuantKind, rng: fhir::Range, body: Binder<Expr>) -> Expr {
292        ExprKind::BoundedQuant(kind, rng, body).intern()
293    }
294
295    pub fn hole(kind: HoleKind) -> Expr {
296        ExprKind::Hole(kind).intern()
297    }
298
299    pub fn kvar(kvar: KVar) -> Expr {
300        ExprKind::KVar(kvar).intern()
301    }
302
303    pub fn alias(alias: AliasReft, args: List<Expr>) -> Expr {
304        ExprKind::Alias(alias, args).intern()
305    }
306
307    pub fn forall(expr: Binder<Expr>) -> Expr {
308        ExprKind::ForAll(expr).intern()
309    }
310
311    pub fn binary_op(op: BinOp, e1: impl Into<Expr>, e2: impl Into<Expr>) -> Expr {
312        ExprKind::BinaryOp(op, e1.into(), e2.into()).intern()
313    }
314
315    pub fn prim_val(op: BinOp, e1: impl Into<Expr>, e2: impl Into<Expr>) -> Expr {
316        Expr::app(InternalFuncKind::Val(op), List::empty(), List::from_arr([e1.into(), e2.into()]))
317    }
318
319    pub fn prim_rel(op: BinOp, e1: impl Into<Expr>, e2: impl Into<Expr>) -> Expr {
320        Expr::app(InternalFuncKind::Rel(op), List::empty(), List::from_arr([e1.into(), e2.into()]))
321    }
322
323    pub fn unit_struct(def_id: DefId) -> Expr {
324        Expr::ctor_struct(def_id, List::empty())
325    }
326
327    pub fn cast(from: Sort, to: Sort, idx: Expr) -> Expr {
328        Expr::app(
329            InternalFuncKind::Cast,
330            List::from_arr([SortArg::Sort(from), SortArg::Sort(to)]),
331            List::from_arr([idx]),
332        )
333    }
334
335    pub fn app(func: impl Into<Expr>, sort_args: List<SortArg>, args: List<Expr>) -> Expr {
336        ExprKind::App(func.into(), sort_args, args).intern()
337    }
338
339    pub fn global_func(kind: SpecFuncKind) -> Expr {
340        ExprKind::GlobalFunc(kind).intern()
341    }
342
343    pub fn internal_func(kind: InternalFuncKind) -> Expr {
344        ExprKind::InternalFunc(kind).intern()
345    }
346
347    pub fn eq(e1: impl Into<Expr>, e2: impl Into<Expr>) -> Expr {
348        ExprKind::BinaryOp(BinOp::Eq, e1.into(), e2.into()).intern()
349    }
350
351    pub fn unary_op(op: UnOp, e: impl Into<Expr>) -> Expr {
352        ExprKind::UnaryOp(op, e.into()).intern()
353    }
354
355    pub fn ne(e1: impl Into<Expr>, e2: impl Into<Expr>) -> Expr {
356        ExprKind::BinaryOp(BinOp::Ne, e1.into(), e2.into()).intern()
357    }
358
359    pub fn ge(e1: impl Into<Expr>, e2: impl Into<Expr>) -> Expr {
360        ExprKind::BinaryOp(BinOp::Ge(Sort::Int), e1.into(), e2.into()).intern()
361    }
362
363    pub fn gt(e1: impl Into<Expr>, e2: impl Into<Expr>) -> Expr {
364        ExprKind::BinaryOp(BinOp::Gt(Sort::Int), e1.into(), e2.into()).intern()
365    }
366
367    pub fn lt(e1: impl Into<Expr>, e2: impl Into<Expr>) -> Expr {
368        ExprKind::BinaryOp(BinOp::Lt(Sort::Int), e1.into(), e2.into()).intern()
369    }
370
371    pub fn le(e1: impl Into<Expr>, e2: impl Into<Expr>) -> Expr {
372        ExprKind::BinaryOp(BinOp::Le(Sort::Int), e1.into(), e2.into()).intern()
373    }
374
375    pub fn implies(e1: impl Into<Expr>, e2: impl Into<Expr>) -> Expr {
376        ExprKind::BinaryOp(BinOp::Imp, e1.into(), e2.into()).intern()
377    }
378
379    pub fn field_proj(e: impl Into<Expr>, proj: FieldProj) -> Expr {
380        ExprKind::FieldProj(e.into(), proj).intern()
381    }
382
383    pub fn field_projs(e: impl Into<Expr>, projs: &[FieldProj]) -> Expr {
384        projs.iter().copied().fold(e.into(), Expr::field_proj)
385    }
386
387    pub fn path_proj(base: Expr, field: FieldIdx) -> Expr {
388        ExprKind::PathProj(base, field).intern()
389    }
390
391    pub fn not(&self) -> Expr {
392        ExprKind::UnaryOp(UnOp::Not, self.clone()).intern()
393    }
394
395    pub fn neg(&self) -> Expr {
396        ExprKind::UnaryOp(UnOp::Neg, self.clone()).intern()
397    }
398
399    pub fn kind(&self) -> &ExprKind {
400        &self.kind
401    }
402
403    /// An expression is an *atom* if it is "self-delimiting", i.e., it has a clear boundary
404    /// when printed. This is used to avoid unnecessary parenthesis when pretty printing.
405    pub fn is_atom(&self) -> bool {
406        !matches!(self.kind(), ExprKind::Abs(..) | ExprKind::BinaryOp(..) | ExprKind::ForAll(..))
407    }
408
409    /// Simple syntactic check to see if the expression is a trivially true predicate. This is used
410    /// mostly for filtering predicates when pretty printing but also to simplify types in general.
411    pub fn is_trivially_true(&self) -> bool {
412        self.is_true()
413            || matches!(self.kind(), ExprKind::BinaryOp(BinOp::Eq | BinOp::Iff | BinOp::Imp, e1, e2) if e1.erase_spans() == e2.erase_spans())
414    }
415
416    /// Simple syntactic check to see if the expression is a trivially false predicate.
417    pub fn is_trivially_false(&self) -> bool {
418        self.is_false()
419    }
420
421    /// Whether the expression is *literally* the constant `true`.
422    fn is_true(&self) -> bool {
423        matches!(self.kind(), ExprKind::Constant(Constant::Bool(true)))
424    }
425
426    /// Whether the expression is *literally* the constant `false`.
427    fn is_false(&self) -> bool {
428        matches!(self.kind(), ExprKind::Constant(Constant::Bool(false)))
429    }
430
431    pub fn from_const(tcx: TyCtxt, c: &Const) -> Expr {
432        match &c.kind {
433            ConstKind::Param(param_const) => Expr::const_generic(*param_const),
434            ConstKind::Value(ty, ValTree::Leaf(scalar)) => {
435                Expr::constant(Constant::from_scalar_int(tcx, *scalar, ty).unwrap())
436            }
437            ConstKind::Value(_ty, ValTree::Branch(_)) => {
438                bug!("todo: ValTree::Branch {c:?}")
439            }
440            // We should have normalized away the unevaluated constants
441            ConstKind::Unevaluated(_) => bug!("unexpected `ConstKind::Unevaluated`"),
442
443            ConstKind::Infer(_) => bug!("unexpected `ConstKind::Infer`"),
444        }
445    }
446
447    pub fn is_binary_op(&self) -> bool {
448        matches!(self.kind(), ExprKind::BinaryOp(..))
449    }
450
451    fn const_op(op: &BinOp, c1: &Constant, c2: &Constant) -> Option<Constant> {
452        match op {
453            BinOp::Iff => c1.iff(c2),
454            BinOp::Imp => c1.imp(c2),
455            BinOp::Or => c1.or(c2),
456            BinOp::And => c1.and(c2),
457            BinOp::Gt(Sort::Int) => c1.gt(c2),
458            BinOp::Ge(Sort::Int) => c1.ge(c2),
459            BinOp::Lt(Sort::Int) => c2.gt(c1),
460            BinOp::Le(Sort::Int) => c2.ge(c1),
461            BinOp::Eq => Some(c1.eq(c2)),
462            BinOp::Ne => Some(c1.ne(c2)),
463            _ => None,
464        }
465    }
466
467    /// Simplify the expression by removing double negations, short-circuiting boolean connectives and
468    /// doing constant folding. Note that we also have [`TypeFoldable::normalize`] which applies beta
469    /// reductions for tuples and abstractions.
470    ///
471    /// Additionally replaces any occurrences of elements in assumed_preds with True.
472    pub fn simplify(&self, assumed_preds: &SnapshotMap<Expr, ()>) -> Expr {
473        struct Simplify<'a> {
474            assumed_preds: &'a SnapshotMap<Expr, ()>,
475        }
476
477        impl TypeFolder for Simplify<'_> {
478            fn fold_expr(&mut self, expr: &Expr) -> Expr {
479                if self.assumed_preds.get(&expr.erase_spans()).is_some() {
480                    return Expr::tt();
481                }
482                let span = expr.span();
483                match expr.kind() {
484                    ExprKind::BinaryOp(op, e1, e2) => {
485                        let e1 = e1.fold_with(self);
486                        let e2 = e2.fold_with(self);
487                        match (op, e1.kind(), e2.kind()) {
488                            (BinOp::And, ExprKind::Constant(Constant::Bool(false)), _) => {
489                                Expr::constant(Constant::Bool(false)).at_opt(e1.span())
490                            }
491                            (BinOp::And, _, ExprKind::Constant(Constant::Bool(false))) => {
492                                Expr::constant(Constant::Bool(false)).at_opt(e2.span())
493                            }
494                            (BinOp::And, ExprKind::Constant(Constant::Bool(true)), _) => e2,
495                            (BinOp::And, _, ExprKind::Constant(Constant::Bool(true))) => e1,
496                            (op, ExprKind::Constant(c1), ExprKind::Constant(c2)) => {
497                                if let Some(c) = Expr::const_op(op, c1, c2) {
498                                    Expr::constant(c).at_opt(span.or(e2.span()))
499                                } else {
500                                    Expr::binary_op(op.clone(), e1, e2).at_opt(span)
501                                }
502                            }
503                            _ => Expr::binary_op(op.clone(), e1, e2).at_opt(span),
504                        }
505                    }
506                    ExprKind::UnaryOp(UnOp::Not, e) => {
507                        let e = e.fold_with(self);
508                        match e.kind() {
509                            ExprKind::Constant(Constant::Bool(b)) => {
510                                Expr::constant(Constant::Bool(!b))
511                            }
512                            ExprKind::UnaryOp(UnOp::Not, e) => e.clone(),
513                            ExprKind::BinaryOp(BinOp::Eq, e1, e2) => {
514                                Expr::binary_op(BinOp::Ne, e1, e2).at_opt(span)
515                            }
516                            _ => Expr::unary_op(UnOp::Not, e).at_opt(span),
517                        }
518                    }
519                    ExprKind::IfThenElse(p, e1, e2) => {
520                        let p = p.fold_with(self);
521                        if p.is_trivially_true() {
522                            e1.fold_with(self).at_opt(span)
523                        } else if p.is_trivially_false() {
524                            e2.fold_with(self).at_opt(span)
525                        } else {
526                            Expr::ite(p, e1.fold_with(self), e2.fold_with(self)).at_opt(span)
527                        }
528                    }
529                    _ => expr.super_fold_with(self),
530                }
531            }
532        }
533        self.fold_with(&mut Simplify { assumed_preds })
534    }
535
536    pub fn to_loc(&self) -> Option<Loc> {
537        match self.kind() {
538            ExprKind::Local(local) => Some(Loc::Local(*local)),
539            ExprKind::Var(var) => Some(Loc::Var(*var)),
540            _ => None,
541        }
542    }
543
544    pub fn to_path(&self) -> Option<Path> {
545        let mut expr = self;
546        let mut proj = vec![];
547        while let ExprKind::PathProj(e, field) = expr.kind() {
548            proj.push(*field);
549            expr = e;
550        }
551        proj.reverse();
552        Some(Path::new(expr.to_loc()?, proj))
553    }
554
555    pub fn is_abs(&self) -> bool {
556        matches!(self.kind(), ExprKind::Abs(..))
557    }
558
559    /// Whether this is an aggregate expression with no fields.
560    pub fn is_unit(&self) -> bool {
561        matches!(self.kind(), ExprKind::Tuple(flds) if flds.is_empty())
562            || matches!(self.kind(), ExprKind::Ctor(Ctor::Struct(_), flds) if flds.is_empty())
563    }
564
565    pub fn eta_expand_abs(&self, inputs: &BoundVariableKinds, output: Sort) -> Lambda {
566        let args = (0..inputs.len())
567            .map(|idx| Expr::bvar(INNERMOST, BoundVar::from_usize(idx), BoundReftKind::Anon))
568            .collect();
569        let body = Expr::app(self, List::empty(), args);
570        Lambda::bind_with_vars(body, inputs.clone(), output)
571    }
572
573    /// Applies a field projection to an expression and optimistically try to beta reduce it
574    pub fn proj_and_reduce(&self, proj: FieldProj) -> Expr {
575        match self.kind() {
576            ExprKind::Tuple(flds) | ExprKind::Ctor(Ctor::Struct(_), flds) => {
577                flds[proj.field_idx() as usize].clone()
578            }
579            _ => Expr::field_proj(self.clone(), proj),
580        }
581    }
582
583    pub fn visit_conj<'a>(&'a self, mut f: impl FnMut(&'a Expr)) {
584        fn go<'a>(e: &'a Expr, f: &mut impl FnMut(&'a Expr)) {
585            if let ExprKind::BinaryOp(BinOp::And, e1, e2) = e.kind() {
586                go(e1, f);
587                go(e2, f);
588            } else {
589                f(e);
590            }
591        }
592        go(self, &mut f);
593    }
594
595    pub fn flatten_conjs(&self) -> Vec<&Expr> {
596        let mut vec = vec![];
597        self.visit_conj(|e| vec.push(e));
598        vec
599    }
600
601    pub fn has_evars(&self) -> bool {
602        struct HasEvars;
603
604        impl TypeVisitor for HasEvars {
605            type BreakTy = ();
606            fn visit_expr(&mut self, expr: &Expr) -> ControlFlow<Self::BreakTy> {
607                if let ExprKind::Var(Var::EVar(_)) = expr.kind() {
608                    ControlFlow::Break(())
609                } else {
610                    expr.super_visit_with(self)
611                }
612            }
613        }
614
615        self.visit_with(&mut HasEvars).is_break()
616    }
617
618    pub fn erase_spans(&self) -> Expr {
619        struct SpanEraser;
620        impl TypeFolder for SpanEraser {
621            fn fold_expr(&mut self, e: &Expr) -> Expr {
622                e.super_fold_with(self).at_opt(None)
623            }
624        }
625        self.fold_with(&mut SpanEraser)
626    }
627}
628
629#[derive(Clone, Copy, PartialEq, Eq, Hash, TyEncodable, TyDecodable, Debug)]
630pub struct ESpan {
631    /// The top-level span information
632    pub span: Span,
633    /// The span for the (base) call-site for def-expanded spans
634    pub base: Option<Span>,
635}
636
637impl ESpan {
638    pub fn new(span: Span) -> Self {
639        Self { span, base: None }
640    }
641
642    pub fn with_base(&self, espan: ESpan) -> Self {
643        Self { span: self.span, base: Some(espan.span) }
644    }
645}
646
647#[derive(
648    Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable, Debug, TypeFoldable, TypeVisitable,
649)]
650pub enum BinOp {
651    Iff,
652    Imp,
653    Or,
654    And,
655    Eq,
656    Ne,
657    Gt(Sort),
658    Ge(Sort),
659    Lt(Sort),
660    Le(Sort),
661    Add(Sort),
662    Sub(Sort),
663    Mul(Sort),
664    Div(Sort),
665    Mod(Sort),
666    BitAnd,
667    BitOr,
668    BitXor,
669    BitShl,
670    BitShr,
671}
672
673#[derive(Clone, Copy, PartialEq, Eq, Hash, Encodable, Debug, Decodable)]
674pub enum UnOp {
675    Not,
676    Neg,
677}
678
679#[derive(Copy, Clone, PartialEq, Eq, Debug, Hash, TyEncodable, TyDecodable)]
680pub enum Ctor {
681    /// for indices represented as `struct` in the refinement logic (e.g. using `refined_by` annotations)
682    Struct(DefId),
683    /// for indices represented as  `enum` in the refinement logic (e.g. using `reflected` annotations)
684    Enum(DefId, VariantIdx),
685}
686
687impl Ctor {
688    pub fn def_id(&self) -> DefId {
689        match self {
690            Self::Struct(def_id) | Self::Enum(def_id, _) => *def_id,
691        }
692    }
693
694    pub fn variant_idx(&self) -> VariantIdx {
695        match self {
696            Self::Struct(_) => FIRST_VARIANT,
697            Self::Enum(_, variant_idx) => *variant_idx,
698        }
699    }
700
701    fn is_enum(&self) -> bool {
702        matches!(self, Self::Enum(..))
703    }
704}
705
706/// # Primitive Properties
707/// Given a primop `op` with signature `(t1,...,tn) -> t`
708/// We define a refined type for `op` expressed as a `RuleMatcher`
709///
710/// ```text
711/// op :: (x1: t1, ..., xn: tn) -> { t[op_val[op](x1,...,xn)] | op_rel[x1,...,xn] }
712/// ```
713/// That is, using two *uninterpreted functions* `op_val` and `op_rel` that respectively denote
714/// 1. The _value_ of the primop, and
715/// 2. Some invariant _relation_ that holds for the primop.
716///
717/// The latter can be extended by the user via a `property` definition, which allows us
718/// to customize primops like `<<` with extra "facts" or lemmas. See `tests/tests/pos/surface/primops00.rs` for an example.
719#[derive(Debug, Clone, TyEncodable, TyDecodable, PartialEq, Eq, Hash)]
720pub enum InternalFuncKind {
721    /// UIF representing the value of a primop
722    Val(BinOp),
723    /// UIF representing the relationship of a primop
724    Rel(BinOp),
725    // Conversions betweeen Sorts
726    Cast,
727}
728
729#[derive(Debug, Clone, TyEncodable, TyDecodable, PartialEq, Eq, Hash)]
730pub enum SpecFuncKind {
731    /// Theory symbols *interpreted* by the SMT solver
732    Thy(liquid_fixpoint::ThyFunc),
733    /// User-defined uninterpreted functions with no definition
734    Uif(FluxDefId),
735    /// User-defined functions with a body definition
736    Def(FluxDefId),
737}
738
739#[derive(Clone, PartialEq, Eq, Hash, TyEncodable, Debug, TyDecodable)]
740pub enum ExprKind {
741    Var(Var),
742    Local(Local),
743    Constant(Constant),
744    /// A rust constant. This can be either `DefKind::Const` or `DefKind::AssocConst`
745    ConstDefId(DefId),
746    BinaryOp(BinOp, Expr, Expr),
747    GlobalFunc(SpecFuncKind),
748    InternalFunc(InternalFuncKind),
749    UnaryOp(UnOp, Expr),
750    FieldProj(Expr, FieldProj),
751    /// A variant used in the logic to represent a variant of an ADT as a pair of the `DefId` and variant-index
752    Ctor(Ctor, List<Expr>),
753    Tuple(List<Expr>),
754    PathProj(Expr, FieldIdx),
755    IfThenElse(Expr, Expr, Expr),
756    KVar(KVar),
757    Alias(AliasReft, List<Expr>),
758    Let(Expr, Binder<Expr>),
759    /// Function application. The syntax allows arbitrary expressions in function position, but in
760    /// practice we are restricted by what's possible to encode in fixpoint. In a nutshell, we need
761    /// to make sure that expressions that can't be encoded are eliminated before we generate the
762    /// fixpoint constraint. Most notably, lambda abstractions have to be fully applied before
763    /// encoding into fixpoint (except when they appear as an index at the top-level).
764    App(Expr, List<SortArg>, List<Expr>),
765    /// Lambda abstractions. They are purely syntactic and we don't encode them in the logic. As such,
766    /// they have some syntactic restrictions that we must carefully maintain:
767    ///
768    /// 1. They can appear as an index at the top level.
769    /// 2. We can only substitute an abstraction for a variable in function position (or as an index).
770    ///    More generally, we need to partially evaluate expressions such that all abstractions in
771    ///    non-index position are eliminated before encoding into fixpoint. Right now, the
772    ///    implementation only evaluates abstractions that are immediately applied to arguments,
773    ///    thus the restriction.
774    Abs(Lambda),
775
776    /// Bounded quantifiers `exists i in 0..4 { pred(i) }` and `forall i in 0..4 { pred(i) }`.
777    BoundedQuant(fhir::QuantKind, fhir::Range, Binder<Expr>),
778    /// A hole is an expression that must be inferred either *semantically* by generating a kvar or
779    /// *syntactically* by generating an evar. Whether a hole can be inferred semantically or
780    /// syntactically depends on the position it appears: only holes appearing in predicate position
781    /// can be inferred with a kvar (provided it satisfies the fixpoint horn constraints) and only
782    /// holes used as an index (a position that fully determines their value) can be inferred with
783    /// an evar.
784    ///
785    /// Holes are implicitly defined in a scope, i.e., their solution could mention free and bound
786    /// variables in this scope. This must be considered when generating an inference variables for
787    /// them (either evar or kvar). In fact, the main reason we have holes is that we want to
788    /// decouple the places where we generate holes (where we don't want to worry about the scope),
789    /// and the places where we generate inference variable for them (where we do need to worry
790    /// about the scope).
791    Hole(HoleKind),
792    ForAll(Binder<Expr>),
793    /// Is the expression constructed from constructor of the given DefId (which should be `reflected` Enum)
794    IsCtor(DefId, VariantIdx, Expr),
795}
796
797impl ExprKind {
798    fn intern(self) -> Expr {
799        Expr { kind: Interned::new(self), espan: None }
800    }
801}
802
803#[derive(Clone, Copy, PartialEq, Eq, Hash, TyEncodable, TyDecodable, Debug)]
804pub enum AggregateKind {
805    Tuple(usize),
806    Adt(DefId),
807}
808
809impl AggregateKind {
810    pub fn to_proj(self, field: u32) -> FieldProj {
811        match self {
812            AggregateKind::Tuple(arity) => FieldProj::Tuple { arity, field },
813            AggregateKind::Adt(def_id) => FieldProj::Adt { def_id, field },
814        }
815    }
816}
817
818#[derive(Clone, Copy, PartialEq, Eq, Hash, TyEncodable, TyDecodable, Debug)]
819pub enum FieldProj {
820    Tuple { arity: usize, field: u32 },
821    Adt { def_id: DefId, field: u32 },
822}
823
824impl FieldProj {
825    pub fn arity(&self, genv: GlobalEnv) -> QueryResult<usize> {
826        match self {
827            FieldProj::Tuple { arity, .. } => Ok(*arity),
828            FieldProj::Adt { def_id, .. } => {
829                Ok(genv.adt_sort_def_of(*def_id)?.struct_variant().fields())
830            }
831        }
832    }
833
834    pub fn field_idx(&self) -> u32 {
835        match self {
836            FieldProj::Tuple { field, .. } | FieldProj::Adt { field, .. } => *field,
837        }
838    }
839}
840
841/// The position where a [hole] appears. This determines how it will be inferred. This is related
842/// to, but not the same as, an [`InferMode`].
843///
844/// [`InferMode`]: super::InferMode
845/// [hole]: ExprKind::Hole
846#[derive(
847    Debug, Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable, TypeFoldable, TypeVisitable,
848)]
849pub enum HoleKind {
850    /// A hole in predicate position (e.g., the predicate in a [`TyKind::Constr`]). It will be
851    /// inferred by generating a kvar.
852    ///
853    /// [`TyKind::Constr`]: super::TyKind::Constr
854    Pred,
855    /// A hole used as a refinement argument or index. It will be inferred by generating an evar.
856    /// The expression filling the hole must have the provided sort.
857    ///
858    /// NOTE(nilehmann) we used to require the `Sort` for generating the evar because we needed it
859    /// to eta-expand aggregate sorts. We've since removed this behavior but I'm keeping it here
860    /// just in case. We could remove in case it becomes too problematic.
861    Expr(Sort),
862}
863
864/// In theory a kvar is just an unknown predicate that can use some variables in scope. In practice,
865/// fixpoint makes a difference between the first and the rest of the arguments, the first one being
866/// the kvar's *self argument*. Fixpoint will only instantiate qualifiers that use the self argument.
867/// Flux generalizes the self argument to be a list. We call the rest of the arguments the *scope*.
868#[derive(Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable)]
869pub struct KVar {
870    pub kvid: KVid,
871    /// The number of arguments consider to be *self arguments*.
872    pub self_args: usize,
873    /// The list of *all* arguments with the self arguments at the beginning, i.e., the
874    /// list of self arguments followed by the scope.
875    pub args: List<Expr>,
876}
877
878#[derive(Clone, Debug, Copy, PartialEq, Eq, Hash, PartialOrd, Ord, Encodable, Decodable)]
879pub struct EarlyReftParam {
880    pub index: u32,
881    pub name: Symbol,
882}
883
884#[derive(Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord, Encodable, Decodable, Debug)]
885pub struct BoundReft {
886    pub var: BoundVar,
887    pub kind: BoundReftKind,
888}
889
890#[derive(Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord, TyEncodable, TyDecodable)]
891pub enum Var {
892    Free(Name),
893    Bound(DebruijnIndex, BoundReft),
894    EarlyParam(EarlyReftParam),
895    EVar(EVid),
896    ConstGeneric(ParamConst),
897}
898
899#[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord, TyEncodable, TyDecodable)]
900pub struct Path {
901    pub loc: Loc,
902    projection: List<FieldIdx>,
903}
904
905#[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord, TyEncodable, TyDecodable)]
906pub enum Loc {
907    Local(Local),
908    Var(Var),
909}
910
911newtype_index! {
912    /// *E*xistential *v*ariable *id*
913    #[debug_format = "?{}e"]
914    #[orderable]
915    #[encodable]
916    pub struct EVid {}
917}
918
919newtype_index! {
920    #[debug_format = "$k{}"]
921    #[encodable]
922    pub struct KVid {}
923}
924
925newtype_index! {
926    #[debug_format = "a{}"]
927    #[orderable]
928    #[encodable]
929    pub struct Name {}
930}
931
932impl KVar {
933    pub fn new(kvid: KVid, self_args: usize, args: Vec<Expr>) -> Self {
934        KVar { kvid, self_args, args: List::from_vec(args) }
935    }
936
937    fn self_args(&self) -> &[Expr] {
938        &self.args[..self.self_args]
939    }
940
941    fn scope(&self) -> &[Expr] {
942        &self.args[self.self_args..]
943    }
944}
945
946impl Var {
947    pub fn to_expr(&self) -> Expr {
948        Expr::var(*self)
949    }
950}
951
952impl Path {
953    pub fn new(loc: Loc, projection: impl Into<List<FieldIdx>>) -> Path {
954        Path { loc, projection: projection.into() }
955    }
956
957    pub fn projection(&self) -> &[FieldIdx] {
958        &self.projection[..]
959    }
960
961    pub fn to_expr(&self) -> Expr {
962        self.projection
963            .iter()
964            .fold(self.loc.to_expr(), |e, f| Expr::path_proj(e, *f))
965    }
966
967    pub fn to_loc(&self) -> Option<Loc> {
968        if self.projection.is_empty() { Some(self.loc) } else { None }
969    }
970}
971
972impl Loc {
973    pub fn to_expr(&self) -> Expr {
974        match self {
975            Loc::Local(local) => Expr::local(*local),
976            Loc::Var(var) => Expr::var(*var),
977        }
978    }
979}
980
981macro_rules! impl_ops {
982    ($($op:ident: $method:ident),*) => {$(
983        impl<Rhs> std::ops::$op<Rhs> for Expr
984        where
985            Rhs: Into<Expr>,
986        {
987            type Output = Expr;
988
989            fn $method(self, rhs: Rhs) -> Self::Output {
990                let sort = crate::rty::Sort::Int;
991                Expr::binary_op(BinOp::$op(sort), self, rhs)
992            }
993        }
994
995        impl<Rhs> std::ops::$op<Rhs> for &Expr
996        where
997            Rhs: Into<Expr>,
998        {
999            type Output = Expr;
1000
1001            fn $method(self, rhs: Rhs) -> Self::Output {
1002                let sort = crate::rty::Sort::Int;
1003                Expr::binary_op(BinOp::$op(sort), self, rhs)
1004            }
1005        }
1006    )*};
1007}
1008impl_ops!(Add: add, Sub: sub, Mul: mul, Div: div);
1009
1010impl From<i32> for Expr {
1011    fn from(value: i32) -> Self {
1012        Expr::constant(Constant::from(value))
1013    }
1014}
1015
1016impl From<&Expr> for Expr {
1017    fn from(e: &Expr) -> Self {
1018        e.clone()
1019    }
1020}
1021
1022impl From<Path> for Expr {
1023    fn from(path: Path) -> Self {
1024        path.to_expr()
1025    }
1026}
1027
1028impl From<Name> for Expr {
1029    fn from(name: Name) -> Self {
1030        Expr::fvar(name)
1031    }
1032}
1033
1034impl From<Var> for Expr {
1035    fn from(var: Var) -> Self {
1036        Expr::var(var)
1037    }
1038}
1039
1040impl From<SpecFuncKind> for Expr {
1041    fn from(kind: SpecFuncKind) -> Self {
1042        Expr::global_func(kind)
1043    }
1044}
1045
1046impl From<InternalFuncKind> for Expr {
1047    fn from(kind: InternalFuncKind) -> Self {
1048        Expr::internal_func(kind)
1049    }
1050}
1051
1052impl From<Loc> for Path {
1053    fn from(loc: Loc) -> Self {
1054        Path::new(loc, vec![])
1055    }
1056}
1057
1058impl From<Name> for Loc {
1059    fn from(name: Name) -> Self {
1060        Loc::Var(Var::Free(name))
1061    }
1062}
1063
1064impl From<Local> for Loc {
1065    fn from(local: Local) -> Self {
1066        Loc::Local(local)
1067    }
1068}
1069
1070#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Encodable, Decodable)]
1071pub struct Real(pub u128);
1072
1073impl liquid_fixpoint::FixpointFmt for Real {
1074    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1075        write!(f, "{}.0", self.0)
1076    }
1077}
1078
1079#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Encodable, Decodable)]
1080pub enum Constant {
1081    Int(BigInt),
1082    Real(Real),
1083    Bool(bool),
1084    Str(Symbol),
1085    Char(char),
1086    BitVec(u128, u32),
1087}
1088
1089impl Constant {
1090    pub const ZERO: Constant = Constant::Int(BigInt::ZERO);
1091    pub const ONE: Constant = Constant::Int(BigInt::ONE);
1092    pub const TRUE: Constant = Constant::Bool(true);
1093
1094    fn to_bool(self) -> Option<bool> {
1095        match self {
1096            Constant::Bool(b) => Some(b),
1097            _ => None,
1098        }
1099    }
1100
1101    fn to_int(self) -> Option<BigInt> {
1102        match self {
1103            Constant::Int(n) => Some(n),
1104            _ => None,
1105        }
1106    }
1107
1108    pub fn iff(&self, other: &Constant) -> Option<Constant> {
1109        let b1 = self.to_bool()?;
1110        let b2 = other.to_bool()?;
1111        Some(Constant::Bool(b1 == b2))
1112    }
1113
1114    pub fn imp(&self, other: &Constant) -> Option<Constant> {
1115        let b1 = self.to_bool()?;
1116        let b2 = other.to_bool()?;
1117        Some(Constant::Bool(!b1 || b2))
1118    }
1119
1120    pub fn or(&self, other: &Constant) -> Option<Constant> {
1121        let b1 = self.to_bool()?;
1122        let b2 = other.to_bool()?;
1123        Some(Constant::Bool(b1 || b2))
1124    }
1125
1126    pub fn and(&self, other: &Constant) -> Option<Constant> {
1127        let b1 = self.to_bool()?;
1128        let b2 = other.to_bool()?;
1129        Some(Constant::Bool(b1 && b2))
1130    }
1131
1132    pub fn eq(&self, other: &Constant) -> Constant {
1133        Constant::Bool(*self == *other)
1134    }
1135
1136    pub fn ne(&self, other: &Constant) -> Constant {
1137        Constant::Bool(*self != *other)
1138    }
1139
1140    pub fn gt(&self, other: &Constant) -> Option<Constant> {
1141        let n1 = self.to_int()?;
1142        let n2 = other.to_int()?;
1143        Some(Constant::Bool(n1 > n2))
1144    }
1145
1146    pub fn ge(&self, other: &Constant) -> Option<Constant> {
1147        let n1 = self.to_int()?;
1148        let n2 = other.to_int()?;
1149        Some(Constant::Bool(n1 >= n2))
1150    }
1151
1152    pub fn from_scalar_int<'tcx, T>(tcx: TyCtxt<'tcx>, scalar: ScalarInt, t: &T) -> Option<Self>
1153    where
1154        T: ToRustc<'tcx, T = rustc_middle::ty::Ty<'tcx>>,
1155    {
1156        use rustc_middle::ty::TyKind;
1157        let ty = t.to_rustc(tcx);
1158        match ty.kind() {
1159            TyKind::Int(int_ty) => Some(Constant::from(scalar_to_int(tcx, scalar, *int_ty))),
1160            TyKind::Uint(uint_ty) => Some(Constant::from(scalar_to_uint(tcx, scalar, *uint_ty))),
1161            TyKind::Bool => {
1162                let b = scalar_to_bits(tcx, scalar, ty)?;
1163                Some(Constant::Bool(b != 0))
1164            }
1165            TyKind::Char => {
1166                let b = scalar_to_bits(tcx, scalar, ty)?;
1167                Some(Constant::Char(char::from_u32(b as u32)?))
1168            }
1169            _ => bug!(),
1170        }
1171    }
1172
1173    /// See [`BigInt::int_min`]
1174    pub fn int_min(bit_width: u32) -> Constant {
1175        Constant::Int(BigInt::int_min(bit_width))
1176    }
1177
1178    /// See [`BigInt::int_max`]
1179    pub fn int_max(bit_width: u32) -> Constant {
1180        Constant::Int(BigInt::int_max(bit_width))
1181    }
1182
1183    /// See [`BigInt::uint_max`]
1184    pub fn uint_max(bit_width: u32) -> Constant {
1185        Constant::Int(BigInt::uint_max(bit_width))
1186    }
1187}
1188
1189impl From<i32> for Constant {
1190    fn from(c: i32) -> Self {
1191        Constant::Int(c.into())
1192    }
1193}
1194
1195impl From<usize> for Constant {
1196    fn from(u: usize) -> Self {
1197        Constant::Int(u.into())
1198    }
1199}
1200
1201impl From<u128> for Constant {
1202    fn from(c: u128) -> Self {
1203        Constant::Int(c.into())
1204    }
1205}
1206
1207impl From<i128> for Constant {
1208    fn from(c: i128) -> Self {
1209        Constant::Int(c.into())
1210    }
1211}
1212
1213impl From<bool> for Constant {
1214    fn from(b: bool) -> Self {
1215        Constant::Bool(b)
1216    }
1217}
1218
1219impl From<Symbol> for Constant {
1220    fn from(s: Symbol) -> Self {
1221        Constant::Str(s)
1222    }
1223}
1224
1225impl From<char> for Constant {
1226    fn from(c: char) -> Self {
1227        Constant::Char(c)
1228    }
1229}
1230
1231impl_internable!(ExprKind);
1232impl_slice_internable!(Expr, KVar);
1233
1234#[derive(Debug)]
1235pub struct FieldBind<T> {
1236    pub name: Symbol,
1237    pub value: T,
1238}
1239
1240impl<T: Pretty> Pretty for FieldBind<T> {
1241    fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1242        w!(cx, f, "{}: {:?}", ^self.name, &self.value)
1243    }
1244}
1245
1246pub(crate) mod pretty {
1247    use flux_rustc_bridge::def_id_to_string;
1248
1249    use super::*;
1250    use crate::{name_of_thy_func, rty::pretty::nested_with_bound_vars};
1251
1252    #[derive(PartialEq, Eq, PartialOrd, Ord)]
1253    enum Precedence {
1254        Iff,
1255        Imp,
1256        Or,
1257        And,
1258        Cmp,
1259        Bitvec,
1260        AddSub,
1261        MulDiv,
1262    }
1263
1264    impl BinOp {
1265        fn precedence(&self) -> Precedence {
1266            match self {
1267                BinOp::Iff => Precedence::Iff,
1268                BinOp::Imp => Precedence::Imp,
1269                BinOp::Or => Precedence::Or,
1270                BinOp::And => Precedence::And,
1271                BinOp::Eq
1272                | BinOp::Ne
1273                | BinOp::Gt(_)
1274                | BinOp::Lt(_)
1275                | BinOp::Ge(_)
1276                | BinOp::Le(_) => Precedence::Cmp,
1277                BinOp::Add(_) | BinOp::Sub(_) => Precedence::AddSub,
1278                BinOp::Mul(_) | BinOp::Div(_) | BinOp::Mod(_) => Precedence::MulDiv,
1279                BinOp::BitAnd | BinOp::BitOr | BinOp::BitShl | BinOp::BitShr | BinOp::BitXor => {
1280                    Precedence::Bitvec
1281                }
1282            }
1283        }
1284    }
1285
1286    impl Precedence {
1287        pub fn is_associative(&self) -> bool {
1288            !matches!(self, Precedence::Imp | Precedence::Cmp)
1289        }
1290    }
1291
1292    pub fn should_parenthesize(op: &BinOp, child: &Expr) -> bool {
1293        if let ExprKind::BinaryOp(child_op, ..) = child.kind() {
1294            child_op.precedence() < op.precedence()
1295                || (child_op.precedence() == op.precedence() && !op.precedence().is_associative())
1296        } else {
1297            false
1298        }
1299    }
1300
1301    impl Pretty for Ctor {
1302        fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1303            match self {
1304                Ctor::Struct(def_id) => {
1305                    w!(cx, f, "{:?}", def_id)
1306                }
1307                Ctor::Enum(def_id, variant_idx) => {
1308                    w!(cx, f, "{:?}::{:?}", def_id, ^variant_idx)
1309                }
1310            }
1311        }
1312    }
1313
1314    impl Pretty for fhir::QuantKind {
1315        fn fmt(&self, _cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1316            match self {
1317                fhir::QuantKind::Exists => w!(cx, f, "∃"),
1318                fhir::QuantKind::Forall => w!(cx, f, "∀"),
1319            }
1320        }
1321    }
1322
1323    impl Pretty for InternalFuncKind {
1324        fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1325            match self {
1326                InternalFuncKind::Val(op) => w!(cx, f, "[{:?}]", op),
1327                InternalFuncKind::Rel(op) => w!(cx, f, "[{:?}]?", op),
1328                InternalFuncKind::Cast => w!(cx, f, "cast"),
1329            }
1330        }
1331    }
1332
1333    impl Pretty for Expr {
1334        fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1335            let e = if cx.simplify_exprs {
1336                self.simplify(&SnapshotMap::default())
1337            } else {
1338                self.clone()
1339            };
1340            match e.kind() {
1341                ExprKind::Var(var) => w!(cx, f, "{:?}", var),
1342                ExprKind::Local(local) => w!(cx, f, "{:?}", ^local),
1343                ExprKind::ConstDefId(did) => w!(cx, f, "{}", ^def_id_to_string(*did)),
1344                ExprKind::Constant(c) => w!(cx, f, "{:?}", c),
1345
1346                ExprKind::BinaryOp(op, e1, e2) => {
1347                    if should_parenthesize(op, e1) {
1348                        w!(cx, f, "({:?})", e1)?;
1349                    } else {
1350                        w!(cx, f, "{:?}", e1)?;
1351                    }
1352                    if matches!(op, BinOp::Div(_)) {
1353                        w!(cx, f, "{:?}", op)?;
1354                    } else {
1355                        w!(cx, f, " {:?} ", op)?;
1356                    }
1357                    if should_parenthesize(op, e2) {
1358                        w!(cx, f, "({:?})", e2)?;
1359                    } else {
1360                        w!(cx, f, "{:?}", e2)?;
1361                    }
1362                    Ok(())
1363                }
1364                ExprKind::UnaryOp(op, e) => {
1365                    if e.is_atom() {
1366                        w!(cx, f, "{:?}{:?}", op, e)
1367                    } else {
1368                        w!(cx, f, "{:?}({:?})", op, e)
1369                    }
1370                }
1371                ExprKind::FieldProj(e, proj) if let ExprKind::Ctor(_, _) = e.kind() => {
1372                    // special case to avoid printing `{n:12}.n` as `12.n` but instead, just print `12`
1373                    // TODO: maintain an invariant that `FieldProj` never has a Ctor as first argument (as always reduced)
1374                    w!(cx, f, "{:?}", e.proj_and_reduce(*proj))
1375                }
1376                ExprKind::FieldProj(e, proj) => {
1377                    if e.is_atom() {
1378                        w!(cx, f, "{:?}.{}", e, ^fmt_field_proj(cx, *proj))
1379                    } else {
1380                        w!(cx, f, "({:?}).{}", e, ^fmt_field_proj(cx, *proj))
1381                    }
1382                }
1383                ExprKind::Tuple(flds) => {
1384                    if let [e] = &flds[..] {
1385                        w!(cx, f, "({:?},)", e)
1386                    } else {
1387                        w!(cx, f, "({:?})", join!(", ", flds))
1388                    }
1389                }
1390                ExprKind::IsCtor(def_id, variant_idx, idx) => {
1391                    w!(cx, f, "({:?} is {:?}::{:?})", idx, def_id, ^variant_idx)
1392                }
1393                ExprKind::Ctor(ctor, flds) => {
1394                    let def_id = ctor.def_id();
1395                    if let Some(adt_sort_def) = cx.adt_sort_def_of(def_id) {
1396                        let variant = adt_sort_def.variant(ctor.variant_idx()).field_names();
1397                        let fields = iter::zip(variant, flds)
1398                            .map(|(name, value)| FieldBind { name: *name, value: value.clone() })
1399                            .collect_vec();
1400                        match ctor {
1401                            Ctor::Struct(_) => {
1402                                w!(cx, f, "{:?} {{ {:?} }}", def_id, join!(", ", fields))
1403                            }
1404                            Ctor::Enum(_, idx) => {
1405                                if fields.is_empty() {
1406                                    w!(cx, f, "{:?}::{:?}", def_id, ^idx.index())
1407                                } else {
1408                                    w!(cx, f, "{:?}::{:?}({:?})", def_id, ^idx.index(), join!(", ", fields))
1409                                }
1410                            }
1411                        }
1412                    } else {
1413                        match ctor {
1414                            Ctor::Struct(_) => {
1415                                w!(cx, f, "{:?} {{ {:?} }}", def_id, join!(", ", flds))
1416                            }
1417                            Ctor::Enum(_, idx) => {
1418                                w!(cx, f, "{:?}::{:?} {{ {:?} }}", def_id, ^idx, join!(", ", flds))
1419                            }
1420                        }
1421                    }
1422                }
1423                ExprKind::PathProj(e, field) => {
1424                    if e.is_atom() {
1425                        w!(cx, f, "{:?}.{:?}", e, field)
1426                    } else {
1427                        w!(cx, f, "({:?}).{:?}", e, field)
1428                    }
1429                }
1430                ExprKind::App(func, _, args) => {
1431                    w!(cx, f, "{:?}({})",
1432                        parens!(func, !func.is_atom()),
1433                        ^args
1434                            .iter()
1435                            .format_with(", ", |arg, f| f(&format_args_cx!(cx, "{:?}", arg)))
1436                    )
1437                }
1438                ExprKind::IfThenElse(p, e1, e2) => {
1439                    w!(cx, f, "if {:?} {{ {:?} }} else {{ {:?} }}", p, e1, e2)
1440                }
1441                ExprKind::Hole(_) => {
1442                    w!(cx, f, "*")
1443                }
1444                ExprKind::KVar(kvar) => {
1445                    w!(cx, f, "{:?}", kvar)
1446                }
1447                ExprKind::Alias(alias, args) => {
1448                    w!(cx, f, "{:?}({:?})", alias, join!(", ", args))
1449                }
1450                ExprKind::Abs(lam) => {
1451                    w!(cx, f, "{:?}", lam)
1452                }
1453                ExprKind::GlobalFunc(SpecFuncKind::Def(did) | SpecFuncKind::Uif(did)) => {
1454                    w!(cx, f, "{}", ^did.name())
1455                }
1456                ExprKind::GlobalFunc(SpecFuncKind::Thy(itf)) => {
1457                    if let Some(name) = name_of_thy_func(*itf) {
1458                        w!(cx, f, "{}", ^name)
1459                    } else {
1460                        w!(cx, f, "<error>")
1461                    }
1462                }
1463                ExprKind::InternalFunc(func) => {
1464                    w!(cx, f, "{:?}", func)
1465                }
1466                ExprKind::ForAll(expr) => {
1467                    let vars = expr.vars();
1468                    cx.with_bound_vars(vars, || {
1469                        if !vars.is_empty() {
1470                            cx.fmt_bound_vars(false, "∀", vars, ". ", f)?;
1471                        }
1472                        w!(cx, f, "{:?}", expr.skip_binder_ref())
1473                    })
1474                }
1475                ExprKind::BoundedQuant(kind, rng, body) => {
1476                    let vars = body.vars();
1477                    cx.with_bound_vars(vars, || {
1478                        w!(
1479                            cx,
1480                            f,
1481                            "{:?} {}..{} {{ {:?} }}",
1482                            kind,
1483                            ^rng.start,
1484                            ^rng.end,
1485                            body.skip_binder_ref()
1486                        )
1487                    })
1488                }
1489                ExprKind::Let(init, body) => {
1490                    let vars = body.vars();
1491                    cx.with_bound_vars(vars, || {
1492                        cx.fmt_bound_vars(false, "(let ", vars, " = ", f)?;
1493                        w!(cx, f, "{:?} in {:?})", init, body.skip_binder_ref())
1494                    })
1495                }
1496            }
1497        }
1498    }
1499
1500    fn fmt_field_proj(cx: &PrettyCx, proj: FieldProj) -> String {
1501        if let FieldProj::Adt { def_id, field } = proj
1502            && let Some(adt_sort_def) = cx.adt_sort_def_of(def_id)
1503        {
1504            format!("{}", adt_sort_def.struct_variant().field_names()[field as usize])
1505        } else {
1506            format!("{}", proj.field_idx())
1507        }
1508    }
1509
1510    impl Pretty for Constant {
1511        fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1512            match self {
1513                Constant::Int(i) => w!(cx, f, "{i}"),
1514                Constant::BitVec(i, sz) => w!(cx, f, "bv({i}, {sz})"),
1515                Constant::Real(r) => w!(cx, f, "{}.0", ^r.0),
1516                Constant::Bool(b) => w!(cx, f, "{b}"),
1517                Constant::Str(sym) => w!(cx, f, "\"{sym}\""),
1518                Constant::Char(c) => w!(cx, f, "\'{c}\'"),
1519            }
1520        }
1521    }
1522
1523    impl Pretty for AliasReft {
1524        fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1525            w!(cx, f, "<({:?}) as {:?}", &self.args[0], self.assoc_id.parent())?;
1526            let args = &self.args[1..];
1527            if !args.is_empty() {
1528                w!(cx, f, "<{:?}>", join!(", ", args))?;
1529            }
1530            w!(cx, f, ">::{}", ^self.assoc_id.name())
1531        }
1532    }
1533
1534    impl Pretty for Lambda {
1535        fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1536            let vars = self.body.vars();
1537            // TODO: remove redundant vars; see Ty
1538            // let redundant_bvars = self.body.redundant_bvars().into_iter().collect();
1539            cx.with_bound_vars(vars, || {
1540                cx.fmt_bound_vars(false, "λ", vars, ". ", f)?;
1541                w!(cx, f, "{:?}", self.body.as_ref().skip_binder())
1542            })
1543        }
1544    }
1545
1546    impl Pretty for Var {
1547        fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1548            match self {
1549                Var::Bound(debruijn, var) => cx.fmt_bound_reft(*debruijn, *var, f),
1550                Var::EarlyParam(var) => w!(cx, f, "{}", ^var.name),
1551                Var::Free(name) => w!(cx, f, "{:?}", ^name),
1552                Var::EVar(evar) => w!(cx, f, "{:?}", ^evar),
1553                Var::ConstGeneric(param) => w!(cx, f, "{}", ^param.name),
1554            }
1555        }
1556    }
1557
1558    impl Pretty for KVar {
1559        fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1560            w!(cx, f, "{:?}", ^self.kvid)?;
1561            match cx.kvar_args {
1562                KVarArgs::All => {
1563                    w!(
1564                        cx,
1565                        f,
1566                        "({:?})[{:?}]",
1567                        join!(", ", self.self_args()),
1568                        join!(", ", self.scope())
1569                    )?;
1570                }
1571                KVarArgs::SelfOnly => w!(cx, f, "({:?})", join!(", ", self.self_args()))?,
1572                KVarArgs::Hide => {}
1573            }
1574            Ok(())
1575        }
1576    }
1577
1578    impl Pretty for Path {
1579        fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1580            w!(cx, f, "{:?}", &self.loc)?;
1581            for field in &self.projection {
1582                w!(cx, f, ".{}", ^u32::from(*field))?;
1583            }
1584            Ok(())
1585        }
1586    }
1587
1588    impl Pretty for Loc {
1589        fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1590            match self {
1591                Loc::Local(local) => w!(cx, f, "{:?}", ^local),
1592                Loc::Var(var) => w!(cx, f, "{:?}", var),
1593            }
1594        }
1595    }
1596
1597    impl Pretty for BinOp {
1598        fn fmt(&self, _cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1599            match self {
1600                BinOp::Iff => w!(cx, f, "⇔"),
1601                BinOp::Imp => w!(cx, f, "⇒"),
1602                BinOp::Or => w!(cx, f, "∨"),
1603                BinOp::And => w!(cx, f, "∧"),
1604                BinOp::Eq => w!(cx, f, "="),
1605                BinOp::Ne => w!(cx, f, "≠"),
1606                BinOp::Gt(_) => w!(cx, f, ">"),
1607                BinOp::Ge(_) => w!(cx, f, "≥"),
1608                BinOp::Lt(_) => w!(cx, f, "<"),
1609                BinOp::Le(_) => w!(cx, f, "≤"),
1610                BinOp::Add(_) => w!(cx, f, "+"),
1611                BinOp::Sub(_) => w!(cx, f, "-"),
1612                BinOp::Mul(_) => w!(cx, f, "*"),
1613                BinOp::Div(_) => w!(cx, f, "/"),
1614                BinOp::Mod(_) => w!(cx, f, "mod"),
1615                BinOp::BitAnd => w!(cx, f, "&"),
1616                BinOp::BitOr => w!(cx, f, "|"),
1617                BinOp::BitXor => w!(cx, f, "^"),
1618                BinOp::BitShl => w!(cx, f, "<<"),
1619                BinOp::BitShr => w!(cx, f, ">>"),
1620            }
1621        }
1622    }
1623
1624    impl Pretty for UnOp {
1625        fn fmt(&self, _cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1626            match self {
1627                UnOp::Not => w!(cx, f, "¬"),
1628                UnOp::Neg => w!(cx, f, "-"),
1629            }
1630        }
1631    }
1632
1633    impl_debug_with_default_cx!(Expr, Loc, Path, Var, KVar, Lambda, AliasReft);
1634
1635    impl PrettyNested for Lambda {
1636        fn fmt_nested(&self, cx: &PrettyCx) -> Result<NestedString, fmt::Error> {
1637            // TODO: remove redundant vars; see Ty
1638            nested_with_bound_vars(cx, "λ", self.body.vars(), None, |prefix| {
1639                let expr_d = self.body.skip_binder_ref().fmt_nested(cx)?;
1640                let text = format!("{}{}", prefix, expr_d.text);
1641                Ok(NestedString { text, children: expr_d.children, key: None })
1642            })
1643        }
1644    }
1645
1646    pub fn aggregate_nested(
1647        cx: &PrettyCx,
1648        ctor: &Ctor,
1649        flds: &[Expr],
1650        is_named: bool,
1651    ) -> Result<NestedString, fmt::Error> {
1652        let def_id = ctor.def_id();
1653        let mut text =
1654            if is_named && ctor.is_enum() { format_cx!(cx, "{:?}", ctor) } else { "".to_string() };
1655        if flds.is_empty() {
1656            // No fields, no index
1657            Ok(NestedString { text, children: None, key: None })
1658        } else if flds.len() == 1 {
1659            // Single field, inline index
1660            text += &format_cx!(cx, "{:?}", flds[0].clone());
1661            Ok(NestedString { text, children: None, key: None })
1662        } else {
1663            let keys = if let Some(adt_sort_def) = cx.adt_sort_def_of(def_id) {
1664                adt_sort_def
1665                    .variant(ctor.variant_idx())
1666                    .field_names()
1667                    .iter()
1668                    .map(|name| format!("{name}"))
1669                    .collect_vec()
1670            } else {
1671                (0..flds.len()).map(|i| format!("arg{i}")).collect_vec()
1672            };
1673            // Multiple fields, nested index
1674            text += "{..}";
1675            let mut children = vec![];
1676            for (key, fld) in iter::zip(keys, flds) {
1677                let fld_d = fld.fmt_nested(cx)?;
1678                children.push(NestedString { key: Some(key), ..fld_d });
1679            }
1680            Ok(NestedString { text, children: Some(children), key: None })
1681        }
1682    }
1683
1684    impl PrettyNested for Expr {
1685        fn fmt_nested(&self, cx: &PrettyCx) -> Result<NestedString, fmt::Error> {
1686            let e = if cx.simplify_exprs {
1687                self.simplify(&SnapshotMap::default())
1688            } else {
1689                self.clone()
1690            };
1691            match e.kind() {
1692                ExprKind::Var(..)
1693                | ExprKind::Local(..)
1694                | ExprKind::Constant(..)
1695                | ExprKind::ConstDefId(..)
1696                | ExprKind::Hole(..)
1697                | ExprKind::GlobalFunc(..)
1698                | ExprKind::InternalFunc(..)
1699                | ExprKind::KVar(..) => debug_nested(cx, &e),
1700
1701                ExprKind::IfThenElse(p, e1, e2) => {
1702                    let p_d = p.fmt_nested(cx)?;
1703                    let e1_d = e1.fmt_nested(cx)?;
1704                    let e2_d = e2.fmt_nested(cx)?;
1705                    let text = format!("(if {} then {} else {})", p_d.text, e1_d.text, e2_d.text);
1706                    let children = float_children(vec![p_d.children, e1_d.children, e2_d.children]);
1707                    Ok(NestedString { text, children, key: None })
1708                }
1709                ExprKind::BinaryOp(op, e1, e2) => {
1710                    let e1_d = e1.fmt_nested(cx)?;
1711                    let e2_d = e2.fmt_nested(cx)?;
1712                    let e1_text = if should_parenthesize(op, e1) {
1713                        format!("({})", e1_d.text)
1714                    } else {
1715                        e1_d.text
1716                    };
1717                    let e2_text = if should_parenthesize(op, e2) {
1718                        format!("({})", e2_d.text)
1719                    } else {
1720                        e2_d.text
1721                    };
1722                    let op_d = debug_nested(cx, op)?;
1723                    let op_text = if matches!(op, BinOp::Div(_)) {
1724                        op_d.text
1725                    } else {
1726                        format!(" {} ", op_d.text)
1727                    };
1728                    let text = format!("{e1_text}{op_text}{e2_text}");
1729                    let children = float_children(vec![e1_d.children, e2_d.children]);
1730                    Ok(NestedString { text, children, key: None })
1731                }
1732                ExprKind::UnaryOp(op, e) => {
1733                    let e_d = e.fmt_nested(cx)?;
1734                    let op_d = debug_nested(cx, op)?;
1735                    let text = if e.is_atom() {
1736                        format!("{}{}", op_d.text, e_d.text)
1737                    } else {
1738                        format!("{}({})", op_d.text, e_d.text)
1739                    };
1740                    Ok(NestedString { text, children: e_d.children, key: None })
1741                }
1742                ExprKind::FieldProj(e, proj) if let ExprKind::Ctor(_, _) = e.kind() => {
1743                    // special case to avoid printing `{n:12}.n` as `12.n` but instead, just print `12`
1744                    // TODO: maintain an invariant that `FieldProj` never has a Ctor as first argument (as always reduced)
1745                    e.proj_and_reduce(*proj).fmt_nested(cx)
1746                }
1747                ExprKind::FieldProj(e, proj) => {
1748                    let e_d = e.fmt_nested(cx)?;
1749                    let text = if e.is_atom() {
1750                        format!("{}.{}", e_d.text, fmt_field_proj(cx, *proj))
1751                    } else {
1752                        format!("({}).{}", e_d.text, fmt_field_proj(cx, *proj))
1753                    };
1754                    Ok(NestedString { text, children: e_d.children, key: None })
1755                }
1756                ExprKind::Tuple(flds) => {
1757                    let mut texts = vec![];
1758                    let mut kidss = vec![];
1759                    for e in flds {
1760                        let e_d = e.fmt_nested(cx)?;
1761                        texts.push(e_d.text);
1762                        kidss.push(e_d.children);
1763                    }
1764                    let text = if let [e] = &texts[..] {
1765                        format!("({e},)")
1766                    } else {
1767                        format!("({})", texts.join(", "))
1768                    };
1769                    let children = float_children(kidss);
1770                    Ok(NestedString { text, children, key: None })
1771                }
1772                ExprKind::Ctor(ctor, flds) => aggregate_nested(cx, ctor, flds, true),
1773                ExprKind::IsCtor(def_id, variant_idx, idx) => {
1774                    let text = format!("is::{:?}::{:?}( {:?} )", def_id, variant_idx, idx);
1775                    Ok(NestedString { text, children: None, key: None })
1776                }
1777                ExprKind::PathProj(e, field) => {
1778                    let e_d = e.fmt_nested(cx)?;
1779                    let text = if e.is_atom() {
1780                        format!("{}.{:?}", e_d.text, field)
1781                    } else {
1782                        format!("({}).{:?}", e_d.text, field)
1783                    };
1784                    Ok(NestedString { text, children: e_d.children, key: None })
1785                }
1786                ExprKind::Alias(alias, args) => {
1787                    let mut texts = vec![];
1788                    let mut kidss = vec![];
1789                    for arg in args {
1790                        let arg_d = arg.fmt_nested(cx)?;
1791                        texts.push(arg_d.text);
1792                        kidss.push(arg_d.children);
1793                    }
1794                    let text = format_cx!(cx, "{:?}({:?})", alias, texts.join(", "));
1795                    let children = float_children(kidss);
1796                    Ok(NestedString { text, children, key: None })
1797                }
1798                ExprKind::App(func, _, args) => {
1799                    let func_d = func.fmt_nested(cx)?;
1800                    let mut texts = vec![];
1801                    let mut kidss = vec![func_d.children];
1802                    for arg in args {
1803                        let arg_d = arg.fmt_nested(cx)?;
1804                        texts.push(arg_d.text);
1805                        kidss.push(arg_d.children);
1806                    }
1807                    let text = if func.is_atom() {
1808                        format!("{}({})", func_d.text, texts.join(", "))
1809                    } else {
1810                        format!("({})({})", func_d.text, texts.join(", "))
1811                    };
1812                    let children = float_children(kidss);
1813                    Ok(NestedString { text, children, key: None })
1814                }
1815                ExprKind::Abs(lambda) => lambda.fmt_nested(cx),
1816                ExprKind::Let(init, body) => {
1817                    // FIXME this is very wrong!
1818                    nested_with_bound_vars(cx, "let", body.vars(), None, |prefix| {
1819                        let body = body.skip_binder_ref().fmt_nested(cx)?;
1820                        let text = format!("{:?} {}{}", init, prefix, body.text);
1821                        Ok(NestedString { text, children: body.children, key: None })
1822                    })
1823                }
1824                ExprKind::BoundedQuant(kind, rng, body) => {
1825                    let left = match kind {
1826                        fhir::QuantKind::Forall => "∀",
1827                        fhir::QuantKind::Exists => "∃",
1828                    };
1829                    let right = Some(format!(" in {}..{}", rng.start, rng.end));
1830
1831                    nested_with_bound_vars(cx, left, body.vars(), right, |all_str| {
1832                        let expr_d = body.as_ref().skip_binder().fmt_nested(cx)?;
1833                        let text = format!("{}{}", all_str, expr_d.text);
1834                        Ok(NestedString { text, children: expr_d.children, key: None })
1835                    })
1836                }
1837                ExprKind::ForAll(expr) => {
1838                    nested_with_bound_vars(cx, "∀", expr.vars(), None, |all_str| {
1839                        let expr_d = expr.as_ref().skip_binder().fmt_nested(cx)?;
1840                        let text = format!("{}{}", all_str, expr_d.text);
1841                        Ok(NestedString { text, children: expr_d.children, key: None })
1842                    })
1843                }
1844            }
1845        }
1846    }
1847}
flux_middle/rty/expr.rs

flux_middle/rty/
expr.rs
