src/theory/mkrewriter

   1 #!/usr/bin/env bash
   2 #
   3 # mkrewriter
   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 rewriter_tables.h from a template
   8 # and a list of theory kinds.
   9 #
  10 # Invocation:
  11 #
  12 #   mkrewriter template-file theory-kind-files...
  13 #
  14 # Output is to standard out.
  15 #
  16
  17 copyright=2010-2014
  18
  19 cat <<EOF
  20 /*********************                                                        */
  21 /** rewriter_tables.h
  22  **
  23  ** Copyright $copyright  New York University and The University of Iowa,
  24  ** and as below.
  25  **
  26  ** This header file automatically generated by:
  27  **
  28  **     $0 $@
  29  **
  30  ** for the CVC4 project.
  31  **/
  32
  33 EOF
  34
  35 me=$(basename "$0")
  36
  37 template=$1; shift
  38
  39 rewriter_includes=
  40 rewrite_init=
  41 rewrite_shutdown=
  42
  43 pre_rewrite_calls=
  44 pre_rewrite_get_cache=
  45 pre_rewrite_set_cache=
  46
  47 post_rewrite_calls=
  48 post_rewrite_get_cache=
  49 post_rewrite_set_cache=
  50
  51 pre_rewrite_attribute_ids=
  52 post_rewrite_attribute_ids=
  53
  54 seen_theory=false
  55 seen_theory_builtin=false
  56
  57 function theory {
  58   # theory ID T header
  59
  60   lineno=${BASH_LINENO[0]}
  61
  62   if $seen_theory; then
  63     echo "$kf:$lineno: error: multiple theories defined in one file !?" >&2
  64     exit 1
  65   fi
  66
  67   # this script doesn't care about the theory class information, but
  68   # makes does make sure it's there
  69   seen_theory=true
  70   if [ "$1" = THEORY_BUILTIN ]; then
  71     if $seen_theory_builtin; then
  72       echo "$kf:$lineno: error: \"builtin\" theory redefined" >&2
  73       exit 1
  74     fi
  75     seen_theory_builtin=true
  76   elif [ -z "$1" -o -z "$2" -o -z "$3" ]; then
  77     echo "$kf:$lineno: error: \"theory\" directive missing class or header argument" >&2
  78     exit 1
  79   elif ! expr "$2" : '\(::*\)' >/dev/null; then
  80     echo "$kf:$lineno: warning: theory class \`$2' isn't fully-qualified (e.g., ::CVC4::theory::foo)" >&2
  81   elif ! expr "$2" : '\(::CVC4::theory::*\)' >/dev/null; then
  82     echo "$kf:$lineno: warning: theory class not under ::CVC4::theory namespace" >&2
  83   fi
  84
  85   theory_id="$1"
  86 }
  87
  88 function alternate {
  89   # alternate ID name T header
  90
  91   lineno=${BASH_LINENO[0]}
  92
  93   if $seen_theory; then
  94     echo "$kf:$lineno: error: multiple theories defined in one file !?" >&2
  95     exit 1
  96   fi
  97
  98   seen_theory=true
  99   seen_endtheory=true
 100 }
 101
 102 function properties {
 103   # properties prop*
 104   lineno=${BASH_LINENO[0]}
 105   check_theory_seen
 106 }
 107
 108 function endtheory {
 109   # endtheory
 110   lineno=${BASH_LINENO[0]}
 111   check_theory_seen
 112   seen_endtheory=true
 113 }
 114
 115 function enumerator {
 116   # enumerator KIND enumerator-class header
 117   lineno=${BASH_LINENO[0]}
 118   check_theory_seen
 119 }
 120
 121 function typechecker {
 122   # typechecker header
 123   lineno=${BASH_LINENO[0]}
 124   check_theory_seen
 125 }
 126
 127 function typerule {
 128   # typerule OPERATOR typechecking-class
 129   lineno=${BASH_LINENO[0]}
 130   check_theory_seen
 131 }
 132
 133 function construle {
 134   # construle OPERATOR isconst-checking-class
 135   lineno=${BASH_LINENO[0]}
 136   check_theory_seen
 137 }
 138
 139 function rewriter {
 140   # rewriter class header
 141   class="$1"
 142   header="$2"
 143
 144   rewriter_includes="${rewriter_includes}#include \"$header\"
 145 "
 146   rewrite_init="${rewrite_init}   ${class}::init();
 147 "
 148   rewrite_shutdown="${rewrite_shutdown}    ${class}::shutdown();
 149 "
 150   pre_rewrite_attribute_ids="${pre_rewrite_attribute_ids} preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<${theory_id}>::pre_rewrite()));
 151 "
 152   post_rewrite_attribute_ids="${post_rewrite_attribute_ids} postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<${theory_id}>::post_rewrite()));
 153 "
 154
 155   pre_rewrite_calls="${pre_rewrite_calls}    case ${theory_id}: return ${class}::preRewrite(node);
 156 "
 157   pre_rewrite_get_cache="${pre_rewrite_get_cache}    case ${theory_id}: return RewriteAttibute<${theory_id}>::getPreRewriteCache(node);
 158 "
 159   pre_rewrite_set_cache="${pre_rewrite_set_cache}    case ${theory_id}: return RewriteAttibute<${theory_id}>::setPreRewriteCache(node, cache);
 160 "
 161
 162   post_rewrite_calls="${post_rewrite_calls}    case ${theory_id}: return ${class}::postRewrite(node);
 163 "
 164   post_rewrite_get_cache="${post_rewrite_get_cache}    case ${theory_id}: return RewriteAttibute<${theory_id}>::getPostRewriteCache(node);
 165 "
 166   post_rewrite_set_cache="${post_rewrite_set_cache}    case ${theory_id}: return RewriteAttibute<${theory_id}>::setPostRewriteCache(node, cache);
 167 "
 168
 169   lineno=${BASH_LINENO[0]}
 170   check_theory_seen
 171 }
 172
 173 function sort {
 174   # sort TYPE cardinality [well-founded ground-term header | not-well-founded] ["comment"]
 175   lineno=${BASH_LINENO[0]}
 176   check_theory_seen
 177 }
 178
 179 function cardinality {
 180   # cardinality TYPE cardinality-computer [header]
 181   lineno=${BASH_LINENO[0]}
 182   check_theory_seen
 183 }
 184
 185 function well-founded {
 186   # well-founded TYPE wellfoundedness-computer [header]
 187   lineno=${BASH_LINENO[0]}
 188   check_theory_seen
 189 }
 190
 191 function variable {
 192   # variable K ["comment"]
 193   lineno=${BASH_LINENO[0]}
 194   check_theory_seen
 195 }
 196
 197 function operator {
 198   # operator K #children ["comment"]
 199   lineno=${BASH_LINENO[0]}
 200   check_theory_seen
 201 }
 202
 203 function parameterized {
 204   # parameterized K1 K2 #children ["comment"]
 205   lineno=${BASH_LINENO[0]}
 206   check_theory_seen
 207 }
 208
 209 function constant {
 210   # constant K T Hasher header ["comment"]
 211   lineno=${BASH_LINENO[0]}
 212   check_theory_seen
 213 }
 214
 215 function nullaryoperator {
 216   # nullaryoperator K ["comment"]
 217   lineno=${BASH_LINENO[0]}
 218   check_theory_seen
 219 }
 220
 221 function check_theory_seen {
 222   if $seen_endtheory; then
 223     echo "$kf:$lineno: error: command after \"endtheory\" declaration (endtheory has to be last)" >&2
 224     exit 1
 225   fi
 226   if ! $seen_theory; then
 227     echo "$kf:$lineno: error: no \"theory\" declaration found (it has to be first)" >&2
 228     exit 1
 229   fi
 230 }
 231
 232 function check_builtin_theory_seen {
 233   if ! $seen_theory_builtin; then
 234     echo "$me: warning: no declaration for the builtin theory found" >&2
 235   fi
 236 }
 237
 238 while [ $# -gt 0 ]; do
 239   kf=$1
 240   seen_theory=false
 241   seen_endtheory=false
 242   b=$(basename $(dirname "$kf"))
 243   source "$kf"
 244   if ! $seen_theory; then
 245     echo "$kf: error: no theory content found in file!" >&2
 246     exit 1
 247   fi
 248   if ! $seen_endtheory; then
 249     echo "$kf:$lineno: error: no \"endtheory\" declaration found (it is required at the end)" >&2
 250     exit 1
 251   fi
 252   shift
 253 done
 254 check_builtin_theory_seen
 255
 256 ## output
 257
 258 # generate warnings about incorrect #line annotations in templates
 259 nl -ba -s' ' "$template"  | grep '^ *[0-9][0-9]* # *line' |
 260   awk '{OFS="";if($1+1!=$3) print "'"$template"':",$1,": warning: incorrect annotation \"#line ",$3,"\" (it should be \"#line ",($1+1),"\")"}' >&2
 261
 262 text=$(cat "$template")
 263 for var in \
 264     rewriter_includes \
 265     pre_rewrite_calls \
 266     post_rewrite_calls \
 267     pre_rewrite_get_cache \
 268     post_rewrite_get_cache \
 269     pre_rewrite_set_cache \
 270     post_rewrite_set_cache \
 271     rewrite_init rewrite_shutdown \
 272     pre_rewrite_attribute_ids \
 273     post_rewrite_attribute_ids \
 274     template \
 275     ; do
 276   eval text="\${text//\\\$\\{$var\\}/\${$var}}"
 277 done
 278 error=`expr "$text" : '.*\${\([^}]*\)}.*'`
 279 if [ -n "$error" ]; then
 280   echo "$template:0: error: undefined replacement \${$error}" >&2
 281   exit 1
 282 fi
 283 echo "$text"