{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- | @futhark repl@
module Futhark.CLI.REPL (main) where

import Control.Exception
import Control.Monad
import Control.Monad.Except
import Control.Monad.Free.Church
import Control.Monad.State
import Data.Char
import Data.List (intercalate, intersperse)
import qualified Data.List.NonEmpty as NE
import qualified Data.Map as M
import Data.Maybe
import qualified Data.Text as T
import qualified Data.Text.IO as T
import Data.Version
import Futhark.Compiler
import Futhark.MonadFreshNames
import Futhark.Util (fancyTerminal)
import Futhark.Util.Options
import Futhark.Version
import Language.Futhark
import qualified Language.Futhark.Interpreter as I
import Language.Futhark.Parser
import qualified Language.Futhark.Semantic as T
import qualified Language.Futhark.TypeChecker as T
import NeatInterpolation (text)
import qualified System.Console.Haskeline as Haskeline
import System.Directory
import System.FilePath
import Text.Read (readMaybe)

banner :: String
 =
  [String] -> String
unlines
    [ String
"|// |\\    |   |\\  |\\   /",
      String
"|/  | \\   |\\  |\\  |/  /",
      String
"|   |  \\  |/  |   |\\  \\",
      String
"|   |   \\ |   |   | \\  \\"
    ]

-- | Run @futhark repl@.
main :: String -> [String] -> IO ()
main :: String -> [String] -> IO ()
main = ()
-> [FunOptDescr ()]
-> String
-> ([String] -> () -> Maybe (IO ()))
-> String
-> [String]
-> IO ()
forall cfg.
cfg
-> [FunOptDescr cfg]
-> String
-> ([String] -> cfg -> Maybe (IO ()))
-> String
-> [String]
-> IO ()
mainWithOptions () [] String
"options... [program.fut]" [String] -> () -> Maybe (IO ())
forall p. [String] -> p -> Maybe (IO ())
run
  where
    run :: [String] -> p -> Maybe (IO ())
run [] p
_ = IO () -> Maybe (IO ())
forall a. a -> Maybe a
Just (IO () -> Maybe (IO ())) -> IO () -> Maybe (IO ())
forall a b. (a -> b) -> a -> b
$ Maybe String -> IO ()
repl Maybe String
forall a. Maybe a
Nothing
    run [String
prog] p
_ = IO () -> Maybe (IO ())
forall a. a -> Maybe a
Just (IO () -> Maybe (IO ())) -> IO () -> Maybe (IO ())
forall a b. (a -> b) -> a -> b
$ Maybe String -> IO ()
repl (Maybe String -> IO ()) -> Maybe String -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just String
prog
    run [String]
_ p
_ = Maybe (IO ())
forall a. Maybe a
Nothing

data StopReason = EOF | Stop | Exit | Load FilePath | Interrupt

repl :: Maybe FilePath -> IO ()
repl :: Maybe String -> IO ()
repl Maybe String
maybe_prog = do
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
fancyTerminal (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
    String -> IO ()
putStr String
banner
    String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Version " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Version -> String
showVersion Version
version String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"."
    String -> IO ()
putStrLn String
"Copyright (C) DIKU, University of Copenhagen, released under the ISC license."
    String -> IO ()
putStrLn String
""
    String -> IO ()
putStrLn String
"Run :help for a list of commands."
    String -> IO ()
putStrLn String
""

  let toploop :: FutharkiState -> InputT IO ()
toploop FutharkiState
s = do
        (Either StopReason Any
stop, FutharkiState
s') <-
          InputT IO (Either StopReason Any, FutharkiState)
-> InputT IO (Either StopReason Any, FutharkiState)
-> InputT IO (Either StopReason Any, FutharkiState)
forall (m :: * -> *) a. MonadMask m => m a -> m a -> m a
Haskeline.handleInterrupt ((Either StopReason Any, FutharkiState)
-> InputT IO (Either StopReason Any, FutharkiState)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StopReason -> Either StopReason Any
forall a b. a -> Either a b
Left StopReason
Interrupt, FutharkiState
s))
            (InputT IO (Either StopReason Any, FutharkiState)
 -> InputT IO (Either StopReason Any, FutharkiState))
-> (InputT IO (Either StopReason Any, FutharkiState)
    -> InputT IO (Either StopReason Any, FutharkiState))
-> InputT IO (Either StopReason Any, FutharkiState)
-> InputT IO (Either StopReason Any, FutharkiState)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InputT IO (Either StopReason Any, FutharkiState)
-> InputT IO (Either StopReason Any, FutharkiState)
forall (m :: * -> *) a.
(MonadIO m, MonadMask m) =>
InputT m a -> InputT m a
Haskeline.withInterrupt
            (InputT IO (Either StopReason Any, FutharkiState)
 -> InputT IO (Either StopReason Any, FutharkiState))
-> InputT IO (Either StopReason Any, FutharkiState)
-> InputT IO (Either StopReason Any, FutharkiState)
forall a b. (a -> b) -> a -> b
$ StateT FutharkiState (InputT IO) (Either StopReason Any)
-> FutharkiState
-> InputT IO (Either StopReason Any, FutharkiState)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (ExceptT StopReason (StateT FutharkiState (InputT IO)) Any
-> StateT FutharkiState (InputT IO) (Either StopReason Any)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT StopReason (StateT FutharkiState (InputT IO)) Any
 -> StateT FutharkiState (InputT IO) (Either StopReason Any))
-> ExceptT StopReason (StateT FutharkiState (InputT IO)) Any
-> StateT FutharkiState (InputT IO) (Either StopReason Any)
forall a b. (a -> b) -> a -> b
$ FutharkiM Any
-> ExceptT StopReason (StateT FutharkiState (InputT IO)) Any
forall a.
FutharkiM a
-> ExceptT StopReason (StateT FutharkiState (InputT IO)) a
runFutharkiM (FutharkiM Any
 -> ExceptT StopReason (StateT FutharkiState (InputT IO)) Any)
-> FutharkiM Any
-> ExceptT StopReason (StateT FutharkiState (InputT IO)) Any
forall a b. (a -> b) -> a -> b
$ FutharkiM () -> FutharkiM Any
forall (f :: * -> *) a b. Applicative f => f a -> f b
forever FutharkiM ()
readEvalPrint) FutharkiState
s

        case Either StopReason Any
stop of
          Left StopReason
Stop -> FutharkiState -> InputT IO ()
finish FutharkiState
s'
          Left StopReason
EOF -> FutharkiState -> InputT IO ()
finish FutharkiState
s'
          Left StopReason
Exit -> FutharkiState -> InputT IO ()
finish FutharkiState
s'
          Left StopReason
Interrupt -> do
            IO () -> InputT IO ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> InputT IO ()) -> IO () -> InputT IO ()
forall a b. (a -> b) -> a -> b
$ Text -> IO ()
T.putStrLn Text
"Interrupted"
            FutharkiState -> InputT IO ()
toploop FutharkiState
s' {futharkiCount :: Int
futharkiCount = FutharkiState -> Int
futharkiCount FutharkiState
s' Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1}
          Left (Load String
file) -> do
            IO () -> InputT IO ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> InputT IO ()) -> IO () -> InputT IO ()
forall a b. (a -> b) -> a -> b
$ Text -> IO ()
T.putStrLn (Text -> IO ()) -> Text -> IO ()
forall a b. (a -> b) -> a -> b
$ Text
"Loading " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack String
file
            Either String FutharkiState
maybe_new_state <-
              IO (Either String FutharkiState)
-> InputT IO (Either String FutharkiState)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either String FutharkiState)
 -> InputT IO (Either String FutharkiState))
-> IO (Either String FutharkiState)
-> InputT IO (Either String FutharkiState)
forall a b. (a -> b) -> a -> b
$ Int
-> LoadedProg -> Maybe String -> IO (Either String FutharkiState)
newFutharkiState (FutharkiState -> Int
futharkiCount FutharkiState
s) (FutharkiState -> LoadedProg
futharkiProg FutharkiState
s) (Maybe String -> IO (Either String FutharkiState))
-> Maybe String -> IO (Either String FutharkiState)
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just String
file
            case Either String FutharkiState
maybe_new_state of
              Right FutharkiState
new_state -> FutharkiState -> InputT IO ()
toploop FutharkiState
new_state
              Left String
err -> do
                IO () -> InputT IO ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> InputT IO ()) -> IO () -> InputT IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
err
                FutharkiState -> InputT IO ()
toploop FutharkiState
s'
          Right Any
_ -> () -> InputT IO ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

      finish :: FutharkiState -> InputT IO ()
finish FutharkiState
s = do
        Bool
quit <- if Bool
fancyTerminal then InputT IO Bool
confirmQuit else Bool -> InputT IO Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
        if Bool
quit then () -> InputT IO ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure () else FutharkiState -> InputT IO ()
toploop FutharkiState
s

  Either String FutharkiState
maybe_init_state <- IO (Either String FutharkiState)
-> IO (Either String FutharkiState)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either String FutharkiState)
 -> IO (Either String FutharkiState))
-> IO (Either String FutharkiState)
-> IO (Either String FutharkiState)
forall a b. (a -> b) -> a -> b
$ Int
-> LoadedProg -> Maybe String -> IO (Either String FutharkiState)
newFutharkiState Int
0 LoadedProg
noLoadedProg Maybe String
maybe_prog
  FutharkiState
s <- case Either String FutharkiState
maybe_init_state of
    Left String
prog_err -> do
      Either String FutharkiState
noprog_init_state <- IO (Either String FutharkiState)
-> IO (Either String FutharkiState)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either String FutharkiState)
 -> IO (Either String FutharkiState))
