def Lean.Elab.Term.elabLiftMethod : TermElab

Equations

• Lean.Elab.Term.elabLiftMethod stx x✝ = Lean.throwErrorAt stx (Lean.toMessageData "invalid use of `(<- ...)`, must be nested inside a 'do' expression")

structure Lean.Elab.Term.ExtractMonadResult : Type

• m : Expr
• returnType : Expr
• expectedType : Expr

@[reducible, inline]

abbrev Lean.Elab.Term.Do.Var : Type

Equations

• Lean.Elab.Term.Do.Var = Lean.Syntax

structure Lean.Elab.Term.Do.Alt (σ : Type) : Type

A doMatch alternative. vars is the array of variables declared by patterns.

• ref : Syntax
• vars : Array Var
• patterns : Syntax
• rhs : σ

def Lean.Elab.Term.Do.instInhabitedAlt.default {a✝ : Type} [Inhabited a✝] : Alt a✝

Equations

• Lean.Elab.Term.Do.instInhabitedAlt.default = { ref := default, vars := default, patterns := default, rhs := default }

instance Lean.Elab.Term.Do.instInhabitedAlt {a✝ : Type} [Inhabited a✝] : Inhabited (Alt a✝)

Equations

• Lean.Elab.Term.Do.instInhabitedAlt = { default := Lean.Elab.Term.Do.instInhabitedAlt.default }

structure Lean.Elab.Term.Do.AltExpr (σ : Type) : Type

A doMatchExpr alternative.

• ref : Syntax
• var? : Option Var
• funName : Syntax
• pvars : Array Syntax
• rhs : σ

def Lean.Elab.Term.Do.instInhabitedAltExpr.default {a✝ : Type} [Inhabited a✝] : AltExpr a✝

Equations

• Lean.Elab.Term.Do.instInhabitedAltExpr.default = { ref := default, var? := default, funName := default, pvars := default, rhs := default }

instance Lean.Elab.Term.Do.instInhabitedAltExpr {a✝ : Type} [Inhabited a✝] : Inhabited (AltExpr a✝)

Equations

• Lean.Elab.Term.Do.instInhabitedAltExpr = { default := Lean.Elab.Term.Do.instInhabitedAltExpr.default }

def Lean.Elab.Term.Do.AltExpr.vars {σ : Type} (alt : AltExpr σ) : Array Var

Equations

• One or more equations did not get rendered due to their size.

inductive Lean.Elab.Term.Do.Code : Type

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 a for x in s
• continue: for interrupting the current iteration of a for x in s
• return e: for returning e as the result for the whole do computation block
• action a: for executing action a as a terminal
• ite: if-then-else
• match: pattern matching
• jmp 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-like doElems (e.g., let, have, let rec). The field stx is the actual doElem, vars is the array of variables declared by it, and cont is the next instruction in the do code block. vars is an array since we have declarations such as let (a, b) := s.

• reassign is an reassignment-like doElem (e.g., x := x + 1).

• joinpoint is a join point declaration: an auxiliary let-declaration used to represent the control-flow.

• seq a k executes action a, ignores its result, and then executes k. We also store the do-elements dbg_trace and assert! as actions in a seq.

A code block C is well-formed if

• For every jmp ref j as in C, there is a joinpoint j ps b k and jmp ref j as is in k, and ps.size == as.size

• decl (xs : Array Var) (doElem : Syntax) (k : Code) : Code
• reassign (xs : Array Var) (doElem : Syntax) (k : Code) : Code
• joinpoint (name : Name) (params : Array (Var × Bool)) (body k : Code) : Code

  The Boolean value in params indicates whether we should use (x : typeof! x) when generating term Syntax or not

• seq (action : Syntax) (k : Code) : Code
• action (action : Syntax) : Code
• break (ref : Syntax) : Code
• continue (ref : Syntax) : Code
• return (ref val : Syntax) : Code
• ite (ref : Syntax) (h? : Option Var) (optIdent cond : Syntax) (thenBranch elseBranch : Code) : Code

  Recall that an if-then-else may declare a variable using optIdent for the branches thenBranch and elseBranch. We store the variable name at var?.

