Lean.Elab.Do

Lean.Elab.Term.Do.mkFreshJP ps body = let _do_jp := fun ps => do let name ← liftM (Lean.mkFreshUserName `_do_jp) pure { name := name, params := ps, body := body }; if Array.isEmpty ps = true then do let y ← liftM (Lean.mkFreshUserName `y) let y ← pure #[(y, false)] _do_jp y else do let y ← pure ps _do_jp y

source

def Lean.Elab.Term.Do.mkFreshJP' (xs : Array Lean.Name) (body : Lean.Elab.Term.Do.Code) :

Lean.Elab.TermElabM Lean.Elab.Term.Do.JPDecl

Equations

Lean.Elab.Term.Do.mkFreshJP' xs body = Lean.Elab.Term.Do.mkFreshJP (Array.map (fun x => (x, true)) xs) body

source

def Lean.Elab.Term.Do.addFreshJP (ps : Array (Lean.Name × Bool)) (body : Lean.Elab.Term.Do.Code) :

StateRefT' IO.RealWorld (Array Lean.Elab.Term.Do.JPDecl) Lean.Elab.TermElabM Lean.Name

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

source

def Lean.Elab.Term.Do.insertVars (rs : Lean.NameSet) (xs : Array Lean.Name) :

Lean.NameSet

Equations

Lean.Elab.Term.Do.insertVars rs xs = Array.foldl (fun a a_1 => Lean.NameSet.insert a a_1) rs xs 0 (Array.size xs)

source

def Lean.Elab.Term.Do.eraseVars (rs : Lean.NameSet) (xs : Array Lean.Name) :

Lean.NameSet

Equations

Lean.Elab.Term.Do.eraseVars rs xs = Array.foldl (fun a a_1 => Std.RBTree.erase a a_1) rs xs 0 (Array.size xs)

source

def Lean.Elab.Term.Do.eraseOptVar (rs : Lean.NameSet) (x? : Option Lean.Name) :

Lean.NameSet

Equations

Lean.Elab.Term.Do.eraseOptVar rs x? = match x? with | none => rs | some x => Lean.NameSet.insert rs x

source

def Lean.Elab.Term.Do.mkSimpleJmp (ref : Lean.Syntax) (rs : Lean.NameSet) (c : Lean.Elab.Term.Do.Code) :

StateRefT' IO.RealWorld (Array Lean.Elab.Term.Do.JPDecl) Lean.Elab.TermElabM Lean.Elab.Term.Do.Code

Equations

