contrib/new-theory

   1 #!/bin/bash
   2 #
   3 # usage: new-theory [--alternate existing-theory] new-theory-dir-name
   4 #
   5
   6 cd "`dirname "$0"`/.."
   7
   8 if ! perl -v &>/dev/null; then
   9   echo "ERROR: perl is required to run this script." >&2
  10   exit 1
  11 fi
  12
  13 if [ ! -e src/theory/theory_engine.h ]; then
  14   echo "ERROR: This script doesn't appear to be the contrib/ subdirectory" >&2
  15   echo "ERROR: of the CVC4 source tree." >&2
  16   exit 1
  17 fi
  18
  19 # Trailing whitespaces in src/Makefile.am mess with the regexps (and are
  20 # generally undesirable, so we throw an error instead of ignoring them).
  21 if grep -q '[[:blank:]]$' src/Makefile.am; then
  22         echo "ERROR: trailing whitespaces in src/Makefile.am" >&2
  23         exit 1
  24 fi
  25
  26 if [ $# -ge 1 -a "$1" = --alternate ]; then
  27   shift
  28   alternate=true
  29   alttheory="$1"
  30   shift
  31 else
  32   alternate=false
  33 fi
  34
  35 if [ $# -ne 1 ]; then
  36   echo "usage: new-theory [--alternate existing-theory] new-theory-dir-name" >&2
  37   echo "e.g.:  new-theory arrays" >&2
  38   echo "e.g.:  new-theory sets" >&2
  39   echo "e.g.:  new-theory rewrite_rules" >&2
  40   echo "e.g.:  new-theory --alternate arith difference-logic" >&2
  41   echo >&2
  42   echo "This tool will create a new src/theory/<new-theory-dir-name>" >&2
  43   echo "directory and fill in some infrastructural files in that directory." >&2
  44   echo "It also will incorporate that directory into the build process." >&2
  45   echo "Please refer to the file README.WHATS-NEXT file created in that" >&2
  46   echo "directory for tips on what to do next." >&2
  47   echo >&2
  48   echo "Theories with multiple words (e.g. \"rewrite_rules\") should have" >&2
  49   echo "directories and namespaces separated by an underscore (_).  The" >&2
  50   echo "resulting class names created by this script will be in CamelCase" >&2
  51   echo "(e.g. RewriteRules) if that convention is followed." >&2
  52   echo >&2
  53   echo "With --alternate, create a new theory directory that is declared as" >&2
  54   echo "an alternate implementation of an existing host theory.  Such" >&2
  55   echo "\"alternates\" share preprocessing, typechecking, rewriting (i.e.," >&2
  56   echo "normal form), and expression kinds with their host theories, but" >&2
  57   echo "differ in decision procedure implementation.  They are selectable" >&2
  58   echo "at runtime with --use-theory." >&2
  59   exit 1
  60 fi
  61
  62 dir="$1"
  63
  64 if [ -e "src/theory/$dir" ]; then
  65   echo "ERROR: Theory \"$dir\" already exists." >&2
  66   echo "ERROR: Please choose a new directory name (or move that one aside)." >&2
  67   echo "ERROR: Or, if you'd like to create an alternate implementation of" >&2
  68   echo "ERROR: $dir, use this program this way:" >&2
  69   echo "ERROR:     new-theory --alternate $dir new-implementation-name" >&2
  70   exit 1
  71 fi
  72
  73 if ! expr "$dir" : '[a-zA-Z][a-zA-Z0-9_]*$' &>/dev/null ||
  74    expr "$dir" : '_$' &>/dev/null; then
  75   echo "ERROR: \"$dir\" is not a valid theory name." >&2
  76   echo "ERROR:" >&2
  77   echo "ERROR: Theory names must start with a letter and be composed of" >&2
  78   echo "ERROR: letters, numbers, and the underscore (_) character; an" >&2
  79   echo "ERROR: underscore cannot be the final character." >&2
  80   exit 1
  81 fi
  82
  83 if $alternate; then
  84   if ! [ -d "src/theory/$alttheory" -a -f "src/theory/$alttheory/kinds" ]; then
  85     echo "ERROR: Theory \"$alttheory\" doesn't exist, or cannot read its kinds file." >&2
  86     exit 1
  87   fi
  88   alt_id="$(
  89     function theory() { echo $1 | sed 's,^THEORY_,,'; exit; }
  90     source "src/theory/$alttheory/kinds"
  91   )"
  92 fi
  93
  94 id="`echo "$dir" | tr a-z A-Z`"
  95 # convoluted, but should be relatively portable and give a CamelCase
  96 # representation for a string.  (e.g. "foo_bar" becomes "FooBar")
  97 camel="`echo "$dir" | awk 'BEGIN { RS="_";ORS="";OFS="" } // {print toupper(substr($1,1,1)),substr($1,2,length($1))} END {print "\n"}'`"
  98
  99 if ! mkdir "src/theory/$dir"; then
 100   echo "ERROR: encountered an error creating directory src/theory/$dir" >&2
 101   exit 1
 102 fi
 103
 104 echo "Theory of $dir"
 105 echo "Theory directory: src/theory/$dir"
 106 echo "Theory id: THEORY_$id"
 107 $alternate && echo "Alternate for theory id: THEORY_$alt_id"
 108 echo "Theory class: CVC4::theory::$dir::Theory$camel"
 109 echo
 110
 111 function copyskel {
 112   src="$1"
 113   dest="`echo "$src" | sed "s/DIR/$dir/g"`"
 114   echo "Creating src/theory/$dir/$dest..."
 115   sed "s/\$dir/$dir/g;s/\$camel/$camel/g;s/\$id/$id/g" \
 116     contrib/theoryskel/$src \
 117     > "src/theory/$dir/$dest"
 118 }
 119
 120 function copyaltskel {
 121   src="$1"
 122   dest="`echo "$src" | sed "s/DIR/$dir/g"`"
 123   echo "Creating src/theory/$dir/$dest..."
 124   sed "s/\$dir/$dir/g;s/\$camel/$camel/g;s/\$id/$id/g;s/\$alt_id/$alt_id/g" \
 125     contrib/alttheoryskel/$src \
 126     > "src/theory/$dir/$dest"
 127 }
 128
 129 function copyoptions {
 130   src="$1"
 131   dest="`echo "$src" | sed "s/DIR/$dir/g"`"
 132   echo "Creating src/options/$dest..."
 133   sed "s/\$dir/$dir/g;s/\$camel/$camel/g;s/\$id/$id/g;s/\$alt_id/$alt_id/g" \
 134     contrib/optionsskel/$src \
 135     > "src/options/$dest"
 136 }
 137
 138 # copy files from the skeleton, with proper replacements
 139 if $alternate; then
 140   alternate01=1
 141   for file in `ls contrib/alttheoryskel`; do
 142     copyaltskel "$file"
 143   done
 144 else
 145   alternate01=0
 146   for file in `ls contrib/theoryskel`; do
 147     copyskel "$file"
 148   done
 149 fi
 150 # Copy the options file independently
 151 for file in `ls contrib/optionsskel`; do
 152   copyoptions "$file"
 153 done
 154
 155
 156 echo
 157 echo "Adding $dir to THEORIES to src/Makefile.theories..."
 158 if grep -q '^THEORIES = .*[^a-zA-Z0-9_]'"$dir"'\([^a-zA-Z0-9_]\|$\)' src/Makefile.theories &>/dev/null; then
 159   echo "NOTE: src/Makefile.theories already lists theory $dir"
 160 else
 161   awk '/^THEORIES = / {print $0,"'"$dir"'"} !/^THEORIES = / {print$0}' src/Makefile.theories > src/Makefile.theories.new-theory
 162   if ! cp -f src/Makefile.theories src/Makefile.theories~; then
 163     echo "ERROR: cannot copy src/Makefile.theories !" >&2
 164     exit 1
 165   fi
 166   if ! mv -f src/Makefile.theories.new-theory src/Makefile.theories; then
 167     echo "ERROR: cannot replace src/Makefile.theories !" >&2
 168     exit 1
 169   fi
 170 fi
 171
 172 echo "Adding sources to src/Makefile.am..."
 173
 174 perl -e '
 175   while(<>) { print; last if /^libcvc4_la_SOURCES = /; }
 176   if('$alternate01') {
 177     while(<>) { if(!/\\$/) { chomp; print "$_ \\\n\ttheory/'"$dir"'/theory_'"$dir"'.h \\\n\ttheory/'"$dir"'/theory_'"$dir"'.cpp\n"; last; } else { print; } }
 178   } else {
 179     while(<>) { if(!/\\$/) { chomp; print "$_ \\\n\ttheory/'"$dir"'/theory_'"$dir"'.h \\\n\ttheory/'"$dir"'/theory_'"$dir"'.cpp \\\n\ttheory/'"$dir"'/theory_'"$dir"'_rewriter.h \\\n\ttheory/'"$dir"'/theory_'"$dir"'_type_rules.h\n"; last; } else { print; } }
 180   }
 181   while(<>) { print; last if /^EXTRA_DIST = /; }
 182   while(<>) { if(!/\\$/) { chomp; print "$_ \\\n\ttheory/'"$dir"'/kinds\n"; last; } else { print; } }
 183   while(<>) { print; }' src/Makefile.am > src/Makefile.am.new-theory
 184 if ! mv -f src/Makefile.am.new-theory src/Makefile.am; then
 185   echo "ERROR: cannot replace src/Makefile.am !" >&2
 186   exit 1
 187 fi
 188
 189 echo "Adding ${dir}_options.toml to src/options/Makefile.am..."
 190 if grep -q '^   ${dir}_options.toml' src/options/Makefile.am &>/dev/null; then
 191   echo "NOTE: src/options/Makefile.am already seems to link to $dir option files"
 192 else
 193   awk -v name="$dir" -f contrib/new-theory.awk src/options/Makefile.am > src/options/Makefile.am.new-theory
 194   if ! cp -f src/options/Makefile.am src/options/Makefile.am~; then
 195     echo "ERROR: cannot copy src/options/Makefile.am !" >&2
 196     exit 1
 197   fi
 198   if ! mv -f src/options/Makefile.am.new-theory src/options/Makefile.am; then
 199     echo "ERROR: cannot replace src/options/Makefile.am !" >&2
 200     exit 1
 201   fi
 202 fi
 203
 204 echo
 205 echo "Rerunning autogen.sh..."
 206 ./autogen.sh