#
# pf.pm
#
# Version 0.03
# 2002-05-09
#
# Project:
#
#   pf2html
#   LaTeX2HTML + pf.sty (hypertext proofs)
#
# Project Homepage at:
#
#   http://www.dbai.tuwien.ac.at/proj/pf2html
#
############################################################################
#
# by:
#
#   Wolfgang Slany
#   Martina Osztovits
#   Martin Glowacki
#
#   Vienna University of Technology,
#   Computer Science Department,
#   Institute of Information Systems,
#   Database and Artificial Intelligence Group
#
#   http://www.dbai.tuwien.ac.at/
#
# If there are any problems or questions, please send them to:
#
#   Wolfgang SLANY
#   http://slany.org/wolfgang/
#
############################################################################
#
# This file is part of pf2html.
#
# pf2html is free software; you can redistribute it and/or modify
# it under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 2 of the License, or
# (at your option) any later version.
#
# pf2html is distributed in the hope that it will be useful,
# but WITHOUT ANY WARRANTY; without even the implied warranty of
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
# GNU General Public License for more details.
#
# You should have received a copy of the GNU General Public License
# along with pf2html; if not, write to the Free Software
# Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
#


package pf;


local($proof_env,$proof_step,$proof_stepstart, $reference,@step, %stepref);
local($bgstep,$endstep);
local($shortennumbers);
local($searchfrom);
local(@treated_level);
local($base_section,$base_file);
local(@level_info, @level_text, @level_step_info);


