using System;
using System.Diagnostics;
using System.Linq;
using miew.Debugging;
namespace agree
{
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////
/// <summary>
/// N-way unification testing
/// </summary>
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////
#if DEBUG
public unsafe class NWayCheck
#else
public unsafe struct NWayCheck
#endif
{
const sbyte TfsCheckBottom = -1;
const sbyte TfsCheckOk = 0;
const int CorefsMax = 500;
const int ArgArityMax = 11;
const int CorefArityMax = 20;
const int MaxParticipants = 16; // (13)
[DebuggerBrowsable(DebuggerBrowsableState.Never)]
int[][] rgrgfix;
[DebuggerBrowsable(DebuggerBrowsableState.Never)]
TypeMgr tm;
Tfs[] participants;
[DebuggerBrowsable(DebuggerBrowsableState.Never)]
byte c_participants;
[DebuggerBrowsable(DebuggerBrowsableState.Never)]
NwayArgs* _corefs, pc_next;
[DebuggerBrowsable(DebuggerBrowsableState.Never)]
NwayArgs** ppmb_next, pp_map_base;
[DebuggerBrowsable(DebuggerBrowsableState.Never)]
NwayArgs*** participant_bases;
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////
/// <summary>
///
/// </summary>
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////
public NWayCheck(TypeMgr tm)
#if !DEBUG
: this()
#endif
{
this.tm = tm;
this.rgrgfix = tm.rgrgfix_by_type;
this.participants = new Tfs[MaxParticipants];
}
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////
/// <summary>
/// n-way unification : locates and traverses a unilateral, type-compatible monotonic descent, if one exists, through
/// any number of internally coreferenced typed feature structures (TFS).
/// </summary>
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////
public bool _check(NwayArgs* pnwa_in)
{
NwayArgs nwa;
foreach (int i_feat in rgrgfix[(int)(pnwa_in->f & Edge.Flag.MultiIdMask)])
{
bool f_expand = false;
NwayArgs* pc = null;
NwayArgs* pnwa = &nwa;
pnwa->c_args = 0;
pnwa->f = 0;
for (int nm, i = 0; i < pnwa_in->c_args; i++)
{
byte tfsix = pnwa_in->rg_tfsix[i];
Tfs tfs = participants[tfsix];
Edge.Flag nf = tfs.TryGetFlagsMark(i_feat, pnwa_in->marks[i], out nm);
if (nf == 0)
continue;
nf = nf & ~(Edge.Flag.Coreference | Edge.Flag.PrunedDuringParsing);
if (pnwa->f == 0 || pnwa->f == nf)
{
pnwa->f = nf;
f_expand = false;
}
else if (nf != 0)
{
Edge.Flag prev = pnwa->f;
pnwa->f = tm.UnifyTypesNoCoref(prev, nf);
if (pnwa->f == Edge.Flag.Bottom)
return false;
if (pnwa->f == nf)
f_expand = false;
else if (pnwa->f != prev)
f_expand = true;
/* note: if (f == prev), retain previous f_expand state */
}
if (nm < 0)
{
NwayArgs* pc_cur = participant_bases[tfsix][~nm];
if (pc_cur == null)
{
byte c_remain = tfs.coref_tally_map[~nm];
Debug.Assert(c_remain > 0);
// orphan corefs (m<0) are not added to coref table. thus, it is not an error for
// a negative mark to appear in the nwa
if (c_remain <= 1)
goto coref_bit_false_positive;
if (pc == null)
{
// nwa can have orphan marks (m<0)
Debug.Assert(tfsix < c_participants);
pc = participant_bases[tfsix][~nm] = pc_next++;
if (nwa.c_args == 0)
pc->f = nwa.f;
else
*pc = nwa;
pc->c_remain = c_remain;
pnwa = pc;
}
else
{
pc->c_remain += c_remain;
participant_bases[tfsix][~nm] = pc;
}
}
else
{
if (!tm.UnifyInTypeNoCoref(ref pnwa->f, pc_cur->f))
return false;
if (pc == null)
{
pc = pc_cur;
pc->f = nwa.f;
pnwa = pc;
for (byte j = 0; j < nwa.c_args; j++)
AddResumePoint(pnwa, nwa.rg_tfsix[j], nwa.marks[j]);
}
else if (pc != pc_cur)
{
pc->c_remain += pc_cur->c_remain;
pc_cur->c_remain = 0;
for (byte j = 0; j < pc_cur->c_args; j++)
{
byte _tfsix = pc_cur->rg_tfsix[j];
int _m = pc_cur->marks[j];
AddResumePoint(pnwa, _tfsix, _m);
if (_m < 0)
participant_bases[_tfsix][~_m] = pc;
}
}
}
Debug.Assert(pc->c_remain > 0);
pc->c_remain--;
}
coref_bit_false_positive:
if (nm != 0)
{
//CheckAddResumePoint(pnwa, tfsix, nm);
for (byte j = 0; j < pnwa->c_args; j++)
if (pnwa->marks[j] == nm && pnwa->rg_tfsix[j] == tfsix)
goto ah3;
byte ii = pnwa->c_args++;
pnwa->rg_tfsix[ii] = tfsix;
pnwa->marks[ii] = nm;
ah3:
;
}
}
if (f_expand && (pnwa->f & Edge.Flag.EtmNonBareType) != 0)
{
Tfs tfs_exp = tm.type_arr[(int)(pnwa->f & Edge.Flag.MultiIdMask)].Expanded;
Debug.Assert(!(tfs_exp is BareTfs));
AddResumePoint(pnwa, AddTfs(tfs_exp), tfs_exp.Edge.Mark);
}
if (pnwa->c_args != 0 && (pc == null || pc->c_remain == 0) && (pnwa->f & Edge.Flag.EtmNonBareType) != 0)
{
if (!_check(pnwa))
return false;
}
}
return true;
}
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////
/// <summary>
///
/// </summary>
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////
void AddResumePoint(NwayArgs* pnwa, byte tfsix, int m)
{
Debug.Assert(m != 0);
Debug.Assert(tfsix < c_participants);
if (pnwa->c_args >= ArgArityMax)
throw new NotImplementedException(String.Format("need n-way arg arity {0}", pnwa->c_args + 1));
byte i = pnwa->c_args++;
pnwa->rg_tfsix[i] = tfsix;
pnwa->marks[i] = m;
}
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////
/// <summary>
/// In general, coreferenced marks should not be added with this function, because it this does not do
/// any re-pointing. However, orphan corefs are not entered into the coref table and thus can appear in the nwa
/// prior to discovering a proper coref amongst the current args. They do not need repointing.
/// </summary>
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////
bool CheckAddResumePoint(NwayArgs* pnwa, byte tfsix, int m)
{
Debug.Assert(m != 0);
for (byte j = 0; j < pnwa->c_args; j++)
if (pnwa->rg_tfsix[j] == tfsix && pnwa->marks[j] == m)
return false;
AddResumePoint(pnwa, tfsix, m);
return true;
}
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////
/// <summary>
///
/// </summary>
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////
byte AddTfs(Tfs tfs)
{
if (c_participants >= MaxParticipants)
throw new InvalidOperationException("need more participant slots");
if (tfs.coref_tally_map == null)
((TfsSection)tfs)._load_coref_tally_map();
byte tfsix = c_participants++;
participants[tfsix] = tfs;
participant_bases[tfsix] = ppmb_next;
ppmb_next += tfs.coref_tally_map.Length;
if (ppmb_next - pp_map_base > CorefsMax)
throw new InvalidOperationException("need more coref slots");
return tfsix;
}
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////
/// <summary>
///
/// </summary>
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////
bool _check(Edge.Flag f, Tfs tfs1, Tfs tfs2)
{
NwayArgs* _p = stackalloc NwayArgs[CorefsMax];
pc_next = _corefs = _p;
NwayArgs** _pp = stackalloc NwayArgs*[CorefsMax];
ppmb_next = pp_map_base = _pp;
NwayArgs*** _ppp = stackalloc NwayArgs**[MaxParticipants];
participant_bases = _ppp;
NwayArgs nwa;
AddResumePoint(&nwa, AddTfs(tfs1), tfs1.Edge.Mark);
AddResumePoint(&nwa, AddTfs(tfs2), tfs2.Edge.Mark);
nwa.f = f;
if (!_check(&nwa))
return false;
/// Self-blocking structures will result in non-zero tally remainders. The presence of such structure implies
/// unification failure.
for (NwayArgs* pc = _corefs; pc < pc_next; pc++)
if (pc->c_remain != 0)
return false;
return true;
}
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////
/// <summary>
///
/// </summary>
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////
public static bool Check(Tfs tfs1, Tfs tfs2)
{
TypeMgr tm = tfs1.tm;
Edge.Flag nf = tm.UnifyTypesNoCoref(
tfs1.Edge.FlagsId & ~Edge.Flag.Coreference,
tfs2.Edge.FlagsId & ~Edge.Flag.Coreference);
if (nf == Edge.Flag.Bottom)
return false;
if ((nf & Edge.Flag.EtmNonBareType) == 0)
return true;
Debug.Assert(nf == tfs1.Edge.FlagsId || nf == tfs2.Edge.FlagsId);
return new NWayCheck(tm)._check(nf, tfs1, tfs2);
}
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////
/// <summary>
///
/// </summary>
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////
public partial struct NwayArgs
{
[DebuggerBrowsable(DebuggerBrowsableState.Never)]
public byte c_args;
[DebuggerBrowsable(DebuggerBrowsableState.Never)]
public fixed byte rg_tfsix[ArgArityMax];
[DebuggerBrowsable(DebuggerBrowsableState.Never)]
public fixed int marks[ArgArityMax];
[DebuggerBrowsable(DebuggerBrowsableState.Never)]
public Edge.Flag f;
[DebuggerBrowsable(DebuggerBrowsableState.Never)]
public int c_remain;
//public int TypeId { get { return (int)(f & Edge.Flag.MultiIdMask); } }
};
};
}