]> matita.cs.unibo.it Git - helm.git/blob - helm/EXPORT/mktheory.pl
basic_rg: reduction was not tail recursive by mistake
[helm.git] / 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";