checkParse 関数の定義を洗練させる

LeanByExample/Reference/Declarative/Infix.lean

@@ -32,17 +32,16 @@ section
 
 open Lean Parser
 
-/-- parse できるかどうかチェックする関数 -/
-def checkParse (cat : Name) (s : String) : MetaM Unit := do
-  if let .error s := runParserCategory (← getEnv) cat s then
-    throwError s
+/-- `s : String` をパースして `Syntax` の項を得る。`cat` は構文カテゴリ。-/
+def parse (cat : Name) (s : String) : MetaM Syntax := do
+  ofExcept <| runParserCategory (← getEnv) cat s
 
 -- 単に連結するとパース不可でエラーになる
 /-- error: <input>:1:6: expected end of input -/
-#guard_msgs in run_meta checkParse `term "1 ⋄ 2 ⋄ 3"
+#guard_msgs in run_meta parse `term "1 ⋄ 2 ⋄ 3"
 
 -- 括弧を付ければOK
-run_meta checkParse `term "1 ⋄ (2 ⋄ 3)"
+run_meta parse `term "1 ⋄ (2 ⋄ 3)"
 
 end
 /- ## 舞台裏

LeanByExample/Reference/Declarative/Local.lean

@@ -58,10 +58,9 @@ end hoge
 
 open Lean Parser in
 
-/-- parse できるかどうかチェックする関数 -/
-def checkParse (cat : Name) (s : String) : MetaM Unit := do
-  if let .error s := runParserCategory (← getEnv) cat s then
-    throwError s
+/-- `s : String` をパースして `Syntax` の項を得る。`cat` は構文カテゴリ。-/
+def parse (cat : Name) (s : String) : MetaM Syntax := do
+  ofExcept <| runParserCategory (← getEnv) cat s
 
 -- `def` は有効範囲を制限できないのでエラーになる
 /--
@@ -70,7 +69,7 @@ error: <input>:1:6: expected 'binder_predicate', 'builtin_dsimproc', 'builtin_si
 'notation', 'postfix', 'prefix', 'simproc', 'syntax' or 'unif_hint'
 -/
 #guard_msgs in
-  run_meta checkParse `command "local def"
+  run_meta parse `command "local def"
 
 /-
 数が多いためすべての例を挙げることはしませんが、いくつか紹介します。たとえば `instance` の場合、`local` を付けて登録したインスタンスがその `section` の内部限定になります。

LeanByExample/Reference/Declarative/Macro.lean

@@ -7,15 +7,14 @@ namespace Macro --#
 
 open Lean Parser
 
-/-- 構文が認識されるかどうかチェックする関数 -/
-def checkParse (cat : Name) (s : String) : MetaM Unit := do
-  if let .error s := runParserCategory (← getEnv) cat s then
-    throwError s
+/-- `s : String` をパースして `Syntax` の項を得る。`cat` は構文カテゴリ。-/
+def parse (cat : Name) (s : String) : MetaM Syntax := do
+  ofExcept <| runParserCategory (← getEnv) cat s
 
 -- 最初は `#greet` が未定義なので、合法的なLeanのコマンドとして認識されない
 /-- error: <input>:1:0: expected command -/
 #guard_msgs in
-  run_meta checkParse `command "#greet"
+  run_meta parse `command "#greet"
 
 -- `#greet` コマンドを定義する
 scoped macro "#greet " : command => `(#eval "Hello World!")

LeanByExample/Reference/Declarative/Scoped.lean

@@ -50,10 +50,9 @@ end
 
 open Lean Parser
 
-/-- parse できるかどうかチェックする関数 -/
-def checkParse (cat : Name) (s : String) : MetaM Unit := do
-  if let .error s := runParserCategory (← getEnv) cat s then
-    throwError s
+/-- `s : String` をパースして `Syntax` の項を得る。`cat` は構文カテゴリ。-/
+def parse (cat : Name) (s : String) : MetaM Syntax := do
+  ofExcept <| runParserCategory (← getEnv) cat s
 
 -- `def` は有効範囲を制限できないのでエラーになる
 /--
@@ -63,7 +62,7 @@ error: <input>:1:7: expected 'binder_predicate', 'builtin_dsimproc', 'builtin_si
 'syntax' or 'unif_hint'
 -/
 #guard_msgs in
-  run_meta checkParse `command "scoped def"
+  run_meta parse `command "scoped def"
 
 /- ## open scoped
 `open scoped` コマンドを利用すると、特定の名前空間にある `scoped` が付けられた名前だけを有効にすることができます。単に [`open`](./Open.md) コマンドを利用するとその名前空間にあるすべての名前が有効になります。

LeanByExample/Reference/Declarative/Syntax.lean

@@ -6,16 +6,15 @@ import Lean
 
 open Lean Parser
 
-/-- parse できるかどうかチェックする関数 -/
-def checkParse (cat : Name) (s : String) : MetaM Unit := do
-  if let .error s := runParserCategory (← getEnv) cat s then
-    throwError s
+/-- `s : String` をパースして `Syntax` の項を得る。`cat` は構文カテゴリ。-/
+def parse (cat : Name) (s : String) : MetaM Syntax := do
+  ofExcept <| runParserCategory (← getEnv) cat s
 
 -- 最初は `#greet` などというコマンドは定義されていないので
 -- そもそも Lean の合法な構文として認められない。
 /-- error: <input>:1:0: expected command -/
 #guard_msgs (error) in
-  #eval checkParse `command "#greet"
+  #eval parse `command "#greet"
 
 -- `#greet` というコマンドのための構文を定義
 syntax "#greet" : command

LeanByExample/Reference/Tactic/Dsimp.lean

@@ -151,15 +151,14 @@ example : True ∨ (s ∩ u = u ∩ s) := by
 
 open Lean Parser
 
-/-- parse できるかどうかチェックする関数 -/
-def checkParse (cat : Name) (s : String) : MetaM Unit := do
-  if let .error s := runParserCategory (← getEnv) cat s then
-    throwError s
+/-- `s : String` をパースして `Syntax` の項を得る。`cat` は構文カテゴリ。-/
+def parse (cat : Name) (s : String) : MetaM Syntax := do
+  ofExcept <| runParserCategory (← getEnv) cat s
 
 -- 識別子を渡したときはパースできる
-run_meta checkParse `tactic "unfold Inter.inter"
+run_meta parse `tactic "unfold Inter.inter"
 
 -- 識別子でないものを渡すとパースできない
 /-- error: <input>:1:7: expected identifier -/
 #guard_msgs in
-  run_meta checkParse `tactic "unfold (· ∩ ·)"
+  run_meta parse `tactic "unfold (· ∩ ·)"