#!/usr/bin/env python
###############################################################################
# Top contributors (to current version):
#   Andres Noetzli, Mudathir Mohamed, Aina Niemetz
#
# This file is part of the cvc5 project.
#
# Copyright (c) 2009-2023 by the authors listed in the file AUTHORS
# in the top-level source directory and their institutional affiliations.
# All rights reserved.  See the file COPYING in the top-level source
# directory for licensing information.
# #############################################################################
##
"""
This script reads cvc5/src/api/cpp/cvc5_kind.h and generates
cvc5/Kind.java file which declares all cvc5 kinds.
"""

import argparse
import os
import sys
import re
import textwrap

# get access to cvc5/src/api/parseenums.py
SOURCE_DIR = '${CMAKE_SOURCE_DIR}/src'
sys.path.insert(0, os.path.abspath(f'{SOURCE_DIR}/api'))

from parseenums import *

#################### Default Filenames ################
DEFAULT_PREFIX = 'Kind'

# Code Blocks

ENUM_JAVA_TOP = \
    r"""package io.github.{namespace};

import io.github.cvc5.CVC5ApiException;
import java.util.HashMap;
import java.util.Map;

public enum {name}
{{
"""

ENUM_JAVA_BOTTOM = \
    r""";

  /* the int value of the {name} */
  private int value;
  private static int minValue = 0;
  private static int maxValue = 0;
  private static Map<Integer, {name}> enumMap = new HashMap<>();

  private {name}(int value)
  {{
    this.value = value;
  }}

  static
  {{
    boolean firstValue = true;
    for ({name} enumerator : {name}.values())
    {{
      int value = enumerator.getValue();
      if (firstValue)
      {{
        minValue = value;
        maxValue = value;
        firstValue = false;
      }}
      minValue = Math.min(minValue, value);
      maxValue = Math.max(maxValue, value);
      enumMap.put(value, enumerator);
    }}
  }}

  public static {name} fromInt(int value) throws CVC5ApiException
  {{
    if (value < minValue || value > maxValue)
    {{
      throw new CVC5ApiException("{name} value " + value + " is outside the valid range ["
          + minValue + "," + maxValue + "]");
    }}
    return enumMap.get(value);
  }}

  public int getValue()
  {{
    return value;
  }}
}}
"""

# mapping from c++ patterns to java
# The order of this map matters, the earlier rules are applied first.
CPP_JAVA_MAPPING = \
    {
        r"\bbool\b": "boolean",
        r"\bconst\b ?": "",
        r"\bint32_t\b": "int",
        r"\bint64_t\b": "long",
        r"\buint32_t\b": "int",
        r"\buint64_t\b": "long",
        r"\bunsigned char\b": "byte",
        r"cvc5::": "cvc5.",
        r"Term::Term\(\)": "{@link Term#Term()}",
        r"ProofRule::(.*?)>": r"{@link ProofRule#\1}>",
        r"([a-zA-Z]*)::(.*?\))": r"{@link \1#\2}",
        r"std::vector<int>": "int[]",
        r"std::vector<Term>": "Term[]",
        r"std::vector<Sort>": "Sort[]",
        r"std::vector<DatatypeDecl>": "DatatypeDecl[]",
        r"std::optional<std::string>" : "String",
        r"std::string": "String",
        r".. note::": "@api.note",
        r".. warning::": "@api.note",
        r"&": "",
        r"::": ".",
        r">": "&gt;",
        r"<": "&lt;",
        r" -- ": " &ndash; ",
        r"@note": "@api.note",
        r"\\rst": "",
        r"\\endrst": "",
        r"\\verbatim embed:rst:leading-asterisk\s*\n": "",
        r"\\endverbatim": "",
        r"(?s)\*\*(.*?)\*\*": r"\1",
        r"``(.*?)``": r"{@code \1}",
        r":cpp:[a-z]*:`(.*?)`": r"\1",
        r"({@code.*)&gt;": r"\1>",
    }

# This splits along math annotations. There are two possible annotations: ":math:`...`"
# and ".. math::" with indentation.  In both cases the result of matching is TAG, CONTENT.
# We use TAG to determine that we shold not apply any replacements to CONTENT and instead
# wrap CONTENT in "{@code ...}".  Note that this has to use four pattern groups, hence
# it will add spurious "None" entries in the list generated by `re.split(...)`.
#          (start tag  indented content lines  an empty or unindented line) OR (inline start tag  content)
#              |                        |                    |              |    |                 |
#              +-----------+            |                    |    +---------+    | +---------------+
#                          |            |                    |    |      +-------+ |
#                          v            v                    v    v      v         v
CPP_SPLIT_MATH = r"(?:(.. math::)((?:\n+  .+)+\n)(?=(?=\s*\n)|\S))|(?:(:math:)`([^`]*)`)"

