Lean.Widget.InteractiveGoal

structure Lean.Widget.InteractiveHypothesis :

Type

instance Lean.Widget.Lean.Widget.InteractiveHypothesis.instRpcEncodingInteractiveHypothesisRpcEncodingPacket :

Lean.Server.RpcEncoding Lean.Widget.InteractiveHypothesis Lean.Widget.Lean.Widget.InteractiveHypothesis.RpcEncodingPacket✝

Equations

Lean.Widget.Lean.Widget.InteractiveHypothesis.instRpcEncodingInteractiveHypothesisRpcEncodingPacket = { rpcEncode := fun {m} [Monad m] [Lean.Server.MonadRpcSession m] a => do let a_1 ← Lean.Server.rpcEncode a.names let a_2 ← Lean.Server.rpcEncode a.type let a_3 ← Lean.Server.rpcEncode a.val? let a_4 ← Lean.Server.rpcEncode a.isInstance let a ← Lean.Server.rpcEncode a.isType pure { names := a_1, type := a_2, val? := a_3, isInstance := a_4, isType := a }, rpcDecode := fun {m} [Monad m] [Lean.Server.MonadRpcSession m] a => do let a_1 ← Lean.Server.rpcDecode a.names let a_2 ← Lean.Server.rpcDecode a.type let a_3 ← Lean.Server.rpcDecode a.val? let a_4 ← Lean.Server.rpcDecode a.isInstance let a ← Lean.Server.rpcDecode a.isType pure { names := a_1, type := a_2, val? := a_3, isInstance := a_4, isType := a } }

source

instance Lean.Widget.Lean.Widget.InteractiveHypothesis.instToJsonRpcEncodingPacket :

Lean.ToJson Lean.Widget.Lean.Widget.InteractiveHypothesis.RpcEncodingPacket✝

Equations

Lean.Widget.Lean.Widget.InteractiveHypothesis.instToJsonRpcEncodingPacket = { toJson := [anonymous] }

source

instance Lean.Widget.instInhabitedInteractiveHypothesis :

Inhabited Lean.Widget.InteractiveHypothesis

Equations

Lean.Widget.instInhabitedInteractiveHypothesis = { default := { names := default, type := default, val? := default, isInstance := default, isType := default } }

source

instance Lean.Widget.Lean.Widget.InteractiveHypothesis.instFromJsonRpcEncodingPacket :

Lean.FromJson Lean.Widget.Lean.Widget.InteractiveHypothesis.RpcEncodingPacket✝

Equations

Lean.Widget.Lean.Widget.InteractiveHypothesis.instFromJsonRpcEncodingPacket = { fromJson? := [anonymous] }

source

structure Lean.Widget.InteractiveGoal :

Type

source

instance Lean.Widget.instInhabitedInteractiveGoal :

Inhabited Lean.Widget.InteractiveGoal

Equations

Lean.Widget.instInhabitedInteractiveGoal = { default := { hyps := default, type := default, userName? := default } }

source

instance Lean.Widget.Lean.Widget.InteractiveGoal.instRpcEncodingInteractiveGoalRpcEncodingPacket :

Lean.Server.RpcEncoding Lean.Widget.InteractiveGoal Lean.Widget.Lean.Widget.InteractiveGoal.RpcEncodingPacket✝

Equations

Lean.Widget.Lean.Widget.InteractiveGoal.instRpcEncodingInteractiveGoalRpcEncodingPacket = { rpcEncode := fun {m} [Monad m] [Lean.Server.MonadRpcSession m] a => do let a_1 ← Lean.Server.rpcEncode a.hyps let a_2 ← Lean.Server.rpcEncode a.type let a ← Lean.Server.rpcEncode a.userName? pure { hyps := a_1, type := a_2, userName? := a }, rpcDecode := fun {m} [Monad m] [Lean.Server.MonadRpcSession m] a => do let a_1 ← Lean.Server.rpcDecode a.hyps let a_2 ← Lean.Server.rpcDecode a.type let a ← Lean.Server.rpcDecode a.userName? pure { hyps := a_1, type := a_2, userName? := a } }

source

