Literate Programming

Idris2 supports several types of literate mode styles.

The unlit’n has been designed based such that we assume that we are parsing markdown-like languages The unlit’n is performed by a Lexer that uses a provided literate style to recognise code blocks and code lines. Anything else is ignored. Idris2 also provides support for recognising both ‘visible’ and ‘invisible’ code blocks using ‘native features’ of each literate style.

A literate style consists of:

a list of String encoded code block deliminators;
a list of line indicators; and
a list of valid file extensions.

Lexing is simple and greedy in that when consuming anything that is a code blocks we treat everything as code until we reach the closing deliminator. This means that use of verbatim modes in a literate file will also be treated as active code.

In future we should add support for literate LaTeX files, and potentially other common document formats. But more importantly, a more intelligent processing of literate documents using a pandoc like library in Idris such as: Edda <https://github.com/jfdm/edda> would also be welcome.

Bird Style Literate Files

We treat files with an extension of .lidr as bird style literate files.

Bird notation is a classic literate mode found in Haskell, (and Orwell) in which visible code lines begin with > and hidden lines with <. Other lines are treated as documentation.

Note

We have diverged from lhs2tex in which < is traditionally used to display inactive code. Bird-style is presented as is, and we recommended use of the other styles for much more comprehensive literate mode.

Embedding in Markdown-like documents

While Bird Style literate mode is useful, it does not lend itself well to more modern markdown-like notations such as Org-Mode and CommonMark. Idris2 also provides support for recognising both ‘visible’ and ‘invisible’ code blocks and lines in both CommonMark and OrgMode documents using native code blocks and lines..

The idea being is that:

Visible content will be kept in the pretty printer’s output;
Invisible content will be removed; and
Specifications will be displayed as is and not touched by the compiler.

OrgMode

We treat files with an extension of .org as org-style literate files. Each of the following markup is recognised regardless of case:

Org mode source blocks for idris sans options are recognised as visible code blocks:
```
#+begin_src idris
data Nat = Z | S Nat
#+end_src
```
Comment blocks that begin with #+BEGIN_COMMENT idris are treated as invisible code blocks:
```
#+begin_comment idris
data Nat = Z | S Nat
#+end_comment
```
Visible code lines, and specifications, are not supported. Invisible code lines are denoted with #+IDRIS::
```
#+IDRIS: data Nat = Z | S Nat
```

Specifications can be given using OrgModes plain source or example blocks:

#+begin_src
map : (f : a -> b)
   -> List a
   -> List b
map f _ = Nil
#+end_src

CommonMark

We treat files with an extension of .md and .markdown as CommonMark style literate files.

CommonMark source blocks for idris sans options are recognised as visible code blocks:
```
```idris
data Nat = Z | S Nat
```

~~~idris
data Nat = Z | S Nat
~~~
```
Comment blocks of the form  are treated as invisible code blocks:
```

```
Code lines are not supported.

Specifications can be given using CommonMark’s pre-formatted blocks (indented by four spaces) or unlabelled code blocks.:

Compare

```idris
map : (f : a -> b)
   -> List a
   -> List b
map f _ = Nil
```

with

    map : (f : a -> b)
       -> List a
       -> List b
    map f _ = Nil

LaTeX

We treat files with an extension of .tex and .ltx as LaTeX style literate files.

We treat environments named code as visible code blocks:

\begin{code}
data Nat = Z | S Nat
\end{code}

We treat environments named hidden as invisible code blocks:

\begin{hidden}
data Nat = Z | S Nat
\end{hidden}

Code lines are not supported.
Specifications can be given using user defined environments.

We do not provide definitions for these code blocks and ask the user to define them. With one such example using fancyverbatim and comment packages as:

\usepackage{fancyvrb}
\DefineVerbatimEnvironment
  {code}{Verbatim}
  {}

\usepackage{comment}

\excludecomment{hidden}