• match (ref gen discrs optMotive : Syntax) (alts : Array (Alt Code)) : Code
• matchExpr (ref : Syntax) («meta» : Bool) (discr : Syntax) (alts : Array (AltExpr Code)) (elseBranch : Code) : Code
• jmp (ref : Syntax) (jpName : Name) (args : Array Syntax) : Code

instance Lean.Elab.Term.Do.instInhabitedCode : Inhabited Code

Equations

• Lean.Elab.Term.Do.instInhabitedCode = { default := Lean.Elab.Term.Do.instInhabitedCode.default }

def Lean.Elab.Term.Do.instInhabitedCode.default : Code

Equations

• Lean.Elab.Term.Do.instInhabitedCode.default = Lean.Elab.Term.Do.Code.action default

def Lean.Elab.Term.Do.Code.getRef? : Code → Option Syntax

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

@[reducible, inline]

abbrev Lean.Elab.Term.Do.VarSet : Type

Equations

• Lean.Elab.Term.Do.VarSet = Std.TreeMap Lean.Name Lean.Syntax Lean.Name.cmp

structure Lean.Elab.Term.Do.CodeBlock : Type

A code block, and the collection of variables updated by it.

• code : Code
• uvars : VarSet

def Lean.Elab.Term.Do.CodeBlock.toMessageData (codeBlock : CodeBlock) : MessageData

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.Do.hasExitPointPred (c : Code) (p : Code → Bool) : Bool

Return true if the give code contains an exit point that satisfies p

Equations

• Lean.Elab.Term.Do.hasExitPointPred c p = Lean.Elab.Term.Do.hasExitPointPred.loop✝ p c

def Lean.Elab.Term.Do.hasExitPoint (c : Code) : Bool

Equations

• Lean.Elab.Term.Do.hasExitPoint c = Lean.Elab.Term.Do.hasExitPointPred c fun (x : Lean.Elab.Term.Do.Code) => true

def Lean.Elab.Term.Do.hasReturn (c : Code) : Bool

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

def Lean.Elab.Term.Do.hasTerminalAction (c : Code) : Bool

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

def Lean.Elab.Term.Do.hasBreakContinue (c : Code) : Bool

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.Do.hasBreakContinueReturn (c : Code) : Bool

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.Do.mkAuxDeclFor {m : Type → Type} [Monad m] [MonadQuotation m] (e : Syntax) (mkCont : Syntax → m Code) : m Code

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.Do.convertTerminalActionIntoJmp (code : Code) (jp : Name) (xs : Array Var) : MacroM Code

Convert action _ e instructions in c into let y ← e; jmp _ jp (xs y).

Equations

• Lean.Elab.Term.Do.convertTerminalActionIntoJmp code jp xs = Lean.Elab.Term.Do.convertTerminalActionIntoJmp.loop✝ jp xs code

structure Lean.Elab.Term.Do.JPDecl : Type

• name : Name
• params : Array (Var × Bool)
• body : Code

def Lean.Elab.Term.Do.attachJP (jpDecl : JPDecl) (k : Code) : Code

Equations

• Lean.Elab.Term.Do.attachJP jpDecl k = Lean.Elab.Term.Do.Code.joinpoint jpDecl.name jpDecl.params jpDecl.body k

def Lean.Elab.Term.Do.attachJPs (jpDecls : Array JPDecl) (k : Code) : Code

Equations

• Lean.Elab.Term.Do.attachJPs jpDecls k = Array.foldr Lean.Elab.Term.Do.attachJP k jpDecls

def Lean.Elab.Term.Do.mkFreshJP (ps : Array (Var × Bool)) (body : Code) : TermElabM JPDecl

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.Do.addFreshJP (ps : Array (Var × Bool)) (body : Code) : StateRefT' IO.RealWorld (Array JPDecl) TermElabM Name

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

