#!/bin/sh

# TEST: tests Beluga by calling it on various examples.
#
# Usage: TEST [options]
#
# [options], if given, are passed to bin/beluga.
# Example: TEST +d
#
# Note that a leading '@' in a filename means that the test should NOT succeed,
#  because the file has a type error that should be caught.


# set $BELUGA to an absolute path to the toplevel .../beluga directory
#
pwd=`pwd`
BELUGA=`dirname $pwd/$0`
cd $BELUGA
BELUGA=`pwd`
# echo BELUGA: $BELUGA

# set $INTERPRETER to the executable
INTERPRETER=$BELUGA/bin/beluga

# set $X to the `beluga' examples directory
X=$BELUGA/examples
cd $X


# We use the following conventions:
#
# - Pure LF signatures (and original converted Twelf example) are in files sources.cfg
# - Proofs written in Beluga (or an original Twelf example) are in test.cfg
#

$INTERPRETER +t \
    $* \
    ../examples-twelf/arith/sources.cfg \
    ../examples-twelf/alloc-sem/sources.cfg \
    ../examples-twelf/ccc/sources.cfg \
    ../examples-twelf/church-rosser/sources.cfg \
    ../examples-twelf/cpsocc/sources.cfg \
    ../examples-twelf/compile/cls/sources.cfg \
    ../examples-twelf/compile/cpm/sources.cfg \
    ../examples-twelf/compile/debruijn/sources.cfg \
    ../examples-twelf/compile/debruijn1/sources.cfg \
    ../examples-twelf/compile/cps/sources.cfg \
    ../examples-twelf/cut-elim/sources.cfg \
    ../examples-twelf/fol/sources.cfg \
    ../examples-twelf/handbook/sources.cfg \
    ../examples-twelf/kolm/sources.cfg \
    ../examples-twelf/lp/sources.cfg \
    ../examples-twelf/lp-horn/sources.cfg \
    ../examples-twelf/mini-ml/sources.cfg \
    ../examples-twelf/prop-calc/sources.cfg
