Mercury programs are heavily transformed before any code is generated. Procedures are put into superhomogeneous form, high order predicates are transformed into first order predicates, some procedures can be inlined; under the commutative semantics, conjunctions and disjunctions can be evaluated in any order. Hence, it is sometimes difficult to relate Mercury source code with its corresponding trace, even if the program is compiled using the strict sequential semantics with all the optimizations switched off. In order to relate the trace with the initial program, it might sometimes be helpful to have a look at the HLDS code (see the Mercury User and Language Reference Manuals [6,5]).
Morphine is connected to the traditional tracer of Mercury. We describe in sub-sections 2.2 to 2.4 the information contained in the trace and we specify in what order each type of events occurs. These descriptions give another point of view of the ``Tracing Mercury Programs'' section of the Mercury user manual3.
A trace is therefore a sequence of events, where each event can be seen as a tuple of a relational database. This trace model is the basis of the trace query mechanism.
The different event attributes are as follows. The identifiers in teletype font are the names used in Morphine to denote event attributes.
(chrono)
attached to an event.
Each event has a unique event number according to its rank in the trace. It is a counter of events.
(call)
attached to a goal.
All events related to a given goal have a unique goal number given at invocation time.
(depth) attached to a goal.
It is the depth of the goal in the proof tree, namely the number of its ancestor goals + 1.
(port) attached to an event.
The different Mercury event types are as follows. We distinguish between external events which are the traditional ports introduced by Byrd [1], and the internal events which refers to what is occurring inside a procedure.
External events
call a new procedure is invoked
exit the current procedure succeeds
fail the current procedure fails
redo another solution for the current procedure is asked for
on backtracking, and a subgoal of the procedure has a choice point.
Internal events:
disj the execution is entering a branch of a disjunction
switch the execution is entering a branch of a switch
then the execution is entering the ``then'' branch of an if-then-else
else the execution is entering the ``else'' branch of an if-then-else
first the execution enters a C code fragment for the first time
later the execution re-enters a C code fragment
exception the execution raises an exception
(det) attached to a goal.
The different Mercury determinism marks are as follows. They characterize the number of potential solutions for a given goal.
det exactly one solution
semidet 0 or 1 solution
nondet 0 or any number of solutions
cc_nondet 0 or one solution
multi at least one solution
cc_multi exactly one solution
failure no solution
erroneous leads to a runtime error
(proc) attached to a goal. A procedure is defined by:
(proc_type)
(def_module)
(decl_module)
(name)
(arity) and a
(mode_number).
The declaration module is the module where the user has declared the procedure. The defining module is the module where the procedure is effectively defined from the compiler point of vue. They may be different if the procedure has been inlined.
The mode number is an integer coding the mode of the procedure. When a predicate has only one mode, the mode number of its corresponding procedure is 0. Otherwise, the mode number is the rank in the order of appearance of the mode declaration.
(args) attached
to a goal and an event.
It gives the current instantiation of the live procedure arguments. We say that
a variable is live at a given point of the execution if it has been
instantiated and if the result of that instantiation is still available. When
it is known that a variable will not be used again, its content is not usually
kept by the Mercury compiler. However, when tracing is on, the content of input
arguments are kept live until the procedure exits, destructive input (di
mode) arguments excepted.
(arg_types) attached
to a goal and an event
It gives the types of the live procedure arguments.
(local_vars)
It gives the instantiation, the types and the names of live local variables that are not arguments of the current procedure.
(GoalPath) attached to a goal and an internal
event.
The goal path indicates in which part of the code the current event
occurs. then and else branches of an if-then-else are
denoted by e and t; conjuncts, disjuncts and
switches are denoted by ci, di and si, where
i is the conjunct (resp disjunct, switch) number.
For example, if an event with goal path [c3, e, d1] is generated, it
means that the event occurred in the first branch of a disjunction, which is in
the else branch of an if-then-else, which is in the third conjunction of the
current goal.
The event structure is illustrated by Figure 1. The
displayed structure is related to an event of the execution of the qsort
program which sorts the list of integers [3, 1, 2] using a
quick sort algorithm. The full code of qsort.m is given in Appendix
A. The information contained in that structure indicates that procedure
qsort:partition/4-0 is currently invoked, it is the 10th trace
events being generated, the 6th goal being invoked, and it has 4thancestors (depth is 5). At this point, only the first two arguments of
partition/4 are instantiated: the first one is bounded to the list of
integer [1, 2] and the second one to the integer 3 ; third and
fourth variable are not live which is indicated by the `-'. The two live local
variables are H, bound to the integer 1, and T bound to
the list of integer [2]. This event occurred in the then branch
of the second conjunction of the first switch of the code of
partition/4.
We call trace of a program execution a sequence of events of the same format; in a sense, a trace is a discretisation of the execution. The Mercury trace can be seen as an extended version of the Byrd box model [1] that binds execution events to goals. In this sub-section, we give a specification of the Mercury trace from the point of view of a given goal in extended BNF notation. Depending on the determinism of the procedure, different sequences of events will be generated.
![\begin{figure}\begin{center}
\begin{tabular}{\vert l\vert c\vert}
\hline
\verb*+...
...
\verb*+ 10: 6 [5] then partition([1, 2], 3, -, -) [s1, c2, t]+
\par\end{figure}](img5.gif)
<det> --> call {disj | switch | then | else}* exit
<semidet> --> call {disj | switch | then | else}* {exit | fail}
<multi> --> call <multi_end>
<multi_end> --> {disj | switch | then | else}*
{exit redo <multi_end> | fail}
<cc_multi> --> call {disj | switch | then | else}* exit
<nondet> --> call <nondet_end>
<nondet_end> --> {disj | switch | then | else}*
{exit redo <nondet_end> | exit | fail}
<cc_nondet> --> call {disj | switch | then | else}*
{exit | fail}
failure --> call fail
<c_code> --> first {later}*
Figure 2 shows an exhaustive trace of the execution of the
qsort program (see Appendix A) on the list [3, 1,2].
In this trace, we only print the following event attributes: Chrono
:Call [Depth] Port Proc/Arity
ArgList GoalPath. We also filtered out all the
procedures that were defined in the module printlist.m which
are not of interest here.
Note that input argument of main procedure is not available at exit ports
(event 65) since it is destructively updated. Note also the hole
between events 48 and 65 that corresponds to events occurring in
printlist.m module.
![\begin{figure}\small
\begin{tex2html_preform}\begin{verbatim}[Morphine]: fget([m...
... main(-, state('<<c_pointer>>'))\end{verbatim}\end{tex2html_preform}\end{figure}](img6.gif)