Equations
- Lean.Elab.Term.elabLiftMethod stx x✝ = Lean.throwErrorAt stx (Lean.toMessageData "invalid use of `(<- ...)`, must be nested inside a 'do' expression")
Instances For
Equations
Instances For
A doMatch
alternative. vars
is the array of variables declared by patterns
.
- ref : Lean.Syntax
- vars : Array Lean.Elab.Term.Do.Var
- patterns : Lean.Syntax
- rhs : σ
Instances For
Equations
- Lean.Elab.Term.Do.instInhabitedAlt = { default := { ref := default, vars := default, patterns := default, rhs := default } }
A doMatchExpr
alternative.
- ref : Lean.Syntax
- var? : Option Lean.Elab.Term.Do.Var
- funName : Lean.Syntax
- pvars : Array Lean.Syntax
- rhs : σ
Instances For
Equations
- Lean.Elab.Term.Do.instInhabitedAltExpr = { default := { ref := default, var? := default, funName := default, pvars := default, rhs := default } }
Equations
- One or more equations did not get rendered due to their size.
Instances For
Auxiliary datastructure for representing a do
code block, and compiling "reassignments" (e.g., x := x + 1
).
We convert Code
into a Syntax
term representing the:
do
-block, or- the visitor argument for the
forIn
combinator.
We say the following constructors are terminals:
break
: for interrupting afor x in s
continue
: for interrupting the current iteration of afor x in s
return e
: for returninge
as the result for the wholedo
computation blockaction a
: for executing actiona
as a terminalite
: if-then-elsematch
: pattern matchingjmp
a goto to a join-point
We say the terminals break
, continue
, action
, and return
are "exit points"
Note that, return e
is not equivalent to action (pure e)
. Here is an example:
def f (x : Nat) : IO Unit := do
if x == 0 then
return ()
IO.println "hello"
Executing #eval f 0
will not print "hello". Now, consider
def g (x : Nat) : IO Unit := do
if x == 0 then
pure ()
IO.println "hello"
The if
statement is essentially a noop, and "hello" is printed when we execute g 0
.
decl
represents all declaration-likedoElem
s (e.g.,let
,have
,let rec
). The fieldstx
is the actualdoElem
,vars
is the array of variables declared by it, andcont
is the next instruction in thedo
code block.vars
is an array since we have declarations such aslet (a, b) := s
.joinpoint
is a join point declaration: an auxiliarylet
-declaration used to represent the control-flow.seq a k
executes actiona
, ignores its result, and then executesk
. We also store the do-elementsdbg_trace
andassert!
as actions in aseq
.
A code block C
is well-formed if
- For every
jmp ref j as
inC
, there is ajoinpoint j ps b k
andjmp ref j as
is ink
, andps.size == as.size
- decl (xs : Array Lean.Elab.Term.Do.Var) (doElem : Lean.Syntax) (k : Lean.Elab.Term.Do.Code) : Lean.Elab.Term.Do.Code
- reassign (xs : Array Lean.Elab.Term.Do.Var) (doElem : Lean.Syntax) (k : Lean.Elab.Term.Do.Code) : Lean.Elab.Term.Do.Code
- joinpoint
(name : Lean.Name)
(params : Array (Lean.Elab.Term.Do.Var × Bool))
(body k : Lean.Elab.Term.Do.Code)
: Lean.Elab.Term.Do.Code
The Boolean value in
params
indicates whether we should use(x : typeof! x)
when generating term Syntax or not - seq (action : Lean.Syntax) (k : Lean.Elab.Term.Do.Code) : Lean.Elab.Term.Do.Code
- action (action : Lean.Syntax) : Lean.Elab.Term.Do.Code
- break (ref : Lean.Syntax) : Lean.Elab.Term.Do.Code
- continue (ref : Lean.Syntax) : Lean.Elab.Term.Do.Code
- return (ref val : Lean.Syntax) : Lean.Elab.Term.Do.Code
- ite
(ref : Lean.Syntax)
(h? : Option Lean.Elab.Term.Do.Var)
(optIdent cond : Lean.Syntax)
(thenBranch elseBranch : Lean.Elab.Term.Do.Code)
: Lean.Elab.Term.Do.Code
Recall that an if-then-else may declare a variable using
optIdent
for the branchesthenBranch
andelseBranch
. We store the variable name atvar?
. - match (ref gen discrs optMotive : Lean.Syntax) (alts : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)) : Lean.Elab.Term.Do.Code
- matchExpr (ref : Lean.Syntax) (meta : Bool) (discr : Lean.Syntax) (alts : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) (elseBranch : Lean.Elab.Term.Do.Code) : Lean.Elab.Term.Do.Code
- jmp (ref : Lean.Syntax) (jpName : Lean.Name) (args : Array Lean.Syntax) : Lean.Elab.Term.Do.Code
Instances For
Equations
- Lean.Elab.Term.Do.instInhabitedCode = { default := Lean.Elab.Term.Do.Code.action default }
Equations
- (Lean.Elab.Term.Do.Code.decl xs doElem k).getRef? = some doElem
- (Lean.Elab.Term.Do.Code.reassign xs doElem k).getRef? = some doElem
- (Lean.Elab.Term.Do.Code.joinpoint name params body k).getRef? = none
- (Lean.Elab.Term.Do.Code.seq a k).getRef? = some a
- (Lean.Elab.Term.Do.Code.action a).getRef? = some a
- (Lean.Elab.Term.Do.Code.break ref).getRef? = some ref
- (Lean.Elab.Term.Do.Code.continue ref).getRef? = some ref
- (Lean.Elab.Term.Do.Code.return ref val).getRef? = some ref
- (Lean.Elab.Term.Do.Code.ite ref h? optIdent cond thenBranch elseBranch).getRef? = some ref
- (Lean.Elab.Term.Do.Code.match ref gen discrs optMotive alts).getRef? = some ref
- (Lean.Elab.Term.Do.Code.matchExpr ref meta discr alts elseBranch).getRef? = some ref
- (Lean.Elab.Term.Do.Code.jmp ref jpName args).getRef? = some ref
Instances For
Instances For
A code block, and the collection of variables updated by it.
- code : Lean.Elab.Term.Do.Code
- uvars : Lean.Elab.Term.Do.VarSet
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Return true if the give code contains an exit point that satisfies p
Equations
Instances For
Equations
Instances For
Equations
- Lean.Elab.Term.Do.hasReturn c = Lean.Elab.Term.Do.hasExitPointPred c fun (x : Lean.Elab.Term.Do.Code) => match x with | Lean.Elab.Term.Do.Code.return ref val => true | x => false
Instances For
Equations
- Lean.Elab.Term.Do.hasTerminalAction c = Lean.Elab.Term.Do.hasExitPointPred c fun (x : Lean.Elab.Term.Do.Code) => match x with | Lean.Elab.Term.Do.Code.action action => true | x => false
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Convert action _ e
instructions in c
into let y ← e; jmp _ jp (xs y)
.
Equations
Instances For
- name : Lean.Name
- params : Array (Lean.Elab.Term.Do.Var × Bool)
- body : Lean.Elab.Term.Do.Code
Instances For
Equations
- Lean.Elab.Term.Do.attachJP jpDecl k = Lean.Elab.Term.Do.Code.joinpoint jpDecl.name jpDecl.params jpDecl.body k
Instances For
Equations
- Lean.Elab.Term.Do.attachJPs jpDecls k = Array.foldr Lean.Elab.Term.Do.attachJP k jpDecls
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Elab.Term.Do.addFreshJP ps body = do let jp ← liftM (Lean.Elab.Term.Do.mkFreshJP ps body) modify fun (jps : Array Lean.Elab.Term.Do.JPDecl) => jps.push jp pure jp.name
Instances For
Equations
- Lean.Elab.Term.Do.insertVars rs xs = Array.foldl (fun (rs : Lean.Elab.Term.Do.VarSet) (x : Lean.Syntax) => Lean.RBMap.insert rs x.getId x) rs xs
Instances For
Equations
- Lean.Elab.Term.Do.eraseVars rs xs = Array.foldl (fun (x1 : Lean.Elab.Term.Do.VarSet) (x2 : Lean.Elab.Term.Do.Var) => Lean.RBMap.erase x1 (Lean.Syntax.getId x2)) rs xs
Instances For
Equations
- Lean.Elab.Term.Do.eraseOptVar rs none = rs
- Lean.Elab.Term.Do.eraseOptVar rs (some x) = Lean.RBMap.insert rs (Lean.Syntax.getId x) x
Instances For
Create a new jointpoint for c
, and jump to it with the variables rs
Equations
- One or more equations did not get rendered due to their size.
Instances For
Create a new joinpoint that takes rs
and val
as arguments. val
must be syntax representing a pure value.
The body of the joinpoint is created using mkJPBody yFresh
, where yFresh
is a fresh variable created by this method.
Equations
- One or more equations did not get rendered due to their size.
Instances For
pullExitPointsAux rs c
auxiliary method for pullExitPoints
, rs
is the set of update variable in the current path.
Auxiliary operation for adding new variables to the collection of updated variables in a CodeBlock.
When a new variable is not already in the collection, but is shadowed by some declaration in c
,
we create auxiliary join points to make sure we preserve the semantics of the code block.
Example: suppose we have the code block print x; let x := 10; return x
. And we want to extend it
with the reassignment x := x + 1
. We first use pullExitPoints
to create
let jp (x!1) := return x!1;
print x;
let x := 10;
jmp jp x
and then we add the reassignment
x := x + 1
let jp (x!1) := return x!1;
print x;
let x := 10;
jmp jp x
Note that we created a fresh variable x!1
to avoid accidental name capture.
As another example, consider
print x;
let x := 10
y := y + 1;
return x;
We transform it into
let jp (y x!1) := return x!1;
print x;
let x := 10
y := y + 1;
jmp jp y x
and then we add the reassignment as in the previous example.
We need to include y
in the jump, because each exit point is implicitly returning the set of
update variables.
We implement the method as follows. Let us
be c.uvars
, then
1- for each return _ y
in c
, we create a join point
let j (us y!1) := return y!1
and replace the return _ y
with jmp us y
2- for each break
, we create a join point
let j (us) := break
and replace the break
with jmp us
.
3- Same as 2 for continue
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Extend the set of updated variables. It assumes ws
is a super set of c.uvars
.
We cannot simply update the field c.uvars
, because c
may have shadowed some variable in ws
.
See discussion at pullExitPoints
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given two code blocks c₁
and c₂
, make sure they have the same set of updated variables.
Let ws
the union of the updated variables in c₁‵ and ‵c₂
.
We use extendUpdatedVars c₁ ws
and extendUpdatedVars c₂ ws
Equations
- One or more equations did not get rendered due to their size.
Instances For
Extending code blocks with variable declarations: let x : t := v
and let x : t ← v
.
We remove x
from the collection of updated variables.
Remark: stx
is the syntax for the declaration (e.g., letDecl
), and xs
are the variables
declared by it. It is an array because we have let-declarations that declare multiple variables.
Example: let (x, y) := t
Equations
- Lean.Elab.Term.Do.mkVarDeclCore xs stx c = { code := Lean.Elab.Term.Do.Code.decl xs stx c.code, uvars := Lean.Elab.Term.Do.eraseVars c.uvars xs }
Instances For
Extending code blocks with reassignments: x : t := v
and x : t ← v
.
Remark: stx
is the syntax for the declaration (e.g., letDecl
), and xs
are the variables
declared by it. It is an array because we have let-declarations that declare multiple variables.
Example: (x, y) ← t
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Elab.Term.Do.mkSeq action c = { code := Lean.Elab.Term.Do.Code.seq action c.code, uvars := c.uvars }
Instances For
Equations
- Lean.Elab.Term.Do.mkTerminalAction action = { code := Lean.Elab.Term.Do.Code.action action, uvars := ∅ }
Instances For
Equations
- Lean.Elab.Term.Do.mkReturn ref val = { code := Lean.Elab.Term.Do.Code.return ref val, uvars := ∅ }
Instances For
Equations
- Lean.Elab.Term.Do.mkBreak ref = { code := Lean.Elab.Term.Do.Code.break ref, uvars := ∅ }
Instances For
Equations
- Lean.Elab.Term.Do.mkContinue ref = { code := Lean.Elab.Term.Do.Code.continue ref, uvars := ∅ }
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Elab.Term.Do.mkPureUnitAction = do let __do_lift ← Lean.Elab.Term.Do.mkPureUnit✝ pure (Lean.Elab.Term.Do.mkTerminalAction __do_lift)
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Return a code block that executes terminal
and then k
with the value produced by terminal
.
This method assumes terminal
is a terminal
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Elab.Term.Do.getLetIdDeclVars letIdDecl = if letIdDecl[0].isIdent = true then #[letIdDecl[0]] else #[]
Instances For
Equations
- Lean.Elab.Term.Do.getPatternVarsEx pattern = (Lean.Elab.Term.getPatternVars pattern <|> Lean.Elab.Term.Quotation.getPatternVars pattern)
Instances For
Equations
- Lean.Elab.Term.Do.getPatternsVarsEx patterns = (Lean.Elab.Term.getPatternsVars patterns <|> Lean.Elab.Term.Quotation.getPatternsVars patterns)
Instances For
Equations
- Lean.Elab.Term.Do.getLetPatDeclVars letPatDecl = Lean.Elab.Term.Do.getPatternVarsEx letPatDecl[0]
Instances For
Equations
- Lean.Elab.Term.Do.getLetEqnsDeclVars letEqnsDecl = if letEqnsDecl[0].isIdent = true then #[letEqnsDecl[0]] else #[]
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Elab.Term.Do.getDoLetVars doLet = Lean.Elab.Term.Do.getLetDeclVars doLet[2]
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Elab.Term.Do.getDoIdDeclVar doIdDecl = doIdDecl[0]
Instances For
Equations
- Lean.Elab.Term.Do.getDoPatDeclVars doPatDecl = Lean.Elab.Term.Do.getPatternVarsEx doPatDecl[0]
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
- ref : Lean.Syntax
- optIdent : Lean.Syntax
- cond : Lean.Syntax
- thenBranch : Lean.Syntax
- elseBranch : Lean.Syntax
Instances For
The procedure ToTerm.run
converts a CodeBlock
into a Syntax
term.
We use this method to convert
1- The CodeBlock
for a root do ...
term into a Syntax
term. This kind of
CodeBlock
never contains break
nor continue
. Moreover, the collection
of updated variables is not packed into the result.
Thus, we have two kinds of exit points
- Code.action e
which is converted into e
- Code.return _ e
which is converted into pure e
We use Kind.regular
for this case.
2- The CodeBlock
for b
at for x in xs do b
. In this case, we need to generate
a Syntax
term representing a function for the xs.forIn
combinator.
a) If b
contain a Code.return _ a
exit point. The generated Syntax
term
has type m (ForInStep (Option α × σ))
, where a : α
, and the σ
is the type
of the tuple of variables reassigned by b
.
We use Kind.forInWithReturn
for this case
b) If b
does not contain a Code.return _ a
exit point. Then, the generated
Syntax
term has type m (ForInStep σ)
.
We use Kind.forIn
for this case.
3- The CodeBlock
c
for a do
sequence nested in a monadic combinator (e.g., MonadExcept.tryCatch
).
The generated Syntax
term for c
must inform whether c
"exited" using Code.action
, Code.return
,
Code.break
or Code.continue
. We use the auxiliary types DoResult
s for storing this information.
For example, the auxiliary type DoResultPBC α σ
is used for a code block that exits with Code.action
,
and Code.break
/Code.continue
, α
is the type of values produced by the exit action
, and
σ
is the type of the tuple of reassigned variables.
The type DoResult α β σ
is usedf for code blocks that exit with
Code.action
, Code.return
, and Code.break
/Code.continue
, β
is the type of the returned values.
We don't use DoResult α β σ
for all cases because:
a) The elaborator would not be able to infer all type parameters without extra annotations. For example,
if the code block does not contain `Code.return _ _`, the elaborator will not be able to infer `β`.
b) We need to pattern match on the result produced by the combinator (e.g., `MonadExcept.tryCatch`),
but we don't want to consider "unreachable" cases.
We do not distinguish between cases that contain break
, but not continue
, and vice versa.
When listing all cases, we use a
to indicate the code block contains Code.action _
, r
for Code.return _ _
,
and b/c
for a code block that contains Code.break _
or Code.continue _
.
a
:Kind.regular
, typem (α × σ)
r
:Kind.regular
, typem (α × σ)
Note that the code that pattern matches on the result will behave differently in this case. It producesreturn a
for this case, andpure a
for the previous one.b/c
:Kind.nestedBC
, typem (DoResultBC σ)
a
andr
:Kind.nestedPR
, typem (DoResultPR α β σ)
a
andbc
:Kind.nestedSBC
, typem (DoResultSBC α σ)
r
andbc
:Kind.nestedSBC
, typem (DoResultSBC α σ)
Again the code that pattern matches on the result will behave differently in this case and the previous one. It producesreturn a
for the constructorDoResultSPR.pureReturn a u
for this case, andpure a
for the previous case.a
,r
,b/c
:Kind.nestedPRBC
, type typem (DoResultPRBC α β σ)
Here is the recipe for adding new combinators with nested do
s.
Example: suppose we want to support repeat doSeq
. Assuming we have repeat : m α → m α
1- Convert doSeq
into codeBlock : CodeBlock
2- Create term term
using mkNestedTerm code m uvars a r bc
where
code
is codeBlock.code
, uvars
is an array containing codeBlock.uvars
,
m
is a Syntax
representing the Monad, and
a
is true if code
contains Code.action _
,
r
is true if code
contains Code.return _ _
,
bc
is true if code
contains Code.break _
or Code.continue _
.
Remark: for combinators such as repeat
that take a single doSeq
, all
arguments, but m
, are extracted from codeBlock
.
3- Create the term repeat $term
4- and then, convert it into a doSeq
using matchNestedTermResult ref (repeat $term) uvsar a r bc
Helper method for annotating term
with the raw syntax ref
.
We use this method to implement finer-grained term infos for do
-blocks.
We use withRef term
to make sure the synthetic position for the with_annotate_term
is equal
to the one for term
. This is important for producing error messages when there is a type mismatch.
Consider the following example:
opaque f : IO Nat
def g : IO String := do
f
There is at type mismatch at f
, but it is detected when elaborating the expanded term
containing the with_annotate_term .. f
. The current getRef
when this annotate
is invoked
is not necessarily f
. Actually, it is the whole do
-block. By using withRef
we ensure
the synthetic position for the with_annotate_term ..
is equal to term
.
Recall that synthetic positions are used when generating error messages.
Equations
- One or more equations did not get rendered due to their size.
Instances For
- regular : Lean.Elab.Term.Do.ToTerm.Kind
- forIn : Lean.Elab.Term.Do.ToTerm.Kind
- forInWithReturn : Lean.Elab.Term.Do.ToTerm.Kind
- nestedBC : Lean.Elab.Term.Do.ToTerm.Kind
- nestedPR : Lean.Elab.Term.Do.ToTerm.Kind
- nestedSBC : Lean.Elab.Term.Do.ToTerm.Kind
- nestedPRBC : Lean.Elab.Term.Do.ToTerm.Kind
Instances For
Equations
- Lean.Elab.Term.Do.ToTerm.Kind.regular.isRegular = true
- x✝.isRegular = false
Instances For
- m : Lean.Syntax
Syntax to reference the monad associated with the do notation.
- returnType : Lean.Syntax
Syntax to reference the result of the monadic computation performed by the do notation.
- uvars : Array Lean.Elab.Term.Do.Var
Instances For
Instances For
Equations
- Lean.Elab.Term.Do.ToTerm.mkUVarTuple = do let ctx ← read liftM (Lean.Elab.Term.Do.mkTuple✝ ctx.uvars)
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Elab.Term.Do.ToTerm.mkJmp ref j args = (Lean.Syntax.mkApp { raw := (Lean.mkIdentFrom ref j).raw } (Lean.TSyntaxArray.mk args)).raw
Instances For
Equations
- Lean.Elab.Term.Do.ToTerm.run code m returnType uvars kind = Lean.Elab.Term.Do.ToTerm.toTerm code { m := m, returnType := returnType, uvars := uvars, kind := kind }
Instances For
Given
a
is true if the code block has aCode.action _
exit pointr
is true if the code block has aCode.return _ _
exit pointbc
is true if the code block has aCode.break _
orCode.continue _
exit point
generate Kind. See comment at the beginning of the ToTerm
namespace.
Equations
- Lean.Elab.Term.Do.ToTerm.mkNestedKind true false false = Lean.Elab.Term.Do.ToTerm.Kind.regular
- Lean.Elab.Term.Do.ToTerm.mkNestedKind false true false = Lean.Elab.Term.Do.ToTerm.Kind.regular
- Lean.Elab.Term.Do.ToTerm.mkNestedKind false false true = Lean.Elab.Term.Do.ToTerm.Kind.nestedBC
- Lean.Elab.Term.Do.ToTerm.mkNestedKind true true false = Lean.Elab.Term.Do.ToTerm.Kind.nestedPR
- Lean.Elab.Term.Do.ToTerm.mkNestedKind true false true = Lean.Elab.Term.Do.ToTerm.Kind.nestedSBC
- Lean.Elab.Term.Do.ToTerm.mkNestedKind false true true = Lean.Elab.Term.Do.ToTerm.Kind.nestedSBC
- Lean.Elab.Term.Do.ToTerm.mkNestedKind true true true = Lean.Elab.Term.Do.ToTerm.Kind.nestedPRBC
- Lean.Elab.Term.Do.ToTerm.mkNestedKind false false false = panicWithPosWithDecl "Lean.Elab.Do" "Lean.Elab.Term.Do.ToTerm.mkNestedKind" 1183 27 "unreachable code has been reached"
Instances For
Equations
- Lean.Elab.Term.Do.ToTerm.mkNestedTerm code m returnType uvars a r bc = Lean.Elab.Term.Do.ToTerm.run code m returnType uvars (Lean.Elab.Term.Do.ToTerm.mkNestedKind a r bc)
Instances For
Given a term term
produced by ToTerm.run
, pattern match on its result.
See comment at the beginning of the ToTerm
namespace.
a
is true if the code block has aCode.action _
exit pointr
is true if the code block has aCode.return _ _
exit pointbc
is true if the code block has aCode.break _
orCode.continue _
exit point
The result is a sequence of doElem
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
- ref : Lean.Syntax
- m : Lean.Syntax
Syntax representing the monad associated with the do notation.
- returnType : Lean.Syntax
Syntax to reference the result of the monadic computation performed by the do notation.
- mutableVars : Lean.Elab.Term.Do.VarSet
- insideFor : Bool
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
- uvars : Array Lean.Elab.Term.Do.Var
- term : Lean.Syntax
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Elab.Term.Do.ToCodeBlock.ensureEOS doElems = if doElems.isEmpty = true then pure PUnit.unit else Lean.throwError (Lean.toMessageData "must be last element in a `do` sequence")
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Generate CodeBlock
for doReturn
which is of the form
"return " >> optional termParser
doElems
is only used for sanity checking.
Equations
- One or more equations did not get rendered due to their size.
Instances For
- x : Lean.Syntax
- optType : Lean.Syntax
- codeBlock : Lean.Elab.Term.Do.CodeBlock
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
- Lean.Elab.Term.Do.ToCodeBlock.tryCatchPred tryCode catches none p = ((p tryCode.code || catches.any fun («catch» : Lean.Elab.Term.Do.ToCodeBlock.Catch) => p «catch».codeBlock.code) || false)
Instances For
"Concatenate" c
with doSeqToCode doElems
Generate CodeBlock
for doLetArrow; doElems
doLetArrow
is of the form
"let " >> optional "mut " >> (doIdDecl <|> doPatDecl)
where
def doIdDecl := leading_parser ident >> optType >> leftArrow >> doElemParser
def doPatDecl := leading_parser termParser >> leftArrow >> doElemParser >> optional (" | " >> doSeq)
Generate CodeBlock
for doReassignArrow; doElems
doReassignArrow
is of the form
(doIdDecl <|> doPatDecl)
Generate CodeBlock
for doIf; doElems
doIf
is of the form
"if " >> optIdent >> termParser >> " then " >> doSeq
>> many (group (try (group (" else " >> " if ")) >> optIdent >> termParser >> " then " >> doSeq))
>> optional (" else " >> doSeq)
Generate CodeBlock
for doUnless; doElems
doUnless
is of the form
"unless " >> termParser >> "do " >> doSeq
Generate CodeBlock
for doFor; doElems
doFor
is of the form
def doForDecl := leading_parser termParser >> " in " >> withForbidden "do" termParser
def doFor := leading_parser "for " >> sepBy1 doForDecl ", " >> "do " >> doSeq
Generate CodeBlock
for doMatch; doElems
Generate CodeBlock
for doMatchExpr; doElems
Generate CodeBlock
for doTry; doElems
def doTry := leading_parser "try " >> doSeq >> many (doCatch <|> doCatchMatch) >> optional doFinally
def doCatch := leading_parser "catch " >> binderIdent >> optional (":" >> termParser) >> darrow >> doSeq
def doCatchMatch := leading_parser "catch " >> doMatchAlts
def doFinally := leading_parser "finally " >> doSeq
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Elab.Term.expandTermFor = Lean.Elab.Term.toDoElem✝ `Lean.Parser.Term.doFor
Instances For
Equations
- Lean.Elab.Term.expandTermTry = Lean.Elab.Term.toDoElem✝ `Lean.Parser.Term.doTry
Instances For
Equations
- Lean.Elab.Term.expandTermUnless = Lean.Elab.Term.toDoElem✝ `Lean.Parser.Term.doUnless
Instances For
Equations
- Lean.Elab.Term.expandTermReturn = Lean.Elab.Term.toDoElem✝ `Lean.Parser.Term.doReturn