From 1ce03104c57fd800db7838930748fb6460fc049c Mon Sep 17 00:00:00 2001 From: ccremers Date: Wed, 15 Mar 2006 21:30:19 +0000 Subject: [PATCH] Major: - Added rho/sigma/constants fields to the runs, on which the new code is based. Over time, .locals should be deprecated in favour of these better variants. - Untyped variant is out of grace for the time being (cf. Athena interm problems) - Improved graph output further. Minor: - Added TERMLISTADD and APPEND macros for more concise code. --- src/cost.c | 2 +- src/dotout.c | 225 ++++++++++++++++++++++++++---------- src/prune_theorems.c | 6 +- src/system.c | 268 ++++++++++++++++++++----------------------- src/system.h | 7 +- src/tac.c | 1 + src/term.c | 66 ++++++++--- src/term.h | 6 + src/termlist.h | 3 + 9 files changed, 358 insertions(+), 226 deletions(-) diff --git a/src/cost.c b/src/cost.c index 5c36115..605c0f5 100644 --- a/src/cost.c +++ b/src/cost.c @@ -25,7 +25,7 @@ selfInitiator (const System sys, const int run) Termlist agents; Termlist seen; - agents = sys->runs[run].agents; + agents = sys->runs[run].rho; seen = NULL; while (agents != NULL) { diff --git a/src/dotout.c b/src/dotout.c index 37dfa74..d33792c 100644 --- a/src/dotout.c +++ b/src/dotout.c @@ -53,11 +53,36 @@ extern Role I_RRSD; * spread over all the runs. */ +static System sys = NULL; /* * code */ +void +printVisualRun (int rid) +{ + int run; + int display; + + display = 1; + for (run = 0; run < rid; run++) + { + if (sys->runs[run].protocol != INTRUDER) + { + display++; + } + } + eprintf ("#%i", display); +} + +//! Remap term stuff +void +termPrintRemap (const Term t) +{ + termPrintCustom (t, "", "V", "(", ")", "\\{ ", " \\}", printVisualRun); +} + //! Draw node void node (const System sys, const int run, const int index) @@ -113,7 +138,7 @@ roledefDraw (Roledef rd) label = TermOp2 (label); } eprintf ("_"); - termPrint (label); + termPrintRemap (label); } } @@ -122,29 +147,29 @@ roledefDraw (Roledef rd) eprintf ("read"); optlabel (); eprintf (" from "); - termPrint (rd->from); + termPrintRemap (rd->from); eprintf ("\\n"); - termPrint (rd->message); + termPrintRemap (rd->message); } if (rd->type == SEND) { eprintf ("send"); optlabel (); eprintf (" to "); - termPrint (rd->to); + termPrintRemap (rd->to); eprintf ("\\n"); - termPrint (rd->message); + termPrintRemap (rd->message); } if (rd->type == CLAIM) { eprintf ("claim"); optlabel (); eprintf ("\\n"); - termPrint (rd->to); + termPrintRemap (rd->to); if (rd->message != NULL) { eprintf (" : "); - termPrint (rd->message); + termPrintRemap (rd->message); } } } @@ -159,7 +184,7 @@ chooseTermNode (const Term t) rsbuf = RUNSEP; RUNSEP = "x"; - termPrint (t); + termPrintRemap (t); RUNSEP = rsbuf; } } @@ -502,6 +527,27 @@ iterate_first_regular_occurrences (const System sys, return true; } +//! Does a term occur in a run? +int +termOccursInRun (Term t, int run) +{ + Roledef rd; + int e; + + rd = sys->runs[run].start; + e = 0; + while (e < sys->runs[run].step) + { + if (roledefSubTerm (rd, t)) + { + return true; + } + e++; + rd = rd->next; + } + return false; +} + //! Draw a class choice /** * \rho classes are already dealt with in the headers, so we should ignore them. @@ -532,7 +578,7 @@ drawClass (const System sys, Binding b) run = TermRunid (varterm); if ((run >= 0) && (run < sys->maxruns)) { - if (inTermlist (sys->runs[run].agents, varterm)) + if (inTermlist (sys->runs[run].rho, varterm)) { return; } @@ -553,7 +599,7 @@ drawClass (const System sys, Binding b) eprintf ("\t"); chooseTermNode (varterm); eprintf (" [label=\"Class:\\nAny "); - termPrint (varterm); + termPrintRemap (varterm); eprintf ("\"];\n"); eprintf ("\t"); chooseTermNode (varterm); @@ -601,7 +647,7 @@ drawBinding (const System sys, Binding b) eprintf ("\t"); arrow (sys, b); eprintf (" [label=\""); - termPrint (b->term); + termPrintRemap (b->term); eprintf ("\"]"); eprintf (";\n"); } @@ -658,7 +704,7 @@ drawBinding (const System sys, Binding b) { // Only explicitly mention redirect term when it differs from the sent term eprintf ("\\n"); - termPrint (b->term); + termPrintRemap (b->term); } eprintf ("\"]"); eprintf (";\n"); @@ -720,14 +766,14 @@ agentsOfRunPrintOthers (const System sys, const int run) { Term agent; - termPrint (roles->term); + termPrintRemap (roles->term); eprintf (" is "); agent = agentOfRunRole (sys, run, roles->term); if (isTermVariable (agent)) { eprintf ("any "); } - termPrint (agent); + termPrintRemap (agent); eprintf ("\\l"); } roles = roles->next; @@ -767,7 +813,7 @@ drawRegularRuns (const System sys) eprintf ("\tsubgraph cluster_run%i {\n", run); eprintf ("\t\tlabel = \""); eprintf ("#%i: ", run); - termPrint (sys->runs[run].protocol->nameterm); + termPrintRemap (sys->runs[run].protocol->nameterm); eprintf (", "); agentsOfRunPrint (sys, run); eprintf ("\\nTesting the second line\";\n", run); @@ -889,9 +935,9 @@ drawRegularRuns (const System sys) { eprintf ("Any "); } - termPrint (agentname); + termPrintRemap (agentname); eprintf (" in role "); - termPrint (rolename); + termPrintRemap (rolename); eprintf ("\\l"); } @@ -953,27 +999,82 @@ drawRegularRuns (const System sys) if (showprotocol) { eprintf ("Protocol "); - termPrint (sys->runs[run].protocol-> - nameterm); + termPrintRemap (sys->runs[run].protocol-> + nameterm); eprintf ("\\l"); } } - eprintf ("Run #%i\\l", run); + eprintf ("Run "); + printVisualRun (run); + eprintf ("\\l"); - // print the other agents - eprintf ("|"); - if (termlistLength (sys->runs[run].agents) > 1) + // rho, sigma, const + void showLocal (Term told, Term tnew) + { + if (realTermVariable (tnew)) + { + // Variables are mapped, maybe. But then we wonder whether they occur in reads. + termPrintRemap (told); + if (termOccursInRun (tnew, run)) + { + eprintf (" : "); + termPrintRemap (deVar (tnew)); + } + else + { + eprintf (" is not read"); + } + } + else + { + termPrintRemap (tnew); + } + eprintf ("\\l"); + } + void showLocals (Termlist tlold, Termlist tlnew, + Term tavoid) + { + while (tlold != NULL && tlnew != NULL) + { + if (!isTermEqual (tlold->term, tavoid)) + { + showLocal (tlold->term, tlnew->term); + } + tlold = tlold->next; + tlnew = tlnew->next; + } + } + + if (termlistLength (sys->runs[run].rho) > 1) { + eprintf ("|"); if (sys->runs[run].role->initiator) { - eprintf ("Chooses:\\l"); + eprintf ("Initiates with:\\l"); } else { - eprintf ("Assumes:\\l"); + eprintf ("Responds to:\\l"); } - agentsOfRunPrintOthers (sys, run); + showLocals (sys->runs[run].protocol-> + rolenames, sys->runs[run].rho, + sys->runs[run].role->nameterm); + } + + if (sys->runs[run].constants != NULL) + { + eprintf ("|Creates:\\l"); + showLocals (sys->runs[run].role-> + declaredconsts, + sys->runs[run].constants, NULL); + } + if (sys->runs[run].sigma != NULL) + { + eprintf ("|Variables:\\l"); + showLocals (sys->runs[run].role-> + declaredvars, + sys->runs[run].sigma, NULL); } // close up @@ -1113,7 +1214,7 @@ drawIntruderChoices (const System sys) eprintf ("\t"); chooseTermNode (b->term); eprintf (" [label=\"Class: any "); - termPrint (b->term); + termPrintRemap (b->term); eprintf ("\",color=\"darkgreen\"];\n"); iterate_first_regular_occurrences (sys, firsthere, b->term); @@ -1135,7 +1236,7 @@ drawIntruderChoices (const System sys) * This is not as nice as we would like it. Furthermore, the function is too big. */ void -dotSemiState (const System sys) +dotSemiState (const System mysys) { static int attack_number = 0; int run; @@ -1145,16 +1246,18 @@ dotSemiState (const System sys) int from_intruder_count; int nodes; + sys = mysys; + // Open graph attack_number++; eprintf ("digraph semiState%i {\n", attack_number); eprintf ("\tlabel = \"[Id %i] Protocol ", sys->attackid); p = (Protocol) sys->current_claim->protocol; - termPrint (p->nameterm); + termPrintRemap (p->nameterm); eprintf (", role "); - termPrint (sys->current_claim->rolename); + termPrintRemap (sys->current_claim->rolename); eprintf (", claim type "); - termPrint (sys->current_claim->type); + termPrintRemap (sys->current_claim->type); eprintf ("\";\n"); // Globals @@ -1242,39 +1345,41 @@ dotSemiState (const System sys) // For debugging we might add more stuff: full dependencies #ifdef DEBUG - { - int r1; + if (DEBUGL (3)) + { + int r1; - for (r1 = 0; r1 < sys->maxruns; r1++) - { - if (sys->runs[r1].protocol != INTRUDER) - { - int e1; + for (r1 = 0; r1 < sys->maxruns; r1++) + { + if (sys->runs[r1].protocol != INTRUDER) + { + int e1; - for (e1 = 0; e1 < sys->runs[r1].step; e1++) - { - int r2; + for (e1 = 0; e1 < sys->runs[r1].step; e1++) + { + int r2; - for (r2 = 0; r2 < sys->maxruns; r2++) - { - if (sys->runs[r2].protocol != INTRUDER) - { - int e2; + for (r2 = 0; r2 < sys->maxruns; r2++) + { + if (sys->runs[r2].protocol != INTRUDER) + { + int e2; - for (e2 = 0; e2 < sys->runs[r2].step; e2++) - { - if (isDependEvent (r1, e1, r2, e2)) - { - eprintf ("\tr%ii%i -> r%ii%i [color=grey];\n", - r1, e1, r2, e2); - } - } - } - } - } - } - } - } + for (e2 = 0; e2 < sys->runs[r2].step; e2++) + { + if (isDependEvent (r1, e1, r2, e2)) + { + eprintf + ("\tr%ii%i -> r%ii%i [color=grey];\n", r1, + e1, r2, e2); + } + } + } + } + } + } + } + } #endif // Intruder choices diff --git a/src/prune_theorems.c b/src/prune_theorems.c index a04dfe3..12f21f9 100644 --- a/src/prune_theorems.c +++ b/src/prune_theorems.c @@ -137,7 +137,7 @@ initiatorAgentsType (const System sys) { Termlist agents; - agents = sys->runs[run].agents; + agents = sys->runs[run].rho; while (agents != NULL) { if (!goodAgentType (agents->term)) @@ -221,7 +221,7 @@ prune_theorems (const System sys) // Check this initiator run Termlist tl; - tl = sys->runs[run].agents; + tl = sys->runs[run].rho; while (tl != NULL) { Termlist tlscan; @@ -280,7 +280,7 @@ prune_theorems (const System sys) { if (sys->runs[run].protocol != INTRUDER) { - if (sys->runs[run].agents != NULL) + if (sys->runs[run].rho != NULL) { Term actor; diff --git a/src/system.c b/src/system.c index 32f5a67..b652c86 100644 --- a/src/system.c +++ b/src/system.c @@ -226,26 +226,27 @@ ensureValidRun (const System sys, int run) for (i = oldsize; i < sys->maxruns; i++) { /* init run */ - struct run myrun = sys->runs[i]; - myrun.protocol = NULL; - myrun.role = NULL; - myrun.agents = NULL; - myrun.step = 0; - myrun.index = NULL; - myrun.start = NULL; + sys->runs[i].protocol = NULL; + sys->runs[i].role = NULL; + sys->runs[i].step = 0; + sys->runs[i].rolelength = 0; - myrun.rho = NULL; - myrun.sigma = NULL; - myrun.constants = NULL; - myrun.locals = NULL; - myrun.artefacts = NULL; - myrun.substitutions = NULL; + sys->runs[i].index = NULL; + sys->runs[i].start = NULL; + sys->runs[i].know = NULL; - myrun.know = NULL; + sys->runs[i].rho = NULL; + sys->runs[i].sigma = NULL; + sys->runs[i].constants = NULL; - myrun.prevSymmRun = -1; - myrun.firstNonAgentRead = -1; - myrun.firstReal = 0; + sys->runs[i].locals = NULL; + sys->runs[i].artefacts = NULL; + sys->runs[i].substitutions = NULL; + + + sys->runs[i].prevSymmRun = -1; + sys->runs[i].firstNonAgentRead = -1; + sys->runs[i].firstReal = 0; } } @@ -321,7 +322,7 @@ agentOfRunRole (const System sys, const int run, const Term role) // Agent variables have the same symbol as the role names, so // we can scan for this. - agents = sys->runs[run].agents; + agents = sys->runs[run].rho; while (agents != NULL) { Term agent; @@ -367,7 +368,7 @@ staticRunSymmetry (const System sys, const int rid) ridSymm = -1; runs = sys->runs; - agents = runs[rid].agents; + agents = runs[rid].rho; while (agents != NULL) { if (isTermVariable (agents->term)) @@ -378,7 +379,7 @@ staticRunSymmetry (const System sys, const int rid) if (ridSymm == -1) return -1; - agents = runs[rid].agents; + agents = runs[rid].rho; while (ridSymm >= 0) { /* compare protocol name, role name */ @@ -391,7 +392,7 @@ staticRunSymmetry (const System sys, const int rid) isEqual = 1; al = agents; - alSymm = runs[ridSymm].agents; + alSymm = runs[ridSymm].rho; while (isEqual && al != NULL) { /* determine equality */ @@ -572,7 +573,6 @@ run_localize (const System sys, const int rid, Termlist fromlist, } - //! Instantiate a role by making a new run for Arachne /** * This involves creation of a new run(id). @@ -588,13 +588,8 @@ roleInstanceArachne (const System sys, const Protocol protocol, int rid; Run runs; Roledef rd; - Termlist scanfrom, scanto; Termlist fromlist = NULL; // deleted at the end Termlist tolist = NULL; // -> .locals - Termlist artefacts = NULL; // -> .artefacts - Termlist rho = NULL; // -> .rho - Termlist sigma = NULL; // -> .sigma - Termlist constants = NULL; // -> .constants Term extterm = NULL; // construction thing (will go to artefacts) /* claim runid, allocate space */ @@ -615,89 +610,95 @@ roleInstanceArachne (const System sys, const Protocol protocol, runs[rid].step = 0; runs[rid].firstReal = 0; - /* scan for types in agent list */ - /* scanners */ - /** - * Because of pre-instantiation unification, some variables might already have been filled in. - * Ignore agent list; instead rely on role->variables. + /* Now we need to create local terms corresponding to rho, sigma, and any local constants. + * + * We maintain our stuff in a from/to list. */ - runs[rid].agents = NULL; - scanfrom = role->variables; - while (scanfrom != NULL) - { - Term newt, oldt; + void createLocal (Term oldt, int isvariable, int isrole) + { + Term newt; - /* Some care has to be taken: after we use this instantiation, we might reset it. - * That is not strictly necessary: whoever set it first, is responsible for getting rid - * of it again. - */ - oldt = scanfrom->term; - newt = deVar (oldt); - if (realTermVariable (newt)) - { - /* This is a variable of the role, that is not instantiated yet. - * Thus, it needs a local copy. - */ - newt = makeTermType (VARIABLE, TermSymb (newt), rid); - newt->stype = oldt->stype; - artefacts = termlistAddNew (artefacts, newt); - } - /* Now we add any role names to the agent list. Note that - * instantiations do not matter: because if the variable is - * instantiated, the rolename will be as well, and thus they will be - * equal anyway. - */ - if (inTermlist (protocol->rolenames, oldt)) - { - /* Add the agent name or role variable... */ - runs[rid].agents = termlistAppend (runs[rid].agents, newt); + // Create new term with the same symbol + if (isvariable) + { + // Force variable + newt = makeTermType (VARIABLE, TermSymb (oldt), rid); + } + else + { + // Force local (weirdly enough called global) + newt = makeTermType (GLOBAL, TermSymb (oldt), rid); + } + newt->stype = oldt->stype; // copy list of types + newt->roleVar = isrole; // set role status - if (isTermVariable (newt)) - { - // It is a protocol role name + // Add to copy list + TERMLISTADD (fromlist, oldt); + TERMLISTADD (tolist, newt); - // Flag this - newt->roleVar = 1; - newt->stype = termlistAddNew (newt->stype, TERM_Agent); + // Add to registration lists + // Everything to destructor list + TERMLISTADD (runs[rid].artefacts, newt); + // Variable / Constant? + if (isvariable) + { + TERMLISTADD (sys->variables, newt); + if (isrole) + { + // role variable + /* + * We use append to make sure the order is + * consistent with the role names list. + */ + TERMLISTAPPEND (runs[rid].rho, newt); + if (!role->initiator) + { + // For non-initiators, we prepend the reading of the role names - // maybe add choose? - // Note that for anything but full type flaws, this is not an issue. - // In the POR reduction, force choose was the default. Here it is not. - /* - * [x] - * TODO currently disabled: something weird was goind on causing weird prunes, - * for match=2. Investigate later. - */ - if (0 && not_read_first (rd, oldt) && switches.match == 2) - { - /* this term is forced as a choose, or it does not occur in the (first) read event */ - if (extterm == NULL) - { - extterm = newt; - } - else - { - extterm = makeTermTuple (newt, extterm); - // NOTE: don't these get double deleted? By roledefdestroy? - artefacts = termlistAddNew (artefacts, extterm); - } - } - } - } - fromlist = termlistAdd (fromlist, oldt); - tolist = termlistAdd (tolist, newt); + // XXX disabled for now TODO [x] [cc] + if (0 == 1 && not_read_first (rd, oldt)) + { + /* this term is forced as a choose, or it does not occur in the (first) read event */ + if (extterm == NULL) + { + extterm = newt; + } + else + { + extterm = makeTermTuple (newt, extterm); + // NOTE: don't these get double deleted? By roledefdestroy? + TERMLISTAPPEND (runs[rid].artefacts, extterm); + } + } + } + } + else + { + // normal variable + TERMLISTAPPEND (runs[rid].sigma, newt); + } + } + else + { + // local constant + TERMLISTADD (runs[rid].constants, newt); + } + } - /* - eprintf ("Created for run %i: ", rid); - termPrint (oldt); - eprintf (" -> "); - termPrint (newt); - eprintf ("\n"); - */ + void createLocals (Termlist list, int isvariable, int isrole) + { + while (list != NULL) + { + createLocal (list->term, isvariable, isrole); + list = list->next; + } + } - scanfrom = scanfrom->next; - } + // Create rho, sigma, constants + createLocals (protocol->rolenames, true, true); + createLocals (role->declaredvars, true, false); + createLocals (role->declaredconsts, false, false); /* Now we prefix the read before rd, if extterm is not NULL. Even if * extterm is NULL, rd is still set as the start and the index pointer of @@ -705,30 +706,6 @@ roleInstanceArachne (const System sys, const Protocol protocol, */ run_prefix_read (sys, rid, rd, extterm); - /* duplicate all locals form this run */ - scanto = role->locals; - while (scanto != NULL) - { - Term t = scanto->term; - if (!inTermlist (fromlist, t)) - { - Term newt; - - newt = create_new_local (t, rid); - if (newt != NULL) - { - artefacts = termlistAddNew (artefacts, newt); - if (realTermVariable (newt)) - { - sys->variables = termlistAdd (sys->variables, newt); - } - fromlist = termlistAdd (fromlist, t); - tolist = termlistAdd (tolist, newt); - } - } - scanto = scanto->next; - } - /* TODO this is not what we want yet, also local knowledge. The local * knowledge (list?) also needs to be substituted on invocation. */ runs[rid].know = NULL; @@ -738,7 +715,6 @@ roleInstanceArachne (const System sys, const Protocol protocol, termlistDelete (fromlist); runs[rid].locals = tolist; - runs[rid].artefacts = artefacts; /* erase any substitutions in the role definition, as they are now copied */ termlistSubstReset (role->variables); @@ -795,6 +771,10 @@ roleInstanceDestroy (const System sys) // Destroy artefacts // + termlistDelete (myrun.rho); + termlistDelete (myrun.sigma); + termlistDelete (myrun.constants); + // sys->variables might contain locals from the run: remove them { Termlist tl; @@ -822,19 +802,6 @@ roleInstanceDestroy (const System sys) } } - /* - * Arachne does real-time reduction of memory, POR does not - * Artefact removal can only be done if knowledge sets are empty, as with Arachne - */ - Termlist artefacts; - // Remove artefacts - artefacts = myrun.artefacts; - while (artefacts != NULL) - { - free (artefacts->term); - artefacts = artefacts->next; - } - /** * Undo the local copies of the substitutions. We cannot restore them however, so this might * prove a problem. We assume that the substlist fixes this at roleInstance time; it should be exact. @@ -854,10 +821,23 @@ roleInstanceDestroy (const System sys) } termlistDelete (myrun.substitutions); + /* + * Artefact removal can only be done if knowledge sets are empty, as with Arachne + */ + { + Termlist artefacts; + // Remove artefacts + artefacts = myrun.artefacts; + while (artefacts != NULL) + { + free (artefacts->term); + artefacts = artefacts->next; + } + } + // remove lists termlistDelete (myrun.artefacts); termlistDelete (myrun.locals); - termlistDelete (myrun.agents); // Destroy run struct allocation in array using realloc // Reduce run count @@ -1059,7 +1039,7 @@ isRunTrusted (const System sys, const int run) { if (run >= 0 && run < sys->maxruns) { - if (!isAgentlistTrusted (sys, sys->runs[run].agents)) + if (!isAgentlistTrusted (sys, sys->runs[run].rho)) { return 0; } @@ -1192,7 +1172,7 @@ void runInstancePrint (const System sys, const int run) { termPrint (sys->runs[run].role->nameterm); - termlistPrint (sys->runs[run].agents); + termlistPrint (sys->runs[run].rho); } //! Print an instantiated scenario (chooses and such) @@ -1350,7 +1330,7 @@ iterateLocalToOther (const System sys, const int myrun, flag = true; tlo = NULL; // construct all others occuring in the reads - for (tls = sys->runs[myrun].locals; tls != NULL; tls = tls->next) + for (tls = sys->runs[myrun].sigma; tls != NULL; tls = tls->next) { Term tt; diff --git a/src/system.h b/src/system.h index 92e3f9d..ef13334 100644 --- a/src/system.h +++ b/src/system.h @@ -41,18 +41,21 @@ struct run { Protocol protocol; //!< Protocol of this run. Role role; //!< Role of this run. - Termlist agents; //!< Agents involved in this run. int step; //!< Current execution point in the run (integer) int rolelength; //!< Length of role + Roledef index; //!< Current execution point in the run (roledef pointer) Roledef start; //!< Head of the run definition. Knowledge know; //!< Current knowledge of the run. + Termlist rho; //!< As in semantics (copies in artefacts) Termlist sigma; //!< As in semantics (copies in artefacts) Termlist constants; //!< As in semantics (copies in artefacts) + Termlist locals; //!< Locals of the run (will be deprecated eventually) - Termlist artefacts; //!< Stuff created especially for this run. + Termlist artefacts; //!< Stuff created especially for this run, which can also include tuples (anything allocated) Termlist substitutions; //!< The substitutions as they came from the roledef unifier + int prevSymmRun; //!< Used for symmetry reduction. Either -1, or the previous run with the same role def and at least a single parameter. int firstNonAgentRead; //!< Used for symmetry reductions for equal agents runs; -1 if there is no candidate. int firstReal; //!< 1 if a choose was inserted, otherwise 0 diff --git a/src/tac.c b/src/tac.c index 62cb3c9..45f0bbe 100644 --- a/src/tac.c +++ b/src/tac.c @@ -1,4 +1,5 @@ #include +#include #include "tac.h" #include "memory.h" #include "switches.h" diff --git a/src/term.c b/src/term.c index 3e97aad..4c953fc 100644 --- a/src/term.c +++ b/src/term.c @@ -313,7 +313,9 @@ termInTerm (Term t, Term tsub) *\sa termTuplePrint() */ void -termPrint (Term term) +termPrintCustom (Term term, char *leftvar, char *rightvar, char *lefttup, + char *righttup, char *leftenc, char *rightenc, + void (*callback) (int rid)) { if (term == NULL) { @@ -330,23 +332,34 @@ termPrint (Term term) #endif if (realTermLeaf (term)) { + if (term->type == VARIABLE && TermRunid (term) >= 0) + eprintf (leftvar); symbolPrint (TermSymb (term)); if (term->type == VARIABLE && TermRunid (term) >= 0) - eprintf ("V"); + eprintf (rightvar); if (TermRunid (term) >= 0) { - eprintf ("%s%i", RUNSEP, TermRunid (term)); + if (callback == NULL) + { + eprintf ("%s%i", RUNSEP, TermRunid (term)); + } + else + { + callback (TermRunid (term)); + } } if (term->subst != NULL) { eprintf ("->"); - termPrint (term->subst); + termPrintCustom (term->subst, leftvar, rightvar, lefttup, righttup, + leftenc, rightenc, callback); } } if (realTermTuple (term)) { eprintf ("("); - termTuplePrint (term); + termTuplePrintCustom (term, leftvar, rightvar, lefttup, righttup, + leftenc, rightenc, callback); eprintf (")"); return; } @@ -356,22 +369,32 @@ termPrint (Term term) && inTermlist (TermKey (term)->stype, TERM_Function)) { /* function application */ - termPrint (TermKey (term)); - eprintf ("("); - termTuplePrint (TermOp (term)); - eprintf (")"); + termPrintCustom (TermKey (term), leftvar, rightvar, lefttup, + righttup, leftenc, rightenc, callback); + eprintf (lefttup); + termTuplePrintCustom (TermOp (term), leftvar, rightvar, lefttup, + righttup, leftenc, rightenc, callback); + eprintf (righttup); } else { /* normal encryption */ - eprintf ("{ "); - termTuplePrint (TermOp (term)); - eprintf (" }"); - termPrint (TermKey (term)); + eprintf (leftenc); + termTuplePrintCustom (TermOp (term), leftvar, rightvar, lefttup, + righttup, leftenc, rightenc, callback); + eprintf (rightenc); + termPrintCustom (TermKey (term), leftvar, rightvar, lefttup, + righttup, leftenc, rightenc, callback); } } } +void +termPrint (Term term) +{ + termPrintCustom (term, "", "V", "(", ")", "{ ", " }", NULL); +} + //! Print an inner (tuple) term to stdout, without brackets. /** * The tuple printing only works correctly for normalized terms. @@ -379,7 +402,9 @@ termPrint (Term term) * desirable to distinguish them. */ void -termTuplePrint (Term term) +termTuplePrintCustom (Term term, char *leftvar, char *rightvar, char *lefttup, + char *righttup, char *leftenc, char *rightenc, + void (*callback) (int rid)) { if (term == NULL) { @@ -390,14 +415,23 @@ termTuplePrint (Term term) while (realTermTuple (term)) { // To remove any brackets, change this into termTuplePrint. - termPrint (TermOp1 (term)); + termPrintCustom (TermOp1 (term), leftvar, rightvar, lefttup, righttup, + leftenc, rightenc, callback); eprintf (","); term = deVar (TermOp2 (term)); } - termPrint (term); + termPrintCustom (term, leftvar, rightvar, lefttup, righttup, leftenc, + rightenc, callback); return; } +//! Print inner tuple +void +termTuplePrint (Term term) +{ + termTuplePrintCustom (term, "", "V", "(", ")", "{ ", " }", NULL); +} + //! Make a deep copy of a term. /** * Leaves are not copied. diff --git a/src/term.h b/src/term.h index e072ef6..0914c79 100644 --- a/src/term.h +++ b/src/term.h @@ -172,7 +172,13 @@ int hasTermVariable (Term term); int isTermEqualFn (Term term1, Term term2); int termSubTerm (Term t, Term tsub); int termInTerm (Term t, Term tsub); +void termPrintCustom (Term term, char *leftvar, char *rightvar, char *lefttup, + char *righttup, char *leftenc, char *rightenc, + void (*callback) (int rid)); void termPrint (Term term); +void termTuplePrintCustom (Term term, char *leftvar, char *rightvar, + char *lefttup, char *righttup, char *leftenc, + char *rightenc, void (*callback) (int rid)); void termTuplePrint (Term term); Term termDuplicate (const Term term); Term termNodeDuplicate (const Term term); diff --git a/src/termlist.h b/src/termlist.h index ebbce82..491da0e 100644 --- a/src/termlist.h +++ b/src/termlist.h @@ -61,4 +61,7 @@ Term termlist_to_tuple (Termlist tl); Termlist tuple_to_termlist (Term t); Termlist termlistMinusTermlist (const Termlist tlbig, const Termlist tlsmall); +#define TERMLISTADD(l,t) l = termlistAdd (l,t) +#define TERMLISTAPPEND(l,t) l = termlistAppend (l,t) + #endif