1use rustc_span::symbol::Ident;
9
10use super::{
11 Async, BaseSort, BaseTy, BaseTyKind, ConstArg, ConstArgKind, ConstantInfo, ConstructorArg,
12 Ensures, EnumDef, Expr, ExprKind, ExprPath, ExprPathSegment, FieldExpr, FnInput, FnOutput,
13 FnRetTy, FnSig, GenericArg, GenericArgKind, GenericParam, Generics, Impl, ImplAssocReft,
14 Indices, ItemKind, Lit, Path, PathSegment, Qualifier, RefineArg, RefineParam, Requires, Sort,
15 SortPath, SpecFunc, StructDef, Trait, TraitAssocReft, TraitRef, Ty, TyAlias, TyKind,
16 UseTreeKind, VariantDef, VariantRet, WhereBoundPredicate,
17};
18use crate::surface::{
19 Axiom, FluxItem, ImplItemFn, Item, PrimOpProp, SortDecl, TraitItemFn, UseTree,
20};
21
22#[macro_export]
23macro_rules! walk_list {
24 ($visitor: expr, $method: ident, $list: expr $(, $($extra_args: expr),* )?) => {
25 {
26 #[allow(for_loops_over_fallibles)]
27 for elem in $list {
28 $visitor.$method(elem $(, $($extra_args,)* )?)
29 }
30 }
31 }
32}
33
34pub trait Visitor<'v>: Sized {
35 fn visit_flux_item(&mut self, item: &'v FluxItem) {
36 walk_flux_item(self, item);
37 }
38
39 fn visit_qualifier(&mut self, qualifier: &'v Qualifier) {
40 walk_qualifier(self, qualifier);
41 }
42
43 fn visit_sort_decl(&mut self, sort_decl: &'v SortDecl) {
44 walk_sort_decl(self, sort_decl);
45 }
46
47 fn visit_defn(&mut self, defn: &'v SpecFunc) {
48 walk_defn(self, defn);
49 }
50
51 fn visit_primop_prop(&mut self, prop: &'v PrimOpProp) {
52 walk_primop_prop(self, prop);
53 }
54
55 fn visit_axiom(&mut self, axiom: &'v Axiom) {
56 walk_axiom(self, axiom);
57 }
58
59 fn visit_refine_param(&mut self, param: &'v RefineParam) {
60 walk_refine_param(self, param);
61 }
62
63 fn visit_generic_param(&mut self, param: &'v GenericParam) {
64 walk_generic_param(self, param);
65 }
66
67 fn visit_sort(&mut self, sort: &'v Sort) {
68 walk_sort(self, sort);
69 }
70
71 fn visit_item(&mut self, item: &'v Item) {
72 walk_item(self, item);
73 }
74
75 fn visit_trait_item(&mut self, item: &'v TraitItemFn) {
76 walk_trait_item(self, item);
77 }
78
79 fn visit_impl_item(&mut self, item: &'v ImplItemFn) {
80 walk_impl_item(self, item);
81 }
82
83 fn visit_trait(&mut self, trait_: &'v Trait) {
84 walk_trait(self, trait_);
85 }
86
87 fn visit_trait_assoc_reft(&mut self, assoc_reft: &'v TraitAssocReft) {
88 walk_trait_assoc_reft(self, assoc_reft);
89 }
90
91 fn visit_impl(&mut self, impl_: &'v Impl) {
92 walk_impl(self, impl_);
93 }
94
95 fn visit_impl_assoc_reft(&mut self, assoc_reft: &'v ImplAssocReft) {
96 walk_impl_assoc_reft(self, assoc_reft);
97 }
98
99 fn visit_trait_ref(&mut self, trait_ref: &'v TraitRef) {
100 walk_trait_ref(self, trait_ref);
101 }
102
103 fn visit_base_sort(&mut self, bsort: &'v BaseSort) {
104 walk_base_sort(self, bsort);
105 }
106
107 fn visit_sort_path(&mut self, path: &'v SortPath) {
108 walk_sort_path(self, path);
109 }
110
111 fn visit_ty_alias(&mut self, ty_alias: &'v TyAlias) {
112 walk_ty_alias(self, ty_alias);
113 }
114
115 fn visit_struct_def(&mut self, struct_def: &'v StructDef) {
116 walk_struct_def(self, struct_def);
117 }
118
119 fn visit_constant(&mut self, _constant: &'v ConstantInfo) {
120 walk_constant(self, _constant);
121 }
122
123 fn visit_enum_def(&mut self, enum_def: &'v EnumDef) {
124 walk_enum_def(self, enum_def);
125 }
126
127 fn visit_variant(&mut self, variant: &'v VariantDef) {
128 walk_variant(self, variant);
129 }
130
131 fn visit_variant_ret(&mut self, ret: &'v VariantRet) {
132 walk_variant_ret(self, ret);
133 }
134
135 fn visit_fn_sig(&mut self, fn_sig: &'v FnSig) {
136 walk_fn_sig(self, fn_sig);
137 }
138
139 fn visit_requires(&mut self, requires: &'v Requires) {
140 walk_requires(self, requires);
141 }
142
143 fn visit_fn_output(&mut self, fn_output: &'v FnOutput) {
144 walk_fn_output(self, fn_output);
145 }
146
147 fn visit_async(&mut self, _asyncness: &'v Async) {}
148
149 fn visit_generics(&mut self, generics: &'v Generics) {
150 walk_generics(self, generics);
151 }
152
153 fn visit_fn_input(&mut self, input: &'v FnInput) {
154 walk_fn_input(self, input);
155 }
156
157 fn visit_fn_ret_ty(&mut self, fn_ret_ty: &'v FnRetTy) {
158 walk_fn_ret_ty(self, fn_ret_ty);
159 }
160
161 fn visit_ensures(&mut self, ensures: &'v Ensures) {
162 walk_ensures(self, ensures);
163 }
164
165 fn visit_where_predicate(&mut self, predicate: &'v WhereBoundPredicate) {
166 walk_where_predicate(self, predicate);
167 }
168
169 fn visit_generic_arg(&mut self, arg: &'v GenericArg) {
170 walk_generic_arg(self, arg);
171 }
172
173 fn visit_refine_arg(&mut self, arg: &'v RefineArg) {
174 walk_refine_arg(self, arg);
175 }
176
177 fn visit_indices(&mut self, indices: &'v Indices) {
178 walk_indices(self, indices);
179 }
180
181 fn visit_ty(&mut self, ty: &'v Ty) {
182 walk_ty(self, ty);
183 }
184
185 fn visit_const_arg(&mut self, const_arg: &'v ConstArg) {
186 walk_const_arg(self, const_arg);
187 }
188
189 fn visit_bty(&mut self, bty: &'v BaseTy) {
190 walk_bty(self, bty);
191 }
192
193 fn visit_path(&mut self, path: &'v Path) {
194 walk_path(self, path);
195 }
196
197 fn visit_path_segment(&mut self, segment: &'v PathSegment) {
198 walk_path_segment(self, segment);
199 }
200
201 fn visit_expr(&mut self, expr: &'v Expr) {
202 walk_expr(self, expr);
203 }
204
205 fn visit_constructor_args(&mut self, expr: &'v ConstructorArg) {
206 match expr {
207 ConstructorArg::FieldExpr(field_expr) => walk_field_expr(self, field_expr),
208 ConstructorArg::Spread(spread) => self.visit_expr(&spread.expr),
209 }
210 }
211
212 fn visit_path_expr(&mut self, qpath: &'v ExprPath) {
213 walk_path_expr(self, qpath);
214 }
215
216 fn visit_path_expr_segment(&mut self, segment: &'v ExprPathSegment) {
217 walk_path_expr_segment(self, segment);
218 }
219
220 fn visit_ident(&mut self, _ident: Ident) {}
221
222 fn visit_literal(&mut self, _lit: Lit) {}
223}
224
225pub fn walk_flux_item<'v, V: Visitor<'v>>(vis: &mut V, item: &'v FluxItem) {
226 match item {
227 FluxItem::Qualifier(qualifier) => vis.visit_qualifier(qualifier),
228 FluxItem::FuncDef(spec_func) => vis.visit_defn(spec_func),
229 FluxItem::SortDecl(sort_decl) => vis.visit_sort_decl(sort_decl),
230 FluxItem::PrimOpProp(prim_op_prop) => vis.visit_primop_prop(prim_op_prop),
231 FluxItem::Axiom(axiom) => vis.visit_axiom(axiom),
232 FluxItem::Use(use_tree) => walk_use_tree(vis, use_tree),
233 }
234}
235
236pub fn walk_use_tree<'v, V: Visitor<'v>>(vis: &mut V, use_tree: &'v UseTree) {
237 vis.visit_path_expr(&use_tree.prefix);
238 match &use_tree.kind {
239 UseTreeKind::Simple => {}
240 UseTreeKind::Nested(items) => {
241 for item in items {
242 walk_use_tree(vis, item);
243 }
244 }
245 }
246}
247
248pub fn walk_qualifier<'v, V: Visitor<'v>>(vis: &mut V, qualifier: &'v Qualifier) {
249 vis.visit_ident(qualifier.name);
250 walk_list!(vis, visit_refine_param, &qualifier.params);
251 vis.visit_expr(&qualifier.expr);
252}
253
254pub fn walk_sort_decl<'v, V: Visitor<'v>>(vis: &mut V, sort_decl: &'v SortDecl) {
255 vis.visit_ident(sort_decl.name);
256 walk_list!(vis, visit_ident, sort_decl.sort_vars.iter().copied());
257}
258
259pub fn walk_defn<'v, V: Visitor<'v>>(vis: &mut V, defn: &'v SpecFunc) {
260 vis.visit_ident(defn.name);
261 walk_list!(vis, visit_ident, defn.sort_vars.iter().copied());
262 walk_list!(vis, visit_refine_param, &defn.params);
263 vis.visit_sort(&defn.output);
264 if let Some(body) = &defn.body {
265 vis.visit_expr(body);
266 }
267}
268
269pub fn walk_primop_prop<'v, V: Visitor<'v>>(vis: &mut V, prop: &'v PrimOpProp) {
270 vis.visit_ident(prop.name);
271 walk_list!(vis, visit_refine_param, &prop.params);
272 vis.visit_expr(&prop.body);
273}
274
275pub fn walk_axiom<'v, V: Visitor<'v>>(vis: &mut V, axiom: &'v Axiom) {
276 vis.visit_ident(axiom.name);
277 walk_list!(vis, visit_refine_param, &axiom.params);
278 vis.visit_expr(&axiom.body);
279}
280
281pub fn walk_requires<'v, V: Visitor<'v>>(vis: &mut V, requires: &'v Requires) {
282 walk_list!(vis, visit_refine_param, &requires.params);
283 vis.visit_expr(&requires.pred);
284}
285
286pub fn walk_refine_param<'v, V: Visitor<'v>>(vis: &mut V, param: &'v RefineParam) {
287 vis.visit_ident(param.ident);
288 vis.visit_sort(¶m.sort);
289}
290
291pub fn walk_generic_param<'v, V: Visitor<'v>>(vis: &mut V, param: &'v GenericParam) {
292 vis.visit_ident(param.name);
293}
294
295pub fn walk_sort<'v, V: Visitor<'v>>(vis: &mut V, sort: &'v Sort) {
296 match sort {
297 Sort::Base(bsort) => vis.visit_base_sort(bsort),
298 Sort::Func { inputs, output } => {
299 walk_list!(vis, visit_base_sort, inputs);
300 vis.visit_base_sort(output);
301 }
302 Sort::Infer => {}
303 }
304}
305
306pub fn walk_item<'v, V: Visitor<'v>>(vis: &mut V, item: &'v Item) {
307 match &item.kind {
308 ItemKind::Fn(fn_sig) => {
309 if let Some(fn_sig) = fn_sig {
310 vis.visit_fn_sig(fn_sig);
311 }
312 }
313 ItemKind::Struct(struct_def) => vis.visit_struct_def(struct_def),
314 ItemKind::Enum(enum_def) => vis.visit_enum_def(enum_def),
315 ItemKind::Trait(trait_) => vis.visit_trait(trait_),
316 ItemKind::Impl(impl_) => vis.visit_impl(impl_),
317 ItemKind::Const(cst) => vis.visit_constant(cst),
318 ItemKind::Static(static_info) => vis.visit_ty(&static_info.ty),
319 ItemKind::TyAlias(ty_alias) => vis.visit_ty_alias(ty_alias),
320 ItemKind::Mod => {}
321 }
322}
323
324pub fn walk_trait_item<'v, V: Visitor<'v>>(vis: &mut V, item: &'v TraitItemFn) {
325 if let Some(fn_sig) = item.sig.as_ref() {
326 vis.visit_fn_sig(fn_sig);
327 }
328}
329
330pub fn walk_impl_item<'v, V: Visitor<'v>>(vis: &mut V, item: &'v ImplItemFn) {
331 if let Some(fn_sig) = item.sig.as_ref() {
332 vis.visit_fn_sig(fn_sig);
333 }
334}
335
336pub fn walk_trait<'v, V: Visitor<'v>>(vis: &mut V, trait_: &'v Trait) {
337 if let Some(generics) = &trait_.generics {
338 vis.visit_generics(generics);
339 }
340 walk_list!(vis, visit_trait_assoc_reft, &trait_.assoc_refinements);
341}
342
343pub fn walk_trait_assoc_reft<'v, V: Visitor<'v>>(vis: &mut V, assoc_reft: &'v TraitAssocReft) {
344 vis.visit_ident(assoc_reft.name);
345 walk_list!(vis, visit_refine_param, &assoc_reft.params);
346 vis.visit_base_sort(&assoc_reft.output);
347 if let Some(expr) = &assoc_reft.body {
348 vis.visit_expr(expr);
349 }
350}
351
352pub fn walk_impl<'v, V: Visitor<'v>>(vis: &mut V, impl_: &'v Impl) {
353 if let Some(generics) = &impl_.generics {
354 vis.visit_generics(generics);
355 }
356 walk_list!(vis, visit_impl_assoc_reft, &impl_.assoc_refinements);
357}
358
359pub fn walk_impl_assoc_reft<'v, V: Visitor<'v>>(vis: &mut V, assoc_reft: &'v ImplAssocReft) {
360 vis.visit_ident(assoc_reft.name);
361 walk_list!(vis, visit_refine_param, &assoc_reft.params);
362 vis.visit_expr(&assoc_reft.body);
363 vis.visit_base_sort(&assoc_reft.output);
364}
365
366pub fn walk_trait_ref<'v, V: Visitor<'v>>(vis: &mut V, trait_ref: &'v TraitRef) {
367 vis.visit_path(&trait_ref.path);
368}
369
370pub fn walk_base_sort<'v, V: Visitor<'v>>(vis: &mut V, bsort: &'v BaseSort) {
371 match bsort {
372 BaseSort::BitVec(_len) => {}
373 BaseSort::Path(path) => vis.visit_sort_path(path),
374 BaseSort::SortOf(qself, path) => {
375 vis.visit_ty(qself);
376 vis.visit_path(path);
377 }
378 BaseSort::Tuple(sorts) => {
379 walk_list!(vis, visit_base_sort, sorts);
380 }
381 }
382}
383
384pub fn walk_sort_path<'v, V: Visitor<'v>>(vis: &mut V, path: &'v SortPath) {
385 walk_list!(vis, visit_ident, path.segments.iter().copied());
386 walk_list!(vis, visit_base_sort, &path.args);
387}
388
389pub fn walk_ty_alias<'v, V: Visitor<'v>>(vis: &mut V, ty_alias: &'v TyAlias) {
390 vis.visit_ident(ty_alias.ident);
391 vis.visit_generics(&ty_alias.generics);
392 walk_list!(vis, visit_refine_param, &ty_alias.params);
393 if let Some(index) = &ty_alias.index {
394 vis.visit_refine_param(index);
395 }
396 vis.visit_ty(&ty_alias.ty);
397}
398pub fn walk_constant<'v, V: Visitor<'v>>(vis: &mut V, constant_info: &'v ConstantInfo) {
399 if let Some(expr) = &constant_info.expr {
400 vis.visit_expr(expr);
401 }
402}
403
404pub fn walk_struct_def<'v, V: Visitor<'v>>(vis: &mut V, struct_def: &'v StructDef) {
405 if let Some(generics) = &struct_def.generics {
406 vis.visit_generics(generics);
407 }
408 if let Some(refined_by) = &struct_def.refined_by {
409 walk_list!(vis, visit_refine_param, refined_by);
410 }
411 walk_list!(vis, visit_expr, &struct_def.invariants);
412 struct_def.fields.iter().flatten().for_each(|field| {
413 vis.visit_ty(field);
414 });
415}
416
417pub fn walk_enum_def<'v, V: Visitor<'v>>(vis: &mut V, enum_def: &'v EnumDef) {
418 if let Some(refined_by) = &enum_def.refined_by {
419 walk_list!(vis, visit_refine_param, refined_by);
420 }
421 walk_list!(vis, visit_expr, &enum_def.invariants);
422 enum_def
423 .variants
424 .iter()
425 .flatten()
426 .for_each(|variant| vis.visit_variant(variant));
427}
428
429pub fn walk_variant<'v, V: Visitor<'v>>(vis: &mut V, variant: &'v VariantDef) {
430 walk_list!(vis, visit_ty, &variant.fields);
431 if let Some(ret) = &variant.ret {
432 vis.visit_variant_ret(ret);
433 }
434}
435
436pub fn walk_fn_trait_ref<'v, V: Visitor<'v>>(
437 vis: &mut V,
438 in_arg: &'v GenericArg,
439 out_arg: &'v GenericArg,
440) {
441 vis.visit_generic_arg(in_arg);
442 vis.visit_generic_arg(out_arg);
443}
444
445pub fn walk_variant_ret<'v, V: Visitor<'v>>(vis: &mut V, ret: &'v VariantRet) {
446 vis.visit_path(&ret.path);
447 vis.visit_indices(&ret.indices);
448}
449
450pub fn walk_fn_sig<'v, V: Visitor<'v>>(vis: &mut V, fn_sig: &'v FnSig) {
457 vis.visit_async(&fn_sig.asyncness);
458
459 walk_list!(vis, visit_refine_param, &fn_sig.params);
460 vis.visit_generics(&fn_sig.generics);
461 walk_list!(vis, visit_requires, &fn_sig.requires);
462 walk_list!(vis, visit_fn_input, &fn_sig.inputs);
463 if let Some(no_panic_expr) = &fn_sig.no_panic {
464 vis.visit_expr(no_panic_expr);
465 }
466 vis.visit_fn_output(&fn_sig.output);
467}
468
469pub fn walk_fn_output<'v, V: Visitor<'v>>(vis: &mut V, fn_output: &'v FnOutput) {
470 vis.visit_fn_ret_ty(&fn_output.returns);
471 walk_list!(vis, visit_ensures, &fn_output.ensures);
472}
473
474pub fn walk_generics<'v, V: Visitor<'v>>(vis: &mut V, generics: &'v Generics) {
475 walk_list!(vis, visit_generic_param, &generics.params);
476 if let Some(predicates) = &generics.predicates {
477 walk_list!(vis, visit_where_predicate, predicates);
478 }
479}
480
481pub fn walk_fn_input<'v, V: Visitor<'v>>(vis: &mut V, arg: &'v FnInput) {
482 match arg {
483 FnInput::Constr(bind, path, pred, _node_id) => {
484 vis.visit_ident(*bind);
485 vis.visit_path(path);
486 vis.visit_expr(pred);
487 }
488 FnInput::StrgRef(bind, ty, _node_id) => {
489 vis.visit_ident(*bind);
490 vis.visit_ty(ty);
491 }
492 FnInput::Ty(bind, ty, _node_id) => {
493 if let Some(bind) = bind {
494 vis.visit_ident(*bind);
495 }
496 vis.visit_ty(ty);
497 }
498 }
499}
500
501pub fn walk_fn_ret_ty<'v, V: Visitor<'v>>(vis: &mut V, fn_ret_ty: &'v FnRetTy) {
502 match fn_ret_ty {
503 FnRetTy::Default(_span) => {}
504 FnRetTy::Ty(ty) => vis.visit_ty(ty),
505 }
506}
507
508pub fn walk_ensures<'v, V: Visitor<'v>>(vis: &mut V, ensures: &'v Ensures) {
509 match ensures {
510 Ensures::Type(bind, ty, _node_id) => {
511 vis.visit_ident(*bind);
512 vis.visit_ty(ty);
513 }
514 Ensures::Pred(pred) => {
515 vis.visit_expr(pred);
516 }
517 }
518}
519
520pub fn walk_where_predicate<'v, V: Visitor<'v>>(vis: &mut V, predicate: &'v WhereBoundPredicate) {
521 vis.visit_ty(&predicate.bounded_ty);
522 walk_list!(vis, visit_trait_ref, &predicate.bounds);
523}
524
525pub fn walk_generic_arg<'v, V: Visitor<'v>>(vis: &mut V, arg: &'v GenericArg) {
526 match &arg.kind {
527 GenericArgKind::Type(ty) => {
528 vis.visit_ty(ty);
529 }
530 GenericArgKind::Constraint(ident, ty) => {
531 vis.visit_ident(*ident);
532 vis.visit_ty(ty);
533 }
534 }
535}
536
537pub fn walk_refine_arg<'v, V: Visitor<'v>>(vis: &mut V, arg: &'v RefineArg) {
538 match arg {
539 RefineArg::Bind(ident, _kind, _span, _node_id) => {
540 vis.visit_ident(*ident);
541 }
542 RefineArg::Expr(e) => {
543 vis.visit_expr(e);
544 }
545 RefineArg::Abs(params, e, _node_id, _span) => {
546 walk_list!(vis, visit_refine_param, params);
547 vis.visit_expr(e);
548 }
549 }
550}
551
552pub fn walk_indices<'v, V: Visitor<'v>>(vis: &mut V, indices: &'v Indices) {
553 walk_list!(vis, visit_refine_arg, &indices.indices);
554}
555
556pub fn walk_ty<'v, V: Visitor<'v>>(vis: &mut V, ty: &'v Ty) {
557 match &ty.kind {
558 TyKind::Base(bty) => vis.visit_bty(bty),
559 TyKind::Indexed { bty, indices } => {
560 vis.visit_indices(indices);
561 vis.visit_bty(bty);
562 }
563
564 TyKind::Exists { bind, bty, pred } => {
565 vis.visit_ident(*bind);
566 vis.visit_bty(bty);
567 vis.visit_expr(pred);
568 }
569 TyKind::GeneralExists { params, ty, pred } => {
570 walk_list!(vis, visit_refine_param, params);
571 vis.visit_ty(ty);
572 if let Some(pred) = pred {
573 vis.visit_expr(pred);
574 }
575 }
576 TyKind::Ref(_mutbl, ty) => {
577 vis.visit_ty(ty);
578 }
579 TyKind::Constr(pred, ty) => {
580 vis.visit_expr(pred);
581 vis.visit_ty(ty);
582 }
583 TyKind::Tuple(tys) => {
584 walk_list!(vis, visit_ty, tys);
585 }
586 TyKind::Array(ty, len) => {
587 vis.visit_const_arg(len);
588 vis.visit_ty(ty);
589 }
590 TyKind::BareFn(bare_fn) => {
591 walk_list!(vis, visit_ty, &bare_fn.inputs);
592 vis.visit_fn_ret_ty(&bare_fn.output);
593 }
594 TyKind::ImplTrait(_node_id, trait_ref) => {
595 walk_list!(vis, visit_trait_ref, trait_ref);
596 }
597 TyKind::Hole => {}
598 }
599}
600
601pub fn walk_const_arg<'v, V: Visitor<'v>>(vis: &mut V, const_arg: &'v ConstArg) {
602 if let ConstArgKind::Path(path) = &const_arg.kind {
603 vis.visit_path(path);
604 }
605}
606
607pub fn walk_bty<'v, V: Visitor<'v>>(vis: &mut V, bty: &'v BaseTy) {
608 match &bty.kind {
609 BaseTyKind::Path(qself, path) => {
610 if let Some(qself) = qself {
611 vis.visit_ty(qself);
612 }
613 vis.visit_path(path);
614 }
615 BaseTyKind::Slice(ty) => vis.visit_ty(ty),
616 BaseTyKind::Ptr(_, ty) => vis.visit_ty(ty),
617 }
618}
619
620pub fn walk_path<'v, V: Visitor<'v>>(vis: &mut V, path: &'v Path) {
621 walk_list!(vis, visit_path_segment, &path.segments);
622 walk_list!(vis, visit_refine_arg, &path.refine);
623}
624
625pub fn walk_path_segment<'v, V: Visitor<'v>>(vis: &mut V, segment: &'v PathSegment) {
626 vis.visit_ident(segment.ident);
627 walk_list!(vis, visit_generic_arg, &segment.args);
628}
629
630pub fn walk_field_expr<'v, V: Visitor<'v>>(vis: &mut V, expr: &'v FieldExpr) {
631 vis.visit_ident(expr.ident);
632 vis.visit_refine_arg(&expr.expr);
633}
634
635pub fn walk_expr<'v, V: Visitor<'v>>(vis: &mut V, expr: &'v Expr) {
636 match &expr.kind {
637 ExprKind::Path(qpath) => vis.visit_path_expr(qpath),
638 ExprKind::Dot(base, fld) => {
639 vis.visit_expr(base);
640 vis.visit_ident(*fld);
641 }
642 ExprKind::Literal(lit) => {
643 vis.visit_literal(*lit);
644 }
645 ExprKind::BinaryOp(_bin_op, deref!(exprs)) => {
646 walk_list!(vis, visit_expr, exprs);
647 }
648 ExprKind::UnaryOp(_un_op, e) => {
649 vis.visit_expr(e);
650 }
651 ExprKind::PrimUIF(_) => {}
652 ExprKind::Call(callee, args) => {
653 vis.visit_expr(callee);
654 walk_list!(vis, visit_expr, args);
655 }
656 ExprKind::AssocReft(qself, path, name) => {
657 vis.visit_ty(qself);
658 vis.visit_path(path);
659 vis.visit_ident(*name);
660 }
661 ExprKind::IfThenElse(deref!(exprs)) => {
662 walk_list!(vis, visit_expr, exprs);
663 }
664 ExprKind::Constructor(path, exprs) => {
665 if let Some(path) = path {
666 vis.visit_path_expr(path);
667 }
668 walk_list!(vis, visit_constructor_args, exprs);
669 }
670 ExprKind::Quant(_, i, _, e) => {
671 vis.visit_refine_param(i);
672 vis.visit_expr(e);
673 }
674 ExprKind::Block(decls, body) => {
675 for decl in decls {
676 vis.visit_expr(&decl.init);
679 vis.visit_refine_param(&decl.param);
680 }
681 vis.visit_expr(body);
682 }
683 ExprKind::SetLiteral(exprs) => {
684 walk_list!(vis, visit_expr, exprs);
685 }
686 ExprKind::Tuple(exprs) => {
687 walk_list!(vis, visit_expr, exprs);
688 }
689 }
690}
691
692pub fn walk_path_expr<'v, V: Visitor<'v>>(vis: &mut V, qpath: &'v ExprPath) {
693 walk_list!(vis, visit_path_expr_segment, &qpath.segments);
694}
695
696pub fn walk_path_expr_segment<'v, V: Visitor<'v>>(vis: &mut V, segment: &'v ExprPathSegment) {
697 vis.visit_ident(segment.ident);
698}