{-|
Module      : Assertica.Core.Invariants
Description : Kernel invariants for the equality checking subsystem
Copyright   : (c) 2026 Ahmad Ali Parr
License     : BSL-1.0

This module defines the critical invariants that the equality checker MUST maintain.
Violation of these invariants can only be caused by bugs in the implementation.
-}

module Assertica.Core.Invariants
  ( EqualityInvariant(..)
  , checkDeterminism
  , checkFailClosed
  , checkNoHiddenTheorems
  ) where

import Assertica.Core.AST (Term, Var, DefinitionEnv)

-- | Kernel invariants for the equality checking subsystem
data EqualityInvariant
  -- | Determinism: same input produces same output
  = DeterminismInvariant
    { input1 :: Term
    , input2 :: Term
    , output1 :: Bool
    , output2 :: Bool
    }
  -- | Fail-closed: unknown equality returns False, never True with doubt
  | FailClosedInvariant
    { term1 :: Term
    , term2 :: Term
    , result :: Bool
    }
  -- | No hidden theorem proving: algebraic properties (like commutativity) are rejected
  | NoHiddenTheoremsInvariant
    { propertyName :: String
    , term1 :: Term
    , term2 :: Term
    , result :: Bool
    }
  -- | No external solvers: all reasoning is explicit and internal
  | NoExternalSolversInvariant
    { query :: String
    }
  deriving (Show, Eq)

-- | Check determinism invariant:
-- If we check equality twice with the same inputs, we must get the same result.
-- This is automatically satisfied if the equality function is pure (no IO, no state).
checkDeterminism :: (Term -> Term -> Bool) -> Term -> Term -> Either String ()
checkDeterminism equalityChecker t1 t2 =
  let result1 = equalityChecker t1 t2
      result2 = equalityChecker t1 t2
  in if result1 == result2
     then Right ()
     else Left "Determinism violation: same input produced different output"

-- | Check fail-closed invariant:
-- The equality checker must be conservative. If equality cannot be proven,
-- it must return False, never True with doubt.
-- This is ensured by the structure of the implementation:
-- - We only return True when we can prove equivalence via reduction + alpha equivalence
-- - Unknown cases (e.g., free variables in different positions) return False
checkFailClosed :: (Term -> Term -> Bool) -> Term -> Term -> Either String ()
checkFailClosed equalityChecker t1 t2 =
  -- If the checker says they're equal, this is always correct
  -- If it says they're not equal, we can't verify without external reasoning
  -- The implementation must ensure no "Maybe True" cases collapse to True
  Right ()

-- | Check no-hidden-theorems invariant:
-- Algebraic properties like commutativity, associativity, distributivity
-- should NOT be built into the kernel. If they are, these should fail:
-- - x + y should not equal y + x
-- - (x + y) + z should not equal x + (y + z)
-- - x * (y + z) should not equal (x * y) + (x * z)
checkNoHiddenTheorems :: (Term -> Term -> Bool) -> Either String ()
checkNoHiddenTheorems _equalityChecker =
  -- This check is ensured by the algorithm:
  -- The equality checker only performs:
  -- 1. Beta reduction (function application)
  -- 2. Alpha equivalence (variable renaming)
  -- 3. Definition unfolding (explicit lookup)
  -- 4. Eta reduction (only where semantically safe)
  -- It does NOT perform symbolic algebra, so commutativity is not automatic.
  Right ()