#!/usr/local/bin/perl

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

sub outputMain			# C++
  # Output the mainline
{
  local ($axiom);

  print "// main code\n\n";
  print HFILE "// main header\n\n";
  print HFILE "extern int DA_fd[2];\n";
  print HFILE "extern int $DAVerb, $DAAbrt, $DARnig;\n";

  print "int DA_fd[2];\n";
  print "int $DAVerb, $DAAbrt, $DARnig;\n\n";
  print "int main (int argc, char **argv)\n{\n";
  print "  $DAVerb = (argc > 1) && !strcmp (argv[1], \"-verbose\");\n";
  print "  pipe (DA_fd);\n";

  foreach $axiom (@axia)
  {
    print "  cout << \"Testing `$axiom'..\" << flush;\n";
    print "  $DATest$axiom ();\n";
    print "  cout << endl;\n";
  }

  print "  cout << \"\nSummary\n\n\"; \n";
  foreach $axiom (@axia)
  {
    print "  cout << \"Axiom `$axiom' tested \" << $DAn$axiom << \" times\";\n";
    print "  if ($DAf$axiom) cout << \", failed \" << $DAf$axiom << \" times\";\n";
    print "  if ($DAa$axiom) cout << \", aborted \" << $DAa$axiom << \" times\";\n";
    print "  if ($DAg$axiom) cout << \", reneged \" << $DAg$axiom << \" times\";\n";
    print "  cout << \".\" << endl;\n";
  }

  print "  exit (0);\n";
  print "}\n";
}
  
sub outputAxia			# C++
  # Output axiom code
{
  local ($axiom, $var, $vars, $init, $result, $type, %globalVar);

  print "// axiom code\n\n";
  print HFILE "// axiom header\n\n";

  for $axiom (@axia)
  {
    local (@localVars, %localFrom, @counts, %counter, $count, %countOf, $numCt, $ctLoc);

    ($vars, $init, $result, $type, $lType, $rType) = &evalEx ($exParam {$axiom}, $axiom);
    print HFILE &deAlias ($type) . " $axiom (void);\n";
    print HFILE &deAlias ($lType) . " $DAl$axiom;\n";
    print HFILE &deAlias ($rType) . " $DAr$axiom;\n";
    print "int $DAn$axiom = 0, $DAf$axiom = 0, $DAa$axiom = 0, $DAg$axiom = 0;\n\n";
    print &deAlias ($type) . " $axiom (void)\n{\n";
    print "$vars\n" if $vars ne "";
    print "$init\n" if $init ne "";
    print "  return $result;\n}\n\n";
    print HFILE "void $DATest$axiom (void);\n";
    print "void $DATest$axiom (void)\n{\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 HFILE &deAlias ($varType {$localFrom{$var}}) . " $var;\n";
	$globalVar{$var} = 1;
      }
    }
    print "  int DA_pid;\n";
    print "  int " . join (", ", @counts) . ";\n\n" if ($#counts >= 0);
    $sp = " ";
    $numCt = 1;
    for $count (@counts)
    {
      $var = $counter {$count};
      $type = $varType {$var};
      die "Fatal error : No test vectors given for type `$type'!\n"
	if (!$typeVectors {$type});
      $numCt *= $typeVectors {$type};
    }
    if ($#counts < 0)
    {
      @counts = ("");
    }
    for $count (@counts)
    {
      if (($numCt > 0) && ($numCt <= $threshold))
      {
	$ctLoc = $count;
	print "$sp if ((DA_pid = fork ()) != 0)\n$sp {\n";
	print "$sp   if (DA_pid == -1)\n$sp     cerr << \"fork failed.\" << endl;\n";
	print "$sp   else\n$sp   {\n";
	print "$sp     read (DA_fd[0], &$DAn$axiom, sizeof (int));\n";
	print "$sp     read (DA_fd[0], &$DAa$axiom, sizeof (int));\n";
	print "$sp     read (DA_fd[0], &$DAg$axiom, sizeof (int));\n";
	print "$sp     read (DA_fd[0], &$DAf$axiom, sizeof (int));\n";
        print "$sp     wait (NULL);\n";
	print "$sp     cerr << '.' << $DAn$axiom << flush;\n";
	print "$sp   }\n$sp }\n$sp else\n$sp {\n";
	$numCt = 0;
	$sp .= "  ";
      }
      if ($count ne "")
      {
	$var = $counter {$count};
	$type = $varType {$var};
	print "$sp for ($count = 0; $count < " . $typeVectors {$type} .
	  "; ++ $count)\n$sp {\n";
	$sp .= "  ";
	$numCt /= $typeVectors {$type};
      }
    }
    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 = 0;\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 = 0;\n";
    print "$sp $DARnig = 0;\n";
    print "$sp if (!$axiom ())\n";
    print "$sp {\n";
    print "$sp   if ($DAAbrt) {\n";
    print "$sp     ++ $DAa$axiom;\n";
    print "$sp     cout << \"counting REQ failure in $axiom\" << endl;\n";
    print "$sp   }\n";
    print "$sp   else if ($DARnig) {\n";
    print "$sp     ++ $DAg$axiom;\n";
    print "$sp     cout << \"counting ENS failure in $axiom\" << endl;\n";
    print "$sp   }\n";
    print "$sp   else\n";
    print "$sp   {\n";
    print "$sp     ++ $DAf$axiom;\n";
    print "$sp     if ($DAVerb)\n";
    print "$sp     {\n";
    print "$sp       cout << \"Axiom `$axiom' failed.\" << endl << \" Test Vectors:\" << endl;\n";
    for $count (@counts)
    {
      if ($count ne "")
      {
	$var = $counter {$count};
	$type = $varType {$var};
	print "$sp       cout << \"  $var = \" << $DAName$type ($count) << endl;\n";
      }
    }
    if ($func = $printOf {$lType})
    {
      print "$sp       cout << \" LHS: \";\n";
      print $seFunc {$func} ? "$sp       $DAl$axiom->" . &deAlias ($func) . " ();\n" :
        "$sp       " . &deAlias ($func) . " ($DAl$axiom);\n";
      print "$sp       cout << endl;\n";
    }
    if ($func = $printOf {$rType})
    {
      print "$sp       cout << \" RHS: \";\n";
      print $seFunc {$func} ? "$sp       $DAr$axiom->" . &deAlias ($func) . " ();\n" :
        "$sp       " . &deAlias ($func) . " ($DAr$axiom);\n";
      print "$sp       cout << endl;\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)
      {
	print "$sp write (DA_fd[1], &$DAn$axiom, sizeof (int));\n";
	print "$sp write (DA_fd[1], &$DAa$axiom, sizeof (int));\n";
	print "$sp write (DA_fd[1], &$DAg$axiom, sizeof (int));\n";
	print "$sp write (DA_fd[1], &$DAf$axiom, sizeof (int));\n";
	print "$sp exit (0);\n";
	chop $sp;
	chop $sp;
	print "$sp }\n";
      }
    }
    print "}\n\n";
  }
  print HFILE "\n";
}

