Skip to content

Commit

Permalink
Slightly restructure Statix documentation and add page on debugging t…
Browse files Browse the repository at this point in the history
…ricks.
  • Loading branch information
hendrikvanantwerpen committed Feb 10, 2021
1 parent 40cb48f commit 9cfa13f
Show file tree
Hide file tree
Showing 7 changed files with 436 additions and 34 deletions.
389 changes: 389 additions & 0 deletions source/langdev/meta/lang/statix/debugging.rst

Large diffs are not rendered by default.

29 changes: 29 additions & 0 deletions source/langdev/meta/lang/statix/getting-started.rst
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@
.. _statix-getting-started:

===============
Getting Started
===============

.. note::

Generate a language project that uses Statix by following :ref:`this guide<langdev-getting-started>` and selecting ``Statix`` for ``Analysis type``.

The best way to get started on Statix is to use the the lectures from the TU Delft compiler construction course.
These lectures explain the concepts that are used in Statix, and discuss scope graph patterns and Statix rules for several language features.
In particular, these are the relevant lectures:

- `Type Checking and Type Constraints <https://tudelft-cs4200-2020.github.io/lectures/2020/09/17/lecture4/>`_
introduces type checking concepts and the basics of Statix specifications.
- `Name Binding and Name Resolution <https://tudelft-cs4200-2020.github.io/lectures/2020/09/24/lecture5/>`_
introduces scope graphs in depth, discusses many name binding patterns in terms of scope graphs and queries,
and shows example Statix rules for many of these patterns.
- `Constraint Semantics and Constraint Resolution <https://tudelft-cs4200-2020.github.io/lectures/2020/10/01/lecture6/>`_
Discusses in the semantics of Statix and some of the algorithms that are used in its implementation.

The lecture pages also link to other presentations and tutorials on Statix and scope graphs.

Example projects using Statix can be found in `this reposity <https://github.com/metaborg/nabl/tree/master/statix.integrationtest/>`_.
The `STLCrec<https://github.com/metaborg/nabl/tree/master/statix.integrationtest/lang.stlcrec>`_ project is the simplest, and shows a simply-typed lambda calculus extended with structural records.
The `Units<https://github.com/metaborg/nabl/tree/master/statix.integrationtest/lang.units>`_ project contains definitions for a language that supports various module and package features.
The `FGJ<https://github.com/metaborg/nabl/tree/master/statix.integrationtest/lang.fgj>`_ project shows a more advanced specification for Featherweight Generic Java, showing scopes as types, complex scope graph patterns, and lazy-substitution-based generics.

20 changes: 2 additions & 18 deletions source/langdev/meta/lang/statix/index.rst
Original file line number Diff line number Diff line change
Expand Up @@ -11,29 +11,13 @@ In addition, statically typed languages require that expressions are consistentl
The Statix language supports the specification of name binding and type checking rules of a language.
The rules of the static semantics are written as logic rules, and solved using a constraint-based approach, and uses scope graphs for name resolution.

.. note::

The documentation in this section is currently very incomplete.
The best way to get started on Statix is to use the the lectures from the TU Delft compiler construction course.
These lectures explain the concepts that are used in Statix, and discuss scope graph patterns and Statix rules for several language features.
In particular, these are the relevant lectures:

- `Type Checking and Type Constraints <https://tudelft-cs4200-2020.github.io/lectures/2020/09/17/lecture4/>`_
introduces type checking concepts and the basics of Statix specifications.
- `Name Binding and Name Resolution <https://tudelft-cs4200-2020.github.io/lectures/2020/09/24/lecture5/>`_
introduces scope graphs in depth, discusses many name binding patterns in terms of scope graphs and queries,
and shows example Statix rules for many of these patterns.
- `Constraint Semantics and Constraint Resolution <https://tudelft-cs4200-2020.github.io/lectures/2020/10/01/lecture6/>`_
Discusses in the semantics of Statix and some of the algorithms that are used in its implementation.

The lecture pages also link to other presentations and tutorials on Statix and scope graphs.

.. toctree::
:maxdepth: 2
:numbered: 3
:caption: Table of Contents

usage
getting-started
debugging
reference
stratego-api
signature-generator
Expand Down
2 changes: 2 additions & 0 deletions source/langdev/meta/lang/statix/nabl2-migration.rst
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
.. _statix-nabl2-migration:

=====================
NaBL2 Migration Guide
=====================
Expand Down
22 changes: 10 additions & 12 deletions source/langdev/meta/lang/statix/reference.rst
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
.. _statix-reference:

==================
Language Reference
==================
Expand All @@ -13,6 +15,10 @@ Language Reference
This section gives a systematic overview of the Statix language.
Statix specifications are organized in modules, consisting of signatures and predicate rules.

.. warning::

This section is currently incomplete. The information that is there is up-to-date, but many constructs are not yet documented.

Lexical matters
---------------

Expand Down Expand Up @@ -249,7 +255,7 @@ patterns, where neither is more general than the other. There rules
are marked with an error.

*Example.* An ``or`` predicate that computes a logical or, with its
last argument the result.
last argument the result.

.. code-block:: statix
Expand Down Expand Up @@ -295,9 +301,9 @@ used in term positions, where they behave as a term of the output
type.

*Example.* Rule for a functional predicate to type check
expressions. The functional predicate ``typeOfExp`` is used in two
term positions: as the result of a fucntional rule, and in an
equality constraint.
expressions. The functional predicate ``typeOfExp`` is used in two
term positions: as the result of a fucntional rule, and in an
equality constraint.

.. code-block:: statix
Expand Down Expand Up @@ -340,11 +346,3 @@ Occurrences
Arithmetic
^^^^^^^^^^

Misc notes
----------

Error messages
^^^^^^^^^^^^^^

Debugging
^^^^^^^^^
4 changes: 4 additions & 0 deletions source/langdev/meta/lang/statix/stratego-api.rst
Original file line number Diff line number Diff line change
Expand Up @@ -8,3 +8,7 @@ Stratego API

The Stratego API to Statix ...

.. warning::

This section has not yet been written.

4 changes: 0 additions & 4 deletions source/langdev/meta/lang/statix/usage.rst

This file was deleted.

0 comments on commit 9cfa13f

Please sign in to comment.