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 BaseSort, BaseTy, BaseTyKind, BinOp, BindKind, ConstArg, ConstArgKind, ConstructorArg,
19 DetachedInherentImpl, DetachedItem, DetachedItemKind, DetachedSpecs, DetachedTrait,
20 DetachedTraitImpl, Ensures, EnumDef, Expr, ExprKind, ExprPath, ExprPathSegment, FieldExpr,
21 FluxItem, FnInput, FnOutput, FnRetTy, FnSig, GenericArg, GenericArgKind, GenericBounds,
22 GenericParam, Generics, Ident, ImplAssocReft, Indices, LetDecl, LitKind, Mutability,
23 ParamMode, Path, PathSegment, PrimOpProp, Qualifier, QuantKind, RefineArg, RefineParam,
24 RefineParams, Requires, Sort, SortDecl, SortPath, SpecFunc, Spread, StructDef,
25 TraitAssocReft, TraitRef, Trusted, Ty, TyAlias, TyKind, UnOp, VariantDef, VariantRet,
26 WhereBoundPredicate,
27 },
28 symbols::{kw, sym},
29 token::{self, Comma, Delimiter::*, IdentIsRaw, Or, Token, TokenKind},
30};
31
32enum SyntaxAttr {
40 Reft,
42 Invariant(Expr),
44 RefinedBy(RefineParams),
46 Hide,
53 Opaque,
55}
56
57#[derive(Default)]
58struct ParsedAttrs {
59 normal: Vec<Attr>,
60 syntax: Vec<SyntaxAttr>,
61}
62
63impl ParsedAttrs {
64 fn is_reft(&self) -> bool {
65 self.syntax
66 .iter()
67 .any(|attr| matches!(attr, SyntaxAttr::Reft))
68 }
69
70 fn is_hide(&self) -> bool {
71 self.syntax
72 .iter()
73 .any(|attr| matches!(attr, SyntaxAttr::Hide))
74 }
75
76 fn is_opaque(&self) -> bool {
77 self.syntax
78 .iter()
79 .any(|attr| matches!(attr, SyntaxAttr::Opaque))
80 }
81
82 fn refined_by(&mut self) -> Option<RefineParams> {
83 let pos = self
84 .syntax
85 .iter()
86 .position(|x| matches!(x, SyntaxAttr::RefinedBy(_)))?;
87 if let SyntaxAttr::RefinedBy(params) = self.syntax.remove(pos) {
88 Some(params)
89 } else {
90 None
91 }
92 }
93
94 fn invariant(&mut self) -> Option<Expr> {
95 let pos = self
96 .syntax
97 .iter()
98 .position(|x| matches!(x, SyntaxAttr::Invariant(_)))?;
99 if let SyntaxAttr::Invariant(exp) = self.syntax.remove(pos) { Some(exp) } else { None }
100 }
101}
102
103pub(crate) fn parse_yes_or_no_with_reason(cx: &mut ParseCtxt) -> ParseResult<bool> {
109 let mut lookahead = cx.lookahead1();
110 if lookahead.advance_if(sym::yes) {
111 if cx.advance_if(token::Comma) {
112 parse_reason(cx)?;
113 }
114 Ok(true)
115 } else if lookahead.advance_if(sym::no) {
116 if cx.advance_if(token::Comma) {
117 parse_reason(cx)?;
118 }
119 Ok(false)
120 } else if lookahead.peek(sym::reason) {
121 parse_reason(cx)?;
122 Ok(true)
123 } else {
124 Err(lookahead.into_error())
125 }
126}
127
128fn parse_reason(cx: &mut ParseCtxt) -> ParseResult {
132 cx.expect(sym::reason)?;
133 cx.expect(token::Eq)?;
134 cx.expect(AnyLit)
135}
136
137pub(crate) fn parse_ident_list(cx: &mut ParseCtxt) -> ParseResult<Vec<Ident>> {
141 punctuated_until(cx, Comma, token::Eof, parse_ident)
142}
143
144pub(crate) fn parse_flux_items(cx: &mut ParseCtxt) -> ParseResult<Vec<FluxItem>> {
148 until(cx, token::Eof, parse_flux_item)
149}
150
151fn parse_flux_item(cx: &mut ParseCtxt) -> ParseResult<FluxItem> {
158 let mut lookahead = cx.lookahead1();
159 if lookahead.peek(token::Pound) || lookahead.peek(kw::Fn) {
160 parse_reft_func(cx).map(FluxItem::FuncDef)
161 } else if lookahead.peek(kw::Local) || lookahead.peek(kw::Qualifier) {
162 parse_qualifier(cx).map(FluxItem::Qualifier)
163 } else if lookahead.peek(kw::Opaque) {
164 parse_sort_decl(cx).map(FluxItem::SortDecl)
165 } else if lookahead.peek(kw::Property) {
166 parse_primop_property(cx).map(FluxItem::PrimOpProp)
167 } else {
168 Err(lookahead.into_error())
169 }
170}
171
172pub(crate) fn parse_detached_specs(cx: &mut ParseCtxt) -> ParseResult<surface::DetachedSpecs> {
176 let items = until(cx, token::Eof, parse_detached_item)?;
177 Ok(surface::DetachedSpecs { items })
178}
179
180pub(crate) fn parse_detached_item(cx: &mut ParseCtxt) -> ParseResult<DetachedItem> {
188 let attrs = parse_attrs(cx)?;
189 let mut lookahead = cx.lookahead1();
190 if lookahead.peek(kw::Fn) {
191 Ok(parse_detached_fn_sig(cx, attrs)?.map_kind(DetachedItemKind::FnSig))
192 } else if lookahead.peek(kw::Mod) {
193 parse_detached_mod(cx)
194 } else if lookahead.peek(kw::Struct) {
195 parse_detached_struct(cx, attrs)
196 } else if lookahead.peek(kw::Enum) {
197 parse_detached_enum(cx, attrs)
198 } else if lookahead.peek(kw::Impl) {
199 parse_detached_impl(cx, attrs)
200 } else if lookahead.peek(kw::Trait) {
201 parse_detached_trait(cx, attrs)
202 } else {
203 Err(lookahead.into_error())
204 }
205}
206
207fn parse_detached_field(cx: &mut ParseCtxt) -> ParseResult<(Ident, Ty)> {
211 let ident = parse_ident(cx)?;
212 cx.expect(token::Colon)?;
213 let ty = parse_type(cx)?;
214 Ok((ident, ty))
215}
216
217fn parse_detached_enum(cx: &mut ParseCtxt, mut attrs: ParsedAttrs) -> ParseResult<DetachedItem> {
221 cx.expect(kw::Enum)?;
222 let path = parse_expr_path(cx)?;
223 let generics = Some(parse_opt_generics(cx)?);
224 let refined_by = attrs.refined_by();
225 let invariants = attrs.invariant().into_iter().collect();
226 let variants = braces(cx, Comma, |cx| parse_variant(cx, true))?
227 .into_iter()
228 .map(Some)
229 .collect();
230 let enum_def = EnumDef { generics, refined_by, variants, invariants, reflected: false };
231 Ok(DetachedItem {
232 attrs: attrs.normal,
233 path,
234 kind: DetachedItemKind::Enum(enum_def),
235 node_id: cx.next_node_id(),
236 })
237}
238
239fn parse_detached_struct(cx: &mut ParseCtxt, mut attrs: ParsedAttrs) -> ParseResult<DetachedItem> {
240 cx.expect(kw::Struct)?;
241 let path = parse_expr_path(cx)?;
242 let generics = Some(parse_opt_generics(cx)?);
243 let refined_by = attrs.refined_by();
244 let opaque = attrs.is_opaque();
245 let invariants = attrs.invariant().into_iter().collect();
246 let fields = if cx.peek(token::OpenBrace) {
247 braces(cx, Comma, parse_detached_field)?
248 .into_iter()
249 .map(|(_, ty)| Some(ty))
250 .collect()
251 } else if cx.peek(token::OpenParen) {
252 parens(cx, Comma, parse_type)?
253 .into_iter()
254 .map(Some)
255 .collect()
256 } else {
257 cx.expect(token::Semi)?;
258 vec![]
259 };
260 let struct_def = StructDef { generics, opaque, refined_by, invariants, fields };
261 Ok(DetachedItem {
262 attrs: attrs.normal,
263 path,
264 kind: DetachedItemKind::Struct(struct_def),
265 node_id: cx.next_node_id(),
266 })
267}
268
269fn ident_path(cx: &mut ParseCtxt, ident: Ident) -> ExprPath {
270 let span = ident.span;
271 let segments = vec![ExprPathSegment { ident, node_id: cx.next_node_id() }];
272 ExprPath { segments, span, node_id: cx.next_node_id() }
273}
274
275fn parse_detached_fn_sig(
276 cx: &mut ParseCtxt,
277 attrs: ParsedAttrs,
278) -> ParseResult<DetachedItem<FnSig>> {
279 let fn_sig = parse_fn_sig(cx, token::Semi)?;
280 let span = fn_sig.span;
281 let ident = fn_sig
282 .ident
283 .ok_or(ParseError { kind: crate::ParseErrorKind::InvalidDetachedSpec, span })?;
284 let path = ident_path(cx, ident);
285 Ok(DetachedItem { attrs: attrs.normal, path, kind: fn_sig, node_id: cx.next_node_id() })
286}
287
288fn parse_detached_mod(cx: &mut ParseCtxt) -> ParseResult<DetachedItem> {
292 cx.expect(kw::Mod)?;
293 let path = parse_expr_path(cx)?;
294 cx.expect(TokenKind::open_delim(Brace))?;
295 let items = until(cx, TokenKind::close_delim(Brace), parse_detached_item)?;
296 cx.expect(TokenKind::close_delim(Brace))?;
297 Ok(DetachedItem {
298 attrs: vec![],
299 path,
300 kind: DetachedItemKind::Mod(DetachedSpecs { items }),
301 node_id: cx.next_node_id(),
302 })
303}
304
305fn parse_detached_trait(cx: &mut ParseCtxt, attrs: ParsedAttrs) -> ParseResult<DetachedItem> {
309 cx.expect(kw::Trait)?;
310 let path = parse_expr_path(cx)?;
311 let _generics = parse_opt_generics(cx)?;
312 cx.expect(TokenKind::open_delim(Brace))?;
313
314 let mut items = vec![];
315 let mut refts = vec![];
316 while !cx.peek(TokenKind::close_delim(Brace)) {
317 let assoc_item_attrs = parse_attrs(cx)?;
318 if assoc_item_attrs.is_reft() {
319 refts.push(parse_trait_assoc_reft(cx)?);
320 } else {
321 items.push(parse_detached_fn_sig(cx, assoc_item_attrs)?);
322 }
323 }
324 cx.expect(TokenKind::close_delim(Brace))?;
325 Ok(DetachedItem {
326 attrs: attrs.normal,
327 path,
328 kind: DetachedItemKind::Trait(DetachedTrait { items, refts }),
329 node_id: cx.next_node_id(),
330 })
331}
332
333fn parse_detached_impl(cx: &mut ParseCtxt, attrs: ParsedAttrs) -> ParseResult<DetachedItem> {
337 let lo = cx.lo();
338 cx.expect(kw::Impl)?;
339 let hi = cx.hi();
340 let span = cx.mk_span(lo, hi);
341 let outer_path = parse_expr_path(cx)?;
342 let _generics = parse_opt_generics(cx)?;
343 let inner_path = if cx.advance_if(kw::For) {
344 let path = parse_expr_path(cx)?;
345 let _generics = parse_opt_generics(cx)?;
346 Some(path)
347 } else {
348 None
349 };
350 cx.expect(TokenKind::open_delim(Brace))?;
351
352 let mut items = vec![];
353 let mut refts = vec![];
354 while !cx.peek(TokenKind::close_delim(Brace)) {
355 let assoc_item_attrs = parse_attrs(cx)?;
357 if assoc_item_attrs.is_reft() && inner_path.is_some() {
358 refts.push(parse_impl_assoc_reft(cx)?);
359 } else {
360 items.push(parse_detached_fn_sig(cx, assoc_item_attrs)?);
361 }
362 }
363 cx.expect(TokenKind::close_delim(Brace))?;
364 if let Some(path) = inner_path {
365 Ok(DetachedItem {
366 attrs: attrs.normal,
367 path,
368 kind: DetachedItemKind::TraitImpl(DetachedTraitImpl {
369 trait_: outer_path,
370 items,
371 refts,
372 span,
373 }),
374 node_id: cx.next_node_id(),
375 })
376 } else {
377 Ok(DetachedItem {
378 attrs: attrs.normal,
379 path: outer_path,
380 kind: DetachedItemKind::InherentImpl(DetachedInherentImpl { items, span }),
381 node_id: cx.next_node_id(),
382 })
383 }
384}
385
386fn parse_attr(cx: &mut ParseCtxt, attrs: &mut ParsedAttrs) -> ParseResult {
387 cx.expect(token::Pound)?;
388 cx.expect(token::OpenBracket)?;
389 let mut lookahead = cx.lookahead1();
390 if lookahead.advance_if(kw::Trusted) {
391 if cx.advance_if(token::OpenParen) {
392 parse_reason(cx)?;
393 cx.expect(token::CloseParen)?;
394 }
395 attrs.normal.push(Attr::Trusted(Trusted::Yes));
396 } else if lookahead.advance_if(sym::hide) {
397 attrs.syntax.push(SyntaxAttr::Hide);
398 } else if lookahead.advance_if(kw::Opaque) {
399 attrs.syntax.push(SyntaxAttr::Opaque);
400 } else if lookahead.advance_if(kw::Reft) {
401 attrs.syntax.push(SyntaxAttr::Reft);
402 } else if lookahead.advance_if(kw::RefinedBy) {
403 attrs
404 .syntax
405 .push(SyntaxAttr::RefinedBy(delimited(cx, Parenthesis, parse_refined_by)?));
406 } else if lookahead.advance_if(kw::Invariant) {
407 attrs
408 .syntax
409 .push(SyntaxAttr::Invariant(delimited(cx, Parenthesis, |cx| parse_expr(cx, true))?));
410 } else {
411 return Err(lookahead.into_error());
412 };
413 cx.expect(token::CloseBracket)
414}
415
416fn parse_attrs(cx: &mut ParseCtxt) -> ParseResult<ParsedAttrs> {
417 let mut attrs = ParsedAttrs::default();
418 repeat_while(cx, token::Pound, |cx| parse_attr(cx, &mut attrs))?;
419 Ok(attrs)
420}
421
422fn parse_reft_func(cx: &mut ParseCtxt) -> ParseResult<SpecFunc> {
430 let attrs = parse_attrs(cx)?;
431 let hide = attrs.is_hide();
432 cx.expect(kw::Fn)?;
433 let name = parse_ident(cx)?;
434 let sort_vars = opt_angle(cx, Comma, parse_ident)?;
435 let params = parens(cx, Comma, |cx| parse_refine_param(cx, RequireSort::Yes))?;
436 cx.expect(token::RArrow)?;
437 let output = parse_sort(cx)?;
438 let body = if cx.peek(token::OpenBrace) {
439 Some(parse_block(cx)?)
440 } else {
441 cx.expect(token::Semi)?;
442 None
443 };
444 Ok(SpecFunc { name, sort_vars, params, output, body, hide })
445}
446
447fn parse_qualifier(cx: &mut ParseCtxt) -> ParseResult<Qualifier> {
453 let lo = cx.lo();
454 let local = cx.advance_if(kw::Local);
455 cx.expect(kw::Qualifier)?;
456 let name = parse_ident(cx)?;
457 let params = parens(cx, Comma, |cx| parse_refine_param(cx, RequireSort::Yes))?;
458 let expr = parse_block(cx)?;
459 let hi = cx.hi();
460 Ok(Qualifier { global: !local, name, params, expr, span: cx.mk_span(lo, hi) })
461}
462
463fn parse_sort_decl(cx: &mut ParseCtxt) -> ParseResult<SortDecl> {
467 cx.expect(kw::Opaque)?;
468 cx.expect(kw::Sort)?;
469 let name = parse_ident(cx)?;
470 let sort_vars = opt_angle(cx, Comma, parse_ident)?;
471 cx.expect(token::Semi)?;
472 Ok(SortDecl { name, sort_vars })
473}
474
475fn parse_binop(cx: &mut ParseCtxt) -> ParseResult<BinOp> {
477 let (op, ntokens) = cx
478 .peek_binop()
479 .ok_or_else(|| cx.unexpected_token(vec![Expected::Str("binary operator")]))?;
480 cx.advance_by(ntokens);
481 Ok(op)
482}
483
484fn parse_primop_property(cx: &mut ParseCtxt) -> ParseResult<PrimOpProp> {
488 let lo = cx.lo();
489 cx.expect(kw::Property)?;
490
491 let name = parse_ident(cx)?;
493
494 cx.expect(token::OpenBracket)?;
496 let op = parse_binop(cx)?;
497 cx.expect(token::CloseBracket)?;
498
499 let params = parens(cx, Comma, |cx| parse_refine_param(cx, RequireSort::No))?;
501
502 let body = parse_block(cx)?;
503 let hi = cx.hi();
504
505 Ok(PrimOpProp { name, op, params, body, span: cx.mk_span(lo, hi) })
506}
507
508pub(crate) fn parse_trait_assoc_refts(cx: &mut ParseCtxt) -> ParseResult<Vec<TraitAssocReft>> {
509 until(cx, token::Eof, parse_trait_assoc_reft)
510}
511
512fn parse_trait_assoc_reft(cx: &mut ParseCtxt) -> ParseResult<TraitAssocReft> {
518 let lo = cx.lo();
519 let final_ = cx.advance_if(kw::Final);
520 cx.expect(kw::Fn)?;
521 let name = parse_ident(cx)?;
522 let params = parens(cx, Comma, |cx| parse_refine_param(cx, RequireSort::Yes))?;
523 cx.expect(token::RArrow)?;
524 let output = parse_base_sort(cx)?;
525 let body = if cx.peek(token::OpenBrace) {
526 Some(parse_block(cx)?)
527 } else {
528 cx.advance_if(token::Semi);
529 None
530 };
531 let hi = cx.hi();
532 Ok(TraitAssocReft { name, params, output, body, span: cx.mk_span(lo, hi), final_ })
533}
534
535pub(crate) fn parse_impl_assoc_refts(cx: &mut ParseCtxt) -> ParseResult<Vec<ImplAssocReft>> {
536 until(cx, token::Eof, parse_impl_assoc_reft)
537}
538
539fn parse_impl_assoc_reft(cx: &mut ParseCtxt) -> ParseResult<ImplAssocReft> {
543 let lo = cx.lo();
544 cx.expect(kw::Fn)?;
545 let name = parse_ident(cx)?;
546 let params = parens(cx, Comma, |cx| parse_refine_param(cx, RequireSort::Yes))?;
547 cx.expect(token::RArrow)?;
548 let output = parse_base_sort(cx)?;
549 let body = parse_block(cx)?;
550 let hi = cx.hi();
551 Ok(ImplAssocReft { name, params, output, body, span: cx.mk_span(lo, hi) })
552}
553
554pub(crate) fn parse_refined_by(cx: &mut ParseCtxt) -> ParseResult<RefineParams> {
558 punctuated_until(cx, Comma, token::Eof, |cx| parse_refine_param(cx, RequireSort::Yes))
559}
560
561pub(crate) fn parse_variant(cx: &mut ParseCtxt, ret_arrow: bool) -> ParseResult<VariantDef> {
567 let lo = cx.lo();
568 let mut fields = vec![];
569 let mut ret = None;
570 let ident = if ret_arrow || cx.peek2(NonReserved, token::OpenParen) {
571 Some(parse_ident(cx)?)
572 } else {
573 None
574 };
575 if cx.peek(token::OpenParen) || cx.peek(token::OpenBrace) {
576 fields = parse_fields(cx)?;
577 if cx.advance_if(token::RArrow) {
578 ret = Some(parse_variant_ret(cx)?);
579 }
580 } else {
581 if ret_arrow {
582 cx.expect(token::RArrow)?;
583 }
584 ret = Some(parse_variant_ret(cx)?);
585 };
586 let hi = cx.hi();
587 Ok(VariantDef { ident, fields, ret, node_id: cx.next_node_id(), span: cx.mk_span(lo, hi) })
588}
589
590fn parse_fields(cx: &mut ParseCtxt) -> ParseResult<Vec<Ty>> {
594 let mut lookahead = cx.lookahead1();
595 if lookahead.peek(token::OpenParen) {
596 parens(cx, Comma, parse_type)
597 } else if lookahead.peek(token::OpenBrace) {
598 braces(cx, Comma, parse_type)
599 } else {
600 Err(lookahead.into_error())
601 }
602}
603
604fn parse_variant_ret(cx: &mut ParseCtxt) -> ParseResult<VariantRet> {
608 let path = parse_path(cx)?;
609 let indices = if cx.peek(token::OpenBracket) {
610 parse_indices(cx)?
611 } else {
612 let hi = cx.hi();
613 Indices { indices: vec![], span: cx.mk_span(hi, hi) }
614 };
615 Ok(VariantRet { path, indices })
616}
617
618pub(crate) fn parse_type_alias(cx: &mut ParseCtxt) -> ParseResult<TyAlias> {
619 let lo = cx.lo();
620 cx.expect(kw::Type)?;
621 let ident = parse_ident(cx)?;
622 let generics = parse_opt_generics(cx)?;
623 let params = if cx.peek(token::OpenParen) {
624 parens(cx, Comma, |cx| parse_refine_param(cx, RequireSort::Yes))?
625 } else {
626 vec![]
627 };
628 let index = if cx.peek(token::OpenBracket) {
629 Some(delimited(cx, Bracket, |cx| parse_refine_param(cx, RequireSort::Yes))?)
630 } else {
631 None
632 };
633 cx.expect(token::Eq)?;
634 let ty = parse_type(cx)?;
635 let hi = cx.hi();
636 Ok(TyAlias {
637 ident,
638 generics,
639 params,
640 index,
641 ty,
642 node_id: cx.next_node_id(),
643 span: cx.mk_span(lo, hi),
644 })
645}
646
647fn parse_opt_generics(cx: &mut ParseCtxt) -> ParseResult<Generics> {
648 if !cx.peek(LAngle) {
649 let hi = cx.hi();
650 return Ok(Generics { params: vec![], predicates: None, span: cx.mk_span(hi, hi) });
651 }
652 let lo = cx.lo();
653 let params = angle(cx, Comma, parse_generic_param)?;
654 let hi = cx.hi();
655 Ok(Generics { params, predicates: None, span: cx.mk_span(lo, hi) })
656}
657
658fn parse_generic_param(cx: &mut ParseCtxt) -> ParseResult<GenericParam> {
659 let name = parse_ident(cx)?;
660 Ok(GenericParam { name, node_id: cx.next_node_id() })
661}
662
663fn invalid_ident_err(ident: &Ident) -> ParseError {
664 ParseError { kind: crate::ParseErrorKind::InvalidBinding, span: ident.span }
665}
666
667fn mut_as_strg(inputs: Vec<FnInput>, ensures: &[Ensures]) -> ParseResult<Vec<FnInput>> {
668 let locs = ensures
670 .iter()
671 .filter_map(|ens| if let Ensures::Type(ident, _, _) = ens { Some(ident) } else { None })
672 .collect::<HashSet<_>>();
673 let mut res = vec![];
675 for input in inputs {
676 if let FnInput::Ty(Some(ident), _, _) = &input
677 && locs.contains(&ident)
678 {
679 let FnInput::Ty(Some(ident), ty, id) = input else {
681 return Err(invalid_ident_err(ident));
682 };
683 let TyKind::Ref(Mutability::Mut, inner_ty) = ty.kind else {
684 return Err(invalid_ident_err(&ident));
685 };
686 res.push(FnInput::StrgRef(ident, *inner_ty, id));
687 } else {
688 res.push(input);
690 }
691 }
692 Ok(res)
693}
694
695pub(crate) fn parse_fn_sig<T: PeekExpected>(cx: &mut ParseCtxt, end: T) -> ParseResult<FnSig> {
703 let lo = cx.lo();
704 let asyncness = parse_asyncness(cx);
705 cx.expect(kw::Fn)?;
706 let ident = if cx.peek(NonReserved) { Some(parse_ident(cx)?) } else { None };
707 let mut generics = parse_opt_generics(cx)?;
708 let params = if cx.peek(token::OpenBracket) {
709 brackets(cx, Comma, |cx| parse_refine_param(cx, RequireSort::Maybe))?
710 } else {
711 vec![]
712 };
713 let inputs = parens(cx, Comma, parse_fn_input)?;
714 let returns = parse_fn_ret(cx)?;
715 let requires = parse_opt_requires(cx)?;
716 let ensures = parse_opt_ensures(cx)?;
717 let inputs = mut_as_strg(inputs, &ensures)?;
718 generics.predicates = parse_opt_where(cx)?;
719 cx.expect(end)?;
720 let hi = cx.hi();
721 Ok(FnSig {
722 asyncness,
723 generics,
724 params,
725 ident,
726 inputs,
727 requires,
728 output: FnOutput { returns, ensures, node_id: cx.next_node_id() },
729 node_id: cx.next_node_id(),
730 span: cx.mk_span(lo, hi),
731 })
732}
733
734fn parse_opt_requires(cx: &mut ParseCtxt) -> ParseResult<Vec<Requires>> {
738 if !cx.advance_if(kw::Requires) {
739 return Ok(vec![]);
740 }
741 punctuated_until(
742 cx,
743 Comma,
744 |t: TokenKind| t.is_keyword(kw::Ensures) || t.is_keyword(kw::Where) || t.is_eof(),
745 parse_requires_clause,
746 )
747}
748
749fn parse_requires_clause(cx: &mut ParseCtxt) -> ParseResult<Requires> {
753 let mut params = vec![];
754 if cx.advance_if(kw::Forall) {
755 params = sep1(cx, Comma, |cx| parse_refine_param(cx, RequireSort::Maybe))?;
756 cx.expect(token::Dot)?;
757 }
758 let pred = parse_expr(cx, true)?;
759 Ok(Requires { params, pred })
760}
761
762fn parse_opt_ensures(cx: &mut ParseCtxt) -> ParseResult<Vec<Ensures>> {
766 if !cx.advance_if(kw::Ensures) {
767 return Ok(vec![]);
768 }
769 punctuated_until(
770 cx,
771 Comma,
772 |t: TokenKind| t.is_keyword(kw::Where) || t.is_eof(),
773 parse_ensures_clause,
774 )
775}
776
777fn parse_ensures_clause(cx: &mut ParseCtxt) -> ParseResult<Ensures> {
782 if cx.peek2(NonReserved, token::Colon) {
783 let ident = parse_ident(cx)?;
785 cx.expect(token::Colon)?;
786 let ty = parse_type(cx)?;
787 Ok(Ensures::Type(ident, ty, cx.next_node_id()))
788 } else {
789 Ok(Ensures::Pred(parse_expr(cx, true)?))
791 }
792}
793
794fn parse_opt_where(cx: &mut ParseCtxt) -> ParseResult<Option<Vec<WhereBoundPredicate>>> {
795 if !cx.advance_if(kw::Where) {
796 return Ok(None);
797 }
798 Ok(Some(punctuated_until(cx, Comma, token::Eof, parse_where_bound)?))
799}
800
801fn parse_where_bound(cx: &mut ParseCtxt) -> ParseResult<WhereBoundPredicate> {
802 let lo = cx.lo();
803 let bounded_ty = parse_type(cx)?;
804 cx.expect(token::Colon)?;
805 let bounds = parse_generic_bounds(cx)?;
806 let hi = cx.hi();
807 Ok(WhereBoundPredicate { span: cx.mk_span(lo, hi), bounded_ty, bounds })
808}
809
810fn parse_fn_ret(cx: &mut ParseCtxt) -> ParseResult<FnRetTy> {
814 if cx.advance_if(token::RArrow) {
815 Ok(FnRetTy::Ty(Box::new(parse_type(cx)?)))
816 } else {
817 let hi = cx.hi();
818 Ok(FnRetTy::Default(cx.mk_span(hi, hi)))
819 }
820}
821
822fn parse_fn_input(cx: &mut ParseCtxt) -> ParseResult<FnInput> {
829 if cx.peek2(NonReserved, token::Colon) {
830 let bind = parse_ident(cx)?;
831 cx.expect(token::Colon)?;
832 if cx.advance_if2(token::And, kw::Strg) {
833 Ok(FnInput::StrgRef(bind, parse_type(cx)?, cx.next_node_id()))
835 } else if cx.peek(NonReserved) {
836 let path = parse_path(cx)?;
837 if cx.peek3(token::OpenBrace, NonReserved, token::Colon) {
838 let bty = path_to_bty(path);
840 let ty = parse_bty_exists(cx, bty)?;
841 Ok(FnInput::Ty(Some(bind), ty, cx.next_node_id()))
842 } else if cx.peek(token::OpenBrace) {
843 let pred = delimited(cx, Brace, |cx| parse_expr(cx, true))?;
845 Ok(FnInput::Constr(bind, path, pred, cx.next_node_id()))
846 } else {
847 let bty = path_to_bty(path);
849 let ty = parse_bty_rhs(cx, bty)?;
850 Ok(FnInput::Ty(Some(bind), ty, cx.next_node_id()))
851 }
852 } else {
853 Ok(FnInput::Ty(Some(bind), parse_type(cx)?, cx.next_node_id()))
855 }
856 } else {
857 Ok(FnInput::Ty(None, parse_type(cx)?, cx.next_node_id()))
859 }
860}
861
862fn parse_asyncness(cx: &mut ParseCtxt) -> Async {
866 let lo = cx.lo();
867 if cx.advance_if(kw::Async) {
868 Async::Yes { node_id: cx.next_node_id(), span: cx.mk_span(lo, cx.hi()) }
869 } else {
870 Async::No
871 }
872}
873
874pub(crate) fn parse_type(cx: &mut ParseCtxt) -> ParseResult<Ty> {
890 let lo = cx.lo();
891 let mut lookahead = cx.lookahead1();
892 let kind = if lookahead.advance_if(kw::Underscore) {
893 TyKind::Hole
894 } else if lookahead.advance_if(token::OpenParen) {
895 let (mut tys, trailing) =
897 punctuated_with_trailing(cx, Comma, token::CloseParen, parse_type)?;
898 cx.expect(token::CloseParen)?;
899 if tys.len() == 1 && !trailing {
900 return Ok(tys.remove(0));
901 } else {
902 TyKind::Tuple(tys)
903 }
904 } else if lookahead.peek(token::OpenBrace) {
905 delimited(cx, Brace, |cx| {
906 if cx.peek2(NonReserved, AnyOf([token::Comma, token::Dot, token::Colon])) {
907 parse_general_exists(cx)
909 } else {
910 let ty = parse_type(cx)?;
912 cx.expect(token::Or)?;
913 let pred = parse_block_expr(cx)?;
914 Ok(TyKind::Constr(pred, Box::new(ty)))
915 }
916 })?
917 } else if lookahead.advance_if(token::And) {
918 let mutbl = if cx.advance_if(kw::Mut) { Mutability::Mut } else { Mutability::Not };
920 TyKind::Ref(mutbl, Box::new(parse_type(cx)?))
921 } else if lookahead.advance_if(token::OpenBracket) {
922 let ty = parse_type(cx)?;
923 if cx.advance_if(token::Semi) {
924 let len = parse_const_arg(cx)?;
926 cx.expect(token::CloseBracket)?;
927 TyKind::Array(Box::new(ty), len)
928 } else {
929 cx.expect(token::CloseBracket)?;
931 let span = cx.mk_span(lo, cx.hi());
932 let kind = BaseTyKind::Slice(Box::new(ty));
933 return parse_bty_rhs(cx, BaseTy { kind, span });
934 }
935 } else if lookahead.advance_if(kw::Impl) {
936 TyKind::ImplTrait(cx.next_node_id(), parse_generic_bounds(cx)?)
938 } else if lookahead.peek(NonReserved) {
939 let path = parse_path(cx)?;
941 let bty = path_to_bty(path);
942 return parse_bty_rhs(cx, bty);
943 } else if lookahead.peek(LAngle) {
944 let bty = parse_qpath(cx)?;
946 return parse_bty_rhs(cx, bty);
947 } else {
948 return Err(lookahead.into_error());
949 };
950 let hi = cx.hi();
951 Ok(Ty { kind, node_id: cx.next_node_id(), span: cx.mk_span(lo, hi) })
952}
953
954fn parse_qpath(cx: &mut ParseCtxt) -> ParseResult<BaseTy> {
958 let lo = cx.lo();
959 cx.expect(LAngle)?;
960 let qself = parse_type(cx)?;
961 cx.expect(kw::As)?;
962 let mut segments = parse_segments(cx)?;
963 cx.expect(RAngle)?;
964 cx.expect(token::PathSep)?;
965 segments.extend(parse_segments(cx)?);
966 let hi = cx.hi();
967
968 let span = cx.mk_span(lo, hi);
969 let path = Path { segments, refine: vec![], node_id: cx.next_node_id(), span };
970 let kind = BaseTyKind::Path(Some(Box::new(qself)), path);
971 Ok(BaseTy { kind, span })
972}
973
974fn parse_general_exists(cx: &mut ParseCtxt) -> ParseResult<TyKind> {
978 let params = sep1(cx, Comma, |cx| parse_refine_param(cx, RequireSort::Maybe))?;
979 cx.expect(token::Dot)?;
980 let ty = parse_type(cx)?;
981 let pred = if cx.advance_if(token::Or) { Some(parse_block_expr(cx)?) } else { None };
982 Ok(TyKind::GeneralExists { params, ty: Box::new(ty), pred })
983}
984
985fn parse_bty_rhs(cx: &mut ParseCtxt, bty: BaseTy) -> ParseResult<Ty> {
991 let lo = bty.span.lo();
992 if cx.peek(token::OpenBracket) {
993 let indices = parse_indices(cx)?;
995 let hi = cx.hi();
996 let kind = TyKind::Indexed { bty, indices };
997 Ok(Ty { kind, node_id: cx.next_node_id(), span: cx.mk_span(lo, hi) })
998 } else if cx.peek(token::OpenBrace) {
999 parse_bty_exists(cx, bty)
1001 } else {
1002 let hi = cx.hi();
1004 let kind = TyKind::Base(bty);
1005 Ok(Ty { kind, node_id: cx.next_node_id(), span: cx.mk_span(lo, hi) })
1006 }
1007}
1008
1009fn parse_bty_exists(cx: &mut ParseCtxt, bty: BaseTy) -> ParseResult<Ty> {
1013 let lo = bty.span.lo();
1014 delimited(cx, Brace, |cx| {
1015 let bind = parse_ident(cx)?;
1016 cx.expect(token::Colon)?;
1017 let pred = parse_block_expr(cx)?;
1018 let hi = cx.hi();
1019 let kind = TyKind::Exists { bind, bty, pred };
1020 Ok(Ty { kind, node_id: cx.next_node_id(), span: cx.mk_span(lo, hi) })
1021 })
1022}
1023
1024fn path_to_bty(path: Path) -> BaseTy {
1025 let span = path.span;
1026 BaseTy { kind: BaseTyKind::Path(None, path), span }
1027}
1028
1029fn parse_indices(cx: &mut ParseCtxt) -> ParseResult<Indices> {
1030 let lo = cx.lo();
1031 let indices = brackets(cx, Comma, parse_refine_arg)?;
1032 let hi = cx.hi();
1033 Ok(Indices { indices, span: cx.mk_span(lo, hi) })
1034}
1035
1036fn parse_fn_bound_input(cx: &mut ParseCtxt) -> ParseResult<GenericArg> {
1037 let lo = cx.lo();
1038 let tys = parens(cx, Comma, parse_type)?;
1039 let hi = cx.hi();
1040 let kind = TyKind::Tuple(tys);
1041 let span = cx.mk_span(lo, hi);
1042 let in_ty = Ty { kind, node_id: cx.next_node_id(), span };
1043 Ok(GenericArg { kind: GenericArgKind::Type(in_ty), node_id: cx.next_node_id() })
1044}
1045
1046fn parse_fn_bound_output(cx: &mut ParseCtxt) -> ParseResult<GenericArg> {
1047 let lo = cx.lo();
1048
1049 let ty = if cx.advance_if(token::RArrow) {
1050 parse_type(cx)?
1051 } else {
1052 Ty { kind: TyKind::Tuple(vec![]), node_id: cx.next_node_id(), span: cx.mk_span(lo, lo) }
1053 };
1054 let hi = cx.hi();
1055 let ident = Ident { name: Output, span: cx.mk_span(lo, hi) };
1056 Ok(GenericArg { kind: GenericArgKind::Constraint(ident, ty), node_id: cx.next_node_id() })
1057}
1058
1059fn parse_fn_bound_path(cx: &mut ParseCtxt) -> ParseResult<Path> {
1060 let lo = cx.lo();
1061 let ident = parse_ident(cx)?;
1062 let in_arg = parse_fn_bound_input(cx)?;
1063 let out_arg = parse_fn_bound_output(cx)?;
1064 let args = vec![in_arg, out_arg];
1065 let segment = PathSegment { ident, args, node_id: cx.next_node_id() };
1066 let hi = cx.hi();
1067 Ok(Path {
1068 segments: vec![segment],
1069 refine: vec![],
1070 node_id: cx.next_node_id(),
1071 span: cx.mk_span(lo, hi),
1072 })
1073}
1074
1075fn parse_generic_bounds(cx: &mut ParseCtxt) -> ParseResult<GenericBounds> {
1076 let path = if cx.peek(sym::FnOnce) || cx.peek(sym::FnMut) || cx.peek(sym::Fn) {
1077 parse_fn_bound_path(cx)?
1078 } else {
1079 parse_path(cx)?
1080 };
1081 Ok(vec![TraitRef { path, node_id: cx.next_node_id() }])
1082}
1083
1084fn parse_const_arg(cx: &mut ParseCtxt) -> ParseResult<ConstArg> {
1085 let lo = cx.lo();
1086 let mut lookahead = cx.lookahead1();
1087 let kind = if lookahead.peek(AnyLit) {
1088 let len = parse_int(cx)?;
1089 ConstArgKind::Lit(len)
1090 } else if lookahead.advance_if(kw::Underscore) {
1091 ConstArgKind::Infer
1092 } else {
1093 return Err(lookahead.into_error());
1094 };
1095 let hi = cx.hi();
1096 Ok(ConstArg { kind, span: cx.mk_span(lo, hi) })
1097}
1098
1099fn parse_path(cx: &mut ParseCtxt) -> ParseResult<Path> {
1103 let lo = cx.lo();
1104 let segments = parse_segments(cx)?;
1105 let refine =
1106 if cx.peek(token::OpenParen) { parens(cx, Comma, parse_refine_arg)? } else { vec![] };
1107 let hi = cx.hi();
1108 Ok(Path { segments, refine, node_id: cx.next_node_id(), span: cx.mk_span(lo, hi) })
1109}
1110
1111fn parse_segments(cx: &mut ParseCtxt) -> ParseResult<Vec<PathSegment>> {
1115 sep1(cx, token::PathSep, parse_segment)
1116}
1117
1118fn parse_segment(cx: &mut ParseCtxt) -> ParseResult<PathSegment> {
1122 let ident = parse_ident(cx)?;
1123 let args = opt_angle(cx, Comma, parse_generic_arg)?;
1124 Ok(PathSegment { ident, node_id: cx.next_node_id(), args })
1125}
1126
1127fn parse_generic_arg(cx: &mut ParseCtxt) -> ParseResult<GenericArg> {
1131 let kind = if cx.peek2(NonReserved, token::Eq) {
1132 let ident = parse_ident(cx)?;
1133 cx.expect(token::Eq)?;
1134 let ty = parse_type(cx)?;
1135 GenericArgKind::Constraint(ident, ty)
1136 } else {
1137 GenericArgKind::Type(parse_type(cx)?)
1138 };
1139 Ok(GenericArg { kind, node_id: cx.next_node_id() })
1140}
1141
1142fn parse_refine_arg(cx: &mut ParseCtxt) -> ParseResult<RefineArg> {
1149 let lo = cx.lo();
1150 let arg = if cx.advance_if(token::At) {
1151 let bind = parse_ident(cx)?;
1153 let hi = cx.hi();
1154 RefineArg::Bind(bind, BindKind::At, cx.mk_span(lo, hi), cx.next_node_id())
1155 } else if cx.advance_if(token::Pound) {
1156 let bind = parse_ident(cx)?;
1158 let hi = cx.hi();
1159 RefineArg::Bind(bind, BindKind::Pound, cx.mk_span(lo, hi), cx.next_node_id())
1160 } else if cx.advance_if(Or) {
1161 let params =
1162 punctuated_until(cx, Comma, Or, |cx| parse_refine_param(cx, RequireSort::Maybe))?;
1163 cx.expect(Or)?;
1164 let body = parse_expr(cx, true)?;
1165 let hi = cx.hi();
1166 RefineArg::Abs(params, body, cx.mk_span(lo, hi), cx.next_node_id())
1167 } else {
1168 RefineArg::Expr(parse_expr(cx, true)?)
1170 };
1171 Ok(arg)
1172}
1173
1174enum RequireSort {
1176 Yes,
1178 Maybe,
1180 No,
1182}
1183
1184fn parse_sort_if_required(cx: &mut ParseCtxt, require_sort: RequireSort) -> ParseResult<Sort> {
1185 match require_sort {
1186 RequireSort::No => Ok(Sort::Infer),
1187 RequireSort::Maybe => {
1188 if cx.advance_if(token::Colon) {
1189 parse_sort(cx)
1190 } else {
1191 Ok(Sort::Infer)
1192 }
1193 }
1194 RequireSort::Yes => {
1195 cx.expect(token::Colon)?;
1196 parse_sort(cx)
1197 }
1198 }
1199}
1200
1201fn parse_refine_param(cx: &mut ParseCtxt, require_sort: RequireSort) -> ParseResult<RefineParam> {
1207 let lo = cx.lo();
1208 let mode = parse_opt_param_mode(cx);
1209 let ident = parse_ident(cx)?;
1210 let sort = parse_sort_if_required(cx, require_sort)?;
1211 let hi = cx.hi();
1212 Ok(RefineParam { mode, ident, sort, span: cx.mk_span(lo, hi), node_id: cx.next_node_id() })
1213}
1214
1215fn parse_opt_param_mode(cx: &mut ParseCtxt) -> Option<ParamMode> {
1219 if cx.advance_if(kw::Hrn) {
1220 Some(ParamMode::Horn)
1221 } else if cx.advance_if(kw::Hdl) {
1222 Some(ParamMode::Hindley)
1223 } else {
1224 None
1225 }
1226}
1227
1228pub(crate) fn parse_expr(cx: &mut ParseCtxt, allow_struct: bool) -> ParseResult<Expr> {
1229 parse_binops(cx, Precedence::MIN, allow_struct)
1230}
1231
1232fn parse_binops(cx: &mut ParseCtxt, base: Precedence, allow_struct: bool) -> ParseResult<Expr> {
1233 let mut lhs = unary_expr(cx, allow_struct)?;
1234 loop {
1235 let lo = cx.lo();
1236 let Some((op, ntokens)) = cx.peek_binop() else { break };
1237 let precedence = Precedence::of_binop(&op);
1238 if precedence < base {
1239 break;
1240 }
1241 cx.advance_by(ntokens);
1242 let next = match precedence.associativity() {
1243 Associativity::Right => precedence,
1244 Associativity::Left => precedence.next(),
1245 Associativity::None => {
1246 if let ExprKind::BinaryOp(op, ..) = &lhs.kind
1247 && Precedence::of_binop(op) == precedence
1248 {
1249 return Err(cx.cannot_be_chained(lo, cx.hi()));
1250 }
1251 precedence.next()
1252 }
1253 };
1254 let rhs = parse_binops(cx, next, allow_struct)?;
1255 let span = lhs.span.to(rhs.span);
1256 lhs = Expr {
1257 kind: ExprKind::BinaryOp(op, Box::new([lhs, rhs])),
1258 node_id: cx.next_node_id(),
1259 span,
1260 }
1261 }
1262 Ok(lhs)
1263}
1264
1265fn unary_expr(cx: &mut ParseCtxt, allow_struct: bool) -> ParseResult<Expr> {
1269 let lo = cx.lo();
1270 let kind = if cx.advance_if(token::Minus) {
1271 ExprKind::UnaryOp(UnOp::Neg, Box::new(unary_expr(cx, allow_struct)?))
1272 } else if cx.advance_if(token::Bang) {
1273 ExprKind::UnaryOp(UnOp::Not, Box::new(unary_expr(cx, allow_struct)?))
1274 } else {
1275 return parse_trailer_expr(cx, allow_struct);
1276 };
1277 let hi = cx.hi();
1278 Ok(Expr { kind, node_id: cx.next_node_id(), span: cx.mk_span(lo, hi) })
1279}
1280
1281fn parse_trailer_expr(cx: &mut ParseCtxt, allow_struct: bool) -> ParseResult<Expr> {
1287 let lo = cx.lo();
1288 let mut e = parse_atom(cx, allow_struct)?;
1289 loop {
1290 let kind = if cx.advance_if(token::Dot) {
1291 let field = parse_ident(cx)?;
1293 ExprKind::Dot(Box::new(e), field)
1294 } else if cx.peek(token::OpenParen) {
1295 let args = parens(cx, Comma, |cx| parse_expr(cx, true))?;
1297 ExprKind::Call(Box::new(e), args)
1298 } else {
1299 break;
1300 };
1301 let hi = cx.hi();
1302 e = Expr { kind, node_id: cx.next_node_id(), span: cx.mk_span(lo, hi) };
1303 }
1304 Ok(e)
1305}
1306
1307fn parse_atom(cx: &mut ParseCtxt, allow_struct: bool) -> ParseResult<Expr> {
1319 let lo = cx.lo();
1320 let mut lookahead = cx.lookahead1();
1321 if lookahead.peek(kw::If) {
1322 parse_if_expr(cx)
1324 } else if lookahead.peek(AnyLit) {
1325 parse_lit(cx)
1327 } else if lookahead.peek(token::OpenParen) {
1328 delimited(cx, Parenthesis, |cx| parse_expr(cx, true))
1329 } else if lookahead.peek(NonReserved) {
1330 let path = parse_expr_path(cx)?;
1331 let kind = if allow_struct && cx.peek(token::OpenBrace) {
1332 let args = braces(cx, Comma, parse_constructor_arg)?;
1334 ExprKind::Constructor(Some(path), args)
1335 } else {
1336 ExprKind::Path(path)
1338 };
1339 let hi = cx.hi();
1340 Ok(Expr { kind, node_id: cx.next_node_id(), span: cx.mk_span(lo, hi) })
1341 } else if allow_struct && lookahead.peek(token::OpenBrace) {
1342 let args = braces(cx, Comma, parse_constructor_arg)?;
1344 let hi = cx.hi();
1345 Ok(Expr {
1346 kind: ExprKind::Constructor(None, args),
1347 node_id: cx.next_node_id(),
1348 span: cx.mk_span(lo, hi),
1349 })
1350 } else if lookahead.advance_if(LAngle) {
1351 let lo = cx.lo();
1353 let qself = parse_type(cx)?;
1354 cx.expect(kw::As)?;
1355 let path = parse_path(cx)?;
1356 cx.expect(RAngle)?;
1357 cx.expect(token::PathSep)?;
1358 let name = parse_ident(cx)?;
1359 let hi = cx.hi();
1360 let kind = ExprKind::AssocReft(Box::new(qself), path, name);
1361 Ok(Expr { kind, node_id: cx.next_node_id(), span: cx.mk_span(lo, hi) })
1362 } else if lookahead.peek(token::OpenBracket) {
1363 parse_prim_uif(cx)
1364 } else if lookahead.peek(kw::Exists) || lookahead.peek(kw::Forall) {
1365 parse_bounded_quantifier(cx)
1366 } else {
1367 Err(lookahead.into_error())
1368 }
1369}
1370
1371fn parse_prim_uif(cx: &mut ParseCtxt) -> ParseResult<Expr> {
1372 let lo = cx.lo();
1373 cx.expect(token::OpenBracket)?;
1374 let op = parse_binop(cx)?;
1375 cx.expect(token::CloseBracket)?;
1376 let hi = cx.hi();
1377 Ok(Expr { kind: ExprKind::PrimUIF(op), node_id: cx.next_node_id(), span: cx.mk_span(lo, hi) })
1378}
1379
1380fn parse_bounded_quantifier(cx: &mut ParseCtxt) -> ParseResult<Expr> {
1385 let lo = cx.lo();
1386 let mut lookahead = cx.lookahead1();
1387 let quant = if lookahead.advance_if(kw::Forall) {
1388 QuantKind::Forall
1389 } else if lookahead.advance_if(kw::Exists) {
1390 QuantKind::Exists
1391 } else {
1392 return Err(lookahead.into_error());
1393 };
1394 let param = parse_refine_param(cx, RequireSort::Maybe)?;
1395 cx.expect(kw::In)?;
1396 let start = parse_int(cx)?;
1397 cx.expect(token::DotDot)?;
1398 let end = parse_int(cx)?;
1399 let body = parse_block(cx)?;
1400 let hi = cx.hi();
1401 Ok(Expr {
1402 kind: ExprKind::BoundedQuant(quant, param, start..end, Box::new(body)),
1403 node_id: cx.next_node_id(),
1404 span: cx.mk_span(lo, hi),
1405 })
1406}
1407
1408fn parse_constructor_arg(cx: &mut ParseCtxt) -> ParseResult<ConstructorArg> {
1412 let lo = cx.lo();
1413 let mut lookahead = cx.lookahead1();
1414 if lookahead.peek(NonReserved) {
1415 let ident = parse_ident(cx)?;
1416 cx.expect(token::Colon)?;
1417 let expr = parse_expr(cx, true)?;
1418 let hi = cx.hi();
1419 Ok(ConstructorArg::FieldExpr(FieldExpr {
1420 ident,
1421 expr,
1422 node_id: cx.next_node_id(),
1423 span: cx.mk_span(lo, hi),
1424 }))
1425 } else if lookahead.advance_if(token::DotDot) {
1426 let spread = parse_expr(cx, true)?;
1427 let hi = cx.hi();
1428 Ok(ConstructorArg::Spread(Spread {
1429 expr: spread,
1430 node_id: cx.next_node_id(),
1431 span: cx.mk_span(lo, hi),
1432 }))
1433 } else {
1434 Err(lookahead.into_error())
1435 }
1436}
1437
1438fn parse_expr_path(cx: &mut ParseCtxt) -> ParseResult<ExprPath> {
1440 let lo = cx.lo();
1441 let segments = sep1(cx, token::PathSep, parse_expr_path_segment)?;
1442 let hi = cx.hi();
1443 Ok(ExprPath { segments, node_id: cx.next_node_id(), span: cx.mk_span(lo, hi) })
1444}
1445
1446fn parse_expr_path_segment(cx: &mut ParseCtxt) -> ParseResult<ExprPathSegment> {
1447 Ok(ExprPathSegment { ident: parse_ident(cx)?, node_id: cx.next_node_id() })
1448}
1449
1450fn parse_if_expr(cx: &mut ParseCtxt) -> ParseResult<Expr> {
1454 let mut branches = vec![];
1455
1456 loop {
1457 let lo = cx.lo();
1458 cx.expect(kw::If)?;
1459 let cond = parse_expr(cx, false)?;
1460 let then_ = parse_block(cx)?;
1461 branches.push((lo, cond, then_));
1462 cx.expect(kw::Else)?;
1463
1464 if !cx.peek(kw::If) {
1465 break;
1466 }
1467 }
1468 let mut else_ = parse_block(cx)?;
1469
1470 let hi = cx.hi();
1471 while let Some((lo, cond, then_)) = branches.pop() {
1472 else_ = Expr {
1473 kind: ExprKind::IfThenElse(Box::new([cond, then_, else_])),
1474 node_id: cx.next_node_id(),
1475 span: cx.mk_span(lo, hi),
1476 };
1477 }
1478 Ok(else_)
1479}
1480
1481fn parse_block(cx: &mut ParseCtxt) -> ParseResult<Expr> {
1483 delimited(cx, Brace, parse_block_expr)
1484}
1485
1486fn parse_block_expr(cx: &mut ParseCtxt) -> ParseResult<Expr> {
1488 let lo = cx.lo();
1489 let decls = repeat_while(cx, kw::Let, parse_let_decl)?;
1490 let body = parse_expr(cx, true)?;
1491 let hi = cx.hi();
1492
1493 if decls.is_empty() {
1494 Ok(body)
1495 } else {
1496 let kind = ExprKind::Block(decls, Box::new(body));
1497 Ok(Expr { kind, node_id: cx.next_node_id(), span: cx.mk_span(lo, hi) })
1498 }
1499}
1500
1501fn parse_let_decl(cx: &mut ParseCtxt) -> ParseResult<LetDecl> {
1503 cx.expect(kw::Let)?;
1504 let param = parse_refine_param(cx, RequireSort::Maybe)?;
1505 cx.expect(token::Eq)?;
1506 let init = parse_expr(cx, true)?;
1507 cx.expect(token::Semi)?;
1508 Ok(LetDecl { param, init })
1509}
1510
1511fn parse_lit(cx: &mut ParseCtxt) -> ParseResult<Expr> {
1515 if let Token { kind: token::Literal(lit), lo, hi } = cx.at(0) {
1516 cx.advance();
1517 Ok(Expr {
1518 kind: ExprKind::Literal(lit),
1519 node_id: cx.next_node_id(),
1520 span: cx.mk_span(lo, hi),
1521 })
1522 } else {
1523 Err(cx.unexpected_token(vec![AnyLit.expected()]))
1524 }
1525}
1526
1527fn parse_ident(cx: &mut ParseCtxt) -> ParseResult<Ident> {
1528 if let Token { kind: token::Ident(name, is_raw), lo, hi } = cx.at(0)
1529 && (!cx.is_reserved(name) || is_raw == IdentIsRaw::Yes)
1530 {
1531 cx.advance();
1532 return Ok(Ident { name, span: cx.mk_span(lo, hi) });
1533 }
1534 Err(cx.unexpected_token(vec![NonReserved.expected()]))
1535}
1536
1537fn parse_int<T: FromStr>(cx: &mut ParseCtxt) -> ParseResult<T> {
1538 if let token::Literal(lit) = cx.at(0).kind
1539 && let LitKind::Integer = lit.kind
1540 && let Ok(value) = lit.symbol.as_str().parse::<T>()
1541 {
1542 cx.advance();
1543 return Ok(value);
1544 }
1545
1546 Err(cx.unexpected_token(vec![Expected::Str(std::any::type_name::<T>())]))
1547}
1548
1549fn parse_sort(cx: &mut ParseCtxt) -> ParseResult<Sort> {
1555 if cx.peek(token::OpenParen) {
1556 let inputs = parens(cx, Comma, parse_base_sort)?;
1558 cx.expect(token::RArrow)?;
1559 let output = parse_base_sort(cx)?;
1560 Ok(Sort::Func { inputs, output })
1561 } else {
1562 let bsort = parse_base_sort(cx)?;
1563 if cx.advance_if(token::RArrow) {
1564 let output = parse_base_sort(cx)?;
1566 Ok(Sort::Func { inputs: vec![bsort], output })
1567 } else {
1568 Ok(Sort::Base(bsort))
1570 }
1571 }
1572}
1573
1574fn parse_base_sort(cx: &mut ParseCtxt) -> ParseResult<BaseSort> {
1581 if cx.advance_if(kw::Bitvec) {
1582 cx.expect(LAngle)?;
1584 let len = parse_int(cx)?;
1585 cx.expect(RAngle)?;
1586 Ok(BaseSort::BitVec(len))
1587 } else if cx.advance_if(LAngle) {
1588 let qself = parse_type(cx)?;
1590 cx.expect(kw::As)?;
1591 let mut path = parse_path(cx)?;
1592 cx.expect(RAngle)?;
1593 cx.expect(token::PathSep)?;
1594 path.segments.push(parse_segment(cx)?);
1595 Ok(BaseSort::SortOf(Box::new(qself), path))
1596 } else {
1597 let segments = sep1(cx, token::PathSep, parse_ident)?;
1599 let args = opt_angle(cx, Comma, parse_base_sort)?;
1600 let path = SortPath { segments, args, node_id: cx.next_node_id() };
1601 Ok(BaseSort::Path(path))
1602 }
1603}
1604
1605#[derive(Clone, Copy, PartialEq, PartialOrd, Debug)]
1607enum Precedence {
1608 Iff,
1610 Implies,
1612 Or,
1614 And,
1616 Compare,
1618 BitOr,
1620 BitXor,
1622 BitAnd,
1624 Shift,
1626 Sum,
1628 Product,
1630 Prefix,
1632}
1633
1634enum Associativity {
1635 Right,
1636 Left,
1637 None,
1638}
1639
1640impl Precedence {
1641 const MIN: Self = Precedence::Iff;
1642
1643 fn of_binop(op: &BinOp) -> Precedence {
1644 match op {
1645 BinOp::Iff => Precedence::Iff,
1646 BinOp::Imp => Precedence::Implies,
1647 BinOp::Or => Precedence::Or,
1648 BinOp::And => Precedence::And,
1649 BinOp::Eq | BinOp::Ne | BinOp::Gt | BinOp::Ge | BinOp::Lt | BinOp::Le => {
1650 Precedence::Compare
1651 }
1652 BinOp::BitOr => Precedence::BitOr,
1653 BinOp::BitXor => Precedence::BitXor,
1654 BinOp::BitAnd => Precedence::BitAnd,
1655 BinOp::BitShl | BinOp::BitShr => Precedence::Shift,
1656 BinOp::Add | BinOp::Sub => Precedence::Sum,
1657 BinOp::Mul | BinOp::Div | BinOp::Mod => Precedence::Product,
1658 }
1659 }
1660
1661 fn next(self) -> Precedence {
1662 match self {
1663 Precedence::Iff => Precedence::Implies,
1664 Precedence::Implies => Precedence::Or,
1665 Precedence::Or => Precedence::And,
1666 Precedence::And => Precedence::Compare,
1667 Precedence::Compare => Precedence::BitOr,
1668 Precedence::BitOr => Precedence::BitXor,
1669 Precedence::BitXor => Precedence::BitAnd,
1670 Precedence::BitAnd => Precedence::Shift,
1671 Precedence::Shift => Precedence::Sum,
1672 Precedence::Sum => Precedence::Product,
1673 Precedence::Product => Precedence::Prefix,
1674 Precedence::Prefix => Precedence::Prefix,
1675 }
1676 }
1677
1678 fn associativity(self) -> Associativity {
1679 match self {
1680 Precedence::Or
1681 | Precedence::And
1682 | Precedence::BitOr
1683 | Precedence::BitXor
1684 | Precedence::BitAnd
1685 | Precedence::Shift
1686 | Precedence::Sum
1687 | Precedence::Product => Associativity::Left,
1688 Precedence::Compare | Precedence::Iff => Associativity::None,
1689 Precedence::Implies | Precedence::Prefix => Associativity::Right,
1690 }
1691 }
1692}