Sheaf.Theory

A theory: its sorts, its operations, and its equations. This is the object the category of theories (the sheaf site) will range over.

A sort: a named carrier the theory ranges over (e.g. Signal, Mesh, Machine). Just a name at this layer.

An operation: a name, the sorts of its arguments (in order), and the sort of its result. This is a sorted arity — the whole of what the signature says about an op. A nullary op (empty argument list) is a constant of its result sort.

An equation: two terms asserted equal (they must be of the same sort in a well-formed theory; that is checked, not assumed here), under premises. With no premises it holds everywhere; with premises it is a conditional equation (a Horn clause of equational logic), holding wherever every premise does. A side condition that is a predicate is stated as a premise p(…) = true over a declared boolean sort, which keeps premises positive, as Horn clauses require.

A premise of a conditional equation: two terms that must be equal for the equation to hold.

A term over the signature: a variable (its name and sort) or an operation applied to sub-terms. Terms are what equations relate and what a later fold interprets; here they exist so equations can be stated and so the printer/parser have something to round-trip.

An equation that holds everywhere.

An equation that holds wherever its premises do.

Build a theory, canonicalising the sort and op lists (deduplicated and ordered) so two theories that declare the same signature in a different order are equal and print identically. Equations keep their given order (order can be semantically relevant to a later rewrite system, so we do not reorder them — only sorts and ops are sets).

The empty theory: no sorts, no ops, no equations. The initial object of the category; a colimit's identity element.

The declared sort names.

The declared operation names.

Is this sort declared in the theory?

Check well-formedness: every op's argument and result sorts are declared, op names are unique, every term in an equation names a declared op with the right arity, every variable is used at a single sort across a clause, the two sides of each equation and of each of its premises have the same sort, and no op is named like a keyword. Returns the list of problems (empty = well formed).

Ways a theory can fail well-formedness (verification level #1 in the master plan: everything refers only to declared sorts, and equations are sort-consistent). Total and decidable.

Print a theory to its canonical textual form. The form is line oriented and stable (sorts then ops then equations, each already in canonical order from theory), so parseTheory . printTheory is the identity on well-constructed theories — the round-trip law that is this phase's exit check. This is a human- and diff-friendly serialisation; it is not the wire protocol (that is vortex-wire).

Parse the canonical form back to a Theory. Deliberately small and forgiving of surrounding whitespace; it is the inverse of printTheory on that printer's own output, which is all the exit check requires. Returns Left with a message on malformed input.