1#!/bin/bash
2
3source ../.acl2holrc.bash
4
5tests_dir=${ACL2_HOL}/tests
6inputs_dir=$tests_dir/inputs
7results_dir=$tests_dir/results
8old_results_dir=$tests_dir/old-results
9logs_dir=$tests_dir/logs
10old_logs_dir=$tests_dir/old-logs
11gold_dir=$tests_dir/gold
12lisp_dir=${ACL2_HOL}/lisp
13
14my_status=0
15
16my_args=$*
17
18if [ "$my_args" = "clean+" ]; then \
19    pushd $lisp_dir ; \
20    make clean ; \
21    my_args=clean ; \
22    popd ; \
23fi
24
25if [ "$my_args" = "clean" ]; then \
26    rm -f diffout diffout.old 2> /dev/null ; \
27    rm -rf $results_dir $old_results_dir $logs_dir $old_logs_dir ; \
28    cd $inputs_dir ; make clean ; cd .. ; \
29    cd round-trip ; ./doit clean ; cd .. ; \
30    exit 0 ; \
31fi
32
33echo "Making books in $lisp_dir..." ; cd $lisp_dir ; make -s ; temp_status=$? ; cd ..
34if [ $temp_status -ne 0 ]; then echo "***Failure making books in $lisp_dir" ; my_status=1 ; fi
35
36echo "Making books in $inputs_dir..." ; cd $inputs_dir ; make -s ; temp_status=$? ; cd ..
37if [ $temp_status -ne 0 ]; then echo "***Failure making books in $inputs_dir" ; my_status=1 ; fi
38
39echo "Converting .lisp files to their essences..."
40
41tests=`ls $inputs_dir/*.lisp`
42
43rm -rf $old_results_dir
44if  [ -e $results_dir ]; then mv $results_dir $old_results_dir ; fi
45mkdir $results_dir
46
47rm -rf $old_logs_dir
48if [ -e $logs_dir ]; then mv $logs_dir $old_logs_dir ; fi
49mkdir $logs_dir
50
51if [ -e diffout ]; then mv diffout diffout.old ; fi
52
53for test in $tests ; do \
54    test=${test##*/} ; \
55    (${ACL2_HOL_LISP}/book-essence.csh $inputs_dir/$test $results_dir/$test) > $logs_dir/$test.out 2> $logs_dir/$test.err ; \
56    testr=${test%.*} ; \
57    (${ACL2_HOL_LISP}/a2ml.csh $results_dir/$test $results_dir/$testr.sml $inputs_dir) > $logs_dir/$test.sml.out 2> $logs_dir/$test.sml.err ; \
58done
59
60(diff -x .svn $results_dir $gold_dir 2>&1) > diffout
61
62if [ -s diffout ] ; then \
63    echo '***Failure*** for main tests!  See diffout and round-trip/diffout for diffs, and see logs/.' ; \
64    my_status=1 ; \
65else \
66    echo 'Success for main tests!' ; \
67fi
68
69echo "Entering round-trip/ directory..."
70pushd round-trip > /dev/null
71./doit
72temp_status=$?
73# Note that round-trip/doit does its own success/failure printing
74if [ $my_status -eq 0 ]; then my_status=$temp_status ; fi
75popd > /dev/null
76
77if [ $my_status -eq 0 ] ; then \
78    echo 'SUCCESS!' ; \
79    exit 0 ; \
80else \
81    echo 'FAILURE!  See failure message(s) above.' ; \
82    exit $my_status ; \
83fi
84