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) mutable used = false [Accessor] qatom : QAtom pool : Pool mutable res : list [Term] = [] 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) // log (TEMP, $ "$vars triggers=$triggers from $formula") this.qatom = qatom this.pool = qatom.term1.Core.TermPool [Profile] \ public Prepare () : void when (qatom.matcher_cache == null) qatom.matcher_cache = qatom.GetTriggers ().Map (GetData) foreach (d in qatom.matcher_cache) foreach ((_, s) in d.trigger) pool.subtrigger_marker.PrepareTrigger (s) public Run () : list [Term] assert (!used) used = true if (Driver.SimplifyMatching) SimplifyMatch () when (Driver.SelfChecks) def ht = Hashtable () foreach (t in res) ht [t] = t def ores = res res = [] MatchTriggers () foreach (t in res) assert (ht.Contains (t), $ "res=$res ores=$ores") def ht2 = Hashtable () foreach (t in res) ht2 [t] = t foreach (t in ores) assert (ht2.Contains (t), $ "X res=$res ores=$ores") else MatchTriggers () res [Profile] \ SimplifyMatch () : void foreach (c in qatom.matcher_cache) when (c.simplify_matcher == null) c.simplify_matcher = SimplifyMatcherCache (this, c) c.simplify_matcher.Run (this) [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.matcher_cache.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.matcher_cache [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 public mutable simplify_matcher : SimplifyMatcherCache [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, null) 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) res ::= qatom.Formula null else def sub = XSubst (vars.Length) def constrained = if (constrain) combined.Constrain (data.names, sub) else combined def add (sub) res ::= sub.Apply (vars, qatom.Formula) 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) public class SimplifyMatcherCache sigma : XSubst names : list [Term] names_ar : array [Term] trigger : list [Term] apply_cache : Hashtable [XSubst, Term] = Hashtable () pool : Pool id : int mutable matcher : Matcher mutable prev_res : IntTree [Term] static mutable current_id : int // linear search is going to be faster for typical triggers (2-3 variables) // than a hashtable search FindName (t : Term) : int for (mutable i = 0; i < names_ar.Length; ++i) when (names_ar [i] === t) return i -1 internal this (matcher : Matcher, data : TriggerData) id = current_id current_id++ pool = matcher.pool names = matcher.qatom.Vars names_ar = names.ToArray () sigma = XSubst (names_ar.Length) trigger = data.trigger.Map ((t, _) => t) Decompose (p : Term, t : Term, rest : list [Term * Term]) : void mutable acc = [] def combine (_) | (p :: pp, t :: tt) => log (SMATCH, $"decompose p=$p t=$t (roots: $(p.Root) $(t.Root))") def t = t.Root if (p.Arity == 0) def idx = FindName (p) if (idx >= 0) if (sigma.vars [idx] == null) sigma.vars [idx] = t combine (pp, tt) sigma.vars [idx] = null else if (sigma.vars [idx] === t) combine (pp, tt) else {} else if (p.Root === t) combine (pp, tt) else {} else acc ::= (p, t) combine (pp, tt) | ([], []) => Match (acc.RevAppend (rest)) | _ => assert (false) combine (p.Children, t.Children) public Run (m : Matcher) : void log (SMATCH, $"run matcher: $trigger") matcher = m unless (pool.simplify_matcher_prev_results.TryGetValue (id, out prev_res)) prev_res = IntTree.Empty () mutable last_update = 0 _ = pool.simplify_matcher_updates.TryGetValue (id, out last_update) unless (Driver.IncrementalSimplifyMatching) last_update = 0 // XXX foreach (p in trigger) def rest = $[(s, null) | s in trigger, s !== p] def visited = Hashtable () mutable skiped = false foreach (t in p.left.parents) def sig = t.right.Root when (t.active && !visited.Contains (sig)) if (t.Root.last_merge >= last_update) visited [sig] = true log (SMATCH, $ "top look into: $t") Decompose (p, t, rest) else skiped = true when (!skiped) break pool.simplify_matcher_updates = pool.simplify_matcher_updates.Replace (id, pool.MatchHeight) pool.simplify_matcher_prev_results = pool.simplify_matcher_prev_results.Replace (id, prev_res) WithHeadAndRoot (head : Term, root : Term) : list [Term] def cache = pool.head_and_root_cache if (root == null) head.parents else mutable ht when (! cache.TryGetValue (head, out ht)) ht = Hashtable () cache [head] = ht foreach (t when t.active in head.parents) ht [t.Root] = t :: ht.GetValueOrDefault (t.Root, []) ht.GetValueOrDefault (root, []) Match (jobs : list [Term * Term]) : void log (SMATCH, $"match: $sigma $jobs") match (jobs) | (p, t) :: jobs => def idx = FindName (p) if (idx >= 0) assert (t != null) if (sigma.vars [idx] == null) sigma.vars [idx] = t Match (jobs) sigma.vars [idx] = null else if (sigma.vars [idx] === t) Match (jobs) else {} else if (p.Arity == 0) assert (t != null) if (p.Root === t) Match (jobs) else {} else def visited = Hashtable () def symbols = WithHeadAndRoot (p.left, t) log (SMATCH, $ "symbols($(p.left),$t) = $symbols") foreach (t in symbols) def sig = t.right.Root when (t.active && !visited.Contains (sig)) log (SMATCH, $ "look into: $t") visited [sig] = true Decompose (p, t, jobs) | [] => mutable term unless (apply_cache.TryGetValue (sigma, out term)) term = sigma.Apply (names, matcher.qatom.Formula) apply_cache [sigma.Clone ()] = term if (prev_res.Contains (term.Id)) log (SMATCH, $ "found match OLD: $names/$sigma $(matcher.qatom.Formula) -> $term") () else log (SMATCH, $ "found match: $names/$sigma $(matcher.qatom.Formula) -> $term") prev_res = prev_res.Add (term.Id, null) matcher.res ::= term