From 9779fd0328c91cf4ddcba5a1f51ed43ae80b8d99 Mon Sep 17 00:00:00 2001
From: Kacper Marzecki <kacper-marzecki@github.com>
Date: Sun, 15 Jun 2025 21:04:57 +0200
Subject: [PATCH] checkpoint failing test

---
 test.exs | 98 +++++++++++++++++++++++++++++---------------------------
 1 file changed, 51 insertions(+), 47 deletions(-)

diff --git a/test.exs b/test.exs
index 77c53ef..a3decc0 100644
--- a/test.exs
+++ b/test.exs
@@ -109,51 +109,56 @@ defmodule Tdd do
     sorted_assumptions_list = Enum.sort_by(assumptions_map, fn {var, _val} -> var end)
     cache_key = {:simplify_constr, tdd_id, sorted_assumptions_list}
 
-    cond do
-      is_terminal_id(tdd_id) ->
+    # Order of checks is critical:
+    # 1. Is the current set of assumptions inherently contradictory? If so, this path is dead.
+    # 2. Is the TDD itself terminal? (Assumptions are consistent at this point)
+    if check_assumptions_consistency(assumptions_map) == :contradiction do
+      # IO.inspect({tdd_id, assumptions_map}, label: "SimplifyContradiction (Early Exit)")
+      # No need to cache here if it's based purely on assumptions,
+      # but if tdd_id was involved, caching the result for {tdd_id, assumptions} is good.
+      # Let's cache it for safety, as tdd_id is part of cache_key.
+      update_state(%{op_cache: Map.put(state.op_cache, cache_key, @false_node_id)})
+      @false_node_id
+    else
+      # 3. Cache lookup
+      if is_terminal_id(tdd_id) do
+        # IO.inspect({tdd_id, assumptions_map}, label: "SimplifyTerminal")
+        # Terminals are not affected by further assumptions if not contradictory
         tdd_id
+      else
+        if Map.has_key?(state.op_cache, cache_key) do
+          # IO.inspect({tdd_id, assumptions_map}, label: "SimplifyFromCache")
+          state.op_cache[cache_key]
+        else
+          # 4. Not contradictory, not terminal, not in cache: Process the node
+          {var, y, n, d} = get_node_details(tdd_id)
+          # IO.inspect({tdd_id, assumptions_map, var}, label: "SimplifyProcessingNode")
+          result_id =
+            case Map.get(assumptions_map, var) do
+              true ->
+                simplify_with_constraints(y, assumptions_map)
 
-      Map.has_key?(state.op_cache, cache_key) ->
-        state.op_cache[cache_key]
+              false ->
+                simplify_with_constraints(n, assumptions_map)
 
-      check_assumptions_consistency(assumptions_map) == :contradiction ->
-        # Path is semantically impossible
-        # Important
-        IO.inspect({tdd_id, assumptions_map}, label: "SimplifyContradiction")
-        update_state(%{op_cache: Map.put(state.op_cache, cache_key, @false_node_id)})
-        @false_node_id
+              :dc ->
+                simplify_with_constraints(d, assumptions_map)
 
-      true ->
-        {var, y, n, d} = get_node_details(tdd_id)
+              nil ->
+                simplified_y = simplify_with_constraints(y, Map.put(assumptions_map, var, true))
+                simplified_n = simplify_with_constraints(n, Map.put(assumptions_map, var, false))
+                simplified_d = simplify_with_constraints(d, Map.put(assumptions_map, var, :dc))
+                make_node_raw(var, simplified_y, simplified_n, simplified_d)
+            end
 
-        result_id =
-          case Map.get(assumptions_map, var) do
-            # Current var is assumed true in path, follow yes branch
-            true ->
-              simplify_with_constraints(y, assumptions_map)
-
-            # Current var is assumed false in path, follow no branch
-            false ->
-              simplify_with_constraints(n, assumptions_map)
-
-            # Current var is assumed don't care in path, follow dc branch
-            :dc ->
-              simplify_with_constraints(d, assumptions_map)
-
-            # Current var is not in assumptions, so it's a decision point.
-            nil ->
-              # Recursively simplify children by adding this var's assignment to assumptions.
-              simplified_y = simplify_with_constraints(y, Map.put(assumptions_map, var, true))
-              simplified_n = simplify_with_constraints(n, Map.put(assumptions_map, var, false))
-              # Assuming :dc can be an assumption value
-              simplified_d = simplify_with_constraints(d, Map.put(assumptions_map, var, :dc))
-              make_node_raw(var, simplified_y, simplified_n, simplified_d)
-          end
-
-        IO.inspect({tdd_id, assumptions_map, result_id}, label: "SimplifyExit")
-        update_state(%{op_cache: Map.put(state.op_cache, cache_key, result_id)})
-        result_id
+          # IO.inspect({tdd_id, assumptions_map, result_id}, label: "SimplifyExitComputed")
+          update_state(%{op_cache: Map.put(state.op_cache, cache_key, result_id)})
+          result_id
+        end
+      end
     end
+
+    # End of nested cond/if
   end
 
   # --- Public Node Creation (Used by Type Constructors) ---
@@ -632,11 +637,10 @@ test_all = fn ->
 
   IO.inspect(Process.get(:test_failures, []))
 end
-
-# Should be tdd_none
-tdd_atom_and_tuple = Tdd.intersect(tdd_atom, tdd_tuple)
-test.("(atom & tuple) <: none", true, Tdd.is_subtype(tdd_atom_and_tuple, tdd_none))
-IO.inspect("tdd_atom_and_tuple")
-Tdd.print_tdd(tdd_atom_and_tuple)
-IO.inspect("tdd_none")
-Tdd.print_tdd(tdd_none)
+# test_all.()
+tdd_atom_minus_foo = Tdd.intersect(tdd_atom, Tdd.negate(tdd_foo))
+test.(":bar <: (atom - :foo)", true, Tdd.is_subtype(tdd_bar, tdd_atom_minus_foo))
+IO.inspect("tdd_atom_minus_foo")
+Tdd.print_tdd(tdd_atom_minus_foo)
+IO.inspect("tdd_bar")
+Tdd.print_tdd(tdd_bar)