using Nemerle.Collections
using System.Text
using Nemerle.Profiling

set namespace Fx7

// #define HASHTABLE_GETLITERALS

public variant Proof
  | Leaf
      lit : Literal
      
  | Rule1
      label : string
      p1 : Proof

  | Rule2
      label : string
      p1 : Proof
      p2 : Proof

  | Rule3
      label : string
      p1 : Proof
      p2 : Proof
      p3 : Proof

  | Rule4
      label : string
      p1 : Proof
      p2 : Proof
      p3 : Proof
      p4 : Proof

  | EqProof
      t1 : Term
      t2 : Term

  | Token
      name : string
      id : int

  | True

  #if !HASHTABLE_GETLITERALS
  mutable last_visited : int
  static mutable current_iter : int
  #endif

  public override ToString () : string
    def sb = StringBuilder ()
    def visited = Hashtable ()

    def print (x)
      if (x == null)
        _ = sb.Append ("NIL")
      else if (visited.Contains (x) && !(x is True)) 
        _ = sb.Append ("...")
      else
        visited [x] = x
        match (x)
          | True =>
            _ = sb.Append ("T")

          | Token (name, id) =>
            _ = sb.Append ($"Tok($name,$id)")

          | Leaf (lit) =>
            visited [x] = x
            _ = sb.Append (lit)

          | Rule1 (label, p1) =>
            visited [x] = x
            _ = sb.Append ("(").Append (label).Append (" ")
            print (p1)
            _ = sb.Append (")")

          | Rule2 (label, p1, p2) =>
            visited [x] = x
            _ = sb.Append ("(").Append (label).Append (" ")
            print (p1)
            _ = sb.Append (" ")
            print (p2)
            _ = sb.Append (")")
          
          | Rule3 (label, p1, p2, p3) =>
            visited [x] = x
            _ = sb.Append ("(").Append (label).Append (" ")
            print (p1)
            _ = sb.Append (" ")
            print (p2)
            _ = sb.Append (" ")
            print (p3)
            _ = sb.Append (")")
      
          | Rule4 (label, p1, p2, p3, p4) =>
            visited [x] = x
            _ = sb.Append ("(").Append (label).Append (" ")
            print (p1)
            _ = sb.Append (" ")
            print (p2)
            _ = sb.Append (" ")
            print (p3)
            _ = sb.Append (" ")
            print (p4)
            _ = sb.Append (")")

          | EqProof (t1, t2) =>
            visited [x] = x
            _ = sb.Append ("(EQ ").Append (t1).Append (" == ").Append (t2).Append (")")
      
    print (this)
    sb.ToString ()

  [Profile] \
  public GetLiterals () : list [Literal]
    #if HASHTABLE_GETLITERALS
    def visited = Hashtable ()
    #else
    ++current_iter
    #endif

    def needed = Hashtable ()
    mutable res = []

    def loop (t)
      #if HASHTABLE_GETLITERALS
      unless (visited.Contains (t))
        visited [t] = t
      #else
      unless (t.last_visited == current_iter)
        t.last_visited = current_iter
      #endif
        match (t)
          | Token \
          | True => {}

          | Leaf (l) =>
            unless (needed.Contains (l))
              needed [l] = l
              res ::= l

          | Rule1 (_, p1) =>
            loop (p1)
            
          | Rule2 (_, p1, p2) =>
            loop (p1)
            loop (p2)
            
          | Rule3 (_, p1, p2, p3) =>
            loop (p1)
            loop (p2)
            loop (p3)

          | Rule4 (_, p1, p2, p3, p4) =>
            loop (p1)
            loop (p2)
            loop (p3)
            loop (p4)

          | EqProof (t1, t2) =>
            loop (t1.ProofOfEqualityWith (t2))

    loop (this)
    res

  [Profile] \
  public GetTokens () : list [Token]
    #if HASHTABLE_GETLITERALS
    def visited = Hashtable ()
    #else
    ++current_iter
    #endif

    def needed = Hashtable ()
    mutable res = []

    def loop (t)
      #if HASHTABLE_GETLITERALS
      unless (visited.Contains (t))
        visited [t] = t
      #else
      unless (t.last_visited == current_iter)
        t.last_visited = current_iter
      #endif
        match (t)
          | Token (n, i) as t =>
            unless (needed.Contains ((n, i)))
              needed [(n, i)] = n
              res ::= t

          | Leaf \
          | True => {}

          | Rule1 (_, p1) =>
            loop (p1)
            
          | Rule2 (_, p1, p2) =>
            loop (p1)
            loop (p2)
            
          | Rule3 (_, p1, p2, p3) =>
            loop (p1)
            loop (p2)
            loop (p3)

          | Rule4 (_, p1, p2, p3, p4) =>
            loop (p1)
            loop (p2)
            loop (p3)
            loop (p4)

          | EqProof => {}

    loop (this)
    res