Skip to content

Commit

Permalink
reviewing tests + complete method signatures for free-variable declar…
Browse files Browse the repository at this point in the history 
…ations
  • Loading branch information
@daviddoret
daviddoret committed Aug 23, 2023
1 parent ff3bfe5 commit 9fa229f
Show file tree
Hide file tree
Showing 2 changed files with 61 additions and 40 deletions.
63 changes: 39 additions & 24 deletions punctilious/core.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2522,32 +2522,38 @@ class Status(repm.ValueName):
scope_initialization_status = Status('scope_initialization_status')
closed_scope_status = Status('closed_scope_status')

def __init__(self, nameset=None, universe_of_discourse=None, status=None, scope=None,
echo=None):
def __init__(self, u: UniverseOfDiscourse, status: (None, FreeVariable.Status) = None,
scope: (None, Formula, typing.FrozenSet[Formula]) = None,
symbol: (None, str, StyledText) = None, index: (None, int) = None,
auto_index: (None, bool) = None, dashed_name: (None, str, StyledText) = None,
acronym: (None, str, StyledText) = None, abridged_name: (None, str, StyledText) = None,
name: (None, str, StyledText) = None, explicit_name: (None, str, StyledText) = None,
nameset: (None, str, NameSet) = None, echo: (None, bool) = None) -> None:
echo = prioritize_value(echo, configuration.echo_free_variable_declaration,
configuration.echo_default, False)
status = FreeVariable.scope_initialization_status if status is None else status
scope = frozenset() if scope is None else scope
status = prioritize_value(status, FreeVariable.scope_initialization_status)
scope = prioritize_value(scope, frozenset())
scope = {scope} if isinstance(scope, Formula) else scope
verify(isinstance(scope, frozenset),
'The scope of a FreeVariable must be of python type frozenset.')
verify(isinstance(status, FreeVariable.Status),
'The status of a FreeVariable must be of the FreeVariable.Status type.')
self._status = status
self._scope = scope
assert isinstance(universe_of_discourse, UniverseOfDiscourse)
if nameset is None:
assert isinstance(u, UniverseOfDiscourse)
if symbol is None:
symbol = configuration.default_free_variable_symbol
index = universe_of_discourse.index_symbol(symbol=symbol)
nameset = NameSet(symbol=symbol, index=index)
if isinstance(nameset, str):
index = u.index_symbol(symbol=symbol)
if isinstance(symbol, str):
# If symbol was passed as a string,
# assume the base was passed without index.
# TODO: Analyse the string if it ends with index in subscript characters.
symbol = StyledText(plaintext=nameset, text_style=text_styles.serif_bold)
index = universe_of_discourse.index_symbol(symbol=symbol)
nameset = NameSet(symbol=symbol, index=index)
super().__init__(nameset=nameset, universe_of_discourse=universe_of_discourse, echo=False)
symbol = StyledText(plaintext=symbol, text_style=text_styles.serif_bold)
if index is None and auto_index:
index = u.index_symbol(symbol=symbol)
super().__init__(universe_of_discourse=u, symbol=symbol, index=index, auto_index=auto_index,
dashed_name=dashed_name, acronym=acronym, abridged_name=abridged_name, name=name,
explicit_name=explicit_name, nameset=nameset, echo=False)
# self.universe_of_discourse.cross_reference_variable(x=self)
super()._declare_class_membership(declarative_class_list.free_variable)
if echo:
Expand Down Expand Up @@ -7066,7 +7072,7 @@ def variable_substitution(self) -> VariableSubstitutionDeclaration:
return self._variable_substitution

