diff options
Diffstat (limited to 'src/expr/mkexpr')
-rwxr-xr-x | src/expr/mkexpr | 177 |
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" |