elpi2html.elpi

/* elpi: embedded lambda prolog interpreter                                  */
/* license: GNU Lesser General Public License Version 2.1 or later           */
/* ------------------------------------------------------------------------- */

accumulate elpi_elpi/elpi-quoted_syntax.

shorten std.{spy, rev, exists}.

pred iter i:(A -> prop), o:list A.
iter _ [].
iter P [X|XS] :- P X, iter P XS.

pred iter-sep i:list string, i:string, i:(list string -> A -> list string -> prop), i:list A, i:list string.
iter-sep _ _ _ [] _.
iter-sep _ S P [X] A :- !, P [] X A.
iter-sep B S P [X|XS] A :- P B X [], write S, iter-sep [] S P XS A.

pred iter-sep2 i:list string, i:string, i:string, i:(list string -> A -> list string -> prop), i:list A, i:list string.
iter-sep2 _ _ _  _ [] _.
iter-sep2 _ S _  P [X] A :- !, P [] X A.
iter-sep2 B S S1 P [X|XS] A :- P B X [S1], write S, iter-sep2 [] S S1 P XS A.

pred monad i:list (S -> S -> prop), i:S, o:S.
monad [] X X.
monad [P|PS] X R :- P X X1, monad PS X1 R.

pred len i:list A, o:int.
len uvar 0.
len [] 0.
len [_|XS] N :- len XS M, N is M + 1.

pred write-to o:ctype "out_stream".
pred write i:string.
write S :- write-to OC, output OC S.

pred sanitize i:string, o:string.
sanitize X Y :-
  monad [
    rex_replace "&" "&",
    rex_replace "<" "&lt;",
    rex_replace ">" "&gt;",
    rex_replace "\"" "&quot;",
    rex_replace "'" "&apos;" ]
  X Y.

pred mk-name i:string, i:A, o:string.
mk-name S1 I Y :-
  Y is "<span class='name' varname='" ^
       {term_to_string I} ^
       "'>" ^ S1 ^ "</span>".

pred cur-int o:int.
pred incr-int i:prop.
incr-int P :- cur-int J, I is J + 1, (cur-int I :- !) => P.

pred var-to-string i:A, i:B, o:string.
var-to-string X I Y :-
  cur-int J, S1 is "x<sub>" ^ {term_to_string J} ^ "</sub>",
  mk-name S1 I Y.
pred uvar-to-string i:A, i:B, o:string.
uvar-to-string X I Y :-
  cur-int J, S1 is "X<sub>" ^ {term_to_string J} ^ "</sub>",
  mk-name S1 I Y.
pred name-to-string i:string, i:B, o:string.
name-to-string X0 I Y :-
  if (rex_match "^_" X0) (X = "_") (X = X0),
  rex_replace "^\\([A-Za-z]+\\)_?\\([0-9]+\\)_?$" "\\1<sub>\\2</sub>" X S1,
  mk-name S1 I Y.

pred concat i:list string, o:string.
concat [] "".
concat [X|XS] S :- concat XS Res, S is X ^ Res.

pred par? i:int, i:int, i:list string, i:list string, o:list string, o:list string.
par? CL PL Open Close Open1 Close1 :-
  if (CL =< PL)
     (Open1 = Open, Close1 = Close)
     (Open1 = ["("|Open], Close1 = [")"|Close]).

kind option type -> type.
type some A -> option A.
type none option A.

pred grab-list i:term, o:list term, o:option term.
grab-list (const "[]") [] none.
grab-list (app [ const "::", X, XS]) [ X | R ] T :- grab-list XS R T.
grab-list X [] (some X).


pred infx i:string, o:int, o:string, o:int, o:int.
% TODO: fix precendences
infx "<"  60 "&nbsp;&lt;&nbsp;"      60 60.
infx "=>" 60 "&nbsp;<b>⇒</b>&nbsp;"  59 59.
infx "="  60 "&nbsp;=&nbsp;"           70 70.
infx "^"  60 "&nbsp;^&nbsp;"           60 60.
infx "is" 60 "&nbsp;<b>is</b>&nbsp;" 60 60.
infx ";"  50 "&nbsp;;&nbsp;"         50 50.
infx "+"  60 "&nbsp;+&nbsp;"           60 60.
infx "*"  60 "&nbsp;*&nbsp;"           60 60.
infx "as"  0 "&nbsp;<b>as</b>&nbsp;" 60 60.

%@log (pp _ _ _ _).

pred pp-compound i:prop.
pp-compound P :- write "<div class='compound'>", P, write "</div>".

