diff options
Diffstat (limited to 'src/options/mkoptions')
-rwxr-xr-x | src/options/mkoptions | 1260 |
1 files changed, 1260 insertions, 0 deletions
diff --git a/src/options/mkoptions b/src/options/mkoptions new file mode 100755 index 000000000..2bfd6a2d9 --- /dev/null +++ b/src/options/mkoptions @@ -0,0 +1,1260 @@ +#!/bin/bash +# +# mkoptions +# Morgan Deters <mdeters@cs.nyu.edu> for CVC4 +# Copyright (c) 2011 The CVC4 Project +# +# The purpose of this script is to create options.{h,cpp} +# from template files and a list of options. +# +# Invocation: +# +# mkoptions (template-file output-file)+ -t options.h-template options.cpp-template (options-file output-dir)+ +# + +copyright=2011 + +me=$(basename "$0") + +function usage { + echo "usage: $me (template-file output-file)+ -t options.h-template options.cpp-template (options-file output-dir)+" >&2 +} + +declare -a templates +declare -a outputs + +while [ "$1" != -t ]; do + if [ "$#" -lt 2 ]; then + echo "$me: error: expected -t on command line" >&2 + usage + exit 1 + fi + templates[${#templates[@]}]="$1"; shift + if [ "$1" = -t ]; then + echo "$me: error: mismatched number of templates and output files (before -t)" >&2 + usage + exit 1 + fi + outputs[${#outputs[@]}]="$1"; shift +done + +shift +if [ "$#" -lt 3 ]; then + echo "$me: error: not enough arguments" >&2 + usage + exit 1 +fi + +options_h_template="$1"; shift +options_cpp_template="$1"; shift + +all_modules_defaults= +all_modules_short_options= +all_modules_long_options= +all_modules_option_handlers= +smt_getoption_handlers= +smt_setoption_handlers= +include_all_option_headers= +all_modules_contributions= +option_handler_includes= +all_custom_handlers= +common_documentation= +remaining_documentation= +common_manpage_documentation= +remaining_manpage_documentation= + +seen_module=false +seen_endmodule=false +expect_doc=false +expect_doc_alternate=false +n_long=256 + +internal= +smtname= +short_option= +short_option_alternate= +long_option= +long_option_alternate= +long_option_alternate_set= +type= +predicates= + +# just for duplicates-checking +all_declared_internal_options= +all_declared_long_options= +all_declared_short_options= +all_declared_smt_options= + +long_option_value_begin=$n_long + +function module { + # module id name + + module_id= + module_name= + module_includes= + module_optionholder_spec= + module_decls= + module_specializations= + module_inlines= + module_accessors= + module_global_definitions= + + seen_module=true + if [ $# -lt 3 -o -z "$1" -o -z "$2" -o -z "$3" ]; then + echo "$kf:$lineno: error: \"module\" directive requires exactly three arguments" >&2 + exit 1 + fi + + module_id="$1"; shift + include="$1"; shift + module_name="$@" + include_all_option_headers="${include_all_option_headers} +#line $lineno \"$kf\" +#include $(check_include "$include")" + all_modules_contributions="${all_modules_contributions} + CVC4_OPTIONS__${module_id}__FOR_OPTION_HOLDER" + module_optionholder_spec="#define CVC4_OPTIONS__${module_id}__FOR_OPTION_HOLDER" + + remaining_documentation="${remaining_documentation}\\n\\n\" +#line $lineno \"$kf\" +\"$module_name options:" + remaining_manpage_documentation="${remaining_manpage_documentation} +.SH `echo "$module_name" | tr a-z A-Z` OPTIONS +" +} + +function endmodule { + # endmodule + check_module_seen + check_doc + seen_endmodule=true + if [ $# -ne 0 ]; then + echo "$kf:$lineno: error: endmodule takes no arguments" >&2 + exit 1 + fi +} + +function common-option { + # common-option option-args... + handle_option COMMON "$@" +} + +function option { + # option option-args... + handle_option STANDARD "$@" +} + +function expert-option { + # expert-option option-args... + handle_option EXPERT "$@" +} + +function undocumented-option { + # undocumented-option option-args... + handle_option UNDOCUMENTED "$@" +} + +function handle_option { + check_module_seen + check_doc + + args=("$@") + + category="${args[0]}" + internal="${args[1]}" + smtname= + short_option= + short_option_alternate= + long_option= + long_option_alternate= + long_option_alternate_set= + type= + readOnly=true + required_argument=false + default_value= + handlers= + predicates= + links= + links_alternate= + + options_already_documented=false + alternate_options_already_documented=false + + if [ "$category" = UNDOCUMENTED ]; then + expect_doc=false + else + expect_doc=true + fi + expect_doc_alternate=false + + # scan ahead to see where the type is + type_pos=2 + while [ $(($type_pos+1)) -lt ${#args[@]} ] && ! expr "${args[$(($type_pos+1))]}" : ":" &>/dev/null; do + let ++type_pos + done + + type="${args[$type_pos]}" + + if [ "$type" = argument ]; then + type=void + required_argument=true + fi + + if [ $type_pos -eq 2 ]; then + expect_doc=false + readOnly=false + else + i=2 + while [ $i -lt $type_pos ]; do + if expr "${args[$i]}" : '--' &>/dev/null || expr "${args[$i]}" : '/--' &>/dev/null; then + if [ -n "$long_option" -o -n "$long_option_alternate" ]; then + echo "$kf:$lineno: error: malformed option line for \`$internal': unexpected \`${args[$i]}'" >&2 + exit 1 + fi + long_option="$(echo "${args[$i]}" | sed 's,/.*,,')" + if [ -n "$long_option" ]; then + if ! expr "$long_option" : '--.' &>/dev/null; then + echo "$kf:$option: bad long option \`$long_option': expected something like \`--foo'" >&2 + exit 1 + fi + long_option="$(echo "$long_option" | sed 's,^--,,')" + fi + if expr "${args[$i]}" : '.*/' &>/dev/null; then + long_option_alternate="$(echo "${args[$i]}" | sed 's,[^/]*/,,')" + long_option_alternate_set=set + if [ -n "$long_option_alternate" ]; then + if ! expr "$long_option_alternate" : '--.' &>/dev/null; then + echo "$kf:$option: bad alternate long option \`$long_option_alternate': expected something like \`--foo'" >&2 + exit 1 + fi + long_option_alternate="$(echo "$long_option_alternate" | sed 's,^--,,')" + fi + fi + elif expr "${args[$i]}" : '-' &>/dev/null || expr "${args[$i]}" : '/-' &>/dev/null; then + if [ -n "$short_option" -o -n "$short_option_alternate" -o -n "$long_option" -o -n "$long_option_alternate" ]; then + echo "$kf:$lineno: error: malformed option line for \`$internal': unexpected \`${args[$i]}'" >&2 + exit 1 + fi + short_option="$(echo "${args[$i]}" | sed 's,/.*,,')" + if [ -n "$short_option" ]; then + if ! expr "$short_option" : '-.$' &>/dev/null; then + echo "$kf:$option: bad short option \`$short_option': expected something like \`-x'" >&2 + exit 1 + fi + short_option="$(echo "$short_option" | sed 's,^-,,')" + fi + if expr "${args[$i]}" : '.*/' &>/dev/null; then + short_option_alternate="$(echo "${args[$i]}" | sed 's,[^/]*/,,')" + if expr "$short_option_alternate" : - &>/dev/null; then + if ! expr "$short_option_alternate" : '-.$' &>/dev/null; then + echo "$kf:$option: bad alternate short option \`$short_option_alternate': expected something like \`-x'" >&2 + exit 1 + fi + short_option_alternate="$(echo "$short_option_alternate" | sed 's,^-,,')" + fi + fi + else + if [ -n "$smtname" -o -n "$short_option" -o -n "$short_option_alternate" -o -n "$long_option" -o -n "$long_option_alternate" ]; then + echo "$kf:$lineno: error: malformed option line for \`$internal': unexpected \`${args[$i]}'" >&2 + exit 1 + fi + smtname="${args[$i]}" + fi + let ++i + done + fi + + if [ "$type" = void -a "$internal" != - ]; then + echo "$kf:$lineno: error: $internal cannot be void-typed; use \`-' as the name if its to be void" >&2 + exit 1 + elif [ "$type" != void -a "$internal" = - ]; then + echo "$kf:$lineno: error: cannot use an unnamed option if its type is not void" >&2 + exit 1 + fi + + if [ "$type" = bool -a -n "$long_option$short_option" -a "$category" != UNDOCUMENTED ]; then + if [ -n "$short_option_alternate" -o -n "$long_option_alternate" ]; then + expect_doc_alternate=true + fi + fi + if [ "$type" = bool -a -n "$long_option" -a -z "$long_option_alternate" -a -z "$long_option_alternate_set" ]; then + long_option_alternate="no-$(echo "$long_option" | sed 's,^--,,')" + fi + if [ "$type" != bool -a -n "$short_option_alternate" ]; then + echo "$kf:$lineno: error: cannot use alternate short option -$short_option_alternate for \`$internal' because it's not of bool type" >&2 + exit 1 + elif [ "$type" != bool -a -n "$long_option_alternate" ]; then + echo "$kf:$lineno: error: cannot use alternate long option --$long_option_alternate for \`$internal' because it's not of bool type" >&2 + exit 1 + fi + + # check for duplicates + if [ "$internal" != - ]; then + if echo " $all_declared_internal_options " | grep -q " $internal "; then + echo "$kf:$lineno: error: internal option name \`$internal' previously declared" >&2 + exit 1 + fi + all_declared_internal_options="$all_declared_internal_options $internal" + fi + if [ -n "$long_option" ]; then + if echo " $all_declared_long_options " | grep -q " $long_option "; then + echo "$kf:$lineno: error: long option name \`--$long_option' previously declared" >&2 + exit 1 + fi + all_declared_long_options="$all_declared_long_options $long_option" + fi + if [ -n "$long_option_alternate" ]; then + if echo " $all_declared_long_options " | grep -q " $long_option_alternate "; then + echo "$kf:$lineno: error: long option name \`--$long_option_alternate' previously declared" >&2 + exit 1 + fi + all_declared_long_options="$all_declared_long_options $long_option_alternate" + fi + if [ -n "$short_option" ]; then + if echo " $all_declared_short_options " | grep -q " $short_option "; then + echo "$kf:$lineno: error: short option name \`-$short_option' previously declared" >&2 + exit 1 + fi + all_declared_short_options="$all_declared_short_options $short_option" + fi + if [ -n "$short_option_alternate" ]; then + if echo " $all_declared_short_options " | grep -q " $short_option_alternate "; then + echo "$kf:$lineno: error: short option name \`-$short_option_alternate' previously declared" >&2 + exit 1 + fi + all_declared_short_options="$all_declared_short_options $short_option_alternate" + fi + if [ -n "$smtname" ]; then + if echo " $all_declared_smt_options " | grep -q " $smtname "; then + echo "$kf:$lineno: error: SMT option name \`$smtname' previously declared" >&2 + exit 1 + fi + all_declared_smt_options="$all_declared_smt_options $smtname" + fi + + # parse attributes + i=$(($type_pos+1)) + while [ $i -lt ${#args[@]} ]; do + attribute="${args[$i]}" + case "$attribute" in + :default) + let ++i + default_value="${args[$i]}" + ;; + :handler) + let ++i + if [ -n "$handlers" ]; then + echo "$kf:$lineno: error: cannot specify more than one handler; maybe you want a :handler and a :predicate" >&2 + exit 1 + fi + handlers="${args[$i]}" + ;; + :predicate) + while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : ":" &>/dev/null; do + let ++i + predicates="${predicates} ${args[$i]}" + done + ;; + :link) + while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : ":" &>/dev/null; do + let ++i + link="${args[$i]}" + if expr "${args[$i]}" : '.*/' &>/dev/null; then + links="${links} $(echo "${args[$i]}" | sed 's,/.*,,')" + links_alternate="${links_alternate} $(echo "${args[$i]}" | sed 's,[^/]*/,,')" + else + links="${links} ${args[$i]}" + links_alternate="${links_alternate} ${args[$i]}" + fi + done + ;; + :include) + while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : ":" &>/dev/null; do + let ++i + module_includes="${module_includes} +#line $lineno \"$kf\" +#include $(check_include "${args[$i]}")" + done + ;; + :handler-include|:predicate-include) + while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : ":" &>/dev/null; do + let ++i + option_handler_includes="${option_handler_includes} +#line $lineno \"$kf\" +#include $(check_include "${args[$i]}")" + done + ;; + :read-write) + readOnly=false + ;; + :read-only) + readOnly=true + ;; + *) + echo "$kf:$lineno: error in option \`$internal': bad attribute \`$attribute'" >&2 + exit 1 + esac + let ++i + done + + # set up structures + if [ "$internal" != - ]; then + # set up a field in the options_holder + module_optionholder_spec="${module_optionholder_spec} \\ + ${internal}__option_t::type $internal; \\ + bool ${internal}__setByUser__;" + all_modules_defaults="${all_modules_defaults:+${all_modules_defaults},} +#line $lineno \"$kf\" + $internal($default_value), +#line $lineno \"$kf\" + ${internal}__setByUser__(false)" + if $readOnly; then + module_decls="${module_decls} +#line $lineno \"$kf\" +extern struct CVC4_PUBLIC ${internal}__option_t { typedef $type type; type operator()() const; bool wasSetByUser() const; } $internal CVC4_PUBLIC;" + module_inlines="${module_inlines} +#line $lineno \"$kf\" +inline ${internal}__option_t::type ${internal}__option_t::operator()() const { return Options::current()[*this]; } +#line $lineno \"$kf\" +inline bool ${internal}__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); } +" + else + module_decls="${module_decls} +#line $lineno \"$kf\" +extern struct CVC4_PUBLIC ${internal}__option_t { typedef $type type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } $internal CVC4_PUBLIC;" + module_inlines="${module_inlines} +#line $lineno \"$kf\" +inline ${internal}__option_t::type ${internal}__option_t::operator()() const { return Options::current()[*this]; } +#line $lineno \"$kf\" +inline bool ${internal}__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); } +#line $lineno \"$kf\" +inline void ${internal}__option_t::set(const ${internal}__option_t::type& v) { Options::current().set(*this, v); } +" + module_specializations="${module_specializations} +#line $lineno \"$kf\" +template <> void Options::set(options::${internal}__option_t, const options::${internal}__option_t::type& x);" + module_accessors="${module_accessors} +#line $lineno \"$kf\" +template <> void Options::set(options::${internal}__option_t, const options::${internal}__option_t::type& x) { d_holder->$internal = x; }" + fi + module_global_definitions="${module_global_definitions} +#line $lineno \"$kf\" +struct ${internal}__option_t $internal;" + module_specializations="${module_specializations} +#line $lineno \"$kf\" +template <> const options::${internal}__option_t::type& Options::operator[](options::${internal}__option_t) const; +#line $lineno \"$kf\" +template <> bool Options::wasSetByUser(options::${internal}__option_t) const;" + if [ "$type" = bool ]; then + module_specializations="${module_specializations} +#line $lineno \"$kf\" +template <> void Options::assignBool(options::${internal}__option_t, std::string option, bool value, SmtEngine* smt);" + elif [ "$internal" != - ]; then + module_specializations="${module_specializations} +#line $lineno \"$kf\" +template <> void Options::assign(options::${internal}__option_t, std::string option, std::string value, SmtEngine* smt);" + fi + + module_accessors="${module_accessors} +#line $lineno \"$kf\" +template <> const options::${internal}__option_t::type& Options::operator[](options::${internal}__option_t) const { return d_holder->$internal; } +#line $lineno \"$kf\" +template <> bool Options::wasSetByUser(options::${internal}__option_t) const { return d_holder->${internal}__setByUser__; }" + fi + + if $required_argument || [ "$type" != bool -a "$type" != void ]; then + expect_arg=: + expect_arg_long=required_argument + else + expect_arg= + expect_arg_long=no_argument + fi + cases= + cases_alternate= + if [ -n "$short_option" ]; then + all_modules_short_options="${all_modules_short_options}$short_option$expect_arg" + cases="${cases} + case '$short_option':" + fi + if [ -n "$short_option_alternate" ]; then + all_modules_short_options="${all_modules_short_options}$short_option_alternate$expect_arg" + cases_alternate="${cases_alternate} + case '$short_option_alternate':" + fi + if [ -n "$long_option" ]; then + all_modules_long_options="${all_modules_long_options} + { \"$(echo "$long_option" | sed 's,=.*,,')\", $expect_arg_long, NULL, $n_long }," + cases="${cases} + case $n_long:// --$long_option" + let ++n_long + fi + if [ -n "$long_option_alternate" ]; then + all_modules_long_options="${all_modules_long_options} + { \"$(echo "$long_option_alternate" | sed 's,=.*,,')\", $expect_arg_long, NULL, $n_long }," + cases_alternate="${cases_alternate} + case $n_long:// --$long_option_alternate" + let ++n_long + fi + run_links= + run_links_alternate= + if [ -n "$links" ]; then + for link in $links; do + run_links="$run_links +#line $lineno \"$kf\" + preemptGetopt(extra_argc, extra_argv, \"$link\");" + done + fi + if [ -n "$links_alternate" ]; then + for link in $links_alternate; do + run_links_alternate="$run_links_alternate +#line $lineno \"$kf\" + preemptGetopt(extra_argc, extra_argv, \"$link\");" + done + fi + if [ "$type" = bool -a -n "$cases" -o -n "$cases_alternate" ]; then + run_handlers= + if [ -n "$handlers" ]; then + echo "$kf:$lineno: error: bool-valued options cannot have handlers" >&2 + exit 1 + fi + if [ -n "$predicates" ]; then + for predicate in $predicates; do + run_handlers="$run_handlers +#line $lineno \"$kf\" + $predicate(option, b, smt);" + done + fi + if [ -n "$run_handlers" ]; then + all_custom_handlers="${all_custom_handlers} +#line $lineno \"$kf\" +template <> void runBoolPredicates(options::${internal}__option_t, std::string option, bool b, SmtEngine* smt) { + $run_handlers +}" + fi + fi + if [ -n "$cases" ]; then + if [ "$type" = bool ]; then + all_modules_option_handlers="${all_modules_option_handlers}${cases} +#line $lineno \"$kf\" + assignBool(options::$internal, argv[old_optind == 0 ? 1 : old_optind], true, NULL);$run_links + break; +" + elif [ -n "$expect_arg" -a "$internal" != - ]; then + run_handlers= + if [ -n "$handlers" ]; then + for handler in $handlers; do + run_handlers="$run_handlers +#line $lineno \"$kf\" + $handler(option, optarg, smt);" + done + else + run_handlers=" +#line $lineno \"$kf\" + handleOption<$type>(option, optarg);" + fi + if [ -n "$predicates" ]; then + for predicate in $predicates; do + run_handlers="$run_handlers +#line $lineno \"$kf\" + $predicate(option, retval, smt);" + done + fi + all_custom_handlers="${all_custom_handlers} +#line $lineno \"$kf\" +template <> options::${internal}__option_t::type runHandlerAndPredicates(options::${internal}__option_t, std::string option, std::string optarg, SmtEngine* smt) { +#line $lineno \"$kf\" + options::${internal}__option_t::type retval = $run_handlers +#line $lineno \"$kf\" + return retval; +}" + all_modules_option_handlers="${all_modules_option_handlers}${cases} +#line $lineno \"$kf\" + assign(options::$internal, argv[old_optind == 0 ? 1 : old_optind], optarg, NULL);$run_links + break; +" + elif [ -n "$expect_arg" ]; then + run_handlers= + if [ -n "$predicates" ]; then + echo "$kf:$lineno: error: void-valued options cannot have predicates" >&2 + exit 1 + fi + if [ -n "$handlers" ]; then + for handler in $handlers; do + run_handlers="$run_handlers +#line $lineno \"$kf\" + $handler(argv[old_optind == 0 ? 1 : old_optind], optarg, smt);" + done + fi + all_modules_option_handlers="${all_modules_option_handlers}${cases} +#line $lineno \"$kf\" + $run_handlers$run_links + break; +" + else + run_handlers= + if [ -n "$predicates" ]; then + echo "$kf:$lineno: error: void-valued options cannot have predicates" >&2 + exit 1 + fi + if [ -n "$handlers" ]; then + for handler in $handlers; do + run_handlers="$run_handlers +#line $lineno \"$kf\" + $handler(argv[old_optind == 0 ? 1 : old_optind], smt);" + done + fi + all_modules_option_handlers="${all_modules_option_handlers}${cases} +#line $lineno \"$kf\" + $run_handlers$run_links + break; +" + fi + fi + if [ -n "$cases_alternate" ]; then + if [ "$type" = bool ]; then + all_modules_option_handlers="${all_modules_option_handlers}${cases_alternate} +#line $lineno \"$kf\" + assignBool(options::$internal, argv[old_optind == 0 ? 1 : old_optind], false, NULL);$run_links_alternate + break; +" + else + echo "$kf:$lineno: internal error: expected BOOL-typed option in alternate handler" >&2 + exit 1 + fi + fi + + if [ -n "$smtname" ]; then + if [ "$internal" != - ]; then + smt_getoption_handlers="${smt_getoption_handlers} +#line $lineno \"$kf\" + if(key == \"$smtname\") { +#line $lineno \"$kf\" + stringstream ss; ss << options::$internal(); + return SExpr(ss.str()); + }" + fi + + if [ "$type" = bool ]; then + smt_setoption_handlers="${smt_setoption_handlers} +#line $lineno \"$kf\" + if(key == \"$smtname\") { +#line $lineno \"$kf\" + Options::current().assignBool(options::$internal, \"$smtname\", optarg == \"true\", smt);$run_links + return; + }" + elif [ -n "$expect_arg" -a "$internal" != - ]; then + run_handlers= + if [ -n "$handlers" ]; then + for handler in $handlers; do + run_handlers="$run_handlers +#line $lineno \"$kf\" + $handler(\"$smtname\", value, smt); +" + done + fi + smt_setoption_handlers="${smt_setoption_handlers} +#line $lineno \"$kf\" + if(key == \"$smtname\") { +#line $lineno \"$kf\" + Options::current().assign(options::$internal, \"$smtname\", optarg, smt);$run_links + return; + }" + elif [ -n "$expect_arg" ]; then + run_handlers= + for handler in $handlers; do + run_handlers="$run_handlers +#line $lineno \"$kf\" + $handler(\"$smtname\", value, smt); +" + done + smt_setoption_handlers="${smt_setoption_handlers} +#line $lineno \"$kf\" + if(key == \"$smtname\") { +#line $lineno \"$kf\" + $run_handlers$run_links + return; + }" + else + run_handlers= + for handler in $handlers; do + run_handlers="$run_handlers +#line $lineno \"$kf\" + $handler(\"$smtname\", smt); +" + done + smt_setoption_handlers="${smt_setoption_handlers} +#line $lineno \"$kf\" + if(key == \"$smtname\") { +#line $lineno \"$kf\" + $run_handlers$run_links + return; + }" + fi + fi + + if [ "$type" = bool ]; then + # emit assignBool/assign + all_custom_handlers="${all_custom_handlers} +#line $lineno \"$kf\" +template <> void Options::assignBool(options::${internal}__option_t, std::string option, bool value, SmtEngine* smt) { +#line $lineno \"$kf\" + runBoolPredicates(options::$internal, option, value, smt); +#line $lineno \"$kf\" + d_holder->$internal = value; +#line $lineno \"$kf\" + d_holder->${internal}__setByUser__ = true; +#line $lineno \"$kf\" + Trace(\"options\") << \"user assigned option $internal\" << std::endl; +}" + elif [ -n "$expect_arg" -a "$internal" != - ] && [ -n "$cases" -o "$cases_alternate" -o "$smtname" ]; then + all_custom_handlers="${all_custom_handlers} +#line $lineno \"$kf\" +template <> void Options::assign(options::${internal}__option_t, std::string option, std::string value, SmtEngine* smt) { +#line $lineno \"$kf\" + d_holder->$internal = runHandlerAndPredicates(options::$internal, option, value, smt); +#line $lineno \"$kf\" + d_holder->${internal}__setByUser__ = true; +#line $lineno \"$kf\" + Trace(\"options\") << \"user assigned option $internal\" << std::endl; +}" + fi +} + +function alias { + # alias (smtname | -option) = (smtname [arg] | -option [arg])+ + check_module_seen + check_doc + + category=STANDARD + internal=- + smtname= + short_option= + short_option_alternate= + long_option= + long_option_alternate= + long_option_alternate_set= + type=void + readOnly=true + required_argument=false + default_value= + handlers= + predicates= + links= + links_alternate= + + options_already_documented=false + alternate_options_already_documented=false + + if [ $# -lt 3 ]; then + echo "$kf:$lineno: error: malformed \"alias\" command; expected more arguments" >&2 + exit 1 + fi + options= + while [ $# -gt 0 -a "$1" != = ]; do + options="$options $1" + shift + done + if [ $# -eq 0 ]; then + echo "$kf:$lineno: error: malformed \"alias\" command; expected \`='" >&2 + exit 1 + fi + shift + if [ $# -eq 0 ]; then + echo "$kf:$lineno: error: malformed \"alias\" command; expected more arguments" >&2 + exit 1 + fi + cases= + for option in $options; do + if ! expr "$option" : - &>/dev/null; then + echo "$kf:$lineno: error: alias for SMT options not yet supported" >&2 + exit 1 + fi + if expr "$option" : -- &>/dev/null; then + option="$(echo "$option" | sed 's,--,,')" + all_modules_long_options="${all_modules_long_options} + { \"$(echo "$option" | sed 's,=.*,,')\", no_argument, NULL, $n_long }," + cases="${cases} + case $n_long:// --$option" + let ++n_long + long_option="${long_option:+$long_option | --}$option" + else + if ! expr "$option" : '-.$' &>/dev/null; then + echo "$kf:$lineno: error: expected short option specification, got \`$option'" >&2 + exit 1 + fi + option="$(echo "$option" | sed 's,-,,')" + all_modules_short_options="${all_modules_short_options}$option" + cases="${cases} + case '$option':" + short_option="${short_option:+$short_option | -}$option" + fi + done + while [ $# -gt 0 ]; do + links="$links +#line $lineno \"$kf\" + preemptGetopt(extra_argc, extra_argv, \"$1\");" + shift + done + all_modules_option_handlers="$all_modules_option_handlers$cases$links + break; +" + expect_doc=true + expect_doc_alternate=false +} + +function warning { + # warning message + check_module_seen + check_doc + + echo "$kf:$lineno: warning: $@" >&2 +} + +function doc { + # doc text... + check_module_seen + expect_doc=false + + if [ -z "$short_option" -a -z "$long_option" ]; then + if [ -n "$short_option_alternate" -o -n "$long_option_alternate" ]; then + if [ -n "$smtname" ]; then + expect_doc_alternate=true + else + doc-alternate "$@" + return + fi + fi + fi + + if [ "$category" = UNDOCUMENTED ]; then + return + fi + + if ! $options_already_documented; then + options_already_documented=true + the_opt= + if [ "$long_option" ]; then + the_opt="--$long_option" + if [ "$short_option" ]; then + shortoptarg= + if expr "$the_opt" : '.*=' &>/dev/null; then + shortoptarg="$(echo "$the_opt" | sed 's,[^=]*=, ,')" + fi + the_opt="$the_opt | -$short_option$shortoptarg" + fi + elif [ "$short_option" ]; then + the_opt="-$short_option" + fi + if [ -z "$the_opt" ]; then + # nothing to document + return + fi + + the_doc="$@" + if [ "$category" = EXPERT ]; then + the_doc="$the_doc (EXPERTS only)" + fi + + doc_line= + while [ -n "$the_doc" ]; do + remaining_doc="$(expr "$the_doc " : '.\{1,53\} \(.*\)')" + the_doc="$(expr "$the_doc " : '\(.\{1,53\}\) ')" + if [ -z "$doc_line" ]; then + if expr "$the_opt" : '.\{23\}' &>/dev/null; then + # break into two lines + doc_line="$(printf ' %s\\n\\\n%-24s %s' "$the_opt" "" "$the_doc")" + else + doc_line="$(printf ' %-22s %s' "$the_opt" "$the_doc")" + fi + else + doc_line="$doc_line\\n$(printf '%-24s %s' "" "$the_doc")" + fi + the_doc="$(expr "$remaining_doc" : '\(.*\) ')" + done + + if [ "$category" = COMMON ]; then + common_documentation="${common_documentation}\\n\" +#line $lineno \"$kf\" +\"$(echo "$doc_line" | sed 's,'\'',\\'\'',g;s,",\\",g')" + common_manpage_documentation="${common_manpage_documentation} +.IP \"$the_opt\" +$@" + else + remaining_documentation="${remaining_documentation}\\n\" +#line $lineno \"$kf\" +\"$(echo "$doc_line" | sed 's,'\'',\\'\'',g;s,",\\",g')" + remaining_manpage_documentation="${remaining_manpage_documentation} +.IP \"$the_opt\" +$@" + fi + else + if [ "$category" = COMMON ]; then + common_manpage_documentation="${common_manpage_documentation} +$@" + else + remaining_manpage_documentation="${remaining_manpage_documentation} +$@" + fi + fi +} + +function doc-alternate { + # doc-alternate text... + check_module_seen + expect_doc_alternate=false + + if $expect_doc; then + echo "$kf:$lineno: error: must provide documentation before alternate documentation" >&2 + exit 1 + fi + + if [ -z "$short_option_alternate" -a -z "$long_option_alternate" ]; then + echo "$kf:$lineno: cannot document an alternative for option \`$internal'; one does not exist" >&2 + exit 1 + fi + + if [ "$category" = UNDOCUMENTED ]; then + return + fi + + if ! $alternate_options_already_documented; then + alternate_options_already_documented=true + the_opt= + if [ "$long_option_alternate" ]; then + the_opt="--$long_option_alternate" + shortoptarg= + if expr "$the_opt" : '.*=' &>/dev/null; then + shortoptarg="$(echo "$the_opt" | sed 's,[^=]*=, ,')" + fi + if [ "$short_option_alternate" ]; then + the_opt="$the_opt | -$short_option_alternate$shortoptarg" + fi + elif [ "$short_option_alternate" ]; then + the_opt="-$short_option_alternate" + fi + if [ -z "$the_opt" ]; then + # nothing to document + return + fi + + the_doc="$@" + if [ "$category" = EXPERT ]; then + the_doc="$the_doc (EXPERTS only)" + fi + + doc_line= + while [ -n "$the_doc" ]; do + remaining_doc="$(expr "$the_doc " : '.\{1,53\} \(.*\)')" + the_doc="$(expr "$the_doc " : '\(.\{1,53\}\) ')" + if [ -z "$doc_line" ]; then + if expr "$the_opt" : '.\{23\}' &>/dev/null; then + # break into two lines + doc_line="$(printf ' %s\\n\\\n%-24s %s' "$the_opt" "" "$the_doc")" + else + doc_line="$(printf ' %-22s %s' "$the_opt" "$the_doc")" + fi + else + doc_line="$doc_line\\n$(printf '%-24s %s' "" "$the_doc")" + fi + the_doc="$(expr "$remaining_doc" : '\(.*\) ')" + done + + if [ "$category" = COMMON ]; then + common_documentation="${common_documentation}\\n\" +#line $lineno \"$kf\" +\"$(echo "$doc_line" | sed 's,'\'',\\'\'',g;s,",\\",g')" + common_manpage_documentation="${common_manpage_documentation} +.IP \"$the_opt\" +$@" + else + remaining_documentation="${remaining_documentation}\\n\" +#line $lineno \"$kf\" +\"$(echo "$doc_line" | sed 's,'\'',\\'\'',g;s,",\\",g')" + remaining_manpage_documentation="${remaining_manpage_documentation} +.IP \"$the_opt\" +$@" + fi + else + if [ "$category" = COMMON ]; then + common_manpage_documentation="${common_manpage_documentation} +$@" + else + remaining_manpage_documentation="${remaining_manpage_documentation} +$@" + fi + fi +} + +function check_doc { + if $expect_doc; then + if [ "$internal" != - ]; then + echo "$kf:$lineno: warning: $internal is lacking documentation" >&2 + elif [ -n "$long_option" ]; then + echo "$kf:$lineno: warning: option --$long_option is lacking documentation" >&2 + elif [ -n "$short_option" ]; then + echo "$kf:$lineno: warning: option -$short_option is lacking documentation" >&2 + elif [ -n "$smtname" ]; then + echo "$kf:$lineno: warning: SMT option $smtname is lacking documentation" >&2 + fi + expect_doc=false + fi + + if $expect_doc_alternate; then + echo "$kf:$lineno: warning: $internal is lacking documentation for the alternative option(s): $short_option_alternate $long_option_alternate" >&2 + expect_doc_alternate=false + fi +} + +function check_module_seen { + if $seen_endmodule; then + echo "$kf:$lineno: error: command after \"endmodule\" declaration (endmodule has to be last)" >&2 + exit 1 + fi + if ! $seen_module; then + echo "$kf:$lineno: error: no \"module\" declaration found (it has to be first)" >&2 + exit 1 + fi +} + +function check_include { + if ! expr "$1" : '".*"$' &>/dev/null && ! expr "$1" : '<.*>$' &>/dev/null; then + echo "\"$1\"" + else + echo "$1" + fi +} + +function output_module { + template="$1" + output="$2" + + filename="$(basename "$output")" + + #echo "generating module $output from $template" + + # 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 \ + module_id \ + module_name \ + module_includes \ + module_optionholder_spec \ + module_decls \ + module_specializations \ + module_inlines \ + module_accessors \ + module_global_definitions \ + template \ + ; do + eval text="\${text//\\\$\\{$var\\}/\${$var}}" + done + error="$(echo "$text" | grep '.*\${[^}]*}.*' | head -n 1)" + if [ -n "$error" ]; then + error="$(echo "$error" | sed 's,.*\${\([^}]*\)}.*,\1,')" + echo "$template:0: error: undefined replacement \${$error}" >&2 + exit 1 + fi + + ( + + # Output header (if this is a .cpp or .c or .h file) and then the + # processed text + + if expr "$output" : '.*\.cpp$' &>/dev/null || expr "$output" : '.*\.[ch]$' &>/dev/null; then + + cat <<EOF +/********************* */ +/** $filename + ** + ** Copyright $copyright The AcSys Group, New York University, and as below. + ** + ** This file automatically generated by: + ** + ** $0 $@ + ** + ** 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 + fi + + echo "$text" + + ) >"$output.tmp" + + diff -q "$output" "$output.tmp" &>/dev/null || (mv -f "$output.tmp" "$output" && echo "regenerated $output") + rm -f "$output.tmp" +} + +while [ $# -gt 0 ]; do + kf="$1"; shift + if [ $# -eq 0 ]; then + echo "$me: error: mismatched number of templates and output files (before -t)" >&2 + usage + exit 1 + fi + outdir="$1"; shift + + #echo "scanning $kf" + + seen_module=false + seen_endmodule=false + b=$(basename $(dirname "$kf")) + lineno=0 + # IFS= forces read to read an entire line + while IFS= read -r line; do + let ++lineno + # read any continuations of the line + while expr "$line" : '.*\\$' &>/dev/null; do + IFS= read -r line2 + line="$(echo "$line" | sed 's,\\$,,')$line2" + let ++lineno + done + if expr "$line" : '[ ].*' &>/dev/null; then + doc "$(echo "$line" | sed 's,^[ ],,')" + elif expr "$line" : '\.[ ]*$' &>/dev/null; then + doc "" + elif expr "$line" : '\.' &>/dev/null; then + echo "$kf:$lineno: error: malformed line during processing of option \`$internal': continuation lines should not have content" >&2 + exit 1 + elif expr "$line" : '/.*' &>/dev/null; then + doc-alternate "$(echo "$line" | sed 's,^/,,')" + else + line="$(echo "$line" | sed 's,\([<>&()!?*]\),\\\1,g')" + if ! eval "$line"; then + echo "$kf:$lineno: error was due to evaluation of this line" >&2 + exit 1 + fi + fi + done < "$kf" + if ! $seen_module; then + echo "$kf: error: no module content found in file!" >&2 + exit 1 + fi + if ! $seen_endmodule; then + echo "$kf:$lineno: error: no \"endmodule\" declaration found (it is required at the end)" >&2 + exit 1 + fi + + output_module "$options_h_template" "$outdir/$(basename "$kf").h" + output_module "$options_cpp_template" "$outdir/$(basename "$kf").cpp" +done + +## final outputs + +i=0; while [ $i -lt ${#templates[@]} ]; do + +template="${templates[$i]}" +output="${outputs[$i]}" + +let ++i + +filename="$(basename "$output")" + +#echo "generating $output from $template" + +# 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 + +long_option_value_end=$n_long + +text=$(cat "$template") +for var in \ + all_modules_defaults \ + all_modules_short_options \ + all_modules_long_options \ + all_modules_option_handlers \ + include_all_option_headers \ + all_modules_contributions \ + option_handler_includes \ + all_custom_handlers \ + common_documentation \ + remaining_documentation \ + common_manpage_documentation \ + remaining_manpage_documentation \ + smt_getoption_handlers \ + smt_setoption_handlers \ + long_option_value_begin \ + long_option_value_end \ + template \ + ; do + eval text="\${text//\\\$\\{$var\\}/\${$var}}" +done +error="$(echo "$text" | grep '.*\${[^}]*}.*' | head -n 1)" +if [ -n "$error" ]; then + error="$(echo "$error" | sed 's,.*\${\([^}]*\)}.*,\1,')" + echo "$template:0: error: undefined replacement \${$error}" >&2 + exit 1 +fi + +( + +# Output header (if this is a .cpp or .c or .h file) and then the +# processed text + +if expr "$output" : '.*\.cpp$' &>/dev/null || expr "$output" : '.*\.[ch]$' &>/dev/null; then + +cat <<EOF +/********************* */ +/** $filename + ** + ** Copyright $copyright The AcSys Group, New York University, and as below. + ** + ** This file automatically generated by: + ** + ** $0 $@ + ** + ** 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 +fi + +echo "$text" + +) >"$output.tmp" + +diff -q "$output" "$output.tmp" &>/dev/null || (mv -f "$output.tmp" "$output" && echo "regenerated $output") +rm -f "$output.tmp" + +done + |