using Nemerle.Collections
using Nemerle.Profiling
using Nemerle.Logging

set namespace Fx7

[CreateMemento] \
public class FreeFunTheory : Theory
  internal this (c : Core)
    base (c)

  public override IsFree : bool
    get { true }

  public override IsMyFunction (_head : string) : bool
    // if nobody else wants it ;-)
    true

  public override IsMyPredicate (_head : string) : bool
    true

  public TellEquality (_u1 : BaseVar, _u2 : BaseVar, _proof : Proof) : void
    assert (false)
    //core.TermPool.Merge (u1, u2, proof)

  public override PushState () : void
    SaveMemento ()

  public override PopState () : void
    RestoreMemento ()

  // tell [this] that u1 != u2
  public TellInequality (u1 : Term, u2 : Term, proof : Proof) : void
    unless (core.Refuted)
      u1.ForbidMerge (u2, proof)