Lean.Elab.Term.Do.mkSimpleJmp ref rs c = let xs := Lean.Elab.Term.Do.nameSetToArray rs; do let jp ← Lean.Elab.Term.Do.addFreshJP (Array.map (fun x => (x, true)) xs) c if Array.isEmpty xs = true then do let unit ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.ident info (String.toSubstring "Unit.unit") (Lean.addMacroScope mainModule `Unit.unit scp) [(`Unit.unit, [])]) pure (Lean.Elab.Term.Do.Code.jmp ref jp #[unit]) else pure (Lean.Elab.Term.Do.Code.jmp ref jp (Array.map (Lean.mkIdentFrom ref) xs))

source

def Lean.Elab.Term.Do.mkJmp (ref : Lean.Syntax) (rs : Lean.NameSet) (val : Lean.Syntax) (mkJPBody : Lean.Syntax → Lean.MacroM Lean.Elab.Term.Do.Code) :

StateRefT' IO.RealWorld (Array Lean.Elab.Term.Do.JPDecl) Lean.Elab.TermElabM Lean.Elab.Term.Do.Code

Equations

Lean.Elab.Term.Do.mkJmp ref rs val mkJPBody = let xs := Lean.Elab.Term.Do.nameSetToArray rs; let args := Array.map (Lean.mkIdentFrom ref) xs; let args := Array.push args val; do let yFresh ← liftM (Lean.mkFreshUserName `y) let ps : Array (Lean.Name × Bool) := Array.map (fun x => (x, true)) xs let ps : Array (Lean.Name × Bool) := Array.push ps (yFresh, false) let jpBody ← Lean.Elab.liftMacroM (mkJPBody (Lean.mkIdentFrom ref yFresh)) let jp ← Lean.Elab.Term.Do.addFreshJP ps jpBody pure (Lean.Elab.Term.Do.Code.jmp ref jp args)

source

partial def Lean.Elab.Term.Do.pullExitPointsAux :

Lean.NameSet → Lean.Elab.Term.Do.Code → StateRefT' IO.RealWorld (Array Lean.Elab.Term.Do.JPDecl) Lean.Elab.TermElabM Lean.Elab.Term.Do.Code

source

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

Lean.Elab.TermElabM Lean.Elab.Term.Do.Code

Equations

Lean.Elab.Term.Do.pullExitPoints c = if Lean.Elab.Term.Do.hasExitPoint c = true then do let discr ← StateRefT'.run (Lean.Elab.Term.Do.pullExitPointsAux ∅ c) #[] let x : Lean.Elab.Term.Do.Code × Array Lean.Elab.Term.Do.JPDecl := discr match x with | (c, jpDecls) => pure (Lean.Elab.Term.Do.attachJPs jpDecls c) else pure c

source

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

Lean.Elab.TermElabM Lean.Elab.Term.Do.Code

Equations

Lean.Elab.Term.Do.extendUpdatedVarsAux c ws = (fun update => update c) (Lean.Elab.Term.Do.extendUpdatedVarsAux.update ws)

source

partial def Lean.Elab.Term.Do.extendUpdatedVarsAux.update (ws : Lean.NameSet) :

Lean.Elab.Term.Do.Code → Lean.Elab.TermElabM Lean.Elab.Term.Do.Code

source

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

Lean.Elab.TermElabM Lean.Elab.Term.Do.CodeBlock

Equations

Lean.Elab.Term.Do.extendUpdatedVars c ws = if (Std.RBTree.any ws fun x => !Lean.NameSet.contains c.uvars x) = true then do let a ← Lean.Elab.Term.Do.extendUpdatedVarsAux c.code ws pure { code := a, uvars := ws } else pure { code := c.code, uvars := ws }

source

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

Lean.Elab.TermElabM (Lean.Elab.Term.Do.CodeBlock × Lean.Elab.Term.Do.CodeBlock)

Equations

Lean.Elab.Term.Do.homogenize c₁ c₂ = let ws := Lean.Elab.Term.Do.union c₁.uvars c₂.uvars; do let c₁ ← Lean.Elab.Term.Do.extendUpdatedVars c₁ ws let c₂ ← Lean.Elab.Term.Do.extendUpdatedVars c₂ ws pure (c₁, c₂)

source

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

Lean.Elab.Term.Do.CodeBlock

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 }

source

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

Lean.Elab.TermElabM Lean.Elab.Term.Do.CodeBlock

Equations

Lean.Elab.Term.Do.mkReassignCore xs stx c = let us := c.uvars; let ws := Lean.Elab.Term.Do.insertVars us xs; let _do_jp := fun code => pure { code := Lean.Elab.Term.Do.Code.reassign xs stx code, uvars := ws }; if Array.any xs (fun x => !Lean.NameSet.contains us x) 0 (Array.size xs) = true then do let y ← Lean.Elab.Term.Do.extendUpdatedVarsAux c.code ws _do_jp y else do let y ← pure c.code _do_jp y

source

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

Lean.Elab.Term.Do.CodeBlock

Equations

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

source

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

Lean.Elab.Term.Do.CodeBlock

Equations

Lean.Elab.Term.Do.mkTerminalAction action = { code := Lean.Elab.Term.Do.Code.action action, uvars := ∅ }

source

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

Lean.Elab.Term.Do.CodeBlock

Equations

Lean.Elab.Term.Do.mkReturn ref val = { code := Lean.Elab.Term.Do.Code.return ref val, uvars := ∅ }

source

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

Lean.Elab.Term.Do.CodeBlock

Equations

Lean.Elab.Term.Do.mkBreak ref = { code := Lean.Elab.Term.Do.Code.break ref, uvars := ∅ }

source

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

Lean.Elab.Term.Do.CodeBlock

Equations

Lean.Elab.Term.Do.mkContinue ref = { code := Lean.Elab.Term.Do.Code.continue ref, uvars := ∅ }

source

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

Lean.Elab.TermElabM Lean.Elab.Term.Do.CodeBlock

Equations

Lean.Elab.Term.Do.mkIte ref optIdent cond thenBranch elseBranch = let x? := if Lean.Syntax.isNone optIdent = true then none else some (Lean.Syntax.getId (Lean.Syntax.getOp optIdent 0)); do let discr ← Lean.Elab.Term.Do.homogenize thenBranch elseBranch let x : Lean.Elab.Term.Do.CodeBlock × Lean.Elab.Term.Do.CodeBlock := discr match x with | (thenBranch, elseBranch) => pure { code := Lean.Elab.Term.Do.Code.ite ref x? optIdent cond thenBranch.code elseBranch.code, uvars := thenBranch.uvars }

source

def Lean.Elab.Term.Do.mkPureUnitAction :

Lean.MacroM Lean.Elab.Term.Do.CodeBlock

Equations

Lean.Elab.Term.Do.mkPureUnitAction = do let a ← Lean.Elab.Term.Do.mkPureUnit pure (Lean.Elab.Term.Do.mkTerminalAction a)

source

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

Lean.MacroM Lean.Elab.Term.Do.CodeBlock

Equations

Lean.Elab.Term.Do.mkUnless cond c = do let thenBranch ← Lean.Elab.Term.Do.mkPureUnitAction let a ← Lean.getRef pure { code := Lean.Elab.Term.Do.Code.ite a none Lean.mkNullNode cond thenBranch.code c.code, uvars := c.uvars }

source

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

Lean.Elab.TermElabM Lean.Elab.Term.Do.CodeBlock

Equations

Lean.Elab.Term.Do.mkMatch ref genParam discrs optType alts = let ws := Array.foldl (fun a a_1 => Lean.Elab.Term.Do.union a a_1.rhs.uvars) ∅ alts 0 (Array.size alts); do let alts ← Array.mapM (fun alt => do let rhs ← Lean.Elab.Term.Do.extendUpdatedVars alt.rhs ws pure { ref := alt.ref, vars := alt.vars, patterns := alt.patterns, rhs := rhs.code }) alts pure { code := Lean.Elab.Term.Do.Code.match ref genParam discrs optType alts, uvars := ws }

source

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

Lean.Elab.TermElabM Lean.Elab.Term.Do.CodeBlock

Equations

Lean.Elab.Term.Do.concat terminal kRef y? k = let _do_jp := fun y => do let discr ← Lean.Elab.Term.Do.homogenize terminal k let x : Lean.Elab.Term.Do.CodeBlock × Lean.Elab.Term.Do.CodeBlock := discr match x with | (terminal, k) => let xs := Lean.Elab.Term.Do.nameSetToArray k.uvars; let _do_jp := fun y => let ps := Array.map (fun x => (x, true)) xs; let ps := Array.push ps (y, false); do let jpDecl ← Lean.Elab.Term.Do.mkFreshJP ps k.code let jp : Lean.Name := jpDecl.name let terminal ← Lean.Elab.liftMacroM (Lean.Elab.Term.Do.convertTerminalActionIntoJmp terminal.code jp xs) pure { code := Lean.Elab.Term.Do.attachJP jpDecl terminal, uvars := k.uvars }; match y? with | some y => do let y ← pure y _do_jp y | none => do let y ← liftM (Lean.mkFreshUserName `y) _do_jp y; if Lean.Elab.Term.Do.hasTerminalAction terminal.code = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.throwErrorAt kRef (Lean.toMessageData "'do' element is unreachable") _do_jp y

source

def Lean.Elab.Term.Do.getLetIdDeclVar (letIdDecl : Lean.Syntax) :

Lean.Name

Equations

Lean.Elab.Term.Do.getLetIdDeclVar letIdDecl = Lean.Syntax.getId (Lean.Syntax.getOp letIdDecl 0)

source

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

Lean.Elab.TermElabM (Array Lean.Name)

Equations

Lean.Elab.Term.Do.getPatternVarsEx pattern = HOrElse.hOrElse (Lean.Elab.Term.getPatternVarNames <$> Lean.Elab.Term.getPatternVars pattern) fun x => Array.map Lean.Syntax.getId <$> Lean.Elab.Term.Quotation.getPatternVars pattern

source

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

Lean.Elab.TermElabM (Array Lean.Name)

Equations

Lean.Elab.Term.Do.getPatternsVarsEx patterns = HOrElse.hOrElse (Lean.Elab.Term.getPatternVarNames <$> Lean.Elab.Term.getPatternsVars patterns) fun x => Array.map Lean.Syntax.getId <$> Lean.Elab.Term.Quotation.getPatternsVars patterns

source

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

Lean.Elab.TermElabM (Array Lean.Name)

Equations

Lean.Elab.Term.Do.getLetPatDeclVars letPatDecl = let pattern := Lean.Syntax.getOp letPatDecl 0; Lean.Elab.Term.Do.getPatternVarsEx pattern

source

def Lean.Elab.Term.Do.getLetEqnsDeclVar (letEqnsDecl : Lean.Syntax) :

Lean.Name

Equations

Lean.Elab.Term.Do.getLetEqnsDeclVar letEqnsDecl = Lean.Syntax.getId (Lean.Syntax.getOp letEqnsDecl 0)

source

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

Lean.Elab.TermElabM (Array Lean.Name)

Equations

Lean.Elab.Term.Do.getLetDeclVars letDecl = let arg := Lean.Syntax.getOp letDecl 0; if (Lean.Syntax.getKind arg == `Lean.Parser.Term.letIdDecl) = true then pure #[Lean.Elab.Term.Do.getLetIdDeclVar arg] else if (Lean.Syntax.getKind arg == `Lean.Parser.Term.letPatDecl) = true then Lean.Elab.Term.Do.getLetPatDeclVars arg else if (Lean.Syntax.getKind arg == `Lean.Parser.Term.letEqnsDecl) = true then pure #[Lean.Elab.Term.Do.getLetEqnsDeclVar arg] else Lean.throwError (Lean.toMessageData "unexpected kind of let declaration")

source

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

Lean.Elab.TermElabM (Array Lean.Name)

Equations

Lean.Elab.Term.Do.getDoLetVars doLet = Lean.Elab.Term.Do.getLetDeclVars (Lean.Syntax.getOp doLet 2)

source

def Lean.Elab.Term.Do.getHaveIdLhsVar (optIdent : Lean.Syntax) :

Lean.Name

Equations

Lean.Elab.Term.Do.getHaveIdLhsVar optIdent = if Lean.Syntax.isNone optIdent = true then `this else Lean.Syntax.getId (Lean.Syntax.getOp optIdent 0)

source

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

Lean.Elab.TermElabM (Array Lean.Name)

Equations

Lean.Elab.Term.Do.getDoHaveVars doHave = let arg := Lean.Syntax.getOp (Lean.Syntax.getOp doHave 1) 0; if (Lean.Syntax.getKind arg == `Lean.Parser.Term.haveIdDecl) = true then pure #[Lean.Elab.Term.Do.getHaveIdLhsVar (Lean.Syntax.getOp arg 0)] else if (Lean.Syntax.getKind arg == `Lean.Parser.Term.letPatDecl) = true then Lean.Elab.Term.Do.getLetPatDeclVars arg else if (Lean.Syntax.getKind arg == `Lean.Parser.Term.haveEqnsDecl) = true then pure #[Lean.Elab.Term.Do.getHaveIdLhsVar (Lean.Syntax.getOp arg 0)] else Lean.throwError (Lean.toMessageData "unexpected kind of have declaration")

source

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

Lean.Elab.TermElabM (Array Lean.Name)

Equations

Lean.Elab.Term.Do.getDoLetRecVars doLetRec = let letRecDecls := Lean.Syntax.getSepArgs (Lean.Syntax.getOp (Lean.Syntax.getOp doLetRec 1) 0); let letDecls := Array.map (fun p => Lean.Syntax.getOp p 2) letRecDecls; let allVars := #[]; do let r ← forIn letDecls allVars fun letDecl r => let allVars := r; do let vars ← Lean.Elab.Term.Do.getLetDeclVars letDecl let allVars : Array Lean.Name := allVars ++ vars pure PUnit.unit pure (ForInStep.yield allVars) let x : Array Lean.Name := r let allVars : Array Lean.Name := x pure allVars

source

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

Lean.Name

Equations

Lean.Elab.Term.Do.getDoIdDeclVar doIdDecl = Lean.Syntax.getId (Lean.Syntax.getOp doIdDecl 0)

source

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

Lean.Elab.TermElabM (Array Lean.Name)

Equations

Lean.Elab.Term.Do.getDoPatDeclVars doPatDecl = let pattern := Lean.Syntax.getOp doPatDecl 0; Lean.Elab.Term.Do.getPatternVarsEx pattern

source

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

Lean.Elab.TermElabM (Array Lean.Name)

Equations

Lean.Elab.Term.Do.getDoLetArrowVars doLetArrow = let decl := Lean.Syntax.getOp doLetArrow 2; if (Lean.Syntax.getKind decl == `Lean.Parser.Term.doIdDecl) = true then pure #[Lean.Elab.Term.Do.getDoIdDeclVar decl] else if (Lean.Syntax.getKind decl == `Lean.Parser.Term.doPatDecl) = true then Lean.Elab.Term.Do.getDoPatDeclVars decl else Lean.throwError (Lean.toMessageData "unexpected kind of 'do' declaration")

source

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

Lean.Elab.TermElabM (Array Lean.Name)

Equations

Lean.Elab.Term.Do.getDoReassignVars doReassign = let arg := Lean.Syntax.getOp doReassign 0; if (Lean.Syntax.getKind arg == `Lean.Parser.Term.letIdDecl) = true then pure #[Lean.Elab.Term.Do.getLetIdDeclVar arg] else if (Lean.Syntax.getKind arg == `Lean.Parser.Term.letPatDecl) = true then Lean.Elab.Term.Do.getLetPatDeclVars arg else Lean.throwError (Lean.toMessageData "unexpected kind of reassignment")

source

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

Lean.Syntax

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

source

def Lean.Elab.Term.Do.mkSingletonDoSeq (doElem : Lean.Syntax) :

Lean.Syntax

Equations

Lean.Elab.Term.Do.mkSingletonDoSeq doElem = Lean.Elab.Term.Do.mkDoSeq #[doElem]

source

structure Lean.Elab.Term.Do.DoIfView :

Type

ref : Lean.Syntax
optIdent : Lean.Syntax
cond : Lean.Syntax
thenBranch : Lean.Syntax
elseBranch : Lean.Syntax

source

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

Option Lean.Syntax

Equations

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

source

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

Type

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

source

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

Inhabited Lean.Elab.Term.Do.ToTerm.Kind

Equations

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

source

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

Lean.Elab.Term.Do.ToTerm.Kind → Bool

Equations

Lean.Elab.Term.Do.ToTerm.Kind.isRegular x = match x with | Lean.Elab.Term.Do.ToTerm.Kind.regular => true | x => false

source

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

Type

source

@[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

source

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

Lean.Elab.Term.Do.ToTerm.M Lean.Syntax

Equations

Lean.Elab.Term.Do.ToTerm.mkUVarTuple = do let ctx ← read let uvarIdents ← Array.mapM Lean.mkIdentFromRef ctx.uvars liftM (Lean.Elab.Term.Do.mkTuple uvarIdents)

source

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

Lean.Elab.Term.Do.ToTerm.M Lean.Syntax

Equations

Lean.Elab.Term.Do.ToTerm.returnToTerm val = do let ctx ← read let u ← Lean.Elab.Term.Do.ToTerm.mkUVarTuple match ctx.kind with | Lean.Elab.Term.Do.ToTerm.Kind.regular => if Array.isEmpty ctx.uvars = true then do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Pure.pure") (Lean.addMacroScope mainModule `Pure.pure scp) [(`Pure.pure, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[val]]) else do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Pure.pure") (Lean.addMacroScope mainModule `Pure.pure scp) [(`Pure.pure, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "MProd.mk") (Lean.addMacroScope mainModule `MProd.mk scp) [(`MProd.mk, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[val, u]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]]) | Lean.Elab.Term.Do.ToTerm.Kind.forIn => do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Pure.pure") (Lean.addMacroScope mainModule `Pure.pure scp) [(`Pure.pure, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "ForInStep.done") (Lean.addMacroScope mainModule `ForInStep.done scp) [(`ForInStep.done, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[u]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]]) | Lean.Elab.Term.Do.ToTerm.Kind.forInWithReturn => do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Pure.pure") (Lean.addMacroScope mainModule `Pure.pure scp) [(`Pure.pure, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "ForInStep.done") (Lean.addMacroScope mainModule `ForInStep.done scp) [(`ForInStep.done, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "MProd.mk") (Lean.addMacroScope mainModule `MProd.mk scp) [(`MProd.mk, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "some") (Lean.addMacroScope mainModule `some scp) [(`Option.some, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[val]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"], u]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]]) | Lean.Elab.Term.Do.ToTerm.Kind.nestedBC => panicWithPosWithDecl "Lean.Elab.Do" "Lean.Elab.Term.Do.ToTerm.returnToTerm" 885 28 "unreachable code has been reached" | Lean.Elab.Term.Do.ToTerm.Kind.nestedPR => do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Pure.pure") (Lean.addMacroScope mainModule `Pure.pure scp) [(`Pure.pure, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "DoResultPR.«return»") (Lean.addMacroScope mainModule `DoResultPR.return scp) [(`DoResultPR.return, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[val, u]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]]) | Lean.Elab.Term.Do.ToTerm.Kind.nestedSBC => do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Pure.pure") (Lean.addMacroScope mainModule `Pure.pure scp) [(`Pure.pure, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "DoResultSBC.«pureReturn»") (Lean.addMacroScope mainModule `DoResultSBC.pureReturn scp) [(`DoResultSBC.pureReturn, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[val, u]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]]) | Lean.Elab.Term.Do.ToTerm.Kind.nestedPRBC => do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Pure.pure") (Lean.addMacroScope mainModule `Pure.pure scp) [(`Pure.pure, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "DoResultPRBC.«return»") (Lean.addMacroScope mainModule `DoResultPRBC.return scp) [(`DoResultPRBC.return, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[val, u]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]])

