path: root/src/options/mkoptions

#!/bin/bash
#
# mkoptions
# Morgan Deters <mdeters@cs.nyu.edu> for CVC4
# Tim King <taking@google.com> for CVC4
# Copyright (c) 2011-2015  The CVC4 Project
#
# Invocation:
#
#   mkoptions module-sed options-file
#   mkoptions summary-sed (options-file)*
#   mkoptions template-sed template-file
#   mkoptions apply-sed-files-to-template template-file (sed-file)*
#
# The primary purpose of this script is to create options/*_options.{h,cpp}
# from template files and a list of options. This additionally generates
# the several documentation files, option_handler_get_option.cpp,
# option_handler_set_option.cpp, and options_holder.{h,cpp}. This script can in
# broad terms be thought of as an interpreter for a domain specific language
# within bash.
#
# The process for generating the files is as follows.
# 1) Scan all of the option files that are of interest.
#    For an options.h file this is a single option file. For the system wide
#    aggregates, like documentation, this is all of the option files.
#
# 2) Each option file is effectively a bash script. To oversimplify, each line
#    in the file corresponds to executing a command in this file.
#    The side effect of running the bash script is to populate the internal
#    variables of this script.
#    See the "eval" call in scan_module to see how internal functions are
#    called.
# 
# 3) The internal variables are then compiled into a map from variables to
#    string values. These maps are printed to standard output. This output
#    is a valid sed file.
#
# 4) These sed maps are then applied to templates files to generate the final
#    output files.
#
# Example of generating a module:
#   mkoptions module-sed src/options/base_options.h src/theory

copyright=2011-2015

me=$(basename "$0")

function usage {
  echo "usage: $me module-sed options-file" >&2
  echo "usage: $me summary-sed (options-file)*" >&2
  echo "usage: $me template-sed template-file" >&2
  echo "usage: $me apply-sed-files-to-template template-file (sed-file)*" >&2
}

# progress_char=/
# if [ -t 1 ]; then r="\r"; else r=""; fi
# function progress {
#   file="$(expr "$1" : '.*\(.................................................................\)')"
#   if [ -z "$file" ]; then file="$1"; else file="[...]$file"; fi
#   [ -t 1 ] && printf "$r%c %-70s (%3d%%)" "$progress_char" "$file" "$(($2*100/$3))"
#   progress_char="`echo "$progress_char" | tr -- '-\\\\|/' '\\\\|/-'`"
# }

function NOTE {
  printf "$r%-80s\n" "$kf:$lineno: note: $@" >&2
}

function WARN {
  printf "$r%-80s\n" "$kf:$lineno: warning: $@" >&2
}

function ERR {
  printf "$r%-80s\n" "$kf:$lineno: error: $@" >&2
  exit 1
}


#options_h_template="$1"; shift
#options_cpp_template="$1"; shift

all_modules_defaults=
all_modules_short_options=
all_modules_long_options=
all_modules_smt_options=
all_modules_option_handlers=
all_modules_get_options=
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=
common_manpage_smt_documentation=
remaining_manpage_smt_documentation=
common_manpage_internals_documentation=
remaining_manpage_internals_documentation=

seen_module=false
seen_endmodule=false
expect_doc=false
expect_doc_alternate=false
seen_doc=false
n_long=256

internal=
smtname=
short_option=
short_option_alternate=
long_option=
long_option_alternate=
long_option_alternate_set=
type=
predicates=
notifications=

# 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
    ERR "\"module\" directive requires exactly three arguments"
  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"

  previous_remaining_documentation="${remaining_documentation}"
  remaining_documentation="${remaining_documentation}\\n\\n\"
#line $lineno \"$kf\"
\"From the $module_name module:"
  remaining_documentation_at_start_of_module="${remaining_documentation}"

  previous_remaining_manpage_documentation="${remaining_manpage_documentation}"
  remaining_manpage_documentation="${remaining_manpage_documentation}
.SH `echo "$module_name" | tr a-z A-Z` OPTIONS
"
  remaining_manpage_documentation_at_start_of_module="${remaining_manpage_documentation}"

  previous_remaining_manpage_smt_documentation="${remaining_manpage_smt_documentation}"
  remaining_manpage_smt_documentation="${remaining_manpage_smt_documentation}
.TP
.I \"`echo "$module_name" | tr a-z A-Z` OPTIONS\"
"
  remaining_manpage_smt_documentation_at_start_of_module="${remaining_manpage_smt_documentation}"

  previous_remaining_manpage_internals_documentation="${remaining_manpage_internals_documentation}"
  remaining_manpage_internals_documentation="${remaining_manpage_internals_documentation}
.TP
.I \"`echo "$module_name" | tr a-z A-Z` OPTIONS\"
"
  remaining_manpage_internals_documentation_at_start_of_module="${remaining_manpage_internals_documentation}"
}

