src/expr/mkmetakind

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