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

flux_middle/rty/
expr.rs
