diff --git a/punctilious/core.py b/punctilious/core.py index fa01e2ea..245f26ef 100644 --- a/punctilious/core.py +++ b/punctilious/core.py @@ -2522,12 +2522,17 @@ 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.') @@ -2535,19 +2540,20 @@ def __init__(self, nameset=None, universe_of_discourse=None, status=None, scope= '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: @@ -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 @@ -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 @@ -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): @@ -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, ...) @@ -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, @@ -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() diff --git a/tests/test_variable_substitution.py b/tests/test_variable_substitution.py index 40062d70..073b64e0 100644 --- a/tests/test_variable_substitution.py +++ b/tests/test_variable_substitution.py @@ -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): @@ -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))))