flux_syntax/parser/
mod.rs

1pub(crate) mod lookahead;
2mod utils;
3use std::{collections::HashSet, str::FromStr, vec};
4
5use lookahead::{AnyLit, LAngle, NonReserved, RAngle};
6use rustc_span::sym::Output;
7use utils::{
8    angle, braces, brackets, delimited, opt_angle, parens, punctuated_until,
9    punctuated_with_trailing, repeat_while, sep1, until,
10};
11
12use crate::{
13    ParseCtxt, ParseError, ParseResult,
14    parser::lookahead::{AnyOf, Expected, PeekExpected},
15    surface::{
16        self, Async,
17        Attr::{self},
18        BaseSort, BaseTy, BaseTyKind, BinOp, BindKind, ConstArg, ConstArgKind, ConstructorArg,
19        DetachedInherentImpl, DetachedItem, DetachedItemKind, DetachedSpecs, DetachedTrait,
20        DetachedTraitImpl, Ensures, EnumDef, Expr, ExprKind, ExprPath, ExprPathSegment, FieldExpr,
21        FluxItem, FnInput, FnOutput, FnRetTy, FnSig, GenericArg, GenericArgKind, GenericBounds,
22        GenericParam, Generics, Ident, ImplAssocReft, Indices, LetDecl, LitKind, Mutability,
23        ParamMode, Path, PathSegment, PrimOpProp, Qualifier, QuantKind, RefineArg, RefineParam,
24        RefineParams, Requires, Sort, SortDecl, SortPath, SpecFunc, Spread, StructDef,
25        TraitAssocReft, TraitRef, Trusted, Ty, TyAlias, TyKind, UnOp, VariantDef, VariantRet,
26        WhereBoundPredicate,
27    },
28    symbols::{kw, sym},
29    token::{self, Comma, Delimiter::*, IdentIsRaw, Or, Token, TokenKind},
30};
31
32/// An attribute that's considered part of the *syntax* of an item.
33///
34/// This is in contrast to a [`surface::Attr`] which changes the behavior of an item. For example,
35/// a `#[refined_by(...)]` is part of the syntax of an adt: we could think of a different syntax
36/// that doesn't use an attribute. The existence of a syntax attribute in the token stream can be
37/// used to decide how to keep parsing, for example, if we see a `#[reft]` we know that the next
38/// item bust be an associated refinement and not a method inside an impl or trait.
39enum SyntaxAttr {
40    /// A `#[reft]` attribute
41    Reft,
42    /// A `#[invariant]` attribute
43    Invariant(Expr),
44    /// A `#[refined_by(...)]` attribute
45    RefinedBy(RefineParams),
46    /// A `#[hide]` attribute
47    ///
48    /// NOTE(nilehmann) This should be considered a normal attribute, but we haven't implemented
49    /// attributes for flux items. If we start seeing more of these we should consider implementing
50    /// the infrastructure necesary to keep a list of attributes inside the flux item like we do
51    /// for rust items.
52    Hide,
53    /// a `#[opaque]` attribute
54    Opaque,
55}
56
57#[derive(Default)]
58struct ParsedAttrs {
59    normal: Vec<Attr>,
60    syntax: Vec<SyntaxAttr>,
61}
62
63impl ParsedAttrs {
64    fn is_reft(&self) -> bool {
65        self.syntax
66            .iter()
67            .any(|attr| matches!(attr, SyntaxAttr::Reft))
68    }
69
70    fn is_hide(&self) -> bool {
71        self.syntax
72            .iter()
73            .any(|attr| matches!(attr, SyntaxAttr::Hide))
74    }
75
76    fn is_opaque(&self) -> bool {
77        self.syntax
78            .iter()
79            .any(|attr| matches!(attr, SyntaxAttr::Opaque))
80    }
81
82    fn refined_by(&mut self) -> Option<RefineParams> {
83        let pos = self
84            .syntax
85            .iter()
86            .position(|x| matches!(x, SyntaxAttr::RefinedBy(_)))?;
87        if let SyntaxAttr::RefinedBy(params) = self.syntax.remove(pos) {
88            Some(params)
89        } else {
90            None
91        }
92    }
93
94    fn invariant(&mut self) -> Option<Expr> {
95        let pos = self
96            .syntax
97            .iter()
98            .position(|x| matches!(x, SyntaxAttr::Invariant(_)))?;
99        if let SyntaxAttr::Invariant(exp) = self.syntax.remove(pos) { Some(exp) } else { None }
100    }
101}
102
103/// ```text
104///   yes ⟨ , reason = ⟨literal⟩ ⟩?
105/// | no ⟨ , reason = ⟨literal⟩ ⟩?
106/// | reason = ⟨literal⟩
107/// ```
108pub(crate) fn parse_yes_or_no_with_reason(cx: &mut ParseCtxt) -> ParseResult<bool> {
109    let mut lookahead = cx.lookahead1();
110    if lookahead.advance_if(sym::yes) {
111        if cx.advance_if(token::Comma) {
112            parse_reason(cx)?;
113        }
114        Ok(true)
115    } else if lookahead.advance_if(sym::no) {
116        if cx.advance_if(token::Comma) {
117            parse_reason(cx)?;
118        }
119        Ok(false)
120    } else if lookahead.peek(sym::reason) {
121        parse_reason(cx)?;
122        Ok(true)
123    } else {
124        Err(lookahead.into_error())
125    }
126}
127
128/// ```text
129/// ⟨reason⟩ := reason = ⟨literal⟩
130/// ```
131fn parse_reason(cx: &mut ParseCtxt) -> ParseResult {
132    cx.expect(sym::reason)?;
133    cx.expect(token::Eq)?;
134    cx.expect(AnyLit)
135}
136
137/// ```text
138/// ⟨ident_list⟩ := ⟨ident⟩,*
139/// ```
140pub(crate) fn parse_ident_list(cx: &mut ParseCtxt) -> ParseResult<Vec<Ident>> {
141    punctuated_until(cx, Comma, token::Eof, parse_ident)
142}
143
144/// ```text
145/// ⟨flux_items⟩ := ⟨flux_item⟩*
146/// ```
147pub(crate) fn parse_flux_items(cx: &mut ParseCtxt) -> ParseResult<Vec<FluxItem>> {
148    until(cx, token::Eof, parse_flux_item)
149}
150
151/// ```text
152/// ⟨flux_item⟩ := ⟨func_def⟩
153///              | ⟨qualifier⟩
154///              | ⟨sort_decl⟩
155///              | ⟨primop_prop⟩
156/// ```
157fn parse_flux_item(cx: &mut ParseCtxt) -> ParseResult<FluxItem> {
158    let mut lookahead = cx.lookahead1();
159    if lookahead.peek(token::Pound) || lookahead.peek(kw::Fn) {
160        parse_reft_func(cx).map(FluxItem::FuncDef)
161    } else if lookahead.peek(kw::Local) || lookahead.peek(kw::Qualifier) {
162        parse_qualifier(cx).map(FluxItem::Qualifier)
163    } else if lookahead.peek(kw::Opaque) {
164        parse_sort_decl(cx).map(FluxItem::SortDecl)
165    } else if lookahead.peek(kw::Property) {
166        parse_primop_property(cx).map(FluxItem::PrimOpProp)
167    } else {
168        Err(lookahead.into_error())
169    }
170}
171
172///```text
173/// ⟨specs⟩ ::= ⟨specs⟩*
174/// ```
175pub(crate) fn parse_detached_specs(cx: &mut ParseCtxt) -> ParseResult<surface::DetachedSpecs> {
176    let items = until(cx, token::Eof, parse_detached_item)?;
177    Ok(surface::DetachedSpecs { items })
178}
179
180///```text
181/// ⟨specs⟩ ::= ⟨fn-spec⟩
182///           | ⟨struct-spec⟩
183///           | ⟨enum-spec⟩
184///           | ⟨mod⟩
185///           | ⟨impl⟩
186/// ```
187pub(crate) fn parse_detached_item(cx: &mut ParseCtxt) -> ParseResult<DetachedItem> {
188    let attrs = parse_attrs(cx)?;
189    let mut lookahead = cx.lookahead1();
190    if lookahead.peek(kw::Fn) {
191        Ok(parse_detached_fn_sig(cx, attrs)?.map_kind(DetachedItemKind::FnSig))
192    } else if lookahead.peek(kw::Mod) {
193        parse_detached_mod(cx)
194    } else if lookahead.peek(kw::Struct) {
195        parse_detached_struct(cx, attrs)
196    } else if lookahead.peek(kw::Enum) {
197        parse_detached_enum(cx, attrs)
198    } else if lookahead.peek(kw::Impl) {
199        parse_detached_impl(cx, attrs)
200    } else if lookahead.peek(kw::Trait) {
201        parse_detached_trait(cx, attrs)
202    } else {
203        Err(lookahead.into_error())
204    }
205}
206
207///```text
208/// ⟨field⟩ ::= ⟨ident⟩ : ⟨type⟩
209/// ```
210fn parse_detached_field(cx: &mut ParseCtxt) -> ParseResult<(Ident, Ty)> {
211    let ident = parse_ident(cx)?;
212    cx.expect(token::Colon)?;
213    let ty = parse_type(cx)?;
214    Ok((ident, ty))
215}
216
217///```text
218/// ⟨enum⟩ := enum Ident ⟨refine_info⟩ { ⟨variant⟩* }
219/// ```
220fn parse_detached_enum(cx: &mut ParseCtxt, mut attrs: ParsedAttrs) -> ParseResult<DetachedItem> {
221    cx.expect(kw::Enum)?;
222    let path = parse_expr_path(cx)?;
223    let generics = Some(parse_opt_generics(cx)?);
224    let refined_by = attrs.refined_by();
225    let invariants = attrs.invariant().into_iter().collect();
226    let variants = braces(cx, Comma, |cx| parse_variant(cx, true))?
227        .into_iter()
228        .map(Some)
229        .collect();
230    let enum_def = EnumDef { generics, refined_by, variants, invariants, reflected: false };
231    Ok(DetachedItem {
232        attrs: attrs.normal,
233        path,
234        kind: DetachedItemKind::Enum(enum_def),
235        node_id: cx.next_node_id(),
236    })
237}
238
239fn parse_detached_struct(cx: &mut ParseCtxt, mut attrs: ParsedAttrs) -> ParseResult<DetachedItem> {
240    cx.expect(kw::Struct)?;
241    let path = parse_expr_path(cx)?;
242    let generics = Some(parse_opt_generics(cx)?);
243    let refined_by = attrs.refined_by();
244    let opaque = attrs.is_opaque();
245    let invariants = attrs.invariant().into_iter().collect();
246    let fields = if cx.peek(token::OpenBrace) {
247        braces(cx, Comma, parse_detached_field)?
248            .into_iter()
249            .map(|(_, ty)| Some(ty))
250            .collect()
251    } else if cx.peek(token::OpenParen) {
252        parens(cx, Comma, parse_type)?
253            .into_iter()
254            .map(Some)
255            .collect()
256    } else {
257        cx.expect(token::Semi)?;
258        vec![]
259    };
260    let struct_def = StructDef { generics, opaque, refined_by, invariants, fields };
261    Ok(DetachedItem {
262        attrs: attrs.normal,
263        path,
264        kind: DetachedItemKind::Struct(struct_def),
265        node_id: cx.next_node_id(),
266    })
267}
268
269fn ident_path(cx: &mut ParseCtxt, ident: Ident) -> ExprPath {
270    let span = ident.span;
271    let segments = vec![ExprPathSegment { ident, node_id: cx.next_node_id() }];
272    ExprPath { segments, span, node_id: cx.next_node_id() }
273}
274
275fn parse_detached_fn_sig(
276    cx: &mut ParseCtxt,
277    attrs: ParsedAttrs,
278) -> ParseResult<DetachedItem<FnSig>> {
279    let fn_sig = parse_fn_sig(cx, token::Semi)?;
280    let span = fn_sig.span;
281    let ident = fn_sig
282        .ident
283        .ok_or(ParseError { kind: crate::ParseErrorKind::InvalidDetachedSpec, span })?;
284    let path = ident_path(cx, ident);
285    Ok(DetachedItem { attrs: attrs.normal, path, kind: fn_sig, node_id: cx.next_node_id() })
286}
287
288///```text
289/// ⟨mod⟩ ::= mod ⟨ident⟩ { ⟨specs⟩ }
290/// ```
291fn parse_detached_mod(cx: &mut ParseCtxt) -> ParseResult<DetachedItem> {
292    cx.expect(kw::Mod)?;
293    let path = parse_expr_path(cx)?;
294    cx.expect(TokenKind::open_delim(Brace))?;
295    let items = until(cx, TokenKind::close_delim(Brace), parse_detached_item)?;
296    cx.expect(TokenKind::close_delim(Brace))?;
297    Ok(DetachedItem {
298        attrs: vec![],
299        path,
300        kind: DetachedItemKind::Mod(DetachedSpecs { items }),
301        node_id: cx.next_node_id(),
302    })
303}
304
305///```text
306/// ⟨trait-spec⟩ ::= trait Ident { ⟨fn-spec⟩* }
307/// ```
308fn parse_detached_trait(cx: &mut ParseCtxt, attrs: ParsedAttrs) -> ParseResult<DetachedItem> {
309    cx.expect(kw::Trait)?;
310    let path = parse_expr_path(cx)?;
311    let _generics = parse_opt_generics(cx)?;
312    cx.expect(TokenKind::open_delim(Brace))?;
313
314    let mut items = vec![];
315    let mut refts = vec![];
316    while !cx.peek(TokenKind::close_delim(Brace)) {
317        let assoc_item_attrs = parse_attrs(cx)?;
318        if assoc_item_attrs.is_reft() {
319            refts.push(parse_trait_assoc_reft(cx)?);
320        } else {
321            items.push(parse_detached_fn_sig(cx, assoc_item_attrs)?);
322        }
323    }
324    cx.expect(TokenKind::close_delim(Brace))?;
325    Ok(DetachedItem {
326        attrs: attrs.normal,
327        path,
328        kind: DetachedItemKind::Trait(DetachedTrait { items, refts }),
329        node_id: cx.next_node_id(),
330    })
331}
332
333///```text
334/// ⟨impl-spec⟩ ::= impl Ident (for Ident)? { ⟨#[assoc] impl_assoc_reft⟩* ⟨fn-spec⟩* }
335/// ```
336fn parse_detached_impl(cx: &mut ParseCtxt, attrs: ParsedAttrs) -> ParseResult<DetachedItem> {
337    let lo = cx.lo();
338    cx.expect(kw::Impl)?;
339    let hi = cx.hi();
340    let span = cx.mk_span(lo, hi);
341    let outer_path = parse_expr_path(cx)?;
342    let _generics = parse_opt_generics(cx)?;
343    let inner_path = if cx.advance_if(kw::For) {
344        let path = parse_expr_path(cx)?;
345        let _generics = parse_opt_generics(cx)?;
346        Some(path)
347    } else {
348        None
349    };
350    cx.expect(TokenKind::open_delim(Brace))?;
351
352    let mut items = vec![];
353    let mut refts = vec![];
354    while !cx.peek(TokenKind::close_delim(Brace)) {
355        // if inner_path.is_none, we are parsing an inherent impl with no associated-refts
356        let assoc_item_attrs = parse_attrs(cx)?;
357        if assoc_item_attrs.is_reft() && inner_path.is_some() {
358            refts.push(parse_impl_assoc_reft(cx)?);
359        } else {
360            items.push(parse_detached_fn_sig(cx, assoc_item_attrs)?);
361        }
362    }
363    cx.expect(TokenKind::close_delim(Brace))?;
364    if let Some(path) = inner_path {
365        Ok(DetachedItem {
366            attrs: attrs.normal,
367            path,
368            kind: DetachedItemKind::TraitImpl(DetachedTraitImpl {
369                trait_: outer_path,
370                items,
371                refts,
372                span,
373            }),
374            node_id: cx.next_node_id(),
375        })
376    } else {
377        Ok(DetachedItem {
378            attrs: attrs.normal,
379            path: outer_path,
380            kind: DetachedItemKind::InherentImpl(DetachedInherentImpl { items, span }),
381            node_id: cx.next_node_id(),
382        })
383    }
384}
385
386fn parse_attr(cx: &mut ParseCtxt, attrs: &mut ParsedAttrs) -> ParseResult {
387    cx.expect(token::Pound)?;
388    cx.expect(token::OpenBracket)?;
389    let mut lookahead = cx.lookahead1();
390    if lookahead.advance_if(kw::Trusted) {
391        if cx.advance_if(token::OpenParen) {
392            parse_reason(cx)?;
393            cx.expect(token::CloseParen)?;
394        }
395        attrs.normal.push(Attr::Trusted(Trusted::Yes));
396    } else if lookahead.advance_if(sym::hide) {
397        attrs.syntax.push(SyntaxAttr::Hide);
398    } else if lookahead.advance_if(kw::Opaque) {
399        attrs.syntax.push(SyntaxAttr::Opaque);
400    } else if lookahead.advance_if(kw::Reft) {
401        attrs.syntax.push(SyntaxAttr::Reft);
402    } else if lookahead.advance_if(kw::RefinedBy) {
403        attrs
404            .syntax
405            .push(SyntaxAttr::RefinedBy(delimited(cx, Parenthesis, parse_refined_by)?));
406    } else if lookahead.advance_if(kw::Invariant) {
407        attrs
408            .syntax
409            .push(SyntaxAttr::Invariant(delimited(cx, Parenthesis, |cx| parse_expr(cx, true))?));
410    } else {
411        return Err(lookahead.into_error());
412    };
413    cx.expect(token::CloseBracket)
414}
415
416fn parse_attrs(cx: &mut ParseCtxt) -> ParseResult<ParsedAttrs> {
417    let mut attrs = ParsedAttrs::default();
418    repeat_while(cx, token::Pound, |cx| parse_attr(cx, &mut attrs))?;
419    Ok(attrs)
420}
421
422/// ```text
423/// ⟨func_def⟩ := ⟨ # [ hide ] ⟩?
424///               fn ⟨ident⟩ ⟨ < ⟨ident⟩,* > ⟩?
425///               ( ⟨refine_param⟩,* )
426///               ->
427///               ⟨sort⟩
428/// ```
429fn parse_reft_func(cx: &mut ParseCtxt) -> ParseResult<SpecFunc> {
430    let attrs = parse_attrs(cx)?;
431    let hide = attrs.is_hide();
432    cx.expect(kw::Fn)?;
433    let name = parse_ident(cx)?;
434    let sort_vars = opt_angle(cx, Comma, parse_ident)?;
435    let params = parens(cx, Comma, |cx| parse_refine_param(cx, RequireSort::Yes))?;
436    cx.expect(token::RArrow)?;
437    let output = parse_sort(cx)?;
438    let body = if cx.peek(token::OpenBrace) {
439        Some(parse_block(cx)?)
440    } else {
441        cx.expect(token::Semi)?;
442        None
443    };
444    Ok(SpecFunc { name, sort_vars, params, output, body, hide })
445}
446
447/// ```text
448/// ⟨qualifier⟩ :=  ⟨ local ⟩?
449///                 qualifier ⟨ident⟩ ( ⟨refine_param⟩,* )
450///                 ⟨block⟩
451/// ```
452fn parse_qualifier(cx: &mut ParseCtxt) -> ParseResult<Qualifier> {
453    let lo = cx.lo();
454    let local = cx.advance_if(kw::Local);
455    cx.expect(kw::Qualifier)?;
456    let name = parse_ident(cx)?;
457    let params = parens(cx, Comma, |cx| parse_refine_param(cx, RequireSort::Yes))?;
458    let expr = parse_block(cx)?;
459    let hi = cx.hi();
460    Ok(Qualifier { global: !local, name, params, expr, span: cx.mk_span(lo, hi) })
461}
462
463/// ```text
464/// ⟨sort_decl⟩ := opaque sort ⟨ident⟩ ;
465/// ```
466fn parse_sort_decl(cx: &mut ParseCtxt) -> ParseResult<SortDecl> {
467    cx.expect(kw::Opaque)?;
468    cx.expect(kw::Sort)?;
469    let name = parse_ident(cx)?;
470    let sort_vars = opt_angle(cx, Comma, parse_ident)?;
471    cx.expect(token::Semi)?;
472    Ok(SortDecl { name, sort_vars })
473}
474
475/// `⟨bin_op⟩ := ⟨ a binary operator ⟩
476fn parse_binop(cx: &mut ParseCtxt) -> ParseResult<BinOp> {
477    let (op, ntokens) = cx
478        .peek_binop()
479        .ok_or_else(|| cx.unexpected_token(vec![Expected::Str("binary operator")]))?;
480    cx.advance_by(ntokens);
481    Ok(op)
482}
483
484/// ```text
485/// ⟨primop_prop⟩ := property ⟨ident⟩ [ ⟨bin_op⟩ ] ( ⟨refine_param⟩,* ) ⟨block⟩
486/// ```
487fn parse_primop_property(cx: &mut ParseCtxt) -> ParseResult<PrimOpProp> {
488    let lo = cx.lo();
489    cx.expect(kw::Property)?;
490
491    // Parse the name
492    let name = parse_ident(cx)?;
493
494    // Parse the operator
495    cx.expect(token::OpenBracket)?;
496    let op = parse_binop(cx)?;
497    cx.expect(token::CloseBracket)?;
498
499    // Parse the args
500    let params = parens(cx, Comma, |cx| parse_refine_param(cx, RequireSort::No))?;
501
502    let body = parse_block(cx)?;
503    let hi = cx.hi();
504
505    Ok(PrimOpProp { name, op, params, body, span: cx.mk_span(lo, hi) })
506}
507
508pub(crate) fn parse_trait_assoc_refts(cx: &mut ParseCtxt) -> ParseResult<Vec<TraitAssocReft>> {
509    until(cx, token::Eof, parse_trait_assoc_reft)
510}
511
512/// ```text
513/// ⟨trait_assoc_reft⟩ := fn ⟨ident⟩ ( ⟨refine_param⟩,* ) -> ⟨base_sort⟩ ;?
514///                     | fn ⟨ident⟩ ( ⟨refine_param⟩,* ) -> ⟨base_sort⟩ ⟨block⟩
515///                     | final fn ⟨ident⟩ ( ⟨refine_param⟩,* ) -> ⟨base_sort⟩ ⟨block⟩
516/// ```
517fn parse_trait_assoc_reft(cx: &mut ParseCtxt) -> ParseResult<TraitAssocReft> {
518    let lo = cx.lo();
519    let final_ = cx.advance_if(kw::Final);
520    cx.expect(kw::Fn)?;
521    let name = parse_ident(cx)?;
522    let params = parens(cx, Comma, |cx| parse_refine_param(cx, RequireSort::Yes))?;
523    cx.expect(token::RArrow)?;
524    let output = parse_base_sort(cx)?;
525    let body = if cx.peek(token::OpenBrace) {
526        Some(parse_block(cx)?)
527    } else {
528        cx.advance_if(token::Semi);
529        None
530    };
531    let hi = cx.hi();
532    Ok(TraitAssocReft { name, params, output, body, span: cx.mk_span(lo, hi), final_ })
533}
534
535pub(crate) fn parse_impl_assoc_refts(cx: &mut ParseCtxt) -> ParseResult<Vec<ImplAssocReft>> {
536    until(cx, token::Eof, parse_impl_assoc_reft)
537}
538
539/// ```text
540/// ⟨impl_assoc_reft⟩ := fn ⟨ident⟩ ( ⟨refine_param⟩,* ) -> ⟨base_sort⟩ ⟨block⟩
541/// ```
542fn parse_impl_assoc_reft(cx: &mut ParseCtxt) -> ParseResult<ImplAssocReft> {
543    let lo = cx.lo();
544    cx.expect(kw::Fn)?;
545    let name = parse_ident(cx)?;
546    let params = parens(cx, Comma, |cx| parse_refine_param(cx, RequireSort::Yes))?;
547    cx.expect(token::RArrow)?;
548    let output = parse_base_sort(cx)?;
549    let body = parse_block(cx)?;
550    let hi = cx.hi();
551    Ok(ImplAssocReft { name, params, output, body, span: cx.mk_span(lo, hi) })
552}
553
554/// ```text
555/// ⟨refined_by⟩ := ⟨refine_param⟩,*
556/// ```
557pub(crate) fn parse_refined_by(cx: &mut ParseCtxt) -> ParseResult<RefineParams> {
558    punctuated_until(cx, Comma, token::Eof, |cx| parse_refine_param(cx, RequireSort::Yes))
559}
560
561/// ```text
562/// ⟨variant⟩ := ⟨fields⟩ -> ⟨variant_ret⟩
563///            | ⟨fields⟩
564///            | ⟨variant_ret⟩
565/// ```
566pub(crate) fn parse_variant(cx: &mut ParseCtxt, ret_arrow: bool) -> ParseResult<VariantDef> {
567    let lo = cx.lo();
568    let mut fields = vec![];
569    let mut ret = None;
570    let ident = if ret_arrow || cx.peek2(NonReserved, token::OpenParen) {
571        Some(parse_ident(cx)?)
572    } else {
573        None
574    };
575    if cx.peek(token::OpenParen) || cx.peek(token::OpenBrace) {
576        fields = parse_fields(cx)?;
577        if cx.advance_if(token::RArrow) {
578            ret = Some(parse_variant_ret(cx)?);
579        }
580    } else {
581        if ret_arrow {
582            cx.expect(token::RArrow)?;
583        }
584        ret = Some(parse_variant_ret(cx)?);
585    };
586    let hi = cx.hi();
587    Ok(VariantDef { ident, fields, ret, node_id: cx.next_node_id(), span: cx.mk_span(lo, hi) })
588}
589
590/// ```text
591/// ⟨fields⟩ := ( ⟨ty⟩,* ) | { ⟨ty⟩,* }
592/// ```
593fn parse_fields(cx: &mut ParseCtxt) -> ParseResult<Vec<Ty>> {
594    let mut lookahead = cx.lookahead1();
595    if lookahead.peek(token::OpenParen) {
596        parens(cx, Comma, parse_type)
597    } else if lookahead.peek(token::OpenBrace) {
598        braces(cx, Comma, parse_type)
599    } else {
600        Err(lookahead.into_error())
601    }
602}
603
604/// ```text
605/// ⟨variant_ret⟩ := ⟨path⟩ ⟨ [ ⟨refine_arg⟩,? ] ⟩?
606/// ```
607fn parse_variant_ret(cx: &mut ParseCtxt) -> ParseResult<VariantRet> {
608    let path = parse_path(cx)?;
609    let indices = if cx.peek(token::OpenBracket) {
610        parse_indices(cx)?
611    } else {
612        let hi = cx.hi();
613        Indices { indices: vec![], span: cx.mk_span(hi, hi) }
614    };
615    Ok(VariantRet { path, indices })
616}
617
618pub(crate) fn parse_type_alias(cx: &mut ParseCtxt) -> ParseResult<TyAlias> {
619    let lo = cx.lo();
620    cx.expect(kw::Type)?;
621    let ident = parse_ident(cx)?;
622    let generics = parse_opt_generics(cx)?;
623    let params = if cx.peek(token::OpenParen) {
624        parens(cx, Comma, |cx| parse_refine_param(cx, RequireSort::Yes))?
625    } else {
626        vec![]
627    };
628    let index = if cx.peek(token::OpenBracket) {
629        Some(delimited(cx, Bracket, |cx| parse_refine_param(cx, RequireSort::Yes))?)
630    } else {
631        None
632    };
633    cx.expect(token::Eq)?;
634    let ty = parse_type(cx)?;
635    let hi = cx.hi();
636    Ok(TyAlias {
637        ident,
638        generics,
639        params,
640        index,
641        ty,
642        node_id: cx.next_node_id(),
643        span: cx.mk_span(lo, hi),
644    })
645}
646
647fn parse_opt_generics(cx: &mut ParseCtxt) -> ParseResult<Generics> {
648    if !cx.peek(LAngle) {
649        let hi = cx.hi();
650        return Ok(Generics { params: vec![], predicates: None, span: cx.mk_span(hi, hi) });
651    }
652    let lo = cx.lo();
653    let params = angle(cx, Comma, parse_generic_param)?;
654    let hi = cx.hi();
655    Ok(Generics { params, predicates: None, span: cx.mk_span(lo, hi) })
656}
657
658fn parse_generic_param(cx: &mut ParseCtxt) -> ParseResult<GenericParam> {
659    let name = parse_ident(cx)?;
660    Ok(GenericParam { name, node_id: cx.next_node_id() })
661}
662
663fn invalid_ident_err(ident: &Ident) -> ParseError {
664    ParseError { kind: crate::ParseErrorKind::InvalidBinding, span: ident.span }
665}
666
667fn mut_as_strg(inputs: Vec<FnInput>, ensures: &[Ensures]) -> ParseResult<Vec<FnInput>> {
668    // 1. Gather ensures
669    let locs = ensures
670        .iter()
671        .filter_map(|ens| if let Ensures::Type(ident, _, _) = ens { Some(ident) } else { None })
672        .collect::<HashSet<_>>();
673    // 2. Walk over inputs and transform references mentioned in ensures
674    let mut res = vec![];
675    for input in inputs {
676        if let FnInput::Ty(Some(ident), _, _) = &input
677            && locs.contains(&ident)
678        {
679            // a known location: better be a mut or else, error!
680            let FnInput::Ty(Some(ident), ty, id) = input else {
681                return Err(invalid_ident_err(ident));
682            };
683            let TyKind::Ref(Mutability::Mut, inner_ty) = ty.kind else {
684                return Err(invalid_ident_err(&ident));
685            };
686            res.push(FnInput::StrgRef(ident, *inner_ty, id));
687        } else {
688            // not a known location, leave unchanged
689            res.push(input);
690        }
691    }
692    Ok(res)
693}
694
695/// ```text
696/// ⟨fn_sig⟩ := ⟨asyncness⟩ fn ⟨ident⟩?
697///             ⟨ [ ⟨refine_param⟩,* ] ⟩?
698///             ( ⟨fn_inputs⟩,* )
699///             ⟨-> ⟨ty⟩⟩?
700///             ⟨requires⟩ ⟨ensures⟩ ⟨where⟩
701/// ```
702pub(crate) fn parse_fn_sig<T: PeekExpected>(cx: &mut ParseCtxt, end: T) -> ParseResult<FnSig> {
703    let lo = cx.lo();
704    let asyncness = parse_asyncness(cx);
705    cx.expect(kw::Fn)?;
706    let ident = if cx.peek(NonReserved) { Some(parse_ident(cx)?) } else { None };
707    let mut generics = parse_opt_generics(cx)?;
708    let params = if cx.peek(token::OpenBracket) {
709        brackets(cx, Comma, |cx| parse_refine_param(cx, RequireSort::Maybe))?
710    } else {
711        vec![]
712    };
713    let inputs = parens(cx, Comma, parse_fn_input)?;
714    let returns = parse_fn_ret(cx)?;
715    let requires = parse_opt_requires(cx)?;
716    let ensures = parse_opt_ensures(cx)?;
717    let inputs = mut_as_strg(inputs, &ensures)?;
718    generics.predicates = parse_opt_where(cx)?;
719    cx.expect(end)?;
720    let hi = cx.hi();
721    Ok(FnSig {
722        asyncness,
723        generics,
724        params,
725        ident,
726        inputs,
727        requires,
728        output: FnOutput { returns, ensures, node_id: cx.next_node_id() },
729        node_id: cx.next_node_id(),
730        span: cx.mk_span(lo, hi),
731    })
732}
733
734/// ```text
735/// ⟨requires⟩ := ⟨ requires ⟨requires_clause⟩,* ⟩?
736/// ```
737fn parse_opt_requires(cx: &mut ParseCtxt) -> ParseResult<Vec<Requires>> {
738    if !cx.advance_if(kw::Requires) {
739        return Ok(vec![]);
740    }
741    punctuated_until(
742        cx,
743        Comma,
744        |t: TokenKind| t.is_keyword(kw::Ensures) || t.is_keyword(kw::Where) || t.is_eof(),
745        parse_requires_clause,
746    )
747}
748
749/// ```text
750/// ⟨requires_clause⟩ := ⟨ forall ⟨refine_param⟩,+ . ⟩? ⟨expr⟩
751/// ```
752fn parse_requires_clause(cx: &mut ParseCtxt) -> ParseResult<Requires> {
753    let mut params = vec![];
754    if cx.advance_if(kw::Forall) {
755        params = sep1(cx, Comma, |cx| parse_refine_param(cx, RequireSort::Maybe))?;
756        cx.expect(token::Dot)?;
757    }
758    let pred = parse_expr(cx, true)?;
759    Ok(Requires { params, pred })
760}
761
762/// ```text
763/// ⟨ensures⟩ := ⟨ensures ⟨ensures_clause⟩,*⟩?
764/// ```
765fn parse_opt_ensures(cx: &mut ParseCtxt) -> ParseResult<Vec<Ensures>> {
766    if !cx.advance_if(kw::Ensures) {
767        return Ok(vec![]);
768    }
769    punctuated_until(
770        cx,
771        Comma,
772        |t: TokenKind| t.is_keyword(kw::Where) || t.is_eof(),
773        parse_ensures_clause,
774    )
775}
776
777/// ```text
778/// ⟨ensures_clause⟩ :=  ⟨ident⟩ : ⟨ty⟩
779///                   |  ⟨expr⟩
780/// ```
781fn parse_ensures_clause(cx: &mut ParseCtxt) -> ParseResult<Ensures> {
782    if cx.peek2(NonReserved, token::Colon) {
783        // ⟨ident⟩ : ⟨ty⟩
784        let ident = parse_ident(cx)?;
785        cx.expect(token::Colon)?;
786        let ty = parse_type(cx)?;
787        Ok(Ensures::Type(ident, ty, cx.next_node_id()))
788    } else {
789        // ⟨expr⟩
790        Ok(Ensures::Pred(parse_expr(cx, true)?))
791    }
792}
793
794fn parse_opt_where(cx: &mut ParseCtxt) -> ParseResult<Option<Vec<WhereBoundPredicate>>> {
795    if !cx.advance_if(kw::Where) {
796        return Ok(None);
797    }
798    Ok(Some(punctuated_until(cx, Comma, token::Eof, parse_where_bound)?))
799}
800
801fn parse_where_bound(cx: &mut ParseCtxt) -> ParseResult<WhereBoundPredicate> {
802    let lo = cx.lo();
803    let bounded_ty = parse_type(cx)?;
804    cx.expect(token::Colon)?;
805    let bounds = parse_generic_bounds(cx)?;
806    let hi = cx.hi();
807    Ok(WhereBoundPredicate { span: cx.mk_span(lo, hi), bounded_ty, bounds })
808}
809
810/// ```text
811/// ⟨fn_ret⟩ := ⟨ -> ⟨ty⟩ ⟩?
812/// ```
813fn parse_fn_ret(cx: &mut ParseCtxt) -> ParseResult<FnRetTy> {
814    if cx.advance_if(token::RArrow) {
815        Ok(FnRetTy::Ty(Box::new(parse_type(cx)?)))
816    } else {
817        let hi = cx.hi();
818        Ok(FnRetTy::Default(cx.mk_span(hi, hi)))
819    }
820}
821
822/// ```text
823/// ⟨fn_input⟩ := ⟨ident⟩ : &strg ⟨ty⟩
824///             | ⟨ident⟩ : ⟨path⟩ { ⟨expr⟩ }
825///             | ⟨ident⟩ : ⟨ty⟩
826///             | ⟨ty⟩
827/// ```
828fn parse_fn_input(cx: &mut ParseCtxt) -> ParseResult<FnInput> {
829    if cx.peek2(NonReserved, token::Colon) {
830        let bind = parse_ident(cx)?;
831        cx.expect(token::Colon)?;
832        if cx.advance_if2(token::And, kw::Strg) {
833            // ⟨ident⟩ : &strg ⟨ty⟩
834            Ok(FnInput::StrgRef(bind, parse_type(cx)?, cx.next_node_id()))
835        } else if cx.peek(NonReserved) {
836            let path = parse_path(cx)?;
837            if cx.peek3(token::OpenBrace, NonReserved, token::Colon) {
838                // ⟨ident⟩ : ⟨path⟩ { ⟨ident⟩ : ⟨expr⟩ }
839                let bty = path_to_bty(path);
840                let ty = parse_bty_exists(cx, bty)?;
841                Ok(FnInput::Ty(Some(bind), ty, cx.next_node_id()))
842            } else if cx.peek(token::OpenBrace) {
843                // ⟨ident⟩ : ⟨path⟩ { ⟨expr⟩ }
844                let pred = delimited(cx, Brace, |cx| parse_expr(cx, true))?;
845                Ok(FnInput::Constr(bind, path, pred, cx.next_node_id()))
846            } else {
847                // ⟨ident⟩ : ⟨ty⟩
848                let bty = path_to_bty(path);
849                let ty = parse_bty_rhs(cx, bty)?;
850                Ok(FnInput::Ty(Some(bind), ty, cx.next_node_id()))
851            }
852        } else {
853            // ⟨ident⟩ : ⟨ty⟩
854            Ok(FnInput::Ty(Some(bind), parse_type(cx)?, cx.next_node_id()))
855        }
856    } else {
857        // ⟨ty⟩
858        Ok(FnInput::Ty(None, parse_type(cx)?, cx.next_node_id()))
859    }
860}
861
862/// ```text
863/// ⟨asyncness⟩ := async?
864/// ```
865fn parse_asyncness(cx: &mut ParseCtxt) -> Async {
866    let lo = cx.lo();
867    if cx.advance_if(kw::Async) {
868        Async::Yes { node_id: cx.next_node_id(), span: cx.mk_span(lo, cx.hi()) }
869    } else {
870        Async::No
871    }
872}
873
874/// ```text
875/// ⟨ty⟩ := _
876///       | { ⟨ident⟩ ⟨,⟨ident⟩⟩* . ⟨ty⟩ | ⟨block_expr⟩ }
877///       | ( ⟨ty⟩,* )
878///       | { ⟨ty⟩ | ⟨block_expr⟩ }
879///       | { ⟨refine_param⟩ ⟨,⟨refine_param⟩⟩* . ⟨ty⟩ | ⟨block_expr⟩ }
880///       | & mut? ⟨ty⟩
881///       | [ ⟨ty⟩ ; ⟨const_arg⟩ ]
882///       | impl ⟨path⟩
883///       | ⟨bty⟩
884///       | ⟨bty⟩ [ ⟨refine_arg⟩,* ]
885///       | ⟨bty⟩ { ⟨ident⟩ : ⟨block_expr⟩ }
886///
887/// ⟨bty⟩ := ⟨path⟩ | ⟨qpath⟩ | [ ⟨ty⟩ ]
888/// ```
889pub(crate) fn parse_type(cx: &mut ParseCtxt) -> ParseResult<Ty> {
890    let lo = cx.lo();
891    let mut lookahead = cx.lookahead1();
892    let kind = if lookahead.advance_if(kw::Underscore) {
893        TyKind::Hole
894    } else if lookahead.advance_if(token::OpenParen) {
895        // ( ⟨ty⟩,* )
896        let (mut tys, trailing) =
897            punctuated_with_trailing(cx, Comma, token::CloseParen, parse_type)?;
898        cx.expect(token::CloseParen)?;
899        if tys.len() == 1 && !trailing {
900            return Ok(tys.remove(0));
901        } else {
902            TyKind::Tuple(tys)
903        }
904    } else if lookahead.peek(token::OpenBrace) {
905        delimited(cx, Brace, |cx| {
906            if cx.peek2(NonReserved, AnyOf([token::Comma, token::Dot, token::Colon])) {
907                // { ⟨refine_param⟩ ⟨,⟨refine_param⟩⟩* . ⟨ty⟩ | ⟨block_expr⟩ }
908                parse_general_exists(cx)
909            } else {
910                // { ⟨ty⟩ | ⟨block_expr⟩ }
911                let ty = parse_type(cx)?;
912                cx.expect(token::Or)?;
913                let pred = parse_block_expr(cx)?;
914                Ok(TyKind::Constr(pred, Box::new(ty)))
915            }
916        })?
917    } else if lookahead.advance_if(token::And) {
918        //  & mut? ⟨ty⟩
919        let mutbl = if cx.advance_if(kw::Mut) { Mutability::Mut } else { Mutability::Not };
920        TyKind::Ref(mutbl, Box::new(parse_type(cx)?))
921    } else if lookahead.advance_if(token::OpenBracket) {
922        let ty = parse_type(cx)?;
923        if cx.advance_if(token::Semi) {
924            // [ ⟨ty⟩ ; ⟨const_arg⟩ ]
925            let len = parse_const_arg(cx)?;
926            cx.expect(token::CloseBracket)?;
927            TyKind::Array(Box::new(ty), len)
928        } else {
929            // [ ⟨ty⟩ ] ...
930            cx.expect(token::CloseBracket)?;
931            let span = cx.mk_span(lo, cx.hi());
932            let kind = BaseTyKind::Slice(Box::new(ty));
933            return parse_bty_rhs(cx, BaseTy { kind, span });
934        }
935    } else if lookahead.advance_if(kw::Impl) {
936        // impl ⟨bounds⟩
937        TyKind::ImplTrait(cx.next_node_id(), parse_generic_bounds(cx)?)
938    } else if lookahead.peek(NonReserved) {
939        // ⟨path⟩ ...
940        let path = parse_path(cx)?;
941        let bty = path_to_bty(path);
942        return parse_bty_rhs(cx, bty);
943    } else if lookahead.peek(LAngle) {
944        // ⟨qpath⟩ ...
945        let bty = parse_qpath(cx)?;
946        return parse_bty_rhs(cx, bty);
947    } else {
948        return Err(lookahead.into_error());
949    };
950    let hi = cx.hi();
951    Ok(Ty { kind, node_id: cx.next_node_id(), span: cx.mk_span(lo, hi) })
952}
953
954/// ```text
955/// ⟨qpath⟩ := < ⟨ty⟩ as ⟨segments⟩> :: ⟨segments⟩
956/// ```
957fn parse_qpath(cx: &mut ParseCtxt) -> ParseResult<BaseTy> {
958    let lo = cx.lo();
959    cx.expect(LAngle)?;
960    let qself = parse_type(cx)?;
961    cx.expect(kw::As)?;
962    let mut segments = parse_segments(cx)?;
963    cx.expect(RAngle)?;
964    cx.expect(token::PathSep)?;
965    segments.extend(parse_segments(cx)?);
966    let hi = cx.hi();
967
968    let span = cx.mk_span(lo, hi);
969    let path = Path { segments, refine: vec![], node_id: cx.next_node_id(), span };
970    let kind = BaseTyKind::Path(Some(Box::new(qself)), path);
971    Ok(BaseTy { kind, span })
972}
973
974/// ```text
975/// { ⟨refine_param⟩ ⟨,⟨refine_param⟩⟩* . ⟨ty⟩ | ⟨block_expr⟩ }
976/// ```
977fn parse_general_exists(cx: &mut ParseCtxt) -> ParseResult<TyKind> {
978    let params = sep1(cx, Comma, |cx| parse_refine_param(cx, RequireSort::Maybe))?;
979    cx.expect(token::Dot)?;
980    let ty = parse_type(cx)?;
981    let pred = if cx.advance_if(token::Or) { Some(parse_block_expr(cx)?) } else { None };
982    Ok(TyKind::GeneralExists { params, ty: Box::new(ty), pred })
983}
984
985/// ```text
986///    ⟨bty⟩ [ ⟨refine_arg⟩,* ]
987/// |  ⟨bty⟩ { ⟨ident⟩ : ⟨block_expr⟩ }
988/// |  ⟨bty⟩
989/// ```
990fn parse_bty_rhs(cx: &mut ParseCtxt, bty: BaseTy) -> ParseResult<Ty> {
991    let lo = bty.span.lo();
992    if cx.peek(token::OpenBracket) {
993        // ⟨bty⟩ [ ⟨refine_arg⟩,* ]
994        let indices = parse_indices(cx)?;
995        let hi = cx.hi();
996        let kind = TyKind::Indexed { bty, indices };
997        Ok(Ty { kind, node_id: cx.next_node_id(), span: cx.mk_span(lo, hi) })
998    } else if cx.peek(token::OpenBrace) {
999        // ⟨bty⟩ { ⟨ident⟩ : ⟨block_expr⟩ }
1000        parse_bty_exists(cx, bty)
1001    } else {
1002        // ⟨bty⟩
1003        let hi = cx.hi();
1004        let kind = TyKind::Base(bty);
1005        Ok(Ty { kind, node_id: cx.next_node_id(), span: cx.mk_span(lo, hi) })
1006    }
1007}
1008
1009/// ```text
1010/// ⟨bty⟩ { ⟨ident⟩ : ⟨block_expr⟩ }
1011/// ```
1012fn parse_bty_exists(cx: &mut ParseCtxt, bty: BaseTy) -> ParseResult<Ty> {
1013    let lo = bty.span.lo();
1014    delimited(cx, Brace, |cx| {
1015        let bind = parse_ident(cx)?;
1016        cx.expect(token::Colon)?;
1017        let pred = parse_block_expr(cx)?;
1018        let hi = cx.hi();
1019        let kind = TyKind::Exists { bind, bty, pred };
1020        Ok(Ty { kind, node_id: cx.next_node_id(), span: cx.mk_span(lo, hi) })
1021    })
1022}
1023
1024fn path_to_bty(path: Path) -> BaseTy {
1025    let span = path.span;
1026    BaseTy { kind: BaseTyKind::Path(None, path), span }
1027}
1028
1029fn parse_indices(cx: &mut ParseCtxt) -> ParseResult<Indices> {
1030    let lo = cx.lo();
1031    let indices = brackets(cx, Comma, parse_refine_arg)?;
1032    let hi = cx.hi();
1033    Ok(Indices { indices, span: cx.mk_span(lo, hi) })
1034}
1035
1036fn parse_fn_bound_input(cx: &mut ParseCtxt) -> ParseResult<GenericArg> {
1037    let lo = cx.lo();
1038    let tys = parens(cx, Comma, parse_type)?;
1039    let hi = cx.hi();
1040    let kind = TyKind::Tuple(tys);
1041    let span = cx.mk_span(lo, hi);
1042    let in_ty = Ty { kind, node_id: cx.next_node_id(), span };
1043    Ok(GenericArg { kind: GenericArgKind::Type(in_ty), node_id: cx.next_node_id() })
1044}
1045
1046fn parse_fn_bound_output(cx: &mut ParseCtxt) -> ParseResult<GenericArg> {
1047    let lo = cx.lo();
1048
1049    let ty = if cx.advance_if(token::RArrow) {
1050        parse_type(cx)?
1051    } else {
1052        Ty { kind: TyKind::Tuple(vec![]), node_id: cx.next_node_id(), span: cx.mk_span(lo, lo) }
1053    };
1054    let hi = cx.hi();
1055    let ident = Ident { name: Output, span: cx.mk_span(lo, hi) };
1056    Ok(GenericArg { kind: GenericArgKind::Constraint(ident, ty), node_id: cx.next_node_id() })
1057}
1058
1059fn parse_fn_bound_path(cx: &mut ParseCtxt) -> ParseResult<Path> {
1060    let lo = cx.lo();
1061    let ident = parse_ident(cx)?;
1062    let in_arg = parse_fn_bound_input(cx)?;
1063    let out_arg = parse_fn_bound_output(cx)?;
1064    let args = vec![in_arg, out_arg];
1065    let segment = PathSegment { ident, args, node_id: cx.next_node_id() };
1066    let hi = cx.hi();
1067    Ok(Path {
1068        segments: vec![segment],
1069        refine: vec![],
1070        node_id: cx.next_node_id(),
1071        span: cx.mk_span(lo, hi),
1072    })
1073}
1074
1075fn parse_generic_bounds(cx: &mut ParseCtxt) -> ParseResult<GenericBounds> {
1076    let path = if cx.peek(sym::FnOnce) || cx.peek(sym::FnMut) || cx.peek(sym::Fn) {
1077        parse_fn_bound_path(cx)?
1078    } else {
1079        parse_path(cx)?
1080    };
1081    Ok(vec![TraitRef { path, node_id: cx.next_node_id() }])
1082}
1083
1084fn parse_const_arg(cx: &mut ParseCtxt) -> ParseResult<ConstArg> {
1085    let lo = cx.lo();
1086    let mut lookahead = cx.lookahead1();
1087    let kind = if lookahead.peek(AnyLit) {
1088        let len = parse_int(cx)?;
1089        ConstArgKind::Lit(len)
1090    } else if lookahead.advance_if(kw::Underscore) {
1091        ConstArgKind::Infer
1092    } else {
1093        return Err(lookahead.into_error());
1094    };
1095    let hi = cx.hi();
1096    Ok(ConstArg { kind, span: cx.mk_span(lo, hi) })
1097}
1098
1099/// ```text
1100/// ⟨path⟩ := ⟨segments⟩ ⟨ ( ⟨refine_arg⟩,* ) ⟩?
1101/// ```
1102fn parse_path(cx: &mut ParseCtxt) -> ParseResult<Path> {
1103    let lo = cx.lo();
1104    let segments = parse_segments(cx)?;
1105    let refine =
1106        if cx.peek(token::OpenParen) { parens(cx, Comma, parse_refine_arg)? } else { vec![] };
1107    let hi = cx.hi();
1108    Ok(Path { segments, refine, node_id: cx.next_node_id(), span: cx.mk_span(lo, hi) })
1109}
1110
1111/// ```text
1112/// ⟨segments⟩ := ⟨segment⟩ ⟨:: ⟨segment⟩ ⟩*
1113/// ```
1114fn parse_segments(cx: &mut ParseCtxt) -> ParseResult<Vec<PathSegment>> {
1115    sep1(cx, token::PathSep, parse_segment)
1116}
1117
1118/// ```text
1119/// ⟨segment⟩ := ⟨ident⟩ ⟨ < ⟨generic_arg⟩,* > ⟩?
1120/// ```
1121fn parse_segment(cx: &mut ParseCtxt) -> ParseResult<PathSegment> {
1122    let ident = parse_ident(cx)?;
1123    let args = opt_angle(cx, Comma, parse_generic_arg)?;
1124    Ok(PathSegment { ident, node_id: cx.next_node_id(), args })
1125}
1126
1127/// ```text
1128/// ⟨generic_arg⟩ := ⟨ty⟩ | ⟨ident⟩ = ⟨ty⟩
1129/// ```
1130fn parse_generic_arg(cx: &mut ParseCtxt) -> ParseResult<GenericArg> {
1131    let kind = if cx.peek2(NonReserved, token::Eq) {
1132        let ident = parse_ident(cx)?;
1133        cx.expect(token::Eq)?;
1134        let ty = parse_type(cx)?;
1135        GenericArgKind::Constraint(ident, ty)
1136    } else {
1137        GenericArgKind::Type(parse_type(cx)?)
1138    };
1139    Ok(GenericArg { kind, node_id: cx.next_node_id() })
1140}
1141
1142/// ```text
1143/// ⟨refine_arg⟩ :=  @ ⟨ident⟩
1144///               |  # ⟨ident⟩
1145///               |  |⟨⟨refine_parm⟩,*| ⟨expr⟩
1146///               |  ⟨expr⟩
1147/// ```
1148fn parse_refine_arg(cx: &mut ParseCtxt) -> ParseResult<RefineArg> {
1149    let lo = cx.lo();
1150    let arg = if cx.advance_if(token::At) {
1151        // @ ⟨ident⟩
1152        let bind = parse_ident(cx)?;
1153        let hi = cx.hi();
1154        RefineArg::Bind(bind, BindKind::At, cx.mk_span(lo, hi), cx.next_node_id())
1155    } else if cx.advance_if(token::Pound) {
1156        // # ⟨ident⟩
1157        let bind = parse_ident(cx)?;
1158        let hi = cx.hi();
1159        RefineArg::Bind(bind, BindKind::Pound, cx.mk_span(lo, hi), cx.next_node_id())
1160    } else if cx.advance_if(Or) {
1161        let params =
1162            punctuated_until(cx, Comma, Or, |cx| parse_refine_param(cx, RequireSort::Maybe))?;
1163        cx.expect(Or)?;
1164        let body = parse_expr(cx, true)?;
1165        let hi = cx.hi();
1166        RefineArg::Abs(params, body, cx.mk_span(lo, hi), cx.next_node_id())
1167    } else {
1168        // ⟨expr⟩
1169        RefineArg::Expr(parse_expr(cx, true)?)
1170    };
1171    Ok(arg)
1172}
1173
1174/// Whether a sort is required in a refinement parameter declaration.
1175enum RequireSort {
1176    /// Definitely require a sort
1177    Yes,
1178    /// Optional sort. Use [`Sort::Infer`] if not present
1179    Maybe,
1180    /// Definitely do not not require a sort. Always use [`Sort::Infer`]
1181    No,
1182}
1183
1184fn parse_sort_if_required(cx: &mut ParseCtxt, require_sort: RequireSort) -> ParseResult<Sort> {
1185    match require_sort {
1186        RequireSort::No => Ok(Sort::Infer),
1187        RequireSort::Maybe => {
1188            if cx.advance_if(token::Colon) {
1189                parse_sort(cx)
1190            } else {
1191                Ok(Sort::Infer)
1192            }
1193        }
1194        RequireSort::Yes => {
1195            cx.expect(token::Colon)?;
1196            parse_sort(cx)
1197        }
1198    }
1199}
1200
1201/// ```text
1202/// ⟨refine_param⟩ := ⟨mode⟩? ⟨ident⟩ ⟨ : ⟨sort⟩ ⟩?    if require_sort is Maybe
1203///                 | ⟨mode⟩? ⟨ident⟩ : ⟨sort⟩         if require_sort is Yes
1204///                 | ⟨mode⟩? ⟨ident⟩                  if require_sort is No
1205/// ```
1206fn parse_refine_param(cx: &mut ParseCtxt, require_sort: RequireSort) -> ParseResult<RefineParam> {
1207    let lo = cx.lo();
1208    let mode = parse_opt_param_mode(cx);
1209    let ident = parse_ident(cx)?;
1210    let sort = parse_sort_if_required(cx, require_sort)?;
1211    let hi = cx.hi();
1212    Ok(RefineParam { mode, ident, sort, span: cx.mk_span(lo, hi), node_id: cx.next_node_id() })
1213}
1214
1215/// ```text
1216/// ⟨mode⟩ := ⟨ hrn | hdl ⟩?
1217/// ```
1218fn parse_opt_param_mode(cx: &mut ParseCtxt) -> Option<ParamMode> {
1219    if cx.advance_if(kw::Hrn) {
1220        Some(ParamMode::Horn)
1221    } else if cx.advance_if(kw::Hdl) {
1222        Some(ParamMode::Hindley)
1223    } else {
1224        None
1225    }
1226}
1227
1228pub(crate) fn parse_expr(cx: &mut ParseCtxt, allow_struct: bool) -> ParseResult<Expr> {
1229    parse_binops(cx, Precedence::MIN, allow_struct)
1230}
1231
1232fn parse_binops(cx: &mut ParseCtxt, base: Precedence, allow_struct: bool) -> ParseResult<Expr> {
1233    let mut lhs = unary_expr(cx, allow_struct)?;
1234    loop {
1235        let lo = cx.lo();
1236        let Some((op, ntokens)) = cx.peek_binop() else { break };
1237        let precedence = Precedence::of_binop(&op);
1238        if precedence < base {
1239            break;
1240        }
1241        cx.advance_by(ntokens);
1242        let next = match precedence.associativity() {
1243            Associativity::Right => precedence,
1244            Associativity::Left => precedence.next(),
1245            Associativity::None => {
1246                if let ExprKind::BinaryOp(op, ..) = &lhs.kind
1247                    && Precedence::of_binop(op) == precedence
1248                {
1249                    return Err(cx.cannot_be_chained(lo, cx.hi()));
1250                }
1251                precedence.next()
1252            }
1253        };
1254        let rhs = parse_binops(cx, next, allow_struct)?;
1255        let span = lhs.span.to(rhs.span);
1256        lhs = Expr {
1257            kind: ExprKind::BinaryOp(op, Box::new([lhs, rhs])),
1258            node_id: cx.next_node_id(),
1259            span,
1260        }
1261    }
1262    Ok(lhs)
1263}
1264
1265/// ```text
1266/// ⟨unary_expr⟩ := - ⟨unary_expr⟩ | ! ⟨unary_expr⟩ | ⟨trailer_expr⟩
1267/// ```
1268fn unary_expr(cx: &mut ParseCtxt, allow_struct: bool) -> ParseResult<Expr> {
1269    let lo = cx.lo();
1270    let kind = if cx.advance_if(token::Minus) {
1271        ExprKind::UnaryOp(UnOp::Neg, Box::new(unary_expr(cx, allow_struct)?))
1272    } else if cx.advance_if(token::Bang) {
1273        ExprKind::UnaryOp(UnOp::Not, Box::new(unary_expr(cx, allow_struct)?))
1274    } else {
1275        return parse_trailer_expr(cx, allow_struct);
1276    };
1277    let hi = cx.hi();
1278    Ok(Expr { kind, node_id: cx.next_node_id(), span: cx.mk_span(lo, hi) })
1279}
1280
1281/// ```text
1282/// ⟨trailer_expr⟩ :=  ⟨trailer⟩ . ⟨ident⟩
1283///                 |  ⟨trailer⟩ ( ⟨expr⟩,* )
1284///                 |  ⟨atom⟩
1285/// ```
1286fn parse_trailer_expr(cx: &mut ParseCtxt, allow_struct: bool) -> ParseResult<Expr> {
1287    let lo = cx.lo();
1288    let mut e = parse_atom(cx, allow_struct)?;
1289    loop {
1290        let kind = if cx.advance_if(token::Dot) {
1291            // ⟨trailer⟩ . ⟨ident⟩
1292            let field = parse_ident(cx)?;
1293            ExprKind::Dot(Box::new(e), field)
1294        } else if cx.peek(token::OpenParen) {
1295            // ⟨trailer⟩ ( ⟨expr⟩,* )
1296            let args = parens(cx, Comma, |cx| parse_expr(cx, true))?;
1297            ExprKind::Call(Box::new(e), args)
1298        } else {
1299            break;
1300        };
1301        let hi = cx.hi();
1302        e = Expr { kind, node_id: cx.next_node_id(), span: cx.mk_span(lo, hi) };
1303    }
1304    Ok(e)
1305}
1306
1307/// ```text
1308/// ⟨atom⟩ := ⟨if_expr⟩
1309///         | ⟨lit⟩
1310///         | ( ⟨expr⟩ )
1311///         | ⟨epath⟩
1312///         | ⟨bounded_quant⟩
1313///         |  <⟨ty⟩ as ⟨path⟩> :: ⟨ident⟩
1314///         | [binop]
1315///         | ⟨epath⟩ { ⟨constructor_arg⟩,* }    if allow_struct
1316///         | { ⟨constructor_arg⟩,* }            if allow_struct
1317/// ```
1318fn parse_atom(cx: &mut ParseCtxt, allow_struct: bool) -> ParseResult<Expr> {
1319    let lo = cx.lo();
1320    let mut lookahead = cx.lookahead1();
1321    if lookahead.peek(kw::If) {
1322        // ⟨if_expr⟩
1323        parse_if_expr(cx)
1324    } else if lookahead.peek(AnyLit) {
1325        // ⟨lit⟩
1326        parse_lit(cx)
1327    } else if lookahead.peek(token::OpenParen) {
1328        delimited(cx, Parenthesis, |cx| parse_expr(cx, true))
1329    } else if lookahead.peek(NonReserved) {
1330        let path = parse_expr_path(cx)?;
1331        let kind = if allow_struct && cx.peek(token::OpenBrace) {
1332            // ⟨epath⟩ { ⟨constructor_arg⟩,* }
1333            let args = braces(cx, Comma, parse_constructor_arg)?;
1334            ExprKind::Constructor(Some(path), args)
1335        } else {
1336            // ⟨epath⟩
1337            ExprKind::Path(path)
1338        };
1339        let hi = cx.hi();
1340        Ok(Expr { kind, node_id: cx.next_node_id(), span: cx.mk_span(lo, hi) })
1341    } else if allow_struct && lookahead.peek(token::OpenBrace) {
1342        // { ⟨constructor_arg⟩,* }
1343        let args = braces(cx, Comma, parse_constructor_arg)?;
1344        let hi = cx.hi();
1345        Ok(Expr {
1346            kind: ExprKind::Constructor(None, args),
1347            node_id: cx.next_node_id(),
1348            span: cx.mk_span(lo, hi),
1349        })
1350    } else if lookahead.advance_if(LAngle) {
1351        // <⟨ty⟩ as ⟨path⟩> :: ⟨ident⟩
1352        let lo = cx.lo();
1353        let qself = parse_type(cx)?;
1354        cx.expect(kw::As)?;
1355        let path = parse_path(cx)?;
1356        cx.expect(RAngle)?;
1357        cx.expect(token::PathSep)?;
1358        let name = parse_ident(cx)?;
1359        let hi = cx.hi();
1360        let kind = ExprKind::AssocReft(Box::new(qself), path, name);
1361        Ok(Expr { kind, node_id: cx.next_node_id(), span: cx.mk_span(lo, hi) })
1362    } else if lookahead.peek(token::OpenBracket) {
1363        parse_prim_uif(cx)
1364    } else if lookahead.peek(kw::Exists) || lookahead.peek(kw::Forall) {
1365        parse_bounded_quantifier(cx)
1366    } else {
1367        Err(lookahead.into_error())
1368    }
1369}
1370
1371fn parse_prim_uif(cx: &mut ParseCtxt) -> ParseResult<Expr> {
1372    let lo = cx.lo();
1373    cx.expect(token::OpenBracket)?;
1374    let op = parse_binop(cx)?;
1375    cx.expect(token::CloseBracket)?;
1376    let hi = cx.hi();
1377    Ok(Expr { kind: ExprKind::PrimUIF(op), node_id: cx.next_node_id(), span: cx.mk_span(lo, hi) })
1378}
1379
1380/// ```text
1381/// ⟨bounded_quant⟩ := forall ⟨refine_param⟩ in ⟨int⟩..⟨int⟩ ⟨block⟩
1382///                  | exists ⟨refine_param⟩ in ⟨int⟩..⟨int⟩ ⟨block⟩
1383/// ```
1384fn parse_bounded_quantifier(cx: &mut ParseCtxt) -> ParseResult<Expr> {
1385    let lo = cx.lo();
1386    let mut lookahead = cx.lookahead1();
1387    let quant = if lookahead.advance_if(kw::Forall) {
1388        QuantKind::Forall
1389    } else if lookahead.advance_if(kw::Exists) {
1390        QuantKind::Exists
1391    } else {
1392        return Err(lookahead.into_error());
1393    };
1394    let param = parse_refine_param(cx, RequireSort::Maybe)?;
1395    cx.expect(kw::In)?;
1396    let start = parse_int(cx)?;
1397    cx.expect(token::DotDot)?;
1398    let end = parse_int(cx)?;
1399    let body = parse_block(cx)?;
1400    let hi = cx.hi();
1401    Ok(Expr {
1402        kind: ExprKind::BoundedQuant(quant, param, start..end, Box::new(body)),
1403        node_id: cx.next_node_id(),
1404        span: cx.mk_span(lo, hi),
1405    })
1406}
1407
1408/// ```text
1409/// ⟨constructor_arg⟩ :=  ⟨ident⟩ : ⟨expr⟩ |  ..
1410/// ```
1411fn parse_constructor_arg(cx: &mut ParseCtxt) -> ParseResult<ConstructorArg> {
1412    let lo = cx.lo();
1413    let mut lookahead = cx.lookahead1();
1414    if lookahead.peek(NonReserved) {
1415        let ident = parse_ident(cx)?;
1416        cx.expect(token::Colon)?;
1417        let expr = parse_expr(cx, true)?;
1418        let hi = cx.hi();
1419        Ok(ConstructorArg::FieldExpr(FieldExpr {
1420            ident,
1421            expr,
1422            node_id: cx.next_node_id(),
1423            span: cx.mk_span(lo, hi),
1424        }))
1425    } else if lookahead.advance_if(token::DotDot) {
1426        let spread = parse_expr(cx, true)?;
1427        let hi = cx.hi();
1428        Ok(ConstructorArg::Spread(Spread {
1429            expr: spread,
1430            node_id: cx.next_node_id(),
1431            span: cx.mk_span(lo, hi),
1432        }))
1433    } else {
1434        Err(lookahead.into_error())
1435    }
1436}
1437
1438/// `⟨epath⟩ := ⟨ident⟩ ⟨ :: ⟨ident⟩ ⟩*`
1439fn parse_expr_path(cx: &mut ParseCtxt) -> ParseResult<ExprPath> {
1440    let lo = cx.lo();
1441    let segments = sep1(cx, token::PathSep, parse_expr_path_segment)?;
1442    let hi = cx.hi();
1443    Ok(ExprPath { segments, node_id: cx.next_node_id(), span: cx.mk_span(lo, hi) })
1444}
1445
1446fn parse_expr_path_segment(cx: &mut ParseCtxt) -> ParseResult<ExprPathSegment> {
1447    Ok(ExprPathSegment { ident: parse_ident(cx)?, node_id: cx.next_node_id() })
1448}
1449
1450/// `⟨if_expr⟩ := if ⟨expr⟩ ⟨block⟩ ⟨ else if ⟨expr⟩ ⟨block⟩ ⟩* else ⟨block⟩`
1451///
1452/// The `⟨expr⟩` in conditions is parsed with `allow_struct = false`
1453fn parse_if_expr(cx: &mut ParseCtxt) -> ParseResult<Expr> {
1454    let mut branches = vec![];
1455
1456    loop {
1457        let lo = cx.lo();
1458        cx.expect(kw::If)?;
1459        let cond = parse_expr(cx, false)?;
1460        let then_ = parse_block(cx)?;
1461        branches.push((lo, cond, then_));
1462        cx.expect(kw::Else)?;
1463
1464        if !cx.peek(kw::If) {
1465            break;
1466        }
1467    }
1468    let mut else_ = parse_block(cx)?;
1469
1470    let hi = cx.hi();
1471    while let Some((lo, cond, then_)) = branches.pop() {
1472        else_ = Expr {
1473            kind: ExprKind::IfThenElse(Box::new([cond, then_, else_])),
1474            node_id: cx.next_node_id(),
1475            span: cx.mk_span(lo, hi),
1476        };
1477    }
1478    Ok(else_)
1479}
1480
1481/// `⟨block⟩ := { ⟨block_expr⟩ }`
1482fn parse_block(cx: &mut ParseCtxt) -> ParseResult<Expr> {
1483    delimited(cx, Brace, parse_block_expr)
1484}
1485
1486/// `⟨block_expr⟩ = ⟨let_decl⟩* ⟨expr⟩`
1487fn parse_block_expr(cx: &mut ParseCtxt) -> ParseResult<Expr> {
1488    let lo = cx.lo();
1489    let decls = repeat_while(cx, kw::Let, parse_let_decl)?;
1490    let body = parse_expr(cx, true)?;
1491    let hi = cx.hi();
1492
1493    if decls.is_empty() {
1494        Ok(body)
1495    } else {
1496        let kind = ExprKind::Block(decls, Box::new(body));
1497        Ok(Expr { kind, node_id: cx.next_node_id(), span: cx.mk_span(lo, hi) })
1498    }
1499}
1500
1501/// `⟨let_decl⟩ := let ⟨refine_param⟩ = ⟨expr⟩ ;`
1502fn parse_let_decl(cx: &mut ParseCtxt) -> ParseResult<LetDecl> {
1503    cx.expect(kw::Let)?;
1504    let param = parse_refine_param(cx, RequireSort::Maybe)?;
1505    cx.expect(token::Eq)?;
1506    let init = parse_expr(cx, true)?;
1507    cx.expect(token::Semi)?;
1508    Ok(LetDecl { param, init })
1509}
1510
1511/// ```text
1512/// ⟨lit⟩ := ⟨a Rust literal like an integer or a boolean⟩
1513/// ```
1514fn parse_lit(cx: &mut ParseCtxt) -> ParseResult<Expr> {
1515    if let Token { kind: token::Literal(lit), lo, hi } = cx.at(0) {
1516        cx.advance();
1517        Ok(Expr {
1518            kind: ExprKind::Literal(lit),
1519            node_id: cx.next_node_id(),
1520            span: cx.mk_span(lo, hi),
1521        })
1522    } else {
1523        Err(cx.unexpected_token(vec![AnyLit.expected()]))
1524    }
1525}
1526
1527fn parse_ident(cx: &mut ParseCtxt) -> ParseResult<Ident> {
1528    if let Token { kind: token::Ident(name, is_raw), lo, hi } = cx.at(0)
1529        && (!cx.is_reserved(name) || is_raw == IdentIsRaw::Yes)
1530    {
1531        cx.advance();
1532        return Ok(Ident { name, span: cx.mk_span(lo, hi) });
1533    }
1534    Err(cx.unexpected_token(vec![NonReserved.expected()]))
1535}
1536
1537fn parse_int<T: FromStr>(cx: &mut ParseCtxt) -> ParseResult<T> {
1538    if let token::Literal(lit) = cx.at(0).kind
1539        && let LitKind::Integer = lit.kind
1540        && let Ok(value) = lit.symbol.as_str().parse::<T>()
1541    {
1542        cx.advance();
1543        return Ok(value);
1544    }
1545
1546    Err(cx.unexpected_token(vec![Expected::Str(std::any::type_name::<T>())]))
1547}
1548
1549/// ```text
1550/// ⟨sort⟩ :=  ⟨base_sort⟩
1551///         |  ( ⟨base_sort⟩,* ) -> ⟨base_sort⟩
1552///         |  ⟨base_sort⟩ -> ⟨base_sort⟩
1553/// ```
1554fn parse_sort(cx: &mut ParseCtxt) -> ParseResult<Sort> {
1555    if cx.peek(token::OpenParen) {
1556        // ( ⟨base_sort⟩,* ) -> ⟨base_sort⟩
1557        let inputs = parens(cx, Comma, parse_base_sort)?;
1558        cx.expect(token::RArrow)?;
1559        let output = parse_base_sort(cx)?;
1560        Ok(Sort::Func { inputs, output })
1561    } else {
1562        let bsort = parse_base_sort(cx)?;
1563        if cx.advance_if(token::RArrow) {
1564            // ⟨base_sort⟩ -> ⟨base_sort⟩
1565            let output = parse_base_sort(cx)?;
1566            Ok(Sort::Func { inputs: vec![bsort], output })
1567        } else {
1568            // ⟨base_sort⟩
1569            Ok(Sort::Base(bsort))
1570        }
1571    }
1572}
1573
1574/// ```text
1575/// ⟨base_sort⟩ := bitvec < ⟨u32⟩ >
1576///              | ⟨sort_path⟩ < ⟨base_sort⟩,* >
1577///              | < ⟨ty⟩ as ⟨path⟩ > :: ⟨segment⟩
1578/// ⟨sort_path⟩ := ⟨ident⟩ ⟨ :: ⟨ident⟩ ⟩* < (⟨base_sort⟩,*) >
1579/// ```
1580fn parse_base_sort(cx: &mut ParseCtxt) -> ParseResult<BaseSort> {
1581    if cx.advance_if(kw::Bitvec) {
1582        // bitvec < ⟨u32⟩ >
1583        cx.expect(LAngle)?;
1584        let len = parse_int(cx)?;
1585        cx.expect(RAngle)?;
1586        Ok(BaseSort::BitVec(len))
1587    } else if cx.advance_if(LAngle) {
1588        // < ⟨ty⟩ as ⟨path⟩ > :: ⟨segment⟩
1589        let qself = parse_type(cx)?;
1590        cx.expect(kw::As)?;
1591        let mut path = parse_path(cx)?;
1592        cx.expect(RAngle)?;
1593        cx.expect(token::PathSep)?;
1594        path.segments.push(parse_segment(cx)?);
1595        Ok(BaseSort::SortOf(Box::new(qself), path))
1596    } else {
1597        // ⟨sort_path⟩ < ⟨base_sort⟩,* >
1598        let segments = sep1(cx, token::PathSep, parse_ident)?;
1599        let args = opt_angle(cx, Comma, parse_base_sort)?;
1600        let path = SortPath { segments, args, node_id: cx.next_node_id() };
1601        Ok(BaseSort::Path(path))
1602    }
1603}
1604
1605// Reference: https://doc.rust-lang.org/reference/expressions.html#expression-precedence
1606#[derive(Clone, Copy, PartialEq, PartialOrd, Debug)]
1607enum Precedence {
1608    /// <=>
1609    Iff,
1610    /// =>
1611    Implies,
1612    /// ||
1613    Or,
1614    /// &&
1615    And,
1616    /// == != < > <= >=
1617    Compare,
1618    /// |
1619    BitOr,
1620    /// ^
1621    BitXor,
1622    /// &
1623    BitAnd,
1624    /// << >>
1625    Shift,
1626    /// + -
1627    Sum,
1628    /// * / %
1629    Product,
1630    /// unary - and !
1631    Prefix,
1632}
1633
1634enum Associativity {
1635    Right,
1636    Left,
1637    None,
1638}
1639
1640impl Precedence {
1641    const MIN: Self = Precedence::Iff;
1642
1643    fn of_binop(op: &BinOp) -> Precedence {
1644        match op {
1645            BinOp::Iff => Precedence::Iff,
1646            BinOp::Imp => Precedence::Implies,
1647            BinOp::Or => Precedence::Or,
1648            BinOp::And => Precedence::And,
1649            BinOp::Eq | BinOp::Ne | BinOp::Gt | BinOp::Ge | BinOp::Lt | BinOp::Le => {
1650                Precedence::Compare
1651            }
1652            BinOp::BitOr => Precedence::BitOr,
1653            BinOp::BitXor => Precedence::BitXor,
1654            BinOp::BitAnd => Precedence::BitAnd,
1655            BinOp::BitShl | BinOp::BitShr => Precedence::Shift,
1656            BinOp::Add | BinOp::Sub => Precedence::Sum,
1657            BinOp::Mul | BinOp::Div | BinOp::Mod => Precedence::Product,
1658        }
1659    }
1660
1661    fn next(self) -> Precedence {
1662        match self {
1663            Precedence::Iff => Precedence::Implies,
1664            Precedence::Implies => Precedence::Or,
1665            Precedence::Or => Precedence::And,
1666            Precedence::And => Precedence::Compare,
1667            Precedence::Compare => Precedence::BitOr,
1668            Precedence::BitOr => Precedence::BitXor,
1669            Precedence::BitXor => Precedence::BitAnd,
1670            Precedence::BitAnd => Precedence::Shift,
1671            Precedence::Shift => Precedence::Sum,
1672            Precedence::Sum => Precedence::Product,
1673            Precedence::Product => Precedence::Prefix,
1674            Precedence::Prefix => Precedence::Prefix,
1675        }
1676    }
1677
1678    fn associativity(self) -> Associativity {
1679        match self {
1680            Precedence::Or
1681            | Precedence::And
1682            | Precedence::BitOr
1683            | Precedence::BitXor
1684            | Precedence::BitAnd
1685            | Precedence::Shift
1686            | Precedence::Sum
1687            | Precedence::Product => Associativity::Left,
1688            Precedence::Compare | Precedence::Iff => Associativity::None,
1689            Precedence::Implies | Precedence::Prefix => Associativity::Right,
1690        }
1691    }
1692}