1:- module(scasp_output,
    2          [ print_model_term/2,
    3            inline_constraints/2,                % +Term, +Options
    4            connector/3,                         % +Semantics,-Conn,+Options
    5            print_connector/2,
    6            ovar_analyze_term/1,                 % +Term
    7            ovar_analyze_term/2,                 % +Term,+Options
    8            ovar_clean/1,                        % +Term
    9            ovar_is_singleton/1,                 % @Var
   10            ovar_var_name/2,                     % @Var, -Name
   11            ovar_set_name/2,                     % +Var, +Name
   12            ovar_set_bindings/1,                 % +Bindings
   13            human_expression/3                   % :Tree, -Children, -Actions
   14          ]).   15:- use_module(library(ansi_term)).   16:- use_module(library(apply)).   17:- use_module(library(option)).   18:- use_module(library(lists)).   19:- use_module(library(prolog_code)).   20:- use_module(library(prolog_format)).   21:- use_module(library(terms)).   22
   23:- use_module(clp/disequality).   24:- use_module(clp/clpq).   25
   26:- meta_predicate
   27    human_expression(:, -, -).

 print_model_term(+Term, +Options) is det

Print a model element to the terminal.

   37:- det(print_model_term/2).   38
   39print_model_term(not(-Term), Options) =>
   40    print_connector(not, Options),
   41    print_connector(negation, Options),
   42    print_plain(Term, likely, Options).
   43print_model_term(-Term, Options) =>
   44    print_connector(negation, Options),
   45    print_plain(Term, false, Options).
   46print_model_term(not(Term), Options) =>
   47    print_connector(not, Options),
   48    print_plain(Term, unlikely, Options).
   49print_model_term(Term, Options) =>
   50    print_plain(Term, true, Options).
   51
   52print_plain(M:Term, Trust, Options) :-
   53    atom(M),
   54    !,
   55    ansi_format(fg('#888'), '~q:', [M]),
   56    print_plain(Term, Trust, Options).
   57print_plain(Term, Trust, _Options) :-
   58    style(Trust, Style),
   59    ansi_format(Style, '~p', [Term]).
   60
   61print_connector(Semantics, Options) :-
   62    connector(Semantics, Conn, Options),
   63    ansi_format(fg(cyan), '~w', [Conn]).
   64
   65style(true,     [bold]).
   66style(false,    [bold, fg(red)]).
   67style(likely,   []).
   68style(unlikely, [fg(red)]).

 connector(+Semantics, -Conn, +Options) is det

Get an ASCII or Unicode connector string with the claimed Semantics.

   75:- det(connector/3).   76
   77connector(Semantics, Conn, Options) :-
   78    option(format(Format), Options, unicode),
   79    connector_string(Semantics, Format, Conn),
   80    !.
   81
   82connector_string(implies,  ascii, ':-').
   83connector_string(and,      ascii, ',').
   84connector_string(negation, ascii, '-').
   85
   86connector_string(implies,  unicode, '\u2190').   % <-
   87connector_string(and,      unicode, ' \u2227').  % /\
   88connector_string(negation, unicode, '\u00ac ').  % -
   89
   90connector_string(not,      _, 'not ').
   91connector_string(proved,   _, 'proved').
   92connector_string(assume,   _, 'assume').
   93connector_string(chs,      _, 'chs').
   94
   95
   96		 /*******************************
   97		 *          CONSTRAINTS		*
   98		 *******************************/

 inline_constraints(+Term, +Options) is det

