flux_attrs_impl/
ast.rs

1use std::mem;
2
3use proc_macro2::{TokenStream, TokenTree};
4use quote::{ToTokens, TokenStreamExt, quote, quote_spanned};
5use syn::{
6    Attribute, Ident, Result, Token, Visibility, braced, bracketed,
7    ext::IdentExt,
8    parenthesized,
9    parse::{Parse, ParseStream, Peek, discouraged::Speculative},
10    punctuated::Punctuated,
11    token::{self, Mut, Paren},
12};
13
14use crate::{flux_tool_attrs, parse_inner, tokens_or_default};
15
16pub struct Items(Vec<Item>);
17
18#[derive(Debug)]
19pub enum Item {
20    Const(syn::ItemConst),
21    Struct(ItemStruct),
22    Enum(ItemEnum),
23    Use(syn::ItemUse),
24    Type(ItemType),
25    Fn(ItemFn),
26    Impl(ItemImpl),
27    Mod(ItemMod),
28    Trait(ItemTrait),
29}
30
31#[derive(Debug)]
32pub struct ItemMod {
33    pub attrs: Vec<Attribute>,
34    pub vis: Visibility,
35    pub unsafety: Option<Token![unsafe]>,
36    pub mod_token: Token![mod],
37    pub ident: Ident,
38    pub content: Option<(token::Brace, Vec<Item>)>,
39    pub semi: Option<Token![;]>,
40}
41
42#[derive(Debug)]
43pub struct ItemTrait {
44    pub attrs: Vec<Attribute>,
45    pub vis: Visibility,
46    pub unsafety: Option<Token![unsafe]>,
47    pub trait_token: Token![trait],
48    pub ident: Ident,
49    pub generics: Generics,
50    pub colon_token: Option<Token![:]>,
51    pub supertraits: Punctuated<syn::TypeParamBound, Token![+]>,
52    pub brace_token: token::Brace,
53    pub items: Vec<TraitItem>,
54}
55
56impl Parse for ItemTrait {
57    fn parse(input: ParseStream) -> Result<Self> {
58        let mut attrs = input.call(Attribute::parse_outer)?;
59        let vis: Visibility = input.parse()?;
60        let unsafety: Option<Token![unsafe]> = input.parse()?;
61        let trait_token: Token![trait] = input.parse()?;
62        let ident: Ident = input.parse()?;
63        let mut generics: Generics = input.parse()?;
64
65        let colon_token: Option<Token![:]> = input.parse()?;
66
67        let mut supertraits = Punctuated::new();
68        if colon_token.is_some() {
69            loop {
70                if input.peek(Token![where]) || input.peek(token::Brace) {
71                    break;
72                }
73                supertraits.push_value(input.parse()?);
74                if input.peek(Token![where]) || input.peek(token::Brace) {
75                    break;
76                }
77                supertraits.push_punct(input.parse()?);
78            }
79        }
80
81        generics.where_clause = input.parse()?;
82
83        let content;
84        let brace_token = braced!(content in input);
85        parse_inner(&content, &mut attrs)?;
86        let mut items = Vec::new();
87        while !content.is_empty() {
88            items.push(content.parse()?);
89        }
90
91        Ok(ItemTrait {
92            attrs,
93            vis,
94            unsafety,
95            trait_token,
96            ident,
97            generics,
98            colon_token,
99            supertraits,
100            brace_token,
101            items,
102        })
103    }
104}
105
106impl ToTokens for ItemTrait {
107    fn to_tokens(&self, tokens: &mut TokenStream) {
108        tokens.append_all(outer(&self.attrs));
109        #[cfg(flux_sysroot)]
110        for item in &self.items {
111            if let TraitItem::Reft(reft) = item {
112                reft.flux_tool_attr().to_tokens(tokens);
113            }
114        }
115        self.vis.to_tokens(tokens);
116        self.unsafety.to_tokens(tokens);
117        self.trait_token.to_tokens(tokens);
118        self.ident.to_tokens(tokens);
119        self.generics.to_tokens(tokens, Mode::Rust);
120        if !self.supertraits.is_empty() {
121            tokens_or_default(self.colon_token.as_ref(), tokens);
122            self.supertraits.to_tokens(tokens);
123        }
124        self.generics.where_clause.to_tokens(tokens);
125        self.brace_token.surround(tokens, |tokens| {
126            tokens.append_all(inner(&self.attrs));
127            tokens.append_all(&self.items);
128        });
129    }
130}
131
132#[derive(Debug)]
133pub enum TraitItem {
134    /// An associated constant within the definition of a trait.
135    Const(syn::TraitItemConst),
136
137    /// An associated function within the definition of a trait.
138    Fn(TraitItemFn),
139
140    /// An associated type within the definition of a trait.
141    Type(syn::TraitItemType),
142
143    /// An associated refinements within the definition of a trait.
144    Reft(TraitItemReft),
145}
146
147impl Parse for TraitItem {
148    fn parse(input: ParseStream) -> Result<Self> {
149        let mut attrs = input.call(Attribute::parse_outer)?;
150        flux_tool_attrs(&mut attrs);
151        let vis: Visibility = input.parse()?;
152        let ahead = input.fork();
153
154        let lookahead = ahead.lookahead1();
155        let mut item = if lookahead.peek(Token![fn]) || peek_signature(&ahead) {
156            input.parse().map(TraitItem::Fn)
157        } else if lookahead.peek(Token![const]) {
158            let const_token: Token![const] = ahead.parse()?;
159            let lookahead = ahead.lookahead1();
160            if lookahead.peek(Ident) || lookahead.peek(Token![_]) {
161                input.advance_to(&ahead);
162                let ident = input.call(Ident::parse_any)?;
163                let colon_token: Token![:] = input.parse()?;
164                let ty: syn::Type = input.parse()?;
165                let default = if let Some(eq_token) = input.parse::<Option<Token![=]>>()? {
166                    let expr: syn::Expr = input.parse()?;
167                    Some((eq_token, expr))
168                } else {
169                    None
170                };
171                let semi_token: Token![;] = input.parse()?;
172                Ok(TraitItem::Const(syn::TraitItemConst {
173                    attrs: Vec::new(),
174                    const_token,
175                    ident,
176                    generics: syn::Generics::default(),
177                    colon_token,
178                    ty,
179                    default,
180                    semi_token,
181                }))
182            } else if lookahead.peek(Token![async])
183                || lookahead.peek(Token![unsafe])
184                || lookahead.peek(Token![extern])
185                || lookahead.peek(Token![fn])
186            {
187                input.parse().map(TraitItem::Fn)
188            } else {
189                Err(lookahead.error())
190            }
191        } else if lookahead.peek(Token![type]) {
192            parse_trait_item_type(input)
193        } else if lookahead.peek(kw::reft) {
194            input.parse().map(TraitItem::Reft)
195        } else {
196            Err(lookahead.error())
197        }?;
198
199        if !matches!(vis, Visibility::Inherited) {
200            return Err(syn::Error::new_spanned(vis, "visibility qualifier not allowed here"));
201        }
202
203        let item_attrs = match &mut item {
204            TraitItem::Const(item) => &mut item.attrs,
205            TraitItem::Fn(item) => &mut item.attrs,
206            TraitItem::Type(item) => &mut item.attrs,
207            TraitItem::Reft(item) => &mut item.attrs,
208        };
209        attrs.append(item_attrs);
210        *item_attrs = attrs;
211        Ok(item)
212    }
213}
214
215impl ToTokens for TraitItem {
216    fn to_tokens(&self, tokens: &mut TokenStream) {
217        match self {
218            TraitItem::Const(item) => item.to_tokens(tokens),
219            TraitItem::Fn(item) => item.to_tokens(tokens),
220            TraitItem::Type(item) => item.to_tokens(tokens),
221            TraitItem::Reft(_) => {}
222        }
223    }
224}
225
226#[derive(Debug)]
227pub struct TraitItemFn {
228    pub attrs: Vec<Attribute>,
229    pub sig: Signature,
230    pub default: Option<Block>,
231    pub semi_token: Option<Token![;]>,
232}
233
234impl Parse for TraitItemFn {
235    fn parse(input: ParseStream) -> Result<Self> {
236        let attrs = input.call(Attribute::parse_outer)?;
237        let sig: Signature = input.parse()?;
238
239        let lookahead = input.lookahead1();
240        let (block, semi_token) = if lookahead.peek(token::Brace) {
241            let block = input.parse()?;
242            (Some(block), None)
243        } else if lookahead.peek(Token![;]) {
244            let semi_token: Token![;] = input.parse()?;
245            (None, Some(semi_token))
246        } else {
247            return Err(lookahead.error());
248        };
249
250        Ok(TraitItemFn { attrs, sig, default: block, semi_token })
251    }
252}
253
254impl ToTokens for TraitItemFn {
255    fn to_tokens(&self, tokens: &mut TokenStream) {
256        let TraitItemFn { attrs, sig, default, semi_token } = self;
257        #[cfg(flux_sysroot)]
258        {
259            let flux_sig = ToTokensFlux(sig);
260            quote!(#[flux_tool::sig(#flux_sig)]).to_tokens(tokens);
261        }
262        let rust_sig = ToTokensRust(sig);
263        quote! {
264            #(#attrs)*
265            #rust_sig #default #semi_token
266        }
267        .to_tokens(tokens);
268    }
269}
270
271#[derive(Debug)]
272#[cfg_attr(not(flux_sysroot), allow(dead_code))]
273pub struct TraitItemReft {
274    /// This is not actually used
275    pub attrs: Vec<Attribute>,
276    pub reft_token: kw::reft,
277    pub name: Ident,
278    pub paren_token: token::Paren,
279    pub params: TokenStream,
280    pub returns: TokenStream,
281    #[allow(dead_code)]
282    pub semi_token: Token![;],
283}
284
285impl TraitItemReft {
286    #[cfg(flux_sysroot)]
287    fn flux_tool_attr(&self) -> TokenStream {
288        quote! {
289            #[flux_tool::assoc(#self)]
290        }
291    }
292}
293
294impl Parse for TraitItemReft {
295    fn parse(input: ParseStream) -> Result<Self> {
296        let reft_token: kw::reft = input.parse()?;
297        let name: Ident = input.parse()?;
298        let content;
299        let paren_token = parenthesized!(content in input);
300        let params = content.parse()?;
301        let mut returns = TokenStream::new();
302        while !input.peek(Token![;]) {
303            returns.append(TokenTree::parse(input)?);
304        }
305        let semi_token: Token![;] = input.parse()?;
306        Ok(TraitItemReft {
307            attrs: vec![],
308            reft_token,
309            name,
310            paren_token,
311            params,
312            returns,
313            semi_token,
314        })
315    }
316}
317
318#[cfg(flux_sysroot)]
319impl ToTokens for TraitItemReft {
320    fn to_tokens(&self, tokens: &mut TokenStream) {
321        let TraitItemReft { reft_token, name, paren_token, params, returns, .. } = self;
322        quote_spanned!(reft_token.span=> fn).to_tokens(tokens);
323        name.to_tokens(tokens);
324        paren_token.surround(tokens, |tokens| {
325            params.to_tokens(tokens);
326        });
327        returns.to_tokens(tokens);
328    }
329}
330
331#[derive(Debug)]
332pub struct ItemFn {
333    pub attrs: Vec<Attribute>,
334    pub vis: Visibility,
335    pub sig: Signature,
336    pub block: Block,
337}
338
339#[derive(Debug)]
340pub struct Generics {
341    pub lt_token: Option<Token![<]>,
342    pub params: Punctuated<GenericParam, Token![,]>,
343    pub gt_token: Option<Token![>]>,
344    pub where_clause: Option<syn::WhereClause>,
345}
346
347impl Default for Generics {
348    fn default() -> Self {
349        Generics { lt_token: None, params: Punctuated::new(), gt_token: None, where_clause: None }
350    }
351}
352
353#[derive(Debug)]
354pub enum GenericParam {
355    /// A lifetime parameter: `'a: 'b + 'c + 'd`.
356    Lifetime(syn::LifetimeParam),
357
358    /// A generic type parameter: `T: Into<String>`.
359    Type(TypeParam),
360
361    /// A const generic parameter: `const LENGTH: usize`.
362    Const(syn::ConstParam),
363}
364
365#[derive(Debug)]
366pub struct TypeParam {
367    pub attrs: Vec<Attribute>,
368    pub ident: Ident,
369    pub as_token: Option<Token![as]>,
370    pub param_kind: ParamKind,
371    pub colon_token: Option<Token![:]>,
372    pub bounds: Punctuated<syn::TypeParamBound, Token![+]>,
373    // pub eq_token: Option<Token![=]>,
374    // pub default: Option<Type>,
375}
376
377#[derive(Debug)]
378pub enum ParamKind {
379    Type(Token![type]),
380    Base(kw::base),
381    Default,
382}
383
384impl ToTokens for ParamKind {
385    fn to_tokens(&self, tokens: &mut TokenStream) {
386        match self {
387            ParamKind::Type(t) => t.to_tokens(tokens),
388            ParamKind::Base(t) => t.to_tokens(tokens),
389            ParamKind::Default => {}
390        }
391    }
392}
393
394#[derive(Debug)]
395pub struct ItemStruct {
396    pub attrs: Vec<Attribute>,
397    pub vis: Visibility,
398    pub struct_token: Token![struct],
399    pub ident: Ident,
400    pub generics: Generics,
401    #[cfg_attr(not(flux_sysroot), allow(dead_code))]
402    pub refined_by: Option<RefinedBy>,
403    pub fields: Fields,
404    pub semi_token: Option<Token![;]>,
405}
406
407#[derive(Debug)]
408pub struct ItemEnum {
409    pub attrs: Vec<Attribute>,
410    pub vis: Visibility,
411    pub enum_token: Token![enum],
412    pub ident: Ident,
413    pub generics: Generics,
414    #[cfg_attr(not(flux_sysroot), allow(dead_code))]
415    pub refined_by: Option<RefinedBy>,
416    pub brace_token: token::Brace,
417    pub variants: Punctuated<Variant, Token![,]>,
418}
419
420#[derive(Debug)]
421pub struct Variant {
422    pub attrs: Vec<Attribute>,
423
424    /// Name of the variant.
425    pub ident: Ident,
426
427    /// Content stored in the variant.
428    pub fields: Fields,
429
430    /// Explicit discriminant: `Variant = 1`
431    pub discriminant: Option<(Token![=], syn::Expr)>,
432
433    #[cfg_attr(not(flux_sysroot), allow(dead_code))]
434    pub ret: Option<VariantRet>,
435}
436
437impl Variant {
438    #[cfg(flux_sysroot)]
439    fn flux_tool_attr(&self) -> TokenStream {
440        let variant = ToTokensFlux(self);
441        quote! {
442            #[flux_tool::variant(#variant)]
443        }
444    }
445}
446
447#[cfg(flux_sysroot)]
448impl ToTokens for ToTokensFlux<&Variant> {
449    fn to_tokens(&self, tokens: &mut TokenStream) {
450        let variant = &self.0;
451        variant
452            .fields
453            .to_tokens(tokens, |f, tokens| f.ty.to_tokens_inner(tokens, Mode::Flux));
454        if let Some(ret) = &variant.ret {
455            if !matches!(variant.fields, Fields::Unit) {
456                ret.arrow_token.to_tokens(tokens);
457            }
458            ret.path.to_tokens_inner(tokens, Mode::Flux);
459            ret.bracket_token.surround(tokens, |tokens| {
460                ret.indices.to_tokens(tokens);
461            });
462        }
463    }
464}
465
466#[cfg_attr(not(flux_sysroot), allow(dead_code))]
467#[derive(Debug)]
468pub struct VariantRet {
469    pub arrow_token: Option<Token![->]>,
470    pub path: Path,
471    pub bracket_token: token::Bracket,
472    pub indices: TokenStream,
473}
474
475#[derive(Debug)]
476pub struct RefinedBy {
477    pub _refined_by: Option<(kw::refined, kw::by)>,
478    pub _bracket_token: token::Bracket,
479    pub params: Punctuated<RefinedByParam, Token![,]>,
480}
481
482impl RefinedBy {
483    #[cfg(flux_sysroot)]
484    fn flux_tool_attr(&self) -> TokenStream {
485        quote! {
486            #[flux_tool::refined_by(#self)]
487        }
488    }
489}
490
491#[derive(Debug)]
492pub struct RefinedByParam {
493    pub ident: Ident,
494    pub colon_token: Token![:],
495    pub sort: Sort,
496}
497
498#[derive(Debug)]
499pub enum Fields {
500    /// Named fields of a struct or struct variant such as `Point { x: f64,
501    /// y: f64 }`.
502    Named(FieldsNamed),
503
504    /// Unnamed fields of a tuple struct or tuple variant such as `Some(T)`.
505    Unnamed(FieldsUnnamed),
506
507    /// Unit struct or unit variant such as `None`.
508    Unit,
509}
510
511impl Fields {
512    fn to_tokens(&self, tokens: &mut TokenStream, mut f: impl FnMut(&Field, &mut TokenStream)) {
513        match self {
514            Fields::Named(fields) => {
515                fields.brace_token.surround(tokens, |tokens| {
516                    for param in fields.named.pairs() {
517                        f(param.value(), tokens);
518                        param.punct().to_tokens(tokens);
519                    }
520                });
521            }
522            Fields::Unnamed(fields) => {
523                fields.paren_token.surround(tokens, |tokens| {
524                    for param in fields.unnamed.pairs() {
525                        f(param.value(), tokens);
526                        param.punct().to_tokens(tokens);
527                    }
528                });
529            }
530            Fields::Unit => {}
531        }
532    }
533}
534
535#[derive(Debug)]
536pub struct FieldsNamed {
537    pub brace_token: token::Brace,
538    pub named: Punctuated<Field, Token![,]>,
539}
540
541#[derive(Debug)]
542pub struct FieldsUnnamed {
543    pub paren_token: token::Paren,
544    pub unnamed: Punctuated<Field, Token![,]>,
545}
546
547#[derive(Debug)]
548pub struct Field {
549    pub attrs: Vec<Attribute>,
550
551    pub vis: Visibility,
552
553    pub _mutability: syn::FieldMutability,
554
555    /// Name of the field, if any.
556    ///
557    /// Fields of tuple structs have no names.
558    pub ident: Option<Ident>,
559
560    pub colon_token: Option<Token![:]>,
561
562    pub ty: Type,
563}
564
565impl Field {
566    fn parse_unnamed(input: ParseStream) -> Result<Self> {
567        Ok(Field {
568            attrs: input.call(Attribute::parse_outer)?,
569            vis: input.parse()?,
570            _mutability: syn::FieldMutability::None,
571            ident: None,
572            colon_token: None,
573            ty: input.parse()?,
574        })
575    }
576
577    fn parse_named(input: ParseStream) -> Result<Self> {
578        let attrs = input.call(Attribute::parse_outer)?;
579        let vis: Visibility = input.parse()?;
580
581        let ident = input.parse()?;
582        let colon_token: Token![:] = input.parse()?;
583        let ty = input.parse()?;
584        Ok(Field {
585            attrs,
586            vis,
587            _mutability: syn::FieldMutability::None,
588            ident: Some(ident),
589            colon_token: Some(colon_token),
590            ty,
591        })
592    }
593
594    #[cfg(flux_sysroot)]
595    fn flux_tool_attr(&self) -> TokenStream {
596        let flux_ty = ToTokensFlux(&self.ty);
597        quote! {
598            #[flux_tool::field(#flux_ty)]
599        }
600    }
601
602    fn to_tokens(&self, tokens: &mut TokenStream) {
603        tokens.append_all(&self.attrs);
604        self.vis.to_tokens(tokens);
605        self.ident.to_tokens(tokens);
606        self.colon_token.to_tokens(tokens);
607        self.ty.to_tokens_inner(tokens, Mode::Rust);
608    }
609}
610
611#[derive(Debug)]
612pub struct ItemType {
613    pub attrs: Vec<Attribute>,
614    pub vis: Visibility,
615    pub type_token: Token![type],
616    pub ident: Ident,
617    pub generics: Generics,
618    pub index_params: Option<IndexParams>,
619    pub eq_token: Token![=],
620    pub ty: Box<Type>,
621    pub semi_token: Token![;],
622}
623
624#[derive(Debug)]
625pub struct IndexParams {
626    pub bracket_token: token::Bracket,
627    pub params: Punctuated<ExistsParam, Token![,]>,
628}
629
630#[derive(Debug)]
631pub struct ItemImpl {
632    pub attrs: Vec<Attribute>,
633    pub impl_token: Token![impl],
634    pub generics: Generics,
635    pub trait_: Option<(syn::Path, Token![for])>,
636    /// The Self type of the impl.
637    pub self_ty: Box<syn::Type>,
638    pub brace_token: token::Brace,
639    pub items: Vec<ImplItem>,
640}
641
642#[derive(Debug)]
643pub enum ImplItem {
644    Fn(ImplItemFn),
645    Type(syn::ImplItemType),
646    Reft(ImplItemReft),
647}
648
649#[derive(Debug)]
650pub struct ImplItemFn {
651    pub attrs: Vec<Attribute>,
652    pub vis: Visibility,
653    pub sig: Signature,
654    pub block: Block,
655}
656
657impl Parse for ImplItemFn {
658    fn parse(input: ParseStream) -> Result<Self> {
659        Ok(ImplItemFn {
660            attrs: input.call(Attribute::parse_outer)?,
661            vis: input.parse()?,
662            sig: input.parse()?,
663            block: input.parse()?,
664        })
665    }
666}
667
668#[derive(Debug)]
669#[cfg_attr(not(flux_sysroot), allow(dead_code))]
670pub struct ImplItemReft {
671    /// This is not actually used
672    pub attrs: Vec<Attribute>,
673    pub reft_token: kw::reft,
674    pub name: Ident,
675    pub paren_token: token::Paren,
676    pub params: TokenStream,
677    pub returns: TokenStream,
678    pub block: Block,
679}
680
681impl ImplItemReft {
682    #[cfg(flux_sysroot)]
683    fn flux_tool_attr(&self) -> TokenStream {
684        quote! {
685            #[flux_tool::assoc(#self)]
686        }
687    }
688}
689
690impl Parse for ImplItemReft {
691    fn parse(input: ParseStream) -> Result<Self> {
692        let reft_token: kw::reft = input.parse()?;
693        let name: Ident = input.parse()?;
694        let content;
695        let paren_token = parenthesized!(content in input);
696        let params = content.parse()?;
697        let mut returns = TokenStream::new();
698        while !input.peek(token::Brace) {
699            returns.append(TokenTree::parse(input)?);
700        }
701        let block: Block = input.parse()?;
702        Ok(ImplItemReft { attrs: vec![], reft_token, name, paren_token, params, returns, block })
703    }
704}
705
706#[cfg(flux_sysroot)]
707impl ToTokens for ImplItemReft {
708    fn to_tokens(&self, tokens: &mut TokenStream) {
709        let ImplItemReft { reft_token, name, paren_token, params, returns, block, .. } = self;
710        quote_spanned!(reft_token.span=> fn).to_tokens(tokens);
711        name.to_tokens(tokens);
712        paren_token.surround(tokens, |tokens| {
713            params.to_tokens(tokens);
714        });
715        returns.to_tokens(tokens);
716        block.to_tokens(tokens);
717    }
718}
719
720#[derive(Debug)]
721pub struct Signature {
722    pub fn_token: Token![fn],
723    pub ident: Ident,
724    pub generics: Generics,
725    pub paren_token: Paren,
726    pub inputs: Punctuated<FnArg, Token![,]>,
727    pub output: ReturnType,
728    pub requires: Option<Requires>,
729    pub ensures: Option<Ensures>,
730}
731
732#[derive(Debug)]
733pub struct Ensures {
734    pub ensures_token: kw::ensures,
735    pub constraints: Punctuated<Constraint, Token![,]>,
736}
737
738#[derive(Debug)]
739pub struct Requires {
740    pub requires_token: kw::requires,
741    pub constraint: Expr,
742}
743
744#[derive(Debug)]
745pub enum Constraint {
746    Type { ident: Ident, colon_token: Token![:], ty: Box<Type> },
747    Expr(Expr),
748}
749
750#[derive(Debug)]
751pub enum FnArg {
752    StrgRef(StrgRef),
753    Typed(PatType),
754}
755
756#[derive(Debug)]
757pub struct PatType {
758    pub pat: Pat,
759    pub colon_token: Token![:],
760    pub ty: Type,
761    pub pred: Option<PatTypePredicate>,
762}
763
764#[derive(Debug)]
765pub enum Pat {
766    Ident(PatIdent),
767    Wild(Token![_]),
768}
769
770#[derive(Debug)]
771pub struct PatIdent {
772    pub mutability: Option<Token![mut]>,
773    pub ident: Ident,
774}
775
776#[derive(Debug)]
777pub struct PatTypePredicate {
778    pub brace_token: token::Brace,
779    pub pred: Expr,
780}
781
782#[derive(Debug)]
783pub struct StrgRef {
784    pub pat: Pat,
785    pub colon_token: Token![:],
786    pub and_token: Token![&],
787    pub strg_token: kw::strg,
788    pub ty: Box<Type>,
789}
790
791#[derive(Debug)]
792pub enum Sort {
793    BaseSort(BaseSort),
794    Func { input: FuncSortInput, arrow: Token![->], output: BaseSort },
795}
796
797#[derive(Debug)]
798pub enum FuncSortInput {
799    Parenthesized { paren_token: token::Paren, inputs: Punctuated<BaseSort, Token![,]> },
800    Single(BaseSort),
801}
802
803#[derive(Debug)]
804pub enum BaseSort {
805    BitVec(BitVecSort),
806    App(Ident, SortArguments),
807}
808
809#[derive(Debug)]
810pub struct BitVecSort {
811    pub bitvec_token: kw::bitvec,
812    pub lt_token: Token![<],
813    pub lit: syn::LitInt,
814    pub gt_token: Token![>],
815}
816
817#[derive(Debug)]
818pub enum SortArguments {
819    None,
820    AngleBracketed(AngleBracketedSortArgs),
821}
822
823#[derive(Debug)]
824pub struct AngleBracketedSortArgs {
825    pub lt_token: Token![<],
826    pub args: Punctuated<BaseSort, Token![,]>,
827    pub gt_token: Token![>],
828}
829
830#[derive(Debug)]
831pub enum Type {
832    Base(BaseType),
833    Indexed(TypeIndexed),
834    Exists(TypeExists),
835    GeneralExists(TypeGeneralExists),
836    Reference(TypeReference),
837    Constraint(TypeConstraint),
838    Array(TypeArray),
839    Tuple(TypeTuple),
840    Ptr(syn::TypePtr),
841}
842
843#[derive(Debug)]
844pub struct TypeTuple {
845    pub paren_token: token::Paren,
846    pub elems: Punctuated<Type, Token![,]>,
847}
848
849impl TypeTuple {
850    fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) {
851        self.paren_token.surround(tokens, |tokens| {
852            for elem in self.elems.pairs() {
853                elem.value().to_tokens_inner(tokens, mode);
854                elem.punct().to_tokens(tokens);
855            }
856        });
857    }
858}
859
860#[derive(Debug)]
861pub struct TypeIndexed {
862    pub bty: BaseType,
863    pub bracket_token: token::Bracket,
864    pub expr: Expr,
865}
866
867#[derive(Debug)]
868pub struct TypeExists {
869    pub bty: BaseType,
870    pub brace_token: token::Brace,
871    pub ident: Ident,
872    pub colon_token: Token![:],
873    pub expr: Expr,
874}
875
876#[derive(Debug)]
877pub struct TypeGeneralExists {
878    pub brace_token: token::Brace,
879    pub params: Punctuated<ExistsParam, Token![,]>,
880    pub dot_token: Token![.],
881    pub ty: Box<Type>,
882    pub or_token: Option<Token![|]>,
883    pub pred: Option<Expr>,
884}
885
886#[derive(Debug)]
887pub struct ExistsParam {
888    pub ident: Ident,
889    pub colon_token: Option<Token![:]>,
890    pub sort: Option<Ident>,
891}
892
893#[derive(Debug)]
894pub struct TypeReference {
895    pub and_token: Token![&],
896    pub lifetime: Option<syn::Lifetime>,
897    pub mutability: Option<Mut>,
898    pub elem: Box<Type>,
899}
900
901#[derive(Debug)]
902pub struct TypeConstraint {
903    pub brace_token: token::Brace,
904    pub ty: Box<Type>,
905    pub or_token: Token![|],
906    pub pred: Expr,
907}
908
909#[derive(Debug)]
910pub struct TypeArray {
911    pub bracket_token: token::Bracket,
912    pub ty: Box<Type>,
913    pub semi_token: Token![;],
914    pub len: TokenStream,
915}
916
917#[derive(Debug)]
918pub enum BaseType {
919    Path(Path),
920    Slice(TypeSlice),
921}
922
923#[derive(Debug)]
924pub struct Path {
925    pub segments: Punctuated<PathSegment, Token![::]>,
926}
927
928#[derive(Debug)]
929pub struct TypeSlice {
930    pub bracket_token: token::Bracket,
931    pub ty: Box<Type>,
932}
933
934#[derive(Debug)]
935pub struct PathSegment {
936    pub ident: Ident,
937    pub arguments: PathArguments,
938}
939
940#[derive(Debug)]
941pub enum PathArguments {
942    None,
943    AngleBracketed(AngleBracketedGenericArguments),
944}
945
946#[derive(Debug)]
947pub struct AngleBracketedGenericArguments {
948    pub lt_token: Token![<],
949    pub args: Punctuated<GenericArgument, Token![,]>,
950    pub gt_token: Token![>],
951}
952
953#[derive(Debug)]
954pub enum GenericArgument {
955    Type(Type),
956}
957
958#[derive(Debug)]
959pub enum ReturnType {
960    Default,
961    Type(Token![->], Box<Type>),
962}
963
964pub type Expr = TokenStream;
965
966#[derive(Debug)]
967pub struct Block {
968    pub brace_token: token::Brace,
969    pub stmts: TokenStream,
970}
971
972impl Parse for Items {
973    fn parse(input: ParseStream) -> Result<Self> {
974        let mut result = Vec::new();
975        while !input.is_empty() {
976            let value = input.parse()?;
977            result.push(value);
978        }
979        Ok(Self(result))
980    }
981}
982
983impl Parse for Item {
984    fn parse(input: ParseStream) -> Result<Self> {
985        let mut attrs = input.call(Attribute::parse_outer)?;
986        flux_tool_attrs(&mut attrs);
987        let ahead = input.fork();
988        let _: Visibility = ahead.parse()?;
989        let lookahead = ahead.lookahead1();
990        let mut item = if lookahead.peek(Token![fn]) {
991            Item::Fn(input.parse()?)
992        } else if lookahead.peek(Token![impl]) {
993            Item::Impl(input.parse()?)
994        } else if lookahead.peek(Token![mod]) {
995            Item::Mod(input.parse()?)
996        } else if lookahead.peek(Token![struct]) {
997            Item::Struct(input.parse()?)
998        } else if lookahead.peek(Token![enum]) {
999            Item::Enum(input.parse()?)
1000        } else if lookahead.peek(Token![use]) {
1001            Item::Use(input.parse()?)
1002        } else if lookahead.peek(Token![type]) {
1003            Item::Type(input.parse()?)
1004        } else if lookahead.peek(Token![trait]) {
1005            Item::Trait(input.parse()?)
1006        } else if lookahead.peek(Token![const]) {
1007            Item::Const(input.parse()?)
1008        } else {
1009            return Err(lookahead.error());
1010        };
1011
1012        item.replace_attrs(attrs);
1013        Ok(item)
1014    }
1015}
1016
1017impl Parse for ItemMod {
1018    fn parse(input: ParseStream) -> Result<Self> {
1019        let mut attrs = input.call(Attribute::parse_outer)?;
1020        let vis: Visibility = input.parse()?;
1021        let unsafety: Option<Token![unsafe]> = input.parse()?;
1022        let mod_token: Token![mod] = input.parse()?;
1023        let ident: Ident =
1024            if input.peek(Token![try]) { input.call(Ident::parse_any) } else { input.parse() }?;
1025
1026        let lookahead = input.lookahead1();
1027        if lookahead.peek(Token![;]) {
1028            Ok(ItemMod {
1029                attrs,
1030                vis,
1031                unsafety,
1032                mod_token,
1033                ident,
1034                content: None,
1035                semi: Some(input.parse()?),
1036            })
1037        } else if lookahead.peek(token::Brace) {
1038            let content;
1039            let brace_token = braced!(content in input);
1040            parse_inner(&content, &mut attrs)?;
1041
1042            let mut items = Vec::new();
1043            while !content.is_empty() {
1044                items.push(content.parse()?);
1045            }
1046
1047            Ok(ItemMod {
1048                attrs,
1049                vis,
1050                unsafety,
1051                mod_token,
1052                ident,
1053                content: Some((brace_token, items)),
1054                semi: None,
1055            })
1056        } else {
1057            Err(lookahead.error())
1058        }
1059    }
1060}
1061
1062impl Parse for ItemStruct {
1063    fn parse(input: ParseStream) -> Result<Self> {
1064        let mut attrs = input.call(Attribute::parse_outer)?;
1065        flux_tool_attrs(&mut attrs);
1066        let vis = input.parse::<Visibility>()?;
1067        let struct_token = input.parse::<Token![struct]>()?;
1068        let ident = input.parse::<Ident>()?;
1069        let generics = input.parse::<Generics>()?;
1070        let refined_by = parse_opt_refined_by(input)?;
1071        let (where_clause, fields, semi_token) = data_struct(input)?;
1072        Ok(ItemStruct {
1073            attrs,
1074            vis,
1075            struct_token,
1076            ident,
1077            generics: Generics { where_clause, ..generics },
1078            refined_by,
1079            fields,
1080            semi_token,
1081        })
1082    }
1083}
1084
1085impl Parse for Generics {
1086    fn parse(input: ParseStream) -> Result<Self> {
1087        if !input.peek(Token![<]) {
1088            return Ok(Generics::default());
1089        }
1090
1091        let lt_token: Token![<] = input.parse()?;
1092
1093        let mut params = Punctuated::new();
1094        loop {
1095            if input.peek(Token![>]) {
1096                break;
1097            }
1098
1099            let attrs = input.call(Attribute::parse_outer)?;
1100            let lookahead = input.lookahead1();
1101            if lookahead.peek(syn::Lifetime) {
1102                params.push_value(GenericParam::Lifetime(syn::LifetimeParam {
1103                    attrs,
1104                    ..input.parse()?
1105                }));
1106            } else if lookahead.peek(Ident) {
1107                params.push_value(GenericParam::Type(TypeParam { attrs, ..input.parse()? }));
1108            } else if lookahead.peek(Token![const]) {
1109                params.push_value(GenericParam::Const(syn::ConstParam { attrs, ..input.parse()? }));
1110            } else if input.peek(Token![_]) {
1111                params.push_value(GenericParam::Type(TypeParam {
1112                    attrs,
1113                    ident: input.call(Ident::parse_any)?,
1114                    as_token: None,
1115                    param_kind: ParamKind::Default,
1116                    colon_token: None,
1117                    bounds: Punctuated::new(),
1118                    // eq_token: None,
1119                    // default: None,
1120                }));
1121            } else {
1122                return Err(lookahead.error());
1123            }
1124
1125            if input.peek(Token![>]) {
1126                break;
1127            }
1128            let punct = input.parse()?;
1129            params.push_punct(punct);
1130        }
1131
1132        let gt_token: Token![>] = input.parse()?;
1133
1134        Ok(Generics {
1135            lt_token: Some(lt_token),
1136            params,
1137            gt_token: Some(gt_token),
1138            where_clause: None,
1139        })
1140    }
1141}
1142
1143fn opt_parse_where_clause_in_signature(input: ParseStream) -> Result<Option<syn::WhereClause>> {
1144    if input.peek(Token![where]) {
1145        parse_where_clause_in_signature(input).map(Some)
1146    } else {
1147        Ok(None)
1148    }
1149}
1150
1151fn parse_where_clause_in_signature(input: ParseStream) -> Result<syn::WhereClause> {
1152    Ok(syn::WhereClause {
1153        where_token: input.parse()?,
1154        predicates: {
1155            let mut predicates = Punctuated::new();
1156            loop {
1157                if input.is_empty()
1158                    || input.peek(token::Brace)
1159                    || input.peek(Token![,])
1160                    || input.peek(Token![;])
1161                    || input.peek(Token![:]) && !input.peek(Token![::])
1162                    || input.peek(Token![=])
1163                    || input.peek(kw::requires)
1164                    || input.peek(kw::ensures)
1165                {
1166                    break;
1167                }
1168                let value = input.parse()?;
1169                predicates.push_value(value);
1170                if !input.peek(Token![,]) {
1171                    break;
1172                }
1173                let punct = input.parse()?;
1174                predicates.push_punct(punct);
1175            }
1176            predicates
1177        },
1178    })
1179}
1180
1181impl Parse for GenericParam {
1182    fn parse(input: ParseStream) -> Result<Self> {
1183        let attrs = input.call(Attribute::parse_outer)?;
1184
1185        let lookahead = input.lookahead1();
1186        if lookahead.peek(Ident) {
1187            Ok(GenericParam::Type(TypeParam { attrs, ..input.parse()? }))
1188        } else if lookahead.peek(syn::Lifetime) {
1189            Ok(GenericParam::Lifetime(syn::LifetimeParam { attrs, ..input.parse()? }))
1190        } else if lookahead.peek(Token![const]) {
1191            Ok(GenericParam::Const(syn::ConstParam { attrs, ..input.parse()? }))
1192        } else {
1193            Err(lookahead.error())
1194        }
1195    }
1196}
1197
1198impl Parse for TypeParam {
1199    fn parse(input: ParseStream) -> Result<Self> {
1200        let attrs = input.call(Attribute::parse_outer)?;
1201        let ident: Ident = input.parse()?;
1202
1203        let as_token: Option<Token![as]> = input.parse()?;
1204        let mut param_kind = ParamKind::Default;
1205        if as_token.is_some() {
1206            param_kind = input.parse()?;
1207        }
1208
1209        let colon_token: Option<Token![:]> = input.parse()?;
1210
1211        let mut bounds = Punctuated::new();
1212        if colon_token.is_some() {
1213            loop {
1214                if input.peek(Token![,]) || input.peek(Token![>]) || input.peek(Token![=]) {
1215                    break;
1216                }
1217                let value: syn::TypeParamBound = input.parse()?;
1218                bounds.push_value(value);
1219                if !input.peek(Token![+]) {
1220                    break;
1221                }
1222                let punct: Token![+] = input.parse()?;
1223                bounds.push_punct(punct);
1224            }
1225        }
1226        // let eq_token: Option<Token![=]> = input.parse()?;
1227        // let default = if eq_token.is_some() { Some(input.parse::<Type>()?) } else { None };
1228
1229        Ok(TypeParam {
1230            attrs,
1231            ident,
1232            as_token,
1233            param_kind,
1234            colon_token,
1235            bounds,
1236            // eq_token,
1237            // default,
1238        })
1239    }
1240}
1241
1242impl Parse for ParamKind {
1243    fn parse(input: ParseStream) -> Result<Self> {
1244        let lookahead = input.lookahead1();
1245        if lookahead.peek(Token![type]) {
1246            input.parse().map(ParamKind::Type)
1247        } else if lookahead.peek(kw::base) {
1248            input.parse().map(ParamKind::Base)
1249        } else {
1250            Err(lookahead.error())
1251        }
1252    }
1253}
1254
1255impl Parse for ItemEnum {
1256    fn parse(input: ParseStream) -> Result<Self> {
1257        let mut attrs = input.call(Attribute::parse_outer)?;
1258        flux_tool_attrs(&mut attrs);
1259        let vis = input.parse::<Visibility>()?;
1260        let enum_token = input.parse::<Token![enum]>()?;
1261        let ident = input.parse::<Ident>()?;
1262        let generics = input.parse::<Generics>()?;
1263        let refined_by = parse_opt_refined_by(input)?;
1264        let (where_clause, brace_token, variants) = data_enum(input)?;
1265        Ok(ItemEnum {
1266            attrs,
1267            vis,
1268            enum_token,
1269            ident,
1270            generics: Generics { where_clause, ..generics },
1271            refined_by,
1272            brace_token,
1273            variants,
1274        })
1275    }
1276}
1277
1278fn parse_opt_refined_by(input: ParseStream) -> Result<Option<RefinedBy>> {
1279    if input.peek(kw::refined) || input.peek(token::Bracket) {
1280        input.parse().map(Some)
1281    } else {
1282        Ok(None)
1283    }
1284}
1285
1286impl Parse for RefinedBy {
1287    fn parse(input: ParseStream) -> Result<Self> {
1288        let refined_by =
1289            if input.peek(kw::refined) { Some((input.parse()?, input.parse()?)) } else { None };
1290        let content;
1291        Ok(RefinedBy {
1292            _refined_by: refined_by,
1293            _bracket_token: bracketed!(content in input),
1294            params: Punctuated::parse_terminated(&content)?,
1295        })
1296    }
1297}
1298
1299impl Parse for RefinedByParam {
1300    fn parse(input: ParseStream) -> Result<Self> {
1301        Ok(RefinedByParam {
1302            ident: input.parse()?,
1303            colon_token: input.parse()?,
1304            sort: input.parse()?,
1305        })
1306    }
1307}
1308
1309impl Parse for Sort {
1310    fn parse(input: ParseStream) -> Result<Self> {
1311        if input.peek(token::Paren) {
1312            let content;
1313            let input_sort = FuncSortInput::Parenthesized {
1314                paren_token: parenthesized!(content in input),
1315                inputs: content.parse_terminated(BaseSort::parse, Token![,])?,
1316            };
1317            Ok(Sort::Func { input: input_sort, arrow: input.parse()?, output: input.parse()? })
1318        } else {
1319            let sort: BaseSort = input.parse()?;
1320            if input.peek(Token![->]) {
1321                Ok(Sort::Func {
1322                    input: FuncSortInput::Single(sort),
1323                    arrow: input.parse()?,
1324                    output: input.parse()?,
1325                })
1326            } else {
1327                Ok(Sort::BaseSort(sort))
1328            }
1329        }
1330    }
1331}
1332
1333impl Parse for BaseSort {
1334    fn parse(input: ParseStream) -> Result<Self> {
1335        if input.peek(kw::bitvec) {
1336            Ok(BaseSort::BitVec(BitVecSort {
1337                bitvec_token: input.parse()?,
1338                lt_token: input.parse()?,
1339                lit: input.parse()?,
1340                gt_token: input.parse()?,
1341            }))
1342        } else {
1343            let ident = input.parse()?;
1344            let arguments = if input.peek(Token![<]) && !input.peek(Token![<=]) {
1345                SortArguments::AngleBracketed(input.parse()?)
1346            } else {
1347                SortArguments::None
1348            };
1349            Ok(BaseSort::App(ident, arguments))
1350        }
1351    }
1352}
1353
1354impl Parse for AngleBracketedSortArgs {
1355    fn parse(input: ParseStream) -> Result<Self> {
1356        Ok(AngleBracketedSortArgs {
1357            lt_token: input.parse()?,
1358            args: parse_until(input, BaseSort::parse, Token![,], Token![>])?,
1359            gt_token: input.parse()?,
1360        })
1361    }
1362}
1363
1364fn data_enum(
1365    input: ParseStream,
1366) -> Result<(Option<syn::WhereClause>, token::Brace, Punctuated<Variant, Token![,]>)> {
1367    let where_clause = input.parse()?;
1368
1369    let content;
1370    let brace = braced!(content in input);
1371    let variants = content.parse_terminated(Variant::parse, Token![,])?;
1372
1373    Ok((where_clause, brace, variants))
1374}
1375
1376impl Parse for Variant {
1377    fn parse(input: ParseStream) -> Result<Self> {
1378        let attrs = input.call(Attribute::parse_outer)?;
1379        let _visibility: Visibility = input.parse()?;
1380        let ident: Ident = input.parse()?;
1381        let fields = if input.peek(token::Brace) {
1382            Fields::Named(input.parse()?)
1383        } else if input.peek(token::Paren) {
1384            Fields::Unnamed(input.parse()?)
1385        } else {
1386            Fields::Unit
1387        };
1388        let discriminant = if input.peek(Token![=]) {
1389            let eq_token: Token![=] = input.parse()?;
1390            let discriminant: syn::Expr = input.parse()?;
1391            Some((eq_token, discriminant))
1392        } else {
1393            None
1394        };
1395        let ret = parse_opt_variant_ret(input)?;
1396        Ok(Variant { attrs, ident, fields, discriminant, ret })
1397    }
1398}
1399
1400fn parse_opt_variant_ret(input: ParseStream) -> Result<Option<VariantRet>> {
1401    if input.peek(Token![->]) { input.parse().map(Some) } else { Ok(None) }
1402}
1403
1404impl Parse for VariantRet {
1405    fn parse(input: ParseStream) -> Result<Self> {
1406        let mut indices = TokenStream::new();
1407        let content;
1408        Ok(VariantRet {
1409            arrow_token: input.parse()?,
1410            path: input.parse()?,
1411            bracket_token: bracketed!(content in input),
1412            indices: {
1413                loop {
1414                    if content.is_empty() {
1415                        break;
1416                    }
1417                    let tt: TokenTree = content.parse()?;
1418                    indices.append(tt);
1419                }
1420                indices
1421            },
1422        })
1423    }
1424}
1425
1426fn data_struct(
1427    input: ParseStream,
1428) -> Result<(Option<syn::WhereClause>, Fields, Option<Token![;]>)> {
1429    let mut lookahead = input.lookahead1();
1430    let mut where_clause = None;
1431    if lookahead.peek(Token![where]) {
1432        where_clause = Some(input.parse()?);
1433        lookahead = input.lookahead1();
1434    }
1435
1436    if where_clause.is_none() && lookahead.peek(token::Paren) {
1437        let fields = input.parse()?;
1438
1439        lookahead = input.lookahead1();
1440        if lookahead.peek(Token![where]) {
1441            where_clause = Some(input.parse()?);
1442            lookahead = input.lookahead1();
1443        }
1444
1445        if lookahead.peek(Token![;]) {
1446            let semi = input.parse()?;
1447            Ok((where_clause, Fields::Unnamed(fields), Some(semi)))
1448        } else {
1449            Err(lookahead.error())
1450        }
1451    } else if lookahead.peek(token::Brace) {
1452        let fields = input.parse()?;
1453        Ok((where_clause, Fields::Named(fields), None))
1454    } else if lookahead.peek(Token![;]) {
1455        let semi = input.parse()?;
1456        Ok((where_clause, Fields::Unit, Some(semi)))
1457    } else {
1458        Err(lookahead.error())
1459    }
1460}
1461
1462impl Parse for FieldsUnnamed {
1463    fn parse(input: ParseStream) -> Result<Self> {
1464        let content;
1465        Ok(FieldsUnnamed {
1466            paren_token: parenthesized!(content in input),
1467            unnamed: content.parse_terminated(Field::parse_unnamed, Token![,])?,
1468        })
1469    }
1470}
1471
1472impl Parse for FieldsNamed {
1473    fn parse(input: ParseStream) -> Result<Self> {
1474        let content;
1475        Ok(FieldsNamed {
1476            brace_token: braced!(content in input),
1477            named: content.parse_terminated(Field::parse_named, Token![,])?,
1478        })
1479    }
1480}
1481
1482impl Parse for ItemFn {
1483    fn parse(input: ParseStream) -> Result<Self> {
1484        Ok(ItemFn {
1485            attrs: input.call(Attribute::parse_outer)?,
1486            vis: input.parse()?,
1487            sig: input.parse()?,
1488            block: input.parse()?,
1489        })
1490    }
1491}
1492
1493impl Parse for ItemType {
1494    fn parse(input: ParseStream) -> Result<Self> {
1495        Ok(ItemType {
1496            attrs: input.call(Attribute::parse_outer)?,
1497            vis: input.parse()?,
1498            type_token: input.parse()?,
1499            ident: input.parse()?,
1500            generics: input.parse()?,
1501            index_params: parse_index_params(input)?,
1502            eq_token: input.parse()?,
1503            ty: input.parse()?,
1504            semi_token: input.parse()?,
1505        })
1506    }
1507}
1508
1509fn parse_index_params(input: ParseStream) -> Result<Option<IndexParams>> {
1510    if input.peek(token::Bracket) {
1511        let content;
1512        Ok(Some(IndexParams {
1513            bracket_token: bracketed!(content in input),
1514            params: Punctuated::parse_terminated(&content)?,
1515        }))
1516    } else {
1517        Ok(None)
1518    }
1519}
1520
1521impl Parse for ItemImpl {
1522    fn parse(input: ParseStream) -> Result<Self> {
1523        let content;
1524        let attrs = input.call(Attribute::parse_outer)?;
1525        let impl_token = input.parse()?;
1526        let mut generics: Generics = input.parse()?;
1527
1528        let mut first_ty = input.parse()?;
1529
1530        let trait_;
1531        let self_ty;
1532        if input.peek(Token![for]) {
1533            let for_token: Token![for] = input.parse()?;
1534            let mut first_ty_ref = &first_ty;
1535            while let syn::Type::Group(ty) = first_ty_ref {
1536                first_ty_ref = &ty.elem;
1537            }
1538            if let syn::Type::Path(syn::TypePath { qself: None, .. }) = first_ty_ref {
1539                while let syn::Type::Group(ty) = first_ty {
1540                    first_ty = *ty.elem;
1541                }
1542                if let syn::Type::Path(syn::TypePath { qself: None, path }) = first_ty {
1543                    trait_ = Some((path, for_token));
1544                } else {
1545                    unreachable!();
1546                }
1547            } else {
1548                return Err(syn::Error::new_spanned(first_ty_ref, "expected trait path"));
1549            }
1550            self_ty = input.parse()?;
1551        } else {
1552            trait_ = None;
1553            self_ty = first_ty;
1554        }
1555        generics.where_clause = input.parse()?;
1556        Ok(ItemImpl {
1557            attrs,
1558            impl_token,
1559            generics,
1560            self_ty: Box::new(self_ty),
1561            trait_,
1562            brace_token: braced!(content in input),
1563            items: {
1564                let mut items = Vec::new();
1565                while !content.is_empty() {
1566                    let value = content.parse()?;
1567                    items.push(value);
1568                }
1569                items
1570            },
1571        })
1572    }
1573}
1574
1575impl ImplItem {
1576    fn replace_attrs(&mut self, new: Vec<Attribute>) -> Vec<Attribute> {
1577        match self {
1578            ImplItem::Fn(ImplItemFn { attrs, .. })
1579            | ImplItem::Type(syn::ImplItemType { attrs, .. })
1580            | ImplItem::Reft(ImplItemReft { attrs, .. }) => mem::replace(attrs, new),
1581        }
1582    }
1583}
1584
1585impl Parse for ImplItem {
1586    fn parse(input: ParseStream) -> Result<Self> {
1587        let mut attrs = input.call(Attribute::parse_outer)?;
1588        flux_tool_attrs(&mut attrs);
1589        let ahead = input.fork();
1590        let _: Visibility = ahead.parse()?;
1591        let lookahead = ahead.lookahead1();
1592        let mut item = if lookahead.peek(Token![fn]) || peek_signature(&ahead) {
1593            ImplItem::Fn(input.parse()?)
1594        } else if lookahead.peek(Token![type]) {
1595            ImplItem::Type(input.parse()?)
1596        } else if lookahead.peek(kw::reft) {
1597            ImplItem::Reft(input.parse()?)
1598        } else {
1599            return Err(lookahead.error());
1600        };
1601        item.replace_attrs(attrs);
1602        Ok(item)
1603    }
1604}
1605
1606impl Parse for Signature {
1607    fn parse(input: ParseStream) -> Result<Self> {
1608        let content;
1609        let fn_token = input.parse()?;
1610        let ident = input.parse()?;
1611        let mut generics: Generics = input.parse()?;
1612        let paren_token = parenthesized!(content in input);
1613        let inputs = content.parse_terminated(FnArg::parse, Token![,])?;
1614        let output = input.parse()?;
1615        generics.where_clause = opt_parse_where_clause_in_signature(input)?;
1616        let requires = parse_requires(input)?;
1617        let ensures = parse_ensures(input)?;
1618        Ok(Signature { fn_token, ident, generics, paren_token, inputs, output, requires, ensures })
1619    }
1620}
1621
1622fn parse_requires(input: ParseStream) -> Result<Option<Requires>> {
1623    if !input.peek(kw::requires) {
1624        return Ok(None);
1625    }
1626
1627    let requires_token = input.parse()?;
1628    let mut constraint = TokenStream::new();
1629    while !(input.is_empty() || input.peek(kw::ensures) || input.peek(token::Brace)) {
1630        let tt: TokenTree = input.parse()?;
1631        constraint.append(tt);
1632    }
1633    Ok(Some(Requires { requires_token, constraint }))
1634}
1635
1636fn parse_ensures(input: ParseStream) -> Result<Option<Ensures>> {
1637    if input.peek(kw::ensures) {
1638        Ok(Some(Ensures {
1639            ensures_token: input.parse()?,
1640            constraints: parse_until(input, Constraint::parse, Token![,], token::Brace)?,
1641        }))
1642    } else {
1643        Ok(None)
1644    }
1645}
1646
1647impl Parse for Constraint {
1648    fn parse(input: ParseStream) -> Result<Self> {
1649        let mut expr = TokenStream::new();
1650
1651        if input.peek(Ident) || input.peek(Token![self]) {
1652            let ident = parse_ident_or_self(input)?;
1653            if input.peek(Token![:]) {
1654                return Ok(Constraint::Type {
1655                    ident,
1656                    colon_token: input.parse()?,
1657                    ty: input.parse()?,
1658                });
1659            }
1660            expr.append(ident);
1661        }
1662
1663        while !(input.is_empty() || input.peek(Token![,]) || input.peek(token::Brace)) {
1664            let tt: TokenTree = input.parse()?;
1665            expr.append(tt);
1666        }
1667        Ok(Constraint::Expr(expr))
1668    }
1669}
1670
1671impl Parse for FnArg {
1672    fn parse(input: ParseStream) -> Result<Self> {
1673        let pat = input.parse()?;
1674        let colon_token = input.parse()?;
1675        let fn_arg = if input.peek(Token![&]) && input.peek2(kw::strg) {
1676            let and_token = input.parse()?;
1677            let strg_token = input.parse()?;
1678            let ty = input.parse()?;
1679            FnArg::StrgRef(StrgRef { pat, colon_token, and_token, strg_token, ty })
1680        } else if input.peek(Ident) {
1681            let bty: BaseType = input.parse()?;
1682            let mut pred = None;
1683            let ty = if input.peek(token::Bracket) {
1684                let content;
1685                Type::Indexed(TypeIndexed {
1686                    bty,
1687                    bracket_token: bracketed!(content in input),
1688                    expr: content.parse()?,
1689                })
1690            } else if input.peek(token::Brace) {
1691                let content;
1692                let brace_token = braced!(content in input);
1693                if content.peek(Ident) && content.peek2(Token![:]) {
1694                    Type::Exists(TypeExists {
1695                        bty,
1696                        brace_token,
1697                        ident: content.parse()?,
1698                        colon_token: content.parse()?,
1699                        expr: content.parse()?,
1700                    })
1701                } else {
1702                    pred = Some(PatTypePredicate { brace_token, pred: content.parse()? });
1703                    Type::Base(bty)
1704                }
1705            } else {
1706                Type::Base(bty)
1707            };
1708            FnArg::Typed(PatType { pat, colon_token, ty, pred })
1709        } else {
1710            FnArg::Typed(PatType { pat, colon_token, ty: input.parse()?, pred: None })
1711        };
1712        Ok(fn_arg)
1713    }
1714}
1715
1716impl Parse for Pat {
1717    fn parse(input: ParseStream) -> Result<Self> {
1718        let pat = if input.peek(Token![_]) {
1719            Pat::Wild(input.parse()?)
1720        } else {
1721            Pat::Ident(PatIdent { mutability: input.parse()?, ident: parse_ident_or_self(input)? })
1722        };
1723        Ok(pat)
1724    }
1725}
1726
1727impl Parse for ReturnType {
1728    fn parse(input: ParseStream) -> Result<Self> {
1729        if input.peek(Token![->]) {
1730            Ok(ReturnType::Type(input.parse()?, input.parse()?))
1731        } else {
1732            Ok(ReturnType::Default)
1733        }
1734    }
1735}
1736
1737impl Parse for Type {
1738    fn parse(input: ParseStream) -> Result<Self> {
1739        let ty = if input.peek(Token![&]) {
1740            Type::Reference(input.parse()?)
1741        } else if input.peek(token::Brace) {
1742            let content;
1743            let brace_token = braced!(content in input);
1744            if content.peek(Ident)
1745                && (content.peek2(Token![:])
1746                    || content.peek2(Token![,])
1747                    || content.peek2(Token![.]))
1748            {
1749                let params = parse_until(&content, ExistsParam::parse, Token![,], Token![.])?;
1750                let dot_token = content.parse()?;
1751                let ty = content.parse()?;
1752                let mut or_token = None;
1753                let mut pred = None;
1754                if content.peek(Token![|]) {
1755                    or_token = Some(content.parse()?);
1756                    pred = Some(content.parse()?);
1757                }
1758                Type::GeneralExists(TypeGeneralExists {
1759                    brace_token,
1760                    params,
1761                    dot_token,
1762                    ty,
1763                    or_token,
1764                    pred,
1765                })
1766            } else {
1767                Type::Constraint(TypeConstraint {
1768                    brace_token,
1769                    ty: content.parse()?,
1770                    or_token: content.parse()?,
1771                    pred: content.parse()?,
1772                })
1773            }
1774        } else if input.peek(token::Bracket) {
1775            let content;
1776            let bracket_token = bracketed!(content in input);
1777            let ty = content.parse()?;
1778            if content.peek(Token![;]) {
1779                Type::Array(TypeArray {
1780                    bracket_token,
1781                    ty,
1782                    semi_token: content.parse()?,
1783                    len: content.parse()?,
1784                })
1785            } else {
1786                parse_rty(input, BaseType::Slice(TypeSlice { bracket_token, ty }))?
1787            }
1788        } else if input.peek(token::Paren) {
1789            Type::Tuple(input.parse()?)
1790        } else if input.peek(Token![*]) {
1791            Type::Ptr(input.parse()?)
1792        } else {
1793            parse_rty(input, input.parse()?)?
1794        };
1795        Ok(ty)
1796    }
1797}
1798
1799impl Parse for TypeTuple {
1800    fn parse(input: ParseStream) -> Result<Self> {
1801        let content;
1802        Ok(TypeTuple {
1803            paren_token: parenthesized!(content in input),
1804            elems: content.parse_terminated(Type::parse, Token![,])?,
1805        })
1806    }
1807}
1808
1809fn parse_rty(input: ParseStream, bty: BaseType) -> Result<Type> {
1810    let ty = if input.peek(token::Bracket) {
1811        let content;
1812        Type::Indexed(TypeIndexed {
1813            bty,
1814            bracket_token: bracketed!(content in input),
1815            expr: content.parse()?,
1816        })
1817    } else if input.peek(token::Brace) {
1818        let ahead = input.fork();
1819        let mut content;
1820        braced!(content in ahead);
1821        if content.peek(Ident) && content.peek2(Token![:]) {
1822            Type::Exists(TypeExists {
1823                bty,
1824                brace_token: braced!(content in input),
1825                ident: content.parse()?,
1826                colon_token: content.parse()?,
1827                expr: content.parse()?,
1828            })
1829        } else {
1830            Type::Base(bty)
1831        }
1832    } else {
1833        Type::Base(bty)
1834    };
1835    Ok(ty)
1836}
1837
1838impl Parse for TypeReference {
1839    fn parse(input: ParseStream) -> Result<Self> {
1840        Ok(TypeReference {
1841            and_token: input.parse()?,
1842            lifetime: input.parse()?,
1843            mutability: input.parse()?,
1844            elem: input.parse()?,
1845        })
1846    }
1847}
1848
1849impl Parse for BaseType {
1850    fn parse(input: ParseStream) -> Result<Self> {
1851        if input.peek(token::Bracket) {
1852            let content;
1853            Ok(BaseType::Slice(TypeSlice {
1854                bracket_token: bracketed!(content in input),
1855                ty: content.parse()?,
1856            }))
1857        } else {
1858            Ok(BaseType::Path(input.parse()?))
1859        }
1860    }
1861}
1862
1863impl Parse for Path {
1864    fn parse(input: ParseStream) -> Result<Self> {
1865        let mut segments = Punctuated::new();
1866        segments.push_value(input.parse()?);
1867        while input.peek(Token![::]) {
1868            segments.push_punct(input.parse()?);
1869            segments.push_value(input.parse()?);
1870        }
1871        Ok(Path { segments })
1872    }
1873}
1874
1875impl Parse for PathSegment {
1876    fn parse(input: ParseStream) -> Result<Self> {
1877        let ident =
1878            if input.peek(Token![Self]) { input.call(Ident::parse_any)? } else { input.parse()? };
1879        let arguments = if input.peek(Token![<]) && !input.peek(Token![<=]) {
1880            PathArguments::AngleBracketed(input.parse()?)
1881        } else {
1882            PathArguments::None
1883        };
1884        Ok(PathSegment { ident, arguments })
1885    }
1886}
1887
1888impl Parse for AngleBracketedGenericArguments {
1889    fn parse(input: ParseStream) -> Result<Self> {
1890        Ok(AngleBracketedGenericArguments {
1891            lt_token: input.parse()?,
1892            args: parse_until(input, GenericArgument::parse, Token![,], Token![>])?,
1893            gt_token: input.parse()?,
1894        })
1895    }
1896}
1897
1898impl Parse for GenericArgument {
1899    fn parse(input: ParseStream) -> Result<Self> {
1900        Ok(GenericArgument::Type(input.parse()?))
1901    }
1902}
1903
1904impl Parse for ExistsParam {
1905    fn parse(input: ParseStream) -> Result<Self> {
1906        let ident = input.parse()?;
1907        let mut colon_token = None;
1908        let mut sort = None;
1909        if input.peek(Token![:]) {
1910            colon_token = Some(input.parse()?);
1911            sort = Some(input.parse()?);
1912        }
1913        Ok(ExistsParam { ident, colon_token, sort })
1914    }
1915}
1916
1917impl Parse for Block {
1918    fn parse(input: ParseStream) -> Result<Self> {
1919        let content;
1920        Ok(Block { brace_token: braced!(content in input), stmts: content.parse()? })
1921    }
1922}
1923
1924fn parse_until<T: Parse, P1: Peek, P2: Peek>(
1925    input: ParseStream,
1926    parser: fn(ParseStream) -> Result<T>,
1927    sep: P1,
1928    end: P2,
1929) -> Result<Punctuated<T, P1::Token>>
1930where
1931    P1::Token: Parse,
1932{
1933    let _ = sep;
1934    let mut params = Punctuated::new();
1935    loop {
1936        if input.peek(end) {
1937            return Ok(params);
1938        }
1939        params.push_value(parser(input)?);
1940        if input.peek(end) {
1941            return Ok(params);
1942        }
1943        params.push_punct(input.parse()?);
1944    }
1945}
1946
1947fn parse_ident_or_self(input: ParseStream) -> Result<Ident> {
1948    if input.peek(Token![self]) { input.call(Ident::parse_any) } else { input.parse() }
1949}
1950
1951mod kw {
1952    syn::custom_keyword!(strg);
1953    syn::custom_keyword!(ensures);
1954    syn::custom_keyword!(requires);
1955    syn::custom_keyword!(refined);
1956    syn::custom_keyword!(by);
1957    syn::custom_keyword!(base);
1958    syn::custom_keyword!(bitvec);
1959    syn::custom_keyword!(reft);
1960}
1961
1962#[derive(Copy, Clone, Eq, PartialEq)]
1963enum Mode {
1964    Flux,
1965    Rust,
1966}
1967
1968impl Item {
1969    fn replace_attrs(&mut self, new: Vec<Attribute>) -> Vec<Attribute> {
1970        match self {
1971            Item::Fn(ItemFn { attrs, .. })
1972            | Item::Mod(ItemMod { attrs, .. })
1973            | Item::Impl(ItemImpl { attrs, .. })
1974            | Item::Enum(ItemEnum { attrs, .. })
1975            | Item::Struct(ItemStruct { attrs, .. })
1976            | Item::Use(syn::ItemUse { attrs, .. })
1977            | Item::Trait(ItemTrait { attrs, .. })
1978            | Item::Type(ItemType { attrs, .. })
1979            | Item::Const(syn::ItemConst { attrs, .. }) => mem::replace(attrs, new),
1980        }
1981    }
1982}
1983
1984impl ToTokens for Items {
1985    fn to_tokens(&self, tokens: &mut TokenStream) {
1986        tokens.append_all(&self.0);
1987    }
1988}
1989
1990impl ToTokens for Item {
1991    fn to_tokens(&self, tokens: &mut TokenStream) {
1992        match self {
1993            Item::Fn(item_fn) => item_fn.to_tokens(tokens),
1994            Item::Impl(item_impl) => item_impl.to_tokens(tokens),
1995            Item::Struct(item_struct) => item_struct.to_tokens(tokens),
1996            Item::Enum(item_enum) => item_enum.to_tokens(tokens),
1997            Item::Use(item_use) => item_use.to_tokens(tokens),
1998            Item::Type(item_type) => item_type.to_tokens(tokens),
1999            Item::Mod(item_mod) => item_mod.to_tokens(tokens),
2000            Item::Trait(item_trait) => item_trait.to_tokens(tokens),
2001            Item::Const(item_const) => item_const.to_tokens(tokens),
2002        }
2003    }
2004}
2005
2006impl ToTokens for ItemMod {
2007    fn to_tokens(&self, tokens: &mut TokenStream) {
2008        tokens.append_all(&self.attrs);
2009        self.vis.to_tokens(tokens);
2010        self.unsafety.to_tokens(tokens);
2011        self.mod_token.to_tokens(tokens);
2012        self.ident.to_tokens(tokens);
2013        if let Some((brace, items)) = &self.content {
2014            brace.surround(tokens, |tokens| {
2015                tokens.append_all(items);
2016            });
2017        }
2018        self.semi.to_tokens(tokens);
2019    }
2020}
2021
2022impl ToTokens for ItemStruct {
2023    fn to_tokens(&self, tokens: &mut TokenStream) {
2024        tokens.append_all(&self.attrs);
2025        #[cfg(flux_sysroot)]
2026        if let Some(refined_by) = &self.refined_by {
2027            refined_by.flux_tool_attr().to_tokens(tokens);
2028        }
2029        self.vis.to_tokens(tokens);
2030        self.struct_token.to_tokens(tokens);
2031        self.ident.to_tokens(tokens);
2032        self.generics.to_tokens(tokens, Mode::Rust);
2033        self.fields.to_tokens(tokens, |field, tokens| {
2034            #[cfg(flux_sysroot)]
2035            field.flux_tool_attr().to_tokens(tokens);
2036            field.to_tokens(tokens);
2037        });
2038        self.semi_token.to_tokens(tokens);
2039    }
2040}
2041
2042impl ToTokens for ItemEnum {
2043    fn to_tokens(&self, tokens: &mut TokenStream) {
2044        tokens.append_all(&self.attrs);
2045        #[cfg(flux_sysroot)]
2046        if let Some(refined_by) = &self.refined_by {
2047            refined_by.flux_tool_attr().to_tokens(tokens);
2048        }
2049        self.vis.to_tokens(tokens);
2050        self.enum_token.to_tokens(tokens);
2051        self.ident.to_tokens(tokens);
2052        self.generics.to_tokens(tokens, Mode::Rust);
2053        self.brace_token.surround(tokens, |tokens| {
2054            self.variants.to_tokens(tokens);
2055        });
2056    }
2057}
2058
2059impl ToTokens for Variant {
2060    fn to_tokens(&self, tokens: &mut TokenStream) {
2061        #[cfg(flux_sysroot)]
2062        self.flux_tool_attr().to_tokens(tokens);
2063        tokens.append_all(&self.attrs);
2064        self.ident.to_tokens(tokens);
2065        self.fields.to_tokens(tokens, Field::to_tokens);
2066        if let Some((eq_token, expr)) = &self.discriminant {
2067            eq_token.to_tokens(tokens);
2068            expr.to_tokens(tokens);
2069        }
2070    }
2071}
2072
2073impl ToTokens for RefinedBy {
2074    fn to_tokens(&self, tokens: &mut TokenStream) {
2075        for param in self.params.pairs() {
2076            param.value().to_tokens(tokens);
2077            param.punct().to_tokens(tokens);
2078        }
2079    }
2080}
2081
2082impl ToTokens for RefinedByParam {
2083    fn to_tokens(&self, tokens: &mut TokenStream) {
2084        self.ident.to_tokens(tokens);
2085        self.colon_token.to_tokens(tokens);
2086        self.sort.to_tokens(tokens);
2087    }
2088}
2089
2090impl ToTokens for Sort {
2091    fn to_tokens(&self, tokens: &mut TokenStream) {
2092        match self {
2093            Sort::BaseSort(bsort) => bsort.to_tokens(tokens),
2094            Sort::Func { input, arrow, output } => {
2095                input.to_tokens(tokens);
2096                arrow.to_tokens(tokens);
2097                output.to_tokens(tokens);
2098            }
2099        }
2100    }
2101}
2102
2103impl ToTokens for FuncSortInput {
2104    fn to_tokens(&self, tokens: &mut TokenStream) {
2105        match self {
2106            FuncSortInput::Parenthesized { paren_token, inputs } => {
2107                paren_token.surround(tokens, |tokens| {
2108                    inputs.to_tokens(tokens);
2109                });
2110            }
2111            FuncSortInput::Single(bsort) => bsort.to_tokens(tokens),
2112        }
2113    }
2114}
2115
2116impl ToTokens for BaseSort {
2117    fn to_tokens(&self, tokens: &mut TokenStream) {
2118        match self {
2119            BaseSort::BitVec(bitvec) => bitvec.to_tokens(tokens),
2120            BaseSort::App(ctor, args) => {
2121                ctor.to_tokens(tokens);
2122                args.to_tokens(tokens);
2123            }
2124        }
2125    }
2126}
2127
2128impl ToTokens for BitVecSort {
2129    fn to_tokens(&self, tokens: &mut TokenStream) {
2130        self.bitvec_token.to_tokens(tokens);
2131        self.lt_token.to_tokens(tokens);
2132        self.lit.to_tokens(tokens);
2133        self.gt_token.to_tokens(tokens);
2134    }
2135}
2136
2137impl ToTokens for SortArguments {
2138    fn to_tokens(&self, tokens: &mut TokenStream) {
2139        match self {
2140            SortArguments::None => {}
2141            SortArguments::AngleBracketed(args) => args.to_tokens(tokens),
2142        }
2143    }
2144}
2145
2146impl ToTokens for AngleBracketedSortArgs {
2147    fn to_tokens(&self, tokens: &mut TokenStream) {
2148        self.lt_token.to_tokens(tokens);
2149        self.args.to_tokens(tokens);
2150        self.gt_token.to_tokens(tokens);
2151    }
2152}
2153
2154impl ToTokens for ItemFn {
2155    fn to_tokens(&self, tokens: &mut TokenStream) {
2156        let ItemFn { attrs, vis, sig, block } = self;
2157        #[cfg(flux_sysroot)]
2158        {
2159            let flux_sig = ToTokensFlux(sig);
2160            quote!(#[flux_tool::sig(#flux_sig)]).to_tokens(tokens);
2161        }
2162        let rust_sig = ToTokensRust(sig);
2163        quote! {
2164            #(#attrs)*
2165            #vis #rust_sig #block
2166        }
2167        .to_tokens(tokens);
2168    }
2169}
2170
2171impl ToTokens for ItemType {
2172    fn to_tokens(&self, tokens: &mut TokenStream) {
2173        #[cfg(flux_sysroot)]
2174        self.flux_tool_attr().to_tokens(tokens);
2175        self.to_tokens_inner(tokens, Mode::Rust);
2176    }
2177}
2178
2179#[cfg(flux_sysroot)]
2180impl ToTokens for ToTokensFlux<&ItemType> {
2181    fn to_tokens(&self, tokens: &mut TokenStream) {
2182        self.0.to_tokens_inner(tokens, Mode::Flux);
2183    }
2184}
2185
2186#[cfg(flux_sysroot)]
2187impl ToTokens for ToTokensFlux<&Type> {
2188    fn to_tokens(&self, tokens: &mut TokenStream) {
2189        self.0.to_tokens_inner(tokens, Mode::Flux);
2190    }
2191}
2192
2193impl ItemType {
2194    fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) {
2195        if mode == Mode::Rust {
2196            tokens.append_all(&self.attrs);
2197            self.vis.to_tokens(tokens);
2198        }
2199        self.type_token.to_tokens(tokens);
2200        self.ident.to_tokens(tokens);
2201        self.generics.to_tokens(tokens, mode);
2202        if let Some(params) = &self.index_params {
2203            params.to_tokens_inner(tokens, mode);
2204        }
2205        self.eq_token.to_tokens(tokens);
2206        self.ty.to_tokens_inner(tokens, mode);
2207        if mode == Mode::Rust {
2208            self.semi_token.to_tokens(tokens);
2209        }
2210    }
2211
2212    #[cfg(flux_sysroot)]
2213    fn flux_tool_attr(&self) -> TokenStream {
2214        let flux_type = ToTokensFlux(self);
2215        quote! {
2216            #[flux_tool::alias(#flux_type)]
2217        }
2218    }
2219}
2220
2221impl Generics {
2222    fn to_tokens(&self, tokens: &mut TokenStream, mode: Mode) {
2223        if self.params.is_empty() {
2224            return;
2225        }
2226
2227        tokens_or_default(self.lt_token.as_ref(), tokens);
2228
2229        for param in self.params.pairs() {
2230            match mode {
2231                Mode::Rust => {
2232                    param.to_tokens(tokens);
2233                }
2234                Mode::Flux => {
2235                    if let GenericParam::Type(p) = param.value() {
2236                        p.to_tokens(tokens, mode);
2237                        param.punct().to_tokens(tokens);
2238                    }
2239                }
2240            }
2241        }
2242
2243        tokens_or_default(self.gt_token.as_ref(), tokens);
2244    }
2245}
2246
2247impl ToTokens for GenericParam {
2248    fn to_tokens(&self, tokens: &mut TokenStream) {
2249        match self {
2250            GenericParam::Lifetime(p) => p.to_tokens(tokens),
2251            GenericParam::Type(p) => p.to_tokens(tokens, Mode::Rust),
2252            GenericParam::Const(p) => p.to_tokens(tokens),
2253        }
2254    }
2255}
2256
2257impl TypeParam {
2258    fn to_tokens(&self, tokens: &mut TokenStream, mode: Mode) {
2259        tokens.append_all(outer(&self.attrs));
2260        self.ident.to_tokens(tokens);
2261
2262        if mode == Mode::Flux {
2263            if let Some(as_token) = self.as_token {
2264                as_token.to_tokens(tokens);
2265                self.param_kind.to_tokens(tokens);
2266            }
2267        }
2268
2269        if !self.bounds.is_empty() && mode == Mode::Rust {
2270            tokens_or_default(self.colon_token.as_ref(), tokens);
2271            self.bounds.to_tokens(tokens);
2272        }
2273        // if let Some(default) = &self.default {
2274        //     tokens_or_default(self.eq_token.as_ref(), tokens);
2275        //     default.to_tokens(tokens);
2276        // }
2277    }
2278}
2279
2280impl IndexParams {
2281    fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) {
2282        if mode == Mode::Flux {
2283            self.bracket_token.surround(tokens, |tokens| {
2284                for param in self.params.pairs() {
2285                    param.value().to_tokens_inner(tokens);
2286                    param.punct().to_tokens(tokens);
2287                }
2288            });
2289        }
2290    }
2291}
2292
2293impl ToTokens for ItemImpl {
2294    fn to_tokens(&self, tokens: &mut TokenStream) {
2295        tokens.append_all(&self.attrs);
2296        #[cfg(flux_sysroot)]
2297        for item in &self.items {
2298            if let ImplItem::Reft(reft) = item {
2299                reft.flux_tool_attr().to_tokens(tokens);
2300            }
2301        }
2302        self.impl_token.to_tokens(tokens);
2303        self.generics.to_tokens(tokens, Mode::Rust);
2304        if let Some((trait_, for_token)) = &self.trait_ {
2305            trait_.to_tokens(tokens);
2306            for_token.to_tokens(tokens);
2307        }
2308        self.self_ty.to_tokens(tokens);
2309        self.generics.where_clause.to_tokens(tokens);
2310        self.brace_token
2311            .surround(tokens, |tokens| tokens.append_all(&self.items));
2312    }
2313}
2314
2315impl ToTokens for ImplItem {
2316    fn to_tokens(&self, tokens: &mut TokenStream) {
2317        match self {
2318            ImplItem::Fn(impl_item_fn) => impl_item_fn.to_tokens(tokens),
2319            ImplItem::Type(impl_item_ty) => impl_item_ty.to_tokens(tokens),
2320            ImplItem::Reft(_) => {}
2321        }
2322    }
2323}
2324
2325impl ToTokens for ImplItemFn {
2326    fn to_tokens(&self, tokens: &mut TokenStream) {
2327        let ImplItemFn { attrs, vis, sig, block } = self;
2328        #[cfg(flux_sysroot)]
2329        {
2330            let flux_sig = ToTokensFlux(sig);
2331            quote!(#[flux_tool::sig(#flux_sig)]).to_tokens(tokens);
2332        }
2333        let rust_sig = ToTokensRust(sig);
2334        quote! {
2335            #(#attrs)*
2336            #vis #rust_sig #block
2337        }
2338        .to_tokens(tokens);
2339    }
2340}
2341
2342#[cfg(flux_sysroot)]
2343struct ToTokensFlux<T>(T);
2344
2345#[cfg(flux_sysroot)]
2346impl ToTokens for ToTokensFlux<&Signature> {
2347    fn to_tokens(&self, tokens: &mut TokenStream) {
2348        self.0.to_tokens_inner(tokens, Mode::Flux);
2349    }
2350}
2351
2352struct ToTokensRust<T>(T);
2353
2354impl ToTokens for ToTokensRust<&Signature> {
2355    fn to_tokens(&self, tokens: &mut TokenStream) {
2356        self.0.to_tokens_inner(tokens, Mode::Rust);
2357    }
2358}
2359
2360impl Signature {
2361    fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) {
2362        self.fn_token.to_tokens(tokens);
2363        if mode == Mode::Rust {
2364            self.ident.to_tokens(tokens);
2365        }
2366        self.generics.to_tokens(tokens, mode);
2367        self.paren_token.surround(tokens, |tokens| {
2368            for fn_arg in self.inputs.pairs() {
2369                fn_arg.value().to_tokens_inner(tokens, mode);
2370                fn_arg.punct().to_tokens(tokens);
2371            }
2372        });
2373        self.output.to_tokens_inner(tokens, mode);
2374        if mode == Mode::Rust {
2375            self.generics.where_clause.to_tokens(tokens);
2376        }
2377        if let Some(requires) = &self.requires {
2378            requires.to_tokens_inner(tokens, mode);
2379        }
2380        if let Some(ensures) = &self.ensures {
2381            ensures.to_tokens_inner(tokens, mode);
2382        }
2383    }
2384}
2385
2386impl Requires {
2387    fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) {
2388        if mode == Mode::Flux {
2389            self.requires_token.to_tokens(tokens);
2390            self.constraint.to_tokens(tokens);
2391        }
2392    }
2393}
2394
2395impl Ensures {
2396    fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) {
2397        if mode == Mode::Flux {
2398            self.ensures_token.to_tokens(tokens);
2399            for constraint in self.constraints.pairs() {
2400                constraint.value().to_tokens_inner(tokens);
2401                constraint.punct().to_tokens(tokens);
2402            }
2403        }
2404    }
2405}
2406
2407impl Constraint {
2408    fn to_tokens_inner(&self, tokens: &mut TokenStream) {
2409        match self {
2410            Constraint::Type { ident, colon_token, ty } => {
2411                ident.to_tokens(tokens);
2412                colon_token.to_tokens(tokens);
2413                ty.to_tokens_inner(tokens, Mode::Flux);
2414            }
2415            Constraint::Expr(e) => e.to_tokens(tokens),
2416        }
2417    }
2418}
2419
2420impl FnArg {
2421    fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) {
2422        match self {
2423            FnArg::StrgRef(strg_ref) => strg_ref.to_tokens_inner(tokens, mode),
2424            FnArg::Typed(pat_type) => {
2425                pat_type.to_tokens_inner(tokens, mode);
2426            }
2427        }
2428    }
2429}
2430
2431impl StrgRef {
2432    fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) {
2433        self.pat.to_tokens_inner(tokens, mode);
2434        self.colon_token.to_tokens(tokens);
2435        self.and_token.to_tokens(tokens);
2436        match mode {
2437            Mode::Flux => self.strg_token.to_tokens(tokens),
2438            Mode::Rust => {
2439                let span = self.strg_token.span;
2440                quote_spanned!(span=> mut).to_tokens(tokens);
2441            }
2442        }
2443        self.ty.to_tokens_inner(tokens, mode);
2444    }
2445}
2446
2447impl ReturnType {
2448    fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) {
2449        match self {
2450            ReturnType::Default => {}
2451            ReturnType::Type(arrow, ty) => {
2452                arrow.to_tokens(tokens);
2453                ty.to_tokens_inner(tokens, mode);
2454            }
2455        }
2456    }
2457}
2458
2459impl PatType {
2460    fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) {
2461        self.pat.to_tokens_inner(tokens, mode);
2462        self.colon_token.to_tokens(tokens);
2463        self.ty.to_tokens_inner(tokens, mode);
2464        if mode == Mode::Flux {
2465            if let Some(pred) = &self.pred {
2466                pred.to_tokens_inner(tokens);
2467            }
2468        }
2469    }
2470}
2471
2472impl Pat {
2473    fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) {
2474        match self {
2475            Pat::Ident(pat_ident) => pat_ident.to_tokens_inner(tokens, mode),
2476            Pat::Wild(underscore_token) => {
2477                underscore_token.to_tokens(tokens);
2478            }
2479        }
2480    }
2481}
2482
2483impl PatIdent {
2484    fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) {
2485        if mode == Mode::Rust {
2486            self.mutability.to_tokens(tokens);
2487        }
2488        self.ident.to_tokens(tokens);
2489    }
2490}
2491
2492impl Type {
2493    fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) {
2494        match self {
2495            Type::Base(bty) => bty.to_tokens_inner(tokens, mode),
2496            Type::Indexed(ty_indexed) => ty_indexed.to_tokens_inner(tokens, mode),
2497            Type::Exists(ty_exists) => ty_exists.to_tokens_inner(tokens, mode),
2498            Type::GeneralExists(ty_general_exists) => {
2499                ty_general_exists.to_tokens_inner(tokens, mode);
2500            }
2501            Type::Reference(ty_reference) => ty_reference.to_tokens_inner(tokens, mode),
2502            Type::Constraint(ty_constraint) => ty_constraint.to_tokens_inner(tokens, mode),
2503            Type::Array(ty_array) => ty_array.to_tokens_inner(tokens, mode),
2504            Type::Tuple(tuple) => tuple.to_tokens_inner(tokens, mode),
2505            Type::Ptr(ty_ptr) => ty_ptr.to_tokens(tokens),
2506        }
2507    }
2508}
2509
2510impl TypeReference {
2511    fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) {
2512        self.and_token.to_tokens(tokens);
2513        if mode == Mode::Rust {
2514            self.lifetime.to_tokens(tokens);
2515        }
2516        self.mutability.to_tokens(tokens);
2517        self.elem.to_tokens_inner(tokens, mode);
2518    }
2519}
2520
2521impl TypeIndexed {
2522    fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) {
2523        self.bty.to_tokens_inner(tokens, mode);
2524        if mode == Mode::Flux {
2525            self.bracket_token.surround(tokens, |tokens| {
2526                self.expr.to_tokens(tokens);
2527            });
2528        }
2529    }
2530}
2531
2532impl TypeArray {
2533    fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) {
2534        self.bracket_token.surround(tokens, |tokens| {
2535            self.ty.to_tokens_inner(tokens, mode);
2536            self.semi_token.to_tokens(tokens);
2537            if mode == Mode::Rust {
2538                self.len.to_tokens(tokens);
2539            } else {
2540                quote!(_).to_tokens(tokens);
2541            }
2542        });
2543    }
2544}
2545
2546impl TypeConstraint {
2547    fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) {
2548        if mode == Mode::Flux {
2549            self.brace_token.surround(tokens, |tokens| {
2550                self.ty.to_tokens_inner(tokens, mode);
2551                self.or_token.to_tokens(tokens);
2552                self.pred.to_tokens(tokens);
2553            });
2554        } else {
2555            self.ty.to_tokens_inner(tokens, mode);
2556        }
2557    }
2558}
2559
2560impl TypeExists {
2561    fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) {
2562        self.bty.to_tokens_inner(tokens, mode);
2563        if mode == Mode::Flux {
2564            self.brace_token.surround(tokens, |tokens| {
2565                self.ident.to_tokens(tokens);
2566                self.colon_token.to_tokens(tokens);
2567                self.expr.to_tokens(tokens);
2568            });
2569        }
2570    }
2571}
2572
2573impl TypeGeneralExists {
2574    fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) {
2575        match mode {
2576            Mode::Flux => {
2577                self.brace_token.surround(tokens, |tokens| {
2578                    for param in self.params.pairs() {
2579                        param.value().to_tokens_inner(tokens);
2580                        param.punct().to_tokens(tokens);
2581                    }
2582                    self.dot_token.to_tokens(tokens);
2583                    self.ty.to_tokens_inner(tokens, mode);
2584                    self.or_token.to_tokens(tokens);
2585                    self.pred.to_tokens(tokens);
2586                });
2587            }
2588            Mode::Rust => {
2589                self.ty.to_tokens_inner(tokens, mode);
2590            }
2591        }
2592    }
2593}
2594
2595impl BaseType {
2596    fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) {
2597        match self {
2598            BaseType::Path(path) => path.to_tokens_inner(tokens, mode),
2599            BaseType::Slice(type_slice) => {
2600                type_slice.to_tokens_inner(tokens, mode);
2601            }
2602        }
2603    }
2604}
2605
2606impl TypeSlice {
2607    fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) {
2608        self.bracket_token.surround(tokens, |tokens| {
2609            self.ty.to_tokens_inner(tokens, mode);
2610        });
2611    }
2612}
2613
2614impl PatTypePredicate {
2615    fn to_tokens_inner(&self, tokens: &mut TokenStream) {
2616        self.brace_token
2617            .surround(tokens, |tokens| self.pred.to_tokens(tokens));
2618    }
2619}
2620
2621impl ExistsParam {
2622    fn to_tokens_inner(&self, tokens: &mut TokenStream) {
2623        self.ident.to_tokens(tokens);
2624        self.colon_token.to_tokens(tokens);
2625        self.sort.to_tokens(tokens);
2626    }
2627}
2628
2629impl Path {
2630    fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) {
2631        for segment in self.segments.pairs() {
2632            segment.value().to_tokens_inner(tokens, mode);
2633            segment.punct().to_tokens(tokens);
2634        }
2635    }
2636}
2637
2638impl PathSegment {
2639    fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) {
2640        self.ident.to_tokens(tokens);
2641        self.arguments.to_tokens_inner(tokens, mode);
2642    }
2643}
2644
2645impl PathArguments {
2646    fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) {
2647        match self {
2648            PathArguments::None => {}
2649            PathArguments::AngleBracketed(args) => args.to_tokens_inner(tokens, mode),
2650        }
2651    }
2652}
2653
2654impl AngleBracketedGenericArguments {
2655    fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) {
2656        self.lt_token.to_tokens(tokens);
2657        for arg in self.args.pairs() {
2658            arg.value().to_tokens_inner(tokens, mode);
2659            arg.punct().to_tokens(tokens);
2660        }
2661        self.gt_token.to_tokens(tokens);
2662    }
2663}
2664
2665impl GenericArgument {
2666    fn to_tokens_inner(&self, tokens: &mut TokenStream, mode: Mode) {
2667        match self {
2668            GenericArgument::Type(ty) => ty.to_tokens_inner(tokens, mode),
2669        }
2670    }
2671}
2672
2673impl ToTokens for Block {
2674    fn to_tokens(&self, tokens: &mut TokenStream) {
2675        self.brace_token
2676            .surround(tokens, |tokens| self.stmts.to_tokens(tokens));
2677    }
2678}
2679
2680fn outer(attrs: &[Attribute]) -> impl Iterator<Item = &Attribute> {
2681    fn is_outer(attr: &&Attribute) -> bool {
2682        match attr.style {
2683            syn::AttrStyle::Outer => true,
2684            syn::AttrStyle::Inner(_) => false,
2685        }
2686    }
2687    attrs.iter().filter(is_outer)
2688}
2689
2690fn inner(attrs: &[Attribute]) -> impl Iterator<Item = &Attribute> {
2691    fn is_inner(attr: &&Attribute) -> bool {
2692        match attr.style {
2693            syn::AttrStyle::Outer => false,
2694            syn::AttrStyle::Inner(_) => true,
2695        }
2696    }
2697    attrs.iter().filter(is_inner)
2698}
2699
2700fn peek_signature(input: ParseStream) -> bool {
2701    let fork = input.fork();
2702    fork.parse::<Option<Token![const]>>().is_ok()
2703        && fork.parse::<Option<Token![async]>>().is_ok()
2704        && fork.parse::<Option<Token![unsafe]>>().is_ok()
2705        && fork.parse::<Option<syn::Abi>>().is_ok()
2706        && fork.peek(Token![fn])
2707}
2708
2709struct FlexibleItemType {
2710    vis: Visibility,
2711    #[expect(dead_code)]
2712    defaultness: Option<Token![default]>,
2713    type_token: Token![type],
2714    ident: Ident,
2715    generics: syn::Generics,
2716    colon_token: Option<Token![:]>,
2717    bounds: Punctuated<syn::TypeParamBound, Token![+]>,
2718    ty: Option<(Token![=], syn::Type)>,
2719    semi_token: Token![;],
2720}
2721
2722enum TypeDefaultness {
2723    #[expect(dead_code)]
2724    Optional,
2725    Disallowed,
2726}
2727
2728#[expect(dead_code)]
2729enum WhereClauseLocation {
2730    // type Ty<T> where T: 'static = T;
2731    BeforeEq,
2732    // type Ty<T> = T where T: 'static;
2733    AfterEq,
2734    // TODO: goes away once the migration period on rust-lang/rust#89122 is over
2735    Both,
2736}
2737
2738impl FlexibleItemType {
2739    fn parse(
2740        input: ParseStream,
2741        allow_defaultness: TypeDefaultness,
2742        where_clause_location: WhereClauseLocation,
2743    ) -> Result<Self> {
2744        let vis: Visibility = input.parse()?;
2745        let defaultness: Option<Token![default]> = match allow_defaultness {
2746            TypeDefaultness::Optional => input.parse()?,
2747            TypeDefaultness::Disallowed => None,
2748        };
2749        let type_token: Token![type] = input.parse()?;
2750        let ident: Ident = input.parse()?;
2751        let mut generics: syn::Generics = input.parse()?;
2752        let (colon_token, bounds) = Self::parse_optional_bounds(input)?;
2753
2754        match where_clause_location {
2755            WhereClauseLocation::BeforeEq | WhereClauseLocation::Both => {
2756                generics.where_clause = input.parse()?;
2757            }
2758            WhereClauseLocation::AfterEq => {}
2759        }
2760
2761        let ty = Self::parse_optional_definition(input)?;
2762
2763        match where_clause_location {
2764            WhereClauseLocation::AfterEq | WhereClauseLocation::Both
2765                if generics.where_clause.is_none() =>
2766            {
2767                generics.where_clause = input.parse()?;
2768            }
2769            _ => {}
2770        }
2771
2772        let semi_token: Token![;] = input.parse()?;
2773
2774        Ok(FlexibleItemType {
2775            vis,
2776            defaultness,
2777            type_token,
2778            ident,
2779            generics,
2780            colon_token,
2781            bounds,
2782            ty,
2783            semi_token,
2784        })
2785    }
2786
2787    fn parse_optional_bounds(
2788        input: ParseStream,
2789    ) -> Result<(Option<Token![:]>, Punctuated<syn::TypeParamBound, Token![+]>)> {
2790        let colon_token: Option<Token![:]> = input.parse()?;
2791
2792        let mut bounds = Punctuated::new();
2793        if colon_token.is_some() {
2794            loop {
2795                if input.peek(Token![where]) || input.peek(Token![=]) || input.peek(Token![;]) {
2796                    break;
2797                }
2798                bounds.push_value(input.parse::<syn::TypeParamBound>()?);
2799                if input.peek(Token![where]) || input.peek(Token![=]) || input.peek(Token![;]) {
2800                    break;
2801                }
2802                bounds.push_punct(input.parse::<Token![+]>()?);
2803            }
2804        }
2805
2806        Ok((colon_token, bounds))
2807    }
2808
2809    fn parse_optional_definition(input: ParseStream) -> Result<Option<(Token![=], syn::Type)>> {
2810        let eq_token: Option<Token![=]> = input.parse()?;
2811        if let Some(eq_token) = eq_token {
2812            let definition: syn::Type = input.parse()?;
2813            Ok(Some((eq_token, definition)))
2814        } else {
2815            Ok(None)
2816        }
2817    }
2818}
2819
2820fn parse_trait_item_type(input: ParseStream) -> Result<TraitItem> {
2821    let FlexibleItemType {
2822        vis,
2823        defaultness: _,
2824        type_token,
2825        ident,
2826        generics,
2827        colon_token,
2828        bounds,
2829        ty,
2830        semi_token,
2831    } = FlexibleItemType::parse(input, TypeDefaultness::Disallowed, WhereClauseLocation::AfterEq)?;
2832
2833    if !matches!(vis, Visibility::Inherited) {
2834        Err(syn::Error::new_spanned(vis, "visibility qualifiers are not permitted here"))
2835    } else {
2836        Ok(TraitItem::Type(syn::TraitItemType {
2837            attrs: Vec::new(),
2838            type_token,
2839            ident,
2840            generics,
2841            colon_token,
2842            bounds,
2843            default: ty,
2844            semi_token,
2845        }))
2846    }
2847}