Equations
- Lean.Elab.Term.elabLiftMethod stx x = Lean.throwErrorAt stx (Lean.toMessageData "invalid use of `(<- ...)`, must be nested inside a 'do' expression")
- ref : Lean.Syntax
- vars : Array Lean.Elab.Term.Do.Var
- patterns : Lean.Syntax
- rhs : σ
A doMatch alternative. vars is the array of variables declared by patterns.
Instances For
Equations
- Lean.Elab.Term.Do.instInhabitedAlt = { default := { ref := default, vars := default, patterns := default, rhs := default } }
- decl: Array Lean.Elab.Term.Do.Var → Lean.Syntax → Lean.Elab.Term.Do.Code → Lean.Elab.Term.Do.Code
- reassign: Array Lean.Elab.Term.Do.Var → Lean.Syntax → Lean.Elab.Term.Do.Code → Lean.Elab.Term.Do.Code
- joinpoint: Lean.Name → Array (Lean.Elab.Term.Do.Var × Bool) → Lean.Elab.Term.Do.Code → Lean.Elab.Term.Do.Code → Lean.Elab.Term.Do.Code
The Boolean value in
paramsindicates whether we should use(x : typeof! x)when generating term Syntax or not - seq: Lean.Syntax → Lean.Elab.Term.Do.Code → Lean.Elab.Term.Do.Code
- action: Lean.Syntax → Lean.Elab.Term.Do.Code
- break: Lean.Syntax → Lean.Elab.Term.Do.Code
- continue: Lean.Syntax → Lean.Elab.Term.Do.Code
- return: Lean.Syntax → Lean.Syntax → Lean.Elab.Term.Do.Code
- ite: Lean.Syntax → Option Lean.Elab.Term.Do.Var → Lean.Syntax → Lean.Syntax → Lean.Elab.Term.Do.Code → Lean.Elab.Term.Do.Code → Lean.Elab.Term.Do.Code
Recall that an if-then-else may declare a variable using
optIdentfor the branchesthenBranchandelseBranch. We store the variable name atvar?. - match: Lean.Syntax → Lean.Syntax → Lean.Syntax → Lean.Syntax → Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Lean.Elab.Term.Do.Code
- jmp: Lean.Syntax → Lean.Name → Array Lean.Syntax → Lean.Elab.Term.Do.Code
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
forIncombinator.
We say the following constructors are terminals:
break: for interrupting afor x in scontinue: for interrupting the current iteration of afor x in sreturn e: for returningeas the result for the wholedocomputation blockaction a: for executing actionaas a terminalite: if-then-elsematch: pattern matchingjmpa 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.
-
declrepresents all declaration-likedoElems (e.g.,let,have,let rec). The fieldstxis the actualdoElem,varsis the array of variables declared by it, andcontis the next instruction in thedocode block.varsis an array since we have declarations such aslet (a, b) := s. -
reassignis an reassignment-likedoElem(e.g.,x := x + 1). -
joinpointis a join point declaration: an auxiliarylet-declaration used to represent the control-flow. -
seq a kexecutes actiona, ignores its result, and then executesk. We also store the do-elementsdbg_traceandassert!as actions in aseq.
A code block C is well-formed if
- For every
jmp ref j asinC, there is ajoinpoint j ps b kandjmp ref j asis ink, andps.size == as.size
Instances For
Equations
- Lean.Elab.Term.Do.instInhabitedCode = { default := Lean.Elab.Term.Do.Code.action default }
Equations
- One or more equations did not get rendered due to their size.
- code : Lean.Elab.Term.Do.Code
- uvars : Lean.Elab.Term.Do.VarSet
A code block, and the collection of variables updated by it.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Return true if the give code contains an exit point that satisfies p
Equations
Equations
Equations
- Lean.Elab.Term.Do.hasReturn c = Lean.Elab.Term.Do.hasExitPointPred c fun x => match x with | Lean.Elab.Term.Do.Code.return ref val => true | x => false
Equations
- Lean.Elab.Term.Do.hasTerminalAction c = Lean.Elab.Term.Do.hasExitPointPred c fun x => match x with | Lean.Elab.Term.Do.Code.action action => true | x => false
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Convert action _ e instructions in c into let y ← e; jmp _ jp (xs y).
Equations
- 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
Equations
- Lean.Elab.Term.Do.attachJPs jpDecls k = Array.foldr Lean.Elab.Term.Do.attachJP k jpDecls (Array.size jpDecls)
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Elab.Term.Do.addFreshJP ps body = do let jp ← liftM (Lean.Elab.Term.Do.mkFreshJP ps body) modify fun jps => Array.push jps jp pure jp.name
Equations
- Lean.Elab.Term.Do.insertVars rs xs = Array.foldl (fun rs x => Lean.RBMap.insert rs (Lean.Syntax.getId x) x) rs xs 0 (Array.size xs)
Equations
- Lean.Elab.Term.Do.eraseVars rs xs = Array.foldl (fun x x_1 => Lean.RBMap.erase x (Lean.Syntax.getId x_1)) rs xs 0 (Array.size xs)
Equations
- Lean.Elab.Term.Do.eraseOptVar rs x? = match x? with | none => rs | some x => Lean.RBMap.insert rs (Lean.Syntax.getId x) x
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.
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.
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.
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.
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.
Extending code blocks with variable declarations: let x : t := v and let x : t ← v.
We remove x from the collection of updated varibles.
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 }
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.
Equations
- Lean.Elab.Term.Do.mkSeq action c = { code := Lean.Elab.Term.Do.Code.seq action c.code, uvars := c.uvars }
Equations
- Lean.Elab.Term.Do.mkTerminalAction action = { code := Lean.Elab.Term.Do.Code.action action, uvars := ∅ }
Equations
- Lean.Elab.Term.Do.mkReturn ref val = { code := Lean.Elab.Term.Do.Code.return ref val, uvars := ∅ }
Equations
- Lean.Elab.Term.Do.mkBreak ref = { code := Lean.Elab.Term.Do.Code.break ref, uvars := ∅ }
Equations
- Lean.Elab.Term.Do.mkContinue ref = { code := Lean.Elab.Term.Do.Code.continue ref, uvars := ∅ }
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Elab.Term.Do.mkPureUnitAction = do let __do_lift ← Lean.Elab.Term.Do.mkPureUnit pure (Lean.Elab.Term.Do.mkTerminalAction __do_lift)
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
- Lean.Elab.Term.Do.getLetIdDeclVar letIdDecl = letIdDecl[0]
Equations
- Lean.Elab.Term.Do.getPatternVarsEx pattern = HOrElse.hOrElse (Lean.Elab.Term.getPatternVars pattern) fun x => Lean.Elab.Term.Quotation.getPatternVars pattern
Equations
- Lean.Elab.Term.Do.getPatternsVarsEx patterns = HOrElse.hOrElse (Lean.Elab.Term.getPatternsVars patterns) fun x => Lean.Elab.Term.Quotation.getPatternsVars patterns
Equations
- Lean.Elab.Term.Do.getLetPatDeclVars letPatDecl = let pattern := letPatDecl[0]; Lean.Elab.Term.Do.getPatternVarsEx pattern
Equations
- Lean.Elab.Term.Do.getLetEqnsDeclVar letEqnsDecl = letEqnsDecl[0]
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Elab.Term.Do.getDoLetVars doLet = Lean.Elab.Term.Do.getLetDeclVars doLet[2]
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Elab.Term.Do.getDoIdDeclVar doIdDecl = doIdDecl[0]
Equations
- Lean.Elab.Term.Do.getDoPatDeclVars doPatDecl = let pattern := doPatDecl[0]; Lean.Elab.Term.Do.getPatternVarsEx pattern
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Elab.Term.Do.mkDoSeq doElems = (Lean.mkNode `Lean.Parser.Term.doSeqIndent #[Lean.mkNullNode (Array.map (fun doElem => Lean.mkNullNode #[doElem, Lean.mkNullNode]) doElems)]).raw
- ref : Lean.Syntax
- optIdent : Lean.Syntax
- cond : Lean.Syntax
- thenBranch : Lean.Syntax
- elseBranch : Lean.Syntax
Instances For
Return some action if doElem is a doExpr
Equations
- Lean.Elab.Term.Do.isDoExpr? doElem = if (Lean.Syntax.getKind doElem == `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, typem (α × σ) -
r:Kind.regular, typem (α × σ)Note that the code that pattern matches on the result will behave differently in this case. It producesreturn afor this case, andpure afor the previous one. -
b/c:Kind.nestedBC, typem (DoResultBC σ) -
aandr:Kind.nestedPR, typem (DoResultPR α β σ) -
aandbc:Kind.nestedSBC, typem (DoResultSBC α σ) -
randbc: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 afor the constructorDoResultSPR.pureReturn a ufor this case, andpure afor the previous case. -
a,r,b/c:Kind.nestedPRBC, type typem (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
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.
- 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.isRegular x = match x with | Lean.Elab.Term.Do.ToTerm.Kind.regular => true | x => false
Syntax to reference the monad associated with the do notation.
m : Lean.SyntaxSyntax to reference the result of the monadic computation performed by the do notation.
returnType : Lean.Syntax- uvars : Array Lean.Elab.Term.Do.Var
Instances For
Equations
- Lean.Elab.Term.Do.ToTerm.mkUVarTuple = do let ctx ← read liftM (Lean.Elab.Term.Do.mkTuple ctx.uvars)
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Elab.Term.Do.ToTerm.mkJmp ref j args = (Lean.Syntax.mkApp { raw := (Lean.mkIdentFrom ref j).raw } (Lean.TSyntaxArray.mk args)).raw
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 }
Given
ais true if the code block has aCode.action _exit pointris true if the code block has aCode.return _ _exit pointbcis true if the code block has aCode.break _orCode.continue _exit point
generate Kind. See comment at the beginning of the ToTerm namespace.
Equations
- One or more equations did not get rendered due to their size.
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)
Given a term term produced by ToTerm.run, pattern match on its result.
See comment at the beginning of the ToTerm namespace.
ais true if the code block has aCode.action _exit pointris true if the code block has aCode.return _ _exit pointbcis 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.
Equations
- One or more equations did not get rendered due to their size.
- ref : Lean.Syntax
Syntax representing the monad associated with the do notation.
m : Lean.SyntaxSyntax to reference the result of the monadic computation performed by the do notation.
returnType : Lean.Syntax- mutableVars : Lean.Elab.Term.Do.VarSet
- insideFor : Bool
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Elab.Term.Do.ToCodeBlock.withFor x = withReader (fun ctx => { ref := ctx.ref, m := ctx.m, returnType := ctx.returnType, mutableVars := ctx.mutableVars, insideFor := true }) x
- 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.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Elab.Term.Do.ToCodeBlock.ensureEOS doElems = if List.isEmpty doElems = true then pure PUnit.unit else Lean.throwError (Lean.toMessageData "must be last element in a `do` sequence")
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
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.
- 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.
Equations
- One or more equations did not get rendered due to their size.
"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 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.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Elab.Term.expandTermFor = Lean.Elab.Term.toDoElem `Lean.Parser.Term.doFor
Equations
- Lean.Elab.Term.expandTermTry = Lean.Elab.Term.toDoElem `Lean.Parser.Term.doTry
Equations
- Lean.Elab.Term.expandTermUnless = Lean.Elab.Term.toDoElem `Lean.Parser.Term.doUnless
Equations
- Lean.Elab.Term.expandTermReturn = Lean.Elab.Term.toDoElem `Lean.Parser.Term.doReturn