ProTrace is a tracing module created to trace rule applications on expressions when an Essence file is parsed and rewritten by Conjure Oxide. The purpose of the module is to visualise the rules applied on the expressions, and simplify the identification of errors for debugging. The module supports multiple output formats such as JSON or human readable, along with different verbosity levels to show only what the user would like to see.

The different verbosity levels include:

• High: All rule applications.
• Medium (default): Successful rule applications.
• Low: Only errors are shown (to be implemented).

Outputs of the trace can be saved in a JSON or text file (depending on the format of trace) when specified by the user, and if the file path is not given, the output will be stored in the location of the input Essence file by default.

The module also provides filtering functionalities for displaying specific rule or rule set applications.

The module is capable of tracing two types of objects: rule and model. A trace can be created using capture_trace, which takes a consumer and a trace type (RuleTrace or ModelTrace).

pub fn capture_trace(consumer: &Consumer, trace: TraceType)

pub enum TraceType<'a> {
    RuleTrace(RuleTrace),
    ModelTrace(&'a ModelTrace),
}

Rules are applied to a given expression to rewrite it into the syntax that Conjure understands. These rule applications can be traced by the module to show users what rules have been tried and successfully applied during parsing. A rule trace consists of:

• An initial expression
• The name of the rule being applied
• The priority of the rule being applied
• The rule set that the rule belongs to
• A transformed expression as a result of rule application
• An optional new variable created during the rule application
• An optional new constraint added to the top of the expression tree created during the rule application

pub struct RuleTrace {
    pub initial_expression: Expression,
    pub rule_name: String,
    pub rule_priority: u16,
    pub rule_set_name: String,
    pub transformed_expression: Option<Expression>,
    pub new_variables_str: Option<String>,
    pub top_level_str: Option<String>,
}

Models of the problem contain expressions along with some constraints. A model trace consists of:

• An initial model
• A rewritten model after rule application

pub struct ModelTrace {
    pub initial_model: Model,
    pub rewritten_model: Option<Model>,
}

Formatters are responsible for converting trace information into a human-readable or JSON string format before it is output by a consumer.

At the core of this system is the MessageFormatter trait, which defines a common interface for all formatters. There are two built-in formatter implementations provided: HumanFormatter and JsonFormatter.

pub trait MessageFormatter: Any + Send + Sync {
    fn format(&self, trace: TraceType) -> String;
}

pub struct HumanFormatter

The HumanFormatter implements the MessageFormatter trait by matching on TraceType and returning a formatted String. All TraceType variants implement the Display trait, which allows for easy string conversion.

Behaviour:

• Successful Rule Applications

  • A message "Successful Transformation" followed by the full formatted RuleTrace, displaying all of its fields.

• Unsuccessful Rule Applications

  • A message like "Unsuccessful Transformation" followed by a partial display showing only:

    • initial expression
    • rule name
    • rule priority
    • rule set name

  • Only shown if the VerbosityLevel is set to High.

• Model Traces

  • For ModelTrace, it simply displays the initial and rewritten model using its Display implementation.

Filtering: Before formatting, the HumanFormatter checks if a rule name filter or rule set name filter has been applied.

pub struct JsonFormatter

The JsonFormatter implements the MessageFormatter trait by matching on TraceType and returning a JSON-formatted String. It uses the serde_json library to serialize data into a pretty-printed JSON structure.

Behaviour:

• Rule Transformations

  • For RuleTrace, it serializes the entire RuleTrace object into a pretty-printed JSON string using serde_json::to_string_pretty.

  • Similar to HumanFormatter displays both successful and unsuccessful rule applications when the verbosity is high.

• Model Traces

  • For ModelTrace, no JSON output is generated. No need since the parsed and rewritten models are produced in JSON already.

Filtering: Before formatting, the JsonFormatter checks if a rule name filter or rule set name filter has been applied.

The Consumer enum represents different types of endpoints that receive, format, and output TraceType data.

Consumers control where the trace data goes to and which format.

• StdoutConsumer prints out the trace to the console
• FileConsumer writes the trace data to a file in one of three ways: as human-readable text, as JSON-formatted text, or to both file types simultaneously.
• BothConsumer writes to both stdout and file(s).

pub enum Consumer {
    StdoutConsumer(StdoutConsumer),
    FileConsumer(FileConsumer),
    BothConsumer(BothConsumer),
}

Each variant implements the Trace trait, meaning it can capture traces and send them to the appropriate destination.

pub trait Trace {
    fn capture(&self, trace: TraceType);
}

A StdoutConsumer outputs the formatted trace data to standard output.

Holds:

• A reference-counted (Arc) formatter that implements the MessageFormatter trait.
  • Arc (Atomic Reference Counted pointer) allows safe shared ownership across multiple consumers.
  • Multiple Consumers might want to share the same formatter without each owning and duplicating it.
• A verbosity VerbosityLevel that can influence what gets printed.

