#!/bin/sh

# Automatic test of Coq

if [ "$1" = -byte ]; then
  coqtop="../bin/coqtop.byte -q -batch"
else
  coqtop="../bin/coqtop -q -batch"
fi

command="$coqtop -top Top -load-vernac-source"

# on compte le nombre de tests et de succès
nbtests=0
nbtestsok=0

# La fonction suivante teste le compilateur sur des fichiers qu'il doit
# accepter
test_success() {
    for f in $1/*.v; do 
	nbtests=`expr $nbtests + 1`
	printf "    "$f"..."
	$command $f $2 > /dev/null 2>&1 
	if [ $? = 0 ]; then
	    echo "Ok"
	    nbtestsok=`expr $nbtestsok + 1`
        else 
	    echo "Error! (should be accepted)"
        fi 
    done
}

# La fonction suivante teste le compilateur sur des fichiers qu'il doit
# refuser
test_failure() {
    for f in $1/*.v; do 
	nbtests=`expr $nbtests + 1`
	printf "    "$f"..."
	$command $f > /dev/null 2>&1
	if [ $? != 0 ]; then 
	    echo "Ok"
	    nbtestsok=`expr $nbtestsok + 1`
        else 
	    echo "Error! (should be rejected)"
        fi 
    done
}

# La fonction suivante teste la sortie des fichiers qu'elle exécute 
test_output() {
    for f in $1/*.v; do 
	nbtests=`expr $nbtests + 1`
	printf "    "$f"..."
        tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`
	$command $f 2>&1 | grep -v "Welcome to Coq" | grep -v "Skipping rcfile loading" > $tmpoutput
        foutput=`dirname $f`/`basename $f .v`.out
        diff $tmpoutput $foutput >& /dev/null
	if [ $? = 0 ]; then 
	    echo "Ok"
	    nbtestsok=`expr $nbtestsok + 1`
        else 
	    echo "Error! (unexpected output)"
        fi 
        rm $tmpoutput
    done
}

# La fonction suivante teste l'analyseur syntaxique fournit par "parser"
# Elle fonctionne comme test_output
test_parser() {
    if [ -d $1 ]; then
    for f in $1/*.v; do
        nbtests=`expr $nbtests + 1`
        printf "    "$f"..."
        tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`
        foutput=`dirname $f`/`basename $f .v`.out
        echo "parse_file 1 \"$f\"" | ../bin/parser > $tmpoutput 2>&1
        perl -ne 'if(/Starting.*Parser Loop/){$printit = 1};print if $printit' \
            $tmpoutput 2>&1 | grep -i error > /dev/null
        if [ $? = 0 ] ; then
            echo "Error! (unexpected output)"
        else
            echo "Ok"
            nbtestsok=`expr $nbtestsok + 1`
        fi
        rm $tmpoutput
    done
    fi
}

# La fonction suivante teste en interactif 
test_interactive() {
    for f in $1/*.v; do 
	nbtests=`expr $nbtests + 1`
	printf "    "$f"..."
	$coqtop < $f > /dev/null 2>&1
	if [ $? = 0 ]; then 
	    echo "Ok"
	    nbtestsok=`expr $nbtestsok + 1`
        else 
	    echo "Error! (should be accepted)"
        fi 
    done
}

# La fonction suivante teste en interactif 
# It expects a line "(* Expected time < XXX.YYs *)" in the .v file 
# with exactly two digits after the dot
# The reference for time is a 6120 bogomips cpu
test_complexity() {
    if [ -f /proc/cpuinfo ]; then
	if grep -q bogomips /proc/cpuinfo; then # i386, ppc
	    bogomips=`sed -n -e "s/bogomips.*: \([0-9]*\).*/\1/p" /proc/cpuinfo | head -1`
	elif grep -q Cpu0Bogo /proc/cpuinfo; then # sparc
	    bogomips=`sed -n -e "s/Cpu0Bogo.*: \([0-9]*\).*/\1/p" /proc/cpuinfo | head -1`
	elif grep -q BogoMIPS /proc/cpuinfo; then # alpha
	    bogomips=`sed -n -e "s/BogoMIPS.*: \([0-9]*\).*/\1/p" /proc/cpuinfo | head -1`
	fi
    fi
    if [ "$bogomips" = "" ]; then
	echo "    cannot run complexity tests (no bogomips found)"
    else
      for f in $1/*.v; do 
        nbtests=`expr $nbtests + 1`
        printf "    "$f"..."
        # extract effective user time
        res=`$command $f 2>&1 | sed -n -e "s/Finished transaction in .*(\([0-9]*\.[0-9]*\)u.*)/\1/p" | head -1`
        if [ $? != 0 ]; then
	  echo "Error! (should be accepted)"
        elif [ "$res" = "" ]; then
          echo "Error! (couldn't find a time measure)"
        else
          # express effective time in centiseconds
          res=`echo "$res"00 | sed -n -e "s/\([0-9]*\)\.\([0-9][0-9]\).*/\1\2/p"`
          # find expected time * 100
          exp=`sed -n -e "s/(\*.*Expected time < \([0-9]\).\([0-9][0-9]\)s.*\*)/\1\2/p" $f`
          ok=`expr \( $res \* $bogomips \) "<" \( $exp \* 6120 \)`
          if [ "$ok" = 1 ]; then
              echo "Ok"
              nbtestsok=`expr $nbtestsok + 1`
          else
              echo "Error! (should run faster)"
          fi
        fi
      done
    fi
}

