src/expr/mkmetakind

   1 #!/usr/bin/env bash
   2 #
   3 # mkmetakind
   4 # Morgan Deters <mdeters@cs.nyu.edu> for CVC4
   5 # Copyright (c) 2010-2013  The CVC4 Project
   6 #
   7 # The purpose of this script is to create metakind.h from a template
   8 # and a list of theory kinds.
   9 #
  10 # This is kept distinct from kind.h because kind.h is a public header
  11 # and metakind.h is intended for the expr package only.
  12 #
  13 # Invocation:
  14 #
  15 #   mkmetakind template-file theory-kind-files...
  16 #
  17 # Output is to standard out.
  18 #
  19
  20 copyright=2010-2014
  21
  22 cat <<EOF
  23 /*********************                                                        */
  24 /** metakind.h
  25  **
  26  ** Copyright $copyright  New York University and The University of Iowa,
  27  ** and as below.
  28  **
  29  ** This header file automatically generated by:
  30  **
  31  **     $0 $@
  32  **
  33  ** for the CVC4 project.
  34  **/
  35
  36 EOF
  37
  38 me=$(basename "$0")
  39
  40 template=$1; shift
  41
  42 metakind_includes=
  43 metakind_kinds=
  44 metakind_constantMaps=
  45 metakind_compares=
  46 metakind_constHashes=
  47 metakind_constPrinters=
  48 metakind_constDeleters=
  49 metakind_ubchildren=
  50 metakind_lbchildren=
  51 metakind_operatorKinds=
  52
  53 seen_theory=false
  54 seen_theory_builtin=false
  55
  56 function theory {
  57   # theory ID T header
  58
  59   lineno=${BASH_LINENO[0]}
  60
  61   if $seen_theory; then
  62     echo "$kf:$lineno: error: multiple theories defined in one file !?" >&2
  63     exit 1
  64   fi
  65
  66   # this script doesn't care about the theory class information, but
  67   # makes does make sure it's there
  68   seen_theory=true
  69   if [ "$1" = THEORY_BUILTIN ]; then
  70     if $seen_theory_builtin; then
  71       echo "$kf:$lineno: error: \"builtin\" theory redefined" >&2
  72       exit 1
  73     fi
  74     seen_theory_builtin=true
  75   elif [ -z "$1" -o -z "$2" -o -z "$3" ]; then
  76     echo "$kf:$lineno: error: \"theory\" directive missing class or header argument" >&2
  77     exit 1
  78   elif ! expr "$2" : '\(::*\)' >/dev/null; then
  79     echo "$kf:$lineno: warning: theory class \`$1' isn't fully-qualified (e.g., ::CVC4::theory::foo)" >&2
  80   elif ! expr "$2" : '\(::CVC4::theory::*\)' >/dev/null; then
  81     echo "$kf:$lineno: warning: theory class not under ::CVC4::theory namespace" >&2
  82   fi
  83
  84   theory_class=$1
  85   metakind_includes="${metakind_includes}
  86 // #include \"theory/$b/$2\""
  87 }
  88
  89 function alternate {
  90   # alternate ID name T header
  91
  92   lineno=${BASH_LINENO[0]}
  93
  94   if $seen_theory; then
  95     echo "$kf:$lineno: error: multiple theories defined in one file !?" >&2
  96     exit 1
  97   fi
  98
  99   seen_theory=true
 100   seen_endtheory=true
 101
 102   theory_id="$1"
 103   name="$2"
 104   theory_class="$3"
 105   theory_header="$4"
 106   theory_includes="${theory_includes}#include \"$theory_header\"
 107 "
 108 }
 109
 110 function properties {
 111   # properties prop*
 112   lineno=${BASH_LINENO[0]}
 113   check_theory_seen
 114 }
 115
 116 function endtheory {
 117   # endtheory
 118   lineno=${BASH_LINENO[0]}
 119   check_theory_seen
 120   seen_endtheory=true
 121 }
 122
 123 function enumerator {
 124   # enumerator KIND enumerator-class header
 125   lineno=${BASH_LINENO[0]}
 126   check_theory_seen
 127 }
 128
 129 function typechecker {
 130   # typechecker header
 131   lineno=${BASH_LINENO[0]}
 132   check_theory_seen
 133 }
 134
 135 function typerule {
 136   # typerule OPERATOR typechecking-class
 137   lineno=${BASH_LINENO[0]}
 138   check_theory_seen
 139 }
 140
 141 function construle {
 142   # construle OPERATOR isconst-checking-class
 143   lineno=${BASH_LINENO[0]}
 144   check_theory_seen
 145 }
 146
 147 function rewriter {
 148   # rewriter class header
 149   lineno=${BASH_LINENO[0]}
 150   check_theory_seen
 151 }
 152
 153 function sort {
 154   # sort TYPE cardinality [well-founded ground-term header | not-well-founded] ["comment"]
 155   lineno=${BASH_LINENO[0]}
 156   check_theory_seen
 157 }
 158
 159 function cardinality {
 160   # cardinality TYPE cardinality-computer [header]
 161   lineno=${BASH_LINENO[0]}
 162   check_theory_seen
 163 }
 164
 165 function well-founded {
 166   # well-founded TYPE wellfoundedness-computer [header]
 167   lineno=${BASH_LINENO[0]}
 168   check_theory_seen
 169 }
 170
 171 function variable {
 172   # variable K ["comment"]
 173
 174   lineno=${BASH_LINENO[0]}
 175
 176   check_theory_seen
 177   register_metakind VARIABLE "$1" 0
 178 }
 179
 180 function operator {
 181   # operator K #children ["comment"]
 182
 183   lineno=${BASH_LINENO[0]}
 184
 185   check_theory_seen
 186   register_metakind OPERATOR "$1" "$2"
 187 }
 188
 189 function parameterized {
 190   # parameterized K1 K2 #children ["comment"]
 191
 192   lineno=${BASH_LINENO[0]}
 193
 194   check_theory_seen
 195   register_metakind PARAMETERIZED "$1" "$3"
 196   if ! expr "$2" : '\[.*\]' &>/dev/null; then
 197     registerOperatorToKind "$1" "$2"
 198   fi
 199 }
 200
 201 function constant {
 202   # constant K T Hasher header ["comment"]
 203
 204   lineno=${BASH_LINENO[0]}
 205
 206   check_theory_seen
 207
 208   if ! expr "$2" : '\(::*\)' >/dev/null; then
 209     if ! primitive_type "$2"; then
 210       # if there's an embedded space, we're probably doing something
 211       # tricky to specify the CONST payload, like "int const*"; in any
 212       # case, this warning gives too many false positives, so disable it
 213       if ! expr "$2" : '..* ..*' >/dev/null; then
 214         echo "$kf:$lineno: warning: constant $1 class \`$2' isn't fully-qualified (e.g., ::CVC4::Rational)" >&2
 215       fi
 216     fi
 217   fi
 218   if ! expr "$3" : '\(::*\)' >/dev/null; then
 219     echo "$kf:$lineno: warning: constant $1 hasher \`$3' isn't fully-qualified (e.g., ::CVC4::RationalHashFunction)" >&2
 220   fi
 221
 222   # Avoid including the same header multiple times
 223   if [ -n "$4" ] && [[ "${metakind_includes}" != *"#include \"$4\""* ]]; then
 224     metakind_includes="${metakind_includes}
 225 #include \"$4\""
 226   fi
 227   register_metakind CONSTANT "$1" 0
 228   metakind_getConst_decls="${metakind_getConst_decls}
 229 template <>
 230 $2 const& NodeValue::getConst< $2 >() const;
 231 "
 232   metakind_constantMaps_decls="${metakind_constantMaps_decls}
 233 template <>
 234 struct ConstantMap< $2 > {
 235   // typedef $theory_class OwningTheory;
 236   enum { kind = ::CVC4::kind::$1 };
 237 };/* ConstantMap< $2 > */
 238
 239 template <>
 240 struct ConstantMapReverse< ::CVC4::kind::$1 > {
 241   typedef $2 T;
 242 };/* ConstantMapReverse< ::CVC4::kind::$1 > */
 243   "
 244   metakind_constantMaps="${metakind_constantMaps}
 245 // The reinterpret_cast of d_children to \"$2 const*\"
 246 // flags a \"strict aliasing\" warning; it's okay, because we never access
 247 // the embedded constant as a NodeValue* child, and never access an embedded
 248 // NodeValue* child as a constant.
 249 #pragma GCC diagnostic ignored \"-Wstrict-aliasing\"
 250
 251 template <>
 252 $2 const& NodeValue::getConst< $2 >() const {
 253   AssertArgument(getKind() == ::CVC4::kind::$1, *this,
 254                  \"Improper kind for getConst<$2>()\");
 255   // To support non-inlined CONSTANT-kinded NodeValues (those that are
 256   // \"constructed\" when initially checking them against the NodeManager
 257   // pool), we must check d_nchildren here.
 258   return d_nchildren == 0
 259     ? *reinterpret_cast< $2 const* >(d_children)
 260     : *reinterpret_cast< $2 const* >(d_children[0]);
 261 }
 262
 263 // re-enable the warning
 264 #pragma GCC diagnostic warning \"-Wstrict-aliasing\"
 265
 266 "
 267   metakind_compares="${metakind_compares}
 268     case kind::$1:
 269       return NodeValueConstCompare< kind::$1, pool >::compare(nv1, nv2);
 270 "
 271   metakind_constHashes="${metakind_constHashes}
 272   case kind::$1:
 273     return $3()(nv->getConst< $2 >());
 274 "
 275   metakind_constPrinters="${metakind_constPrinters}
 276   case kind::$1:
 277     out << nv->getConst< $2 >();
 278     break;
 279 "
 280   cname=`echo "$2" | awk 'BEGIN {FS="::"} {print$NF}'`
 281   metakind_constDeleters="${metakind_constDeleters}
 282   case kind::$1:
 283     std::allocator< $2 >().destroy(reinterpret_cast< $2* >(nv->d_children));
 284     break;
 285 "
 286 }
 287
 288 function nullaryoperator {
 289   # nullaryoperator K ["comment"]
 290
 291   lineno=${BASH_LINENO[0]}
 292
 293   check_theory_seen
 294   register_metakind NULLARY_OPERATOR "$1" 0
 295 }
 296
 297 function registerOperatorToKind {
 298   operatorKind=$1
 299   applyKind=$2
 300   metakind_operatorKinds="${metakind_operatorKinds}
 301     case kind::$applyKind: return kind::$operatorKind;";
 302 }
 303
 304 function register_metakind {
 305   mk=$1
 306   k=$2
 307   nc=$3
 308
 309   metakind_kinds="${metakind_kinds}    metakind::$mk, /* $k */
 310 ";
 311
 312   # figure out the range given by $nc
 313   if expr "$nc" : '[0-9][0-9]*$' >/dev/null; then
 314     lb=$nc
 315     ub=$nc
 316   elif expr "$nc" : '[0-9][0-9]*:$' >/dev/null; then
 317     let `echo "$nc" | awk 'BEGIN{FS=":"}{print"lb="$1}'`
 318     ub="expr::NodeValue::MAX_CHILDREN"
 319   elif expr "$nc" : '[0-9][0-9]*:[0-9][0-9]*$' >/dev/null; then
 320     let `echo "$nc" | awk 'BEGIN{FS=":"}{print"lb="$1" ub="$2}'`
 321     if [ $ub -lt $lb ]; then
 322       echo "$kf:$lineno: error in range \`$nc': LB < UB (in definition of $k)" >&2
 323       exit 1
 324     fi
 325   else
 326     echo "$kf:$lineno: can't parse range \`$nc' in definition of $k" >&2
 327     exit 1
 328   fi
 329
 330   metakind_lbchildren="${metakind_lbchildren}
 331     $lb, /* $k */"
 332   metakind_ubchildren="${metakind_ubchildren}
 333     $ub, /* $k */"
 334 }
 335
 336 # Returns 0 if arg is a primitive C++ type, or a pointer to same; 1
 337 # otherwise.  Really all this does is check whether we should issue a
 338 # "not fully qualified" warning or not.
 339 function primitive_type {
 340   strip=`expr "$1" : ' *\(.*\)\* *'`
 341   if [ -n "$strip" ]; then
 342     primitive_type "$strip" >&2
 343     return $?
 344   fi
 345
 346   case "$1" in
 347     bool|int|size_t|long|void|char|float|double) return 0;;
 348     *) return 1;;
 349   esac
 350 }
 351
 352 function check_theory_seen {
 353   if $seen_endtheory; then
 354     echo "$kf:$lineno: error: command after \"endtheory\" declaration (endtheory has to be last)" >&2
 355     exit 1
 356   fi
 357   if ! $seen_theory; then
 358     echo "$kf:$lineno: error: no \"theory\" declaration found (it has to be first)" >&2
 359     exit 1
 360   fi
 361 }
 362
 363 function check_builtin_theory_seen {
 364   if ! $seen_theory_builtin; then
 365     echo "$me: warning: no declaration for the builtin theory found" >&2
 366   fi
 367 }
 368
 369 while [ $# -gt 0 ]; do
 370   kf=$1
 371   seen_theory=false
 372   seen_endtheory=false
 373   b=$(basename $(dirname "$kf"))
 374   metakind_kinds="${metakind_kinds}
 375     /* from $b */
 376 "
 377   metakind_operatorKinds="${metakind_operatorKinds}
 378
 379     /* from $b */"
 380   source "$kf"
 381   if ! $seen_theory; then
 382     echo "$kf: error: no theory content found in file!" >&2
 383     exit 1
 384   fi
 385   if ! $seen_endtheory; then
 386     echo "$kf:$lineno: error: no \"endtheory\" declaration found (it is required at the end)" >&2
 387     exit 1
 388   fi
 389   shift
 390 done
 391 check_builtin_theory_seen
 392
 393 ## output
 394
 395 text=$(cat "$template")
 396 for var in \
 397     metakind_includes \
 398     metakind_kinds \
 399     metakind_constantMaps \
 400     metakind_constantMaps_decls \
 401     metakind_getConst_decls \
 402     metakind_compares \
 403     metakind_constHashes \
 404     metakind_constPrinters \
 405     metakind_constDeleters \
 406     metakind_ubchildren \
 407     metakind_lbchildren \
 408     metakind_operatorKinds \
 409     template \
 410     ; do
 411   eval text="\${text//\\\$\\{$var\\}/\${$var}}"
 412 done
 413 error=`expr "$text" : '.*\${\([^}]*\)}.*'`
 414 if [ -n "$error" ]; then
 415   echo "$template:0: error: undefined replacement \${$error}" >&2
 416   exit 1
 417 fi
 418 echo "$text"