source

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

Lean.Elab.Term.Do.ToTerm.M Lean.Syntax

Equations

Lean.Elab.Term.Do.ToTerm.continueToTerm = do let ctx ← read let u ← Lean.Elab.Term.Do.ToTerm.mkUVarTuple match ctx.kind with | Lean.Elab.Term.Do.ToTerm.Kind.regular => panicWithPosWithDecl "Lean.Elab.Do" "Lean.Elab.Term.Do.ToTerm.continueToTerm" 894 28 "unreachable code has been reached" | Lean.Elab.Term.Do.ToTerm.Kind.forIn => do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Pure.pure") (Lean.addMacroScope mainModule `Pure.pure scp) [(`Pure.pure, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "ForInStep.yield") (Lean.addMacroScope mainModule `ForInStep.yield scp) [(`ForInStep.yield, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[u]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]]) | Lean.Elab.Term.Do.ToTerm.Kind.forInWithReturn => do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Pure.pure") (Lean.addMacroScope mainModule `Pure.pure scp) [(`Pure.pure, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "ForInStep.yield") (Lean.addMacroScope mainModule `ForInStep.yield scp) [(`ForInStep.yield, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "MProd.mk") (Lean.addMacroScope mainModule `MProd.mk scp) [(`MProd.mk, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "none") (Lean.addMacroScope mainModule `none scp) [(`Option.none, [])], u]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]]) | Lean.Elab.Term.Do.ToTerm.Kind.nestedBC => do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Pure.pure") (Lean.addMacroScope mainModule `Pure.pure scp) [(`Pure.pure, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "DoResultBC.«continue»") (Lean.addMacroScope mainModule `DoResultBC.continue scp) [(`DoResultBC.continue, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[u]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]]) | Lean.Elab.Term.Do.ToTerm.Kind.nestedPR => panicWithPosWithDecl "Lean.Elab.Do" "Lean.Elab.Term.Do.ToTerm.continueToTerm" 898 28 "unreachable code has been reached" | Lean.Elab.Term.Do.ToTerm.Kind.nestedSBC => do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Pure.pure") (Lean.addMacroScope mainModule `Pure.pure scp) [(`Pure.pure, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "DoResultSBC.«continue»") (Lean.addMacroScope mainModule `DoResultSBC.continue scp) [(`DoResultSBC.continue, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[u]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]]) | Lean.Elab.Term.Do.ToTerm.Kind.nestedPRBC => do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Pure.pure") (Lean.addMacroScope mainModule `Pure.pure scp) [(`Pure.pure, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "DoResultPRBC.«continue»") (Lean.addMacroScope mainModule `DoResultPRBC.continue scp) [(`DoResultPRBC.continue, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[u]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]])