-> IO (Either String FutharkiState)
-> IO (Either String FutharkiState)
forall a b. (a -> b) -> a -> b
$ Int
-> LoadedProg -> Maybe String -> IO (Either String FutharkiState)
newFutharkiState Int
0 LoadedProg
noLoadedProg Maybe String
forall a. Maybe a
Nothing
      case Either String FutharkiState
noprog_init_state of
        Left String
err ->
          String -> IO FutharkiState
forall a. HasCallStack => String -> a
error (String -> IO FutharkiState) -> String -> IO FutharkiState
forall a b. (a -> b) -> a -> b
$ String
"Failed to initialise interpreter state: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
err
        Right FutharkiState
s -> do
          IO () -> IO ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
prog_err
          FutharkiState -> IO FutharkiState
forall (f :: * -> *) a. Applicative f => a -> f a
pure FutharkiState
s {futharkiLoaded :: Maybe String
futharkiLoaded = Maybe String
maybe_prog}
    Right FutharkiState
s ->
      FutharkiState -> IO FutharkiState
forall (f :: * -> *) a. Applicative f => a -> f a
pure FutharkiState
s
  Settings IO -> InputT IO () -> IO ()
forall (m :: * -> *) a.
(MonadIO m, MonadMask m) =>
Settings m -> InputT m a -> m a
Haskeline.runInputT Settings IO
forall (m :: * -> *). MonadIO m => Settings m
Haskeline.defaultSettings (InputT IO () -> IO ()) -> InputT IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ FutharkiState -> InputT IO ()
toploop FutharkiState
s

  String -> IO ()
putStrLn String
"Leaving 'futhark repl'."

confirmQuit :: Haskeline.InputT IO Bool
confirmQuit :: InputT IO Bool
confirmQuit = do
  Maybe Char
c <- String -> InputT IO (Maybe Char)
forall (m :: * -> *).
(MonadIO m, MonadMask m) =>
String -> InputT m (Maybe Char)
Haskeline.getInputChar String
"Quit REPL? (y/n) "
  case Maybe Char
c of
    Maybe Char
Nothing -> Bool -> InputT IO Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True -- EOF
    Just Char
'y' -> Bool -> InputT IO Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
    Just Char
'n' -> Bool -> InputT IO Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
    Maybe Char
_ -> InputT IO Bool
confirmQuit

-- | Representation of breaking at a breakpoint, to allow for
-- navigating through the stack frames and such.
data Breaking = Breaking
  { Breaking -> NonEmpty StackFrame
breakingStack :: NE.NonEmpty I.StackFrame,
    -- | Index of the current breakpoint (with
    -- 0 being the outermost).
    Breaking -> Int
breakingAt :: Int
  }

data FutharkiState = FutharkiState
  { FutharkiState -> LoadedProg
futharkiProg :: LoadedProg,
    FutharkiState -> Int
futharkiCount :: Int,
    FutharkiState -> (Env, Ctx)
futharkiEnv :: (T.Env, I.Ctx),
    -- | Are we currently stopped at a breakpoint?
    FutharkiState -> Maybe Breaking
futharkiBreaking :: Maybe Breaking,
    -- | Skip breakpoints at these locations.
    FutharkiState -> [Loc]
futharkiSkipBreaks :: [Loc],
    FutharkiState -> Bool
futharkiBreakOnNaN :: Bool,
    -- | The currently loaded file.
    FutharkiState -> Maybe String
futharkiLoaded :: Maybe FilePath
  }

extendEnvs :: LoadedProg -> (T.Env, I.Ctx) -> [String] -> (T.Env, I.Ctx)
extendEnvs :: LoadedProg -> (Env, Ctx) -> [String] -> (Env, Ctx)
extendEnvs LoadedProg
prog (Env
tenv, Ctx
ictx) [String]
opens = (Env
tenv', Ctx
ictx')
  where
    tenv' :: Env
tenv' = Imports -> Env -> Env
T.envWithImports Imports
t_imports Env
tenv
    ictx' :: Ctx
ictx' = [Env] -> Ctx -> Ctx
I.ctxWithImports [Env]
i_envs Ctx
ictx
    t_imports :: Imports
t_imports = ((String, FileModule) -> Bool) -> Imports -> Imports
forall a. (a -> Bool) -> [a] -> [a]
filter ((String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
opens) (String -> Bool)
-> ((String, FileModule) -> String) -> (String, FileModule) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, FileModule) -> String
forall a b. (a, b) -> a
fst) (Imports -> Imports) -> Imports -> Imports
forall a b. (a -> b) -> a -> b
$ LoadedProg -> Imports
lpImports LoadedProg
prog
    i_envs :: [Env]
i_envs = ((String, Env) -> Env) -> [(String, Env)] -> [Env]
forall a b. (a -> b) -> [a] -> [b]
map (String, Env) -> Env
forall a b. (a, b) -> b
snd ([(String, Env)] -> [Env]) -> [(String, Env)] -> [Env]
forall a b. (a -> b) -> a -> b
$ ((String, Env) -> Bool) -> [(String, Env)] -> [(String, Env)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
opens) (String -> Bool)
-> ((String, Env) -> String) -> (String, Env) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, Env) -> String
forall a b. (a, b) -> a
fst) ([(String, Env)] -> [(String, Env)])
-> [(String, Env)] -> [(String, Env)]
forall a b. (a -> b) -> a -> b
$ Map String Env -> [(String, Env)]
forall k a. Map k a -> [(k, a)]
M.toList (Map String Env -> [(String, Env)])
-> Map String Env -> [(String, Env)]
forall a b. (a -> b) -> a -> b
$ Ctx -> Map String Env
I.ctxImports Ctx
ictx

newFutharkiState :: Int -> LoadedProg -> Maybe FilePath -> IO (Either String FutharkiState)
newFutharkiState :: Int
-> LoadedProg -> Maybe String -> IO (Either String FutharkiState)
newFutharkiState Int
count LoadedProg
prev_prog Maybe String
maybe_file = ExceptT String IO FutharkiState -> IO (Either String FutharkiState)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT String IO FutharkiState
 -> IO (Either String FutharkiState))
-> ExceptT String IO FutharkiState
-> IO (Either String FutharkiState)
forall a b. (a -> b) -> a -> b
$ do
  (LoadedProg
prog, Env
tenv, Ctx
ienv) <- case Maybe String
maybe_file of
    Maybe String
Nothing -> do
      -- Load the builtins through the type checker.
      LoadedProg
prog <-
        (NonEmpty ProgError -> String)
-> Either (NonEmpty ProgError) LoadedProg
-> ExceptT String IO LoadedProg
forall err a.
(err -> String) -> Either err a -> ExceptT String IO a
badOnLeft NonEmpty ProgError -> String
prettyProgErrors (Either (NonEmpty ProgError) LoadedProg
 -> ExceptT String IO LoadedProg)
-> ExceptT String IO (Either (NonEmpty ProgError) LoadedProg)
-> ExceptT String IO LoadedProg
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< IO (Either (NonEmpty ProgError) LoadedProg)
-> ExceptT String IO (Either (NonEmpty ProgError) LoadedProg)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (LoadedProg
-> [String] -> VFS -> IO (Either (NonEmpty ProgError) LoadedProg)
reloadProg LoadedProg
prev_prog [] VFS
forall k a. Map k a
M.empty)
      -- Then into the interpreter.
      Ctx
ienv <-
        (Ctx -> (String, Prog) -> ExceptT String IO Ctx)
-> Ctx -> [(String, Prog)] -> ExceptT String IO Ctx
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM
          (\Ctx
ctx -> (InterpreterError -> String)
-> Either InterpreterError Ctx -> ExceptT String IO Ctx
forall err a.
(err -> String) -> Either err a -> ExceptT String IO a
badOnLeft InterpreterError -> String
forall a. Show a => a -> String
show (Either InterpreterError Ctx -> ExceptT String IO Ctx)
-> ((String, Prog)
    -> ExceptT String IO (Either InterpreterError Ctx))
-> (String, Prog)
-> ExceptT String IO Ctx
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< F ExtOp Ctx -> ExceptT String IO (Either InterpreterError Ctx)
forall (m :: * -> *) a.
MonadIO m =>
F ExtOp a -> m (Either InterpreterError a)
runInterpreter' (F ExtOp Ctx -> ExceptT String IO (Either InterpreterError Ctx))
-> ((String, Prog) -> F ExtOp Ctx)
-> (String, Prog)
-> ExceptT String IO (Either InterpreterError Ctx)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ctx -> (String, Prog) -> F ExtOp Ctx
I.interpretImport Ctx
ctx)
          Ctx
I.initialCtx
          ([(String, Prog)] -> ExceptT String IO Ctx)
