1#!/usr/bin/env bash
2#
3# mktheorytraits
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 theory_traits.h from a template
8# and a list of theory kinds.
9#
10# Invocation:
11#
12#   mktheorytraits template-file theory-kind-files...
13#
14# Output is to standard out.
15#
16
17copyright=2010-2014
18
19filename=`basename "$1" | sed 's,_template,,'`
20
21cat <<EOF
22/*********************                                                        */
23/** $filename
24 **
25 ** Copyright $copyright  New York University and The University of Iowa,
26 ** and as below.
27 **
28 ** This header file automatically generated by:
29 **
30 **     $0 $@
31 **
32 ** for the CVC4 project.
33 **/
34
35EOF
36
37me=$(basename "$0")
38
39template=$1; shift
40
41theory_traits=
42theory_includes=
43theory_constructors=
44theory_for_each_macro="#define CVC4_FOR_EACH_THEORY \\
45"
46
47type_enumerator_includes=
48mk_type_enumerator_cases=
49
50theory_has_check="false"
51theory_has_propagate="false"
52theory_has_ppStaticLearn="false"
53theory_has_notifyRestart="false"
54theory_has_presolve="false"
55theory_has_postsolve="false"
56
57theory_stable_infinite="false"
58theory_finite="false"
59theory_polite="false"
60theory_parametric="false"
61
62rewriter_class=
63rewriter_header=
64
65theory_id=
66theory_class=
67
68type_constants=
69type_kinds=
70
71seen_theory=false
72seen_theory_builtin=false
73
74function theory {
75  # theory ID T header
76
77  lineno=${BASH_LINENO[0]}
78
79  if $seen_theory; then
80    echo "$kf:$lineno: error: multiple theories defined in one file !?" >&2
81    exit 1
82  fi
83
84  # this script doesn't care about the theory class information, but
85  # makes does make sure it's there
86  seen_theory=true
87  if [ "$1" = THEORY_BUILTIN ]; then
88    if $seen_theory_builtin; then
89      echo "$kf:$lineno: error: \"builtin\" theory redefined" >&2
90      exit 1
91    fi
92    seen_theory_builtin=true
93  elif [ -z "$1" -o -z "$2" -o -z "$3" ]; then
94    echo "$kf:$lineno: error: \"theory\" directive missing class or header argument" >&2
95    exit 1
96  elif ! expr "$2" : '\(::*\)' >/dev/null; then
97    echo "$kf:$lineno: warning: theory class \`$2' isn't fully-qualified (e.g., ::CVC4::theory::foo)" >&2
98  elif ! expr "$2" : '\(::CVC4::theory::*\)' >/dev/null; then
99    echo "$kf:$lineno: warning: theory class not under ::CVC4::theory namespace" >&2
100  fi
101
102  theory_id="$1"
103  theory_class="$2"
104
105  theory_header="$3"
106  theory_includes="${theory_includes}#include \"$theory_header\"
107"
108  theory_for_each_macro="${theory_for_each_macro} CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::${theory_id}) \\
109"
110}
111
112function alternate {
113  # alternate ID name T header
114
115  lineno=${BASH_LINENO[0]}
116
117  if $seen_theory; then
118    echo "$kf:$lineno: error: multiple theories defined in one file !?" >&2
119    exit 1
120  fi
121
122  seen_theory=true
123  seen_endtheory=true
124
125  theory_header="$4"
126  theory_includes="${theory_includes}#include \"$theory_header\"
127"
128
129  eval "alternate_for_$1=\"\${alternate_for_$1}
130      if(engine->useTheoryAlternative(\\\"$2\\\")) {
131        engine->addTheory< $3 >($1);
132        return;
133      }\""
134}
135
136function rewriter {
137  # rewriter class header
138  lineno=${BASH_LINENO[0]}
139  check_theory_seen
140
141  rewriter_class="$1"
142  rewriter_header="$2"
143
144  theory_includes="${theory_includes}#include \"$2\"
145"
146}
147
148function endtheory {
149  # endtheory
150  lineno=${BASH_LINENO[0]}
151  check_theory_seen
152
153  seen_endtheory=true
154
155  theory_constructors="${theory_constructors}
156    case $theory_id:
157\$alternate_for_$theory_id
158      engine->addTheory< $theory_class >($theory_id);
159      return;
160"
161
162  theory_traits="${theory_traits}
163template<>
164struct TheoryTraits<${theory_id}> {
165    // typedef ${theory_class} theory_class;
166    typedef ${rewriter_class} rewriter_class;
167
168    static const bool isStableInfinite = ${theory_stable_infinite};
169    static const bool isFinite = ${theory_finite};
170    static const bool isPolite = ${theory_polite};
171    static const bool isParametric = ${theory_parametric};
172
173    static const bool hasCheck = ${theory_has_check};
174    static const bool hasPropagate = ${theory_has_propagate};
175    static const bool hasPpStaticLearn = ${theory_has_ppStaticLearn};
176    static const bool hasNotifyRestart = ${theory_has_notifyRestart};
177    static const bool hasPresolve = ${theory_has_presolve};
178    static const bool hasPostsolve = ${theory_has_postsolve};
179};/* struct TheoryTraits<${theory_id}> */
180"
181
182  # warnings about theory content and properties
183  dir="$(dirname "$kf")/../../"
184  if [ -e "$dir/$theory_header" ]; then
185    for function in check propagate ppStaticLearn notifyRestart presolve postsolve; do
186       if eval "\$theory_has_$function"; then
187         grep '\<'"$function"' *\((\|;\)' "$dir/$theory_header" | grep -vq '^ */\(/\|\*\)' ||
188           echo "$kf: warning: $theory_class has property \"$function\" in its kinds file but doesn't appear to declare the function" >&2
189       else
190         grep '\<'"$function"' *\((\|;\)' "$dir/$theory_header" | grep -vq '^ */\(/\|\*\)' &&
191           echo "$kf: warning: $theory_class does not have property \"$function\" in its kinds file but appears to declare the function" >&2
192       fi
193     done
194  else
195    echo "$me: warning: theory header \"$theory_header\" does not exist or is unreadable" >&2
196  fi
197
198  theory_has_check="false"
199  theory_has_propagate="false"
200  theory_has_ppStaticLearn="false"
201  theory_has_notifyRestart="false"
202  theory_has_presolve="false"
203  theory_has_postsolve="false"
204
205  theory_stable_infinite="false"
206  theory_finite="false"
207  theory_polite="false"
208  theory_parametric="false"
209
210  rewriter_class=
211  rewriter_header=
212
213  theory_id=
214  theory_class=
215
216  type_constants=
217  type_kinds=
218
219  lineno=${BASH_LINENO[0]}
220}
221
222function enumerator {
223  # enumerator KIND enumerator-class header
224  lineno=${BASH_LINENO[0]}
225  check_theory_seen
226  type_enumerator_includes="${type_enumerator_includes}
227#line $lineno \"$kf\"
228#include \"$3\""
229  if expr "$type_constants" : '.* '"$1"' ' &>/dev/null; then
230    mk_type_enumerator_type_constant_cases="${mk_type_enumerator_type_constant_cases}
231#line $lineno \"$kf\"
232    case $1:
233#line $lineno \"$kf\"
234      return new $2(type, tep);
235"
236  elif expr "$type_kinds" : '.* '"$1"' ' &>/dev/null; then
237    mk_type_enumerator_cases="${mk_type_enumerator_cases}
238#line $lineno \"$kf\"
239  case kind::$1:
240#line $lineno \"$kf\"
241    return new $2(type, tep);
242"
243  else
244    echo "$kf:$lineno: error: don't know anything about $1; enumerator must appear after definition" >&2
245    echo "type_constants: $type_constants" >&2
246    echo "type_kinds    : $type_kinds" >&2
247    exit 1
248  fi
249}
250
251function typechecker {
252  # typechecker header
253  lineno=${BASH_LINENO[0]}
254  check_theory_seen
255}
256
257function typerule {
258  # typerule OPERATOR typechecking-class
259  lineno=${BASH_LINENO[0]}
260  check_theory_seen
261}
262
263function construle {
264  # construle OPERATOR isconst-checking-class
265  lineno=${BASH_LINENO[0]}
266  check_theory_seen
267}
268
269function properties {
270  # properties property*
271  lineno=${BASH_LINENO[0]}
272  check_theory_seen
273  while (( $# ));
274  do
275    property="$1"
276    case "$property" in
277       finite) theory_finite="true";;
278       stable-infinite) theory_stable_infinite="true";;
279       parametric) theory_parametric="true";;
280       polite) theory_polite="true";;
281       check) theory_has_check="true";;
282       propagate) theory_has_propagate="true";;
283       ppStaticLearn) theory_has_ppStaticLearn="true";;
284       presolve) theory_has_presolve="true";;
285       postsolve) theory_has_postsolve="true";;
286       notifyRestart) theory_has_notifyRestart="true";;
287       *) echo "$kf:$lineno: error: unknown theory property \"$property\"" >&2; exit 1;;
288    esac
289    shift
290  done
291}
292
293function sort {
294  # sort TYPE cardinality [well-founded ground-term header | not-well-founded] ["comment"]
295  lineno=${BASH_LINENO[0]}
296  check_theory_seen
297  if [ "$3" = well-founded ]; then
298    register_sort "$1" "$2" "$6"
299  else
300    register_sort "$1" "$2" "$4"
301  fi
302}
303
304function cardinality {
305  # cardinality TYPE cardinality-computer [header]
306  lineno=${BASH_LINENO[0]}
307  check_theory_seen
308}
309
310function well-founded {
311  # well-founded TYPE wellfoundedness-computer [header]
312  lineno=${BASH_LINENO[0]}
313  check_theory_seen
314}
315
316function variable {
317  # variable K ["comment"]
318  lineno=${BASH_LINENO[0]}
319  check_theory_seen
320  register_kind "$1" 0 "$2"
321}
322
323function operator {
324  # operator K #children ["comment"]
325  lineno=${BASH_LINENO[0]}
326  check_theory_seen
327  register_kind "$1" "$2" "$3"
328}
329
330function parameterized {
331  # parameterized K1 K2 #children ["comment"]
332  lineno=${BASH_LINENO[0]}
333  check_theory_seen
334  register_kind "$1" "$3" "$4"
335}
336
337function constant {
338  # constant K T Hasher header ["comment"]
339  lineno=${BASH_LINENO[0]}
340  check_theory_seen
341  register_kind "$1" 0 "$5"
342}
343
344function nullaryoperator {
345  # nullaryoperator K ["comment"]
346  lineno=${BASH_LINENO[0]}
347  check_theory_seen
348  register_kind "$1" 0 "$2"
349}
350
351function register_sort {
352  id=$1
353  cardinality=$2
354  comment=$3
355  type_constant_to_theory_id="${type_constant_to_theory_id}   case $id: return $theory_id; break;
356"
357  type_constants="${type_constants} $1 "
358}
359
360function register_kind {
361  r=$1
362  nc=$2
363  comment=$3
364  kind_to_theory_id="${kind_to_theory_id}   case kind::$r: return $theory_id; break;
365"
366  type_kinds="${type_kinds} $1 "
367}
368
369function check_theory_seen {
370  if $seen_endtheory; then
371    echo "$kf:$lineno: error: command after \"endtheory\" declaration (endtheory has to be last)" >&2
372    exit 1
373  fi
374  if ! $seen_theory; then
375    echo "$kf:$lineno: error: no \"theory\" declaration found (it has to be first)" >&2
376    exit 1
377  fi
378}
379
380function check_builtin_theory_seen {
381  if ! $seen_theory_builtin; then
382    echo "$me: warning: no declaration for the builtin theory found" >&2
383  fi
384}
385
386while [ $# -gt 0 ]; do
387  kf=$1
388  seen_theory=false
389  seen_endtheory=false
390  b=$(basename $(dirname "$kf"))
391  source "$kf"
392  if ! $seen_theory; then
393    echo "$kf: error: no theory content found in file!" >&2
394    exit 1
395  fi
396  if ! $seen_endtheory; then
397    echo "$kf:$lineno: error: no \"endtheory\" declaration found (it is required at the end)" >&2
398    exit 1
399  fi
400  shift
401done
402check_builtin_theory_seen
403
404## output
405
406eval "theory_constructors=\"$theory_constructors\""
407
408# generate warnings about incorrect #line annotations in templates
409nl -ba -s' ' "$template"  | grep '^ *[0-9][0-9]* # *line' |
410  awk '{OFS="";if($1+1!=$3) print "'"$template"':",$1,": warning: incorrect annotation \"#line ",$3,"\" (it should be \"#line ",($1+1),"\")"}' >&2
411
412text=$(cat "$template")
413for var in \
414    theory_traits \
415    theory_for_each_macro \
416    theory_includes \
417    theory_constructors \
418    template \
419    type_enumerator_includes \
420    mk_type_enumerator_type_constant_cases \
421    mk_type_enumerator_cases \
422    ; do
423  eval text="\${text//\\\$\\{$var\\}/\${$var}}"
424done
425error=`expr "$text" : '.*\${\([^}]*\)}.*'`
426if [ -n "$error" ]; then
427  echo "$template:0: error: undefined replacement \${$error}" >&2
428  exit 1
429fi
430echo "$text"
431