@[inline]
Equations
- Lean.IR.Sorry.visitExpr x = (fun getSorryDepFor? => match x with | Lean.IR.Expr.fap f x => getSorryDepFor? f | Lean.IR.Expr.pap f x => getSorryDepFor? f | x => pure ()) Lean.IR.Sorry.visitExpr.getSorryDepFor?
Equations
- Lean.IR.Sorry.visitExpr.getSorryDepFor? f = let found := fun g => if (g == `sorryAx) = true then throw f else throw g; if (f == `sorryAx) = true then throw f else do let a ← get match Lean.NameMap.find? a.localSorryMap f with | some g => found g | x => do let a ← liftM (Lean.IR.findDecl f) match a with | some (Lean.IR.Decl.fdecl x x_1 x_2 x_3 { sorryDep? := some g }) => found g | x => pure ()
Equations
- Lean.IR.Sorry.visitDecl d = match d with | Lean.IR.Decl.fdecl f x x_1 b x_2 => do let a ← get match Lean.NameMap.find? a.localSorryMap f with | some x => pure () | none => do let a ← ExceptT.run (Lean.IR.Sorry.visitFndBody b) match a with | Except.ok x => pure () | Except.error g => modify fun s => { localSorryMap := Lean.NameMap.insert s.localSorryMap f g, modified := true } | x => pure ()
Equations
- Lean.IR.updateSorryDep decls = do let discr ← StateT.run (Lean.IR.Sorry.collect decls) { localSorryMap := ∅, modified := false } let x : Unit × Lean.IR.Sorry.State := discr match x with | (x, s) => pure (Array.map (fun decl => match decl with | Lean.IR.Decl.fdecl f xs t b info => match Lean.NameMap.find? s.localSorryMap f with | some g => Lean.IR.Decl.fdecl f xs t b { sorryDep? := some g } | x => decl | x => decl) decls)