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 set namespace Fx7 public partial class Term public partial class Pool [Copy] mutable internal matcher_proofs : IntTree [IntTree [SubstLite]] = IntTree.Empty () [Copy] mutable internal matcher_proofs_updated_at : int [Copy] mutable internal matcher_partial_updates : IntTree [int] = IntTree.Empty () [Copy] mutable internal matcher_prev_results : IntTree [Term.Matcher.PrevResults] = IntTree.Empty () mutable internal subtrigger_marker : SubTriggerMarker mutable internal subtrigger_marker2 : SubTriggerMarker internal trigger_data_cache : Hashtable [list [Term] * list [Term], Matcher.TriggerData] = Hashtable () // simplify matcher stuff [Copy] mutable internal simplify_matcher_prev_results : IntTree [IntTree [Term]] = IntTree.Empty () [Copy] mutable internal simplify_matcher_updates : IntTree [int] = IntTree.Empty () internal head_and_root_cache : Hashtable [Term, Hashtable [Term, list [Term]]] = Hashtable () // ------------------------------------------------------------------------- // Matcher public class Matcher public type PrevResults = array [SubstLite] public class XSubst public vars : array [Term] public this (n : int) vars = array (n) this (v : array [Term]) vars = v.Clone () :> array [Term] public override ToString () : string $ "XSubst( $(vars.ToList()) )" public override GetHashCode () : int mutable res = 0 foreach (t in vars) unchecked res = res * 13 + if (t == null) 1 else t.Id res public Clone () : XSubst XSubst (vars) [Nemerle.OverrideObjectEquals] \ public Eqauls (other : XSubst) : bool assert (vars.Length == other.vars.Length) foreach (i in [0 .. vars.Length - 1]) when (vars [i] : object != other.vars [i]) return (false) true public Apply (stars : list [Term], t : Term) : Term mutable i = 0 mutable s = Subst.Empty () foreach (t in stars) //log (TEMP, $"$t->$(vars[i])") s = s.Add (t.Id, vars [i]) i++ t.Apply (s) public Apply (stars : list [Term], f : ToCNF.Fact) : void mutable i = 0 mutable s = Subst.Empty () foreach (t in stars) //log (TEMP, $"$t->$(vars[i])") s = s.Add (t.Id, vars [i]) i++ // log (TEMP, $"terms= $(f.Terms.ToList())") foreach (t in f.Terms) //log (TEMP, $"apply($t)") f.AddTerm (t.Apply (s)) mutable used = false [Accessor] qatom : QAtom pool : Pool res : Vec [ToCNF.Fact] public static Start (pool : Pool, is_partial : bool) : void pool.subtrigger_marker = SubTriggerMarker (pool, is_partial) when (Driver.SelfChecks) pool.subtrigger_marker2 = SubTriggerMarker (pool, is_partial, fake = true) pool.head_and_root_cache.Clear () pool.MatchHeight++ public static Stop (pool : Pool) : void pool.subtrigger_marker.SaveUpdates () pool.MatchHeight++ pool.matcher_proofs = pool.subtrigger_marker.Proofs public this (qatom : QAtom, res : Vec [ToCNF.Fact]) // log (TEMP, $ "$vars triggers=$triggers from $formula") this.qatom = qatom this.pool = qatom.term1.Core.TermPool this.res = res [Profile] \ public Prepare () : void when (qatom.MatcherCache == null) qatom.MatcherCache = qatom.GetTriggers ().Map (GetData) foreach (d in qatom.MatcherCache) foreach ((_, s) in d.trigger) pool.subtrigger_marker.PrepareTrigger (s) public Run () : void assert (!used) used = true MatchTriggers () [Profile] \ MatchTriggers () : void def id = qatom.term1.Id mutable prev_res unless (pool.matcher_prev_results.TryGetValue (id, out prev_res)) prev_res = null def len = qatom.MatcherCache.Length def new_res = array (len) mutable is_new = false foreach (i in [0 .. len - 1]) def prev = if (prev_res == null) pool.EmptySubst else prev_res [i] new_res [i] = MatchTrigger (prev, qatom.MatcherCache [i]) when (!is_new && !(new_res [i] === prev)) is_new = true when (is_new) pool.matcher_prev_results = pool.matcher_prev_results.Replace (id, new_res) [Record] \ internal class TriggerData public trigger : list [Term * Term] public names : list [int] public linear : bool [Profile] \ GetData (trigger : list [Term]) : TriggerData def vars = qatom.Vars def star_sub = vars.FoldLeft (IntTree.Empty (), (v, m) => m.Add (v.Id, v.pool.Star)) def index (idx, e, l) match (l) | x :: xs => if (x.Id == e) idx else index (idx + 1, e, xs) | [] => assert (false) def names = $[ index (0, n, vars) | t in trigger, n in pool.subtrigger_marker.ExtractStarsNames (star_sub, t) ] def linear = names.Sort (_ - _).RemoveDuplicates ().Length == names.Length TriggerData (trigger.Map (t => (t, t.Apply (star_sub))), names, linear) RunMarker (t : Term, st : Term) : SubstLite def res = pool.subtrigger_marker.TriggerMatches (t, st) when (Driver.SelfChecks) def res2 = pool.subtrigger_marker2.TriggerMatches (t, st) if (res == null || res2 == null) assert (res == null && res2 == null) else //log (TEMP, $"compare: $res, $res2") def pres = res.PruneJunk () def pres2 = res2.PruneJunk () assert (pres === res2, $"for $t $res -> $pres <> $res2 -> $pres2") res DoMatch (combined : SubstLite, prev_res : SubstLite, data : TriggerData, constrain : bool) : SubstLite def vars = qatom.Vars if (combined == null) assert (vars is []) unless (prev_res === pool.EmptySubst) def fact = qatom.GetFreshFact () assert (fact.Terms.Length == 0, $ "broken empty fact $fact") res.Add (fact) null else def sub = XSubst (vars.Length) def constrained = if (constrain) combined.Constrain (data.names, sub) else combined def add (sub) def fact = qatom.GetFreshFact () res.Add (fact) sub.Apply (vars, fact) def res = constrained.Subtract (prev_res) res.Iter (data.names, sub, add) constrained [Profile] \ MatchMTrigger (prev_res : SubstLite, data : TriggerData) : SubstLite def substs = data.trigger.Map (RunMarker) def empty = pool.EmptySubst if (substs.Exists (_ == empty : object)) assert (prev_res === empty, $ "t=$(data.trigger), substs= $substs, prev_res=$prev_res") prev_res else DoMatch (SubstLite.Construct (pool, substs), prev_res, data, constrain = true) [Profile] \ MatchTrigger (prev_res : SubstLite, data : TriggerData) : SubstLite //log (TEMP, $ "$(data.trigger.Map((_,b)=>b))") match (data.trigger) | [(t, s)] => def combined = RunMarker (t, s) if (combined === pool.EmptySubst) assert (prev_res === pool.EmptySubst, $ "t=$(data.trigger), substs= $combined, prev_res=$prev_res") prev_res else DoMatch (combined, prev_res, data, constrain = !data.linear) | _ => MatchMTrigger (prev_res, data)