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