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

flux_middle/rty/
expr.rs