def Lean.Elab.Term.Do.insertVars (rs : VarSet) (xs : Array Var) : VarSet

Equations

• Lean.Elab.Term.Do.insertVars rs xs = Array.foldl (fun (rs : Lean.Elab.Term.Do.VarSet) (x : Lean.Syntax) => Std.TreeMap.insert rs x.getId x) rs xs

def Lean.Elab.Term.Do.eraseVars (rs : VarSet) (xs : Array Var) : VarSet

Equations

• Lean.Elab.Term.Do.eraseVars rs xs = Array.foldl (fun (x1 : Lean.Elab.Term.Do.VarSet) (x2 : Lean.Elab.Term.Do.Var) => Std.TreeMap.erase x1 (Lean.Syntax.getId x2)) rs xs

def Lean.Elab.Term.Do.eraseOptVar (rs : VarSet) (x? : Option Var) : VarSet

Equations

• Lean.Elab.Term.Do.eraseOptVar rs none = rs
• Lean.Elab.Term.Do.eraseOptVar rs (some x) = Std.TreeMap.insert rs (Lean.Syntax.getId x) x

def Lean.Elab.Term.Do.mkSimpleJmp (ref : Syntax) (rs : VarSet) (c : Code) : StateRefT' IO.RealWorld (Array JPDecl) TermElabM Code

Create a new join point for c, and jump to it with the variables rs

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.Do.mkJmp (ref : Syntax) (rs : VarSet) (val : Syntax) (mkJPBody : Syntax → MacroM Code) : StateRefT' IO.RealWorld (Array JPDecl) TermElabM Code

Create a new join point that takes rs and val as arguments. val must be syntax representing a pure value. The body of the join point 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.

partial def Lean.Elab.Term.Do.pullExitPointsAux (rs : VarSet) (c : Code) : StateRefT' IO.RealWorld (Array JPDecl) TermElabM Code

pullExitPointsAux rs c auxiliary method for pullExitPoints, rs is the set of update variable in the current path.

def Lean.Elab.Term.Do.pullExitPoints (c : Code) : TermElabM Code

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.

def Lean.Elab.Term.Do.extendUpdatedVarsAux (c : Code) (ws : VarSet) : TermElabM Code

Equations

• Lean.Elab.Term.Do.extendUpdatedVarsAux c ws = Lean.Elab.Term.Do.extendUpdatedVarsAux.update✝ ws c

def Lean.Elab.Term.Do.extendUpdatedVars (c : CodeBlock) (ws : VarSet) : TermElabM CodeBlock

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.

def Lean.Elab.Term.Do.homogenize (c₁ c₂ : CodeBlock) : TermElabM (CodeBlock × CodeBlock)

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.

def Lean.Elab.Term.Do.mkVarDeclCore (xs : Array Var) (stx : Syntax) (c : CodeBlock) : CodeBlock

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 }

def Lean.Elab.Term.Do.mkReassignCore (xs : Array Var) (stx : Syntax) (c : CodeBlock) : TermElabM CodeBlock

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.

def Lean.Elab.Term.Do.mkSeq (action : Syntax) (c : CodeBlock) : CodeBlock

Equations

• Lean.Elab.Term.Do.mkSeq action c = { code := Lean.Elab.Term.Do.Code.seq action c.code, uvars := c.uvars }

def Lean.Elab.Term.Do.mkTerminalAction (action : Syntax) : CodeBlock

Equations

• Lean.Elab.Term.Do.mkTerminalAction action = { code := Lean.Elab.Term.Do.Code.action action }

def Lean.Elab.Term.Do.mkReturn (ref val : Syntax) : CodeBlock

Equations

• Lean.Elab.Term.Do.mkReturn ref val = { code := Lean.Elab.Term.Do.Code.return ref val }