@property
def vs(self) -> InferenceRuleDeclaration:
def vs(self) -> VariableSubstitutionDeclaration:
"""An inference-rule: P ⊢ P'
Abridged property: u.i.vs
Expand Down Expand Up @@ -8478,7 +8484,7 @@ def variable_substitution(self) -> VariableSubstitutionInclusion:
return self._variable_substitution

@property
def vs(self) -> InferenceRuleInclusion:
def vs(self) -> VariableSubstitutionInclusion:

return self.variable_substitution

Expand Down Expand Up @@ -8629,18 +8635,18 @@ def cross_reference_simple_objct(self, o: SimpleObjct):
if o not in self.simple_objcts:
self.simple_objcts[o.nameset] = o

def cross_reference_symbolic_objct(self, o: SymbolicObject):
def cross_reference_symbolic_objct(self, o: TheoreticalObject):
"""Cross-references a symbolic-objct in this universe-of-discourse.
:param o: a symbolic-objct.
"""
verify(is_in_class(o, classes.symbolic_objct),
verify(is_in_class(o=o, c=classes.symbolic_objct),
'Cross-referencing a symbolic-objct in a universe-of-discourse requires '
'an object of type SymbolicObjct.', o=o, slf=self)
duplicate = self.symbolic_objcts.get(o.nameset)
verify(duplicate is None,
'A symbolic-object already exists in the current universe-of-discourse with a '
'duplicate (symbol, index) pair.', o=o, duplicate=duplicate, slf=self)
verify(severity=verification_severities.warning, assertion=duplicate is None,
msg='A symbolic-object already exists in the current universe-of-discourse with a '
'duplicate (symbol, index) pair.', o=o, duplicate=duplicate, slf=self)
self.symbolic_objcts[o.nameset] = o

def cross_reference_theory(self, t: TheoryElaborationSequence):
Expand Down Expand Up @@ -8670,7 +8676,10 @@ def declare_formula(self, relation: Relation, *parameters, nameset: (None, str,
nameset=nameset, lock_variable_scope=lock_variable_scope, echo=echo)
return phi

def declare_free_variable(self, symbol=None, echo=None):
def declare_free_variable(self, symbol: (None, str, StyledText) = None,
dashed_name: (None, str, StyledText) = None, acronym: (None, str, StyledText) = None,
abridged_name: (None, str, StyledText) = None, name: (None, str, StyledText) = None,
explicit_name: (None, str, StyledText) = None, echo: (None, bool) = None):
"""Declare a free-variable in this universe-of-discourse.
A shortcut function for FreeVariable(universe_of_discourse=u, ...)
Expand Down Expand Up @@ -8867,7 +8876,11 @@ def take_note(self, t: TheoryElaborationSequence, content: str,

# @FreeVariableContext()
@contextlib.contextmanager
def v(self, symbol=None, echo=None):
def v(self, symbol: (None, str, StyledText) = None, index: (None, int) = None,
auto_index: (None, bool) = None, dashed_name: (None, str, StyledText) = None,
acronym: (None, str, StyledText) = None, abridged_name: (None, str, StyledText) = None,
name: (None, str, StyledText) = None, explicit_name: (None, str, StyledText) = None,
echo: (None, bool) = None):
"""Declare a free-variable in this universe-of-discourse.
This method is expected to be as in a with statement,
Expand All @@ -8881,8 +8894,10 @@ def v(self, symbol=None, echo=None):
use declare_free_variable() instead.
"""
# return self.declare_free_variable(symbol=symbol)
x = FreeVariable(universe_of_discourse=self, nameset=symbol,
status=FreeVariable.scope_initialization_status, echo=echo)
status = FreeVariable.scope_initialization_status
x = FreeVariable(u=self, status=status, symbol=symbol, index=index, auto_index=auto_index,
dashed_name=dashed_name, acronym=acronym, abridged_name=abridged_name, name=name,
explicit_name=explicit_name, echo=echo)
yield x
x.lock_scope()

Expand Down
38 changes: 22 additions & 16 deletions tests/test_variable_substitution.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,15 +10,17 @@ def test_variable_substitution_without_variable(self):
u = pu.UniverseOfDiscourse()
o1 = u.o.declare()
o2 = u.o.declare()
r1 = u.r.declare(1, signal_proposition=True)
r2 = u.r.declare(2, signal_proposition=True)
r1 = u.r.declare(arity=1, signal_proposition=True)
r2 = u.r.declare(arity=2, signal_proposition=True)
t = u.t()
a = u.declare_axiom(random_data.random_sentence())
ap = t.include_axiom(a)
p_formula = u.f(r1, u.f(r2, o1, o2))
p_statement = t.i.axiom_interpretation.infer_statement(ap, p_formula, echo=True)
a = u.declare_axiom(natural_language=random_data.random_sentence())
ap = t.include_axiom(a=a)
p_formula = r1(r2(o1, o2))
p_statement = t.i.axiom_interpretation.infer_statement(axiom=ap, formula=p_formula,
echo=True)
# y_sequence = tuple()
p_prime = t.i.vs.infer_statement(p_statement, echo=True)
p_prime = t.i.vs.infer_statement(p=p_statement, phi=(), echo=True)
self.assertTrue(p_prime.is_formula_syntactically_equivalent_to(p_statement))
self.assertEqual('𝑟₁(𝑟₂(𝑜₁, 𝑜₂))', p_prime.rep_formula(encoding=pu.encodings.unicode))

def test_variable_substitution_with_free_variables(self):
Expand All @@ -30,14 +32,18 @@ def test_variable_substitution_with_free_variables(self):
o4 = u.o.declare()
o5 = u.o.declare()
o6 = u.o.declare()
r1 = u.r.declare(1, signal_proposition=True)
r2 = u.r.declare(2, signal_proposition=True)
t = u.t('test_variable_substitution_with_free_variables')
f = u.r.declare(arity=1, signal_proposition=True, symbol='f', auto_index=False)
g = u.r.declare(arity=2, signal_proposition=True, symbol='g', auto_index=False)
t = u.t()
a = u.declare_axiom(random_data.random_sentence())
ap = t.include_axiom(a)
with u.v() as x, u.v() as y, u.v() as z:
p_formula = u.f(r1, u.f(r2, u.f(r2, z, u.f(r2, u.f(r1, x), y)), u.f(r2, x, y)))
p_statement = t.i.axiom_interpretation.infer_statement(ap, p_formula, echo=True)
y_sequence = (o4, o6, o5) # sequence: (z, x, y)
p_prime = t.i.vs.infer_statement(p_statement, *y_sequence, echo=True)
self.assertEqual('◆₁(◆₂(◆₂(ℴ₄, ◆₂(◆₁(ℴ₆), ℴ₅)), ◆₂(ℴ₆, ℴ₅)))', p_prime.rep_formula())
with u.v(symbol='x', auto_index=False) as x, u.v(symbol='y', auto_index=False) as y, u.v(
symbol='z', auto_index=False) as z:
p_statement = t.i.axiom_interpretation.infer_statement(axiom=ap,
formula=f(g(g(z, g(f(x), y)), g(x, y))), echo=True)
self.assertEqual('𝑓(𝑔(𝑔(𝐳, 𝑔(𝑓(𝐱), 𝐲)), 𝑔(𝐱, 𝐲)))',
p_statement.rep_formula(encoding=pu.encodings.unicode))
p_prime = t.i.vs.infer_statement(p=p_statement, phi=(o4, o6, o5), echo=True)
self.assertEqual('𝑓(𝑔(𝑔(𝑜₄, 𝑔(𝑓(𝑜₆), 𝑜₅)), 𝑔(𝑜₆, 𝑜₅)))',
p_prime.rep_formula(encoding=pu.encodings.unicode))
p_prime.is_formula_syntactically_equivalent_to(o2=f(g(g(o4, g(f(o6), o5)), g(o6, o5))))

0 comments on commit 9fa229f

Please sign in to comment.