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

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)

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 typeParse (typeParse: String): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do
-def exprParse (s: 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

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

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 := "<stdin>")
 
-
 /-- 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)
 

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 =>

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 =>

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 s := parseTerm env source |>.toOption |>.get!
-    let expr := (← syntax_to_expr s) |>.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 s := parseTerm env source |>.toOption |>.get!
-    let _expr := (← runTermElabMInMeta <| syntax_to_expr s) |>.toOption |>.get!
+    let _expr := (← runTermElabMInMeta <| elabTerm s) |>.toOption |>.get!
     return LSpec.TestSeq.done
   runMetaMSeq env metaM