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};
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_primop_prop(&mut self, prop: &PrimOpProp) {
41        walk_primop_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_primop_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(&param.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                // the order here is important because the parameter is not in scope
549                // in the initializer
550                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}
flux_syntax/surface/visit.rs

flux_syntax/surface/
visit.rs
