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

set namespace Fx7

public class QAtom  : Atom
  public this (t1 : Term)
    base (t1, null)
    assert (t1.Name == "forall")
    assert (t1.Arity == 2 || t1.Arity == 3)
    SaveExplicitTriggers ()
  
  public Formula : Term
    [Memoize (InvalidValue = null)] \
    get
      match (term1.Children)
        | [_, _, c] | [_, c] => c
        | _ => assert (false)

  mutable instantiator : ToCNF.Instantiator
  public GetFreshFact (is_existential = false) : ToCNF.Fact
    when (instantiator == null)
      instantiator = ToCNF.Instantiator (this)
    instantiator.GetFreshFact (is_existential)

  public GenFact (sub : Term -> Term, res : Vec [ToCNF.Fact], is_existential = false) : void
    def fact = GetFreshFact (is_existential)
    foreach (t in fact.Terms)
      fact.AddTerm (sub (t))
    res.Add (fact)

 
  /*
  [Memoize (InvalidValue = null)] \
  public Skolemize () : Literal
    def core = term1.Core
    def sub = Vars.FoldLeft (IntTree.Empty (), fun (t, acc) {
      acc.Add (t.Id, core.TermPool.FreshVar ())
    })
    core.TermToLiteral (MinDepth + 1, Formula.Apply (sub))
    */
 
  //public override ToString () : string
  //  $ "(FORALL $Vars $(GetTriggers ()) $Formula)"
  
  public Dump () : string
    $ "FORALL $Vars. $Formula ::: $(GetTriggers ().ToList ())"

  mutable empty_vars_subst : Subst

  loop_test (pat : Term) : bool
    if (!Driver.LoopTest || pat.Core.CurrentStrategy >= 3)
      false
    else
      // look for instance of pat in term
      def check (term, pat, sub)
        if (sub == null) null
        else if (pat : object == term) sub
        else if (term.NameDesc == pat.NameDesc)
          List.FoldLeft2 (term.Children, pat.Children, sub, check)
        else 
          match (sub.Find (pat.Id))
            | Some (null) =>
              sub.Replace (pat.Id, term)
            | Some (term') when term : object == term' =>
              sub
            | _ => null

      def is_larger (sub)
        sub.Exists (fun (_, t) { t != null && ! t.IsVar })
        
      def find_any (t)
        if (t : object == pat || t.Name == "forall") false
        else
          def sub = check (t, pat, empty_vars_subst)
          if (sub != null && is_larger (sub)) true
          else t.Children.Exists (find_any)
          
      assert (empty_vars_subst != null)
      //log (TEMP, $ "loop_test ($pat)")
      find_any (Formula)
   
  
  public Vars : list [Term]
    [Memoize (InvalidValue = null)] \
    get
      def v = term1.Children.Head
      assert (v.Name == "$@vars")
      def real_vars = Hashtable ()
      empty_vars_subst = IntTree.Empty ()
      foreach (v in v.Children)
        if (real_vars.Contains (v))
          throw FatalError ($ "duplicate variable $v in $this")
        else
          empty_vars_subst = empty_vars_subst.Add (v.Id, null)
        real_vars [v] = false
      Formula.Iter (fun (t) {
        when (real_vars.Contains (t))
          real_vars [t] = true
      })
      def res = v.Children.Filter (fun (x) { real_vars [x] })
      //if (res is []) throw FatalError ($ "formula $Formula doesn't use any of its quantified variables") else 
      res

  public HasExplicitTriggers : bool
    get
      cache [0] != null

  SaveExplicitTriggers () : void
    match (term1.Children)
      | [_, (Name = "PATS", Children = children), _] when !Driver.IgnoreTriggers =>
        def triggerize (t, acc)
          if (t.Name == "PROMOTE" || t.Name == "PLUNGE")
            assert (t.Arity == 0)
            acc
          else if (t.Name == "MPAT")
            t.Children :: acc
          else
            assert (!t.IsVar)
            [t] :: acc
        cache [0] = children.FoldLeft ([], triggerize).ToArray ()
      | _ => {}

  TriggerForTransitivity (form : Term) : list [list [Term]]
    def pool = form.Core.TermPool

    def get_const (_ : Term)
      | E ("not", [E ("=", [t, V (name)])]) \
      | E ("not", [E ("=", [V (name), t])]) =>
        Some ((pool.Get ("not", [t]), name))
      | E ("=", [t, V (name)]) \
      | E ("=", [V (name), t]) =>
        Some ((t, name))
      | _ => None ()
        
    def check (res : Term, a : Term, b : Term)
      match ((get_const (res), get_const (a), get_const (b)))
        | (Some ((res, name1)), Some ((a, name2)), Some ((b, name3))) when name1 == name2 && name1 == name3 =>
          check (res, a, b)
        | _ =>
          match ((res, a, b))
            | (E (name1, [x', z']), E ("not", [E (name2, [x, y]) as a']), E ("not", [E (name3, [y', z]) as b'])) \
                 when name1 == name2 && name2 == name3 =>
              if (y === y')
                if (x' === x && z' === z && Vars.Contains (x) && Vars.Contains (y) && Vars.Contains (z))
                  log (INFO, $"$form found to be transtivity axiom, trigger: $(a'), $(b')")
                  [[a', b']]
                else null
              else if (x === z) check (res, b, a)
              else null
            | _ => null

    match (form)
      | E ("or", [ch1, ch2, ch3]) =>
        if (ch1.Name != "not") check (ch1, ch2, ch3)
        else if (ch2.Name != "not") check (ch2, ch1, ch3)
        else check (ch3, ch1, ch2)
      | _ => null

  DoGetTriggers (skip_arith : bool) : list [list [Term]]
    match (term1.Children)
      | [_, E ("NOPATS", exclude), form] \
      | [_, E ("PATS", _), form] with exclude = [] \
      | [_, form] with exclude = [] =>
        def vars = Vars
        mutable triggers = []
        def like_it (t)
          match (t.Name) 
            | "and" | "or" | "not" | "=" => false
            | "<=" | ">=" | "<" | ">" | "-" | "+" | "*" | "~" =>
              !skip_arith
              /*
              // we don't like (<= x c), (<= x y) and the like
              // we do like (<= (f x) c), (<= (f x) (f y))
              match (t.Children)
                | [_c1, _c2] when skip_arith => false
                  //if (vars.Contains (c1) || vars.Contains (c2)) false
                  //else true
                | _ => true
              */
            | _ => true
        def childrens = Hashtable ()
        mutable tries = []
        def get_triggers (t)
          if (t.IsVar)
            if (List.ContainsRef (vars, t)) [t]
            else []
          else
            def backup = triggers
            def used_vars = t.Children.Map (get_triggers)
            if (backup : object == triggers)
              def ht = Hashtable ()
              mutable res = []
              foreach (vs in used_vars)
                foreach (v when !ht.Contains (v) in vs)
                  res ::= v
                  ht [v] = v
              when (!List.ContainsRef (exclude, t) && 
                    like_it (t) &&
                    !List.ContainsRef (triggers, t))
                if (ht.Count == vars.Length)
                  unless (loop_test (t))
                    triggers ::= t
                else
                  when (triggers is [] &&
                        t.Children.ForAll (fun (x) { 
                          !childrens.Contains (x) ||
                          childrens [x].Length < ht.Count
                        }))
                    tries ::= (t, res)
                    childrens [t] = res
              res
            else vars

        _ = get_triggers (form)
        
        if (! (triggers is []))
          $[[x] | x in triggers]
        else if (TriggerForTransitivity (form) != null)
          TriggerForTransitivity (form)
        else
          def gotit = Hashtable ()
          foreach (v in Vars) gotit [v] = false
          tries = tries.Rev ().Sort (fun ((_, v1), (_, v2)) { v2.Length - v1.Length })
          mutable remaining_vars = Vars.Length
          mutable trigger = []
          //log (TEMP, $"find multitrigger in $term1")
          foreach ((t, vars) in tries)
            //log (TEMP, $"consider $vars (from $t)")
            def backup = remaining_vars
            foreach (v in vars)
              when (!gotit [v])
                gotit [v] = true
                remaining_vars--
            when (backup != remaining_vars)
              trigger ::= t
            when (remaining_vars == 0) break
          if (remaining_vars != 0)
            log (WARN, $ "cannot find any suitable triggers in $term1")
            []
          else
            [trigger]

      | _ => assert (false)

  mutable matcher_cache : array [Term.Matcher.TriggerData]
  mutable matcher_cache_strategy : int

  internal MatcherCache : array [Term.Matcher.TriggerData]
    get
      when (matcher_cache_strategy != term1.Core.CurrentStrategy)
        matcher_cache = null
      matcher_cache
    set
      matcher_cache = value
      matcher_cache_strategy = term1.Core.CurrentStrategy
      

  static num_strategies = 4
  cache : array [array [list [Term]]] = array (num_strategies + 1)
  public GetTriggers () : array [list [Term]]
    def core = term1.Core
    def strategy = core.CurrentStrategy
    if (cache [0] != null)
      cache [0]
    else if (cache [strategy] != null)
      cache [strategy]
    else
      def lres =
        match (strategy)
          | 1 => DoGetTriggers (skip_arith = true)
          | 2 => DoGetTriggers (skip_arith = true) // just full arith checks
          | 3 => DoGetTriggers (skip_arith = false)
          | _ => assert (false)
      def res = lres.ToArray ()
      cache [strategy] = res
      when (Driver.VerboseQuant) log (INFO, $"found trigger [s:$strategy]: $(Dump())")
      res