- Matching is now typed.
This commit is contained in:
parent
c7e290197c
commit
c3d5123ab0
@ -7,6 +7,7 @@
|
||||
#include "binding.h"
|
||||
#include "warshall.h"
|
||||
#include "memory.h"
|
||||
#include "debug.h"
|
||||
|
||||
/*
|
||||
* Idea is the ev_from *has to* precede the ev_to
|
||||
@ -203,7 +204,13 @@ binding_add (int run_from, int ev_from, int run_to, int ev_to)
|
||||
Binding b;
|
||||
|
||||
b = binding_create (run_from, ev_from, run_to, ev_to);
|
||||
eprintf ("Adding binding (%i,%i) --->> (%i,%i)\n",run_from, ev_from, run_to, ev_to);
|
||||
#ifdef DEBUG
|
||||
if (DEBUGL (5))
|
||||
{
|
||||
eprintf ("Adding binding (%i,%i) --->> (%i,%i)\n", run_from, ev_from,
|
||||
run_to, ev_to);
|
||||
}
|
||||
#endif
|
||||
sys->bindings = list_insert (sys->bindings, b);
|
||||
|
||||
/*
|
||||
|
@ -701,8 +701,11 @@ protocolCompile (Symbol prots, Tac tc, Tac tcroles)
|
||||
{
|
||||
if (sys->engine == ARACHNE_ENGINE)
|
||||
{
|
||||
pr->rolenames =
|
||||
termlistAppend (pr->rolenames, levelVar (tcroles->t1.sym));
|
||||
Term rolename;
|
||||
|
||||
rolename = levelVar (tcroles->t1.sym);
|
||||
rolename->stype = termlistAdd (NULL, TERM_Agent);
|
||||
pr->rolenames = termlistAppend (pr->rolenames, rolename);
|
||||
}
|
||||
else
|
||||
{
|
||||
|
112
src/mgu.c
112
src/mgu.c
@ -14,6 +14,85 @@
|
||||
New version yields a termlist with substituted variables, which can later be reset to NULL.
|
||||
*/
|
||||
|
||||
//! Global constant. If true, typed checking
|
||||
int welltyped = 1;
|
||||
|
||||
void
|
||||
showSubst (Term t)
|
||||
{
|
||||
#ifdef DEBUG
|
||||
if (!DEBUGL (5))
|
||||
return;
|
||||
|
||||
indent ();
|
||||
printf ("Substituting ");
|
||||
termPrint (t);
|
||||
printf (", typed ");
|
||||
termlistPrint (t->stype);
|
||||
if (realTermLeaf (t->subst))
|
||||
{
|
||||
printf ("->");
|
||||
termlistPrint (t->subst->stype);
|
||||
}
|
||||
else
|
||||
{
|
||||
printf (", composite term");
|
||||
}
|
||||
if (t->type != VARIABLE)
|
||||
{
|
||||
printf (" (bound roleconstant)");
|
||||
}
|
||||
printf ("\n");
|
||||
#endif
|
||||
}
|
||||
|
||||
//! See if a substitution is valid
|
||||
__inline__ int
|
||||
goodsubst (Term tvar, Term tsubst)
|
||||
{
|
||||
if (tvar->stype == NULL || (!welltyped))
|
||||
{
|
||||
return 1;
|
||||
}
|
||||
else
|
||||
{
|
||||
/**
|
||||
* Check if each type of the substitution is allowed in the variable
|
||||
*/
|
||||
if (!realTermLeaf (tsubst))
|
||||
{
|
||||
// Typed var cannot match with non-leaf
|
||||
return 0;
|
||||
}
|
||||
else
|
||||
{
|
||||
// It's a leaf, but what type?
|
||||
if (termlistContained (tvar->stype, tsubst->stype))
|
||||
{
|
||||
return 1;
|
||||
}
|
||||
else
|
||||
{
|
||||
#ifdef DEBUG
|
||||
if (DEBUGL (5))
|
||||
{
|
||||
eprintf ("Substitution fails on ");
|
||||
termPrint (tvar);
|
||||
eprintf (" -/-> ");
|
||||
termPrint (tsubst);
|
||||
eprintf (", because type: \n");
|
||||
termlistPrint (tvar->stype);
|
||||
eprintf (" does not contain ");
|
||||
termlistPrint (tsubst->stype);
|
||||
eprintf ("\n");
|
||||
}
|
||||
#endif
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
//! Undo all substitutions in a list of variables.
|
||||
/**
|
||||
* The termlist should contain only variables.
|
||||
@ -43,34 +122,6 @@ termMguTerm (Term t1, Term t2)
|
||||
if (t1 == t2)
|
||||
return NULL;
|
||||
|
||||
#ifdef DEBUG
|
||||
void showSubst (Term t)
|
||||
{
|
||||
if (!DEBUGL (5))
|
||||
return;
|
||||
|
||||
indent ();
|
||||
printf ("Substituting ");
|
||||
termPrint (t);
|
||||
printf (", typed ");
|
||||
termlistPrint (t->stype);
|
||||
if (realTermLeaf (t->subst))
|
||||
{
|
||||
printf ("->");
|
||||
termlistPrint (t->subst->stype);
|
||||
}
|
||||
else
|
||||
{
|
||||
printf (", composite term");
|
||||
}
|
||||
if (t->type != VARIABLE)
|
||||
{
|
||||
printf (" (bound roleconstant)");
|
||||
}
|
||||
printf ("\n");
|
||||
}
|
||||
#endif
|
||||
|
||||
if (!(hasTermVariable (t1) || hasTermVariable (t2)))
|
||||
{
|
||||
if (isTermEqual (t1, t2))
|
||||
@ -86,7 +137,7 @@ termMguTerm (Term t1, Term t2)
|
||||
/* symmetrical tests for single variable */
|
||||
if (realTermVariable (t1))
|
||||
{
|
||||
if (termOccurs (t2, t1))
|
||||
if (termOccurs (t2, t1) || !goodsubst (t1, t2))
|
||||
return MGUFAIL;
|
||||
else
|
||||
{
|
||||
@ -99,7 +150,7 @@ termMguTerm (Term t1, Term t2)
|
||||
}
|
||||
if (realTermVariable (t2))
|
||||
{
|
||||
if (termOccurs (t1, t2))
|
||||
if (termOccurs (t1, t2) || !goodsubst (t2, t1))
|
||||
return MGUFAIL;
|
||||
else
|
||||
{
|
||||
@ -265,4 +316,3 @@ termMguSubTerm (Term t1, Term t2, int (*iterator) (),
|
||||
}
|
||||
return flag;
|
||||
}
|
||||
|
||||
|
@ -597,6 +597,7 @@ roleInstance (const System sys, const Protocol protocol, const Role role,
|
||||
// Make new var for this run
|
||||
newt = makeTermType (VARIABLE, newt->left.symb, rid);
|
||||
artefacts = termlistAdd (artefacts, newt);
|
||||
newt->stype = oldt->stype;
|
||||
// Copy substitution
|
||||
newt->subst = oldt->subst;
|
||||
// Remove any old substitution! It is now propagated!
|
||||
@ -604,7 +605,9 @@ roleInstance (const System sys, const Protocol protocol, const Role role,
|
||||
}
|
||||
// Add to agent list, possibly
|
||||
if (inTermlist (protocol->rolenames, oldt))
|
||||
runs[rid].agents = termlistAdd (runs[rid].agents, newt);
|
||||
{
|
||||
runs[rid].agents = termlistAdd (runs[rid].agents, newt);
|
||||
}
|
||||
fromlist = termlistAdd (fromlist, oldt);
|
||||
tolist = termlistAdd (tolist, newt);
|
||||
|
||||
|
@ -297,7 +297,7 @@ termPrint (Term term)
|
||||
return;
|
||||
}
|
||||
#ifdef DEBUG
|
||||
if (!DEBUGL (1))
|
||||
if (!DEBUGL (4))
|
||||
{
|
||||
term = deVar (term);
|
||||
}
|
||||
|
Loading…
Reference in New Issue
Block a user