0 | module TTImp.Interactive.Completion
  1 |
  2 | import Idris.Syntax
  3 | import Idris.Parser
  4 |
  5 | import Data.String
  6 |
  7 | import Libraries.Data.WithDefault
  8 |
  9 | ||| Completion tasks are varied:
 10 | ||| are we trying to fill in a name, a REPL command, a pragma?
 11 | data Task
 12 |   = NameCompletion    String
 13 |   | CommandCompletion String
 14 |   | PragmaCompletion  (Maybe KwPragma) String
 15 |
 16 | ||| Completion receives the whole line it is supposed to work on.
 17 | ||| We start by trying to make sense of it as:
 18 | ||| 1. an ignored prefix (e.g. 'map' in 'map rever', '  ' in '  %def')
 19 | ||| 2. a completion task
 20 | parseTask : (line : String) -> Maybe (String, Task)
 21 | parseTask line =
 22 |   let (indnt, focus) = break (not . isSpace) line in
 23 |   case strM focus of
 24 |     StrCons '%' rest => case break isSpace rest of
 25 |         (pref, "") => pure (indnt, PragmaCompletion Nothing pref)
 26 |         (prag, rest) => do let prag = "%" ++ prag
 27 |                            let (spcs, rest) = break (not . isSpace) rest
 28 |                            let [kwprag] = filter ((prag ==) . show) allPragmas
 29 |                             | _ => Nothing
 30 |                            pure (concat {t = List} [indnt, prag, spcs]
 31 |                                 , PragmaCompletion (Just kwprag) rest)
 32 |     StrCons ':' rest => pure (indnt, CommandCompletion rest)
 33 |     _ => let ("", rest) = bimap Prelude.reverse Prelude.reverse
 34 |                         $ break (\ x => not (isAlphaNum x || x > chr 160))
 35 |                         $ Prelude.reverse line
 36 |               | (pref, rest) => pure (rest, NameCompletion pref)
 37 |          in Nothing
 38 |
 39 | ||| Name completion receives the prefix of the name to be completed
 40 | nameCompletion : {auto c : Ref Ctxt Defs} ->
 41 |                  (pref : String) -> Core (List String)
 42 | nameCompletion pref = do
 43 |   log "ide-mode.completion" 30 $ "Looking at name completions for \{show pref}"
 44 |   defs <- get Ctxt
 45 |   let cns = currentNS defs
 46 |   nms <- flip mapMaybeM !(allNames (gamma defs)) $ \ nsn => do
 47 |     -- the name better be a completion
 48 |     log "ide-mode.completion" 50 $ "Looking at \{show nsn}"
 49 |     let (ns, n) = splitNS nsn
 50 |     let True = pref `isPrefixOf` nameRoot n
 51 |       | False => pure Nothing
 52 |     -- and it better be visible
 53 |     Just def <- lookupCtxtExact nsn (gamma defs)
 54 |       | Nothing => pure Nothing
 55 |     let True = visibleIn cns nsn (collapseDefault $ visibility def)
 56 |       | False => pure Nothing
 57 |     pure (Just n)
 58 |   pure (map show $ nub nms)
 59 |
 60 | ||| Completion among a list of constants
 61 | oneOfCompletion : String -> List String -> Maybe (List String)
 62 | oneOfCompletion pref candidates = do
 63 |     let cs@(_ :: _) = filter (pref `isPrefixOf`) candidates
 64 |       | _ => Nothing
 65 |     pure cs
 66 |
 67 | ||| Pragma completion receives everything on the line following the % character
 68 | ||| and completes either the pragma itself of one of its arguments
 69 | ||| %def         -> %default
 70 | ||| %default to  -> %default total
 71 | ||| %logging "id -> %logging "ide-mode.(...)" with all the valid topics!
 72 | pragmaCompletion : {auto c : Ref Ctxt Defs} ->
 73 |                    (prag : Maybe KwPragma) -> (pref : String) ->
 74 |                    Core (Maybe (String, List String))
 75 | pragmaCompletion Nothing pref = pure $ do
 76 |   let ps@(_ :: _) = flip List.mapMaybe allPragmas $ \ prag => do
 77 |                       let prag = show prag
 78 |                       guard ("%" ++ pref `isPrefixOf` prag)
 79 |                       pure prag
 80 |     | _ => Nothing
 81 |   pure ("", ps)
 82 | pragmaCompletion (Just kw) pref = go (pragmaArgs kw) (break isSpace pref) where
 83 |
 84 |   go : List PragmaArg -> (String, String) -> Core (Maybe (String, List String))
 85 |   go (AName {} :: _) (here, "") = do
 86 |     ns@(_ :: _) <- nameCompletion here
 87 |       | _ => pure Nothing
 88 |     pure (Just ("", ns))
 89 |   go (AnOnOff :: _) (here, "") = pure (("",) <$> oneOfCompletion here ["on", "off"])
 90 |   go (AnOptionalLoggingTopic :: _) (here, "") = do
 91 |     let StrCons '"' here = strM here
 92 |       | _ => pure Nothing
 93 |     let lvls@(_ :: _) = filter ((here `isPrefixOf`) . fst) knownTopics
 94 |       | _ => pure Nothing
 95 |     pure (Just ("", map (show . fst) lvls))
 96 |   go (ALangExt :: _) (here, "") = pure (("",) <$> oneOfCompletion here (map show allLangExts))
 97 |   go (ATotalityLevel :: _) (here, "") = pure (("",) <$> oneOfCompletion here ["partial", "covering", "total"])
 98 |   go (_ :: args) (skip, rest) =
 99 |     let (indnt, rest) = break (not . isSpace) rest in
100 |     map (mapFst ((skip ++ indnt) ++)) <$> go args (break isSpace rest)
101 |   go _ (_, _) = pure Nothing
102 |
103 | ||| Completion receives the full line and returns
104 | ||| 1. the ignored prefix
105 | ||| 2. the list of possible completions
106 | export
107 | completion : {auto c : Ref Ctxt Defs} ->
108 |              (line : String) -> Core (Maybe (String, List String))
109 | completion line = do
110 |   let Just (ctxt, task) = parseTask line
111 |     | _ => pure Nothing
112 |   case task of
113 |     NameCompletion pref => (Just . (ctxt,)) <$> nameCompletion pref
114 |     PragmaCompletion mprag pref => map (mapFst (ctxt ++)) <$> pragmaCompletion mprag pref
115 |     CommandCompletion pref => case words pref of
116 |       ["logging"] => pure $ Just (ctxt ++ ":logging", map ((" " ++) . show . fst) knownTopics)
117 |       [pref] => let commands = concatMap fst parserCommandsForHelp in
118 |                 pure $ map ((ctxt,) . map (":" ++)) $ oneOfCompletion pref commands
119 |       ["logging", w] => pure $ map (ctxt ++ ":logging ",) (oneOfCompletion w (map (show . fst) knownTopics))
120 |       _ => pure Nothing
121 |