-> [(String, Prog)] -> ExceptT String IO Ctx
forall a b. (a -> b) -> a -> b
$ ((String, FileModule) -> (String, Prog))
-> Imports -> [(String, Prog)]
forall a b. (a -> b) -> [a] -> [b]
map ((FileModule -> Prog) -> (String, FileModule) -> (String, Prog)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FileModule -> Prog
fileProg) (LoadedProg -> Imports
lpImports LoadedProg
prog)

      let (Env
tenv, Ctx
ienv') =
            LoadedProg -> (Env, Ctx) -> [String] -> (Env, Ctx)
extendEnvs LoadedProg
prog (Env
T.initialEnv, Ctx
ienv) [String
"/prelude/prelude"]

      (LoadedProg, Env, Ctx) -> ExceptT String IO (LoadedProg, Env, Ctx)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (LoadedProg
prog, Env
tenv, Ctx
ienv')
    Just String
file -> do
      LoadedProg
prog <- (NonEmpty ProgError -> String)
-> Either (NonEmpty ProgError) LoadedProg
-> ExceptT String IO LoadedProg
forall err a.
(err -> String) -> Either err a -> ExceptT String IO a
badOnLeft NonEmpty ProgError -> String
prettyProgErrors (Either (NonEmpty ProgError) LoadedProg
 -> ExceptT String IO LoadedProg)
-> ExceptT String IO (Either (NonEmpty ProgError) LoadedProg)
-> ExceptT String IO LoadedProg
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< IO (Either (NonEmpty ProgError) LoadedProg)
-> ExceptT String IO (Either (NonEmpty ProgError) LoadedProg)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (LoadedProg
-> [String] -> VFS -> IO (Either (NonEmpty ProgError) LoadedProg)
reloadProg LoadedProg
prev_prog [String
file] VFS
forall k a. Map k a
M.empty)
      IO () -> ExceptT String IO ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> ExceptT String IO ()) -> IO () -> ExceptT String IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Warnings -> String
forall a. Pretty a => a -> String
pretty (Warnings -> String) -> Warnings -> String
forall a b. (a -> b) -> a -> b
$ LoadedProg -> Warnings
lpWarnings LoadedProg
prog

      Ctx
ienv <-
        (Ctx -> (String, Prog) -> ExceptT String IO Ctx)
-> Ctx -> [(String, Prog)] -> ExceptT String IO Ctx
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM
          (\Ctx
ctx -> (InterpreterError -> String)
-> Either InterpreterError Ctx -> ExceptT String IO Ctx
forall err a.
(err -> String) -> Either err a -> ExceptT String IO a
badOnLeft InterpreterError -> String
forall a. Show a => a -> String
show (Either InterpreterError Ctx -> ExceptT String IO Ctx)
-> ((String, Prog)
    -> ExceptT String IO (Either InterpreterError Ctx))
-> (String, Prog)
-> ExceptT String IO Ctx
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< F ExtOp Ctx -> ExceptT String IO (Either InterpreterError Ctx)
forall (m :: * -> *) a.
MonadIO m =>
F ExtOp a -> m (Either InterpreterError a)
runInterpreter' (F ExtOp Ctx -> ExceptT String IO (Either InterpreterError Ctx))
-> ((String, Prog) -> F ExtOp Ctx)
-> (String, Prog)
-> ExceptT String IO (Either InterpreterError Ctx)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ctx -> (String, Prog) -> F ExtOp Ctx
I.interpretImport Ctx
ctx)
          Ctx
I.initialCtx
          ([(String, Prog)] -> ExceptT String IO Ctx)
-> [(String, Prog)] -> ExceptT String IO Ctx
forall a b. (a -> b) -> a -> b
$ ((String, FileModule) -> (String, Prog))
-> Imports -> [(String, Prog)]
forall a b. (a -> b) -> [a] -> [b]
map ((FileModule -> Prog) -> (String, FileModule) -> (String, Prog)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FileModule -> Prog
fileProg) (LoadedProg -> Imports
lpImports LoadedProg
prog)

      let (Env
tenv, Ctx
ienv') =
            LoadedProg -> (Env, Ctx) -> [String] -> (Env, Ctx)
extendEnvs LoadedProg
prog (Env
T.initialEnv, Ctx
ienv) [String
"/prelude/prelude", String -> String
dropExtension String
file]

      (LoadedProg, Env, Ctx) -> ExceptT String IO (LoadedProg, Env, Ctx)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (LoadedProg
prog, Env
tenv, Ctx
ienv')

  FutharkiState -> ExceptT String IO FutharkiState
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    FutharkiState :: LoadedProg
-> Int
-> (Env, Ctx)
-> Maybe Breaking
-> [Loc]
-> Bool
-> Maybe String
-> FutharkiState
FutharkiState
      { futharkiProg :: LoadedProg
futharkiProg = LoadedProg
prog,
        futharkiCount :: Int
futharkiCount = Int
count,
        futharkiEnv :: (Env, Ctx)
futharkiEnv = (Env
tenv, Ctx
ienv),
        futharkiBreaking :: Maybe Breaking
futharkiBreaking = Maybe Breaking
forall a. Maybe a
Nothing,
        futharkiSkipBreaks :: [Loc]
futharkiSkipBreaks = [Loc]
forall a. Monoid a => a
mempty,
        futharkiBreakOnNaN :: Bool
futharkiBreakOnNaN = Bool
False,
        futharkiLoaded :: Maybe String
futharkiLoaded = Maybe String
maybe_file
      }
  where
    badOnLeft :: (err -> String) -> Either err a -> ExceptT String IO a
    badOnLeft :: (err -> String) -> Either err a -> ExceptT String IO a
badOnLeft err -> String
_ (Right a
x) = a -> ExceptT String IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x
    badOnLeft err -> String
p (Left err
err) = String -> ExceptT String IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> ExceptT String IO a) -> String -> ExceptT String IO a
forall a b. (a -> b) -> a -> b
$ err -> String
p err
err

    prettyProgErrors :: NonEmpty ProgError -> String
prettyProgErrors = Doc -> String
forall a. Pretty a => a -> String
pretty (Doc -> String)
-> (NonEmpty ProgError -> Doc) -> NonEmpty ProgError -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty ProgError -> Doc
pprProgErrors

getPrompt :: FutharkiM String
getPrompt :: FutharkiM String
getPrompt = do
  Int
i <- (FutharkiState -> Int) -> FutharkiM Int
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets FutharkiState -> Int
futharkiCount
  String -> FutharkiM String
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> FutharkiM String) -> String -> FutharkiM String
forall a b. (a -> b) -> a -> b
$ String
"[" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"]> "

-- The ExceptT part is more of a continuation, really.
newtype FutharkiM a = FutharkiM {FutharkiM a
-> ExceptT StopReason (StateT FutharkiState (InputT IO)) a
runFutharkiM :: ExceptT StopReason (StateT FutharkiState (Haskeline.InputT IO)) a}
  deriving
    ( a -> FutharkiM b -> FutharkiM a
(a -> b) -> FutharkiM a -> FutharkiM b
(forall a b. (a -> b) -> FutharkiM a -> FutharkiM b)
-> (forall a b. a -> FutharkiM b -> FutharkiM a)
-> Functor FutharkiM
forall a b. a -> FutharkiM b -> FutharkiM a
forall a b. (a -> b) -> FutharkiM a -> FutharkiM b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> FutharkiM b -> FutharkiM a
$c<$ :: forall a b. a -> FutharkiM b -> FutharkiM a
fmap :: (a -> b) -> FutharkiM a -> FutharkiM b
$cfmap :: forall a b. (a -> b) -> FutharkiM a -> FutharkiM b
Functor,
      Functor FutharkiM
a -> FutharkiM a
Functor FutharkiM
-> (forall a. a -> FutharkiM a)
-> (forall a b. FutharkiM (a -> b) -> FutharkiM a -> FutharkiM b)
-> (forall a b c.
    (a -> b -> c) -> FutharkiM a -> FutharkiM b -> FutharkiM c)
-> (forall a b. FutharkiM a -> FutharkiM b -> FutharkiM b)
-> (forall a b. FutharkiM a -> FutharkiM b -> FutharkiM a)
-> Applicative FutharkiM
FutharkiM a -> FutharkiM b -> FutharkiM b
FutharkiM a -> FutharkiM b -> FutharkiM a
FutharkiM (a -> b) -> FutharkiM a -> FutharkiM b
(a -> b -> c) -> FutharkiM a -> FutharkiM b -> FutharkiM c
forall a. a -> FutharkiM a
forall a b. FutharkiM a -> FutharkiM b -> FutharkiM a
forall a b. FutharkiM a -> FutharkiM b -> FutharkiM b
forall a b. FutharkiM (a -> b) -> FutharkiM a -> FutharkiM b
forall a b c.
(a -> b -> c) -> FutharkiM a -> FutharkiM b -> FutharkiM c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: FutharkiM a -> FutharkiM b -> FutharkiM a
$c<* :: forall a b. FutharkiM a -> FutharkiM b -> FutharkiM a
*> :: FutharkiM a -> FutharkiM b -> FutharkiM b
$c*> :: forall a b. FutharkiM a -> FutharkiM b -> FutharkiM b
liftA2 :: (a -> b -> c) -> FutharkiM a -> FutharkiM b -> FutharkiM c
$cliftA2 :: forall a b c.
(a -> b -> c) -> FutharkiM a -> FutharkiM b -> FutharkiM c
<*> :: FutharkiM (a -> b) -> FutharkiM a -> FutharkiM b
$c<*> :: forall a b. FutharkiM (a -> b) -> FutharkiM a -> FutharkiM b
pure :: a -> FutharkiM a
$cpure :: forall a. a -> FutharkiM a
$cp1Applicative :: Functor FutharkiM
Applicative,
      Applicative FutharkiM
a -> FutharkiM a
Applicative FutharkiM
-> (forall a b. FutharkiM a -> (a -> FutharkiM b) -> FutharkiM b)
-> (forall a b. FutharkiM a -> FutharkiM b -> FutharkiM b)
-> (forall a. a -> FutharkiM a)
-> Monad FutharkiM
FutharkiM a -> (a -> FutharkiM b) -> FutharkiM b
FutharkiM a -> FutharkiM b -> FutharkiM b
forall a. a -> FutharkiM a
forall a b. FutharkiM a -> FutharkiM b -> FutharkiM b
forall a b. FutharkiM a -> (a -> FutharkiM b) -> FutharkiM b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> FutharkiM a
$creturn :: forall a. a -> FutharkiM a
>> :: FutharkiM a -> FutharkiM b -> FutharkiM b
$c>> :: forall a b. FutharkiM a -> FutharkiM b -> FutharkiM b
>>= :: FutharkiM a -> (a -> FutharkiM b) -> FutharkiM b
$c>>= :: forall a b. FutharkiM a -> (a -> FutharkiM b) -> FutharkiM b
$cp1Monad :: Applicative FutharkiM
Monad,
      MonadState FutharkiState,
      Monad FutharkiM
Monad FutharkiM
-> (forall a. IO a -> FutharkiM a) -> MonadIO FutharkiM
IO a -> FutharkiM a
forall a. IO a -> FutharkiM a
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
liftIO :: IO a -> FutharkiM a
$cliftIO :: forall a. IO a -> FutharkiM a
$cp1MonadIO :: Monad FutharkiM
MonadIO,
      MonadError StopReason
    )

readEvalPrint :: FutharkiM ()
readEvalPrint :: FutharkiM ()
readEvalPrint = do
  String
prompt <- FutharkiM String
getPrompt
  Text
line <- String -> FutharkiM Text
inputLine String
prompt
  Maybe Breaking
breaking <- (FutharkiState -> Maybe Breaking) -> FutharkiM (Maybe Breaking)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets FutharkiState -> Maybe Breaking
futharkiBreaking
  case Text -> Maybe (Char, Text)
T.uncons Text
line of
    Maybe (Char, Text)
Nothing
      | Maybe Breaking -> Bool
forall a. Maybe a -> Bool
isJust Maybe Breaking
breaking -> StopReason -> FutharkiM ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError StopReason
Stop
      | Bool
otherwise -> () -> FutharkiM ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    Just (Char
':', Text
command) -> do
      let (Text
cmdname, Text
rest) = (Char -> Bool) -> Text -> (Text, Text)
T.break Char -> Bool
isSpace Text
command
          arg :: Text
arg = (Char -> Bool) -> Text -> Text
T.dropWhileEnd Char -> Bool
isSpace (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> Text -> Text
T.dropWhile Char -> Bool
isSpace Text
rest
      case ((Text, (Command, Text)) -> Bool)
-> [(Text, (Command, Text))] -> [(Text, (Command, Text))]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Text
cmdname Text -> Text -> Bool
`T.isPrefixOf`) (Text -> Bool)
-> ((Text, (Command, Text)) -> Text)
-> (Text, (Command, Text))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text, (Command, Text)) -> Text
forall a b. (a, b) -> a
fst) [(Text, (Command, Text))]
commands of
        [] -> IO () -> FutharkiM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> FutharkiM ()) -> IO () -> FutharkiM ()
