package yuujinchou

README.mkd

# Yuujinchou: Name Manipulation Combinators

_Yuujinchou_ is a tiny OCaml combinator library for manipulating names. It was motivated by the practical need in implementing the `import` or `include` statements that are present in almost all programming languages. Here are some examples of such statements:
```agda
open import M -- Agda
```
```python
import foo # Python
```
The ability to import content from other files is a prerequisite of organizing large-scale software. However, it also brings up new design issues: how could programmers avoid imported content from colliding or shadowing the content in the current scope? For example, maybe in the current scope we have defined a function called `test`, and do not want to import another function also called `test`. To address this, many programming languages allow programmers to selectively hide or rename part of the imported content:
```agda
open import M renaming (a to b) public -- renaming a to b, and then re-exporting the content
```
```python
import foo as bar # putting content of foo under the prefix bar
```
We can treat the hiding or renaming as a partial function from names to names. One can take this aspect seriously and vastly generalize the mechanism into a fully-fledged combinator library. This library is the result of such thinking---a concise yet powerful (perhaps overkilling) combinator language for manipulating names in programming languages.

## Applications

This library was motivated by the import mechanism in most programming languages, but can be used in any situation involving selecting names. For example, during interactive theorem proving, perhaps you want to unfold some definitions but not others. This library gives you a powerful language to support fancy name selection.

## Technical Overview

### Hierarchical Names

We assume names are hierarchical and can be encoded as lists of strings. For example, the name `a.b` is represented as an OCaml list `["a"; "b"]`.

### Core Language and Pattern Builders

See [combinators](doc/combinators.mkd) for a detailed explanation of the core language. The core language is not directly accissible. Instead, you should build a pattern by the pattern builders in the `Pattern` module, which are documented in [the library wrapper file](src/yuujinchou.mli).

### Running Patterns

The pattern matching engine is the `run` function in the `Action` module, again documented in [the library wrapper file](src/yuujinchou.mli). The result of pattern matching is one of the following:

1. ```Ok `NoMatch```: the pattern runs successfully but does not match the name.
2. ```Ok `Matched [(name1, attr1); (name2, attr2); ...]```: the pattern matches the name but it was renamed into other names, tagged with attributes. It is possible that the set of new names is empty despite the old name being matched because we support the intersection (meet) operator.
3. ```Error error```: the pattern is ill-formed.

It is crucial to understand the concept "mode" and "attribute" before running it:

#### Modes

There are two modes of the pattern matching engine: the _normal_ mode and the _inverse_ mode. The motivation to have the inverse mode is to hide names from being imported. Think about the pattern `a.b`, which would normally select the name `a.b` from the imported content. Its dual meaning---selecting everything _other than_ the name `a.b`---is exactly the hiding operator we are looking for. The inverse mode has been extended to the entire core language and the [details are explained in another document](doc/combinators.mkd). It is recommended to study how the core language works under the normal mode first.

#### Attributes

Attributes are custom tags attached to matched names. For example, you could attach `Public` or `Private` to names when implementing the import statement. You need to supply a lattice structure for your attribute type `t` via the following three values:

1. A default value of type `t`.

> The default attribute attached to the new names until the engine encounters the `PatAttr` pattern that explicitly sets the new default attribute.

2. A join operator of type `t -> t -> t`.

> An operator to resolve the conflicting attributes by taking their "union". The exact meaning of "union" depends on the lattice structure. This is used in the sequencing combinator and the join combinator.

3. A meet operator of type `t -> t -> t`:

> An operator to resolve the conflicting attributes by taking their "intersection". The exact meaning of "intersection" depends on the lattice structure. This is used in the meet combinator.

For example, when implementing the traditional import statement, the attribute type can be
```ocaml
type attr = Public | Private
```
You can then implement the meet and join operators by making `Pubilc` the top element and `Private` the bottom element in a lattice. The rationale is that if a name is simultanously imported as a public name (to be re-exported) and a private name (not to be re-exported), then in most programming languages it _will_ be re-exported. This suggests that the join operator should outputs `Public` whenever one of the inputs is `Public`. It seems natural to make the meet operator the dual of the join operator.
```
let join_attr a1 a2 =
  match a1, a2 with
  | Public, _ | _, Public -> Public
  | Private, Private -> Private

let meet_attr a1 a2 =
  match a1, a2 with
  | Private, _ | _, Private -> Private
  | Public, Public -> Public
```

### Namespace Support

This library intends to treat a namespace as the prefix of a group of names. That is, there is no namespace `a`, but only a group of unrelated names that happen to have the prefix `a`.

Note that namespaces (name prefixes of unrelated declarations) are different from modules (groups of declarations that are bound together). This library does not provide special support for modules (yet).

## Examples

### Haskell

```haskell
import Mod -- x is available an both x and Mod.x
```
```ocaml
join [any; renaming_prefix [] ["Mod"]]
```

---

```haskell
import Mod (x,y)
```
```ocaml
join [id ["x"]; id ["y"]]
```

---

```haskell
import qualified Mod
```
```ocaml
join [renaming_prefix [] ["Mod"]]
```

---

```haskell
import qualified Mod hiding (x,y)
```
```ocaml
renaming_scope [] ["Mod"] @@ meet [skip ["x"]; skip ["y"]]
```