#!/bin/bash

# NAME
#     tgc - generate and check a correctness theorem for a Leo compiler stage
#
# USAGE
#     tgc STAGE FILE1 FILE2 THEOREMFILE
#
#     STAGE is one of the following:
#         parsing            Check if FILE2 is a valid AST from parsing Leo source FILE1
#     Unsupported for now:
#         canonicalization   Check if FILE2 is a valid canonicalization of FILE1
#         type-inference     Check if FILE2 is a valid type inference of FILE1
#
#     THEOREMFILE is where the theorem will be written.  It must end in ".lisp".
#
# DESCRIPTION
#     Generate and check a correctness theorem for the Leo compiler stage given by STAGE,
#     using FILE1 and FILE2 as the before and after files from the Leo compiler.
#     Write THEOREMFILE containing an ACL2 theorem of correctness of the given compiler stage.
#     Check (prove) the correctness of THEOREMFILE, and if proved, exit with status 0.
#
# NOTES
#     This script expects a number of files to accompany it in a bundle:
#       lx86cl64
#       leo-acl2.lx86cl64
#       theorem-template-parsing.tl
#     Unspported for now:
#       theorem-template-canonicalization.tl
#       theorem-template-type-inference.tl
#
# AUTHOR
#     Eric McCarthy (bendyarm on GitHub)
#
# COPYRIGHT (C) 2021-2022 Aleo Systems Inc.


# Source and AST file and theorem file names, if relative,
# are relative to the current directory.
# Record this directory in case something later changes PWD.
initialPWD="$PWD"

# Bundle files are in the directory containing this script.
# That includes theorem template files.
thisDir=$( cd "$(dirname "${BASH_SOURCE[0]}")" ; pwd -P )

if [ $# -ne 4 ]; then
    echo "tgc: wrong number of arguments" >&2
    exit 2
fi

# Unsupported for now:  && "$1" != canonicalization && "$1" != type-inference
if [[ "$1" != parsing ]]; then
#     echo "tgc: STAGE must be 'parsing', 'canonicalization' or 'type-inference'" >&2
    echo "tgc: STAGE must be 'parsing'" >&2
    exit 2
fi
STAGE="$1"

FILE1="$2"
FILE2="$3"
FILE1HASH=`sha256sum $2 | cut -d' ' -f1`
FILE2HASH=`sha256sum $3 | cut -d' ' -f1`

# When THEOREMFILE is passed to the lisp command, it must be
# an absolute path.  (If the FILEs are relative to PWD, it is fine.)
# Here we add PWD to THEOREMFILE.  This could be made smarter to handle ~.
if [[ "$4" == "/*" ]]
then
    THEOREMFILE="$4"
else
    THEOREMFILE="$initialPWD"/"$4"
fi

# See also *stage-information* in batch-theorems.lisp
case "$1" in
    parsing)
        TEMPLATEFILE="${thisDir}/theorem-template-parsing.tl"
        ;;
#     canonicalization)
#         TEMPLATEFILE="${thisDir}/theorem-template-canonicalization.tl"
#         ;;
#     type-inference)
#         TEMPLATEFILE="${thisDir}/theorem-template-type-inference.tl"
#         ;;
    *)
        echo "tgc: STAGE must be 'parsing'" >&2
#        echo "tgc: STAGE must be 'parsing' or 'canonicalization' or 'type-inference'" >&2
        exit 2
        ;;
esac


# add literal double quotes
STG="\"$STAGE\""
TEMPLF="\"$TEMPLATEFILE\""
THEOF="\"$THEOREMFILE\""
AF1="\"$FILE1\""
AF2="\"$FILE2\""
AF1H="\"$FILE1HASH\""
AF2H="\"$FILE2HASH\""
lispCommand="(tgc $STG $TEMPLF $THEOF $AF1 $AF2 $AF1H $AF2H)"

# This might be needed --- see any saved_acl2 script
export CCL_DEFAULT_DIRECTORY="$thisDir"

# Prevents package from being switched to LEO at startup.
export ACL2_CUSTOMIZATION=NONE

echo Running Lisp Command: $lispCommand
echo  "$lispCommand" | exec "$thisDir/lx86cl64" -I "$thisDir/leo-acl2.lx86cl64" -K ISO-8859-1 -e "(acl2::acl2-default-restart)"
