Method parse_structure

leanr-syntax/src/parser.rs:211–254

Parse structure declaration

(&mut self)

    /// Parse structure declaration
    fn parse_structure(&mut self) -> crate::Result<StructureDecl> {
        let start = self.expect(TokenKind::Structure)?.span;

        let name = self.parse_ident()?;
        let universe_params = self.parse_universe_params()?;
        let params = self.parse_params()?;

        let extends = Vec::new(); // TODO: Parse extends

        self.expect(TokenKind::Where)?;

        let mut fields = Vec::new();
        while !self.is_eof() && !self.check(&TokenKind::RBrace) {
            let field_name = self.parse_ident()?;
            self.expect(TokenKind::Colon)?;
            let field_type = Box::new(self.parse_expr()?);

            fields.push(Field {
                span: field_name.span.to(field_type.span()),
                name: field_name,
                type_: field_type,
            });

            if !self.check(&TokenKind::Comma) {
                break;
            }
            self.advance();
        }

        let end = if let Some(last) = fields.last() {
            last.span
        } else {
            name.span
        };

        Ok(StructureDecl {
            span: start.to(end),
            name,
            universe_params,
            params,
            extends,
            fields,
        })
    }

    /// Parse universe parameters: .{u v}
    fn parse_universe_params(&mut self) -> crate::Result<Vec<Ident>> {