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

flux_middle/rty/
expr.rs
