Experimental/internal API for 0.2; subject to change before 0.3. Typed registry helpers for generated equation and matcher metadata.
Summary
Functions
Builds an in-memory equation registry snapshot from the environment.
Returns equation definitions known to the registry.
Returns generated ordinary equation names for a source definition.
Returns generated ordinary equation names for a source definition in an environment.
Returns generated ordinary equation identities for a source definition.
Returns generated ordinary equation identities for a source definition in an environment.
Returns generated matcher equation names for a matcher declaration.
Returns generated matcher equation identities for a matcher declaration.
Returns matcher declarations known to the registry.
Returns matcher declarations generated for a source definition.
Returns whether a generated theorem can be realized from registry metadata.
Realizes any generated ordinary, unfold, or matcher equation theorem without installing it.
Realizes every theorem known to the generated equation registry.
Returns the source definition or matcher for a generated theorem name.
Returns compact registry counts for diagnostics and validation output.
Returns all generated theorem names known to the registry.
Returns all generated theorem identities known to the registry.
Returns the unfold theorem identity for a source definition.
Returns the unfold theorem name for a source definition.
Validates registry coherence and theorem realization.
Functions
@spec build(Theoria.Env.t()) :: Theoria.Equation.Extension.Registry.t()
Builds an in-memory equation registry snapshot from the environment.
@spec definitions(Theoria.Env.t()) :: [Theoria.Equation.Info.t()]
Returns equation definitions known to the registry.
@spec equation_identities(Theoria.Equation.Info.t()) :: [atom()]
Returns generated ordinary equation names for a source definition.
@spec equation_identities(Theoria.Env.t(), atom()) :: {:ok, [atom()]} | {:error, term()}
Returns generated ordinary equation names for a source definition in an environment.
@spec equation_ids(Theoria.Equation.Info.t()) :: [Theoria.Equation.Identity.t()]
Returns generated ordinary equation identities for a source definition.
@spec equation_ids(Theoria.Env.t(), atom()) :: {:ok, [Theoria.Equation.Identity.t()]} | {:error, term()}
Returns generated ordinary equation identities for a source definition in an environment.
@spec matcher_equation_identities(Theoria.Env.t(), Theoria.Env.Matcher.t()) :: [ atom() ]
Returns generated matcher equation names for a matcher declaration.
@spec matcher_equation_ids(Theoria.Env.t(), Theoria.Env.Matcher.t()) :: [ Theoria.Equation.Identity.t() ]
Returns generated matcher equation identities for a matcher declaration.
@spec matchers(Theoria.Env.t()) :: [Theoria.Env.Matcher.t()]
Returns matcher declarations known to the registry.
@spec matchers_for(Theoria.Env.t(), atom()) :: [Theoria.Env.Matcher.t()]
Returns matcher declarations generated for a source definition.
@spec realizable?(Theoria.Env.t(), term()) :: boolean()
Returns whether a generated theorem can be realized from registry metadata.
@spec realize(Theoria.Env.t(), term()) :: {:ok, Theoria.Theorem.t()} | {:error, term()}
Realizes any generated ordinary, unfold, or matcher equation theorem without installing it.
@spec realize_all(Theoria.Env.t()) :: {:ok, [Theoria.Theorem.t()]} | {:error, term()}
Realizes every theorem known to the generated equation registry.
@spec source_for(Theoria.Env.t() | Theoria.Equation.Extension.Registry.t(), term()) :: {:ok, atom()} | :error
Returns the source definition or matcher for a generated theorem name.
@spec summary(Theoria.Env.t() | Theoria.Equation.Extension.Registry.t()) :: map()
Returns compact registry counts for diagnostics and validation output.
@spec theorem_identities(Theoria.Env.t() | Theoria.Equation.Extension.Registry.t()) :: [atom()]
Returns all generated theorem names known to the registry.
@spec theorem_ids(Theoria.Env.t() | Theoria.Equation.Extension.Registry.t()) :: [ Theoria.Equation.Identity.t() ]
Returns all generated theorem identities known to the registry.
@spec unfold_id(Theoria.Env.t(), atom()) :: {:ok, Theoria.Equation.Identity.t()} | {:error, term()}
Returns the unfold theorem identity for a source definition.
@spec unfold_identity(Theoria.Env.t(), atom()) :: {:ok, atom()} | {:error, term()}
Returns the unfold theorem name for a source definition.
@spec validate(Theoria.Env.t()) :: :ok | {:error, term()}
Validates registry coherence and theorem realization.