instance Lean.Widget.Lean.Widget.InteractiveGoal.instToJsonRpcEncodingPacket :

Lean.ToJson Lean.Widget.Lean.Widget.InteractiveGoal.RpcEncodingPacket✝

Equations

Lean.Widget.Lean.Widget.InteractiveGoal.instToJsonRpcEncodingPacket = { toJson := [anonymous] }

source

instance Lean.Widget.Lean.Widget.InteractiveGoal.instFromJsonRpcEncodingPacket :

Lean.FromJson Lean.Widget.Lean.Widget.InteractiveGoal.RpcEncodingPacket✝

Equations

Lean.Widget.Lean.Widget.InteractiveGoal.instFromJsonRpcEncodingPacket = { fromJson? := [anonymous] }

source

def Lean.Widget.InteractiveGoal.pretty (g : Lean.Widget.InteractiveGoal) :

Lean.Format

Equations

Lean.Widget.InteractiveGoal.pretty g = Id.run (let indent := 2; let ret := match g.userName? with | some userName => Lean.format "case " ++ Lean.format userName ++ Lean.format "" | none => Lean.Format.nil; do let r ← let col := g.hyps; forIn col ret fun hyp r => let ret := r; let ret := Lean.Widget.InteractiveGoal.addLine ret; let names := String.intercalate " " (Array.toList hyp.names); match hyp.val? with | some val => let ret := ret ++ Lean.Format.group (Lean.format "" ++ Lean.format names ++ Lean.format " : " ++ Lean.format (Lean.Widget.TaggedText.stripTags hyp.type) ++ Lean.format " :=" ++ Lean.format (Lean.Format.nest indent (Lean.Format.line ++ Std.Format.text (Lean.Widget.TaggedText.stripTags val))) ++ Lean.format ""); do pure PUnit.unit pure (ForInStep.yield ret) | none => let ret := ret ++ Lean.Format.group (Lean.format "" ++ Lean.format names ++ Lean.format " :" ++ Lean.format (Lean.Format.nest indent (Lean.Format.line ++ Std.Format.text (Lean.Widget.TaggedText.stripTags hyp.type))) ++ Lean.format ""); do pure PUnit.unit pure (ForInStep.yield ret) let x : Lean.Format := r let ret : Lean.Format := x let ret : Lean.Format := Lean.Widget.InteractiveGoal.addLine ret ret ++ (Lean.format "⊢ " ++ Lean.format (Lean.Format.nest indent (Std.Format.text (Lean.Widget.TaggedText.stripTags g.type))) ++ Lean.format ""))

source

structure Lean.Widget.InteractiveTermGoal :

Type

source

instance Lean.Widget.instInhabitedInteractiveTermGoal :

Inhabited Lean.Widget.InteractiveTermGoal

Equations

Lean.Widget.instInhabitedInteractiveTermGoal = { default := { hyps := default, type := default, range := default } }

source

instance Lean.Widget.Lean.Widget.InteractiveTermGoal.instRpcEncodingInteractiveTermGoalRpcEncodingPacket :

Lean.Server.RpcEncoding Lean.Widget.InteractiveTermGoal Lean.Widget.Lean.Widget.InteractiveTermGoal.RpcEncodingPacket✝

Equations

Lean.Widget.Lean.Widget.InteractiveTermGoal.instRpcEncodingInteractiveTermGoalRpcEncodingPacket = { rpcEncode := fun {m} [Monad m] [Lean.Server.MonadRpcSession m] a => do let a_1 ← Lean.Server.rpcEncode a.hyps let a_2 ← Lean.Server.rpcEncode a.type let a ← Lean.Server.rpcEncode a.range pure { hyps := a_1, type := a_2, range := a }, rpcDecode := fun {m} [Monad m] [Lean.Server.MonadRpcSession m] a => do let a_1 ← Lean.Server.rpcDecode a.hyps let a_2 ← Lean.Server.rpcDecode a.type let a ← Lean.Server.rpcDecode a.range pure { hyps := a_1, type := a_2, range := a } }

source

instance Lean.Widget.Lean.Widget.InteractiveTermGoal.instFromJsonRpcEncodingPacket :

