ExMaude.Parser (ExMaude v0.2.0)

Parser for Maude command output.

This module provides functions to parse various Maude command outputs into structured Elixir data. It handles the text-based responses from Maude and converts them into maps, lists, and tuples that are easier to work with in Elixir.

Supported Output Formats

The parser handles several types of Maude output:

Reduction/Rewrite results - result Type: value format
Search solutions - Multiple solutions with substitutions
Error messages - Warnings and errors from Maude
Module listings - Lists of loaded modules
Term parsing - Basic AST representation of Maude terms

Usage

This module is primarily used internally by ExMaude.Maude and ExMaude.Server, but can be used directly for custom output parsing:

# Parse a reduce result
{:ok, "42", "Nat"} = ExMaude.Parser.parse_result("result Nat: 42")

# Parse search output
solutions = ExMaude.Parser.parse_search_results(maude_output)

# Check for errors in output
:ok = ExMaude.Parser.parse_errors(clean_output)
{:error, issues} = ExMaude.Parser.parse_errors("Error: bad input")

Limitations

The term parser (parse_term/1) provides basic parsing but does not handle all Maude syntax. Complex nested terms with parentheses in arguments may not parse correctly. For full parsing, consider using NimbleParsec-based parsers or Maude's own parse command.

Summary

Functions

parse_backend_response(output)

Parses a backend's raw command output into the public response shape.

parse_errors(output)

Parses error messages from Maude output.

parse_module_list(output)

Parses module list output.

parse_result(output)

Parses a reduce/rewrite result to extract the value.

parse_search_results(output)

Parses search command output into a list of solutions.

parse_term(input)

Parses a Maude term into an Elixir term structure.

Functions

parse_backend_response(output)

@spec parse_backend_response(String.t()) ::
  {:ok, String.t()} | {:error, ExMaude.Error.t()}

Parses a backend's raw command output into the public response shape.

This is the single source of truth for how Maude's text output is turned into {:ok, value} / {:error, %ExMaude.Error{}} — every backend should funnel its stdout through this helper to keep the public contract stable.

The input is the text emitted between two Maude> prompts, with the trailing prompt already stripped.

Examples

iex> ExMaude.Parser.parse_backend_response("result Nat: 6")
{:ok, "6"}

iex> ExMaude.Parser.parse_backend_response("")
{:ok, ""}

iex> {:error, err} = ExMaude.Parser.parse_backend_response("Warning: module FOO not found")
...> err.type
:module_not_found

parse_errors(output)

@spec parse_errors(String.t()) ::
  :ok | {:error, [{:warning | :error, String.t()}, ...]}

Parses error messages from Maude output.

Examples

iex> ExMaude.Parser.parse_errors("Warning: blah\nError: something bad")
{:error, [warning: "blah", error: "something bad"]}

parse_module_list(output)

@spec parse_module_list(String.t()) :: [map()]

Parses module list output.

Examples

iex> output = "fmod BOOL\nfmod NAT\nmod MY-MOD\n"
...> ExMaude.Parser.parse_module_list(output)
[
  %{type: :fmod, name: "BOOL"},
  %{type: :fmod, name: "NAT"},
  %{type: :mod, name: "MY-MOD"}
]

parse_result(output)

@spec parse_result(String.t()) :: {:ok, String.t(), String.t()} | {:error, :no_result}

Parses a reduce/rewrite result to extract the value.

Examples

iex> ExMaude.Parser.parse_result("result Nat: 6")
{:ok, "6", "Nat"}

iex> ExMaude.Parser.parse_result("result Bool: true")
{:ok, "true", "Bool"}

parse_search_results(output)

@spec parse_search_results(String.t()) :: [map()]

Parses search command output into a list of solutions.

Examples

iex> output =
...>   "Solution 1 (state 5)\nS:State --> active\n\nSolution 2 (state 8)\nS:State --> inactive\n"
...>
...> ExMaude.Parser.parse_search_results(output)
[
  %{solution: 1, state_num: 5, substitution: %{"S:State" => "active"}},
  %{solution: 2, state_num: 8, substitution: %{"S:State" => "inactive"}}
]

parse_term(input)

@spec parse_term(String.t()) :: {:const, String.t()} | {:app, String.t(), list()}

Parses a Maude term into an Elixir term structure.

This provides a basic AST representation of Maude terms.

Examples

iex> ExMaude.Parser.parse_term("s(s(0))")
{:app, "s", [{:app, "s", [{:const, "0"}]}]}

iex> ExMaude.Parser.parse_term("true and false")
{:app, "and", [{:const, "true"}, {:const, "false"}]}