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