Merge pull request #2 from siddhartha-gadgil/cleanup

feat: general cleanup

Author: siddhartha-gadgil

LeanSearchClient/Basic.lean

@@ -1,4 +1,4 @@
-import Lean
+import Lean.Data.Options
 
 register_option leansearch.queries : Nat :=
   { defValue := 6

LeanSearchClient/Examples.lean

@@ -3,29 +3,37 @@ Copyright (c) 2024 Siddhartha Gadgil. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Siddhartha Gadgil
 -/
-import Lean
+import Lean.Elab.Tactic.Meta
+import Lean.Meta.Tactic.TryThis
 import LeanSearchClient.Basic
 
 /-!
 # LeanSearchClient
 
-In this file, we provide syntax for search using the [leansearch API](https://leansearch.net/) from within Lean. It allows you to search for Lean tactics and theorems using natural language.
+In this file, we provide syntax for search using the [leansearch API](https://leansearch.net/)
+from within Lean. It allows you to search for Lean tactics and theorems using natural language.
 
-We provide syntax to make a query and generate `TryThis` options to click or use a code action to use the results. The queries are of three forms:
+We provide syntax to make a query and generate `TryThis` options to click or
+use a code action to use the results.
+
+The queries are of three forms:
 
 * `Command` syntax: `#leansearch "search query"` as a command.
 * `Term` syntax: `#leansearch "search query"` as a term.
 * `Tactic` syntax: `#leansearch "search query"` as a tactic.
 
-In all cases results are displayed in the Lean Infoview and clicking these replaces the query text. In the cases of a query for tactics only valid tactics are displayed.
+In all cases results are displayed in the Lean Infoview and clicking these replaces the query text.
+In the cases of a query for tactics only valid tactics are displayed.
 -/
 
+namespace LeanSearchClient
+
 open Lean Meta Elab Tactic Parser Term
 
-def getQueryJson (s: String)(num_results : Nat := 6) : IO <| Array Json := do
+def getQueryJson (s : String) (num_results : Nat := 6) : IO <| Array Json := do
   let apiUrl := "https://leansearch.net/api/search"
   let s' := s.replace " " "%20"
-  let q := apiUrl++ s!"?query={s'}&num_results={num_results}"
+  let q := apiUrl ++ s!"?query={s'}&num_results={num_results}"
   let s ← IO.Process.output {cmd := "curl", args := #["-X", "GET", q]}
   let js := Json.parse s.stdout |>.toOption |>.get!
   return js.getArr? |>.toOption |>.get!
@@ -42,8 +50,7 @@ def queryNum : CoreM Nat := do
 
 namespace SearchResult
 
-
-def ofJson? (js: Json) : Option SearchResult :=
+def ofJson? (js : Json) : Option SearchResult :=
   match js.getObjValAs? String "formal_name" with
   | Except.ok name =>
       let type? := js.getObjValAs? String "formal_type" |>.toOption
@@ -54,7 +61,7 @@ def ofJson? (js: Json) : Option SearchResult :=
       some {name := name, type? := type?, docString? := doc?, doc_url? := docurl?, kind? := kind?}
   | _ => none
 
-def query (s: String)(num_results : Nat) :
+def query (s : String) (num_results : Nat) :
     IO <| Array SearchResult := do
   let jsArr ← getQueryJson s num_results
   return jsArr.filterMap ofJson?
@@ -65,12 +72,12 @@ def toCommandSuggestion (sr : SearchResult) : TryThis.Suggestion :=
     | none => ""
   {suggestion := s!"#check {sr.name}", postInfo? := sr.type?.map fun s => s!" -- {s}" ++ s!"\n{data}"}
 
-def toTermSuggestion (sr: SearchResult) : TryThis.Suggestion :=
+def toTermSuggestion (sr : SearchResult) : TryThis.Suggestion :=
   match sr.type? with
   | some type => {suggestion := sr.name, postInfo? := some s!" (type: {type})"}
   | none => {suggestion := sr.name}
 
-def toTacticSuggestions (sr: SearchResult) : Array TryThis.Suggestion :=
+def toTacticSuggestions (sr : SearchResult) : Array TryThis.Suggestion :=
   match sr.type? with
   | some type => #[{suggestion := s!"apply {sr.name}"},
         {suggestion := s!"have : {type} := {sr.name}"},
@@ -80,24 +87,24 @@ def toTacticSuggestions (sr: SearchResult) : Array TryThis.Suggestion :=
 
 end SearchResult
 
-def getQueryCommandSuggestions (s: String)(num_results : Nat) :
-  IO <| Array TryThis.Suggestion := do
-    let searchResults ←  SearchResult.query s num_results
-    return searchResults.map SearchResult.toCommandSuggestion
-
-def getQueryTermSuggestions (s: String)(num_results : Nat) :
-  IO <| Array TryThis.Suggestion := do
-    let searchResults ←  SearchResult.query s num_results
-    return searchResults.map SearchResult.toTermSuggestion
-
-def getQueryTacticSuggestionGroups (s: String)(num_results : Nat) :
-  IO <| Array (String ×  Array TryThis.Suggestion) := do
-    let searchResults ←  SearchResult.query s num_results
-    return searchResults.map fun sr =>
-      let fullName := match sr.type? with
-        | some type => s!"{sr.name} (type: {type})"
-        | none => sr.name
-      (fullName, sr.toTacticSuggestions)
+def getQueryCommandSuggestions (s : String) (num_results : Nat) :
+    IO <| Array TryThis.Suggestion := do
+  let searchResults ←  SearchResult.query s num_results
+  return searchResults.map SearchResult.toCommandSuggestion
+
+def getQueryTermSuggestions (s : String) (num_results : Nat) :
+    IO <| Array TryThis.Suggestion := do
+  let searchResults ←  SearchResult.query s num_results
+  return searchResults.map SearchResult.toTermSuggestion
+
+def getQueryTacticSuggestionGroups (s : String) (num_results : Nat) :
+    IO <| Array (String ×  Array TryThis.Suggestion) := do
+  let searchResults ←  SearchResult.query s num_results
+  return searchResults.map fun sr =>
+    let fullName := match sr.type? with
+      | some type => s!"{sr.name} (type: {type})"
+      | none => sr.name
+    (fullName, sr.toTacticSuggestions)
 
 def defaultTerm (expectedType? : Option Expr) : MetaM Expr := do
   match expectedType? with
@@ -108,48 +115,56 @@ def defaultTerm (expectedType? : Option Expr) : MetaM Expr := do
       return mkConst ``True.intro
   | none => return mkConst ``True.intro
 
-def checkTactic (target: Expr)(tac: Syntax):
-  TermElabM (Option Nat) :=
-    withoutModifyingState do
-    try
-      let goal ← mkFreshExprMVar target
-      let (goals, _) ←
-        withoutErrToSorry do
-        Elab.runTactic goal.mvarId! tac
-          (← read) (← get)
-      return some goals.length
-    catch _ =>
-      return none
+def checkTactic (target : Expr) (tac : Syntax) :
+    TermElabM (Option Nat) :=
+  withoutModifyingState do
+  try
+    let goal ← mkFreshExprMVar target
+    let (goals, _) ←
+      withoutErrToSorry do
+      Elab.runTactic goal.mvarId! tac
+        (← read) (← get)
+    return some goals.length
+  catch _ =>
+    return none
+
+def incompleteQuery : String :=
+  "#leansearch query should end with a `.` or `?`.\n\
+   Note this command sends your query to an external service at https://leansearch.net/."
 
 open Command
+
 syntax (name := leansearch_cmd) "#leansearch" str : command
-@[command_elab leansearch_cmd] def leanSearchImpl : CommandElab :=
+
+@[command_elab leansearch_cmd] def leanSearchCommandImpl : CommandElab :=
   fun stx => Command.liftTermElabM do
   match stx with
   | `(command| #leansearch $s) =>
     let s := s.getString
     if s.endsWith "." || s.endsWith "?" then
       let suggestions ← getQueryCommandSuggestions s (← queryNum)
-      TryThis.addSuggestions stx suggestions (header:= "Lean Search Results")
+      TryThis.addSuggestions stx suggestions (header := "Lean Search Results")
     else
-      logWarning "Lean search query should end with a full stop (period) or a question mark. Note this command sends your query to an external service at https://leansearch.net/."
+      logWarning incompleteQuery
   | _ => throwUnsupportedSyntax
 
 syntax (name := leansearch_term) "#leansearch" str : term
+
 @[term_elab leansearch_term] def leanSearchTermImpl : TermElab :=
   fun stx expectedType? => do
   match stx with
   | `(#leansearch $s) =>
     let s := s.getString
     if s.endsWith "." || s.endsWith "?" then
       let suggestions ← getQueryTermSuggestions s (← queryNum)
-      TryThis.addSuggestions stx suggestions (header:= "Lean Search Results")
+      TryThis.addSuggestions stx suggestions (header := "Lean Search Results")
     else
-      logWarning "Lean search query should end with a full stop (period) or a question mark. Note this command sends your query to an external service at https://leansearch.net/."
+      logWarning incompleteQuery
     defaultTerm expectedType?
   | _ => throwUnsupportedSyntax
 
 syntax (name := leansearch_tactic) "#leansearch" str : tactic
+
 @[tactic leansearch_tactic] def leanSearchTacticImpl : Tactic :=
   fun stx => withMainContext do
   match stx with
@@ -173,7 +188,7 @@ syntax (name := leansearch_tactic) "#leansearch" str : tactic
               pure false
           | _ => pure false
         unless sg.isEmpty do
-          TryThis.addSuggestions stx sg (header:= s!"From: {name}")
+          TryThis.addSuggestions stx sg (header := s!"From: {name}")
     else
-      logWarning "Lean search query should end with a full stop (period) or a question mark. Note this command sends your query to an external service at https://leansearch.net/."
+      logWarning incompleteQuery
   | _ => throwUnsupportedSyntax

LeanSearchClient/Syntax.lean

@@ -0,0 +1 @@
+import LeanSearchClientTest.Examples

LeanSearchClientTest.lean

@@ -0,0 +1,35 @@
+import LeanSearchClient.Syntax
+
+/-!
+# Lean Search Examples
+
+Examples of using the leansearch API. The search is triggered when the sentence ends with a full stop (period) or a question mark.
+-/
+
+/--
+warning: #leansearch query should end with a `.` or `?`.
+Note this command sends your query to an external service at https://leansearch.net/.
+-/
+#guard_msgs in
+#leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m"
+
+/--
+warning: #leansearch query should end with a `.` or `?`.
+Note this command sends your query to an external service at https://leansearch.net/.
+-/
+#guard_msgs in
+example := #leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m"
+
+set_option leansearch.queries 1
+
+/--
+info: From: Nat.succ_lt_succ (type: ∀ {n m : Nat}, n < m → Nat.succ n < Nat.succ m)
+• apply Nat.succ_lt_succ
+• have : ∀ {n m : Nat}, n < m → Nat.succ n < Nat.succ m := Nat.succ_lt_succ
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example : 3 ≤ 5 := by
+  #leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."
+  sorry

LeanSearchClientTest/Examples.lean

@@ -17,13 +17,13 @@ The following are examples of using the leansearch API. The search is triggered
 ### Query Command
 
 ```lean
-#leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m"
+#leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."
 ```
 
 ### Query Term
 
 ```lean
-example := #leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m"
+example := #leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."
 ```
 
 ### Query Tactic
@@ -32,6 +32,6 @@ Note that only valid tactics are displayed.
 
 ```lean
 example : 3 ≤ 5 := by
-  #leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m"
+  #leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."
   sorry
 ```

Main.lean

@@ -0,0 +1,9 @@
+name = "LeanSearchClient"
+testDriver = "LeanSearchClientTest"
+defaultTargets = ["LeanSearchClient"]
+
+[[lean_lib]]
+name = "LeanSearchClient"
+
+[[lean_lib]]
+name = "LeanSearchClientTest"