flux_syntax/parser/
mod.rs

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

flux_syntax/parser/
mod.rs
