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

set namespace Fx7

// TODO: make this handle several relations at once

[CreateMemento] \
public class TcTheory : PlainVarTheory
  #region nested classes
  [Rollbackable] \
  public class Var : BaseVar
    pool : TcTheory

    // a triple (v1, v2, p) represents v1 <: v2 by p
    // next = [(v1, v2, p) | v1.Root = this ]
    // prev = [(v1, v2, p) | v2.Root = this ]
    [Copy] internal mutable next : list [Var * Var * Proof]
    [Copy] internal mutable prev : list [Var * Var * Proof]
    [Copy] internal mutable repr : Var

    internal Root : Var
      get
        when (repr.repr : object != repr)
          WillWrite ()
          repr = repr.Root
        repr

    internal IsCanon : bool
      get
        repr : object == this

    internal HasNext (v : Var) : bool
      def v = v.Root
      foreach ((_, v', _) in Root.next)
        when (v : object == v'.Root)
          log (TC, $"true: $this <: $v")
          return (true)
      log (TC, $"false: $this <: $v")
      false

    internal NextProof (v : Var) : Proof
      def vr = v.Root
      foreach ((v1, v2, p) in Root.next)
        when (vr : object == v2.Root)
          return (Proof.Rule3 ("tc-1", 
                        Proof.EqProof (term, v1.term),
                        Proof.EqProof (v2.term, v.term),
                        p))
      null

    internal Merge (other : Var) : void
      assert (other : object != this)
      assert (IsCanon && other.IsCanon)
      WillWrite ()
      other.WillWrite ()
      next += other.next
      prev += other.prev
      other.next = null
      other.prev = null
      other.repr = this

    internal this (p : TcTheory, t : Term)
      base (t)
      assert (t != null)
      pool = p
      repr = this
      next = [(this, this, Proof.True ())]
      prev = next
      // log (CNT, $"create for id=$(t.Id) $t")

    public override ToString () : string
      def id = if (term == null) 0 else term.Id
      $ "tc$id:$term"
  #endregion

  #region Rollback handling
  internal mutable current_level : int = 0
  [Copy] mutable rollback_queue : list [Var] = []

  public override PushState () : void
    current_level++
    SaveMemento ()
    rollback_queue = []
    
  public override PopState () : void
    current_level--
    foreach (r in rollback_queue)
      r.Rollback ()
    RestoreMemento ()

  QueueRollback (t : Var) : void
    rollback_queue ::= t
  #endregion
    
  subtyping_symbol : string
    get
      core.SubtypingSymbol

  internal this (i : int, c : Core)
    base (c, i)

  public override IsMyFunction (_head : string) : bool
    false

  public override IsMyPredicate (head : string) : bool
    head == subtyping_symbol

  public override MakeAlien (t : Term, _outer : bool) : void
    _ = GetVar (t)

  vars : Hashtable [Term, Var] = Hashtable ()
  GetVar (t : Term) : Var
    mutable v
    if (vars.TryGetValue (t, out v))
      v
    else
      v = Var (this, t)
      vars [t] = v
      v

  AssertSubtyping (neg : bool, u1 : Var, u2 : Var, proof : Proof) : void
    log (TC, $"$u1 <: $u2 (neg = $neg)")
    unless (core.Refuted)
      def t1 = u1.term
      def t2 = u2.term
      def t = core.TermPool.Get (subtyping_symbol, [t1, t2])
      t.MakeActive ()
      if (neg)
        t1.ForbidMerge (t2, proof)
        t.ForbidMerge (core.TermPool.True, proof)
      else
        core.TermPool.Merge (t, core.TermPool.True, proof)
        def r1 = u1.Root
        def r2 = u2.Root
        r1.WillWrite ()
        r2.WillWrite ()
        r1.next ::= (u1, u2, proof)
        r2.prev ::= (u1, u2, proof)
        
        def p = u2.NextProof (u1)
        when (p != null)
          log (TC, $ "induce merge: $(t1) = $(t2)")
          core.TermPool.Merge (t1, t2, Proof.Rule2 ("tc-cycle", p, proof))

        foreach ((v1, v2, p) in r1.prev)
          unless (v1.HasNext (u2))
            AssertSubtyping (false, v1, u2, 
                  Proof.Rule3 ("tc-comp-1", p, proof, EqProof (v2, u1)))
        
        foreach ((v1, v2, p) in r2.next)
          unless (u1.HasNext (v2))
            AssertSubtyping (false, u1, v2, 
                  Proof.Rule3 ("tc-comp-2", p, proof, EqProof (v1, u2)))

  [Profile] \
  public override AssertPredicate (neg : bool, head : string, children : list [Term], proof : Proof) : void
    assert (head == subtyping_symbol)
    log (TC, $ "assert (neg=$neg, $head $children)")

    match (children)
      | [t1, t2] =>
        def u1 = GetVar (t1)
        def u2 = GetVar (t2)
        when (neg || !u1.HasNext (u2))
          AssertSubtyping (neg, u1, u2, proof)
      | _ => assert (false)

  EqProof (u1 : Var, u2 : Var) : Proof
    Proof.EqProof (u1.term, u2.term)

  [Profile] \
  public override TellEquality (u1 : Term, u2 : Term, _proof : Proof) : void
    log (TC, $ "telleq $u1 = $u2")
    def u1 = GetVar (u1).Root
    def u2 = GetVar (u2).Root

    def u1next = u1.next
    def u1prev = u1.prev
    def u2next = u2.next
    def u2prev = u2.prev

    u1.Merge (u2)

    foreach ((v1, w1, p1) in u1next)
      foreach ((v2, w2, p2) in u2prev)
        // v1 = u1, w2 = u2
        if (w1.Root : object == v2.Root && w1.Root : object != u1.Root)
          log (TC, $ "induce merge 1: $(u1) = $(v2)")
          core.TermPool.Merge (u1.term, v2.term, Proof.Rule4 ("tc-cycle-1", p1, p2, 
                        EqProof (v1, w2), EqProof (w1, v2)))
        else if (!v2.HasNext (w1))
          AssertSubtyping (false, v2, w1, Proof.Rule3 ("tc-eq-1", p1, p2, EqProof (v1, w2)))
        else {}
        
    foreach ((v1, w1, p1) in u1prev)
      foreach ((v2, w2, p2) in u2next)
        // w1 = u1, v2 = u2
        if (v1.Root : object == w2.Root && v1.Root : object != u1.Root)
          log (TC, $ "induce merge 2: $(u1) = $(w2)")
          core.TermPool.Merge (u1.term, w2.term, Proof.Rule4 ("tc-cycle-2", p1, p2, 
                        EqProof (v1, w2), EqProof (w1, v2)))
        else if (!v1.HasNext (w2))
          AssertSubtyping (false, v1, w2, Proof.Rule3 ("tc-eq-2", p1, p2, EqProof (w1, v2)))
        else {}