flux_middle/fhir/
visit.rs

1use super::{
2    AliasReft, AssocItemConstraint, AssocItemConstraintKind, BaseTy, BaseTyKind, Ensures, EnumDef,
3    Expr, ExprKind, FieldDef, FieldExpr, FluxItem, FnDecl, FnOutput, FnSig, ForeignItem,
4    ForeignItemKind, FuncSort, GenericArg, GenericBound, Generics, Impl, ImplAssocReft, ImplItem,
5    ImplItemKind, Item, ItemKind, Lit, OpaqueTy, OwnerNode, Path, PathExpr, PathSegment,
6    PolyFuncSort, PolyTraitRef, QPath, Qualifier, RefineParam, Requires, Sort, SortPath, SpecFunc,
7    StructDef, TraitAssocReft, TraitItem, TraitItemKind, Ty, TyAlias, TyKind, VariantDef,
8    VariantRet, WhereBoundPredicate,
9};
10use crate::fhir::{Axiom, PrimOpProp, QPathExpr, QuantDom, SortDecl, StructKind};
11
12#[macro_export]
13macro_rules! walk_list {
14    ($visitor: expr, $method: ident, $list: expr $(, $($extra_args: expr),* )?) => {
15        {
16            #[allow(for_loops_over_fallibles)]
17            for elem in $list {
18                $visitor.$method(elem $(, $($extra_args,)* )?)
19            }
20        }
21    }
22}
23
24pub trait Visitor<'v>: Sized {
25    fn visit_flux_item(&mut self, item: &FluxItem<'v>) {
26        walk_flux_item(self, item);
27    }
28
29    fn visit_qualifier(&mut self, qualifier: &Qualifier<'v>) {
30        walk_qualifier(self, qualifier);
31    }
32
33    fn visit_sort_decl(&mut self, sort_decl: &SortDecl) {
34        walk_sort_decl(self, sort_decl);
35    }
36
37    fn visit_func(&mut self, func: &SpecFunc<'v>) {
38        walk_func(self, func);
39    }
40
41    fn visit_primop_prop(&mut self, prop: &PrimOpProp<'v>) {
42        walk_primop_prop(self, prop);
43    }
44
45    fn visit_axiom(&mut self, axiom: &Axiom<'v>) {
46        walk_axiom(self, axiom);
47    }
48
49    fn visit_node(&mut self, node: &OwnerNode<'v>) {
50        walk_node(self, node);
51    }
52
53    fn visit_item(&mut self, item: &Item<'v>) {
54        walk_item(self, item);
55    }
56
57    fn visit_trait_item(&mut self, trait_item: &TraitItem<'v>) {
58        walk_trait_item(self, trait_item);
59    }
60
61    fn visit_impl_item(&mut self, impl_item: &ImplItem<'v>) {
62        walk_impl_item(self, impl_item);
63    }
64
65    fn visit_foreign_item(&mut self, foreign_item: &ForeignItem<'v>) {
66        walk_foreign_item(self, foreign_item);
67    }
68
69    fn visit_generics(&mut self, generics: &Generics<'v>) {
70        walk_generics(self, generics);
71    }
72
73    fn visit_where_predicate(&mut self, predicate: &WhereBoundPredicate<'v>) {
74        walk_where_predicate(self, predicate);
75    }
76
77    fn visit_impl(&mut self, impl_: &Impl<'v>) {
78        walk_impl(self, impl_);
79    }
80
81    fn visit_impl_assoc_reft(&mut self, assoc_reft: &ImplAssocReft<'v>) {
82        walk_impl_assoc_reft(self, assoc_reft);
83    }
84
85    fn visit_trait_assoc_reft(&mut self, assoc_reft: &TraitAssocReft<'v>) {
86        walk_trait_assoc_reft(self, assoc_reft);
87    }
88
89    fn visit_struct_def(&mut self, struct_def: &StructDef<'v>) {
90        walk_struct_def(self, struct_def);
91    }
92
93    fn visit_enum_def(&mut self, enum_def: &EnumDef<'v>) {
94        walk_enum_def(self, enum_def);
95    }
96
97    fn visit_variant(&mut self, variant: &VariantDef<'v>) {
98        walk_variant(self, variant);
99    }
100
101    fn visit_field_def(&mut self, field: &FieldDef<'v>) {
102        walk_field_def(self, field);
103    }
104
105    fn visit_variant_ret(&mut self, ret: &VariantRet<'v>) {
106        walk_variant_ret(self, ret);
107    }
108
109    fn visit_ty_alias(&mut self, ty_alias: &TyAlias<'v>) {
110        walk_ty_alias(self, ty_alias);
111    }
112
113    fn visit_opaque_ty(&mut self, opaque_ty: &OpaqueTy<'v>) {
114        walk_opaque_ty(self, opaque_ty);
115    }
116
117    fn visit_generic_bound(&mut self, bound: &GenericBound<'v>) {
118        walk_generic_bound(self, bound);
119    }
120
121    fn visit_poly_trait_ref(&mut self, trait_ref: &PolyTraitRef<'v>) {
122        walk_poly_trait_ref(self, trait_ref);
123    }
124
125    fn visit_fn_sig(&mut self, sig: &FnSig<'v>) {
126        walk_fn_sig(self, sig);
127    }
128
129    fn visit_fn_decl(&mut self, decl: &FnDecl<'v>) {
130        walk_fn_decl(self, decl);
131    }
132
133    fn visit_refine_param(&mut self, param: &RefineParam<'v>) {
134        walk_refine_param(self, param);
135    }
136
137    fn visit_requires(&mut self, requires: &Requires<'v>) {
138        walk_requires(self, requires);
139    }
140
141    fn visit_ensures(&mut self, ensures: &Ensures<'v>) {
142        walk_ensures(self, ensures);
143    }
144
145    fn visit_fn_output(&mut self, output: &FnOutput<'v>) {
146        walk_fn_output(self, output);
147    }
148
149    fn visit_generic_arg(&mut self, arg: &GenericArg<'v>) {
150        walk_generic_arg(self, arg);
151    }
152
153    fn visit_ty(&mut self, ty: &Ty<'v>) {
154        walk_ty(self, ty);
155    }
156
157    fn visit_bty(&mut self, bty: &BaseTy<'v>) {
158        walk_bty(self, bty);
159    }
160
161    fn visit_qpath(&mut self, qpath: &QPath<'v>) {
162        walk_qpath(self, qpath);
163    }
164
165    fn visit_path(&mut self, path: &Path<'v>) {
166        walk_path(self, path);
167    }
168
169    fn visit_path_segment(&mut self, segment: &PathSegment<'v>) {
170        walk_path_segment(self, segment);
171    }
172
173    fn visit_assoc_item_constraint(&mut self, constraint: &AssocItemConstraint<'v>) {
174        walk_assoc_item_constraint(self, constraint);
175    }
176
177    fn visit_sort(&mut self, sort: &Sort<'v>) {
178        walk_sort(self, sort);
179    }
180
181    fn visit_sort_path(&mut self, path: &SortPath<'v>) {
182        walk_sort_path(self, path);
183    }
184
185    fn visit_poly_func_sort(&mut self, func: &PolyFuncSort<'v>) {
186        walk_poly_func_sort(self, func);
187    }
188
189    fn visit_func_sort(&mut self, func: &FuncSort<'v>) {
190        walk_func_sort(self, func);
191    }
192
193    fn visit_domain(&mut self, dom: &QuantDom) {
194        walk_domain(self, dom);
195    }
196
197    fn visit_expr(&mut self, expr: &Expr<'v>) {
198        walk_expr(self, expr);
199    }
200
201    fn visit_field_expr(&mut self, expr: &FieldExpr<'v>) {
202        walk_field_expr(self, expr);
203    }
204
205    fn visit_alias_reft(&mut self, alias_reft: &AliasReft<'v>) {
206        walk_alias_reft(self, alias_reft);
207    }
208
209    fn visit_literal(&mut self, _lit: &Lit) {}
210
211    fn visit_path_expr(&mut self, _path: &PathExpr<'v>) {}
212}
213
214fn walk_sort_decl<'v, V: Visitor<'v>>(_vis: &mut V, _sort_decl: &SortDecl) {}
215
216fn walk_func<'v, V: Visitor<'v>>(vis: &mut V, func: &SpecFunc<'v>) {
217    walk_list!(vis, visit_refine_param, func.args);
218    vis.visit_sort(&func.sort);
219    if let Some(body) = &func.body {
220        vis.visit_expr(body);
221    }
222}
223
224fn walk_primop_prop<'v, V: Visitor<'v>>(vis: &mut V, prop: &PrimOpProp<'v>) {
225    walk_list!(vis, visit_refine_param, prop.args);
226    vis.visit_expr(&prop.body);
227}
228
229fn walk_axiom<'v, V: Visitor<'v>>(vis: &mut V, axiom: &Axiom<'v>) {
230    walk_list!(vis, visit_refine_param, axiom.args);
231    vis.visit_expr(&axiom.body);
232}
233
234fn walk_qualifier<'v, V: Visitor<'v>>(vis: &mut V, qualifier: &Qualifier<'v>) {
235    walk_list!(vis, visit_refine_param, qualifier.args);
236    vis.visit_expr(&qualifier.expr);
237}
238
239fn walk_flux_item<'v, V: Visitor<'v>>(vis: &mut V, item: &FluxItem<'v>) {
240    match item {
241        FluxItem::Qualifier(qualifier) => {
242            vis.visit_qualifier(qualifier);
243        }
244        FluxItem::Func(func) => {
245            vis.visit_func(func);
246        }
247        FluxItem::PrimOpProp(prop) => {
248            vis.visit_primop_prop(prop);
249        }
250        FluxItem::Axiom(axiom) => {
251            vis.visit_axiom(axiom);
252        }
253        FluxItem::SortDecl(sort_decl) => {
254            vis.visit_sort_decl(sort_decl);
255        }
256    }
257}
258
259pub fn walk_impl<'v, V: Visitor<'v>>(vis: &mut V, impl_: &Impl<'v>) {
260    walk_list!(vis, visit_impl_assoc_reft, impl_.assoc_refinements);
261}
262
263pub fn walk_struct_def<'v, V: Visitor<'v>>(vis: &mut V, struct_def: &StructDef<'v>) {
264    walk_list!(vis, visit_refine_param, struct_def.params);
265    walk_list!(vis, visit_expr, struct_def.invariants);
266    if let StructKind::Transparent { fields } = struct_def.kind {
267        walk_list!(vis, visit_field_def, fields);
268    }
269}
270
271pub fn walk_enum_def<'v, V: Visitor<'v>>(vis: &mut V, enum_def: &EnumDef<'v>) {
272    walk_list!(vis, visit_refine_param, enum_def.params);
273    walk_list!(vis, visit_variant, enum_def.variants);
274    walk_list!(vis, visit_expr, enum_def.invariants);
275}
276
277pub fn walk_variant<'v, V: Visitor<'v>>(vis: &mut V, variant: &VariantDef<'v>) {
278    walk_list!(vis, visit_refine_param, variant.params);
279    walk_list!(vis, visit_field_def, variant.fields);
280    vis.visit_variant_ret(&variant.ret);
281}
282
283pub fn walk_field_def<'v, V: Visitor<'v>>(vis: &mut V, field: &FieldDef<'v>) {
284    let FieldDef { ty, lifted: _ } = field;
285    vis.visit_ty(ty);
286}
287
288pub fn walk_variant_ret<'v, V: Visitor<'v>>(vis: &mut V, ret: &VariantRet<'v>) {
289    let VariantRet { idx, enum_id: _ } = ret;
290    vis.visit_expr(idx);
291}
292
293pub fn walk_ty_alias<'v, V: Visitor<'v>>(vis: &mut V, ty_alias: &TyAlias<'v>) {
294    if let Some(index) = &ty_alias.index {
295        vis.visit_refine_param(index);
296    }
297    vis.visit_ty(&ty_alias.ty);
298}
299
300pub fn walk_opaque_ty<'v, V: Visitor<'v>>(vis: &mut V, opaque_ty: &OpaqueTy<'v>) {
301    walk_list!(vis, visit_generic_bound, opaque_ty.bounds);
302}
303
304pub fn walk_generic_bound<'v, V: Visitor<'v>>(vis: &mut V, bound: &GenericBound<'v>) {
305    match bound {
306        GenericBound::Trait(trait_ref) => vis.visit_poly_trait_ref(trait_ref),
307        GenericBound::Outlives => {}
308    }
309}
310
311pub fn walk_poly_trait_ref<'v, V: Visitor<'v>>(vis: &mut V, trait_ref: &PolyTraitRef<'v>) {
312    walk_list!(vis, visit_refine_param, trait_ref.refine_params);
313    vis.visit_path(&trait_ref.trait_ref);
314}
315
316pub fn walk_node<'v, V: Visitor<'v>>(vis: &mut V, node: &OwnerNode<'v>) {
317    match node {
318        OwnerNode::Item(item) => vis.visit_item(item),
319        OwnerNode::TraitItem(trait_item) => vis.visit_trait_item(trait_item),
320        OwnerNode::ImplItem(impl_item) => vis.visit_impl_item(impl_item),
321        OwnerNode::ForeignItem(foreign_item) => vis.visit_foreign_item(foreign_item),
322    }
323}
324
325pub fn walk_item<'v, V: Visitor<'v>>(vis: &mut V, item: &Item<'v>) {
326    vis.visit_generics(&item.generics);
327    match &item.kind {
328        ItemKind::Enum(enum_def) => vis.visit_enum_def(enum_def),
329        ItemKind::Struct(struct_def) => vis.visit_struct_def(struct_def),
330        ItemKind::TyAlias(ty_alias) => vis.visit_ty_alias(ty_alias),
331        ItemKind::Trait(trait_) => {
332            walk_list!(vis, visit_trait_assoc_reft, trait_.assoc_refinements);
333        }
334        ItemKind::Impl(impl_) => vis.visit_impl(impl_),
335        ItemKind::Fn(fn_sig) => vis.visit_fn_sig(fn_sig),
336        ItemKind::Const(info) => {
337            if let Some(expr) = info {
338                vis.visit_expr(expr);
339            }
340        }
341        ItemKind::Static(ty) => {
342            if let Some(ty) = ty {
343                vis.visit_ty(ty);
344            }
345        }
346    }
347}
348
349pub fn walk_trait_item<'v, V: Visitor<'v>>(vis: &mut V, trait_item: &TraitItem<'v>) {
350    vis.visit_generics(&trait_item.generics);
351    match &trait_item.kind {
352        TraitItemKind::Fn(fn_sig) => vis.visit_fn_sig(fn_sig),
353        TraitItemKind::Type => {}
354        TraitItemKind::Const => {}
355    }
356}
357
358pub fn walk_impl_item<'v, V: Visitor<'v>>(vis: &mut V, impl_item: &ImplItem<'v>) {
359    vis.visit_generics(&impl_item.generics);
360    match &impl_item.kind {
361        ImplItemKind::Fn(fn_sig) => vis.visit_fn_sig(fn_sig),
362        ImplItemKind::Const => {}
363        ImplItemKind::Type => {}
364    }
365}
366
367pub fn walk_foreign_item<'v, V: Visitor<'v>>(vis: &mut V, impl_item: &ForeignItem<'v>) {
368    match &impl_item.kind {
369        ForeignItemKind::Fn(fn_sig, generics) => {
370            vis.visit_generics(generics);
371            vis.visit_fn_sig(fn_sig);
372        }
373        ForeignItemKind::Static(ty, _, _, generics) => {
374            vis.visit_generics(generics);
375            vis.visit_ty(ty);
376        }
377    }
378}
379
380pub fn walk_trait_assoc_reft<'v, V: Visitor<'v>>(vis: &mut V, assoc_reft: &TraitAssocReft<'v>) {
381    walk_list!(vis, visit_refine_param, assoc_reft.params);
382    vis.visit_sort(&assoc_reft.output);
383    if let Some(expr) = &assoc_reft.body {
384        vis.visit_expr(expr);
385    }
386}
387
388pub fn walk_impl_assoc_reft<'v, V: Visitor<'v>>(vis: &mut V, assoc_reft: &ImplAssocReft<'v>) {
389    walk_list!(vis, visit_refine_param, assoc_reft.params);
390    vis.visit_sort(&assoc_reft.output);
391    vis.visit_expr(&assoc_reft.body);
392}
393
394pub fn walk_generics<'v, V: Visitor<'v>>(vis: &mut V, generics: &Generics<'v>) {
395    walk_list!(vis, visit_refine_param, generics.refinement_params);
396    if let Some(predicates) = generics.predicates {
397        walk_list!(vis, visit_where_predicate, predicates);
398    }
399}
400
401pub fn walk_where_predicate<'v, V: Visitor<'v>>(vis: &mut V, predicate: &WhereBoundPredicate<'v>) {
402    vis.visit_ty(&predicate.bounded_ty);
403    walk_list!(vis, visit_generic_bound, predicate.bounds);
404}
405
406pub fn walk_fn_sig<'v, V: Visitor<'v>>(vis: &mut V, sig: &FnSig<'v>) {
407    vis.visit_fn_decl(sig.decl);
408}
409
410pub fn walk_fn_decl<'v, V: Visitor<'v>>(vis: &mut V, decl: &FnDecl<'v>) {
411    walk_list!(vis, visit_requires, decl.requires);
412    walk_list!(vis, visit_ty, decl.inputs);
413    vis.visit_fn_output(&decl.output);
414}
415
416pub fn walk_refine_param<'v, V: Visitor<'v>>(vis: &mut V, param: &RefineParam<'v>) {
417    vis.visit_sort(&param.sort);
418}
419
420pub fn walk_requires<'v, V: Visitor<'v>>(vis: &mut V, requires: &Requires<'v>) {
421    walk_list!(vis, visit_refine_param, requires.params);
422    vis.visit_expr(&requires.pred);
423}
424
425pub fn walk_ensures<'v, V: Visitor<'v>>(vis: &mut V, constraint: &Ensures<'v>) {
426    match constraint {
427        Ensures::Type(loc, ty) => {
428            vis.visit_path_expr(loc);
429            vis.visit_ty(ty);
430        }
431        Ensures::Pred(pred) => {
432            vis.visit_expr(pred);
433        }
434    }
435}
436
437pub fn walk_fn_output<'v, V: Visitor<'v>>(vis: &mut V, output: &FnOutput<'v>) {
438    walk_list!(vis, visit_refine_param, output.params);
439    vis.visit_ty(&output.ret);
440    walk_list!(vis, visit_ensures, output.ensures);
441}
442
443pub fn walk_generic_arg<'v, V: Visitor<'v>>(vis: &mut V, arg: &GenericArg<'v>) {
444    match arg {
445        GenericArg::Type(ty) => vis.visit_ty(ty),
446        GenericArg::Const(_) | GenericArg::Infer => {}
447    }
448}
449
450pub fn walk_ty<'v, V: Visitor<'v>>(vis: &mut V, ty: &Ty<'v>) {
451    match ty.kind {
452        TyKind::BaseTy(bty) => vis.visit_bty(&bty),
453        TyKind::Indexed(bty, idx) => {
454            vis.visit_bty(&bty);
455            vis.visit_expr(&idx);
456        }
457        TyKind::Exists(params, ty) => {
458            walk_list!(vis, visit_refine_param, params);
459            vis.visit_ty(ty);
460        }
461        TyKind::Constr(pred, ty) => {
462            vis.visit_expr(&pred);
463            vis.visit_ty(ty);
464        }
465        TyKind::StrgRef(loc, ty) => {
466            vis.visit_path_expr(loc);
467            vis.visit_ty(ty);
468        }
469        TyKind::Ref(ty, _) => {
470            vis.visit_ty(ty);
471        }
472        TyKind::BareFn(bare_fn) => {
473            walk_list!(vis, visit_refine_param, bare_fn.params);
474            vis.visit_fn_decl(bare_fn.decl);
475        }
476        TyKind::Tuple(tys) => {
477            walk_list!(vis, visit_ty, tys);
478        }
479        TyKind::Array(ty, _len) => {
480            vis.visit_ty(ty);
481        }
482        TyKind::OpaqueDef(opaque_ty) => {
483            vis.visit_opaque_ty(opaque_ty);
484        }
485        TyKind::TraitObject(poly_traits, _) => {
486            walk_list!(vis, visit_poly_trait_ref, poly_traits);
487        }
488        TyKind::Never | TyKind::Infer | TyKind::Err(_) => {}
489    }
490}
491
492pub fn walk_bty<'v, V: Visitor<'v>>(vis: &mut V, bty: &BaseTy<'v>) {
493    match &bty.kind {
494        BaseTyKind::Path(path) => vis.visit_qpath(path),
495        BaseTyKind::Slice(ty) => vis.visit_ty(ty),
496        BaseTyKind::RawPtr(ty, _mtblt) => {
497            vis.visit_ty(ty);
498        }
499        BaseTyKind::Err(_) => {}
500    }
501}
502
503pub fn walk_qpath<'v, V: Visitor<'v>>(vis: &mut V, qpath: &QPath<'v>) {
504    match qpath {
505        QPath::Resolved(qself, path) => {
506            if let Some(self_ty) = qself {
507                vis.visit_ty(self_ty);
508            }
509            vis.visit_path(path);
510        }
511        QPath::TypeRelative(qself, assoc) => {
512            vis.visit_ty(qself);
513            vis.visit_path_segment(assoc);
514        }
515    }
516}
517
518pub fn walk_path<'v, V: Visitor<'v>>(vis: &mut V, path: &Path<'v>) {
519    walk_list!(vis, visit_path_segment, path.segments);
520    walk_list!(vis, visit_expr, path.refine);
521}
522
523pub fn walk_path_segment<'v, V: Visitor<'v>>(vis: &mut V, segment: &PathSegment<'v>) {
524    walk_list!(vis, visit_generic_arg, segment.args);
525    walk_list!(vis, visit_assoc_item_constraint, segment.constraints);
526}
527
528pub fn walk_assoc_item_constraint<'v, V: Visitor<'v>>(
529    vis: &mut V,
530    constraint: &AssocItemConstraint<'v>,
531) {
532    match &constraint.kind {
533        AssocItemConstraintKind::Equality { term } => {
534            vis.visit_ty(term);
535        }
536    }
537}
538
539pub fn walk_sort<'v, V: Visitor<'v>>(vis: &mut V, sort: &Sort<'v>) {
540    match sort {
541        Sort::Path(path) => vis.visit_sort_path(path),
542        Sort::Func(func) => vis.visit_poly_func_sort(func),
543        Sort::SortOf(bty) => vis.visit_bty(bty),
544        Sort::Tuple(sorts) => {
545            walk_list!(vis, visit_sort, *sorts);
546        }
547        Sort::Loc | Sort::BitVec(_) | Sort::Infer | Sort::Err(_) => {}
548    }
549}
550
551pub fn walk_sort_path<'v, V: Visitor<'v>>(vis: &mut V, path: &SortPath<'v>) {
552    walk_list!(vis, visit_sort, path.args);
553}
554
555pub fn walk_poly_func_sort<'v, V: Visitor<'v>>(vis: &mut V, func: &PolyFuncSort<'v>) {
556    let PolyFuncSort { params: _, fsort } = func;
557    vis.visit_func_sort(fsort);
558}
559
560pub fn walk_func_sort<'v, V: Visitor<'v>>(vis: &mut V, func: &FuncSort<'v>) {
561    walk_list!(vis, visit_sort, func.inputs_and_output);
562}
563
564pub fn walk_alias_reft<'v, V: Visitor<'v>>(vis: &mut V, alias: &AliasReft<'v>) {
565    match alias {
566        AliasReft::Qualified { qself, trait_, name: _ } => {
567            vis.visit_ty(qself);
568            vis.visit_path(trait_);
569        }
570        AliasReft::TypeRelative { qself, name: _ } => {
571            vis.visit_ty(qself);
572        }
573    }
574}
575
576pub fn walk_field_expr<'v, V: Visitor<'v>>(vis: &mut V, expr: &FieldExpr<'v>) {
577    vis.visit_expr(&expr.expr);
578}
579
580pub fn walk_domain<'v, V: Visitor<'v>>(vis: &mut V, dom: &QuantDom) {
581    match dom {
582        QuantDom::Bounded { start, end } => {
583            vis.visit_literal(&Lit::Int(*start as u128));
584            vis.visit_literal(&Lit::Int(*end as u128));
585        }
586        QuantDom::Unbounded => {}
587    }
588}
589
590pub fn walk_expr<'v, V: Visitor<'v>>(vis: &mut V, expr: &Expr<'v>) {
591    match expr.kind {
592        ExprKind::Var(qpath) => walk_qpath_expr(vis, qpath),
593        ExprKind::Dot(base, _fld) => {
594            vis.visit_expr(base);
595        }
596        ExprKind::Literal(lit) => vis.visit_literal(&lit),
597        ExprKind::BinaryOp(_op, e1, e2) => {
598            vis.visit_expr(e1);
599            vis.visit_expr(e2);
600        }
601        ExprKind::PrimApp(_op, e1, e2) => {
602            vis.visit_expr(e1);
603            vis.visit_expr(e2);
604        }
605        ExprKind::UnaryOp(_op, e) => vis.visit_expr(e),
606        ExprKind::App(func, args) => {
607            vis.visit_path_expr(&func);
608            walk_list!(vis, visit_expr, args);
609        }
610        ExprKind::Alias(alias_reft, args) => {
611            vis.visit_alias_reft(&alias_reft);
612            walk_list!(vis, visit_expr, args);
613        }
614        ExprKind::IfThenElse(e1, e2, e3) => {
615            vis.visit_expr(e1);
616            vis.visit_expr(e2);
617            vis.visit_expr(e3);
618        }
619        ExprKind::Abs(refine_params, body) => {
620            walk_list!(vis, visit_refine_param, refine_params);
621            vis.visit_expr(body);
622        }
623        ExprKind::Record(exprs) | ExprKind::SetLiteral(exprs) | ExprKind::Tuple(exprs) => {
624            walk_list!(vis, visit_expr, exprs);
625        }
626        ExprKind::Constructor(path, exprs, spread) => {
627            if let Some(path) = path {
628                vis.visit_path_expr(&path);
629            }
630            walk_list!(vis, visit_field_expr, exprs);
631            if let Some(s) = spread {
632                vis.visit_expr(&s.expr);
633            }
634        }
635        ExprKind::Quant(_, param, dom, expr) => {
636            vis.visit_domain(&dom);
637            vis.visit_refine_param(&param);
638            vis.visit_expr(expr);
639        }
640        ExprKind::Block(decls, body) => {
641            for decl in decls {
642                vis.visit_expr(&decl.init);
643                vis.visit_refine_param(&decl.param);
644            }
645            vis.visit_expr(body);
646        }
647        ExprKind::Err(_) => {}
648    }
649}
650
651pub fn walk_qpath_expr<'v, V: Visitor<'v>>(vis: &mut V, qpath: QPathExpr<'v>) {
652    match qpath {
653        QPathExpr::Resolved(path, _param_kind) => {
654            vis.visit_path_expr(&path);
655        }
656        QPathExpr::TypeRelative(qself, _ident) => vis.visit_ty(qself),
657    }
658}
flux_middle/fhir/visit.rs

flux_middle/fhir/
visit.rs
