1 files changed, 177 insertions, 0 deletions
diff --git a/src/expr/mkexpr b/src/expr/mkexpr
new file mode 100755
index 000000000..de6de014d
--- /dev/null
+++ b/src/expr/mkexpr
@@ -0,0 +1,177 @@
+#!/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 {
+  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"