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

copyright=2010-2012

cat <<EOF
/*********************                                                        */
/** instantiator_tables.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

instantiator_includes=
instantiator_class=
theory_id=
theory_class=
theory_header=

make_instantiator_cases=
instantiator=

seen_theory=false
seen_theory_builtin=false

function theory {
  # theory id T header

  lineno=${BASH_LINENO[0]}

  if $seen_theory; then
    echo "$kf:$lineno: theory declaration can only appear once" >&2
    exit 1;
  fi

  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"
  theory_class="$2"
  theory_header="$3"

  instantiator_class=
  instantiator=NULL
}

function instantiator {
  # instantiator class header
  lineno=${BASH_LINENO[0]}
  check_theory_seen

  if [ -n "$instantiator_class" ]; then
    echo "$kf:$lineno: error: cannot have two \"instantiator\" directives" >&2
    exit 1
  fi

  instantiator_class="$1"
  instantiator_header="$2"

  if [ -z "$instantiator_class" -o -z "$instantiator_header" ]; then
    echo "$kf:$lineno: error: \"instantiator\" directive missing class or header argument" >&2
    exit 1
  fi

  instantiator_includes="${instantiator_includes}#include \"$theory_header\"
#line $lineno \"$kf\"
#include \"$instantiator_header\"
"
  instantiator="new $instantiator_class(c, qe, static_cast< $theory_class* >(this))";
}

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

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

  make_instantiator_cases="${make_instantiator_cases}
#line $lineno \"$kf\"
  case $theory_id:
    return $instantiator;
"
}

function typechecker {
  # typechecker header
  lineno=${BASH_LINENO[0]}
  check_theory_seen
}

function typerule {
  # typerule OPERATOR typechecking-class
  lineno=${BASH_LINENO[0]}
  check_theory_seen
}

function rewriter {
  # rewriter class header
  lineno=${BASH_LINENO[0]}
  check_theory_seen
}

function sort {
  # sort TYPE cardinality [well-founded ground-term header | not-well-founded] ["comment"]
  lineno=${BASH_LINENO[0]}
  check_theory_seen
}

function cardinality {
  # cardinality TYPE cardinality-computer [header]
  lineno=${BASH_LINENO[0]}
  check_theory_seen
}

function well-founded {
  # well-founded TYPE wellfoundedness-computer [header]
  lineno=${BASH_LINENO[0]}
  check_theory_seen
}

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

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

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

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

function check_theory_seen {
  if $seen_endtheory; then
    echo "$kf:$lineno: error: command after \"endtheory\" declaration (endtheory has to be last)" >&2
    exit 1
  fi
  if ! $seen_theory; then
    echo "$kf:$lineno: error: no \"theory\" declaration found (it has to be first)" >&2
    exit 1
  fi
}

function check_builtin_theory_seen {
  if ! $seen_theory_builtin; then
    echo "$me: warning: no declaration for the builtin theory found" >&2
  fi
}

while [ $# -gt 0 ]; do
  kf=$1
  seen_theory=false
  seen_endtheory=false
  b=$(basename $(dirname "$kf"))
  source "$kf"
  if ! $seen_theory; then
    echo "$kf: error: no theory content found in file!" >&2
    exit 1
  fi
  if ! $seen_endtheory; then
    echo "$kf:$lineno: error: no \"endtheory\" declaration found (it is required at the end)" >&2
    exit 1
  fi
  shift
done
check_builtin_theory_seen

## output

# generate warnings about incorrect #line annotations in templates
nl -ba -s' ' "$template"  | grep '^ *[0-9][0-9]* # *line' |
  awk '{OFS="";if($1+1!=$3) print "'"$template"':",$1,": warning: incorrect annotation \"#line ",$3,"\" (it should be \"#line ",($1+1),"\")"}' >&2

text=$(cat "$template")
for var in \
    instantiator_includes \
    make_instantiator_cases \
    template \
    ; 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"