Metastatic.Adapters.Agda (Metastatic v0.33.0)

View Source

Agda language adapter for Metastatic.

This adapter provides bidirectional transformation between Agda source code and MetaAST (M2) representation using a Haskell-based parser bridge.

Architecture

  • parse/1 - Agda source → Agda AST (via Agda compiler parser bridge)
  • to_meta/1 - Agda AST → MetaAST (M2 abstraction)
  • from_meta/2 - MetaAST → Agda AST (M2 reification)
  • unparse/1 - Agda AST → Agda source

Examples

iex> {:ok, ast} = Metastatic.Adapters.Agda.parse("1 + 2")
iex> {:ok, meta_ast, _metadata} = Metastatic.Adapters.Agda.ToMeta.transform(ast)
iex> meta_ast
{:binary_op, [category: :arithmetic, operator: :+],
 [{:literal, [subtype: :integer], 1}, {:literal, [subtype: :integer], 2}]}