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