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

flux_syntax/surface/
visit.rs
