Add expr.type

This commit is contained in:
Leni Aniva 2023-05-25 13:40:03 -07:00
parent e0c5f76451
commit 068a188fea
2 changed files with 25 additions and 0 deletions

View File

@ -46,6 +46,10 @@ def execute (command: Command): Subroutine Lean.Json := do
match Lean.fromJson? command.payload with
| .ok args => inspect args
| .error x => return errorJson x
| "expr.type" =>
match Lean.fromJson? command.payload with
| .ok args => expr_type args
| .error x => return errorJson x
| "proof.start" =>
match Lean.fromJson? command.payload with
| .ok args => proof_start args
@ -90,6 +94,19 @@ def execute (command: Command): Subroutine Lean.Json := do
boundExpr? := boundExpr?,
module? := module?
}: InspectResult)
expr_type (args: ExprType): Subroutine Lean.Json := do
let env ← Lean.MonadEnv.getEnv
match syntax_from_str env args.expr with
| .error str => return errorI "parsing" str
| .ok syn => do
match (← syntax_to_expr syn) with
| .error str => return errorI "elab" str
| .ok expr => do
try
let format ← Lean.Meta.ppExpr (← Lean.Meta.inferType expr)
return Lean.toJson <| ({ type := toString format }: ExprTypeResult)
catch exception =>
return errorI "typing" (← exception.toMessageData.toString)
proof_start (args: ProofStart): Subroutine Lean.Json := do
let state ← get
let env ← Lean.MonadEnv.getEnv

View File

@ -42,6 +42,14 @@ structure InspectResult where
module?: Option String
deriving Lean.ToJson
-- Get the type of an expression
structure ExprType where
expr: String
deriving Lean.FromJson
structure ExprTypeResult where
type: String
deriving Lean.ToJson
structure ProofStart where
name: Option String -- Identifier of the proof
-- Only one of the fields below may be populated.