Many files added. Symbolic links missing. examples and contrib missing due

[helm.git] / helm / EXPORT / mktheory.pl

diff --git a/helm/EXPORT/mktheory.pl b/helm/EXPORT/mktheory.pl
new file mode 100755 (executable)
index 0000000..2be018e
--- /dev/null
+++ b/helm/EXPORT/mktheory.pl
@@ -0,0 +1,151 @@
+#!/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";