Revise λ−term signature symbols

Author: v--

src/notebook/math/lambda_/algebraic_types/alpha.py

@@ -4,6 +4,7 @@
 from ....support.schemas import SchemaInferenceError
 from ..assertions import VariableTypeAssertion
 from ..instantiation import AtomicLambdaSchemaInstantiation, infer_instantiation_from_term, instantiate_term_schema
+from ..signature import ConstantTermSymbol
 from ..terms import Constant, TypedAbstraction, TypedApplication, TypedTerm
 from ..type_derivation import (
     AssumptionTree,
@@ -109,7 +110,7 @@ def visit_sum_elim(
         if not isinstance(self.other, TypedApplication) or \
             not isinstance(self.other.left, TypedApplication) or \
             not isinstance(self.other.left.left, TypedApplication) or \
-            self.other.left.left.left != Constant('S₋'):
+            self.other.left.left.left != Constant(ConstantTermSymbol('S₋')):
             raise NotAlphaEquivalent
 
         other_sum_term = self.other.right

src/notebook/math/lambda_/algebraic_types/test_alpha.py

@@ -15,6 +15,7 @@
     parse_variable,
     parse_variable_assertion,
 )
+from ..signature import BaseTypeSymbol
 from ..type_derivation import RuleApplicationTree, TypeDerivationError, apply, assume, premise
 from ..types import BaseType
 from .alpha import alpha_convert_derivation
@@ -85,8 +86,8 @@ def factory(x: str, y: str) -> RuleApplicationTree:
             ),
 
             premise(
-                tree=assume(VariableTypeAssertion(parse_variable(x), BaseType('𝟙'))),
-                discharge=VariableTypeAssertion(parse_variable(x), BaseType('𝟙'))
+                tree=assume(VariableTypeAssertion(parse_variable(x), BaseType(BaseTypeSymbol('𝟙')))),
+                discharge=VariableTypeAssertion(parse_variable(x), BaseType(BaseTypeSymbol('𝟙')))
             ),
 
             premise(

src/notebook/math/lambda_/curry_howard/derivation_to_proof.py

@@ -33,7 +33,7 @@ def type_connective_to_formula_connective(conn: BinaryTypeConnective) -> BinaryC
 class TypeToFormulaVisitor(TypeVisitor[Formula]):
     @override
     def visit_base(self, type_: BaseType) -> PropConstant:
-        match type_.name:
+        match type_.value.name:
             case '𝟙':
                 return PropConstant(PropConstantSymbol.VERUM)
 

src/notebook/math/lambda_/curry_howard/proof_to_derivation.py

@@ -19,6 +19,7 @@
 from ..assertions import VariableTypeAssertion
 from ..instantiation import AtomicLambdaSchemaInstantiation
 from ..parsing import parse_type_variable
+from ..signature import BaseTypeSymbol
 from ..terms import Variable
 from ..type_derivation import tree as dtree
 from ..type_system import TypingRule
@@ -52,10 +53,10 @@ class FormulaToTypeVisitor(FormulaVisitor[SimpleType]):
     def visit_prop_constant(self, formula: PropConstant) -> BaseType:
         match formula.value:
             case PropConstantSymbol.VERUM:
-                return BaseType('𝟙')
+                return BaseType(BaseTypeSymbol('𝟙'))
 
             case PropConstantSymbol.FALSUM:
-                return BaseType('𝟘')
+                return BaseType(BaseTypeSymbol('𝟘'))
 
     @override
     def visit_predicate(self, formula: PredicateApplication) -> TypeVariable:

src/notebook/math/lambda_/parsing/parser.py

@@ -50,7 +50,7 @@ def __init__(self, signature: LambdaSignature, source: str, tokens: Sequence[Lam
     def _parse_base_type(self) -> BaseType:
         head = self.peek_unsafe()
         self.advance()
-        return BaseType(head.value)
+        return BaseType(self.signature.get_base_type_symbol(head.value))
 
     def parse_type_variable(self) -> TypeVariable:
         identifier = self.parse_greek_identifier('SMALL_GREEK_IDENTIFIER')
@@ -137,7 +137,7 @@ def parse_type(self, *, parse_schema: bool) -> SimpleType | SimpleTypeSchema:
     def _parse_constant(self) -> Constant:
         head = self.peek_unsafe()
         self.advance()
-        return Constant(head.value)
+        return Constant(self.signature.get_constant_term_symbol(head.value))
 
     def parse_term_placeholder(self) -> TermPlaceholder:
         identifier = self.parse_latin_identifier('CAPITAL_LATIN_IDENTIFIER')

src/notebook/math/lambda_/parsing/test_parser.py

@@ -88,13 +88,13 @@ def test_parsing_invalid_variable_suffix() -> None:
 @pytest_parametrize_kwargs(
     dict(
         term='𝐐',
-        expected=Constant('𝐐')
+        expected=Constant(ConstantTermSymbol('𝐐'))
     ),
     dict(
         term='(𝐐(𝐐x))',
         expected=UntypedApplication(
-            Constant('𝐐'),
-            UntypedApplication(Constant('𝐐'), Variable(LatinIdentifier('x')))
+            Constant(ConstantTermSymbol('𝐐')),
+            UntypedApplication(Constant(ConstantTermSymbol('𝐐')), Variable(LatinIdentifier('x')))
         )
     )
 )

src/notebook/math/lambda_/signature/signature.py

@@ -2,7 +2,7 @@
 
 from ....support.collections import MissingKeyError, TrieMapping
 from .exceptions import LambdaSignatureError
-from .symbols import SignatureSymbol
+from .symbols import BaseTypeSymbol, ConstantTermSymbol, SignatureSymbol
 
 
 class LambdaSignature:
@@ -25,6 +25,22 @@ def add_symbol(self, symbol: SignatureSymbol) -> None:
     def __getitem__(self, name: str) -> SignatureSymbol:
         return self.trie[name]
 
+    def get_constant_term_symbol(self, name: str) -> ConstantTermSymbol:
+        sym = self[name]
+
+        if not isinstance(sym, ConstantTermSymbol):
+            raise LambdaSignatureError(f'Expected {name} to be a constant term symbol, but got a {sym.get_kind_string()}')
+
+        return sym
+
+    def get_base_type_symbol(self, name: str) -> BaseTypeSymbol:
+        sym = self[name]
+
+        if not isinstance(sym, BaseTypeSymbol):
+            raise LambdaSignatureError(f'Expected {name} to be a constant term symbol, but got a {sym.get_kind_string()}')
+
+        return sym
+
     def __contains__(self, symbol: SignatureSymbol) -> bool:
         try:
             existing = self.trie[symbol.name]

src/notebook/math/lambda_/terms/terms.py

@@ -2,15 +2,16 @@
 
 from ....parsing.identifiers import LatinIdentifier
 from ..alphabet import BinderSymbol
+from ..signature import ConstantTermSymbol
 from ..types import SimpleType
 
 
 @dataclass(frozen=True)
 class Constant:
-    name: str
+    value: ConstantTermSymbol
 
     def __str__(self) -> str:
-        return str(self.name)
+        return str(self.value)
 
     def __repr__(self) -> str:
         return f"parse_term('{self}')"

src/notebook/math/lambda_/types/types.py

@@ -2,14 +2,15 @@
 
 from ....parsing.identifiers import GreekIdentifier
 from ..alphabet import BinaryTypeConnective
+from ..signature import BaseTypeSymbol
 
 
 @dataclass(frozen=True)
 class BaseType:
-    name: str
+    value: BaseTypeSymbol
 
     def __str__(self) -> str:
-        return str(self.name)
+        return str(self.value)
 
     def __repr__(self) -> str:
         return f"parse_type('{self}')"

src/notebook/math/lambda_/untyped/alpha.py

@@ -11,12 +11,12 @@ def are_terms_alpha_equivalent(m: UntypedTerm, n: UntypedTerm) -> bool:
         case (Constant(), Constant()):
             assert isinstance(m, Constant)
             assert isinstance(n, Constant)
-            return m.name == n.name
+            return m == n
 
         case (Variable(), Variable()):
             assert isinstance(m, Variable)
             assert isinstance(n, Variable)
-            return m.identifier == n.identifier
+            return m == n
 
         case (UntypedApplication(), UntypedApplication()):
             assert isinstance(m, UntypedApplication)