#!/usr/bin/env perl # quick and dirty perl hack to HTML-ize prover9 output # written and put into the public domain by Hans Lub, hanslub42@gmail.com # VERSION: 0.02 (24/8/10) # TODO: more derivations (like binary resolution) # highlighting subterms or specific sides of an equation? use strict; my $javascript = < Prover9 output highlighter

Move the mouse cursor over the red:[red] justifications after the blue:[generated clauses] below to highlight the corresponding parent literals (i.e. the _from_, _into_ or resolved literals in the parent clauses) . "Active" literals (like the _from_ literal in a paramodulation, or the satellites in a hyperresolution step) get a [red]:pink background, the other ones a [blue]:lightblue one. Not all justifications work and no effort is made to highlight subterms of literals.

Highlighting is "sticky" and stays around until a different justification is highlighted (so that one can scroll around large output sets)

If there is more than one clause with the same number (those will always be identical) , only the first occurence gets highlighted.

EOF $intro = miniwikify($intro); my $current_clause; # the current clause my $lastclause; # some justifications implicitly assume a working clause from some previous justification ... # ... remember it here. my $justno = 0; # running counter to number the justifications my $debug = 0; my $mark_constants = 1; # whether to make constants stand out. print "$intro

\n";

while (<>) {
     # Parse proof line
     my ($intro, $number, $number2, $clause, $label, $justification) = 
        / (                   
           (^\d+)                                  # In CLAUSES FOR SEARCH section, clauses start with a number
          | ^given.*?:\s*(\d+)                     # In SEARCH section, clauses start with "given ... : nn
          )
         ([^.\#]*)                                 # the clause proper
         (\#[^.]*)?\.\s*                           # possibly an attribute, and certainly a dot
         \[(.*?)\]\.                               # the justification is always there, in [] brackets and terminated by a dot
        /x;                                        # Long live regexps with whitespace and comments!
     $number ||= $number2;                                                 
     $current_clause = $number;
     debug($justification);
     
     unless ($number) {                            # Only lines with a $number are interesting
         my $ordinary_line = $_;
         $ordinary_line = span($ordinary_line, style => "color:firebrick;") if (/^===/);  # Paint === BLAH === lines red (like Emacs comment lines)
         print $ordinary_line; 
         next;
     }

     # Treat literals:
     my @literals = split /\s*\|\s*/, $clause;     # split the clause into literals
     my $litnumber = 0;
     foreach my $literal (@literals) {             # wrap each literal in separate  tag
         $literal =~  s/\b([a-tA-Z](?>[\w\_\$\d]*))(?!\()/span($1, style => "font-weight:bold;")/ge if $mark_constants;
         # NB: the (?> ..) syntax above is "experimental" according to perl docs!
         $literal = span($literal, id=>"lit_${number}_${litnumber}");
         $litnumber++;
     }
     $clause = join span(" | ",style=>"color:red;"), @literals;

     $lastclause = 0;
     # Treat justifications, e.g. copy(6) or para(1(a,1),11(a,1)):
     my @justifications =split_terms($justification);
     foreach my $justification (@justifications) { # split justification list
         my ($rule, undef,$details) = ($justification =~ /^(\w+)(\((.*)\))?$/); # we know that justification ends with a )
         $justification = annotate_rule($rule, $details); # annotate (presumably by adding some hover effect)
     }
     $justification = join ", ", @justifications;

     print "$intro " . span($clause, style => "color:blue;") . "$label. [$justification].\n";
}

print "

\n"; # the function 'make_hoverable' adds an appropriate hover effect to some html element. The spans to highlight (and their background colours) # are specified in the argument %target2colour sub make_hoverable { # call like make_hoverable("para(1(a,1),11(b,6))",lit_1_1=>$fromcolour, lit_11_2=>$intocolour) my ($element, %target2colour) = @_; my $onmouseover = "if (unhighlight_all) {unhighlight_all()} this.style.backgroundColor='silver';"; my $unhighlight = "document.getElementById('justification_$justno').style.backgroundColor='white';"; foreach my $target (keys %target2colour) { $onmouseover .= "highlight('$target', '$target2colour{$target}'); "; $unhighlight .= "highlight('$target', 'white'); "; } $onmouseover .= "unhighlight_all = function() {$unhighlight}; return true;"; # put anonymous unhighlight function into var 'unhighlight_all' my $result = span($element, id => "justification_$justno", style => "color:red;", onmouseover => $onmouseover); $justno++; return $result; } # the function 'split_terms' splits a list of terms taking care to ignore the commas *within* terms # e.g: split_terms("a,b(c,d),e") = ("a","b(c,d)","e") sub split_terms { my($text) = @_; $text .= ","; my @terms; my $seen; my @chars = split //, $text; my $parencount = 0; for (my $i = 0; $i < length($text); $i++) { $parencount++ if $chars[$i] eq "("; $parencount-- if $chars[$i] eq ")"; if ($parencount == 0 and $chars[$i] eq ",") { $seen =~ s/^\s+//; $seen =~ s/\s+$//; push @terms, $seen; $seen = ""; next; } $seen .= $chars[$i]; } return @terms; } # The function 'annotate_rule' takes two arguments like "para" and "9(a,1),8(a,1)" and returns the complete justification ("para(9(a,1),8(a,1))") # within a with Javascript to add the hover effect sub annotate_rule { my ($rule, $details) = @_; my $the_clause = $lastclause || $current_clause; my (@hoverspans, $i); return $rule unless $details; if ($rule eq "para") { ### paramodulation ### my ($fromlit, $intolit) = map {literal($_)} split_terms($details); return make_hoverable("$rule($details)", $fromlit => "pink", $intolit => "lightblue"); } elsif ($rule eq "xx" or $rule eq "merge") { ### x=x or merge ### my $litno = letter2number($details); return make_hoverable("$rule($details)", "lit_${the_clause}_${litno}" => "lightblue"); } elsif ($rule eq "ur" or $rule eq "hyper") { ### hyper- or unit resolution ### my @details = split_terms($details); my $planet = shift @details; while($details[$i+2]) { my($planet_lit, $sattelite_clause, $sattelite_lit) = (letter2number($details[$i]), $details[$i+1], letter2number($details[$i+2])); push(@hoverspans,"lit_${planet}_${planet_lit}"=>"lightblue", "lit_${sattelite_clause}_${sattelite_lit}" => "pink"); $i += 3; } return make_hoverable("$rule($details)",@hoverspans); } elsif ($rule eq "rewrite") { ### rewrite (difficult!) $details =~ s/[\[\]]//g; # get rid of [] brackets my @details = split_terms($details); foreach my $rewrite_step (@details) { my ($clause, $direction) = ($rewrite_step =~ /^(\d+).*?(R)?/); push(@hoverspans, "lit_${clause}_0" => # clauses used for rewriting must be unit clauses (??) ($direction ? "plum" : "pink")); # plum clauses should be read in reverse } return make_hoverable("$rule([$details])",@hoverspans); } elsif ($rule eq "flip") { ### flip (often the clause has disappeared ### my $litno = letter2number($details); return make_hoverable("$rule($details)", "lit_${the_clause}_${litno}" => "lightblue"); } else { ### anything else: print as-is ### return "$rule($details)"; } } # The function 'literal' takes a clause/(sub)term spec like "9(b,1)" and returns its corresponding span id ("lit_9_2") sub literal { my ($text) = @_; my ($clause, $litletter) = ($text =~ /^(\d+)\(([a-z])/); my $litno = letter2number($litletter); $lastclause = $clause; # remember working clause in global var return "lit_${clause}_${litno}"; } # a -> 0, b -> 1 etc sub letter2number { my ($letter) = @_; return unpack("c", $letter) - 97; } # build a ""bla" ...>bleh" element sub span { my ($text, %attr) = @_; my @attrlist; foreach my $key (keys %attr) { push @attrlist, "$key=\"$attr{$key}\""; } my $attrlist = join ' ', @attrlist; return "$text"; } sub miniwikify { my ($text) = @_; $text =~ s/(\w+):\[([^]]+)\]/span($2,style=>"color:$1;")/ge; # green:[plants] $text =~ s/\[([^]]+)\]:(\w+)/span($1,style=>"background-color:$2;")/ge; #[clouds]:blue $text =~ s/_([^_]+)_/$1<\/em>/g; # _important_ return $text; } sub debug { my ($text) = @_; print STDERR "$text\n" if $debug; }