sub outputDispensers		# C++
  # 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";
  print HFILE "// dispenser header\n\n";

  for $vector (@vectors)
  {
    $type = $vectorType {$vector};
    push (@vectorTypes, $type) unless $typeVectors {$type} ++;
    $typeVector {$type, $typeVectors {$type} - 1} = $vector;
  }
  for $type (@vectorTypes)
  {
    print HFILE &deAlias ($type) . " $DADisp$type (int);\n";
    print HFILE "char *$DAName$type (int);\n";

    print &deAlias ($type) . " $DADisp$type (int $DAi" . "n)\n{\n";
    print "  switch ($DAi" . "n)\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 "char *$DAName$type (int $DAi" . "n)\n{\n";
    print "  switch ($DAi" . "n)\n  {\n";
    for $i (0 .. $n - 1)
    {
      print "    " . (($i == $n - 1) ? "default" : "case $i") .
	" : return \"" . $typeVector {$type, $i} . "\";\n";
    }
    print "  }\n}\n\n";
  }
  print HFILE "\n";
}

sub outputVectors		# C++
  # Output vector code
{
  local ($type, $vector, $vars, $init, $result);

  print "// vector code\n\n";
  print HFILE "// vector header\n\n";

  for $vector (@vectors)
  {
    $type = &deAlias ($vectorType {$vector});
    if ($vectorOnce {$vector})
    {
      print HFILE "$type $vector (void);\n";
      print HFILE "$type $DAReal$vector (void);\n";
      print HFILE "$type $DAGlob$vector;\n";
      print HFILE "int $DAOnce$vector;\n";
      print "$type $vector (void)\n{\n" .
	"  if (!$DAOnce$vector)\n  {\n    $DAGlob$vector = $DAReal$vector ();\n" .
	  "    $DAOnce$vector = 1;\n  }\n  return $DAGlob$vector;\n}\n\n" .
	    "$type $DAReal$vector (void)\n";
    }
    else
    {
      print HFILE "$type $vector (void);\n";
      print "$type $vector (void)\n";
    }
    $varNum = 0;
    $sp = " ";
    ($vars, $init, $result) = &evalEx ($exParam {$vector});
    print "{\n";
    print "$vars\n" if $vars ne "";
    print "$init\n" if $init ne "";
    print "  return $result;\n}\n\n";
  }

  print HFILE "\n";
}

sub openOutput			# C++
  # Open output files
{
  open (CFILE, ">$outputFile");
  $headerFile = $outputFile;
  $headerFile =~ s/\.cc$/.hh/;
  $headerFile =~ s/\.C$/.H/;
  $headerFile =~ s/\.c$/.h/;
  open (HFILE, ">$headerFile");
  select (HFILE);
  print "/* Daistish C++ header file\n";
  &reportParameters;
  print "*/\n\n";
  print "#include <iostream.h>\n";
  print "#include <stdlib.h>\n";
  print "#include <unistd.h>\n";
  print "#include <sys/wait.h>\n";
  for $i (@includeFiles)
  {
    print '#include "' . $i. '"' . "\n";
  }
  print "\n";
  select (CFILE);
  print "/* Daistish C++ code file\n";
  &reportParameters;
  print "*/\n\n";
  print '#include "' . $headerFile. '"' . "\n\n";
}

sub closeOutput			# C++
  # Close output files
{
  select (STDOUT);
  close (CFILE);
  close (HFILE);
}

sub deAlias
  # Return an unaliased alias if it is an alias
{
  local ($i) = @_;
  $isAlias {$i} ? $aliasOf {$i} : $i;
}

sub evalEx			# C++
  # Returns variables, processing and result to evaluate an expression
  # This holds the majority of the C++ 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$sp {\n$i0$sp   $temp = $r0;\n$sp }\n";
      $init .= "$sp else\n$sp {\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 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_]*$/);
}

###################################################
## Below here is all of the input-handling stuff ##
###################################################
##   Useful:
## @alii, %isAlias, %aliasOf
## @types, %isType
## @vectors, %isVector, %vectorType, %exParam, %vectorOnce
## @funcs, %isFunc, %seFunc, %funcType, %funcSeParam, %funcSigs
## %printOf
## @infix, %isInfix
## @vars, %isVar, %axiomVars, %varType
## &constType
## @axia, %isAxiom, %exParam
###################################################

