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