This commit was manufactured by cvs2svn to create branch 'moogle'.

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

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