ExMaude.Backend behaviour (ExMaude v0.2.0)

View Source

Behaviour for ExMaude communication backends.

All backends must implement this behaviour to be used interchangeably by the ExMaude API. This enables swapping between different communication strategies:

  • :port - Erlang Port with PTY wrapper (default, safe)
  • :cnode - C-Node with binary protocol (production)
  • :nif - Native Implemented Function via Rustler (lowest latency)

Configuration

config :ex_maude,
  backend: :port  # :port | :cnode | :nif

Example

# Get the configured backend module
backend = ExMaude.Backend.impl()

# Start a worker
{:ok, server} = backend.start_link([])

# Execute a command
{:ok, result} = backend.execute(server, "reduce in NAT : 1 + 2 .")

Summary

Types

Backend module types

Backend configuration atoms

Callbacks

Checks if the backend worker is alive and ready.

Executes a Maude command and returns the result.

Loads a Maude file into the session.

Starts a backend worker process.

Stops the backend worker.

Functions

Checks if a backend is available on this system.

Returns a list of all available backends on this system.

Returns the path to the C-Node bridge binary.

Returns the backend implementation module based on configuration.

Types

backend_module()

@type backend_module() ::
  ExMaude.Backend.Port | ExMaude.Backend.CNode | ExMaude.Backend.NIF

Backend module types

backend_type()

@type backend_type() :: :port | :cnode | :nif

Backend configuration atoms

command()

@type command() :: String.t()

result()

@type result() :: {:ok, String.t()} | {:error, term()}

Callbacks

alive?(server)

@callback alive?(server :: GenServer.server()) :: boolean()

Checks if the backend worker is alive and ready.

execute(server, command, keyword)

@callback execute(server :: GenServer.server(), command(), keyword()) :: result()

Executes a Maude command and returns the result.

Options

  • :timeout - Maximum time to wait in ms

load_file(server, path)

@callback load_file(server :: GenServer.server(), path :: Path.t()) ::
  :ok | {:error, term()}

Loads a Maude file into the session.

start_link(opts)

@callback start_link(opts :: keyword()) :: GenServer.on_start()

Starts a backend worker process.

Options

  • :maude_path - Path to Maude executable (optional)
  • :timeout - Default command timeout in ms
  • :preload_modules - List of Maude files to load on startup

stop(server)

@callback stop(server :: GenServer.server()) :: :ok

Stops the backend worker.

Functions

available?(atom)

@spec available?(backend_type()) :: boolean()

Checks if a backend is available on this system.

The Port backend is always available. C-Node requires the maude_bridge binary to be compiled. NIF reports available when the Rustler-precompiled native function table has been loaded (probed via a cheap nif_loaded/0 NIF that raises :nif_not_loaded while the stub is in place).

Examples

ExMaude.Backend.available?(:port)
#=> true

ExMaude.Backend.available?(:cnode)
#=> true if priv/maude_bridge has been compiled

ExMaude.Backend.available?(:nif)
#=> true if the precompiled NIF binary loaded for this platform

available_backends()

@spec available_backends() :: [atom()]

Returns a list of all available backends on this system.

cnode_binary()

@spec cnode_binary() :: Path.t()

Returns the path to the C-Node bridge binary.

impl()

@spec impl() :: backend_module()

Returns the backend implementation module based on configuration.

Reads :backend from the :ex_maude application env (defaults to :port) and maps it to the implementation module.

Examples

ExMaude.Backend.impl()
#=> ExMaude.Backend.Port