Source code for ulkb.extension

# Copyright (C) 2023 IBM Corp.
# SPDX-License-Identifier: Apache-2.0

from . import error
from .object import Object

__all__ = [
    'Assertion',
    'Assumption',
    'Extension',
    'ExtensionError',
    'NewAxiom',
    'NewConstant',
    'NewDefinition',
    'NewPythonTypeAlias',
    'NewTheorem',
    'NewTypeConstructor',
    'NewTypeSpec',
    'Notation',
]


class ExtensionError(error.Error):
    def __init__(self, ext, reason):
        super().__init__(f'{ext.__class__.__name__}: {reason}')
        self.extension = ext
        self.reason = reason


[docs] class Extension(Object): @property def id(self): return self.get_id() def get_id(self): return None def error(self, msg): raise ExtensionError(self, msg)
class Assumption(Extension): pass class NewTypeConstructor(Assumption): def __init__(self, arg1, **kwargs): super().__init__( # (tcons,) arg1, **kwargs) def _preprocess_arg(self, arg, i): arg = super()._preprocess_arg(arg, i) if i == 1: # tcons return self.TypeConstructor.check( arg, self.__class__.__name__, None, i) else: error.should_not_get_here() def get_id(self): return self[0].id class NewConstant(Assumption): def __init__( # (const,) self, arg1, **kwargs): super().__init__(arg1, **kwargs) def _preprocess_arg(self, arg, i): arg = super()._preprocess_arg(arg, i) if i == 1: # const return self.Constant.check( arg, self.__class__.__name__, None, i) else: error.should_not_get_here() def get_id(self): return self[0].id class NewAxiom(Assumption): def __init__( # (const, form) self, arg1, arg2, **kwargs): super().__init__(arg1, arg2, **kwargs) def _preprocess_arg(self, arg, i): arg = super()._preprocess_arg(arg, i) if i == 1: # const arg = self._preprocess_arg_constant(self, arg, i) return arg.check_formula(self.__class__.__name__, None, i) elif i == 2: # form return self._preprocess_arg_formula(self, arg, i) else: error.should_not_get_here() def get_id(self): return self[0].id class Assertion(Extension): pass class NewDefinition(Assertion): def __init__( # (equal,) self, arg1, **kwargs): super().__init__(arg1, **kwargs) def _preprocess_arg(self, arg, i): arg = super()._preprocess_arg(arg, i) if i == 1: # equal arg = self._preprocess_arg_equal(self, arg, i) l, r = arg.unpack_equal() if not l.is_variable(): error.arg_error( arg, 'not a definitional equation', self.__class__.__name__, None, i) elif r.has_free_variables(): error.arg_error( arg, 'definiens is not closed', self.__class__.__name__, None, i) elif not (r.type_variables <= l.type_variables): msg = error._build_plural_message( 'extra type variable%s in definiens', *(r.type_variables - l.type_variables)) error.arg_error( arg, msg, self.__class__.__name__, None, i) return arg else: error.should_not_get_here() def get_id(self): l, _ = self[0]._unpack_equal() return l.id class NewTheorem(Assertion): def __init__( # (const, seq) self, arg1, arg2, **kwargs): super().__init__(arg1, arg2, **kwargs) def _preprocess_arg(self, arg, i): arg = super()._preprocess_arg(arg, i) if i == 1: # const arg = self._preprocess_arg_constant(self, arg, i) return arg.check_formula(self.__class__.__name__, None, i) elif i == 2: # seq return self._preprocess_arg_sequent(self, arg, i) else: error.should_not_get_here() def get_id(self): return self[0].id class Notation(Extension): pass class NewPythonTypeAlias(Notation): def __init__( # (py_type, type, spec) self, arg1, arg2, arg3=None, **kwargs): super().__init__(arg1, arg2, arg3, **kwargs) def _preprocess_arg(self, arg, i): if i != 3: # skip possible None arg = super()._preprocess_arg(arg, i) if i == 1: # py_type or str arg = __builtins__.get(arg, arg) return error.check_arg_class( arg, type, self.__class__.__name__, None, i) elif i == 2: # type return self.Type.check( arg, self.__class__.__name__, None, i) elif i == 3: if isinstance(arg, type): arg = arg.__name__ return error.check_optional_arg( arg, lambda x: isinstance(x, str), None, None, self.__class__.__name__, None, i) else: error.should_not_get_here() class NewTypeSpec(Notation): def __init__( # (type, spec) self, arg1, **kwargs): super().__init__(arg1, **kwargs) def _preprocess_arg(self, arg, i): arg = super()._preprocess_arg(arg, i) if isinstance(arg, type): arg = arg.__name__ return error.check_arg_class( arg, str, self.__class__.__name__, None, i)