newt/src/Commands.newt

-- For shared code between REPL and LSP
module Commands

import Prelude
import Lib.ProcessModule
import Lib.Types
import Lib.TopContext
import Lib.Common
import Data.List1
import Lib.Tokenizer
import Lib.Token
import Lib.Elab
import Data.String
import Lib.Eval
import Data.SortedMap

-- For now we cheat and assume capitalized directories are a module component
decomposeName : String → String × String
decomposeName fn =
    go Nil $ Lin <>< split (fst $ splitFileName fn) "/"
    where
        go : List String → SnocList String → String × String
        go acc Lin = (".", joinBy "." acc)
        go acc (xs :< x) = if isUpper $ strIndex x 0
            then go (x :: acc) xs
            else (joinBy "/" (xs :< x <>> Nil), joinBy "." acc)


switchModule : FileSource → String → M (Maybe ModContext)
switchModule repo modns = do
    top <- getTop
    let (Just mod) = lookupMap' modns top.modules | Nothing => pure Nothing
    modifyTop [ currentMod := mod; ops := mod.modOps ]
    pure $ Just mod

-- The cheap version of type at point, find the token, lookup in global context
-- Later we will either get good FC for entries or scan them all and build a cache.
getHoverInfo : FileSource → String → Int → Int → M (Maybe (String × FC))
getHoverInfo repo modns row col = do
    Just mod <- switchModule repo modns | _ => pure Nothing
    top <- getTop

    -- Find the token at the point
    let lines = split mod.modSource "\n"
    let line = fromMaybe "" (getAt' row lines)
    let (Right toks) = tokenise "" line | Left _ => pure Nothing
    let (Just name) = getTok toks       | _ => pure Nothing

    -- Lookup the name
    let (Just e) = lookupRaw name top   | _ => pure Nothing
    ty <- nf Nil e.type
    pure $ Just ("\{show e.name} : \{rpprint Nil ty}", e.fc)

    where
        getTok : List BTok → Maybe String
        getTok Nil = Nothing
        getTok (tok :: toks) =
            if tok.bounds.startCol <= col && (col <= tok.bounds.endCol)
            then Just $ value tok else getTok toks

data FileEdit = MkEdit FC String
data CodeAction
  = CaseSplitAction (List FileEdit)
  | AddMissingAction (List FileEdit)
  | Intro String FileEdit


applyDCon : QName × Int × Tm → List String
applyDCon (QN _ nm, _, tm) = go (Lin :< nm) tm
  where
    go : SnocList String → Tm → List String
    go acc (Pi _ nm Explicit _ _ u) = go (acc :< nm) u
    go acc (Pi _ _ _ _ _ u) = go acc u
    go acc _ = acc <>> Nil

data Flavor = EqSplit | FatArrowSplit | MonadSplit

-- Not quite right, we also need to check for let...
-- But it's a first pass
splitEquals : SnocList Char → List Char → (Flavor × String × String)
splitEquals acc Nil = (EqSplit, pack (acc <>> Nil), "")
splitEquals acc xs@('=' :: '>' :: _) = (FatArrowSplit, pack (acc <>> Nil), pack xs)
splitEquals acc xs@('=' :: _) = (EqSplit, pack (acc <>> Nil), pack xs)
splitEquals acc xs@('<' :: '-' :: _) = (MonadSplit, pack (acc <>> Nil), pack xs)
splitEquals acc (x :: xs) = splitEquals (acc :< x) xs

needParens : SnocList Char → List Char → Bool
needParens (xs :< ' ') ys = needParens xs ys
needParens xs (' ' :: ys) = needParens xs ys
needParens (xs :< '(') (')' :: ys) = False
needParens _ _ = True

addParens : Bool → List String → String
addParens _ (x :: Nil) = x
addParens False s = unwords s
addParens True s = "(\{unwords s})"

-- resugar operator applications
-- assumes the components are simple identifiers
resugarOper : List String → List String
resugarOper Nil = Nil
resugarOper (x :: xs) = go Lin (split x "_") xs
  where
    go : SnocList String → List String → List String → List String
    go acc Nil xs = acc <>> xs
    go acc ("" :: rest) (x :: xs) = go (acc :< x) rest xs
    -- If there are not enough parts, bail and fall back to `_+_ x`
    go acc ("" :: rest) Nil = (x :: xs)
    go acc (x :: xs) ys = go (acc :< x) xs ys

-- REVIEW - maybe pass in QName and use applyDCon in here, especially if we want to get better names?
makeEdits : FC → List QName → Bool → M (List FileEdit)
makeEdits fc@(MkFC uri (MkBounds sr sc er ec)) names inPlace = do
  cons <- map applyDCon <$> traverse lookupDCon names
  top <- getTop
  let (Just mod) = lookupMap' top.currentMod.modName top.modules | _ => pure Nil
  let lines = split mod.modSource "\n"
  let (Just line) = getAt' sr lines | _ => pure Nil
  let cs = unpack line
  let head = take (cast sc) cs
  let tail = drop (S $ cast (ec - 1)) cs
  let (splitKind, before, after) = splitEquals Lin tail
  let np = needParens (Lin <>< head) tail
  let cons = map (addParens np ∘ resugarOper) cons
  let phead = pack head
  let indent = getIndent 0 head
  let nextrow = scan indent lines (sr + 1)

  -- No init or first :: rest for add missing case
  let (edits, rest) = doFirst inPlace cons

  let phead = pack head
  let fc' = MkFC uri (MkBounds nextrow 0 nextrow 0)
  let srest =
    case splitKind of
      EqSplit => joinBy "" $ map (\ap => phead ++ ap ++ before ++ "= ?\n") rest
      FatArrowSplit => joinBy "" $ map (\ap => phead ++ ap ++ before ++ "=> ?\n") rest
      MonadSplit => joinBy "" $ map (\ap => "  | \{pack head}\{ap}\{before}=> ?\n") rest

  putStrLn "Split \{show line} HD '\{show head}' TL '\{show tail}'"
  putStrLn srest
  let edits = MkEdit fc' (srest) :: edits
  putStrLn "edits \{debugStr edits}"
  pure edits
  where
    getIndent : Int → List Char → Int
    getIndent acc (' ' :: rest) = getIndent (1 + acc) rest
    getIndent acc _ = acc

    scan : Int → List String → Int → Int
    scan indent lines row =
      let x = getIndent 0 $ unpack $ fromMaybe "" $ getAt' row lines in
      if x <= indent then row else scan indent lines (row + 1)

    doFirst : Bool → List String → (List FileEdit × List String)
    doFirst True (first :: rest) = (MkEdit fc first :: Nil, rest)
    doFirst _ cons = (Nil, cons)

addMissingCases : Int → Int → FC → Context → List QName → M (Maybe CodeAction)
addMissingCases _ _ fc@(MkFC uri (MkBounds sr sc er ec)) ctx names = do
  top <- getTop
  edits <- makeEdits fc names False
  putStrLn "Add Missing \{show fc} \{show names}"
  pure $ Just $ AddMissingAction edits

getCaseSplit : Int → Int → FC → Context → String → Val → M (Maybe CodeAction)
getCaseSplit row col fc@(MkFC uri (MkBounds sr sc er ec)) ctx nm scty = do
  top <- getTop
  -- It's getting vars for the type
  scty <- unlet ctx.env scty
  cons <- getConstructors ctx fc scty
  ty <- quote (length' ctx.env) scty
  cons <- filterM (checkCase ctx nm scty) cons
  let names = map fst cons
  putStrLn "Make splits for \{show names}"
  edits <- makeEdits fc names True
  pure $ Just $ CaseSplitAction edits

posInFC : Int → Int → FC → Bool
-- FIXME ec + 1 again...
posInFC row col (MkFC _ (MkBounds sr sc er ec)) = (sr <= row && row <= er) && (sc <= col && col <= ec + 1)

getHole : ModContext → Int → Int → Maybe MetaEntry
getHole mod row col =
  find isUserMeta $ listValues mod.modMetaCtx.metas
  where
    isUserMeta : MetaEntry → Bool
    isUserMeta (Unsolved fc _ _ _ User _) = posInFC row col fc
    isUserMeta _ = False

introActions : Maybe MetaEntry → M (List CodeAction)
introActions (Just $ Unsolved fc qn ctx vty User constraints) =
  catchError (do
    -- Are there ever any constraints?
    top <- getTop
    vty <- forceMeta vty
    putStrLn "intros for \{show vty}"
    case vty of
      VPi _ nm Explicit _ a b => do
        let str = "(\\ \{nm} => ?)"
        pure $ Intro str (MkEdit fc str) :: Nil
      _ => do
        -- Prelude.Nat not a vref?
        -- also need to handle pi types
        cons <- getConstructors ctx fc vty
        putStrLn "constructors \{show cons}"
        pure $ map makeEdit cons
  ) $ \ err => do
      putStrLn "Got error in introActions:"
      putStrLn $ showError "" err
      pure Nil
  where

    introDCon : QName × Int × Tm → List String
    introDCon (QN _ nm, _, tm) = go (Lin :< nm) tm
      where
        go : SnocList String → Tm → List String
        go acc (Pi _ nm Explicit _ _ u) = go (acc :< "?") u
        go acc (Pi _ _ _ _ _ u) = go acc u
        go acc _ = acc <>> Nil

    makeEdit : (QName × Int × Tm) → CodeAction
    makeEdit con@(QN _ nm, _, _) =
      let str = unwords $ resugarOper $ introDCon con
      in Intro str $ MkEdit fc $ str

introActions _ = pure Nil

getActions : FileSource → String → Int → Int → M (List CodeAction)
getActions repo modns row col = do
  Just mod <- switchModule repo modns | _ => pure Nil
  top <- getTop
  let infos = filter (posInFC row col ∘ getFC) top.currentMod.modInfos
  putStrLn "Filter got \{show $ length' infos}"
  actions <- go Nil $ infos
  let hole = getHole mod row col
  putStrLn "Hole \{debugStr hole}"
  intros <- introActions $ getHole mod row col
  pure $ actions ++ intros
  where
    getAction : EditorInfo → M (Maybe CodeAction)
    getAction (CaseSplit fc ctx nm scty) = getCaseSplit row col fc ctx nm scty
    getAction (MissingCases fc ctx names) = addMissingCases row col fc ctx names

    go : List CodeAction → List EditorInfo → M (List CodeAction)
    go acc Nil = pure acc
    go acc (x :: xs) = do
      Right (Just res) <- tryError $ getAction x
        | _ => go acc xs
      go (res :: acc) xs