#!/bin/bash
#
# mkexpr
# Morgan Deters <mdeters@cs.nyu.edu> for CVC4
# Copyright (c) 2010  The CVC4 Project
#
# The purpose of this script is to create {expr,expr_manager}.{h,cpp}
# from template files and a list of theory kinds.  Basically it just
# sets up the public interface for access to constants.
#
# Invocation:
#
#   mkexpr template-file theory-kind-files...
#
# Output is to standard out.
#

copyright=2010

filename=`basename "$1" | sed 's,_template,,'`

cat <<EOF
/*********************                                                        */
/** $filename
 **
 ** Copyright $copyright  The AcSys Group, New York University, and as below.
 **
 ** This file automatically generated by:
 **
 **     $0 $@
 **
 ** for the CVC4 project.
 **/

EOF

me=$(basename "$0")

template=$1; shift

includes=
getConst_instantiations=
getConst_implementations=
mkConst_instantiations=
mkConst_implementations=

seen_theory=false
seen_theory_builtin=false

function theory {
  # theory T header

  lineno=${BASH_LINENO[0]}

  # this script doesn't care about the theory class information, but
  # makes does make sure it's there
  seen_theory=true
  if [ "$1" = builtin ]; then
    if $seen_theory_builtin; then
      echo "$kf:$lineno: error: \"builtin\" theory redefined" >&2
      exit 1
    fi
    seen_theory_builtin=true
  elif [ -z "$1" -o -z "$2" ]; then
    echo "$kf:$lineno: error: \"theory\" directive missing class or header argument" >&2
    exit 1
  elif ! expr "$1" : '\(::*\)' >/dev/null; then
    echo "$kf:$lineno: warning: theory class \`$1' isn't fully-qualified (e.g., ::CVC4::theory::foo)" >&2
  elif ! expr "$1" : '\(::CVC4::theory::*\)' >/dev/null; then
    echo "$kf:$lineno: warning: theory class not under ::CVC4::theory namespace" >&2
  fi
}

function variable {
  # variable K ["comment"]

  lineno=${BASH_LINENO[0]}

  check_theory_seen
}

function operator {
  # operator K #children ["comment"]

  lineno=${BASH_LINENO[0]}

  check_theory_seen
}

function nonatomic_operator {
  # nonatomic_operator K #children ["comment"]

  lineno=${BASH_LINENO[0]}

  check_theory_seen
}

function parameterized {
  # parameterized K #children ["comment"]

  lineno=${BASH_LINENO[0]}

  check_theory_seen
}

function constant {
  # constant K T Hasher header ["comment"]

  lineno=${BASH_LINENO[0]}

  check_theory_seen

  includes="${includes}
#include \"$4\""
  mkConst_instantiations="${mkConst_instantiations}
template <>
Expr ExprManager::mkConst($2 const& val);
"
  mkConst_implementations="${mkConst_implementations}
template <>
Expr ExprManager::mkConst($2 const& val) {
  return Expr(this, new Node(d_nodeManager->mkConst< $2 >(val)));
}
"
  getConst_instantiations="${getConst_instantiations}
template <>
$2 const & Expr::getConst< $2 >() const;
"
  getConst_implementations="${getConst_implementations}
template <>
$2 const & Expr::getConst() const {
  // check even for production builds
  CheckArgument(getKind() == ::CVC4::kind::$1, *this,
                \"Improper kind for getConst<$2>()\");
  return d_node->getConst< $2 >();
}
"
}

function check_theory_seen {
  if ! $seen_theory; then
    echo "$kf:$lineno: error: no \"theory\" declaration found (it has to be first)" >&2
    exit 1
  fi
}

function check_builtin_theory_seen {
  if ! $seen_theory_builtin; then
    echo "$me: warning: no declaration for the builtin theory found" >&2
  fi
}

while [ $# -gt 0 ]; do
  kf=$1
  seen_theory=false
  b=$(basename $(dirname "$kf"))
  source "$kf"
  check_theory_seen
  shift
done
check_builtin_theory_seen

## output

text=$(cat "$template")
for var in \
    includes \
    template \
    getConst_instantiations \
    getConst_implementations \
    mkConst_instantiations \
    mkConst_implementations; do
  eval text="\${text//\\\$\\{$var\\}/\${$var}}"
done
error=`expr "$text" : '.*\${\([^}]*\)}.*'`
if [ -n "$error" ]; then
  echo "$template:0: error: undefined replacement \${$error}" >&2
  exit 1
fi
echo "$text"