ExTLA.Spec.Rewriter (ExTLA v0.6.0)

Copy Markdown View Source

Resolves the three name classes of 02-dsl-semantics.md §1 inside a spec block.

Inside a spec block a bare identifier is one of exactly three things, and the class is determined syntactically, never by inference:

SyntaxClassRewrites to
^nameConstantMap.fetch!(constants, :name)
nameVariableMap.fetch!(state, :name)
let name = …Localleft alone; ordinary Elixir

Why locals are over-approximated

A bare name that is neither a declared variable nor a constant may still be a perfectly good local: a let pattern, a fn argument, a comprehension generator, a case clause head. bound_names/1 collects every name bound anywhere in the block, ignoring scope, and a read of a name in that set is left alone.

Over-approximating is the deliberate direction to be wrong in. Missing a binding would turn working Elixir into a spurious "undeclared variable" error; including one too many only means a genuine typo is reported by Elixir's own compiler ("undefined variable") instead of by this one. The first is a regression, the second is a slightly worse message.

Summary

Types

t()

Functions

bound_names(ast)

Every name bound anywhere in the AST, ignoring scope. See the module note on why this over-approximates.

pattern_names(pattern)

The variable names bound by a pattern. A pinned name is a value, not a binding, so ^x contributes nothing.

reject_action_property()

The rejection builder for action_property: §4 requires old./new..

reject_init()

The rejection builder for init: there is no earlier state to read.

reject_param(state_arg)

The rejection builder for a params: generator, which receives the pre-state as its own argument.

rewrite(ast, ctx)

Rewrite an expression, resolving ^constants and bare variables.

Types

t()

@type t() :: %ExTLA.Spec.Rewriter{
  bound: term(),
  constants: term(),
  constants_ast: term(),
  declaration: term(),
  line: term(),
  module: term(),
  params: term(),
  read: term(),
  variables: term()
}

Functions

bound_names(ast)

Every name bound anywhere in the AST, ignoring scope. See the module note on why this over-approximates.

pattern_names(pattern)

The variable names bound by a pattern. A pinned name is a value, not a binding, so ^x contributes nothing.

reject_action_property()

The rejection builder for action_property: §4 requires old./new..

reject_init()

The rejection builder for init: there is no earlier state to read.

reject_param(state_arg)

The rejection builder for a params: generator, which receives the pre-state as its own argument.

rewrite(ast, ctx)

Rewrite an expression, resolving ^constants and bare variables.