#!/bin/bash
#set -x
TEMP=`getopt -o c:d:m: -- "$@"`
libdir="`pwd`/library"
matitac="`pwd`/matitac.opt"
devel="library"
matitadep="./matitadep.opt"
eval set -- "$TEMP"
while true ; do
  case "$1" in
    -d) libdir="$2"; shift 2 ;;
    -c) matitac="$2"; shift 2 ;;
    -m) devel="$2"; shift 2 ;;
    --) shift; break ;;
     *) echo "Usage: errors_bench [-c MATITAC_PATH] [-d LIBRARY_DIR] [-m MATITAMAKE_DEVEL]"; exit 1 ;;
  esac
done
if ! [ -d "$libdir" ] ; then
  echo "Can't find library directory '$libdir'"
  exit 2
fi
if ! [ -x "$matitac" ] ; then
  echo "Can't find executable Matita compiler '$matitac'"
  exit 2
fi

ma_s=$(find $libdir -name "*.ma" -type f)
sorted_ma_s=$($matitadep -order $ma_s)

log="bench_disamberrors.txt"
rm -f "$log"
echo -e "# FILENAME\tOUTCOME\tEXPECTED_ERROR\tERRORS\tSPURIOUS_ERRORS" > $log
# format: tab-separated fields:
#   FILENAME OUTCOME EXPECTED_ERROR ERRORS SPURIOUS_ERRORS
# field descriptions:
#   OUTCOME is one of {"OK","KO","UNKNOWN(n)"}, n is an exit code
#   EXPECTED_ERROR is FROM-TO, where FROM and TO are character counts
#   ERRORS, same format as above (FROM-TO)
#   SPURIOUS_ERRORS, same format as above (FROM-TO)
log_outcome ()
{
  echo -e "$1|$2|$3|$4|$5" >> "$log"
}

for ma in $sorted_ma_s ; do
  mo=`echo $ma | sed 's/\.ma$/.mo/'`
  make -C $libdir $mo # ensure deps for $mo have been built
  rotten_mas=$(ls $libdir/$ma.*.rottened)
  for rotten_ma in $rotten_mas ; do
    rotten_ma=$(echo $rotten_ma | sed s@^$(pwd)/@@)  # prettier names
    echo "$rotten_ma ..."
    tmp="bench_disamberrors.tmp"
    $matitac $rotten_ma &> $tmp
    outcome=$?
    if [ "$outcome" = 3 ] ; then
      outcome="KO"
    elif [ "$outcome" = 0 ] ; then
      outcome="OK"
    else
      outcome="UNKNOWN($outcome)"
    fi
    supposed_error=$(grep ^error-at: $rotten_ma | cut -f 2 -d' ')
    errors=""
    spurious_errors=""
    error_pass=""
    error_loc=""
    while read e ; do
      if echo "$e" | grep -q "Error at" && [ -n "$error_pass" ] ; then
        # this is an error location line
        if echo "$e" | grep -q "Spurious" ; then
          loc=$(echo "$e" | sed 's/:.*$//' | cut -f 4 -d ' ')
          if ! echo "$spurious_errors" | grep -q "$loc"; then
            if ! [ -z "$spurious_errors" ] ; then spurious_errors="$spurious_errors," ; fi
            spurious_errors="$spurious_errors$loc"
          fi
        else
          loc=$(echo "$e" | sed 's/:.*$//' | cut -f 3 -d ' ')
          if ! echo "$errors" | grep -q "$loc"; then
            if ! [ -z "$errors" ] ; then errors="$errors," ; fi
            errors="$errors$loc"
          fi
        fi
      fi
      error_pass=$(echo "$e" | grep "during phases " | sed 's/:.*$//' | cut -f 6 -d' ' | grep "4\|6")
    done < $tmp
    log_outcome $rotten_ma $outcome $supposed_error $errors $spurious_errors
  done
done

echo "See $log for benchmark results"