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 internal trees : Hashtable [Term, SubTriggerMarker.TriggerTree] = Hashtable () internal indexed_triggers_by_head : Hashtable [Term, list [Term]] = Hashtable () internal indexed_triggers : Hashtable [Term, object] = Hashtable () internal prev_results : Hashtable [Term * IntTree [SubstLite], SubstLite] = Hashtable () internal class SubTriggerMarker //linear triggers have all variables different, so there's no need for using a tree //there is also no need to remember the variables' names //which has a benefit of possibility to reuse results for subtriggers differing only //by names of variables !:) // We however do want the results in SubstLite to be unique, therefore a tree structure // for remembering lists of terms is used #region trigger tree mutable indexing_done : bool internal variant TriggerTree | Node children : list [Term * TriggerTree] | Leaf trigger : Term public static Add (th : TriggerTree, trig : Term) : TriggerTree def loop (_) | (null, t :: ts) => Node ([(t, loop (null, ts))]) | (null, []) => Leaf (trig) | (Node (ch), t :: ts) => if (ch.Exists ((t', _) => t' === t)) Node (ch.Map ((t', n) => if (t' === t) (t, loop (n, ts)) else (t', n))) else Node ((t, loop (null, ts)) :: ch) | (Leaf (trig') as n, []) => assert (trig' === trig) n | _ => assert (false) loop (th, trig.Children) [Profile] \ public PrepareTrigger (t : Term) : void def IsConst (trigger : Term) : bool mutable ok = true trigger.Iter (fun (t) { ok = ok && !t.IsStar }) ok def IsFlat (t : Term) : bool t.Children.ForAll (t => IsConst (t) || t.IsStar) && t.Children.Exists (_.IsStar) assert (!indexing_done) when (!Driver.FlatMatching) return when (!pool.indexed_triggers.Contains (t) && IsFlat (t)) pool.indexed_triggers [t] = null when (! pool.indexed_triggers_by_head.Contains (t.left)) pool.indexed_triggers_by_head [t.left] = [] pool.indexed_triggers_by_head [t.left] ::= t if (pool.trees.Contains (t.left)) pool.trees [t.left] = TriggerTree.Add (pool.trees [t.left], t) else pool.trees [t.left] = TriggerTree.Add (null, t) #endregion // proofs[t][x] = list of substitutions making x to be equal to t // proofs[t][x].Apply (t) == x [Accessor] \ mutable proofs : IntTree [IntTree [SubstLite]] = IntTree.Empty () mutable done : Hashtable [Term, bool * IntTree [SubstLite]] = Hashtable () mutable proofs_updated_at : int internal is_partial : bool core : Core pool : Pool fake : bool fake_str : string static const_tree : IntTree [SubstLite] = IntTree.Empty ().Add (int.MaxValue, null) internal this (p : Pool, is_partial : bool, fake = false) pool = p core = p.core proofs = p.matcher_proofs proofs_updated_at = p.matcher_proofs_updated_at this.is_partial = is_partial fake_str = "" when (fake) proofs = IntTree.Empty () proofs_updated_at = 0 this.fake = true fake_str = "fake " internal SaveUpdates () : void if (is_partial) mutable updates = pool.matcher_partial_updates foreach (t in done.Keys) updates = updates.Replace (t.Id, pool.MatchHeight) pool.matcher_partial_updates = updates else pool.matcher_proofs_updated_at = pool.MatchHeight pool.matcher_partial_updates = IntTree.Empty () //extracts stars' names in the same order FindSubTriggerMatches matches them internal ExtractStarsNames(sub : Subst, subtrigger : Term) : list [int] if (sub.Contains (subtrigger.Id)) [subtrigger.Id] else if(subtrigger.left==null) [] else def concatsubs (_,t,substitutions) ExtractStarsNames(sub,t)+substitutions subtrigger.FoldIndexedChildren([],concatsubs) enum Result | Star | Constant | Match | NoMatch | NothingNew // ---------------------------------------------------------------------------- // The regular subtrigger recursive matcher // ---------------------------------------------------------------------------- [Profile] \ SubTriggerRec (subtrigger : Term) : Result * IntTree [SubstLite] log (SUBT, $ "SubTriggerRec ($subtrigger)") core.TheDriver.subtrigger_misses++ //indices used by reqursive Find... def indices = array(subtrigger.Arity) //easy access to children of subtrigger def children = array(subtrigger.Arity) def subproofs = array(subtrigger.Arity) //if subtrigger has no stars it can be matched faster mutable is_const=true //if one of the subtriggers is impossible, then so are we mutable impossible=false def remember_index (idx, t, _) // memoize index used for child when(!impossible) (indices [idx], subproofs [idx]) = FindSubTriggerMatches (t) is_const = is_const && indices [idx] == Result.Constant impossible = impossible || indices [idx] == Result.NoMatch children [idx] = t null _ = subtrigger.FoldIndexedChildren ( null, remember_index ) if(is_const) // subtrigger.MakeActive () done [subtrigger] = (false, const_tree) (Result.Constant, const_tree) else if(impossible) done [subtrigger] = (false, IntTree.Empty ()) (Result.NoMatch, IntTree.Empty ()) // there is no match for sure else //checks if t matches idx-th child of subtrigger def matches_child (idx, t, substitutions) if (substitutions == null) null else //log (SUBT, $ "idx=$idx, t=$t, subs=$substitutions") match( indices[idx] ) | Result.Star => //star always matches (and t has no stars since it's active) pool.MakeSubstLite ([(t.Root, null)]) :: substitutions | Result.Constant => //constant matches only other constants from its eqivalence class children[idx].MakeActive () if(t.SameAs (children[idx])) substitutions else null | _ => def proof = subproofs [idx] assert (proof != null) mutable assignments if (proof.TryGetValue (t.Root.Id, out assignments)) log (SUBT, $"childmatch: $t $(t.Root), hit -> $assignments") assignments :: substitutions else log (SUBT, $"childmatch: $t $(t.Root), miss") null //in this representation the head of the real term is on the left def symbol=subtrigger.left //one of these terms must match subtrigger to make whole eqiv. class match the subtrigger def terms_with_good_head= symbol.parents mutable our_proof mutable last_update if (!fake && proofs.TryGetValue (subtrigger.Id, out our_proof)) if (Driver.LastMerge && pool.matcher_partial_updates.TryGetValue (subtrigger.Id, out last_update)) {} else last_update = proofs_updated_at when (Driver.FnLastMerge && symbol.last_merge < last_update) done [subtrigger] = (false, our_proof) return (Result.NothingNew, our_proof) else our_proof = IntTree.Empty () last_update = 0 def initial_proof = if (last_update == 0) null else our_proof //log (TEMP, $"t=$subtrigger our_proof[$last_update/$proofs_updated_at]=$our_proof ") impossible = our_proof.IsEmpty def visited = Hashtable () mutable anything = false log (SUBT, $"class last merge: $(symbol.last_merge)") foreach (t in terms_with_good_head) when(t.active) if (t.Root.last_merge >= last_update) core.TheDriver.subtrigger_sub_misses++ else core.TheDriver.subtrigger_sub_hits++ log (SUBT, $"rec-checking $t [Root=$(t.Root.Id)/$(t.Root)] act=$(t.active) last_merge: $(t.Root.last_merge) (vs $last_update)") when(t.active && t.Root.last_merge >= last_update) anything = true def sig = t.right.Root when (!visited.Contains (sig.Id)) visited [sig.Id] = true //log (SUBT, $"subcmp: $subtrigger $t ?") match(t.FoldIndexedChildren([], matches_child)) | null => log (SUBT, "--> checked/miss") () | substitutions => log (SUBT, $"--> checked/hit, $substitutions") impossible=false //log (SUBT, $"subcmp: $subtrigger $t => OK") mutable prev_substitutions if(our_proof.TryGetValue (t.Root.Id, out prev_substitutions)) def new_sub = prev_substitutions.Merge (substitutions) unless (new_sub === prev_substitutions) our_proof = our_proof.Replace (t.Root.Id, new_sub) else our_proof = our_proof.Add (t.Root.Id, SubstLite.Construct (pool, substitutions)) if (anything) core.TheDriver.subtrigger_anything++ else core.TheDriver.subtrigger_nothing++ if (our_proof === initial_proof) done [subtrigger] = (false, our_proof) else done [subtrigger] = (true, our_proof) proofs = proofs.Replace (subtrigger.Id, our_proof) if (impossible) (Result.NoMatch, our_proof) else if (initial_proof === our_proof) (Result.NothingNew, our_proof) else (Result.Match, our_proof) // ---------------------------------------------------------------------------- // Matcher for flat triggers // ---------------------------------------------------------------------------- [Record] \ class FlatTrigger public initial_proof : IntTree [SubstLite] public mutable our_proof : IntTree [SubstLite] public last_update : int [Profile] \ SubTriggerFlat (subtrigger : Term) : void log (SUBT, $ "SubTriggerFlat ($subtrigger)") def triggers = Hashtable () mutable min_update = proofs_updated_at //log (TEMP, $"indexed: $(pool.indexed_triggers_by_head [subtrigger.left])") def flats = pool.indexed_triggers_by_head [subtrigger.left] // Doesn't seem to do any good //when (flats is [_]) // _ = SubTriggerRec (subtrigger) // return foreach (t in flats) core.TheDriver.subtrigger_flats++ mutable tmp2 if (proofs.TryGetValue (t.Id, out tmp2)) // XXX not sure if looking into matcher_partial_updates is worth it mutable update if (pool.matcher_partial_updates.TryGetValue (t.Id, out update)) {} else update = proofs_updated_at triggers [t] = FlatTrigger (tmp2, tmp2, update) else triggers [t] = FlatTrigger (null, IntTree.Empty (), 0) min_update = 0 foreach (c in t.Children) unless (c.IsStar) c.MakeActive () def find_triggers (_) | (t, lst, c :: cc) => //log (TEMP, $"lst=$lst") find_triggers (t, $[n | Node (ch) in lst, (t, n) in ch, t.IsStar || t.Root === c.Root], cc) | (t, lst, []) => //log (TEMP, $"lst=$lst") def children = t.Children foreach (TriggerTree.Leaf (trig) in lst) //log (TEMP, $"check: $trig for $t") def flat = triggers [trig] when (t.Root.last_merge >= flat.last_update) //log (TEMP, $"check: $flat $(flat.our_proof)") def subst = List.FoldLeft2 (trig.Children, children, null, (trig, c, subst) => if (trig.IsStar) pool.MakeSubstLite ([(c.Root, subst)]) else { assert (c.Root === trig.Root); subst }) mutable prev_substitutions if (flat.our_proof.TryGetValue (t.Root.Id, out prev_substitutions)) def new_sub = prev_substitutions.Merge ([subst]) unless (new_sub === prev_substitutions) flat.our_proof = flat.our_proof.Replace (t.Root.Id, new_sub) else flat.our_proof = flat.our_proof.Add (t.Root.Id, subst) //log (TEMP, $"stop check") def visited = Hashtable () def root = pool.trees [subtrigger.left] log (SUBT, $"last_merge: $(subtrigger.left.last_merge), last_update: $min_update") when (!Driver.FnLastMerge || subtrigger.left.last_merge >= min_update) mutable anything = false foreach (t in subtrigger.left.parents) log (SUBT, $"flat-checking $t [Root=$(t.Root.Id)/$(t.Root)] act=$(t.active) last_merge: $(t.Root.last_merge)") when (t.active && t.Root.last_merge >= min_update) anything = true def sig = t.right.Root when (!visited.Contains (sig.Id)) visited [sig.Id] = true find_triggers (t, [root], t.Children) if (anything) core.TheDriver.subtrigger_anything++ else core.TheDriver.subtrigger_nothing++ foreach (t in flats) def d = triggers [t] if (d.our_proof === d.initial_proof) done [t] = (false, d.our_proof) else done [t] = (true, d.our_proof) proofs = proofs.Replace (t.Id, d.our_proof) // ---------------------------------------------------------------------------- // Main subtrigger entry // ---------------------------------------------------------------------------- [Profile] \ FindSubTriggerMatches (subtrigger : Term) : Result * IntTree [SubstLite] log (SUBT, $ "FindSubTrigger $fake_str($subtrigger)") def res = if(subtrigger.IsStar) (Result.Star, null) else if (subtrigger.left==null) //is constant (Result.Constant, null) else //is application mutable tmp if (done.TryGetValue (subtrigger, out tmp)) def (is_new, the_proof) = tmp core.TheDriver.subtrigger_hits++ if (the_proof.IsEmpty) (Result.NoMatch, the_proof) else if (the_proof === const_tree) (Result.Constant, the_proof) else if (is_new) (Result.Match, the_proof) else (Result.NothingNew, the_proof) else if (!fake && pool.indexed_triggers.Contains (subtrigger)) indexing_done = true SubTriggerFlat (subtrigger) FindSubTriggerMatches (subtrigger) // will use the cache else //we have to go the hard way... SubTriggerRec (subtrigger) log (SUBT, $ "end FindSubTrigger $fake_str($subtrigger) => $res") res [Profile] \ internal TriggerMatches (trigger : Term, star_trigger : Term) : SubstLite def empty = pool.EmptySubst if (trigger === star_trigger) null else core.TheDriver.num_matchings++ def (idx, proof) = FindSubTriggerMatches (star_trigger) log (SUBT, $"FindSubTriggerMatches $fake_str($star_trigger): $idx, $proof") mutable tmp if (idx == Result.NoMatch) empty else if (pool.prev_results.TryGetValue ((star_trigger, proof), out tmp)) log (SUBT, $"TriggerMatches: From cache: $tmp") tmp else //trigger should not be a constant, nor consist only of stars assert (idx == Result.Match || idx == Result.NothingNew, $ "invalid trigger: $trigger") def res = proof.Fold (empty, (_, v, substs) => if (substs === empty) v else substs.TopMerge ([v])) when (pool.prev_results.Count > 10000) pool.prev_results.Clear () // keep it small pool.prev_results [(star_trigger, proof)] = res res