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

flux_middle/rty/
expr.rs
