diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-04-25 23:44:00 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-04-25 23:44:00 +0000 |
commit | 97111ecb8681838f2d201420cda12ca9fc7184ed (patch) | |
tree | eee78a3ff75c1c9535b1db89ed273116a6ef3542 /src/expr/mkkind | |
parent | de164c9308f6461472b95c23aae68d9d9686d8ae (diff) |
Monday tasks:
* new "well-foundedness" type property (like cardinality) specified in
Theory kinds files; specifies well-foundedness and a ground term
* well-foundedness / finite checks in Datatypes now superseded by type
system isFinite(), isWellFounded(), mkGroundTerm().
* new "RecursionBreaker" template class, a convenient class that keeps
a "seen" trail without you having to pass it around (which is
difficult in cases of mutual recursion) of the idea of passing
around a "seen" trail
Diffstat (limited to 'src/expr/mkkind')
-rwxr-xr-x | src/expr/mkkind | 100 |
1 files changed, 94 insertions, 6 deletions
diff --git a/src/expr/mkkind b/src/expr/mkkind index 08d874c79..47d02863e 100755 --- a/src/expr/mkkind +++ b/src/expr/mkkind @@ -63,7 +63,11 @@ type_constant_list= type_constant_to_theory_id= type_cardinalities= type_constant_cardinalities= -type_cardinalities_includes= +type_wellfoundednesses= +type_constant_wellfoundednesses= +type_groundterms= +type_constant_groundterms= +type_properties_includes= seen_theory=false seen_theory_builtin=false @@ -121,10 +125,24 @@ function rewriter { } function sort { - # sort TYPE cardinality ["comment"] + # sort TYPE cardinality [well-founded ground-term header | not-well-founded] ["comment"] lineno=${BASH_LINENO[0]} check_theory_seen - register_sort "$1" "$2" "$3" + if [ "$3" = well-founded ]; then + wf=true + groundterm="$4" + header="$5" + comment="$6" + elif [ "$3" = not-well-founded ]; then + wf=false + groundterm= + header= + comment="$4" + else + echo "$kf:$lineno: expected third argument to be \"well-founded\" or \"not-well-founded\"" >&2 + exit 1 + fi + register_sort "$1" "$2" "$wf" "$groundterm" "$header" "$comment" } function cardinality { @@ -134,6 +152,13 @@ function cardinality { register_cardinality "$1" "$2" "$3" } +function well-founded { + # well-founded TYPE wellfoundedness-computer groundterm-computer [header] + lineno=${BASH_LINENO[0]} + check_theory_seen + register_wellfoundedness "$1" "$2" "$3" "$4" +} + function variable { # variable K ["comment"] @@ -173,7 +198,10 @@ function constant { function register_sort { id=$1 cardinality=$2 - comment=$3 + wellfoundedness=$3 + groundterm=$4 + header=$5 + comment=$6 type_constant_list="${type_constant_list} ${id}, /**< ${comment} */ " @@ -184,6 +212,23 @@ function register_sort { type_constant_cardinalities="${type_constant_cardinalities}#line $lineno \"$kf\" case $id: return Cardinality($cardinality); " + type_constant_wellfoundednesses="${type_constant_wellfoundednesses}#line $lineno \"$kf\" + case $id: return $wellfoundedness; +" + if [ -n "$groundterm" ]; then + type_constant_groundterms="${type_constant_groundterms}#line $lineno \"$kf\" + case $id: return $groundterm; +" + if [ -n "$header" ]; then + type_properties_includes="${type_properties_includes}#line $lineno \"$kf\" +#include \"$header\" +" + fi + else + type_constant_groundterms="${type_constant_groundterms}#line $lineno \"$kf\" + case $id: Unhandled(tc); +" + fi } function register_cardinality { @@ -195,7 +240,46 @@ function register_cardinality { case $id: return $cardinality_computer; " if [ -n "$header" ]; then - type_cardinalities_includes="${type_cardinalities_includes}#line $lineno \"$kf\" + type_properties_includes="${type_properties_includes}#line $lineno \"$kf\" +#include \"$header\" +" + fi +} + +function register_wellfoundedness { + id=$1 + wellfoundedness_computer=$(sed 's,%TYPE%,typeNode,g' <<<"$2") + groundterm_computer=$(sed 's,%TYPE%,typeNode,g' <<<"$3") + header=$4 + + # "false" is a special well-foundedness computer that doesn't + # require an associated groundterm-computer; anything else does + if [ "$wellfoundedness_computer" != false ]; then + if [ -z "$groundterm_computer" ]; then + echo "$kf:$lineno: ground-term computer missing in command \"well-founded\"" >&2 + exit 1 + fi + else + if [ -n "$groundterm_computer" ]; then + echo "$kf:$lineno: ground-term computer specified for not-well-founded type" >&2 + exit 1 + fi + fi + + type_wellfoundednesses="${type_wellfoundednesses}#line $lineno \"$kf\" + case $id: return $wellfoundedness_computer; +" + if [ -n "$groundterm_computer" ]; then + type_groundterms="${type_groundterms}#line $lineno \"$kf\" + case $id: return $groundterm_computer; +" + else + type_groundterms="${type_groundterms}#line $lineno \"$kf\" + case $id: Unhandled(typeNode); +" + fi + if [ -n "$header" ]; then + type_properties_includes="${type_properties_includes}#line $lineno \"$kf\" #include \"$header\" " fi @@ -272,7 +356,11 @@ for var in \ type_constant_to_theory_id \ type_cardinalities \ type_constant_cardinalities \ - type_cardinalities_includes \ + type_wellfoundednesses \ + type_constant_wellfoundednesses \ + type_groundterms \ + type_constant_groundterms \ + type_properties_includes \ theory_descriptions \ template \ ; do |