diff options
Diffstat (limited to 'src/expr/mkkind')
| -rwxr-xr-x | src/expr/mkkind | 131 |
1 files changed, 107 insertions, 24 deletions
diff --git a/src/expr/mkkind b/src/expr/mkkind index cffdc0caa..6d75164d1 100755 --- a/src/expr/mkkind +++ b/src/expr/mkkind @@ -5,7 +5,7 @@ # Copyright (c) 2010 The CVC4 Project # # The purpose of this script is to create kind.h from a prologue, -# middle, epilogue, and a list of theory kinds. +# middle section, epilogue, and a list of theory kinds. # # Invocation: # @@ -14,11 +14,13 @@ # Output is to standard out. # +copyright=2010 + cat <<EOF /********************* -*- C++ -*- */ /** kind.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,44 +31,125 @@ cat <<EOF EOF -prologue=$1; shift -middle=$1; shift -epilogue=$1; shift +me=$(basename "$0") -cases= +template=$1; shift -function special { - r=$1 - comment=$2 +kind_decls= +kind_printers= - echo " $r, /*! $comment */" - cases="$cases case $r: out << \"$r\"; break; -" +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 + register_kind "$1" 0 "$2" } function operator { - special "$1" "$2" + # operator K #children ["comment"] + + lineno=${BASH_LINENO[0]} + + check_theory_seen + register_kind "$1" "$2" "$3" } function parameterized { - special "$1" "$2" + # parameterized K #children ["comment"] + + lineno=${BASH_LINENO[0]} + + check_theory_seen + register_kind "$1" "$2" "$3" } function constant { - special "$1" "$3" + # constant K T Hasher header ["comment"] + + lineno=${BASH_LINENO[0]} + + check_theory_seen + register_kind "$1" 0 "$5" +} + +function register_kind { + r=$1 + nc=$2 + comment=$3 + + kind_decls="${kind_decls} $r, /*! $comment */ +" + kind_printers="${kind_printers} case $r: out << \"$r\"; break; +" +} + +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 } -cat "$prologue" while [ $# -gt 0 ]; do - b=$(basename $(dirname "$1")) - echo - echo " /* from $b */" - cases="$cases + kf=$1 + seen_theory=false + b=$(basename $(dirname "$kf")) + kind_decls="${kind_decls} + /* from $b */ +" + kind_printers="${kind_printers} /* from $b */ " - source "$1" + source "$kf" + check_theory_seen shift done -cat "$middle" -echo "$cases" -cat "$epilogue" +check_builtin_theory_seen + +## output + +text=$(cat "$template") +for var in kind_decls kind_printers; 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" |