#!/usr/bin/perl
#
sub Usage()
{
    print "This script extracts dependencies from environment directives in a Mizar article\n";
    print "and sorts them according to a given list.\n";
    print "Usage: \t./makeenv.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 Dumpevd()
{
    my @lar = ();
    open (LAR, "< $ARGV[1]");
    while (<LAR>)
    {
	$l=$_;
	@lar=(@lar,$l);
    }
    close LAR;
    @lar=('tarski_0','tarski_a',@lar);
    my $b=$a;
    $b=~s/^.*\///;
    print "$b.an: ";
    my @ts=();
    my @br=();
    foreach my $key (notations,constructors,registrations,requirements,definitions,equalities,expansions,theorems,schemes)
    {
	if ($_[0]{$key}) 
	{
	    @br = split /,/,$_[0]{$key};
	    push(@ts,@br);
        }
    }
    my %work;
    @work{@ts}=undef;
    @ts=sort keys %work;
    my $l=@lar;
    my $m=@ts;
    for ($i=0;$i<$l;$i++)
    {
	my $b=0;
	for ($j=0;$j<$m;$j++)
	{
	    my $lar1=$lar[$i];
	    $lar1=~s/\n//;
	    if ($lar1 eq lc($ts[$j]))
	    {
		print "$lar1.an ";
		$b++;
		break;
	    }
        }
        if ($b==$m) { break; }
    }
    print "\n";
}

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

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

&Extractenvironment;
&Dumpevd(\%env);
