###############################################################################
# Top contributors (to current version):
#   Makai Mann, Mathias Preiner, Andres Noetzli
#
# 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.
# #############################################################################
#
# The build system configuration.
##

# Check that scikit-build is installed
# Provides CMake files for Python bindings
check_python_module("skbuild" "scikit-build")

# setuptools for installing the module
check_python_module("setuptools")

# Find cmake modules distributed with scikit-build
# They are distributed under <scikit-build directory>/resources/cmake

# This 'sys.stdout' hack is needed because importing skbuild prints to stdout
# in some versions, and this stores the wrong value to OUTPUT_VARIABLE. 
# Once scikit is removed, this whole command will be removed too.
execute_process(
  COMMAND
    ${Python_EXECUTABLE} -c "from __future__ import print_function; \
      import os; import sys; \
      sys.stdout = open(os.devnull, 'w'); \
      import skbuild; \
      sys.stdout = sys.__stdout__; \
      cmake_module_path=os.path.join(os.path.dirname(skbuild.__file__), \
        'resources', 'cmake'); print(cmake_module_path, end='')"
  OUTPUT_VARIABLE
    SKBUILD_CMAKE_MODULE_PATH
  RESULT_VARIABLE
    RET_SKBUILD_CMAKE_MODULE_PATH
)

