using Nemerle.Collections
using Nemerle.Utility
using Nemerle.Logging

set namespace Fx7

public abstract class Theory
  protected core : Core
  protected mutable inside_final_check : bool
  
  public virtual IsFree : bool
    get { false }

  public abstract IsMyFunction (head : string) : bool
  public abstract IsMyPredicate (head : string) : bool

  // Run when the core needs to find out if given constraints in given theory
  // are still valid. Can be run multiple times.
  public FinalCheck () : void
    if (inside_final_check) {}
    else
      inside_final_check = true
      try
        FinalCheckImpl (core.CurrentStrategy >= 2)
      finally
        inside_final_check = false


  public FullFinalCheck () : void
    if (inside_final_check) {}
    else
      inside_final_check = true
      try
        FinalCheckImpl (true)
      finally
        inside_final_check = false
  
  public virtual FinalCheckImpl (_full : bool) : void
    {}

  public virtual Clear () : void
    {}

  public abstract PushState () : void
  public abstract PopState () : void

  protected this (c : Core)
    core = c


public abstract class PlainVarTheory : Theory
  public Id : int
    
  // For linear arithmetic, in a term "g(1 + 2 + f(x))":
  // "f(x)" is inner alien
  // "1 + 2 + f(x)" is outer alien
  // "1 + 2" is not alien at all (unless used elsewhere)
  // The theory is obligated to broadcast any equalities between aliens.
  public abstract MakeAlien (t : Term, outer : bool) : void

  // not for equality, only for theory specific predicates
  public abstract AssertPredicate (neg : bool, head : string, children : list [Term], proof : Proof) : void
  // tell [this] that u1 = u2
  public abstract TellEquality (u1 : Term, u2 : Term, proof : Proof) : void

  protected this (c : Core, i : int)
    base (c)
    Id = i
  
[Record] \
public abstract class BaseVar
  public term : Term