content: {-|
  Module      : Idris.Interactive
  Description : Bits and pieces for editing source files interactively, called from the REPL
  
  License     : BSD3
  Maintainer  : The Idris Community.
  -}
  
  {-# LANGUAGE PatternGuards #-}
  
  module Idris.Interactive(
      caseSplitAt, addClauseFrom, addProofClauseFrom
    , addMissing, makeWith, makeCase, doProofSearch
    , makeLemma
    ) where
  
  import Idris.AbsSyntax
  import Idris.CaseSplit
  import Idris.Core.Evaluate
  import Idris.Core.TT
  import Idris.Delaborate
  import Idris.Elab.Term
  import Idris.Elab.Value
  import Idris.ElabDecls
  import Idris.Error
  import Idris.ErrReverse
  import Idris.IdeMode hiding (IdeModeCommand(..))
  import Idris.Output
  
  import Util.Pretty
  import Util.System
  
  import Data.Char
  import Data.List (isSuffixOf)
  import System.Directory
  import System.IO
  
  caseSplitAt :: FilePath -> Bool -> Int -> Name -> Idris ()
  caseSplitAt fn updatefile l n
     = do src <- runIO $ readSourceStrict fn
          (ok, res) <- splitOnLine l n fn
          logLvl 1 (showSep "\n" (map show res))
          let (before, (ap : later)) = splitAt (l-1) (lines src)
          res' <- replaceSplits ap res (not ok)
          let new = concat res'
          if updatefile
            then do let fb = fn ++ "~" -- make a backup!
                    runIO $ writeSource fb (unlines before ++ new ++ unlines later)
                    runIO $ copyFile fb fn
            else -- do iputStrLn (show res)
              iPrintResult new
  
  addClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()
  addClauseFrom fn updatefile l n = do
      -- if a definition already exists, add missing cases rather than
      -- adding a new definition.
      ist <- getIState
      cl <- getInternalApp fn l
      let fulln = getAppName cl
      let metavars = lookup fulln (idris_metavars ist)
      case metavars of
        Nothing -> addMissing fn updatefile l n
        Just _ -> do
          src <- runIO $ readSourceStrict fn
          let (before, tyline : later) = splitAt (l-1) (lines src)
          let indent = getIndent 0 (show n) tyline
          cl <- getClause l fulln n fn
          -- add clause before first blank line in 'later'
          let (nonblank, rest) = span (not . all isSpace) (tyline:later)
          if updatefile
            then do let fb = fn ++ "~"
                    runIO $ writeSource fb (unlines (before ++ nonblank) ++
                                          replicate indent ' ' ++
                                          cl ++ "\n" ++
                                          unlines rest)
                    runIO $ copyFile fb fn
            else iPrintResult cl
    where
      getIndent i n [] = 0
      getIndent i n xs | take 9 xs == "implementation " = i
      getIndent i n xs | take (length n) xs == n = i
      getIndent i n (x : xs) = getIndent (i + 1) n xs
  
      getAppName (PApp _ r _) = getAppName r
      getAppName (PRef _ _ r) = r
      getAppName (PTyped n _) = getAppName n
      getAppName _ = n
  
  addProofClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()
  addProofClauseFrom fn updatefile l n
     = do src <- runIO $ readSourceStrict fn
          let (before, tyline : later) = splitAt (l-1) (lines src)
          let indent = getIndent 0 (show n) tyline
          cl <- getProofClause l n fn
          -- add clause before first blank line in 'later'
          let (nonblank, rest) = span (not . all isSpace) (tyline:later)
          if updatefile
            then do let fb = fn ++ "~"
                    runIO $ writeSource fb (unlines (before ++ nonblank) ++
                                          replicate indent ' ' ++
                                          cl ++ "\n" ++
                                          unlines rest)
                    runIO $ copyFile fb fn
            else iPrintResult cl
      where
         getIndent i n [] = 0
         getIndent i n xs | take (length n) xs == n = i
         getIndent i n (x : xs) = getIndent (i + 1) n xs
  
  addMissing :: FilePath -> Bool -> Int -> Name -> Idris ()
  addMissing fn updatefile l n
     = do src <- runIO $ readSourceStrict fn
          let (before, tyline : later) = splitAt (l-1) (lines src)
          let indent = getIndent tyline
          i <- getIState
          cl <- getInternalApp fn l
          let n' = getAppName cl
  
          extras <- case lookupCtxtExact n' (idris_patdefs i) of
                         Nothing -> return ""
                         Just (_, tms) -> do tms' <- nameMissing tms
                                             showNew (show n ++ "_rhs") 1 indent tms'
          let (nonblank, rest) = span (not . all isSpace) (tyline:later)
          if updatefile
            then do let fb = fn ++ "~"
                    runIO $ writeSource fb (unlines (before ++ nonblank)
                                          ++ extras
                                          ++ (if null extras then "" else "\n")
                                          ++ unlines rest)
                    runIO $ (length src `seq` copyFile fb fn)
            else iPrintResult extras
      where showPat = show . stripNS
            stripNS tm = mapPT dens tm where
                dens (PRef fc hls n) = PRef fc hls (nsroot n)
                dens t = t
  
            nsroot (NS n _) = nsroot n
            nsroot (SN (WhereN _ _ n)) = nsroot n
            nsroot n = n
  
            getAppName (PApp _ r _) = getAppName r
            getAppName (PRef _ _ r) = r
            getAppName (PTyped n _) = getAppName n
            getAppName _ = n
  
            makeIndent ind | ".lidr" `isSuffixOf` fn = '>' : ' ' : replicate (ind-2) ' '
                           | otherwise               = replicate ind ' '
  
            showNew nm i ind (tm : tms)
                          = do (nm', i') <- getUniq nm i
                               rest <- showNew nm i' ind tms
                               return (makeIndent ind ++
                                       showPat tm ++ " = ?" ++ nm' ++
                                       (if null rest then "" else
                                           "\n" ++ rest))
            showNew nm i _ [] = return ""
  
            getIndent s = length (takeWhile isSpace s)
  
  
  makeWith :: FilePath -> Bool -> Int -> Name -> Idris ()
  makeWith fn updatefile l n = do
    src <- runIO $ readSourceStrict fn
    i <- getIState
    indentWith <- getIndentWith
    let (before, tyline : later) = splitAt (l-1) (lines src)
    let ind = getIndent tyline
  --  runIO . traceIO $ "indentWith = " ++ show indentWith
    let with = mkWith tyline n indentWith
    -- add clause before first blank line in 'later',
    -- or (TODO) before first line with same indentation as tyline
    let (nonblank, rest) = span (\x -> not (all isSpace x) &&
                                       not (ind == getIndent x)) later
    if updatefile
      then do
        let fb = fn ++ "~"
        runIO $ writeSource fb (unlines (before ++ nonblank) ++
                                with ++ "\n" ++ unlines rest)
        runIO $ copyFile fb fn
      else iPrintResult (with ++ "\n")
    where getIndent s = length (takeWhile isSpace s)
  
  -- Replace the given metavariable on the given line with a 'case'
  -- block, using a _ for the scrutinee
  makeCase :: FilePath -> Bool -> Int -> Name -> Idris ()
  makeCase fn updatefile l n
     = do src <- runIO $ readSourceStrict fn
          let (before, tyline : later) = splitAt (l-1) (lines src)
          let newcase = addCaseSkel (show n) tyline
  
          if updatefile then
             do let fb = fn ++ "~"
                runIO $ writeSource fb (unlines (before ++ newcase ++ later))
                runIO $ copyFile fb fn
             else iPrintResult (showSep "\n" newcase ++"\n")
    where addCaseSkel n line =
              let b = brackets False line in
              case findSubstr ('?':n) line of
                   Just (before, pos, after) ->
                        [before ++ (if b then "(" else "") ++ "case _ of",
                         take (pos + (if b then 6 else 5)) (repeat ' ') ++
                               "case_val => ?" ++ n ++ (if b then ")" else "")
                               ++ after]
                   Nothing -> fail "No such metavariable"
  
          -- Assume case needs to be bracketed unless the metavariable is
          -- on its own after an =
          brackets eq line | line == '?' : show n = not eq
          brackets eq ('=':ls) = brackets True ls
          brackets eq (' ':ls) = brackets eq ls
          brackets eq (l : ls) = brackets False ls
          brackets eq [] = True
  
          findSubstr n xs = findSubstr' [] 0 n xs
  
          findSubstr' acc i n xs | take (length n) xs == n
                  = Just (reverse acc, i, drop (length n) xs)
          findSubstr' acc i n [] = Nothing
          findSubstr' acc i n (x : xs) = findSubstr' (x : acc) (i + 1) n xs
  
  
  doProofSearch :: FilePath -> Bool -> Bool ->
                   Int -> Name -> [Name] -> Maybe Int -> Idris ()
  doProofSearch fn updatefile rec l n hints Nothing
      = doProofSearch fn updatefile rec l n hints (Just 20)
  doProofSearch fn updatefile rec l n hints (Just depth)
      = do src <- runIO $ readSourceStrict fn
           let (before, tyline : later) = splitAt (l-1) (lines src)
           ctxt <- getContext
           mn <- case lookupNames n ctxt of
                      [x] -> return x
                      [] -> return n
                      ns -> ierror (CantResolveAlts ns)
           i <- getIState
           let (top, envlen, psnames)
                = case lookup mn (idris_metavars i) of
                       Just (t, e, ns, False, d) -> (t, e, ns)
                       _ -> (Nothing, 0, [])
           let fc = fileFC fn
           let body t = PProof [Try (TSeq Intros (ProofSearch rec False depth t psnames hints))
                                    (ProofSearch rec False depth t psnames hints)]
           let def = PClause fc mn (PRef fc [] mn) [] (body top) []
           newmv_pre <- idrisCatch
               (do elabDecl' EAll (recinfo (fileFC "proofsearch")) (PClauses fc [] mn [def])
                   (tm, ty) <- elabVal (recinfo (fileFC "proofsearch")) ERHS (PRef fc [] mn)
                   ctxt <- getContext
                   i <- getIState
                   return . flip displayS "" . renderPretty 1.0 80 $
                     pprintPTerm defaultPPOption [] [] (idris_infixes i)
                       (stripNS
                          (dropCtxt envlen
                             (delab i (fst (specialise ctxt [] [(mn, 1)] tm))))))
               (\e -> return ("?" ++ show n))
           let newmv = guessBrackets False tyline (show n) newmv_pre
           if updatefile then
              do let fb = fn ++ "~"
                 runIO $ writeSource fb (unlines before ++
                                       updateMeta tyline (show n) newmv ++ "\n"
                                         ++ unlines later)
                 runIO $ copyFile fb fn
              else iPrintResult newmv
      where dropCtxt 0 sc = sc
            dropCtxt i (PPi _ _ _ _ sc) = dropCtxt (i - 1) sc
            dropCtxt i (PLet _ _ _ _ _ _ sc) = dropCtxt (i - 1) sc
            dropCtxt i (PLam _ _ _ _ sc) = dropCtxt (i - 1) sc
            dropCtxt _ t = t
  
            stripNS tm = mapPT dens tm where
                dens (PRef fc hls n) = PRef fc hls (nsroot n)
                dens t = t
  
            nsroot (NS n _) = nsroot n
            nsroot (SN (WhereN _ _ n)) = nsroot n
            nsroot n = n
  
  updateMeta ('?':cs) n new
      | length cs >= length n
        = case splitAt (length n) cs of
               (mv, c:cs) ->
                    if ((isSpace c || c == ')' || c == '}') && mv == n)
                       then new ++ (c : cs)
                       else '?' : mv ++ c : updateMeta cs n new
               (mv, []) -> if (mv == n) then new else '?' : mv
  updateMeta ('=':'>':cs) n new = '=':'>':updateMeta cs n new
  updateMeta ('=':cs) n new = '=':updateMeta cs n new
  updateMeta (c:cs) n new
    = c : updateMeta cs n new
  updateMeta [] n new = ""
  
  guessBrackets brack ('?':cs) n new
      | length cs >= length n
        = case splitAt (length n) cs of
               (mv, c:cs) ->
                    if ((isSpace c || c == ')' || c == '}') && mv == n)
                       then addBracket brack new
                       else guessBrackets True cs n new
               (mv, []) -> if (mv == n) then addBracket brack new else '?' : mv
  guessBrackets brack ('=':'>':cs) n new = guessBrackets False cs n new
  guessBrackets brack ('-':'>':cs) n new = guessBrackets False cs n new
  guessBrackets brack ('=':cs) n new = guessBrackets False cs n new
  guessBrackets brack (c:cs) n new
    = guessBrackets (brack || not (isSpace c)) cs n new
  guessBrackets brack [] n new = ""
  
  checkProv line n = isProv' False line n
    where
      isProv' p cs n | take (length n) cs == n = p
      isProv' _ ('?':cs) n = isProv' False cs n
      isProv' _ ('{':cs) n = isProv' True cs n
      isProv' _ ('}':cs) n = isProv' True cs n
      isProv' p (_:cs) n = isProv' p cs n
      isProv' _ [] n = False
  
  addBracket False new = new
  addBracket True new@('(':xs) | last xs == ')' = new
  addBracket True new | any isSpace new = '(' : new ++ ")"
                      | otherwise = new
  
  
  makeLemma :: FilePath -> Bool -> Int -> Name -> Idris ()
  makeLemma fn updatefile l n
     = do src <- runIO $ readSourceStrict fn
          let (before, tyline : later) = splitAt (l-1) (lines src)
  
          -- if the name is in braces, rather than preceded by a ?, treat it
          -- as a lemma in a provisional definition
  
          let isProv = checkProv tyline (show n)
  
          ctxt <- getContext
          (fname, mty_full) <- case lookupTyName n ctxt of
                                    [t] -> return t
                                    [] -> ierror (NoSuchVariable n)
                                    ns -> ierror (CantResolveAlts (map fst ns))
  
          i <- getIState
          let mty = errReverse i mty_full
  
          margs <- case lookup fname (idris_metavars i) of
                        Just (_, arity, _, _, _) -> return arity
                        _ -> return (-1)
  
          if (not isProv) then do
              let skip = guessImps i (tt_ctxt i) mty
              let impty = stripMNBind skip margs (delab i mty)
              let interfaces = guessInterfaces i (tt_ctxt i) [] (allNamesIn impty) mty
  
              let lem = show n ++ " : " ++
                              constraints i interfaces mty ++
                              showTmOpts (defaultPPOption { ppopt_pinames = True })
                                         impty
              let lem_app = guessBrackets False tyline (show n) (show n ++ appArgs skip margs mty)
  
              if updatefile then
                 do let fb = fn ++ "~"
                    runIO $ writeSource fb (addLem before tyline lem lem_app later)
                    runIO $ copyFile fb fn
                 else case idris_outputmode i of
                        RawOutput _  -> iPrintResult $ lem ++ "\n" ++ lem_app
                        IdeMode n h ->
                          let good = SexpList [SymbolAtom "ok",
                                               SexpList [SymbolAtom "metavariable-lemma",
                                                         SexpList [SymbolAtom "replace-metavariable",
                                                                   StringAtom lem_app],
                                                         SexpList [SymbolAtom "definition-type",
                                                                   StringAtom lem]]]
                          in runIO . hPutStrLn h $ convSExp "return" good n
  
            else do -- provisional definition
              let lem_app = show n ++ appArgs [] (-1) mty ++
                                   " = ?" ++ show n ++ "_rhs"
              if updatefile then
                 do let fb = fn ++ "~"
                    runIO $ writeSource fb (addProv before tyline lem_app later)
                    runIO $ copyFile fb fn
                 else case idris_outputmode i of
                        RawOutput _  -> iPrintResult lem_app
                        IdeMode n h ->
                          let good = SexpList [SymbolAtom "ok",
                                               SexpList [SymbolAtom "provisional-definition-lemma",
                                                         SexpList [SymbolAtom "definition-clause",
                                                                   StringAtom lem_app]]]
                          in runIO . hPutStrLn h $ convSExp "return" good n
  
    where appArgs skip 0 _ = ""
          appArgs skip i (Bind n@(UN c) (Pi _ _ _ _) sc)
             | (thead c /= '_' && n `notElem` skip)
                  = " " ++ show n ++ appArgs skip (i - 1) sc
          appArgs skip i (Bind _ (Pi _ _ _ _) sc) = appArgs skip (i - 1) sc
          appArgs skip i _ = ""
  
          stripMNBind _ args t | args <= 0 = stripImp t
          stripMNBind skip args (PPi b n@(UN c) _ ty sc)
             | n `notElem` skip ||
                 take 4 (str c) == "__pi" -- keep in type, but not in app
                  = PPi b n NoFC (stripImp ty) (stripMNBind skip (args - 1) sc)
          stripMNBind skip args (PPi b _ _ ty sc) = stripMNBind skip (args - 1) sc
          stripMNBind skip args t = stripImp t
  
          stripImp (PApp fc f as) = PApp fc (stripImp f) (map placeholderImp as)
            where
              placeholderImp tm@(PImp _ _ _ _ _) = tm { getTm = Placeholder }
              placeholderImp tm = tm { getTm = stripImp (getTm tm) }
          stripImp (PPi b n f ty sc) = PPi b n f (stripImp ty) (stripImp sc)
          stripImp t = t
  
          constraints :: IState -> [Name] -> Type -> String
          constraints i [] ty = ""
          constraints i [n] ty = showSep ", " (showConstraints i [n] ty) ++ " => "
          constraints i ns ty = "(" ++ showSep ", " (showConstraints i ns ty) ++ ") => "
  
          showConstraints i ns (Bind n (Pi _ _ ty _) sc)
              | n `elem` ns = show (delab i ty) :
                                showConstraints i ns (substV (P Bound n Erased) sc)
              | otherwise = showConstraints i ns (substV (P Bound n Erased) sc)
          showConstraints _ _ _ = []
  
          -- Guess which binders should be implicits in the generated lemma.
          -- Make them implicit if they appear guarded by a top level constructor,
          -- or at the top level themselves.
          -- Also, make interface implementations implicit
          guessImps :: IState -> Context -> Term -> [Name]
          -- machine names aren't lifted
          guessImps ist ctxt (Bind n@(MN _ _) (Pi _ _ ty _) sc)
             = n : guessImps ist ctxt sc
          guessImps ist ctxt (Bind n (Pi _ _ ty _) sc)
             | guarded ctxt n (substV (P Bound n Erased) sc)
                  = n : guessImps ist ctxt sc
             | isInterface ist ty
                  = n : guessImps ist ctxt sc
             | paramty ty = n : guessImps ist ctxt sc
             | ignoreName n = n : guessImps ist ctxt sc
             | otherwise = guessImps ist ctxt sc
          guessImps ist ctxt _ = []
  
          paramty (TType _) = True
          paramty (Bind _ (Pi _ _ (TType _) _) sc) = paramty sc
          paramty _ = False
  
          -- TMP HACK unusable name so don't lift
          ignoreName n = case show n of
                              "_aX" -> True
                              _ -> False
  
          guessInterfaces :: IState -> Context -> [Name] -> [Name] -> Term -> [Name]
          guessInterfaces ist ctxt binders usednames (Bind n (Pi _ _ ty _) sc)
             | isParamInterface ist ty && any (\x -> elem x usednames)
                                              (paramNames binders ty)
                  = n : guessInterfaces ist ctxt (n : binders) usednames sc
             | otherwise = guessInterfaces ist ctxt (n : binders) usednames sc
          guessInterfaces ist ctxt _ _ _ = []
  
          paramNames bs ty | (P _ _ _, args) <- unApply ty
               = vnames args
            where vnames [] = []
                  vnames (V i : xs) | i < length bs = bs !! i : vnames xs
                  vnames (_ : xs) = vnames xs
  
          isInterface ist t
             | (P _ n _, args) <- unApply t
                  = case lookupCtxtExact n (idris_interfaces ist) of
                         Just _ -> True
                         _ -> False
             | otherwise = False
  
          isParamInterface ist t
             | (P _ n _, args) <- unApply t
                  = case lookupCtxtExact n (idris_interfaces ist) of
                         Just _ -> any isV args
                         _ -> False
             | otherwise = False
            where isV (V _) = True
                  isV _ = False
  
          guarded ctxt n (P _ n' _) | n == n' = True
          guarded ctxt n ap@(App _ _ _)
              | (P _ f _, args) <- unApply ap,
                isConName f ctxt = any (guarded ctxt n) args
  --         guarded ctxt n (Bind (UN cn) (Pi t) sc) -- ignore shadows
  --             | thead cn /= '_' = guarded ctxt n t || guarded ctxt n sc
          guarded ctxt n (Bind _ (Pi _ _ t _) sc)
              = guarded ctxt n t || guarded ctxt n sc
          guarded ctxt n _ = False
  
          blank = all isSpace
  
          addLem before tyline lem lem_app later
              = let (bef_end, blankline : bef_start)
                         = case span (not . blank) (reverse before) of
                                (bef, []) -> (bef, [""])
                                x -> x
                    mvline = updateMeta tyline (show n) lem_app in
                  unlines $ reverse bef_start ++
                            [blankline, lem, blankline] ++
                            reverse bef_end ++ mvline : later
  
          addProv before tyline lem_app later
              = let (later_bef, blankline : later_end)
                        = case span (not . blank) later of
                               (bef, []) -> (bef, [""])
                               x -> x in
                    unlines $ before ++ tyline :
                              (later_bef ++ [blankline, lem_app, blankline] ++
                                        later_end)
  