def Lean.Elab.Term.Do.mkBreak (ref : Syntax) : CodeBlock

Equations

• Lean.Elab.Term.Do.mkBreak ref = { code := Lean.Elab.Term.Do.Code.break ref }

def Lean.Elab.Term.Do.mkContinue (ref : Syntax) : CodeBlock

Equations

• Lean.Elab.Term.Do.mkContinue ref = { code := Lean.Elab.Term.Do.Code.continue ref }

def Lean.Elab.Term.Do.mkIte (ref optIdent cond : Syntax) (thenBranch elseBranch : CodeBlock) : TermElabM CodeBlock

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.Do.mkPureUnitAction : MacroM CodeBlock

Equations

• Lean.Elab.Term.Do.mkPureUnitAction = do let __do_lift ← Lean.Elab.Term.Do.mkPureUnit✝ pure (Lean.Elab.Term.Do.mkTerminalAction __do_lift)

def Lean.Elab.Term.Do.mkUnless (cond : Syntax) (c : CodeBlock) : MacroM CodeBlock

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.Do.mkMatch (ref genParam discrs optMotive : Syntax) (alts : Array (Alt CodeBlock)) : TermElabM CodeBlock

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.Do.mkMatchExpr (ref : Syntax) («meta» : Bool) (discr : Syntax) (alts : Array (AltExpr CodeBlock)) (elseBranch : CodeBlock) : TermElabM CodeBlock

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.Do.concat (terminal : CodeBlock) (kRef : Syntax) (y? : Option Var) (k : CodeBlock) : TermElabM CodeBlock

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.

def Lean.Elab.Term.Do.getLetIdVars (letId : Syntax) : Array Var

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.Do.getLetIdDeclVars (letIdDecl : Syntax) : Array Var

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.Do.getPatternVarsEx (pattern : Syntax) : TermElabM (Array Var)

Equations

• Lean.Elab.Term.Do.getPatternVarsEx pattern = (Lean.Elab.Term.getPatternVars pattern <|> Lean.Elab.Term.Quotation.getPatternVars pattern)

def Lean.Elab.Term.Do.getPatternsVarsEx (patterns : Array Syntax) : TermElabM (Array Var)

Equations

• Lean.Elab.Term.Do.getPatternsVarsEx patterns = (Lean.Elab.Term.getPatternsVars patterns <|> Lean.Elab.Term.Quotation.getPatternsVars patterns)

def Lean.Elab.Term.Do.getLetPatDeclVars (letPatDecl : Syntax) : TermElabM (Array Var)

Equations

• Lean.Elab.Term.Do.getLetPatDeclVars letPatDecl = Lean.Elab.Term.Do.getPatternVarsEx letPatDecl[0]

def Lean.Elab.Term.Do.getLetEqnsDeclVars (letEqnsDecl : Syntax) : Array Var

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.Do.getLetDeclVars (letDecl : Syntax) : TermElabM (Array Var)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.Do.getDoLetVars (doLet : Syntax) : TermElabM (Array Var)

Equations

• Lean.Elab.Term.Do.getDoLetVars doLet = Lean.Elab.Term.Do.getLetDeclVars doLet[2]

def Lean.Elab.Term.Do.getDoHaveVars (doHave : Syntax) : TermElabM (Array Var)

Equations

• Lean.Elab.Term.Do.getDoHaveVars doHave = Lean.Elab.Term.Do.getLetDeclVars doHave[1]

def Lean.Elab.Term.Do.getDoLetRecVars (doLetRec : Syntax) : TermElabM (Array Var)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.Do.getDoIdDeclVar (doIdDecl : Syntax) : Var

Equations

• Lean.Elab.Term.Do.getDoIdDeclVar doIdDecl = doIdDecl[0]

def Lean.Elab.Term.Do.getDoPatDeclVars (doPatDecl : Syntax) : TermElabM (Array Var)

Equations

