Theory Scala

(*:maxLineLen=78:*)

theory Scala
imports Base
begin

chapter ‹Isabelle/Scala systems programming \label{sec:scala}›

text ‹
  Isabelle/ML and Isabelle/Scala are the two main implementation languages of
  the Isabelle environment:

    ▪ Isabelle/ML is for ∗‹mathematics›, to develop tools within the context
    of symbolic logic, e.g.\ for constructing proofs or defining
    domain-specific formal languages. See the ∗‹Isabelle/Isar implementation
    manual› @{cite "isabelle-implementation"} for more details.

    ▪ Isabelle/Scala is for ∗‹physics›, to connect with the world of systems
    and services, including editors and IDE frameworks.

  There are various ways to access Isabelle/Scala modules and operations:

    ▪ Isabelle command-line tools (\secref{sec:scala-tools}) run in a separate
    Java process.

    ▪ Isabelle/ML antiquotations access Isabelle/Scala functions
    (\secref{sec:scala-functions}) via the PIDE protocol: execution happens
    within the running Java process underlying Isabelle/Scala.

    ▪ The ▩‹Console/Scala› plugin of Isabelle/jEdit @{cite "isabelle-jedit"}
    operates on the running Java application, using the Scala
    read-eval-print-loop (REPL).

  The main Isabelle/Scala functionality is provided by ▩‹Pure.jar›, but
  further add-ons are bundled with Isabelle, e.g.\ to access SQLite or
  PostgreSQL using JDBC (Java Database Connectivity).

  Other components may augment the system environment by providing a suitable
  \<^path>‹etc/settings› shell script in the component directory. Some shell
  functions are available to help with that:

    ▪ Function \<^bash_function>‹classpath› adds ▩‹jar› files in Isabelle path
    notation (POSIX). On Windows, this is converted to native path names
    before invoking @{tool java} or @{tool scala} (\secref{sec:scala-tools}).

    ▪ Function \<^bash_function>‹isabelle_scala_service› registers global
    service providers as subclasses of
    \<^scala_type>‹isabelle.Isabelle_System.Service›, using the raw Java name
    according to @{scala_method (in java.lang.Object) getClass} (it should be
    enclosed in single quotes to avoid special characters like ▩‹$› to be
    interpreted by the shell).

    Particular Isabelle/Scala services require particular subclasses:
    instances are filtered according to their dynamic type. For example, class
    \<^scala_type>‹isabelle.Isabelle_Scala_Tools› collects Scala command-line
    tools, and class \<^scala_type>‹isabelle.Scala.Functions›
    collects Scala functions (\secref{sec:scala-functions}).
›


section ‹Command-line tools \label{sec:scala-tools}›

subsection ‹Java Runtime Environment \label{sec:tool-java}›

text ‹
  The @{tool_def java} tool is a direct wrapper for the Java Runtime
  Environment, within the regular Isabelle settings environment
  (\secref{sec:settings}) and Isabelle classpath. The command line arguments
  are that of the bundled Java distribution: see option ▩‹-help› in
  particular.

  The ▩‹java› executable is taken from @{setting ISABELLE_JDK_HOME}, according
  to the standard directory layout for regular distributions of OpenJDK.

  The shell function \<^bash_function>‹isabelle_jdk› allows shell scripts to
  invoke other Java tools robustly (e.g.\ ▩‹isabelle_jdk jar›), without
  depending on accidental operating system installations.
›


subsection ‹Scala toplevel \label{sec:tool-scala}›

text ‹
  The @{tool_def scala} tool is a direct wrapper for the Scala toplevel,
  similar to @{tool java} above. The command line arguments are that of the
  bundled Scala distribution: see option ▩‹-help› in particular. This allows
  to interact with Isabelle/Scala interactively.
›

subsubsection ‹Example›

text ‹
  Explore the Isabelle system environment in Scala:
  @{verbatim [display, indent = 2] ‹$ isabelle scala›}
  @{scala [display, indent = 2]
‹import isabelle._

val isabelle_home = Isabelle_System.getenv("ISABELLE_HOME")

val options = Options.init()
options.bool("browser_info")
options.string("document")›}
›


subsection ‹Scala compiler \label{sec:tool-scalac}›

