## Modal: a tree rewriting system

This repository contains a small implementation of Modal, a homoiconic tree‑rewriting language. Modal programs are collections of rewrite rules applied to a tree until no rule matches. See the original description for background and examples: [Modal in a Postcard](https://wiki.xxiivv.com/site/modal).

### Core concepts

- **Program**: an ordered list of rules. Rule order matters; the first matching rule is applied.
- **Tree**: symbolic S‑expressions (atoms and lists), serialized with parentheses.
- **Rule**: `<> left right`, where `left` and `right` are trees. Matching is structural.
- **Registers**: variables in patterns prefixed with `?` (e.g., `?x`). They bind to subtrees during a match and are substituted on the right side.
- **Evaluation**: scan the serialized tree left‑to‑right; at each node, try rules top‑to‑bottom; on first match, replace the matched subtree with the rule’s right side (with current bindings) and restart scanning from the beginning. Halt when a full scan finds no match.

### Syntax quick reference

- Atom: `word` or a quoted symbol like `(0)` used in number encoding.
- Tree: `(head tail...)` or nested pairs to encode lists, e.g., `(a (b (c ())))`.
- Rule: `<> (a bat) (a black cat)`.
- Register: `?name` in the left or right side; repeated occurrences must match the same subtree.

### Minimal operational semantics

1. Parsing: read tokens into an AST of `Atom(value)` or `List([nodes...])`.
2. Matching: `match(pattern, tree, env)`
   - If `pattern` is a register `?r` and `?r` unbound: bind `env[r] = tree`.
   - If `pattern` is a register `?r` and bound: require structural equality with `env[r]`.
   - If both atoms: require exact equality.
   - If both lists: same arity; match element‑wise recursively.
   - Otherwise: fail.
3. Rewriting: substitute registers in the right‑hand side using `env`, producing a new subtree.
4. Driver loop:
   - Linearize the AST positions in left‑to‑right preorder over the serialized form.
   - For each position, try rules in order; on first success, perform rewrite and restart from the beginning.
   - If no rewrite happened in a full pass, halt.

### Numbers and common encodings

- Natural numbers: unary parentheses around `0`:
  - `0` = 0, `(0)` = 1, `((0))` = 2, `(((0)))` = 3, ...
- Lists: nested pairs ending with `()` (nil): `(a (b (c ())))`.

### Examples

Rules:

```modal
<> (copy ?a) (?a ?a)
<> (swap ?x ?y) (?y ?x)
```

Input and result:

```modal
(copy cat) (swap bat rat)
(cat cat) (swap bat rat)
(cat cat) (rat bat)
```

Conditionals via boolean tables and a ternary (see reference):

```modal
<> (ife #t ?t ?f) ?t
<> (ife #f ?t ?f) ?f
```

Unary subtraction:

```modal
<> ((?a) - (?b)) (?a - ?b)
<> (?a - 0) (difference ?a)
```

### Side effects and IO

The language core is pure rewriting. Implementations may expose host effects via special registers. The reference uses `?:` to emit symbols to the console (e.g., `(print (sum ?:))`). Treat such registers as implementation‑defined hooks that consume or produce host effects during rewriting. Keep them minimal and explicit.

### Implementation guide (porting to another language)

- Data model:
  - AST types: `Atom`, `List`.
  - Rule: `{ left: Node, right: Node }`.
  - Environment: map from register name to bound `Node`.
- Parser:
  - Tokenize `(` `)` and atoms; build AST; preserve atom spelling verbatim.
  - Identify registers by leading `?` at parse or match time.
- Matcher:
  - Structural recursion with immutable `env`; fail fast on arity/shape mismatch.
  - Registers are single‑assignment within a match; repeated occurrences unify.
- Rewriter:
  - Deep substitute registers in `right` using `env`; do not capture or mutate `env` across matches.
- Evaluator:
  - Left‑to‑right scan order over the current tree; rule priority is program order.
  - On rewrite, replace exactly the matched subtree, then restart scanning from the root.
  - Terminate when a full scan applies zero rewrites.
- IO hooks (optional):
  - Dispatch atoms/registers like `?:` to host functions with explicit semantics.
  - Keep IO operations deterministic relative to rewrite steps.

### Determinism and termination

- Determinism depends on rule order; different orders may yield different results.
- Termination is not guaranteed; design rules with explicit base cases.

### Repository layout

- `modal.c`: reference implementation (C).
- `logic.modal`: sample rules/programs.

### Further reading

- Original write‑up and worked examples: [Modal in a Postcard](https://wiki.xxiivv.com/site/modal).