diff --git a/src/TODO-trampolines.txt b/src/TODO-trampolines.txt deleted file mode 100644 index bbba405..0000000 --- a/src/TODO-trampolines.txt +++ /dev/null @@ -1,8 +0,0 @@ -1 subtermUnify arachne.c +961 -3 unify mgu.c +233 ; mgu.c +247 ; mgu.c +281 - -dependencies: - -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 cbcc816..1bc48f8 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -30,6 +30,7 @@ #include #include #include +#include #include "mymalloc.h" #include "term.h" @@ -995,6 +996,95 @@ makeDepend (Term tsmall, struct md_state *state) return true; } +struct betg_state +{ + Binding b; + int run; + int index; + int newdecr; +}; + +int +unifiesWithKeys (Termlist substlist, Termlist keylist, + struct betg_state *ptr_betgState) +{ + int old_length; + int newgoals; + + assert (ptr_betgState != NULL); + + // TODO this is a hack: in this case we really should not use subterm + // unification but interm instead. However, this effectively does the same + // by avoiding branches that get immediately pruned anyway. + if (!ptr_betgState->newdecr && keylist != NULL) + { + return true; + } + + // We need some adapting because the height would increase; we therefore + // have to add recv goals before we know whether it unifies. + old_length = sys->runs[ptr_betgState->run].height; + newgoals = + add_recv_goals (ptr_betgState->run, old_length, ptr_betgState->index + 1); + + { + // wrap substitution lists + + void wrapSubst (Termlist sl) + { + if (sl == NULL) + { + if (switches.output == PROOF) + { + Roledef rd; + + indentPrint (); + eprintf ("Suppose "); + termPrint ((ptr_betgState->b)->term); + eprintf (" originates first at run %i, event %i, as part of ", + ptr_betgState->run, ptr_betgState->index); + rd = + roledef_shift (sys->runs[ptr_betgState->run].start, + ptr_betgState->index); + termPrint (rd->message); + eprintf ("\n"); + } + // new create key goals, bind etc. + createDecryptionChain (ptr_betgState->b, ptr_betgState->run, + ptr_betgState->index, keylist, iterate); + } + else + { + struct md_state State; + + // TODO CONTEXT for makeDepend in State + + State.neworders = 0; + State.sl = sl; + State.tvar = sl->term; + State.allgood = true; + iterateTermOther (ptr_betgState->run, State.tvar, makeDepend, + &State); + if (State.allgood) + { + wrapSubst (sl->next); + } + while (State.neworders > 0) + { + State.neworders--; + dependPopEvent (); + } + } + } + + wrapSubst (substlist); + } + + // undo + goal_remove_last (newgoals); + sys->runs[ptr_betgState->run].height = old_length; + return true; +} //! Try to bind a specific existing run to a goal. /** @@ -1011,82 +1101,15 @@ bind_existing_to_goal (const Binding b, const int run, const int index, int newdecr) { Term bigterm; + struct betg_state betgState; - int unifiesWithKeys (Termlist substlist, Termlist keylist, void *state) - { - int old_length; - int newgoals; - - // TODO this is a hack: in this case we really should not use subterm - // unification but interm instead. However, this effectively does the same - // by avoiding branches that get immediately pruned anyway. - if (!newdecr && keylist != NULL) - { - return true; - } - // We need some adapting because the height would increase; we therefore - // have to add recv goals before we know whether it unifies. - old_length = sys->runs[run].height; - newgoals = add_recv_goals (run, old_length, index + 1); - - { - // wrap substitution lists - - void wrapSubst (Termlist sl) - { - if (sl == NULL) - { - if (switches.output == PROOF) - { - Roledef rd; - - indentPrint (); - eprintf ("Suppose "); - termPrint (b->term); - eprintf (" originates first at run %i, event %i, as part of ", - run, index); - rd = roledef_shift (sys->runs[run].start, index); - termPrint (rd->message); - eprintf ("\n"); - } - // new create key goals, bind etc. - createDecryptionChain (b, run, index, keylist, iterate); - } - else - { - struct md_state State; - - - // TODO CONTEXT for makeDepend in State - - 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 (State.neworders > 0) - { - State.neworders--; - dependPopEvent (); - } - } - } - - wrapSubst (substlist); - } - - // undo - goal_remove_last (newgoals); - sys->runs[run].height = old_length; - return true; - } + betgState.b = b; + betgState.run = run; + betgState.index = index; + betgState.newdecr = newdecr; bigterm = roledef_shift (sys->runs[run].start, index)->message; - subtermUnify (bigterm, b->term, NULL, NULL, unifiesWithKeys, NULL); + subtermUnify (bigterm, b->term, NULL, NULL, unifiesWithKeys, &betgState); } diff --git a/src/mgu.c b/src/mgu.c index a964a89..a1b61e7 100644 --- a/src/mgu.c +++ b/src/mgu.c @@ -322,7 +322,7 @@ keycallback (Termlist tl, struct su_kcb_state *ptr_kcb_state) */ int subtermUnify (Term tbig, Term tsmall, Termlist tl, Termlist keylist, - int (*callback) (Termlist, Termlist, void *), void *state) + int (*callback) (), void *state) { int proceed; struct su_kcb_state kcb_state; diff --git a/src/mgu.h b/src/mgu.h index 2fc430b..4ca2f2c 100644 --- a/src/mgu.h +++ b/src/mgu.h @@ -39,6 +39,6 @@ int checkRoletermMatch (const Term t1, const Term t2, const Termlist tl); int unify (Term t1, Term t2, Termlist tl, int (*callback) (), void *state); int subtermUnify (Term tbig, Term tsmall, Termlist tl, Termlist keylist, - int (*callback) (Termlist, Termlist, void *), void *state); + int (*callback) (), void *state); #endif