Complex multiple interacting trampolines removal.
This commit is contained in:
parent
cdda26f21f
commit
c256afc7ca
@ -1,10 +1,8 @@
|
|||||||
2 iterateTermOther arachne.c +1053 ; system.c +1155
|
|
||||||
1 subtermUnify arachne.c +961
|
1 subtermUnify arachne.c +961
|
||||||
3 unify mgu.c +233 ; mgu.c +247 ; mgu.c +281
|
3 unify mgu.c +233 ; mgu.c +247 ; mgu.c +281
|
||||||
|
|
||||||
dependencies:
|
dependencies:
|
||||||
|
|
||||||
iterateTermOther is called using makeDepend and addOther
|
|
||||||
subtermUnify is called using unifiesWithKeys
|
subtermUnify is called using unifiesWithKeys
|
||||||
unify is called using unify_combine_enc and unify_combined_tup, and a callback using the keys list? (which propagates back to subtermunify data)
|
unify is called using unify_combine_enc and unify_combined_tup, and a callback using the keys list? (which propagates back to subtermunify data)
|
||||||
|
|
||||||
|
127
src/arachne.c
127
src/arachne.c
@ -935,6 +935,66 @@ createDecryptionChain (const Binding b, const int run, const int index,
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
struct md_state
|
||||||
|
{
|
||||||
|
int neworders;
|
||||||
|
int allgood;
|
||||||
|
Term tvar;
|
||||||
|
Termlist sl;
|
||||||
|
};
|
||||||
|
|
||||||
|
//! makeDepend for next function
|
||||||
|
/** the idea is, that a substitution in run x with
|
||||||
|
* something containing should be wrapped; this
|
||||||
|
* occurs for all subterms of other runs.
|
||||||
|
*/
|
||||||
|
int
|
||||||
|
makeDepend (Term tsmall, struct md_state *state)
|
||||||
|
{
|
||||||
|
Term tsubst;
|
||||||
|
|
||||||
|
tsubst = deVar (tsmall);
|
||||||
|
if (!realTermVariable (tsubst))
|
||||||
|
{
|
||||||
|
// Only for non-variables (i.e. local constants)
|
||||||
|
int r1, e1;
|
||||||
|
|
||||||
|
r1 = TermRunid (tsubst);
|
||||||
|
e1 = firstOccurrence (sys, r1, tsubst, SEND);
|
||||||
|
if (e1 >= 0)
|
||||||
|
{
|
||||||
|
int r2, e2;
|
||||||
|
|
||||||
|
r2 = TermRunid (state->tvar);
|
||||||
|
e2 = firstOccurrence (sys, r2, tsubst, RECV);
|
||||||
|
if (e2 >= 0)
|
||||||
|
{
|
||||||
|
|
||||||
|
if (dependPushEvent (r1, e1, r2, e2))
|
||||||
|
{
|
||||||
|
state->neworders++;
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
state->allgood = false;
|
||||||
|
if (switches.output == PROOF)
|
||||||
|
{
|
||||||
|
indentPrint ();
|
||||||
|
eprintf ("Substitution for ");
|
||||||
|
termSubstPrint (state->sl->term);
|
||||||
|
eprintf (" (subterm ");
|
||||||
|
termPrint (tsmall);
|
||||||
|
eprintf (") could not be safely bound.\n");
|
||||||
|
}
|
||||||
|
return false;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
//! Try to bind a specific existing run to a goal.
|
//! Try to bind a specific existing run to a goal.
|
||||||
/**
|
/**
|
||||||
@ -994,70 +1054,23 @@ bind_existing_to_goal (const Binding b, const int run, const int index,
|
|||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
int neworders;
|
struct md_state State;
|
||||||
int allgood;
|
|
||||||
Term tvar;
|
|
||||||
|
|
||||||
// the idea is, that a substitution in run x with
|
|
||||||
// something containing should be wrapped; this
|
|
||||||
// occurs for all subterms of other runs.
|
|
||||||
int makeDepend (Term tsmall)
|
|
||||||
{
|
|
||||||
Term tsubst;
|
|
||||||
|
|
||||||
tsubst = deVar (tsmall);
|
// TODO CONTEXT for makeDepend in State
|
||||||
if (!realTermVariable (tsubst))
|
|
||||||
{
|
|
||||||
// Only for non-variables (i.e. local constants)
|
|
||||||
int r1, e1;
|
|
||||||
|
|
||||||
r1 = TermRunid (tsubst);
|
State.neworders = 0;
|
||||||
e1 = firstOccurrence (sys, r1, tsubst, SEND);
|
State.sl = sl;
|
||||||
if (e1 >= 0)
|
State.tvar = sl->term;
|
||||||
{
|
State.allgood = true;
|
||||||
int r2, e2;
|
iterateTermOther (run, State.tvar, makeDepend, &State);
|
||||||
|
if (State.allgood)
|
||||||
r2 = TermRunid (tvar);
|
|
||||||
e2 = firstOccurrence (sys, r2, tsubst, RECV);
|
|
||||||
if (e2 >= 0)
|
|
||||||
{
|
|
||||||
|
|
||||||
if (dependPushEvent (r1, e1, r2, e2))
|
|
||||||
{
|
|
||||||
neworders++;
|
|
||||||
return true;
|
|
||||||
}
|
|
||||||
else
|
|
||||||
{
|
|
||||||
allgood = false;
|
|
||||||
if (switches.output == PROOF)
|
|
||||||
{
|
|
||||||
indentPrint ();
|
|
||||||
eprintf ("Substitution for ");
|
|
||||||
termSubstPrint (sl->term);
|
|
||||||
eprintf (" (subterm ");
|
|
||||||
termPrint (tsmall);
|
|
||||||
eprintf (") could not be safely bound.\n");
|
|
||||||
}
|
|
||||||
return false;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
return true;
|
|
||||||
}
|
|
||||||
|
|
||||||
neworders = 0;
|
|
||||||
allgood = true;
|
|
||||||
tvar = sl->term;
|
|
||||||
iterateTermOther (run, tvar, makeDepend);
|
|
||||||
if (allgood)
|
|
||||||
{
|
{
|
||||||
wrapSubst (sl->next);
|
wrapSubst (sl->next);
|
||||||
}
|
}
|
||||||
while (neworders > 0)
|
while (State.neworders > 0)
|
||||||
{
|
{
|
||||||
neworders--;
|
State.neworders--;
|
||||||
dependPopEvent ();
|
dependPopEvent ();
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
28
src/system.c
28
src/system.c
@ -1128,6 +1128,19 @@ iterateEventsType (const System sys, const int run, const int evtype,
|
|||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
struct ao_state
|
||||||
|
{
|
||||||
|
Termlist tlo;
|
||||||
|
};
|
||||||
|
|
||||||
|
//! Helper for next
|
||||||
|
int
|
||||||
|
addOther (Term t, struct ao_state *state)
|
||||||
|
{
|
||||||
|
state->tlo = termlistAddNew (state->tlo, t);
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
|
||||||
// Iterate over all 'others': local variables of a run that are instantiated and contain some term of another run.
|
// Iterate over all 'others': local variables of a run that are instantiated and contain some term of another run.
|
||||||
/**
|
/**
|
||||||
* Now incorporates "checkterm" required argument of myrun to the callback:
|
* Now incorporates "checkterm" required argument of myrun to the callback:
|
||||||
@ -1140,15 +1153,10 @@ iterateLocalToOther (const System sys, const int myrun,
|
|||||||
{
|
{
|
||||||
Termlist tlo, tls;
|
Termlist tlo, tls;
|
||||||
int flag;
|
int flag;
|
||||||
|
struct ao_state State;
|
||||||
int addOther (Term t)
|
|
||||||
{
|
|
||||||
tlo = termlistAddNew (tlo, t);
|
|
||||||
return true;
|
|
||||||
}
|
|
||||||
|
|
||||||
flag = true;
|
flag = true;
|
||||||
tlo = NULL;
|
State.tlo = NULL;
|
||||||
// construct all others occuring in the recvs
|
// construct all others occuring in the recvs
|
||||||
for (tls = sys->runs[myrun].sigma; tls != NULL; tls = tls->next)
|
for (tls = sys->runs[myrun].sigma; tls != NULL; tls = tls->next)
|
||||||
{
|
{
|
||||||
@ -1157,11 +1165,11 @@ iterateLocalToOther (const System sys, const int myrun,
|
|||||||
tt = tls->term;
|
tt = tls->term;
|
||||||
if (realTermVariable (tt) && tt->subst != NULL);
|
if (realTermVariable (tt) && tt->subst != NULL);
|
||||||
{
|
{
|
||||||
iterateTermOther (myrun, tt->subst, addOther);
|
iterateTermOther (myrun, tt->subst, addOther, &State);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
// now iterate over all of them
|
// now iterate over all of them
|
||||||
for (tls = tlo; flag && (tls != NULL); tls = tls->next)
|
for (tls = State.tlo; flag && (tls != NULL); tls = tls->next)
|
||||||
{
|
{
|
||||||
if (!callback (sys, tls->term, myrun))
|
if (!callback (sys, tls->term, myrun))
|
||||||
{
|
{
|
||||||
@ -1170,7 +1178,7 @@ iterateLocalToOther (const System sys, const int myrun,
|
|||||||
}
|
}
|
||||||
|
|
||||||
// clean up
|
// clean up
|
||||||
termlistDelete (tlo);
|
termlistDelete (State.tlo);
|
||||||
return flag;
|
return flag;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
34
src/term.c
34
src/term.c
@ -1560,21 +1560,39 @@ termSubstPrint (Term t)
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
// Iterate over subterm constants of other runs in a term
|
typedef int (*CallBack) ();
|
||||||
// Callback should return true to progress. This is reported in the final thing.
|
|
||||||
int
|
struct ito_contain
|
||||||
iterateTermOther (const int myrun, Term t, int (*callback) (Term t))
|
|
||||||
{
|
{
|
||||||
int testOther (Term t, int *state)
|
int myrun;
|
||||||
|
CallBack callback;
|
||||||
|
void *ito_state;
|
||||||
|
};
|
||||||
|
|
||||||
|
int
|
||||||
|
testOther (Term t, struct ito_contain *state)
|
||||||
{
|
{
|
||||||
int run;
|
int run;
|
||||||
|
|
||||||
run = TermRunid (t);
|
run = TermRunid (t);
|
||||||
if (run >= 0 && run != myrun)
|
if (run >= 0 && run != state->myrun)
|
||||||
{
|
{
|
||||||
return callback (t);
|
return state->callback (t, state->ito_state);
|
||||||
}
|
}
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
return term_iterate_state_deVar (t, testOther, NULL, NULL, NULL, NULL);
|
|
||||||
|
// Iterate over subterm constants of other runs in a term
|
||||||
|
// Callback should return true to progress. This is reported in the final thing.
|
||||||
|
int
|
||||||
|
iterateTermOther (const int myrun, Term t, int (*callback) (),
|
||||||
|
void *ito_state)
|
||||||
|
{
|
||||||
|
struct ito_contain State;
|
||||||
|
|
||||||
|
State.myrun = myrun;
|
||||||
|
State.callback = callback;
|
||||||
|
State.ito_state = ito_state;
|
||||||
|
|
||||||
|
return term_iterate_state_deVar (t, testOther, NULL, NULL, NULL, &State);
|
||||||
}
|
}
|
||||||
|
@ -213,7 +213,7 @@ Term getTermFunction (Term t);
|
|||||||
unsigned int termHidelevel (const Term tsmall, Term tbig);
|
unsigned int termHidelevel (const Term tsmall, Term tbig);
|
||||||
void termSubstPrint (Term t);
|
void termSubstPrint (Term t);
|
||||||
|
|
||||||
int iterateTermOther (const int myrun, Term t, int (*callback) (Term t));
|
int iterateTermOther (const int myrun, Term t, int (*callback) (), void *s);
|
||||||
|
|
||||||
extern char *RUNSEP; // by default, set to "#"
|
extern char *RUNSEP; // by default, set to "#"
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user