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 Const(syn::TraitItemConst),
136
137 Fn(TraitItemFn),
139
140 Type(syn::TraitItemType),
142
143 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 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 Lifetime(syn::LifetimeParam),
357
358 Type(TypeParam),
360
361 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 }
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 pub ident: Ident,
426
427 pub fields: Fields,
429
430 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(FieldsNamed),
503
504 Unnamed(FieldsUnnamed),
506
507 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 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 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 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 }));
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 Ok(TypeParam {
1230 attrs,
1231 ident,
1232 as_token,
1233 param_kind,
1234 colon_token,
1235 bounds,
1236 })
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 }
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 BeforeEq,
2732 AfterEq,
2734 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}