sub addTypes			# C++
  # Add basic types
  #   set @types, %isType, @alii, %isAlias, %aliasOf, %isFunc, @funcs, %seFunc,
  #     %funcType, %funcSeParam, %funcParams{name}, @infix, %isInfix, $infixSearch
{
  &typeAdd ("int");
  &typeAdd ("string");
  &typeAdd ("char");
  &typeAdd ("bool");
  &aliasAdd ("bool", "int");
  &aliasAdd ("string", "char *");
  &constAdd ("true", "bool", "1");
  &constAdd ("false", "bool", "0");
  &func1Add ("not", "bool", "!", "bool");
  &fixIn ("bool", "*", "==", "!=", ">");
  &fixIn ("bool", "bool", "&&", "||", "^^");
  &fixIn ("int", "int", "+", "-", "*", "/", "%");
  &fixIn ("*", "*", "?", ":");	# The ternary operator is hard wired
  $infixSearch = "\\>\\!\\=\\&\\|\\+\\-\\*\\/\\?\\:\\^\\%"; # characters allowed in an infix op
}

sub typeAdd
  # Add types
  #   set @types, %isType
{
  local ($type) = @_;

  push (@types, $type);
  $isType {$type} = 1;
}

sub constAdd
  # Add zero parameter function with alias
  #   in : name, type, alias
  #   set @funcs, %isFunc, %funcType, %seFunc, %funcSeParam, %funcSigs
  #     @alii, %isAlias, %aliasOf
{
  local ($const, $type, $value, $sig) = @_;

  $sig = "!";
  push (@funcs, $const);
  $isFunc {$const} = 1;
  $funcSigs {$const} = $sig;
  $funcType {$const, $sig} = $type;
  $seFunc {$const, $sig} = 0;
  $funcSeParam {$const, $sig} = -1;
  push (@alii, $const);
  $isAlias {$const} = 1;
  $aliasOf {$const} = $value;
}

sub func1Add
  # Add one parameter function with alias
  #   in : name, type, alias, type
  #   set @funcs, %isFunc, %funcType, %seFunc, %funcSeParam, %funcSigs
  #     @alii, %isAlias, %aliasOf
{
  local ($func, $type, $alias, $param, $sig) = @_;

  $sig = "($param";
  push (@funcs, $func);
  $isFunc {$func} = 1;
  $funcSigs {$func} = $sig;
  $funcType {$func, $sig} = $type;
  $seFunc {$func, $sig} = 0;
  $funcSeParam {$func, $sig} = -1;
  push (@alii, $func);
  $isAlias {$func} = 1;
  $aliasOf {$func} = $alias;
}

sub aliasAdd
  # Add alias
  #   set @alii, %isAlias, %aliasOf
{
  local ($of, $is) = @_;

  push (@alii, $of);
  $isAlias {$of} = 1;
  $aliasOf {$of} = $is;
}

sub fixIn
  # Add infix functions
  #   set @infex, %funcType, %isInfix, %funcParam, %funcParams
{
  local ($type, $param, $func, $sig);

  $type = shift;
  $param = shift;
  $sig = "($param,$param";
  while ($func = shift)
  {
    $isInfix {$func} = 1;
    push (@infex, "$func");
    $funcType {$func, $sig} = $type;
    $seFunc {$func, $sig} = 0;
    $funcSeParam {$func, $sig} = -1;
    $funcSigs {$func} = $sig;
  }
}

sub constType			# C++
  # Return the type of a constant
  #   in : symbol
  #   out : constant type of symbol
{
  local ($const, $ret) = @_;
  $ret = "int" if $const =~ /^[0-9]+|-[0-9]+$/;
  $ret = "string" if $const =~ /^\"[^\"]*\"$/; # "
  $ret = "char" if $const =~ /^\'[^\']*\'$/;
  $ret;
}

sub readAxia
  # Read axioms
  #   sets : %isAxiom, @axia, $globAx, %exParam {name}
{
  local ($axiom, $axiomRoot, %primed);

  $currentTask = "Reading axia.";
  while (&nextSymbol)
  {
    &exitError ("Expecting an axiom name.") unless $axiom = &pullIdentifier;
    $currentObject = $axiom;
    &exitError ("Axiom name `$axiom' is already a type name.") if $isType {$axiom};
    &exitError ("Axiom name `$axiom' is already a function name.")
      if $isFunc {$axiom};
    &exitError ("Axiom name `$axiom' is already in use.") if $isAxiom {$axiom};
    &exitError ("Axiom name `$axiom' is already a vector name.") if $isVector {$axiom};
    &exitError ("Axiom name `$axiom' is already a variable name.") if $isVar {$axiom};
    $isAxiom {$axiom} = 1;
    push (@axia, $axiom);
    &nextSymbol;
    %primed = ();
    $exParam {$axiom} = &getEx ("A"); # expression is for an axiom
  }
  $currentObject = "";
  $currentTask = "";
}

sub checkAxia			# C++ - bool, ? :
  # Checks current axia for type, infix sanity
  #   sets : @vars, %isVar {var}, %varType {var}
{
  local ($axiom, $root, $loc, $func);

  $currentTask = "Checking axia.";

  foreach $i (@vars)
  {
    &exitError ("Type of variable `$i' not specified.")
      unless $varType {$i};
  }

  foreach $axiom (@axia)
  {
    $currentObject = "axiom `$axiom'";
    $loc = $root = $exParam {$axiom};
    $func = $exParam {$root};
    if ($func eq "not")		# not at root
    {
      $loc = $exParam {"$root.0"};
      $func = $exParam {$loc};
    }
    &exitError ("Root of axiom must be an optionally negated binary function.")
      unless (($isFunc {$func} && ($exParam {"$loc.n"} == 2)) ||
	      ($isInfix {$func} && ($func ne "?") && ($func ne ":")));
    &exitError ("Root of axiom must be a boolean function.")
      unless &axiomCheck ($axiom, $root) eq "bool";
  }
}