forall a b. (a -> b) -> a -> b
$ Text -> IO ()
T.putStrLn (Text -> IO ()) -> Text -> IO ()
forall a b. (a -> b) -> a -> b
$ Text
"Unknown command '" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
cmdname Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"'"
        [(Text
_, (Command
cmdf, Text
_))] -> Command
cmdf Text
arg
        [(Text, (Command, Text))]
matches ->
          IO () -> FutharkiM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> FutharkiM ()) -> (Text -> IO ()) -> Command
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> IO ()
T.putStrLn Command -> Command
forall a b. (a -> b) -> a -> b
$
            Text
"Ambiguous command; could be one of "
              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Text] -> Text
forall a. Monoid a => [a] -> a
mconcat (Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
intersperse Text
", " (((Text, (Command, Text)) -> Text)
-> [(Text, (Command, Text))] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (Text, (Command, Text)) -> Text
forall a b. (a, b) -> a
fst [(Text, (Command, Text))]
matches))
    Maybe (Char, Text)
_ -> do
      -- Read a declaration or expression.
      Either SyntaxError (Either UncheckedDec UncheckedExp)
maybe_dec_or_e <- FutharkiM Text
-> String
-> Text
-> FutharkiM
     (Either SyntaxError (Either UncheckedDec UncheckedExp))
forall (m :: * -> *).
Monad m =>
m Text
-> String
-> Text
-> m (Either SyntaxError (Either UncheckedDec UncheckedExp))
parseDecOrExpIncrM (String -> FutharkiM Text
inputLine String
"  ") String
prompt Text
line

      case Either SyntaxError (Either UncheckedDec UncheckedExp)
maybe_dec_or_e of
        Left (SyntaxError Loc
_ String
err) -> IO () -> FutharkiM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> FutharkiM ()) -> IO () -> FutharkiM ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
err
        Right (Left UncheckedDec
d) -> UncheckedDec -> FutharkiM ()
onDec UncheckedDec
d
        Right (Right UncheckedExp
e) -> UncheckedExp -> FutharkiM ()
onExp UncheckedExp
e
  (FutharkiState -> FutharkiState) -> FutharkiM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((FutharkiState -> FutharkiState) -> FutharkiM ())
-> (FutharkiState -> FutharkiState) -> FutharkiM ()
forall a b. (a -> b) -> a -> b
$ \FutharkiState
s -> FutharkiState
s {futharkiCount :: Int
futharkiCount = FutharkiState -> Int
futharkiCount FutharkiState
s Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1}
  where
    inputLine :: String -> FutharkiM Text
inputLine String
prompt = do
      Maybe String
inp <- ExceptT
  StopReason (StateT FutharkiState (InputT IO)) (Maybe String)
-> FutharkiM (Maybe String)
forall a.
ExceptT StopReason (StateT FutharkiState (InputT IO)) a
-> FutharkiM a
FutharkiM (ExceptT
   StopReason (StateT FutharkiState (InputT IO)) (Maybe String)
 -> FutharkiM (Maybe String))
-> ExceptT
     StopReason (StateT FutharkiState (InputT IO)) (Maybe String)
-> FutharkiM (Maybe String)
forall a b. (a -> b) -> a -> b
$ StateT FutharkiState (InputT IO) (Maybe String)
-> ExceptT
     StopReason (StateT FutharkiState (InputT IO)) (Maybe String)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT FutharkiState (InputT IO) (Maybe String)
 -> ExceptT
      StopReason (StateT FutharkiState (InputT IO)) (Maybe String))
-> StateT FutharkiState (InputT IO) (Maybe String)
-> ExceptT
     StopReason (StateT FutharkiState (InputT IO)) (Maybe String)
forall a b. (a -> b) -> a -> b
$ InputT IO (Maybe String)
-> StateT FutharkiState (InputT IO) (Maybe String)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (InputT IO (Maybe String)
 -> StateT FutharkiState (InputT IO) (Maybe String))
-> InputT IO (Maybe String)
-> StateT FutharkiState (InputT IO) (Maybe String)
forall a b. (a -> b) -> a -> b
$ String -> InputT IO (Maybe String)
forall (m :: * -> *).
(MonadIO m, MonadMask m) =>
String -> InputT m (Maybe String)
Haskeline.getInputLine String
prompt
      case Maybe String
inp of
        Just String
s -> Text -> FutharkiM Text
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Text -> FutharkiM Text) -> Text -> FutharkiM Text
forall a b. (a -> b) -> a -> b
$ String -> Text
T.pack String
s
        Maybe String
Nothing -> StopReason -> FutharkiM Text
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError StopReason
EOF

getIt :: FutharkiM (Imports, VNameSource, T.Env, I.Ctx)
getIt :: FutharkiM (Imports, VNameSource, Env, Ctx)
getIt = do
  Imports
imports <- (FutharkiState -> Imports) -> FutharkiM Imports
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((FutharkiState -> Imports) -> FutharkiM Imports)
-> (FutharkiState -> Imports) -> FutharkiM Imports
forall a b. (a -> b) -> a -> b
$ LoadedProg -> Imports
lpImports (LoadedProg -> Imports)
-> (FutharkiState -> LoadedProg) -> FutharkiState -> Imports
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FutharkiState -> LoadedProg
futharkiProg
  VNameSource
src <- (FutharkiState -> VNameSource) -> FutharkiM VNameSource
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((FutharkiState -> VNameSource) -> FutharkiM VNameSource)
-> (FutharkiState -> VNameSource) -> FutharkiM VNameSource
forall a b. (a -> b) -> a -> b
$ LoadedProg -> VNameSource
lpNameSource (LoadedProg -> VNameSource)
-> (FutharkiState -> LoadedProg) -> FutharkiState -> VNameSource
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FutharkiState -> LoadedProg
futharkiProg
  (Env
tenv, Ctx
ienv) <- (FutharkiState -> (Env, Ctx)) -> FutharkiM (Env, Ctx)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets FutharkiState -> (Env, Ctx)
futharkiEnv
  (Imports, VNameSource, Env, Ctx)
-> FutharkiM (Imports, VNameSource, Env, Ctx)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Imports
imports, VNameSource
src, Env
tenv, Ctx
ienv)

onDec :: UncheckedDec -> FutharkiM ()
onDec :: UncheckedDec -> FutharkiM ()
onDec UncheckedDec
d = do
  Imports
old_imports <- (FutharkiState -> Imports) -> FutharkiM Imports
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((FutharkiState -> Imports) -> FutharkiM Imports)
-> (FutharkiState -> Imports) -> FutharkiM Imports
forall a b. (a -> b) -> a -> b
$ LoadedProg -> Imports
lpImports (LoadedProg -> Imports)
-> (FutharkiState -> LoadedProg) -> FutharkiState -> Imports
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FutharkiState -> LoadedProg
futharkiProg
  ImportName
cur_import <- (FutharkiState -> ImportName) -> FutharkiM ImportName
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((FutharkiState -> ImportName) -> FutharkiM ImportName)
-> (FutharkiState -> ImportName) -> FutharkiM ImportName
forall a b. (a -> b) -> a -> b
$ String -> ImportName
T.mkInitialImport (String -> ImportName)
-> (FutharkiState -> String) -> FutharkiState -> ImportName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe String
"." (Maybe String -> String)
-> (FutharkiState -> Maybe String) -> FutharkiState -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FutharkiState -> Maybe String
futharkiLoaded
  let mkImport :: (String, SrcLoc) -> ImportName