Lean.FromJson Lean.Widget.Lean.Widget.InteractiveTermGoal.RpcEncodingPacket✝

Equations

Lean.Widget.Lean.Widget.InteractiveTermGoal.instFromJsonRpcEncodingPacket = { fromJson? := [anonymous] }

source

instance Lean.Widget.Lean.Widget.InteractiveTermGoal.instToJsonRpcEncodingPacket :

Lean.ToJson Lean.Widget.Lean.Widget.InteractiveTermGoal.RpcEncodingPacket✝

Equations

Lean.Widget.Lean.Widget.InteractiveTermGoal.instToJsonRpcEncodingPacket = { toJson := [anonymous] }

source

def Lean.Widget.InteractiveTermGoal.toInteractiveGoal (g : Lean.Widget.InteractiveTermGoal) :

Lean.Widget.InteractiveGoal

Equations

Lean.Widget.InteractiveTermGoal.toInteractiveGoal g = { hyps := g.hyps, type := g.type, userName? := none }

source

structure Lean.Widget.InteractiveGoals :

Type

source

instance Lean.Widget.Lean.Widget.InteractiveGoals.instToJsonRpcEncodingPacket :

Lean.ToJson Lean.Widget.Lean.Widget.InteractiveGoals.RpcEncodingPacket✝

Equations

Lean.Widget.Lean.Widget.InteractiveGoals.instToJsonRpcEncodingPacket = { toJson := [anonymous] }

source

instance Lean.Widget.Lean.Widget.InteractiveGoals.instRpcEncodingInteractiveGoalsRpcEncodingPacket :

Lean.Server.RpcEncoding Lean.Widget.InteractiveGoals Lean.Widget.Lean.Widget.InteractiveGoals.RpcEncodingPacket✝

Equations

Lean.Widget.Lean.Widget.InteractiveGoals.instRpcEncodingInteractiveGoalsRpcEncodingPacket = { rpcEncode := fun {m} [Monad m] [Lean.Server.MonadRpcSession m] a => do let a ← Lean.Server.rpcEncode a.goals pure { goals := a }, rpcDecode := fun {m} [Monad m] [Lean.Server.MonadRpcSession m] a => do let a ← Lean.Server.rpcDecode a.goals pure { goals := a } }

source

instance Lean.Widget.Lean.Widget.InteractiveGoals.instFromJsonRpcEncodingPacket :

Lean.FromJson Lean.Widget.Lean.Widget.InteractiveGoals.RpcEncodingPacket✝

Equations

Lean.Widget.Lean.Widget.InteractiveGoals.instFromJsonRpcEncodingPacket = { fromJson? := [anonymous] }

source

def Lean.Widget.addInteractiveHypothesis (hyps : Array Lean.Widget.InteractiveHypothesis) (ids : Array Lean.Name) (type : Lean.Expr) (value? : optParam (Option Lean.Expr) none) :

Lean.MetaM (Array Lean.Widget.InteractiveHypothesis)

Equations

Lean.Widget.addInteractiveHypothesis hyps ids type value? = do let a ← Lean.Widget.exprToInteractive type let a_1 ← Option.mapM Lean.Widget.exprToInteractive value? let a_2 ← Lean.Meta.isClass? type let a_3 ← Lean.Meta.instantiateMVars type pure (Array.push hyps { names := Array.map toString ids, type := a, val? := a_1, isInstance := Option.isSome a_2, isType := Lean.Expr.isSort a_3 })

source

def Lean.Widget.goalToInteractive (mvarId : Lean.MVarId) :

Lean.MetaM Lean.Widget.InteractiveGoal

Equations