source

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

Lean.Elab.Term.Do.ToTerm.M Lean.Syntax

Equations

Lean.Elab.Term.Do.ToTerm.breakToTerm = do let ctx ← read let u ← Lean.Elab.Term.Do.ToTerm.mkUVarTuple match ctx.kind with | Lean.Elab.Term.Do.ToTerm.Kind.regular => panicWithPosWithDecl "Lean.Elab.Do" "Lean.Elab.Term.Do.ToTerm.breakToTerm" 906 28 "unreachable code has been reached" | Lean.Elab.Term.Do.ToTerm.Kind.forIn => do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Pure.pure") (Lean.addMacroScope mainModule `Pure.pure scp) [(`Pure.pure, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "ForInStep.done") (Lean.addMacroScope mainModule `ForInStep.done scp) [(`ForInStep.done, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[u]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]]) | Lean.Elab.Term.Do.ToTerm.Kind.forInWithReturn => do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Pure.pure") (Lean.addMacroScope mainModule `Pure.pure scp) [(`Pure.pure, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "ForInStep.done") (Lean.addMacroScope mainModule `ForInStep.done scp) [(`ForInStep.done, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "MProd.mk") (Lean.addMacroScope mainModule `MProd.mk scp) [(`MProd.mk, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "none") (Lean.addMacroScope mainModule `none scp) [(`Option.none, [])], u]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]]) | Lean.Elab.Term.Do.ToTerm.Kind.nestedBC => do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Pure.pure") (Lean.addMacroScope mainModule `Pure.pure scp) [(`Pure.pure, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "DoResultBC.«break»") (Lean.addMacroScope mainModule `DoResultBC.break scp) [(`DoResultBC.break, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[u]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]]) | Lean.Elab.Term.Do.ToTerm.Kind.nestedPR => panicWithPosWithDecl "Lean.Elab.Do" "Lean.Elab.Term.Do.ToTerm.breakToTerm" 910 28 "unreachable code has been reached" | Lean.Elab.Term.Do.ToTerm.Kind.nestedSBC => do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Pure.pure") (Lean.addMacroScope mainModule `Pure.pure scp) [(`Pure.pure, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "DoResultSBC.«break»") (Lean.addMacroScope mainModule `DoResultSBC.break scp) [(`DoResultSBC.break, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[u]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]]) | Lean.Elab.Term.Do.ToTerm.Kind.nestedPRBC => do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Pure.pure") (Lean.addMacroScope mainModule `Pure.pure scp) [(`Pure.pure, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "DoResultPRBC.«break»") (Lean.addMacroScope mainModule `DoResultPRBC.break scp) [(`DoResultPRBC.break, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[u]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]])

source

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

Lean.Elab.Term.Do.ToTerm.M Lean.Syntax

Equations

