From 1bb389ee04b2390adb918b4e2a7cb8dd681e8600 Mon Sep 17 00:00:00 2001
From: Siddhartha Gadgil <siddhartha.gadgil@gmail.com>
Date: Thu, 12 Sep 2024 14:47:35 +0530
Subject: [PATCH 1/7] Moogle code draft (some renaming remains)

---
 LeanSearchClient/MoogleExamples.lean |  34 ++++++++
 LeanSearchClient/Syntax.lean         | 126 +++++++++++++++++++++++++++
 2 files changed, 160 insertions(+)
 create mode 100644 LeanSearchClient/MoogleExamples.lean

diff --git a/LeanSearchClient/MoogleExamples.lean b/LeanSearchClient/MoogleExamples.lean
new file mode 100644
index 0000000..c9ede7c
--- /dev/null
+++ b/LeanSearchClient/MoogleExamples.lean
@@ -0,0 +1,34 @@
+import LeanSearchClient.Syntax
+
+/-!
+# Moogle 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: #moogle query should end with a `.` or `?`.
+Note this command sends your query to an external service at https://www.moogle.ai/api/search.
+-/
+#guard_msgs in
+#moogle "If a natural number n is less than m, then the successor of n is less than the successor of m"
+
+/--
+warning: #moogle query should end with a `.` or `?`.
+Note this command sends your query to an external service at https://www.moogle.ai/api/search.
+-/
+#guard_msgs in
+example := #moogle "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.lt (type: Nat → Nat → Prop)
+• have : Nat → Nat → Prop := Nat.lt
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example : 3 ≤ 5 := by
+  #moogle "If a natural number n is less than m, then the successor of n is less than the successor of m."
+  sorry
diff --git a/LeanSearchClient/Syntax.lean b/LeanSearchClient/Syntax.lean
index 36fc126..74ff26d 100644
--- a/LeanSearchClient/Syntax.lean
+++ b/LeanSearchClient/Syntax.lean
@@ -38,12 +38,31 @@ def getQueryJson (s : String) (num_results : Nat := 6) : IO <| Array Json := do
   let js := Json.parse s.stdout |>.toOption |>.get!
   return js.getArr? |>.toOption |>.get!
 
