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

flux_syntax/parser/
mod.rs
