ExMaude.Result.Reduction (ExMaude v0.4.0)

View Source

Result of a Maude reduce operation.

This struct is useful when an application has raw, verbose Maude output and wants the normalized term together with rewrite and timing statistics. ExMaude.reduce/3 itself returns only the normalized term string.

Maude Output Format

The parser expects Maude's standard reduction output format:

reduce in NAT : 1 + 2 + 3 .
rewrites: 3 in 0ms cpu (0ms real) (~ rewrites/second)
result Nat: 6

Examples

output = "rewrites: 3 in 1ms cpu (1ms real)\nresult Nat: 6"
{:ok, result} = ExMaude.Result.Reduction.parse(output)
result.term.value
# => "6"
result.rewrites
# => 3

# Create manually
term = ExMaude.Term.new("6", "Nat")
result = ExMaude.Result.Reduction.new(term, rewrites: 3, time_ms: 1)

Summary

Types

t()

Functions

new(term, opts \\ [])

Creates a new Reduction result.

parse(output, module \\ nil)

Parses Maude reduction output into a Reduction result.

Types

t()

@type t() :: %ExMaude.Result.Reduction{
  rewrites: non_neg_integer() | nil,
  term: ExMaude.Term.t(),
  time_ms: non_neg_integer() | nil
}

Functions

new(term, opts \\ [])

@spec new(
  ExMaude.Term.t(),
  keyword()
) :: t()

Creates a new Reduction result.

Examples

term = ExMaude.Term.new("6", "Nat")
result = ExMaude.Result.Reduction.new(term, rewrites: 3, time_ms: 1)

parse(output, module \\ nil)

@spec parse(String.t(), String.t() | nil) :: {:ok, t()} | {:error, term()}

Parses Maude reduction output into a Reduction result.

Extracts the term, rewrite count, and timing information from Maude's verbose output.