Get constraints on variables notated as Var | {Constraints} and use assigned variable names. Note that this binds the attributed variables in Term. This code is normally used on a copy or inside double negation (\+ \+ ( inline_constraints(Term, Options), ...)).

  108inline_constraints(Term, Options) :-
  109    term_attvars(Term, AttVars),
  110    maplist(inline_constraint(Options), AttVars).
  111
  112inline_constraint(_Options, Var) :-
  113    get_neg_var(Var, List),
  114    List \== [],
  115    !,
  116    var_name(Var, Name),
  117    del_attrs(Var),
  118    Var = '| '(Name, {'\u2209'(Name, List)}).
  119inline_constraint(_Options, Var) :-
  120    is_clpq_var(Var),
  121    clpqr_dump_constraints([Var], [Var], Constraints),
  122    Constraints \== [],
  123    !,
  124    var_name(Var, Name),
  125    sort(0, @>, Constraints, Sorted),
  126    comma_list(Term0, Sorted),
  127    del_attrs(Var),
  128    replace_var(Var, Name, Term0, Term),
  129    Var = '| '(Name, {Term}).
  130inline_constraint(_Options, Var) :-
  131    var_name(Var, Name),
  132    del_attrs(Var),
  133    Var = Name.
  134
  135var_name(Var, Name) :-
  136    ovar_var_name(Var, Name0),
  137    !,
  138    Name = '$VAR'(Name0).
  139var_name(Var, Name) :-
  140    ovar_is_singleton(Var),
  141    !,
  142    Name = '$VAR'('_').
  143var_name(Var, Var).

 replace_var(+Var, +Name, +TermIn, -TermOut)

  147replace_var(Var, Name, TermIn, TermOut) :-
  148    Var == TermIn,
  149    !,
  150    TermOut = Name.
  151replace_var(Var, Name, TermIn, TermOut) :-
  152    compound(TermIn),
  153    !,
  154    same_functor(TermIn, TermOut, Arity),
  155    replace_var(1, Arity, Var, Name, TermIn, TermOut).
  156replace_var(_, _, Term, Term).
  157
  158replace_var(I, Arity, Var, Name, TermIn, TermOut) :-
  159    I =< Arity,
  160    !,
  161    arg(I, TermIn, AIn),
  162    arg(I, TermOut, AOut),
  163    replace_var(Var, Name, AIn, AOut),
  164    I2 is I+1,
  165    replace_var(I2, Arity, Var, Name, TermIn, TermOut).
  166replace_var(_, _, _, _, _, _).
  167
  168
  169
  170
  171
  172		 /*******************************
  173		 *        VARIABLE ANALYSIS	*
  174		 *******************************/

 ovar_analyze_term(+Term) is det

 ovar_analyze_term(+Term, +Options) is det

Analyze variables in an output term. Adds attributes to these variables that indicate their status and make this available through ovar_is_singleton/1 and ovar_var_name/1.

  183ovar_analyze_term(Tree) :-
  184    ovar_analyze_term(Tree, []).
  185
  186ovar_analyze_term(Tree, Options) :-
  187    term_attvars(Tree, AttVars),
  188    convlist(ovar_var_name, AttVars, VarNames),
  189    term_singletons(Tree, Singletons),
  190    term_variables(Tree, AllVars),
  191    (   option(name_constraints(true), Options)
  192    ->  maplist(mark_singleton_no_attvar, Singletons)
  193    ;   maplist(mark_singleton, Singletons)
  194    ),
  195    foldl(name_variable(VarNames), AllVars, 0, _).
  196
  197mark_singleton(Var) :-
  198    (   ovar_var_name(Var, _)
  199    ->  true
  200    ;   put_attr(Var, scasp_output, singleton)
  201    ).
  202
  203mark_singleton_no_attvar(Var) :-
  204    (   attvar(Var)
  205    ->  true
  206    ;   put_attr(Var, scasp_output, singleton)
  207    ).
  208
  209name_variable(Assigned, Var, N0, N) :-
  210    (   (   ovar_is_singleton(Var)
  211        ;   ovar_var_name(Var, _)
  212        )
  213    ->  N = N0
  214    ;   between(N0, 100000, N1),
  215        L is N1 mod 26 + 0'A,
  216        I is N1 // 26,
  217        (   I == 0
  218        ->  char_code(Name, L)
  219        ;   format(atom(Name), '~c~d', [L, I])
  220        ),
  221        \+ memberchk(Name, Assigned)
  222    ->  ovar_set_name(Var, Name),                % make sure it is unique
  223        N is N1+1
  224    ).
  225
  226attr_unify_hook(_Attr, _Value).

 ovar_clean(+Term)

Delete all attributes added by ovar_analyze_term/1

  232ovar_clean(Term) :-
  233    term_attvars(Term, Attvars),
  234    maplist(del_var_info, Attvars).
  235
  236del_var_info(V) :-
  237    del_attr(V, scasp_output).

 ovar_is_singleton(@Var) is semidet

True when Var is a singleton variable

  244ovar_is_singleton(Var) :-
  245    get_attr(Var, scasp_output, singleton).

 ovar_set_name(+Var, +Name)

Set the name of Var to Name.

  251ovar_set_name(Var, Name) :-
  252    put_attr(Var, scasp_output, name(Name)).

 ovar_set_bindings(+Bindings) is det

Given Bindings as a list of Name=Var, set the names of the variables.

  259ovar_set_bindings(Bindings) :-
  260    maplist(ovar_set_binding, Bindings).
  261
  262ovar_set_binding(Name=Var) :-
  263    (   var(Var)
  264    ->  ovar_set_name(Var, Name)
  265    ;   true
  266    ).

 ovar_var_name(@Var, -Name) is semidet