mkImport = (String -> SrcLoc -> ImportName) -> (String, SrcLoc) -> ImportName
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((String -> SrcLoc -> ImportName)
 -> (String, SrcLoc) -> ImportName)
-> (String -> SrcLoc -> ImportName)
-> (String, SrcLoc)
-> ImportName
forall a b. (a -> b) -> a -> b
$ ImportName -> String -> SrcLoc -> ImportName
T.mkImportFrom ImportName
cur_import
      files :: [String]
files = ((String, SrcLoc) -> String) -> [(String, SrcLoc)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (ImportName -> String
T.includeToFilePath (ImportName -> String)
-> ((String, SrcLoc) -> ImportName) -> (String, SrcLoc) -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, SrcLoc) -> ImportName
mkImport) ([(String, SrcLoc)] -> [String]) -> [(String, SrcLoc)] -> [String]
forall a b. (a -> b) -> a -> b
$ UncheckedDec -> [(String, SrcLoc)]
forall (f :: * -> *) vn. DecBase f vn -> [(String, SrcLoc)]
decImports UncheckedDec
d

  LoadedProg
cur_prog <- (FutharkiState -> LoadedProg) -> FutharkiM LoadedProg
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets FutharkiState -> LoadedProg
futharkiProg
  Either (NonEmpty ProgError) LoadedProg
imp_r <- IO (Either (NonEmpty ProgError) LoadedProg)
-> FutharkiM (Either (NonEmpty ProgError) LoadedProg)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either (NonEmpty ProgError) LoadedProg)
 -> FutharkiM (Either (NonEmpty ProgError) LoadedProg))
-> IO (Either (NonEmpty ProgError) LoadedProg)
-> FutharkiM (Either (NonEmpty ProgError) LoadedProg)
forall a b. (a -> b) -> a -> b
$ LoadedProg
-> [String] -> VFS -> IO (Either (NonEmpty ProgError) LoadedProg)
extendProg LoadedProg
cur_prog [String]
files VFS
forall k a. Map k a
M.empty
  case Either (NonEmpty ProgError) LoadedProg
imp_r of
    Left NonEmpty ProgError
e -> IO () -> FutharkiM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> FutharkiM ()) -> IO () -> FutharkiM ()
forall a b. (a -> b) -> a -> b
$ Text -> IO ()
T.putStrLn (Text -> IO ()) -> Text -> IO ()
forall a b. (a -> b) -> a -> b
$ Doc -> Text
forall a. Pretty a => a -> Text
prettyText (Doc -> Text) -> Doc -> Text
forall a b. (a -> b) -> a -> b
$ NonEmpty ProgError -> Doc
pprProgErrors NonEmpty ProgError
e
    Right LoadedProg
prog -> do
      (Env, Ctx)
env <- (FutharkiState -> (Env, Ctx)) -> FutharkiM (Env, Ctx)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets FutharkiState -> (Env, Ctx)
futharkiEnv
      let (Env
tenv, Ctx
ienv) = LoadedProg -> (Env, Ctx) -> [String] -> (Env, Ctx)
extendEnvs LoadedProg
prog (Env, Ctx)
env (((String, SrcLoc) -> String) -> [(String, SrcLoc)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, SrcLoc) -> String
forall a b. (a, b) -> a
fst ([(String, SrcLoc)] -> [String]) -> [(String, SrcLoc)] -> [String]
forall a b. (a -> b) -> a -> b
$ UncheckedDec -> [(String, SrcLoc)]
forall (f :: * -> *) vn. DecBase f vn -> [(String, SrcLoc)]
decImports UncheckedDec
d)
          imports :: Imports
imports = LoadedProg -> Imports
lpImports LoadedProg
prog
          src :: VNameSource
src = LoadedProg -> VNameSource
lpNameSource LoadedProg
prog
      case Imports
