1/*  Part of s(CASP)-Prolog
    2
    3    Author:        Jan Wielemaker
    4    E-mail:        jan@swi-prolog.org
    5    WWW:           https://www.swi-prolog.org
    6    Copyright (c)  2021-2023, SWI-Prolog Solutions b.v.
    7    All rights reserved.
    8
    9    Redistribution and use in source and binary forms, with or without
   10    modification, are permitted provided that the following conditions
   11    are met:
   12
   13    1. Redistributions of source code must retain the above copyright
   14       notice, this list of conditions and the following disclaimer.
   15
   16    2. Redistributions in binary form must reproduce the above copyright
   17       notice, this list of conditions and the following disclaimer in
   18       the documentation and/or other materials provided with the
   19       distribution.
   20
   21    THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
   22    "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
   23    LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
   24    FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
   25    COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
   26    INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
   27    BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
   28    LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
   29    CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
   30    LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
   31    ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
   32    POSSIBILITY OF SUCH DAMAGE.
   33*/
   34
   35:- module(scasp_just_html,
   36          [ html_justification_tree//2,		% :Tree, +Options
   37            html_model//2,			% :Model, +Options
   38            html_model_term//2,			% :Atom, +Options
   39            html_bindings//2,                   % :Bindings, +Options
   40            html_program/1,                     % :Dict
   41            html_program//1,                    % :Dict
   42            html_query//2,                      % :Query, +Options
   43            html_predicate//2,                  % :Predicate, +Options
   44            html_rule//2,                       % :Rule, +Options
   45            html_term//2                        % +Term, +Options
   46          ]).   47:- use_module(common).   48:- use_module(output).   49:- use_module(html_text).   50:- use_module(messages).   51:- use_module(source_ref).   52:- use_module(listing).   53
   54:- use_module(library(http/html_write)).   55:- use_module(library(http/term_html)).   56:- use_module(library(http/html_head), [html_resource/2]).   57:- if(exists_source(library(http/http_server_files))).   58:- use_module(library(http/http_server_files), []).   59:- endif.   60:- use_module(library(dcg/high_order)).   61:- use_module(library(lists)).   62:- use_module(library(option)).   63:- use_module(library(prolog_code)).   64:- use_module(library(apply)).   65
   66:- meta_predicate
   67    html_model(:, +, ?, ?),
   68    html_model_term(:, +, ?, ?),
   69    html_justification_tree(:, +, ?, ?),
   70    html_program(:),
   71    html_program(:, ?, ?),
   72    html_query(:, +, ?, ?),
   73    html_predicate(:, +, ?, ?),
   74    html_rule(:, +, ?, ?).   75
   76:- multifile user:file_search_path/2.   77
   78user:file_search_path(js,  library(scasp/web/js)).
   79user:file_search_path(css, library(scasp/web/css)).
   80
   81:- html_resource(scasp,
   82                 [ virtual(true),
   83                   requires([ jquery,
   84                              js('scasp.js'),
   85                              css('scasp.css')
   86                            ]),
   87                   ordered(true)
   88                 ]).

 html_justification_tree(:Tree, +Options)// is det

Convert the tree to HTML. The caller should use ovar_analyze_term/1 on Tree to name variables and identify singletons. This is not done in this predicate as the user may or may not wish to combine the variable analysis with the bindings and/or model. Options processed:

pred(Boolean)

When false (default true), ignore user pred/1 rules.

justify_nmr(Boolean)

When false (default true), do not omit a justification for the global constraints.

show(Format)

One of human, machine or both.

source(Boolean)

