#!/bin/bash
#
# mkrewriter
# Morgan Deters <mdeters@cs.nyu.edu> for CVC4
# Copyright (c) 2010  The CVC4 Project
#
# The purpose of this script is to create kind.h from a template and a
# list of theory kinds.
#
# Invocation:
#
#   mkkind template-file theory-kind-files...
#
# Output is to standard out.
#

copyright=2010

cat <<EOF
/*********************                                                        */
/** kind.h
 **
 ** Copyright $copyright  The AcSys Group, New York University, and as below.
 **
 ** This header file automatically generated by:
 **
 **     $0 $@
 **
 ** for the CVC4 project.
 **/

EOF

me=$(basename "$0")

template=$1; shift

rewriter_includes= 
rewrite_init=
rewrite_shutdown=

pre_rewrite_calls= 
pre_rewrite_get_cache= 
pre_rewrite_set_cache=

post_rewrite_calls=
post_rewrite_get_cache= 
post_rewrite_set_cache=

seen_theory=false
seen_theory_builtin=false

function theory {
  # theory T header

  lineno=${BASH_LINENO[0]}

  # this script doesn't care about the theory class information, but
  # makes does make sure it's there
  seen_theory=true
  if [ "$1" = THEORY_BUILTIN ]; then
    if $seen_theory_builtin; then
      echo "$kf:$lineno: error: \"builtin\" theory redefined" >&2
      exit 1
    fi
    seen_theory_builtin=true
  elif [ -z "$1" -o -z "$2" -o -z "$3" ]; then
    echo "$kf:$lineno: error: \"theory\" directive missing class or header argument" >&2
    exit 1
  elif ! expr "$2" : '\(::*\)' >/dev/null; then
    echo "$kf:$lineno: warning: theory class \`$2' isn't fully-qualified (e.g., ::CVC4::theory::foo)" >&2
  elif ! expr "$2" : '\(::CVC4::theory::*\)' >/dev/null; then
    echo "$kf:$lineno: warning: theory class not under ::CVC4::theory namespace" >&2
  fi
  
  theory_id="$1"  
}

function properties {
  # properties prop*
  lineno=${BASH_LINENO[0]}
}

function endtheory {
  # endtheory
  lineno=${BASH_LINENO[0]}
}

function rewriter {
  # rewriter class header
  class="$1" 
  header="$2"
  
  rewriter_includes="${rewriter_includes}#include \"$header\"
"
  rewrite_init="${rewrite_init}   ${class}::init();
"
  rewrite_shutdown="${rewrite_shutdown}    ${class}::shutdown(); 
"

  pre_rewrite_calls="${pre_rewrite_calls}    case ${theory_id}: return ${class}::preRewrite(node);
"
  pre_rewrite_get_cache="${pre_rewrite_get_cache}    case ${theory_id}: return RewriteAttibute<${theory_id}>::getPreRewriteCache(node); 
"
  pre_rewrite_set_cache="${pre_rewrite_set_cache}    case ${theory_id}: return RewriteAttibute<${theory_id}>::setPreRewriteCache(node, cache); 
"

  post_rewrite_calls="${post_rewrite_calls}    case ${theory_id}: return ${class}::postRewrite(node);
"
  post_rewrite_get_cache="${post_rewrite_get_cache}    case ${theory_id}: return RewriteAttibute<${theory_id}>::getPostRewriteCache(node); 
" 
  post_rewrite_set_cache="${post_rewrite_set_cache}    case ${theory_id}: return RewriteAttibute<${theory_id}>::setPostRewriteCache(node, cache); 
"

  lineno=${BASH_LINENO[0]}
  
}

function sort {
  # sort TYPE ["comment"]  
  lineno=${BASH_LINENO[0]}
}

function variable {
  # variable K ["comment"]
  lineno=${BASH_LINENO[0]}
}

function operator {
  # operator K #children ["comment"]
  lineno=${BASH_LINENO[0]}
}

function parameterized {
  # parameterized K1 K2 #children ["comment"]
  lineno=${BASH_LINENO[0]}
}

function constant {
  # constant K T Hasher header ["comment"]
  lineno=${BASH_LINENO[0]}
}

while [ $# -gt 0 ]; do
  kf=$1
  seen_theory=false
  b=$(basename $(dirname "$kf"))
  source "$kf"
  check_theory_seen
  shift
done
check_builtin_theory_seen

## output

text=$(cat "$template")
for var in rewriter_includes pre_rewrite_calls post_rewrite_calls pre_rewrite_get_cache post_rewrite_get_cache pre_rewrite_set_cache post_rewrite_set_cache rewrite_init rewrite_shutdown; do
  eval text="\${text//\\\$\\{$var\\}/\${$var}}"
done
error=`expr "$text" : '.*\${\([^}]*\)}.*'`
if [ -n "$error" ]; then
  echo "$template:0: error: undefined replacement \${$error}" >&2
  exit 1
fi
echo "$text"