using System.Text

using SCG = System.Collections.Generic

using Nemerle.Utility
using Nemerle.Logging
using Nemerle.Collections
using Nemerle.Imperative
using Nemerle.Profiling
using Nemerle.Assertions
using Nemerle

// #define DETERMINISTIC

set namespace Fx7

public type Subst = IntTree [Term]

[Rollbackable] \
[ExtensionPattern (E (name, children) = Term where (Name = name, Children = children))] \
[ExtensionPattern (V (name) = Term where (Name = name, Arity = 0))] \
public partial class Term : System.IComparable [Term], System.IEquatable [Term]
  type E = ProofGen.E

  public Id : int
  
  left : Term
  right : Term
  [Accessor] depth : int

  pool : Pool

  // true if the current term doesn't have itself listed as a parent of its children
  mutable skip_parents : bool

  mutable parents : list [Term]
  [Copy] mutable proof_parent : Term
  [Copy] mutable proof : Proof // proof that proof_parent is what it is

  [Copy] public mutable Root : Term
  [Copy] mutable eqc_next : Term

  [Accessor] [Copy] mutable active : bool

  [Copy] mutable forbidden_merges : list [Term * Term * Proof] = []
  [Copy] mutable distinct_mask : ulong
  [Copy] internal mutable Alienated : bool

  // The last time any subterm of this term (including itself) was involved in 
  // a merge or the term was activated.
  //
  // Time is given as value of pool.MatchHeight
  [Copy] mutable last_merge : int

  mutable stats : StatsRec

  internal Stats : StatsRec
    get
      when (stats == null)
        stats = StatsRec (this)
      stats

  #pragma warning disable 649
  internal class StatsRec
    internal mutable instantiations : int
    internal mutable usable_instantiations : int
    internal mutable iters_account : float
    or_depth : int

    internal Dump (p : Term) : void
      when (iters_account > 0)
        def s = string.Format ("{0:0.00}", iters_account)
        System.Console.WriteLine ($ "TA:\t$instantiations\t$usable_instantiations" 
                                    "\t$or_depth\t$s\t$p")
   
    internal this (p : Term)
      def ordepth (rev, t)
        match (t.Name)
          | "and" when rev \
          | "or" when !rev =>
            t.Children.FoldLeft (0, fun (t, acc) { acc + ordepth (rev, t) })
          | "and" | "or" =>
            t.Children.FoldLeft (1, fun (t, acc) { acc * ordepth (rev, t) })
          | "not" => ordepth (!rev, t.OnlyChild)
          | _ => 1
      or_depth = ordepth (false, p.Children.Last)
  #pragma warning restore 649

  #region Theory dispatch
  // the real term that can use this var
  [Copy] internal mutable var0 : Term
  [Copy] internal mutable var1 : Term
  [Copy] internal mutable var2 : Term

  internal Var [idx : int] : Term
    get
      if (idx == 0) var0
      else if (idx == 1) var1
      else if (idx == 2) var2
      else assert (false)

  internal SetVar (idx : int, reason : Term) : void
    WillWrite ()
    if (idx == 0) var0 = reason
    else if (idx == 1) var1 = reason
    else if (idx == 2) var2 = reason
    else assert (false)
  #endregion

  SetNoSkip () : void
    if (!skip_parents || left == null) {}
    else
      skip_parents = false
      pool.core.TheDriver.num_noskips++
      left.WillWrite ()
      left.parents ::= this
      right.WillWrite ()
      right.parents ::= this
      left.SetNoSkip ()
      right.SetNoSkip ()


  private this (p : Pool, id : int, left : Term, right : Term, skip_parents : bool)
    this.pool = p
    this.Id = id
    this.left = left
    this.right = right
    this.skip_parents = skip_parents

    // either both or none
    assert ((left == null) == (right == null))
    // negative id -> we're APPLY
    assert ((id > 0) == (left == null))

    if (left == null)
      if (p.name_by_id [Id].ForAll (char.IsDigit))
        depth = 0
      else
        depth = 1
    else if (left.depth > right.depth)
      depth = left.depth + 1
    else
      depth = right.depth + 1

    log (VTERM, $ "create term $Name $id l=$left r=$right $(skip_parents)")

    when (left != null && !skip_parents)
      left.WillWrite ()
      left.parents ::= this
      right.WillWrite ()
      right.parents ::= this
      when (left.skip_parents || right.skip_parents) 
        //log (WARN, $"set no skip: $(left.skip_parents) $(right.skip_parents) $(ToString())")
        left.SetNoSkip ()
        right.SetNoSkip ()

    parents = []
    
    Root = this
    eqc_next = this

    proof_parent = null
    proof = Proof.True ()

  static limit = 100
  PrintLength (limit : int) : int
    if (limit < 0) 10000
    else
      FoldIndexedChildren (2 + Name.Length, (_, c, len) =>
        len + c.PrintLength (limit - len))

  IPrint (sb : StringBuilder, ind : int) : void
    if (ind < 0) Print (sb, false)
    else
      _ = sb.Append (string (' ', ind))
      if (Arity == 0) _ = sb.Append (Name).Append ('\n')
      else if (PrintLength (limit - ind) < limit - ind)
        Print (sb, false)
        _ = sb.Append ('\n')
      else
        _ = sb.Append ('(').Append (Name).Append ('\n')
        IterChildren (c => c.IPrint (sb, ind + 1))
        _ = sb.Remove (sb.Length - 1, 1).Append (")\n") // replace last \n with )\n
        

  Print (sb : StringBuilder, exact : bool) : void
    if (exact)
      if (left == null)
        _ = sb.Append (pool.name_by_id [Id])
      else
        _ = sb.Append ('(')
        left.Print (sb, exact)
        _ = sb.Append (' ')
        right.Print (sb, exact)
        _ = sb.Append (')')
    else
      //_ = sb.Append (Id).Append ("/")
      if (left != null && left.Id < 0)
        _ = sb.Append ('{')
        left.Print (sb, exact)
        _ = sb.Append (' ')
        right.Print (sb, exact)
        _ = sb.Append ('}')
      else if (Arity == 0) _ = sb.Append (Name)
      else
        _ = sb.Append ('(').Append (Name)
        IterChildren (fun (c) {
          _ = sb.Append (' ');
          c.Print (sb, exact)
        })
        _ = sb.Append (')')
      

  SPrint (sb : StringBuilder, pred : bool) : void
    def add (n)
      | "<" | ">" | "<=" | ">=" => _ = sb.Append (n)
      | _ =>
        if (n.StartsWith ("|") || n.ForAll (char.IsLetterOrDigit))
          _ = sb.Append (n)
        else
          _ = sb.Append ('|').Append (n).Append ('|')

    if (Arity == 0)
      def n =
        match (Name)
          | "$@true" | "Smt.true" => "@true"
          | "$@false" | "Smt.false" => "@false"
          | t => t
      match (Name)
        | "true" when pred => _ = sb.Append ("TRUE")
        | "false" when pred => _ = sb.Append ("FALSE")
        | _ =>
          if (pred)
            _ = sb.Append ("(EQ |@true| ")
            add (n)
            _ = sb.Append (")")
          else
            add (n)
    else
      def normal (name, pred = false)
        _ = sb.Append ('(')
        add (name)
        IterChildren (fun (c) {
          _ = sb.Append (' ');
          c.SPrint (sb, pred)
        })
        _ = sb.Append (')')

      match (Name)
        | "not" when (OnlyChild.Name == "=") =>
          _ = sb.Append ("(NEQ ")
          OnlyChild.Child_1of2.SPrint (sb, false)
          _ = sb.Append (" ")
          OnlyChild.Child_2of2.SPrint (sb, false)
          _ = sb.Append (")")
        | "not" when !pred =>
          _ = sb.Append ("(NEQ |@true| ")
          OnlyChild.SPrint (sb, false)
          _ = sb.Append (")")
        | "not" | "and" | "or" =>
          normal (Name.ToUpper (), pred = true)
        | "distinct" =>
          normal (Name.ToUpper ())
        | "=" => normal ("EQ")
        | "-" when Arity == 1 \
        | "~" when Arity == 1 => 
          _ = sb.Append ("(- 0 ")
          OnlyChild.SPrint (sb, pred = false)
          _ = sb.Append (')')
        | "forall" | "exists" =>
          _ = sb.Append ('(').Append (Name.ToUpper ()).Append (" (")
          match (Children) 
            | [vars, pats, form] \
            | [vars, form] with pats = null =>
              foreach (v in vars.Children)
                _ = sb.Append (' ')
                v.SPrint (sb, false)
              _ = sb.Append (')')
              when (pats != null)
                _ = sb.Append (' ')
                pats.SPrint (sb, false)
              _ = sb.Append (' ')
              form.SPrint (sb, true)
              _ = sb.Append (')')
            | _ => assert (false)
        | "<" | ">" | "<=" | ">=" => normal (Name)
        | n => 
          if (pred)
            _ = sb.Append ("(EQ |@true| ")
            normal (n)
            _ = sb.Append (")")
          else
            normal (n)
      

  public Core : Core
    get
      pool.core

  public Name : string
    get
      if (left == null)
        pool.name_by_id [Id]
      else if (left.left == null)
        pool.name_by_id [left.Id]
      else
        "$@apply"

  public NameDesc : int
    get
      if (left == null)
        Id
      else if (left.left == null)
        left.Id
      else
        assert (false)


  public Children : list [Term]
    [Memoize (InvalidValue = null)] \
    get
      //log (TEMP, $"get_Children: $Name/$Arity [$this] [$left] [$right]")
      def loop (t, n)
        if (n == 1)
          assert (t != null, $ "bad struct: $Name/$Arity")
          [t]
        else t.left :: loop (t.right, n - 1)
      if (left == null) []
      else
        loop (right, Arity)


  public SimplerThan (other : Term) : bool
    if (this.depth < other.depth) true
    else if (this.depth == other.depth && Id < other.Id) true
    else false

  public SameAs (other : Term) : bool
    Root : object == other.Root

  public IsCanon : bool
    get
      Root : object == this

  public IsStar : bool
    get
      this == pool.Star : object

  public ToExactString () : string
    def sb = StringBuilder ()
    Print (sb, true)
    sb.ToString ()

  public override ToString () : string
    def sb = StringBuilder ()
    Print (sb, false)
    sb.ToString ()

  public ToSimplString (pred : bool) : string
    def sb = StringBuilder ()
    SPrint (sb, pred)
    sb.ToString ()

  public ToPrettyString () : string
    def sb = StringBuilder ()
    IPrint (sb, 0)
    sb.ToString ()

  public IsVar : bool
    get { !IsInterpreted && left == null }

  public IsInterpreted : bool
    get { false }

  public MakeActive () : void
    def activate (t)
      unless (t.active)
        when (t.left != null)
          activate (t.left)
          activate (t.right)
        //log (TEMP, $ "activate @$(pool.MatchHeight): $t")
        log (VTERM, $ "activate @$(pool.MatchHeight): $t")
        t.WillWrite ()
        assert (!t.active && t.IsCanon, $"act=$(t.active) can=$(t.Root)/$t")
        t.active = true
        t.last_merge = pool.MatchHeight
        when (Driver.FnLastMerge)
          t.UpdateFnLastMerge ()
        when (t.left != null)
          match (pool.CheckSigHit (t))
            | Some ((t', proof)) => pool.Merge (t, t', proof)
            | None => {}
    activate (this)

  [Profile] \
  UpdateFnLastMerge () : void
    log (VTERM, $"update fn last merge: $(pool.MatchHeight) $(ToExactString())")
    when (left != null && 
          left.last_merge != pool.MatchHeight && 
          left.left == null && 
          left.Id > 0 && 
          pool.arity_by_id [left.Id] > 0)
      log (VTERM, $"do it update fn last merge: $(pool.MatchHeight) $(ToExactString())")
      left.WillWrite ()
      left.last_merge = pool.MatchHeight

  public Arity : int
    get
      if (left == null)
        pool.arity_by_id [Id]
      else
        pool.arity_by_id [left.Id]

  public IsReal : bool
    get
      if (left == null)
        pool.arity_by_id [Id] == 0
      else
        left.Id >= 0 && pool.arity_by_id [left.Id] > 0
        
  public OnlyChild : Term
    get
      assert (Arity == 1 && right != null)
      right

  public Child_1of2 : Term
    get
      assert (Arity == 2 && right.left != null)
      right.left

  public Child_2of2 : Term
    get
      assert (Arity == 2 && right.right != null)
      right.right

  public SigEqualTo (other : Term) : bool
    //SameAs (other)
    if (left == null || other.left == null) false 
    else left : object == other.left && right.Root : object == other.right.Root

  public ProofOfSigEqualityWith (other : Term) : Proof
    right.ProofOfEqualityWith (other.right)
    //ProofOfEqualityWith (other)

  public Iter (f : Term -> void) : void
    def loop (t, n)
      if (n == 1) t.Iter (f)
      else
        t.left.Iter (f)
        loop (t.right, n - 1)

    f (this)
    unless (left == null)
      loop (right, Arity)

  public FoldIndexedChildren['a] (ini : 'a, f : int * Term * 'a -> 'a) : 'a
    def arity = Arity
    def loop (n, t, acc)
      if (n == arity - 1)
        f (n, t, acc)
      else
        loop (n + 1, t.right, f (n, t.left, acc))

    if (arity == 0) ini
    else loop (0, right, ini)

  public IterChildren (f : Term -> void) : void
    def loop (t, n)
      if (n == 1) f (t)
      else
        f (t.left)
        loop (t.right, n - 1)

    unless (left == null)
      loop (right, Arity)

  public MapChildren (f : Term -> Term) : Term
    def skip_parents = pool.IsParentSkipping (Name)
    def map (depth, t)
      if (depth == 0)
        def t' = f (t)
        if (t' === t) null
        else t'
      else
        def left = f (t.left)
        def right = map (depth - 1, t.right)
        if (left === t.left && right === null)
          null
        else
          def right' = if (right == null) t.right else right
          pool.GetApply (left, right', skip_parents)
    if (Arity == 0) this
    else 
      def res = map (Arity - 1, right)
      if (res == null) this
      else pool.GetApply (left, res, skip_parents)

  public ExtractProof (get_lit : Literal -> E, proof : Proof, t1 : Term, t2 : Term) : E
    def fake (comment)
      E.App ("eq_fake", [comment, E.App ("=", [E.Term (t1, false), E.Term (t2, false)])])

    //log (TEMP, $"Extract(t1=$(t1.ToExactString()) t2=$(t2.ToExactString()))")
    match (proof)
      | _ when t1 === t2 => E.App ("eq_refl", [E.Term (t1, false)])

      | Leaf (lit) =>
        if (lit.atom.term1 === t1 && lit.atom.term2 === t2)
          get_lit (lit)
        else if (lit.atom.term1 === t2 && lit.atom.term2 === t1)
          E.App ("eq_symm", [get_lit (lit)])
        else
          fake (E.App ("fake_lit", [E.Lit (lit)]))

      | Rule2 ("fun-congr", _, _) =>
        assert (t1.Arity == t2.Arity)
        assert (t1.Name == t2.Name)
        def f = t1.Name
        def id = "eqtmp"
        def loop (_)
          | (t1 :: rest1, t2 :: rest2, pref, proof) =>
            if (t1 === t2)
              loop (rest1, rest2, E.Term (t2, false) :: pref, proof)
            else
              def p = 
                E.App (f, pref.Rev () + [E.Ref (id)] + rest1.Map (E.Term (_, false)))
              def newproof = E.App ("eq_mon", [E.Lambda (id, p), t1.EProofOfEqualityWith (get_lit, t2)]) 
              def proof = 
                if (proof != null)
                  E.App ("eq_trans", [proof, newproof])
                else newproof
              loop (rest1, rest2, E.Term (t2, prop = false) :: pref, proof)
          | ([], [], _, proof) => proof
          | _ => assert (false)
        loop (t1.Children, t2.Children, [], null)

      | Rule1 (label, _) \
      | Rule2 (label, _, _) \
      | Rule3 (label, _, _, _) \
      | Rule4 (label, _, _, _, _) =>
        fake (E.App ("unknown_rule", [E.Ref (label)]))

      | True =>
        fake (E.Ref ("true_proof"))

      | Token | EqProof => assert (false, $ "proof=$proof t1=$t1 t2=$t2")


  public EProofOfEqualityWith (get_lit : Literal -> E, other : Term) : E
    //log (TEMP, $"EPEW(t1=$(ToExactString()) t2=$(other.ToExactString())) $(System.Environment.StackTrace)")
    if (other === this)
      E.App ("eq_refl", [E.Term (this, false)])
    else if (other.proof_parent === this)
      ExtractProof (get_lit, other.proof, this, other)
    else if (proof_parent === other)
      ExtractProof (get_lit, proof, this, other)
    else
      assert (other != null)
      assert (Root : object == other.Root)

      def our_proofparents = Hashtable ()
      def mark_parents (t)
        when (t != null)
          our_proofparents [t] = t
          mark_parents (t.proof_parent)
      mark_parents (this)

      def middle =
        if (our_proofparents.Contains (other)) proof_parent
        else other.proof_parent

      E.App ("eq_trans", [this.EProofOfEqualityWith (get_lit, middle), 
                          middle.EProofOfEqualityWith (get_lit, other)])

  [Profile] \
  public ProofOfEqualityWith (other : Term) : Proof
    if (other : object == this) Proof.True ()
    else
      assert (other != null)
      assert (Root : object == other.Root)

      def our_proofparents = Hashtable ()
      def mark_parents (t)
        when (t != null)
          our_proofparents [t] = t
          mark_parents (t.proof_parent)
      mark_parents (this)

      def our_proof_till (proof, t, end)
        if (t : object == end) proof
        else 
          def proof = Proof.Rule2 ("fun-trans", proof, t.proof)
          our_proof_till (proof, t.proof_parent, end)
      
      def collect_proof (proof, t)
        if (our_proofparents.Contains (t))
          our_proof_till (proof, this, t)
        else
          def proof = Proof.Rule2 ("fun-trans'", proof, t.proof)
          collect_proof (proof, t.proof_parent)

      collect_proof (Proof.True (), other)

  public ProofOfCanonForm () : Proof
    ProofOfEqualityWith (Root)

  public LexiCmp (other : Term) : int
    if (this : object == other) 0
    else
      def res = string.CompareOrdinal (Name, other.Name)
      if (res != 0) res
      else
        if (left == null)
          if (other.left == null) 0
          else -1
        else
          if (other.left == null) 1
          else
            def res = left.LexiCmp (other.left)
            if (res != 0) res
            else right.LexiCmp (other.right)
          

  // make [this] a new proof Root
  ReverseProofPath () : void
    def loop (t, par, reason)
      if (t.proof_parent == null)
        assert (t.proof is Proof.True)
      else
        loop (t.proof_parent, t, t.proof)
      t.WillWrite ()
      t.proof_parent = par
      t.proof = reason

    when (proof_parent != null)
      WillWrite ()
      loop (proof_parent, this, proof)
      proof = Proof.True ()


  public Apply (sub : IntTree [Term]) : Term
    mutable res = null
    if (sub.TryGetValue (Id, out res))
      res
    else
      if (left == null) this
      else if (left : object == pool.Forall2 || left : object == pool.Forall3)
        // OK, it get's tricky here, we need to avoid capture
        def vars = right.left
        assert (vars.Name == "$@vars")
        def broken =
          vars.FoldIndexedChildren ([], (_, t, acc) => 
            if (sub.Contains (t.Id)) t.Id :: acc else acc)
        def sub =
          if (broken is []) sub
          else
            // log (WARN, $"capture! $(System.Environment.StackTrace)")
            sub.Fold (IntTree.Empty (), (id, v, acc) =>
              if (broken.Contains (id)) acc
              else acc.Add (id, v))
        pool.GetApply (left, right.Apply (sub), true)
      else
        pool.GetApply (left.Apply (sub), right.Apply (sub), skip_parents)


  [Profile] \
  internal CannotMergeProof (other : Term) : Proof
    assert (Root : object != other.Root)

    mutable mask = Root.distinct_mask & other.Root.distinct_mask
    when (mask != 0)
      mutable ptr = 0
      while (mask & 1 == 0)
        mask >>= 1
        ptr++
      def (proof, terms) = pool.distinct_stack [ptr]
      mutable t1 = null, t2 = null
      foreach (t in terms)
        when (t.Root : object == this.Root) t1 = t
        when (t.Root : object == other.Root) t2 = t
      assert (t1 != null && t2 != null)
      return (Proof.Rule3 ("distinct", 
                           Proof.EqProof (t1, this), 
                           Proof.EqProof (t2, other), 
                           proof))
   
    def check_one (t1, t2, proof)
      if (t1.Root : object == this.Root && t2.Root : object == other.Root)
        Proof.Rule3 ("cannot-merge", 
                        Proof.EqProof (t1, this),
                        Proof.EqProof (t2, other),
                        proof)
      else null

    mutable res = null
    def check_both (t1, t2, proof)
      when (res == null) res = check_one (t1, t2, proof)
      when (res == null) res = check_one (t2, t1, proof)
      res != null
    
    _ = Root.forbidden_merges.Exists (check_both)
    _ = other.Root.forbidden_merges.Exists (check_both)
    res

  public ForbidMerge (other : Term, proof : Proof) : void
    log (TERM, $ "forbid $this = $other by $proof")
    if (Root : object == other.Root)
      pool.core.Refute (Proof.Rule2 ("forbid-merge", proof, Proof.EqProof (this, other)))
    else
      when (CannotMergeProof (other) == null)
        Root.WillWrite ()
        Root.forbidden_merges ::= (this, other, proof)
 
  
  internal IterEqc (f : Term -> void) : void
    f (this)
    for (mutable p = eqc_next; p : object != this; p = p.eqc_next)
      f (p)

  public override GetHashCode () : int
    Id

  [Nemerle.OverrideObjectEquals] \
  public Equals (other : Term) : bool implements System.IEquatable[Term].Equals
    this : object == other

  public CompareTo (other : Term) : int
    Id - other.Id