sub axiomCheck			# C++ - bool, ? :
  # Checks axiom for sanity
  #   in : axiom name, subaxiom location, desired type, ternary ':' acceptability
  #   out : type
  #   sets : $processing - set a variable type
{
  local ($axiom, $loc, $ternOk, $type, $looseType, $value, $paramN, @typeList, $sig, $funcSig) = @_;

  $value = $exParam {$loc};

  if ($value eq "(")
  {
    $type = &axiomCheck ($axiom, $exParam {"$loc.0"});
  }
  elsif ($value eq "?")
  {
    &exitError (&exReport ($exParam {$axiom}, $loc) .
		"\nCondition of ternary `?' must have type `bool'.")
      unless &axiomCheck ($axiom, $exParam {"$loc.0"}) eq "bool";
    &exitError (&exReport ($exParam {$axiom}, $loc) .
		"\nMissing ternary separator ':' following '?' operator.")
      unless $exParam {$exParam {"$loc.1"}} eq ":";
    $type = &axiomCheck ($axiom, $exParam {"$loc.1"}, 1);
  }
  elsif ($value eq ":")
  {
    &exitError (&exReport ($exParam {$axiom}, $loc) .
		"\nUnexpected ternary separator `:' encountered.") unless $ternOk;
    $type = &axiomCheck ($axiom, $exParam {"$loc.0"});
    $looseType = &axiomCheck ($axiom, $exParam {"$loc.1"});
    &exitError (&exReport ($exParam {$axiom}, $loc) .
	     "\nLHS (`$type') and RHS (`$looseType') of ternary `:' must have same types.")
      unless $looseType eq $type;
  }
  elsif ($isFunc {$value} || $isInfix {$value})
  {
    $sig = "!";
    if ($exParam {"$loc.n"} >= 0)
    {
      for $paramN (0 .. $exParam {"$loc.n"} - 1)
      {
        push (@typeList, &axiomCheck ($axiom, $exParam {"$loc.$paramN"}));
      }
      $sig = "(" . join (",", @typeList);
    }
    &exitError (&exReport ($exParam {$axiom}, $loc) .
	     "\nNo signature for function `$value' matches `" . &signatureOf ($sig) . "'.")
      unless $funcSig = &matchSig ($funcSigs {$value}, $sig);
    $type = $funcType {$value, $funcSig};
    $exParam {"$loc.s"} = $funcSig;
  }
  elsif ($isType {$value})
  {
    &axiomCheck ($axiom, $exParam {"$loc.0"});
    $type = $value;
  }
  elsif ($isVar {$value})
  {
    $type = $varType {$value};
  }
  else
  {
    &exitError (&exReport ($exParam {$axiom}, $loc) .
		"\naxiomCheck sanity error with `$value', contact the author!")
      unless ($type = &constType ($value));
  }

  $type;
}

sub reportAxia
  # Reports current axia
{
  local ($axiom);

  print "Axia : " . join (", ", @axia) . "\n";
  foreach $axiom (@axia)
  {
    print "  " . $axiom . " " . &exReport ($exParam {$axiom}) . "\n";
  }
}

sub readVectors
  # Read test vectors
  #   sets : %isVector, %vectorOnce, @vectors
  #     %exParam {name.0.1.2.3}
{
  local ($vector, $vectorOnce, $vectorRoot);

  $currentTask = "Reading vectors.";
  while (&nextSymbol)
  {
    $currentObject = "";
    &exitError ("Expecting a vector name.") unless $vector = &pullVectorName;
    $onceVector = $vector =~ s/^\{(.*)\}$/\1/;
    $currentObject = "`$vector'";
    &exitError ("Vector name `$vector' is already a function name.") if $isFunc {$vector};
    &exitError ("Vector name `$vector' is already a type name.") if $isType {$vector};
    &exitError ("Vector name `$vector' is already in use.") if $isVector {$vector};
    $isVector {$vector} = 1;
    $vectorOnce {$vector} = $onceVector;
    push (@vectors, $vector);
    &nextSymbol;
    $exParam {$vector} = &getEx ("V"); # expression is for a vector
  }
  $currentObject = "";
  $currentTask = "";
}

sub checkVectors
  # Checks all vector type sanities
  #   sets : %vectorType {name}
{
  local ($vector);

  $currentTask = "Checking vectors.";
  for $vector (@vectors)
  {
    &vectorCheck ($vector);
  }
  $currentObject = "";
  $currentTask = "";
}

sub vectorCheck
  # Checks vector type sanity
  #   in : vector name
  #   out : vector type
  #   sets : %vectorType {name}
  #     %vectorInUse {name} -- vector is in use
  #     %vectorDone {name} -- vector is done
{
  local ($vector, $type) = @_;

  if (!$vectorDone {$vector})
  {
    &exitError ("Vector `$vector' used recursively.") if ($vectorInUse {$vector});
    $vectorInUse {$vector} = 1;

    $currentObject = "test vector `$vector'";
    $vectorType {$vector} = &vectorParamCheck ($exParam {$vector});

    $vectorInUse {$vector} = 0;
    $vectorDone {$vector} = 1;
  }
  $vectorType {$vector};
}

