path: root/src/expr/mkmetakind

#!/bin/bash
#
# mkmetakind
# Morgan Deters <mdeters@cs.nyu.edu> for CVC4
# Copyright (c) 2010  The CVC4 Project
#
# The purpose of this script is to create metakind.h from a prologue,
# two middle sections, epilogue, and a list of theory kinds.
#
# This is kept distinct from kind.h because kind.h is a public header
# and metakind.h is intended for the expr package only.
#
# Invocation:
#
#   mkmetakind prologue-file middle1-file middle2-file epilogue-file theory-kind-files...
#
# Output is to standard out.
#

copyright=2010

cat <<EOF
/*********************                                           -*- C++ -*-  */
/** metakind.h
 **
 ** Copyright $copyright  The AcSys Group, New York University, and as below.
 **
 ** This header file automatically generated by:
 **
 **     $0 $@
 **
 ** for the CVC4 project.
 **/

EOF

me=$(basename "$0")

template=$1; shift

metakind_includes=
metakind_kinds=
metakind_constantMaps=
metakind_compares=
metakind_constHashes=
metakind_constPrinters=
metakind_ubchildren=
metakind_lbchildren=

seen_theory=false
seen_theory_builtin=false

function theory {
  # theory T header

  lineno=${BASH_LINENO[0]}

  # this script doesn't care about the theory class information, but
  # makes does make sure it's there
  seen_theory=true
  if [ "$1" = builtin ]; then
    if $seen_theory_builtin; then
      echo "$kf:$lineno: error: \"builtin\" theory redefined" >&2
      exit 1
    fi
    seen_theory_builtin=true
  elif [ -z "$1" -o -z "$2" ]; then
    echo "$kf:$lineno: error: \"theory\" directive missing class or header argument" >&2
    exit 1
  elif ! expr "$1" : '\(::*\)' >/dev/null; then
    echo "$kf:$lineno: warning: theory class \`$1' isn't fully-qualified (e.g., ::CVC4::theory::foo)" >&2
  elif ! expr "$1" : '\(::CVC4::theory::*\)' >/dev/null; then
    echo "$kf:$lineno: warning: theory class not under ::CVC4::theory namespace" >&2
  fi

  theory_class=$1
  if [ "$1" != builtin ]; then
    metakind_includes="${metakind_includes}
// #include \"theory/$b/$2\""
  fi
}

function variable {
  # variable K ["comment"]

  lineno=${BASH_LINENO[0]}

  check_theory_seen
  register_metakind VARIABLE "$1" 0
}

function operator {
  # operator K #children ["comment"]

  lineno=${BASH_LINENO[0]}

  check_theory_seen
  register_metakind OPERATOR "$1" "$2"
}

function parameterized {
  # parameterized K #children ["comment"]

  lineno=${BASH_LINENO[0]}

  check_theory_seen
  register_metakind PARAMETERIZED "$1" "$2"
}

function constant {
  # constant K T Hasher header ["comment"]

  lineno=${BASH_LINENO[0]}

  check_theory_seen

  if ! expr "$2" : '\(::*\)' >/dev/null; then
    echo "$kf:$lineno: warning: constant $1 class \`$2' isn't fully-qualified (e.g., ::CVC4::Rational)" >&2
  fi
  if ! expr "$3" : '\(::*\)' >/dev/null; then
    echo "$kf:$lineno: warning: constant $1 hasher \`$3' isn't fully-qualified (e.g., ::CVC4::RationalHashFcn)" >&2
  fi

  if [ -n "$4" ]; then
    metakind_includes="${metakind_includes}
#include \"$4\""
  fi
  register_metakind CONSTANT "$1" 0
  metakind_constantMaps="${metakind_constantMaps}
}/* CVC4::kind::metakind namespace */
}/* CVC4::kind namespace */

namespace expr {

template <>
inline const $2 & NodeValue::getConst< $2 >() const {
  Assert(getKind() == ::CVC4::kind::$1);
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // \"constructed\" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< const $2 * >(d_children)
    : *reinterpret_cast< const $2 * >(d_children[0]);
}

}/* CVC4::expr namespace */

namespace kind {
namespace metakind {

template <>
struct ConstantMap< $2 > {
  // typedef $theory_class OwningTheory;
  enum { kind = ::CVC4::kind::$1 };
};/* ConstantMap< $2 > */

template <>
struct ConstantMapReverse< ::CVC4::kind::$1 > {
  typedef $2 T;
};/* ConstantMapReverse< ::CVC4::kind::$1 > */

"
  metakind_compares="${metakind_compares}
    case kind::$1:
      return NodeValueConstCompare< kind::$1, pool >::compare(nv1, nv2);
"
  metakind_constHashes="${metakind_constHashes}
  case kind::$1:
    return $3::hash(nv->getConst< $2 >());
"
  metakind_constPrinters="${metakind_constPrinters}
  case kind::$1:
    out << nv->getConst< $2 >();
    break;
"
}

function register_metakind {
  mk=$1
  k=$2
  nc=$3
  metakind_kinds="${metakind_kinds}    metakind::$mk, /* $k */
";

  # figure out the range given by $nc
  if expr "$nc" : '^[0-9]\+$' >/dev/null; then
    lb=$nc
    ub=$nc
  elif expr "$nc" : '^[0-9]\+:$' >/dev/null; then
    let `echo "$nc" | awk 'BEGIN{FS=":"}{print"lb="$1}'`
    ub=MAX_CHILDREN
  elif expr "$nc" : '^[0-9]\+:[0-9]\+$' >/dev/null; then
    let `echo "$nc" | awk 'BEGIN{FS=":"}{print"lb="$1" ub="$2}'`
    if [ $ub -lt $lb ]; then
      echo "$kf:$lineno: error in range \`$nc': LB < UB (in definition of $k)" >&2
      exit 1
    fi
  else
    echo "$kf:$lineno: can't parse range \`$nc' in definition of $k" >&2
    exit 1
  fi

  metakind_lbchildren="${metakind_lbchildren}
    $lb, /* $k */"
  metakind_ubchildren="${metakind_ubchildren}
    $ub, /* $k */"
}

function check_theory_seen {
  if ! $seen_theory; then
    echo "$kf:$lineno: error: no \"theory\" declaration found (it has to be first)" >&2
    exit 1
  fi
}

function check_builtin_theory_seen {
  if ! $seen_theory_builtin; then
    echo "$me: warning: no declaration for the builtin theory found" >&2
  fi
}

while [ $# -gt 0 ]; do
  kf=$1
  seen_theory=false
  b=$(basename $(dirname "$kf"))
  metakind_kinds="${metakind_kinds}
    /* from $b */
"
  source "$kf"
  check_theory_seen
  shift
done
check_builtin_theory_seen

## output

text=$(cat "$template")
for var in metakind_includes metakind_kinds metakind_constantMaps \
           metakind_compares metakind_constHashes metakind_constPrinters \
           metakind_ubchildren metakind_lbchildren; do
  eval text="\${text//\\\$\\{$var\\}/\${$var}}"
done
error=`expr "$text" : '.*\${\([^}]*\)}.*'`
if [ -n "$error" ]; then
  echo "$template:0: error: undefined replacement \${$error}" >&2
  exit 1
fi
echo "$text"