From c256afc7ca67112941e15f886a930c3bae957510 Mon Sep 17 00:00:00 2001 From: Cas Cremers Date: Mon, 5 Nov 2018 14:43:00 +0100 Subject: [PATCH] Complex multiple interacting trampolines removal. --- src/TODO-trampolines.txt | 2 - src/arachne.c | 127 +++++++++++++++++++++------------------ src/system.c | 28 ++++++--- src/term.c | 42 +++++++++---- src/term.h | 2 +- 5 files changed, 119 insertions(+), 82 deletions(-) diff --git a/src/TODO-trampolines.txt b/src/TODO-trampolines.txt index 2c8de51..bbba405 100644 --- a/src/TODO-trampolines.txt +++ b/src/TODO-trampolines.txt @@ -1,10 +1,8 @@ -2 iterateTermOther arachne.c +1053 ; system.c +1155 1 subtermUnify arachne.c +961 3 unify mgu.c +233 ; mgu.c +247 ; mgu.c +281 dependencies: -iterateTermOther is called using makeDepend and addOther 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) diff --git a/src/arachne.c b/src/arachne.c index 8186093..6e824ac 100644 --- a/src/arachne.c +++ b/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. /** @@ -994,70 +1054,23 @@ bind_existing_to_goal (const Binding b, const int run, const int index, } else { - int neworders; - int allgood; - Term tvar; + struct md_state State; - // 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); - if (!realTermVariable (tsubst)) - { - // Only for non-variables (i.e. local constants) - int r1, e1; + // TODO CONTEXT for makeDepend in State - r1 = TermRunid (tsubst); - e1 = firstOccurrence (sys, r1, tsubst, SEND); - if (e1 >= 0) - { - int r2, e2; - - 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) + State.neworders = 0; + State.sl = sl; + State.tvar = sl->term; + State.allgood = true; + iterateTermOther (run, State.tvar, makeDepend, &State); + if (State.allgood) { wrapSubst (sl->next); } - while (neworders > 0) + while (State.neworders > 0) { - neworders--; + State.neworders--; dependPopEvent (); } } diff --git a/src/system.c b/src/system.c index 0632d48..c1ad20c 100644 --- a/src/system.c +++ b/src/system.c @@ -1128,6 +1128,19 @@ iterateEventsType (const System sys, const int run, const int evtype, 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. /** * Now incorporates "checkterm" required argument of myrun to the callback: @@ -1140,15 +1153,10 @@ iterateLocalToOther (const System sys, const int myrun, { Termlist tlo, tls; int flag; - - int addOther (Term t) - { - tlo = termlistAddNew (tlo, t); - return true; - } + struct ao_state State; flag = true; - tlo = NULL; + State.tlo = NULL; // construct all others occuring in the recvs 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; if (realTermVariable (tt) && tt->subst != NULL); { - iterateTermOther (myrun, tt->subst, addOther); + iterateTermOther (myrun, tt->subst, addOther, &State); } } // 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)) { @@ -1170,7 +1178,7 @@ iterateLocalToOther (const System sys, const int myrun, } // clean up - termlistDelete (tlo); + termlistDelete (State.tlo); return flag; } diff --git a/src/term.c b/src/term.c index ac63010..1138bec 100644 --- a/src/term.c +++ b/src/term.c @@ -1560,21 +1560,39 @@ termSubstPrint (Term t) } } +typedef int (*CallBack) (); + +struct ito_contain +{ + int myrun; + CallBack callback; + void *ito_state; +}; + +int +testOther (Term t, struct ito_contain *state) +{ + int run; + + run = TermRunid (t); + if (run >= 0 && run != state->myrun) + { + return state->callback (t, state->ito_state); + } + return true; +} + // 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) (Term t)) +iterateTermOther (const int myrun, Term t, int (*callback) (), + void *ito_state) { - int testOther (Term t, int *state) - { - int run; + struct ito_contain State; - run = TermRunid (t); - if (run >= 0 && run != myrun) - { - return callback (t); - } - return true; - } - return term_iterate_state_deVar (t, testOther, NULL, NULL, NULL, NULL); + State.myrun = myrun; + State.callback = callback; + State.ito_state = ito_state; + + return term_iterate_state_deVar (t, testOther, NULL, NULL, NULL, &State); } diff --git a/src/term.h b/src/term.h index f9d014f..ca62308 100644 --- a/src/term.h +++ b/src/term.h @@ -213,7 +213,7 @@ Term getTermFunction (Term t); unsigned int termHidelevel (const Term tsmall, Term tbig); 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 "#"