#!/bin/sh

# TEST: tests Beluga by calling it on various examples.
#
# Usage: TEST [options]
#
# [options], if given, are passed to bin/interpreter.
# 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/interpreter 

# 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 are in test.cfg
# - Files ending in .bel contain Beluga programs

$INTERPRETER +t \
    $* \
    arith/arith.bel \
    compile/cls/sources.cfg \
    compile/cls/test.cfg \
    compile/cpm/sources.cfg \
    compile/cpm/test.cfg \
    compile/debruijn/sources.cfg \
    compile/debruijn/test.cfg \
    compile/debruijn1/sources.cfg \
    compile/debruijn1/test.cfg \
    compile/cps/sources.cfg \
    compile/cxm/sources.cfg \
    count-var/cntvar.bel \
    count-var/cntvar-explicit.bel \
    count-var/cntvar-2.bel \
    copy/copy.bel \
    copy/copy-explicit.bel \
    copy/copy-simple.bel \
    copy/copy-simple-explicit.bel \
    cut-elim.bel \
    debruijn1/sources.cfg \
    equal/eq-proof-tuple.bel \
    equal/eq-proof.bel \
    fol/sources.cfg \
    fol/test.cfg \
    free-vars/fvnat.bel \
    free-vars/fvnat-explicit.bel \
    lp-horn/sources.cfg \
    mini-ml/eval-sub-1.bel \
    mini-ml/eval-sub-1-explicit.bel \
    mini-ml/eval-sub.bel \
    mini-ml/eval-sub-explicit.bel \
    mini-ml/tps.bel \
    mini-ml/vsound.bel \
    mini-ml/vsound-explicit.bel \
    path/path.bel \
    path/path-typed.bel \
    small-step/lam.bel \
    small-step/system-f.bel \
    small-step/system-f-iso.bel \
    test/backarrow.bel \
    test/case1.bel \
    test/case1-explicit.bel \
    test/case2.bel \
    test/case2-explicit.bel \
    test/cross.bel \
    test/dependency.bel \
    test/id.bel \
    test/id-simple.bel \
    test/id-explicit.bel \
    test/test.bel \
    test/test-simple.bel \
    test/test-simple-explicit.bel \
    test/schema.bel \
    tpcert.bel \
    typed-eval/tpeval.bel \
    typed-eval/tpeval-explicit.bel \
    typed-eval/tpeval2.bel \
    unique/unique.bel \
    unique/unique-eval.bel \
    LF/arith.lf \
    LF/arith-rec1.lf \
    LF/lambda.lf \
    LF/lambda-rec.lf \
    LF/simple-typing.lf \
    LF/lam-tp-rec.lf \
    LF/cut-elim.lf \
    LF/kindtest.lf \
    LF/mini-ml.lf \
    LF/mini-ml-rec.lf \
    LF/vsound.lf \
    LF/vsound-rec.lf \
    LF/tpeval.lf \
    LF/tpeval-rec.lf \
    LF/tpcert.lf \
    LF/tps.lf \
    ../examples-twelf/arith/sources.cfg \
    ../examples-twelf/alloc-sem/sources.cfg \
    ../examples-twelf/ccc/sources.cfg \
    ../examples-twelf/church-rosser/sources.cfg \
    ../examples-twelf/church-rosser/test.cfg \
    ../examples-twelf/cpsocc/sources.cfg \
    ../examples-twelf/compile/cls/sources.cfg \
    ../examples-twelf/compile/cls/test.cfg \
    ../examples-twelf/compile/cpm/sources.cfg \
    ../examples-twelf/compile/cpm/test.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/mini-ml/test.cfg \
    ../examples-twelf/prop-calc/sources.cfg \
    test/alpha.bel \
    test/sigma1.bel \
    test/sigma2.bel \
    test/sigma3.bel \
    test/sigma4.bel \
    test/implicit-obj.bel 
