Source code for ulkb.theory

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

import importlib
import sys

from . import error, util
from .expression import *
from .extension import *
from .object import *
from .rule import RuleAxiom
from .theory_settings import *

__all__ = [
    'Theory',
]


[docs] class Theory(Object): """The state of the logic developments so far. A :class:`Theory` consists of a sequence of extensions (:class:`Extension`). Multiple :class:`Theory` objects can coexist, but at any time only one of them is the current or *top* theory. By default, :doc:`commands <commands>` and other top-level functions operate over the top theory. The top theory can be accessed using :attr:`Theory.top` or :func:`_thy`. It can be changed using :func:`Theory.push` and restored using :func:`Theory.pop`. Parameters: args: Extensions. load_prelude: Whether to load the standard prelude. kwargs: Annotations. Returns: :class:`Theory`. """ #: The top theory. top = None #: Theory stack. _stack = [] #: Prefix of the prelude module (initialized by __init__.py). _prelude_prefix = None @classmethod def _dup(cls, *args, **kwargs): return cls(*args, load_prelude=False, **kwargs) @classmethod def _check_args(cls, self, *args, theory=None): if not isinstance(self, Theory): thy = theory if theory is not None else cls._thy() args = (self, *args) else: thy = self return thy, args
[docs] @classmethod def push(cls, theory): """Pushes `theory` onto theory stack. Makes `theory` the new top theory. Parameters: theory: :class:`Theory`. Returns: `theory`. """ cls._stack.append(theory) cls.top = theory return theory
[docs] @classmethod def pop(cls): """Pops theory from theory stack. Makes the theory immediately below the popped one the new top theory. Returns: The popped theory. """ assert len(cls._stack) > 1 theory = cls._stack.pop() cls.top = cls._stack[-1] return theory
__slots__ = ( '_cached_ids', '_cached_type_constructors', '_cached_type_constructors_dict', '_cached_constants', '_cached_constants_dict', '_cached_axioms_dict', '_cached_definitions_dict', '_cached_theorems_dict', '_cached_python_type_aliases_dict', '_cached_python_type_alias_specs_dict', '_cached_type_specs_dict', '_prelude', '_prelude_offset', '_settings', ) def __init__(self, *args, load_prelude=True, **kwargs): super().__init__(**kwargs) self._settings = TheorySettings() if load_prelude: self._prelude = self._load_prelude() self._prelude_offset = len(self.args) else: self._prelude = None self._prelude_offset = 0 for ext in args: self._extend(ext) def __enter__(self): return self.push(self) def __exit__(self, err_type, err_val, err_bt): if err_val is not None: raise err_val else: return self.pop() def _set_args(self, args): self._args = list(args) # make args mutable def _reset_object_caches(self): self._hash = None self._hexdigest = None def _build_ids_cache(self): return dict() def _build_type_constructors_cache(self): return set() def _build_type_constructors_dict_cache(self): return dict() def _build_constants_cache(self): return set() def _build_constants_dict_cache(self): return dict() def _build_axioms_dict_cache(self): return dict() def _build_definitions_dict_cache(self): return dict() def _build_theorems_dict_cache(self): return dict() def _build_python_type_aliases_dict_cache(self): return dict() def _build_python_type_alias_specs_dict_cache(self): return dict() def _build_type_specs_dict_cache(self): return dict() # -- Modules -----------------------------------------------------------
[docs] def load(self, mod_name): """Loads module into theory. Parameters: mod_name: Module name. Returns: The loaded module. """ with self: if mod_name in sys.modules: importlib.reload(sys.modules[mod_name]) else: importlib.import_module(mod_name) return sys.modules[mod_name]
# -- Prelude ----------------------------------------------------------- def _load_prelude(self): from types import ModuleType mod = self.load(self._prelude_prefix + '.prelude') for k in dir(mod): v = getattr(mod, k) if isinstance(v, ModuleType): self.load(v.__name__) return mod @property def prelude(self): """Prelude module or ``None`` (not loaded).""" return self.get_prelude()
[docs] def get_prelude(self): """Gets prelude module. Returns: Prelude module or ``None`` (not loaded). """ return self._prelude
@property def prelude_offset(self): """Start index of non-prelude extensions.""" return self.get_prelude_offset()
[docs] def get_prelude_offset(self): """Gets start index of non-prelude extensions. Returns: Start index of non-prelude extensions. """ return self._prelude_offset
@property def args_no_prelude(self): """Theory arguments excluding prelude extensions.""" return self.get_args_no_prelude()
[docs] def get_args_no_prelude(self): """Gets theory arguments excluding prelude extensions. Returns: Theory arguments excluding prelude extensions. """ return self[self._prelude_offset:]
# -- Settings ---------------------------------------------------------- @property def settings(self): """Theory settings table. See also: :class:`ulkb.theory_settings.TheorySettings`. """ return self.get_settings()
[docs] def get_settings(self): """Gets theory settings table. Returns: Theory settings table. See also: :class:`ulkb.theory_settings.TheorySettings`. """ return self._settings
# -- Adding extensions -------------------------------------------------
[docs] def extend(self, ext): """Adds extension. Parameters: ext: :class:`Extension`. Returns: `ext`. Raises: ExtensionError: `ext` cannot be added to theory. See also: :func:`extend`. """ return self._extend(Extension.check(ext))
def _extend( self, ext, func_name=None, arg_name=None, arg_position=None): if ext in self.args: return ext # nothing to do if ext.id is not None and ext.id in self.ids: raise ext.error(f"extension '{ext.id}' already exists") if ext.is_new_type_constructor(): pass elif ext.is_new_constant(): (const,) = ext._unpack_new_constant() self._check_extension_types(ext, const.type) elif ext.is_new_axiom(): const, form = ext._unpack_new_axiom() self._check_extension_types(ext, form) self._cache_extension(NewConstant(const)) elif ext.is_new_definition(): (form,) = ext._unpack_new_definition() l, r = form._unpack_equal() self._check_extension_types(ext, form) self._cache_extension(NewConstant(Constant(l.id, l.type))) self._check_extension_constants(ext, r) elif ext.is_new_theorem(): const, seq = ext._unpack_extension() for form in util.chain(seq.hypotheses, [seq.conclusion]): self._check_extension_types(ext, form) self._cache_extension(NewConstant(const)) elif ext.is_new_python_type_alias(): (_, type, spec) = ext._unpack_new_python_type_alias() self._check_extension_types(ext, type) if spec is not None and not hasattr(self, spec): raise ext.error(f"undefined type alias spec '{spec}'") elif ext.is_new_type_spec(): (spec,) = ext._unpack_new_type_spec() if not hasattr(self, spec): raise ext.error(f"undefined type spec '{spec}'") else: error.should_not_get_here() self._cache_extension(ext) self.args.append(ext) return ext def _check_extension_constants(self, ext, term): for c in term.constants: if (c.id not in self.constants_dict or not util.any_map( lambda x: c.type.matches(x.type), term.constants)): raise ext.error(f"undefined constant '{c}'") return term def _check_extension_types(self, ext, term): if term.type_constructors <= self.type_constructors: return term else: msg = error._build_plural_message( 'undefined type constructor%s', *(term.type_constructors - self.type_constructors)) raise ext.error(msg) def _cache_extension(self, ext): if ext.id is not None: self.ids[ext.id] = ext if ext.is_new_type_constructor(): (tcons,) = ext._unpack_new_type_constructor() self.type_constructors.add(tcons) self.type_constructors_dict[tcons] = tcons self.type_constructors_dict[tcons.id] = tcons elif ext.is_new_constant(): (const,) = ext._unpack_new_constant() self.constants.add(const) self.constants_dict[const] = const self.constants_dict[const.id] = const elif ext.is_new_axiom(): const, form = ext._unpack_new_axiom() seq = RuleAxiom(form) self.axioms_dict[const] = seq self.axioms_dict[const.id] = seq elif ext.is_new_definition(): (form,) = ext._unpack_new_definition() l, r = form._unpack_equal() const = self.constants_dict[l.id] seq = RuleAxiom(self.Equal(const, r)) self.definitions_dict[const] = seq self.definitions_dict[const.id] = seq elif ext.is_new_theorem(): const, seq = ext._unpack_new_theorem() self.theorems_dict[const] = seq self.theorems_dict[const.id] = seq elif ext.is_new_python_type_alias(): py_type, type, spec = ext._unpack_new_python_type_alias() self.python_type_aliases_dict[py_type.__name__] = type self.python_type_aliases_dict[py_type] = type if spec is not None: spec = getattr(self, spec) self.python_type_alias_specs_dict[py_type.__name__] = spec self.python_type_alias_specs_dict[py_type] = spec elif ext.is_new_type_spec(): (spec,) = ext._unpack_new_type_spec() spec = getattr(self, spec) self.type_specs_dict[spec.constructor.id] = spec self.type_specs_dict[spec.constructor] = spec else: error.should_not_get_here() self._reset_object_caches() def _uncache_extension(self, ext): if ext.id is not None: self.ids.pop(ext.id) if ext.is_new_type_constructor(): (tcons,) = ext._unpack_new_type_constructor() self.type_constructors.remove(tcons) self.type_constructors_dict.pop(tcons) self.type_constructors_dict.pop(tcons.id) elif ext.is_new_constant(): (const,) = ext._unpack_new_constant() self._uncache_constant(const) elif ext.is_new_axiom(): const, form = ext._unpack_new_axiom() self._uncache_constant(const) self.axioms_dict.pop(const) self.axioms_dict.pop(const.id) elif ext.is_new_definition(): (form,) = ext._unpack_new_definition() l, _ = form._unpack_equal() const = self.lookup_constant(l.id) self._uncache_constant(const) self.definitions_dict.pop(const) self.definitions_dict.pop(const.id) elif ext.is_new_theorem(): const, _ = ext._unpack_new_theorem() self._uncache_constant(const) self.theorems_dict.pop(const) self.theorems_dict.pop(const.id) elif ext.is_new_python_type_alias(): py_type, _, spec = ext._unpack_new_python_type_alias() self.python_type_aliases_dict.pop(py_type.__name__) self.python_type_aliases_dict.pop(py_type) if spec is not None: self.python_type_alias_specs_dict.pop(py_type.__name__) self.python_type_alias_specs_dict.pop(py_type) else: error.should_not_get_here() self._reset_object_caches() def _uncache_constant(self, const): self.constants.remove(const) self.constants_dict.pop(const) self.constants_dict.pop(const.id)
[docs] def new_base_type(self, arg1, **kwargs): """Adds new base type. Parameters: arg1: Id. kwargs: Annotations. Returns: :class:`TypeApplication`. .. code-block:: python :caption: Equivalent to: self.extend(NewTypeConstructor( TypeConstructor(arg1, 0, None, **kwargs)))[0]() See also: :func:`new_base_type`. """ return self.new_type_constructor(arg1, 0, None, **kwargs)()
[docs] def new_type_constructor(self, arg1, arg2, arg3=None, **kwargs): """Adds new type constructor. Parameters: arg1: Id. arg2: Arity. arg3: Associativity (``'left'`` or ``'right'``). kwargs: Annotations. Returns: :class:`TypeConstructor`. .. code-block:: python :caption: Equivalent to: self.extend(NewTypeConstructor( TypeConstructor(arg1, arg2, arg3, **kwargs)))[0] See also: :func:`new_type_constructor`. """ return self._extend(NewTypeConstructor( TypeConstructor(arg1, arg2, arg3, **kwargs)))[0]
[docs] def new_constant(self, arg1, arg2, **kwargs): """Adds new constant. Parameters: arg1: Id. arg2: :class:`Type`. kwargs: Annotations. Returns: :class:`Constant`. .. code-block:: python :caption: Equivalent to: self.extend(NewConstant(Constant(arg1, arg2, **kwargs)))[0] See also: :func:`new_constant`. """ return self._extend(NewConstant(Constant(arg1, arg2, **kwargs)))[0]
[docs] def new_axiom(self, arg1, arg2=None, **kwargs): """Adds new axiom. If `arg2` is not given, uses `arg1` to generate an id. Parameters: arg1: Id or :class:`Formula`. arg2: :class:`Formula`. kwargs: Annotations. Returns: :class:`Sequent`. .. code-block:: python :caption: Equivalent to: self.extend(NewAxiom( Constant(arg1, arg2.type), arg2, **kwargs)); self.axioms_dict[arg1] See also: :func:`new_axiom`. """ if arg2 is None: arg2, arg1 = arg1, arg1._as_id() self._extend(NewAxiom(Constant(arg1, arg2.type), arg2, **kwargs)) return self.axioms_dict[arg1]
[docs] def new_definition(self, arg1, arg2, **kwargs): """Adds new definition. Parameters: arg1: Id. arg2: :class:`Term`. kwargs: Annotations. Returns: :class:`Constant`. .. code-block:: python :caption: Equivalent to: self.extend(NewDefinition( Equal(Constant(arg1, arg2.type), arg2), **kwargs)); self.constants_dict[arg1] See also: :func:`new_definition`. """ self._extend(NewDefinition( self.Equal(Variable(arg1, arg2.type), arg2), **kwargs)) return self.constants_dict[arg1]
[docs] def new_theorem(self, arg1, arg2=None, **kwargs): """Adds new theorem. If `arg2` is not given, uses `arg1` to generate an id. Parameters: arg1: Id or :class:`Sequent`. arg2: :class:`Sequent`. kwargs: Annotations. Returns: :class:`Sequent` .. code-block:: python :caption: Equivalent to: extend(NewTheorem( Constant(arg1, BoolType()), arg2), **kwargs)); self.theorems_dict[arg1] See also: :func:`new_theorem`. """ if arg2 is None: arg2, arg1 = arg1, arg1._as_id() self._extend(NewTheorem(Constant(arg1, bool), arg2, **kwargs)) return self.theorems_dict[arg1]
[docs] def new_python_type_alias(self, arg1, arg2, arg3=None, **kwargs): """Adds new Python type alias. Parameters: arg1: Python type. arg2: :class:`Type`. arg3: Type specification. kwargs: Annotations. Returns: :class:`Type`. .. code-block:: python :caption: Equivalent to: extend(NewPythonTypeAlias(arg1, arg2, **kwargs))[1] See also: :func:`new_python_type_alias`. """ return self._extend(NewPythonTypeAlias(arg1, arg2, arg3, **kwargs))
# -- Removing extensions -----------------------------------------------
[docs] def reset(self, arg=None): """Removes all extensions since *arg* (inclusive). If `arg` is an id, goes back to the extension preceding the one introducing the object with id `arg`. If `arg` is an object, goes back to the extension preceding the one introducing `arg`. If `arg` is a non-negative integer, goes back to the extension preceding the one at offset `arg`. If `arg` is a negative integer, drops the last `abs(arg)` extensions. If `arg` is not given, goes back to the initial state; i.e., makes `arg` equal to :attr:`Theory.prelude_offset`. Parameters: arg: Id, :class:`Object`, or int. Returns: The number of extensions removed. Raises: LookupError: `arg` not in theory. """ if arg is None: start = self.prelude_offset elif isinstance(arg, int): if arg >= 0: start = arg else: start = len(self.args) + arg elif Object.test(arg): if Extension.test(arg) and arg in self.args: start = self.args.index(arg) elif hasattr(arg, 'id'): start = self.args.index(self.lookup_extension(arg.id)) else: raise LookupError(f"no such extension '{arg}'") else: # arg is an id start = self.args.index(self.lookup_extension(arg)) if start < self.prelude_offset: self._prelude_offset = start n = len(self.args) for i in range(n - 1, start - 1, -1): ext = self.args[i] self._uncache_extension(ext) self.args.pop() return n - start
# -- Querying extensions -----------------------------------------------
[docs] def enumerate_extensions( self, *args, limit=None, offset=None, id=None, class_=None): """Enumerates extensions matching criteria. If `offset` is not given, assumes :attr:`Theory.prelude_offset`. Parameters: args: Expressions that must occur in extension. limit: Maximum number of results. offset: Minimum offset. id: Id (regex). class_: Class. Returns: An iterator of index-:class:`Extension` pairs. See also: :func:`enumerate_extensions`. """ offset = offset if offset is not None else self._prelude_offset if id is not None: _id_re = util.compile(id) if class_ is not None: error.check_arg_is_type( class_, 'enumerate_extensions', 'class_') if args: args_cts, args_tcs = set(), set() for i, arg in enumerate(args): if isinstance(arg, type): try: arg = self.lookup_python_type_alias(arg) except: pass Expression.check(arg, 'enumerate_extensions', None, i) if arg.is_term(): args_cts.update(arg.constants) args_tcs.update(arg.type_constructors) n = 0 for i, x in enumerate(self[offset:]): if id and (not x.id or not _id_re.match(x.id)): continue if class_ and not isinstance(x, class_): continue if args: if args_cts: cts = set.union(set(), *map( lambda t: t.constants, filter(Term.test, x.args))) if args_cts.isdisjoint(cts): continue if args_tcs: tcs = set.union(set(), *map( lambda t: t.type_constructors, filter(Expression.test, x.args))) if not (args_tcs & tcs): continue if limit is not None and n >= limit: break n += 1 yield (offset + i, x)
def _lookup(self, dict_, target, arg, default): obj = dict_.get(arg, default) if obj is not util.Nil: return obj else: raise LookupError(f"no such {target} '{arg}'")
[docs] def lookup_extension(self, arg, default=util.Nil): """Searches for extension. If `default` is given, returns it instead of raising an exception. Parameters: arg: Id. default: Value. Returns: :class:`Extension`. Raises: LookupError: `arg` not in theory. See also: :func:`lookup_extension`. """ return self._lookup(self.ids, 'extension', arg, default)
[docs] def lookup_type_constructor(self, arg, default=util.Nil): """Searches for type constructor. If `default` is given, returns it instead of raising an exception. Parameters: arg: Id or :class:`TypeConstructor`. default: Value. Returns: :class:`TypeConstructor`. Raises: LookupError: `arg` not in theory. See also: :func:`lookup_type_constructor`. """ return self._lookup( self.type_constructors_dict, 'type constructor', arg, default)
[docs] def lookup_constant(self, arg, default=util.Nil): """Searches for constant. If `default` is given, returns it instead of raising an exception. Parameters: arg: Id or :class:`Constant`. default: Value. Returns: :class:`Constant`. Raises: LookupError: `arg` not in theory. See also: :func:`lookup_constant`. """ return self._lookup(self.constants_dict, 'constant', arg, default)
[docs] def lookup_axiom(self, arg, default=util.Nil): """Searches for axiom. If `default` is given, returns it instead of raising an exception. Parameters: arg: Id or :class:`Constant`. default: Value. Returns: :class:`Sequent`. Raises: LookupError: `arg` not in theory. See also: :func:`lookup_axiom`. """ return self._lookup(self.axioms_dict, 'axiom', arg, default)
[docs] def lookup_definition(self, arg, default=util.Nil): """Searches for definition. If `default` is given, returns it instead of raising an exception. Parameters: arg: Id or :class:`Constant`. default: Value. Returns: :class:`Sequent`. Raises: LookupError: `arg` not in theory. See also: :func:`lookup_definition`. """ return self._lookup( self.definitions_dict, 'definition', arg, default)
[docs] def lookup_theorem(self, arg, default=util.Nil): """Searches for theorem. If `default` is given, returns it instead of raising an exception. Parameters: arg: Id or :class:`Constant`. default: Value. Returns: :class:`Sequent`. Raises: LookupError: `arg` not in theory. See also: :func:`lookup_theorem`. """ return self._lookup( self.theorems_dict, 'theorem', arg, default)
[docs] def lookup_python_type_alias(self, arg, default=util.Nil): """Searches for Python type alias. If `default` is given, returns it instead of raising an exception. Parameters: arg: Id. default: Value. Returns: :class:`Type`. Raises: LookupError: `arg` not in theory. See also: :func:`lookup_python_type_alias`. """ return self._lookup( self.python_type_aliases_dict, 'type alias', arg, default)
def lookup_python_type_alias_spec(self, arg, default=util.Nil): """Searches for Python type alias specification. If `default` is given, returns it instead of raising an exception. Parameters: arg: Id. default: Value. Returns: Type specification. Raises: LookupError: `arg` not in theory. """ return self._lookup( self.python_type_alias_specs_dict, 'type alias spec', arg, default) # -- Showing extensions ------------------------------------------------
[docs] def show_extensions( self, *args, limit=None, offset=None, id=None, class_=None, **kwargs): """Prints extensions matching criteria. If `offset` is not given, assumes :attr:`Theory.prelude_offset`. Parameters: args: Expressions that must occur in extension. limit: Maximum number of results. offset: Minimum offset. id: Id (regex). class_: Class. kwargs: Extra arguments to be passed to :func:`print`. See also: :func:`show_extensions`, :func:`show_type_constructors`, :func:`show_constants`, :func:`show_axioms`, :func:`show_definitions`, :func:`show_theorems`, :func:`show_python_type_aliases`. """ sep = kwargs.pop('sep', '\t') for i, ext in self.enumerate_extensions( *args, limit=limit, offset=offset, id=id, class_=class_): print(i, ext, sep=sep, **kwargs)
Theory.push(Theory(load_prelude=False))