%    pp Level  ParensBefore   Term    ParensAfter
pred pp i:int, i:list string, i:term, i:list string.
pp L B (app [ const OP, Left, Right ]) A :- infx OP LOP S PL PR, !,
  par? L LOP B A B1 A1,
  pp-compound (pp PL B1 Left  [S]),
  pp-compound (pp PR [] Right A1).

pp L B (app [ const ":-" , Hd , Hyps ]) A :-
  par? L 60 B A B1 A1,
  if (Hyps = app [ const "," , const "!" | Rest])
     (Hyps2 = app [ const "," | Rest], NeckCut = " neckcut")
     (Hyps2 = Hyps, NeckCut = ""),
  write "<div class='hyps'>",
  pp 59 B1 Hyps2 [],
  write "</div>",
  Concl is "<div class='concl" ^ NeckCut ^ "'><div class='compound'>",
  write Concl,
  pp 59 [] Hd A1,
  write "</div></div>".

pp L B (app [ const C, lam _ ] as T) A :- (C = "pi"; C = "sigma"), !,
  par? L 60 B A B1 A1,
  pp-quantifier-block B1 C T [] A1.

pred pp-quantifier-block i:list string, i:string, i:term, i:list string, i:list string.
pp-quantifier-block B C (app [ const C, lam F ]) Args A :- !, incr-int (
  new_int I,
  pi x\ if (C = "pi") (var-to-string x I X) (uvar-to-string x I X),
        is-name x X => pp-quantifier-block B C (F x) [X|Args] A).
pp-quantifier-block B C T Args A :-
  write "<div class='compound'>",
  write-math-quantifier B C,
  iter-sep [] " " (b\ x\ a\ write x) {rev Args} [],
  write ". </div><div class='compound'>",
  pp 60 [] T A,
  write "</div>".

pred write-math-quantifier i:list string, i:string.
write-math-quantifier B "pi"    :- write {concat B}, write "<b>∀</b>".
write-math-quantifier B "sigma" :- write {concat B}, write "<b>∃</b>".

pp L B (app [ const "," | Args ]) A :-
  par? L 60 B A B1 A1,
  write "<div class='hyp compound' level='60'>",
  iter-sep2 B1 "</div><div class='hyp compound'>" "," (pp 59) Args A1,
  write "</div>".

pp L B (app [ const "::", HD, TL ]) A :-
  par? L 99 B A B1 A1,
  grab-list TL Args Last,
  write "<div class='compound' level='99'><b>[</b><div class='compound'>",
  iter-sep2 B1 "</div><div class='compound'> " "<b>,</b>" (pp 61) [HD|Args] [],
  if (Last = some X) (write " <b>|</b> ", pp 0 [] X []) (true),
  write "</div><b>]</b></div>", write {concat A1}.

pp L B (app Args) A :-
  par? L 65 B A B1 A1,
  iter-sep B1 " " (pp 66) Args A1.

pp L B (lam F) A :- incr-int (
  par? L 70 B A B1 A1,
  new_int I,
  pi x\
    write "<div class='compound' level='70'><b>λ</b>",
    write {concat B1},
    var-to-string x I X, write X,
    write ". </div><div class='compound'>",
    is-name x X => pp 10 [] (F x) A1,
    write "</div>").

pp _ B (const "!") A :- !,
  write {concat B},
  write "<span class='cut'>!</span>",
  write {concat A}.

pp _ B (const "discard") A :-
  write {concat B},
  write "_",
  write {concat A}.

pp _ B (const X) A :-
  write {concat B},
  write {sanitize X},
  write {concat A}.

pp _ B X A :- is-name X Y, !,
  write {concat B}, write Y, write {concat A}.

pp _ B (cdata S) A :- is_cdata S _, !,
  term_to_string S Y,
  write {concat B},
  write Y,
  write {concat A}.

pp _ B X A :- write "ERROR".

pred hd-symbol i:term.
hd-symbol (app [ const ":-", H, _ ]) :- hd-symbol H.
hd-symbol (app [ const S | _ ]) :- write S.
hd-symbol (const S) :- write S.

type is-name term -> string -> prop.
pred write-clause i:clause.
write-clause (clause Loc [] (arg Body)) :-
  new_int I,
  (pi x\ X is "X" ^ {term_to_string I}),
  name-to-string X I A1,
  pi x\ is-name x A1 => write-clause (clause Loc [] (Body x)).
write-clause (clause Loc [A|Args] (arg Body)) :-
  new_int I, name-to-string A I A1,
  pi x\ is-name x A1 => write-clause (clause Loc Args (Body x)).