BEGIN
{
  # setting path for config files
  $config_path[0] = $main::LATEX2HTMLDIR;           # path to LaTeX2HTML
  $config_path[1] = $main::LATEX2HTMLDIR."/styles"; # path to LaTeX2HTML styles
  $config_path[2] = $home;                          # path to users home
  $config_path[3] = $main::texfilepath;             # starting path

  # load all pf config files
  for($i=0;$i<=$#config_path;$i++)
  {
    $config_file = $config_path[$i]."/pf.config";

    if ( -e  $config_file )
    {
      print "\nLoading $config_file ...";

      require $config_file;
    }
  }

  $shortennumbers = 0;

  $proof_env       = "\\\\(begin|end)$main::O(\\d+)${main::C}".
                     "proof$main::O\\2$main::C";

  $proof_step      = "\\\\(step)$main::O(\\d+)$main::C(.*)".
                     "$main::O\\2$main::C$main::O(\\d+)".
                     "$main::C(.*)$main::O\\4$main::C";

  $proof_stepstart = "\\\\(step)$main::O(\\d+)".
                     "$main::C(.*)$main::O\\2$main::C";

  $bgstep = "\\\\begin$main::O(\\d+)${main::C}(step\\+)$main::O\\1".
            "$main::C$main::O(\\d+)$main::C(.*)$main::O\\3$main::C";

  $endstep = "\\\\end$main::O(\\d+)${main::C}(step\\+)$main::O\\6$main::C";

  $reference = "\\\\(stepref|levelref)${main::O}(\\d+)".
               "$main::C(.*)${main::O}\\2$main::C";

  # Define default texts
  if ( !defined $proof )       { $proof = "<b>Proof:</b>"; }
  if ( !defined $assume )      { $assume = "Assume"; }
  if ( !defined $let )         { $let = "Let"; }
  if ( !defined $prove )       { $prove = "Prove"; }
  if ( !defined $case )        { $case = "Case"; }
  if ( !defined $proofsketch ) { $proofsketch = "Proof Sketch"; }
  if ( !defined $qed )         { $qed = "QED"; }
  if ( !defined $linktext )    { $linktext = "(Link - more detailed proof)"; }
  if ( !defined $headingtext ) { $headingtext = "More detailed proof"; }

  $partnum     = 0;

  # add body extensions
  $main::BODYTEXT = $main::BODYTEXT . $pf_body;

  # add bookmark link
  $main::CHILDLINE = $main::CHILDLINE . $pf_bookmark;
}


sub do_cmd_proofsection
{
  # parameters to this command between <#nr#> and <#nr#>

  local($_) = @_;

  debug("do_cmd_proofsection");

  s/$main::next_pair_pr_rx//;

  $heading = $2;

  if ( $heading )
  {
    $heading="<H3>$heading</H3>";
  }

  $main::TITLE = "$heading";

  return "$_";
}


sub do_cmd_pfshortnumbers
{
  # parameters to this command between <#nr#> and <#nr#>

  local($_) = @_;

  s/$main::next_pair_pr_rx/$shortennumbers=$2;/eo;

  return "";
}


sub short_display {
  local($x,@s) = @_;
  local($level) = $#s + 1;

  if ($level > $shortennumbers)
  {
    @_[0] = "<$level>$s[$#s]";
  }
}


sub short_level_display
{
  local($x,@s) = @_;
  local($level) = $#s + 1;

  if ($level > $shortennumbers) {
    @_[0] = "<$level>";
  }
}


sub replace_step
{
  local($label,$text,@step) = @_;
  local($stepnumber) = join('.',@step);
  local($origstepnumber)=$stepnumber;

  if ($label eq "")
  {
    $label = "QED$origstepnumber";
  }

  $stepref{$label} = $stepnumber;
  &short_display($stepnumber,@step);

  return "<BR><A NAME=\"$origstepnumber\">$stepnumber:<\/A> ";
}


sub do_cmd_pfsketch
{
   &text_only("$proofsketch:",@_);
}


# do_cmd_pf
#
# Martina Osztovits
# 2000-09-12
#
# Martin Glowacki
# 2001-10-25
#
#
# Directly called by latex2html. Inserts the text for the title of
# a proof section into the HTML output file.
#
#
# parameters:
#
# @_ ... contains the rest of the latex proof
#
#
# return value:
#
# new rest of the proof, containing the title text of the proof

sub do_cmd_pf
{
  local($_) = @_;

  # inserts the title text of the proof and returns the new rest of
  # the proof
  return $proof . $_;
}


# do_cmd_qed
#
# Martina Osztovits
# 2000-09-12
#
# Martin Glowacki
# 2001-11-01
#
#
# Directly called by latex2html. Inserts the qed text
# into the HTML output file.
#
#
# parameters:
#
# @_ ... contains the rest of the latex proof
#
#
# return value:
#
# new rest of the proof, containing the title text of the proof

sub do_cmd_qed
{
   local($_) = @_;

   return "<B>$qed.</B><p>$_";
}


# ...
# ...
# ...

sub do_cmd_assume
{
  local($_) = @_;

  "<B>$assume:</B>".$_;
}


sub do_cmd_prove
{
  local($_) = @_;

   "<B>$prove:</B>".$_;
}


sub do_cmd_pflet
{
   &text_only("$let:",@_);
}


sub do_cmd_case
{
   &text_only("$case:",@_);
}


sub do_env_assumeplus
{
   &text_only("$assume:",@_);
}


sub do_env_proveplus
{
   &text_only("$prove:",@_);
}


sub do_env_caseplus
{
   &text_only("$case:",@_);
}


sub text_only
{
  local($text, $_) = @_;

  "<B>${text}</B> $_<BR>";
}


sub getnext
{
  local (@searchfor, $searchind, $lastind, $cmd, @cmd,$i);

  @searchfor = ('\\begin','\\end','\\stepref','\\nostep','\\qedstep','\\step','\\levelref','\\toplevel','\\pfstepnumber','\\pflevelnumber');
  @cmd = ('bgpfenv','endpfenv','do_cmd_stepref','do_cmd_nostep','do_cmd_qedstep','do_cmd_step','do_cmd_levelref','do_cmd_toplevel','do_cmd_pfstepnumber','do_cmd_pflevelnumber');
  $cmd = undef;
  $lastind = -1;

  for($i=0;$i < @searchfor; $i++) {
    if(($searchind = index($_[0],@searchfor[$i],$searchfrom)) > -1)
    {
      if ($lastind == -1)
      {
         $cmd = @cmd[$i];
         $lastind = $searchind;
      }
      elsif ($lastind > $searchind)
      {
         $cmd = @cmd[$i];
         $lastind = $searchind;
      }
    }
  }

  $searchfrom = $lastind;
  $cmd;
}


sub bgpfenv
{
  local(*param) = @_;
  local($pfenvs);
  local($matched);

  $pfenvs = "\\\\begin$main::O(\\d+)${main::C}(proof|noproof|step\\+)$main::O\\1$main::C";

  if ($param =~ /$pfenvs/ms && index($param,$&,$searchfrom) == $searchfrom)
  {
    $matched = $2;

    debug("bgpfenv: $matched");

    if ($matched eq 'proof')
    {
      &bgproof(*param);
    }
    elsif ($matched eq 'noproof')
    {
      &bgnoproof(*param);
    }
    elsif ($matched eq 'step+')
    {
      &bgstepplus(*param);
    }
  }
  else
  {
    $searchfrom++;
  }
}


sub endpfenv
{
  local(*param) = @_;
  local($pfenvs);

  $pfenvs = "\\\\end$main::O(\\d+)${main::C}(proof|noproof|step\\+)$main::O\\1$main::C";

  if ($param =~ /$pfenvs/ms && index($param,$&,$searchfrom) == $searchfrom)
  {
    if ($2 eq 'proof')
    {
      &endproof(*param);
    }
    elsif ($2 eq 'noproof')
    {
      &endnoproof(*param);
    }
    elsif ($2 eq 'step+')
    {
      &endstepplus(*param);
    }
  }
  else
  {
    $searchfrom++;
  }
}


sub fill_level
{
  local($tofill) = @_;
  local($level)  = $#step + 1;

  push(@level_info,$level);
  push(@level_text,$tofill);
  push(@level_step_info,join('.',@step));
}


sub bgproof
{
  local(*param) = @_;
  local($bgproof);
  local($thisproof);

  debug("bgproof");

  $bgproof = "\\\\begin$main::O(\\d+)${main::C}proof$main::O\\1$main::C";

  $param =~ /$bgproof/ms;
  &fill_level("$`");
  push(@step,0);

  if ( $#step >= $max_level )
  {
    $max_level= $#step+1;
  }

  # COM: $#step entspricht der Baumtiefe des Absatzes
  # COM: $partnum entspricht Absatznummer (nicht Nummerierung)

  my $jf = $javafunc;

  $javafunc = "";

  $mm_show = $html_show;
  $mm_show =~ s/--Section--/$partnum/g;
  $mm_show =~ s/--Background--/$bgcol/g;

  $jf .= $mm_show;

  $mm_show = $html_hide;
  $mm_show =~ s/--Section--/$partnum/g;
  $mm_show =~ s/--Background--/$bgcol/g;

  $jf .= $mm_show;

  my $bgindex = $#step;

  if ( $#step > $#bglist )
  {
    $bgindex = $#bglist;
  }

  my $bgcol = $bglist[$bgindex];

  $mm_show = $startdetail;
  $mm_show =~ s/--Section--/$partnum/g;
  $mm_show =~ s/--Background--/$bgcol/g;

  $jf .= $mm_show;

  &fill_level($jf);

  $partnum++;

  $param =~ s/.*?$bgproof//ms;
  $searchfrom = 0;

  $param;
}


sub endproof
{
  local(*param) = @_;
  local($endproof);
  local($sectext);

  $endproof = "\\\\end$main::O(\\d+)${main::C}proof$main::O\\1$main::C";
  $param =~ /$endproof/;

  &fill_level("$`$enddetail");

  if ( !defined pop(@step))
  {
       print STDERR "Wrong nesting of proof environments\n";
  }

  $param =~ s/.*?$endproof//ms;
  $searchfrom =0;

  $param;
}


sub bgnoproof
{
  local(*param) = @_;
  local($bgproof);

  $bgproof = "\\\\begin$main::O(\\d+)${main::C}noproof$main::O\\1$main::C";
  push(@step,0);
  $param =~ s/$bgproof//;

  $param;
}


sub endnoproof
{
  local(*param) = @_;
  local($endproof);

  $endproof = "\\\\end$main::O(\\d+)${main::C}noproof$main::O\\1$main::C";

  if ( !defined pop(@step))
  {
    print STDERR "Wrong nesting of proof environments\n";
  }

  $param =~ s/$endproof//;

  $param;
}


sub endstepplus
{
  # This procedure should be never called directly!!

  local(*param) = @_;

  $searchfrom++;
}


sub bgstepplus
{
  local(*param) = @_;
  local(*param) = @_;

  local($step,$replace_step);

  if ($param =~ /$bgstep(.*)$endstep/ms)
  {
    $step = pop(@step);
    push(@step,$step + 1 );
    $replace_step = &replace_step($4,$5,@step);

    if (!defined $step)
    {
      print STDERR "$step:@step: Step not within a proof environment\n";
    }

    $param =~ /$bgstep(.*)$endstep/ms;
    &fill_level("$`$replace_step");
    $param =~ s/.*?$bgstep(.*)$endstep//ms;
    $searchfrom=0;
  }
  else
  {
    $searchfrom++;
  }
}


sub do_cmd_step
{
  local(*param) = @_;
  local($step,$replace_step);

  if (  $param =~ /$proof_step/ms )
  {
    $step = pop(@step);
    push(@step,$step + 1 );
    $replace_step = &replace_step($3,$5,@step);

    if (!defined $step)
    {
      print STDERR "$step:@step: Step not within a proof environment\n";
    }

    $param =~ /$proof_step/ms;
    &fill_level("$`$replace_step");
    $param =~ s/.*?$proof_step/$5/ms;
    $searchfrom=0;
  }
  else
  {
    $searchfrom++;
  }

  $param;
}


sub do_cmd_nostep
{
  local(*param) = @_;
  local($step,$stepnumber);
  local($nostepref) = "\\\\(nostep)$main::O(\\d+)$main::C(.*)$main::O\\2$main::C";

  $step = pop(@step);
  push(@step,$step + 1);

  if ($param =~ s/$nostepref//ms)
  {
    &replace_step($3,'',@step);
  }
  else
  {
    $searchfrom++;
  }

  $param;
}


sub do_cmd_qedstep
{
  local(*param) = @_;
  local($step,$stepnumber);

  $step = pop(@step);
  push(@step,$step + 1);
  $stepnumber = &replace_step("","Q.E.D.",@step);
  &short_display($stepnumber,@step);
  $param =~ /\\qedstep/;
  &fill_level("$`<BR>${stepnumber}Q.E.D.");
  $param =~ s/.*?\\qedstep//ms;
  $searchfrom=0;

  $param;
}

sub do_cmd_stepref
{
  local(*param) = @_;
  $param =~ /$reference/;

  local($replacewith) =  $stepref{$3} ;
  local($origref);
  local(@replacewith) = split(/\./,$replacewith);
  local($i) = 0;
  local($filenr);

  if (!defined $replacewith)
  {
    $replacewith = '??';
  }
  elsif ($#replacewith > $#step)
  {
    $replacewith = '??';
  }
  else
  {
    $i=0;

    while($i <= $#replacewith && $replacewith ne '??')
    {
      if ($step[$i] < $replacewith[$i])
      {
        $replacewith = '??';
      }

      $i++;
    }
  }

  $origref= $replacewith;

  if ($replacewith ne '??')
  {
    &short_display($replacewith, @replacewith);

    # Querverweise
    $replacewith="<A HREF=\"#$origref\">$replacewith<\/A>";
  }

  if (!($param =~ /$reference/ms))
  {
    $searchfrom++;
  }
  else
  {
    $searchfrom=0;
    &fill_level("$`$replacewith");
    $param =~ s/.*?$reference//ms;
  }

  $param;
}


sub do_cmd_levelref
{
  local(*param) = @_;

  $param =~ /$reference/;

  local($replacewith) =  $stepref{$3} ;
  local(@replacewith) = split(/\./,$replacewith);
  local($i) = 0;

  if (!defined $replacewith)
  {
       $replacewith = '??';
  }
  elsif ($#replacewith > $#step)
  {
       $replacewith = '??';
  }
  else
  {
    $i=0;

    while($i <= $#replacewith && $replacewith ne '??')
    {
      if ($step[$i] < $replacewith[$i])
      {
        $replacewith = '??';
      }

      $i++;
    }
  }

  if ($replacewith ne '??')
  {
    &short_level_display($replacewith, @replacewith);
  }

  if (!($param =~ /$reference/))
  {
    $searchfrom++;
  }
  else
  {
    $searchfrom=0;
    &fill_level("$`$replacewith");
    $param =~ s/.*?$reference//ms;
  }

  $param;
}


sub do_cmd_toplevel
{
  local(*param) = @_;
  local($level) = $#step + 1;
  local($replacewith);

  $param =~ /\\toplevel/;

  if ($level > $shortennumbers)
  {
    $replacewith = "<0>";
  }
  else
  {
    $replacewith="0";
  }

  $searchfrom=0;
  &fill_level("$`$replacewith");
  $param =~ s/.*?\\toplevel//ms;

  $param;
}


sub do_cmd_pfstepnumber
{
  local(*param) = @_;
  local($level,$number,$longnumber);
  local($replacewith);
  local($pfstepnumber) = "\\\\pfstepnumber$main::O(\\d+)$main::C(.*)$main::O\\1$main::C$main::O(\\d+)$main::C(.*)$main::O\\3$main::C$main::O(\\d+)$main::C(.*)$main::O\\5$main::C";

  if ($param =~ /$pfstepnumber/)
  {
    $level = $2;
    $number = $4;
    $longnumber = $6;

    if ($level > $shortennumbers)
    {
      $replacewith="<$level>$number";
    }
    else
    {
      $replacewith="$longnumber";
    }

    $searchfrom=0;
    &fill_level("$`$replacewith");
    $param =~ s/.*?$pfstepnumber//ms;
  }
  else
  {
    $searchfrom++;
  }

  $param;
}


sub do_cmd_pflevelnumber
{
  local(*param) = @_;
  local($level,$longnumber);
  local($replacewith);
  local($pflevelnumber) = "\\\\pflevelnumber$main::O(\\d+)$main::C(.*)$main::O\\1$main::C$main::O(\\d+)$main::C(.*)$main::O\\3$main::C";

  if ($param =~ /$pflevelnumber/)
  {
    $level = $2;
    $longnumber = $4;

    my $origref = $level + 1;
    #my $origref = $level;

    if ( $origref > $shortennumbers )
    {
      $replacewith="<$level>";
      # oder
      # $replacewith="<$origref>";
      # <1>.1 statt <0>.1
    }
    else
    {
      $replacewith="$longnumber";
    }

    $replacewith = "<a href=\"#$origref\">$replacewith</a>";

    $searchfrom=0;
    &fill_level("$`$replacewith");
    $param =~ s/.*?$pflevelnumber//ms;
  }
  else
  {
    $searchfrom++;
  }

  $param;
}


sub do_env_proof
{
  # Changes for level version:
  # $base_section: to keep track of the base_section and calculate the index of
  # the new sections
  # @level_info: stores the level on which the text occured
  # @level_text: stores the text.

  debug("do_env_proof");

  $searchfrom = 0;
  $base_section=$main::i;
  @treated_level=();
  undef @level_info;
  undef @level_text;
  $main::CURRENT_FILE =~ /node(\d+)$main::EXTN/;
  $base_file=$1;
  local($newlevel) = $main::section_commands{$main::curr_sec}+1;
  $main::section_commands{'proofsection'}=$newlevel;
  $main::section_headings{'proofsection'}='<H3>';

  local($next);
  local($text) = @_;

  # Adds a proof section for hiding the hole proof.
  $text = "\\begin<<0>>proof<<0>>" . $text . "\\end<<0>>proof<<0>>";

  # debug proof text
 # debug($text);

  # init step stack (empty stack)
  @step = ();

  # init max_level (depth is 0 because step stack is empty)
  $max_level = 0;

  while (defined ($next = &getnext($text)))
  {
    &{$next}(*text);
  }

  if ( !defined pop(@step) && defined pop(@step))
  {
    print STDERR "Wrong nesting of proof environments\n";
  }

  for ($i=1;$i<=2;$i++)
  {
    $prev_section = $base_section+($i-2)*5;

    if ($i == 1)
    {
      $text = $level_text[0];
    }
    else
    {
      @main::sections=(@main::sections[0..$prev_section],'','proofsection','<','<' ,"<1>>$headingtext<<1>>$level_text[0]",@main::sections[${prev_section}+1..$#main::sections]);
    }

    for ($j=1;$j<=$#level_info;$j++)
    {
      $this_section = $prev_section +5;

      @main::sections[$this_section] .= $level_text[$j];
    }
  }

  "\n$text\n";
}


sub debug
{
#  print "\n".$_[0];
}


1;


# EOF pf.pm