function endmodule {
  # endmodule
  check_module_seen
  check_doc
  seen_endmodule=true
  if [ $# -ne 0 ]; then
    ERR "endmodule takes no arguments"
  fi

  # check, and if no documented options, remove the headers

  if [ "$remaining_documentation" = "$remaining_documentation_at_start_of_module" ]; then
    remaining_documentation="$previous_remaining_documentation"
  fi

  if [ "$remaining_manpage_documentation" = "$remaining_manpage_documentation_at_start_of_module" ]; then
    remaining_manpage_documentation="$previous_remaining_manpage_documentation"
  fi

  if [ "$remaining_manpage_smt_documentation" = "$remaining_manpage_smt_documentation_at_start_of_module" ]; then
    remaining_manpage_smt_documentation="$previous_remaining_manpage_smt_documentation"
  fi

  if [ "$remaining_manpage_internals_documentation" = "$remaining_manpage_internals_documentation_at_start_of_module" ]; then
    remaining_manpage_internals_documentation="$previous_remaining_manpage_internals_documentation"
  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=
  notifications=
  links=
  links_alternate=
  smt_links=

  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
  seen_doc=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
          ERR "malformed option line for \`$internal': unexpected \`${args[$i]}'"
        fi
        long_option="$(echo "${args[$i]}" | sed 's,/.*,,')"
        if [ -n "$long_option" ]; then
          if ! expr "$long_option" : '\--.' &>/dev/null; then
            ERR "bad long option \`$long_option': expected something like \`--foo'"
          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
              ERR "bad alternate long option \`$long_option_alternate': expected something like \`--foo'"
            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
          ERR "malformed option line for \`$internal': unexpected \`${args[$i]}'"
        fi
        short_option="$(echo "${args[$i]}" | sed 's,/.*,,')"
        if [ -n "$short_option" ]; then
          if ! expr "$short_option" : '\-.$' &>/dev/null; then
            ERR "bad short option \`$short_option': expected something like \`-x'"
          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
              ERR "bad alternate short option \`$short_option_alternate': expected something like \`-x'"
            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
          ERR "malformed option line for \`$internal': unexpected \`${args[$i]}'"
        fi
        smtname="${args[$i]}"
      fi
      let ++i
    done
  fi

  if [ "$type" = void -a "$internal" != - ]; then
    ERR "$internal cannot be void-typed; use \`-' as the name if its to be void"
  elif [ "$type" != void -a "$internal" = - ]; then
    ERR "cannot use an unnamed option if its type is not void"
  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
    ERR "cannot use alternate short option -$short_option_alternate for \`$internal' because it's not of bool type"
  elif [ "$type" != bool -a -n "$long_option_alternate" ]; then
    ERR "cannot use alternate long option --$long_option_alternate for \`$internal' because it's not of bool type"
  fi

  # check that normal options are accessible via SmtEngine too
  if [ -n "$long_option$short_option$long_option_alternate$short_option_alternate" -a -z "$smtname" -a "$internal" != - ]; then
    if [ -n "$long_option" ]; then
      smtname="$long_option"
    else
      WARN "$internal is inaccessible via SmtEngine (no smt name for option) but can be set via command-line: $long_option $short_option $long_option_alternate $short_option_alternate"
    fi
  fi
  # in options files, use an smt name of ":" to force there not to be one
  if [ "$smtname" = : ]; then
    smtname=
  fi

  # check for duplicates
  if [ "$internal" != - ]; then
    if echo " $all_declared_internal_options " | grep -q " $internal "; then
      ERR "internal option name \`$internal' previously declared"
    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
      ERR "long option name \`--$long_option' previously declared"
    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
      ERR "long option name \`--$long_option_alternate' previously declared"
    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
      ERR "short option name \`-$short_option' previously declared"
    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
      ERR "short option name \`-$short_option_alternate' previously declared"
    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
      ERR "SMT option name \`$smtname' previously declared"
    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
         ERR "cannot specify more than one handler; maybe you want a :handler and a :predicate"
       fi
       handlers="${args[$i]}"
       ;;
    :predicate)
       while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : '\:' &>/dev/null; do
         let ++i
         predicates="${predicates} ${args[$i]}"
       done
       ;;
    :notify)
       while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : '\:' &>/dev/null; do
         let ++i
         notifications="${notifications} ${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]}"
         fi
       done
       ;;
    :link-smt)
       j=0
       while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : '\:' &>/dev/null; do
         let ++i
         let ++j
         if [ $j -eq 3 ]; then
           echo "$kf:$lineno: error: attribute :link-smt can only take two arguments" >&2
           exit 1
         fi
         if expr "${args[$i]}" : '.*/' &>/dev/null; then
           echo "$kf:$lineno: error: attribute :link-smt cannot take alternates" >&2
           exit 1
         fi
         smt_links="${smt_links} ${args[$i]}"
       done
       if [ $j -eq 1 ]; then
         smt_links="${smt_links} \"true\""
       fi
       ;;
    :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
       ;;
    *)
       ERR "error in option \`$internal': bad attribute \`$attribute'"
    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);"
    elif [ "$internal" != - ]; then
      module_specializations="${module_specializations}
