#!/bin/bash

pgm="bin/why3 prove"

coma_bad () {
    test -d $1 || exit 1
    for f in $1/*.coma ; do
        printf "  $f... "
        if $pgm $2 $f > /dev/null 2>&1; then
            echo "failed! (should have an error)"
            echo $pgm $2 $f
            $pgm $2 $f
            exit 1
        fi
        echo "ok"
    done
}

coma_good () {
    test -d $1 || exit 1
    rm -f bench_errors
    rm -f bench_error
    for f in $1/*.$2 ; do
        printf "  $f... "
        if ! $pgm $f > /dev/null 2> bench_error; then
            echo "failed!"
            echo "invocation: $pgm $opts $f" | tee -a bench_errors
            cat bench_error | tee -a bench_errors
            rm -f bench_errors bench_error
            exit 1
        fi
        rm -f bench_error
        echo "ok"
    done
}

simple_test() {
    if ! "$@" > /dev/null 2> /dev/null; then
        echo "failed!"
        echo "$@"
        "$@"
        exit 1
    fi
    echo "ok"
}

replay () {
    pgm="bin/why3 replay"
    test -d $1 || exit 1
    for f in $1/*/; do
        printf "  $f... "
        simple_test $pgm $f
    done
}

make -j

echo "=== Checking bad files (Coma) ==="
coma_bad ./bench/plugins/coma/bad
echo ""

echo "=== Checking good files (Coma) ==="
coma_good ./examples/coma coma
coma_good ./bench/plugins/coma/good coma
echo ""

echo "=== Checking replay (Coma) ==="
replay ./examples/coma
echo ""