1 files changed, 89 insertions, 26 deletions
diff --git a/src/theory/mktheoryof b/src/theory/mktheoryof
index b80985c47..ef967342b 100755
--- a/src/theory/mktheoryof
+++ b/src/theory/mktheoryof
@@ -14,11 +14,13 @@
 # Output is to standard out.
 #
 
+copyright=2010
+
 cat <<EOF
 /*********************                                           -*- C++ -*-  */
 /** theoryof_table.h
  **
- ** Copyright 2010  The AcSys Group, New York University, and as below.
+ ** Copyright $copyright  The AcSys Group, New York University, and as below.
  **
  ** This header file automatically generated by:
  **
@@ -29,47 +31,108 @@ cat <<EOF
 
 EOF
 
-prologue=$1; shift
-middle=$1; shift
-epilogue=$1; shift
+template=$1; shift
+
+theoryof_table_includes=
+theoryof_table_registers=
 
-registers=
+seen_theory=false
+seen_theory_builtin=false
 
-function special {
-  r=$1
-  comment=$2
+function theory {
+  lineno=${BASH_LINENO[0]}
 
-  registers="$registers    d_table[::CVC4::kind::$r] = th;
+  # 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
+
+  theoryof_table_includes="${theoryof_table_includes}#include \"theory/$b/$2\"
+"
+  theoryof_table_registers="${theoryof_table_registers}
+  /* from $b */
+  void registerTheory($1* th) {
 "
 }
 
+function variable {
+  # variable K ["comment"]
+
+  lineno=${BASH_LINENO[0]}
+
+  do_theoryof "$1"
+}
+
 function operator {
-  special "$1" "$2"
+  # operator K #children ["comment"]
+
+  lineno=${BASH_LINENO[0]}
+
+  do_theoryof "$1"
 }
 
 function parameterized {
-  special "$1" "$2"
+  # parameterized K #children ["comment"]
+
+  lineno=${BASH_LINENO[0]}
+
+  do_theoryof "$1"
 }
 
 function constant {
-  special "$1" "$3"
+  # constant K T Hasher header ["comment"]
+
+  lineno=${BASH_LINENO[0]}
+
+  do_theoryof "$1"
 }
 
-cat "$prologue"
-while [ $# -gt 0 ]; do
-  b=$(basename $(dirname "$1"))
-  B=$(echo "$b" | tr 'a-z' 'A-Z')
-  echo "#include \"theory/$b/theory_def.h\""
-  registers="$registers
-  /* from $b */
-  void registerTheory(::CVC4::theory::$b::Theory$B* th) {
+function do_theoryof {
+  check_theory_seen
+  theoryof_table_registers="${theoryof_table_registers}    d_table[::CVC4::kind::$1] = th;
 "
-  source "$1"
-  registers="$registers  }
+}
+
+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
+}
+
+while [ $# -gt 0 ]; do
+  kf=$1
+  seen_theory=false
+  b=$(basename $(dirname "$kf"))
+  source "$kf"
+  check_theory_seen
+  theoryof_table_registers="${theoryof_table_registers}  }
 "
   shift
 done
-echo
-cat "$middle"
-echo "$registers"
-cat "$epilogue"
+
+## output
+
+text=$(cat "$template")
+for var in theoryof_table_includes theoryof_table_registers; 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"