From b883cc1ba1fd445da1cf774b2945e2462fe5e3bc Mon Sep 17 00:00:00 2001 From: Balletie Date: Sat, 25 Jun 2016 17:38:08 +0200 Subject: [PATCH 1/7] Initial skeleton of Spoofax REPL documentation --- requirements.txt | 2 +- .../langdev/manual/env/repl/configuration.rst | 27 +++++++++++++++++++ source/langdev/manual/env/repl/contact.rst | 3 +++ source/langdev/manual/env/repl/index.rst | 23 ++++++++++++++++ .../langdev/manual/env/repl/installation.rst | 6 +++++ source/langdev/manual/index.rst | 1 + 6 files changed, 61 insertions(+), 1 deletion(-) create mode 100644 source/langdev/manual/env/repl/configuration.rst create mode 100644 source/langdev/manual/env/repl/contact.rst create mode 100644 source/langdev/manual/env/repl/index.rst create mode 100644 source/langdev/manual/env/repl/installation.rst 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/repl/configuration.rst b/source/langdev/manual/env/repl/configuration.rst new file mode 100644 index 0000000..6015758 --- /dev/null +++ b/source/langdev/manual/env/repl/configuration.rst @@ -0,0 +1,27 @@ +============= +Configuration +============= + +The REPL supports the configuration of any language with a DynSem +specification. The configuration consists of two parts: the +configuration in the ESV, and the creation of DynSem rules specific to +the REPL. + +ESV configuration +----------------- + +The ESV configuration of the REPL supports setting two properties: the +evaluation method and the start symbol that is used inside of the +REPL. + +.. code-block:: esv + + module Shell + + shell + evaluation method : "dynsem" + shell start symbol : Expr + +When the user entered an expression, the REPL first tries to parse +using the start symbol as configured above. If that fails it, uses the +default start symbol as specified in the ESV as a fallback. diff --git a/source/langdev/manual/env/repl/contact.rst b/source/langdev/manual/env/repl/contact.rst new file mode 100644 index 0000000..bdf664d --- /dev/null +++ b/source/langdev/manual/env/repl/contact.rst @@ -0,0 +1,3 @@ +======= +Contact +======= diff --git a/source/langdev/manual/env/repl/index.rst b/source/langdev/manual/env/repl/index.rst new file mode 100644 index 0000000..d5f000c --- /dev/null +++ b/source/langdev/manual/env/repl/index.rst @@ -0,0 +1,23 @@ +================ +REPL environment +================ + +The **Spoofax REPL** provides an interactive environment for +evaluating expressions in your language, much like the REPLs provided +by for example Haskell and Python. The 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 REPL to work for your language. + +.. note:: The REPL 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 + contact diff --git a/source/langdev/manual/env/repl/installation.rst b/source/langdev/manual/env/repl/installation.rst new file mode 100644 index 0000000..44c6ac7 --- /dev/null +++ b/source/langdev/manual/env/repl/installation.rst @@ -0,0 +1,6 @@ +============ +Installation +============ + +There are two frontends for the REPL: one for the terminal, the other +in the form of an Eclipse plugin. diff --git a/source/langdev/manual/index.rst b/source/langdev/manual/index.rst index 7d7dd1b..2f966b3 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/repl/index project config From 8e6c290c1048940c62d8bb21562f0b41875f4846 Mon Sep 17 00:00:00 2001 From: Balletie Date: Tue, 28 Jun 2016 11:52:27 +0200 Subject: [PATCH 2/7] Add documentation and manual for configuring the REPL --- .../langdev/manual/env/repl/configuration.rst | 125 +++++++++++++++++- source/langdev/meta/lang/dynsem/index.rst | 2 + 2 files changed, 120 insertions(+), 7 deletions(-) diff --git a/source/langdev/manual/env/repl/configuration.rst b/source/langdev/manual/env/repl/configuration.rst index 6015758..41e7c52 100644 --- a/source/langdev/manual/env/repl/configuration.rst +++ b/source/langdev/manual/env/repl/configuration.rst @@ -3,9 +3,34 @@ Configuration ============= The REPL supports the configuration of any language with a DynSem -specification. The configuration consists of two parts: the -configuration in the ESV, and the creation of DynSem rules specific to -the REPL. +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 REPL. 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 REPL. 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 REPL. + +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 +REPL, which will be explained in the next section. ESV configuration ----------------- @@ -15,13 +40,99 @@ evaluation method and the start symbol that is used inside of the REPL. .. code-block:: esv + :linenos: module Shell shell - evaluation method : "dynsem" - shell start symbol : Expr + evaluation method : "dynsem" + shell start symbol : Shell When the user entered an expression, the REPL first tries to parse -using the start symbol as configured above. If that fails it, uses the -default start symbol as specified in the ESV as a fallback. +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 REPL-specific rules. The first is a rule for initializing the +execution environment for the REPL, shown below. The second are the +rules for implementing REPL-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 REPL. It instantiates the +semantic components that form the execution environment for the REPL: +an environment with an initial variable binding of :math:`x \mapsto +4`, and an empty store. The REPL 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 REPL are the read-write semantic components (in +this case, the environment and the store). + +REPL-specific semantics +~~~~~~~~~~~~~~~~~~~~~~~ + +The second kind of configuration are the rules for the REPL-specific +semantics. These can be seen as entry points for the REPL 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 +REPL-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 REPL. + +.. 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 REPL. In line 9, the +original specification is recursively invoked. 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 ====== From 1c06d8ba814b13420ab20eddc9931eabb4e22625 Mon Sep 17 00:00:00 2001 From: Balletie Date: Tue, 28 Jun 2016 12:16:31 +0200 Subject: [PATCH 3/7] Add short installation and contributing info --- source/langdev/manual/env/repl/contact.rst | 20 ++++++++++++--- .../langdev/manual/env/repl/installation.rst | 25 +++++++++++++++---- 2 files changed, 37 insertions(+), 8 deletions(-) diff --git a/source/langdev/manual/env/repl/contact.rst b/source/langdev/manual/env/repl/contact.rst index bdf664d..8d6cbb7 100644 --- a/source/langdev/manual/env/repl/contact.rst +++ b/source/langdev/manual/env/repl/contact.rst @@ -1,3 +1,17 @@ -======= -Contact -======= +============ +Contributing +============ + +The source code can be found at the GitHub `repository`_. If you have +found a bug, or have an issue with the REPL, please create an issue at +the `issues tracker`_. + +License +------- + +The Spoofax REPL is released under the permissive Apache 2.0 +`license`_. + +.. _repository: https://github.com/metaborg/spoofax-shell +.. _issues 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/repl/installation.rst b/source/langdev/manual/env/repl/installation.rst index 44c6ac7..cd4de7d 100644 --- a/source/langdev/manual/env/repl/installation.rst +++ b/source/langdev/manual/env/repl/installation.rst @@ -1,6 +1,21 @@ -============ -Installation -============ +====================== +Installation and Usage +====================== -There are two frontends for the REPL: one for the terminal, the other -in the form of an Eclipse plugin. +There are two clients for the REPL: 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. From 4a76f07b3f81bb7cb889ce3920799ce846d08850 Mon Sep 17 00:00:00 2001 From: Balletie Date: Tue, 28 Jun 2016 12:17:37 +0200 Subject: [PATCH 4/7] Rename contact.rst to contributing.rst --- .../langdev/manual/env/repl/{contact.rst => contributing.rst} | 0 source/langdev/manual/env/repl/index.rst | 2 +- 2 files changed, 1 insertion(+), 1 deletion(-) rename source/langdev/manual/env/repl/{contact.rst => contributing.rst} (100%) diff --git a/source/langdev/manual/env/repl/contact.rst b/source/langdev/manual/env/repl/contributing.rst similarity index 100% rename from source/langdev/manual/env/repl/contact.rst rename to source/langdev/manual/env/repl/contributing.rst diff --git a/source/langdev/manual/env/repl/index.rst b/source/langdev/manual/env/repl/index.rst index d5f000c..7914265 100644 --- a/source/langdev/manual/env/repl/index.rst +++ b/source/langdev/manual/env/repl/index.rst @@ -20,4 +20,4 @@ the REPL to work for your language. installation configuration - contact + contributing From de82a19b45567e2d0f4e420c77b4e4b4f4b885e8 Mon Sep 17 00:00:00 2001 From: Balletie Date: Fri, 1 Jul 2016 11:20:36 +0200 Subject: [PATCH 5/7] Use "shell" consistently, instead of both "shell" and "REPL" Feedback of @hendrikvanantwerpen --- .../langdev/manual/env/repl/configuration.rst | 44 +++++++++---------- .../langdev/manual/env/repl/contributing.rst | 8 ++-- source/langdev/manual/env/repl/index.rst | 23 +++++----- .../langdev/manual/env/repl/installation.rst | 6 +-- 4 files changed, 42 insertions(+), 39 deletions(-) diff --git a/source/langdev/manual/env/repl/configuration.rst b/source/langdev/manual/env/repl/configuration.rst index 41e7c52..a667183 100644 --- a/source/langdev/manual/env/repl/configuration.rst +++ b/source/langdev/manual/env/repl/configuration.rst @@ -2,18 +2,18 @@ Configuration ============= -The REPL supports the configuration of any language with a DynSem +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 REPL. We explain each +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 REPL. For example, Haskell's GHCi has the ``let x = +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 REPL. +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. @@ -30,14 +30,14 @@ specify a grammar rule for it as shown below. Shell.Let = = > {non-assoc} The start symbol is also specified in the ESV configuration of the -REPL, which will be explained in the next section. +shell, which will be explained in the next section. ESV configuration ----------------- -The ESV configuration of the REPL supports setting two properties: the +The ESV configuration of the shell supports setting two properties: the evaluation method and the start symbol that is used inside of the -REPL. +shell. .. code-block:: esv :linenos: @@ -48,7 +48,7 @@ REPL. evaluation method : "dynsem" shell start symbol : Shell -When the user entered an expression, the REPL first tries to parse +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. @@ -57,9 +57,9 @@ 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 REPL-specific rules. The first is a rule for initializing the -execution environment for the REPL, shown below. The second are the -rules for implementing REPL-specific semantics. +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 @@ -70,10 +70,10 @@ The initialization rule ~~~~~~~~~~~~~~~~~~~~~~~ The initialization rule shown below is evaluated upon the first -evaluation done after starting up the REPL. It instantiates the -semantic components that form the execution environment for the REPL: +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 REPL uses and updates the semantic +4`, and an empty store. The shell uses and updates the semantic components in its successive evaluations. .. code-block:: dynsem @@ -101,21 +101,21 @@ 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 REPL are the read-write semantic components (in +that is used by the shell are the read-write semantic components (in this case, the environment and the store). -REPL-specific semantics -~~~~~~~~~~~~~~~~~~~~~~~ +Shell-specific semantics +~~~~~~~~~~~~~~~~~~~~~~~~ -The second kind of configuration are the rules for the REPL-specific -semantics. These can be seen as entry points for the REPL to the +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 -REPL-specific syntax that we made earlier in this section. With 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 REPL. +successive evaluations done by the user of the shell. .. code-block:: dynsem :linenos: @@ -134,5 +134,5 @@ successive evaluations done by the user of the REPL. 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 REPL. In line 9, the +after execution should be available to the shell. In line 9, the original specification is recursively invoked. diff --git a/source/langdev/manual/env/repl/contributing.rst b/source/langdev/manual/env/repl/contributing.rst index 8d6cbb7..57b69bb 100644 --- a/source/langdev/manual/env/repl/contributing.rst +++ b/source/langdev/manual/env/repl/contributing.rst @@ -3,15 +3,15 @@ Contributing ============ The source code can be found at the GitHub `repository`_. If you have -found a bug, or have an issue with the REPL, please create an issue at -the `issues tracker`_. +found a bug, or have problem with the shell, please create an issue at +the `issue tracker`_. License ------- -The Spoofax REPL is released under the permissive Apache 2.0 +The Spoofax Shell is released under the permissive Apache 2.0 `license`_. .. _repository: https://github.com/metaborg/spoofax-shell -.. _issues tracker: https://github.com/metaborg/spoofax-shell/issues +.. _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/repl/index.rst b/source/langdev/manual/env/repl/index.rst index 7914265..6c88867 100644 --- a/source/langdev/manual/env/repl/index.rst +++ b/source/langdev/manual/env/repl/index.rst @@ -1,17 +1,18 @@ -================ -REPL environment -================ +================= +Shell environment +================= -The **Spoofax REPL** provides an interactive environment for -evaluating expressions in your language, much like the REPLs provided -by for example Haskell and Python. The REPL is useful for quickly -experimenting with code snippets, by allowing the code snippets to be -evaluated in the context of previous evaluations. +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 REPL to work for your language. +the shell to work for your language. -.. note:: The REPL for Spoofax is still in development. As such, it +.. note:: The shell for Spoofax is still in development. As such, it currently only supports languages that use DynSem for their dynamic semantics specification. @@ -21,3 +22,5 @@ the REPL to work for your language. installation configuration contributing + +.. _REPL: https://en.wikipedia.org/wiki/Read%E2%80%93eval%E2%80%93print_loop diff --git a/source/langdev/manual/env/repl/installation.rst b/source/langdev/manual/env/repl/installation.rst index cd4de7d..a02a044 100644 --- a/source/langdev/manual/env/repl/installation.rst +++ b/source/langdev/manual/env/repl/installation.rst @@ -2,9 +2,9 @@ Installation and Usage ====================== -There are two clients for the REPL: one for the terminal, the other -in the form of an Eclipse plugin. Their installation and usage is -explained in this section. +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 --------------- From eb081723a1ca9a81916cfe3778b78500d2647105 Mon Sep 17 00:00:00 2001 From: Balletie Date: Fri, 1 Jul 2016 11:24:07 +0200 Subject: [PATCH 6/7] Also rename folder from repl to shell --- source/langdev/manual/env/{repl => shell}/configuration.rst | 0 source/langdev/manual/env/{repl => shell}/contributing.rst | 0 source/langdev/manual/env/{repl => shell}/index.rst | 0 source/langdev/manual/env/{repl => shell}/installation.rst | 0 source/langdev/manual/index.rst | 2 +- 5 files changed, 1 insertion(+), 1 deletion(-) rename source/langdev/manual/env/{repl => shell}/configuration.rst (100%) rename source/langdev/manual/env/{repl => shell}/contributing.rst (100%) rename source/langdev/manual/env/{repl => shell}/index.rst (100%) rename source/langdev/manual/env/{repl => shell}/installation.rst (100%) diff --git a/source/langdev/manual/env/repl/configuration.rst b/source/langdev/manual/env/shell/configuration.rst similarity index 100% rename from source/langdev/manual/env/repl/configuration.rst rename to source/langdev/manual/env/shell/configuration.rst diff --git a/source/langdev/manual/env/repl/contributing.rst b/source/langdev/manual/env/shell/contributing.rst similarity index 100% rename from source/langdev/manual/env/repl/contributing.rst rename to source/langdev/manual/env/shell/contributing.rst diff --git a/source/langdev/manual/env/repl/index.rst b/source/langdev/manual/env/shell/index.rst similarity index 100% rename from source/langdev/manual/env/repl/index.rst rename to source/langdev/manual/env/shell/index.rst diff --git a/source/langdev/manual/env/repl/installation.rst b/source/langdev/manual/env/shell/installation.rst similarity index 100% rename from source/langdev/manual/env/repl/installation.rst rename to source/langdev/manual/env/shell/installation.rst diff --git a/source/langdev/manual/index.rst b/source/langdev/manual/index.rst index 2f966b3..0a853cd 100644 --- a/source/langdev/manual/index.rst +++ b/source/langdev/manual/index.rst @@ -9,6 +9,6 @@ Language Development Manual env/eclipse env/intellij/index - env/repl/index + env/shell/index project config From 9aa1c41e2b253d4d55401a30aab21e502e7a24d2 Mon Sep 17 00:00:00 2001 From: Balletie Date: Fri, 1 Jul 2016 11:24:28 +0200 Subject: [PATCH 7/7] Include document in main ToC at front page. --- index.rst | 1 + 1 file changed, 1 insertion(+) 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