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 class Workaround892 : SCG.IEqualityComparer [list [Term * SubstLite]] public Equals (a : list [Term * SubstLite], b : list [Term * SubstLite]) : bool a.Equals (b) public GetHashCode (a : list [Term * SubstLite]) : int mutable res = 0 mutable some_null = false mutable some_non_null = false mutable last_id = int.MinValue foreach ((t, s) in a) assert (last_id < t.Id) last_id = t.Id unchecked res *= 13 res ^= t.Id if (s != null) some_non_null = true res ^= s.GetHashCode () else some_null = true assert (! (some_null && some_non_null), $"a=$a") res subst_set_cache : SCG.Dictionary [list [Term * SubstLite], SubstLite] = \ SCG.Dictionary (Workaround892 ()) internal EmptySubst : SubstLite [Profile] \ internal MakeSubstLite (children : list [Term * SubstLite]) : SubstLite use_cache (subst_set_cache [children]) SubstLite (this, children) internal merge_cache : Hashtable [SubstLite * list [SubstLite], SubstLite] = Hashtable () public class SubstLite pool : Pool // invariant: list sorted by Term.Id // invariant: each path in the tree, ending with null, has the same height // ==> if one SubstLite is null then are all null children : list [Term * SubstLite] // only called by Pool.MakeSubstLite to make given list of arguments // reference-unique internal this (p : Pool, c : list [Term * SubstLite]) pool = p children = c public override ToString () : string def sb = System.Text.StringBuilder ("{\n") def iter (ind, s) foreach ((t, s) in s.children) _ = sb.Append (ind).Append (t) unless (t.Root === t) _ = sb.Append (" / ").Append (t.Root) _ = sb.Append ('\n') when (s != null) iter (ind + " ", s) iter ("", this) sb.Append ("}").ToString () GetXSubsts (names : list [int] = null, acc : Matcher.XSubst = null) : Hashtable [Matcher.XSubst, object] if (this.children is []) Hashtable () else def height (s) if (s == null) 0 else 1 + height (s.children.Head [1]) def size = height (this) def names = if (names == null) $[0 .. size - 1] else assert (names.Length == size) names def sbst = if (acc == null) Matcher.XSubst (size) else acc def res = Hashtable () this.Iter (names, sbst, a => { assert (! res.Contains (a)); res [a.Clone ()] = null }) res ValidateMerge (others : list [SubstLite], res : SubstLite) : void def h1 = this.GetXSubsts () def h2 = Construct (pool, others).GetXSubsts () def h3 = res.GetXSubsts () foreach (a in h3.Keys) assert (h1.Contains (a) || h2.Contains (a)) foreach (a in h1.Keys) assert (h3.Contains (a)) foreach (a in h2.Keys) assert (h3.Contains (a)) // Return (AND over others) [Profile] \ public static Construct (pool : Pool, others : list [SubstLite]) : SubstLite match (others) | [] => null | [one] => one | _ => def f (s, acc) def cache = Hashtable () def loop (s) def recurse (t, s) if (s == null) (t, loop (s)) else def s' = use_cache (cache [s]) loop (s) (t, s') if (s == null) acc else pool.MakeSubstLite (s.children.Map (recurse)) loop (s) def empty = pool.EmptySubst def others = $[o | o in others, o != null] use_cache (pool.merge_cache [(empty,others)]) others.Rev ().FoldLeft (null, f) // Return (this + (AND over others)) [Profile] \ public TopMerge (others : list [SubstLite]) : SubstLite Merge (others) [Profile] \ public Merge (others : list [SubstLite]) : SubstLite //log (TEMP, $"merge: $this$others") def driver = pool.core.TheDriver driver.num_merges++ unless (others is [_]) driver.num_non_unit_merges++ mutable tmp_res def merge (_) | (a, null, b :: bb) => merge (a, b, bb) | (null, null, []) => null | (null, _, _) => assert (false) | (_, null, _) => assert (false) | (a, b, []) when a === b => a | (a, b, bb) when pool.merge_cache.TryGetValue ((a, b::bb), out tmp_res) => driver.num_merge_hits++ tmp_res | (a, b, bb) => driver.num_merge_misses++ mutable bb' = null def get_bb () when (bb' == null) bb' = Construct (pool, bb) bb' def extend (t, s) if (s == null) (t, get_bb ()) else (t, Construct (pool, [s, get_bb ()])) def loop (_) | (acc, (t1, s1) :: r1, (t2, s2) :: r2) when t1 === t2 => loop ((t1, merge (s1, s2, bb)) :: acc, r1, r2) | (acc, [], r) => pool.MakeSubstLite (r.Map (extend).RevAppend (acc).Rev ()) | (acc, r, []) => pool.MakeSubstLite (r.RevAppend (acc).Rev ()) | (acc, (t1, s1) :: r1, ((t2, _) :: _) as r2) when t1.Id < t2.Id => loop ((t1, s1) :: acc, r1, r2) | (acc, r1, (t2, s2) :: r2) => loop (extend (t2, s2) :: acc, r1, r2) def tmp = loop ([], a.children, b.children) pool.merge_cache[(a,b::bb)] = tmp tmp def res = merge (this, null, others) when (Driver.SelfChecks) ValidateMerge (others, res) res // Return (this \ other) [Profile] \ public Subtract (other : SubstLite) : SubstLite assert (other != null) // XXX don't think this works def cache = Hashtable () def sub (a, b) assert (a != null && b != null) use_cache (cache [(a, b)]) if (a === b) pool.EmptySubst else def loop (_) | (acc, (t1, s1) :: r1, (t2, s2) :: r2) when t1 === t2 => if (s1 == null || s2 == null) assert (s1 == null && s2 == null, $"s1=$s1 s2=$s2") loop (acc, r1, r2) else def s3 = sub (s1, s2) if (s3.children is []) loop (acc, r1, r2) else loop ((t1, s3) :: acc, r1, r2) | (acc, [], _) => pool.MakeSubstLite (acc.Rev ()) | (acc, r, []) => pool.MakeSubstLite (r.RevAppend (acc).Rev ()) | (acc, (t1, s1) :: r1, ((t2, _) :: _) as r2) when t1.Id < t2.Id => loop ((t1, s1) :: acc, r1, r2) | (acc, r1, _ :: r2) => loop (acc, r1, r2) if (b.children is []) a else loop ([], a.children, b.children) def res = sub (this, other) when (Driver.SelfChecks) def h1 = this.GetXSubsts () def h2 = other.GetXSubsts () def h3 = res.GetXSubsts () foreach (k in h3.Keys) assert (h1.Contains (k) && !h2.Contains (k)) foreach (k in h1.Keys) assert (h2.Contains (k) || h3.Contains (k)) res [Profile] \ public Iter (names : list [int], acc : Matcher.XSubst, leaf_fn : Matcher.XSubst -> void, allow_constraints = false) : void def loop (_) | (null, []) => leaf_fn (acc) | (_, []) => assert (false) | (s, n :: ns) => def t' = acc.vars [n] if (t' == null) foreach ((t, s) in s.children) acc.vars [n] = t loop (s, ns) acc.vars [n] = null else //log (TEMP, $"iter look for $(t'.Id)->$(t') $($[t.Id | (t,_) in s.children]) in $s") if (allow_constraints) foreach ((t, s) in s.children) when (t' === t) loop (s, ns) when (t'.Id <= t.Id) break else match (s.children) | [(t, s)] when t === t' => loop (s, ns) | l => assert (false, $"t'=$(t') $l") loop (this, names) // Not efficient, don't use except in opt-in assertions. public PruneJunk (skip_found = false) : SubstLite def prune (s) if (s == null) null else s.PruneJunk (skip_found) def ch = $[(t, prune (s)) | (t, s) in children, t.IsCanon] foreach ((t, s) when !t.IsCanon in children) mutable found = false foreach ((t', s') when t' === t.Root in ch) found = true assert (s == null || s.PruneJunk (skip_found = true).Subtract (s').children is []) unless (skip_found) assert (found, $"t=$t/$(t.Root), $this") def ch = $[(t, s) | (t, s) in ch, s == null || ! (s.children is [])] pool.MakeSubstLite (ch) [Profile] \ public Constrain (names : list [int], acc : Matcher.XSubst) : SubstLite def needed = need_it: def seen = acc.Clone () foreach (n in names) when (seen.vars [n] != null) need_it (true) seen.vars [n] = pool.Star false if (!needed) this else def empty = pool.EmptySubst def cache = Hashtable () def loop (_) | (null, []) => null | (_, []) => assert (false) | (s, (n :: ns) as l) => def pref = $[acc.vars [n] | n in l, acc.vars [n] != null] use_cache (cache [(pref, s)]) def t' = acc.vars [n] //log (TEMP, $"compute: prev=$(t') $n::$ns $s") if (t' == null) mutable res = [] foreach ((t, s) in s.children) acc.vars [n] = t def s = loop (s, ns) if (s === empty) {} else res ::= (t, s) acc.vars [n] = null match (res.Rev ()) | [] => empty | lst => pool.MakeSubstLite (lst) else def s' = found: foreach ((t, s) in s.children) when (t' === t) found (s) when (t'.Id <= t.Id) found (empty) empty if (s' === empty) empty else def s' = loop (s', ns) if (s' === empty) empty else pool.MakeSubstLite ([(t', s')]) def res = loop (this, names) when (Driver.SelfChecks) def h1 = Hashtable () def h2 = Hashtable () res.Iter (names, acc, leaf_fn = h => h1 [h.Clone ()] = null, allow_constraints = false) this.Iter (names, acc, leaf_fn = h => { def h = h.Clone (); assert (h1.Contains (h), $ "$names $h $this -> $res"); h2 [h] = null }, allow_constraints = true) foreach (h in h2.Keys) assert (h1.Contains (h)) res