#!/bin/sh
#
# tpa-run.sh - Script to run TxlProp's "assert" phase
#  -- (C) 2005 Jonathan Yavner

# Directory where our files are
mydir=${0%tpa-run.sh}

# Abort on first error
set -e
trap 'rm -f tpa_output[12345].xml tpa_o[0-9]*.xml' EXIT

# Parse the options
qv="-q"
while [ $# -gt 0 ]; do
    if [ "$1" = "-quiet" ]; then
	qv="-q -q"
    elif [ "$1" = "-brief" ]; then
	qv="-q"
    elif [ "$1" = "-verbose" ]; then
	qv="-v"
    elif [ "$1" = "-keeptmp" ]; then
	trap '' EXIT
    else
	break
    fi
    shift
done

# Test validity
if [ $# -ne 1 ]; then
    echo "$0 [-quiet] [-brief] [-verbose] [-keeptmp] input.xml >output.xml" >&2
    echo "" >&2
    echo "Run TxlProp's 'assert' phase.  Options:" >&2
    echo "  -quiet    = Say nothing" >&2
    echo "  -brief    = One line per call to TXL (default)" >&2
    echo "  -verbose  = Verbose output" >&2
    echo "  -keeptmp  = Keep temporary files" >&2
    echo "" >&2
    exit 1
fi

# Initial pass
if [ "$qv" = "-q" ]; then echo "  ...tpa-assert..." >&2; fi
txl       $qv $1              ${mydir}tpa-assert.Txl    >tpa_output1.xml
if [ "$qv" = "-q" ]; then echo "  ...tpa-migrate..." >&2; fi
txl       $qv tpa_output1.xml ${mydir}tpa-migrate.Txl   >tpa_output2.xml
if [ "$qv" = "-q" ]; then echo "  ...tpa-construct..." >&2; fi
txl -s 99 $qv tpa_output2.xml ${mydir}tpa-construct.Txl >tpa_output3.xml
if [ "$qv" = "-q" ]; then echo "  ...tpa-match..." >&2; fi
txl       $qv tpa_output3.xml ${mydir}tpa-match.Txl     >tpa_output4.xml
if [ "$qv" = "-q" ]; then echo "  ...tpa-expr..." >&2; fi
txl -s 60 $qv tpa_output4.xml ${mydir}tpa-expr.Txl      >tpa_output5.xml
if [ "$qv" = "-q" ]; then echo "  ...tpa-paradigm..." >&2; fi
txl -s 60 $qv tpa_output5.xml ${mydir}tpa-paradigm.Txl  >tpa_o0.xml

# Simplification loop
for ((loop=1; $loop<100; loop=$loop+1)); do
    ((prev=$loop-1))
    if [ "$qv" = "-q" ]; then echo "  ~~~Simplification ($loop)~~~" >&2; fi
    if [ "$qv" = "-q" ]; then echo "    ...tpa-expr..." >&2; fi
    txl -s 60 $qv tpa_o${prev}.xml ${mydir}tpa-expr.Txl  >tpa_o${loop}.xml
    if cmp -s tpa_o${prev}.xml tpa_o${loop}.xml; then echo -n; else continue; fi
    if [ "$qv" = "-q" ]; then echo "    ...tpa-split..." >&2; fi
    txl -s 60 $qv tpa_o${prev}.xml ${mydir}tpa-split.Txl >tpa_o${loop}.xml
    if cmp -s tpa_o${prev}.xml tpa_o${loop}.xml; then echo -n; else continue; fi
    if [ "$qv" = "-q" ]; then echo "    ...tpa-join..." >&2; fi
    txl -s 60 $qv tpa_o${prev}.xml ${mydir}tpa-join.Txl  >tpa_o${loop}.xml
    if cmp -s tpa_o${prev}.xml tpa_o${loop}.xml; then break; fi
done

if [ $loop -eq 100 ]; then
    echo "  (Simplification  did not converge!)" >&2;
    exit 1
fi

if [ "$qv" = "-q" ]; then echo "  ...tpa-cleanup..." >&2; fi
txl $qv tpa_o$loop.xml ${mydir}tpa-cleanup.Txl
