main.py

"""
_sympy_ docs: https://docs.sympy.org/latest/modules/core.html#sympy.core.sympify.sympify
"""

from enum import Enum, auto

from sympy import categories, pprint, default_sort_key
from textx import metamodel_from_file

class Object:
    sym: categories.Object

    def __init__(self, parent: 'Category', name: str):
        self.parent = parent
        self.name = name
        self.sym = categories.Object(name)
    
    def __repr__(self):
        return repr(self.sym)

    def __str__(self):
        return str(self.sym)
    
    def _sympy_(self):
        return self.sym

class ArrowType(Enum):
    Total = auto()
    Partial = auto()
    Inclusion = auto()

    @staticmethod
    def from_str(s: str) -> 'ArrowType':
        match s:
            case "→" | "\\to" | "->":
                return ArrowType.Total
            case "⇀" | "\\rightharpoonup" | "\\harpoon":
                return ArrowType.Partial
            case "↪" | "\\hookrightarrow" | "\\hook" | "\\->":
                return ArrowType.Inclusion
            case _:
                raise ValueError(f"Inappropriate value {s!r}.")

class Arrow:
    sym: categories.Morphism
    type: ArrowType

    def __init__(self, parent: 'Category', name: str, domain: Object, arrow: str, codomain: Object):
        self.parent = parent
        self.name = name
        self.domain = domain
        self.codomain = codomain
        self.type = ArrowType.from_str(arrow)

        self.sym = categories.NamedMorphism(domain.sym, codomain.sym, name)

    def __repr__(self):
        return repr(self.sym)

    def __str__(self):
        return str(self.sym)
    
    def _sympy_(self):
        return self.sym

class Category:
    sym: categories.Category
    diagram: categories.Diagram

    def __init__(self, parent, name: str, statements: list[Object | Arrow]):
        self.parent = parent
        self.name = name
        self.statements = statements
        self.diagram = categories.Diagram(
            [
                stmt.sym
                for stmt in statements
                if isinstance(stmt, Arrow)
            ]
        )
        
        self.sym = categories.Category(name, commutative_diagrams=[self.diagram])

    def __repr__(self):
        return repr(self.sym)

    def __str__(self):
        return str(self.sym)
    
    def _sympy_(self):
        return self.sym


catlang = metamodel_from_file(
    'grammar.tx',
    classes=[Object, Arrow, Category],
)


fpl = catlang.model_from_file('demos/fpl.cl')
morphemes = catlang.model_from_file('demos/morphemes.cl')

cat = fpl.category.diagram
premises_keys = sorted(cat.premises.keys(), key=default_sort_key)
print("Deductions:")
for premise in premises_keys:
    pprint(premise, use_unicode=True)