Lean.Elab.Term.Do.ToTerm.actionTerminalToTerm action = Lean.withRef action (Lean.withFreshMacroScope do let ctx ← read let u ← Lean.Elab.Term.Do.ToTerm.mkUVarTuple match ctx.kind with | Lean.Elab.Term.Do.ToTerm.Kind.regular => if Array.isEmpty ctx.uvars = true then pure action else do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Bind.bind") (Lean.addMacroScope mainModule `Bind.bind scp) [(`Bind.bind, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[action, Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.fun #[Lean.Syntax.atom info "fun", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.basicFun #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "y") (Lean.addMacroScope mainModule `y scp) []], Lean.Syntax.atom info "=>", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Pure.pure") (Lean.addMacroScope mainModule `Pure.pure scp) [(`Pure.pure, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "MProd.mk") (Lean.addMacroScope mainModule `MProd.mk scp) [(`MProd.mk, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "y") (Lean.addMacroScope mainModule `y scp) [], u]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]]]]]]) | Lean.Elab.Term.Do.ToTerm.Kind.forIn => do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Bind.bind") (Lean.addMacroScope mainModule `Bind.bind scp) [(`Bind.bind, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[action, Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.fun #[Lean.Syntax.atom info "fun", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.basicFun #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.hole #[Lean.Syntax.atom info "_"], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.typeAscription #[Lean.Syntax.atom info ":", Lean.Syntax.ident info (String.toSubstring "PUnit") (Lean.addMacroScope mainModule `PUnit scp) [(`PUnit, [])]]]], Lean.Syntax.atom info ")"]], Lean.Syntax.atom info "=>", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Pure.pure") (Lean.addMacroScope mainModule `Pure.pure scp) [(`Pure.pure, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "ForInStep.yield") (Lean.addMacroScope mainModule `ForInStep.yield scp) [(`ForInStep.yield, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[u]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]]]]]]) | Lean.Elab.Term.Do.ToTerm.Kind.forInWithReturn => do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Bind.bind") (Lean.addMacroScope mainModule `Bind.bind scp) [(`Bind.bind, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[action, Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.fun #[Lean.Syntax.atom info "fun", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.basicFun #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.hole #[Lean.Syntax.atom info "_"], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.typeAscription #[Lean.Syntax.atom info ":", Lean.Syntax.ident info (String.toSubstring "PUnit") (Lean.addMacroScope mainModule `PUnit scp) [(`PUnit, [])]]]], Lean.Syntax.atom info ")"]], Lean.Syntax.atom info "=>", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Pure.pure") (Lean.addMacroScope mainModule `Pure.pure scp) [(`Pure.pure, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "ForInStep.yield") (Lean.addMacroScope mainModule `ForInStep.yield scp) [(`ForInStep.yield, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "MProd.mk") (Lean.addMacroScope mainModule `MProd.mk scp) [(`MProd.mk, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "none") (Lean.addMacroScope mainModule `none scp) [(`Option.none, [])], u]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]]]]]]) | Lean.Elab.Term.Do.ToTerm.Kind.nestedBC => panicWithPosWithDecl "Lean.Elab.Do" "Lean.Elab.Term.Do.ToTerm.actionTerminalToTerm" 921 28 "unreachable code has been reached" | Lean.Elab.Term.Do.ToTerm.Kind.nestedPR => do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Bind.bind") (Lean.addMacroScope mainModule `Bind.bind scp) [(`Bind.bind, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[action, Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.fun #[Lean.Syntax.atom info "fun", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.basicFun #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "y") (Lean.addMacroScope mainModule `y scp) []], Lean.Syntax.atom info "=>", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Pure.pure") (Lean.addMacroScope mainModule `Pure.pure scp) [(`Pure.pure, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "DoResultPR.«pure»") (Lean.addMacroScope mainModule `DoResultPR.pure scp) [(`DoResultPR.pure, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "y") (Lean.addMacroScope mainModule `y scp) [], u]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]]]]) | Lean.Elab.Term.Do.ToTerm.Kind.nestedSBC => do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Bind.bind") (Lean.addMacroScope mainModule `Bind.bind scp) [(`Bind.bind, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[action, Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.fun #[Lean.Syntax.atom info "fun", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.basicFun #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "y") (Lean.addMacroScope mainModule `y scp) []], Lean.Syntax.atom info "=>", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Pure.pure") (Lean.addMacroScope mainModule `Pure.pure scp) [(`Pure.pure, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "DoResultSBC.«pureReturn»") (Lean.addMacroScope mainModule `DoResultSBC.pureReturn scp) [(`DoResultSBC.pureReturn, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "y") (Lean.addMacroScope mainModule `y scp) [], u]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]]]]) | Lean.Elab.Term.Do.ToTerm.Kind.nestedPRBC => do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Bind.bind") (Lean.addMacroScope mainModule `Bind.bind scp) [(`Bind.bind, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[action, Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.fun #[Lean.Syntax.atom info "fun", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.basicFun #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "y") (Lean.addMacroScope mainModule `y scp) []], Lean.Syntax.atom info "=>", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Pure.pure") (Lean.addMacroScope mainModule `Pure.pure scp) [(`Pure.pure, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "DoResultPRBC.«pure»") (Lean.addMacroScope mainModule `DoResultPRBC.pure scp) [(`DoResultPRBC.pure, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "y") (Lean.addMacroScope mainModule `y scp) [], u]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]]]]))

source

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

Lean.Elab.Term.Do.ToTerm.M Lean.Syntax

Equations

Lean.Elab.Term.Do.ToTerm.seqToTerm action k = Lean.withRef action (Lean.withFreshMacroScope (if (Lean.Syntax.getKind action == `Lean.Parser.Term.doDbgTrace) = true then let msg := Lean.Syntax.getOp action 1; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.dbgTrace #[Lean.Syntax.atom info "dbg_trace", msg, Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"], k]) else if (Lean.Syntax.getKind action == `Lean.Parser.Term.doAssert) = true then let cond := Lean.Syntax.getOp action 1; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.assert #[Lean.Syntax.atom info "assert!", cond, Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"], k]) else do let a ← read let action ← Lean.withRef action do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[action, Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.typeAscription #[Lean.Syntax.atom info ":", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[a.m, Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "PUnit") (Lean.addMacroScope mainModule `PUnit scp) [(`PUnit, [])]]]]]], Lean.Syntax.atom info ")"]) let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Bind.bind") (Lean.addMacroScope mainModule `Bind.bind scp) [(`Bind.bind, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[action, Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.fun #[Lean.Syntax.atom info "fun", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.basicFun #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.hole #[Lean.Syntax.atom info "_"], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.typeAscription #[Lean.Syntax.atom info ":", Lean.Syntax.ident info (String.toSubstring "PUnit") (Lean.addMacroScope mainModule `PUnit scp) [(`PUnit, [])]]]], Lean.Syntax.atom info ")"]], Lean.Syntax.atom info "=>", k]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]])))

source

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

Lean.Elab.Term.Do.ToTerm.M Lean.Syntax

Equations

Lean.Elab.Term.Do.ToTerm.declToTerm decl k = Lean.withRef decl (Lean.withFreshMacroScope (let kind := Lean.Syntax.getKind decl; if (kind == `Lean.Parser.Term.doLet) = true then let letDecl := Lean.Syntax.getOp decl 2; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.let #[Lean.Syntax.atom info "let", letDecl, Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"], k]) else if (kind == `Lean.Parser.Term.doLetRec) = true then let letRecToken := Lean.Syntax.getOp decl 0; let letRecDecls := Lean.Syntax.getOp decl 1; pure (Lean.mkNode `Lean.Parser.Term.letrec #[letRecToken, letRecDecls, Lean.mkNullNode, k]) else if (kind == `Lean.Parser.Term.doLetArrow) = true then let arg := Lean.Syntax.getOp decl 2; let ref := arg; if (Lean.Syntax.getKind arg == `Lean.Parser.Term.doIdDecl) = true then let id := Lean.Syntax.getOp arg 0; let type := Lean.Elab.Term.expandOptType id (Lean.Syntax.getOp arg 1); let doElem := Lean.Syntax.getOp arg 3; match Lean.Elab.Term.Do.isDoExpr? doElem with | some action => do let a ← read let action ← Lean.withRef action do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[action, Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.typeAscription #[Lean.Syntax.atom info ":", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[a.m, Lean.Syntax.node Lean.SourceInfo.none `null #[type]]]]], Lean.Syntax.atom info ")"]) let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "Bind.bind") (Lean.addMacroScope mainModule `Bind.bind scp) [(`Bind.bind, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[action, Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.fun #[Lean.Syntax.atom info "fun", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.basicFun #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[id, Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.typeAscription #[Lean.Syntax.atom info ":", type]]], Lean.Syntax.atom info ")"]], Lean.Syntax.atom info "=>", k]], Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"]]]) | none => liftM (Lean.Macro.throwErrorAt decl "unexpected kind of 'do' declaration") else liftM (Lean.Macro.throwErrorAt decl "unexpected kind of 'do' declaration") else if (kind == `Lean.Parser.Term.doHave) = true then let args := Lean.Syntax.getArgs decl; let args := args ++ #[Lean.mkNullNode, k]; pure (Lean.mkNode `Lean.Parser.Term.have args) else liftM (Lean.Macro.throwErrorAt decl "unexpected kind of 'do' declaration")))

source

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

Lean.MacroM Lean.Syntax

Equations

Lean.Elab.Term.Do.ToTerm.reassignToTerm reassign k = Lean.withRef reassign (Lean.withFreshMacroScope (let kind := Lean.Syntax.getKind reassign; if (kind == `Lean.Parser.Term.doReassign) = true then let arg := Lean.Syntax.getOp reassign 0; if (Lean.Syntax.getKind arg == `Lean.Parser.Term.letIdDecl) = true then let x := Lean.Syntax.getOp arg 0; let val := Lean.Syntax.getOp arg 4; do let newVal ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.ensureTypeOf #[Lean.Syntax.atom info "ensure_type_of%", x, Lean.quote "invalid reassignment, value", val]) let arg : Lean.Syntax := Lean.Syntax.setArg arg 4 newVal let letDecl : Lean.Syntax := Lean.mkNode `Lean.Parser.Term.letDecl #[arg] let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.let #[Lean.Syntax.atom info "let", letDecl, Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"], k]) else let letDecl := Lean.mkNode `Lean.Parser.Term.letDecl #[arg]; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.let #[Lean.Syntax.atom info "let", letDecl, Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"], k]) else Lean.Macro.throwErrorAt reassign "unexpected kind of 'do' reassignment"))

source

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

Lean.MacroM Lean.Syntax

Equations

Lean.Elab.Term.Do.ToTerm.mkIte optIdent cond thenBranch elseBranch = if Lean.Syntax.isNone optIdent = true then do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `termIfThenElse #[Lean.Syntax.atom info "if", cond, Lean.Syntax.atom info "then", thenBranch, Lean.Syntax.atom info "else", elseBranch]) else let h := Lean.Syntax.getOp optIdent 0; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `termDepIfThenElse #[Lean.Syntax.atom info "if", h, Lean.Syntax.atom info ":", cond, Lean.Syntax.atom info "then", thenBranch, Lean.Syntax.atom info "else", elseBranch])

source

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

Lean.Elab.Term.Do.ToTerm.M Lean.Syntax

Equations

Lean.Elab.Term.Do.ToTerm.mkJoinPoint j ps body k = Lean.withRef body (Lean.withFreshMacroScope do let pTypes ← Array.mapM (fun x => match x with | (id, useTypeOf) => if useTypeOf = true then do let a ← Lean.mkIdentFromRef id let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.typeOf #[Lean.Syntax.atom info "type_of%", a]) else do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.hole #[Lean.Syntax.atom info "_"])) ps let ps ← Array.mapM (fun x => match x with | (id, useTypeOf) => Lean.mkIdentFromRef id) ps let a ← Lean.mkIdentFromRef j let a_1 ← read let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.let_delayed #[Lean.Syntax.atom info "let_delayed", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letDecl #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letIdDecl #[a, Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (Array.map (fun x => match x with | (ps, pTypes) => Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.explicitBinder #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[ps], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ":", pTypes], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info ")"]) (Array.zip ps pTypes))), Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.typeSpec #[Lean.Syntax.atom info ":", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[a_1.m, Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.hole #[Lean.Syntax.atom info "_"]]]]], Lean.Syntax.atom info ":=", body]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"], k]))

source

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

Lean.Syntax

Equations

Lean.Elab.Term.Do.ToTerm.mkJmp ref j args = Lean.Syntax.mkApp (Lean.mkIdentFrom ref j) args

source

partial def Lean.Elab.Term.Do.ToTerm.toTerm :

Lean.Elab.Term.Do.Code → Lean.Elab.Term.Do.ToTerm.M Lean.Syntax

source

def Lean.Elab.Term.Do.ToTerm.run (code : Lean.Elab.Term.Do.Code) (m : Lean.Syntax) (uvars : optParam (Array Lean.Name) #[]) (kind : optParam Lean.Elab.Term.Do.ToTerm.Kind Lean.Elab.Term.Do.ToTerm.Kind.regular) :

Lean.MacroM Lean.Syntax

Equations

Lean.Elab.Term.Do.ToTerm.run code m uvars kind = do let term ← Lean.Elab.Term.Do.ToTerm.toTerm code { m := m, uvars := uvars, kind := kind } pure term

source

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

Lean.Elab.Term.Do.ToTerm.Kind

Equations

Lean.Elab.Term.Do.ToTerm.mkNestedKind a r bc = match a, r, bc with | true, false, false => Lean.Elab.Term.Do.ToTerm.Kind.regular | false, true, false => Lean.Elab.Term.Do.ToTerm.Kind.regular | false, false, true => Lean.Elab.Term.Do.ToTerm.Kind.nestedBC | true, true, false => Lean.Elab.Term.Do.ToTerm.Kind.nestedPR | true, false, true => Lean.Elab.Term.Do.ToTerm.Kind.nestedSBC | false, true, true => Lean.Elab.Term.Do.ToTerm.Kind.nestedSBC | true, true, true => Lean.Elab.Term.Do.ToTerm.Kind.nestedPRBC | false, false, false => panicWithPosWithDecl "Lean.Elab.Do" "Lean.Elab.Term.Do.ToTerm.mkNestedKind" 1068 27 "unreachable code has been reached"

source

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

Lean.MacroM Lean.Syntax

Equations

Lean.Elab.Term.Do.ToTerm.mkNestedTerm code m uvars a r bc = Lean.Elab.Term.Do.ToTerm.run code m uvars (Lean.Elab.Term.Do.ToTerm.mkNestedKind a r bc)

source

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

Lean.MacroM (List Lean.Syntax)

Equations

Lean.Elab.Term.Do.ToTerm.matchNestedTermResult term uvars a r bc = let toDoElems := fun auxDo => Lean.Elab.Term.getDoSeqElems (Lean.Elab.Term.getDoSeq auxDo); do let a ← Array.mapM Lean.mkIdentFromRef uvars let u ← Lean.Elab.Term.Do.mkTuple a match a, r, bc with | true, false, false => if Array.isEmpty uvars = true then do let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.do #[Lean.Syntax.atom info "do", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqIndent #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doExpr #[term], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]]) pure (toDoElems a) else do let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.do #[Lean.Syntax.atom info "do", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqIndent #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doLetArrow #[Lean.Syntax.atom info "let", Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doIdDecl #[Lean.Syntax.ident info (String.toSubstring "r") (Lean.addMacroScope mainModule `r scp) [], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info "←", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doExpr #[term]]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doReassign #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letPatDecl #[u, Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info ":=", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.proj #[Lean.Syntax.ident info (String.toSubstring "r") (Lean.addMacroScope mainModule `r scp) [], Lean.Syntax.atom info ".", Lean.Syntax.node Lean.SourceInfo.none `fieldIdx #[Lean.Syntax.atom info "2"]]]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doExpr #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "pure") (Lean.addMacroScope mainModule `pure scp) [(`Pure.pure, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.proj #[Lean.Syntax.ident info (String.toSubstring "r") (Lean.addMacroScope mainModule `r scp) [], Lean.Syntax.atom info ".", Lean.Syntax.node Lean.SourceInfo.none `fieldIdx #[Lean.Syntax.atom info "1"]]]]], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]]) pure (toDoElems a) | false, true, false => if Array.isEmpty uvars = true then do let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.do #[Lean.Syntax.atom info "do", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqIndent #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doLetArrow #[Lean.Syntax.atom info "let", Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doIdDecl #[Lean.Syntax.ident info (String.toSubstring "r") (Lean.addMacroScope mainModule `r scp) [], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info "←", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doExpr #[term]]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doReturn #[Lean.Syntax.atom info "return", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "r") (Lean.addMacroScope mainModule `r scp) []]], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]]) pure (toDoElems a) else do let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.do #[Lean.Syntax.atom info "do", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqIndent #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doLetArrow #[Lean.Syntax.atom info "let", Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doIdDecl #[Lean.Syntax.ident info (String.toSubstring "r") (Lean.addMacroScope mainModule `r scp) [], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info "←", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doExpr #[term]]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doReassign #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letPatDecl #[u, Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info ":=", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.proj #[Lean.Syntax.ident info (String.toSubstring "r") (Lean.addMacroScope mainModule `r scp) [], Lean.Syntax.atom info ".", Lean.Syntax.node Lean.SourceInfo.none `fieldIdx #[Lean.Syntax.atom info "2"]]]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doReturn #[Lean.Syntax.atom info "return", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.proj #[Lean.Syntax.ident info (String.toSubstring "r") (Lean.addMacroScope mainModule `r scp) [], Lean.Syntax.atom info ".", Lean.Syntax.node Lean.SourceInfo.none `fieldIdx #[Lean.Syntax.atom info "1"]]]], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]]) pure (toDoElems a) | false, false, true => toDoElems <$> do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.do #[Lean.Syntax.atom info "do", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqIndent #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doLetArrow #[Lean.Syntax.atom info "let", Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doIdDecl #[Lean.Syntax.ident info (String.toSubstring "r") (Lean.addMacroScope mainModule `r scp) [], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info "←", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doExpr #[term]]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doMatch #[Lean.Syntax.atom info "match", Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchDiscr #[Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.ident info (String.toSubstring "r") (Lean.addMacroScope mainModule `r scp) []]], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info "with", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlts #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlt #[Lean.Syntax.atom info "|", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "DoResultBC.«break»") (Lean.addMacroScope mainModule `DoResultBC.break scp) [(`DoResultBC.break, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "u") (Lean.addMacroScope mainModule `u scp) []]]], Lean.Syntax.atom info "=>", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqIndent #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doReassign #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letPatDecl #[u, Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info ":=", Lean.Syntax.ident info (String.toSubstring "u") (Lean.addMacroScope mainModule `u scp) []]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doBreak #[Lean.Syntax.atom info "break"], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlt #[Lean.Syntax.atom info "|", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "DoResultBC.«continue»") (Lean.addMacroScope mainModule `DoResultBC.continue scp) [(`DoResultBC.continue, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "u") (Lean.addMacroScope mainModule `u scp) []]]], Lean.Syntax.atom info "=>", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqIndent #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doReassign #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letPatDecl #[u, Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info ":=", Lean.Syntax.ident info (String.toSubstring "u") (Lean.addMacroScope mainModule `u scp) []]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doContinue #[Lean.Syntax.atom info "continue"], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]]]]], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]]) | true, true, false => toDoElems <$> do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.do #[Lean.Syntax.atom info "do", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqIndent #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doLetArrow #[Lean.Syntax.atom info "let", Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doIdDecl #[Lean.Syntax.ident info (String.toSubstring "r") (Lean.addMacroScope mainModule `r scp) [], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info "←", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doExpr #[term]]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doMatch #[Lean.Syntax.atom info "match", Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchDiscr #[Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.ident info (String.toSubstring "r") (Lean.addMacroScope mainModule `r scp) []]], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info "with", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlts #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlt #[Lean.Syntax.atom info "|", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "DoResultPR.«pure»") (Lean.addMacroScope mainModule `DoResultPR.pure scp) [(`DoResultPR.pure, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "a") (Lean.addMacroScope mainModule `a scp) [], Lean.Syntax.ident info (String.toSubstring "u") (Lean.addMacroScope mainModule `u scp) []]]], Lean.Syntax.atom info "=>", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqIndent #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doReassign #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letPatDecl #[u, Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info ":=", Lean.Syntax.ident info (String.toSubstring "u") (Lean.addMacroScope mainModule `u scp) []]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doExpr #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "pure") (Lean.addMacroScope mainModule `pure scp) [(`Pure.pure, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "a") (Lean.addMacroScope mainModule `a scp) []]]], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlt #[Lean.Syntax.atom info "|", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "DoResultPR.«return»") (Lean.addMacroScope mainModule `DoResultPR.return scp) [(`DoResultPR.return, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "b") (Lean.addMacroScope mainModule `b scp) [], Lean.Syntax.ident info (String.toSubstring "u") (Lean.addMacroScope mainModule `u scp) []]]], Lean.Syntax.atom info "=>", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqIndent #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doReassign #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letPatDecl #[u, Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info ":=", Lean.Syntax.ident info (String.toSubstring "u") (Lean.addMacroScope mainModule `u scp) []]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doReturn #[Lean.Syntax.atom info "return", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "b") (Lean.addMacroScope mainModule `b scp) []]], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]]]]], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]]) | true, false, true => toDoElems <$> do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.do #[Lean.Syntax.atom info "do", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqIndent #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doLetArrow #[Lean.Syntax.atom info "let", Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doIdDecl #[Lean.Syntax.ident info (String.toSubstring "r") (Lean.addMacroScope mainModule `r scp) [], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info "←", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doExpr #[term]]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doMatch #[Lean.Syntax.atom info "match", Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchDiscr #[Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.ident info (String.toSubstring "r") (Lean.addMacroScope mainModule `r scp) []]], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info "with", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlts #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlt #[Lean.Syntax.atom info "|", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "DoResultSBC.«pureReturn»") (Lean.addMacroScope mainModule `DoResultSBC.pureReturn scp) [(`DoResultSBC.pureReturn, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "a") (Lean.addMacroScope mainModule `a scp) [], Lean.Syntax.ident info (String.toSubstring "u") (Lean.addMacroScope mainModule `u scp) []]]], Lean.Syntax.atom info "=>", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqIndent #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doReassign #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letPatDecl #[u, Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info ":=", Lean.Syntax.ident info (String.toSubstring "u") (Lean.addMacroScope mainModule `u scp) []]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doExpr #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "pure") (Lean.addMacroScope mainModule `pure scp) [(`Pure.pure, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "a") (Lean.addMacroScope mainModule `a scp) []]]], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlt #[Lean.Syntax.atom info "|", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "DoResultSBC.«break»") (Lean.addMacroScope mainModule `DoResultSBC.break scp) [(`DoResultSBC.break, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "u") (Lean.addMacroScope mainModule `u scp) []]]], Lean.Syntax.atom info "=>", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqIndent #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doReassign #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letPatDecl #[u, Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info ":=", Lean.Syntax.ident info (String.toSubstring "u") (Lean.addMacroScope mainModule `u scp) []]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doBreak #[Lean.Syntax.atom info "break"], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlt #[Lean.Syntax.atom info "|", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "DoResultSBC.«continue»") (Lean.addMacroScope mainModule `DoResultSBC.continue scp) [(`DoResultSBC.continue, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "u") (Lean.addMacroScope mainModule `u scp) []]]], Lean.Syntax.atom info "=>", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqIndent #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doReassign #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letPatDecl #[u, Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info ":=", Lean.Syntax.ident info (String.toSubstring "u") (Lean.addMacroScope mainModule `u scp) []]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doContinue #[Lean.Syntax.atom info "continue"], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]]]]], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]]) | false, true, true => toDoElems <$> do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.do #[Lean.Syntax.atom info "do", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqIndent #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doLetArrow #[Lean.Syntax.atom info "let", Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doIdDecl #[Lean.Syntax.ident info (String.toSubstring "r") (Lean.addMacroScope mainModule `r scp) [], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info "←", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doExpr #[term]]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doMatch #[Lean.Syntax.atom info "match", Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchDiscr #[Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.ident info (String.toSubstring "r") (Lean.addMacroScope mainModule `r scp) []]], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info "with", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlts #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlt #[Lean.Syntax.atom info "|", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "DoResultSBC.«pureReturn»") (Lean.addMacroScope mainModule `DoResultSBC.pureReturn scp) [(`DoResultSBC.pureReturn, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "a") (Lean.addMacroScope mainModule `a scp) [], Lean.Syntax.ident info (String.toSubstring "u") (Lean.addMacroScope mainModule `u scp) []]]], Lean.Syntax.atom info "=>", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqIndent #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doReassign #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letPatDecl #[u, Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info ":=", Lean.Syntax.ident info (String.toSubstring "u") (Lean.addMacroScope mainModule `u scp) []]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doReturn #[Lean.Syntax.atom info "return", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "a") (Lean.addMacroScope mainModule `a scp) []]], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlt #[Lean.Syntax.atom info "|", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "DoResultSBC.«break»") (Lean.addMacroScope mainModule `DoResultSBC.break scp) [(`DoResultSBC.break, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "u") (Lean.addMacroScope mainModule `u scp) []]]], Lean.Syntax.atom info "=>", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqIndent #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doReassign #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letPatDecl #[u, Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info ":=", Lean.Syntax.ident info (String.toSubstring "u") (Lean.addMacroScope mainModule `u scp) []]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doBreak #[Lean.Syntax.atom info "break"], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlt #[Lean.Syntax.atom info "|", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "DoResultSBC.«continue»") (Lean.addMacroScope mainModule `DoResultSBC.continue scp) [(`DoResultSBC.continue, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "u") (Lean.addMacroScope mainModule `u scp) []]]], Lean.Syntax.atom info "=>", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqIndent #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doReassign #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letPatDecl #[u, Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info ":=", Lean.Syntax.ident info (String.toSubstring "u") (Lean.addMacroScope mainModule `u scp) []]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doContinue #[Lean.Syntax.atom info "continue"], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]]]]], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]]) | true, true, true => toDoElems <$> do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.do #[Lean.Syntax.atom info "do", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqIndent #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doLetArrow #[Lean.Syntax.atom info "let", Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doIdDecl #[Lean.Syntax.ident info (String.toSubstring "r") (Lean.addMacroScope mainModule `r scp) [], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info "←", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doExpr #[term]]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doMatch #[Lean.Syntax.atom info "match", Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchDiscr #[Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.ident info (String.toSubstring "r") (Lean.addMacroScope mainModule `r scp) []]], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info "with", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlts #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlt #[Lean.Syntax.atom info "|", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "DoResultPRBC.«pure»") (Lean.addMacroScope mainModule `DoResultPRBC.pure scp) [(`DoResultPRBC.pure, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "a") (Lean.addMacroScope mainModule `a scp) [], Lean.Syntax.ident info (String.toSubstring "u") (Lean.addMacroScope mainModule `u scp) []]]], Lean.Syntax.atom info "=>", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqIndent #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doReassign #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letPatDecl #[u, Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info ":=", Lean.Syntax.ident info (String.toSubstring "u") (Lean.addMacroScope mainModule `u scp) []]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doExpr #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "pure") (Lean.addMacroScope mainModule `pure scp) [(`Pure.pure, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "a") (Lean.addMacroScope mainModule `a scp) []]]], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlt #[Lean.Syntax.atom info "|", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "DoResultPRBC.«return»") (Lean.addMacroScope mainModule `DoResultPRBC.return scp) [(`DoResultPRBC.return, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "a") (Lean.addMacroScope mainModule `a scp) [], Lean.Syntax.ident info (String.toSubstring "u") (Lean.addMacroScope mainModule `u scp) []]]], Lean.Syntax.atom info "=>", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqIndent #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doReassign #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letPatDecl #[u, Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info ":=", Lean.Syntax.ident info (String.toSubstring "u") (Lean.addMacroScope mainModule `u scp) []]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doReturn #[Lean.Syntax.atom info "return", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "a") (Lean.addMacroScope mainModule `a scp) []]], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlt #[Lean.Syntax.atom info "|", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "DoResultPRBC.«break»") (Lean.addMacroScope mainModule `DoResultPRBC.break scp) [(`DoResultPRBC.break, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "u") (Lean.addMacroScope mainModule `u scp) []]]], Lean.Syntax.atom info "=>", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqIndent #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doReassign #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letPatDecl #[u, Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info ":=", Lean.Syntax.ident info (String.toSubstring "u") (Lean.addMacroScope mainModule `u scp) []]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doBreak #[Lean.Syntax.atom info "break"], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlt #[Lean.Syntax.atom info "|", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Lean.Syntax.ident info (String.toSubstring "DoResultPRBC.«continue»") (Lean.addMacroScope mainModule `DoResultPRBC.continue scp) [(`DoResultPRBC.continue, [])], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.ident info (String.toSubstring "u") (Lean.addMacroScope mainModule `u scp) []]]], Lean.Syntax.atom info "=>", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqIndent #[Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doReassign #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letPatDecl #[u, Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info ":=", Lean.Syntax.ident info (String.toSubstring "u") (Lean.addMacroScope mainModule `u scp) []]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"]], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doSeqItem #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.doContinue #[Lean.Syntax.atom info "continue"], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]]]]], Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]]) | false, false, false => panicWithPosWithDecl "Lean.Elab.Do" "Lean.Elab.Term.Do.ToTerm.matchNestedTermResult" 1124 27 "unreachable code has been reached"

source

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

Bool

Equations

Lean.Elab.Term.Do.isMutableLet doElem = let kind := Lean.Syntax.getKind doElem; (kind == `Lean.Parser.Term.doLetArrow || kind == `Lean.Parser.Term.doLet) && !Lean.Syntax.isNone (Lean.Syntax.getOp doElem 1)

source

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

Type

ref : Lean.Syntax
m : Lean.Syntax
mutableVars : Lean.NameSet
insideFor : Bool

source

@[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

source

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

Lean.Elab.Term.Do.ToCodeBlock.M α

Equations

Lean.Elab.Term.Do.ToCodeBlock.withNewMutableVars newVars mutable x = withReader (fun ctx => if mutable = true then { ref := ctx.ref, m := ctx.m, mutableVars := Lean.Elab.Term.Do.insertVars ctx.mutableVars newVars, insideFor := ctx.insideFor } else ctx) x

source

def Lean.Elab.Term.Do.ToCodeBlock.checkReassignable (xs : Array Lean.Name) :

Lean.Elab.Term.Do.ToCodeBlock.M Unit

Equations

Lean.Elab.Term.Do.ToCodeBlock.checkReassignable xs = let throwInvalidReassignment := fun x => Lean.throwError (Lean.toMessageData "'" ++ Lean.toMessageData (Lean.Name.simpMacroScopes x) ++ Lean.toMessageData "' cannot be reassigned"); do let ctx ← read let r ← forIn xs PUnit.unit fun x r => if Lean.NameSet.contains ctx.mutableVars x = true then do pure PUnit.unit pure (ForInStep.yield PUnit.unit) else do throwInvalidReassignment x pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure PUnit.unit

source

def Lean.Elab.Term.Do.ToCodeBlock.checkNotShadowingMutable (xs : Array Lean.Name) :

Lean.Elab.Term.Do.ToCodeBlock.M Unit

Equations

Lean.Elab.Term.Do.ToCodeBlock.checkNotShadowingMutable xs = let throwInvalidShadowing := fun x => Lean.throwError (Lean.toMessageData "mutable variable '" ++ Lean.toMessageData (Lean.Name.simpMacroScopes x) ++ Lean.toMessageData "' cannot be shadowed"); do let ctx ← read let r ← forIn xs PUnit.unit fun x r => if Lean.NameSet.contains ctx.mutableVars x = true then do throwInvalidShadowing x pure (ForInStep.yield PUnit.unit) else do pure PUnit.unit pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure PUnit.unit

source

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

Lean.Elab.Term.Do.ToCodeBlock.M α

Equations

Lean.Elab.Term.Do.ToCodeBlock.withFor x = withReader (fun ctx => { ref := ctx.ref, m := ctx.m, mutableVars := ctx.mutableVars, insideFor := true }) x

source

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

Type

uvars : Array Lean.Name
term : Lean.Syntax

source

def Lean.Elab.Term.Do.ToCodeBlock.mkForInBody (x : Lean.Syntax) (forInBody : Lean.Elab.Term.Do.CodeBlock) :

Lean.Elab.Term.Do.ToCodeBlock.M Lean.Elab.Term.Do.ToCodeBlock.ToForInTermResult

Equations

Lean.Elab.Term.Do.ToCodeBlock.mkForInBody x forInBody = do let ctx ← read let uvars : Lean.NameSet := forInBody.uvars let uvars : Array Lean.Name := Lean.Elab.Term.Do.nameSetToArray uvars let term ← Lean.Elab.liftMacroM (Lean.Elab.Term.Do.ToTerm.run forInBody.code ctx.m uvars (if Lean.Elab.Term.Do.hasReturn forInBody.code = true then Lean.Elab.Term.Do.ToTerm.Kind.forInWithReturn else Lean.Elab.Term.Do.ToTerm.Kind.forIn)) pure { uvars := uvars, term := term }

source

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

Lean.Elab.Term.Do.ToCodeBlock.M Unit

Equations

Lean.Elab.Term.Do.ToCodeBlock.ensureInsideFor = do let a ← read if a.insideFor = true then pure PUnit.unit else Lean.throwError (Lean.toMessageData "invalid 'do' element, it must be inside 'for'")

source

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

Lean.Elab.Term.Do.ToCodeBlock.M Unit

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

source

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

Lean.Elab.Term.Do.ToCodeBlock.M (List Lean.Syntax × Lean.Syntax)

Equations

Lean.Elab.Term.Do.ToCodeBlock.expandLiftMethod doElem = if (!Lean.Elab.Term.hasLiftMethod doElem) = true then pure ([], doElem) else do let discr ← StateT.run (Lean.Elab.Term.Do.ToCodeBlock.expandLiftMethodAux false false doElem) [] let x : Lean.Syntax × List Lean.Syntax := discr match x with | (doElem, doElemsNew) => pure (doElemsNew, doElem)

source

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

Lean.Elab.Term.Do.ToCodeBlock.M Unit

Equations

Lean.Elab.Term.Do.ToCodeBlock.checkLetArrowRHS doElem = let kind := Lean.Syntax.getKind doElem; if (kind == `Lean.Parser.Term.doLetArrow || kind == `Lean.Parser.Term.doLet || kind == `Lean.Parser.Term.doLetRec || kind == `Lean.Parser.Term.doHave || kind == `Lean.Parser.Term.doReassign || kind == `Lean.Parser.Term.doReassignArrow) = true then Lean.throwErrorAt doElem (Lean.toMessageData "invalid kind of value '" ++ Lean.toMessageData kind ++ Lean.toMessageData "' in an assignment") else pure PUnit.unit

source

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

Lean.Elab.Term.Do.ToCodeBlock.M Lean.Elab.Term.Do.CodeBlock

Equations

Lean.Elab.Term.Do.ToCodeBlock.doReturnToCode doReturn doElems = Lean.withRef doReturn do Lean.Elab.Term.Do.ToCodeBlock.ensureEOS doElems let argOpt : Lean.Syntax := Lean.Syntax.getOp doReturn 1 let _do_jp : Lean.Syntax → Lean.Elab.Term.Do.ToCodeBlock.M Lean.Elab.Term.Do.CodeBlock := fun arg => do let a ← Lean.getRef pure (Lean.Elab.Term.Do.mkReturn a arg) if Lean.Syntax.isNone argOpt = true then do let y ← Lean.Elab.liftMacroM Lean.Elab.Term.Do.mkUnit _do_jp y else do let y ← pure (Lean.Syntax.getOp argOpt 0) _do_jp y

source

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

Type

source

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

Lean.NameSet

Equations

Lean.Elab.Term.Do.ToCodeBlock.getTryCatchUpdatedVars tryCode catches finallyCode? = let ws := tryCode.uvars; let ws := Array.foldl (fun ws alt => Lean.Elab.Term.Do.union alt.codeBlock.uvars ws) ws catches 0 (Array.size catches); let ws := match finallyCode? with | none => ws | some c => Lean.Elab.Term.Do.union c.uvars ws; ws

source

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

Bool

Equations

Lean.Elab.Term.Do.ToCodeBlock.tryCatchPred tryCode catches finallyCode? p = (p tryCode.code || Array.any catches (fun catch => p catch.codeBlock.code) 0 (Array.size catches) || match finallyCode? with | none => false | some finallyCode => p finallyCode.code)