write-clause (clause Loc [] C) :- !,
  write "<div class='clause' predicate='", hd-symbol C, write "'>",
  write "<div class='loc'>",
    term_to_string Loc LocS, write LocS,
  write "</div>",
  cur-int 0 =>
  if (C = app [const ":-"|_])
     (pp 0 [] C [])
     (write "<div class='hyps'><div class='hyp'></div></div><div class='concl'>",
       pp 0 [] C [],
      write "</div>"),
  write "</div>\n".

pred write-preamble i:string.
write-preamble F :-
  write "<!DOCTYPE html>
         <html>
         <head>
           <meta charset='UTF-8'>
           <title>",
  write F,
  write "  </title>
           <link rel='stylesheet'
             href='https://code.jquery.com/ui/1.12.1/themes/base/jquery-ui.css'>
           <script src='https://code.jquery.com/jquery-1.12.4.js'></script>
           <script src='https://code.jquery.com/ui/1.12.1/jquery-ui.js'></script>
           <script>
           $( function() {
               $( '.clause' ).each(function() { $( this ).resizable({
                    start: function( event, ui ) {
                      //$( ui.element ).css('max-width','100%');
                    }
              }); });
           } );
// Highlight the box around compound elements
$( function() {
  $('.compound').each(function() {
    $( this ).mouseover(function (e) {
      e.stopPropagation();
      $( this ).addClass('hover')
    }).mouseout(function (e) {
      $( this ).removeClass('hover')
    })
  });
});

// Highlight all variables named the same
$( function() {
  $('.name').each(function() {
    $( this ).mouseover(function (e) {
      $( 'span[varname=' + $( this ).attr('varname') + ']' ).addClass('samevar')
    }).mouseout(function (e) {
      $( 'span[varname=' + $( this ).attr('varname') + ']' ).removeClass('samevar')
    })
  });
});

           </script>
           <style>
           .clause{
             display: inline-block;
             padding: 1em;
             margin: 5px;
             border: 2px solid black;
             width: 30em;
             cursor: default;
           }
           .hidden {
             display: none;
           }
           .hyps {
             display: block;
           }
           .hyp {
             display: inline-block;
             margin-right: 1em;
             margin-top: 0.5em;
           }
           .compound {
             display: inline-block;
             vertical-align: top;
             padding-left: 1em;
             text-indent: -1em;
             border: 1px solid transparent;
           }
/*
           .hover:after {
             content: attr(level);
             position: fixed;
             right: 0;
             top: 0;
           }
*/
           .hover {
             border: 1px dotted grey;
             transition: border 0.5s;
           }
           .samevar {
             color: #22aD22;
             transition: color 0.5s;
             border: 1px dotted #22aD22;
             transition: border 0.5s;
           }
           .name {
             border: 1px solid transparent;
           }
           .concl {
             display: block;
             border-top: 1px solid black;
           }
           .neckcut {
             border-top: 2px solid red;
           }
           .cut {
             color: red;
           }
           .loc {
             display: block;
             background-color: #ecebeb;
           }
         </style>
         </head>
         <body>
         <h1>",
  write F,
  write "</h1>
         <script type='text/javascript'>
         function filter() {
           var f = document.getElementById('filter').value;
           var cl = document.getElementsByClassName('clause');
           for (i=0;i < cl.length; i++) {
             if (cl[i].getAttribute('predicate') === f || f === '' ) {
               cl[i].classList.remove('hidden')
             } else {
               cl[i].classList.add('hidden')
             }
           }
         }
         </script>
         <p>Filter predicate: <input onkeyup='filter();' type='text' id='filter' name='filter'></p>
".

pred write-end.
write-end :-
  write "</body></html>".

pred filter-out i:list A, i:(A -> prop), o:list A.
filter-out [] _ [].
filter-out [X|XS] P R :-
  if (P X) (R = [X | RS]) (R = RS),
  filter-out XS P RS.

pred write-html i:list clause, i:string, i:(string -> prop).
write-html P F R :-
  filter-out P (c\
    sigma Loc LocS \ c = (clause Loc _ _),
    term_to_string Loc LocS, not(R LocS)) PF,
  write-preamble F,
  iter write-clause PF,
  write-end.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

pred main-quoted i:list clause, i:string, i:list string.

% entry point from a software having the program in compiled form
main-quoted P OUT FILTERS :-
  open_out OUT OC,
  R = (x\exists FILTERS (y\ rex_match y x)),
  write-to OC => write-html P OUT R,
  close_out OC.

pred main i:list string.
type main prop.

% entry point from the command line
main [IN,OUT|FILTERS] :- !,
  quote_syntax IN "main" P _,
  main-quoted P OUT FILTERS.

main _ :- usage.
main.

usage :-
  halt "usage: elpi elpi2html.elpi -exec main -- in out [filter]".

% vim: set ft=lprolog: