using Nemerle.Logging
using Nemerle.Utility

set namespace Fx7

public class Atom
  public term1 : Term
  public term2 : Term

  public PosLit : Literal
  public NegLit : Literal

  public mutable MinDepth : int = int.MaxValue

  public this (t1 : Term, t2 : Term)
    #if DETERMINISTIC
    if (t2 == null || Driver.ProofLogging || t1.LexiCmp (t2) <= 0)
    #else
    if (t2 == null || Driver.ProofLogging || t1.Id < t2.Id)
    #endif
      term1 = t1
      term2 = t2
    else
      term1 = t2
      term2 = t1
    //assert (t1.Name != "and" && (t2 == null || t2.Name != "and"))

    def pool = t1.Core.LiteralPool
    PosLit = Literal (pool, this, false)
    NegLit = Literal (pool, this, true)
  

  public GetLiteral (is_neg : bool) : Literal
    if (is_neg) NegLit else PosLit

  public IsQuantified : bool
    get
      term2 == null && term1.Name == "forall"

  public Iter (f : Term -> void) : void
    term1.Iter (f)
    when (term2 != null)
      term2.Iter (f)

  public override GetHashCode () : int
    unchecked
      term1.GetHashCode () ^ 
        if (term2 == null) 12397 else term2.GetHashCode () << 13
    
  [Nemerle.OverrideObjectEquals] \
  public Equals (that : Atom) : bool
    term1 : object == that.term1 && term2 : object == that.term2

  public override ToString () : string
    if (term2 == null) // || term2.Name == "$@true")
      term1.ToString ()
    else
      $ "(= $term1 $term2)"
      
  public ToSimplString () : string
    if (term2 == null)
      term1.ToSimplString (true)
    else
      $ "(EQ $(term1.ToSimplString(false)) $(term2.ToSimplString(false)))"
      
  public ToTerm (c : Core = null) : Term
    def c = if (c == null) term1.Core else c
    if (term2 == null) term1
    else c.TermPool.Get ("=", [term1, term2])

  public Score : double
    get
      PosLit.Score + NegLit.Score