Source code for fosf.parsers.theory

#!/usr/bin/env python3

from lark import Lark

from fosf.config import FOSF_GRAMMAR
from fosf.parsers.taxonomy import TaxonomyParser, _TaxonomyTransformer
from fosf.syntax.base import Sort, Tag
from fosf.syntax.terms import NormalTerm, Term
from fosf.syntax.theory import OsfTheory, TheoryTag


class _OsfTheoryTransformer(_TaxonomyTransformer):
    def __init__(self):
        super().__init__()
        self.definitions: dict[Sort, Term] = {}
        self.tags: dict[Tag, TheoryTag] = {}

    def theory(self, tree):
        return tree[0], self.definitions, self.tags, self.domains, self.ranges

    def domain(self, tree):
        feature = tree[0]
        sort = tree[1]
        if feature in self.domains and sort != self.domains[feature]:
            msg = f"Multiple domain declarations for {feature}"
            raise RuntimeError(msg)
        self.domains[feature] = sort

    def range(self, tree):
        feature = tree[0]
        sort = tree[1]
        if feature in self.ranges and sort != self.ranges[feature]:
            msg = f"Multiple range declarations for {feature}"
            raise RuntimeError(msg)
        self.ranges[feature] = sort

    def definition(self, tree):
        sort = tree[0]
        term = tree[1]
        self.definitions[sort] = term

    def theory_term(self, tree):
        tag = Tag(tree[0].value)
        sort = tree[1]
        if len(tree) <= 2:
            self.tags[tag] = TheoryTag(tag, sort)
            return NormalTerm(tag, sort)
        pairs = tree[2]
        features = {}
        subterms = {}
        for f, term in pairs:
            subterms[f] = term
            features[f] = term.X
        theory_tag = TheoryTag(tag, sort, features)
        self.tags[tag] = theory_tag
        return NormalTerm(tag, sort, subterms)

    def theory_unsorted_term(self, tree):
        tag = Tag(tree[0].value)
        if len(tree) > 1:
            return NormalTerm(tag, s=None, subterms=tree[1])
        return NormalTerm(tag)

    def theory_subterms(self, tree):
        return tree

    def theory_subterm(self, tree):
        return tree[0], tree[1]

    def transform(self, parse_tree, **kwargs):
        self.definitions = {}
        self.tags = {}
        self.domains = {}
        self.ranges = {}
        return super().transform(parse_tree, **kwargs)




class OsfTheoryParser(TaxonomyParser):
    def __init__(self):
        self.parser = Lark.open_from_package("fosf", FOSF_GRAMMAR, start="theory")
        self.transformer = _OsfTheoryTransformer()



    def parse(self, expression: str, ensure_closed=False, **kwargs) -> OsfTheory:
        parse_tree = self.parser.parse(expression)
        return OsfTheory(
            *self.transformer.transform(parse_tree, **kwargs), ensure_closed=ensure_closed
        )