#!/usr/bin/perl

# Assumptions:
#  Comments on one line are stripped
#  Comments on many lines:
#   nothing after *) (end of command)
#  Commands could be nested (but see previous assumption)
#  Commands don't span on several lines
#  If a line is commented, the comment must begin at the begin of line and end
#   at the end of line
#  In a line, before a command only spaces are allowed

$curi = $ARGV[0];
$with_types = ($ARGV[1] ? ".types" : "");
$ident = " ";
$cid = 1;
$opencom = 0;
$openscheme = 0;
$openfix = 0;
$opengoal = 0;

print <<EOT;
<?xml version="1.0" encoding="ISO-8859-1"?>
<!DOCTYPE Theory SYSTEM "http://localhost:8081/getdtd?uri=maththeory.dtd">

<Theory uri="cic:/$curi">
EOT

while (<STDIN>) {
 chomp;
 if ($opencom > 0) {
  $opencom-- if (/\*\)/ && !/\(\*.*\*\)/);
 } else {
  if (/\(\*.*\*\)/) { # (* comment *)
   s/\(\*.*\*\)//;
  } elsif (/\(\*/) {
   # (* comment
   $opencom++;
   $_ = "";
  }

  if (/Require /) {
   s/ *Require *(.*)\..*/$1/;
   print "$ident<!-- Require $_ -->\n";
  } elsif (/Goal /) {
   $opengoal = 1;
  } elsif (/Section /) {
   s/ *Section *(.*)\..*/$1/;
   print "$ident<SECTION uri=\"$1\">\n";
   $ident = $ident." ";
  } elsif (/Chapter /) {
   s/ *Chapter *(.*)\..*/$1/;
   print "$ident<SECTION uri=\"$1\">\n";
   $ident = $ident." ";
  } elsif (/End /) {
   chop($ident);
   print "$ident</SECTION>\n";
  } elsif (/Variable(s?) /) {
   s/ *Variable(s?) *([^:]*):.*/$2/;
   s/ //g;
   @vl = split /,/;
   foreach (@vl) {
    print "$ident<VARIABLE uri=\"$_.var$with_types\"/>\n";
   }
  } elsif (/Hypothesis /) {
   s/ *Hypothesis *([^ :]*)( |:).*/$1/;
   @vl = split /,/;
   foreach (@vl) {
    print "$ident<VARIABLE uri=\"$_.var$with_types\"/>\n";
   }
  } elsif (/^ *Inductive /) {
   if (/ *Inductive *[^ :]+ ([^ :]*) :=/) {
    s/ *Inductive *[^ :]+ ([^ :]*) *:=.*/$1/;
   } elsif (/ *Inductive *[^ :]*( |:)/) {
    s/ *Inductive *([^ :\[]*)( |:|\[).*/$1/;
   }
   print "$ident<DEFINITION uri=\"$_.ind$with_types\"/>\n";
  } elsif (/ *CoInductive /) {
   if (/ *CoInductive *[^ :]+ ([^ :]*) *:=/) {
    s/ *CoInductive *[^ :]+ ([^ :]*) *:=.*/$1/;
   } elsif (/ *CoInductive *[^ :]*( |:)/) {
    s/ *CoInductive *([^ :]*)( |:).*/$1/;
   }
   print "$ident<DEFINITION uri=\"$_.ind$with_types\"/>\n";
  } elsif (/^ *Fixpoint /) {
   s/ *Fixpoint *([^ \[]*)( |\[).*/$1/;
   print "$ident<DEFINITION uri=\"$_.con$with_types\"/>\n";
   $openfix = 1;
  } elsif (/ *CoFixpoint /) {
   s/ *CoFixpoint *([^ \[]*)( |\[).*/$1/;
   print "$ident<DEFINITION uri=\"$_.con$with_types\"/>\n";
   $openfix = 1;
  } elsif (/^ *Definition /) {
   s/ *Definition *([^ :]*)( |:)?.*/$1/;
   print "$ident<DEFINITION uri=\"$_.con$with_types\"/>\n";
  } elsif (/Local /) {
   s/ *Local *([^ :]*)( |:)?.*/$1/;
   print "$ident<DEFINITION uri=\"$_.con$with_types\"/>\n";
  } elsif (/Lemma /) {
   s/ *Lemma *([^ :]*)( |:)?.*/$1/;
   print "$ident<THEOREM id=\"id$cid\" uri=\"$_.con$with_types\"/>\n";
   $cid++;
  } elsif (/Theorem /) {
   s/ *Theorem *([^ :]+)( |:)?.*/$1/;
   print "$ident<THEOREM id=\"id$cid\" uri=\"$_.con$with_types\"/>\n";
   $cid++;
  } elsif (/Remark /) {
   s/ *Remark *([^ :]*)( |:)?.*/$1/;
   print "$ident<THEOREM id=\"id$cid\" uri=\"$_.con$with_types\"/>\n";
   $cid++;
  } elsif (/Scheme /) {
   s/ *Scheme *([^ :]*)( |:)?.*/$1/;
   print "$ident<THEOREM id=\"id$cid\" uri=\"$_.con$with_types\"/>\n";
   $cid++;
   $openscheme = 1;
  } elsif (/Save / && $opengoal) {
   s/ *Save *([^ \.]*)( |\.).*/$1/;
   print "$ident<THEOREM id=\"id$cid\" uri=\"$_.con$with_types\"/>\n";
   $cid++;
  } elsif (/with / && $openscheme) {
   s/ *with *([^ :]*)( |:).*/$1/;
   print "$ident<THEOREM id=\"id$cid\" uri=\"$_.con$with_types\"/>\n";
   $cid++;
  } elsif (/with / && $openfix) {
   s/ *with *([^ :]*)( |:).*/$1/;
   print "$ident<DEFINITION uri=\"$_.con$with_types\"/>\n";
   $cid++;
  } elsif (/Axiom /) {
   s/ *Axiom *([^ :]*)( |:).*/$1/;
   print "$ident<AXIOM id=\"id$cid\" uri=\"$_.con$with_types\"/>\n";
   $cid++;
  } elsif (/Parameter /) {
   s/ *Parameter *([^ :]*)( |:).*/$1/;
   print "$ident<AXIOM id=\"id$cid\" uri=\"$_.con$with_types\"/>\n";
   $cid++;
  } elsif (/Record /) {
   s/ *Record *([^ :]*)( |:).*/$1/;
   print "$ident<DEFINITION uri=\"$_.ind$with_types\"/>\n";
   $cid++;
  }

  if ($openscheme && (/\./)) {
   $openscheme = 0;
  } elsif ($openfix && (/\./)) {
   $openfix = 0;
  }

 }
}

print "</Theory>\n";
