<commit_before>{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
             PatternGuards #-}

module Idris.REPL where

import Idris.AbsSyntax
import Idris.REPLParser
import Idris.ElabDecls
import Idris.ElabTerm
import Idris.Error
import Idris.Delaborate
import Idris.Compiler
import Idris.Prover
import Idris.Parser
import Paths_idris

import Core.Evaluate
import Core.ProofShell
import Core.TT
import Core.Constraints

import System.Console.Haskeline as H
import System.FilePath
import System.Environment
import System.Process
import System.Directory
import System.IO
import Control.Monad
import Control.Monad.State
import Data.List
import Data.Char
import Data.Version

repl :: IState -> [FilePath] -> Idris ()
repl orig mods
   = H.catch
      (do let prompt = mkPrompt mods
          x <- lift $ getInputLine (prompt ++ "> ")
          case x of
              Nothing -> do iputStrLn "Bye bye"
                            return ()
              Just input -> H.catch 
                              (do ms <- processInput input orig mods
                                  case ms of
                                      Just mods -> repl orig mods
                                      Nothing -> return ())
                              ctrlC)
      ctrlC
   where ctrlC :: SomeException -> Idris ()
         ctrlC e = do iputStrLn (show e)
                      repl orig mods

mkPrompt [] = "Idris"
mkPrompt [x] = "*" ++ dropExtension x
mkPrompt (x:xs) = "*" ++ dropExtension x ++ " " ++ mkPrompt xs

lit f = case splitExtension f of
            (_, ".lidr") -> True
            _ -> False

processInput :: String -> IState -> [FilePath] -> Idris (Maybe [FilePath])
processInput cmd orig inputs
    = do i <- get
         let fn = case inputs of
                        (f:_) -> f
                        _ -> ""
         case parseCmd i cmd of
                Left err ->   do liftIO $ print err
                                 return (Just inputs)
                Right Reload -> do put (orig { idris_options = idris_options i })
                                   clearErr
                                   mods <- mapM loadModule inputs  
                                   return (Just inputs)
                Right Edit -> do edit fn orig
                                 return (Just inputs)
                Right AddProof -> do idrisCatch (addProof fn orig)
                                                (\e -> iputStrLn (show e))
                                     return (Just inputs)
                Right Quit -> do iputStrLn "Bye bye"
                                 return Nothing
                Right cmd  -> do idrisCatch (process fn cmd)
                                            (\e -> iputStrLn (show e))
                                 return (Just inputs)

edit :: FilePath -> IState -> Idris ()
edit "" orig = iputStrLn "Nothing to edit"
edit f orig
    = do i <- get
         env <- liftIO $ getEnvironment
         let editor = getEditor env
         let line = case errLine i of
                        Just l -> " +" ++ show l ++ " "
                        Nothing -> " "
         let cmd = editor ++ line ++ f
         liftIO $ system cmd
         clearErr
         put (orig { idris_options = idris_options i })
         loadModule f
         iucheck
         return ()
   where getEditor env | Just ed <- lookup "EDITOR" env = ed
                       | Just ed <- lookup "VISUAL" env = ed
                       | otherwise = "vi"

addProof :: FilePath -> IState -> Idris ()
addProof "" orig = iputStrLn "Nothing to add to"
addProof f orig
    = do let fb = f ++ "~"
         liftIO $ copyFile f fb -- make a backup in case something goes wrong!
         prog <- liftIO $ readFile fb
         i <- get
         case last_proof i of
            Nothing -> iputStrLn "No proof to add"
            Just (n, p) -> do let prog' = insertScript (showProof (lit f) n p) (lines prog)
                              liftIO $ writeFile f (unlines prog')
                              iputStrLn $ "Added proof " ++ show n
                              put (i { last_proof = Nothing })
                              -- lift $ removeFile fb -- uncomment when less scared :)

insertScript :: String -> [String] -> [String]
insertScript prf [] = "\n---------- Proofs ----------" : "" : [prf]
insertScript prf (p@"---------- Proofs ----------" : "" : xs) 
    = p : "" : prf : xs
insertScript prf (x : xs) = x : insertScript prf xs

process :: FilePath -> Command -> Idris ()
process fn Help = iputStrLn displayHelp
process fn (Eval t) 
                 = do (tm, ty) <- elabVal toplevel False t
                      ctxt <- getContext
                      ist <- get 
                      let tm' = normaliseAll ctxt [] tm
                      let ty' = normaliseAll ctxt [] ty
                      logLvl 3 $ "Raw: " ++ show (tm', ty')
                      imp <- impShow
                      iputStrLn (showImp imp (delab ist tm') ++ " : " ++ 
                                 showImp imp (delab ist ty'))
process fn (ExecVal t) 
                    = do (tm, ty) <- elabVal toplevel False t 
--                                         (PApp fc (PRef fc (NS (UN "print") ["prelude"]))
--                                                           [pexp t])
                         (tmpn, tmph) <- liftIO tempfile
                         liftIO $ hClose tmph
                         compile tmpn tm
                         liftIO $ system tmpn
                         return ()
    where fc = FC "(input)" 0 
process fn (Check (PRef _ n))
                  = do ctxt <- getContext
                       ist <- get
                       imp <- impShow
                       case lookupTy Nothing n ctxt of
                        [t] -> iputStrLn $ show n ++ " : " ++
                                  showImp imp (delab ist t)
                        _ -> iputStrLn $ "No such variable " ++ show n
process fn (Check t) = do (tm, ty) <- elabVal toplevel False t
                          ctxt <- getContext
                          ist <- get 
                          imp <- impShow
                          let ty' = normaliseC ctxt [] ty
                          iputStrLn (showImp imp (delab ist tm) ++ " : " ++ 
                                    showImp imp (delab ist ty))
process fn Universes = do i <- get
                          let cs = idris_constraints i
--                        iputStrLn $ showSep "\n" (map show cs)
                          liftIO $ print (map fst cs)
                          let n = length cs
                          iputStrLn $ "(" ++ show n ++ " constraints)"
                          case ucheck cs of
                            Error e -> iputStrLn $ pshow i e
                            OK _ -> iputStrLn "Universes OK"
process fn (Defn n) = do i <- get
                         iputStrLn "Compiled patterns:\n"
                         liftIO $ print (lookupDef Nothing n (tt_ctxt i))
                         case lookupCtxt Nothing n (idris_patdefs i) of
                            [] -> return ()
                            [d] -> do iputStrLn "Original definiton:\n"
                                      mapM_ (printCase i) d
                         case lookupTotal n (tt_ctxt i) of
                            [t] -> iputStrLn (showTotal t i)
                            _ -> return ()
    where printCase i (lhs, rhs) = do liftIO $ putStr $ showImp True (delab i lhs)
                                      liftIO $ putStr " = "
                                      liftIO $ putStrLn $ showImp True (delab i rhs)
process fn (TotCheck n) = do i <- get
                             case lookupTotal n (tt_ctxt i) of
                                [t] -> iputStrLn (showTotal t i)
                                _ -> return ()
process fn (Info n) = do i <- get
                         let oi = lookupCtxt Nothing n (idris_optimisation i)
                         liftIO $ print oi
process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t
                         ctxt <- getContext
                         ist <- get
                         let tm' = specialise ctxt (idris_statics ist) tm
                         iputStrLn (show (delab ist tm'))
process fn (Prove n) = prover (lit fn) n
process fn (HNF t)  = do (tm, ty) <- elabVal toplevel False t
                         ctxt <- getContext
                         ist <- get
                         let tm' = simplify ctxt [] tm
                         iputStrLn (show (delab ist tm'))
process fn TTShell  = do ist <- get
                         let shst = initState (tt_ctxt ist)
                         shst' <- lift $ runShell shst
                         return ()
process fn Execute = do (m, _) <- elabVal toplevel False 
                                        (PApp fc 
                                           (PRef fc (UN "run__IO"))
                                           [pexp $ PRef fc (NS (UN "main") ["main"])])
--                                      (PRef (FC "main" 0) (NS (UN "main") ["main"]))
                        (tmpn, tmph) <- liftIO tempfile
                        liftIO $ hClose tmph
                        compile tmpn m<commit_msg>Recheck totality after an interactive proof<commit_after>{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
             PatternGuards #-}

module Idris.REPL where

import Idris.AbsSyntax
import Idris.REPLParser
import Idris.ElabDecls
import Idris.ElabTerm
import Idris.Error
import Idris.Delaborate
import Idris.Compiler
import Idris.Prover
import Idris.Parser
import Idris.Coverage
import Paths_idris

import Core.Evaluate
import Core.ProofShell
import Core.TT
import Core.Constraints

import System.Console.Haskeline as H
import System.FilePath
import System.Environment
import System.Process
import System.Directory
import System.IO
import Control.Monad
import Control.Monad.State
import Data.List
import Data.Char
import Data.Version

repl :: IState -> [FilePath] -> Idris ()
repl orig mods
   = H.catch
      (do let prompt = mkPrompt mods
          x <- lift $ getInputLine (prompt ++ "> ")
          case x of
              Nothing -> do iputStrLn "Bye bye"
                            return ()
              Just input -> H.catch 
                              (do ms <- processInput input orig mods
                                  case ms of
                                      Just mods -> repl orig mods
                                      Nothing -> return ())
                              ctrlC)
      ctrlC
   where ctrlC :: SomeException -> Idris ()
         ctrlC e = do iputStrLn (show e)
                      repl orig mods

mkPrompt [] = "Idris"
mkPrompt [x] = "*" ++ dropExtension x
mkPrompt (x:xs) = "*" ++ dropExtension x ++ " " ++ mkPrompt xs

lit f = case splitExtension f of
            (_, ".lidr") -> True
            _ -> False

processInput :: String -> IState -> [FilePath] -> Idris (Maybe [FilePath])
processInput cmd orig inputs
    = do i <- get
         let fn = case inputs of
                        (f:_) -> f
                        _ -> ""
         case parseCmd i cmd of
                Left err ->   do liftIO $ print err
                                 return (Just inputs)
                Right Reload -> do put (orig { idris_options = idris_options i })
                                   clearErr
                                   mods <- mapM loadModule inputs  
                                   return (Just inputs)
                Right Edit -> do edit fn orig
                                 return (Just inputs)
                Right AddProof -> do idrisCatch (addProof fn orig)
                                                (\e -> iputStrLn (show e))
                                     return (Just inputs)
                Right Quit -> do iputStrLn "Bye bye"
                                 return Nothing
                Right cmd  -> do idrisCatch (process fn cmd)
                                            (\e -> iputStrLn (show e))
                                 return (Just inputs)

edit :: FilePath -> IState -> Idris ()
edit "" orig = iputStrLn "Nothing to edit"
edit f orig
    = do i <- get
         env <- liftIO $ getEnvironment
         let editor = getEditor env
         let line = case errLine i of
                        Just l -> " +" ++ show l ++ " "
                        Nothing -> " "
         let cmd = editor ++ line ++ f
         liftIO $ system cmd
         clearErr
         put (orig { idris_options = idris_options i })
         loadModule f
         iucheck
         return ()
   where getEditor env | Just ed <- lookup "EDITOR" env = ed
                       | Just ed <- lookup "VISUAL" env = ed
                       | otherwise = "vi"

addProof :: FilePath -> IState -> Idris ()
addProof "" orig = iputStrLn "Nothing to add to"
addProof f orig
    = do let fb = f ++ "~"
         liftIO $ copyFile f fb -- make a backup in case something goes wrong!
         prog <- liftIO $ readFile fb
         i <- get
         case last_proof i of
            Nothing -> iputStrLn "No proof to add"
            Just (n, p) -> do let prog' = insertScript (showProof (lit f) n p) (lines prog)
                              liftIO $ writeFile f (unlines prog')
                              iputStrLn $ "Added proof " ++ show n
                              put (i { last_proof = Nothing })
                              -- lift $ removeFile fb -- uncomment when less scared :)

insertScript :: String -> [String] -> [String]
insertScript prf [] = "\n---------- Proofs ----------" : "" : [prf]
insertScript prf (p@"---------- Proofs ----------" : "" : xs) 
    = p : "" : prf : xs
insertScript prf (x : xs) = x : insertScript prf xs

process :: FilePath -> Command -> Idris ()
process fn Help = iputStrLn displayHelp
process fn (Eval t) 
                 = do (tm, ty) <- elabVal toplevel False t
                      ctxt <- getContext
                      ist <- get 
                      let tm' = normaliseAll ctxt [] tm
                      let ty' = normaliseAll ctxt [] ty
                      logLvl 3 $ "Raw: " ++ show (tm', ty')
                      imp <- impShow
                      iputStrLn (showImp imp (delab ist tm') ++ " : " ++ 
                                 showImp imp (delab ist ty'))
process fn (ExecVal t) 
                    = do (tm, ty) <- elabVal toplevel False t 
--                                         (PApp fc (PRef fc (NS (UN "print") ["prelude"]))
--                                                           [pexp t])
                         (tmpn, tmph) <- liftIO tempfile
                         liftIO $ hClose tmph
                         compile tmpn tm
                         liftIO $ system tmpn
                         return ()
    where fc = FC "(input)" 0 
process fn (Check (PRef _ n))
                  = do ctxt <- getContext
                       ist <- get
                       imp <- impShow
                       case lookupTy Nothing n ctxt of
                        [t] -> iputStrLn $ show n ++ " : " ++
                                  showImp imp (delab ist t)
                        _ -> iputStrLn $ "No such variable " ++ show n
process fn (Check t) = do (tm, ty) <- elabVal toplevel False t
                          ctxt <- getContext
                          ist <- get 
                          imp <- impShow
                          let ty' = normaliseC ctxt [] ty
                          iputStrLn (showImp imp (delab ist tm) ++ " : " ++ 
                                    showImp imp (delab ist ty))
process fn Universes = do i <- get
                          let cs = idris_constraints i
--                        iputStrLn $ showSep "\n" (map show cs)
                          liftIO $ print (map fst cs)
                          let n = length cs
                          iputStrLn $ "(" ++ show n ++ " constraints)"
                          case ucheck cs of
                            Error e -> iputStrLn $ pshow i e
                            OK _ -> iputStrLn "Universes OK"
process fn (Defn n) = do i <- get
                         iputStrLn "Compiled patterns:\n"
                         liftIO $ print (lookupDef Nothing n (tt_ctxt i))
                         case lookupCtxt Nothing n (idris_patdefs i) of
                            [] -> return ()
                            [d] -> do iputStrLn "Original definiton:\n"
                                      mapM_ (printCase i) d
                         case lookupTotal n (tt_ctxt i) of
                            [t] -> iputStrLn (showTotal t i)
                            _ -> return ()
    where printCase i (lhs, rhs) = do liftIO $ putStr $ showImp True (delab i lhs)
                                      liftIO $ putStr " = "
                                      liftIO $ putStrLn $ showImp True (delab i rhs)
process fn (TotCheck n) = do i <- get
                             case lookupTotal n (tt_ctxt i) of
                                [t] -> iputStrLn (showTotal t i)
                                _ -> return ()
process fn (Info n) = do i <- get
                         let oi = lookupCtxt Nothing n (idris_optimisation i)
                         liftIO $ print oi
process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t
                         ctxt <- getContext
                         ist <- get
                         let tm' = specialise ctxt (idris_statics ist) tm
                         iputStrLn (show (delab ist tm'))
process fn (Prove n) = do prover (lit fn) n
                          -- recheck totality
                          i <- get
                          totcheck (FC "(input)" 0, n)
                          mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)
                          mapM_ checkDeclTotality (idris_totcheck i)
process fn (HNF t)  = do (tm, ty) <- elabVal toplevel False t
                         ctxt <- getContext
                         ist <- get
                         let tm' = simplify ctxt [] tm
                         iputStrLn (show (delab ist tm'))
process fn TTShell  = do ist <- get
                         let shst = initState (tt_ctxt ist)
                         shst' <- lift $ runShell shst
                         return ()
process fn Execute = do (m, _) <- elabVal toplevel False 
                                        (PApp fc 
                                           (PRef fc (UN "run__IO"))
                                           [pexp $ PRef fc (NS (UN "main") ["main"])])
--                                      (PRef (FC "main" 0) (NS (UN "main") ["main"]))
                        (tmpn, tmph) <- liftIO tempfile
                        liftIO $ hClose tmph
                        compile tmpn m
{'fraction_non_alphanumeric': 0.0874074074074074, 'fraction_numerical': 0.00037037037037037035, 'mean_word_length': 1.0431304723813641, 'pattern_counts': {'":': 0, '<': 78, '<?xml version=': 0, '>': 94, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 82, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6566625', 'n_tokens_mistral': 5012, 'n_tokens_neox': 4721, 'n_words': 1695}