TLX.Importer.ExprParser (TLX v0.5.2)

Copy Markdown

Parses TLA+ expressions into Elixir AST matching the form produced by TLX.Expr.e/1 at DSL compile time.

The resulting AST can be round-tripped through Macro.to_string/1 to produce valid Elixir source for re-emission via TLX.Importer.Codegen.

Currently parsed (sprints 54–55):

  • Integer and boolean literals, identifiers, parenthesization
  • Arithmetic: +, -, * (binary)
  • Comparison: =, #, /=, <, <=, >, >=, \in, \subseteq
  • Logical: /\, \/, ~
  • Implication: =>, <=>
  • IF ... THEN ... ELSE
  • Sets: literal {a, b, c}, comprehensions {x \in S : P} and {expr : x \in S}, binary set ops (\union, \intersect, \), unary SUBSET, UNION
  • Range: a..b
  • Quantifiers: \E x \in S : P, \A x \in S : P, CHOOSE x \in S : P
  • Functions: f[x] (application), DOMAIN f, [f EXCEPT ![x]=v] (single- and multi-key), [a \|-> 1, b \|-> 2] (records)
  • Built-in calls: Cardinality(S)

Sprints 56–58 cover extended arithmetic, tuples, Cartesian, function constructor/set, sequences, LAMBDA, CASE, and temporal operators.

Per ADR-0013, callers fall back to raw-string capture on parse failure.

Summary

Functions

parse(source)

Parse a TLA+ expression string into Elixir AST.

parse_expr(binary, opts \\ [])

Parses the given binary as parse_expr.

Functions

parse(source)

Parse a TLA+ expression string into Elixir AST.

Returns {:ok, ast} on success or {:error, reason} on failure.

parse_expr(binary, opts \\ [])

@spec parse_expr(binary(), keyword()) ::
  {:ok, [term()], rest, context, line, byte_offset}
  | {:error, reason, rest, context, line, byte_offset}
when line: {pos_integer(), byte_offset},
     byte_offset: non_neg_integer(),
     rest: binary(),
     reason: String.t(),
     context: map()

Parses the given binary as parse_expr.

Returns {:ok, [token], rest, context, position, byte_offset} or {:error, reason, rest, context, line, byte_offset} where position describes the location of the parse_expr (start position) as {line, offset_to_start_of_line}.

To column where the error occurred can be inferred from byte_offset - offset_to_start_of_line.

Options

  • :byte_offset - the byte offset for the whole binary, defaults to 0
  • :line - the line and the byte offset into that line, defaults to {1, byte_offset}
  • :context - the initial context value. It will be converted to a map