#!/bin/sh

# auto bench for why

pgm=$1
option=$2
coqc="coqc -I ../lib/coq"

pvstc () {
    context=`dirname $1`
    theory=`basename $1`
    cd $context
    echo "(typecheck "'"'$theory'"'")" > pvstc.el
    pvs -q -batch -l pvstc.el
    cd ..
}

provers () {
    file=$1
    base=$2
    dir=`dirname $1`
    # running Coq
    if ! $coqc "$base"_why.v > /dev/null 2>&1; then
	echo "coq FAILED"
	$coqc "$base"_why.v
	exit 1
    fi
#      if ! $coqc -I $dir "$base"_valid.v > /dev/null 2>&1; then
#  	echo "coq validation FAILED"
#  	$coqc -I $dir "$base"_valid.v
#  	exit 1
#      fi
    echo -n "coq ok... "
    # running PVS
    if ! $pgm --pvs $f > /dev/null 2>&1; then
	echo "pvs generation FAILED"
	$pgm --pvs $f
	exit 1
    fi
    if test "$option" = "pvs"; then 
    if ! pvstc "$base"_why > /dev/null 2>&1; then
	echo "pvs typecheck FAILED"
	pvs -q -v 3 -batch -l pvstc.el
	exit 1
    fi
    echo "pvs ok"
    else
    echo
    fi
}

good_tc () {
    for f in $1/*.mlw; do
	echo -n "  "$f"... "
	base=$1/`basename $f .mlw`
	# running Why
	if ! $pgm --type-only $f > /dev/null 2>&1; then
	    echo "why FAILED"
	    $pgm --type-only $f
	    exit 1
	fi
	echo "why ok... "
    done
}

good_ml () {
    for f in $1/*.mlw; do
	echo -n "  "$f"... "
	base=$1/`basename $f .mlw`
	# running Why
	if ! $pgm --coq-@COQVER@ $f > /dev/null 2>&1; then
	    echo "why FAILED"
	    $pgm --coq-@COQVER@ $f
	    exit 1
	fi
	echo -n "why ok... "
	provers $f $base
#  		echo -n "coq ok..."
#  		$pgm --ocaml --ocaml-ext $f > $base.ml 2>/dev/null
#  		if ocamlc -c $base.ml > /dev/null 2>&1; then
#  		    echo "ocaml ok"
#  		else
#  		    echo "ocaml FAILED"
#  		fi
    done
}

bads () {
    for f in $1/*.mlw; do
	echo -n "  "$f"... "
	if $pgm $2 $f > /dev/null 2>&1; then 
	    echo "$pgm $2 $f"
	    echo "FAILED!"
	    exit 1 
        else 
	    echo "ok"
	fi
    done
}

# 1. Syntax
echo "=== Checking parsing errors ==="
bads bad/syntax --parse-only
echo ""

# 2. Typing
echo "=== Checking typing errors ==="
bads bad/typing --type-only
echo ""

# 2. Other
echo "=== Checking other errors ==="
bads bad/other
echo ""

# 3. benchmark
echo "=== Type-checking good files ==="
good_tc provers
echo ""

echo "=== Checking good files ==="
good_ml good
echo ""

