1use super::{
2 AliasReft, AssocItemConstraint, AssocItemConstraintKind, BaseTy, BaseTyKind, Ensures, EnumDef,
3 Expr, ExprKind, FieldDef, FieldExpr, FluxItem, FnDecl, FnOutput, FnSig, ForeignItem,
4 ForeignItemKind, FuncSort, GenericArg, GenericBound, Generics, Impl, ImplAssocReft, ImplItem,
5 ImplItemKind, Item, ItemKind, Lifetime, Lit, OpaqueTy, OwnerNode, Path, PathExpr, PathSegment,
6 PolyFuncSort, PolyTraitRef, QPath, Qualifier, RefineParam, Requires, Sort, SortPath, SpecFunc,
7 StructDef, TraitAssocReft, TraitItem, TraitItemKind, Ty, TyAlias, TyKind, VariantDef,
8 VariantRet, WhereBoundPredicate,
9};
10use crate::fhir::{PrimProp, StructKind};
11
12#[macro_export]
13macro_rules! walk_list {
14 ($visitor: expr, $method: ident, $list: expr $(, $($extra_args: expr),* )?) => {
15 {
16 #[allow(for_loops_over_fallibles)]
17 for elem in $list {
18 $visitor.$method(elem $(, $($extra_args,)* )?)
19 }
20 }
21 }
22}
23
24pub trait Visitor<'v>: Sized {
25 fn visit_flux_item(&mut self, item: &FluxItem<'v>) {
26 walk_flux_item(self, item);
27 }
28
29 fn visit_qualifier(&mut self, qualifier: &Qualifier<'v>) {
30 walk_qualifier(self, qualifier);
31 }
32
33 fn visit_func(&mut self, func: &SpecFunc<'v>) {
34 walk_func(self, func);
35 }
36
37 fn visit_prim_prop(&mut self, prop: &PrimProp<'v>) {
38 walk_prim_prop(self, prop);
39 }
40
41 fn visit_node(&mut self, node: &OwnerNode<'v>) {
42 walk_node(self, node);
43 }
44
45 fn visit_item(&mut self, item: &Item<'v>) {
46 walk_item(self, item);
47 }
48
49 fn visit_trait_item(&mut self, trait_item: &TraitItem<'v>) {
50 walk_trait_item(self, trait_item);
51 }
52
53 fn visit_impl_item(&mut self, impl_item: &ImplItem<'v>) {
54 walk_impl_item(self, impl_item);
55 }
56
57 fn visit_foreign_item(&mut self, foreign_item: &ForeignItem<'v>) {
58 walk_foreign_item(self, foreign_item);
59 }
60
61 fn visit_generics(&mut self, generics: &Generics<'v>) {
62 walk_generics(self, generics);
63 }
64
65 fn visit_where_predicate(&mut self, predicate: &WhereBoundPredicate<'v>) {
66 walk_where_predicate(self, predicate);
67 }
68
69 fn visit_impl(&mut self, impl_: &Impl<'v>) {
70 walk_impl(self, impl_);
71 }
72
73 fn visit_impl_assoc_reft(&mut self, assoc_reft: &ImplAssocReft<'v>) {
74 walk_impl_assoc_reft(self, assoc_reft);
75 }
76
77 fn visit_trait_assoc_reft(&mut self, assoc_reft: &TraitAssocReft<'v>) {
78 walk_trait_assoc_reft(self, assoc_reft);
79 }
80
81 fn visit_struct_def(&mut self, struct_def: &StructDef<'v>) {
82 walk_struct_def(self, struct_def);
83 }
84
85 fn visit_enum_def(&mut self, enum_def: &EnumDef<'v>) {
86 walk_enum_def(self, enum_def);
87 }
88
89 fn visit_variant(&mut self, variant: &VariantDef<'v>) {
90 walk_variant(self, variant);
91 }
92
93 fn visit_field_def(&mut self, field: &FieldDef<'v>) {
94 walk_field_def(self, field);
95 }
96
97 fn visit_variant_ret(&mut self, ret: &VariantRet<'v>) {
98 walk_variant_ret(self, ret);
99 }
100
101 fn visit_ty_alias(&mut self, ty_alias: &TyAlias<'v>) {
102 walk_ty_alias(self, ty_alias);
103 }
104
105 fn visit_opaque_ty(&mut self, opaque_ty: &OpaqueTy<'v>) {
106 walk_opaque_ty(self, opaque_ty);
107 }
108
109 fn visit_generic_bound(&mut self, bound: &GenericBound<'v>) {
110 walk_generic_bound(self, bound);
111 }
112
113 fn visit_poly_trait_ref(&mut self, trait_ref: &PolyTraitRef<'v>) {
114 walk_poly_trait_ref(self, trait_ref);
115 }
116
117 fn visit_fn_sig(&mut self, sig: &FnSig<'v>) {
118 walk_fn_sig(self, sig);
119 }
120
121 fn visit_fn_decl(&mut self, decl: &FnDecl<'v>) {
122 walk_fn_decl(self, decl);
123 }
124
125 fn visit_refine_param(&mut self, param: &RefineParam<'v>) {
126 walk_refine_param(self, param);
127 }
128
129 fn visit_requires(&mut self, requires: &Requires<'v>) {
130 walk_requires(self, requires);
131 }
132
133 fn visit_ensures(&mut self, ensures: &Ensures<'v>) {
134 walk_ensures(self, ensures);
135 }
136
137 fn visit_fn_output(&mut self, output: &FnOutput<'v>) {
138 walk_fn_output(self, output);
139 }
140
141 fn visit_generic_arg(&mut self, arg: &GenericArg<'v>) {
142 walk_generic_arg(self, arg);
143 }
144
145 fn visit_lifetime(&mut self, _lft: &Lifetime) {}
146
147 fn visit_ty(&mut self, ty: &Ty<'v>) {
148 walk_ty(self, ty);
149 }
150
151 fn visit_bty(&mut self, bty: &BaseTy<'v>) {
152 walk_bty(self, bty);
153 }
154
155 fn visit_qpath(&mut self, qpath: &QPath<'v>) {
156 walk_qpath(self, qpath);
157 }
158
159 fn visit_path(&mut self, path: &Path<'v>) {
160 walk_path(self, path);
161 }
162
163 fn visit_path_segment(&mut self, segment: &PathSegment<'v>) {
164 walk_path_segment(self, segment);
165 }
166
167 fn visit_assoc_item_constraint(&mut self, constraint: &AssocItemConstraint<'v>) {
168 walk_assoc_item_constraint(self, constraint);
169 }
170
171 fn visit_sort(&mut self, sort: &Sort<'v>) {
172 walk_sort(self, sort);
173 }
174
175 fn visit_sort_path(&mut self, path: &SortPath<'v>) {
176 walk_sort_path(self, path);
177 }
178
179 fn visit_poly_func_sort(&mut self, func: &PolyFuncSort<'v>) {
180 walk_poly_func_sort(self, func);
181 }
182
183 fn visit_func_sort(&mut self, func: &FuncSort<'v>) {
184 walk_func_sort(self, func);
185 }
186
187 fn visit_expr(&mut self, expr: &Expr<'v>) {
188 walk_expr(self, expr);
189 }
190
191 fn visit_field_expr(&mut self, expr: &FieldExpr<'v>) {
192 walk_field_expr(self, expr);
193 }
194
195 fn visit_alias_reft(&mut self, alias_reft: &AliasReft<'v>) {
196 walk_alias_reft(self, alias_reft);
197 }
198
199 fn visit_literal(&mut self, _lit: &Lit) {}
200
201 fn visit_path_expr(&mut self, _path: &PathExpr<'v>) {}
202}
203
204fn walk_func<'v, V: Visitor<'v>>(vis: &mut V, func: &SpecFunc<'v>) {
205 walk_list!(vis, visit_refine_param, func.args);
206 vis.visit_sort(&func.sort);
207 if let Some(body) = &func.body {
208 vis.visit_expr(body);
209 }
210}
211
212fn walk_prim_prop<'v, V: Visitor<'v>>(vis: &mut V, prop: &PrimProp<'v>) {
213 walk_list!(vis, visit_refine_param, prop.args);
214 vis.visit_expr(&prop.body);
215}
216
217fn walk_qualifier<'v, V: Visitor<'v>>(vis: &mut V, qualifier: &Qualifier<'v>) {
218 walk_list!(vis, visit_refine_param, qualifier.args);
219 vis.visit_expr(&qualifier.expr);
220}
221
222fn walk_flux_item<'v, V: Visitor<'v>>(vis: &mut V, item: &FluxItem<'v>) {
223 match item {
224 FluxItem::Qualifier(qualifier) => {
225 vis.visit_qualifier(qualifier);
226 }
227 FluxItem::Func(func) => {
228 vis.visit_func(func);
229 }
230 FluxItem::PrimProp(prop) => {
231 vis.visit_prim_prop(prop);
232 }
233 }
234}
235
236pub fn walk_impl<'v, V: Visitor<'v>>(vis: &mut V, impl_: &Impl<'v>) {
237 walk_list!(vis, visit_impl_assoc_reft, impl_.assoc_refinements);
238}
239
240pub fn walk_struct_def<'v, V: Visitor<'v>>(vis: &mut V, struct_def: &StructDef<'v>) {
241 walk_list!(vis, visit_refine_param, struct_def.params);
242 walk_list!(vis, visit_expr, struct_def.invariants);
243 if let StructKind::Transparent { fields } = struct_def.kind {
244 walk_list!(vis, visit_field_def, fields);
245 }
246}
247
248pub fn walk_enum_def<'v, V: Visitor<'v>>(vis: &mut V, enum_def: &EnumDef<'v>) {
249 walk_list!(vis, visit_refine_param, enum_def.params);
250 walk_list!(vis, visit_variant, enum_def.variants);
251 walk_list!(vis, visit_expr, enum_def.invariants);
252}
253
254pub fn walk_variant<'v, V: Visitor<'v>>(vis: &mut V, variant: &VariantDef<'v>) {
255 walk_list!(vis, visit_refine_param, variant.params);
256 walk_list!(vis, visit_field_def, variant.fields);
257 vis.visit_variant_ret(&variant.ret);
258}
259
260pub fn walk_field_def<'v, V: Visitor<'v>>(vis: &mut V, field: &FieldDef<'v>) {
261 let FieldDef { ty, lifted: _ } = field;
262 vis.visit_ty(ty);
263}
264
265pub fn walk_variant_ret<'v, V: Visitor<'v>>(vis: &mut V, ret: &VariantRet<'v>) {
266 let VariantRet { idx, enum_id: _ } = ret;
267 vis.visit_expr(idx);
268}
269
270pub fn walk_ty_alias<'v, V: Visitor<'v>>(vis: &mut V, ty_alias: &TyAlias<'v>) {
271 if let Some(index) = &ty_alias.index {
272 vis.visit_refine_param(index);
273 }
274 vis.visit_ty(&ty_alias.ty);
275}
276
277pub fn walk_opaque_ty<'v, V: Visitor<'v>>(vis: &mut V, opaque_ty: &OpaqueTy<'v>) {
278 walk_list!(vis, visit_generic_bound, opaque_ty.bounds);
279}
280
281pub fn walk_generic_bound<'v, V: Visitor<'v>>(vis: &mut V, bound: &GenericBound<'v>) {
282 match bound {
283 GenericBound::Trait(trait_ref) => vis.visit_poly_trait_ref(trait_ref),
284 GenericBound::Outlives(_) => {}
285 }
286}
287
288pub fn walk_poly_trait_ref<'v, V: Visitor<'v>>(vis: &mut V, trait_ref: &PolyTraitRef<'v>) {
289 walk_list!(vis, visit_refine_param, trait_ref.refine_params);
290 vis.visit_path(&trait_ref.trait_ref);
291}
292
293pub fn walk_node<'v, V: Visitor<'v>>(vis: &mut V, node: &OwnerNode<'v>) {
294 match node {
295 OwnerNode::Item(item) => vis.visit_item(item),
296 OwnerNode::TraitItem(trait_item) => vis.visit_trait_item(trait_item),
297 OwnerNode::ImplItem(impl_item) => vis.visit_impl_item(impl_item),
298 OwnerNode::ForeignItem(foreign_item) => vis.visit_foreign_item(foreign_item),
299 }
300}
301
302pub fn walk_item<'v, V: Visitor<'v>>(vis: &mut V, item: &Item<'v>) {
303 vis.visit_generics(&item.generics);
304 match &item.kind {
305 ItemKind::Enum(enum_def) => vis.visit_enum_def(enum_def),
306 ItemKind::Struct(struct_def) => vis.visit_struct_def(struct_def),
307 ItemKind::TyAlias(ty_alias) => vis.visit_ty_alias(ty_alias),
308 ItemKind::Trait(trait_) => {
309 walk_list!(vis, visit_trait_assoc_reft, trait_.assoc_refinements);
310 }
311 ItemKind::Impl(impl_) => vis.visit_impl(impl_),
312 ItemKind::Fn(fn_sig) => vis.visit_fn_sig(fn_sig),
313 ItemKind::Const(info) => {
314 if let Some(expr) = info {
315 vis.visit_expr(expr);
316 }
317 }
318 }
319}
320
321pub fn walk_trait_item<'v, V: Visitor<'v>>(vis: &mut V, trait_item: &TraitItem<'v>) {
322 vis.visit_generics(&trait_item.generics);
323 match &trait_item.kind {
324 TraitItemKind::Fn(fn_sig) => vis.visit_fn_sig(fn_sig),
325 TraitItemKind::Type => {}
326 TraitItemKind::Const => {}
327 }
328}
329
330pub fn walk_impl_item<'v, V: Visitor<'v>>(vis: &mut V, impl_item: &ImplItem<'v>) {
331 vis.visit_generics(&impl_item.generics);
332 match &impl_item.kind {
333 ImplItemKind::Fn(fn_sig) => vis.visit_fn_sig(fn_sig),
334 ImplItemKind::Const => {}
335 ImplItemKind::Type => {}
336 }
337}
338
339pub fn walk_foreign_item<'v, V: Visitor<'v>>(vis: &mut V, impl_item: &ForeignItem<'v>) {
340 match &impl_item.kind {
341 ForeignItemKind::Fn(fn_sig, generics) => {
342 vis.visit_generics(generics);
343 vis.visit_fn_sig(fn_sig);
344 }
345 }
346}
347
348pub fn walk_trait_assoc_reft<'v, V: Visitor<'v>>(vis: &mut V, assoc_reft: &TraitAssocReft<'v>) {
349 walk_list!(vis, visit_refine_param, assoc_reft.params);
350 vis.visit_sort(&assoc_reft.output);
351 if let Some(expr) = &assoc_reft.body {
352 vis.visit_expr(expr);
353 }
354}
355
356pub fn walk_impl_assoc_reft<'v, V: Visitor<'v>>(vis: &mut V, assoc_reft: &ImplAssocReft<'v>) {
357 walk_list!(vis, visit_refine_param, assoc_reft.params);
358 vis.visit_sort(&assoc_reft.output);
359 vis.visit_expr(&assoc_reft.body);
360}
361
362pub fn walk_generics<'v, V: Visitor<'v>>(vis: &mut V, generics: &Generics<'v>) {
363 walk_list!(vis, visit_refine_param, generics.refinement_params);
364 if let Some(predicates) = generics.predicates {
365 walk_list!(vis, visit_where_predicate, predicates);
366 }
367}
368
369pub fn walk_where_predicate<'v, V: Visitor<'v>>(vis: &mut V, predicate: &WhereBoundPredicate<'v>) {
370 vis.visit_ty(&predicate.bounded_ty);
371 walk_list!(vis, visit_generic_bound, predicate.bounds);
372}
373
374pub fn walk_fn_sig<'v, V: Visitor<'v>>(vis: &mut V, sig: &FnSig<'v>) {
375 vis.visit_fn_decl(sig.decl);
376}
377
378pub fn walk_fn_decl<'v, V: Visitor<'v>>(vis: &mut V, decl: &FnDecl<'v>) {
379 walk_list!(vis, visit_requires, decl.requires);
380 walk_list!(vis, visit_ty, decl.inputs);
381 vis.visit_fn_output(&decl.output);
382}
383
384pub fn walk_refine_param<'v, V: Visitor<'v>>(vis: &mut V, param: &RefineParam<'v>) {
385 vis.visit_sort(¶m.sort);
386}
387
388pub fn walk_requires<'v, V: Visitor<'v>>(vis: &mut V, requires: &Requires<'v>) {
389 walk_list!(vis, visit_refine_param, requires.params);
390 vis.visit_expr(&requires.pred);
391}
392
393pub fn walk_ensures<'v, V: Visitor<'v>>(vis: &mut V, constraint: &Ensures<'v>) {
394 match constraint {
395 Ensures::Type(loc, ty) => {
396 vis.visit_path_expr(loc);
397 vis.visit_ty(ty);
398 }
399 Ensures::Pred(pred) => {
400 vis.visit_expr(pred);
401 }
402 }
403}
404
405pub fn walk_fn_output<'v, V: Visitor<'v>>(vis: &mut V, output: &FnOutput<'v>) {
406 walk_list!(vis, visit_refine_param, output.params);
407 vis.visit_ty(&output.ret);
408 walk_list!(vis, visit_ensures, output.ensures);
409}
410
411pub fn walk_generic_arg<'v, V: Visitor<'v>>(vis: &mut V, arg: &GenericArg<'v>) {
412 match arg {
413 GenericArg::Lifetime(lft) => vis.visit_lifetime(lft),
414 GenericArg::Type(ty) => vis.visit_ty(ty),
415 GenericArg::Const(_) | GenericArg::Infer => {}
416 }
417}
418
419pub fn walk_ty<'v, V: Visitor<'v>>(vis: &mut V, ty: &Ty<'v>) {
420 match ty.kind {
421 TyKind::BaseTy(bty) => vis.visit_bty(&bty),
422 TyKind::Indexed(bty, idx) => {
423 vis.visit_bty(&bty);
424 vis.visit_expr(&idx);
425 }
426 TyKind::Exists(params, ty) => {
427 walk_list!(vis, visit_refine_param, params);
428 vis.visit_ty(ty);
429 }
430 TyKind::Constr(pred, ty) => {
431 vis.visit_expr(&pred);
432 vis.visit_ty(ty);
433 }
434 TyKind::StrgRef(lft, loc, ty) => {
435 vis.visit_lifetime(&lft);
436 vis.visit_path_expr(loc);
437 vis.visit_ty(ty);
438 }
439 TyKind::Ref(lft, mty) => {
440 vis.visit_lifetime(&lft);
441 vis.visit_ty(mty.ty);
442 }
443 TyKind::BareFn(bare_fn) => vis.visit_fn_decl(bare_fn.decl),
444 TyKind::Tuple(tys) => {
445 walk_list!(vis, visit_ty, tys);
446 }
447 TyKind::Array(ty, _len) => {
448 vis.visit_ty(ty);
449 }
450 TyKind::RawPtr(ty, _mtblt) => {
451 vis.visit_ty(ty);
452 }
453 TyKind::OpaqueDef(opaque_ty) => {
454 vis.visit_opaque_ty(opaque_ty);
455 }
456 TyKind::TraitObject(poly_traits, lft, _) => {
457 walk_list!(vis, visit_poly_trait_ref, poly_traits);
458 vis.visit_lifetime(&lft);
459 }
460 TyKind::Never | TyKind::Infer | TyKind::Err(_) => {}
461 }
462}
463
464pub fn walk_bty<'v, V: Visitor<'v>>(vis: &mut V, bty: &BaseTy<'v>) {
465 match &bty.kind {
466 BaseTyKind::Path(path) => vis.visit_qpath(path),
467 BaseTyKind::Slice(ty) => vis.visit_ty(ty),
468 BaseTyKind::Err(_) => {}
469 }
470}
471
472pub fn walk_qpath<'v, V: Visitor<'v>>(vis: &mut V, qpath: &QPath<'v>) {
473 match qpath {
474 QPath::Resolved(qself, path) => {
475 if let Some(self_ty) = qself {
476 vis.visit_ty(self_ty);
477 }
478 vis.visit_path(path);
479 }
480 QPath::TypeRelative(qself, assoc) => {
481 vis.visit_ty(qself);
482 vis.visit_path_segment(assoc);
483 }
484 }
485}
486
487pub fn walk_path<'v, V: Visitor<'v>>(vis: &mut V, path: &Path<'v>) {
488 walk_list!(vis, visit_path_segment, path.segments);
489 walk_list!(vis, visit_expr, path.refine);
490}
491
492pub fn walk_path_segment<'v, V: Visitor<'v>>(vis: &mut V, segment: &PathSegment<'v>) {
493 walk_list!(vis, visit_generic_arg, segment.args);
494 walk_list!(vis, visit_assoc_item_constraint, segment.constraints);
495}
496
497pub fn walk_assoc_item_constraint<'v, V: Visitor<'v>>(
498 vis: &mut V,
499 constraint: &AssocItemConstraint<'v>,
500) {
501 match &constraint.kind {
502 AssocItemConstraintKind::Equality { term } => {
503 vis.visit_ty(term);
504 }
505 }
506}
507
508pub fn walk_sort<'v, V: Visitor<'v>>(vis: &mut V, sort: &Sort<'v>) {
509 match sort {
510 Sort::Path(path) => vis.visit_sort_path(path),
511 Sort::Func(func) => vis.visit_poly_func_sort(func),
512 Sort::SortOf(bty) => vis.visit_bty(bty),
513 Sort::Loc | Sort::BitVec(_) | Sort::Infer | Sort::Err(_) => {}
514 }
515}
516
517pub fn walk_sort_path<'v, V: Visitor<'v>>(vis: &mut V, path: &SortPath<'v>) {
518 walk_list!(vis, visit_sort, path.args);
519}
520
521pub fn walk_poly_func_sort<'v, V: Visitor<'v>>(vis: &mut V, func: &PolyFuncSort<'v>) {
522 let PolyFuncSort { params: _, fsort } = func;
523 vis.visit_func_sort(fsort);
524}
525
526pub fn walk_func_sort<'v, V: Visitor<'v>>(vis: &mut V, func: &FuncSort<'v>) {
527 walk_list!(vis, visit_sort, func.inputs_and_output);
528}
529
530pub fn walk_alias_reft<'v, V: Visitor<'v>>(vis: &mut V, alias: &AliasReft<'v>) {
531 vis.visit_ty(alias.qself);
532 vis.visit_path(&alias.path);
533}
534
535pub fn walk_field_expr<'v, V: Visitor<'v>>(vis: &mut V, expr: &FieldExpr<'v>) {
536 vis.visit_expr(&expr.expr);
537}
538
539pub fn walk_expr<'v, V: Visitor<'v>>(vis: &mut V, expr: &Expr<'v>) {
540 match expr.kind {
541 ExprKind::Var(path, _) => vis.visit_path_expr(&path),
542 ExprKind::Dot(base, _fld) => {
543 vis.visit_expr(base);
544 }
545 ExprKind::Literal(lit) => vis.visit_literal(&lit),
546 ExprKind::BinaryOp(_op, e1, e2) => {
547 vis.visit_expr(e1);
548 vis.visit_expr(e2);
549 }
550 ExprKind::PrimApp(_op, e1, e2) => {
551 vis.visit_expr(e1);
552 vis.visit_expr(e2);
553 }
554 ExprKind::UnaryOp(_op, e) => vis.visit_expr(e),
555 ExprKind::App(_func, args) => {
556 walk_list!(vis, visit_expr, args);
557 }
558 ExprKind::Alias(alias_reft, args) => {
559 vis.visit_alias_reft(&alias_reft);
560 walk_list!(vis, visit_expr, args);
561 }
562 ExprKind::IfThenElse(e1, e2, e3) => {
563 vis.visit_expr(e1);
564 vis.visit_expr(e2);
565 vis.visit_expr(e3);
566 }
567 ExprKind::Abs(refine_params, body) => {
568 walk_list!(vis, visit_refine_param, refine_params);
569 vis.visit_expr(body);
570 }
571 ExprKind::Record(fields) => {
572 walk_list!(vis, visit_expr, fields);
573 }
574 ExprKind::Constructor(path, exprs, spread) => {
575 if let Some(path) = path {
576 vis.visit_path_expr(&path);
577 }
578 walk_list!(vis, visit_field_expr, exprs);
579 if let Some(s) = spread {
580 vis.visit_expr(&s.expr);
581 }
582 }
583 ExprKind::BoundedQuant(_, param, _, expr) => {
584 vis.visit_refine_param(¶m);
585 vis.visit_expr(expr);
586 }
587 ExprKind::Block(decls, body) => {
588 for decl in decls {
589 vis.visit_expr(&decl.init);
590 vis.visit_refine_param(&decl.param);
591 }
592 vis.visit_expr(body);
593 }
594 ExprKind::Err(_) => {}
595 }
596}