True when var is not a singleton and has the assigned name. Names are assigned as A, B, ... A1, B1, ...

  273ovar_var_name(Var, Name) :-
  274    get_attr(Var, scasp_output, name(Name)).
  275
  276
  277		 /*******************************
  278		 *         HUMAN (#PRED)	*
  279		 *******************************/

 human_expression(:Tree, -Children, -Actions) is semidet

If there is a human print rule for Atom, return a list of format actions as Actions. Actions is currently a list of text(String) and @(Var:Type), where Type can be the empty atom.

  287human_expression(Tree, Children, Actions) :-
  288    tree_atom_children(Tree, M, Atom, ChildrenIn),
  289    current_predicate(M:pr_pred_predicate/4),
  290    \+ predicate_property(M:pr_pred_predicate(_,_,_,_), imported_from(_)),
  291    human_utterance(Atom, ChildrenIn, M, Children, Human),
  292    (   Human = format(Fmt, Args)
  293    ->  parse_fmt(Fmt, Args, Actions)
  294    ;   Actions = Human                          % html(Terms)
  295    ).
  296
  297tree_atom_children(M0:(Atom0-Children), M, Atom, Children) :-
  298    clean_atom(Atom0, M0, Atom, M).
  299
  300clean_atom(goal_origin(Atom0, _), M0, Atom, M) =>
  301    clean_atom(Atom0, M0, Atom, M).
  302clean_atom(not(-Atom0), M0, Atom, M) =>
  303    Atom = not(-Atom1),
  304    strip_module(M0:Atom0, M, Atom1).
  305clean_atom(not(Atom0), M0, Atom, M) =>
  306    Atom = not(Atom1),
  307    strip_module(M0:Atom0, M, Atom1).
  308clean_atom(-(Atom0), M0, Atom, M) =>
  309    Atom = -(Atom1),
  310    strip_module(M0:Atom0, M, Atom1).
  311clean_atom(Atom0, M0, Atom, M) =>
  312    strip_module(M0:Atom0, M, Atom).
  313
  314human_utterance(Atom, Children0, M, Children, Format) =>
  315    M:pr_pred_predicate(Atom, ChildSpec, Cond, Format),
  316    match_children(ChildSpec, M, Children0, Children),
  317    call(Cond),
  318    !.
  319
  320match_children(*, _, Children0, Children) =>
  321    Children = Children0.
  322match_children(-, _, _, Children) =>
  323    Children = [].
  324match_children([H|T], M, Children0, Children) =>
  325    append(Pre, [Atom-C0|Post], Children0),
  326    match_node(H, M, Atom, C0, C),
  327    !,
  328    append([Pre,C,Post], Children2),
  329    match_children(T, M, Children2, Children).
  330match_children([], _, Children0, Children) =>
  331    Children = Children0.
  332
  333match_node(Node-ChildSpec, M, Atom, C0, C) =>
  334    match_node(Node, M, Atom),
  335    match_children(ChildSpec, M, C0, C).
  336match_node(Node, M, Atom, C0, C) =>
  337    match_node(Node, M, Atom),
  338    C = C0.

 match_node(+Spec, +Module, +Atom) is semidet

Succeed if Spec (from the :- pred declaration) matches Atom from the justification tree.

  345match_node(Node, M, goal_origin(Child, _)) :-
  346    !,
  347    match_node(Node, M, Child).
  348match_node(Node, _M, Node).
  349match_node(Node, _M, proved(Node)).
  350match_node(not(Node), M, not(M:Node)).
  351match_node(Node, M, proved(M:Node)).
  352match_node(Node, M, M:Node).

 parse_fmt(+Fmt, +Args, -Actions) is det

Translate a human template and its arguments into a list of actions for our DCG. The template allows form interpolating a variable, optionally with a type. The core translator adds ~p to the format and a term @(Var:Type) or @(Var:'') to the arguments. Actions is a list of text(String) or @(Var:Type).

  362:- det(parse_fmt/3).  363
  364parse_fmt(Fmt, Args, Actions) :-
  365    format_spec(Fmt, Spec),
  366    fmt_actions(Spec, Args, Actions).
  367
  368fmt_actions([], [], []).
  369fmt_actions([text(S)|T0], Args, [text(S)|T]) :-
  370    fmt_actions(T0, Args, T).
  371fmt_actions([escape(nothing, no_colon, p)|T0], [A0|Args], [A0|T]) :-
  372    fmt_actions(T0, Args, T).
  373
  374% portray rules for inlines constraints. Possibly we need something that
  375% alows us to specify that an operator always requires spaces?
  376
  377user:portray('| '(Var, Constraints)) :-
  378    format('~p | ~p', [Var, Constraints]).
  379user:portray('\u2209'(Var, List)) :-
  380    format('~p \u2209 ~p', [Var, List])