Skip to main content

flux_syntax/surface/
visit.rs

1//! A visitor for types in [`surface`]
2//!
3//! In general there's no specific order except that [refinement parameters] should be
4//! visited in an order that matches their scope. Name resolution relies on this gurantee.
5//!
6//! [`surface`]: crate::surface
7//! [refinement parameters]: crate::surface::RefineParam
8use 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(&param.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
450// Explicit refinement params must be brought into scope *before* the generics, because a
451// `where` clause lives in `generics.predicates` and may mention them, e.g. an `hrn` parameter
452// used in the refinement of an `Fn`-trait bound e.g. tests/tests/pos/abstract_refinements/test05.rs
453// Implicit params (named inputs, `@`/`#` binders) are already pre-collected in `on_fn_sig`
454// before the walk, so only the explicit ones need this.
455
456pub 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                // the order here is important because the parameter is not in scope
677                // in the initializer
678                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}