#!/bin/bash
# Copyright (C) 2015 INRIA

BASEDIR="`pwd`"
SRCDIR=$BASEDIR/src
TOOLS=$SRCDIR/TOOLS
DEBUG=$BASEDIR/_debug
RUNNER_MOD_BASE=$TOOLS/runner.mod.file
RUNNER_SIG_BASE=$TOOLS/runner.sig.file
RUNNER_MOD_TARGET=$DEBUG/runner.mod
RUNNER_SIG_TARGET=$DEBUG/runner.sig
RUNNER_MOD_TARGET_SRC=$SRCDIR/runner.mod
RUNNER_SIG_TARGET_SRC=$SRCDIR/runner.sig

export CMD="tjsim -b runner -s run."

ARGS=("$@")
ELEMENTS=${#ARGS[@]}

rm -f $RUNNER_MOD_TARGET_SRC
rm -f $RUNNER_SIG_TARGET_SRC

rm -rf $DEBUG
mkdir $DEBUG

cp `find $SRCDIR -name "*.sig"` $DEBUG
cp `find $SRCDIR/kernel -name "*.sig"` $DEBUG
cp `find $SRCDIR/utils -name "*.sig"` $DEBUG
cp `find $SRCDIR/fpc/tableaux -name "*.sig"` $DEBUG
cp `find $SRCDIR/tests/tableaux -name "*.sig"` $DEBUG
cp `find $SRCDIR/kernel -name "*.mod"` $DEBUG
cp `find $SRCDIR/utils -name "*.mod"` $DEBUG
cp `find $SRCDIR/fpc/tableaux -name "*.mod"` $DEBUG
cp `find $SRCDIR/tests/tableaux -name "*.mod"` $DEBUG
cp $TOOLS/kernel_debug/tableaux-kernel.mod.debug $DEBUG/tableaux-kernel.mod
cp $TOOLS/Makefile.debug $DEBUG/Makefile

echo -e "module runner.\\n" >> $RUNNER_MOD_TARGET
echo -e "sig runner.\\n" >> $RUNNER_SIG_TARGET

if [ $ELEMENTS -ne 1 ]
  then echo "Error: at least one certificate must be given!"
  else
  for (( i=0;i<$ELEMENTS;i++)); do
        echo -e "accum_sig ${ARGS[${i}]}\\n." >> $RUNNER_SIG_TARGET
        echo -e "accumulate ${ARGS[${i}]}\\n." >> $RUNNER_MOD_TARGET
  done

  `cat $RUNNER_SIG_BASE >> $RUNNER_SIG_TARGET`
  `cat $RUNNER_MOD_BASE >> $RUNNER_MOD_TARGET`

  cd $DEBUG && make>/dev/null && $CMD
  rm -rf $DEBUG
fi
