From 65ac0d5c5821bd4a5e65a7d7ff57eee9ba690249 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 31 Mar 2024 15:55:08 -0700 Subject: [PATCH] feat: Specify type in echo --- Pantograph.lean | 2 +- Pantograph/Environment.lean | 6 +++--- Pantograph/Library.lean | 25 +++++++++++++++++++------ Pantograph/Protocol.lean | 1 + Pantograph/Serial.lean | 9 ++++----- Test/Metavar.lean | 8 ++++---- Test/Proofs.lean | 4 ++-- Test/Serial.lean | 8 ++++---- 8 files changed, 38 insertions(+), 25 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index bcf8395..075a7f6 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -71,7 +71,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do Environment.addDecl args expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do let state ← get - exprEcho args.expr state.options + exprEcho args.expr args.type state.options options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do let state ← get let options := state.options diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean index 19c3249..f00e857 100644 --- a/Pantograph/Environment.lean +++ b/Pantograph/Environment.lean @@ -98,13 +98,13 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr def addDecl (args: Protocol.EnvAdd): CoreM (Protocol.CR Protocol.EnvAddResult) := do let env ← Lean.MonadEnv.getEnv let tvM: Elab.TermElabM (Except String (Expr × Expr)) := do - let type ← match syntax_from_str env args.type with + let type ← match parseTerm env args.type with | .ok syn => do - match ← syntax_to_expr syn with + match ← elabTerm syn with | .error e => return .error e | .ok expr => pure expr | .error e => return .error e - let value ← match syntax_from_str env args.value with + let value ← match parseTerm env args.value with | .ok syn => do try let expr ← Elab.Term.elabTerm (stx := syn) (expectedType? := .some type) diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index f44fcad..d2bc8a0 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -109,21 +109,34 @@ def envAdd (name: String) (type: String) (value: String) (isTheorem: Bool): Lean.CoreM (Protocol.CR Protocol.EnvAddResult) := Environment.addDecl { name, type, value, isTheorem } -/-- This must be a TermElabM since the parsed expr contains extra information -/ -def exprParse (s: String): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do +def typeParse (typeParse: String): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do let env ← Lean.MonadEnv.getEnv - let syn ← match syntax_from_str env s with + let syn ← match parseTerm env typeParse with | .error str => return .error $ errorI "parsing" str | .ok syn => pure syn - match ← syntax_to_expr syn with + match ← elabType syn with + | .error str => return .error $ errorI "elab" str + | .ok expr => return .ok expr + +/-- This must be a TermElabM since the parsed expr contains extra information -/ +def exprParse (exprStr: String) (expectedType?: Option String := .none): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do + let env ← Lean.MonadEnv.getEnv + let expectedType? ← match ← expectedType?.mapM typeParse with + | .none => pure $ .none + | .some (.ok t) => pure $ .some t + | .some (.error e) => return .error e + let syn ← match parseTerm env exprStr with + | .error str => return .error $ errorI "parsing" str + | .ok syn => pure syn + match ← elabTerm syn expectedType? with | .error str => return .error $ errorI "elab" str | .ok expr => return .ok expr @[export pantograph_expr_echo_m] -def exprEcho (expr: String) (options: @&Protocol.Options): +def exprEcho (expr: String) (expectedType?: Option String := .none) (options: @&Protocol.Options): Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) := do let termElabM: Lean.Elab.TermElabM _ := do - let expr ← match ← exprParse expr with + let expr ← match ← exprParse expr expectedType? with | .error e => return .error e | .ok expr => pure expr try diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index cd42ab8..7a2b341 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -98,6 +98,7 @@ structure StatResult where -- Return the type of an expression structure ExprEcho where expr: String + type: Option String deriving Lean.FromJson structure ExprEchoResult where expr: Expression diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index f829611..2eb09c6 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -25,23 +25,22 @@ def instantiateAll (e: Lean.Expr) : Lean.MetaM Lean.Expr := do --- Input Functions --- /-- Read syntax object from string -/ -def syntax_from_str (env: Environment) (s: String): Except String Syntax := +def parseTerm (env: Environment) (s: String): Except String Syntax := Parser.runParserCategory (env := env) (catName := `term) (input := s) (fileName := "") - /-- Parse a syntax object. May generate additional metavariables! -/ -def syntax_to_expr_type (syn: Syntax): Elab.TermElabM (Except String Expr) := do +def elabType (syn: Syntax): Elab.TermElabM (Except String Expr) := do try let expr ← Elab.Term.elabType syn return .ok expr catch ex => return .error (← ex.toMessageData.toString) -def syntax_to_expr (syn: Syntax): Elab.TermElabM (Except String Expr) := do +def elabTerm (syn: Syntax) (expectedType? : Option Expr := .none): Elab.TermElabM (Except String Expr) := do try - let expr ← Elab.Term.elabTerm (stx := syn) (expectedType? := .none) + let expr ← Elab.Term.elabTerm (stx := syn) expectedType? return .ok expr catch ex => return .error (← ex.toMessageData.toString) diff --git a/Test/Metavar.lean b/Test/Metavar.lean index 9820dde..9595b35 100644 --- a/Test/Metavar.lean +++ b/Test/Metavar.lean @@ -17,12 +17,12 @@ def addTest (test: LSpec.TestSeq): TestM Unit := do def test_instantiate_mvar: TestM Unit := do let env ← Lean.MonadEnv.getEnv let value := "@Nat.le_trans 2 2 5 (@of_eq_true (@LE.le Nat instLENat 2 2) (@eq_true (@LE.le Nat instLENat 2 2) (@Nat.le_refl 2))) (@of_eq_true (@LE.le Nat instLENat 2 5) (@eq_true_of_decide (@LE.le Nat instLENat 2 5) (@Nat.decLe 2 5) (@Eq.refl Bool Bool.true)))" - let syn ← match syntax_from_str env value with + let syn ← match parseTerm env value with | .ok s => pure $ s | .error e => do addTest $ assertUnreachable e return () - let expr ← match ← syntax_to_expr syn with + let expr ← match ← elabTerm syn with | .ok expr => pure $ expr | .error e => do addTest $ assertUnreachable e @@ -36,14 +36,14 @@ def test_instantiate_mvar: TestM Unit := do def startProof (expr: String): TestM (Option GoalState) := do let env ← Lean.MonadEnv.getEnv - let syn? := syntax_from_str env expr + let syn? := parseTerm env expr addTest $ LSpec.check s!"Parsing {expr}" (syn?.isOk) match syn? with | .error error => IO.println error return Option.none | .ok syn => - let expr? ← syntax_to_expr_type syn + let expr? ← elabType syn addTest $ LSpec.check s!"Elaborating" expr?.isOk match expr? with | .error error => diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 833c02e..133eee0 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -32,14 +32,14 @@ def startProof (start: Start): TestM (Option GoalState) := do | .none => return Option.none | .expr expr => - let syn? := syntax_from_str env expr + let syn? := parseTerm env expr addTest $ LSpec.check s!"Parsing {expr}" (syn?.isOk) match syn? with | .error error => IO.println error return Option.none | .ok syn => - let expr? ← syntax_to_expr_type syn + let expr? ← elabType syn addTest $ LSpec.check s!"Elaborating" expr?.isOk match expr? with | .error error => diff --git a/Test/Serial.lean b/Test/Serial.lean index c2810c8..f186bbb 100644 --- a/Test/Serial.lean +++ b/Test/Serial.lean @@ -55,8 +55,8 @@ def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do ] let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (source, target) => do let env ← MonadEnv.getEnv - let s := syntax_from_str env source |>.toOption |>.get! - let expr := (← syntax_to_expr s) |>.toOption |>.get! + let s := parseTerm env source |>.toOption |>.get! + let expr := (← elabTerm s) |>.toOption |>.get! let test := LSpec.check source ((← serialize_expression_ast expr) = target) return LSpec.TestSeq.append suites test) LSpec.TestSeq.done let metaM := termElabM.run' (ctx := defaultTermElabMContext) @@ -67,8 +67,8 @@ def test_instance (env: Environment): IO LSpec.TestSeq := do let metaM: MetaM LSpec.TestSeq := do let env ← MonadEnv.getEnv let source := "λ x y: Nat => HAdd.hAdd Nat Nat Nat (instHAdd Nat instAddNat) x y" - let s := syntax_from_str env source |>.toOption |>.get! - let _expr := (← runTermElabMInMeta <| syntax_to_expr s) |>.toOption |>.get! + let s := parseTerm env source |>.toOption |>.get! + let _expr := (← runTermElabMInMeta <| elabTerm s) |>.toOption |>.get! return LSpec.TestSeq.done runMetaMSeq env metaM