helm/EXPORT/mktheory.pl

   1 #!/usr/bin/perl
   2
   3 # Assumptions:
   4 #  Comments on one line are stripped
   5 #  Comments on many lines:
   6 #   nothing after *) (end of command)
   7 #  Commands could be nested (but see previous assumption)
   8 #  Commands don't span on several lines
   9 #  If a line is commented, the comment must begin at the begin of line and end
  10 #   at the end of line
  11 #  In a line, before a command only spaces are allowed
  12
  13 $curi = $ARGV[0];
  14 $with_types = ($ARGV[1] ? ".types" : "");
  15 $ident = " ";
  16 $cid = 1;
  17 $opencom = 0;
  18 $openscheme = 0;
  19 $openfix = 0;
  20 $opengoal = 0;
  21
  22 print <<EOT;
  23 <?xml version="1.0" encoding="ISO-8859-1"?>
  24 <!DOCTYPE Theory SYSTEM "http://localhost:8081/getdtd?uri=maththeory.dtd">
  25
  26 <Theory uri="cic:/$curi">
  27 EOT
  28
  29 while (<STDIN>) {
  30  chomp;
  31  if ($opencom > 0) {
  32   $opencom-- if (/\*\)/ && !/\(\*.*\*\)/);
  33  } else {
  34   if (/\(\*.*\*\)/) { # (* comment *)
  35    s/\(\*.*\*\)//;
  36   } elsif (/\(\*/) {
  37    # (* comment
  38    $opencom++;
  39    $_ = "";
  40   }
  41
  42   if (/Require /) {
  43    s/ *Require *(.*)\..*/$1/;
  44    print "$ident<!-- Require $_ -->\n";
  45   } elsif (/Goal /) {
  46    $opengoal = 1;
  47   } elsif (/Section /) {
  48    s/ *Section *(.*)\..*/$1/;
  49    print "$ident<SECTION uri=\"$1\">\n";
  50    $ident = $ident." ";
  51   } elsif (/Chapter /) {
  52    s/ *Chapter *(.*)\..*/$1/;
  53    print "$ident<SECTION uri=\"$1\">\n";
  54    $ident = $ident." ";
  55   } elsif (/End /) {
  56    chop($ident);
  57    print "$ident</SECTION>\n";
  58   } elsif (/Variable(s?) /) {
  59    s/ *Variable(s?) *([^:]*):.*/$2/;
  60    s/ //g;
  61    @vl = split /,/;
  62    foreach (@vl) {
  63     print "$ident<VARIABLE uri=\"$_.var$with_types\"/>\n";
  64    }
  65   } elsif (/Hypothesis /) {
  66    s/ *Hypothesis *([^ :]*)( |:).*/$1/;
  67    @vl = split /,/;
  68    foreach (@vl) {
  69     print "$ident<VARIABLE uri=\"$_.var$with_types\"/>\n";
  70    }
  71   } elsif (/^ *Inductive /) {
  72    if (/ *Inductive *[^ :]+ ([^ :]*) :=/) {
  73     s/ *Inductive *[^ :]+ ([^ :]*) *:=.*/$1/;
  74    } elsif (/ *Inductive *[^ :]*( |:)/) {
  75     s/ *Inductive *([^ :\[]*)( |:|\[).*/$1/;
  76    }
  77    print "$ident<DEFINITION uri=\"$_.ind$with_types\"/>\n";
  78   } elsif (/ *CoInductive /) {
  79    if (/ *CoInductive *[^ :]+ ([^ :]*) *:=/) {
  80     s/ *CoInductive *[^ :]+ ([^ :]*) *:=.*/$1/;
  81    } elsif (/ *CoInductive *[^ :]*( |:)/) {
  82     s/ *CoInductive *([^ :]*)( |:).*/$1/;
  83    }
  84    print "$ident<DEFINITION uri=\"$_.ind$with_types\"/>\n";
  85   } elsif (/^ *Fixpoint /) {
  86    s/ *Fixpoint *([^ \[]*)( |\[).*/$1/;
  87    print "$ident<DEFINITION uri=\"$_.con$with_types\"/>\n";
  88    $openfix = 1;
  89   } elsif (/ *CoFixpoint /) {
  90    s/ *CoFixpoint *([^ \[]*)( |\[).*/$1/;
  91    print "$ident<DEFINITION uri=\"$_.con$with_types\"/>\n";
  92    $openfix = 1;
  93   } elsif (/^ *Definition /) {
  94    s/ *Definition *([^ :]*)( |:)?.*/$1/;
  95    print "$ident<DEFINITION uri=\"$_.con$with_types\"/>\n";
  96   } elsif (/Local /) {
  97    s/ *Local *([^ :]*)( |:)?.*/$1/;
  98    print "$ident<DEFINITION uri=\"$_.con$with_types\"/>\n";
  99   } elsif (/Lemma /) {
 100    s/ *Lemma *([^ :]*)( |:)?.*/$1/;
 101    print "$ident<THEOREM id=\"id$cid\" uri=\"$_.con$with_types\"/>\n";
 102    $cid++;
 103   } elsif (/Theorem /) {
 104    s/ *Theorem *([^ :]+)( |:)?.*/$1/;
 105    print "$ident<THEOREM id=\"id$cid\" uri=\"$_.con$with_types\"/>\n";
 106    $cid++;
 107   } elsif (/Remark /) {
 108    s/ *Remark *([^ :]*)( |:)?.*/$1/;
 109    print "$ident<THEOREM id=\"id$cid\" uri=\"$_.con$with_types\"/>\n";
 110    $cid++;
 111   } elsif (/Scheme /) {
 112    s/ *Scheme *([^ :]*)( |:)?.*/$1/;
 113    print "$ident<THEOREM id=\"id$cid\" uri=\"$_.con$with_types\"/>\n";
 114    $cid++;
 115    $openscheme = 1;
 116   } elsif (/Save / && $opengoal) {
 117    s/ *Save *([^ \.]*)( |\.).*/$1/;
 118    print "$ident<THEOREM id=\"id$cid\" uri=\"$_.con$with_types\"/>\n";
 119    $cid++;
 120   } elsif (/with / && $openscheme) {
 121    s/ *with *([^ :]*)( |:).*/$1/;
 122    print "$ident<THEOREM id=\"id$cid\" uri=\"$_.con$with_types\"/>\n";
 123    $cid++;
 124   } elsif (/with / && $openfix) {
 125    s/ *with *([^ :]*)( |:).*/$1/;
 126    print "$ident<DEFINITION uri=\"$_.con$with_types\"/>\n";
 127    $cid++;
 128   } elsif (/Axiom /) {
 129    s/ *Axiom *([^ :]*)( |:).*/$1/;
 130    print "$ident<AXIOM id=\"id$cid\" uri=\"$_.con$with_types\"/>\n";
 131    $cid++;
 132   } elsif (/Parameter /) {
 133    s/ *Parameter *([^ :]*)( |:).*/$1/;
 134    print "$ident<AXIOM id=\"id$cid\" uri=\"$_.con$with_types\"/>\n";
 135    $cid++;
 136   } elsif (/Record /) {
 137    s/ *Record *([^ :]*)( |:).*/$1/;
 138    print "$ident<DEFINITION uri=\"$_.ind$with_types\"/>\n";
 139    $cid++;
 140   }
 141
 142   if ($openscheme && (/\./)) {
 143    $openscheme = 0;
 144   } elsif ($openfix && (/\./)) {
 145    $openfix = 0;
 146   }
 147
 148  }
 149 }
 150
 151 print "</Theory>\n";