-> VNameSource
-> Env
-> ImportName
-> UncheckedDec
-> (Warnings, Either TypeError (Env, Dec, VNameSource))
T.checkDec Imports
imports VNameSource
src Env
tenv ImportName
cur_import UncheckedDec
d of
        (Warnings
_, Left TypeError
e) -> IO () -> FutharkiM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> FutharkiM ()) -> IO () -> FutharkiM ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ TypeError -> String
forall a. Pretty a => a -> String
pretty TypeError
e
        (Warnings
_, Right (Env
tenv', Dec
d', VNameSource
src')) -> do
          let new_imports :: Imports
new_imports = ((String, FileModule) -> Bool) -> Imports -> Imports
forall a. (a -> Bool) -> [a] -> [a]
filter ((String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` ((String, FileModule) -> String) -> Imports -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, FileModule) -> String
forall a b. (a, b) -> a
fst Imports
old_imports) (String -> Bool)
-> ((String, FileModule) -> String) -> (String, FileModule) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, FileModule) -> String
forall a b. (a, b) -> a
fst) Imports
imports
          Either InterpreterError Ctx
int_r <- F ExtOp Ctx -> FutharkiM (Either InterpreterError Ctx)
forall a. F ExtOp a -> FutharkiM (Either InterpreterError a)
runInterpreter (F ExtOp Ctx -> FutharkiM (Either InterpreterError Ctx))
-> F ExtOp Ctx -> FutharkiM (Either InterpreterError Ctx)
forall a b. (a -> b) -> a -> b
$ do
            let onImport :: Ctx -> (String, FileModule) -> F ExtOp Ctx
onImport Ctx
ienv' (String
s, FileModule
imp) =
                  Ctx -> (String, Prog) -> F ExtOp Ctx
I.interpretImport Ctx
ienv' (String
s, FileModule -> Prog
T.fileProg FileModule
imp)
            Ctx
ienv' <- (Ctx -> (String, FileModule) -> F ExtOp Ctx)
-> Ctx -> Imports -> F ExtOp Ctx
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Ctx -> (String, FileModule) -> F ExtOp Ctx
onImport Ctx
ienv Imports
new_imports
            Ctx -> Dec -> F ExtOp Ctx
I.interpretDec Ctx
ienv' Dec
d'
          case Either InterpreterError Ctx
int_r of
            Left InterpreterError
err -> IO () -> FutharkiM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> FutharkiM ()) -> IO () -> FutharkiM ()
forall a b. (a -> b) -> a -> b
$ InterpreterError -> IO ()
forall a. Show a => a -> IO ()
print InterpreterError
err
            Right Ctx
ienv' -> (FutharkiState -> FutharkiState) -> FutharkiM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((FutharkiState -> FutharkiState) -> FutharkiM ())
-> (FutharkiState -> FutharkiState) -> FutharkiM ()
forall a b. (a -> b) -> a -> b
$ \FutharkiState
s ->
              FutharkiState
s
                { futharkiEnv :: (Env, Ctx)
futharkiEnv = (Env
tenv', Ctx
ienv'),
                  futharkiProg :: LoadedProg
futharkiProg = LoadedProg
prog {lpNameSource :: VNameSource
lpNameSource = VNameSource
src'}
                }

onExp :: UncheckedExp -> FutharkiM ()
onExp :: UncheckedExp -> FutharkiM ()
onExp UncheckedExp
e = do
  (Imports
imports, VNameSource
src, Env
tenv, Ctx
ienv) <- FutharkiM (Imports, VNameSource, Env, Ctx)
getIt
  case Imports
-> VNameSource
-> Env
-> UncheckedExp
-> (Warnings, Either TypeError ([TypeParam], Exp))
T.checkExp Imports
imports VNameSource
src Env
tenv UncheckedExp
e of
    (Warnings
_, Left TypeError
err) -> IO () -> FutharkiM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> FutharkiM ()) -> IO () -> FutharkiM ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ TypeError -> String
forall a. Pretty a => a -> String
pretty TypeError
err
    (Warnings
_, Right ([TypeParam]
tparams, Exp
e'))
      | [TypeParam] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypeParam]
tparams -> do
          Either InterpreterError Value
r <- F ExtOp Value -> FutharkiM (Either InterpreterError Value)
forall a. F ExtOp a -> FutharkiM (Either InterpreterError a)
runInterpreter (F ExtOp Value -> FutharkiM (Either InterpreterError Value))
-> F ExtOp Value -> FutharkiM (Either InterpreterError Value)
forall a b. (a -> b) -> a -> b
$ Ctx -> Exp -> F ExtOp Value
I.interpretExp Ctx
ienv Exp
e'
          case Either InterpreterError Value
r of
            Left InterpreterError
err -> IO () -> FutharkiM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> FutharkiM ()) -> IO () -> FutharkiM ()
forall a b. (a -> b) -> a -> b
$ InterpreterError -> IO ()
forall a. Show a => a -> IO ()
print InterpreterError
err
            Right Value
v -> IO () -> FutharkiM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> FutharkiM ()) -> IO () -> FutharkiM ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Value -> String
forall a. Pretty a => a -> String
pretty Value
v
      | Bool
otherwise -> IO () -> FutharkiM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> FutharkiM ()) -> IO () -> FutharkiM ()
forall a b. (a -> b) -> a -> b
$ do
          String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Inferred type of expression: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PatType -> String
forall a. Pretty a => a -> String
pretty (Exp -> PatType
typeOf Exp
e')
          String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$
            String
"The following types are ambiguous: "
              String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ((TypeParam -> String) -> [TypeParam] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (VName -> String
forall v. IsName v => v -> String
prettyName (VName -> String) -> (TypeParam -> VName) -> TypeParam -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeParam -> VName
forall vn. TypeParamBase vn -> vn
typeParamName) [TypeParam]
tparams)

prettyBreaking :: Breaking -> String
prettyBreaking :: Breaking -> String
prettyBreaking Breaking
b =
  Int -> [String] -> String
prettyStacktrace (Breaking -> Int
breakingAt Breaking
b) ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (StackFrame -> String) -> [StackFrame] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map StackFrame -> String
forall a. Located a => a -> String
locStr ([StackFrame] -> [String]) -> [StackFrame] -> [String]
forall a b. (a -> b) -> a -> b
$ NonEmpty StackFrame -> [StackFrame]
forall a. NonEmpty a -> [a]
NE.toList (NonEmpty StackFrame -> [StackFrame])
-> NonEmpty StackFrame -> [StackFrame]
forall a b. (a -> b) -> a -> b
$ Breaking -> NonEmpty StackFrame
breakingStack Breaking
b

-- Are we currently willing to break for this reason?  Among othe
-- things, we do not want recursive breakpoints.  It could work fine
-- technically, but is probably too confusing to be useful.
breakForReason :: FutharkiState -> I.StackFrame -> I.BreakReason -> Bool
breakForReason :: FutharkiState -> StackFrame -> BreakReason -> Bool
breakForReason FutharkiState
s StackFrame
_ BreakReason
I.BreakNaN
  | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ FutharkiState -> Bool
futharkiBreakOnNaN FutharkiState
s = Bool
False
breakForReason FutharkiState
s StackFrame
top BreakReason
_ =
  Maybe Breaking -> Bool
forall a. Maybe a -> Bool
isNothing (FutharkiState -> Maybe Breaking
futharkiBreaking FutharkiState
s)
    Bool -> Bool -> Bool
&& StackFrame -> Loc
forall a. Located a => a -> Loc
locOf StackFrame
top Loc -> [Loc] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` FutharkiState -> [Loc]
futharkiSkipBreaks FutharkiState
s

runInterpreter :: F I.ExtOp a -> FutharkiM (Either I.InterpreterError a)
runInterpreter :: F ExtOp a -> FutharkiM (Either InterpreterError a)
runInterpreter F ExtOp a
m = F ExtOp a
-> (a -> FutharkiM (Either InterpreterError a))
-> (ExtOp (FutharkiM (Either InterpreterError a))
    -> FutharkiM (Either InterpreterError a))
-> FutharkiM (Either InterpreterError a)
forall (f :: * -> *) a.
F f a -> forall r. (a -> r) -> (f r -> r) -> r
runF F ExtOp a
m (Either InterpreterError a -> FutharkiM (Either InterpreterError a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either InterpreterError a
 -> FutharkiM (Either InterpreterError a))
-> (a -> Either InterpreterError a)
-> a
-> FutharkiM (Either InterpreterError a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Either InterpreterError a
forall a b. b -> Either a b
Right) ExtOp (FutharkiM (Either InterpreterError a))
-> FutharkiM (Either InterpreterError a)
forall b.
ExtOp (FutharkiM (Either InterpreterError b))
-> FutharkiM (Either InterpreterError b)
intOp
  where
    intOp :: ExtOp (FutharkiM (Either InterpreterError b))
-> FutharkiM (Either InterpreterError b)
intOp (I.ExtOpError InterpreterError
err) =
      Either InterpreterError b -> FutharkiM (Either InterpreterError b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either InterpreterError b
 -> FutharkiM (Either InterpreterError b))
-> Either InterpreterError b
-> FutharkiM (Either InterpreterError b)
forall a b. (a -> b) -> a -> b
$ InterpreterError -> Either InterpreterError b
forall a b. a -> Either a b
Left InterpreterError
err
    intOp (I.ExtOpTrace String
w String
v FutharkiM (Either InterpreterError b)
c) = do
      IO () -> FutharkiM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> FutharkiM ()) -> IO () -> FutharkiM ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
w String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v
      FutharkiM (Either InterpreterError b)
c
    intOp (I.ExtOpBreak Loc
w BreakReason
why NonEmpty StackFrame
callstack FutharkiM (Either InterpreterError b)
c) = do
      FutharkiState
s <- FutharkiM FutharkiState
forall s (m :: * -> *). MonadState s m => m s
get

      let why' :: String
why' = case BreakReason
why of
            BreakReason
I.BreakPoint -> String
"Breakpoint"
            BreakReason
I.BreakNaN -> String
"NaN produced"
          top :: StackFrame
top = NonEmpty StackFrame -> StackFrame
forall a. NonEmpty a -> a
NE.head NonEmpty StackFrame
callstack
          ctx :: Ctx
ctx = StackFrame -> Ctx
I.stackFrameCtx StackFrame
top
          tenv :: Env
tenv = Env -> Env
I.typeCheckerEnv (Env -> Env) -> Env -> Env
forall a b. (a -> b) -> a -> b
$ Ctx -> Env
I.ctxEnv Ctx
ctx
          breaking :: Breaking
breaking = NonEmpty StackFrame -> Int -> Breaking
Breaking NonEmpty StackFrame
callstack Int
0

      -- Are we supposed to respect this breakpoint?
      Bool -> FutharkiM () -> FutharkiM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (FutharkiState -> StackFrame -> BreakReason -> Bool
breakForReason FutharkiState
s StackFrame
top BreakReason
why) (FutharkiM () -> FutharkiM ()) -> FutharkiM () -> FutharkiM ()
forall a b. (a -> b) -> a -> b
$ do
        IO () -> FutharkiM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> FutharkiM ()) -> IO () -> FutharkiM ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
why' String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" at " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Loc -> String
forall a. Located a => a -> String
locStr Loc
w
        IO () -> FutharkiM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> FutharkiM ()) -> IO () -> FutharkiM ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Breaking -> String
prettyBreaking Breaking
breaking
        IO () -> FutharkiM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> FutharkiM ()) -> IO () -> FutharkiM ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"<Enter> to continue."

        -- Note the cleverness to preserve the Haskeline session (for
        -- line history and such).
        (Either StopReason Any
stop, FutharkiState
s') <-
          ExceptT
  StopReason
  (StateT FutharkiState (InputT IO))
  (Either StopReason Any, FutharkiState)
-> FutharkiM (Either StopReason Any, FutharkiState)
forall a.
ExceptT StopReason (StateT FutharkiState (InputT IO)) a
-> FutharkiM a
FutharkiM (ExceptT
   StopReason
   (StateT FutharkiState (InputT IO))
   (Either StopReason Any, FutharkiState)
 -> FutharkiM (Either StopReason Any, FutharkiState))
-> (InputT IO (Either StopReason Any, FutharkiState)
    -> ExceptT
         StopReason
         (StateT FutharkiState (InputT IO))
         (Either StopReason Any, FutharkiState))
-> InputT IO (Either StopReason Any, FutharkiState)
-> FutharkiM (Either StopReason Any, FutharkiState)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT
  FutharkiState (InputT IO) (Either StopReason Any, FutharkiState)
-> ExceptT
     StopReason
     (StateT FutharkiState (InputT IO))
     (Either StopReason Any, FutharkiState)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT
   FutharkiState (InputT IO) (Either StopReason Any, FutharkiState)
 -> ExceptT
      StopReason
      (StateT FutharkiState (InputT IO))
      (Either StopReason Any, FutharkiState))
-> (InputT IO (Either StopReason Any, FutharkiState)
    -> StateT
         FutharkiState (InputT IO) (Either StopReason Any, FutharkiState))
-> InputT IO (Either StopReason Any, FutharkiState)
-> ExceptT
     StopReason
     (StateT FutharkiState (InputT IO))
     (Either StopReason Any, FutharkiState)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InputT IO (Either StopReason Any, FutharkiState)
-> StateT
     FutharkiState (InputT IO) (Either StopReason Any, FutharkiState)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (InputT IO (Either StopReason Any, FutharkiState)
 -> FutharkiM (Either StopReason Any, FutharkiState))
-> InputT IO (Either StopReason Any, FutharkiState)
-> FutharkiM (Either StopReason Any, FutharkiState)
forall a b. (a -> b) -> a -> b
$
            StateT FutharkiState (InputT IO) (Either StopReason Any)
-> FutharkiState
-> InputT IO (Either StopReason Any, FutharkiState)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT
              (ExceptT StopReason (StateT FutharkiState (InputT IO)) Any
-> StateT FutharkiState (InputT IO) (Either StopReason Any)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT StopReason (StateT FutharkiState (InputT IO)) Any
 -> StateT FutharkiState (InputT IO) (Either StopReason Any))
-> ExceptT StopReason (StateT FutharkiState (InputT IO)) Any
-> StateT FutharkiState (InputT IO) (Either StopReason Any)
forall a b. (a -> b) -> a -> b
$ FutharkiM Any
-> ExceptT StopReason (StateT FutharkiState (InputT IO)) Any
forall a.
FutharkiM a
-> ExceptT StopReason (StateT FutharkiState (InputT IO)) a
runFutharkiM (FutharkiM Any
 -> ExceptT StopReason (StateT FutharkiState (InputT IO)) Any)
-> FutharkiM Any
-> ExceptT StopReason (StateT FutharkiState (InputT IO)) Any
forall a b. (a -> b) -> a -> b
$ FutharkiM () -> FutharkiM Any
forall (f :: * -> *) a b. Applicative f => f a -> f b
forever FutharkiM ()
readEvalPrint)
              FutharkiState
s
                { futharkiEnv :: (Env, Ctx)
futharkiEnv = (Env
tenv, Ctx
ctx),
                  futharkiCount :: Int
futharkiCount = FutharkiState -> Int
futharkiCount FutharkiState
s Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1,
                  futharkiBreaking :: Maybe Breaking
futharkiBreaking = Breaking -> Maybe Breaking
forall a. a -> Maybe a
Just Breaking
breaking
                }

        case Either StopReason Any
stop of
          Left (Load String
file) -> StopReason -> FutharkiM ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (StopReason -> FutharkiM ()) -> StopReason -> FutharkiM ()
forall a b. (a -> b) -> a -> b
$ String -> StopReason
Load String
file
          Either StopReason Any