if (NOT EXISTS ${SKBUILD_CMAKE_MODULE_PATH})
  message(FATAL_ERROR "Expected CMake module path from
                       scikit-build at ${SKBUILD_CMAKE_MODULE_PATH}")
endif()

# Add scikit-build cmake files to cmake module path
# Required for Cython target below
list(APPEND CMAKE_MODULE_PATH ${SKBUILD_CMAKE_MODULE_PATH})

find_package(Python ${BUILD_BINDINGS_PYTHON_VERSION} EXACT COMPONENTS Development)
# Some cmake packages are not compatible with the newest version
# of FindPython, introduced in cmake 3.12.
# We define the symbols below to be backward compatible.
# FindPython Development sets Python_INCLUDE_DIRS and Python_LIBRARIES
if (NOT DEFINED PYTHON_INCLUDE_DIRS)
  set(PYTHON_INCLUDE_DIRS "${Python_INCLUDE_DIRS}")
endif()
if (NOT DEFINED PYTHON_LIBRARIES)
  set(PYTHON_LIBRARIES "${Python_LIBRARIES}")
endif()

find_package(PythonExtensions REQUIRED)
find_package(Cython 3.0.0 REQUIRED)

set(CYTHON_FLAGS "-X embedsignature=True")

configure_file(genenums.py.in genenums.py)

# Generate cvc5kinds.{pxd,pxi}
set(GENERATED_KINDS_FILES
  "${CMAKE_CURRENT_BINARY_DIR}/cvc5kinds.pxd"
  "${CMAKE_CURRENT_BINARY_DIR}/cvc5kinds.pxi"
)
add_custom_command(
  OUTPUT
    ${GENERATED_KINDS_FILES}
  COMMAND
    "${Python_EXECUTABLE}"
    "${CMAKE_CURRENT_BINARY_DIR}/genenums.py"
    --enums-header "${PROJECT_SOURCE_DIR}/include/cvc5/cvc5_kind.h"
    --enums-file-prefix "${CMAKE_CURRENT_BINARY_DIR}/cvc5kinds"
  DEPENDS
    "${CMAKE_CURRENT_BINARY_DIR}/genenums.py"
    "${PROJECT_SOURCE_DIR}/src/api/parseenums.py"
    "${PROJECT_SOURCE_DIR}/include/cvc5/cvc5_kind.h"
)
add_custom_target(cvc5kinds DEPENDS ${GENERATED_KINDS_FILES})

# Generate cvc5proofrules.{pxd,pxi}
set(GENERATED_PROOF_RULES_FILES
  "${CMAKE_CURRENT_BINARY_DIR}/cvc5proofrules.pxd"
  "${CMAKE_CURRENT_BINARY_DIR}/cvc5proofrules.pxi"
)
add_custom_command(
  OUTPUT
    ${GENERATED_PROOF_RULES_FILES}
  COMMAND
    "${Python_EXECUTABLE}"
    "${CMAKE_CURRENT_BINARY_DIR}/genenums.py"
    --enums-header "${PROJECT_SOURCE_DIR}/include/cvc5/cvc5_proof_rule.h"
    --enums-file-prefix "${CMAKE_CURRENT_BINARY_DIR}/cvc5proofrules"
  DEPENDS
    "${CMAKE_CURRENT_BINARY_DIR}/genenums.py"
    "${PROJECT_SOURCE_DIR}/src/api/parseenums.py"
    "${PROJECT_SOURCE_DIR}/include/cvc5/cvc5_proof_rule.h"
)
add_custom_target(cvc5proofrules DEPENDS ${GENERATED_PROOF_RULES_FILES})


set(GENERATED_TYPES_FILES
  "${CMAKE_CURRENT_BINARY_DIR}/cvc5types.pxd"
  "${CMAKE_CURRENT_BINARY_DIR}/cvc5types.pxi"
)
add_custom_command(
  OUTPUT
    ${GENERATED_TYPES_FILES}
  COMMAND
    "${Python_EXECUTABLE}"
    "${CMAKE_CURRENT_BINARY_DIR}/genenums.py"
    --enums-header "${PROJECT_SOURCE_DIR}/include/cvc5/cvc5_types.h"
    --enums-file-prefix "${CMAKE_CURRENT_BINARY_DIR}/cvc5types"
  DEPENDS
    "${CMAKE_CURRENT_BINARY_DIR}/genenums.py"
    "${PROJECT_SOURCE_DIR}/src/api/parseenums.py"
    "${PROJECT_SOURCE_DIR}/include/cvc5/cvc5_types.h"
)
add_custom_target(cvc5types DEPENDS ${GENERATED_TYPES_FILES})

include_directories(${CMAKE_CURRENT_BINARY_DIR})   # for cvc5kinds.pxi
add_cython_target(cvc5_python_base CXX)

add_library(cvc5_python_base
            MODULE
            cvc5_python_base)
add_dependencies(cvc5_python_base cvc5kinds cvc5types cvc5proofrules )

target_include_directories(cvc5_python_base
  PRIVATE
  ${PYTHON_INCLUDE_DIRS}
  ${PROJECT_SOURCE_DIR}/include   # for public API headers
  ${CMAKE_BINARY_DIR}/include     # for cvc5_export.h
)

target_link_libraries(cvc5_python_base cvc5parser cvc5)

# Disable -Werror and other warnings for code generated by Cython.
set(PY_SRC_FLAGS "")
check_cxx_compiler_flag("-Werror" HAVE_CXX_FLAGWerror)
if(HAVE_CXX_FLAGWerror)
  set(PY_SRC_FLAGS "${PY_SRC_FLAGS} -Wno-error")
endif()
check_cxx_compiler_flag("-Wshadow" HAVE_CXX_FLAGWshadow)
if(HAVE_CXX_FLAGWshadow)
  set(PY_SRC_FLAGS "${PY_SRC_FLAGS} -Wno-shadow")
endif()
check_cxx_compiler_flag("-Wimplicit-fallthrough" HAVE_CXX_FLAGWimplicit_fallthrough)
if(HAVE_CXX_FLAGWimplicit_fallthrough)
  set(PY_SRC_FLAGS "${PY_SRC_FLAGS} -Wno-implicit-fallthrough")
endif()
# Note: Visibility is reset to default here since otherwise the PyInit_...
# function will not be exported correctly
# (https://github.com/cython/cython/issues/3380).
set_target_properties(cvc5_python_base
                      PROPERTIES
                      COMPILE_FLAGS "${PY_SRC_FLAGS}"
                      CXX_VISIBILITY_PRESET default
                      VISIBILITY_INLINES_HIDDEN 0
                      LIBRARY_OUTPUT_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}/cvc5")

python_extension_module(cvc5_python_base)

# Copy the pythonic API to the right place. It does not come with its own
# installation routine and consists only of a few files that need to go to
# the right place.
#find_package(CVC5PythonicAPI)

#set(COPIED_PYTHONIC_FILES
#  "${CMAKE_CURRENT_BINARY_DIR}/cvc5/pythonic/__init__.py"
#  "${CMAKE_CURRENT_BINARY_DIR}/cvc5/pythonic/cvc5_pythonic.py"
#  "${CMAKE_CURRENT_BINARY_DIR}/cvc5/pythonic/cvc5_pythonic_printer.py"
#)

#add_custom_command(
#  OUTPUT
#    ${COPIED_PYTHONIC_FILES}
#  COMMAND
#    ${CMAKE_COMMAND} -E copy_directory
#    "${CVC5PythonicAPI_BASEDIR}/cvc5_pythonic_api"
#    "${CMAKE_CURRENT_BINARY_DIR}/cvc5/pythonic"
  # Remove the license of the Pythonic API from the package's source files.
  # The license file is included in the package's dist-info dir by setup()
#  COMMAND
#    ${CMAKE_COMMAND} -E remove
#    "${CMAKE_CURRENT_BINARY_DIR}/cvc5/pythonic/LICENSE.txt"
#  DEPENDS cvc5_python_base CVC5PythonicAPI
#)

#add_custom_target(cvc5_python_api ALL DEPENDS ${COPIED_PYTHONIC_FILES})

set(LICENSE_FILES
  "${CMAKE_BINARY_DIR}/COPYING"
  "${CMAKE_BINARY_DIR}/licenses/lgpl-3.0.txt"
  "${CMAKE_BINARY_DIR}/licenses/pythonic-LICENSE"
)

add_custom_command(
  OUTPUT
    ${LICENSE_FILES}
  COMMAND
    ${CMAKE_COMMAND} -E copy
    "${PROJECT_SOURCE_DIR}/COPYING"
    "${CMAKE_BINARY_DIR}/COPYING"
  COMMAND
    ${CMAKE_COMMAND} -E copy_directory
    "${PROJECT_SOURCE_DIR}/licenses"
    "${CMAKE_BINARY_DIR}/licenses"
  COMMAND
    ${CMAKE_COMMAND} -E copy
    "${CVC5PythonicAPI_BASEDIR}/cvc5_pythonic_api/LICENSE.txt"
    "${CMAKE_BINARY_DIR}/licenses/pythonic-LICENSE"
  DEPENDS CVC5PythonicAPI
)

# Copy license files to build directory where setup() can find them
add_custom_target(cvc5_python_licenses DEPENDS ${LICENSE_FILES})

# Installation based on https://bloerg.net/2012/11/10/cmake-and-distutils.html
# Create a wrapper python directory and generate a distutils setup.py file
configure_file(setup.py.in setup.py)
configure_file(__init__.py.in cvc5/__init__.py)

# figure out if we're in a virtualenv
execute_process(OUTPUT_VARIABLE IN_VIRTUALENV
  COMMAND
  "${Python_EXECUTABLE}"
  -c
  "from __future__ import print_function; import os;
print('YES' if 'VIRTUAL_ENV' in os.environ else 'NO', end='')")

set(INSTALL_CMD
    "${Python_EXECUTABLE} ${CMAKE_CURRENT_BINARY_DIR}/setup.py install")
# if we're in a virtualenv, we install it in the virtualenv lib location
# otherwise install in site-packages
# option --single-version-externally-managed prevents it from being
# an .egg distribution and --record records the list of installed files
if ("${IN_VIRTUALENV}" STREQUAL "NO")
  set(INSTALL_CMD "${INSTALL_CMD}
          --root=\$ENV{DESTDIR}
          --single-version-externally-managed
          --install-layout=deb
          --record=cvc5-installed-files.txt")
endif()

message("Python bindings install command: ${INSTALL_CMD}")

install(CODE "execute_process(COMMAND ${INSTALL_CMD})"
        FILE_PERMISSIONS OWNER_EXECUTE OWNER_WRITE OWNER_READ)