From 0734109a07ad740f1d6cc56f1bf8a28b9135b46a Mon Sep 17 00:00:00 2001
From: David Doret <david.doret@me.com>
Date: Tue, 3 Oct 2023 05:53:15 +0200
Subject: [PATCH] documentation #195 + inference validation #126 + support for
 the composition of collection-like formulae + usage of
 sequent-collection-comma to define inference-rules + enhanced exceptions with
 user-friendly reports + #220 interdiction of variable-substitution of
 propositional objects with non-propositional objects.

---
 .idea/workspace.xml     | 22 ++++++------
 src/punctilious/core.py | 75 ++++++++++++++++-------------------------
 2 files changed, 40 insertions(+), 57 deletions(-)

diff --git a/.idea/workspace.xml b/.idea/workspace.xml
index 691bc94e..c7165261 100644
--- a/.idea/workspace.xml
+++ b/.idea/workspace.xml
@@ -392,10 +392,10 @@
     <recent_temporary>
       <list>
         <item itemvalue="Python tests.Python tests in test_biconditional_elimination_1.py" />
+        <item itemvalue="Python tests.Python tests in test_biconditional_elimination_2.py" />
+        <item itemvalue="Python tests.Python tests in test_biconditional_introduction.py" />
         <item itemvalue="Python tests.Python tests in test_absorption.py" />
         <item itemvalue="Python tests.Python tests in test_conjunction_elimination_1.py" />
-        <item itemvalue="Python tests.Python tests in test_biconditional_introduction.py" />
-        <item itemvalue="Python tests.Python tests in test_biconditional_elimination_2.py" />
       </list>
     </recent_temporary>
   </component>
@@ -408,14 +408,6 @@
       <option name="presentableId" value="Default" />
       <updated>1687980987309</updated>
     </task>
-    <task id="LOCAL-00286" summary="#201 + #195">
-      <option name="closed" value="true" />
-      <created>1694895891980</created>
-      <option name="number" value="00286" />
-      <option name="presentableId" value="LOCAL-00286" />
-      <option name="project" value="LOCAL" />
-      <updated>1694895891980</updated>
-    </task>
     <task id="LOCAL-00287" summary="#201 + #195">
       <option name="closed" value="true" />
       <created>1694897599057</created>
@@ -800,7 +792,15 @@
       <option name="project" value="LOCAL" />
       <updated>1696302457345</updated>
     </task>
-    <option name="localTasksCounter" value="335" />
+    <task id="LOCAL-00335" summary="documentation #195 + inference validation #126 + support for the composition of collection-like formulae + usage of sequent-collection-comma to define inference-rules + enhanced exceptions with user-friendly reports + #220 interdiction of variable-substitution of propositional objects with non-propositional objects.">
+      <option name="closed" value="true" />
+      <created>1696304726518</created>
+      <option name="number" value="00335" />
+      <option name="presentableId" value="LOCAL-00335" />
+      <option name="project" value="LOCAL" />
+      <updated>1696304726518</updated>
+    </task>
+    <option name="localTasksCounter" value="336" />
     <servers />
   </component>
   <component name="Vcs.Log.Tabs.Properties">