_ -> do
            IO () -> FutharkiM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> FutharkiM ()) -> IO () -> FutharkiM ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"Continuing..."
            FutharkiState -> FutharkiM ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put
              FutharkiState
s
                { futharkiCount :: Int
futharkiCount =
                    FutharkiState -> Int
futharkiCount FutharkiState
s',
                  futharkiSkipBreaks :: [Loc]
futharkiSkipBreaks =
                    FutharkiState -> [Loc]
futharkiSkipBreaks FutharkiState
s' [Loc] -> [Loc] -> [Loc]
forall a. Semigroup a => a -> a -> a
<> FutharkiState -> [Loc]
futharkiSkipBreaks FutharkiState
s,
                  futharkiBreakOnNaN :: Bool
futharkiBreakOnNaN =
                    FutharkiState -> Bool
futharkiBreakOnNaN FutharkiState
s'
                }

      FutharkiM (Either InterpreterError b)
c

runInterpreter' :: MonadIO m => F I.ExtOp a -> m (Either I.InterpreterError a)
runInterpreter' :: F ExtOp a -> m (Either InterpreterError a)
runInterpreter' F ExtOp a
m = F ExtOp a
-> (a -> m (Either InterpreterError a))
-> (ExtOp (m (Either InterpreterError a))
    -> m (Either InterpreterError a))
-> m (Either InterpreterError a)
forall (f :: * -> *) a.
F f a -> forall r. (a -> r) -> (f r -> r) -> r
runF F ExtOp a
m (Either InterpreterError a -> m (Either InterpreterError a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either InterpreterError a -> m (Either InterpreterError a))
-> (a -> Either InterpreterError a)
-> a
-> m (Either InterpreterError a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Either InterpreterError a
forall a b. b -> Either a b
Right) ExtOp (m (Either InterpreterError a))
-> m (Either InterpreterError a)
forall (f :: * -> *) b.
MonadIO f =>
ExtOp (f (Either InterpreterError b))
-> f (Either InterpreterError b)
intOp
  where
    intOp :: ExtOp (f (Either InterpreterError b))
-> f (Either InterpreterError b)
intOp (I.ExtOpError InterpreterError
err) = Either InterpreterError b -> f (Either InterpreterError b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either InterpreterError b -> f (Either InterpreterError b))
-> Either InterpreterError b -> f (Either InterpreterError b)
forall a b. (a -> b) -> a -> b
$ InterpreterError -> Either InterpreterError b
forall a b. a -> Either a b
Left InterpreterError
err
    intOp (I.ExtOpTrace String
w String
v f (Either InterpreterError b)
c) = do
      IO () -> f ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> f ()) -> IO () -> f ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
w String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v
      f (Either InterpreterError b)
c
    intOp (I.ExtOpBreak Loc
_ BreakReason
_ NonEmpty StackFrame
_ f (Either InterpreterError b)
c) = f (Either InterpreterError b)
c

type Command = T.Text -> FutharkiM ()

loadCommand :: Command
loadCommand :: Command
loadCommand Text
file = do
  Maybe String
loaded <- (FutharkiState -> Maybe String) -> FutharkiM (Maybe String)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets FutharkiState -> Maybe String
futharkiLoaded
  case (Text -> Bool
T.null Text
file, Maybe String
loaded) of
    (Bool
True, Just String
loaded') -> StopReason -> FutharkiM ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (StopReason -> FutharkiM ()) -> StopReason -> FutharkiM ()
forall a b. (a -> b) -> a -> b
$ String -> StopReason
Load String
loaded'
    (Bool
True, Maybe String
Nothing) -> IO () -> FutharkiM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> FutharkiM ()) -> IO () -> FutharkiM ()
forall a b. (a -> b) -> a -> b
$ Text -> IO ()
T.putStrLn Text
"No file specified and no file previously loaded."
    (Bool
False, Maybe String
_) -> StopReason -> FutharkiM ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (StopReason -> FutharkiM ()) -> StopReason -> FutharkiM ()
forall a b. (a -> b) -> a -> b
$ String -> StopReason
Load (String -> StopReason) -> String -> StopReason
forall a b. (a -> b) -> a -> b
$ Text -> String
T.unpack Text
file

genTypeCommand ::
  (String -> T.Text -> Either SyntaxError a) ->
  (Imports -> VNameSource -> T.Env -> a -> (Warnings, Either T.TypeError b)) ->
  (b -> String) ->
  Command
genTypeCommand :: (String -> Text -> Either SyntaxError a)
-> (Imports
    -> VNameSource -> Env -> a -> (Warnings, Either TypeError b))
-> (b -> String)
-> Command
genTypeCommand String -> Text -> Either SyntaxError a
f Imports
-> VNameSource -> Env -> a -> (Warnings, Either TypeError b)
g b -> String
h Text
e = do
  String
prompt <- FutharkiM String
getPrompt
  case String -> Text -> Either SyntaxError a
f String
prompt Text
e of
    Left (SyntaxError Loc
_ String
err) -> IO () -> FutharkiM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> FutharkiM ()) -> IO () -> FutharkiM ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
err
    Right a
e' -> do
      (Imports
imports, VNameSource
src, Env
tenv, Ctx
_) <- FutharkiM (Imports, VNameSource, Env, Ctx)
getIt
      case (Warnings, Either TypeError b) -> Either TypeError b
forall a b. (a, b) -> b
snd ((Warnings, Either TypeError b) -> Either TypeError b)
-> (Warnings, Either TypeError b) -> Either TypeError b
forall a b. (a -> b) -> a -> b
$ Imports
-> VNameSource -> Env -> a -> (Warnings, Either TypeError b)
g Imports
imports VNameSource
src Env
tenv a
e' of
        Left TypeError
err -> IO () -> FutharkiM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> FutharkiM ()) -> IO () -> FutharkiM ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ TypeError -> String
forall a. Pretty a => a -> String
pretty TypeError
err
        Right b
x -> IO () -> FutharkiM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> FutharkiM ()) -> IO () -> FutharkiM ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ b -> String
h b
x

typeCommand :: Command
typeCommand :: Command
typeCommand = (String -> Text -> Either SyntaxError UncheckedExp)
-> (Imports
    -> VNameSource
    -> Env
    -> UncheckedExp
    -> (Warnings, Either TypeError ([TypeParam], Exp)))
-> (([TypeParam], Exp) -> String)
-> Command
forall a b.
(String -> Text -> Either SyntaxError a)
-> (Imports
    -> VNameSource -> Env -> a -> (Warnings, Either TypeError b))
-> (b -> String)
-> Command
genTypeCommand String -> Text -> Either SyntaxError UncheckedExp
parseExp Imports
-> VNameSource
-> Env
-> UncheckedExp
-> (Warnings, Either TypeError ([TypeParam], Exp))
T.checkExp ((([TypeParam], Exp) -> String) -> Command)
-> (([TypeParam], Exp) -> String) -> Command
forall a b. (a -> b) -> a -> b
$ \([TypeParam]
ps, Exp
e) ->
  Exp -> String
forall a. Pretty a => a -> String
pretty Exp
e String -> String -> String
forall a. Semigroup a => a -> a -> a
<> (TypeParam -> String) -> [TypeParam] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((String
" " String -> String -> String
forall a. Semigroup a => a -> a -> a
<>) (String -> String) -> (TypeParam -> String) -> TypeParam -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeParam -> String
forall a. Pretty a => a -> String
pretty) [TypeParam]
ps
    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" : "
    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> PatType -> String
forall a. Pretty a => a -> String
pretty (Exp -> PatType
typeOf Exp
e)

mtypeCommand :: Command
mtypeCommand :: Command
mtypeCommand = (String -> Text -> Either SyntaxError (ModExpBase NoInfo Name))
-> (Imports
    -> VNameSource
    -> Env
    -> ModExpBase NoInfo Name
    -> (Warnings, Either TypeError (MTy, ModExpBase Info VName)))
-> ((MTy, ModExpBase Info VName) -> String)
-> Command
forall a b.
(String -> Text -> Either SyntaxError a)
-> (Imports
    -> VNameSource -> Env -> a -> (Warnings, Either TypeError b))
-> (b -> String)
-> Command
genTypeCommand String -> Text -> Either SyntaxError (ModExpBase NoInfo Name)
parseModExp Imports
-> VNameSource
-> Env
-> ModExpBase NoInfo Name
-> (Warnings, Either TypeError (MTy, ModExpBase Info VName))
T.checkModExp (((MTy, ModExpBase Info VName) -> String) -> Command)
-> ((MTy, ModExpBase Info VName) -> String) -> Command
forall a b. (a -> b) -> a -> b
$ MTy -> String
forall a. Pretty a => a -> String
pretty (MTy -> String)
-> ((MTy, ModExpBase Info VName) -> MTy)
-> (MTy, ModExpBase Info VName)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MTy, ModExpBase Info VName) -> MTy
forall a b. (a, b) -> a
fst

unbreakCommand :: Command
unbreakCommand :: Command
unbreakCommand Text
_ = do
  Maybe StackFrame
top <- (FutharkiState -> Maybe StackFrame) -> FutharkiM (Maybe StackFrame)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((FutharkiState -> Maybe StackFrame)
 -> FutharkiM (Maybe StackFrame))
-> (FutharkiState -> Maybe StackFrame)
-> FutharkiM (Maybe StackFrame)
forall a b. (a -> b) -> a -> b
$ (Breaking -> StackFrame) -> Maybe Breaking -> Maybe StackFrame
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (NonEmpty StackFrame -> StackFrame
forall a. NonEmpty a -> a
NE.head (NonEmpty StackFrame -> StackFrame)
-> (Breaking -> NonEmpty StackFrame) -> Breaking -> StackFrame
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Breaking -> NonEmpty StackFrame
breakingStack) (Maybe Breaking -> Maybe StackFrame)
-> (FutharkiState -> Maybe Breaking)
-> FutharkiState
-> Maybe StackFrame
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FutharkiState -> Maybe Breaking
futharkiBreaking
  case Maybe StackFrame
