1 files changed, 112 insertions, 0 deletions
diff --git a/modal/README.md b/modal/README.md
new file mode 100644
index 0000000..954a904
--- /dev/null
+++ b/modal/README.md
@@ -0,0 +1,112 @@
+## 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).
+
+