test_bugs () {
    # Process verifications concerning submitted bugs. A message is
    # printed for all opened bugs (still active or seems to be closed).
    # For closed bugs that behave as expected, no message is printed

    # All files are assumed to have <# of the bug>.v as a name

    echo "Testing opened bugs..."
    # We first test opened bugs that should not succeed
    files=`/bin/ls -1 $1/opened/shoulnotsucceed/*.v 2> /dev/null`
    for f in $files; do 
	nbtests=`expr $nbtests + 1`
	printf "    "$f"..."
	$command $f $2 > /dev/null 2>&1 
	if [ $? = 0 ]; then
	    echo "still active"
	    nbtestsok=`expr $nbtestsok + 1`
        else 
	    echo "Error! (bug seems to be closed, please check)"
        fi 
    done

    # And opened bugs that should not fail
    files=`/bin/ls -1 $1/opened/shouldnotfail/*.v 2> /dev/null`
    for f in $files; do 
	nbtests=`expr $nbtests + 1`
	printf "    "$f"..."
	$command $f > /dev/null 2>&1
	if [ $? != 0 ]; then 
	    echo "still active"
	    nbtestsok=`expr $nbtestsok + 1`
        else 
	    echo "Error! (bug seems to be closed, please check)"
        fi 
    done

    echo "Testing closed bugs..."
    # Then closed bugs that should succeed
    files=`/bin/ls -1 $1/closed/shouldsucceed/*.v 2> /dev/null`
    for f in $files; do 
	nbtests=`expr $nbtests + 1`
	printf "    "$f"..."
	$command $f $2 > /dev/null 2>&1 
	if [ $? = 0 ]; then
	    echo "Ok"
	    nbtestsok=`expr $nbtestsok + 1`
        else 
	    echo "Error! (bug seems to be opened, please check)"
        fi 
    done


    # At last, we test closed bugs that should fail
    files=`/bin/ls -1 $1/closed/shouldfail/*.v 2> /dev/null`
    for f in $files; do 
	nbtests=`expr $nbtests + 1`
	printf "    "$f"..."
	$command $f > /dev/null 2>&1
	if [ $? != 0 ]; then 
	    echo "Ok"
	    nbtestsok=`expr $nbtestsok + 1`
        else 
	    echo "Error! (bug seems to be opened, please check)"
        fi 
    done
    
}

test_features () {
    # Process verifications concerning submitted bugs. A message is
    # printed for all opened bugs (still active or seem to be closed.
    # For closed bugs that behave as expected, no message is printed

    echo "Testing wishes..."
    files=`/bin/ls -1 $1/*.v 2> /dev/null`
    for f in $files; do 
	nbtests=`expr $nbtests + 1`
	printf "    "$f"..."
	$command $f $2 > /dev/null 2>&1 
	if [ $? != 0 ]; then
	    echo "still wished"
	    nbtestsok=`expr $nbtestsok + 1`
        else 
	    echo "Good news! (wish seems to be granted, please check)"
        fi
    done
}

# Programme principal

echo "Success tests"
test_success success
echo "Failure tests"
test_failure failure
echo "Bugs tests"
test_bugs bugs
echo "Output tests"
test_output output
echo "Parser tests"
test_parser parser
echo "Interactive tests"
test_interactive interactive
echo "Complexity tests"
test_complexity complexity
echo "Module tests"
$coqtop -compile modules/Nat
$coqtop -compile modules/plik
test_success modules "-I modules -impredicative-set"
#echo "Ideal-features tests"
#test_features ideal-features

pourcentage=`expr 100 \* $nbtestsok / $nbtests`
echo
echo "$nbtestsok tests passed over $nbtests, i.e. $pourcentage %"