Whether a code block is alive or dead.
- deadSyntactically : CodeLiveness
We inferred the code is semantically dead and don't need to elaborate it at all.
- deadSemantically : CodeLiveness
We inferred the code is semantically dead, but we need to elaborate it to produce a program.
- alive : CodeLiveness
The code is alive. (Or it is dead, but we failed to prove it so.)
Instances For
The least upper bound of two code livenesses.
Instances For
- monadInfo : MonadInfo
Inferred and cached information about the monad.
The mutable variables in declaration order.
- mutVarDefs : Std.HashMap Name FVarId
Maps mutable variable names to their initial FVarIds.
- doBlockResultType : Expr
The expected type of the current
doblock. This can be different fromearlyReturnTypeinforloopdoblocks, for example. - contInfo : ContInfoRef
Information about
return,breakandcontinuecontinuations. - deadCode : CodeLiveness
Whether the current
doelement is dead code.elabDoElemwill emit a warning if not.alive.
Instances For
Whether the continuation of a do element is duplicable and if so whether it is just pure r for
the result variable r. Saying nonDuplicable is always safe; duplicable allows for more
optimizations.
- nonDuplicable : DoElemContKind
- duplicable : DoElemContKind
Instances For
Elaboration of a do block do $e; $rest, results in a call
elabTerm `(do $e; $rest) = elabElem e dec, where elabElem e · is the elaborator for do
element e, and dec is the DoElemCont describing the elaboration of the rest of the block
rest.
If the semantics of e resumes its continuation rest, its elaborator must bind its result to
resultName, ensure that it has type resultType and then elaborate rest using dec.
Clearly, for term elements e : m α, the result has type α.
More subtly, for binding elements let x := e or let x ← e, the result has type PUnit and is
unrelated to the type of the bound variable x.
Examples:
returndrops the continuation;return x; pure ()elaborates topure x.let x ← e; rest xelaborates toe >>= fun x => rest x.let x := 3; let y ← (let x ← e); rest xelaborates tolet x := 3; e >>= fun x_1 => let y := (); rest x, which is immediately zeta-reduced tolet x := 3; e >>= fun x_1 => rest x.one; twoelaborates toone >>= fun (_ : PUnit) => two; it is an error ifonedoes not have typePUnit.
- resultName : Name
The name of the monadic result variable.
- resultType : Expr
The type of the monadic result.
The continuation to elaborate the
restof the block. It assumes that the result of thedoblock is bound toresultNamewith the correct type (that is,resultType, potentially refined by a dependentmatch).- kind : DoElemContKind
Whether we are OK with generating the code of the continuation multiple times, e.g. in different branches of a
matchorif.
Instances For
The type of elaborators for do block elements.
It is elabTerm `(do $e; $rest) = elabElem e dec, where elabElem e · is the elaborator for do
element e, and dec is the DoElemCont describing the elaboration of the rest of the block
rest.
Instances For
- resultType : Expr
The elaborator constructing a jump site to the return continuation, given some return value. The type of this return value determines the type of the jump expression; this could very well be different than the
resultTypein case an interveningmatchas refinedresultType. Sokmust not hardcode the typeresultTypeinto its definition; rather it should infer the type of the return value argument.
Instances For
Information about a success, return, break or continue continuation that will be filled in
after the code using it has been elaborated.
- returnCont : ReturnCont
Instances For
The expression pure (α:=α) e.
Instances For
Create a DoElemCont returning the result using pure.
Instances For
Create a ReturnCont returning the result using pure.
Instances For
Throw an error if the given name is not a declared mut variable.
Instances For
Throw an error if a declaration of the given name would shadow a mut variable.
Instances For
Create a fresh α that would fit in m α.
Instances For
Like controlAt TermElabM, but it maintains the state using the DoElabM's ref cell instead of returning it
in the TermElabM result. This makes it possible to run multiple DoElabM computations in a row.
Instances For
Instances For
The subset of mutVars that were reassigned in any of the childCtxs relative to the given
rootCtx.
Instances For
Restores the local context to oldCtx and adds the new reaching definitions of the mut vars and
result. Then resume the continuation k with the mutVars restored to the given oldMutVars.
This function is useful to de-nest
let mut x := 0
let y := 3
let z ← do
let mut y ← e
x := y + 1
pure y
let y := y + 3
pure (x + y + z)
into
let mut x := 0
let y := 3
let mut y† ← e
x := y† + 1
let z ← pure y†
let y := y + 3
pure (x + y + z)
Note that the continuation of the let z ← ... bind, roughly
k := .cont `z _ `(let y := y + 3; pure (x + y + z)),
needs to elaborated in a local context that contains the reassignment of x, but not the shadowing
mut var definition of y.
Instances For
Return $e >>= fun ($dec.resultName : $dec.resultType) => $(← dec.k), cancelling
the bind if $(← dec.k) is pure $dec.resultName or e is some pure computation.
Instances For
Return let $k.resultName : PUnit := PUnit.unit; $(← k.k), ensuring that the result type of k.k
is PUnit and then immediately zeta-reduce the let.
Instances For
Elaborate the DoElemCont with the deadCode flag set to deadSyntactically to emit warnings.
Instances For
Instances For
Instances For
Instances For
Call caller with a duplicable proxy of dec.
When the proxy is elaborated more than once, a join point is introduced so that dec is only
elaborated once to fill in the RHS of this join point.
This is useful for control-flow constructs like if and match, where multiple tail-called
branches share the continuation.
Instances For
Prepare the context for elaborating the body of a loop.
This includes setting the return continuation, break continuation, continue continuation, as
well as the changed result type of the do block in the loop body.
Instances For
Instances For
Instances For
Registers a do element elaborator for the given syntax node kind.
A do element elaborator should have type DoElab (which is
Lean.Syntax → DoElemCont → DoElabM Expr), i.e. should take syntax of the given syntax node kind
and a DoElemCont as parameters and produce an expression.
When elaborating a do block do e; rest, the elaborator for e is invoked with the syntax of e
and the DoElemCont representing rest.
The elab_rules and elab commands should usually be preferred over using this attribute
directly.