diff options
Diffstat (limited to 'src/expr/mkmetakind')
| -rwxr-xr-x | src/expr/mkmetakind | 248 |
1 files changed, 248 insertions, 0 deletions
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind new file mode 100755 index 000000000..15551d54d --- /dev/null +++ b/src/expr/mkmetakind @@ -0,0 +1,248 @@ +#!/bin/bash +# +# mkmetakind +# Morgan Deters <mdeters@cs.nyu.edu> for CVC4 +# Copyright (c) 2010 The CVC4 Project +# +# The purpose of this script is to create metakind.h from a prologue, +# two middle sections, epilogue, and a list of theory kinds. +# +# This is kept distinct from kind.h because kind.h is a public header +# and metakind.h is intended for the expr package only. +# +# Invocation: +# +# mkmetakind prologue-file middle1-file middle2-file epilogue-file theory-kind-files... +# +# Output is to standard out. +# + +copyright=2010 + +cat <<EOF +/********************* -*- C++ -*- */ +/** metakind.h + ** + ** Copyright $copyright The AcSys Group, New York University, and as below. + ** + ** This header file automatically generated by: + ** + ** $0 $@ + ** + ** for the CVC4 project. + **/ + +EOF + +me=$(basename "$0") + +template=$1; shift + +metakind_includes= +metakind_kinds= +metakind_constantMaps= +metakind_compares= +metakind_constHashes= +metakind_constPrinters= +metakind_ubchildren= +metakind_lbchildren= + +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 + + theory_class=$1 + if [ "$1" != builtin ]; then + metakind_includes="${metakind_includes} +// #include \"theory/$b/$2\"" + fi +} + +function variable { + # variable K ["comment"] + + lineno=${BASH_LINENO[0]} + + check_theory_seen + register_metakind VARIABLE "$1" 0 +} + +function operator { + # operator K #children ["comment"] + + lineno=${BASH_LINENO[0]} + + check_theory_seen + register_metakind OPERATOR "$1" "$2" +} + +function parameterized { + # parameterized K #children ["comment"] + + lineno=${BASH_LINENO[0]} + + check_theory_seen + register_metakind PARAMETERIZED "$1" "$2" +} + +function constant { + # constant K T Hasher header ["comment"] + + lineno=${BASH_LINENO[0]} + + check_theory_seen + + if ! expr "$2" : '\(::*\)' >/dev/null; then + echo "$kf:$lineno: warning: constant $1 class \`$2' isn't fully-qualified (e.g., ::CVC4::Rational)" >&2 + fi + if ! expr "$3" : '\(::*\)' >/dev/null; then + echo "$kf:$lineno: warning: constant $1 hasher \`$3' isn't fully-qualified (e.g., ::CVC4::RationalHashFcn)" >&2 + fi + + if [ -n "$4" ]; then + metakind_includes="${metakind_includes} +#include \"$4\"" + fi + register_metakind CONSTANT "$1" 0 + metakind_constantMaps="${metakind_constantMaps} +}/* CVC4::kind::metakind namespace */ +}/* CVC4::kind namespace */ + +namespace expr { + +template <> +inline const $2 & NodeValue::getConst< $2 >() const { + Assert(getKind() == ::CVC4::kind::$1); + // To support non-inlined CONSTANT-kinded NodeValues (those that are + // \"constructed\" when initially checking them against the NodeManager + // pool), we must check d_nchildren here. + return d_nchildren == 0 + ? *reinterpret_cast< const $2 * >(d_children) + : *reinterpret_cast< const $2 * >(d_children[0]); +} + +}/* CVC4::expr namespace */ + +namespace kind { +namespace metakind { + +template <> +struct ConstantMap< $2 > { + // typedef $theory_class OwningTheory; + enum { kind = ::CVC4::kind::$1 }; +};/* ConstantMap< $2 > */ + +template <> +struct ConstantMapReverse< ::CVC4::kind::$1 > { + typedef $2 T; +};/* ConstantMapReverse< ::CVC4::kind::$1 > */ + +" + metakind_compares="${metakind_compares} + case kind::$1: + return NodeValueConstCompare< kind::$1, pool >::compare(nv1, nv2); +" + metakind_constHashes="${metakind_constHashes} + case kind::$1: + return $3::hash(nv->getConst< $2 >()); +" + metakind_constPrinters="${metakind_constPrinters} + case kind::$1: + out << nv->getConst< $2 >(); + break; +" +} + +function register_metakind { + mk=$1 + k=$2 + nc=$3 + metakind_kinds="${metakind_kinds} metakind::$mk, /* $k */ +"; + + # figure out the range given by $nc + if expr "$nc" : '^[0-9]\+$' >/dev/null; then + lb=$nc + ub=$nc + elif expr "$nc" : '^[0-9]\+:$' >/dev/null; then + let `echo "$nc" | awk 'BEGIN{FS=":"}{print"lb="$1}'` + ub=MAX_CHILDREN + elif expr "$nc" : '^[0-9]\+:[0-9]\+$' >/dev/null; then + let `echo "$nc" | awk 'BEGIN{FS=":"}{print"lb="$1" ub="$2}'` + if [ $ub -lt $lb ]; then + echo "$kf:$lineno: error in range \`$nc': LB < UB (in definition of $k)" >&2 + exit 1 + fi + else + echo "$kf:$lineno: can't parse range \`$nc' in definition of $k" >&2 + exit 1 + fi + + metakind_lbchildren="${metakind_lbchildren} + $lb, /* $k */" + metakind_ubchildren="${metakind_ubchildren} + $ub, /* $k */" +} + +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")) + metakind_kinds="${metakind_kinds} + /* from $b */ +" + source "$kf" + check_theory_seen + shift +done +check_builtin_theory_seen + +## output + +text=$(cat "$template") +for var in metakind_includes metakind_kinds metakind_constantMaps \ + metakind_compares metakind_constHashes metakind_constPrinters \ + metakind_ubchildren metakind_lbchildren; 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" |