+def getMoogleQueryJson (s : String) (num_results : Nat := 6) : IO <| Array Json := do
+  let apiUrl := "https://www.moogle.ai/api/search"
+  let data := Json.arr
+    #[Json.mkObj [("isFind", false), ("contents", s)]]
+  let s ← IO.Process.output {cmd := "curl", args := #[apiUrl, "-H", "content-type: application/json",  "--data", data.pretty]}
+  match Json.parse s.stdout with
+  | Except.error e =>
+    IO.throwServerError s!"Could not parse JSON from {s.stdout}; error: {e}"
+  | Except.ok js =>
+  let result? := js.getObjValAs?  Json "data"
+  match result? with
+    | Except.ok result =>
+        match result.getArr? with
+        | Except.ok arr => return arr[0:num_results]
+        | Except.error e => IO.throwServerError s!"Could not obtain array from {js}; error: {e}"
+    | _ => IO.throwServerError s!"Could not obtain data from {js}"
+
+
 structure SearchResult where
   name : String
   type? : Option String
   docString? : Option String
   doc_url? : Option String
   kind? : Option String
+  deriving Repr
 
 def queryNum : CoreM Nat := do
   return leansearch.queries.get (← getOptions)
@@ -61,11 +80,36 @@ def ofJson? (js : Json) : Option SearchResult :=
       some {name := name, type? := type?, docString? := doc?, doc_url? := docurl?, kind? := kind?}
   | _ => none
 
+def ofMoogleJson? (js : Json) : MetaM <| Option SearchResult :=
+  match js.getObjValAs? String "declarationName" with
+  | Except.ok name => do
+      let type? ←
+        try
+          let info ←  getConstInfo name.toName
+          let fmt ← PrettyPrinter.ppExpr info.type
+          pure <| some fmt.pretty
+        catch _ =>
+          pure none
+      let doc? := js.getObjValAs? String "declarationDocString" |>.toOption
+      let doc? := doc?.filter fun s => s != ""
+      let docurl? := none
+      let kind? := js.getObjValAs? String "declarationType" |>.toOption
+      return some {name := name, type? := type?, docString? := doc?, doc_url? := docurl?, kind? := kind?}
+  | _ => return none
+
 def query (s : String) (num_results : Nat) :
     IO <| Array SearchResult := do
   let jsArr ← getQueryJson s num_results
   return jsArr.filterMap ofJson?
 
+def queryMoogle (s : String) (num_results : Nat) :
+    MetaM <| Array SearchResult := do
+  let jsArr ← getMoogleQueryJson s num_results
+  jsArr.filterMapM ofMoogleJson?
+
+-- #eval queryMoogle "There are infinitely many primes" 12
+
+
 def toCommandSuggestion (sr : SearchResult) : TryThis.Suggestion :=
   let data := match sr.docString? with
     | some doc => s!"{doc}\n"
@@ -106,6 +150,25 @@ def getQueryTacticSuggestionGroups (s : String) (num_results : Nat) :
       | none => sr.name
     (fullName, sr.toTacticSuggestions)
 
+def getMoogleQueryCommandSuggestions (s: String)(num_results : Nat) :
+  MetaM <| Array TryThis.Suggestion := do
+    let searchResults ←  SearchResult.queryMoogle s num_results
+    return searchResults.map SearchResult.toCommandSuggestion
+
+def getMoogleQueryTermSuggestions (s: String)(num_results : Nat) :
+  MetaM <| Array TryThis.Suggestion := do
+    let searchResults ←  SearchResult.queryMoogle s num_results
+    return searchResults.map SearchResult.toTermSuggestion
+
+def getMoogleQueryTacticSuggestionGroups (s: String)(num_results : Nat) :
+  MetaM <| Array (String ×  Array TryThis.Suggestion) := do
+    let searchResults ←  SearchResult.queryMoogle 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
   | some type =>
@@ -132,6 +195,10 @@ 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/."
 
+def incompleteMoogleQuery : String :=
+  "#moogle query should end with a `.` or `?`.\n\
+   Note this command sends your query to an external service at https://www.moogle.ai/api/search."
+
 open Command
 
 syntax (name := leansearch_cmd) "#leansearch" str : command
@@ -192,3 +259,62 @@ syntax (name := leansearch_tactic) "#leansearch" str : tactic
     else
       logWarning incompleteQuery
   | _ => throwUnsupportedSyntax
+
+syntax (name := moogle_cmd) "#moogle" str : command
+
+@[command_elab moogle_cmd] def moogleSearchCommandImpl : CommandElab :=
+  fun stx => Command.liftTermElabM do
+  match stx with
+  | `(command| #moogle $s) =>
+    let s := s.getString
+    if s.endsWith "." || s.endsWith "?" then
+      let suggestions ← getMoogleQueryCommandSuggestions s (← queryNum)
+      TryThis.addSuggestions stx suggestions (header := "Moogle Results")
+    else
+      logWarning incompleteMoogleQuery
+  | _ => throwUnsupportedSyntax
+
+syntax (name := moogle_term) "#moogle" str : term
+
+@[term_elab moogle_term] def moogleSearchTermImpl : TermElab :=
+  fun stx expectedType? => do
+  match stx with
+  | `(#moogle $s) =>
+    let s := s.getString
+    if s.endsWith "." || s.endsWith "?" then
+      let suggestions ← getMoogleQueryTermSuggestions s (← queryNum)
+      TryThis.addSuggestions stx suggestions (header := "Moogle Results")
+    else
+      logWarning incompleteMoogleQuery
+    defaultTerm expectedType?
+  | _ => throwUnsupportedSyntax
+
+syntax (name := moogle_tactic) "#moogle" str : tactic
+
+@[tactic moogle_tactic] def moogleSearchTacticImpl : Tactic :=
+  fun stx => withMainContext do
+  match stx with
+  | `(tactic|#moogle $s) =>
+    let s := s.getString
+    if s.endsWith "." || s.endsWith "?" then
+      let target ← getMainTarget
+      let suggestionGroups ←
+          getMoogleQueryTacticSuggestionGroups s (← queryNum)
+      for (name, sg) in suggestionGroups do
+        let sg ←  sg.filterM fun s =>
+          let sugTxt := s.suggestion
+          match sugTxt with
+          | .string s => do
+            let stx? := runParserCategory (← getEnv) `tactic s
+            match stx? with
+            | Except.ok stx =>
+              let n? ← checkTactic target stx
+              return n?.isSome
+            | Except.error _ =>
+              pure false
+          | _ => pure false
+        unless sg.isEmpty do
+          TryThis.addSuggestions stx sg (header := s!"From: {name}")
+    else
+      logWarning incompleteMoogleQuery
+  | _ => throwUnsupportedSyntax

From 2dddae198c71484b8caca2b486ac3aa07596ed0d Mon Sep 17 00:00:00 2001
From: Siddhartha Gadgil <siddhartha.gadgil@gmail.com>
Date: Thu, 12 Sep 2024 14:53:56 +0530
Subject: [PATCH 2/7] Names, docs corrected

---
 LeanSearchClient/Basic.lean          |  5 +++++
 LeanSearchClient/MoogleExamples.lean |  4 ++--
 LeanSearchClient/Syntax.lean         | 17 +++++++++++++----
 3 files changed, 20 insertions(+), 6 deletions(-)

diff --git a/LeanSearchClient/Basic.lean b/LeanSearchClient/Basic.lean
index 6498e35..b3511a3 100644
--- a/LeanSearchClient/Basic.lean
+++ b/LeanSearchClient/Basic.lean
@@ -4,3 +4,8 @@ register_option leansearch.queries : Nat :=
   { defValue := 6
     group := "leansearch"
     descr := "Number of results requested from leansearch (default 6)" }
+
+register_option moogle.queries : Nat :=
+  { defValue := 6
+    group := "moogle"
+    descr := "Number of results requested from leansearch (default 6)" }
diff --git a/LeanSearchClient/MoogleExamples.lean b/LeanSearchClient/MoogleExamples.lean
index c9ede7c..484540b 100644
--- a/LeanSearchClient/MoogleExamples.lean
+++ b/LeanSearchClient/MoogleExamples.lean
@@ -3,7 +3,7 @@ import LeanSearchClient.Syntax
 /-!
 # Moogle Examples
 
-Examples of using the leansearch API. The search is triggered when the sentence ends with a full stop (period) or a question mark.
+Examples of using the Moogle API. The search is triggered when the sentence ends with a full stop (period) or a question mark.
 -/
 
 /--
@@ -20,7 +20,7 @@ Note this command sends your query to an external service at https://www.moogle.
 #guard_msgs in
 example := #moogle "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
+set_option moogle.queries 1
 
 /--
 info: From: Nat.lt (type: Nat → Nat → Prop)
diff --git a/LeanSearchClient/Syntax.lean b/LeanSearchClient/Syntax.lean
index 74ff26d..f81649d 100644
--- a/LeanSearchClient/Syntax.lean
+++ b/LeanSearchClient/Syntax.lean
@@ -11,17 +11,24 @@ import LeanSearchClient.Basic
 # LeanSearchClient
 
 In this file, we provide syntax for search using the [leansearch API](https://leansearch.net/)
+and the [Moogle API](https://www.moogle.ai/api/search).
 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:
+The queries are of three forms. For leansearch these are:
 
 * `Command` syntax: `#leansearch "search query"` as a command.
 * `Term` syntax: `#leansearch "search query"` as a term.
 * `Tactic` syntax: `#leansearch "search query"` as a tactic.
 
+The corresponding syntax for Moogle is:
+
+* `Command` syntax: `#moogle "search query"` as a command.
+* `Term` syntax: `#moogle "search query"` as a term.
+* `Tactic` syntax: `#moogle "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.
 -/
@@ -67,6 +74,8 @@ structure SearchResult where
 def queryNum : CoreM Nat := do
   return leansearch.queries.get (← getOptions)
 
+def moogleQueryNum : CoreM Nat := do
+  return moogle.queries.get (← getOptions)
 namespace SearchResult
 
 def ofJson? (js : Json) : Option SearchResult :=
@@ -268,7 +277,7 @@ syntax (name := moogle_cmd) "#moogle" str : command
   | `(command| #moogle $s) =>
     let s := s.getString
     if s.endsWith "." || s.endsWith "?" then
-      let suggestions ← getMoogleQueryCommandSuggestions s (← queryNum)
+      let suggestions ← getMoogleQueryCommandSuggestions s (← moogleQueryNum)
       TryThis.addSuggestions stx suggestions (header := "Moogle Results")
     else
       logWarning incompleteMoogleQuery
@@ -282,7 +291,7 @@ syntax (name := moogle_term) "#moogle" str : term
   | `(#moogle $s) =>
     let s := s.getString
     if s.endsWith "." || s.endsWith "?" then
-      let suggestions ← getMoogleQueryTermSuggestions s (← queryNum)
+      let suggestions ← getMoogleQueryTermSuggestions s (← moogleQueryNum)
       TryThis.addSuggestions stx suggestions (header := "Moogle Results")
     else
       logWarning incompleteMoogleQuery
@@ -299,7 +308,7 @@ syntax (name := moogle_tactic) "#moogle" str : tactic
     if s.endsWith "." || s.endsWith "?" then
       let target ← getMainTarget
       let suggestionGroups ←
-          getMoogleQueryTacticSuggestionGroups s (← queryNum)
+          getMoogleQueryTacticSuggestionGroups s (← moogleQueryNum)
       for (name, sg) in suggestionGroups do
         let sg ←  sg.filterM fun s =>
           let sugTxt := s.suggestion

From 49fa2fe48aac9a67937c480640a55b8abcdf143b Mon Sep 17 00:00:00 2001
From: Siddhartha Gadgil <siddhartha.gadgil@gmail.com>
Date: Thu, 12 Sep 2024 15:00:54 +0530
Subject: [PATCH 3/7] More symmetric names

---
 LeanSearchClient/Syntax.lean | 44 ++++++++++++++++++------------------
 1 file changed, 22 insertions(+), 22 deletions(-)

diff --git a/LeanSearchClient/Syntax.lean b/LeanSearchClient/Syntax.lean
index f81649d..cb89c05 100644
--- a/LeanSearchClient/Syntax.lean
+++ b/LeanSearchClient/Syntax.lean
@@ -37,7 +37,7 @@ namespace LeanSearchClient
 
 open Lean Meta Elab Tactic Parser Term
 
-def getQueryJson (s : String) (num_results : Nat := 6) : IO <| Array Json := do
+def getLeanSearchQueryJson (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}"
@@ -71,14 +71,14 @@ structure SearchResult where
   kind? : Option String
   deriving Repr
 
-def queryNum : CoreM Nat := do
+def leansearchQueryNum : CoreM Nat := do
   return leansearch.queries.get (← getOptions)
 
 def moogleQueryNum : CoreM Nat := do
   return moogle.queries.get (← getOptions)
 namespace SearchResult
 
-def ofJson? (js : Json) : Option SearchResult :=
+def ofLeanSearchJson? (js : Json) : Option SearchResult :=
   match js.getObjValAs? String "formal_name" with
   | Except.ok name =>
       let type? := js.getObjValAs? String "formal_type" |>.toOption
@@ -106,10 +106,10 @@ def ofMoogleJson? (js : Json) : MetaM <| Option SearchResult :=
       return some {name := name, type? := type?, docString? := doc?, doc_url? := docurl?, kind? := kind?}
   | _ => return none
 
-def query (s : String) (num_results : Nat) :
+def queryLeanSearch (s : String) (num_results : Nat) :
     IO <| Array SearchResult := do
-  let jsArr ← getQueryJson s num_results
-  return jsArr.filterMap ofJson?
+  let jsArr ← getLeanSearchQueryJson s num_results
+  return jsArr.filterMap ofLeanSearchJson?
 
 def queryMoogle (s : String) (num_results : Nat) :
     MetaM <| Array SearchResult := do
@@ -140,19 +140,19 @@ def toTacticSuggestions (sr : SearchResult) : Array TryThis.Suggestion :=
 
 end SearchResult
 
-def getQueryCommandSuggestions (s : String) (num_results : Nat) :
+def getLeanSearchQueryCommandSuggestions (s : String) (num_results : Nat) :
     IO <| Array TryThis.Suggestion := do
-  let searchResults ←  SearchResult.query s num_results
+  let searchResults ←  SearchResult.queryLeanSearch s num_results
   return searchResults.map SearchResult.toCommandSuggestion
 
-def getQueryTermSuggestions (s : String) (num_results : Nat) :
+def getLeanSearchQueryTermSuggestions (s : String) (num_results : Nat) :
     IO <| Array TryThis.Suggestion := do
-  let searchResults ←  SearchResult.query s num_results
+  let searchResults ←  SearchResult.queryLeanSearch s num_results
   return searchResults.map SearchResult.toTermSuggestion
 
-def getQueryTacticSuggestionGroups (s : String) (num_results : Nat) :
+def getLeanSearchQueryTacticSuggestionGroups (s : String) (num_results : Nat) :
     IO <| Array (String ×  Array TryThis.Suggestion) := do
-  let searchResults ←  SearchResult.query s num_results
+  let searchResults ←  SearchResult.queryLeanSearch s num_results
   return searchResults.map fun sr =>
     let fullName := match sr.type? with
       | some type => s!"{sr.name} (type: {type})"
@@ -200,7 +200,7 @@ def checkTactic (target : Expr) (tac : Syntax) :
   catch _ =>
     return none
 
-def incompleteQuery : String :=
+def incompleteLeanSearchQuery : String :=
   "#leansearch query should end with a `.` or `?`.\n\
    Note this command sends your query to an external service at https://leansearch.net/."
 
@@ -218,10 +218,10 @@ syntax (name := leansearch_cmd) "#leansearch" str : command
   | `(command| #leansearch $s) =>
     let s := s.getString
     if s.endsWith "." || s.endsWith "?" then
-      let suggestions ← getQueryCommandSuggestions s (← queryNum)
+      let suggestions ← getLeanSearchQueryCommandSuggestions s (← leansearchQueryNum)
       TryThis.addSuggestions stx suggestions (header := "Lean Search Results")
     else
-      logWarning incompleteQuery
+      logWarning incompleteLeanSearchQuery
   | _ => throwUnsupportedSyntax
 
 syntax (name := leansearch_term) "#leansearch" str : term
@@ -232,10 +232,10 @@ syntax (name := leansearch_term) "#leansearch" str : term
   | `(#leansearch $s) =>
     let s := s.getString
     if s.endsWith "." || s.endsWith "?" then
-      let suggestions ← getQueryTermSuggestions s (← queryNum)
+      let suggestions ← getLeanSearchQueryTermSuggestions s (← leansearchQueryNum)
       TryThis.addSuggestions stx suggestions (header := "Lean Search Results")
     else
-      logWarning incompleteQuery
+      logWarning incompleteLeanSearchQuery
     defaultTerm expectedType?
   | _ => throwUnsupportedSyntax
 
@@ -249,7 +249,7 @@ syntax (name := leansearch_tactic) "#leansearch" str : tactic
     if s.endsWith "." || s.endsWith "?" then
       let target ← getMainTarget
       let suggestionGroups ←
-          getQueryTacticSuggestionGroups s (← queryNum)
+          getLeanSearchQueryTacticSuggestionGroups s (← leansearchQueryNum)
       for (name, sg) in suggestionGroups do
         let sg ←  sg.filterM fun s =>
           let sugTxt := s.suggestion
@@ -266,12 +266,12 @@ syntax (name := leansearch_tactic) "#leansearch" str : tactic
         unless sg.isEmpty do
           TryThis.addSuggestions stx sg (header := s!"From: {name}")
     else
-      logWarning incompleteQuery
+      logWarning incompleteLeanSearchQuery
   | _ => throwUnsupportedSyntax
 
 syntax (name := moogle_cmd) "#moogle" str : command
 
-@[command_elab moogle_cmd] def moogleSearchCommandImpl : CommandElab :=
+@[command_elab moogle_cmd] def moogleCommandImpl : CommandElab :=
   fun stx => Command.liftTermElabM do
   match stx with
   | `(command| #moogle $s) =>
@@ -285,7 +285,7 @@ syntax (name := moogle_cmd) "#moogle" str : command
 
 syntax (name := moogle_term) "#moogle" str : term
 
-@[term_elab moogle_term] def moogleSearchTermImpl : TermElab :=
+@[term_elab moogle_term] def moogleTermImpl : TermElab :=
   fun stx expectedType? => do
   match stx with
   | `(#moogle $s) =>
@@ -300,7 +300,7 @@ syntax (name := moogle_term) "#moogle" str : term
 
 syntax (name := moogle_tactic) "#moogle" str : tactic
 
-@[tactic moogle_tactic] def moogleSearchTacticImpl : Tactic :=
+@[tactic moogle_tactic] def moogleTacticImpl : Tactic :=
   fun stx => withMainContext do
   match stx with
   | `(tactic|#moogle $s) =>

From 05e26f9daa726e3207964509131f4d85df7576fe Mon Sep 17 00:00:00 2001
From: Siddhartha Gadgil <siddhartha.gadgil@gmail.com>
Date: Thu, 12 Sep 2024 15:19:33 +0530
Subject: [PATCH 4/7] refactored "incompleteSyntax"

---
 LeanSearchClient/Syntax.lean | 24 +++++++++++-------------
 1 file changed, 11 insertions(+), 13 deletions(-)

diff --git a/LeanSearchClient/Syntax.lean b/LeanSearchClient/Syntax.lean
index cb89c05..1cdde73 100644
--- a/LeanSearchClient/Syntax.lean
+++ b/LeanSearchClient/Syntax.lean
@@ -116,7 +116,6 @@ def queryMoogle (s : String) (num_results : Nat) :
   let jsArr ← getMoogleQueryJson s num_results
   jsArr.filterMapM ofMoogleJson?
 
--- #eval queryMoogle "There are infinitely many primes" 12
 
 
 def toCommandSuggestion (sr : SearchResult) : TryThis.Suggestion :=
@@ -200,13 +199,12 @@ def checkTactic (target : Expr) (tac : Syntax) :
   catch _ =>
     return none
 
-def incompleteLeanSearchQuery : String :=
-  "#leansearch query should end with a `.` or `?`.\n\
-   Note this command sends your query to an external service at https://leansearch.net/."
+def incompleteSearchQuery (name url : String) : String :=
+  s!"{name} query should end with a `.` or `?`.\n\
+   Note this command sends your query to an external service at {url}."
+
+
 
-def incompleteMoogleQuery : String :=
-  "#moogle query should end with a `.` or `?`.\n\
-   Note this command sends your query to an external service at https://www.moogle.ai/api/search."
 
 open Command
 
@@ -221,7 +219,7 @@ syntax (name := leansearch_cmd) "#leansearch" str : command
       let suggestions ← getLeanSearchQueryCommandSuggestions s (← leansearchQueryNum)
       TryThis.addSuggestions stx suggestions (header := "Lean Search Results")
     else
-      logWarning incompleteLeanSearchQuery
+      logWarning <| incompleteSearchQuery "#leansearch" "https://leansearch.net/"
   | _ => throwUnsupportedSyntax
 
 syntax (name := leansearch_term) "#leansearch" str : term
@@ -235,7 +233,7 @@ syntax (name := leansearch_term) "#leansearch" str : term
       let suggestions ← getLeanSearchQueryTermSuggestions s (← leansearchQueryNum)
       TryThis.addSuggestions stx suggestions (header := "Lean Search Results")
     else
-      logWarning incompleteLeanSearchQuery
+      logWarning <| incompleteSearchQuery "#leansearch" "https://leansearch.net/"
     defaultTerm expectedType?
   | _ => throwUnsupportedSyntax
 
@@ -266,7 +264,7 @@ syntax (name := leansearch_tactic) "#leansearch" str : tactic
         unless sg.isEmpty do
           TryThis.addSuggestions stx sg (header := s!"From: {name}")
     else
-      logWarning incompleteLeanSearchQuery
+      logWarning <| incompleteSearchQuery "#leansearch" "https://leansearch.net/"
   | _ => throwUnsupportedSyntax
 
 syntax (name := moogle_cmd) "#moogle" str : command
@@ -280,7 +278,7 @@ syntax (name := moogle_cmd) "#moogle" str : command
       let suggestions ← getMoogleQueryCommandSuggestions s (← moogleQueryNum)
       TryThis.addSuggestions stx suggestions (header := "Moogle Results")
     else
-      logWarning incompleteMoogleQuery
+      logWarning <| incompleteSearchQuery "#moogle" "https://www.moogle.ai/api/search"
   | _ => throwUnsupportedSyntax
 
 syntax (name := moogle_term) "#moogle" str : term
@@ -294,7 +292,7 @@ syntax (name := moogle_term) "#moogle" str : term
       let suggestions ← getMoogleQueryTermSuggestions s (← moogleQueryNum)
       TryThis.addSuggestions stx suggestions (header := "Moogle Results")
     else
-      logWarning incompleteMoogleQuery
+      logWarning <| incompleteSearchQuery "#moogle" "https://www.moogle.ai/api/search"
     defaultTerm expectedType?
   | _ => throwUnsupportedSyntax
 
@@ -325,5 +323,5 @@ syntax (name := moogle_tactic) "#moogle" str : tactic
         unless sg.isEmpty do
           TryThis.addSuggestions stx sg (header := s!"From: {name}")
     else
-      logWarning incompleteMoogleQuery
+      logWarning <| incompleteSearchQuery "#moogle" "https://www.moogle.ai/api/search"
   | _ => throwUnsupportedSyntax

From 1e1e49bb9ec9a98c7eaa4b989fa467a8699f0fb0 Mon Sep 17 00:00:00 2001
From: Siddhartha Gadgil <siddhartha.gadgil@gmail.com>
Date: Thu, 12 Sep 2024 17:53:52 +0530
Subject: [PATCH 5/7] reduced some code duplication

---
 LeanSearchClient/Syntax.lean | 215 +++++++++++++++--------------------
 1 file changed, 93 insertions(+), 122 deletions(-)

diff --git a/LeanSearchClient/Syntax.lean b/LeanSearchClient/Syntax.lean
index 1cdde73..77c6f96 100644
--- a/LeanSearchClient/Syntax.lean
+++ b/LeanSearchClient/Syntax.lean
@@ -71,11 +71,6 @@ structure SearchResult where
   kind? : Option String
   deriving Repr
 
-def leansearchQueryNum : CoreM Nat := do
-  return leansearch.queries.get (← getOptions)
-
-def moogleQueryNum : CoreM Nat := do
-  return moogle.queries.get (← getOptions)
 namespace SearchResult
 
 def ofLeanSearchJson? (js : Json) : Option SearchResult :=
@@ -106,18 +101,6 @@ def ofMoogleJson? (js : Json) : MetaM <| Option SearchResult :=
       return some {name := name, type? := type?, docString? := doc?, doc_url? := docurl?, kind? := kind?}
   | _ => return none
 
-def queryLeanSearch (s : String) (num_results : Nat) :
-    IO <| Array SearchResult := do
-  let jsArr ← getLeanSearchQueryJson s num_results
-  return jsArr.filterMap ofLeanSearchJson?
-
-def queryMoogle (s : String) (num_results : Nat) :
-    MetaM <| Array SearchResult := do
-  let jsArr ← getMoogleQueryJson s num_results
-  jsArr.filterMapM ofMoogleJson?
-
-
-
 def toCommandSuggestion (sr : SearchResult) : TryThis.Suggestion :=
   let data := match sr.docString? with
     | some doc => s!"{doc}\n"
@@ -139,43 +122,16 @@ def toTacticSuggestions (sr : SearchResult) : Array TryThis.Suggestion :=
 
 end SearchResult
 
-def getLeanSearchQueryCommandSuggestions (s : String) (num_results : Nat) :
-    IO <| Array TryThis.Suggestion := do
-  let searchResults ←  SearchResult.queryLeanSearch s num_results
-  return searchResults.map SearchResult.toCommandSuggestion
 
-def getLeanSearchQueryTermSuggestions (s : String) (num_results : Nat) :
-    IO <| Array TryThis.Suggestion := do
-  let searchResults ←  SearchResult.queryLeanSearch s num_results
-  return searchResults.map SearchResult.toTermSuggestion
-
-def getLeanSearchQueryTacticSuggestionGroups (s : String) (num_results : Nat) :
-    IO <| Array (String ×  Array TryThis.Suggestion) := do
-  let searchResults ←  SearchResult.queryLeanSearch 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 queryLeanSearch (s : String) (num_results : Nat) :
+    MetaM <| Array SearchResult := do
+  let jsArr ← getLeanSearchQueryJson s num_results
+  return jsArr.filterMap SearchResult.ofLeanSearchJson?
 
-def getMoogleQueryCommandSuggestions (s: String)(num_results : Nat) :
-  MetaM <| Array TryThis.Suggestion := do
-    let searchResults ←  SearchResult.queryMoogle s num_results
-    return searchResults.map SearchResult.toCommandSuggestion
-
-def getMoogleQueryTermSuggestions (s: String)(num_results : Nat) :
-  MetaM <| Array TryThis.Suggestion := do
-    let searchResults ←  SearchResult.queryMoogle s num_results
-    return searchResults.map SearchResult.toTermSuggestion
-
-def getMoogleQueryTacticSuggestionGroups (s: String)(num_results : Nat) :
-  MetaM <| Array (String ×  Array TryThis.Suggestion) := do
-    let searchResults ←  SearchResult.queryMoogle 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 queryMoogle (s : String) (num_results : Nat) :
+    MetaM <| Array SearchResult := do
+  let jsArr ← getMoogleQueryJson s num_results
+  jsArr.filterMapM SearchResult.ofMoogleJson?
 
 def defaultTerm (expectedType? : Option Expr) : MetaM Expr := do
   match expectedType? with
@@ -199,55 +155,70 @@ def checkTactic (target : Expr) (tac : Syntax) :
   catch _ =>
     return none
 
-def incompleteSearchQuery (name url : String) : String :=
-  s!"{name} query should end with a `.` or `?`.\n\
-   Note this command sends your query to an external service at {url}."
-
-
+structure SearchServer where
+  name : String
+  url : String
+  cmd: String
+  query : String → Nat → MetaM  (Array SearchResult)
+  queryNum : CoreM Nat
+
+def leanSearchServer : SearchServer :=
+  {name := "LeanSearch", cmd := "#leansearch", url := "https://leansearch.net/",
+   query := queryLeanSearch, queryNum := return leansearch.queries.get (← getOptions)}
+
+def moogleServer : SearchServer :=
+  {name := "Moogle", cmd := "#moogle", url := "https://www.moogle.ai/api/search",
+   query := queryMoogle, queryNum := return moogle.queries.get (← getOptions)}
+
+namespace SearchServer
+
+def getCommandSuggestions (ss : SearchServer) (s : String)(num_results : Nat) :
+    MetaM (Array TryThis.Suggestion) := do
+  let suggestions ← ss.query s num_results
+  return suggestions.map SearchResult.toCommandSuggestion
+
+def getTermSuggestions (ss : SearchServer) (s : String)(num_results : Nat) :
+    MetaM (Array TryThis.Suggestion) := do
+  let suggestions ← ss.query s num_results
+  return suggestions.map SearchResult.toTermSuggestion
+
+def getTacticSuggestionGroups (ss : SearchServer) (s : String)(num_results : Nat) :
+    MetaM (Array (String ×  Array TryThis.Suggestion)) := do
+  let suggestions ← ss.query s num_results
+  return suggestions.map fun sr =>
+    let fullName := match sr.type? with
+      | some type => s!"{sr.name} (type: {type})"
+      | none => sr.name
+    (fullName, sr.toTacticSuggestions)
 
+def incompleteSearchQuery (ss : SearchServer) : String :=
+  s!"{ss.cmd} query should end with a `.` or `?`.\n\
+   Note this command sends your query to an external service at {ss.url}."
 
 open Command
-
-syntax (name := leansearch_cmd) "#leansearch" str : command
-
-@[command_elab leansearch_cmd] def leanSearchCommandImpl : CommandElab :=
-  fun stx => Command.liftTermElabM do
-  match stx with
-  | `(command| #leansearch $s) =>
+def searchCommandSuggestions (ss: SearchServer) (stx: Syntax) (s: TSyntax `str) : CommandElabM Unit := Command.liftTermElabM do
     let s := s.getString
     if s.endsWith "." || s.endsWith "?" then
-      let suggestions ← getLeanSearchQueryCommandSuggestions s (← leansearchQueryNum)
-      TryThis.addSuggestions stx suggestions (header := "Lean Search Results")
+      let suggestions ← ss.getCommandSuggestions s (← ss.queryNum)
+      TryThis.addSuggestions stx suggestions (header := s!"{ss.name} Search Results")
     else
-      logWarning <| incompleteSearchQuery "#leansearch" "https://leansearch.net/"
-  | _ => throwUnsupportedSyntax
-
-syntax (name := leansearch_term) "#leansearch" str : term
+      logWarning <| ss.incompleteSearchQuery
 
-@[term_elab leansearch_term] def leanSearchTermImpl : TermElab :=
-  fun stx expectedType? => do
-  match stx with
-  | `(#leansearch $s) =>
+def searchTermSuggestions (ss: SearchServer) (stx: Syntax)
+    (s: TSyntax `str)  : TermElabM Unit := do
     let s := s.getString
     if s.endsWith "." || s.endsWith "?" then
-      let suggestions ← getLeanSearchQueryTermSuggestions s (← leansearchQueryNum)
-      TryThis.addSuggestions stx suggestions (header := "Lean Search Results")
+      let suggestions ← ss.getTermSuggestions s (← ss.queryNum)
+      TryThis.addSuggestions stx suggestions (header := s!"{ss.name} Search Results")
     else
-      logWarning <| incompleteSearchQuery "#leansearch" "https://leansearch.net/"
-    defaultTerm expectedType?
-  | _ => throwUnsupportedSyntax
-
-syntax (name := leansearch_tactic) "#leansearch" str : tactic
+      logWarning <| ss.incompleteSearchQuery
 
-@[tactic leansearch_tactic] def leanSearchTacticImpl : Tactic :=
-  fun stx => withMainContext do
-  match stx with
-  | `(tactic|#leansearch $s) =>
+def searchTacticSuggestions (ss: SearchServer) (stx: Syntax) (s: TSyntax `str) : TacticM Unit := do
     let s := s.getString
     if s.endsWith "." || s.endsWith "?" then
       let target ← getMainTarget
       let suggestionGroups ←
-          getLeanSearchQueryTacticSuggestionGroups s (← leansearchQueryNum)
+          ss.getTacticSuggestionGroups s (← ss.queryNum)
       for (name, sg) in suggestionGroups do
         let sg ←  sg.filterM fun s =>
           let sugTxt := s.suggestion
@@ -264,21 +235,47 @@ syntax (name := leansearch_tactic) "#leansearch" str : tactic
         unless sg.isEmpty do
           TryThis.addSuggestions stx sg (header := s!"From: {name}")
     else
-      logWarning <| incompleteSearchQuery "#leansearch" "https://leansearch.net/"
+      logWarning <| ss.incompleteSearchQuery
+
+end SearchServer
+
+open Command
+
+syntax (name := leansearch_cmd) "#leansearch" str : command
+
+@[command_elab leansearch_cmd] def leanSearchCommandImpl : CommandElab :=
+  fun stx =>
+  match stx with
+  | `(command| #leansearch $s) =>
+    leanSearchServer.searchCommandSuggestions  stx s
+  | _ => throwUnsupportedSyntax
+
+syntax (name := leansearch_term) "#leansearch" str : term
+
+@[term_elab leansearch_term] def leanSearchTermImpl : TermElab :=
+  fun stx expectedType? => do
+  match stx with
+  | `(#leansearch $s) =>
+    leanSearchServer.searchTermSuggestions stx s
+    defaultTerm expectedType?
+  | _ => throwUnsupportedSyntax
+
+syntax (name := leansearch_tactic) "#leansearch" str : tactic
+
+@[tactic leansearch_tactic] def leanSearchTacticImpl : Tactic :=
+  fun stx => withMainContext do
+  match stx with
+  | `(tactic|#leansearch $s) =>
+    leanSearchServer.searchTacticSuggestions stx s
   | _ => throwUnsupportedSyntax
 
 syntax (name := moogle_cmd) "#moogle" str : command
 
 @[command_elab moogle_cmd] def moogleCommandImpl : CommandElab :=
-  fun stx => Command.liftTermElabM do
+  fun stx =>
   match stx with
   | `(command| #moogle $s) =>
-    let s := s.getString
-    if s.endsWith "." || s.endsWith "?" then
-      let suggestions ← getMoogleQueryCommandSuggestions s (← moogleQueryNum)
-      TryThis.addSuggestions stx suggestions (header := "Moogle Results")
-    else
-      logWarning <| incompleteSearchQuery "#moogle" "https://www.moogle.ai/api/search"
+    moogleServer.searchCommandSuggestions stx s
   | _ => throwUnsupportedSyntax
 
 syntax (name := moogle_term) "#moogle" str : term
@@ -287,12 +284,7 @@ syntax (name := moogle_term) "#moogle" str : term
   fun stx expectedType? => do
   match stx with
   | `(#moogle $s) =>
-    let s := s.getString
-    if s.endsWith "." || s.endsWith "?" then
-      let suggestions ← getMoogleQueryTermSuggestions s (← moogleQueryNum)
-      TryThis.addSuggestions stx suggestions (header := "Moogle Results")
-    else
-      logWarning <| incompleteSearchQuery "#moogle" "https://www.moogle.ai/api/search"
+    moogleServer.searchTermSuggestions stx s
     defaultTerm expectedType?
   | _ => throwUnsupportedSyntax
 
@@ -302,26 +294,5 @@ syntax (name := moogle_tactic) "#moogle" str : tactic
   fun stx => withMainContext do
   match stx with
   | `(tactic|#moogle $s) =>
-    let s := s.getString
-    if s.endsWith "." || s.endsWith "?" then
-      let target ← getMainTarget
-      let suggestionGroups ←
-          getMoogleQueryTacticSuggestionGroups s (← moogleQueryNum)
-      for (name, sg) in suggestionGroups do
-        let sg ←  sg.filterM fun s =>
-          let sugTxt := s.suggestion
-          match sugTxt with
-          | .string s => do
-            let stx? := runParserCategory (← getEnv) `tactic s
-            match stx? with
-            | Except.ok stx =>
-              let n? ← checkTactic target stx
-              return n?.isSome
-            | Except.error _ =>
-              pure false
-          | _ => pure false
-        unless sg.isEmpty do
-          TryThis.addSuggestions stx sg (header := s!"From: {name}")
-    else
-      logWarning <| incompleteSearchQuery "#moogle" "https://www.moogle.ai/api/search"
+    moogleServer.searchTacticSuggestions stx s
   | _ => throwUnsupportedSyntax

From 9fc966a255257330b25a63cce09b22d6c3a18466 Mon Sep 17 00:00:00 2001
From: Siddhartha Gadgil <siddhartha.gadgil@gmail.com>
Date: Thu, 12 Sep 2024 20:54:16 +0530
Subject: [PATCH 6/7] further reduced duplication

---
 LeanSearchClient/Syntax.lean | 62 +++++++++++++++---------------------
 1 file changed, 25 insertions(+), 37 deletions(-)

diff --git a/LeanSearchClient/Syntax.lean b/LeanSearchClient/Syntax.lean
index 77c6f96..bcf9d37 100644
--- a/LeanSearchClient/Syntax.lean
+++ b/LeanSearchClient/Syntax.lean
@@ -170,6 +170,8 @@ def moogleServer : SearchServer :=
   {name := "Moogle", cmd := "#moogle", url := "https://www.moogle.ai/api/search",
    query := queryMoogle, queryNum := return moogle.queries.get (← getOptions)}
 
+instance : Inhabited SearchServer := ⟨leanSearchServer⟩
+
 namespace SearchServer
 
 def getCommandSuggestions (ss : SearchServer) (s : String)(num_results : Nat) :
@@ -241,58 +243,44 @@ end SearchServer
 
 open Command
 
-syntax (name := leansearch_cmd) "#leansearch" str : command
-
-@[command_elab leansearch_cmd] def leanSearchCommandImpl : CommandElab :=
-  fun stx =>
-  match stx with
-  | `(command| #leansearch $s) =>
-    leanSearchServer.searchCommandSuggestions  stx s
-  | _ => throwUnsupportedSyntax
-
-syntax (name := leansearch_term) "#leansearch" str : term
-
-@[term_elab leansearch_term] def leanSearchTermImpl : TermElab :=
-  fun stx expectedType? => do
-  match stx with
-  | `(#leansearch $s) =>
-    leanSearchServer.searchTermSuggestions stx s
-    defaultTerm expectedType?
-  | _ => throwUnsupportedSyntax
+declare_syntax_cat search_cmd
 
-syntax (name := leansearch_tactic) "#leansearch" str : tactic
+syntax "#leansearch" : search_cmd
+syntax "#moogle" : search_cmd
 
-@[tactic leansearch_tactic] def leanSearchTacticImpl : Tactic :=
-  fun stx => withMainContext do
-  match stx with
-  | `(tactic|#leansearch $s) =>
-    leanSearchServer.searchTacticSuggestions stx s
-  | _ => throwUnsupportedSyntax
+syntax (name := search_cmd) search_cmd str : command
 
-syntax (name := moogle_cmd) "#moogle" str : command
+def getSearchServer (sc : Syntax) : SearchServer :=
+  match sc with
+  | `(search_cmd| #leansearch) => leanSearchServer
+  | `(search_cmd| #moogle) => moogleServer
+  | _ => panic! "unsupported search command"
 
-@[command_elab moogle_cmd] def moogleCommandImpl : CommandElab :=
+@[command_elab search_cmd] def searchCommandImpl : CommandElab :=
   fun stx =>
   match stx with
-  | `(command| #moogle $s) =>
-    moogleServer.searchCommandSuggestions stx s
+  | `(command| $sc:search_cmd $s) => do
+    let ss := getSearchServer sc
+    ss.searchCommandSuggestions  stx s
   | _ => throwUnsupportedSyntax
 
-syntax (name := moogle_term) "#moogle" str : term
+syntax (name := search_term) search_cmd str : term
 
-@[term_elab moogle_term] def moogleTermImpl : TermElab :=
+@[term_elab search_term] def searchTermImpl : TermElab :=
   fun stx expectedType? => do
   match stx with
-  | `(#moogle $s) =>
-    moogleServer.searchTermSuggestions stx s
+  | `($sc:search_cmd $s) =>
+    let ss := getSearchServer sc
+    ss.searchTermSuggestions stx s
     defaultTerm expectedType?
   | _ => throwUnsupportedSyntax
 
-syntax (name := moogle_tactic) "#moogle" str : tactic
+syntax (name := search_tactic) search_cmd str : tactic
 
-@[tactic moogle_tactic] def moogleTacticImpl : Tactic :=
+@[tactic search_tactic] def searchTacticImpl : Tactic :=
   fun stx => withMainContext do
   match stx with
-  | `(tactic|#moogle $s) =>
-    moogleServer.searchTacticSuggestions stx s
+  | `(tactic|$sc:search_cmd $s) =>
+    let ss := getSearchServer sc
+    ss.searchTacticSuggestions stx s
   | _ => throwUnsupportedSyntax

From 05f5fe675bac676b6815d6c49df42c1c546cd1fa Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Fri, 13 Sep 2024 13:33:38 +1000
Subject: [PATCH 7/7] Apply suggestions from code review

---
 LeanSearchClient/Syntax.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/LeanSearchClient/Syntax.lean b/LeanSearchClient/Syntax.lean
index bcf9d37..b86846b 100644
--- a/LeanSearchClient/Syntax.lean
+++ b/LeanSearchClient/Syntax.lean
@@ -174,17 +174,17 @@ instance : Inhabited SearchServer := ⟨leanSearchServer⟩
 
 namespace SearchServer
 
-def getCommandSuggestions (ss : SearchServer) (s : String)(num_results : Nat) :
+def getCommandSuggestions (ss : SearchServer) (s : String) (num_results : Nat) :
     MetaM (Array TryThis.Suggestion) := do
   let suggestions ← ss.query s num_results
   return suggestions.map SearchResult.toCommandSuggestion
 
-def getTermSuggestions (ss : SearchServer) (s : String)(num_results : Nat) :
+def getTermSuggestions (ss : SearchServer) (s : String) (num_results : Nat) :
     MetaM (Array TryThis.Suggestion) := do
   let suggestions ← ss.query s num_results
   return suggestions.map SearchResult.toTermSuggestion
 
-def getTacticSuggestionGroups (ss : SearchServer) (s : String)(num_results : Nat) :
+def getTacticSuggestionGroups (ss : SearchServer) (s : String) (num_results : Nat) :
     MetaM (Array (String ×  Array TryThis.Suggestion)) := do
   let suggestions ← ss.query s num_results
   return suggestions.map fun sr =>