When false (default true), do not omit source locations.

  110:- det(html_justification_tree//2).  111
  112html_justification_tree(M:Tree, Options) -->
  113    emit(div(class('scasp-justification'),
  114             ul(class('scasp-justification'),
  115                \justification_tree(Tree,
  116                                    [ depth(0),
  117                                      module(M)
  118                                    | Options
  119                                    ])))).

 justification_tree(+Tree, +Options)//

Emit HTML for Tree. Tree is of the format as returned by justification_tree/3, a term of the shape Atom-ListOfChildren. The first clause deals with mapping subtrees to human descriptions. The remainder deals with special cases where there are no global constraints. normal_justification_tree/2 deals with the general case.

  130justification_tree(Tree, Options) -->
  131    { \+ option(show(machine), Options),        % human or both
  132      option(pred(true), Options, true),
  133      option(module(M), Options),
  134      human_expression(M:Tree, Children, Actions)
  135    },
  136    !,
  137    (   {Children == [], Actions == html([])}
  138    ->  []
  139    ;   {Children == []}
  140    ->  emit(li([ div(class(node),
  141                      [ \human_atom(Tree, Actions, Options),
  142                        \connect(Options)
  143                      ])
  144                ]))
  145    ;   { incr_indent(Options, Options1),
  146          (   Tree == o_nmr_check
  147          ->  ExtraClasses = ['scasp-global-constraints']
  148          ;   ExtraClasses = []
  149          )
  150        },
  151        emit(li( class([collapsable|ExtraClasses]),
  152             [ div(class([node, 'collapsable-header']),
  153                   [ \human_atom(Tree, Actions, Options),
  154                     \connector(implies, Options)
  155                   ]),
  156               ul(class('collapsable-content'),
  157                  \justification_tree_children(Children, Options1))
  158            ]))
  159    ).
  160justification_tree(query-[Query,o_nmr_check-[]], Options) -->
  161    !,
  162    justification_tree(Query, Options),
  163    full_stop(Options).
  164justification_tree(query-Children, Options) -->
  165    !,
  166    justification_tree_children(Children, Options),
  167    full_stop(Options).
  168justification_tree(o_nmr_check-[], _Options) -->
  169    !.
  170justification_tree(Tree, Options) -->
  171    normal_justification_tree(Tree, Options).
  172
  173normal_justification_tree(goal_origin(Term, Origin)-[], Options) -->
  174    !,
  175    { scasp_source_reference_file_line(Origin, File, Line) },
  176    emit(li([ div(class(node),
  177                  [ \tree_atom(Term, Options),
  178                    \origin(File, Line, Options),
  179                    \connect(Options)
  180                  ])
  181            ])).
  182normal_justification_tree(Term-[], Options) -->
  183    !,
  184    emit(li([ div(class(node),
  185                  [ \tree_atom(Term, Options),
  186                    \connect(Options)
  187                  ])
  188            ])).
  189normal_justification_tree(o_nmr_check-_, Options) -->
  190    { option(justify_nmr(false), Options) },
  191    !.
  192normal_justification_tree(goal_origin(Term, Origin)-Children, Options) -->
  193    { incr_indent(Options, Options1),
  194      (   Term == o_nmr_check
  195      ->  ExtraClasses = ['scasp-global-constraints']
  196      ;   ExtraClasses = []
  197      ),
  198      scasp_source_reference_file_line(Origin, File, Line)
  199    },
  200    !,
  201    emit(li(class([collapsable|ExtraClasses]),
  202            [ div(class([node, 'collapsable-header']),
  203                  [ \tree_atom(Term, Options),
  204                    \connector(implies, [origin(File:Line)|Options]),
  205                    \origin(File, Line, Options)
  206                  ]),
  207              ul(class('collapsable-content'),
  208                 \justification_tree_children(Children, Options1))
  209            ])).
  210normal_justification_tree(Term-Children, Options) -->
  211    { incr_indent(Options, Options1),
  212      (   Term == o_nmr_check
  213      ->  ExtraClasses = ['scasp-global-constraints']
  214      ;   ExtraClasses = []
  215      )
  216    },
  217    emit(li(class([collapsable|ExtraClasses]),
  218            [ div(class([node, 'collapsable-header']),
  219                  [ \tree_atom(Term, Options),
  220                    \connector(implies, Options)
  221                  ]),
  222              ul(class('collapsable-content'),
  223                 \justification_tree_children(Children, Options1))
  224            ])).
  225
  226justification_tree_children([A,B|Rs], Options) -->
  227    !,
  228    justification_tree(A, [connect(and)|Options]),
  229    justification_tree_children([B|Rs], Options).
  230justification_tree_children([A], Options) -->
  231    justification_tree(A, Options).
  232
  233connect(Options) -->
  234    { option(connect(Connector), Options) },
  235    !,
  236    connector(Connector, Options).
  237connect(_) -->
  238    [].

 human_atom(+Tree, +Human, +Options)// is det

Emits an atom handled by a pred/1 rule. Human is a sequence of actions as produced by human_expression/3.

  245human_atom(_, Actions, Options) -->
  246    { option(show(human), Options),
  247      empty_actions(Actions)
  248    },
  249    !.
  250human_atom(_Atom-_Children, Actions, Options) -->
  251    { option(show(human), Options),
  252      !,
  253      css_classes(Options, Classes)
  254    },
  255    emit(span(class(['scasp-atom'|Classes]),
  256              \actions(Actions, Options))).
  257human_atom(Atom-_Children, _Actions, Options) -->
  258    { option(show(machine), Options),
  259      !
  260    },
  261    emit(span(class('scasp-atom'), \machine_atom(Atom, Options))).
  262human_atom(Atom-_Children, Actions, Options) -->
  263    { css_classes(Options, Classes),
  264      scasp_atom_string(Atom, String)
  265    },
  266    emit(span(class('scasp-atom'),
  267              [ span([class(human), title(String)],
  268                     span(class(Classes), \actions(Actions, Options))),
  269                span(class(machine), \machine_atom(Atom, Options))
  270              ])).
  271
  272empty_actions('').
  273empty_actions([]).
  274
  275
  276tree_atom(Atom, Options) -->
  277    { option(show(machine), Options) },
  278    !,
  279    emit(span(class('scasp-atom'), \machine_atom(Atom, Options))).
  280tree_atom(Atom, Options) -->
  281    { option(show(human), Options),
  282      !
  283    },
  284    emit(span(class('scasp-atom'), \atom(Atom, Options))).
  285tree_atom(Atom, Options) -->
  286    { scasp_atom_string(Atom, String)
  287    },
  288    emit(span(class(['scasp-atom']),
  289              [ span([class(human), title(String)], \atom(Atom, Options)),
  290                span(class(machine), \machine_atom(Atom, Options))
  291              ])).
  292
  293scasp_atom_string(goal_origin(Atom, _Origin), String) =>
  294    scasp_atom_string(Atom, String).
  295scasp_atom_string(Atom, String) =>
  296    with_output_to(string(String),
  297                   print_model_term_v(Atom, [])).
  298
  299print_model_term_v(Atom, Options) :-
  300    \+ \+ ( inline_constraints(Atom, Options),
  301            print_model_term(Atom, Options)
  302          ).

 html_model(:Model, +Options)// is det

Emit the model as HTML terms. We export the model as a dict with nested model terms.

  310html_model(M:Model, Options) -->
  311    { (   option(class(Class), Options)
  312      ->  Classes = [Class]
  313      ;   Classes = []
  314      ),
  315      Options1 = [module(M)|Options]
  316    },
  317    emit(ul(class(['scasp-model'|Classes]),
  318            \sequence(model_item_r(Options1), Model))).
  319
  320model_item_r(Options, Atom) -->
  321    emit(li(class('scasp-atom'),
  322                  \model_term(Atom, Options))).

 html_model_term(:Atom, +Options)// is det

Emit a model term.

  328html_model_term(M:Atom, Options) -->
  329    model_term(Atom, [module(M)|Options]).
  330
  331model_term(Atom, Options) -->
  332    { option(show(human), Options),
  333      !
  334    },
  335    atom(Atom, Options).
  336model_term(Atom, Options) -->
  337    { option(show(machine), Options),
  338      !
  339    },
  340    machine_atom(Atom, Options).
  341model_term(Atom, Options) -->
  342    { scasp_atom_string(Atom, String)
  343    },
  344    emit([ span([class(human), title(String)], \atom(Atom, Options)),
  345           span(class(machine), \machine_atom(Atom, Options))
  346         ]).

 html_bindings(+Bindings, +Options)//

Print the variable bindings.

  353html_bindings([], _Options) -->
  354    [].
  355html_bindings([H|T], Options) -->
  356    (   {T==[]}
  357    ->  html_binding(H, [last(true)|Options])
  358    ;   html_binding(H, Options),
  359        html_bindings(T, Options)
  360    ).
  361
  362html_binding(Name=Value, Options) -->
  363    emit(div(class('scasp-binding'),
  364             [ var(Name),
  365               ' = ',
  366               \html_term(Value, Options),
  367               \connect_binding(Options)
  368             ])).
  369
  370connect_binding(Options) -->
  371    { option(last(true), Options) },
  372    !.
  373connect_binding(_Options) -->
  374    emit(',').

 html_program(:Dict)

  380html_program(Dict) :-
  381    phrase(html_program(Dict), Tokens),
  382    print_html(current_output, Tokens).

 html_program(:Dict)//

Emit the current program in human format using HTML.

  388html_program(M:Dict) -->
  389    { Dict1 = Dict.put(module, M)
  390    },
  391    html_program_section(query,       Dict1),
  392    html_program_section(user,        Dict1),
  393    html_program_section(duals,       Dict1),
  394    html_program_section(constraints, Dict1),
  395    html_program_section(dcc,         Dict1).
  396
  397html_program_section(Section, Dict) -->
  398    { _{module:M, options:Options} :< Dict,
  399      Content = Dict.get(Section),
  400      Content \= [],
  401      scasp_code_section_title(Section, Default, Title),
  402      Opt =.. [Section,true],
  403      option(Opt, Options, Default)
  404    },
  405    !,
  406    html(h2(Title)),
  407    (   {Section == query}
  408    ->  {ovar_set_bindings(Dict.bindings)},
  409        html_query(M:Content, Options)
  410    ;   sequence(predicate_r(M:Options), Content)
  411    ).
  412html_program_section(_, _) -->
  413    [].
  414
  415predicate_r(M:Options, Clauses) -->
  416    html_predicate(M:Clauses, Options).

 html_query(:Query, +Options)//

Emit the query. This rule accepts the query both in s(CASP) and normal Prolog notation.

  424:- det(html_query//2).  425
  426html_query(M:Query, Options) -->
  427    { (   is_list(Query)
  428      ->  prolog_query(Query, Prolog)
  429      ;   Prolog = Query
  430      ),
  431      !,
  432      comma_list(Prolog, List0),
  433      clean_query(List0, List)
  434    },
  435    (   { option(show(human), Options) }
  436    ->  emit(div(class('scasp-query'),
  437                 [ div(class('scasp-query-title'), 'I would like to know if'),
  438                   \query_terms(List, [module(M)|Options])
  439                 ]))
  440    ;   { option(show(machine), Options) }
  441    ->  emit(div(class('scasp-query'),
  442                 [ span(class('scasp-query-title'), '?- '),
  443                   \term(Prolog, [numbervars(true)|Options])
  444                 ]))
  445    ;   emit(div(class('scasp-query'),
  446                  [ div(class(human),
  447                        [ div(class('scasp-query-title'),
  448                              'I would like to know if'),
  449                          \query_terms(List, [module(M)|Options])
  450                        ]),
  451                    div(class(machine),
  452                        [ '?- ', \term(Prolog, [numbervars(true)|Options])
  453                        ])
  454                  ]))
  455    ).
  456html_query(_, _) -->
  457    emit(div(class(comment), '% No query')).
  458
  459prolog_query([not(o_false)], _) =>
  460    fail.
  461prolog_query(List, Query), is_list(List) =>
  462    clean_query(List, List1),
  463    (   List1 == []
  464    ->  Query = true
  465    ;   comma_list(Query, List1)
  466    ).
  467
  468clean_query(Q0, Q) :-
  469    delete(Q0, o_nmr_check, Q1),
  470    delete(Q1, true, Q).
  471
  472query_terms([], Options) -->
  473    query_term(true, Options).
  474query_terms([H1,H2|T], Options) -->
  475    !,
  476    query_term(H1, [connect(and)|Options]),
  477    query_terms([H2|T], Options).
  478query_terms([Last], Options) -->
  479    { option(end(End), Options, ?)
  480    },
  481    query_term(Last, [connect(End)|Options]).
  482
  483query_term(Term, Options) -->
  484    emit(div(class('scasp-query-literal'),
  485             [ \atom(Term, Options),
  486               \connect(Options)
  487             ])).

 html_predicate(:Rules, Options)//

  491html_predicate(M:Clauses, Options) -->
  492    emit(div(class('scasp-predicate'),
  493             \sequence(html_rule_r(M, Options), Clauses))).
  494
  495html_rule_r(M, Options, Clause) -->
  496    html_rule(M:Clause, Options).

 html_rule(:Rule, +Options)//

  500html_rule(Rule, Options) -->
  501    { ovar_analyze_term(Rule) },
  502    html_rule_(Rule, Options),
  503    { ovar_clean(Rule) }.
  504
  505html_rule_(M:(Head0 :- Body), Options) -->
  506    !,
  507    { MOptions = [module(M)|Options],
  508      raise_negation(Head0, Head)
  509    },
  510    emit(div(class('scasp-rule'),
  511             [ div(class('scasp-head'),
  512                   [ \atom(Head, MOptions),
  513                     ', if'
  514                   ]),
  515               div(class('scasp-body'),
  516                   \html_body(Body, [end(.)|MOptions]))
  517             ])).
  518html_rule_(M:Head, Options) -->
  519    emit(div(class('scasp-rule'),
  520             div(class('scasp-head'),
  521                 [ \atom(Head, [module(M)|Options]),
  522                   \connector('.', Options)
  523                 ]))).
  524
  525html_body(forall(X, not(Goal)), Options) -->
  526    !,
  527    emit(div(class('scasp-query-literal'),
  528             [ 'there exist no ', \html_term(X, Options),
  529               ' for which ', \atom(Goal, Options)
  530             ])).
  531html_body(Body, Options) -->
  532    { comma_list(Body, List0),
  533      maplist(raise_negation, List0, List)
  534    },
  535    query_terms(List, Options).

 atom(+SCASPAtom, +Options)//

Emit an s(CASP) atom with annotations as they appear in the model and justification.

  544atom(Atom, Options) -->
  545    { option(pred(true), Options, true),
  546      option(module(DefM), Options),
  547      option(source_module(M), Options, DefM),
  548      human_expression(M:(Atom-[]), [], Actions),
  549      !,
  550      css_classes(Options, Classes)
  551    },
  552    emit(span(class(Classes), \actions(Actions, Options))).
  553atom(not(GlobalConstraint), Options) -->
  554    { is_global_constraint(GlobalConstraint, N)
  555    },
  556    !,
  557    utter(global_constraint(N), Options).
  558atom(not(Term), Options) -->
  559    !,
  560    utter(not(Term), [class(not)|Options]).
  561atom(-Term, Options) -->
  562    !,
  563    utter(-(Term), [class(neg)|Options]).
  564atom(proved(Term), Options) -->
  565    !,
  566    utter(proved(Term), [class(proved)|Options]).
  567atom(assume(Term), Options) -->
  568    !,
  569    utter(assume(Term), [class(assume)|Options]).
  570atom(chs(Term), Options) -->
  571    !,
  572    utter(chs(Term), [class(chs)|Options]).
  573atom(abduced(Term), Options) -->
  574    !,
  575    utter(abduced(Term), [class(abducible)|Options]).
  576atom(M:Term, Options) -->
  577    { atom(M) },
  578    !,
  579    atom(Term, [module(M)|Options]).
  580atom(o_nmr_check, Options) -->
  581    !,
  582    utter(global_constraints_hold, Options).
  583atom(is(Value,Expr), Options) -->
  584    !,
  585    { css_classes(Options, Classes)
  586    },
  587    emit(span(class([arithmetic|Classes]),
  588              [ \expr(Expr, Options), &(nbsp), is, &(nbsp), \html_term(Value, Options)
  589              ])).
  590atom(Comp, Options) -->
  591    { human_connector(Comp, Text),
  592      !,
  593      Comp =.. [_,Left,Right],
  594      css_classes(Options, Classes)
  595    },
  596    emit(span(class([arithmetic|Classes]),
  597              [ \html_term(Left, Options),
  598                &(nbsp), Text, &(nbsp),
  599                \html_term(Right, Options)
  600              ])).
  601atom(Term, Options) -->
  602    utter(holds(Term), Options).

 expr(+Term, +Options)// is det

Render an expression.

To be done

- Should deal with parenthesis where needed. Possibly it is a better option to use term//2 from library(http/html_term) and add a portray hook for that?

  612expr(Term, Options) -->
  613    { compound(Term),
  614      compound_name_arguments(Term, Op, [Left, Right])
  615    },
  616    !,
  617    emit(span([ \expr(Left, Options),
  618                &(nbsp), Op, &(nbsp),
  619                \expr(Right, Options)
  620              ])).
  621expr(Term, Options) -->
  622    { compound(Term),
  623      compound_name_arguments(Term, Op, [Arg])
  624    },
  625    !,
  626    emit(span([ Op,
  627                \expr(Arg, Options)
  628              ])).
  629expr(Simple, Options) -->
  630    html_term(Simple, Options).

 utter(+Expression, +Options)

  634utter(global_constraints_hold, _Options) -->
  635    { human_connector(global_constraints_hold, Text) },
  636    emit(Text).
  637utter(global_constraint(N), _Options) -->
  638    { human_connector(global_constraint(N), Text) },
  639    emit(Text).
  640utter(not(-(Atom)), Options) -->
  641    !,
  642    { human_connector(may, Text) },
  643    emit([Text, ' ']),
  644    atom(Atom, Options).
  645utter(not(Atom), Options) -->
  646    { human_connector(not, Text) },
  647    emit([Text, ' ']),
  648    atom(Atom, Options).
  649utter(-(Atom), Options) -->
  650    { human_connector(-, Text) },
  651    emit([Text, ' ']),
  652    atom(Atom, Options).
  653utter(proved(Atom), Options) -->
  654    { human_connector(proved, Text) },
  655    atom(Atom, Options),
  656    emit([', ', Text]).
  657utter(chs(Atom), Options) -->
  658    { human_connector(chs, Text) },
  659    emit([Text, ' ']),
  660    atom(Atom, Options).
  661utter(abduced(Atom), Options) -->
  662    { human_connector(abducible, Text) },
  663    emit([Text, ' ']),
  664    atom(Atom, Options).
  665utter(according_to(File, Line), _Options) -->
  666    { human_connector(according_to, Text) },
  667    emit(span(class('scasp-source-reference'),
  668              span(class(human), [' [', Text, ' ~w:~w]'-[File, Line]]))).
  669utter(assume(Atom), Options) -->
  670    { human_connector(assume, Text) },
  671    emit([Text, ' ']),
  672    atom(Atom, Options).
  673utter(holds(Atom), Options) -->
  674    { css_classes(Options, Classes) },
  675    (   { atom(Atom) }
  676    ->  { human_connector(holds, Text) },
  677        emit([span(class(Classes), Atom), Text])
  678    ;   { Atom =.. [Name|Args] }
  679    ->  { human_connector(holds_for, Text) },
  680        emit([span(class(Classes), Name), Text]),
  681        list(Args, Options)
  682    ).
  683
  684css_classes(Options, [atom|Classes]) :-
  685    findall(Class, member(class(Class), Options), Classes0),
  686    (   Classes0 == []
  687    ->  Classes = [pos]
  688    ;   Classes = Classes0
  689    ).
  690
  691
  692:- det(html_term//2).  693
  694html_term(Var, Options) -->
  695    { var(Var) },
  696    !,
  697    var(Var, Options).
  698html_term(@(Var:''), Options) -->
  699    { var(Var)
  700    },
  701    !,
  702    var(Var, Options).
  703html_term(@(Var:Type), Options) -->
  704    { var(Var)
  705    },
  706    !,
  707    typed_var(Var, Type, Options).
  708html_term(@(Value:''), Options) -->
  709    !,
  710    html_term(Value, Options).
  711html_term(@(Value:Type), Options) -->
  712    emit('the ~w '-[Type]),
  713    !,
  714    html_term(Value, Options).
  715html_term(Term, _Options) -->
  716    { var_number(Term, _) },
  717    !,
  718    emit('~p'-[Term]).
  719html_term('| '(Var, {Constraints}), Options) -->
  720    !,
  721    inlined_var(Var, Constraints, Options).
  722html_term(Term, _Options) -->
  723    { emitting_as(plain) },
  724    !,
  725    [ ansi(code, '~p', [Term]) ].
  726html_term(Term, Options) -->
  727    term(Term, [numbervars(true)|Options]).

 var(+Var, +Options)//

Handle a variable, optionally with constraints and annotated using ovar_analyze_term/2.

  734var(Var, Options) -->
  735    { copy_term(Var, Copy),
  736      inline_constraints(Copy, Options),
  737      nonvar(Copy),
  738      Copy = '| '(V, {Constraints})
  739    },
  740    !,
  741    inlined_var(V, Constraints, Options).
  742var(Var, _Options) -->
  743    { ovar_var_name(Var, Name)
  744    },
  745    !,
  746    emit(var(Name)).
  747var(_, _) -->
  748    emit(anything).

 inlined_var(+Var, +Constraint, +Options)//

Deal with constraints as represented after inline_constraints/2.

  754inlined_var(Var, Constraints, Options) -->
  755    { Constraints = '\u2209'(Var, List),
  756      Var == '$VAR'('_')
  757    },
  758    !,
  759    (   {List = [One]}
  760    ->  emit('anything except for '),
  761        html_term(One, Options)
  762    ;   emit('anything except for '),
  763        list(List, [last_connector(or)|Options])
  764    ).
  765inlined_var(Var, Constraints, Options) -->
  766    { Constraints = '\u2209'(Var, List),
  767      compound(Var),
  768      Var = '$VAR'(Name)
  769    },
  770    !,
  771    (   {List = [One]}
  772    ->  {human_connector(neq, Text)},
  773        emit([var(Name), ' ', Text, ' ']),
  774        html_term(One, Options)
  775    ;   {human_connector(not_in, Text)},
  776        emit([var(Name), ' ', Text, ' ']),
  777        list(List, [last_connector(or)|Options])
  778    ).
  779inlined_var(Var, Constraints, Options) -->
  780    { comma_list(Constraints, CLPQ)
  781    },
  782    clpq(Var, CLPQ, Options).

 clpq(@Var, +Constraints, +Options)//

  786clpq(Var, [Constraint|More], Options) -->
  787    { compound(Constraint),
  788      Constraint =.. [_,A,B],
  789      Var == A,
  790      human_connector(Constraint, Text),
  791      (   nonvar(Var),
  792          Var = '$VAR'(Name)
  793      ->  Id = var(Name)
  794      ;   Id = number
  795      )
  796    },
  797    emit(['any ', Id, ' ', Text, ' ']),
  798    html_term(B, Options),
  799    (   {More == []}
  800    ->  []
  801    ;   emit(' and '),
  802        clpq_and(More, Var, Options)
  803    ).
  804
  805clpq_and([Constraint|More], Var, Options) -->
  806    { compound(Constraint),
  807      Constraint =.. [_,A,B],
  808      A == Var,
  809      human_connector(Constraint, Text)
  810    },
  811    emit([Text, ' ']),
  812    html_term(B, Options),
  813    (   {More == []}
  814    ->  []
  815    ;   emit(' and '),
  816        clpq_and(More, Var, Options)
  817    ).

 typed_var(@Var, +Type, +Options)//

  821typed_var(Var, Type, Options) -->
  822    { copy_term(Var, Copy),
  823      inline_constraints(Copy, Options),
  824      nonvar(Copy),
  825      Copy = '| '(V, {Constraints})
  826    },
  827    !,
  828    inlined_typed_var(V, Type, Constraints, Options).
  829typed_var(Var, Type, _Options) -->
  830    { ovar_var_name(Var, Name)
  831    },
  832    !,
  833    emit([var(Name), ', a ', Type]).
  834typed_var(_Var, Type, _Options) -->
  835    emit(['a ', Type]).
  836
  837
  838inlined_typed_var(Var, Type, Constraints, Options) -->
  839    { Constraints = '\u2209'(Var, List),
  840      Var == '$VAR'('_')
  841    },
  842    !,
  843    (   {List = [One]}
  844    ->  emit(['any ', Type, ' except for ']),
  845        html_term(One, Options)
  846    ;   emit(['any ', Type, ' except for ']),
  847        list(List, [last_connector(or)|Options])
  848    ).
  849inlined_typed_var(Var, Type, Constraints, Options) -->
  850    { Constraints = '\u2209'(Var, List),
  851      nonvar(Var),
  852      Var = '$VAR'(Name)
  853    },
  854    !,
  855    (   {List = [One]}
  856    ->  emit([var(Name), ', a ', Type, ' other than ']),
  857        html_term(One, Options)
  858    ;   emit([var(Name), ', a ', Type, ' not ']),
  859        list(List, [last_connector(or)|Options])
  860    ).
  861inlined_typed_var(Var, Type, Constraints, Options) --> % TBD: include type in NLP
  862    { comma_list(Constraints, CLPQ)
  863    },
  864    clpq(Var, CLPQ, [type(Type)|Options]).

 list(+Elements, +Options) is det

Emit a collection as "a, b, and c"

  870list([L1,L], Options) -->
  871    !,
  872    { option(last_connector(Conn), Options, and),
  873      human_connector(Conn, Text)
  874    },
  875    html_term(L1, Options),
  876    emit(', ~w '-[Text]),
  877    html_term(L, Options).
  878list([H|T], Options) -->
  879    html_term(H, Options),
  880    (   {T==[]}
  881    ->  []
  882    ;   emit(', '),
  883        list(T, Options)
  884    ).
  885
  886actions(html(HTML), _) -->
  887    !,
  888    emit(HTML).
  889actions([], _) --> [].
  890actions([H|T], Options) -->
  891    action(H, Options),
  892    actions(T, Options).
  893
  894action(text(S), _) -->
  895    !,
  896    emit(S).
  897action(Term, Options) -->
  898    html_term(Term, Options).

 connector(+Meaning, +Options)//

Emit a logical connector.

  904connector(Meaning, Options) -->
  905    { option(show(human), Options),
  906      !,
  907      human_connector(Meaning, Text)
  908    },
  909    emit_human_connector(Meaning, Text, Options).
  910connector(Meaning, Options) -->
  911    { option(show(machine), Options)
  912    },
  913    !,
  914    emit_machine_connector(Meaning, Options).
  915connector(Meaning, Options) -->
  916    { human_connector(Meaning, Text)
  917    },
  918    emit([ span(class(human),   \emit_human_connector(Meaning, Text, Options)),
  919           span(class(machine), \emit_machine_connector(Meaning, Options))
  920         ]).
  921
  922emit_human_connector(and, Text, _) --> emit([', ', Text]).
  923emit_human_connector(not, Text, _) --> emit([Text, ' ']).
  924emit_human_connector(-,   Text, _) --> emit([Text, ' ']).
  925emit_human_connector(?,   Text, _) --> emit(Text).
  926emit_human_connector(.,   Text, _) --> emit(Text).
  927emit_human_connector(implies, Text, Options) -->
  928    emit([', ', \origin_annotated(Text, Options)]).
  929
  930emit_machine_connector(and, _) --> emit(',').
  931emit_machine_connector(not, _) --> emit('not ').
  932emit_machine_connector(-,   _) --> emit('\u00ac ').
  933emit_machine_connector(?,   _) --> emit(?).
  934emit_machine_connector(.,   _) --> emit(.).
  935emit_machine_connector(implies, Options) -->
  936    origin_annotated(' \u2190', Options).
  937
  938human_connector(Term, Connector) :-
  939    phrase(scasp_justification_message(Term), List),
  940    (   List = [Connector]
  941    ->  true
  942    ;   Connector = List
  943    ).
  944
  945full_stop(Options) -->
  946    { option(show(human), Options) },
  947    !.
  948full_stop(_Options) -->
  949    emit(span([class(machine), title('QED')], '\u220e')).
  950
  951incr_indent(Options0, [depth(D)|Options2]) :-
  952    select_option(depth(D0), Options0, Options1),
  953    select_option(connect(_), Options1, Options2, _),
  954    D is D0+1.
  955
  956		 /*******************************
  957		 *         MACHINE HTML		*
  958		 *******************************/

 machine_atom(+SCASPAtom, +Options)//

Emit an s(CASP) atom with annotations as they appear in the model and justification.

  965machine_atom(goal_origin(Term, _Origin), Options) -->
  966    !,
  967    machine_atom(Term, Options).
  968machine_atom(not(Term), Options) -->
  969    !,
  970    emit([span(class([connector,not]), not), ' ']),
  971    machine_atom(Term, [class(not)|Options]).
  972machine_atom(-Term, Options) -->
  973    !,
  974    emit([span(class([connector,neg]), '\u00ac'), ' ']),
  975    machine_atom(Term, [class(neg)|Options]).
  976machine_atom(proved(Term), Options) -->
  977    !,
  978    emit([ span(class([connector,proved]), proved), '(',
  979           \machine_atom(Term, [class(proved)|Options]),
  980           ')'
  981         ]).
  982machine_atom(assume(Term), Options) -->
  983    !,
  984    emit([ span(class([connector,assume]), assume), '(',
  985           \machine_atom(Term, [class(assume)|Options]),
  986           ')'
  987         ]).
  988machine_atom(chs(Term), Options) -->
  989    !,
  990    emit([ span(class([connector,chs]), chs), '(',
  991           \machine_atom(Term, [class(chs)|Options]),
  992           ')'
  993         ]).
  994machine_atom(M:Term, Options) -->
  995    { atom(M) },
  996    !,
  997    emit(span(class(module), [M,:])),
  998    machine_atom(Term, [module(M)|Options]).
  999machine_atom(Term, Options) -->
 1000    { css_classes(Options, Classes),
 1001      merge_options(Options, [numbervars(true)], WOptions)
 1002    },
 1003    emit(span(class(Classes), \term(Term, WOptions))).
 1004
 1005:- multifile
 1006    term_html:portray//2. 1007
 1008term_html:portray(Term, Options) -->
 1009    { nonvar(Term),
 1010      Term = '| '(Var, Constraints)
 1011    },
 1012    term(Var, Options),
 1013    emit(' | '),
 1014    term(Constraints, Options).
 1015
 1016origin(File, Line, Options) -->
 1017    {    option(source(true), Options)   },
 1018    !,
 1019    utter(according_to(File, Line), Options).
 1020origin(_, _, _) --> [].
 1021
 1022origin_annotated(Content, Options) -->
 1023    { option(origin(File:Line), Options)
 1024    },
 1025    !,
 1026    emit(span([ class(scasp_origin),
 1027                'data-file'(File),
 1028                'data-line'(Line)
 1029              ], Content)).
 1030origin_annotated(Content, _) -->
 1031    emit(Content)