#!/usr/bin/perl
#
my %env=(vocabularies,'',notations,'',definitions,'',theorems,'',schemes,'',registrations,'',constructors,'',requirements,'');
#my $tosort='notations'.'definitions';
my $tosort='notations';

sub Dumpevd()
{
    my @lar = ();
    open (LAR, "< $ARGV[1]");
    while (<LAR>)
    {
	$l=$_;
	@lar=(@lar,$l);
    }
    close LAR;

    open (EVD,"> $a.evd");
    print EVD "environ\n\n";
    foreach my $key (vocabularies,notations,constructors,registrations,requirements,definitions,theorems,schemes)
    {
	if ($_[0]{$key}) 
	{
	    my $line = " $key ";
	    my @br = split /,/,$_[0]{$key};
	    my @ts = ();
	    my $i=index ($tosort, $key);
	    if ( $i != -1)
	    {
		my $l=@lar;
		$m=@br;
		for ($j=0;$j<$m;$j++)
		{
		    if ('tarski' eq lc($br[$j]))
		    {
			@ts=(@ts,'TARSKI');
		    }
		}
		for ($i=0;$i<$l;$i++)
		{
		    for ($j=0;$j<$m;$j++)
		    {
			my $lar1=$lar[$i];
			$lar1=~s/\n//;
			if ($lar1 eq lc($br[$j]))
			{
			    @ts=(@ts,$br[$j]);
			}
		    }
		}
		@br=@ts;
	    } 
	    $line = $line.$br[0];
	    for ($i=1;$i<=$#br;$i++)
	    {
		if ((length($line)+3+length($br[$i]))<=79)
		{
		    $line = $line.", $br[$i]";
		}
		else
		{
		    print EVD "$line,\n";
		    $line="      $br[$i]";
		}
	    }
	    print EVD "$line;\n";	
	}
    }
    print EVD "\n";
    close EVD;
}

sub Extractcomments()
{
    open(MIZ,"< $a.miz"); 
    open(CMM,"> $a.cmm"); 
    my $e;
    while (<MIZ>)
    {   
	$e=$_;
	my $i=index($e,'begin');
	my $j=index($e,'::');
	if ($i != -1 && ($j == -1 || $j>$i)) {last;}
	if ($j != -1) {print CMM substr($e,$j);}
    }
    print CMM "\n";
    close MIZ;
    close CMM;
}

sub Extractenvironment()
{
    open(MIZ,"< $a.miz"); 
    my $e;
    my $l;
    while (<MIZ>)
    {
	$l=$_;
	$l=~s/::.*//g;
	$e=$e.$l;
    }   
    close MIZ;
    $e =~ s/\s//g;
    $e =~ s/begin.*//g;
    $e =~ s/^.*environ//g;
    my @dirs=split /;/,$e;
    for ($i=0;$i<=$#dirs;$i++)
    {
	my $dir = $dirs[$i];
	$dir =~ /([a-z]+)/;
	my $d = $1;
	$dir =~ /([^a-z]+$)/;
       	$env{$d}=$env{$d}.",$1";
	$env{$d} =~ s/^,//g;	      
    }
}

sub Extractarticle()
{
    open(MIZ,"< $a.miz"); 
    open(TMP,"> $a.tmp"); 
    my $e;
    my $f=0;
    while (<MIZ>)
    {   
	$e=$_;
	my $i=index($e,'begin');
	my $j=index($e,'::');
	if ($i != -1 && ($j == -1 || $j>$i)) {$f=1;}
	if ($f == 1) {print TMP $e;}
    }
    close MIZ;
    close TMP;
}

sub Usage()
{
    print "This script sorts certain environment directives in a Mizar article according to a given list.\n";
    print "Usage: \t./newevd.pl <mizar-article-name> <article-list-file>\n";
    print "Note : \t<mizar-article-name> must be a valid Mizar article name (with '.miz' extension).\n\n";
    exit 1;
}

$a=$ARGV[0];
if ($a eq '' || $ARGV[1] eq '') {&Usage;}
if (substr($a,length($a)-4) ne '.miz') {&Usage;}
$a=~s/\.miz$//;
&Extractcomments;
&Extractenvironment;
&Dumpevd(\%env);
&Extractarticle;
`cat $a.cmm $a.evd $a.tmp > $a.miz`;