# Converts RST lists to HTML lists.  This is much more permissive then the RST specs.
# RST compatible lists are converted correctly, but it might produce garbage in other
# cases.
def format_list(comment):
    lines = []
    indents = [] # Stores the indentation levels
    for line in comment.split('\n'):
        l = line[4:] # Strip " *  "
        # Skip blank lines
        if not l.strip():
            lines.append(line)
            continue
        spaces = re.search(r'\S', l).start()
        is_item = l[spaces:].startswith("- ")

        if len(indents) == 0:
            # Normal lines get appended
            if not is_item:
                lines.append(line)
                continue
            else:
                # Start a list
                lines.append( '   * <ul>')
                lines.append(f'   * <li>{l[spaces + 2:]}')
                indents.append(spaces)
                continue
        # This is a continuation of the current item
        if not is_item and spaces >= indents[-1] + 2:
            lines.append(line)
            continue
        # This is a new item
        if is_item and spaces == indents[-1]:
            lines.append( '   * </li>')
            lines.append(f'   * <li>{l[spaces + 2:]}')
            continue
        # This is a new sublist
        if is_item and spaces > indents[-1]:
            lines.append( '   * <ul>')
            lines.append(f'   * <li>{l[spaces + 2:]}')
            indents.append(spaces)
            continue
        # If we are here, we are in a list, but the current line
        # is not indented enough.
        while len(indents) > 0:
            indents.pop()
            # Close sublist
            lines.append( '   * </li></ul>')
            # The last indentation is a special case
            if len(indents) == 1:
                if is_item:
                    lines.append( '   * </li>')
                    lines.append(f'   * <li>{l[spaces + 2:]}')
                if not is_item:
                    lines.append( '   * </li></ul>')
                    indents.pop()
                    lines.append(line)
                break
            if len(indents) == 0 or spaces > indents[-1]:
                if is_item:
                    lines.append( '   * </li>')
                    lines.append(f'   * <li>{l[spaces + 2:]}')
                if not is_item:
                    lines.append(line)
                break
    return '\n'.join(lines)


# convert from c++ doc to java doc
def format_comment(comment):
    # We do not want to apply any replacement within math strings.
    components = re.split(CPP_SPLIT_MATH, comment)
    comment = ""
    i = 0
    while i < len(components):
        component = components[i]
        # Skip spurious None introduced by the empty capture groups.
        if component == None:
            i = i + 1
            continue
        if component == ":math:" or component == ".. math::":
            insert = components[i+1].replace(">", "&gt;").replace("<", "&lt;")
            i = i + 2
            if component == ":math:":
                comment += "\(" + insert + "\)"
            else:
                comment += "\[" + insert + "\]"
        else:
            for pattern, replacement in CPP_JAVA_MAPPING.items():
                component = re.sub(pattern, replacement, component)
            comment += component
            i = i + 1
    comment = """  /**\n{}\n   */""".format(
            textwrap.indent(comment, '   * ', lambda line: True))
    comment = comment.replace("- {@link Solver#mkString(std.wstring)}", "")
    comment = format_list(comment)
    return comment


# Files generation
def gen_java(parser: EnumParser, path):
    for namespace in parser.namespaces:
        for enum in namespace.enums:
            subnamespace = namespace.name.replace('::', '.')
            filedir = os.path.join(path, subnamespace.replace('.', '/'))
            if not os.path.exists(filedir):
                os.mkdir(filedir)
            filename = os.path.join(filedir, enum.name + ".java")
            with open(filename, "w") as f:
                code = ENUM_JAVA_TOP.format(name=enum.name,
                                            namespace=subnamespace)
                for name, value in enum.enumerators.items():
                    comment = enum.enumerators_doc.get(name, '')
                    comment = format_comment(comment)
                    code += "{comment}\n  {name}({enum_value}),\n".format(
                        comment=comment, name=name, enum_value=value)
                code += ENUM_JAVA_BOTTOM.format(name=enum.name)
                f.write(code)


if __name__ == "__main__":
    parser = argparse.ArgumentParser(
        'Read an enums header file and generate a '
        'corresponding java file')
    parser.add_argument('--enums-header',
                        metavar='<ENUMS_HEADER>',
                        help='The header file to read enums from')
    parser.add_argument('--java-api-path',
                        metavar='<ENUMS_FILE_PREFIX>',
                        help='The prefix for the generated .java file',
                        default=DEFAULT_PREFIX)

    args = parser.parse_args()
    enums_header = args.enums_header
    java_api_path = args.java_api_path

    ep = EnumParser()
    ep.parse(enums_header)

    gen_java(ep, java_api_path)