1:- module(scasp_just_html,
    2          [ html_justification_tree//2,		% :Tree, +Options
    3            html_model//2,			% :Model, +Options
    4            html_bindings//2,                   % :Bindings, +Options
    5            html_program/1,                     % :Dict
    6            html_program//1,                    % :Dict
    7            html_query//2,                      % :Query, +Options
    8            html_predicate//2,                  % :Predicate, +Options
    9            html_rule//2,                       % :Rule, +Options
   10            html_term//2                        % +Term, +Options
   11          ]).   12:- use_module(common).   13:- use_module(output).   14:- use_module(html_text).   15:- use_module(messages).   16:- use_module(source_ref).   17:- use_module(listing).   18
   19:- use_module(library(http/html_write)).   20:- use_module(library(http/term_html)).   21:- use_module(library(http/html_head), [html_resource/2]).   22:- if(exists_source(library(http/http_server_files))).   23:- use_module(library(http/http_server_files), []).   24:- endif.   25:- use_module(library(dcg/high_order)).   26:- use_module(library(lists)).   27:- use_module(library(option)).   28:- use_module(library(prolog_code)).   29:- use_module(library(apply)).   30
   31:- meta_predicate
   32    html_model(:, +, ?, ?),
   33    html_justification_tree(:, +, ?, ?),
   34    html_program(:),
   35    html_program(:, ?, ?),
   36    html_query(:, +, ?, ?),
   37    html_predicate(:, +, ?, ?),
   38    html_rule(:, +, ?, ?).   39
   40:- multifile user:file_search_path/2.   41
   42user:file_search_path(js,  library(scasp/web/js)).
   43user:file_search_path(css, library(scasp/web/css)).
   44
   45:- html_resource(scasp,
   46                 [ virtual(true),
   47                   requires([ jquery,
   48                              js('scasp.js'),
   49                              css('scasp.css')
   50                            ]),
   51                   ordered(true)
   52                 ]).   53
   54/** <module> Render s(CASP) justification as HTML
   55*/
   56
   57%!  html_justification_tree(:Tree, +Options)// is det.
   58%
   59%   Convert the tree to HTML. The  caller should use ovar_analyze_term/1
   60%   on Tree to name variables and identify  singletons. This is not done
   61%   in this predicate as the user may or  may not wish to combine the
   62%   variable analysis with the bindings and/or model. Options processed:
   63%
   64%     - pred(Boolean)
   65%       When `false` (default `true`), ignore user pred/1 rules.
   66%     - justify_nmr(Boolean)
   67%       When `false` (default `true`), do not omit a justification for
   68%       the global constraints.
   69%     - source(Boolean)
   70%       When `false` (default `true`), do not omit source locations.
   71
   72:- det(html_justification_tree//2).   73
   74html_justification_tree(M:Tree, Options) -->
   75    emit(div(class('scasp-justification'),
   76             ul(class('scasp-justification'),
   77                \justification_tree(Tree,
   78                                    [ depth(0),
   79                                      module(M)
   80                                    | Options
   81                                    ])))).
   82
   83%!  justification_tree(+Tree, +Options)//
   84%
   85%   Emit  HTML  for  Tree.  Tree  is  of   the  format  as  returned  by
   86%   justification_tree/3, a term of the   shape Atom-ListOfChildren. The
   87%   first clause deals with mapping subtrees  to human descriptions. The
   88%   remainder deals with  special  cases  where   there  are  no  global
   89%   constraints.  normal_justification_tree/2  deals  with  the  general
   90%   case.
   91
   92justification_tree(Tree, Options) -->
   93    { \+ option(show(machine), Options),
   94      option(pred(true), Options, true),
   95      option(module(M), Options),
   96      human_expression(M:Tree, Children, Actions)
   97    },
   98    !,
   99    (   {Children == []}
  100    ->  emit(li([ div(class(node),
  101                      [ \human_atom(Tree, Actions, Options),
  102                        \connect(Options)
  103                      ])
  104                ]))
  105    ;   { incr_indent(Options, Options1),
  106          (   Tree == o_nmr_check
  107          ->  ExtraClasses = ['scasp-global-constraints']
  108          ;   ExtraClasses = []
  109          )
  110        },
  111        emit(li( class([collapsable|ExtraClasses]),
  112             [ div(class([node, 'collapsable-header']),
  113                   [ \human_atom(Tree, Actions, Options),
  114                     \connector(implies, Options)
  115                   ]),
  116               ul(class('collapsable-content'),
  117                  \justification_tree_children(Children, Options1))
  118            ]))
  119    ).
  120justification_tree(query-[Query,o_nmr_check-[]], Options) -->
  121    !,
  122    justification_tree(Query, Options),
  123    full_stop(Options).
  124justification_tree(query-Children, Options) -->
  125    !,
  126    justification_tree_children(Children, Options),
  127    full_stop(Options).
  128justification_tree(o_nmr_check-[], _Options) -->
  129    !.
  130justification_tree(Tree, Options) -->
  131    normal_justification_tree(Tree, Options).
  132
  133normal_justification_tree(goal_origin(Term, Origin)-[], Options) -->
  134    !,
  135    { scasp_source_reference_file_line(Origin, File, Line) },
  136    emit(li([ div(class(node),
  137                  [ \tree_atom(Term, Options),
  138                    \origin(File, Line, Options),
  139                    \connect(Options)
  140                  ])
  141            ])).
  142normal_justification_tree(Term-[], Options) -->
  143    !,
  144    emit(li([ div(class(node),
  145                  [ \tree_atom(Term, Options),
  146                    \connect(Options)
  147                  ])
  148            ])).
  149normal_justification_tree(o_nmr_check-_, Options) -->
  150    { option(justify_nmr(false), Options) },
  151    !.
  152normal_justification_tree(goal_origin(Term, Origin)-Children, Options) -->
  153    { incr_indent(Options, Options1),
  154      (   Term == o_nmr_check
  155      ->  ExtraClasses = ['scasp-global-constraints']
  156      ;   ExtraClasses = []
  157      ),
  158      scasp_source_reference_file_line(Origin, File, Line)
  159    },
  160    !,
  161    emit(li(class([collapsable|ExtraClasses]),
  162            [ div(class([node, 'collapsable-header']),
  163                  [ \tree_atom(Term, Options),
  164                    \connector(implies, [origin(File:Line)|Options]),
  165                    \origin(File, Line, Options)
  166                  ]),
  167              ul(class('collapsable-content'),
  168                 \justification_tree_children(Children, Options1))
  169            ])).
  170normal_justification_tree(Term-Children, Options) -->
  171    { incr_indent(Options, Options1),
  172      (   Term == o_nmr_check
  173      ->  ExtraClasses = ['scasp-global-constraints']
  174      ;   ExtraClasses = []
  175      )
  176    },
  177    emit(li(class([collapsable|ExtraClasses]),
  178            [ div(class([node, 'collapsable-header']),
  179                  [ \tree_atom(Term, Options),
  180                    \connector(implies, Options)
  181                  ]),
  182              ul(class('collapsable-content'),
  183                 \justification_tree_children(Children, Options1))
  184            ])).
  185
  186justification_tree_children([A,B|Rs], Options) -->
  187    !,
  188    justification_tree(A, [connect(and)|Options]),
  189    justification_tree_children([B|Rs], Options).
  190justification_tree_children([A], Options) -->
  191    justification_tree(A, Options).
  192
  193connect(Options) -->
  194    { option(connect(Connector), Options) },
  195    !,
  196    connector(Connector, Options).
  197connect(_) -->
  198    [].
  199
  200%!  human_atom(+Tree, +Human, +Options)// is det.
  201%
  202%   @tbd Deal with Human == '', deleting the node.
  203
  204human_atom(Atom-_Children, Actions, Options) -->
  205    { css_classes(Options, Classes),
  206      scasp_atom_string(Atom, String)
  207    },
  208    emit(span(class('scasp-atom'),
  209              [ span([class(human), title(String)],
  210                     span(class(Classes), \actions(Actions, Options))),
  211                span(class(machine), \machine_atom(Atom, Options))
  212              ])).
  213
  214tree_atom(Atom, Options) -->
  215    { option(show(machine), Options) },
  216    !,
  217    emit(span(class(['scasp-atom']),
  218              span(class(machine), \machine_atom(Atom, Options)))).
  219tree_atom(Atom, Options) -->
  220    { scasp_atom_string(Atom, String)
  221    },
  222    emit(span(class(['scasp-atom']),
  223              [ span([class(human), title(String)], \atom(Atom, Options)),
  224                span(class(machine), \machine_atom(Atom, Options))
  225              ])).
  226
  227scasp_atom_string(goal_origin(Atom, _Origin), String) =>
  228    scasp_atom_string(Atom, String).
  229scasp_atom_string(Atom, String) =>
  230    with_output_to(string(String),
  231                   print_model_term_v(Atom, [])).
  232
  233print_model_term_v(Atom, Options) :-
  234    \+ \+ ( inline_constraints(Atom, Options),
  235            print_model_term(Atom, Options)
  236          ).
  237
  238
  239%!  html_model(:Model, +Options)// is det.
  240%
  241%   Emit the model as HTML terms.   We export the model as a dict with
  242%   nested model terms.
  243
  244html_model(M:Model, Options) -->
  245    { (   option(class(Class), Options)
  246      ->  Classes = [Class]
  247      ;   Classes = []
  248      ),
  249      Options1 = [module(M)|Options]
  250    },
  251    emit(ul(class(['scasp-model'|Classes]),
  252            \sequence(model_term_r(Options1), Model))).
  253
  254model_term_r(Options, Atom) -->
  255    { scasp_atom_string(Atom, String)
  256    },
  257    emit(li(class(['scasp-atom']),
  258            [ span([class(human), title(String)], \atom(Atom, Options)),
  259              span(class(machine), \machine_atom(Atom, Options))
  260            ])).
  261
  262
  263%!  html_bindings(+Bindings, +Options)//
  264%
  265%   Print the variable bindings.
  266
  267html_bindings([], _Options) -->
  268    [].
  269html_bindings([H|T], Options) -->
  270    (   {T==[]}
  271    ->  html_binding(H, [last(true)|Options])
  272    ;   html_binding(H, Options),
  273        html_bindings(T, Options)
  274    ).
  275
  276html_binding(Name=Value, Options) -->
  277    emit(div(class('scasp-binding'),
  278             [ var(Name),
  279               ' = ',
  280               \html_term(Value, Options),
  281               \connect_binding(Options)
  282             ])).
  283
  284connect_binding(Options) -->
  285    { option(last(true), Options) },
  286    !.
  287connect_binding(_Options) -->
  288    emit(',').
  289
  290%!  html_program(:Dict)
  291%
  292%
  293
  294html_program(Dict) :-
  295    phrase(html_program(Dict), Tokens),
  296    print_html(current_output, Tokens).
  297
  298%!  html_program(:Dict)//
  299%
  300%   Emit the current program in human format using HTML.
  301
  302html_program(M:Dict) -->
  303    { Dict1 = Dict.put(module, M)
  304    },
  305    html_program_section(query,       Dict1),
  306    html_program_section(user,        Dict1),
  307    html_program_section(duals,       Dict1),
  308    html_program_section(constraints, Dict1),
  309    html_program_section(dcc,         Dict1).
  310
  311html_program_section(Section, Dict) -->
  312    { _{module:M, options:Options} :< Dict,
  313      Content = Dict.get(Section),
  314      Content \= [],
  315      scasp_code_section_title(Section, Default, Title),
  316      Opt =.. [Section,true],
  317      option(Opt, Options, Default)
  318    },
  319    !,
  320    html(h2(Title)),
  321    (   {Section == query}
  322    ->  {ovar_set_bindings(Dict.bindings)},
  323        html_query(M:Content, Options)
  324    ;   sequence(predicate_r(M:Options), Content)
  325    ).
  326html_program_section(_, _) -->
  327    [].
  328
  329predicate_r(M:Options, Clauses) -->
  330    html_predicate(M:Clauses, Options).
  331
  332
  333%!  html_query(:Query, +Options)//
  334%
  335%   Emit the query. This rule accepts  the   query  both  in s(CASP) and
  336%   normal Prolog notation.
  337
  338:- det(html_query//2).  339
  340html_query(M:Query, Options) -->
  341    { (   is_list(Query)
  342      ->  prolog_query(Query, Prolog)
  343      ;   Prolog = Query
  344      ),
  345      !,
  346      comma_list(Prolog, List0),
  347      clean_query(List0, List)
  348    },
  349    emit(div(class('scasp-query'),
  350             [ div(class(human),
  351                   [ div(class('scasp-query-title'),
  352                         'I would like to know if'),
  353                     \query_terms(List, [module(M)|Options])
  354                   ]),
  355               div(class(machine),
  356                   [ '?- ', \term(Prolog, [numbervars(true)|Options])
  357                   ])
  358             ])).
  359html_query(_, _) -->
  360    emit(div(class(comment), '% No query')).
  361
  362prolog_query([not(o_false)], _) =>
  363    fail.
  364prolog_query(List, Query), is_list(List) =>
  365    clean_query(List, List1),
  366    (   List1 == []
  367    ->  Query = true
  368    ;   comma_list(Query, List1)
  369    ).
  370
  371clean_query(Q0, Q) :-
  372    delete(Q0, o_nmr_check, Q1),
  373    delete(Q1, true, Q).
  374
  375query_terms([], Options) -->
  376    query_term(true, Options).
  377query_terms([H1,H2|T], Options) -->
  378    !,
  379    query_term(H1, [connect(and)|Options]),
  380    query_terms([H2|T], Options).
  381query_terms([Last], Options) -->
  382    { option(end(End), Options, ?)
  383    },
  384    query_term(Last, [connect(End)|Options]).
  385
  386query_term(Term, Options) -->
  387    emit(div(class('scasp-query-literal'),
  388             [ \atom(Term, Options),
  389               \connect(Options)
  390             ])).
  391
  392%!  html_predicate(:Rules, Options)//
  393
  394html_predicate(M:Clauses, Options) -->
  395    emit(div(class('scasp-predicate'),
  396             \sequence(html_rule_r(M, Options), Clauses))).
  397
  398html_rule_r(M, Options, Clause) -->
  399    html_rule(M:Clause, Options).
  400
  401%!  html_rule(:Rule, +Options)//
  402
  403html_rule(Rule, Options) -->
  404    { ovar_analyze_term(Rule) },
  405    html_rule_(Rule, Options),
  406    { ovar_clean(Rule) }.
  407
  408html_rule_(M:(Head0 :- Body), Options) -->
  409    !,
  410    { MOptions = [module(M)|Options],
  411      raise_negation(Head0, Head)
  412    },
  413    emit(div(class('scasp-rule'),
  414             [ div(class('scasp-head'),
  415                   [ \atom(Head, MOptions),
  416                     ', if'
  417                   ]),
  418               div(class('scasp-body'),
  419                   \html_body(Body, [end(.)|MOptions]))
  420             ])).
  421html_rule_(M:Head, Options) -->
  422    emit(div(class('scasp-rule'),
  423             div(class('scasp-head'),
  424                 [ \atom(Head, [module(M)|Options]),
  425                   \connector('.', Options)
  426                 ]))).
  427
  428html_body(forall(X, not(Goal)), Options) -->
  429    !,
  430    emit(div(class('scasp-query-literal'),
  431             [ 'there exist no ', \html_term(X, Options),
  432               ' for which ', \atom(Goal, Options)
  433             ])).
  434html_body(Body, Options) -->
  435    { comma_list(Body, List0),
  436      maplist(raise_negation, List0, List)
  437    },
  438    query_terms(List, Options).
  439
  440
  441
  442%!  atom(+SCASPAtom, +Options)//
  443%
  444%   Emit an s(CASP) atom with annotations as   they  appear in the model
  445%   and justification.
  446
  447atom(Atom, Options) -->
  448    { option(pred(true), Options, true),
  449      option(module(DefM), Options),
  450      option(source_module(M), Options, DefM),
  451      human_expression(M:(Atom-[]), [], Actions),
  452      !,
  453      css_classes(Options, Classes)
  454    },
  455    emit(span(class(Classes), \actions(Actions, Options))).
  456atom(not(GlobalConstraint), Options) -->
  457    { is_global_constraint(GlobalConstraint, N)
  458    },
  459    !,
  460    utter(global_constraint(N), Options).
  461atom(not(Term), Options) -->
  462    !,
  463    utter(not(Term), [class(not)|Options]).
  464atom(-Term, Options) -->
  465    !,
  466    utter(-(Term), [class(neg)|Options]).
  467atom(proved(Term), Options) -->
  468    !,
  469    utter(proved(Term), [class(proved)|Options]).
  470atom(assume(Term), Options) -->
  471    !,
  472    utter(assume(Term), [class(assume)|Options]).
  473atom(chs(Term), Options) -->
  474    !,
  475    utter(chs(Term), [class(chs)|Options]).
  476atom(abduced(Term), Options) -->
  477    !,
  478    utter(abduced(Term), [class(abducible)|Options]).
  479atom(M:Term, Options) -->
  480    { atom(M) },
  481    !,
  482    atom(Term, [module(M)|Options]).
  483atom(o_nmr_check, Options) -->
  484    !,
  485    utter(global_constraints_hold, Options).
  486atom(is(Value,Expr), Options) -->
  487    !,
  488    { css_classes(Options, Classes)
  489    },
  490    emit(span(class([arithmetic|Classes]),
  491              [ \expr(Expr, Options), &(nbsp), is, &(nbsp), \html_term(Value, Options)
  492              ])).
  493atom(Comp, Options) -->
  494    { human_connector(Comp, Text),
  495      !,
  496      Comp =.. [_,Left,Right],
  497      css_classes(Options, Classes)
  498    },
  499    emit(span(class([arithmetic|Classes]),
  500              [ \html_term(Left, Options),
  501                &(nbsp), Text, &(nbsp),
  502                \html_term(Right, Options)
  503              ])).
  504atom(Term, Options) -->
  505    utter(holds(Term), Options).
  506
  507%!  expr(+Term, +Options)// is det.
  508%
  509%   Render an expression.
  510%
  511%   @tbd Should deal with parenthesis  where   needed.  Possibly it is a
  512%   better option to use term//2 from  library(http/html_term) and add a
  513%   portray hook for that?
  514
  515expr(Term, Options) -->
  516    { compound(Term),
  517      compound_name_arguments(Term, Op, [Left, Right])
  518    },
  519    !,
  520    emit(span([ \expr(Left, Options),
  521                &(nbsp), Op, &(nbsp),
  522                \expr(Right, Options)
  523              ])).
  524expr(Term, Options) -->
  525    { compound(Term),
  526      compound_name_arguments(Term, Op, [Arg])
  527    },
  528    !,
  529    emit(span([ Op,
  530                \expr(Arg, Options)
  531              ])).
  532expr(Simple, Options) -->
  533    html_term(Simple, Options).
  534
  535%!  utter(+Expression, +Options)
  536
  537utter(global_constraints_hold, _Options) -->
  538    { human_connector(global_constraints_hold, Text) },
  539    emit(Text).
  540utter(global_constraint(N), _Options) -->
  541    { human_connector(global_constraint(N), Text) },
  542    emit(Text).
  543utter(not(-(Atom)), Options) -->
  544    !,
  545    { human_connector(may, Text) },
  546    emit([Text, ' ']),
  547    atom(Atom, Options).
  548utter(not(Atom), Options) -->
  549    { human_connector(not, Text) },
  550    emit([Text, ' ']),
  551    atom(Atom, Options).
  552utter(-(Atom), Options) -->
  553    { human_connector(-, Text) },
  554    emit([Text, ' ']),
  555    atom(Atom, Options).
  556utter(proved(Atom), Options) -->
  557    { human_connector(proved, Text) },
  558    atom(Atom, Options),
  559    emit([', ', Text]).
  560utter(chs(Atom), Options) -->
  561    { human_connector(chs, Text) },
  562    emit([Text, ' ']),
  563    atom(Atom, Options).
  564utter(abduced(Atom), Options) -->
  565    { human_connector(abducible, Text) },
  566    emit([Text, ' ']),
  567    atom(Atom, Options).
  568utter(according_to(File, Line), _Options) -->
  569    { human_connector(according_to, Text) },
  570    emit(span(class('scasp-source-reference'),
  571              span(class(human), [' [', Text, ' ~w:~w]'-[File, Line]]))).
  572utter(assume(Atom), Options) -->
  573    { human_connector(assume, Text) },
  574    emit([Text, ' ']),
  575    atom(Atom, Options).
  576utter(holds(Atom), Options) -->
  577    { css_classes(Options, Classes) },
  578    (   { atom(Atom) }
  579    ->  { human_connector(holds, Text) },
  580        emit([span(class(Classes), Atom), Text])
  581    ;   { Atom =.. [Name|Args] }
  582    ->  { human_connector(holds_for, Text) },
  583        emit([span(class(Classes), Name), Text]),
  584        list(Args, Options)
  585    ).
  586
  587css_classes(Options, [atom|Classes]) :-
  588    findall(Class, member(class(Class), Options), Classes0),
  589    (   Classes0 == []
  590    ->  Classes = [pos]
  591    ;   Classes = Classes0
  592    ).
  593
  594
  595:- det(html_term//2).  596
  597html_term(Var, Options) -->
  598    { var(Var) },
  599    !,
  600    var(Var, Options).
  601html_term(@(Var:''), Options) -->
  602    { var(Var)
  603    },
  604    !,
  605    var(Var, Options).
  606html_term(@(Var:Type), Options) -->
  607    { var(Var)
  608    },
  609    !,
  610    typed_var(Var, Type, Options).
  611html_term(@(Value:''), Options) -->
  612    !,
  613    html_term(Value, Options).
  614html_term(@(Value:Type), Options) -->
  615    emit('the ~w '-[Type]),
  616    !,
  617    html_term(Value, Options).
  618html_term(Term, _Options) -->
  619    { var_number(Term, _) },
  620    !,
  621    emit('~p'-[Term]).
  622html_term('| '(Var, {Constraints}), Options) -->
  623    !,
  624    inlined_var(Var, Constraints, Options).
  625html_term(Term, _Options) -->
  626    { emitting_as(plain) },
  627    !,
  628    [ ansi(code, '~p', [Term]) ].
  629html_term(Term, Options) -->
  630    term(Term, [numbervars(true)|Options]).
  631
  632%!  var(+Var, +Options)//
  633%
  634%   Handle a variable, optionally with   constraints and annotated using
  635%   ovar_analyze_term/2.
  636
  637var(Var, Options) -->
  638    { copy_term(Var, Copy),
  639      inline_constraints(Copy, Options),
  640      nonvar(Copy),
  641      Copy = '| '(V, {Constraints})
  642    },
  643    !,
  644    inlined_var(V, Constraints, Options).
  645var(Var, _Options) -->
  646    { ovar_var_name(Var, Name)
  647    },
  648    !,
  649    emit(var(Name)).
  650var(_, _) -->
  651    emit(anything).
  652
  653%!  inlined_var(+Var, +Constraint, +Options)//
  654%
  655%   Deal with constraints as represented after inline_constraints/2.
  656
  657inlined_var(Var, Constraints, Options) -->
  658    { Constraints = '\u2209'(Var, List),
  659      Var == '$VAR'('_')
  660    },
  661    !,
  662    (   {List = [One]}
  663    ->  emit('anything except for '),
  664        html_term(One, Options)
  665    ;   emit('anything except for '),
  666        list(List, [last_connector(or)|Options])
  667    ).
  668inlined_var(Var, Constraints, Options) -->
  669    { Constraints = '\u2209'(Var, List),
  670      compound(Var),
  671      Var = '$VAR'(Name)
  672    },
  673    !,
  674    (   {List = [One]}
  675    ->  {human_connector(neq, Text)},
  676        emit([var(Name), ' ', Text, ' ']),
  677        html_term(One, Options)
  678    ;   {human_connector(not_in, Text)},
  679        emit([var(Name), ' ', Text, ' ']),
  680        list(List, [last_connector(or)|Options])
  681    ).
  682inlined_var(Var, Constraints, Options) -->
  683    { comma_list(Constraints, CLPQ)
  684    },
  685    clpq(Var, CLPQ, Options).
  686
  687%!  clpq(@Var, +Constraints, +Options)//
  688
  689clpq(Var, [Constraint|More], Options) -->
  690    { compound(Constraint),
  691      Constraint =.. [_,A,B],
  692      Var == A,
  693      human_connector(Constraint, Text),
  694      (   nonvar(Var),
  695          Var = '$VAR'(Name)
  696      ->  Id = var(Name)
  697      ;   Id = number
  698      )
  699    },
  700    emit(['any ', Id, ' ', Text, ' ']),
  701    html_term(B, Options),
  702    (   {More == []}
  703    ->  []
  704    ;   emit(' and '),
  705        clpq_and(More, Var, Options)
  706    ).
  707
  708clpq_and([Constraint|More], Var, Options) -->
  709    { compound(Constraint),
  710      Constraint =.. [_,A,B],
  711      A == Var,
  712      human_connector(Constraint, Text)
  713    },
  714    emit([Text, ' ']),
  715    html_term(B, Options),
  716    (   {More == []}
  717    ->  []
  718    ;   emit(' and '),
  719        clpq_and(More, Var, Options)
  720    ).
  721
  722%!  typed_var(@Var, +Type, +Options)//
  723
  724typed_var(Var, Type, Options) -->
  725    { copy_term(Var, Copy),
  726      inline_constraints(Copy, Options),
  727      nonvar(Copy),
  728      Copy = '| '(V, {Constraints})
  729    },
  730    !,
  731    inlined_typed_var(V, Type, Constraints, Options).
  732typed_var(Var, Type, _Options) -->
  733    { ovar_var_name(Var, Name)
  734    },
  735    !,
  736    emit([var(Name), ', a ', Type]).
  737typed_var(_Var, Type, _Options) -->
  738    emit(['a ', Type]).
  739
  740
  741inlined_typed_var(Var, Type, Constraints, Options) -->
  742    { Constraints = '\u2209'(Var, List),
  743      Var == '$VAR'('_')
  744    },
  745    !,
  746    (   {List = [One]}
  747    ->  emit(['any ', Type, ' except for ']),
  748        html_term(One, Options)
  749    ;   emit(['any ', Type, ' except for ']),
  750        list(List, [last_connector(or)|Options])
  751    ).
  752inlined_typed_var(Var, Type, Constraints, Options) -->
  753    { Constraints = '\u2209'(Var, List),
  754      nonvar(Var),
  755      Var = '$VAR'(Name)
  756    },
  757    !,
  758    (   {List = [One]}
  759    ->  emit([var(Name), ', a ', Type, ' other than ']),
  760        html_term(One, Options)
  761    ;   emit([var(Name), ', a ', Type, ' not ']),
  762        list(List, [last_connector(or)|Options])
  763    ).
  764inlined_typed_var(Var, Type, Constraints, Options) --> % TBD: include type in NLP
  765    { comma_list(Constraints, CLPQ)
  766    },
  767    clpq(Var, CLPQ, [type(Type)|Options]).
  768
  769%!  list(+Elements, +Options) is det.
  770%
  771%   Emit a collection as "a, b, and c"
  772
  773list([L1,L], Options) -->
  774    !,
  775    { option(last_connector(Conn), Options, and),
  776      human_connector(Conn, Text)
  777    },
  778    html_term(L1, Options),
  779    emit(', ~w '-[Text]),
  780    html_term(L, Options).
  781list([H|T], Options) -->
  782    html_term(H, Options),
  783    (   {T==[]}
  784    ->  []
  785    ;   emit(', '),
  786        list(T, Options)
  787    ).
  788
  789actions(html(HTML), _) -->
  790    !,
  791    emit(HTML).
  792actions([], _) --> [].
  793actions([H|T], Options) -->
  794    action(H, Options),
  795    actions(T, Options).
  796
  797action(text(S), _) -->
  798    !,
  799    emit(S).
  800action(Term, Options) -->
  801    html_term(Term, Options).
  802
  803%!  connector(+Meaning, +Options)//
  804%
  805%   Emit a logical connector.
  806
  807connector(and, _Options) -->
  808    { human_connector(and, Text) },
  809    emit([ span(class(human), [', ', Text]),
  810           span(class(machine), ',')
  811         ]).
  812connector(not, _Options) -->
  813    { human_connector(not, Text) },
  814    emit([ span(class(human), [Text, ' ']),
  815           span(class(machine), 'not ')
  816         ]).
  817connector(-, _Options) -->
  818    { human_connector(-, Text) },
  819    emit([ span(class(human), [Text, ' ']),
  820           span(class(machine), '\u00ac ')
  821         ]).
  822connector(implies, Options) -->
  823    { human_connector(implies, Text) },
  824    emit([ span(class(human),
  825                [', ', \origin_annotated(Text, Options)]),
  826           span(class(machine),
  827                \origin_annotated(' \u2190', Options))
  828         ]).
  829connector(?, _Options) -->
  830    { human_connector(?, Text) },
  831    emit([ span(class(human), Text),
  832           span(class(machine), '.')
  833         ]).
  834connector('.', _Options) -->
  835    emit([ span(class('full-stop'), '.')
  836         ]).
  837
  838human_connector(Term, Connector) :-
  839    phrase(scasp_justification_message(Term), List),
  840    (   List = [Connector]
  841    ->  true
  842    ;   Connector = List
  843    ).
  844
  845full_stop(_Options) -->
  846    emit(span(class(machine), '\u220e')).              % QED block
  847
  848incr_indent(Options0, [depth(D)|Options2]) :-
  849    select_option(depth(D0), Options0, Options1),
  850    select_option(connect(_), Options1, Options2, _),
  851    D is D0+1.
  852
  853		 /*******************************
  854		 *         MACHINE HTML		*
  855		 *******************************/
  856
  857%!  machine_atom(+SCASPAtom, +Options)//
  858%
  859%   Emit an s(CASP) atom with annotations as   they  appear in the model
  860%   and justification.
  861
  862machine_atom(goal_origin(Term, _Origin), Options) -->
  863    !,
  864    machine_atom(Term, Options).
  865machine_atom(not(Term), Options) -->
  866    !,
  867    emit([span(class([connector,not]), not), ' ']),
  868    machine_atom(Term, [class(not)|Options]).
  869machine_atom(-Term, Options) -->
  870    !,
  871    emit([span(class([connector,neg]), '\u00ac'), ' ']),
  872    machine_atom(Term, [class(neg)|Options]).
  873machine_atom(proved(Term), Options) -->
  874    !,
  875    emit([ span(class([connector,proved]), proved), '(',
  876           \machine_atom(Term, [class(proved)|Options]),
  877           ')'
  878         ]).
  879machine_atom(assume(Term), Options) -->
  880    !,
  881    emit([ span(class([connector,assume]), assume), '(',
  882           \machine_atom(Term, [class(assume)|Options]),
  883           ')'
  884         ]).
  885machine_atom(chs(Term), Options) -->
  886    !,
  887    emit([ span(class([connector,chs]), chs), '(',
  888           \machine_atom(Term, [class(chs)|Options]),
  889           ')'
  890         ]).
  891machine_atom(M:Term, Options) -->
  892    { atom(M) },
  893    !,
  894    emit(span(class(module), [M,:])),
  895    machine_atom(Term, [module(M)|Options]).
  896machine_atom(Term, Options) -->
  897    { css_classes(Options, Classes),
  898      merge_options(Options, [numbervars(true)], WOptions)
  899    },
  900    emit(span(class(Classes), \term(Term, WOptions))).
  901
  902:- multifile
  903    term_html:portray//2.  904
  905term_html:portray(Term, Options) -->
  906    { nonvar(Term),
  907      Term = '| '(Var, Constraints)
  908    },
  909    term(Var, Options),
  910    emit(' | '),
  911    term(Constraints, Options).
  912
  913origin(File, Line, Options) -->
  914    {    option(source(true), Options)   },
  915    !,
  916    utter(according_to(File, Line), Options).
  917origin(_, _, _) --> [].
  918
  919origin_annotated(Content, Options) -->
  920    { option(origin(File:Line), Options)
  921    },
  922    !,
  923    emit(span([ class(scasp_origin),
  924                'data-file'(File),
  925                'data-line'(Line)
  926              ], Content)).
  927origin_annotated(Content, _) -->
  928    emit(Content)