ExMaude.Result.Reduction (ExMaude v0.2.0)

View Source

Result of a Maude reduce operation.

A reduction result contains the normalized term along with performance metrics like the number of rewrites applied and execution time.

Structure

  • :term - The resulting ExMaude.Term after reduction
  • :rewrites - Number of rewrite steps applied
  • :time_ms - Time taken in milliseconds

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

Key patterns parsed:

PatternDescription
rewrites: NNumber of rewrite steps applied
in NmsExecution time in milliseconds
result Sort: TermThe resulting term with its sort

Examples

{:ok, output} = ExMaude.execute("reduce in NAT : 1 + 2 + 3 .")
{: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)

See Also

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.