erro/test_composition_to_application.py at main · FruitfulApproach/erro · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
"""
Test CompositionToApplicationProofStep functionality.
Tests converting (c∘b)da to cbda when both forms exist.
"""

import sys
sys.path.append('.')

from PyQt6.QtCore import QPointF
from PyQt6.QtWidgets import QApplication
from widget.object_node import Object
from widget.diagram_scene import DiagramScene
from core.proof_step import CompositionToApplicationProofStep

def test_composition_to_application():
    print("Testing CompositionToApplicationProofStep:")
    print("=" * 50)

    # Create QApplication instance
    app = QApplication.instance() or QApplication(sys.argv)

    # Create scene
    scene = DiagramScene()

    # Test Case 1: Node with both (c∘b)da and cbda elements
    print("\nTest Case 1: Node with both (c∘b)da and cbda")
    print("-" * 50)

    # Create a node with both composition and application forms
    node1 = Object(text="(c∘b)da, cbda:X")
    node1.setPos(QPointF(0, 0))
    scene.addItem(node1)

    print(f"Before: {node1.get_display_text()}")

    # Test if proof step is applicable
    is_applicable = CompositionToApplicationProofStep.is_applicable([node1], [])
    print(f"Is applicable: {is_applicable}")

    if is_applicable:
        # Apply the proof step
        proof_step = CompositionToApplicationProofStep(scene, [node1], [])
        proof_step.apply()

        print(f"After: {node1.get_display_text()}")
        print(f"Expected: '(c∘b)da=cbda:X'")
        print(f"Match: {node1.get_display_text() == '(c∘b)da=cbda:X'}")

        # Test undo
        proof_step.unapply()
        print(f"After undo: {node1.get_display_text()}")

    # Test Case 2: Node with complex composition
    print("\nTest Case 2: Node with complex composition (g∘h∘k)ab and ghkab")
    print("-" * 50)

    node2 = Object(text="(g∘h∘k)ab, ghkab, other:Y")
    node2.setPos(QPointF(100, 0))
    scene.addItem(node2)

    print(f"Before: {node2.get_display_text()}")

    is_applicable = CompositionToApplicationProofStep.is_applicable([node2], [])
    print(f"Is applicable: {is_applicable}")

    if is_applicable:
        proof_step = CompositionToApplicationProofStep(scene, [node2], [])
        proof_step.apply()

        print(f"After: {node2.get_display_text()}")
        expected = "(g∘h∘k)ab=ghkab, other:Y"
        print(f"Expected: '{expected}'")
        # Note: order might vary, so just check that both elements are converted to equality
        result_text = node2.get_display_text()
        has_equality = "=" in result_text and "(g∘h∘k)ab" in result_text and "ghkab" in result_text
        print(f"Contains expected equality: {has_equality}")

    # Test Case 3: Node with only composition (no matching application)
    print("\nTest Case 3: Node with only composition (no match)")
    print("-" * 50)

    node3 = Object(text="(f∘g)x, other:Z")
    node3.setPos(QPointF(200, 0))
    scene.addItem(node3)

    print(f"Before: {node3.get_display_text()}")

    is_applicable = CompositionToApplicationProofStep.is_applicable([node3], [])
    print(f"Is applicable: {is_applicable}")
    print("Should be False since no matching flattened form exists")

    # Test Case 4: Node with nested compositions
    print("\nTest Case 4: Node with nested composition ((a∘b)∘c)d and abcd")
    print("-" * 50)

    node4 = Object(text="((a∘b)∘c)d, abcd:W")
    node4.setPos(QPointF(300, 0))
    scene.addItem(node4)

    print(f"Before: {node4.get_display_text()}")

    is_applicable = CompositionToApplicationProofStep.is_applicable([node4], [])
    print(f"Is applicable: {is_applicable}")

    if is_applicable:
        proof_step = CompositionToApplicationProofStep(scene, [node4], [])
        proof_step.apply()

        print(f"After: {node4.get_display_text()}")
        # The flattening should remove all ∘ symbols
        has_equality = "=" in node4.get_display_text()
        print(f"Creates equality: {has_equality}")

    print("\n" + "=" * 50)
    print("Test completed!")

if __name__ == "__main__":
    test_composition_to_application()