1/*  File:    scasp_just_dot.pl
    2    Author:  Roy Ratcliffe
    3    Created: Jun  8 2025
    4    Purpose: Generate a DOT graph from a JSON source produced by s(CASP)
    5    License: MIT License
    6    Version: 1.0.0
    7    Status:  Stable
    8    Updated: 2025-06-08
    9
   10Copyright (c) 2025, Roy Ratcliffe, Northumberland, United Kingdom
   11
   12Permission is hereby granted, free of charge,  to any person obtaining a
   13copy  of  this  software  and    associated   documentation  files  (the
   14"Software"), to deal in  the   Software  without  restriction, including
   15without limitation the rights to  use,   copy,  modify,  merge, publish,
   16distribute, sub-license, and/or sell copies  of   the  Software,  and to
   17permit persons to whom the Software is   furnished  to do so, subject to
   18the following conditions:
   19
   20    The above copyright notice and this permission notice shall be
   21    included in all copies or substantial portions of the Software.
   22
   23THE SOFTWARE IS PROVIDED "AS IS", WITHOUT  WARRANTY OF ANY KIND, EXPRESS
   24OR  IMPLIED,  INCLUDING  BUT  NOT   LIMITED    TO   THE   WARRANTIES  OF
   25MERCHANTABILITY, FITNESS FOR A PARTICULAR   PURPOSE AND NONINFRINGEMENT.
   26IN NO EVENT SHALL THE AUTHORS  OR   COPYRIGHT  HOLDERS BE LIABLE FOR ANY
   27CLAIM, DAMAGES OR OTHER LIABILITY,  WHETHER   IN  AN ACTION OF CONTRACT,
   28TORT OR OTHERWISE, ARISING FROM,  OUT  OF   OR  IN  CONNECTION  WITH THE
   29SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
   30
   31*/
   32
   33:- module(scasp_just_dot,
   34          [ scasp_just_dot_print/3              % Stream, Src, Options
   35          ]).   36:- autoload(library(http/json), [json_read_dict/2]).   37:- autoload(library(apply), [maplist/3]).   38:- autoload(library(option), [select_option/4, option/3]).   39:- autoload(library(dcg/high_order), [sequence//2]).   40:- use_module(library(settings), [setting/4, setting/2]).   41
   42:- setting(tab, nonneg, 2, 'Tab size for indentation').   43:- setting(rankdir, atom, 'LR', 'Direction of the graph layout').   44:- setting(bgcolor, atom, transparent, 'Background colour of the graph').   45:- setting(node, list(compound), [ style=filled,
   46                                   fillcolor=lightyellow,
   47                                   color=darkred,
   48                                   fontname="Arial",
   49                                   fontsize=10
   50                                 ], 'Node attributes').   51:- setting(edge, list(compound), [color=darkred], 'Edge default attributes').   52:- setting(edge_true, list(compound), [color=darkgreen], 'Edge attributes for true').   53:- setting(edge_false, list(compound), [color=darkred], 'Edge attributes for false').   54:- setting(edge_likely, list(compound), [ color=darkgreen,
   55                                          style=dashed
   56                                        ], 'Edge attributes for likely').   57:- setting(edge_unlikely, list(compound), [ color=darkred,
   58                                            style=dashed
   59                                          ], 'Edge attributes for unlikely').
 scasp_just_dot_print(+Stream, +Src, +Options) is det
Reads a JSON file from Src, which is expected to be in the format produced by the s(CASP) solver, and prints a DOT representation of the justification graph to the specified Stream. The Options parameter allows customisation of the output, such as indentation size, graph direction, background colour, node attributes, edge attributes, and nodes to elide.

The JSON source should contain a dictionary with the following structure, simplified for clarity:

{
    "solver": {...},
    "query": {...},
    "answers": [
        {
            "bindings": {...},
            "model": [{"truth": ..., "value": {...}}],
            "tree": {
                "node": {"value": {...}},
                "children": [
                    {
                        "node": {"value": {...}},
                        "children": [...]
                    },
                    ...
                ]
            }
        },
        ...
    ]
}

The answers field is a list of answers, each containing bindings, a model, and a tree structure. The tree field represents the justification tree, where each node has a value and may have children, forming a hierarchical structure of implications.

The output is a DOT graph representation of the justification tree, where each node corresponds to a term in the justification, and edges represent implications between nodes. The graph is directed, with arrows indicating the direction of implications from one node to another.

The output is formatted as a DOT graph, which can be visualised using graph visualisation tools like Graphviz. The output can be customised using the Options parameter, which allows for setting various attributes of the graph, such as:

This predicate is useful for visualising the justification structure of s(CASP) queries, making it easier to understand the relationships between different terms and their implications in the context of logic programming and answer set programming.

  126scasp_just_dot_print(Stream, Src, Options) :-
  127    read_json_dict(Src, Dict),
  128    phrase(json_dot(Dict, Options), Lines),
  129    print_message_lines(Stream, '', Lines).
  130
  131read_json_dict(Src, Dict) :-
  132    setup_call_cleanup(open(Src, read, Stream),
  133                       json_read_dict(Stream, Dict),
  134                       close(Stream)).
  135
  136json_dot(Dict, Options) -->
  137    tab_dot(Options), ['// solver ~s'-[Dict.solver], nl],
  138    tab_dot(Options), ['// query '], value_w(Dict.query), [nl],
  139    line_dot('digraph {', Options, Options_),
  140    answers_dot(Dict.answers, Options_),
  141    line_dot('}', Options).
  142
  143answers_dot(Answers, Options) -->
  144    setting_dot(rankdir, Options),
  145    setting_dot(bgcolor, Options),
  146    setting_dot(node, Options),
  147    setting_dot(edge, Options),
  148    sequence(answer_dot(Options), Answers).
  149
  150answer_dot(Options, Answer) -->
  151    dict_comment_dot(Answer, [excludes([ bindings,
  152                                         model,
  153                                         constraints,
  154                                         tree,
  155                                         time
  156                                       ])|Options]),
  157    { dict_pairs(Answer.bindings, _, Bindings)
  158    },
  159    sequence(binding_comment_dot(Options), Bindings),
  160    sequence(truth_comment_dot(Options), Answer.model),
  161    answer_tree_dot(Answer.tree, Options).
  162
  163answer_tree_dot(_{node:Node, children:Children}, Options) -->
  164    { value_term(Node.value, query)
  165    },
  166    line_dot('subgraph {', Options, Options_),
  167    sequence(answer_tree_query_dot([], Options_), Children),
  168    line_dot('}', Options).
  169
  170answer_tree_query_dot(Implies, Options, Answer) -->
  171    { Node = Answer.node,
  172      value_term(Node.value, Value)
  173    },
  174    line_dot('// ~w'-[Value], Options),
  175    line_dot('subgraph {', Options, Options_),
  176    sequence(implies_dot(Node, Options_), Implies),
  177    sequence(answer_tree_query_dot([Node|Implies], Options_), Answer.children),
  178    line_dot('}', Options).
 implies_dot(+Node0, +Options, +Node)// is det
Generates a DOT graph representation of an implication from Node0 to Node.

If Node0 is not in the list of elided nodes, it generates a line indicating the implication from Node0 to Node. If Node0 is in the list of elided nodes, it generates a comment line indicating that the implication is elided.

The elision is controlled by the elides/1 option in Options, which is a list of nodes that should not be displayed in the graph.

The predicate constructs a DOT line in the format:

~s"~w" -> "~w";

where ~s is replaced by the elided comment "// elided " if Node0 or Node is in the elides list, else "" if neither Node0 nor Node is elided, and the ~w format strings are replaced by the string representations of Node0 and Node.

The predicate uses the line_dot//2 DCG rule to format the output line according to the DOT syntax, including the optional comment if the node is elided. The Elides variable is used to check if either Node0 or Node is in the list of elided nodes. If neither is elided, it generates a standard DOT line containing the implication. If either is elided, it generates a comment line indicating that the implication is elided.

  208implies_dot(Node0, Options, Node) -->
  209    { value_term(Node0.value, Value0),
  210      value_term(Node.value, Value),
  211      option(elides(Elides), Options, []),
  212      (   \+ memberchk(Value0, Elides),
  213          \+ memberchk(Value, Elides)
  214      ->  Elided = ""
  215      ;   Elided = "// elided "
  216      ),
  217      edge_attributes(Node0.truth, Attributes, Options)
  218    },
  219    line_dot('~s"~w" -> "~w" ~w;'-[Elided, Value0, Value, Attributes], Options).
  220
  221edge_attributes(Truth, Attributes, Options) :-
  222    atom_string(Truth_, Truth),
  223    edge_attributes_(Truth_, Attributes, Options).
  224
  225edge_attributes_(Truth, Attributes, Options) :-
  226    option(edge(Truth, Attributes), Options),
  227    !.
  228edge_attributes_(Truth, Attributes, _) :-
  229    atomic_list_concat([edge, Truth], '_', Name),
  230    setting(Name, Attributes),
  231    !.
  232edge_attributes_(_, [], _).
  233
  234binding_comment_dot(Options, Binding-Truth) -->
  235    tab_dot(Options), ['// ~w: '-[Binding]], truth_w(Truth), [nl].
  236
  237truth_comment_dot(Options, Truth) -->
  238    tab_dot(Options), ['// '], truth_w(Truth), [nl].
  239
  240dict_comment_dot(Dict, Options) -->
  241    { dict_pairs(Dict, _, Pairs)
  242    },
  243    sequence(pair_comment_dot(Options), Pairs).
  244
  245pair_comment_dot(Options, Key-Value) -->
  246    { includes_or_not_excludes(Key, Options)
  247    },
  248    !,
  249    line_dot('// ~k ~k'-[Key, Value], Options).
  250pair_comment_dot(_, _) --> [].
 includes_or_not_excludes(+Key, +Options) is semidet
Determines if a Key should be included in the output based on the provided Options. Succeeds if Key is included (if includes/1 is present), not excluded (if excludes/1 is present), or always succeeds if neither option is present.

If the includes/1 option is present, it checks if Key is a member of the Includes list. If the excludes/1 option is present, it checks that Key is not a member of the Excludes list.

  263includes_or_not_excludes(Key, Options) :-
  264    (   option(includes(Includes), Options)
  265    ->  memberchk(Key, Includes)
  266    ;   option(excludes(Excludes), Options)
  267    ->  \+ memberchk(Key, Excludes)
  268    ;   true % succeed if neither includes nor excludes (default behaviour)
  269    ).
  270
  271setting_dot(Name, Options) -->
  272    { setting(Name, Value)
  273    },
  274    setting_dot(Name, Value, Options).
  275
  276setting_dot(Name, Value, Options) -->
  277    { is_list(Value)
  278    },
  279    !,
  280    line_dot('~p ~p;'-[Name, Value], Options).
  281setting_dot(Name, Value, Options) -->
  282    line_dot('~w;'-[Name=Value], Options).
  283
  284tab_dot(Options0, Options) -->
  285    { indent(Options0, Tab, Options)
  286    },
  287    [Tab].
  288
  289tab_dot(Options) --> tab_dot(Options, _).
  290
  291line_dot(Line, Options0, Options) --> tab_dot(Options0, Options), [Line, nl].
  292
  293line_dot(Line, Options) --> line_dot(Line, Options, _).
  294
  295truth_w(_{truth:Truth, value:Value}) -->
  296    { value_term(Value, Term)
  297    },
  298    ['~w ~w'-[Truth, Term]].
  299
  300value_w(Value) -->
  301    { value_term(Value, Term)
  302    },
  303    ['~w'-[Term]].
 value_term(+Value:dict, -Term) is semidet
Converts a Prolog dictionary (parsed from JSON) that represents a term into an actual Prolog term. The predicate deals with cases where the dictionary represents different types of terms, such as variables, atoms, numbers, rational numbers, and compound terms. It recursively processes the arguments of compound terms to construct the final term. The predicate handles the following cases:

The predicate employs dictionary pattern matching (:<) to safely extract the relevant fields from the dictionary, and for clarity. It handles nested compounds by recursively mapping the arguments to value terms. The predicate is semi-deterministic, meaning it succeeds at most once; if the input dictionary does not match any of the expected patterns, it fails silently. This allows for safe handling of the JSON structure without raising exceptions for unexpected formats.

The implementation assumes that the JSON structure follows a specific format, where each term is represented as a dictionary with a type field indicating whether it is a variable, atom, number, rational, or compound. If the JSON structure changes or new term types are added, the predicate will require updating.

The value_term/2 predicate is used to convert the JSON representation of terms into Prolog terms, which can then be used in further processing or output---particularly useful in the context of generating a DOT graph from a JSON source produced by s(CASP), where terms represent nodes in the justification tree. It is a crucial part of justification tree processing, allowing the conversion of JSON representations of terms into Prolog terms that can be used to construct the graph structure, and designed to be used in conjunction with the dict_term/2 helper predicate, which handles the conversion of a Prolog dictionary (parsed from JSON) into a Prolog term. The dict_term/2 predicate is responsible for converting the dictionary representation of terms into actual Prolog terms.

  351value_term(Value, Term), is_dict(Value) => dict_term(Value, Term).
  352value_term(Value, List), is_list(Value) => maplist(value_term, Value, List).
  353
  354dict_term(Value, Var), _{type:"var",
  355                         name:Var} :< Value => true.
  356dict_term(Value, Atom), _{type:"atom",
  357                          value:String} :< Value => atom_string(Atom, String).
  358dict_term(Value, Value), _{type:"number",
  359                           value:Value} :< Value => true.
  360dict_term(Value, Rational), _{type:"rational",
  361                              numerator:Numerator,
  362                              denominator:Denominator} :< Value =>
  363    rational(Rational, Numerator, Denominator).
  364dict_term(Value, Term), _{type:"compound",
  365                          functor:Functor,
  366                          args:Args} :< Value =>
  367    atom_string(Functor_, Functor),
  368    maplist(value_term, Args, Args_),
  369    Term =.. [Functor_|Args_].
 indent(+Options0:list, +Width:nonneg, -Tab:compound, -Options:list) is det
Computes the next indentation level and returns a tabulation format for output.
  381indent(Options0, Width, '~t~*|'-[Indent0], [indent(Indent)|Options]) :-
  382    select_option(indent(Indent0), Options0, Options, 0),
  383    Indent is Indent0 + Width.
  384
  385indent(Options0, Tab, Options) :-
  386    setting(tab, DefaultWidth),
  387    option(tab(Width), Options0, DefaultWidth),
  388    indent(Options0, Width, Tab, Options)