#line $lineno \"$kf\"
template <> void Options::assign(options::${internal}__option_t, std::string option, std::string value);"
    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=
  run_smt_links=
  run_notifications=
  if [ -n "$links" -a -z "$smt_links" -a -n "$smtname" ]; then
    WARN "$smtname has no :link-smt, but equivalent command-line has :link"
  elif [ -n "$smt_links" -a -z "$links" ] && [ -n "$short_option" -o -n "$short_option_alternate" -o -n "$long_option" -o "$long_option_alternate" ]; then
    WARN "$smtname has a :link-smt, but equivalent command-line has no :link"
  fi
  if [ -n "$links" ]; then
    # command-line links
    for link in $links; do
      run_links="$run_links
#line $lineno \"$kf\"
      extender->pushBackPreemption(\"$link\");"
    done
  fi
  if [ -n "$smt_links" ]; then
    # smt links
    smt_links=($smt_links)
    i=0
    while [ $i -lt ${#smt_links[@]} ]; do
      run_smt_links="$run_smt_links
#line $lineno \"$kf\"
    setOption(std::string(\"${smt_links[$i]}\"), (${smt_links[$(($i+1))]}));"
      i=$((i+2))
    done
  fi
  if [ -n "$links_alternate" ]; then
    # command-line links
    for link in $links_alternate; do
      run_links_alternate="$run_links_alternate
#line $lineno \"$kf\"
      extender->pushBackPreemption(\"$link\");"
    done
  fi
  if [ -n "$notifications" ]; then
    for notification in $notifications; do
      run_notifications="$run_notifications
#line $lineno \"$kf\"
  d_handler->$notification(option);"
    done
  fi
  if [ "$type" = bool ] && [ -n "$cases" -o -n "$cases_alternate" -o -n "$smtname" ]; then
    run_handlers=
    if [ -n "$handlers" ]; then
      ERR "bool-valued options cannot have handlers"
    fi
    if [ -n "$predicates" ]; then
      for predicate in $predicates; do
        run_handlers="$run_handlers
#line $lineno \"$kf\"
  handler->$predicate(option, b);"
      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, options::OptionsHandler* handler) {
  $run_handlers
}"
    fi
  fi
  if [ -n "$cases" ]; then
    if [ "$type" = bool ]; then
      all_modules_option_handlers="${all_modules_option_handlers}${cases}
#line $lineno \"$kf\"
      options->assignBool(options::$internal, option, true);$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->$handler(option, optionarg);"
        done
      else
        run_handlers="
#line $lineno \"$kf\"
  handleOption<$type>(option, optionarg);"
      fi
      if [ -n "$predicates" ]; then
        for predicate in $predicates; do
          run_handlers="$run_handlers
#line $lineno \"$kf\"
  handler->$predicate(option, retval);"
        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 optionarg, options::OptionsHandler* handler) {
#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\"
      options->assign(options::$internal, option, optionarg);$run_links
      break;
"
    elif [ -n "$expect_arg" ]; then
      run_handlers=
      if [ -n "$predicates" ]; then
        ERR "void-valued options cannot have predicates"
      fi
      if [ -n "$handlers" ]; then
        for handler in $handlers; do
          run_handlers="$run_handlers
#line $lineno \"$kf\"
      handler->$handler(option, optionarg);"
        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
        ERR "void-valued options cannot have predicates"
      fi
      if [ -n "$handlers" ]; then
        for handler in $handlers; do
          run_handlers="$run_handlers
#line $lineno \"$kf\"
      handler->$handler(option);"
        done
      fi
      all_modules_option_handlers="${all_modules_option_handlers}${cases}
#line $lineno \"$kf\"
      $run_handlers$run_links
      break;
"
    fi
  fi # ends if [ -n "$cases" ];
  if [ -n "$cases_alternate" ]; then
    if [ "$type" = bool ]; then
      all_modules_option_handlers="${all_modules_option_handlers}${cases_alternate}
#line $lineno \"$kf\"
      options->assignBool(options::$internal, option, false);$run_links_alternate
      break;
"
    else
      ERR "internal error: expected BOOL-typed option in alternate handler"
    fi
  fi

  if [ -n "$smtname" ]; then
    all_modules_smt_options="${all_modules_smt_options:+$all_modules_smt_options,}
#line $lineno \"$kf\"
  \"$smtname\""
    if [ "$internal" != - ]; then
      case "$type" in
      bool)
        all_modules_get_options="${all_modules_get_options:+$all_modules_get_options
#line $lineno \"$kf\"
  }{ std::vector<std::string> v; v.push_back(\"$smtname\"); v.push_back(std::string(d_holder->$internal ? \"true\" : \"false\")); opts.push_back(v); }"
        smt_getoption_handlers="${smt_getoption_handlers}
#line $lineno \"$kf\"
  if(key == \"$smtname\") {
#line $lineno \"$kf\"
    return std::string(options::$internal() ? \"true\" : \"false\");
  }";;
      int|unsigned|int*_t|uint*_t|unsigned\ long|long|float|double)
        all_modules_get_options="${all_modules_get_options:+$all_modules_get_options
#line $lineno \"$kf\"
  }{ std::stringstream ss; ss << std::fixed << std::setprecision(8); ss << d_holder->$internal; std::vector<std::string> v; v.push_back(\"$smtname\"); v.push_back(ss.str()); opts.push_back(v); }"
        smt_getoption_handlers="${smt_getoption_handlers}
#line $lineno \"$kf\"
  if(key == \"$smtname\") {
#line $lineno \"$kf\"
    std::stringstream ss; ss << std::fixed << std::setprecision(8); ss << options::$internal(); return ss.str();
  }";;
      *)
        all_modules_get_options="${all_modules_get_options:+$all_modules_get_options
#line $lineno \"$kf\"
  }{ std::stringstream ss; ss << d_holder->$internal; std::vector<std::string> v; v.push_back(\"$smtname\"); v.push_back(ss.str()); opts.push_back(v); }"
        smt_getoption_handlers="${smt_getoption_handlers}
#line $lineno \"$kf\"
  if(key == \"$smtname\") {
#line $lineno \"$kf\"
    std::stringstream ss; ss << options::$internal();
    return ss.str();
  }";;
      esac
    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\", optionarg == \"true\");$run_smt_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->$handler(\"$smtname\", optionarg);
"
        done
      fi
      smt_setoption_handlers="${smt_setoption_handlers}
#line $lineno \"$kf\"
  if(key == \"$smtname\") {
#line $lineno \"$kf\"
    Options::current()->assign(options::$internal, \"$smtname\", optionarg);$run_smt_links
    return;
  }"
    elif [ -n "$expect_arg" ]; then
      run_handlers=
      for handler in $handlers; do
        run_handlers="$run_handlers
#line $lineno \"$kf\"
    handler->$handler(\"$smtname\", optionarg);
"
      done
      smt_setoption_handlers="${smt_setoption_handlers}
#line $lineno \"$kf\"
  if(key == \"$smtname\") {
#line $lineno \"$kf\"
    $run_handlers$run_smt_links
    return;
  }"
    else
      run_handlers=
      for handler in $handlers; do
        run_handlers="$run_handlers
#line $lineno \"$kf\"
    handler->$handler(\"$smtname\");
"
      done
      smt_setoption_handlers="${smt_setoption_handlers}
#line $lineno \"$kf\"
  if(key == \"$smtname\") {
#line $lineno \"$kf\"
    $run_handlers$run_smt_links
    return;
  }"
    fi
  elif [ -n "$long_option" -o "$long_option_alternate" ] && [ "$internal" != - ]; then
    case "$type" in
    bool)
      getoption_name="$long_option"
      inv=
      # case where we have a --disable but no corresponding --enable
      if [ -z "$getoption_name" ]; then
        getoption_name="$long_option_alternate"
        inv='!'
      fi
      all_modules_get_options="${all_modules_get_options:+$all_modules_get_options
#line $lineno \"$kf\"
  }{ std::vector<std::string> v; v.push_back(\"$getoption_name\"); v.push_back(std::string((${inv}d_holder->$internal) ? \"true\" : \"false\")); opts.push_back(v); }";;
    int|unsigned|int*_t|uint*_t|unsigned\ long|long|float|double)
        all_modules_get_options="${all_modules_get_options:+$all_modules_get_options
#line $lineno \"$kf\"
  }{ std::stringstream ss; ss << std::fixed << std::setprecision(8); ss << d_holder->$internal; std::vector<std::string> v; v.push_back(\"$long_option\"); v.push_back(ss.str()); opts.push_back(v); }";;
    *)
      all_modules_get_options="${all_modules_get_options:+$all_modules_get_options
#line $lineno \"$kf\"
  }{ std::stringstream ss; ss << std::fixed << std::setprecision(8); ss << d_holder->$internal; std::vector<std::string> v; v.push_back(\"$long_option\"); v.push_back(ss.str()); opts.push_back(v); }";;
    esac
  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) {
#line $lineno \"$kf\"
  runBoolPredicates(options::$internal, option, value, d_handler);
#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;$run_notifications
}"
  elif [ -n "$expect_arg" -a "$internal" != - ] && [ -n "$cases" -o -n "$cases_alternate" -o -n "$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) {
#line $lineno \"$kf\"
  d_holder->$internal = runHandlerAndPredicates(options::$internal, option, value, d_handler);
#line $lineno \"$kf\"
  d_holder->${internal}__setByUser__ = true;
#line $lineno \"$kf\"
  Trace(\"options\") << \"user assigned option $internal\" << std::endl;$run_notifications
}"
  fi
}

function common-alias {
  # common-alias -option[=arg] = (-option[=arg])+
  handle_alias COMMON "$@"
}

function alias {
  # alias -option[=arg] = (-option[=arg])+
  handle_alias STANDARD "$@"
}

function expert-alias {
  # expert-alias -option[=arg] = (-option[=arg])+
  handle_alias EXPERT "$@"
}

function undocumented-alias {
  # undocumented-alias -option[=arg] = (-option[=arg])+
  handle_alias UNDOCUMENTED "$@"
}

function handle_alias {
  # handle_alias CATEGORY -option[=arg] = (-option[=arg])+
  check_module_seen
  check_doc

  category="$1"
  shift

  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=
  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

  if [ $# -lt 3 ]; then
    ERR "malformed \"alias\" command; expected more arguments"
  fi
  if [ "$1" = '=' ]; then
    ERR "malformed \"alias\" command; expected option name"
  fi
  option="$1"
  shift
  if [ "$1" != '=' ]; then
    ERR "malformed \"alias\" command; expected \`='"
  fi
  shift
  if [ $# -eq 0 ]; then
    ERR "malformed \"alias\" command; expected more arguments"
  fi
  cases=
  if ! expr "$option" : '\-' &>/dev/null; then
    ERR "alias for SMT options not yet supported"
  fi
  if expr "$option" : '\--' &>/dev/null; then
    if expr "$option" : '.*=' &>/dev/null; then
      expect_arg_long=required_argument
      arg="$(echo "$option" | sed 's,[^=]*=\(.*\),\1,')"
      option="$(echo "$option" | sed 's,--,,;s,=.*,,')"
    else
      expect_arg_long=no_argument
      arg=
      option="$(echo "$option" | sed 's,--,,')"
    fi
    all_modules_long_options="${all_modules_long_options}
  { \"$(echo "$option" | sed 's,=.*,,')\", $expect_arg_long, 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
      if ! expr "$option" : '\-.=' &>/dev/null; then
        ERR "expected short option specification, got \`$option'"
      fi
      expect_arg=:
      arg="$(echo "$option" | sed 's,[^=]*=,,')"
      option="$(echo "$option" | sed 's,-\(.\)=.*,\1,')"
    else
      expect_arg=
      arg=
      option="$(echo "$option" | sed 's,-,,')"
    fi
    all_modules_short_options="${all_modules_short_options}$option$expect_arg"
      cases="${cases}
    case '$option':"
    short_option="${short_option:+$short_option | -}$option"
  fi

  while [ $# -gt 0 ]; do
    linkopt="$1"
    # on the RHS, we're looking for =ARG, where "ARG" is *exactly* what
    # was given on the LHS
    if expr "$linkopt" : '.*=' &>/dev/null; then
      linkarg="$(echo "$linkopt" | sed 's,[^=]*=,,')"
      if [ "$linkarg" = "$arg" ]; then
        # we found =ARG
        linkopt="$(echo "$linkopt" | sed 's,=.*,,')"
      else
        # false positive: =SOMETHING, where SOMETHING != ARG
        linkarg=
      fi
    else
      linkarg=
    fi
    links="$links
#line $lineno \"$kf\"
      extender->pushBackPreemption(\"$linkopt\");"
    if [ "$linkarg" ]; then
      # include also the arg
      links="$links
#line $lineno \"$kf\"
      extender->pushBackPreemption(optionarg.c_str());"
    fi
    shift
  done
  all_modules_option_handlers="$all_modules_option_handlers$cases$links
      break;
"
}

function warning {
  # warning message
  check_module_seen
  check_doc

  WARN "$*"
}

function doc {
  # doc text...
  check_module_seen
  expect_doc=false
  seen_doc=true

  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
        if [ "$internal" != - ]; then
          if ! $alternate_options_already_documented; then
            if [ "$short_option_alternate" ]; then
              if [ "$long_option_alternate" ]; then
                altopt="s -$short_option_alternate and --$long_option_alternate, each of"
              else
                altopt=" -$short_option_alternate,"
              fi
            else
              altopt=" --$long_option_alternate,"
            fi
            if [ -z "$default_value" ]; then
              typedefault="($type)"
            else
              typedefault="($type, default = $default_value)"
            fi
            mansmtdoc="$@"
            if [ "$category" = EXPERT ]; then
              mansmtdoc="$mansmtdoc (EXPERTS only)"
            fi
            altmanopt="`echo "$altopt" | sed 's,-,\\\\\\-,g'`"
            mansmtdoc="`echo "$mansmtdoc" | sed 's,-,\\\\\\-,g'`"
            typedefault="`echo "$typedefault" | sed 's,-,\\\\\\-,g'`"
            if [ "$category" = COMMON ]; then
              common_manpage_internals_documentation="${common_manpage_internals_documentation}
.TP
.B \"$internal\"
$typedefault
.br
.B \"This internal Boolean flag is undocumented; however, its alternate option$altmanopt which reverses the sense of the option, is documented thusly:\"
$mansmtdoc"
            else
              remaining_manpage_internals_documentation="${remaining_manpage_internals_documentation}
.TP
.B \"$internal\"
$typedefault
.br
.B \"This internal Boolean flag is undocumented; however, its alternate option$altmanopt which reverses the sense of the option, is documented thusly:\"
$mansmtdoc"
            fi
          else
            if [ "$category" = COMMON ]; then
              common_manpage_internals_documentation="${common_manpage_internals_documentation}
$@"
            else
              remaining_manpage_internals_documentation="${remaining_manpage_internals_documentation}
$@"
            fi
          fi
        fi
        doc-alternate "$@"
        return
      fi
    fi
  fi

  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 ! $options_already_documented; then
    options_already_documented=true

    the_doc="$@"
    mandoc="$@"
    mansmtdoc="$@"
    if [ "$category" = EXPERT ]; then
      the_doc="$the_doc (EXPERTS only)"
      mandoc="$mandoc (EXPERTS only)"
      mansmtdoc="$mansmtdoc (EXPERTS only)"
    fi

    if [ "$type" = bool -a -n "$long_option" -a "$long_option_alternate" = "no-$long_option" ]; then
      the_doc="$the_doc [*]"
      mandoc="$mandoc [*]"
    fi

    # in man, minus sign is \-, different from hyphen
    the_manopt="`echo "$the_opt" | sed 's,-,\\\\\\-,g'`"
    mandoc="`echo "$mandoc" | sed 's,-,\\\\\\-,g'`"
    mansmtdoc="`echo "$mansmtdoc" | sed 's,-,\\\\\\-,g'`"

    if [ "$the_opt" ]; then
      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_manopt\"
$mandoc"
      elif [ "$category" != UNDOCUMENTED ]; then
        remaining_documentation="${remaining_documentation}\\n\"
#line $lineno \"$kf\"
\"$(echo "$doc_line" | sed 's,'\'',\\'\'',g;s,",\\",g')"
        remaining_manpage_documentation="${remaining_manpage_documentation}
.IP \"$the_manopt\"
$mandoc"
      fi
    fi

    if [ "$smtname" -a "$category" != UNDOCUMENTED ]; then
      if [ "$category" = COMMON ]; then
        common_manpage_smt_documentation="${common_manpage_smt_documentation}
.TP
.B \"$smtname\"
($type) $mansmtdoc"
      else
        remaining_manpage_smt_documentation="${remaining_manpage_smt_documentation}
.TP
.B \"$smtname\"
($type) $mansmtdoc"
      fi
    fi
    if [ "$internal" != - ]; then
      if [ -z "$default_value" ]; then
        typedefault="($type)"
      else
        typedefault="($type, default = $default_value)"
      fi
      typedefault="`echo "$typedefault" | sed 's,-,\\\\\\-,g'`"
      if [ "$category" = COMMON ]; then
        common_manpage_internals_documentation="${common_manpage_internals_documentation}
.TP
.B \"$internal\"
$typedefault
.br
$mansmtdoc"
      else
        remaining_manpage_internals_documentation="${remaining_manpage_internals_documentation}
.TP
.B \"$internal\"
$typedefault
.br
$mansmtdoc"
      fi
    fi
  else
    if [ "$the_opt" -a "$category" != UNDOCUMENTED ]; then
      if [ "$category" = COMMON ]; then
        common_manpage_documentation="${common_manpage_documentation}
$@"
      else
        remaining_manpage_documentation="${remaining_manpage_documentation}
$@"
      fi
    fi

    if [ "$smtname" -a "$category" != UNDOCUMENTED ]; then
      if [ "$category" = COMMON ]; then
        common_manpage_smt_documentation="${common_manpage_smt_documentation}
$@"
      else
        remaining_manpage_smt_documentation="${remaining_manpage_smt_documentation}
$@"
      fi
    fi

    if [ "$internal" != - ]; then
      if [ "$category" = COMMON ]; then
        common_manpage_internals_documentation="${common_manpage_internals_documentation}
$@"
      else
        remaining_manpage_internals_documentation="${remaining_manpage_internals_documentation}
$@"
      fi
    fi
  fi
}

function doc-alternate {
  # doc-alternate text...
  check_module_seen
  expect_doc_alternate=false

  if $expect_doc; then
    ERR "must provide documentation before alternate documentation"
  fi

  if [ -z "$short_option_alternate" -a -z "$long_option_alternate" ]; then
    ERR "cannot document an alternative for option \`$internal'; one does not exist"
  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

    # in man, minus sign is \-, different from hyphen
    the_manopt="`echo "$the_opt" | sed 's,-,\\\\\\-,g'`"

    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_manopt\"
$@"
    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_manopt\"
$@"
    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
      WARN "$internal is lacking documentation"
    elif [ -n "$long_option" ]; then
      WARN "option --$long_option is lacking documentation"
    elif [ -n "$short_option" ]; then
      WARN "option -$short_option is lacking documentation"
    elif [ -n "$smtname" ]; then
      WARN "SMT option $smtname is lacking documentation"
    fi
    expect_doc=false
  elif ! $seen_doc; then
    if [ -n "$internal" -a "$internal" != - ]; then
      if [ -z "$default_value" ]; then
        typedefault="($type)"
      else
        typedefault="($type, default = $default_value)"
      fi
      if [ "$category" = COMMON ]; then
        common_manpage_internals_documentation="${common_manpage_internals_documentation}
.TP
.B \"$internal\"
$typedefault
.br
[undocumented]"
      else
        remaining_manpage_internals_documentation="${remaining_manpage_internals_documentation}
.TP
.B \"$internal\"
$typedefault
.br
[undocumented]"
      fi
    fi
  fi

  if $expect_doc_alternate; then
    WARN "$internal is lacking documentation for the alternative option(s): $short_option_alternate $long_option_alternate"
    expect_doc_alternate=false
  fi
}

function check_module_seen {
  if $seen_endmodule; then
    ERR "command after \"endmodule\" declaration (endmodule has to be last)"
  fi
  if ! $seen_module; then
    ERR "no \"module\" declaration found (it has to be first)"
  fi
}

function check_include {
  if ! expr "$1" : '".*"$' &>/dev/null && ! expr "$1" : '<.*>$' &>/dev/null; then
    echo "\"$1\""
  else
    echo "$1"
  fi
}

function apply_sed_files_to_template {
  template="$1"
  sed_files="$2"
  command="$3"

  filename="$(basename "$sed_file")"
  filename="${filename%.*}"

  echo "applying sed files $sed_files to $template to get $filename " 1>&2

  sed_args=""
  for file in $sed_files; do
    sed_args+=" -f $file"
  done
  
  echo "applying sed files $sed_args " 1>&2

  output_working=$(sed $sed_args "$template")
  error="$(echo "$output_working" | grep '.*\${[^}]*}.*' | head -n 1)"
  if [ -n "$error" ]; then
    error="$(echo "$error" | sed 's,.*\${\([^}]*\)}.*,\1,')"
    kf="$template"
    lineno=0
    ERR "undefined replacement \${$error}"
  fi

  
  # Output header (if this is a .cpp or .c or .h file) and then the
  # processed text

  if expr "$filename" : '.*\.cpp$' &>/dev/null || expr "$filename" : '.*\.[ch]$' &>/dev/null; then


  cat <<EOF
/*********************                                                        */
/** $filename
 **
 ** Copyright $copyright  New York University and The University of Iowa,
 ** and as below.
 **
 ** This file automatically generated by:
 **
 **     $command
 **
 ** 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.                     */

EOF
  fi

  echo -n "$output_working"
  echo ""
}

function output_module_sed {
  options_file="$1"

  echo "generating sed file from $options_file" 1>&2


  for var in \
      module_id \
      module_name \
      module_includes \
      module_optionholder_spec \
      module_decls \
      module_specializations \
      module_inlines \
      module_accessors \
      module_global_definitions \
      ; do
    repl="$(eval "echo \"\${$var}\"" | sed 's,\\,\\\\,g;s/,/\\,/g;s,&,\\\&,g;$!s,$,\\,g')"
    # a little nasty; for multi-line replacements, bash can eat a final
    # (blank) newline, and so we get a final \ on the final line, leading
    # to malformed replacements in the sed script
    repl2="$(echo "$repl" | sed '$s,\\*$,,')"
    while [ "$repl" != "$repl2" ]; do
      repl="$repl2"
      repl2="$(echo "$repl" | sed '$s,\\*$,,')"
    done
    repl="$repl2"
    echo -n ";s,$(eval echo "\$\{$var\}"),$repl,g"
  done
}

function output_summary_sed {
  echo "generating summary sed" 1>&2

  long_option_value_end=$n_long

  for var in \
      smt_getoption_handlers \
      smt_setoption_handlers \
      long_option_value_begin \
      long_option_value_end \
      option_handler_includes \
      all_modules_defaults \
      all_modules_short_options \
      all_modules_long_options \
      all_modules_smt_options \
      all_modules_option_handlers \
      all_modules_get_options \
      include_all_option_headers \
      all_modules_contributions \
      all_custom_handlers \
      common_documentation \
      remaining_documentation \
      common_manpage_documentation \
      remaining_manpage_documentation \
      common_manpage_smt_documentation \
      remaining_manpage_smt_documentation \
      common_manpage_internals_documentation \
      remaining_manpage_internals_documentation \
      ; do
    let ++count
    repl="$(eval "echo \"\${$var}\"" | sed 's,\\,\\\\,g;s/,/\\,/g;s,&,\\\&,g;$!s,$,\\,g')"
    # a little nasty; for multi-line replacements, bash can eat a final
    # (blank) newline, and so we get a final \ on the final line, leading
    # to malformed replacements in the sed script
    repl2="$(echo "$repl" | sed '$s,\\*$,,')"
    while [ "$repl" != "$repl2" ]; do
      repl="$repl2"
      repl2="$(echo "$repl" | sed '$s,\\*$,,')"
    done
    repl="$repl2"
    echo -n ";s,$(eval echo "\$\{$var\}"),$repl,g"
  done
}


function output_template_sed {
  template="$1"

  echo "generating $template" 1>&2

  # 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

  for var in \
      template \
      ; do
    let ++count
    repl="$(eval "echo \"\${$var}\"" | sed 's,\\,\\\\,g;s/,/\\,/g;s,&,\\\&,g;$!s,$,\\,g')"
    # a little nasty; for multi-line replacements, bash can eat a final
    # (blank) newline, and so we get a final \ on the final line, leading
    # to malformed replacements in the sed script
    repl2="$(echo "$repl" | sed '$s,\\*$,,')"
    while [ "$repl" != "$repl2" ]; do
      repl="$repl2"
      repl2="$(echo "$repl" | sed '$s,\\*$,,')"
    done
    repl="$repl2"
    echo -n ";s,$(eval echo "\$\{$var\}"),$repl,g"
  done
}



function scan_module {
  kf="$1";

  echo "scanning $kf" >&2
  let ++count
  #progress "$kf" $count $total

  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
      ERR "malformed line during processing of option \`$internal': continuation lines should not have content"
    elif expr "$line" : '/.*' &>/dev/null; then
      doc-alternate "$(echo "$line" | sed 's,^/,,')"
    else
      line="$(echo "$line" | sed 's,\([<>&()!?*]\),\\\1,g')"
      #progress "$kf" $count $total
      if ! eval "$line"; then
        ERR "error was due to evaluation of this line"
      fi
    fi
  done < "$kf"

  if ! $seen_module; then
    ERR "no module content found in file!"
  fi
  if ! $seen_endmodule; then
    ERR "no \"endmodule\" declaration found (it is required at the end)"
  fi

  echo "done scanning $kf" >&2
}


running_command="$1"

if [ "$running_command" = "module-sed" ]; then
#   mkoptions module-sed options-file
  echo "args: $#" >&2
  if [ "$#" -eq 2 ]; then
    options_file="$2"
    scan_module  "$options_file"
    output_module_sed "$options_file"
  else
    usage
    exit 1
  fi
elif [ "$running_command" = "apply-sed-files-to-template" ]; then
#   mkoptions apply-sed-files-to-template template-file (sed-file)*
  echo "args: $#" >&2
  if [ "$#" -ge 2 ]; then
    shift;
    options_template="$1"; shift
    sed_files="$@"
    apply_sed_files_to_template "$options_template" "$sed_files" "$*"
  else
    usage
    exit 1
  fi
elif [ "$running_command" = "summary-sed" ]; then
#   mkoptions summary-sed (options-file)*
  echo "args: $#" >&2
  shift;

  while [ $# -gt 0 ]; do
    kf="$1"; shift
    scan_module "$kf"
  done
  output_summary_sed 
elif [ "$running_command" = "template-sed" ]; then
#   mkoptions template-sed template-file
  if [ "$#" -eq 2 ]; then
    template_file="$2"
    output_template_sed "$template_file"
  else
    echo "$me: error: expected -t on command line" >&2
    usage
    exit 1
  fi
else
  echo "$me: error: $running_command" >&2
  usage
  exit 1
fi

exit 0