1#!/bin/csh -f
2
3set a2ml = ${ACL2_HOL_LISP}/a2ml
4
5if ( ($#argv != 2) && ($#argv != 3)) then
6	echo "Usage: $0 infile outfile [infile_dir]"
7	exit 1
8endif
9
10set tmpfile = /tmp/workxxx
11set infile = $argv[1]
12set outfile = $argv[2]
13if ( ($#argv == 3)) then
14    set infile_dir = $argv[3]
15else
16    set infile_dir = ""
17endif
18
19rm -f $tmpfile
20echo "(include-book " '"'"${a2ml}"'")' > $tmpfile
21echo "(a2ml "'"'"$infile"'" "'"$outfile"'" "'"$infile_dir"'")' >> $tmpfile
22echo "(value :q) (quit)" >> $tmpfile
23${ACL2} < $tmpfile
24