#!/usr/local/bin/perl
# Danish (goes with Java, get it?)
# Tim Preston and 145 crew, 27 March 1998
# based on Daistish III++, Merlin P. D. Hughes, 8 June 1995
# $Id: da,v 1.2 1995/09/06 17:47:03 hughesm Exp hughesm $
require "ctime.pl";
&initialise;
&addTypes;
&processRCFile;
&processParameters;
&useFiles (@aliasFiles);
&readAlii;
&useFiles (@signatureFiles);
&readSignatures;
&useFiles (@vectorFiles);
&readVectors;
&useFiles ();
&checkVectors;
&useFiles (@axiomFiles);
&readAxia;
&useFiles ();
&checkAxia;
if ($verbose)
{
&reportParameters;
&reportAlii;
&reportSignatures;
&reportTypes;
&reportVectors;
&reportAxia;
}
&openOutput;
&outputVectors;
&outputDispensers;
&outputAxia;
&outputMain;
&closeOutput;
end;
# OUTPUT MODULE ---------------------------------------------------------------
sub outputMain # Java
# Output the mainline
{
local ($axiom);
print "// main code\n\n";
print " public static void main (String argv[]) {\n";
print " $DAVerb = ((argv.length > 0) && argv[0].equals( \"-verbose\"));";
print "\n\n";
foreach $axiom (@axia)
{
if ($web)
{
print " if ($DAVerb) System.out.print (\"<A NAME=fail$axiom>\");\n";
}
print " $DATest$axiom ();\n";
print " System.out.println ();\n";
}
print " System.out.println (\"Summary\");\n";
foreach $axiom (@axia)
{
print " System.out.print (\"Axiom `$axiom' tested \" + $DAn$axiom + \" times\");\n";
if ($web)
{
print " if ($DAf$axiom != 0) System.out.print (($DAVerb ? \", <A HREF=#fail$axiom>failed<\/A> \" : \", failed \") + $DAf$axiom + \" times\");\n";
}
else
{
print " if ($DAf$axiom != 0) System.out.print (\", failed \" + $DAf$axiom + \" times\");\n";
}
print " if ($DAa$axiom != 0) System.out.print (\", aborted \" + $DAa$axiom + \" times\");\n";
print " if ($DAg$axiom != 0) System.out.print (\", reneged \" + $DAg$axiom + \" times\");\n";
print " System.out.println (\".\");\n";
}
print " }\n\n}\n";
}
sub outputAxia # Java
# Output axiom code
{
local ($axiom, $var, $vars, $init, $result, $type, %globalVar);
print " // axiom code\n\n";
for $axiom (@axia)
{
local (@localVars, %localFrom, @counts, %counter, $count, %countOf, $numCt, $ctLoc);
$sp = " ";
($vars, $init, $result, $type, $lType, $rType) = &evalEx ($exParam {$axiom}, $axiom);
print " private static " . &deAlias ($lType) . " $DAl$axiom;\n";
print " private static " . &deAlias ($rType) . " $DAr$axiom;\n";
print " private static int $DAn$axiom = 0, $DAf$axiom = 0, $DAa$axiom = 0, $DAg$axiom = 0;\n";
for $var (@localVars)
{
$count = "$DAi" . $localFrom {$var};
push (@counts, $count) unless $counter {$count};
$counter {$count} = $localFrom {$var};
$countOf {$var} = $count;
if (!$globalVar {$var})
{
print " private static " . &deAlias ($varType {$localFrom{$var}}) . " $var;\n";
$globalVar{$var} = 1;
}
}
print "\n private static " . &deAlias ($type) . " $axiom () {\n";
print "$vars\n" if $vars ne "";
print "$init\n" if $init ne "";
print " return $result;\n }\n\n";
print " private static void $DATest$axiom () {\n";
print " int " . join (", ", @counts) . ";\n\n" if ($#counts >= 0);
$sp = " ";
for $count (@counts)
{
$var = $counter {$count};
$type = $varType {$var};
if ($web)
{
die "<FONT COLOR=\"#FF0022\">Fatal error<\/FONT> : No test vectors given for type `$type'!\n"
if (!$typeVectors {$type});
}
else
{
die "Fatal error : No test vectors given for type `$type'!\n"
if (!$typeVectors {$type});
}
}
if ($#counts < 0)
{
@counts = ("");
}
for $count (@counts)
{
if ($count ne "")
{
$var = $counter {$count};
$type = $varType {$var};
print "$sp for ($count = 0; $count < " . $typeVectors {$type} .
"; ++ $count) {\n";
$sp .= " ";
}
}
for $side ($DAl, $DAr)
{
local (@types, %doneType, $vector);
for $var (@localVars)
{
$type = $varType {$localFrom {$var}};
push (@types, $type) unless $doneType {$type};
$doneType {$type} = 1;
}
for $type (@types)
{
for $i (0 .. $typeVectors {$type} - 1)
{
$vector = $typeVector {$type, $i};
print "$sp $DAOnce$vector = false;\n" if ($vectorOnce {$vector});
}
}
for $var (@localVars)
{
if ($var =~ /^$side/)
{
$type = $varType {$localFrom {$var}};
$count = $countOf {$var};
print "$sp $var = $DADisp$type ($count);\n";
}
}
}
print "$sp ++ $DAn$axiom;\n";
print "$sp $DAAbrt = false;\n";
print "$sp $DARnig = false;\n";
print "$sp if (!$axiom ()) {\n";
print "$sp if ($DAAbrt) {\n";
print "$sp ++ $DAa$axiom;\n";
print "$sp System.out.println (\"counting REQ failure in $axiom\");\n";
print "$sp }\n";
print "$sp else if ($DARnig) {\n";
print "$sp ++ $DAg$axiom;\n";
print "$sp System.out.println (\"counting ENS failure in $axiom\");\n";
print "$sp }\n";
print "$sp else {\n";
print "$sp ++ $DAf$axiom;\n";
print "$sp if ($DAVerb) {\n";
print "$sp System.out.println (\"Axiom `$axiom' failed.\");\n";
print "$sp System.out.println (\" Test Vectors:\");\n";
for $count (@counts)
{
if ($count ne "")
{
$var = $counter {$count};
$type = $varType {$var};
print "$sp System.out.println (\" $var = \" + $DAName$type ($count));\n";
}
}
if ($func = $printOf {$lType})
{
print "$sp System.out.print (\" LHS: \");\n";
print $seFunc {$func} ? "$sp $DAl$axiom." . &deAlias ($func) . " ();\n" :
"$sp " . &deAlias ($func) . " ($DAl$axiom);\n";
print "$sp System.out.println ();\n";
}
if ($func = $printOf {$rType})
{
print "$sp System.out.print (\" RHS: \");\n";
print $seFunc {$func} ? "$sp $DAr$axiom." . &deAlias ($func) . " ();\n" :
"$sp " . &deAlias ($func) . " ($DAr$axiom);\n";
print "$sp System.out.println ();\n";
}
print "$sp }\n";
print "$sp }\n";
print "$sp }\n";
for $count (reverse @counts)
{
if ($count ne "")
{
chop $sp;
chop $sp;
print "$sp }\n";
}
if ($ctLoc eq $count)
{
chop $sp;
chop $sp;
}
}
print " }\n\n";
}
}
sub outputDispensers # Java
# Output vector dispenser code
# sets : %typeVectors {type} -- number of test vectors for a type
# %typeVector {type,n} -- test vectors for a type
{
local ($vector, $type, @vectorTypes, $n);
print " // dispenser code\n\n";
for $vector (@vectors)
{
$type = $vectorType {$vector};
push (@vectorTypes, $type) unless $typeVectors {$type} ++;
$typeVector {$type, $typeVectors {$type} - 1} = $vector;
}
for $type (@vectorTypes)
{
print " private static ".&deAlias ($type) . " $DADisp$type (int $DAi" . "n) {\n";
print " switch ($DAi" . "n) {\n";
$n = $typeVectors {$type};
for $i (0 .. $n - 1)
{
print " " . (($i == $n - 1) ? "default" : "case $i") .
" : return " . $typeVector {$type, $i} . " ();\n";
}
print " }\n }\n\n";
print " private static String $DAName$type (int $DAi" . "n) {\n";
print " switch ($DAi" . "n) {\n";
for $i (0 .. $n - 1)
{
print " " . (($i == $n - 1) ? "default" : "case $i") .
" : return \"" . $typeVector {$type, $i} . "\";\n";
}
print " }\n }\n\n";
}
}
sub outputVectors # Java
# Output vector code
{
local ($type, $vector, $vars, $init, $result);
print " // vector code\n\n";
for $vector (@vectors)
{
$type = &deAlias ($vectorType {$vector});
if ($vectorOnce {$vector})
{
print " private static boolean $DAOnce$vector = false;\n";
print " private static $type $DAGlob$vector;\n";
print " private static $type $vector () {\n";
print " if (!$DAOnce$vector) {\n";
print " $DAGlob$vector = $DAReal$vector ();\n";
print " $DAOnce$vector = true;\n";
print " }\n return $DAGlob$vector;\n }\n\n";
print " private static $type $DAReal$vector () {\n";
}
else
{
print " private static $type $vector () {\n";
}
$varNum = 0;
$sp = " ";
($vars, $init, $result) = &evalEx ($exParam {$vector});
print "$vars\n" if $vars ne "";
print "$init\n" if $init ne "";
print " return $result;\n }\n\n";
}
}
sub openOutput # Java
# Open output files
{
open (JFILE, ">$outputFile"); #must figure how to handle multiple java imports TP
select (JFILE);
print "/* Danish java code file\n";
&reportParameters;
print "*/\n\n";
for $i (@javaFiles)
{
$i =~ s/\.java$//;
#strip away directory name
$myind = rindex $i, "/";
$myi = substr $i, $myind + 1;
print "import " . $myi. ";" . "\n\n";
}
print "public class tester {\n\n";
print " protected static boolean $DAVerb;\n";
print " protected static boolean $DAAbrt;\n";
print " protected static boolean $DARnig;\n\n";
}
sub closeOutput # Java
# Close output files
{
select (STDOUT);
close (JFILE);
}
sub evalEx # Java
# Returns variables, processing and result to evaluate an expression
# This holds the majority of the Java specific work
# in : location, (? set $DAv,$DAl,$DAr variable || ? = axiom name)
# out : variables, init code, result, type, lrvars
{
local ($loc, $setVar, $value, $vars, $init, $result, $type, @lrVars, $temp, $count, $v, $i, $r, $l, $calc, $i0, $r0, $i1, $r1, $sig, $paramN) = @_;
$vars = "";
$init = "";
$result = "";
$type = "";
@lrVars = ();
$value = $exParam {$loc};
if ($value eq "(")
{
($vars, $init, $result, $type) = &evalEx ($exParam {"$loc.0"});
$result = "($result)";
}
elsif ($value eq "?")
{
($v, $i, $r) = &evalEx ($exParam {"$loc.0"});
$vars .= $v;
$init .= $i;
$l = $exParam {"$loc.1"}; # location of ':'
$sp .= " ";
($v, $i0, $r0) = &evalEx ($exParam {"$l.0"});
$vars .= $v;
($v, $i1, $r1, $type) = &evalEx ($exParam {"$l.1"});
$vars .= $v;
chop $sp;
chop $sp;
if (($i0 eq "") && ($i1 eq ""))
{
$result = "(($r) ? ($r0) : ($r1))";
}
else
{
$temp = "$DAt" . $varNum ++;
$vars .= " " . &deAlias ($type) . " $temp;\n";
$init .= "$sp if ($r) {\n$i0$sp $temp = $r0;\n$sp }\n";
$init .= "$sp else {\n$i1$sp $temp = $r1;\n$sp }\n";
$result = $temp;
}
}
elsif ($isInfix {$value})
{
$DAv = $DAl if $setVar;
$sig = $exParam {"$loc.s"};
($v, $i, $r, $type) = &evalEx ($exParam {"$loc.0"});
$vars .= $v;
$init .= $i;
if ($setVar)
{
$init .= "$sp $DAv$setVar = $r;\n";
$r = "$DAv$setVar";
push (@lrVars, $type);
}
$result = "($r " . &deAlias ($value);
$DAv = $DAr if $setVar;
($v, $i, $r, $type) = &evalEx ($exParam {"$loc.1"});
$vars .= $v;
$init .= $i;
if ($setVar)
{
$init .= "$sp $DAv$setVar = $r;\n";
$r = "$DAv$setVar";
push (@lrVars, $type);
}
$result .= " $r)";
$type = $funcType {$value, $sig};
}
elsif ($isFunc {$value})
{
$DAv = $DAl if $setVar;
$sig = $exParam {"$loc.s"};
if ($seFunc {$value, $sig})
{
$calc = "";
if ($funcSeParam {$value, $sig} < 0)
{
$temp = "$DAt" . $varNum ++;
$result = $temp;
$vars .= " " . &deAlias ($funcType {$value, $sig}) . " $temp;\n";
}
if ($exParam {"$loc.n"} >= 0)
{
$calc .= " (";
$count = 0;
for $paramN (0 .. $exParam {"$loc.n"} - 1)
{
($v, $i, $r, $type) = &evalEx ($exParam {"$loc.$paramN"});
$vars .= $v;
$init .= $i;
if ($setVar)
{
$init .= "$sp $DAv$setVar = $r;\n";
$r = "$DAv$setVar";
push (@lrVars, $type);
}
if ($paramN == $funcSeParam {$value, $sig})
{
if (&simpleVar ($r))
{
$result = $r;
}
else
{
$temp = "$DAt" . $varNum ++;
$result = $temp;
$vars .= " " . &deAlias ($funcType {$value, $sig}) . " $temp;\n";
$init .= "$sp $temp = $r;\n";
}
}
else
{
$calc .= ", " if $count ++;
$calc .= $r;
}
$DAv = $DAr if $setVar;
}
$calc .= ")";
}
$init .= "$sp $result." . &deAlias ($value) . "$calc;\n";
}
else
{
$result = &deAlias ($value);
if ($exParam {"$loc.n"} >= 0)
{
$result .= " (";
$count = 0;
for $paramN (0 .. $exParam {"$loc.n"} - 1)
{
if ($setVar && ($value eq "not")) # not at root
{
($v, $i, $r, $type, @lrVars) = &evalEx ($exParam {"$loc.$paramN"}, $setVar );
}
else
{
($v, $i, $r, $type) = &evalEx ($exParam {"$loc.$paramN"});
}
$vars .= $v;
$init .= $i;
if ($setVar && ($value ne "not")) # not at root
{
$init .= "$sp $DAv$setVar = $r;\n";
$r = "$DAv$setVar";
push (@lrVars, $type);
}
if ($paramN == $funcSeParam {$value, $sig})
{
# It may be worth assigning $r to a temp variable if it is non-simple.
$result = "($r).$result";
}
else
{
$result .= ", " if $count ++;
$result .= $r;
}
$DAv = $DAr if $setVar;
}
$result .= ")";
}
}
$type = $funcType {$value, $sig};
}
elsif ($isVector {$value})
{
$result = "$value ()";
$type = $vectorType {$value};
}
elsif ($isVar {$value})
{
$result = $exParam {"$loc'"} ? "$DAv" . $exParam {"$loc'"} . "_$value" : "$DAv$value";
$type = $varType {$value};
push (@localVars, $result) unless $localFrom {$result};
$localFrom {$result} = $value;
}
elsif ($isType {$value})
{
($v, $i, $result) = &evalEx ($exParam {"$loc.0"});
$vars .= $v;
$init .= $i;
}
elsif ($type = &constType ($value))
{
$result = $value;
}
else
{
&exitError ("Catastrophic eval failure with `$value' at `$loc'; contact the author.");
}
($vars, $init, $result, $type, @lrVars);
}
sub deAlias
# Return an unaliased alias if it is an alias
{
local ($i) = @_;
$isAlias {$i} ? $aliasOf {$i} : $i;
}
sub simpleVar
# Returns whether or not the parameter is a simple variable ($DAt\d+)
# in : exp
# out : true/false
{
local ($i) = @_;
return ($i =~ /^[a-zA-Z_][a-zA-Z0-9_]*$/);
}
sub reportAxia
# Reports current axia
{
local ($axiom);
print "Axia : " . join (", ", @axia) . "\n";
foreach $axiom (@axia)
{
print " " . $axiom . " " . &exReport ($exParam {$axiom}) . "\n";
}
}
sub reportVectors
# Reports current vectors
{
local ($vector);
print "Vectors : " . join (", ", @vectors) . "\n";
foreach $vector (@vectors)
{
print " " . $vectorType {$vector} . " " . $vector . " " . &exReport ($exParam {$vector}) . "\n";
}
}
sub reportSignatures
# Reports current signatures
{
local ($sig, $func, $type, $p0, $p1);
print "Signatures : " . join (", ", sort @funcs) . "\n";
foreach $func (sort @funcs)
{
foreach $sig (split (/;/, $funcSigs {$func}))
{
$type = $funcType {$func, $sig};
print $seFunc {$func, $sig} ? " {$type} $func " : " $type $func ";
print &signatureOf ($sig, $funcSeParam {$func, $sig}) . "\n";
}
}
foreach $func (@infex)
{
foreach $sig (split (/;/, $funcSigs {$func}))
{
($p0, $p1) = split (/,/, $sig);
print " " . $funcType {$func, $sig} . " $p0 $func $p1)\n";
}
}
}
sub reportTypes
# Reports current types
{
local ($type, $print);
print "Types : " . join (", ", sort @types) . "\n";
foreach $type (sort @types)
{
$print = $printOf {$type};
print " $type : " . ($seFunc {$print} ? "{$print}" : $print) . "\n"
if $print;
}
}
sub reportParameters
# Reports parameters
{
print "Output : " . $outputFile . "\n";
print "Java code : " . join (",", @javaFiles) . "\n";
print "Alii : " . join (",", @aliasFiles) . "\n";
print "Signatures : " . join (",", @signatureFiles) . "\n";
print "Test Vectors : " . join (",", @vectorFiles) . "\n";
print "Axia : " . join (",", @axiomFiles) . "\n";
}
sub reportAlii
# Reports current alii
{
print "Aliases : " . join (", ", sort @alii) . "\n";
foreach $alias (sort @alii)
{
print " " . $alias . " ";
print ($isAlias {$alias} ? "=" : "#");
print " " . $aliasOf {$alias} . "\n";
}
}
sub syntaxError
# Reports syntax error and exits
{
die "Syntax: danish {-o