diff options
Diffstat (limited to 'src/expr/mkkind')
-rwxr-xr-x | src/expr/mkkind | 98 |
1 files changed, 88 insertions, 10 deletions
diff --git a/src/expr/mkkind b/src/expr/mkkind index fa80894b2..08d874c79 100755 --- a/src/expr/mkkind +++ b/src/expr/mkkind @@ -4,8 +4,8 @@ # Morgan Deters <mdeters@cs.nyu.edu> for CVC4 # Copyright (c) 2010-2011 The CVC4 Project # -# The purpose of this script is to create kind.h from a template and a -# list of theory kinds. +# The purpose of this script is to create kind.h (and also +# type_properties.h) from a template and a list of theory kinds. # # Invocation: # @@ -16,9 +16,11 @@ copyright=2010-2011 +filename=`basename "$1" | sed 's,_template,,'` + cat <<EOF /********************* */ -/** kind.h +/** $filename ** ** Copyright $copyright The AcSys Group, New York University, and as below. ** @@ -29,6 +31,23 @@ cat <<EOF ** for the CVC4 project. **/ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ + +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ + +/* Edit the template file instead: */ +/* $1 */ + EOF me=$(basename "$0") @@ -42,6 +61,9 @@ kind_to_theory_id= type_constant_descriptions= type_constant_list= type_constant_to_theory_id= +type_cardinalities= +type_constant_cardinalities= +type_cardinalities_includes= seen_theory=false seen_theory_builtin=false @@ -89,6 +111,7 @@ function endtheory { # endtheory lineno=${BASH_LINENO[0]} check_theory_seen + seen_endtheory=true } function rewriter { @@ -98,10 +121,17 @@ function rewriter { } function sort { - # sort TYPE ["comment"] + # sort TYPE cardinality ["comment"] lineno=${BASH_LINENO[0]} check_theory_seen - register_sort "$1" "$2" + register_sort "$1" "$2" "$3" +} + +function cardinality { + # cardinality TYPE cardinality-computer [header] + lineno=${BASH_LINENO[0]} + check_theory_seen + register_cardinality "$1" "$2" "$3" } function variable { @@ -142,14 +172,33 @@ function constant { function register_sort { id=$1 - comment=$2 + cardinality=$2 + comment=$3 type_constant_list="${type_constant_list} ${id}, /**< ${comment} */ " type_constant_descriptions="${type_constant_descriptions} case $id: out << \"${comment}\"; break; " - type_constant_to_theory_id="${type_constant_to_theory_id} case $id: return $theory_id; break; + type_constant_to_theory_id="${type_constant_to_theory_id} case $id: return $theory_id; +" + type_constant_cardinalities="${type_constant_cardinalities}#line $lineno \"$kf\" + case $id: return Cardinality($cardinality); +" +} + +function register_cardinality { + id=$1 + cardinality_computer=$(sed 's,%TYPE%,typeNode,g' <<<"$2") + header=$3 + + type_cardinalities="${type_cardinalities}#line $lineno \"$kf\" + case $id: return $cardinality_computer; +" + if [ -n "$header" ]; then + type_cardinalities_includes="${type_cardinalities_includes}#line $lineno \"$kf\" +#include \"$header\" " + fi } function register_kind { @@ -161,11 +210,15 @@ function register_kind { " kind_printers="${kind_printers} case $r: out << \"$r\"; break; " - kind_to_theory_id="${kind_to_theory_id} case kind::$r: return $theory_id; break; + kind_to_theory_id="${kind_to_theory_id} case kind::$r: return $theory_id; " } function check_theory_seen { + if $seen_endtheory; then + echo "$kf:$lineno: error: command after \"endtheory\" declaration (endtheory has to be last)" >&2 + exit 1 + fi if ! $seen_theory; then echo "$kf:$lineno: error: no \"theory\" declaration found (it has to be first)" >&2 exit 1 @@ -181,6 +234,7 @@ function check_builtin_theory_seen { while [ $# -gt 0 ]; do kf=$1 seen_theory=false + seen_endtheory=false b=$(basename $(dirname "$kf")) kind_decls="${kind_decls} /* from $b */ @@ -189,15 +243,39 @@ while [ $# -gt 0 ]; do /* from $b */ " source "$kf" - check_theory_seen + if ! $seen_theory; then + echo "$kf: error: no theory content found in file!" >&2 + exit 1 + fi + if ! $seen_endtheory; then + echo "$kf:$lineno: error: no \"endtheory\" declaration found (it is required at the end)" >&2 + exit 1 + fi shift done check_builtin_theory_seen ## output +# generate warnings about incorrect #line annotations in templates +nl -ba -s' ' "$template" | grep '^ *[0-9][0-9]* # *line' | + awk '{OFS="";if($1+1!=$3) print "'"$template"':",$1,": warning: incorrect annotation \"#line ",$3,"\" (it should be \"#line ",($1+1),"\")"}' >&2 + text=$(cat "$template") -for var in kind_decls kind_printers kind_to_theory_id theory_enum type_constant_list type_constant_descriptions type_constant_to_theory_id theory_descriptions; do +for var in \ + kind_decls \ + kind_printers \ + kind_to_theory_id \ + theory_enum \ + type_constant_list \ + type_constant_descriptions \ + type_constant_to_theory_id \ + type_cardinalities \ + type_constant_cardinalities \ + type_cardinalities_includes \ + theory_descriptions \ + template \ + ; do eval text="\${text//\\\$\\{$var\\}/\${$var}}" done error=`expr "$text" : '.*\${\([^}]*\)}.*'` |