102 lines
3.0 KiB
Python
102 lines
3.0 KiB
Python
"""
|
|
The Context helps handle multiple hypotheses in a given proof context.
|
|
"""
|
|
|
|
from __future__ import annotations
|
|
|
|
from .props import Prop
|
|
from dataclasses import dataclass
|
|
|
|
@dataclass(frozen=True)
|
|
class Context:
|
|
"""
|
|
Base Context that contains multiple assumptions for a given proof.
|
|
"""
|
|
|
|
props : set[Prop]
|
|
|
|
def contains(self, prop : Prop) -> bool:
|
|
"""
|
|
Determine whether a proposition is given in the context.
|
|
|
|
:param prop: The proposition to consider.
|
|
:type prop: Prop
|
|
:return: Whether the proposition is contained in the context.
|
|
:rtype: bool
|
|
"""
|
|
return prop in self.props
|
|
|
|
@classmethod
|
|
def empty(cls):
|
|
return cls(props=set())
|
|
|
|
def isempty(self) -> bool:
|
|
"""
|
|
Determine whether the context is empty.
|
|
"""
|
|
return len(self.props) == 0
|
|
|
|
def issubseteq(self, other : Context) -> bool:
|
|
"""
|
|
Determine whether this context is a subset of another context.
|
|
|
|
:param other: The potentially larger context.
|
|
:type other: Context
|
|
:return: Whether this context is a subset.
|
|
:rtype: bool
|
|
"""
|
|
return self.props.issubset(other.props)
|
|
|
|
def issuperseteq(self, other : Context) -> bool:
|
|
"""
|
|
Determine whether this context has another context as its subset.
|
|
|
|
:param other: The potentially contained context.
|
|
:type other: Context
|
|
:return: Whether the context is a subset of this one.
|
|
:rtype: bool
|
|
"""
|
|
return other.issubseteq(self)
|
|
|
|
def union(self, other : Context) -> Context:
|
|
"""
|
|
Create a context that contains the propositions of two contexts.
|
|
|
|
:param other: The other context.
|
|
:type other: Context
|
|
:return: A context containing the propositions of both contexts.
|
|
:type: Context
|
|
"""
|
|
return Context(props=self.props.union(other.props))
|
|
|
|
def with_prop(self, prop : Prop) -> Context:
|
|
"""
|
|
Add a new proposition to the context.
|
|
|
|
:param prop: Proposition to add.
|
|
:type prop: Prop
|
|
:return: A context with the proposition included.
|
|
:rtype: Context
|
|
"""
|
|
if prop in self.props:
|
|
return self
|
|
else:
|
|
new_props = [ p for p in self.props ]
|
|
new_props.append(prop)
|
|
return Context(props=set(new_props))
|
|
|
|
def without_prop(self, prop : Prop) -> Context:
|
|
"""
|
|
Remove a proposition from the context, if it was present at all.
|
|
|
|
:param prop: Proposition to remove.
|
|
:type prop: Prop
|
|
:return: A context without the proposition.
|
|
:rtype: Context
|
|
"""
|
|
if prop not in self.props:
|
|
return self
|
|
else:
|
|
new_props = [ p for p in self.props if p != prop ]
|
|
return Context(props=set(new_props))
|