#!/bin/sh

#
# This script requires two arguments which are file names:
#
# 1. The name of a C source file which defines a three-valued halting
#    decider function, whose prototype is:
#
#      ternary halting_decider(const char *program, const char *input);
#
#    This function tries to answer the question: does the program,
#    when given the specified input, halt? It can return TRUE, or FALSE.
#    It can also return ERROR when, for whatever reason, it deems
#    that neither TRUE nor FALSE is the correct answer.
#
# 2. The name of a C source file which defines the following boolean
#    function, which returns 0 or 1:
#
#      int error_decider(const char *hdecider, const char *program,
#                        const char *input);
#
#    Error decider functions try to answer the question: does the given
#    program, when operating on the given input, behave in such
#    a way that the given decider must return ERROR for that program?
#

set -e # stop on any errors

MYDIR=$(dirname "$0")

CFLAGS="-Wall -W -ansi -Wno-unused -Wstrict-prototypes -Wmissing-prototypes"
STANDALONE_ONLY=

. "$MYDIR"/lib.sh

while [ $# -ge 1 ] ; do
  case "$1" in
  --standalone-only )
    STANDALONE_ONLY=y
    shift
    ;;
  --* | -* )
    printf "%s: unrecognized option %s\n" "$0" "$1"
    exit 1
    ;;
  * )
    break
    ;;
  esac
done

if [ $# != 2 ] ; then
  printf "usage: %s [ <options> ] <halting_decider>.c <error_decider.c>\n" "$0"
  printf "options:\n"
  printf "  --standalone-only   generate only stand-alone decider, compile it,\n"
  printf "                      and do not execute it.\n"
  exit 1
fi

ORIG_HALTING_DECIDER=$1
ORIG_ERROR_DECIDER=$2

HD_FULL_HASH=$(file_hash $ORIG_HALTING_DECIDER)
ED_FULL_HASH=$(file_hash $ORIG_ERROR_DECIDER)
HD_HASH=$(short_hash $HD_FULL_HASH)
ED_HASH=$(short_hash $ED_FULL_HASH)

HALTING_DECIDER=hd-${HD_HASH}.c
ERROR_DECIDER=ed-${ED_HASH}.c

cp $ORIG_HALTING_DECIDER $HALTING_DECIDER
cp $ORIG_ERROR_DECIDER $ERROR_DECIDER

PROGRAM_BASENAME=pg-${HD_HASH}-${ED_HASH}
PROGRAM_CLASS_BASENAME=pg-"*"-${ED_HASH}
STANDALONE_DECIDER_BASENAME=sa-${HD_HASH}

printf "halting decider: %s\n" $HALTING_DECIDER
printf "error decider: %s\n" $ERROR_DECIDER

if [ -z "$STANDALONE_ONLY" ] ; then
  printf "\n"
  printf "generating program %s from these deciders\n" $PROGRAM_BASENAME.c

cat > ${PROGRAM_BASENAME}.c <<!
#include <stdio.h>
#include <stdlib.h>
#include "ternary.h"

ternary halting_decider(const char *, const char *);
int error_decider(const char *, const char *, const char *);

#define HD_HASH "$HD_HASH"
#define ED_HASH "$ED_HASH"
#define PG_BASE "$PROGRAM_BASENAME"
#define PG_CLAS "$PROGRAM_CLASS_BASENAME"
#define PG_SELF PG_BASE ".c"
#define HD_NAME "$HALTING_DECIDER"

int main(int argc, char **argv)
{
  const char *input;

  if (argc != 2) {
    fprintf(stderr, "this program test case requires input\n");
    return EXIT_FAILURE;
  }

  input = argv[1];

  if (error_decider(HD_NAME, PG_SELF, input)) {
    switch (halting_decider(PG_SELF, input)) {
    case FALSE:
      printf("decider %s RIGHT: %s/%s does not halt\n", HD_NAME, PG_SELF, input);
      for(;;);
    case TRUE:
      printf("decider %s RIGHT: %s/%s halts\n", HD_NAME, PG_SELF, input);
      return EXIT_SUCCESS;
    case ERROR:
      printf("decider %s WRONG: TRUE and FALSE are viable answers for %s\n",
             HD_NAME, PG_CLAS);
      abort();
    }
  } else {
    switch (halting_decider(PG_SELF, input)) {
    case FALSE:
      printf("decider %s WRONG: %s/%s does not halt\n", HD_NAME, PG_SELF, input);
      return EXIT_SUCCESS;
    case TRUE:
      printf("decider %s WRONG: %s/%s halts\n", HD_NAME, PG_SELF, input);
      for(;;);
    case ERROR:
      printf("decider %s WRONG: neither TRUE nor FALSE false is right for %s\n",
             HD_NAME, PG_CLAS);
      abort();
    }
  }
  /* notreached */
  puts("internal error");
  abort();
}

#include "$ERROR_DECIDER"
#include "$HALTING_DECIDER"
!

  printf "compiling %s to %s\n" $PROGRAM_BASENAME.c $PROGRAM_BASENAME
  gcc $CFLAGS $PROGRAM_BASENAME.c -o $PROGRAM_BASENAME
fi

printf "\n"

printf "generating standalone decider %s\n" $STANDALONE_DECIDER_BASENAME.c
cat > $STANDALONE_DECIDER_BASENAME.c <<!
#include <stdio.h>
#include <stdlib.h>
#include "ternary.h"

ternary halting_decider(const char *, const char *);

int main(int argc, char **argv)
{
  if (argc != 3) {
    fprintf(stderr, "usage: %s <program>.c <input>\n", argv[0]);
    return EXIT_FAILURE;
  }

  switch (halting_decider(argv[1], argv[2])) {
  case FALSE:
    printf("%s: %s will not halt on %s\n", argv[0], argv[1], argv[2]);
    break;
  case TRUE:
    printf("%s: %s will halt on %s\n", argv[0], argv[1], argv[2]);
    break;
  case ERROR:
    printf("%s: for %s run on %s, the answer is ERROR\n",
            argv[0], argv[1], argv[2]);
    break;
  }

  return 0;
}

#include "$HALTING_DECIDER"
!
printf "compiling %s to %s\n" $STANDALONE_DECIDER_BASENAME.c $STANDALONE_DECIDER_BASENAME
gcc $CFLAGS $STANDALONE_DECIDER_BASENAME.c -o $STANDALONE_DECIDER_BASENAME

if [ -z "$STANDALONE_ONLY" ] ; then
  printf "\n"

  printf "executing stand alone decider: %s %s %s\n" \
    ./$STANDALONE_DECIDER_BASENAME $PROGRAM_BASENAME.c $PROGRAM_BASENAME.c

  ./$STANDALONE_DECIDER_BASENAME $PROGRAM_BASENAME.c $PROGRAM_BASENAME.c

  printf "\n"

  printf "executing test case %s %s\n" ./$PROGRAM_BASENAME $PROGRAM_BASENAME.c
  ./$PROGRAM_BASENAME $PROGRAM_BASENAME.c
fi