top of
    Maybe StackFrame
Nothing -> IO () -> FutharkiM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> FutharkiM ()) -> IO () -> FutharkiM ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"Not currently stopped at a breakpoint."
    Just StackFrame
top' -> do
      (FutharkiState -> FutharkiState) -> FutharkiM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((FutharkiState -> FutharkiState) -> FutharkiM ())
-> (FutharkiState -> FutharkiState) -> FutharkiM ()
forall a b. (a -> b) -> a -> b
$ \FutharkiState
s -> FutharkiState
s {futharkiSkipBreaks :: [Loc]
futharkiSkipBreaks = StackFrame -> Loc
forall a. Located a => a -> Loc
locOf StackFrame
top' Loc -> [Loc] -> [Loc]
forall a. a -> [a] -> [a]
: FutharkiState -> [Loc]
futharkiSkipBreaks FutharkiState
s}
      StopReason -> FutharkiM ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError StopReason
Stop

nanbreakCommand :: Command
nanbreakCommand :: Command
nanbreakCommand Text
_ = do
  (FutharkiState -> FutharkiState) -> FutharkiM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((FutharkiState -> FutharkiState) -> FutharkiM ())
-> (FutharkiState -> FutharkiState) -> FutharkiM ()
forall a b. (a -> b) -> a -> b
$ \FutharkiState
s -> FutharkiState
s {futharkiBreakOnNaN :: Bool
futharkiBreakOnNaN = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ FutharkiState -> Bool
futharkiBreakOnNaN FutharkiState
s}
  Bool
b <- (FutharkiState -> Bool) -> FutharkiM Bool
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets FutharkiState -> Bool
futharkiBreakOnNaN
  IO () -> FutharkiM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> FutharkiM ()) -> IO () -> FutharkiM ()
forall a b. (a -> b) -> a -> b
$
    String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$
      if Bool
b
        then String
"Now treating NaNs as breakpoints."
        else String
"No longer treating NaNs as breakpoints."

frameCommand :: Command
frameCommand :: Command
frameCommand Text
which = do
  Maybe (NonEmpty StackFrame)
maybe_stack <- (FutharkiState -> Maybe (NonEmpty StackFrame))
-> FutharkiM (Maybe (NonEmpty StackFrame))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((FutharkiState -> Maybe (NonEmpty StackFrame))
 -> FutharkiM (Maybe (NonEmpty StackFrame)))
-> (FutharkiState -> Maybe (NonEmpty StackFrame))
-> FutharkiM (Maybe (NonEmpty StackFrame))
forall a b. (a -> b) -> a -> b
$ (Breaking -> NonEmpty StackFrame)
-> Maybe Breaking -> Maybe (NonEmpty StackFrame)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Breaking -> NonEmpty StackFrame
breakingStack (Maybe Breaking -> Maybe (NonEmpty StackFrame))
-> (FutharkiState -> Maybe Breaking)
-> FutharkiState
-> Maybe (NonEmpty StackFrame)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FutharkiState -> Maybe Breaking
futharkiBreaking
  case (Maybe (NonEmpty StackFrame)
maybe_stack, String -> Maybe Int
forall a. Read a => String -> Maybe a
readMaybe (String -> Maybe Int) -> String -> Maybe Int
forall a b. (a -> b) -> a -> b
$ Text -> String
T.unpack Text
which) of
    (Just NonEmpty StackFrame
stack, Just Int
i)
      | StackFrame
frame : [StackFrame]
_ <- Int -> NonEmpty StackFrame -> [StackFrame]
forall a. Int -> NonEmpty a -> [a]
NE.drop Int
i NonEmpty StackFrame
stack -> do
          let breaking :: Breaking
breaking = NonEmpty StackFrame -> Int -> Breaking
Breaking NonEmpty StackFrame
stack Int
i
              ctx :: Ctx
ctx = StackFrame -> Ctx
I.stackFrameCtx StackFrame
frame
              tenv :: Env
tenv = Env -> Env
I.typeCheckerEnv (Env -> Env) -> Env -> Env
forall a b. (a -> b) -> a -> b
$ Ctx -> Env
I.ctxEnv Ctx
ctx
          (FutharkiState -> FutharkiState) -> FutharkiM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((FutharkiState -> FutharkiState) -> FutharkiM ())
-> (FutharkiState -> FutharkiState) -> FutharkiM ()
forall a b. (a -> b) -> a -> b
$ \FutharkiState
s ->
            FutharkiState
s
              { futharkiEnv :: (Env, Ctx)
futharkiEnv = (Env
tenv, Ctx
ctx),
                futharkiBreaking :: Maybe Breaking
futharkiBreaking = Breaking -> Maybe Breaking
forall a. a -> Maybe a
Just Breaking
breaking
              }
          IO () -> FutharkiM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> FutharkiM ()) -> IO () -> FutharkiM ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Breaking -> String
prettyBreaking Breaking
breaking
    (Just NonEmpty StackFrame
_, Maybe Int
_) ->
      IO () -> FutharkiM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> FutharkiM ()) -> IO () -> FutharkiM ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Invalid stack index: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Text -> String
T.unpack Text
which
    (Maybe (NonEmpty StackFrame)
Nothing, Maybe Int
_) ->
      IO () -> FutharkiM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> FutharkiM ()) -> IO () -> FutharkiM ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"Not stopped at a breakpoint."

pwdCommand :: Command
pwdCommand :: Command
pwdCommand Text
_ = IO () -> FutharkiM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> FutharkiM ()) -> IO () -> FutharkiM ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> IO String -> IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< IO String
getCurrentDirectory

cdCommand :: Command
cdCommand :: Command
cdCommand Text
dir
  | Text -> Bool
T.null Text
dir = IO () -> FutharkiM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> FutharkiM ()) -> IO () -> FutharkiM ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"Usage: ':cd <dir>'."
  | Bool
otherwise =
      IO () -> FutharkiM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> FutharkiM ()) -> IO () -> FutharkiM ()
forall a b. (a -> b) -> a -> b
$
        String -> IO ()
setCurrentDirectory (Text -> String
T.unpack Text
dir)
          IO () -> (IOException -> IO ()) -> IO ()
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` \(IOException
err :: IOException) -> IOException -> IO ()
forall a. Show a => a -> IO ()
print IOException
err

helpCommand :: Command
helpCommand :: Command
helpCommand Text
_ = IO () -> FutharkiM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> FutharkiM ()) -> IO () -> FutharkiM ()
forall a b. (a -> b) -> a -> b
$
  [(Text, (Command, Text))]
-> ((Text, (Command, Text)) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Text, (Command, Text))]
commands (((Text, (Command, Text)) -> IO ()) -> IO ())
-> ((Text, (Command, Text)) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(Text
cmd, (Command
_, Text
desc)) -> do
    Text -> IO ()
T.putStrLn (Text -> IO ()) -> Text -> IO ()
forall a b. (a -> b) -> a -> b
$ Text
":" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
cmd
    Text -> IO ()
T.putStrLn (Text -> IO ()) -> Text -> IO ()
forall a b. (a -> b) -> a -> b
$ Int -> Text -> Text
T.replicate (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Text -> Int
T.length Text
cmd) Text
"-"
    Text -> IO ()
T.putStr Text
desc
    Text -> IO ()
T.putStrLn Text
""
    Text -> IO ()
T.putStrLn Text
""

quitCommand :: Command
quitCommand :: Command
quitCommand Text
_ = StopReason -> FutharkiM ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError StopReason
Exit

commands :: [(T.Text, (Command, T.Text))]
commands :: [(Text, (Command, Text))]
commands =
  [ ( Text
"load",
      ( Command
loadCommand,
        [text|
Load a Futhark source file.  Usage:

  > :load foo.fut

If the loading succeeds, any expressions entered subsequently can use the
declarations in the source file.

Only one source file can be loaded at a time.  Using the :load command a
second time will replace the previously loaded file.  It will also replace
any declarations entered at the REPL.

|]
      )
    ),
    ( Text
"type",
      ( Command
typeCommand,
        [text|
Show the type of an expression, which must fit on a single line.
|]
      )
    ),
    ( Text
"mtype",
      ( Command
mtypeCommand,
        [text|
Show the type of a module expression, which must fit on a single line.
|]
      )
    ),
    ( Text
"unbreak",
      ( Command
unbreakCommand,
        [text|
Skip all future occurences of the current breakpoint.
|]
      )
    ),
    ( Text
"nanbreak",
      ( Command
nanbreakCommand,
        [text|
Toggle treating operators that produce new NaNs as breakpoints.  We consider a NaN
to be "new" if none of the arguments to the operator in question is a NaN.
|]
      )
    ),
    ( Text
"frame",
      ( Command
frameCommand,
        [text|
While at a break point, jump to another stack frame, whose variables can then
be inspected.  Resuming from the breakpoint will jump back to the innermost
stack frame.
|]
      )
    ),
    ( Text
"pwd",
      ( Command
pwdCommand,
        [text|
Print the current working directory.
|]
      )
    ),
    ( Text
"cd",
      ( Command
cdCommand,
        [text|
Change the current working directory.
|]
      )
    ),
    ( Text
"help",
      ( Command
helpCommand,
        [text|
Print a list of commands and a description of their behaviour.
|]
      )
    ),
    ( Text
"quit",
      ( Command
quitCommand,
        [text|
Exit REPL.
|]
      )
    )
  ]