sub vectorParamCheck
  # Checks type sanity of parameters within test vector
  #   in : vector parameter location (name.0.1.2)
  #   out : type at parameter location
{
  local ($place, $ternOk, $func, $type, $type2, $paramN, $save, $test) = @_;

  $func = $exParam {$place};
  if ($func eq "(")
  {
    $type = &vectorParamCheck ($exParam {"$place.0"});
  }
  elsif ($func eq "?")
  {
    $test = $exParam {"$place.0"};
    $type = &vectorParamCheck ($test);
    &exitError (&exReport ($exParam {$vector}, $test) .
		"\nType of `" . $exParam {$test} . "' ($type) does not match " .
		"boolean required by `?' operator.")
      unless ($type eq "bool");
    &exitError (&exReport ($exParam {$vector}, $exParam {"$place.1"}) .
		"\nMissing ternary separator `:' following `?' operator.")
      unless $exParam {$exParam {"$place.1"}} eq ":";
    $type = &vectorParamCheck ($exParam {"$place.1"}, 1);
  }
  elsif ($func eq ":")
  {
    &exitError (&exReport ($exParam {$vector}, $place) .
		"\nUnexpected ternary separator `:' encountered.") unless $ternOk;
    $type = &vectorParamCheck ($exParam {"$place.0"}, 1);
    $type2 = &vectorParamCheck ($exParam {"$place.1"}, 1);
    &exitError (&exReport ($exParam {$vector}, $place) .
		"\nType of RHS of `:' operator does not match type of LHS.")
      unless ($type eq $type2);
  }
  elsif ($isFunc {$func} || $isInfix {$func})
  {
    local (@typeList, $sig, $funcSig);
    
    $sig = "!";
    if ($exParam {"$place.n"} >= 0)
    {
      for $paramN (0 .. $exParam {"$place.n"} - 1)
      {
	$test = $exParam {"$place.$paramN"};
	push (@typeList, &vectorParamCheck ($test));
      }
      $sig = "(" . join (",", @typeList);
    }
    &exitError (&exReport ($exParam {$vector}, $place) .
		"\nNo signature for function `$func' matches `" . &signatureOf ($sig) . "'.")
      unless $funcSig = &matchSig ($funcSigs {$func}, $sig);
    $type = $funcType {$func, $funcSig};
    $exParam {"$place.s"} = $funcSig;
  }
  elsif ($isVector {$func})
  {
    $save = $currentObject;
    $type = &vectorCheck ($func);
    $currentObject = $save;
  }
  elsif ($isType {$func})
  {
    &vectorParamCheck ($exParam {"$place.0"});
    $type = $func;
  }
  else
  {
    &exitError ("Unknown variable `$func' used in test vector.")
      unless $type = &constType ($func);
  }

  $type;
}

sub reportVectors
  # Reports current vectors
{
  local ($vector);

  print "Vectors : " . join (", ", @vectors) . "\n";
  foreach $vector (@vectors)
  {
    print "  " . $vectorType {$vector} . " " . $vector . " " . &exReport ($exParam {$vector}) . "\n";
  }
}

