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

copyright=2010-2014

filename=`basename "$1" | sed 's,_template,,'`

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

/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */

/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */

/* Edit the template file instead:                     */
/* $1 */

EOF

me=$(basename "$0")

template=$1; shift

kind_decls=
kind_printers=
kind_to_theory_id=

type_constant_descriptions=
type_constant_list=
type_constant_to_theory_id=
type_cardinalities=
type_constant_cardinalities=
type_wellfoundednesses=
type_constant_wellfoundednesses=
type_groundterms=
type_constant_groundterms=
type_properties_includes=

seen_theory=false
seen_theory_builtin=false

theory_enum=
theory_descriptions=
theory_stats_prefixes=

function theory {
  # theory ID T header

  lineno=${BASH_LINENO[0]}

  if $seen_theory; then
    echo "$kf:$lineno: error: multiple theories defined in one file !?" >&2
    exit 1
  fi

  # 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"
  theory_enum="${theory_enum}  $1,
"
  theory_descriptions="${theory_descriptions}  case ${theory_id}: out << \"${theory_id}\"; break;
"
  prefix=$(echo "$theory_id" | tr '[:upper:]' '[:lower:]')
  theory_stats_prefixes="${theory_stats_prefixes}  case ${theory_id}: return \"theory::${prefix#theory_}\"; break;
"
}

function alternate {
  # alternate ID name T header

  lineno=${BASH_LINENO[0]}

  if $seen_theory; then
    echo "$kf:$lineno: error: multiple theories defined in one file !?" >&2
    exit 1
  fi

  seen_theory=true
  seen_endtheory=true
}

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

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

function enumerator {
  # enumerator KIND enumerator-class header
  lineno=${BASH_LINENO[0]}
  check_theory_seen
}

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 construle {
  # construle OPERATOR isconst-checking-class
  lineno=${BASH_LINENO[0]}
  check_theory_seen
}

function rewriter {
  # properties prop*
  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
  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 {
  # cardinality TYPE cardinality-computer [header]
  lineno=${BASH_LINENO[0]}
  check_theory_seen
  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"]

  lineno=${BASH_LINENO[0]}

  check_theory_seen
  register_kind "$1" 0 "$2"
}

function operator {
  # operator K #children ["comment"]

  lineno=${BASH_LINENO[0]}

  check_theory_seen
  register_kind "$1" "$2" "$3"
}

function parameterized {
  # parameterized K1 K2 #children ["comment"]

  lineno=${BASH_LINENO[0]}

  check_theory_seen
  register_kind "$1" "$3" "$4"
}

function constant {
  # constant K T Hasher header ["comment"]

  lineno=${BASH_LINENO[0]}

  check_theory_seen
  register_kind "$1" 0 "$5"
}

function nullaryoperator {
  # nullaryoperator K ["comment"]

  lineno=${BASH_LINENO[0]}

  check_theory_seen
  register_kind "$1" 0 "$2"
}

function register_sort {
  id=$1
  cardinality=$2
  wellfoundedness=$3
  groundterm=$4
  header=$5
  comment=$6

  type_constant_list="${type_constant_list}  ${id}, /**< ${comment} */
"
  type_constant_descriptions="${type_constant_descriptions}  case $id:  out << \"${comment}\"; break;
"
  type_constant_to_theory_id="${type_constant_to_theory_id}  case $id: return $theory_id;
"
  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 {
  id=$1
  cardinality_computer=$(sed 's,%TYPE%,typeNode,g' <<<"$2")
  header=$3

  type_cardinalities="${type_cardinalities}#line $lineno \"$kf\"
  case $id: return $cardinality_computer;
"
  if [ -n "$header" ]; then
    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
}

function register_kind {
  r=$1
  nc=$2
  comment=$3
  register_kind_counter=$[register_kind_counter+1]

  kind_decls="${kind_decls}  $r, /**< $comment ($register_kind_counter) */
"
  kind_printers="${kind_printers}  case $r: out << \"$r\"; break;
"
  kind_to_theory_id="${kind_to_theory_id}  case kind::$r: return $theory_id;
"
}

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"))
  kind_decls="${kind_decls}
  /* from $b */
"
  kind_printers="${kind_printers}
  /* from $b */
"
  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 \
    kind_decls \
    kind_printers \
    kind_to_theory_id \
    theory_enum \
    type_constant_list \
    type_constant_descriptions \
    type_constant_to_theory_id \
    type_cardinalities \
    type_constant_cardinalities \
    type_wellfoundednesses \
    type_constant_wellfoundednesses \
    type_groundterms \
    type_constant_groundterms \
    type_properties_includes \
    theory_descriptions \
    theory_stats_prefixes \
    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"