diff --git a/src/punctilious/core.py b/src/punctilious/core.py
index 7aaae225..0287ea76 100644
--- a/src/punctilious/core.py
+++ b/src/punctilious/core.py
@@ -6789,19 +6789,18 @@ def __init__(self, t: TheoryElaborationSequence, echo: (None, bool) = None,
         super().__init__(t=t, i=i, dashed_name=dashed_name, abridged_name=abridged_name, name=name,
             explicit_name=explicit_name, echo=echo, proof=proof)
 
-    def check_premises_validity(self, p_implies_q: FlexibleFormula,
-            raise_exception: bool = True) -> bool:
+    def check_premises_validity(self, p_implies_q: FlexibleFormula) -> bool:
         """
         .. include:: ../../include/check_premises_validity_python_method.rstinc
 
         """
         error_code: ErrorCode = error_codes.error_003_inference_premise_validity_error
         # Validate that expected formula-statements are formula-statements.
-        formula_ok, _, _ = verify_formula_statement(t=self.t, input_value=p_implies_q,
+        verify_formula_statement(t=self.t, input_value=p_implies_q,
             form=self.i.parameter_p_implies_q, mask=self.i.parameter_p_implies_q_mask,
-            raise_exception=raise_exception, error_code=error_code)
+            raise_exception=True, error_code=error_code)
         # The method either raises an exception during validation, or return True.
-        return formula_ok
+        return True
 
     def compose_paragraph_proof(self, o: InferredStatement) -> collections.abc.Generator[
         Composable, Composable, bool]:
@@ -6852,35 +6851,25 @@ def __init__(self, t: TheoryElaborationSequence, echo: (None, bool) = None,
             abridged_name=abridged_name, name=name, explicit_name=explicit_name, echo=echo,
             proof=proof)
 
-    def check_premises_validity(self, a: AxiomInclusion, p: FlexibleFormula,
-            raise_exception: bool = True) -> tuple[bool, (None, str)]:
+    def check_premises_validity(self, a: AxiomInclusion, p: FlexibleFormula) -> bool:
         """
         .. include:: ../../include/check_premises_validity_python_method.rstinc
 
         """
         error_code: ErrorCode = error_codes.error_003_inference_premise_validity_error
-        ok: bool
-        msg: (None, str)
         # Validate that expected formula-statements are formula-statements.
         # TODO: NICETOHAVE: AxiomInterpretationInclusion: replace these verify statements with a generic validate_axiom_inclusion function.
-        ok, msg = verify(assertion=isinstance(a, AxiomInclusion),
+        verify(assertion=isinstance(a, AxiomInclusion),
             msg=f'⌜{a}⌝ passed as argument ⌜a⌝ is not an axiom-inclusion.', a=a,
-            raise_exception=raise_exception, error_code=error_code)
-        if not ok:
-            return ok, msg
-        ok, msg = verify(assertion=self.t.contains_theoretical_objct(a),
+            raise_exception=True, error_code=error_code)
+        verify(assertion=self.t.contains_theoretical_objct(a),
             msg=f'⌜{a}⌝ passed as argument ⌜a⌝ is not contained in theory-elaboration-sequence ⌜{self.t}⌝.',
-            a=a, raise_exception=raise_exception, error_code=error_code)
-        if not ok:
-            return ok, msg
-        ok, formula, msg = verify_formula(u=self.u, input_value=p, raise_exception=raise_exception,
-            error_code=error_code)
-        if not ok:
-            return ok, msg
+            a=a, raise_exception=True, error_code=error_code)
+        verify_formula(u=self.u, input_value=p, raise_exception=True, error_code=error_code)
         # TODO: BUG: validate_formula does not support basic masks like: ⌜P⌝ where P is a free-variable.
         # validate_formula(u=self.u, input_value=p, form=self.i.parameter_p,
         #    mask=self.i.parameter_p_mask)
-        return True, None
+        return True
 
     def compose_paragraph_proof(self, o: InferredStatement) -> collections.abc.Generator[
         Composable, Composable, bool]:
@@ -6931,19 +6920,17 @@ def __init__(self, t: TheoryElaborationSequence, echo: (None, bool) = None,
             abridged_name=abridged_name, name=name, explicit_name=explicit_name, echo=echo,
             proof=proof)
 
-    def check_premises_validity(self, p_iff_q: FlexibleFormula,
-            raise_exception: bool = True) -> bool:
+    def check_premises_validity(self, p_iff_q: FlexibleFormula) -> bool:
         """
         .. include:: ../../include/check_premises_validity_python_method.rstinc
 
         """
         error_code: ErrorCode = error_codes.error_003_inference_premise_validity_error
         # Validate that expected formula-statements are formula-statements.
-        formula_ok, _, _ = verify_formula_statement(t=self.t, input_value=p_iff_q,
-            form=self.i.parameter_p_iff_q, mask=self.i.parameter_p_iff_q_mask,
-            raise_exception=raise_exception, error_code=error_code)
+        verify_formula_statement(t=self.t, input_value=p_iff_q, form=self.i.parameter_p_iff_q,
+            mask=self.i.parameter_p_iff_q_mask, raise_exception=True, error_code=error_code)
         # The method either raises an exception during validation, or return True.
-        return formula_ok
+        return True
 
     def compose_paragraph_proof(self, o: InferredStatement) -> collections.abc.Generator[
         Composable, Composable, bool]:
@@ -6993,19 +6980,17 @@ def __init__(self, t: TheoryElaborationSequence, echo: (None, bool) = None,
             abridged_name=abridged_name, name=name, explicit_name=explicit_name, echo=echo,
             proof=proof)
 
-    def check_premises_validity(self, p_iff_q: FlexibleFormula,
-            raise_exception: bool = True) -> bool:
+    def check_premises_validity(self, p_iff_q: FlexibleFormula) -> bool:
         """
         .. include:: ../../include/check_premises_validity_python_method.rstinc
 
         """
         error_code: ErrorCode = error_codes.error_003_inference_premise_validity_error
         # Validate that expected formula-statements are formula-statements.
-        formula_ok, _, _ = verify_formula_statement(t=self.t, input_value=p_iff_q,
-            form=self.i.parameter_p_iff_q, mask=self.i.parameter_p_iff_q_mask,
-            raise_exception=raise_exception, error_code=error_code)
+        verify_formula_statement(t=self.t, input_value=p_iff_q, form=self.i.parameter_p_iff_q,
+            mask=self.i.parameter_p_iff_q_mask, raise_exception=True, error_code=error_code)
         # The method either raises an exception during validation, or return True.
-        return formula_ok
+        return True
 
     def compose_paragraph_proof(self, o: InferredStatement) -> collections.abc.Generator[
         Composable, Composable, bool]:
@@ -7055,24 +7040,22 @@ def __init__(self, t: TheoryElaborationSequence, echo: (None, bool) = None,
             abridged_name=abridged_name, name=name, explicit_name=explicit_name, echo=echo,
             proof=proof)
 
-    def check_premises_validity(self, p_implies_q: FlexibleFormula, q_implies_p: FlexibleFormula,
-            raise_exception: bool = True) -> bool:
+    def check_premises_validity(self, p_implies_q: FlexibleFormula,
+            q_implies_p: FlexibleFormula) -> bool:
         """
         .. include:: ../../include/check_premises_validity_python_method.rstinc
 
         """
         error_code: ErrorCode = error_codes.error_003_inference_premise_validity_error
         # Validate that expected formula-statements are formula-statements in the current theory.
-        formula_ok, _, _ = verify_formula_statement(arg='p_implies_q', t=self.t,
-            input_value=p_implies_q, form=self.i.parameter_p_implies_q,
-            mask=self.i.parameter_p_implies_q_mask, raise_exception=raise_exception,
-            error_code=error_code)
-        formula_ok, _, _ = verify_formula_statement(arg='q_implies_p', t=self.t,
-            input_value=q_implies_p, form=self.i.parameter_q_implies_p,
-            mask=self.i.parameter_q_implies_p_mask, raise_exception=raise_exception,
-            error_code=error_code)
+        verify_formula_statement(arg='p_implies_q', t=self.t, input_value=p_implies_q,
+            form=self.i.parameter_p_implies_q, mask=self.i.parameter_p_implies_q_mask,
+            raise_exception=True, error_code=error_code)
+        verify_formula_statement(arg='q_implies_p', t=self.t, input_value=q_implies_p,
+            form=self.i.parameter_q_implies_p, mask=self.i.parameter_q_implies_p_mask,
+            raise_exception=True, error_code=error_code)
         # The method either raises an exception during validation, or return True.
-        return formula_ok
+        return True
 
     def compose_paragraph_proof(self, o: InferredStatement) -> collections.abc.Generator[
         Composable, Composable, bool]:
@@ -9735,7 +9718,7 @@ def __init__(self, i: InferenceRuleInclusion, premises: typing.NamedTuple,
         # Check that the premises are valid.
         # If they are not, raise a Punctilious Exception and stop processing.
         # If they are, complete the inference process.
-        self._inference_rule.check_premises_validity(**premises._asdict(), raise_exception=True)
+        self._inference_rule.check_premises_validity(**premises._asdict())
         super().__init__(theory=t, valid_proposition=valid_proposition, symbol=symbol, index=index,
             auto_index=auto_index, dashed_name=dashed_name, acronym=acronym,
             abridged_name=abridged_name, name=name, explicit_name=explicit_name, ref=ref,