Lean.Widget.goalToInteractive mvarId = do let a ← Lean.getMCtx let discr ← pure (Lean.MetavarContext.findDecl? a mvarId) match discr with | some mvarDecl => do let a ← Lean.getOptions let ppAuxDecls : Bool := Lean.Option.get a Lean.Meta.pp.auxDecls let lctx : Lean.LocalContext := mvarDecl.lctx let a ← Lean.getOptions let lctx : Id Lean.LocalContext := StateT.run' (Lean.LocalContext.sanitizeNames lctx) { options := a, nameStem2Idx := ∅, userName2Sanitized := ∅ } Lean.Meta.withLCtx lctx mvarDecl.localInstances do let discr ← Lean.Meta.ToHide.collect mvarDecl.type let x : Lean.FVarIdSet × Lean.FVarIdSet := discr match x with | (hidden, hiddenProp) => (fun pushPending => (fun ppVars => do let discr ← Lean.LocalContext.foldlM lctx (fun x localDecl => match x with | (varNames, prevType?, hyps) => if (!ppAuxDecls && Lean.LocalDecl.isAuxDecl localDecl || Std.RBTree.contains hidden (Lean.LocalDecl.fvarId localDecl)) = true then pure (varNames, prevType?, hyps) else ppVars varNames prevType? hyps localDecl) (#[], none, #[]) let x : Array Lean.Name × Option Lean.Expr × Array Lean.Widget.InteractiveHypothesis := discr match x with | (varNames, type?, hyps) => do let hyps ← pushPending varNames type? hyps let goalTp ← Lean.Meta.instantiateMVars mvarDecl.type let goalFmt ← Lean.Widget.exprToInteractive goalTp let userName? : Option String := match mvarDecl.userName with | Lean.Name.anonymous => none | name => some (toString (Lean.Name.eraseMacroScopes name)) pure { hyps := hyps, type := goalFmt, userName? := userName? }) (Lean.Widget.goalToInteractive.ppVars hiddenProp)) Lean.Widget.goalToInteractive.pushPending | x => Lean.throwError (Lean.toMessageData "unknown goal " ++ Lean.toMessageData mvarId.name ++ Lean.toMessageData "")

source

def Lean.Widget.goalToInteractive.pushPending (ids : Array Lean.Name) (type? : Option Lean.Expr) (hyps : Array Lean.Widget.InteractiveHypothesis) :

Lean.MetaM (Array Lean.Widget.InteractiveHypothesis)

Equations

Lean.Widget.goalToInteractive.pushPending ids type? hyps = if Array.isEmpty ids = true then pure hyps else match ids, type? with | x, none => pure hyps | x, some type => Lean.Widget.addInteractiveHypothesis hyps ids type none

source

def Lean.Widget.goalToInteractive.ppVars (hiddenProp : Lean.FVarIdSet) (varNames : Array Lean.Name) (prevType? : Option Lean.Expr) (hyps : Array Lean.Widget.InteractiveHypothesis) (localDecl : Lean.LocalDecl) :

Lean.MetaM (Array Lean.Name × Option Lean.Expr × Array Lean.Widget.InteractiveHypothesis)

Equations

Lean.Widget.goalToInteractive.ppVars hiddenProp varNames prevType? hyps localDecl = if Std.RBTree.contains hiddenProp (Lean.LocalDecl.fvarId localDecl) = true then do let hyps ← Lean.Widget.goalToInteractive.pushPending varNames prevType? hyps let type ← Lean.Meta.instantiateMVars (Lean.LocalDecl.type localDecl) let hyps ← Lean.Widget.addInteractiveHypothesis hyps #[] type none pure (#[], none, hyps) else match localDecl with | Lean.LocalDecl.cdecl x x_1 varName type x_2 => let varName := Lean.Name.simpMacroScopes varName; do let type ← Lean.Meta.instantiateMVars type if (prevType? == none || prevType? == some type) = true then pure (Array.push varNames varName, some type, hyps) else do let hyps ← Lean.Widget.goalToInteractive.pushPending varNames prevType? hyps pure (#[varName], some type, hyps) | Lean.LocalDecl.ldecl x x_1 varName type val x_2 => let varName := Lean.Name.simpMacroScopes varName; do let hyps ← Lean.Widget.goalToInteractive.pushPending varNames prevType? hyps let type ← Lean.Meta.instantiateMVars type let val ← Lean.Meta.instantiateMVars val let hyps ← Lean.Widget.addInteractiveHypothesis hyps #[varName] type (some val) pure (#[], none, hyps)