git @ Cat's Eye Technologies Ebfer / master src / ebfer / parser.py
master

Tree @master (Download .tar.gz)

parser.py @master — raw · history · blame 

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
# Copyright (c) 2025-2026 Chris Pressey, Cat's Eye Technologies.
# This file is distributed under a 2-clause BSD license.  See LICENSES/ dir.
# SPDX-License-Identifier: LicenseRef-BSD-2-Clause-X-Ebfer

from .scanner import Scanner
from .term import Ctor, IntValue, Term
from .ast import Rule, Theorem, Development


class Parser(object):
    def __init__(self, text: str):
        self.scanner = Scanner(text, "...")

    def development(self) -> Development:
        theorems = []
        functions = []
        rules = []
        seen_rules = set()
        while self.scanner.on("fun"):  # Ebferism
            functions.append(self.fun_decl())
        while self.scanner.on("rule"):
            rule = self.rule_decl()
            if rule.lhs.symbol in seen_rules:
                self.scanner.syntax_error(
                    "Multiple definitions of rule for {}".format(rule.lhs.symbol)
                )
            seen_rules.add(rule.lhs.symbol)
            rules.append(rule)
        while self.scanner.on("proof", "theorem"):
            theorems.append(self.theorem())
        return Development(functions=functions, rules=rules, theorems=theorems)

    def fun_decl(self) -> Rule:
        self.scanner.expect("fun")
        return self.rule()

    def rule_decl(self) -> Rule:
        self.scanner.expect("rule")
        return self.rule()

    def rule(self) -> Rule:
        lhs = self.term()
        assert isinstance(lhs, Ctor)
        self.scanner.expect("=>")
        rhs = self.term()
        return Rule(lhs=lhs, rhs=rhs)

    def theorem(self) -> Theorem:
        rule = None
        if self.scanner.consume("theorem"):
            rule = self.rule()
        self.scanner.expect("proof")
        terms = []
        while not self.scanner.on("qed"):
            terms.append(self.term())
        self.scanner.expect("qed")
        return Theorem(rule=rule, terms=terms)

    def term(self) -> Term:
        is_decoration = False
        if self.scanner.consume("*"):
            is_decoration = True
        if self.scanner.on_type("identifier"):
            assert self.scanner.token
            symbol = ("*" if is_decoration else "") + self.scanner.token
            self.scanner.scan()
            subterms = []
            if self.scanner.consume('('):
                while not self.scanner.on(')'):
                    subterms.append(self.term())
                    if not self.scanner.on(')'):
                        self.scanner.expect(',')
                self.scanner.expect(')')
            return Ctor(symbol=symbol, subterms=subterms)
        elif self.scanner.on_type("integer literal"):  # Ebferism
            assert self.scanner.token
            value = IntValue(value=int(self.scanner.token))
            self.scanner.scan()
            return value
        else:
            self.scanner.syntax_error(
                f"Expected identifier or integer literal, found '{self.scanner.token}'"
            )
            raise