From ef0ffd2f0849597a31467337fde353b96b260dda Mon Sep 17 00:00:00 2001
From: Kacper Marzecki <kacper-marzecki@github.com>
Date: Sun, 15 Jun 2025 21:44:33 +0200
Subject: [PATCH] checkpoint

---
 test.exs | 47 +++++++++++++++++++++++++++++++----------------
 1 file changed, 31 insertions(+), 16 deletions(-)

diff --git a/test.exs b/test.exs
index a3decc0..2296cdf 100644
--- a/test.exs
+++ b/test.exs
@@ -83,23 +83,43 @@ defmodule Tdd do
   # --- Semantic Constraint Checking ---
   # assumptions_map is {variable_id => value (true, false, :dc)}
   defp check_assumptions_consistency(assumptions_map) do
+    # Check 1: Primary type mutual exclusivity
     primary_true_predicates =
       Enum.reduce(assumptions_map, MapSet.new(), fn
         {{0, predicate_name}, true}, acc_set -> MapSet.put(acc_set, predicate_name)
         _otherwise, acc_set -> acc_set
       end)
 
-    IO.inspect({assumptions_map, primary_true_predicates, MapSet.size(primary_true_predicates)},
-      label: "CheckConsistency"
-    )
-
     if MapSet.size(primary_true_predicates) > 1 do
+      # IO.inspect(assumptions_map, label: "Contradiction: Primary Types")
       :contradiction
     else
-      # TODO: Add more semantic checks here, e.g.:
-      # - {v_int_lt_N, true} and {v_int_gt_M, true} where N <= M.
-      # - {v_tuple_size_eq_2, true} and {v_tuple_size_eq_3, true}.
-      :consistent
+      # Check 2: Specific atom value conflicts, e.g. {1, :value, :foo} == true AND {1, :value, :bar} == true
+      atom_value_trues =
+        Enum.reduce(assumptions_map, MapSet.new(), fn
+          {{1, :value, atom_val}, true}, acc_set -> MapSet.put(acc_set, atom_val)
+          _otherwise, acc_set -> acc_set
+        end)
+
+      if MapSet.size(atom_value_trues) > 1 do
+        # IO.inspect(assumptions_map, label: "Contradiction: Atom Values")
+        :contradiction
+      else
+        # Check 3: Tuple size conflicts, e.g. {4, :size, 2} == true AND {4, :size, 3} == true
+        tuple_size_trues =
+          Enum.reduce(assumptions_map, MapSet.new(), fn
+            {{4, :size, size_val}, true}, acc_set -> MapSet.put(acc_set, size_val)
+            _otherwise, acc_set -> acc_set
+          end)
+
+        if MapSet.size(tuple_size_trues) > 1 do
+          # IO.inspect(assumptions_map, label: "Contradiction: Tuple Sizes")
+          :contradiction
+        else
+          # Add more checks as new variable types are introduced
+          :consistent
+        end
+      end
     end
   end
 
@@ -584,7 +604,7 @@ test_all = fn ->
   test.("(atom - :foo) <: atom", true, Tdd.is_subtype(tdd_atom_minus_foo, tdd_atom))
   test.("(atom - :foo) <: :foo", false, Tdd.is_subtype(tdd_atom_minus_foo, tdd_foo))
   # True if :bar is in (atom - :foo)
-  test.("(atom - :foo) <: :bar", true, Tdd.is_subtype(tdd_atom_minus_foo, tdd_bar))
+  test.("(atom - :foo) <: :bar", false, Tdd.is_subtype(tdd_atom_minus_foo, tdd_bar))
   test.(":bar <: (atom - :foo)", true, Tdd.is_subtype(tdd_bar, tdd_atom_minus_foo))
 
   # (atom - :foo) | :foo should be atom
@@ -637,10 +657,5 @@ test_all = fn ->
 
   IO.inspect(Process.get(:test_failures, []))
 end
-# 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)
+
+test_all.()