#!/usr/bin/perl
#
sub Usage()
{
    print "This script displays the last Mizar article that a given article depends on according to a given list.\n";
    print "Usage: \t./lastenv.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;
}

my %env=(vocabularies,'',notations,'',constructors,'',registrations,'',requirements,'',definitions,'',equalities,'',expansions,'',theorems,'',schemes,'');

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

    my $z=0;
    my $last='';
    foreach my $key (notations,registrations,requirements,definitions,equalities,expansions,constructors,theorems,schemes)
    {
        my @br = split /,/,$_[0]{$key};
        my @ts = ();
    	my $l=@lar;
	$m=@br;
	for ($i=$z;$i<$l;$i++)
	{
	    for ($j=0;$j<$m;$j++)
	    {
		my $lar1=$lar[$i];
		$lar1=~s/\n//;
		if ($lar1 eq lc($br[$j]))
		{
		    $last=$br[$j];
		    $z=$i;
    		}
	    }
	}
    }
    print "$last\n"; 
}

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;
}

$a=$ARGV[0];
if ($a eq '' || $ARGV[1] eq '') {&Usage;}
if (substr($a,length($a)-4) ne '.miz') {&Usage;}
$a=~s/\.miz$//;
&Extractcomments;
&Extractenvironment;
&DumpLast(\%env);