• Lean.Elab.Term.Do.getDoPatDeclVars doPatDecl = Lean.Elab.Term.Do.getPatternVarsEx doPatDecl[0]

def Lean.Elab.Term.Do.getDoLetArrowVars (doLetArrow : Syntax) : TermElabM (Array Var)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.Do.getDoReassignVars (doReassign : Syntax) : TermElabM (Array Var)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.Do.mkDoSeq (doElems : Array Syntax) : Syntax

Equations

• One or more equations did not get rendered due to their size.

structure Lean.Elab.Term.Do.DoIfView : Type

• ref : Syntax
• optIdent : Syntax
• cond : Syntax
• thenBranch : Syntax
• elseBranch : Syntax

def Lean.Elab.Term.Do.isDoExpr? (doElem : Syntax) : Option Syntax

Return some action if doElem is a doExpr <action>

Equations

• Lean.Elab.Term.Do.isDoExpr? doElem = if (doElem.getKind == `Lean.Parser.Term.doExpr) = true then some doElem[0] else none

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 DoResults 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, type m (α × σ)

• r: Kind.regular, type m (α × σ) Note that the code that pattern matches on the result will behave differently in this case. It produces return a for this case, and pure a for the previous one.

• b/c: Kind.nestedBC, type m (DoResultBC σ)

• a and r: Kind.nestedPR, type m (DoResultPR α β σ)

• a and bc: Kind.nestedSBC, type m (DoResultSBC α σ)

• r and bc: Kind.nestedSBC, type m (DoResultSBC α σ) Again the code that pattern matches on the result will behave differently in this case and the previous one. It produces return a for the constructor DoResultSPR.pureReturn a u for this case, and pure a for the previous case.

• a, r, b/c: Kind.nestedPRBC, type type m (DoResultPRBC α β σ)

Here is the recipe for adding new combinators with nested dos. 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

def Lean.Elab.Term.Do.annotate {m : Type → Type} [Monad m] [MonadRef m] [MonadQuotation m] (ref term : Syntax) : m Syntax

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.

inductive Lean.Elab.Term.Do.ToTerm.Kind : Type

• regular : Kind
• forIn : Kind
• forInWithReturn : Kind
• nestedBC : Kind
• nestedPR : Kind
• nestedSBC : Kind
• nestedPRBC : Kind

instance Lean.Elab.Term.Do.ToTerm.instInhabitedKind : Inhabited Kind

Equations

• Lean.Elab.Term.Do.ToTerm.instInhabitedKind = { default := Lean.Elab.Term.Do.ToTerm.Kind.regular }

def Lean.Elab.Term.Do.ToTerm.Kind.isRegular : Kind → Bool

Equations

• Lean.Elab.Term.Do.ToTerm.Kind.regular.isRegular = true
• x✝.isRegular = false

structure Lean.Elab.Term.Do.ToTerm.Context : Type

• m : Syntax

  Syntax to reference the monad associated with the do notation.

• returnType : Syntax

  Syntax to reference the result of the monadic computation performed by the do notation.

• uvars : Array Var
• kind : Kind

@[reducible, inline]

abbrev Lean.Elab.Term.Do.ToTerm.M (α : Type) : Type

Equations

• Lean.Elab.Term.Do.ToTerm.M = ReaderT Lean.Elab.Term.Do.ToTerm.Context Lean.MacroM

def Lean.Elab.Term.Do.ToTerm.mkUVarTuple : M Syntax

Equations

• Lean.Elab.Term.Do.ToTerm.mkUVarTuple = do let ctx ← read liftM (Lean.Elab.Term.Do.mkTuple✝ ctx.uvars)

def Lean.Elab.Term.Do.ToTerm.returnToTerm (val : Syntax) : M Syntax

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.Do.ToTerm.continueToTerm : M Syntax

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.Do.ToTerm.breakToTerm : M Syntax

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.Do.ToTerm.actionTerminalToTerm (action : Syntax) : M Syntax

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.Do.ToTerm.seqToTerm (action k : Syntax) : M Syntax

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.Do.ToTerm.declToTerm (decl k : Syntax) : M Syntax

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.Do.ToTerm.reassignToTerm (reassign k : Syntax) : MacroM Syntax

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.Do.ToTerm.mkIte (optIdent cond thenBranch elseBranch : Syntax) : MacroM Syntax

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.Do.ToTerm.mkJoinPoint (j : Name) (ps : Array (Syntax × Bool)) (body k : Syntax) : M Syntax

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.Do.ToTerm.mkJmp (ref : Syntax) (j : Name) (args : Array Syntax) : Syntax

Equations

• Lean.Elab.Term.Do.ToTerm.mkJmp ref j args = (Lean.Syntax.mkApp { raw := (Lean.mkIdentFrom ref j).raw } (Lean.TSyntaxArray.mk args)).raw

partial def Lean.Elab.Term.Do.ToTerm.toTerm (c : Code) : M Syntax

def Lean.Elab.Term.Do.ToTerm.run (code : Code) (m returnType : Syntax) (uvars : Array Var := #[]) (kind : Kind := Kind.regular) : MacroM Syntax

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 }

def Lean.Elab.Term.Do.ToTerm.mkNestedKind (a r bc : Bool) : Kind

Given

• a is true if the code block has a Code.action _ exit point
• r is true if the code block has a Code.return _ _ exit point
• bc is true if the code block has a Code.break _ or Code.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" 1196 27 "unreachable code has been reached"

def Lean.Elab.Term.Do.ToTerm.mkNestedTerm (code : Code) (m returnType : Syntax) (uvars : Array Var) (a r bc : Bool) : MacroM Syntax

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)

def Lean.Elab.Term.Do.ToTerm.matchNestedTermResult (term : Syntax) (uvars : Array Var) (a r bc : Bool) : MacroM (List Syntax)

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 a Code.action _ exit point
• r is true if the code block has a Code.return _ _ exit point
• bc is true if the code block has a Code.break _ or Code.continue _ exit point

The result is a sequence of doElem

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.Do.isMutableLet (doElem : Syntax) : Bool

Equations

• One or more equations did not get rendered due to their size.

structure Lean.Elab.Term.Do.ToCodeBlock.Context : Type

• ref : Syntax
• m : Syntax

  Syntax representing the monad associated with the do notation.

• returnType : Syntax

  Syntax to reference the result of the monadic computation performed by the do notation.

• mutableVars : VarSet
• insideFor : Bool

@[reducible, inline]

abbrev Lean.Elab.Term.Do.ToCodeBlock.M (α : Type) : Type

Equations

• Lean.Elab.Term.Do.ToCodeBlock.M = ReaderT Lean.Elab.Term.Do.ToCodeBlock.Context Lean.Elab.TermElabM

def Lean.Elab.Term.Do.ToCodeBlock.withNewMutableVars {α : Type} (newVars : Array Var) (mutable : Bool) (x : M α) : M α

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.Do.ToCodeBlock.checkReassignable (xs : Array Var) : M Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.Do.ToCodeBlock.checkNotShadowingMutable (xs : Array Var) : M Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.Do.ToCodeBlock.withFor {α : Type} (x : M α) : M α

Equations

• One or more equations did not get rendered due to their size.

structure Lean.Elab.Term.Do.ToCodeBlock.ToForInTermResult : Type

• uvars : Array Var
• term : Syntax

def Lean.Elab.Term.Do.ToCodeBlock.mkForInBody : Syntax → (forInBody : CodeBlock) → M ToForInTermResult

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.Do.ToCodeBlock.ensureInsideFor : M Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.Do.ToCodeBlock.ensureEOS (doElems : List Syntax) : M Unit

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")

def Lean.Elab.Term.Do.ToCodeBlock.expandLiftMethod (doElem : Syntax) : M (List Syntax × Syntax)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.Do.ToCodeBlock.checkLetArrowRHS (doElem : Syntax) : M Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.Do.ToCodeBlock.doReturnToCode (doReturn : Syntax) (doElems : List Syntax) : M CodeBlock

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.

structure Lean.Elab.Term.Do.ToCodeBlock.Catch : Type

• x : Syntax
• optType : Syntax
• codeBlock : CodeBlock

def Lean.Elab.Term.Do.ToCodeBlock.getTryCatchUpdatedVars (tryCode : CodeBlock) (catches : Array Catch) (finallyCode? : Option CodeBlock) : VarSet

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.Do.ToCodeBlock.tryCatchPred (tryCode : CodeBlock) (catches : Array Catch) (finallyCode? : Option CodeBlock) (p : Code → Bool) : Bool

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)

partial def Lean.Elab.Term.Do.ToCodeBlock.concatWith (c : CodeBlock) (doElems : List Syntax) : M CodeBlock

"Concatenate" c with doSeqToCode doElems

partial def Lean.Elab.Term.Do.ToCodeBlock.doLetArrowToCode (doLetArrow : Syntax) (doElems : List Syntax) : M CodeBlock

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)

partial def Lean.Elab.Term.Do.ToCodeBlock.doLetElseToCode (doLetElse : Syntax) (doElems : List Syntax) : M CodeBlock

partial def Lean.Elab.Term.Do.ToCodeBlock.doReassignArrowToCode (doReassignArrow : Syntax) (doElems : List Syntax) : M CodeBlock

Generate CodeBlock for doReassignArrow; doElems doReassignArrow is of the form

(doIdDecl <|> doPatDecl)

partial def Lean.Elab.Term.Do.ToCodeBlock.doIfToCode (doIf : Syntax) (doElems : List Syntax) : M CodeBlock

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)

partial def Lean.Elab.Term.Do.ToCodeBlock.doUnlessToCode (doUnless : Syntax) (doElems : List Syntax) : M CodeBlock

Generate CodeBlock for doUnless; doElems doUnless is of the form

"unless " >> termParser >> "do " >> doSeq

partial def Lean.Elab.Term.Do.ToCodeBlock.doForToCode (doFor : Syntax) (doElems : List Syntax) : M CodeBlock

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

partial def Lean.Elab.Term.Do.ToCodeBlock.doMatchToCode (doMatch : Syntax) (doElems : List Syntax) : M CodeBlock

Generate CodeBlock for doMatch; doElems

partial def Lean.Elab.Term.Do.ToCodeBlock.doMatchExprToCode (doMatchExpr : Syntax) (doElems : List Syntax) : M CodeBlock

Generate CodeBlock for doMatchExpr; doElems

partial def Lean.Elab.Term.Do.ToCodeBlock.doTryToCode (doTry : Syntax) (doElems : List Syntax) : M CodeBlock

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

partial def Lean.Elab.Term.Do.ToCodeBlock.doSeqToCode : List Syntax → M CodeBlock

def Lean.Elab.Term.Do.ToCodeBlock.run (doStx m returnType : Syntax) : TermElabM CodeBlock

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.Do.elabDo : TermElab

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Term.expandTermFor : Macro

Equations

• Lean.Elab.Term.expandTermFor = Lean.Elab.Term.toDoElem✝ `Lean.Parser.Term.doFor

def Lean.Elab.Term.expandTermTry : Macro

Equations

• Lean.Elab.Term.expandTermTry = Lean.Elab.Term.toDoElem✝ `Lean.Parser.Term.doTry

def Lean.Elab.Term.expandTermUnless : Macro

Equations

• Lean.Elab.Term.expandTermUnless = Lean.Elab.Term.toDoElem✝ `Lean.Parser.Term.doUnless

def Lean.Elab.Term.expandTermReturn : Macro

Equations

• Lean.Elab.Term.expandTermReturn = Lean.Elab.Term.toDoElem✝ `Lean.Parser.Term.doReturn