using System;
using System.Collections.Generic;
using System.Diagnostics;
using System.Linq;
using System.Threading;
using System.Threading.Tasks;
using glue.Debugging;
using glue.Extensions.Enumerable;
using glue.Tasks;
using agree;
namespace agree
{
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
/// <summary>
///
/// </summary>
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
[DebuggerDisplay("#{id}")]
public abstract partial class Unification
{
[DebuggerBrowsable(DebuggerBrowsableState.Never)]
TypeMgr tm;
[DebuggerBrowsable(DebuggerBrowsableState.Never)]
Tray tr_dst;
Dictionary<TfsEdge, UnifCoref> corefs = null;
public Tray TargetTray { get { return tr_dst; } }
public Unification(Tray tr_dst)
{
this.tr_dst = tr_dst;
this.tm = tr_dst.tm;
#if DEBUG
if (Debugger.IsAttached)
id = System.Threading.Interlocked.Increment(ref next_id);
#endif
}
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
/// a unification equivalence class
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
sealed partial class UnifCoref : List<TfsEdge>
{
readonly public List<PoolMark> pmx = new List<PoolMark>();
public Edge Master;
public void AddPm(PoolMark pm)
{
Debug.Assert(!pmx.Contains(pm));
pmx.Add(pm);
}
public void AddPms(IEnumerable<PoolMark> pms)
{
Debug.Assert(!pmx.Intersect(pms).Any());
pmx.AddRange(pms);
}
public void RemovePm(PoolMark pm)
{
bool b = pmx.Remove(pm);
Debug.Assert(b);
}
};
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
///
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
[Flags]
enum Options : byte
{
None = 0,
ForceExpand = 1,
};
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
/// <summary>
/// add the specified edge to the specified equivalence class
/// </summary>
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
void AddTfsMark(UnifCoref uc, TfsEdge te)
{
Debug.Assert(!uc.Contains(te, TfsEdge.TfsMarkComparer.Instance));
corefs[te] = uc;
uc.Add(te);
}
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
/// <summary>
/// when at least one of the two edges is coreferenced, it is always possible to resolve the coreference with no
/// more than one binary unification operation. that is, you'd never have to, say, unify both inputs with an
/// existing equivalence class in two separate operations. see the five cases below.
/// </summary>
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
bool _unify_corefs(Options o, ConstraintPool cp, int m, TfsEdge te1, TfsEdge te2, out Edge e)
{
Debug.Assert(!te1.Equals(te2));
Edge.Flag f1 = te1.Edge.FlagsId, f2 = te2.Edge.FlagsId;
Debug.Assert(((f1 | f2) & Edge.Flag.Coreference) > 0);
UnifCoref uc, uc1 = null, uc2 = null;
if (corefs == null)
corefs = new Dictionary<TfsEdge, UnifCoref>(TfsEdge.TfsMarkComparer.Instance);
else
{
if ((f1 & Edge.Flag.Coreference) != 0)
corefs.TryGetValue(te1, out uc1);
if ((f2 & Edge.Flag.Coreference) != 0)
corefs.TryGetValue(te2, out uc2);
}
/// there are five possible cases when encountering at least one coreference on the two source edges
if (uc1 == null && uc2 == null)
{
Debug.Assert(m != 0);
/// did not pick up any coreference from either edge; start a new one.
#if DEBUG
uc = new UnifCoref(this);
#else
uc = new UnifCoref();
#endif
if ((f1 & Edge.Flag.Coreference) != 0)
AddTfsMark(uc, te1);
if ((f2 & Edge.Flag.Coreference) != 0)
AddTfsMark(uc, te2);
uc.AddPm(new PoolMark(cp, m));
if (!_unify(o, te1, te2, out uc.Master))
return _fail(out e);
e = uc.Master;
AddTfsMark(uc, tr_dst.WrapAsTargetTfs(e));
return true;
}
else if (uc1 == uc2)
{
/// picked up the exact same coreference from the two different edges; not much to do.
if (m != 0)
uc1.AddPm(new PoolMark(cp, m));
e = uc1.Master;
return true;
}
else if (uc2 == null)
{
/// found left side coreference, but not right.
uc = uc1;
if ((f2 & Edge.Flag.Coreference) != 0)
AddTfsMark(uc, te2);
te1 = tr_dst.TargetTfs;
te1.Edge = uc1.Master;
}
else if (uc1 == null)
{
/// found right side coreference, but not left.
Debug.Assert(m != 0); // todo: note: asymmetry
uc = uc2;
if ((f1 & Edge.Flag.Coreference) != 0)
AddTfsMark(uc, te1);
te2 = tr_dst.TargetTfs;
te2.Edge = uc2.Master;
}
else
{
/// merge existing left and right coreferences.
uc = uc1;
uc.AddPms(uc2.pmx);
foreach (TfsEdge te_xfer in uc2)
AddTfsMark(uc, te_xfer);
te1 = te2 = tr_dst.TargetTfs;
te1.Edge = uc1.Master;
te2.Edge = uc2.Master;
}
if (m != 0)
uc.AddPm(new PoolMark(cp, m));
if (!_unify(o, te1, te2, out uc.Master))
return _fail(out e);
e = uc.Master;
Debug.Assert(uc.Contains(tr_dst.WrapAsTargetTfs(e), TfsEdge.TfsMarkComparer.Instance));
return true;
}
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
/// <summary>
/// unify.
/// </summary>
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
unsafe bool _unify(Options o, TfsEdge te1, TfsEdge te2, out Edge e)
{
Debug.Assert(!te1.Equals(te2));
/// find the best mark to recycle if one or more of the input TFSs are within the target TFS
int m1 = te1.Edge.Mark;
int m2 = te2.Edge.Mark;
Debug.Assert(te1.Edge.Mark != te2.Edge.Mark || te1.Edge.Mark == 0 || te1.TfsId != te2.TfsId);
int m = 0;
Edge.Flag nf, f1 = te1.Edge.FlagsId, f2 = te2.Edge.FlagsId;
bool b1, tgt1 = (te1.ttid & 0xFFFFFFC0) == Tray.TargetId, tgt2 = (te2.ttid & 0xFFFFFFC0) == Tray.TargetId;
// ensure that, a destructive input TFS--if any--is on the left. swap if necessary.
if ((m1 | m2) != 0)
{
if (tgt1)
{
m = m1;
if (m2 == 0 || !tgt2)
goto done;
else if (m1 == 0)
goto swap;
else if ((f2 & Edge.Flag.Coreference) == 0 || (f1 & Edge.Flag.Coreference) != 0)
goto done;
}
else if (!tgt2)
goto done;
swap:
{
TfsEdge te = te2;
te2 = te1;
te1 = te;
/// swap done, reload
m = m1 = m2;
m2 = te2.Edge.Mark;
f1 = f2;
f2 = te2.Edge.FlagsId;
b1 = tgt2;
tgt2 = tgt1;
tgt1 = b1;
}
}
done:
if ((f1 & Edge.Flag.EtmMask) == Edge.Flag.EtmString || (f2 & Edge.Flag.EtmMask) == Edge.Flag.EtmString)
return tm.strings.Unify(m, te1.Edge, te2.Edge, tr_dst, out e);
/// find glb of the types of the two TFS nodes
int tid1 = (int)(f1 & tm.MultiIdMask);
int tid2 = (int)(f2 & tm.MultiIdMask);
if (tid2 == 0 || tid1 == tid2)
nf = f1;
else if (tid1 == 0)
nf = f2;
else
{
int k = tid1 > tid2 ? (tid2 << tm.c_t_bits) + tid1 : (tid1 << tm.c_t_bits) + tid2;
TypeMgr.GlbCacheEntry[] rge = tm.glb_cache[k % TypeMgr.GLB_CACHE_ENTRIES];
TypeMgr.GlbCacheEntry gce;
if (rge != null)
{
int gk, i = 0;
do
if ((gk = (gce = rge[i]).k) == k)
goto got_glb;
while (gk < k && ++i < rge.Length);
}
tm.ComputeAndCacheGlb(tid1, tid2, out gce.f);
got_glb:
if ((nf = gce.f) == Edge.Flag.CachedBottom)
return _fail(out e);
}
Debug.Assert(tm.GetEdgeType(nf).IsBare == ((nf & Edge.Flag.EtmNonBareType) == 0));
/// create new edge, generating a new mark if one is needed because the type is non-bare or the edge is coreferenced
nf |= ((f1 | f2) & Edge.Flag.Coreference);
e = tr_dst.CreateRecycledEdge(nf, m);
if ((nf & Edge.Flag.EtmNonBareType) != 0)
{
/// Type has features and now has a non-zero mark.
m = e.Mark;
Debug.Assert(m != 0 && m != m2);
/// if the marks are equal (and not in cloned TFSes), they must both be 0, a case of non-bare GLB result
Debug.Assert(m1 != m2 || m1 == 0 || te1.TfsId != te2.TfsId);
TfsEdge nte1 = te1;
TfsEdge nte2 = te2;
Edge* pne1 = &nte1.Edge;
Edge* pne2 = &nte2.Edge;
if (m1 == 0) *pne1 = default(Edge);
if (m2 == 0) *pne2 = default(Edge);
Edge ne;
ConstraintPool[] rgcp = tm.rgcp_by_type[(int)(nf & tm.MultiIdMask)];
foreach (ConstraintPool cp in rgcp)
{
b1 = m1 != 0 && cp.TryGetEdge(m1, out *pne1);
if ((m2 != 0 && cp.TryGetEdge(m2, out *pne2)) || b1)
{
#if DEBUG
ne = default(Edge);
#endif
if (*(ulong*)pne1 == *(ulong*)pne2)
{
if (pne1->Mark == 0)
{
ne = *pne1;
goto opt;
}
else if (tgt1 & tgt2)
{
Debug.Assert(pne1->IsCoreferenced);
ne = *pne1;
goto opt;
}
else if (!pne1->IsCoreferenced)
{
ne = tr_dst.CreateEdge(pne1->FlagsId);
goto opt;
}
}
// the following is not the case when picking up non-persisted corefs from m1!=m2 retrieving
// identical non-zero marks with different types
//Debug.Assert(pne1->Mark == 0 || pne1->Mark != pne2->Mark);
if (((pne1->FlagsId | pne2->FlagsId) & Edge.Flag.Coreference) != 0)
{
if (m == m1 && (pne1->FlagsId & Edge.Flag.Coreference) != 0)
{
if (!_unify_corefs(o, null, 0, nte1, nte2, out ne))
goto cleanup_fail;
}
else
{
if (!_unify_corefs(o, cp, m, nte1, nte2, out ne))
goto cleanup_fail;
}
}
else if (!_unify(o, nte1, nte2, out ne))
goto cleanup_fail;
opt:
/// If the result is not one of the input types and it has features, or if we are expanding the type
/// hierarchy, unify with the constraints on the type
if ((ne.FlagsId & Edge.Flag.EtmNonBareType) != 0)
{
int ntid = (int)(ne.FlagsId & tm.MultiIdMask);
Debug.Assert(ntid != tm.StringId);
if ((o & Options.ForceExpand) > 0 ||
((int)(pne1->FlagsId & tm.MultiIdMask) != ntid && (int)(pne2->FlagsId & tm.MultiIdMask) != ntid))
{
/// the following can change the edge
if (!_unify(Options.None, tr_dst.WrapAsTargetTfs(ne), tm.type_arr[ntid].Expanded.Clone(), out ne))
goto cleanup_fail;
}
}
/// persist the new edge.
if (ne.FlagsId == 0)
{
/// ...or remove it if destructive
if (m == m1)
cp.RemoveEdge(m);
}
else if (m != m1 || *(ulong*)&ne != *(ulong*)pne1)
cp.SetEdge(m, ne);
/// if destructive in the target, remove the edge that wasn't retained
if (m2 != 0 && tgt2)
{
Debug.Assert(m == m1);
if (pne2->IsCoreferenced)
corefs[nte2].RemovePm(new PoolMark(cp, m2));
cp.RemoveEdge(m2);
}
continue;
cleanup_fail:
foreach (ConstraintPool dcp in rgcp)
{
/// if non-destructive, we only have to clean up for as far as we progressed.
if (m != m1 && dcp == cp)
break;
if (dcp.TryRemoveEdge(m, out ne) && ne.Mark != 0)
tr_dst.RudeTruncate(ne);
}
return false;
}
}
}
return true;
}
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
/// <summary>
///
/// </summary>
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
void _persist_coref_edges()
{
if (corefs == null)
return;
foreach (var tfsc in corefs.Values.Distinct())
{
Edge e = tfsc.Master;
foreach (PoolMark pm in tfsc.pmx)
pm.Pool.SetEdge(pm.in_mark, e);
}
}
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
/// <summary>
///
/// </summary>
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
public void _remove_vacuous_corefs()
{
if (corefs == null)
return;
//var to_remove = corefs.Values.Where(cr => cr.pmx.Count == 1).ToArray();
foreach (var tfsc in corefs.Values.Distinct()/*.ToArray()*/)
{
//Debug.Assert(tfsc.pmx.Count > 0);
if (tfsc.pmx.Count == 1)
{
tr_dst.ChangeEdgeCoreference(tfsc.pmx.First(), false);
tfsc.pmx.Clear();
}
}
}
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
/// <summary>
///
/// </summary>
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
public partial class Expander : Unification
{
public Expander(Tray target_tray) : base(target_tray) { }
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////
///
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////
public bool ExpandEntry(TfsEdge te_def, TfsEdge te_inst_type_exp, out TfsEdge result)
{
result = tr_dst.CreateTfs(default(Edge));
if (!_unify(Options.ForceExpand, te_def, te_inst_type_exp, out result.Edge))
return false;
if (corefs != null)
{
_persist_coref_edges();
_remove_vacuous_corefs();
}
return true;
}
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////
///
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////
public bool ExpandType(Type host_type, out TfsEdge result)
{
#if DEBUG
_t_exp = host_type;
#endif
result = host_type.Definition;
if ((host_type.m_flags & Type.Flags.HasAnyFeatures) == 0)
return true;
Type[] iea = host_type.Parents.Where(p => p.HasAnyFeatures).ToArray();
/// If the conjoined parents are distinct as they should be, then we don't need to clone the top level
/// TFSs and we will only clone interior usages.
Debug.Assert(iea.IsDistinct());
if (iea.Length == 0)
iea = tm.rgt_top_singleton;
for (int i = 0; i < iea.Length; i++)
{
if (!_unify(Options.ForceExpand, result, iea[i].Expanded, out result.Edge))
return _fail(out result);
if (i == 0)
result = tr_dst.WrapAsTargetTfs(result.Edge);
}
if (corefs != null && corefs.Count > 0)
{
_persist_coref_edges();
_remove_vacuous_corefs();
}
/// don't return a target TFS or really weird stuff will happen
Debug.Assert(result.IsTarget);
result = tr_dst.CreateTfs(result.Edge);
return true;
}
};
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
/// <summary>
///
/// </summary>
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
public class Checker : Unification
{
public Checker(Tray target_tray) : base(target_tray) { }
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////
///
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////
public bool Check(TfsEdge te1, TfsEdge te2)
{
Edge e;
// todo: consider the ability to set destination mark to -1 such that we never switch to destructive
// unify, and don't write out any edges. is this possible without n-way? seems like coreferencing might
// need 'scratch' space, except in the n-way approach
if (!_unify(Options.None, te1, te2, out e))
return false;
tr_dst.RudeTruncate(e);
return true;
}
};
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
/// <summary>
///
/// </summary>
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
public class Unifier : Unification
{
public Unifier(Tray target_tray) : base(target_tray) { }
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////
///
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////
public bool Unify(TfsEdge te1, TfsEdge te2, out Edge result)
{
if (!_unify(Options.None, te1, te2, out result))
return false;
if (corefs != null)
{
_persist_coref_edges();
//_remove_vacuous_corefs();
}
return true;
}
};
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
/// <summary>
/// todo: decide if we want to resurrect this
/// </summary>
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
public class Async : Unifier
{
public Async(Tray target_tray) : base(target_tray) { }
public Task CleanupTask { get { return Tasks.CompletedTask; } }
public Task ResultTask { get { return Tasks.CompletedTask; } }
public void Fail() { }
public Task<Edge> UnifyAsync(TfsEdge e1, TfsEdge e2) { throw new InvalidOperationException(); }
};
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
/// <summary>
///
/// </summary>
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
public class Partial : Async
{
public Partial(Tray target_tray) : base(target_tray) { }
int e_daughter_mark;
Edge e_partial;
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////
/// <summary>
///
/// </summary>
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////
public void CompleteSkeleton(TfsEdge mother, TfsEdge daughter, Edge partial, out Edge result)
{
Debug.Assert(corefs != null);
//Debug.Assert(tfs_id != Tray.TargetId);
Debug.Assert(ResultTask.IsCompleted);
this.e_daughter_mark = daughter.Edge.Mark;
this.e_partial = partial;
/// Copy remainder to the destination tray
result = tr_dst.ShallowCopyEdge(mother.Edge);
_copy_remainder(mother, result);
}
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////
/// <summary>
///
/// </summary>
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////
void _copy_remainder(TfsEdge te_src, Edge e_dst)
{
ConstraintPool[] rgcp_src = ((te_src.ttid ^ tr_dst.tix) & 0x3F) == 0 ? tr_dst.Pools : te_src.Tray.Pools;
int m = te_src.Edge.Mark;
#if DEBUG
TfsEdge te_original_source = te_src;
foreach (int fix in te_original_source.Type._deprec_feat_indexes)
#else
foreach (int fix in te_src.Type._deprec_feat_indexes) // todo
#endif
{
ConstraintPool cp = rgcp_src[fix];
if (cp.TryGetEdge(m, out te_src.Edge))
{
Edge ne_dst;
if ((te_src.Edge.FlagsId & Edge.Flag.Coreference) > 0)
{
UnifCoref tfsc;
if (corefs.TryGetValue(te_src, out tfsc))
ne_dst = tfsc.Master;
else
{
if (te_src.Edge.Mark == e_daughter_mark)
ne_dst = e_partial;
else
{
ne_dst = tr_dst.ShallowCopyEdge(te_src.Edge);
_copy_remainder(te_src, ne_dst);
}
#if DEBUG
tfsc = new UnifCoref(this);
#else
tfsc = new UnifCoref();
#endif
tfsc.Master = ne_dst;
corefs.Add(te_src, tfsc);
corefs.Add(tr_dst.WrapAsTargetTfs(tfsc.Master), tfsc);
}
tfsc.AddPm(new PoolMark(cp, e_dst.Mark));
}
else if (te_src.Edge.Mark == e_daughter_mark)
{
ne_dst = e_partial;
}
else if (te_src.Edge.Mark == Edge.MarkBare)
{
ne_dst = te_src.Edge;
}
else
{
ne_dst = tr_dst.ShallowCopyEdge(te_src.Edge);
_copy_remainder(te_src, ne_dst);
}
if (tr_dst.Pools != rgcp_src)
cp = tr_dst.Pools[fix];
cp.SetEdge(e_dst.Mark, ne_dst);
}
else
Debug.Assert(!cp.ContainsInMark(e_dst.Mark));
}
}
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////
/// <summary>
///
/// </summary>
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////
public bool UnifyAndComplete(TfsEdge mother, TfsEdge daughter, TfsEdge candidate, out TfsEdge full)
{
Edge e, partial;
if (!Unify(daughter, candidate, out partial))
{
full = default(TfsEdge);
return false;
}
CompleteSkeleton(mother, daughter, partial, out e);
full = tr_dst.CreateTfs(e);
return true;
}
};
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
/// <summary>
///
/// </summary>
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
public class Pruning : Partial
{
public Pruning(Tray target_tray) : base(target_tray) { }
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////
/// <summary>
/// Prune a sub-graph, and then remove any unused coreferences (and unmark the edge coreference bit) which
/// have only a single use remaining.
/// </summary>
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////
public void PruneBelow(ConstraintPool cp, int m)
{
if (_prune_below(cp, m))
cp.SetEdge(m, Edge.PrunedEdge);
//_remove_vacuous_corefs();
}
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
/// <summary>
/// This differs from Tray.RudeTruncate because this is smart about not pruning into coreference subtrees that
/// are still needed
/// </summary>
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
public bool _prune_below(ConstraintPool cp, int m)
{
Edge ne;
if (!cp.TryGetEdge(m, out ne))
return false;
if (ne.IsCoreferenced)
{
/// remove an edge that leads to this coreference...
UnifCoref coref = corefs[tr_dst.WrapAsTargetTfs(ne)];
coref.RemovePm(new PoolMark(cp, m));
/// ...but only remove below it if that was its last use. This allows sub-graphs to
/// be pruned without disturbing the coreferenced portions that are still accessible
/// from without.
if (coref.pmx.Count > 0)
goto skip_subtree_pruning;
}
if (ne.Mark != 0 && (ne.FlagsId & Edge.Flag.EtmNonBareType) != 0)
{
foreach (ConstraintPool ncp in tm.rgcp_by_type[tm.GetEdgeTypeId(ne.FlagsId)])
_prune_below(ncp, ne.Mark);
}
skip_subtree_pruning:
cp.RemoveEdge(m);
return true;
}
};
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
/// <summary>
///
/// </summary>
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
bool _fail()
{
Async a = this as Async;
if (a != null)
a.Fail();
return false;
}
public bool _fail(out Edge e)
{
e = default(Edge);
return _fail();
}
public bool _fail(out TfsEdge te)
{
te = default(TfsEdge);
return _fail();
}
};
}