From 1e1e49bb9ec9a98c7eaa4b989fa467a8699f0fb0 Mon Sep 17 00:00:00 2001 From: Siddhartha Gadgil Date: Thu, 12 Sep 2024 17:53:52 +0530 Subject: [PATCH] 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