-#!/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";