1pub mod visit;
2use std::{borrow::Cow, fmt, ops::Range};
3
4use flux_config::PartialInferOpts;
5pub use rustc_ast::{
6 Mutability,
7 token::{Lit, LitKind},
8};
9pub use rustc_span::{Span, symbol::Ident};
10use rustc_span::{Symbol, symbol::sym};
11
12use crate::surface::visit::Visitor;
13
14#[derive(Copy, Clone, Debug, Hash, PartialEq, Eq)]
17pub struct NodeId(pub(super) usize);
18
19impl NodeId {
20 pub fn as_usize(&self) -> usize {
21 self.0
22 }
23}
24
25#[derive(Debug)]
26pub struct SortDecl {
27 pub name: Ident,
28 pub sort_vars: Vec<Ident>,
29}
30
31#[derive(Debug)]
32pub enum FluxItem {
33 Qualifier(Qualifier),
34 FuncDef(SpecFunc),
35 SortDecl(SortDecl),
36 PrimOpProp(PrimOpProp),
37}
38
39impl FluxItem {
40 pub fn name(&self) -> Ident {
41 match self {
42 FluxItem::Qualifier(qualifier) => qualifier.name,
43 FluxItem::FuncDef(spec_func) => spec_func.name,
44 FluxItem::SortDecl(sort_decl) => sort_decl.name,
45 FluxItem::PrimOpProp(primop_prop) => primop_prop.name,
46 }
47 }
48}
49
50#[derive(Debug)]
51pub struct Qualifier {
52 pub name: Ident,
53 pub params: RefineParams,
54 pub expr: Expr,
55 pub span: Span,
56 pub global: bool,
57}
58
59#[derive(Debug)]
62pub struct SpecFunc {
63 pub name: Ident,
64 pub sort_vars: Vec<Ident>,
65 pub params: RefineParams,
66 pub output: Sort,
67 pub body: Option<Expr>,
69 pub hide: bool,
73}
74
75#[derive(Debug)]
77pub struct PrimOpProp {
78 pub name: Ident,
80 pub op: BinOp,
82 pub params: RefineParams,
85 pub body: Expr,
87 pub span: Span,
88}
89
90#[derive(Debug)]
91pub struct Generics {
92 pub params: Vec<GenericParam>,
93 pub predicates: Option<Vec<WhereBoundPredicate>>,
94 pub span: Span,
95}
96
97#[derive(Debug)]
98pub struct GenericParam {
99 pub name: Ident,
100 pub node_id: NodeId,
101}
102
103#[derive(Debug)]
104pub struct TyAlias {
105 pub ident: Ident,
106 pub generics: Generics,
107 pub params: RefineParams,
108 pub index: Option<RefineParam>,
109 pub ty: Ty,
110 pub node_id: NodeId,
111 pub span: Span,
112}
113
114pub struct Item {
115 pub attrs: Vec<Attr>,
116 pub kind: ItemKind,
117 pub node_id: NodeId,
118}
119
120pub enum ItemKind {
121 Fn(Option<FnSig>),
122 Struct(StructDef),
123 Enum(EnumDef),
124 Trait(Trait),
125 Impl(Impl),
126 Const(ConstantInfo),
127 TyAlias(Box<TyAlias>),
128 Mod,
131}
132
133pub struct TraitItemFn {
134 pub attrs: Vec<Attr>,
135 pub sig: Option<FnSig>,
136 pub node_id: NodeId,
137}
138
139pub struct ImplItemFn {
140 pub attrs: Vec<Attr>,
141 pub sig: Option<FnSig>,
142 pub node_id: NodeId,
143}
144
145#[derive(Debug)]
146pub struct DetachedSpecs {
147 pub items: Vec<DetachedItem>,
148}
149
150#[derive(Debug)]
151pub struct DetachedTraitImpl {
152 pub trait_: ExprPath,
153 pub items: Vec<DetachedItem<FnSig>>,
154 pub refts: Vec<ImplAssocReft>,
155 pub span: Span,
156}
157
158#[derive(Debug, Default)]
159pub struct DetachedTrait {
160 pub items: Vec<DetachedItem<FnSig>>,
161 pub refts: Vec<TraitAssocReft>,
162}
163
164#[derive(Debug)]
165pub struct DetachedInherentImpl {
166 pub items: Vec<DetachedItem<FnSig>>,
167 pub span: Span,
168}
169
170impl DetachedInherentImpl {
171 pub fn extend(&mut self, other: DetachedInherentImpl) {
172 self.items.extend(other.items);
173 }
174}
175
176#[derive(Debug)]
177pub struct DetachedItem<K = DetachedItemKind> {
178 pub attrs: Vec<Attr>,
179 pub path: ExprPath,
180 pub kind: K,
181 pub node_id: NodeId,
182}
183
184impl<K> DetachedItem<K> {
185 pub fn map_kind<R>(self, f: impl FnOnce(K) -> R) -> DetachedItem<R> {
186 DetachedItem {
187 attrs: self.attrs,
188 path: self.path,
189 kind: f(self.kind),
190 node_id: self.node_id,
191 }
192 }
193}
194
195impl DetachedItem<DetachedItemKind> {
196 pub fn span(&self) -> Span {
197 match &self.kind {
198 DetachedItemKind::InherentImpl(impl_) => impl_.span,
199 DetachedItemKind::TraitImpl(trait_impl) => trait_impl.span,
200 _ => self.path.span,
201 }
202 }
203}
204
205#[derive(Debug)]
206pub enum DetachedItemKind {
207 FnSig(FnSig),
208 Mod(DetachedSpecs),
209 Struct(StructDef),
210 Enum(EnumDef),
211 InherentImpl(DetachedInherentImpl),
212 TraitImpl(DetachedTraitImpl),
213 Trait(DetachedTrait),
214}
215
216#[derive(Debug)]
217pub struct ConstantInfo {
218 pub expr: Option<Expr>,
219}
220
221#[derive(Debug)]
222pub struct StructDef {
223 pub generics: Option<Generics>,
224 pub refined_by: Option<RefineParams>,
225 pub fields: Vec<Option<Ty>>,
226 pub opaque: bool,
227 pub invariants: Vec<Expr>,
228}
229
230#[derive(Debug)]
231pub struct EnumDef {
232 pub generics: Option<Generics>,
233 pub refined_by: Option<RefineParams>,
234 pub variants: Vec<Option<VariantDef>>,
235 pub invariants: Vec<Expr>,
236 pub reflected: bool,
237}
238
239#[derive(Debug)]
240pub struct VariantDef {
241 pub ident: Option<Ident>,
242 pub fields: Vec<Ty>,
243 pub ret: Option<VariantRet>,
244 pub node_id: NodeId,
245 pub span: Span,
246}
247
248#[derive(Debug)]
249pub struct VariantRet {
250 pub path: Path,
251 pub indices: Indices,
254}
255
256pub type RefineParams = Vec<RefineParam>;
257
258#[derive(Debug)]
259pub struct RefineParam {
260 pub ident: Ident,
261 pub sort: Sort,
262 pub mode: Option<ParamMode>,
263 pub span: Span,
264 pub node_id: NodeId,
265}
266
267#[derive(Clone, Copy, Debug, PartialEq, Eq)]
268pub enum ParamMode {
269 Horn,
270 Hindley,
271}
272
273#[derive(Debug)]
274pub enum Sort {
275 Base(BaseSort),
277 Func { inputs: Vec<BaseSort>, output: BaseSort },
280 Infer,
282}
283
284#[derive(Debug)]
285pub enum BaseSort {
286 BitVec(u32),
288 SortOf(Box<Ty>, Path),
289 Path(SortPath),
290}
291
292#[derive(Debug)]
294pub struct SortPath {
295 pub segments: Vec<Ident>,
297 pub args: Vec<BaseSort>,
299 pub node_id: NodeId,
300}
301
302#[derive(Debug)]
303pub struct Impl {
304 pub generics: Option<Generics>,
305 pub assoc_refinements: Vec<ImplAssocReft>,
306}
307
308#[derive(Debug)]
309pub struct ImplAssocReft {
310 pub name: Ident,
311 pub params: RefineParams,
312 pub output: BaseSort,
313 pub body: Expr,
314 pub span: Span,
315}
316
317#[derive(Debug)]
318pub struct Trait {
319 pub generics: Option<Generics>,
320 pub assoc_refinements: Vec<TraitAssocReft>,
321}
322
323#[derive(Debug)]
324pub struct TraitAssocReft {
325 pub name: Ident,
326 pub params: RefineParams,
327 pub output: BaseSort,
328 pub body: Option<Expr>,
329 pub span: Span,
330 pub final_: bool,
331}
332
333#[derive(Debug)]
334pub struct FnSig {
335 pub asyncness: Async,
336 pub ident: Option<Ident>,
337 pub generics: Generics,
338 pub params: RefineParams,
339 pub requires: Vec<Requires>,
341 pub inputs: Vec<FnInput>,
343 pub output: FnOutput,
344 pub span: Span,
346 pub node_id: NodeId,
347}
348
349#[derive(Debug)]
350pub struct Requires {
351 pub params: RefineParams,
353 pub pred: Expr,
354}
355
356#[derive(Debug)]
357pub struct FnOutput {
358 pub returns: FnRetTy,
360 pub ensures: Vec<Ensures>,
362 pub node_id: NodeId,
363}
364
365#[derive(Debug)]
366pub enum Ensures {
367 Type(Ident, Ty, NodeId),
369 Pred(Expr),
371}
372
373#[derive(Debug)]
374pub enum FnRetTy {
375 Default(Span),
376 Ty(Box<Ty>),
377}
378
379#[derive(Debug, Copy, Clone)]
380pub enum Async {
381 Yes { node_id: NodeId, span: Span },
382 No,
383}
384
385#[derive(Debug)]
386pub struct WhereBoundPredicate {
387 pub span: Span,
388 pub bounded_ty: Ty,
389 pub bounds: GenericBounds,
390}
391
392pub type GenericBounds = Vec<TraitRef>;
393
394#[derive(Debug)]
395pub struct TraitRef {
396 pub path: Path,
397 pub node_id: NodeId,
398}
399
400impl TraitRef {
401 fn is_fn_trait_name(name: Symbol) -> bool {
402 name == sym::FnOnce || name == sym::FnMut || name == sym::Fn
403 }
404
405 pub fn as_fn_trait_ref(&self) -> Option<(&GenericArg, &GenericArg)> {
406 if let [segment] = self.path.segments.as_slice()
407 && Self::is_fn_trait_name(segment.ident.name)
408 && let [in_arg, out_arg] = segment.args.as_slice()
409 {
410 return Some((in_arg, out_arg));
411 }
412 None
413 }
414}
415
416#[derive(Debug)]
417pub enum FnInput {
418 Constr(Ident, Path, Expr, NodeId),
420 StrgRef(Ident, Ty, NodeId),
422 Ty(Option<Ident>, Ty, NodeId),
425}
426
427#[derive(Debug)]
428pub struct Ty {
429 pub kind: TyKind,
430 pub node_id: NodeId,
431 pub span: Span,
432}
433
434#[derive(Debug)]
435pub enum TyKind {
436 Base(BaseTy),
438 Indexed {
440 bty: BaseTy,
441 indices: Indices,
442 },
443 Exists {
445 bind: Ident,
446 bty: BaseTy,
447 pred: Expr,
448 },
449 GeneralExists {
450 params: RefineParams,
451 ty: Box<Ty>,
452 pred: Option<Expr>,
453 },
454 Ref(Mutability, Box<Ty>),
456 Constr(Expr, Box<Ty>),
458 Tuple(Vec<Ty>),
459 Array(Box<Ty>, ConstArg),
460 ImplTrait(NodeId, GenericBounds),
462 Hole,
463}
464
465impl Ty {
466 pub fn is_refined(&self) -> bool {
467 struct IsRefinedVisitor {
468 is_refined: bool,
469 }
470 let mut vis = IsRefinedVisitor { is_refined: false };
471 impl visit::Visitor for IsRefinedVisitor {
472 fn visit_ty(&mut self, ty: &Ty) {
473 match &ty.kind {
474 TyKind::Tuple(_)
475 | TyKind::Ref(..)
476 | TyKind::Array(..)
477 | TyKind::ImplTrait(..)
478 | TyKind::Hole
479 | TyKind::Base(_) => {
480 visit::walk_ty(self, ty);
481 }
482 TyKind::Indexed { .. }
483 | TyKind::Exists { .. }
484 | TyKind::GeneralExists { .. }
485 | TyKind::Constr(..) => {
486 self.is_refined = true;
487 }
488 }
489 }
490 }
491 vis.visit_ty(self);
492 vis.is_refined
493 }
494
495 pub fn is_potential_const_arg(&self) -> Option<&Path> {
496 if let TyKind::Base(bty) = &self.kind
497 && let BaseTyKind::Path(None, path) = &bty.kind
498 && let [segment] = &path.segments[..]
499 && segment.args.is_empty()
500 {
501 Some(path)
502 } else {
503 None
504 }
505 }
506}
507#[derive(Debug)]
508pub struct BaseTy {
509 pub kind: BaseTyKind,
510 pub span: Span,
511}
512
513#[derive(Debug)]
514pub enum BaseTyKind {
515 Path(Option<Box<Ty>>, Path),
516 Slice(Box<Ty>),
517}
518
519#[derive(PartialEq, Eq, Clone, Debug, Copy)]
520pub struct ConstArg {
521 pub kind: ConstArgKind,
522 pub span: Span,
523}
524
525#[derive(PartialEq, Eq, Clone, Debug, Copy)]
526pub enum ConstArgKind {
527 Lit(usize),
528 Infer,
529}
530
531#[derive(Debug)]
532pub struct Indices {
533 pub indices: Vec<RefineArg>,
534 pub span: Span,
535}
536
537#[derive(Debug)]
538pub enum RefineArg {
539 Bind(Ident, BindKind, Span, NodeId),
541 Expr(Expr),
542 Abs(RefineParams, Expr, Span, NodeId),
543}
544
545#[derive(Debug, Clone, Copy)]
546pub enum BindKind {
547 At,
548 Pound,
549}
550
551#[derive(Debug, Eq, PartialEq, Copy, Clone)]
553pub enum Trusted {
554 Yes,
555 No,
556}
557
558impl Trusted {
559 pub fn to_bool(self) -> bool {
560 match self {
561 Trusted::Yes => true,
562 Trusted::No => false,
563 }
564 }
565}
566
567impl From<bool> for Trusted {
568 fn from(value: bool) -> Self {
569 if value { Trusted::Yes } else { Trusted::No }
570 }
571}
572
573#[derive(Debug, Eq, PartialEq, Copy, Clone)]
575pub enum Ignored {
576 Yes,
577 No,
578}
579
580impl Ignored {
581 pub fn to_bool(self) -> bool {
582 match self {
583 Ignored::Yes => true,
584 Ignored::No => false,
585 }
586 }
587}
588
589impl From<bool> for Ignored {
590 fn from(value: bool) -> Self {
591 if value { Ignored::Yes } else { Ignored::No }
592 }
593}
594
595#[derive(Debug)]
604pub enum Attr {
605 Trusted(Trusted),
607 TrustedImpl(Trusted),
609 Ignore(Ignored),
611 ProvenExternally,
613 ShouldFail,
615 Qualifiers(Vec<Ident>),
617 Reveal(Vec<Ident>),
619 InferOpts(PartialInferOpts),
621}
622
623#[derive(Debug)]
624pub struct Path {
625 pub segments: Vec<PathSegment>,
626 pub refine: Vec<RefineArg>,
627 pub node_id: NodeId,
628 pub span: Span,
629}
630
631impl Path {
632 pub fn last(&self) -> &PathSegment {
633 self.segments
634 .last()
635 .expect("path must have at least one segment")
636 }
637}
638
639#[derive(Debug)]
640pub struct PathSegment {
641 pub ident: Ident,
642 pub args: Vec<GenericArg>,
643 pub node_id: NodeId,
644}
645
646#[derive(Debug)]
647pub struct GenericArg {
648 pub kind: GenericArgKind,
649 pub node_id: NodeId,
650}
651
652#[derive(Debug)]
653pub enum GenericArgKind {
654 Type(Ty),
655 Constraint(Ident, Ty),
656}
657
658#[derive(Debug)]
659pub struct FieldExpr {
660 pub ident: Ident,
661 pub expr: Expr,
662 pub span: Span,
663 pub node_id: NodeId,
664}
665
666#[derive(Debug)]
667pub struct Spread {
668 pub expr: Expr,
669 pub span: Span,
670 pub node_id: NodeId,
671}
672
673#[derive(Debug)]
674pub enum ConstructorArg {
675 FieldExpr(FieldExpr),
676 Spread(Spread),
677}
678
679#[derive(Debug)]
680pub struct Expr {
681 pub kind: ExprKind,
682 pub node_id: NodeId,
683 pub span: Span,
684}
685
686#[derive(Debug)]
687pub enum QuantKind {
688 Forall,
689 Exists,
690}
691
692#[derive(Debug)]
693pub enum ExprKind {
694 Path(ExprPath),
695 Dot(Box<Expr>, Ident),
696 Literal(Lit),
697 BinaryOp(BinOp, Box<[Expr; 2]>),
698 UnaryOp(UnOp, Box<Expr>),
699 Call(Box<Expr>, Vec<Expr>),
700 PrimUIF(BinOp),
702 AssocReft(Box<Ty>, Path, Ident),
704 IfThenElse(Box<[Expr; 3]>),
705 Constructor(Option<ExprPath>, Vec<ConstructorArg>),
706 BoundedQuant(QuantKind, RefineParam, Range<usize>, Box<Expr>),
707 Block(Vec<LetDecl>, Box<Expr>),
708}
709
710#[derive(Debug)]
711pub struct LetDecl {
712 pub param: RefineParam,
713 pub init: Expr,
714}
715
716#[derive(Debug, Clone)]
718pub struct ExprPath {
719 pub segments: Vec<ExprPathSegment>,
720 pub node_id: NodeId,
721 pub span: Span,
722}
723
724#[derive(Debug, Clone)]
725pub struct ExprPathSegment {
726 pub ident: Ident,
727 pub node_id: NodeId,
728}
729#[derive(Copy, Clone, Hash, Eq, PartialEq)]
730pub enum BinOp {
731 Iff,
732 Imp,
733 Or,
734 And,
735 Eq,
736 Ne,
737 Gt,
738 Ge,
739 Lt,
740 Le,
741 Add,
742 Sub,
743 Mul,
744 Div,
745 Mod,
746 BitOr,
747 BitXor,
748 BitAnd,
749 BitShl,
750 BitShr,
751}
752
753impl fmt::Debug for BinOp {
754 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
755 match self {
756 BinOp::Iff => write!(f, "<=>"),
757 BinOp::Imp => write!(f, "=>"),
758 BinOp::Or => write!(f, "||"),
759 BinOp::And => write!(f, "&&"),
760 BinOp::Eq => write!(f, "=="),
761 BinOp::Ne => write!(f, "!="),
762 BinOp::Lt => write!(f, "<"),
763 BinOp::Le => write!(f, "<="),
764 BinOp::Gt => write!(f, ">"),
765 BinOp::Ge => write!(f, ">="),
766 BinOp::Add => write!(f, "+"),
767 BinOp::Sub => write!(f, "-"),
768 BinOp::Mod => write!(f, "mod"),
769 BinOp::Mul => write!(f, "*"),
770 BinOp::Div => write!(f, "/"),
771 BinOp::BitOr => write!(f, "|"),
772 BinOp::BitXor => write!(f, "^"),
773 BinOp::BitAnd => write!(f, "&"),
774 BinOp::BitShl => write!(f, "<<"),
775 BinOp::BitShr => write!(f, ">>"),
776 }
777 }
778}
779
780impl rustc_errors::IntoDiagArg for BinOp {
781 fn into_diag_arg(self, _path: &mut Option<std::path::PathBuf>) -> rustc_errors::DiagArgValue {
782 rustc_errors::DiagArgValue::Str(Cow::Owned(format!("{self:?}")))
783 }
784}
785
786#[derive(Copy, Clone)]
787pub enum UnOp {
788 Not,
789 Neg,
790}
791
792impl fmt::Debug for UnOp {
793 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
794 match self {
795 Self::Not => write!(f, "!"),
796 Self::Neg => write!(f, "-"),
797 }
798 }
799}
800
801impl BindKind {
802 pub fn token_str(&self) -> &'static str {
803 match self {
804 BindKind::At => "@",
805 BindKind::Pound => "#",
806 }
807 }
808}
809
810pub struct Punctuated<T, P> {
812 inner: Vec<(T, P)>,
813 last: Option<Box<T>>,
814}
815
816impl<T, P> From<Vec<(T, P)>> for Punctuated<T, P> {
817 fn from(inner: Vec<(T, P)>) -> Self {
818 Self { inner, last: None }
819 }
820}
821
822impl<T, P> Punctuated<T, P> {
823 pub fn len(&self) -> usize {
824 self.inner.len() + self.last.is_some() as usize
825 }
826
827 pub fn is_empty(&self) -> bool {
830 self.inner.len() == 0 && self.last.is_none()
831 }
832
833 pub fn push_value(&mut self, value: T) {
841 assert!(
842 self.empty_or_trailing(),
843 "Punctuated::push_value: cannot push value if Punctuated is missing trailing punctuation",
844 );
845
846 self.last = Some(Box::new(value));
847 }
848
849 pub fn empty_or_trailing(&self) -> bool {
854 self.last.is_none()
855 }
856
857 pub fn trailing_punct(&self) -> bool {
860 self.last.is_none() && !self.is_empty()
861 }
862
863 pub fn into_values(self) -> Vec<T> {
864 let mut v: Vec<T> = self.inner.into_iter().map(|(v, _)| v).collect();
865 if let Some(last) = self.last {
866 v.push(*last);
867 }
868 v
869 }
870}