pub struct StdoutConsumer {
    pub formatter: Arc<dyn MessageFormatter>,
    pub verbosity: VerbosityLevel,
}

dyn = dynamic dispatch. At runtime, it calls the correct format method for the actual formatter. When capturing a trace: It formats the trace using its assigned formatter.

A FileConsumer writes the formatted trace data to one or more files.

Holds:

• A reference-counted (Arc) formatter.
• A formatter type to determine whether to write in Human, JSON, or both formats.
• verbosity
• Path to the file for the JSON trace. (Optional)
• Path to the file for the human-readable trace. (Optional)
• is first flag used for managing JSON array formatting when appending traces.

pub struct FileConsumer {
    pub formatter: Arc<dyn MessageFormatter>,
    pub formatter_type: FormatterType,
    pub verbosity: VerbosityLevel,
    pub json_file_path: Option<String>, 
    pub human_file_path: Option<String>, 
    pub is_first: std::cell::Cell<bool>, 
}

When capturing a trace:

Based on the selected FormatterType: Human: Writes human-readable output to the human file. Json: Writes JSON output to the JSON file. Both: Writes to both files using respective formatters (HumanFormatter and JsonFormatter directly).

A BothConsumer sends the formatted trace data to both:

• Standard output (via an internal StdoutConsumer)
• Files (via an internal FileConsumer)

pub struct BothConsumer {
    stdout_consumer: StdoutConsumer,
    file_consumer: FileConsumer,
}

It combines the behaviours of StdoutConsumer and FileConsumer by calling method capture on both its fields.

If users would like to only see specific rules or rule sets during rule application tracing, rule filters can be applied using the command-line argument --filter-rule-name or --filter-rule-set followed by comma-separated rule names or sets. The output will only show rules that is in the rule filters, otherwise the rule application will be completely skipped. This feature was added for the abstraction of unimportant rule applications during tracing, allowing users to only see the rules they require.

When both rule name and rule set filters are used in tandem, any rules that pass either the rule name or the rule set filter will be displayed. For example, if the rule name filter is normalise_associative_commutative and the rule set filter is Minion, any rule that has the rule name normalise_associative_commutative or is in the rule set Minion will be displayed.

Rule filters will be applied to both FileConsumer and StdoutConsumer.

Rule filters can alse be hard-coded into the program or accessed using the following functions:

pub fn set_rule_filter(rule_name: Option<Vec<String>>)

pub fn get_rule_filter() -> Option<Vec<String>>

pub fn set_rule_set_filter(rule_set: Option<Vec<String>>)

pub fn get_rule_set_filter() -> Option<Vec<String>>

This feature was motivated by the need for a unified interface that allows developers to capture messages—whether to stdout or a file—with the flexibility of a typical debug print statement, but with added control.

Default messages are always printed out and additional message types can be filtered and viewed using the command-line argument --get-info-about, followed by the desired message Kind.

For example, running --get-info-about rules will display all the enabled rule sets, individual rules, their assigned priorities, and the sets they belong to. To improve readability, output is color-coded: error messages appear in red, while all other information is shown in green.

pub enum Kind {
    Parser,
    Rules,
    Error,
    Solver,
    Model,
    Default,
}
fn display_message(message: String, file_path: Option<String>, kind: Kind)

Similar to how a Consumer is created in solve.rs for cargo run solve, a combined_consumer is manually constructed for each integration test, with its fields explicitly set rather than being derived from command-line arguments. This consumer is configured to log successful rule applications to two separate files—one in a human-readable format and the other in JSON. It is then passed to the rewrite_naive function. By establishing a uniform internal interface for tracing in both cargo run and cargo test, we were able to significantly reduce code duplication and streamline the overall tracing logic.

   let combined_consumer = create_consumer(
            "file",
            VerbosityLevel::Medium,
            "both",
            Some(format!("{path}/{essence_base}.generated-rule-trace.json")),
            Some(format!("{path}/{essence_base}.generated-rule-trace.txt")),
        );

The rule traces is verified using the functions read_human_rule_trace and read_json_rule_trace defined in testing.rs which compare the generated trace output to the expected one. read_json_rule_trace ignores the id fields since they can change from one run to another.

Enable rule tracing

-T, --tracing

Select output location for trace result: stdout or file [default: stdout]

-L, --trace-output <TRACE_OUTPUT>

Select verbosity level for trace [default: medium] [possible values: low, medium, high]

--verbosity <VERBOSITY>

Select the format of the trace output: human or json [default: human]

-F, --formatter <FORMATTER>

Optionally save traces to specific files: first for JSON, second for human format

-f, --trace-file [<JSON_TRACE> <HUMAN_TRACE>]

Filter messages by given kind [possible values: parser, rules, error, solver, model, default]

--get-info-about <KIND_FILTER>

Filter rule trace to only show given rule names (comma separated)

--filter-rule-name <RULE_NAME_FILTER>

Filter rule trace to only show given rule set names (comma separated)

--filter-rule-set <RULE_SET_FILTER>