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

flux_syntax/parser/
mod.rs