sub getEx
  # Reads an expression
  #   in : type; "A" = axiom, "V" = vector
  #   out : root location
  #   sets : $globAx, %exParam {loc}
{
  local ($ex, $loc, $inLoc, $value, $paramN, $inFunc, $type, $prime) = @_;

  $loc = $globAx ++;

  if (s/^\(//)
  {
    $exParam {$loc} = "(";
    &nextSymbol;
    $exParam {"$loc.0"} = &getEx ($ex);
    &nextSymbol;
    &exitError ("Missing closing parenthesis.") unless s/^\)//;
  }
  else
  {
    &exitError ("Expecting an expression.") unless ($value = &pullSymbol) ne "";
    &exitError ("Not expecting an axiom name (`$value') here.") if $isAxiom {$value};
    &exitError ("Not expecting a vector name (`$value') here.")
      if ($ex eq "A") && $isVector {$value};
    $exParam {$loc} = $value;
    if ($isFunc {$value})
    {
      $paramN = -1;
      &nextSymbol;
      if (s/^\(//)
      {
	&nextSymbol;
	$paramN = 0;
	while (!/^\)/)
	{
	  if ($paramN > 0)
	  {
	    &exitError ("Missing parameter-separating comma.") unless s/^,//;
	    &nextSymbol;
	  }
	  $exParam {"$loc.$paramN"} = &getEx ($ex);
	  &nextSymbol;
	  ++ $paramN;
	}
	&exitError ("Missing closing parenthesis.") unless s/^\)//;
      }
      $exParam {"$loc.n"} = $paramN;
    }
    elsif ($isType {$value})
    {
      &nextSymbol;
      if (s/^\(//)
      {
	&nextSymbol;
	$exParam {"$loc.0"} = &getEx ($ex);
	&nextSymbol;
	&exitError ("Missing closing parenthesis.") unless s/^\)//;
      }
      else
      {
	&exitError ("Not expecting a type specification (`$value') here.") if ($ex eq "V");
	$type = $value;
	&exitError ("Expecting a variable name for type specification.") unless $value = &pullIdentifier;
	&exitError ("Not expecting an axiom name (`$value') here.") if $isAxiom {$value};
	&exitError ("Not expecting a vector name (`$value') here.") if $isVector {$value};
	&exitError ("Not expecting a function name (`$value') here.") if $isFunc {$value};
	&exitError ("Not expecting a type name (`$value') here.") if $isType {$value};
	push (@vars, $value) unless $isVar {$value};
	$isVar {$value} = 1;
	&exitError ("Conflicting type `$type' for variable `$value', was " .
		    $varType {$value} . ".")
	  if $varType {$value} && ($varType {$value} ne $type);
	$varType {$value} = $type;
	$exParam {$loc} = $value;
	&nextSymbol;
#	$prime = 0; # primes
#	while (s/^\'//)
#	{
#	  ++ $prime;
#	  &nextSymbol;
#	}
	$exParam{"$loc'"} = ++ $primed{$value};
	&exitError ("Name `$value' is not a known function but is used as such.")
	  if (/^\(/);
      }
    }
    else
    {
      if (($ex eq "A") && !&constType ($value))
      {
	push (@vars, $value) unless $isVar {$value};
	$isVar {$value} = 1;
      }
      &nextSymbol;
#     $prime = 0;
#     while (s/^\'//)
#     {
#       ++ $prime;
#	&nextSymbol;
#     }
      $exParam{"$loc'"} = ++ $primed{$value};
      &exitError ("Name `$value' is not a known function but is used as such.")
        if (/^\(/);
    }
  }
  &nextSymbol;
  if ($inFunc = &pullInfix)
  {
    &exitError ("Infix-like expression `$inFunc' not recognised.")
      unless $isInfix {$inFunc};
    $inLoc = $loc;
    $loc = $globAx ++;
    $exParam {$loc} = $inFunc;
    $exParam {"$loc.0"} = $inLoc;
    &nextSymbol;
    $exParam {"$loc.1"} = &getEx ($ex);
    $exParam {"$loc.n"} = 2;
  }
  $loc;
}

sub exReport
  # Returns an ascii expression
  #   in : location
  #   out : string
{
  local ($loc, $notify, $value, $paramN, $ret, $arrow) = @_;

  $value = $exParam {$loc};
  $arrow = ($loc eq $notify) ? " ----> " : "";
  if ($value eq "(")
  {
    $ret = "$arrow(" . &exReport ($exParam {"$loc.0"}, $notify) . ")";
  }
  elsif ($isInfix {$value})
  {
    $ret = &exReport ($exParam {"$loc.0"}, $notify) . " $arrow$value " .
      &exReport ($exParam {"$loc.1"}, $notify);
  }
  elsif ($isFunc {$value})
  {
    $ret = "$arrow$value";
    if ($exParam {"$loc.n"} >= 0)
    {
      $ret .= " (";
      for $paramN (0 .. $exParam {"$loc.n"} - 1)
      {
	$ret .= ", " if ($paramN > 0);
	$ret .= &exReport ($exParam {"$loc.$paramN"}, $notify);
      }
      $ret .= ")";
    }
  }
  elsif ($isType {$value})
  {
    $ret = "$arrow$value (" . &exReport ($exParam {"$loc.0"}, $notify) . ")";
  }
  elsif ($isVar {$value})
  {
    $ret = "$arrow$value" . ("'" x $exParam {"$loc'"});
  }
  else
  {
    $ret = "$arrow$value";
  }

  $ret;
}

sub readSignatures
  # Read signatures
  #   sets: %isType, @types, %isFunc, @funcs, %funcSigs{func}, %funcType{sig}
  #     %funcType{sig}, -- function return value
  #     %seFunc{sig}, -- does it return by side effect
  #     %funcSeParam{sig}, -- which parameter is a side effect parameter (or -1)
  #     %printOf{type} -- name of print function for type
{
  local ($funcRet, $funcName, $funcSig, $typeName, $isSe, $param, $paramN, $type, $seParam, $sig);

  $currentTask = "Reading signatures.";
  while (&nextSymbol)
  {
    local (@typeList);

    $currentObject = "";
    &exitError ("Expecting a signature return type.") unless $funcRet = &pullType;
    $isSe = $funcRet =~ s/^\{(.*)\}$/\1/;
    &exitError ("Type name `$funcRet' is already a function.") if $isFunc {$funcRet};
    &nextSymbol;
    &exitError ("Expecting a signature function name.") unless $funcName = &pullIdentifier;
    $currentObject = "`$funcName'";
    &exitError ("Function name `$funcName' is already a type.") if $isType {$funcName};
    push (@funcs, $funcName) unless $isFunc {$funcName};
    $isFunc {$funcName} = 1;
    if ($funcRet ne "")
    {				# genuine function
      &nextSymbol;
      &exitError ("Return type must be non-wild.") if ($funcRet eq "*");
      &exitError ("Function name `$funcRet' used as a type.") if $isFunc {$funcRet};
      $seParam = -1;
      $currentObject .= " parameters";
      $funcSig = "!";
      if (s/^\(//)
      {
	local ($isSe);

	$paramN = 0;
	&nextSymbol;
	while (!/^\)/)
	{
	  if ($paramN > 0)
	  {
	    &exitError ("Missing type-separating comma.") unless s/^,//;
	    &nextSymbol;
	  }
	  &exitError ("Expecting type name.") unless $param = &pullType;
	  $isSe = $param =~ s/^\{(.*)\}$/\1/;
	  &exitError ("Parameter type must be non-nil.") if ($funcRet eq "");
	  &exitError ("Function name `$param' used as a type.") if $isFunc {$param};
	  push (@typeList, $param);
	  if ($isSe)
	  {
	    &exitError ("More then one side-effect parameter with `$param'.")
	      if ($seParam >= 0);
	    &exitError ("Side-effect parameter type `$param' does not match return type.")
	      if $seFunc {$funcName} && ($param ne $funcRet);
	    $seParam = $paramN;
	  }
	  &nextSymbol;
	  ++ $paramN;
	}
	&exitError ("Missing type list terminating parenthesis.") unless s/^\)//;
	$funcSig = "(" . join (",", @typeList);
      }
      for $type (@typeList)
      {
	push (@types, $type) unless $isType {$type} || ($type eq "*");
	$isType {$type} = 1 unless ($type eq "*");
      }
      $sig = &matchSig ($funcSigs {$funcName}, $funcSig);
      &exitError ("There is already a `$funcName' function with a compatible signature. It looks like `" . &signatureOf ($sig) . "', this looks like `" . &signatureOf ($funcSig) . "'.")
	if $sig;
      $funcSigs {$funcName} .= ";" if $funcSigs {$funcName};
      $funcSigs {$funcName} .= $funcSig;
      $funcType {$funcName, $funcSig} = $funcRet;
      $seFunc {$funcName, $funcSig} = $isSe;
      $funcSeParam {$funcName, $funcSig} = $seParam;
    }
    else
    {				# printing function
      &nextSymbol;
      &exitError ("Missing type list introductory parenthesis.") unless s/^\(//;
      &nextSymbol;
      &exitError ("Expecting type name.") unless $typeName = &pullType;
      $isSe = $typeName =~ s/^\{(.*)\}$/\1/;
      &exitError ("Printing functions require a non-wild non-nil type parameter.")
	if ($typeName eq "") || ($typeName eq "*");
      &exitError ("Function name `$typeName' used as a type.") if $isFunc {$typeName};
      &nextSymbol;
      &exitError ("Missing type list terminating parenthesis.") unless s/^\)//;
      &exitError ("There is already a printing function for type `$typeName'.")
	if $printOf {$typeName};
      $printOf {$typeName} = $funcName;
      push (@types, $typeName) unless $isType {$typeName};
      $isType {$typeName} = 1;
      $seFunc {$funcName} = $isSe;
    }
  }
  $currentObject = "";
  $currentTask = "";
}

sub matchSig
  # Returns a matching signature from a signature list with a signature
  #   in : signature list, signature
  #   out : signature or "?"
{
  local ($sigs, $test, $sig, $tmp, @sigList, @typeList, $match, $ret) = @_;

  $ret = "";
  if ($sigs)
  {
    $test =~ s/^\(//;
    @typeList = split (/,/, $test);
    for $sig (split (/;/, $sigs))
    {
      $tmp = $sig;
      $tmp =~ s/^\(//;
      @sigList = split (/,/, $tmp);
      $match = ($#sigList == $#typeList);
      if ($match)
      {
	for $i (0 .. $#sigList)
	{
	  $match &= ($typeList[$i] eq "*") || ($sigList[$i] eq "*") ||
	    ($typeList[$i] eq $sigList[$i]);
	}
	$ret = $sig if $match;
      }
    }
  }

  $ret;
}

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 signatureOf
  # Returns a textual signature
  #   out: text signature
{
  local ($sig, $se, @types) = @_;

  $se = -1 if $se eq "";
  $sig =~ s/^\(//;
  @types = split (/,/, $sig);
  $types[$se] = "{" . $types[$se] . "}" if ($se >= 0);
  ($sig ne "!") ? "(" . join (", ", @types) . ")" : "";
}

sub readAlii
  # Read alii
  #   sets: %isAlias, %aliasOf, @alii
{
  local ($aliasName, $aliasDefn);

  $currentTask = "Reading axia.";
  while (&nextSymbol)
  {
    $currentObject = "";
    &exitError ("Expecting an alias name.") unless $aliasName = &pullIdentifier;
    $currentObject = "`$aliasName'";
    &exitError ("Duplicate alias `$aliasName'.") if $isAlias {$aliasName};
    &nextSymbol;
    &exitError ("Expecting an alias definition.") unless ($aliasDefn = &pullAlias) ne "";
    $aliasDefn = "" if $aliasDefn eq "{}";
    $isAlias {$aliasName} = 1;
    $aliasOf {$aliasName} = $aliasDefn;
    push (@alii, $aliasName);
  }
  $currentObject = "";
  $currentTask = "";
}

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 exitError
  # Report error and exit
{
  die &fileDetails . @_[0] . "\n";
}

sub initialise
  # Initialise global state
{
  $verbose = 0;
  $lineNumber = "NIL";
  $eof = 0;
  $fileName = "NIL";
  @fileList = ();
  $currentTask = "init";
  $currentObject = "world";
  $outputFile = "";
  @includeFiles = ();
  @aliasFiles = ();
  @signatureFiles = ();
  @vectorFiles = ();
  @axiomFiles = ();
  $parameterString = join (" ", @ARGV);
  $globAx = 1;
  $threshold = 512;

  $DAOnce = "DA_Once_";
  $DAGlob = "DA_Glob_";
  $DAReal = "DA_Real_";
  $DADisp = "DA_Disp_";
  $DAName = "DA_Name_";
  $DATest = "DA_Test_";
  $DAVerb = "DA_Verbose";
  $DAAbrt = "DA_Abort";
  $DARnig = "DA_Reneg";
  $DAt = "DA_t_";
  $DAi = "DA_i_";
  $DAl = "DA_l_";
  $DAr = "DA_r_";
  $DAn = "DA_n_";		      # number tried
  $DAf = "DA_f_";		      # number failed
  $DAa = "DA_a_";		      # number aborted
  $DAg = "DA_g_";		      # number reneged
}

sub processRCFile
  # Process .daistishrc options
  #   desires: .daistishrc
  #   sets: $outputFile
  #     @includeFiles, @aliasFiles, @signatureFiles, @vectorFiles
{
  local ($parameters);

  if (open (RCFILE, ".daistishrc"))
  {
    while (<RCFILE>)
    {
      $parameters = " " . $_;
      $outputFile = $1 if ($parameters =~ s/\s+-o\s*(\S+)\s*/ /);
      $threshold = $1 if ($parameters =~ s/\s+-t\s*(\S+)\s*/ /);
      push (includeFiles, $1) while ($parameters =~ s/\s+-i\s*(\S+)\s*/ /);
      push (aliasFiles, $1) while ($parameters =~ s/\s+-a\s*(\S+)\s*/ /);
      push (signatureFiles, $1) while ($parameters =~ s/\s+-s\s*(\S+)\s*/ /);
      push (vectorFiles, $1) while ($parameters =~ s/\s+-v\s*(\S+)\s*/ /);
      $parameters =~ s/^\s*(\S+(\s+\S+)*)\s*$/\1/;
      die "Syntax error on line $. in .daistishrc file (`$parameters').\n"
	if $parameters =~ /\S/;
    }
    close (RCFILE);
  }
}

sub processParameters
  # Processes command line options
  #   needs: @ARGV
  #   sets: $outputFile
  #     @includeFiles, @aliasFiles, @signatureFiles, @vectorFiles, @axiomFiles
{
  local ($parameters);

  $parameters = " " . $parameterString;
  @includeFiles = () if ($parameters =~ /\s+-i\s*(\S+)\s*/);
  @aliasFiles = () if ($parameters =~ /\s+-a\s*(\S+)\s*/);
  @signatureFiles = () if ($parameters =~ /\s+-s\s*(\S+)\s*/);
  @vectorFiles = () if ($parameters =~ /\s+-v\s*(\S+)\s*/);
  $outputFile = $1 if ($parameters =~ s/\s+-o\s*(\S+)\s*/ /);
  $threshold = $1 if ($parameters =~ s/\s+-t\s*(\S+)\s*/ /);
  push (includeFiles, $1) while ($parameters =~ s/\s+-i\s*(\S+)\s*/ /);
  push (aliasFiles, $1) while ($parameters =~ s/\s+-a\s*(\S+)\s*/ /);
  push (signatureFiles, $1) while ($parameters =~ s/\s+-s\s*(\S+)\s*/ /);
  push (vectorFiles, $1) while ($parameters =~ s/\s+-v\s*(\S+)\s*/ /);
  $verbose = ($parameters =~ s/\s+-dump\s*/ /);
  &syntaxError if ($parameters =~ /\s+-/);
  @axiomFiles = split (" ", $parameters);
  die "No output file\n" if ($outputFile eq "");
}

sub reportParameters
  # Reports parameters
{
  print "Output : " . $outputFile . "\n";
  print "Includes : " . join (",", @includeFiles) . "\n";
  print "Alii : " . join (",", @aliasFiles) . "\n";
  print "Signatures : " . join (",", @signatureFiles) . "\n";
  print "Test Vectors : " . join (",", @vectorFiles) . "\n";
  print "Axia : " . join (",", @axiomFiles) . "\n";
}

sub syntaxError
  # Reports syntax error and exits
{
  die "Syntax: daistish {-o <output file> | -i <include file> |" .
      " -a <alias file> | -s <signature file> | -v <test vector file> | -dump |" .
      " <axiom file>}\n";
}

sub useFiles
  # Start using a new set of files
  #   out: file list
{
  @fileList = @_;
  $fileName = "NIL";
  &getLine;
  while (s/--.*$//) {}
}

sub getLine
  # Reads a new line from the current fileList
{
  if (($fileName eq "NIL") || eof)
  {
    local ($name);
    
    close (FILE) if $fileName ne "NIL";
    if ($name = shift (@fileList))
    {
      $fileName = $name;
      $fileLine = 0;
      die "Cannot open file `$fileName'.\n" unless open (FILE, $fileName);
      $eof = 0;
    }
    else
    {
      $fileLine = "EOF";
      $eof = 1;
    }
  }
  ++ $fileLine if !$eof;
  $_ = <FILE>;
}

sub fileDetails
  # Returns current file, line number, symbols, current object
  #   out: $fileName . $fileLine . $_ . $currentObject
{
  chop;
  "Parse failure" . ($fileName ne "NIL" ? " in file `$fileName', line $fileLine" : "") . ($_ ? ", at `$_'" : "") . ($currentObject ? " with $currentObject" : "") . ".\n";
}

sub nextSymbol
  # Go to start of next symbol
  #   out: not EOF
{
  for (s/^\s+//; !$_ && !$eof; s/^\s+//)
  {
    &getLine;
    while (s/--.*$//) {}
  }
  !$eof;
}

sub pullIdentifier
  # Return an identifier symbol
  #   out: identifier word or ""
{
  s/^([a-zA-Z_][a-zA-Z0-9_]*)// ? $1 : "";
}

sub pullSymbol
  # Return an identifier or constant symbol
  #   out: identifier word or ""
{
  s/^([a-zA-Z0-9_]+|-[0-9]+|\"[^\"]*\"|\'[^\']*\')// ? $1 : "";	# "
}

sub pullType
  # Return a type symbol
  # Valid sequences are * ident {} {*} {ident}
  #   out: identifier word or ""
{
  s/^(\*|[a-zA-Z_][a-zA-Z0-9_]*|\{\}|\{\*\}|\{[a-zA-Z_][a-zA-Z0-9_]*\})// ? $1 : "";
}

sub pullVectorName
  # Return a vector name
  # Valid sequences are ident {ident}
  #   out: name or ""
{
  s/^([a-zA-Z_][a-zA-Z0-9_]*|\{([a-zA-Z_][a-zA-Z0-9_]*)\})// ? $1 : "";
}

sub pullAlias
  # Return an alias definition
  # Valid sequences are to EOL
  #   out: alias or ""
{
  s/^(.*\S)\s*$// ? $1 : "";
}

sub pullInfix
  # Return an infix name
  # Vald sequences are $infixSearch+
  #   out : name or ""
{
  s/^([$infixSearch]+)// ? $1 : "";
}