Equations
- Lean.Elab.Command.elabModuleDoc stx = match Lean.Syntax.getOp stx 1 with | Lean.Syntax.atom x val => let doc := String.extract val 0 (String.bsize val - 2); Lean.modifyEnv fun env => Lean.addMainModuleDoc env doc | x => Lean.throwErrorAt stx (Lean.toMessageData "unexpected module doc string" ++ Lean.toMessageData (Lean.indentD (Lean.MessageData.ofSyntax (Lean.Syntax.getOp stx 1))) ++ Lean.toMessageData "")
def
Lean.Elab.Command.withNamespace
{α : Type}
(ns : Lean.Name)
(elabFn : Lean.Elab.Command.CommandElabM α)
:
Equations
- Lean.Elab.Command.withNamespace ns elabFn = do Lean.Elab.Command.addNamespace ns let a ← elabFn modify fun s => { env := s.env, messages := s.messages, scopes := List.drop (Lean.Name.getNumParts ns) s.scopes, nextMacroScope := s.nextMacroScope, maxRecDepth := s.maxRecDepth, nextInstIdx := s.nextInstIdx, ngen := s.ngen, infoState := s.infoState, traceState := s.traceState } pure a
Equations
- Lean.Elab.Command.elabNamespace stx = let discr := stx; if Lean.Syntax.isOfKind discr `Lean.Parser.Command.namespace = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr 1; let n := discr; Lean.Elab.Command.addNamespace (Lean.Syntax.getId n) else let discr := stx; Lean.Elab.throwUnsupportedSyntax
Equations
- Lean.Elab.Command.elabSection stx = let discr := stx; if Lean.Syntax.isOfKind discr `Lean.Parser.Command.section = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; if Lean.Syntax.matchesNull discr_2 1 = true then let discr := Lean.Syntax.getArg discr_2 0; cond (Lean.Syntax.isOfKind discr `ident) (let header := discr; Lean.Elab.Command.addScopes false false (Lean.Syntax.getId header)) (let discr := Lean.Syntax.getArg discr_2 0; Lean.Elab.throwUnsupportedSyntax) else let discr_3 := Lean.Syntax.getArg discr 1; if Lean.Syntax.matchesNull discr_3 0 = true then do let a ← Lean.getCurrNamespace Lean.Elab.Command.addScope false false "" a else let discr := Lean.Syntax.getArg discr 1; Lean.Elab.throwUnsupportedSyntax else let discr := stx; Lean.Elab.throwUnsupportedSyntax
Equations
- Lean.Elab.Command.elabEnd stx = let header? := Lean.Syntax.getOptionalIdent? (Lean.Syntax.getArg stx 1); let endSize := match header? with | none => 1 | some n => Lean.Name.getNumParts n; do let scopes ← Lean.Elab.Command.getScopes let _do_jp : Unit → Lean.Elab.Command.CommandElabM Unit := fun y => match header? with | none => if Lean.Elab.Command.checkAnonymousScope scopes = true then pure PUnit.unit else Lean.throwError (Lean.toMessageData "invalid 'end', name is missing") | some header => if Lean.Elab.Command.checkEndHeader header scopes = true then pure PUnit.unit else do Lean.Elab.addCompletionInfo (Lean.Elab.CompletionInfo.endSection stx (List.map (fun scope => scope.header) scopes)) Lean.throwError (Lean.toMessageData "invalid 'end', name mismatch") if endSize < List.length scopes then do modify fun s => { env := s.env, messages := s.messages, scopes := List.drop endSize s.scopes, nextMacroScope := s.nextMacroScope, maxRecDepth := s.maxRecDepth, nextInstIdx := s.nextInstIdx, ngen := s.ngen, infoState := s.infoState, traceState := s.traceState } let y ← Lean.Elab.Command.popScopes endSize _do_jp y else do let a ← get let n : Nat := List.length a.scopes - 1 modify fun s => { env := s.env, messages := s.messages, scopes := List.drop n s.scopes, nextMacroScope := s.nextMacroScope, maxRecDepth := s.maxRecDepth, nextInstIdx := s.nextInstIdx, ngen := s.ngen, infoState := s.infoState, traceState := s.traceState } Lean.Elab.Command.popScopes n let y ← Lean.throwError (Lean.toMessageData "invalid 'end', insufficient scopes") _do_jp y
Equations
- Lean.Elab.Command.elabNonComputableSection stx = let discr := stx; if Lean.Syntax.isOfKind discr `Lean.Parser.Command.noncomputableSection = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; let discr_3 := Lean.Syntax.getArg discr 2; if Lean.Syntax.matchesNull discr_3 1 = true then let discr := Lean.Syntax.getArg discr_3 0; cond (Lean.Syntax.isOfKind discr `ident) (let header := discr; Lean.Elab.Command.addScopes false true (Lean.Syntax.getId header)) (let discr := Lean.Syntax.getArg discr_3 0; Lean.Elab.throwUnsupportedSyntax) else let discr_4 := Lean.Syntax.getArg discr 2; if Lean.Syntax.matchesNull discr_4 0 = true then do let a ← Lean.getCurrNamespace Lean.Elab.Command.addScope false true "" a else let discr := Lean.Syntax.getArg discr 2; Lean.Elab.throwUnsupportedSyntax else let discr := stx; Lean.Elab.throwUnsupportedSyntax
Equations
- Lean.Elab.Command.elabInitQuot stx = do let a ← Lean.getEnv match Lean.Environment.addDecl a Lean.Declaration.quotDecl with | Except.ok env => Lean.setEnv env | Except.error ex => do let a ← Lean.getOptions Lean.throwError (Lean.KernelException.toMessageData ex a)
Equations
- Lean.Elab.Command.elabExport stx = let id := Lean.Syntax.getId (Lean.Syntax.getOp stx 1); do let ns ← Lean.resolveNamespace id let currNamespace ← Lean.getCurrNamespace let _do_jp : PUnit → Lean.Elab.Command.CommandElabM Unit := fun y => do let _ ← Lean.getEnv let ids : Array Lean.Syntax := Lean.Syntax.getArgs (Lean.Syntax.getOp stx 3) let aliases ← Array.foldlM (fun aliases idStx => let id := Lean.Syntax.getId idStx; do let declName ← Lean.Elab.resolveOpenDeclId ns idStx pure ((currNamespace ++ id, declName) :: aliases)) [] ids 0 (Array.size ids) modify fun s => { env := List.foldl (fun env p => Lean.addAlias env p.fst p.snd) s.env aliases, messages := s.messages, scopes := s.scopes, nextMacroScope := s.nextMacroScope, maxRecDepth := s.maxRecDepth, nextInstIdx := s.nextInstIdx, ngen := s.ngen, infoState := s.infoState, traceState := s.traceState } if (ns == currNamespace) = true then do let y ← Lean.throwError (Lean.toMessageData "invalid 'export', self export") _do_jp y else do let y ← pure PUnit.unit _do_jp y
Equations
- Lean.Elab.Command.elabOpen n = do let openDecls ← Lean.Elab.elabOpenDecl (Lean.Syntax.getOp n 1) Lean.Elab.Command.modifyScope fun scope => { header := scope.header, opts := scope.opts, currNamespace := scope.currNamespace, openDecls := openDecls, levelNames := scope.levelNames, varDecls := scope.varDecls, varUIds := scope.varUIds, isNoncomputable := scope.isNoncomputable }
Equations
- Lean.Elab.Command.elabVariable x = let discr := x; if Lean.Syntax.isOfKind discr `Lean.Parser.Command.variable = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr 1; let binders := Lean.Syntax.getArgs discr; do Lean.Elab.Command.runTermElabM none fun x => Lean.Elab.Term.withAutoBoundImplicit (Lean.Elab.Term.elabBinders binders fun x => pure ()) let r ← forIn binders PUnit.unit fun binder r => do let a ← Lean.Elab.Command.replaceBinderAnnotation binder if a = true then do pure PUnit.unit pure (ForInStep.yield PUnit.unit) else do let varUIds ← Array.mapM (Lean.withFreshMacroScope ∘ Lean.MonadQuotation.addMacroScope) (Lean.Elab.Command.getBracketedBinderIds binder) Lean.Elab.Command.modifyScope fun scope => { header := scope.header, opts := scope.opts, currNamespace := scope.currNamespace, openDecls := scope.openDecls, levelNames := scope.levelNames, varDecls := Array.push scope.varDecls binder, varUIds := scope.varUIds ++ varUIds, isNoncomputable := scope.isNoncomputable } pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure PUnit.unit else let discr := x; Lean.Elab.throwUnsupportedSyntax
Equations
- Lean.Elab.Command.elabCheckCore ignoreStuckTC x = let discr := x; if Lean.Syntax.isOfKind discr `Lean.Parser.Command.check = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr 1; let term := discr; let tk := discr_1; Lean.withoutModifyingEnv (Lean.Elab.Command.runTermElabM (some `_check) fun x => do let e ← Lean.Elab.Term.elabTerm term none true true Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing ignoreStuckTC let a ← liftM (Lean.Meta.instantiateMVars e) let discr ← Lean.Elab.Term.levelMVarToParam a 1 let x : Lean.Expr × Nat := discr match x with | (e, x) => do let type ← liftM (Lean.Meta.inferType e) if Lean.Expr.isSyntheticSorry e = true then pure PUnit.unit else Lean.Elab.logInfoAt tk (Lean.toMessageData "" ++ Lean.toMessageData e ++ Lean.toMessageData " : " ++ Lean.toMessageData type ++ Lean.toMessageData "")) else let discr := x; Lean.Elab.throwUnsupportedSyntax
Equations
- Lean.Elab.Command.elabReduce x = let discr := x; if Lean.Syntax.isOfKind discr `Lean.Parser.Command.reduce = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr 1; let term := discr; let tk := discr_1; Lean.withoutModifyingEnv (Lean.Elab.Command.runTermElabM (some `_check) fun x => do let e ← Lean.Elab.Term.elabTerm term none true true Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing false let a ← liftM (Lean.Meta.instantiateMVars e) let discr ← Lean.Elab.Term.levelMVarToParam a 1 let x : Lean.Expr × Nat := discr match x with | (e, x) => withTheReader Lean.Core.Context (fun ctx => { options := Lean.KVMap.setBool ctx.options `smartUnfolding false, currRecDepth := ctx.currRecDepth, maxRecDepth := ctx.maxRecDepth, ref := ctx.ref, currNamespace := ctx.currNamespace, openDecls := ctx.openDecls, initHeartbeats := ctx.initHeartbeats, maxHeartbeats := ctx.maxHeartbeats }) do let e ← Lean.Meta.withTransparency Lean.Meta.TransparencyMode.all (liftM (Lean.Meta.reduce e true false false)) Lean.Elab.logInfoAt tk (Lean.MessageData.ofExpr e)) else let discr := x; Lean.Elab.throwUnsupportedSyntax
Equations
- Lean.Elab.Command.hasNoErrorMessages = do let a ← get pure !Lean.MessageLog.hasErrors a.messages
Equations
- Lean.Elab.Command.failIfSucceeds x = let resetMessages := do let s ← get let messages : Lean.MessageLog := s.messages modify fun s => { env := s.env, messages := { msgs := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } }, scopes := s.scopes, nextMacroScope := s.nextMacroScope, maxRecDepth := s.maxRecDepth, nextInstIdx := s.nextInstIdx, ngen := s.ngen, infoState := s.infoState, traceState := s.traceState } pure messages; let restoreMessages := fun prevMessages => modify fun s => { env := s.env, messages := prevMessages ++ Lean.MessageLog.errorsToWarnings s.messages, scopes := s.scopes, nextMacroScope := s.nextMacroScope, maxRecDepth := s.maxRecDepth, nextInstIdx := s.nextInstIdx, ngen := s.ngen, infoState := s.infoState, traceState := s.traceState }; do let prevMessages ← resetMessages let _do_jp : Bool → Lean.Elab.Command.CommandElabM Unit := fun succeeded => if succeeded = true then Lean.throwError (Lean.toMessageData "unexpected success") else pure PUnit.unit let y ← tryFinally (tryCatch (do x Lean.Elab.Command.hasNoErrorMessages) fun ex => match ex with | ex@h:(Lean.Exception.error x x_1) => do Lean.Elab.logException ex pure false | Lean.Exception.internal id x => do let a ← liftM (Lean.InternalExceptionId.getName id) Lean.Elab.logError (Lean.MessageData.ofName a) pure false) (restoreMessages prevMessages) _do_jp y
Equations
- Lean.Elab.Command.elabCheckFailure x = let discr := x; if Lean.Syntax.isOfKind discr `Lean.Parser.Command.check_failure = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr 1; let term := discr; do let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.check #[Lean.Syntax.atom info "#check", term]) Lean.Elab.Command.failIfSucceeds (Lean.Elab.Command.elabCheckCore false a) else let discr := x; Lean.Elab.throwUnsupportedSyntax
Equations
- Lean.Elab.Command.elabEvalUnsafe x = let discr := x; if Lean.Syntax.isOfKind discr `Lean.Parser.Command.eval = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr 1; let term := discr; let tk := discr_1; let n := `_eval; do let _ ← read let addAndCompile : Lean.Expr → Lean.Elab.TermElabM Unit := fun value => do let a ← liftM (Lean.Meta.instantiateMVars value) let discr ← Lean.Elab.Term.levelMVarToParam a 1 let x : Lean.Expr × Nat := discr match x with | (value, x) => do let type ← liftM (Lean.Meta.inferType value) let us : Array Lean.Name := (Lean.collectLevelParams { visitedLevel := ∅, visitedExpr := ∅, params := #[] } value).params let value ← liftM (Lean.Meta.instantiateMVars value) let decl : Lean.Declaration := Lean.Declaration.defnDecl { toConstantVal := { name := n, levelParams := Array.toList us, type := type }, value := value, hints := Lean.ReducibilityHints.opaque, safety := Lean.DefinitionSafety.unsafe } Lean.Elab.Term.ensureNoUnassignedMVars decl Lean.addAndCompile decl let elabEvalTerm : Lean.Elab.TermElabM Lean.Expr := do let e ← Lean.Elab.Term.elabTerm term none true true Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing false let a ← liftM (Lean.Meta.isProp e) if a = true then liftM (Lean.Meta.mkDecide e) else pure e let elabMetaEval : Lean.Elab.Command.CommandElabM Unit := Lean.Elab.Command.runTermElabM (some n) fun x => do let a ← elabEvalTerm let e ← liftM (Lean.Elab.Command.mkRunMetaEval a) let env ← Lean.getEnv let opts ← Lean.getOptions let _do_jp : (Lean.Environment → Lean.Options → IO (String × Except IO.Error Lean.Environment)) → Lean.Elab.TermElabM Unit := fun act => do let discr ← liftM (act env opts) let x : String × Except IO.Error Lean.Environment := discr match x with | (out, res) => do Lean.Elab.logInfoAt tk (Function.comp Lean.MessageData.ofFormat Lean.format out) match res with | Except.error e => Lean.throwError (Function.comp Lean.MessageData.ofFormat Lean.format (IO.Error.toString e)) | Except.ok env => do Lean.setEnv env pure () let y ← tryFinally (do addAndCompile e Lean.evalConst (Lean.Environment → Lean.Options → IO (String × Except IO.Error Lean.Environment)) n) (Lean.setEnv env) _do_jp y let elabEval : Lean.Elab.Command.CommandElabM Unit := Lean.Elab.Command.runTermElabM (some n) fun x => do let a ← elabEvalTerm let e ← liftM (Lean.Elab.Command.mkRunEval a) let env ← Lean.getEnv let _do_jp : IO (String × Except IO.Error Unit) → Lean.Elab.TermElabM Unit := fun act => do let discr ← liftM act let x : String × Except IO.Error Unit := discr match x with | (out, res) => do Lean.Elab.logInfoAt tk (Function.comp Lean.MessageData.ofFormat Lean.format out) match res with | Except.error e => Lean.throwError (Function.comp Lean.MessageData.ofFormat Lean.format (IO.Error.toString e)) | Except.ok x => pure () let y ← tryFinally (do addAndCompile e Lean.evalConst (IO (String × Except IO.Error Unit)) n) (Lean.setEnv env) _do_jp y let a ← Lean.getEnv if Lean.Environment.contains a `Lean.MetaEval = true then elabMetaEval else elabEval else let discr := x; Lean.Elab.throwUnsupportedSyntax
@[implementedBy Lean.Elab.Command.elabEvalUnsafe]
Equations
- Lean.Elab.Command.elabSynth stx = let term := Lean.Syntax.getOp stx 1; Lean.withoutModifyingEnv (Lean.Elab.Command.runTermElabM (some `_synth_cmd) fun x => do let inst ← Lean.Elab.Term.elabTerm term none true true Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing false let inst ← liftM (Lean.Meta.instantiateMVars inst) let val ← liftM (Lean.Meta.synthInstance inst none) Lean.Elab.logInfo (Lean.MessageData.ofExpr val) pure ())
Equations
- Lean.Elab.Command.elabSetOption stx = do let options ← Lean.Elab.elabSetOption (Lean.Syntax.getOp stx 1) (Lean.Syntax.getOp stx 2) modify fun s => { env := s.env, messages := s.messages, scopes := s.scopes, nextMacroScope := s.nextMacroScope, maxRecDepth := Lean.Option.get options Lean.maxRecDepth, nextInstIdx := s.nextInstIdx, ngen := s.ngen, infoState := s.infoState, traceState := s.traceState } Lean.Elab.Command.modifyScope fun scope => { header := scope.header, opts := options, currNamespace := scope.currNamespace, openDecls := scope.openDecls, levelNames := scope.levelNames, varDecls := scope.varDecls, varUIds := scope.varUIds, isNoncomputable := scope.isNoncomputable }
Equations
- Lean.Elab.Command.expandInCmd stx = let cmd₁ := Lean.Syntax.getOp stx 0; let cmd₂ := Lean.Syntax.getOp stx 2; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.section #[Lean.Syntax.atom info "section", Lean.Syntax.node Lean.SourceInfo.none `null #[]], cmd₁, cmd₂, Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.end #[Lean.Syntax.atom info "end", Lean.Syntax.node Lean.SourceInfo.none `null #[]]])