1use std::{fmt, iter, ops::ControlFlow, sync::OnceLock};
2
3use flux_arc_interner::{Interned, List, impl_internable, impl_slice_internable};
4use flux_common::bug;
5use flux_macros::{TypeFoldable, TypeVisitable};
6use flux_rustc_bridge::{
7 ToRustc,
8 const_eval::{scalar_to_bits, scalar_to_int, scalar_to_uint},
9 ty::{Const, ConstKind, ValTree, VariantIdx},
10};
11use itertools::Itertools;
12use rustc_abi::{FIRST_VARIANT, FieldIdx};
13use rustc_data_structures::snapshot_map::SnapshotMap;
14use rustc_hir::def_id::DefId;
15use rustc_index::newtype_index;
16use rustc_macros::{Decodable, Encodable, TyDecodable, TyEncodable};
17use rustc_middle::{
18 mir::Local,
19 ty::{ParamConst, ScalarInt, TyCtxt},
20};
21use rustc_span::{Span, Symbol};
22use rustc_type_ir::{BoundVar, DebruijnIndex, INNERMOST};
23
24use super::{
25 BaseTy, Binder, BoundReftKind, BoundVariableKinds, FuncSort, GenericArgs, GenericArgsExt as _,
26 IntTy, Sort, UintTy,
27};
28use crate::{
29 big_int::BigInt,
30 def_id::FluxDefId,
31 fhir::{self},
32 global_env::GlobalEnv,
33 pretty::*,
34 queries::QueryResult,
35 rty::{
36 BoundVariableKind, SortArg,
37 fold::{
38 TypeFoldable, TypeFolder, TypeSuperFoldable, TypeSuperVisitable, TypeVisitable as _,
39 TypeVisitor,
40 },
41 },
42};
43
44#[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 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 match bty {
261 BaseTy::Int(_) => {
262 let bits = bits as i128;
263 ExprKind::Constant(Constant::from(bits)).intern()
264 }
265 BaseTy::Uint(_) => ExprKind::Constant(Constant::from(bits)).intern(),
266 BaseTy::Bool => ExprKind::Constant(Constant::Bool(bits != 0)).intern(),
267 BaseTy::Char => {
268 let c = char::from_u32(bits.try_into().unwrap()).unwrap();
269 ExprKind::Constant(Constant::Char(c)).intern()
270 }
271 _ => bug!(),
272 }
273 }
274
275 pub fn ite(p: impl Into<Expr>, e1: impl Into<Expr>, e2: impl Into<Expr>) -> Expr {
276 ExprKind::IfThenElse(p.into(), e1.into(), e2.into()).intern()
277 }
278
279 pub fn abs(lam: Lambda) -> Expr {
280 ExprKind::Abs(lam).intern()
281 }
282
283 pub fn let_(init: Expr, body: Binder<Expr>) -> Expr {
284 ExprKind::Let(init, body).intern()
285 }
286
287 pub fn bounded_quant(kind: fhir::QuantKind, rng: fhir::Range, body: Binder<Expr>) -> Expr {
288 ExprKind::BoundedQuant(kind, rng, body).intern()
289 }
290
291 pub fn hole(kind: HoleKind) -> Expr {
292 ExprKind::Hole(kind).intern()
293 }
294
295 pub fn kvar(kvar: KVar) -> Expr {
296 ExprKind::KVar(kvar).intern()
297 }
298
299 pub fn alias(alias: AliasReft, args: List<Expr>) -> Expr {
300 ExprKind::Alias(alias, args).intern()
301 }
302
303 pub fn forall(expr: Binder<Expr>) -> Expr {
304 ExprKind::ForAll(expr).intern()
305 }
306
307 pub fn binary_op(op: BinOp, e1: impl Into<Expr>, e2: impl Into<Expr>) -> Expr {
308 ExprKind::BinaryOp(op, e1.into(), e2.into()).intern()
309 }
310
311 pub fn prim_val(op: BinOp, e1: impl Into<Expr>, e2: impl Into<Expr>) -> Expr {
312 Expr::app(InternalFuncKind::Val(op), List::empty(), List::from_arr([e1.into(), e2.into()]))
313 }
314
315 pub fn prim_rel(op: BinOp, e1: impl Into<Expr>, e2: impl Into<Expr>) -> Expr {
316 Expr::app(InternalFuncKind::Rel(op), List::empty(), List::from_arr([e1.into(), e2.into()]))
317 }
318
319 pub fn unit_struct(def_id: DefId) -> Expr {
320 Expr::ctor_struct(def_id, List::empty())
321 }
322
323 pub fn cast(from: Sort, to: Sort, idx: Expr) -> Expr {
324 Expr::app(
325 InternalFuncKind::Cast,
326 List::from_arr([SortArg::Sort(from), SortArg::Sort(to)]),
327 List::from_arr([idx]),
328 )
329 }
330
331 pub fn app(func: impl Into<Expr>, sort_args: List<SortArg>, args: List<Expr>) -> Expr {
332 ExprKind::App(func.into(), sort_args, args).intern()
333 }
334
335 pub fn global_func(kind: SpecFuncKind) -> Expr {
336 ExprKind::GlobalFunc(kind).intern()
337 }
338
339 pub fn internal_func(kind: InternalFuncKind) -> Expr {
340 ExprKind::InternalFunc(kind).intern()
341 }
342
343 pub fn eq(e1: impl Into<Expr>, e2: impl Into<Expr>) -> Expr {
344 ExprKind::BinaryOp(BinOp::Eq, e1.into(), e2.into()).intern()
345 }
346
347 pub fn unary_op(op: UnOp, e: impl Into<Expr>) -> Expr {
348 ExprKind::UnaryOp(op, e.into()).intern()
349 }
350
351 pub fn ne(e1: impl Into<Expr>, e2: impl Into<Expr>) -> Expr {
352 ExprKind::BinaryOp(BinOp::Ne, e1.into(), e2.into()).intern()
353 }
354
355 pub fn ge(e1: impl Into<Expr>, e2: impl Into<Expr>) -> Expr {
356 ExprKind::BinaryOp(BinOp::Ge(Sort::Int), e1.into(), e2.into()).intern()
357 }
358
359 pub fn gt(e1: impl Into<Expr>, e2: impl Into<Expr>) -> Expr {
360 ExprKind::BinaryOp(BinOp::Gt(Sort::Int), e1.into(), e2.into()).intern()
361 }
362
363 pub fn lt(e1: impl Into<Expr>, e2: impl Into<Expr>) -> Expr {
364 ExprKind::BinaryOp(BinOp::Lt(Sort::Int), e1.into(), e2.into()).intern()
365 }
366
367 pub fn le(e1: impl Into<Expr>, e2: impl Into<Expr>) -> Expr {
368 ExprKind::BinaryOp(BinOp::Le(Sort::Int), e1.into(), e2.into()).intern()
369 }
370
371 pub fn implies(e1: impl Into<Expr>, e2: impl Into<Expr>) -> Expr {
372 ExprKind::BinaryOp(BinOp::Imp, e1.into(), e2.into()).intern()
373 }
374
375 pub fn field_proj(e: impl Into<Expr>, proj: FieldProj) -> Expr {
376 ExprKind::FieldProj(e.into(), proj).intern()
377 }
378
379 pub fn field_projs(e: impl Into<Expr>, projs: &[FieldProj]) -> Expr {
380 projs.iter().copied().fold(e.into(), Expr::field_proj)
381 }
382
383 pub fn path_proj(base: Expr, field: FieldIdx) -> Expr {
384 ExprKind::PathProj(base, field).intern()
385 }
386
387 pub fn not(&self) -> Expr {
388 ExprKind::UnaryOp(UnOp::Not, self.clone()).intern()
389 }
390
391 pub fn neg(&self) -> Expr {
392 ExprKind::UnaryOp(UnOp::Neg, self.clone()).intern()
393 }
394
395 pub fn kind(&self) -> &ExprKind {
396 &self.kind
397 }
398
399 pub fn is_atom(&self) -> bool {
402 !matches!(self.kind(), ExprKind::Abs(..) | ExprKind::BinaryOp(..) | ExprKind::ForAll(..))
403 }
404
405 pub fn is_trivially_true(&self) -> bool {
408 self.is_true()
409 || matches!(self.kind(), ExprKind::BinaryOp(BinOp::Eq | BinOp::Iff | BinOp::Imp, e1, e2) if e1.erase_spans() == e2.erase_spans())
410 }
411
412 pub fn is_trivially_false(&self) -> bool {
414 self.is_false()
415 }
416
417 fn is_true(&self) -> bool {
419 matches!(self.kind(), ExprKind::Constant(Constant::Bool(true)))
420 }
421
422 fn is_false(&self) -> bool {
424 matches!(self.kind(), ExprKind::Constant(Constant::Bool(false)))
425 }
426
427 pub fn from_const(tcx: TyCtxt, c: &Const) -> Expr {
428 match &c.kind {
429 ConstKind::Param(param_const) => Expr::const_generic(*param_const),
430 ConstKind::Value(ty, ValTree::Leaf(scalar)) => {
431 Expr::constant(Constant::from_scalar_int(tcx, *scalar, ty).unwrap())
432 }
433 ConstKind::Value(_ty, ValTree::Branch(_)) => {
434 bug!("todo: ValTree::Branch {c:?}")
435 }
436 ConstKind::Unevaluated(_) => bug!("unexpected `ConstKind::Unevaluated`"),
438
439 ConstKind::Infer(_) => bug!("unexpected `ConstKind::Infer`"),
440 }
441 }
442
443 pub fn is_binary_op(&self) -> bool {
444 matches!(self.kind(), ExprKind::BinaryOp(..))
445 }
446
447 fn const_op(op: &BinOp, c1: &Constant, c2: &Constant) -> Option<Constant> {
448 match op {
449 BinOp::Iff => c1.iff(c2),
450 BinOp::Imp => c1.imp(c2),
451 BinOp::Or => c1.or(c2),
452 BinOp::And => c1.and(c2),
453 BinOp::Gt(Sort::Int) => c1.gt(c2),
454 BinOp::Ge(Sort::Int) => c1.ge(c2),
455 BinOp::Lt(Sort::Int) => c2.gt(c1),
456 BinOp::Le(Sort::Int) => c2.ge(c1),
457 BinOp::Eq => Some(c1.eq(c2)),
458 BinOp::Ne => Some(c1.ne(c2)),
459 _ => None,
460 }
461 }
462
463 pub fn simplify(&self, assumed_preds: &SnapshotMap<Expr, ()>) -> Expr {
469 struct Simplify<'a> {
470 assumed_preds: &'a SnapshotMap<Expr, ()>,
471 }
472
473 impl TypeFolder for Simplify<'_> {
474 fn fold_expr(&mut self, expr: &Expr) -> Expr {
475 if self.assumed_preds.get(&expr.erase_spans()).is_some() {
476 return Expr::tt();
477 }
478 let span = expr.span();
479 match expr.kind() {
480 ExprKind::BinaryOp(op, e1, e2) => {
481 let e1 = e1.fold_with(self);
482 let e2 = e2.fold_with(self);
483 match (op, e1.kind(), e2.kind()) {
484 (BinOp::And, ExprKind::Constant(Constant::Bool(false)), _) => {
485 Expr::constant(Constant::Bool(false)).at_opt(e1.span())
486 }
487 (BinOp::And, _, ExprKind::Constant(Constant::Bool(false))) => {
488 Expr::constant(Constant::Bool(false)).at_opt(e2.span())
489 }
490 (BinOp::And, ExprKind::Constant(Constant::Bool(true)), _) => e2,
491 (BinOp::And, _, ExprKind::Constant(Constant::Bool(true))) => e1,
492 (op, ExprKind::Constant(c1), ExprKind::Constant(c2)) => {
493 if let Some(c) = Expr::const_op(op, c1, c2) {
494 Expr::constant(c).at_opt(span.or(e2.span()))
495 } else {
496 Expr::binary_op(op.clone(), e1, e2).at_opt(span)
497 }
498 }
499 _ => Expr::binary_op(op.clone(), e1, e2).at_opt(span),
500 }
501 }
502 ExprKind::UnaryOp(UnOp::Not, e) => {
503 let e = e.fold_with(self);
504 match e.kind() {
505 ExprKind::Constant(Constant::Bool(b)) => {
506 Expr::constant(Constant::Bool(!b))
507 }
508 ExprKind::UnaryOp(UnOp::Not, e) => e.clone(),
509 ExprKind::BinaryOp(BinOp::Eq, e1, e2) => {
510 Expr::binary_op(BinOp::Ne, e1, e2).at_opt(span)
511 }
512 _ => Expr::unary_op(UnOp::Not, e).at_opt(span),
513 }
514 }
515 ExprKind::IfThenElse(p, e1, e2) => {
516 let p = p.fold_with(self);
517 if p.is_trivially_true() {
518 e1.fold_with(self).at_opt(span)
519 } else if p.is_trivially_false() {
520 e2.fold_with(self).at_opt(span)
521 } else {
522 Expr::ite(p, e1.fold_with(self), e2.fold_with(self)).at_opt(span)
523 }
524 }
525 _ => expr.super_fold_with(self),
526 }
527 }
528 }
529 self.fold_with(&mut Simplify { assumed_preds })
530 }
531
532 pub fn to_loc(&self) -> Option<Loc> {
533 match self.kind() {
534 ExprKind::Local(local) => Some(Loc::Local(*local)),
535 ExprKind::Var(var) => Some(Loc::Var(*var)),
536 _ => None,
537 }
538 }
539
540 pub fn to_path(&self) -> Option<Path> {
541 let mut expr = self;
542 let mut proj = vec![];
543 while let ExprKind::PathProj(e, field) = expr.kind() {
544 proj.push(*field);
545 expr = e;
546 }
547 proj.reverse();
548 Some(Path::new(expr.to_loc()?, proj))
549 }
550
551 pub fn is_abs(&self) -> bool {
552 matches!(self.kind(), ExprKind::Abs(..))
553 }
554
555 pub fn is_unit(&self) -> bool {
557 matches!(self.kind(), ExprKind::Tuple(flds) if flds.is_empty())
558 || matches!(self.kind(), ExprKind::Ctor(Ctor::Struct(_), flds) if flds.is_empty())
559 }
560
561 pub fn eta_expand_abs(&self, inputs: &BoundVariableKinds, output: Sort) -> Lambda {
562 let args = (0..inputs.len())
563 .map(|idx| Expr::bvar(INNERMOST, BoundVar::from_usize(idx), BoundReftKind::Annon))
564 .collect();
565 let body = Expr::app(self, List::empty(), args);
566 Lambda::bind_with_vars(body, inputs.clone(), output)
567 }
568
569 pub fn proj_and_reduce(&self, proj: FieldProj) -> Expr {
571 match self.kind() {
572 ExprKind::Tuple(flds) | ExprKind::Ctor(Ctor::Struct(_), flds) => {
573 flds[proj.field_idx() as usize].clone()
574 }
575 _ => Expr::field_proj(self.clone(), proj),
576 }
577 }
578
579 pub fn flatten_conjs(&self) -> Vec<&Expr> {
580 fn go<'a>(e: &'a Expr, vec: &mut Vec<&'a Expr>) {
581 if let ExprKind::BinaryOp(BinOp::And, e1, e2) = e.kind() {
582 go(e1, vec);
583 go(e2, vec);
584 } else {
585 vec.push(e);
586 }
587 }
588 let mut vec = vec![];
589 go(self, &mut vec);
590 vec
591 }
592
593 pub fn has_evars(&self) -> bool {
594 struct HasEvars;
595
596 impl TypeVisitor for HasEvars {
597 type BreakTy = ();
598 fn visit_expr(&mut self, expr: &Expr) -> ControlFlow<Self::BreakTy> {
599 if let ExprKind::Var(Var::EVar(_)) = expr.kind() {
600 ControlFlow::Break(())
601 } else {
602 expr.super_visit_with(self)
603 }
604 }
605 }
606
607 self.visit_with(&mut HasEvars).is_break()
608 }
609
610 pub fn erase_spans(&self) -> Expr {
611 struct SpanEraser;
612 impl TypeFolder for SpanEraser {
613 fn fold_expr(&mut self, e: &Expr) -> Expr {
614 e.super_fold_with(self).at_opt(None)
615 }
616 }
617 self.fold_with(&mut SpanEraser)
618 }
619}
620
621#[derive(Clone, Copy, PartialEq, Eq, Hash, TyEncodable, TyDecodable, Debug)]
622pub struct ESpan {
623 pub span: Span,
625 pub base: Option<Span>,
627}
628
629impl ESpan {
630 pub fn new(span: Span) -> Self {
631 Self { span, base: None }
632 }
633
634 pub fn with_base(&self, espan: ESpan) -> Self {
635 Self { span: self.span, base: Some(espan.span) }
636 }
637}
638
639#[derive(
640 Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable, Debug, TypeFoldable, TypeVisitable,
641)]
642pub enum BinOp {
643 Iff,
644 Imp,
645 Or,
646 And,
647 Eq,
648 Ne,
649 Gt(Sort),
650 Ge(Sort),
651 Lt(Sort),
652 Le(Sort),
653 Add(Sort),
654 Sub(Sort),
655 Mul(Sort),
656 Div(Sort),
657 Mod(Sort),
658 BitAnd,
659 BitOr,
660 BitShl,
661 BitShr,
662}
663
664#[derive(Clone, Copy, PartialEq, Eq, Hash, Encodable, Debug, Decodable)]
665pub enum UnOp {
666 Not,
667 Neg,
668}
669
670#[derive(Copy, Clone, PartialEq, Eq, Debug, Hash, TyEncodable, TyDecodable)]
671pub enum Ctor {
672 Struct(DefId),
674 Enum(DefId, VariantIdx),
676}
677
678impl Ctor {
679 pub fn def_id(&self) -> DefId {
680 match self {
681 Self::Struct(def_id) | Self::Enum(def_id, _) => *def_id,
682 }
683 }
684
685 pub fn variant_idx(&self) -> VariantIdx {
686 match self {
687 Self::Struct(_) => FIRST_VARIANT,
688 Self::Enum(_, variant_idx) => *variant_idx,
689 }
690 }
691
692 fn is_enum(&self) -> bool {
693 matches!(self, Self::Enum(..))
694 }
695}
696
697#[derive(Debug, Clone, TyEncodable, TyDecodable, PartialEq, Eq, Hash)]
711pub enum InternalFuncKind {
712 Val(BinOp),
714 Rel(BinOp),
716 Cast,
718}
719
720#[derive(Debug, Clone, TyEncodable, TyDecodable, PartialEq, Eq, Hash)]
721pub enum SpecFuncKind {
722 Thy(liquid_fixpoint::ThyFunc),
724 Uif(FluxDefId),
726 Def(FluxDefId),
728}
729
730#[derive(Clone, PartialEq, Eq, Hash, TyEncodable, Debug, TyDecodable)]
731pub enum ExprKind {
732 Var(Var),
733 Local(Local),
734 Constant(Constant),
735 ConstDefId(DefId),
736 BinaryOp(BinOp, Expr, Expr),
737 GlobalFunc(SpecFuncKind),
738 InternalFunc(InternalFuncKind),
739 UnaryOp(UnOp, Expr),
740 FieldProj(Expr, FieldProj),
741 Ctor(Ctor, List<Expr>),
743 Tuple(List<Expr>),
744 PathProj(Expr, FieldIdx),
745 IfThenElse(Expr, Expr, Expr),
746 KVar(KVar),
747 Alias(AliasReft, List<Expr>),
748 Let(Expr, Binder<Expr>),
749 App(Expr, List<SortArg>, List<Expr>),
755 Abs(Lambda),
765
766 BoundedQuant(fhir::QuantKind, fhir::Range, Binder<Expr>),
768 Hole(HoleKind),
782 ForAll(Binder<Expr>),
783}
784
785impl ExprKind {
786 fn intern(self) -> Expr {
787 Expr { kind: Interned::new(self), espan: None }
788 }
789}
790
791#[derive(Clone, Copy, PartialEq, Eq, Hash, TyEncodable, TyDecodable, Debug)]
792pub enum AggregateKind {
793 Tuple(usize),
794 Adt(DefId),
795}
796
797impl AggregateKind {
798 pub fn to_proj(self, field: u32) -> FieldProj {
799 match self {
800 AggregateKind::Tuple(arity) => FieldProj::Tuple { arity, field },
801 AggregateKind::Adt(def_id) => FieldProj::Adt { def_id, field },
802 }
803 }
804}
805
806#[derive(Clone, Copy, PartialEq, Eq, Hash, TyEncodable, TyDecodable, Debug)]
807pub enum FieldProj {
808 Tuple { arity: usize, field: u32 },
809 Adt { def_id: DefId, field: u32 },
810}
811
812impl FieldProj {
813 pub fn arity(&self, genv: GlobalEnv) -> QueryResult<usize> {
814 match self {
815 FieldProj::Tuple { arity, .. } => Ok(*arity),
816 FieldProj::Adt { def_id, .. } => {
817 Ok(genv.adt_sort_def_of(*def_id)?.struct_variant().fields())
818 }
819 }
820 }
821
822 pub fn field_idx(&self) -> u32 {
823 match self {
824 FieldProj::Tuple { field, .. } | FieldProj::Adt { field, .. } => *field,
825 }
826 }
827}
828
829#[derive(
835 Debug, Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable, TypeFoldable, TypeVisitable,
836)]
837pub enum HoleKind {
838 Pred,
843 Expr(Sort),
850}
851
852#[derive(Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable)]
857pub struct KVar {
858 pub kvid: KVid,
859 pub self_args: usize,
861 pub args: List<Expr>,
864}
865
866#[derive(Clone, Debug, Copy, PartialEq, Eq, Hash, PartialOrd, Ord, Encodable, Decodable)]
867pub struct EarlyReftParam {
868 pub index: u32,
869 pub name: Symbol,
870}
871
872#[derive(Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord, Encodable, Decodable, Debug)]
873pub struct BoundReft {
874 pub var: BoundVar,
875 pub kind: BoundReftKind,
876}
877
878#[derive(Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord, TyEncodable, TyDecodable)]
879pub enum Var {
880 Free(Name),
881 Bound(DebruijnIndex, BoundReft),
882 EarlyParam(EarlyReftParam),
883 EVar(EVid),
884 ConstGeneric(ParamConst),
885}
886
887#[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord, TyEncodable, TyDecodable)]
888pub struct Path {
889 pub loc: Loc,
890 projection: List<FieldIdx>,
891}
892
893#[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord, TyEncodable, TyDecodable)]
894pub enum Loc {
895 Local(Local),
896 Var(Var),
897}
898
899newtype_index! {
900 #[debug_format = "?{}e"]
902 #[orderable]
903 #[encodable]
904 pub struct EVid {}
905}
906
907newtype_index! {
908 #[debug_format = "$k{}"]
909 #[encodable]
910 pub struct KVid {}
911}
912
913newtype_index! {
914 #[debug_format = "a{}"]
915 #[orderable]
916 #[encodable]
917 pub struct Name {}
918}
919
920impl KVar {
921 pub fn new(kvid: KVid, self_args: usize, args: Vec<Expr>) -> Self {
922 KVar { kvid, self_args, args: List::from_vec(args) }
923 }
924
925 fn self_args(&self) -> &[Expr] {
926 &self.args[..self.self_args]
927 }
928
929 fn scope(&self) -> &[Expr] {
930 &self.args[self.self_args..]
931 }
932}
933
934impl Var {
935 pub fn to_expr(&self) -> Expr {
936 Expr::var(*self)
937 }
938}
939
940impl Path {
941 pub fn new(loc: Loc, projection: impl Into<List<FieldIdx>>) -> Path {
942 Path { loc, projection: projection.into() }
943 }
944
945 pub fn projection(&self) -> &[FieldIdx] {
946 &self.projection[..]
947 }
948
949 pub fn to_expr(&self) -> Expr {
950 self.projection
951 .iter()
952 .fold(self.loc.to_expr(), |e, f| Expr::path_proj(e, *f))
953 }
954
955 pub fn to_loc(&self) -> Option<Loc> {
956 if self.projection.is_empty() { Some(self.loc) } else { None }
957 }
958}
959
960impl Loc {
961 pub fn to_expr(&self) -> Expr {
962 match self {
963 Loc::Local(local) => Expr::local(*local),
964 Loc::Var(var) => Expr::var(*var),
965 }
966 }
967}
968
969macro_rules! impl_ops {
970 ($($op:ident: $method:ident),*) => {$(
971 impl<Rhs> std::ops::$op<Rhs> for Expr
972 where
973 Rhs: Into<Expr>,
974 {
975 type Output = Expr;
976
977 fn $method(self, rhs: Rhs) -> Self::Output {
978 let sort = crate::rty::Sort::Int;
979 Expr::binary_op(BinOp::$op(sort), self, rhs)
980 }
981 }
982
983 impl<Rhs> std::ops::$op<Rhs> for &Expr
984 where
985 Rhs: Into<Expr>,
986 {
987 type Output = Expr;
988
989 fn $method(self, rhs: Rhs) -> Self::Output {
990 let sort = crate::rty::Sort::Int;
991 Expr::binary_op(BinOp::$op(sort), self, rhs)
992 }
993 }
994 )*};
995}
996impl_ops!(Add: add, Sub: sub, Mul: mul, Div: div);
997
998impl From<i32> for Expr {
999 fn from(value: i32) -> Self {
1000 Expr::constant(Constant::from(value))
1001 }
1002}
1003
1004impl From<&Expr> for Expr {
1005 fn from(e: &Expr) -> Self {
1006 e.clone()
1007 }
1008}
1009
1010impl From<Path> for Expr {
1011 fn from(path: Path) -> Self {
1012 path.to_expr()
1013 }
1014}
1015
1016impl From<Name> for Expr {
1017 fn from(name: Name) -> Self {
1018 Expr::fvar(name)
1019 }
1020}
1021
1022impl From<Var> for Expr {
1023 fn from(var: Var) -> Self {
1024 Expr::var(var)
1025 }
1026}
1027
1028impl From<SpecFuncKind> for Expr {
1029 fn from(kind: SpecFuncKind) -> Self {
1030 Expr::global_func(kind)
1031 }
1032}
1033
1034impl From<InternalFuncKind> for Expr {
1035 fn from(kind: InternalFuncKind) -> Self {
1036 Expr::internal_func(kind)
1037 }
1038}
1039
1040impl From<Loc> for Path {
1041 fn from(loc: Loc) -> Self {
1042 Path::new(loc, vec![])
1043 }
1044}
1045
1046impl From<Name> for Loc {
1047 fn from(name: Name) -> Self {
1048 Loc::Var(Var::Free(name))
1049 }
1050}
1051
1052impl From<Local> for Loc {
1053 fn from(local: Local) -> Self {
1054 Loc::Local(local)
1055 }
1056}
1057
1058#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Encodable, Decodable)]
1059pub struct Real(pub u128);
1060
1061impl liquid_fixpoint::FixpointFmt for Real {
1062 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1063 write!(f, "{}.0", self.0)
1064 }
1065}
1066
1067#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Encodable, Decodable)]
1068pub enum Constant {
1069 Int(BigInt),
1070 Real(Real),
1071 Bool(bool),
1072 Str(Symbol),
1073 Char(char),
1074 BitVec(u128, u32),
1075}
1076
1077impl Constant {
1078 pub const ZERO: Constant = Constant::Int(BigInt::ZERO);
1079 pub const ONE: Constant = Constant::Int(BigInt::ONE);
1080 pub const TRUE: Constant = Constant::Bool(true);
1081
1082 fn to_bool(self) -> Option<bool> {
1083 match self {
1084 Constant::Bool(b) => Some(b),
1085 _ => None,
1086 }
1087 }
1088
1089 fn to_int(self) -> Option<BigInt> {
1090 match self {
1091 Constant::Int(n) => Some(n),
1092 _ => None,
1093 }
1094 }
1095
1096 pub fn iff(&self, other: &Constant) -> Option<Constant> {
1097 let b1 = self.to_bool()?;
1098 let b2 = other.to_bool()?;
1099 Some(Constant::Bool(b1 == b2))
1100 }
1101
1102 pub fn imp(&self, other: &Constant) -> Option<Constant> {
1103 let b1 = self.to_bool()?;
1104 let b2 = other.to_bool()?;
1105 Some(Constant::Bool(!b1 || b2))
1106 }
1107
1108 pub fn or(&self, other: &Constant) -> Option<Constant> {
1109 let b1 = self.to_bool()?;
1110 let b2 = other.to_bool()?;
1111 Some(Constant::Bool(b1 || b2))
1112 }
1113
1114 pub fn and(&self, other: &Constant) -> Option<Constant> {
1115 let b1 = self.to_bool()?;
1116 let b2 = other.to_bool()?;
1117 Some(Constant::Bool(b1 && b2))
1118 }
1119
1120 pub fn eq(&self, other: &Constant) -> Constant {
1121 Constant::Bool(*self == *other)
1122 }
1123
1124 pub fn ne(&self, other: &Constant) -> Constant {
1125 Constant::Bool(*self != *other)
1126 }
1127
1128 pub fn gt(&self, other: &Constant) -> Option<Constant> {
1129 let n1 = self.to_int()?;
1130 let n2 = other.to_int()?;
1131 Some(Constant::Bool(n1 > n2))
1132 }
1133
1134 pub fn ge(&self, other: &Constant) -> Option<Constant> {
1135 let n1 = self.to_int()?;
1136 let n2 = other.to_int()?;
1137 Some(Constant::Bool(n1 >= n2))
1138 }
1139
1140 pub fn from_scalar_int<'tcx, T>(tcx: TyCtxt<'tcx>, scalar: ScalarInt, t: &T) -> Option<Self>
1141 where
1142 T: ToRustc<'tcx, T = rustc_middle::ty::Ty<'tcx>>,
1143 {
1144 use rustc_middle::ty::TyKind;
1145 let ty = t.to_rustc(tcx);
1146 match ty.kind() {
1147 TyKind::Int(int_ty) => Some(Constant::from(scalar_to_int(tcx, scalar, *int_ty))),
1148 TyKind::Uint(uint_ty) => Some(Constant::from(scalar_to_uint(tcx, scalar, *uint_ty))),
1149 TyKind::Bool => {
1150 let b = scalar_to_bits(tcx, scalar, ty)?;
1151 Some(Constant::Bool(b != 0))
1152 }
1153 TyKind::Char => {
1154 let b = scalar_to_bits(tcx, scalar, ty)?;
1155 Some(Constant::Char(char::from_u32(b as u32)?))
1156 }
1157 _ => bug!(),
1158 }
1159 }
1160
1161 pub fn int_min(bit_width: u32) -> Constant {
1163 Constant::Int(BigInt::int_min(bit_width))
1164 }
1165
1166 pub fn int_max(bit_width: u32) -> Constant {
1168 Constant::Int(BigInt::int_max(bit_width))
1169 }
1170
1171 pub fn uint_max(bit_width: u32) -> Constant {
1173 Constant::Int(BigInt::uint_max(bit_width))
1174 }
1175}
1176
1177impl From<i32> for Constant {
1178 fn from(c: i32) -> Self {
1179 Constant::Int(c.into())
1180 }
1181}
1182
1183impl From<usize> for Constant {
1184 fn from(u: usize) -> Self {
1185 Constant::Int(u.into())
1186 }
1187}
1188
1189impl From<u128> for Constant {
1190 fn from(c: u128) -> Self {
1191 Constant::Int(c.into())
1192 }
1193}
1194
1195impl From<i128> for Constant {
1196 fn from(c: i128) -> Self {
1197 Constant::Int(c.into())
1198 }
1199}
1200
1201impl From<bool> for Constant {
1202 fn from(b: bool) -> Self {
1203 Constant::Bool(b)
1204 }
1205}
1206
1207impl From<Symbol> for Constant {
1208 fn from(s: Symbol) -> Self {
1209 Constant::Str(s)
1210 }
1211}
1212
1213impl From<char> for Constant {
1214 fn from(c: char) -> Self {
1215 Constant::Char(c)
1216 }
1217}
1218
1219impl_internable!(ExprKind);
1220impl_slice_internable!(Expr, KVar);
1221
1222#[derive(Debug)]
1223pub struct FieldBind<T> {
1224 pub name: Symbol,
1225 pub value: T,
1226}
1227
1228impl<T: Pretty> Pretty for FieldBind<T> {
1229 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1230 w!(cx, f, "{}: {:?}", ^self.name, &self.value)
1231 }
1232}
1233
1234pub(crate) mod pretty {
1235 use flux_rustc_bridge::def_id_to_string;
1236
1237 use super::*;
1238 use crate::{name_of_thy_func, rty::pretty::nested_with_bound_vars};
1239
1240 #[derive(PartialEq, Eq, PartialOrd, Ord)]
1241 enum Precedence {
1242 Iff,
1243 Imp,
1244 Or,
1245 And,
1246 Cmp,
1247 Bitvec,
1248 AddSub,
1249 MulDiv,
1250 }
1251
1252 impl BinOp {
1253 fn precedence(&self) -> Precedence {
1254 match self {
1255 BinOp::Iff => Precedence::Iff,
1256 BinOp::Imp => Precedence::Imp,
1257 BinOp::Or => Precedence::Or,
1258 BinOp::And => Precedence::And,
1259 BinOp::Eq
1260 | BinOp::Ne
1261 | BinOp::Gt(_)
1262 | BinOp::Lt(_)
1263 | BinOp::Ge(_)
1264 | BinOp::Le(_) => Precedence::Cmp,
1265 BinOp::Add(_) | BinOp::Sub(_) => Precedence::AddSub,
1266 BinOp::Mul(_) | BinOp::Div(_) | BinOp::Mod(_) => Precedence::MulDiv,
1267 BinOp::BitAnd | BinOp::BitOr | BinOp::BitShl | BinOp::BitShr => Precedence::Bitvec,
1268 }
1269 }
1270 }
1271
1272 impl Precedence {
1273 pub fn is_associative(&self) -> bool {
1274 !matches!(self, Precedence::Imp | Precedence::Cmp)
1275 }
1276 }
1277
1278 pub fn should_parenthesize(op: &BinOp, child: &Expr) -> bool {
1279 if let ExprKind::BinaryOp(child_op, ..) = child.kind() {
1280 child_op.precedence() < op.precedence()
1281 || (child_op.precedence() == op.precedence() && !op.precedence().is_associative())
1282 } else {
1283 false
1284 }
1285 }
1286
1287 impl Pretty for Ctor {
1288 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1289 match self {
1290 Ctor::Struct(def_id) => {
1291 w!(cx, f, "{:?}", def_id)
1292 }
1293 Ctor::Enum(def_id, variant_idx) => {
1294 w!(cx, f, "{:?}::{:?}", def_id, ^variant_idx)
1295 }
1296 }
1297 }
1298 }
1299
1300 impl Pretty for fhir::QuantKind {
1301 fn fmt(&self, _cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1302 match self {
1303 fhir::QuantKind::Exists => w!(cx, f, "∃"),
1304 fhir::QuantKind::Forall => w!(cx, f, "∀"),
1305 }
1306 }
1307 }
1308
1309 impl Pretty for InternalFuncKind {
1310 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1311 match self {
1312 InternalFuncKind::Val(op) => w!(cx, f, "[{:?}]", op),
1313 InternalFuncKind::Rel(op) => w!(cx, f, "[{:?}]?", op),
1314 InternalFuncKind::Cast => w!(cx, f, "cast"),
1315 }
1316 }
1317 }
1318
1319 impl Pretty for Expr {
1320 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1321 let e = if cx.simplify_exprs {
1322 self.simplify(&SnapshotMap::default())
1323 } else {
1324 self.clone()
1325 };
1326 match e.kind() {
1327 ExprKind::Var(var) => w!(cx, f, "{:?}", var),
1328 ExprKind::Local(local) => w!(cx, f, "{:?}", ^local),
1329 ExprKind::ConstDefId(did) => w!(cx, f, "{}", ^def_id_to_string(*did)),
1330 ExprKind::Constant(c) => w!(cx, f, "{:?}", c),
1331
1332 ExprKind::BinaryOp(op, e1, e2) => {
1333 if should_parenthesize(op, e1) {
1334 w!(cx, f, "({:?})", e1)?;
1335 } else {
1336 w!(cx, f, "{:?}", e1)?;
1337 }
1338 if matches!(op, BinOp::Div(_)) {
1339 w!(cx, f, "{:?}", op)?;
1340 } else {
1341 w!(cx, f, " {:?} ", op)?;
1342 }
1343 if should_parenthesize(op, e2) {
1344 w!(cx, f, "({:?})", e2)?;
1345 } else {
1346 w!(cx, f, "{:?}", e2)?;
1347 }
1348 Ok(())
1349 }
1350 ExprKind::UnaryOp(op, e) => {
1351 if e.is_atom() {
1352 w!(cx, f, "{:?}{:?}", op, e)
1353 } else {
1354 w!(cx, f, "{:?}({:?})", op, e)
1355 }
1356 }
1357 ExprKind::FieldProj(e, proj) => {
1358 if e.is_atom() {
1359 w!(cx, f, "{:?}.{}", e, ^fmt_field_proj(cx, *proj))
1360 } else {
1361 w!(cx, f, "({:?}).{}", e, ^fmt_field_proj(cx, *proj))
1362 }
1363 }
1364 ExprKind::Tuple(flds) => {
1365 if let [e] = &flds[..] {
1366 w!(cx, f, "({:?},)", e)
1367 } else {
1368 w!(cx, f, "({:?})", join!(", ", flds))
1369 }
1370 }
1371 ExprKind::Ctor(ctor, flds) => {
1372 let def_id = ctor.def_id();
1373 if let Some(adt_sort_def) = cx.adt_sort_def_of(def_id) {
1374 let variant = adt_sort_def.variant(ctor.variant_idx()).field_names();
1375 let fields = iter::zip(variant, flds)
1376 .map(|(name, value)| FieldBind { name: *name, value: value.clone() })
1377 .collect_vec();
1378 match ctor {
1379 Ctor::Struct(_) => {
1380 w!(cx, f, "{:?} {{ {:?} }}", def_id, join!(", ", fields))
1381 }
1382 Ctor::Enum(_, idx) => {
1383 if fields.is_empty() {
1384 w!(cx, f, "{:?}::{:?}", def_id, ^idx.index())
1385 } else {
1386 w!(cx, f, "{:?}::{:?}({:?})", def_id, ^idx.index(), join!(", ", fields))
1387 }
1388 }
1389 }
1390 } else {
1391 match ctor {
1392 Ctor::Struct(_) => {
1393 w!(cx, f, "{:?} {{ {:?} }}", def_id, join!(", ", flds))
1394 }
1395 Ctor::Enum(_, idx) => {
1396 w!(cx, f, "{:?}::{:?} {{ {:?} }}", def_id, ^idx, join!(", ", flds))
1397 }
1398 }
1399 }
1400 }
1401 ExprKind::PathProj(e, field) => {
1402 if e.is_atom() {
1403 w!(cx, f, "{:?}.{:?}", e, field)
1404 } else {
1405 w!(cx, f, "({:?}).{:?}", e, field)
1406 }
1407 }
1408 ExprKind::App(func, _, args) => {
1409 w!(cx, f, "{:?}({})",
1410 parens!(func, !func.is_atom()),
1411 ^args
1412 .iter()
1413 .format_with(", ", |arg, f| f(&format_args_cx!(cx, "{:?}", arg)))
1414 )
1415 }
1416 ExprKind::IfThenElse(p, e1, e2) => {
1417 w!(cx, f, "if {:?} {{ {:?} }} else {{ {:?} }}", p, e1, e2)
1418 }
1419 ExprKind::Hole(_) => {
1420 w!(cx, f, "*")
1421 }
1422 ExprKind::KVar(kvar) => {
1423 w!(cx, f, "{:?}", kvar)
1424 }
1425 ExprKind::Alias(alias, args) => {
1426 w!(cx, f, "{:?}({:?})", alias, join!(", ", args))
1427 }
1428 ExprKind::Abs(lam) => {
1429 w!(cx, f, "{:?}", lam)
1430 }
1431 ExprKind::GlobalFunc(SpecFuncKind::Def(did) | SpecFuncKind::Uif(did)) => {
1432 w!(cx, f, "{}", ^did.name())
1433 }
1434 ExprKind::GlobalFunc(SpecFuncKind::Thy(itf)) => {
1435 if let Some(name) = name_of_thy_func(*itf) {
1436 w!(cx, f, "{}", ^name)
1437 } else {
1438 w!(cx, f, "<error>")
1439 }
1440 }
1441 ExprKind::InternalFunc(func) => {
1442 w!(cx, f, "{:?}", func)
1443 }
1444 ExprKind::ForAll(expr) => {
1445 let vars = expr.vars();
1446 cx.with_bound_vars(vars, || {
1447 if !vars.is_empty() {
1448 cx.fmt_bound_vars(false, "∀", vars, ". ", f)?;
1449 }
1450 w!(cx, f, "{:?}", expr.skip_binder_ref())
1451 })
1452 }
1453 ExprKind::BoundedQuant(kind, rng, body) => {
1454 let vars = body.vars();
1455 cx.with_bound_vars(vars, || {
1456 w!(
1457 cx,
1458 f,
1459 "{:?} {}..{} {{ {:?} }}",
1460 kind,
1461 ^rng.start,
1462 ^rng.end,
1463 body.skip_binder_ref()
1464 )
1465 })
1466 }
1467 ExprKind::Let(init, body) => {
1468 let vars = body.vars();
1469 cx.with_bound_vars(vars, || {
1470 cx.fmt_bound_vars(false, "(let ", vars, " = ", f)?;
1471 w!(cx, f, "{:?} in {:?})", init, body.skip_binder_ref())
1472 })
1473 }
1474 }
1475 }
1476 }
1477
1478 fn fmt_field_proj(cx: &PrettyCx, proj: FieldProj) -> String {
1479 if let FieldProj::Adt { def_id, field } = proj
1480 && let Some(adt_sort_def) = cx.adt_sort_def_of(def_id)
1481 {
1482 format!("{}", adt_sort_def.struct_variant().field_names()[field as usize])
1483 } else {
1484 format!("{}", proj.field_idx())
1485 }
1486 }
1487
1488 impl Pretty for Constant {
1489 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1490 match self {
1491 Constant::Int(i) => w!(cx, f, "{i}"),
1492 Constant::BitVec(i, sz) => w!(cx, f, "bv({i}, {sz})"),
1493 Constant::Real(r) => w!(cx, f, "{}.0", ^r.0),
1494 Constant::Bool(b) => w!(cx, f, "{b}"),
1495 Constant::Str(sym) => w!(cx, f, "\"{sym}\""),
1496 Constant::Char(c) => w!(cx, f, "\'{c}\'"),
1497 }
1498 }
1499 }
1500
1501 impl Pretty for AliasReft {
1502 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1503 w!(cx, f, "<({:?}) as {:?}", &self.args[0], self.assoc_id.parent())?;
1504 let args = &self.args[1..];
1505 if !args.is_empty() {
1506 w!(cx, f, "<{:?}>", join!(", ", args))?;
1507 }
1508 w!(cx, f, ">::{}", ^self.assoc_id.name())
1509 }
1510 }
1511
1512 impl Pretty for Lambda {
1513 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1514 let vars = self.body.vars();
1515 cx.with_bound_vars(vars, || {
1516 cx.fmt_bound_vars(false, "λ", vars, ". ", f)?;
1517 w!(cx, f, "{:?}", self.body.as_ref().skip_binder())
1518 })
1519 }
1520 }
1521
1522 impl Pretty for Var {
1523 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1524 match self {
1525 Var::Bound(debruijn, var) => cx.fmt_bound_reft(*debruijn, *var, f),
1526 Var::EarlyParam(var) => w!(cx, f, "{}", ^var.name),
1527 Var::Free(name) => w!(cx, f, "{:?}", ^name),
1528 Var::EVar(evar) => w!(cx, f, "{:?}", ^evar),
1529 Var::ConstGeneric(param) => w!(cx, f, "{}", ^param.name),
1530 }
1531 }
1532 }
1533
1534 impl Pretty for KVar {
1535 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1536 w!(cx, f, "{:?}", ^self.kvid)?;
1537 match cx.kvar_args {
1538 KVarArgs::All => {
1539 w!(
1540 cx,
1541 f,
1542 "({:?})[{:?}]",
1543 join!(", ", self.self_args()),
1544 join!(", ", self.scope())
1545 )?;
1546 }
1547 KVarArgs::SelfOnly => w!(cx, f, "({:?})", join!(", ", self.self_args()))?,
1548 KVarArgs::Hide => {}
1549 }
1550 Ok(())
1551 }
1552 }
1553
1554 impl Pretty for Path {
1555 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1556 w!(cx, f, "{:?}", &self.loc)?;
1557 for field in &self.projection {
1558 w!(cx, f, ".{}", ^u32::from(*field))?;
1559 }
1560 Ok(())
1561 }
1562 }
1563
1564 impl Pretty for Loc {
1565 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1566 match self {
1567 Loc::Local(local) => w!(cx, f, "{:?}", ^local),
1568 Loc::Var(var) => w!(cx, f, "{:?}", var),
1569 }
1570 }
1571 }
1572
1573 impl Pretty for BinOp {
1574 fn fmt(&self, _cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1575 match self {
1576 BinOp::Iff => w!(cx, f, "⇔"),
1577 BinOp::Imp => w!(cx, f, "⇒"),
1578 BinOp::Or => w!(cx, f, "∨"),
1579 BinOp::And => w!(cx, f, "∧"),
1580 BinOp::Eq => w!(cx, f, "="),
1581 BinOp::Ne => w!(cx, f, "≠"),
1582 BinOp::Gt(_) => w!(cx, f, ">"),
1583 BinOp::Ge(_) => w!(cx, f, "≥"),
1584 BinOp::Lt(_) => w!(cx, f, "<"),
1585 BinOp::Le(_) => w!(cx, f, "≤"),
1586 BinOp::Add(_) => w!(cx, f, "+"),
1587 BinOp::Sub(_) => w!(cx, f, "-"),
1588 BinOp::Mul(_) => w!(cx, f, "*"),
1589 BinOp::Div(_) => w!(cx, f, "/"),
1590 BinOp::Mod(_) => w!(cx, f, "mod"),
1591 BinOp::BitAnd => w!(cx, f, "&"),
1592 BinOp::BitOr => w!(cx, f, "|"),
1593 BinOp::BitShl => w!(cx, f, "<<"),
1594 BinOp::BitShr => w!(cx, f, ">>"),
1595 }
1596 }
1597 }
1598
1599 impl Pretty for UnOp {
1600 fn fmt(&self, _cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1601 match self {
1602 UnOp::Not => w!(cx, f, "¬"),
1603 UnOp::Neg => w!(cx, f, "-"),
1604 }
1605 }
1606 }
1607
1608 impl_debug_with_default_cx!(Expr, Loc, Path, Var, KVar, Lambda, AliasReft);
1609
1610 impl PrettyNested for Lambda {
1611 fn fmt_nested(&self, cx: &PrettyCx) -> Result<NestedString, fmt::Error> {
1612 nested_with_bound_vars(cx, "λ", self.body.vars(), None, |prefix| {
1613 let expr_d = self.body.skip_binder_ref().fmt_nested(cx)?;
1614 let text = format!("{}{}", prefix, expr_d.text);
1615 Ok(NestedString { text, children: expr_d.children, key: None })
1616 })
1617 }
1618 }
1619
1620 pub fn aggregate_nested(
1621 cx: &PrettyCx,
1622 ctor: &Ctor,
1623 flds: &[Expr],
1624 is_named: bool,
1625 ) -> Result<NestedString, fmt::Error> {
1626 let def_id = ctor.def_id();
1627 let mut text =
1628 if is_named && ctor.is_enum() { format_cx!(cx, "{:?}", ctor) } else { "".to_string() };
1629 if flds.is_empty() {
1630 Ok(NestedString { text, children: None, key: None })
1632 } else if flds.len() == 1 {
1633 text += &format_cx!(cx, "{:?} ", flds[0].clone());
1635 Ok(NestedString { text, children: None, key: None })
1636 } else {
1637 let keys = if let Some(adt_sort_def) = cx.adt_sort_def_of(def_id) {
1638 adt_sort_def
1639 .variant(ctor.variant_idx())
1640 .field_names()
1641 .iter()
1642 .map(|name| format!("{name}"))
1643 .collect_vec()
1644 } else {
1645 (0..flds.len()).map(|i| format!("arg{i}")).collect_vec()
1646 };
1647 text += "{..}";
1649 let mut children = vec![];
1650 for (key, fld) in iter::zip(keys, flds) {
1651 let fld_d = fld.fmt_nested(cx)?;
1652 children.push(NestedString { key: Some(key), ..fld_d });
1653 }
1654 Ok(NestedString { text, children: Some(children), key: None })
1655 }
1656 }
1657
1658 impl PrettyNested for Expr {
1659 fn fmt_nested(&self, cx: &PrettyCx) -> Result<NestedString, fmt::Error> {
1660 let e = if cx.simplify_exprs {
1661 self.simplify(&SnapshotMap::default())
1662 } else {
1663 self.clone()
1664 };
1665 match e.kind() {
1666 ExprKind::Var(..)
1667 | ExprKind::Local(..)
1668 | ExprKind::Constant(..)
1669 | ExprKind::ConstDefId(..)
1670 | ExprKind::Hole(..)
1671 | ExprKind::GlobalFunc(..)
1672 | ExprKind::InternalFunc(..)
1673 | ExprKind::KVar(..) => debug_nested(cx, &e),
1674
1675 ExprKind::IfThenElse(p, e1, e2) => {
1676 let p_d = p.fmt_nested(cx)?;
1677 let e1_d = e1.fmt_nested(cx)?;
1678 let e2_d = e2.fmt_nested(cx)?;
1679 let text = format!("(if {} then {} else {})", p_d.text, e1_d.text, e2_d.text);
1680 let children = float_children(vec![p_d.children, e1_d.children, e2_d.children]);
1681 Ok(NestedString { text, children, key: None })
1682 }
1683 ExprKind::BinaryOp(op, e1, e2) => {
1684 let e1_d = e1.fmt_nested(cx)?;
1685 let e2_d = e2.fmt_nested(cx)?;
1686 let e1_text = if should_parenthesize(op, e1) {
1687 format!("({})", e1_d.text)
1688 } else {
1689 e1_d.text
1690 };
1691 let e2_text = if should_parenthesize(op, e2) {
1692 format!("({})", e2_d.text)
1693 } else {
1694 e2_d.text
1695 };
1696 let op_d = debug_nested(cx, op)?;
1697 let op_text = if matches!(op, BinOp::Div(_)) {
1698 op_d.text
1699 } else {
1700 format!(" {} ", op_d.text)
1701 };
1702 let text = format!("{e1_text}{op_text}{e2_text}");
1703 let children = float_children(vec![e1_d.children, e2_d.children]);
1704 Ok(NestedString { text, children, key: None })
1705 }
1706 ExprKind::UnaryOp(op, e) => {
1707 let e_d = e.fmt_nested(cx)?;
1708 let op_d = debug_nested(cx, op)?;
1709 let text = if e.is_atom() {
1710 format!("{}{}", op_d.text, e_d.text)
1711 } else {
1712 format!("{}({})", op_d.text, e_d.text)
1713 };
1714 Ok(NestedString { text, children: e_d.children, key: None })
1715 }
1716 ExprKind::FieldProj(e, proj) => {
1717 let e_d = e.fmt_nested(cx)?;
1718 let text = if e.is_atom() {
1719 format!("{}.{}", e_d.text, fmt_field_proj(cx, *proj))
1720 } else {
1721 format!("({}).{}", e_d.text, fmt_field_proj(cx, *proj))
1722 };
1723 Ok(NestedString { text, children: e_d.children, key: None })
1724 }
1725 ExprKind::Tuple(flds) => {
1726 let mut texts = vec![];
1727 let mut kidss = vec![];
1728 for e in flds {
1729 let e_d = e.fmt_nested(cx)?;
1730 texts.push(e_d.text);
1731 kidss.push(e_d.children);
1732 }
1733 let text = if let [e] = &texts[..] {
1734 format!("({e},)")
1735 } else {
1736 format!("({})", texts.join(", "))
1737 };
1738 let children = float_children(kidss);
1739 Ok(NestedString { text, children, key: None })
1740 }
1741 ExprKind::Ctor(ctor, flds) => aggregate_nested(cx, ctor, flds, true),
1742 ExprKind::PathProj(e, field) => {
1743 let e_d = e.fmt_nested(cx)?;
1744 let text = if e.is_atom() {
1745 format!("{}.{:?}", e_d.text, field)
1746 } else {
1747 format!("({}).{:?}", e_d.text, field)
1748 };
1749 Ok(NestedString { text, children: e_d.children, key: None })
1750 }
1751 ExprKind::Alias(alias, args) => {
1752 let mut texts = vec![];
1753 let mut kidss = vec![];
1754 for arg in args {
1755 let arg_d = arg.fmt_nested(cx)?;
1756 texts.push(arg_d.text);
1757 kidss.push(arg_d.children);
1758 }
1759 let text = format_cx!(cx, "{:?}({:?})", alias, texts.join(", "));
1760 let children = float_children(kidss);
1761 Ok(NestedString { text, children, key: None })
1762 }
1763 ExprKind::App(func, _, args) => {
1764 let func_d = func.fmt_nested(cx)?;
1765 let mut texts = vec![];
1766 let mut kidss = vec![func_d.children];
1767 for arg in args {
1768 let arg_d = arg.fmt_nested(cx)?;
1769 texts.push(arg_d.text);
1770 kidss.push(arg_d.children);
1771 }
1772 let text = if func.is_atom() {
1773 format!("{}({})", func_d.text, texts.join(", "))
1774 } else {
1775 format!("({})({})", func_d.text, texts.join(", "))
1776 };
1777 let children = float_children(kidss);
1778 Ok(NestedString { text, children, key: None })
1779 }
1780 ExprKind::Abs(lambda) => lambda.fmt_nested(cx),
1781 ExprKind::Let(init, body) => {
1782 nested_with_bound_vars(cx, "let", body.vars(), None, |prefix| {
1784 let body = body.skip_binder_ref().fmt_nested(cx)?;
1785 let text = format!("{:?} {}{}", init, prefix, body.text);
1786 Ok(NestedString { text, children: body.children, key: None })
1787 })
1788 }
1789 ExprKind::BoundedQuant(kind, rng, body) => {
1790 let left = match kind {
1791 fhir::QuantKind::Forall => "∀",
1792 fhir::QuantKind::Exists => "∃",
1793 };
1794 let right = Some(format!(" in {}..{}", rng.start, rng.end));
1795
1796 nested_with_bound_vars(cx, left, body.vars(), right, |all_str| {
1797 let expr_d = body.as_ref().skip_binder().fmt_nested(cx)?;
1798 let text = format!("{}{}", all_str, expr_d.text);
1799 Ok(NestedString { text, children: expr_d.children, key: None })
1800 })
1801 }
1802 ExprKind::ForAll(expr) => {
1803 nested_with_bound_vars(cx, "∀", expr.vars(), None, |all_str| {
1804 let expr_d = expr.as_ref().skip_binder().fmt_nested(cx)?;
1805 let text = format!("{}{}", all_str, expr_d.text);
1806 Ok(NestedString { text, children: expr_d.children, key: None })
1807 })
1808 }
1809 }
1810 }
1811 }
1812}