contrib/new-theory

   1 #!/bin/bash
   2 #
   3 # usage: new-theory theory-directory-name
   4 #
   5
   6 cd "`dirname "$0"`/.."
   7
   8 if [ ! -e src/theory/theory_engine.h ]; then
   9   echo "ERROR: This script doesn't appear to be the contrib/ subdirectory" >&2
  10   echo "ERROR: of the CVC4 source tree." >&2
  11   exit 1
  12 fi
  13
  14 if [ $# -ne 1 ]; then
  15   echo "usage: new-theory theory-directory-name" >&2
  16   echo "e.g.:  new-theory arith" >&2
  17   echo "e.g.:  new-theory arrays" >&2
  18   echo "e.g.:  new-theory sets" >&2
  19   echo "e.g.:  new-theory rewrite_rules" >&2
  20   echo >&2
  21   echo "This tool will create a new src/theory/<theory-directory-name>" >&2
  22   echo "directory and fill in some infrastructural files in that directory." >&2
  23   echo "It also will incorporate that directory into the build process." >&2
  24   echo "Please refer to the file README.WHATS-NEXT file created in that" >&2
  25   echo "directory for tips on what to do next."
  26   echo
  27   echo "Theories with multiple words (e.g. \"rewrite_rules\") should have" >&2
  28   echo "directories and namespaces separated by an underscore (_).  The" >&2
  29   echo "resulting class names created by this script will be in CamelCase" >&2
  30   echo "(e.g. RewriteRules) if that convention is followed." >&2
  31   exit 1
  32 fi
  33
  34 dir="$1"
  35
  36 if [ -e "src/theory/$dir" ]; then
  37   echo "ERROR: Theory \"$dir\" already exists." >&2
  38   echo "ERROR: Please choose a new directory name (or move that one aside)." >&2
  39   exit 1
  40 fi
  41
  42 if ! expr "$dir" : '[a-zA-Z][a-zA-Z0-9_]*$' &>/dev/null ||
  43    expr "$dir" : '_$' &>/dev/null; then
  44   echo "ERROR: \"$dir\" is not a valid theory name." >&2
  45   echo "ERROR:" >&2
  46   echo "ERROR: Theory names must start with a letter and be composed of" >&2
  47   echo "ERROR: letters, numbers, and the underscore (_) character; an" >&2
  48   echo "ERROR: underscore cannot be the final character." >&2
  49   exit 1
  50 fi
  51
  52 id="`echo "$dir" | tr a-z A-Z`"
  53 # convoluted, but should be relatively portable and give a CamelCase
  54 # representation for a string.  (e.g. "foo_bar" becomes "FooBar")
  55 camel="`echo "$dir" | awk 'BEGIN { RS="_";ORS="";OFS="" } // {print toupper(substr($1,1,1)),substr($1,2,length($1))} END {print "\n"}'`"
  56
  57 if ! mkdir "src/theory/$dir"; then
  58   echo "ERROR: encountered an error creating directory src/theory/$dir" >&2
  59   exit 1
  60 fi
  61
  62 echo "Theory of $dir"
  63 echo "Theory directory: src/theory/$dir"
  64 echo "Theory id: THEORY_$id"
  65 echo "Theory class: CVC4::theory::$dir::Theory$camel"
  66 echo
  67
  68 function copyskel {
  69   src="$1"
  70   dest="`echo "$src" | sed "s/DIR/$dir/g"`"
  71   echo "Creating src/theory/$dir/$dest..."
  72   sed "s/\$dir/$dir/g;s/\$camel/$camel/g;s/\$id/$id/g" \
  73     contrib/theoryskel/$src \
  74     > "src/theory/$dir/$dest"
  75 }
  76
  77 # copy files from the skeleton, with proper replacements
  78 for file in `ls contrib/theoryskel`; do
  79   copyskel "$file"
  80 done
  81
  82 echo
  83 echo "Adding $dir to SUBDIRS in src/theory/Makefile.am..."
  84 if grep -q '^SUBDIRS = .*[^a-zA-Z0-9_]'"$dir"'\([^a-zA-Z0-9_]\|$\)' src/theory/Makefile.am &>/dev/null; then
  85   echo "NOTE: src/theory/Makefile.am already descends into dir $dir"
  86 else
  87   awk '/^SUBDIRS = / {print $0,"'"$dir"'"} !/^SUBDIRS = / {print$0}' src/theory/Makefile.am > src/theory/Makefile.am.new-theory
  88   if ! cp -f src/theory/Makefile.am src/theory/Makefile.am~; then
  89     echo "ERROR: cannot copy src/theory/Makefile.am !" >&2
  90     exit 1
  91   fi
  92   if ! mv -f src/theory/Makefile.am.new-theory src/theory/Makefile.am; then
  93     echo "ERROR: cannot replace src/theory/Makefile.am !" >&2
  94     exit 1
  95   fi
  96 fi
  97
  98 echo "Adding lib$theory.la to LIBADD in src/theory/Makefile.am..."
  99 if grep -q '^   @builddir@/'"$dir"'/lib'"$dir"'\.la\>' src/theory/Makefile.am &>/dev/null; then
 100   echo "NOTE: src/theory/Makefile.am already seems to include lib$theory.la"
 101 else
 102   awk '!/^libtheory_la_LIBADD = / {print$0} /^libtheory_la_LIBADD = / {while(/\\ *$/){print $0;getline} print $0,"\\";print "\t@builddir@/'"$dir"'/lib'"$dir"'.la"}' src/theory/Makefile.am > src/theory/Makefile.am.new-theory
 103   if ! cp -f src/theory/Makefile.am src/theory/Makefile.am~; then
 104     echo "ERROR: cannot copy src/theory/Makefile.am !" >&2
 105     exit 1
 106   fi
 107   if ! mv -f src/theory/Makefile.am.new-theory src/theory/Makefile.am; then
 108     echo "ERROR: cannot replace src/theory/Makefile.am !" >&2
 109     exit 1
 110   fi
 111 fi
 112
 113 echo
 114 echo "Rerunning autogen.sh..."
 115 ./autogen.sh