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

flux_middle/rty/
expr.rs
