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