

# ---------------------------------------------------------------------
# Configuration
# ---------------------------------------------------------------------

parseBin=$RAC/bin/parse
translateBook=$RAC/lisp/translate
acl2Bin=$ACL2

# ---------------------------------------------------------------------
# options parsing
# ---------------------------------------------------------------------

usage() {
    cat <<USAGEEOF
Usage:

  rac [options] srcfile

rac parses the given srcfile, checks that it satisfies the RAC
subset restrictions, and optionally generates various outputs.

Options are:

  -a                 Generate lisp output for ACL2.

  -r                 Extract only the RAC code.

  -I dir             Look for include files in directory 'dir'

  -h                 Print this message.
USAGEEOF
}

srcfile=
acl2=
rac=
incdirs="-I $RAC/include"
last=

while [[ "$1" != "" ]]; do
    case "$1" in
    -a | --acl2)
        acl2=1
        ;;
    -r | --rac)
        rac=1
        ;;
    -I)
        incdirs="$incdirs $2";
        shift
        ;;
    -h)
        usage
        exit
        ;;
    -*)
        echo "Unknow option $1"
        usage
        exit 1
        ;;
    *)
        if [[ "$last" ]]; then
          echo $1
          usage
          exit 1
        else
          last="$1"
        fi
        ;;
    esac

    shift
done

# Extract the source filename and
# make sure only one of ctos, acl2, rac is specified

if [[ -z "$last" ]]
then
    usage;
    exit 1
else
    srcfile=$last;
fi

if [[ "$acl2" && "$rac" ]]
then
    usage;
    exit 1
fi

# ---------------------------------------------------------------------
# Call the rac parser in the appropriate mode
# ---------------------------------------------------------------------

# Die immediately on any error
set -e

basename=${srcfile%.*}
cppopts="-D__RAC__ -C -std=c++14 -x c++"

# The goals of the pipeline are:
#  * rename assert into __RAC_ASSERT to avoid their expansion (they are defined
#    as macro but the parser need to see them as a function call).
#  * preprocess the file using gcc.

# Add the file name otherwise g++ would report error in <STDIN>.
echo "# 1 \"$basename.cpp\"" | \
  # Add the source code to the stream.
  cat - $basename.cpp | \
  # Resolve the includes but do not preprocess the macros
  g++ $cppopts $incdirs -E -fdirectives-only - | \
  # Remove assert definition and rename asserts. Also remove defition that
  # raise redefinition warnings.
  sed "s/#define assert.*//g;
       s/assert/__RAC_ASSERT/g
       s/#define __STDC__ 1//g;
       s/#define __STDC_UTF_16__ 1//g;
       s/#define __STDC_UTF_32__ 1//g;
       s/#define __STDC_HOSTED__ 1//g;" | \
  # And finaly, fully preprocess the file
  g++ $cppopts $incdirs -E -o $basename.i -;

if [[ -z "$acl2" && -z "$rac" ]]
then
    $parseBin $basename $RAC_EXTRA_FLAGS
fi

if [[ "$rac" ]]
then
    $parseBin $basename -rac $RAC_EXTRA_FLAGS
fi

if [[ "$acl2" ]]
then

    $parseBin $basename -acl2 $RAC_EXTRA_FLAGS

    # Disable the loading of acl2-customization.lsp which could break the
    # certification.
    ACL2_CUSTOMIZATION="NONE" $acl2Bin > $basename.acl2.log <<EOF
      (include-book "$translateBook")
      (set-inhibit-output-lst '(prove event proof-tree))
      (translate-program "$basename.ast.lsp" "$basename.lisp" state)
      (pretty-print "$basename.ast.lsp" "$basename.ast.pp" state)
      :u
      (include-book "rtl/rel11/lib/rac" :dir :system)
      (certify-book "$basename" 1)
EOF

# Disable exit on error: when everything is fine, there is no `ACL2 error` so,
# greps fails.
set +e
cat $basename.acl2.log | grep 'ACL2 Error' &> /dev/null
if [[ $? == "0" ]]
then
  echo "Certification failed ! Please check $basename.acl2.log for more details."
  exit 1
fi

fi
