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