using System.Console
using Nemerle.Collections
using Nemerle.Utility
using Nemerle.Logging
using Nemerle.Imperative
using Nemerle.Profiling

set namespace Fx7

#define MULTI_REF
//#define DETERMINISTIC

public type Vec ['a] = System.Collections.Generic.List ['a]

public delegate Callback () : void

public class Core
  public TermPool : Term.Pool
  public TheDriver : Driver

  public event OnPush : Callback
  public event OnPop : Callback

  public mutable Refuted : bool
  public mutable RefutationProof : list [Literal]
  public mutable ProofObject : Proof

  internal mutable PlainPredicates : Hashtable [string, string] = Hashtable ()

  internal ImportantLiterals : Hashtable [Literal, float] = Hashtable ()
  internal mutable CurrentStrategy : int = 3
  
  pending : Queue [void -> void] = Queue ()
  mutable state_level = 0

  internal mutable LiteralPool : SimpleSolver
  internal mutable linear_theory : LinearTheory

  public this (d : Driver)
    TermPool = Term.Pool (this)
    free_fun_th = FreeFunTheory (this)
    TheDriver = d
    def arith ()
      linear_theory = LinearTheory (0, this)
      linear_theory
    mutable thr = [arith () : PlainVarTheory]

    mutable id = 1
    when (Driver.EnableTcTheory)
      thr ::= TcTheory (id, this)
      id++
    thr = thr.Rev ()
    var_theories = thr.ToArray ()

    theories = thr.Map (fun (x) { x : Theory }) + [free_fun_th]


  #region Theory dispatch
  free_fun_th : FreeFunTheory
  theories : list [Theory]
  internal var_theories : array [PlainVarTheory]

  public IsSomeTheoryPredicate (name : string) : bool
    when (name == "distinct")
      return (true)
    foreach (t in var_theories)
      when (t.IsMyPredicate (name))
        return (true)
    false

  [Profile] \
  AddVar (thr : int, t : Term) : void
    when (thr == -1)
      return

    log (COREV, $"AddVar($t) root=$(t.Root)")

    def old_t = t.Var [thr]
    assert (old_t : object != t)

    def th = var_theories [thr]
    th.MakeAlien (t, outer = th.IsMyFunction (t.Name))
    t.SetVar (thr, t)
   
    if (old_t != null)
      th.TellEquality (t, old_t, Proof.EqProof (t, old_t))
    else if (t : object != t.Root)
      if (t.Root.Var [thr] != null)
        // whoops, we already had a variable here
        def root_t = t.Root.Var [thr]
        log (COREV, $"AddVar: assert eq $t = $root_t to $th")
        th.TellEquality (t, root_t, Proof.EqProof (t, root_t))
      else
        log (COREV, $"AddVar: copy var $(t.Root) <- $t")
        t.Root.SetVar (thr, t)
    else {}

  // -1 is UIF
  TheoryOf (t : Term) : int
    foreach (i in [0 .. var_theories.Length - 1])
      def th = var_theories [i]
      when (th.IsMyFunction (t.Name))
        return (i)
    -1
    

  // thr:
  // -2 -- don't create top-alien
  // -1 -- do create it
  [Profile] \
  Alienate (thr : int, t : Term) : void
    DoAlienate (thr, t)
  
  DoAlienate (thr : int, t : Term) : void
    log (COREV, $"Alienate($thr, $t) done=$(t.Alienated)")
    def thr' = TheoryOf (t)
    unless (t.Alienated)
      t.WillWrite ()
      t.Alienated = true
      foreach (c in t.Children)
        DoAlienate (thr', c)
    when (thr != thr' && thr != -2)
      when (thr != -1 && t.Var [thr] : object != t)
        AddVar (thr, t)
      when (thr' != -1 && t.Var [thr'] : object != t)
        AddVar (thr', t)
    

  AssertPredicate (neg : bool, t : Term, proof : Proof) : void
    if (t.Name == "distinct")
      if (neg)
        // we probably should check each possibility here, but we won't
        {}
      else
        t.IterChildren (Alienate (-1, _))
        TermPool.AssertDistinct (t.Children, proof)
    else
      foreach (i in [0 .. var_theories.Length - 1])
        def th = var_theories [i]
        when (th.IsMyPredicate (t.Name))
          log (COREV, $ "tell struct-pred $t")
          t.IterChildren (Alienate (i, _))
          th.AssertPredicate (neg, t.Name, t.Children, proof)
 
  // used by TermPool.Merge
  internal TellEquality (t1 : Term, t2 : Term) : void
    log (CORE, $"TellEquality($t1, $t2)")
    
    foreach (i in [0 .. var_theories.Length - 1])
      def r1 = t1.Var [i]
      def r2 = t2.Var [i]
      if (r1 == null)
        if (r2 != null)
          t1.SetVar (i, r2)
        else {}
      else
        if (r2 != null)
          log (CORE, $"will telleq: $t1 $t2")
          pending.Push (fun () {
            log (CORE, $"run telleq: $t1 $t2");
            Alienate (-2, r1);
            Alienate (-2, r2);
            var_theories [i].TellEquality (r1, r2, Proof.EqProof (r1, r2))
          })
        else
          t2.SetVar (i, r1)
      
  TellInequality (t1 : Term, t2 : Term, proof : Proof) : void
    log (COREV, $ "tell struct-ineq $t1 $t2")
    Alienate (-1, t1)
    Alienate (-1, t2)
    free_fun_th.TellInequality (t1, t2, proof)


  TellEquality (t1 : Term, t2 : Term, proof : Proof) : void
    log (COREV, $ "tell struct-eq $t1 $t2")
    // using -2 here is problematic
    Alienate (-1, t1)
    Alienate (-1, t2)
    TermPool.Merge (t1, t2, proof)
  #endregion


  #region push and pop
  [Profile] \
  public PushState () : void
    assert (!Refuted)
    log (CORE, "( push")
    state_level++
    OnPush ()
    foreach (th in var_theories)
      th.PushState ()
    free_fun_th.PushState ()

  [Profile] \
  public PopState () : void
    log (CORE, "pop )")
    state_level--
    free_fun_th.PopState ()
    foreach (th in var_theories)
      th.PopState ()
    OnPop ()
    Reset ()
 
  internal Reset () : void
    log (CORE, "reset")
    pending.Clear ()
    Refuted = false
    RefutationProof = null
    ProofObject = null

  public Refute (proof : Proof) : void
    log (CORE, $"Refute, lits=$(proof.GetLiterals())")
    unless (Refuted)
      Refuted = true
      RefutationProof = proof.GetLiterals ()
      ProofObject = proof

  public ClearTheories () : void
    theories.Iter (_.Clear ())

  public Assert (lit : Literal) : void
    SetActive (lit)
    assert (!lit.atom.IsQuantified)
    DoAssert (lit)

  [Profile] \
  public FinalCheck (full_check : bool) : void
    while (true)
      while (!pending.IsEmpty)
        pending.Take () ()
        when (Refuted) break
      theories.Iter (_.FinalCheck ())
      when (Refuted || pending.IsEmpty) break

    when (full_check)
      theories.Iter (_.FullFinalCheck ())
      when (!Refuted && !pending.IsEmpty)
        FinalCheck (true) // need to redo :/
  #endregion


  #region Utils
  // we don't want true randomness here
  // http://crypto.mat.sbg.ac.at/results/karl/server/node4.html
  mutable rand_seed : uint = 1 : uint
  public Rand () : uint
    unchecked
      rand_seed *= 3039177861
    rand_seed

  public Rand (max : int) : int
    unchecked
      (Rand () % (max :> uint)) :> int

  public RandomizeList ['a] (l : list ['a]) : list ['a]
    def a = l.ToArray ()
    def len = a.Length
    repeat (len)
      a [Rand (len)] <-> a [Rand (len)]
    List.FromArray (a)

  [System.Runtime.InteropServices.DllImport ("rdtsc.dll")] \
  public static extern read_tsc () : long
  #endregion


  #region Assert helpers
  DoAssert (lit : Literal) : void
    TheDriver.num_asserts++
    log (CORE, $"assert $lit")
    unless (Refuted)
      AssertOnly (lit, Proof.Leaf (lit))
      while (!Refuted && !pending.IsEmpty)
        pending.Take () ()
  
  AssertOnly (lit : Literal, proof : Proof) : void
    unless (Refuted)
      def t1 = lit.atom.term1
      def t2 = lit.atom.term2
      if (lit.atom.IsQuantified) {}
      else if (t2 == null)
        AssertPredicate (lit.IsNeg, t1, proof)
      else
        if (lit.IsNeg)
          TellInequality (t1, t2, proof)
        else
          TellEquality (t1, t2, proof)

  SetActive (l : Literal) : void
    unless (l.atom.IsQuantified)
      l.atom.term1.MakeActive ()
      when (l.atom.term2 != null)
        l.atom.term2.MakeActive ()
  #endregion


  #region CNF conversion
  internal mutable all_clauses : list [Clause] = []
  internal mutable all_atoms : list [Atom] = []

  public MakeClause (lits : array [Literal], proof : Rule) : Clause
    def c = Clause (lits, proof)
    all_clauses ::= c
    c

  literal_cache : Hashtable [Term, Literal] = Hashtable ()
  atom_cache : Hashtable [Atom, Atom] = Hashtable ()
  known_predicates : Hashtable [string, string] = Hashtable ()
  ite_expanded : Hashtable [Term, Term] = Hashtable ()

  mk (name : string, ch1 : Term) : Term
    TermPool.Get (name, [ch1])

  mk (name : string, ch1 : Term, ch2 : Term) : Term
    TermPool.Get (name, [ch1, ch2])
 
  mk (name : string, ch : list [Term]) : Term
    TermPool.Get (name, ch)

  mutable ite_assertion : Term

  ExpandITE (f : Term) : Term
    if (ite_expanded.Contains (f))
      ite_expanded [f]
    else if (f.Name == "ite")
      match (f.Children)
        | [cond, th, el] =>
          def fv = TermPool.FreshVar ()
          ite_expanded [f] = fv
          def th = mk ("or", mk ("=", fv, ExpandITE (th)), mk ("not", cond))
          def el = mk ("or", mk ("=", fv, ExpandITE (el)), cond)
          if (ite_assertion == null)
            ite_assertion = mk ("and", th, el)
          else
            ite_assertion = mk ("and", [th, el, ite_assertion])
          fv
        | _ => throw FatalError ("bad ITE")
    else
      def t = mk (f.Name, f.Children.Map (ExpandITE))
      ite_expanded [f] = t
      t

  [Profile] \
  public TermToLiteral (depth : int, t : Term) : Literal
    mutable res
    if (literal_cache.TryGetValue (t, out res)) res
    else
      res =
        match (t.Name)
          | "not" => ~TermToLiteral (depth, t.OnlyChild)
          | "and" | "or" => PAtom (t).GetLiteral (false)
          | "forall" => QAtom (t).GetLiteral (false)
          | "true" with neg = false \
          | "false" with neg = true =>
            Atom (TermPool.True, TermPool.True).GetLiteral (neg)

          | "=" =>
            def t1 = ExpandITE (t.Child_1of2)
            def t2 = ExpandITE (t.Child_2of2)
            Atom (t1, t2).GetLiteral (false)
          
          | name when IsSomeTheoryPredicate (name) =>
            Atom (ExpandITE (t), null).GetLiteral (false)

          | name =>
            unless (known_predicates.Contains (name))
              known_predicates [name] = name
              unless (name.IndexOf ('.') != -1)
                log (INFO, $ "new predicate: $name")
            Atom (ExpandITE (t), TermPool.True).GetLiteral (false)

      assert (ite_assertion == null)
      // it might be the case, that the atom constructor will do some
      // canonicalization
      when (atom_cache.Contains (res.atom))
        res = atom_cache [res.atom].GetLiteral (res.IsNeg)
      when (res.atom.MinDepth > depth)
        res.atom.MinDepth = depth
      all_atoms ::= res.atom
      atom_cache [res.atom] = res.atom
      literal_cache [t] = res
      res

  #endregion