text ‹
  The @{tool_def scalac} tool is a direct wrapper for the Scala compiler; see
  also @{tool scala} above. The command line arguments are that of the
  bundled Scala distribution.

  This allows to compile further Scala modules, depending on existing
  Isabelle/Scala functionality. The resulting ▩‹class› or ▩‹jar› files can be
  added to the Java classpath using the shell function
  \<^bash_function>‹classpath›. Thus add-on components can register themselves
  in a modular manner, see also \secref{sec:components}.

  Note that Isabelle/jEdit @{cite "isabelle-jedit"} has its own mechanisms for
  adding plugin components. This needs special attention, since it overrides
  the standard Java class loader.
›


subsection ‹Scala script wrapper›

text ‹
  The executable @{executable "$ISABELLE_HOME/bin/isabelle_scala_script"}
  allows to run Isabelle/Scala source files stand-alone programs, by using a
  suitable ``hash-bang'' line and executable file permissions. For example:
  @{verbatim [display, indent = 2] ‹#!/usr/bin/env isabelle_scala_script›}
  @{scala [display, indent = 2]
‹val options = isabelle.Options.init()
Console.println("browser_info = " + options.bool("browser_info"))
Console.println("document = " + options.string("document"))›}

  This assumes that the executable may be found via the @{setting PATH} from
  the process environment: this is the case when Isabelle settings are active,
  e.g.\ in the context of the main Isabelle tool wrapper
  \secref{sec:isabelle-tool}. Alternatively, the full
  🗏‹$ISABELLE_HOME/bin/isabelle_scala_script› may be specified in expanded
  form.
›


subsection ‹Project setup for common Scala IDEs›

text ‹
  The @{tool_def scala_project} tool creates a project configuration for
  Isabelle/Scala/jEdit:
  @{verbatim [display]
‹Usage: isabelle scala_project [OPTIONS] PROJECT_DIR

  Options are:
    -L           make symlinks to original scala files

  Setup Gradle project for Isabelle/Scala/jEdit --- to support Scala IDEs
  such as IntelliJ IDEA.›}

  The generated configuration is for Gradle⁋‹🌐‹https://gradle.org››, but the
  main purpose is to import it into common Scala IDEs, such as IntelliJ
  IDEA⁋‹🌐‹https://www.jetbrains.com/idea››. This allows to explore the
  sources with static analysis and other hints in real-time.

  The specified project directory needs to be fresh. The generated files refer
  to physical file-system locations, using the path notation of the underlying
  OS platform. Thus the project needs to be recreated whenever the Isabelle
  installation is changed or moved.

  ┉
  By default, Scala sources are ∗‹copied› from the Isabelle distribution and
  editing them within the IDE has no permanent effect.

  Option ▩‹-L› produces ∗‹symlinks› to the original files: this allows to
  develop Isabelle/Scala/jEdit within an external Scala IDE. Note that
  building the result always requires ▩‹isabelle jedit -b› on the
  command-line.
›


section ‹Registered Isabelle/Scala functions \label{sec:scala-functions}›

subsection ‹Defining functions in Isabelle/Scala›

text ‹
  A Scala functions of type \<^scala_type>‹String => String› may be wrapped as
  \<^scala_type>‹isabelle.Scala.Fun› and collected via an instance of the
  class \<^scala_type>‹isabelle.Scala.Functions›. A system component
  can then register that class via \<^bash_function>‹isabelle_scala_service›
  in \<^path>‹etc/settings› (\secref{sec:components}). An example is the
  predefined collection of \<^scala_type>‹isabelle.Scala.Functions› in
  Isabelle/▩‹Pure.jar› with the following line in
  🗏‹$ISABELLE_HOME/etc/settings›:
  @{verbatim [display, indent = 2] ‹isabelle_scala_service 'isabelle.Functions'›}

  The overall list of registered functions is accessible in Isabelle/Scala as
  \<^scala_object>‹isabelle.Scala.functions›.
›


subsection ‹Invoking functions in Isabelle/ML›

text ‹
  Isabelle/PIDE provides a protocol to invoke registered Scala functions in
  ML: this works both within the Prover IDE and in batch builds.

  The subsequent ML antiquotations refer to Scala functions in a
  formally-checked manner.

  \begin{matharray}{rcl}
  @{ML_antiquotation_def "scala_function"} & : & ‹ML_antiquotation› \\
  @{ML_antiquotation_def "scala"} & : & ‹ML_antiquotation› \\
  @{ML_antiquotation_def "scala_thread"} & : & ‹ML_antiquotation› \\
  \end{matharray}

  \<^rail>‹
    (@{ML_antiquotation scala_function} |
     @{ML_antiquotation scala} |
     @{ML_antiquotation scala_thread}) @{syntax embedded}
  ›

  ➧ ‹@{scala_function name}› inlines the checked function name as ML string
    literal.

  ➧ ‹@{scala name}› and ‹@{scala_thread name}› invoke the checked function via
  the PIDE protocol. In Isabelle/ML this appears as a function of type
  \<^ML_type>‹string -> string›, which is subject to interrupts within the ML
  runtime environment as usual. A \<^scala>‹null› result in Scala raises an
  exception \<^ML>‹Scala.Null› in ML. The execution of ‹@{scala}› works via a
  Scala future on a bounded thread farm, while ‹@{scala_thread}› always forks
  a separate Java thread.

  The standard approach of representing datatypes via strings works via XML in
  YXML transfer syntax. See Isabelle/ML operations and modules @{ML
  YXML.string_of_body}, @{ML YXML.parse_body}, @{ML_structure XML.Encode},
  @{ML_structure XML.Decode}; similarly for Isabelle/Scala. Isabelle symbols
  may have to be recoded via Scala operations
  \<^scala_method>‹isabelle.Symbol.decode› and
  \<^scala_method>‹isabelle.Symbol.encode›.
›


subsubsection ‹Examples›

text ‹
  Invoke the predefined Scala function \<^scala_function>‹echo›:
›

ML ‹
  val s = "test";
  val s' = \<^scala>‹echo› s;
  \<^assert> (s = s')
›

text ‹
  Let the Scala compiler process some toplevel declarations, producing a list
  of errors:
›

ML ‹
  val source = "class A(a: Int, b: Boolean)"
  val errors =
    \<^scala>‹scala_toplevel› source
    |> YXML.parse_body
    |> let open XML.Decode in list string end;

  \<^assert> (null errors)›

text ‹
  The above is merely for demonstration. See \<^ML>‹Scala_Compiler.toplevel›
  for a more convenient version with builtin decoding and treatment of errors.
›


section ‹Documenting Isabelle/Scala entities›

text ‹
  The subsequent document antiquotations help to document Isabelle/Scala
  entities, with formal checking of names against the Isabelle classpath.

  \begin{matharray}{rcl}
  @{antiquotation_def "scala"} & : & ‹antiquotation› \\
  @{antiquotation_def "scala_object"} & : & ‹antiquotation› \\
  @{antiquotation_def "scala_type"} & : & ‹antiquotation› \\
  @{antiquotation_def "scala_method"} & : & ‹antiquotation› \\
  \end{matharray}

  \<^rail>‹
    (@@{antiquotation scala} | @@{antiquotation scala_object})
      @{syntax embedded}
    ;
    @@{antiquotation scala_type} @{syntax embedded} types
    ;
    @@{antiquotation scala_method} class @{syntax embedded} types args
    ;
    class: ('(' @'in' @{syntax name} types ')')?
    ;
    types: ('[' (@{syntax name} ',' +) ']')?
    ;
    args: ('(' (nat | (('_' | @{syntax name}) + ',')) ')')?
  ›

  ➧ ‹@{scala s}› is similar to ‹@{verbatim s}›, but the given source text is
  checked by the Scala compiler as toplevel declaration (without evaluation).
  This allows to write Isabelle/Scala examples that are statically checked.

  ➧ ‹@{scala_object x}› checks the given Scala object name (simple value or
  ground module) and prints the result verbatim.

  ➧ ‹@{scala_type T[A]}› checks the given Scala type name (with optional type
  parameters) and prints the result verbatim.

  ➧ ‹@{scala_method (in c[A]) m[B](n)}› checks the given Scala method ‹m› in
  the context of class ‹c›. The method argument slots are either specified by
  a number ‹n› or by a list of (optional) argument types; this may refer to
  type variables specified for the class or method: ‹A› or ‹B› above.

  Everything except for the method name ‹m› is optional. The absence of the
  class context means that this is a static method. The absence of arguments
  with types means that the method can be determined uniquely as ▩‹(›‹m›▩‹ _)›
  in Scala (no overloading).
›


subsubsection ‹Examples›

text ‹
  Miscellaneous Isabelle/Scala entities:

    ▪ object: \<^scala_object>‹isabelle.Isabelle_Process›
    ▪ type without parameter: @{scala_type isabelle.Console_Progress}
    ▪ type with parameter: @{scala_type List[A]}
    ▪ static method: \<^scala_method>‹isabelle.Isabelle_System.bash›
    ▪ class and method with type parameters:
      @{scala_method (in List[A]) map[B]("A => B")}
    ▪ overloaded method with argument type: @{scala_method (in Int) "+" (Int)}
›

end