module html.
import control, maps, alist.
import goals.
import lj, fol, printer.
%%%%%% Some primitives for putputing html sources. %%%%%%%
type html_open_append string -> o -> o.
type html_open_out string -> o -> o.
type html_table string -> o -> o.
type html_color string -> o -> o.
type html_env string -> o -> o.
type html_row, html_datum o -> o.
html_open_append FileName G :-
open_append FileName Out,
((pi X\ ooo X :- output Out X) => G),
close_out Out.
html_open_out FileName G :-
open_out FileName Out,
((pi X\ ooo X :- output Out X) => G),
close_out Out.
html_table Attributes G :-
ooo "
\n".
html_row G :- ooo "\n", G, ooo "
\n".
html_datum G :- ooo "", G, ooo " | \n".
html_color Color G :-
ooo "", G, ooo "".
html_env String G :-
ooo "<", ooo String, ooo ">", G, ooo "", ooo String, ooo ">".
%%%%%%% Printing of terms and formulas %%%%%%%%%
type html_term i -> o.
html_term Term :-
if (print_name_term Term Name nil)
(ooo Name)
(print_name_term Term Name Terms, ooo "(", ooo Name,
forevery (T\ (ooo " ", html_term T)) Terms, ooo ")").
type html_form form -> o.
type html_forall_list string -> (i -> form) -> o.
type html_exists_list string -> (i -> form) -> o.
html_form truth :- html_color "blue" (ooo "truth").
html_form false :- html_color "blue" (ooo "false").
html_form (neg A) :-
ooo "(",html_color "blue" (ooo "neg "), html_form A, ooo ")".
html_form (A and B) :-
ooo "(", html_form A, html_color "blue" (ooo " and "), html_form B, ooo ")".
html_form (A or B) :-
ooo "(", html_form A, html_color "blue" (ooo " or "), html_form B, ooo ")".
html_form (A imp B) :-
ooo "(", html_form A, html_color "blue" (ooo " => "), html_form B, ooo ")".
html_form (forall Name B) :-
ooo "(", html_color "green" (ooo "forall "),
html_forall_list Name B, ooo ")".
html_forall_list Name (x\ forall Name' (B x)) :- !,
choose_name Name Cname, ooo Cname, ooo ", ",
piname Cname x\(html_forall_list Name' (B x)).
html_forall_list Name B :-
choose_name Name Cname, ooo Cname, ooo " ", piname Cname x\(html_form (B x)).
html_form (exists Name B) :-
ooo "(", html_color "green" (ooo "exists "),
html_exists_list Name B, ooo ")".
html_exists_list Name (x\ exists Name' (B x)) :- !,
choose_name Name Cname, ooo Cname, ooo ", ",
piname Cname x\(html_exists_list Name' (B x)).
html_exists_list Name B :-
choose_name Name Cname, ooo Cname, ooo " ", piname Cname x\(html_form (B x)).
html_form Atom :-
if (print_name_pred Atom Name nil)
(ooo Name)
(print_name_pred Atom Name Terms, ooo "(", ooo Name,
forevery (T\ (ooo " ", html_term T)) Terms, ooo ")").
%%%% Print of sequents. %%%%%
type html_seq goal -> o.
type html_vars list (pair i string) -> o.
type html_hyps int -> list form -> o.
type html_conc form -> o.
html_seq (Vars | Delta --> C) :-
html_open_append "seq.html"
(html_table "Border=5 CELLPADDING=4 CELLSPACING=3"
(html_vars Vars,
load_print_names Vars (html_hyps 1 Delta, html_conc C)),
ooo"\n").
html_vars nil.
html_vars (V::Vs) :-
html_row (html_datum (html_color "red" (ooo "Vars")),
html_datum
(html_env "tt"
(forevery (v\(sigma N\sigma V\(v = (pr V N), ooo N, ooo " ")))
(V::Vs)))).
html_conc C :-
html_row (html_datum (html_color "red" (ooo "Thus")),
html_datum (html_env "tt" (html_form C))).
html_hyps N nil.
html_hyps N (H::Hs) :-
html_row (html_datum (html_color "red" (term_to_string N S, ooo S)),
html_datum (html_env "tt" (html_form H))),
M is (N + 1), html_hyps M Hs.