muro

# Muro

**A spec never becomes evidence. Evidence never becomes a run.**

An explicit affine dependent type theory. Elixir parses, checks, and emits `.muro`. Only run terms become running code. Users do not need Agda.

The language book is [`manual/`](manual/index.md). That is what [muro-lang.dev](https://muro-lang.dev) will render. It is not ExDoc. Elixir API docs, when added, stay on `@moduledoc` / `mix docs`. Agda in `agda/Muro/` is a third layer: the rules of the calculus, not a certificate that a `.muro` file is correct.

## Install

[muro on Hex](https://hex.pm/packages/muro) is published by the [murolang](https://hex.pm/users/murolang) organization. Releases are listed in [CHANGELOG.md](CHANGELOG.md).

```elixir
def deps do
  [
    {:muro, "~> 0.2"}
  ]
end
```

A clone is for changing the kernel. A `.muro` file is checked with `mix muro.check` from a project that depends on the package.

---

## One-shot (humans and agents)

Two jobs. Do not mix them.

| You want to… | Do this |
| --- | --- |
| Add a Muro program | Write a `.muro` file against [`manual/grammar.md`](manual/grammar.md). Check with `mix muro.check path.muro`. Do not change Agda or the Elixir kernel. |
| Change the type theory | Follow [`manual/extending.md`](manual/extending.md). Agda first, then the matching Elixir clause. Users still only run Mix. |

Agents: read [`manual/for-agents.md`](manual/for-agents.md). Copy syntax from `examples/`, not from memory.

Skeleton:

```
-- comments start with --
def plus : run Π (n : Nat) → Π (m : Nat) → Nat :=
  λ (n : Nat) → λ (m : Nat) →
    match n motive (λ _ → Nat)
      | 0 => m
      | suc np => suc(plus np m)
```

```
mix muro.check examples/your_file.muro
```

A definition is in the book the moment `Parser.parse/1` returns it. The checker sees the whole book (forward references are allowed). Emit keeps only `run`.

---

## Manual

| Page | For |
| --- | --- |
| [Start](manual/start.md) | Install, first file, emit |
| [The wall](manual/wall.md) | spec / evidence / run |
| [Terms](manual/language.md) | Π, λ, match, quantities |
| [Grammar](manual/grammar.md) | What the parser implements |
| [Examples](manual/examples.md) | Every file in `examples/` |
| [For agents](manual/for-agents.md) | Operational contract |
| [Limits](manual/limits.md) | What the language does not do |

Index: [`manual/index.md`](manual/index.md). Machine-readable list: [`manual/manifest.yml`](manual/manifest.yml).

---

## Build

```
mise install
mix deps.get
mix test
mix muro.check
mix muro.check examples/half_ok.muro
```

Agda 2.8+ and standard library 2.3 (optional unless you change the kernel):

```
git clone --depth 1 --branch v2.3 https://github.com/agda/agda-stdlib.git vendor/agda-stdlib
make agda
```

`Muro.Lexer.tokenize/1` is the highlighter. It walks a fragment with the parser's lexical rules and returns `{kind, start, stop}` byte spans. A snippet that `Parser.parse/1` rejects still yields spans, and joining the slices gives the source back. `Muro.MakeupLexer` maps those spans onto Makeup tags (language `"muro"`, extension `.muro`) and is registered when the application starts. HTML and colors stay with the caller.

`Muro.Check.check_sig/1` returns `:ok` on the book. CI runs the Elixir job and `make agda` on every push and pull request. `make agda` checks the theorem modules (`Muro.Judgement`, `Muro.Wall`, `Muro.Consistency`) under `--safe`; conversion in ⊢ is a relation, `Muro.Consistency` proves that no closed normal evidence term has type Empty, `Empty-evid` itself is not proved, and data / ν / Tensor are still outside ⊢. `Type` is one impredicative sort; kinds (`Π (x : A) → Type`) are well-formed but are not terms of type `Type`, in Agda and in Elixir alike.

## Names

| | |
| --- | --- |
| Language | Muro |
| Theory | MuroTT |
| Files | `.muro` |
| Elixir | `Muro`, `Muro.Check`, `Muro.Emit`, `Muro.Parser` |
| Agda | `Muro.*` |