diff --git a/index.rst b/index.rst index 5522001..ad30987 100644 --- a/index.rst +++ b/index.rst @@ -30,6 +30,7 @@ Quick Start - Manual - :doc:`source/langdev/manual/env/intellij/index` + - :doc:`source/langdev/manual/env/shell/index` - :doc:`source/langdev/manual/config` - Meta-Languages diff --git a/requirements.txt b/requirements.txt index f495ed2..3601070 100644 --- a/requirements.txt +++ b/requirements.txt @@ -4,4 +4,4 @@ recommonmark>=0.4.0 sphinx_rtd_theme>=0.1.9 pygments>=2.1.3 javasphinx>=0.9.13 -git+https://github.com/metaborg/metaborg-pygments.git@master#egg=metaborg-pygments +git+https://github.com/spoofax-shell/metaborg-pygments.git@master#egg=metaborg-pygments diff --git a/source/langdev/manual/env/shell/configuration.rst b/source/langdev/manual/env/shell/configuration.rst new file mode 100644 index 0000000..a667183 --- /dev/null +++ b/source/langdev/manual/env/shell/configuration.rst @@ -0,0 +1,138 @@ +============= +Configuration +============= + +The shell supports the configuration of any language with a DynSem +specification. The configuration consists of three parts: the +(optional) extension of the syntax, the configuration in the ESV, and +the creation of DynSem rules specific to the shell. We explain each +part of the configuration with a running example. + +Extending the syntax definition +------------------------------- +Sometimes a language has a slightly different syntax inside the +context of a shell. For example, Haskell's GHCi has the ``let x = +`` syntax for defining new variables and functions. In our +example, we try to replicate the same behavior for our shell. + +To extend the syntax, we use a new start symbol called ``Shell``, and +specify a grammar rule for it as shown below. + +.. code-block:: sdf3 + :linenos: + + context-free start-symbols + // Define it as start symbol. + Prog Shell + + context-free syntax + // Syntax for the Shell. + Shell.Let = = > {non-assoc} + +The start symbol is also specified in the ESV configuration of the +shell, which will be explained in the next section. + +ESV configuration +----------------- + +The ESV configuration of the shell supports setting two properties: the +evaluation method and the start symbol that is used inside of the +shell. + +.. code-block:: esv + :linenos: + + module Shell + + shell + evaluation method : "dynsem" + shell start symbol : Shell + +When the user entered an expression, the shell first tries to parse +using the start symbol as configured above. If that fails, it uses the +ordinary start symbol as a fallback. + +Extending the DynSem specification +---------------------------------- + +To allow expressions to be evaluated in the context of previous +evaluations, one has to extend one's DynSem specification with two +kinds of shell-specific rules. The first is a rule for initializing the +execution environment for the shell, shown below. The second are the +rules for implementing shell-specific semantics. + +.. note:: This section assumes basic knowledge of DynSem, and that + your language already has a DynSem specification. To learn + more about DynSem, refer to the + :ref:`DynSem documentation `. + +The initialization rule +~~~~~~~~~~~~~~~~~~~~~~~ + +The initialization rule shown below is evaluated upon the first +evaluation done after starting up the shell. It instantiates the +semantic components that form the execution environment for the shell: +an environment with an initial variable binding of :math:`x \mapsto +4`, and an empty store. The shell uses and updates the semantic +components in its successive evaluations. + +.. code-block:: dynsem + :linenos: + + signature + + sorts + ShellInit + + constructors + ShellInit : ShellInit + + arrows + // Note: the ShellInit rule must have this exact signature. + ShellInit -init-> ShellInit + + rules + // Initialization of shell state: an environment with "x" bound to 4, + // and an empty store. + ShellInit() -init-> ShellInit() :: Env { "x" |--> NumV(4) }, Store {}. + +The rule must have the exact signature as shown above. That is, the +sort must be of the name ``ShellInit``, with an arity of +zero. Furthermore, the input of the rule must be ``ShellInit``, and +its name must be ``init``. The result value of the rule can be +anything, as it is discarded. The only part of the result of this rule +that is used by the shell are the read-write semantic components (in +this case, the environment and the store). + +Shell-specific semantics +~~~~~~~~~~~~~~~~~~~~~~~~ + +The second kind of configuration are the rules for the shell-specific +semantics. These can be seen as entry points for the shell to the +interpreter. The rules are all named ``shell``, so that they are +distinct of the ordinary semantics. An example of such a rule is shown +below: it implements binding the result of an expression to a +variable. This rule specifies the dynamic semantics of the +shell-specific syntax that we made earlier in this section. With the +specification of this rule, the bound variable can be used in +successive evaluations done by the user of the shell. + +.. code-block:: dynsem + :linenos: + + signature + arrows + Expr -shell-> V + + rules + // let x = 2 + Let(x, e) :: E -shell-> v :: E' + where + E |- e :: Store {} --> v :: Store _; + E |- bindVar(x, v) --> E'. + +Note that the environment ``E`` is passed as a *read-write* component, +instead of a *read-only* component. This is because in this case the +environment *should* be writable, since the resulting environment +after execution should be available to the shell. In line 9, the +original specification is recursively invoked. diff --git a/source/langdev/manual/env/shell/contributing.rst b/source/langdev/manual/env/shell/contributing.rst new file mode 100644 index 0000000..57b69bb --- /dev/null +++ b/source/langdev/manual/env/shell/contributing.rst @@ -0,0 +1,17 @@ +============ +Contributing +============ + +The source code can be found at the GitHub `repository`_. If you have +found a bug, or have problem with the shell, please create an issue at +the `issue tracker`_. + +License +------- + +The Spoofax Shell is released under the permissive Apache 2.0 +`license`_. + +.. _repository: https://github.com/metaborg/spoofax-shell +.. _issue tracker: https://github.com/metaborg/spoofax-shell/issues +.. _license: https://github.com/metaborg/spoofax-shell/blob/master/LICENSE diff --git a/source/langdev/manual/env/shell/index.rst b/source/langdev/manual/env/shell/index.rst new file mode 100644 index 0000000..6c88867 --- /dev/null +++ b/source/langdev/manual/env/shell/index.rst @@ -0,0 +1,26 @@ +================= +Shell environment +================= + +The **Spoofax Shell** provides an interactive environment for +evaluating expressions in your language, much like the shells provided +by for example Haskell and Python. An interactive shell (sometimes +also called a `REPL`_) is useful for quickly experimenting with code +snippets, by allowing the code snippets to be evaluated in the context +of previous evaluations. + +This part of the documentation explains how to install and configure +the shell to work for your language. + +.. note:: The shell for Spoofax is still in development. As such, it + currently only supports languages that use DynSem for their dynamic + semantics specification. + +.. toctree:: + :maxdepth: 1 + + installation + configuration + contributing + +.. _REPL: https://en.wikipedia.org/wiki/Read%E2%80%93eval%E2%80%93print_loop diff --git a/source/langdev/manual/env/shell/installation.rst b/source/langdev/manual/env/shell/installation.rst new file mode 100644 index 0000000..a02a044 --- /dev/null +++ b/source/langdev/manual/env/shell/installation.rst @@ -0,0 +1,21 @@ +====================== +Installation and Usage +====================== + +There are two clients for the Spoofax Shell: one for the terminal, the +other in the form of an Eclipse plugin. Their installation and usage +is explained in this section. + +Terminal client +--------------- + +The download location, installation and usage details of the terminal +client are available on the `release page`_. Run ``:help`` to show a +list of commands that are available. + +.. _release page: https://github.com/spoofax-shell/spoofax-shell/releases/tag/v0.0.3-SNAPSHOT + +Eclipse plugin +-------------- + +.. todo:: This has not been written yet. diff --git a/source/langdev/manual/index.rst b/source/langdev/manual/index.rst index 7d7dd1b..0a853cd 100644 --- a/source/langdev/manual/index.rst +++ b/source/langdev/manual/index.rst @@ -9,5 +9,6 @@ Language Development Manual env/eclipse env/intellij/index + env/shell/index project config diff --git a/source/langdev/meta/lang/dynsem/index.rst b/source/langdev/meta/lang/dynsem/index.rst index f9f7345..fe5d168 100644 --- a/source/langdev/meta/lang/dynsem/index.rst +++ b/source/langdev/meta/lang/dynsem/index.rst @@ -1,3 +1,5 @@ +.. _dynsemdocumentation: + ====== DynSem ======