{-# LANGUAGE CPP
           , DataKinds
           , OverloadedStrings
           , FlexibleContexts
           , GADTs
           , RankNTypes
           #-}
{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
module Language.Hakaru.Repl where


import           Language.Hakaru.Types.Sing
import           Language.Hakaru.Syntax.ABT
import qualified Language.Hakaru.Syntax.AST as T
import           Language.Hakaru.Syntax.AST.Transforms
import           Language.Hakaru.Syntax.Variable ()
import qualified Language.Hakaru.Parser.AST as U
import           Language.Hakaru.Parser.Parser (parseHakaru, parseReplLine)
import           Language.Hakaru.Parser.SymbolResolve (resolveAST)
import           Language.Hakaru.Pretty.Concrete
import           Language.Hakaru.Syntax.TypeCheck
import           Language.Hakaru.Sample
import           Language.Hakaru.Syntax.Value

import           Control.Monad.State.Strict (StateT, evalStateT, get, modify)
import           Control.Monad.IO.Class
import           Data.List (intercalate)
import qualified Data.Text      as Text
import qualified Data.Text.IO   as IO
import qualified Data.Vector    as V
import           Text.PrettyPrint (renderStyle, style, mode, Mode(LeftMode))
import qualified System.Random.MWC as MWC
import           System.Console.Repline

type Binding = (U.AST' Text.Text -> U.AST' Text.Text)
type ReplM = HaskelineT (StateT Binding IO)

initialReplState :: Binding
initialReplState :: Binding
initialReplState = Binding
forall a. a -> a
id

extendBindings :: Binding -> Binding -> Binding
extendBindings :: Binding -> Binding -> Binding
extendBindings = (Binding -> Binding -> Binding) -> Binding -> Binding -> Binding
forall a b c. (a -> b -> c) -> b -> a -> c
flip Binding -> Binding -> Binding
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.)

triv :: TrivialABT T.Term '[] a -> TrivialABT T.Term '[] a
triv :: TrivialABT Term '[] a -> TrivialABT Term '[] a
triv = TrivialABT Term '[] a -> TrivialABT Term '[] a
forall a. a -> a
id

app1 :: a -> U.AST' a -> U.AST' a
app1 :: a -> AST' a -> AST' a
app1 a
s AST' a
x = a -> AST' a
forall a. a -> AST' a
U.Var a
s AST' a -> AST' a -> AST' a
forall a. AST' a -> AST' a -> AST' a
`U.App` AST' a
x
       
resolveAndInfer :: U.AST' Text.Text
              -> Either Text.Text (TypedAST (TrivialABT T.Term))
resolveAndInfer :: AST' Text -> Either Text (TypedAST (TrivialABT Term))
resolveAndInfer AST' Text
x = AST' Text
-> TypeCheckMode -> Either Text (TypedAST (TrivialABT Term))
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
AST' Text -> TypeCheckMode -> Either Text (TypedAST abt)
resolveAndInferWithMode AST' Text
x TypeCheckMode
LaxMode

resolveAndInferWithMode
  :: ABT T.Term abt
  => U.AST' Text.Text
  -> TypeCheckMode
  -> Either Text.Text (TypedAST abt)
resolveAndInferWithMode :: AST' Text -> TypeCheckMode -> Either Text (TypedAST abt)
resolveAndInferWithMode AST' Text
x TypeCheckMode
mode' =
    let m :: TypeCheckMonad (TypedAST abt)
m = AST -> TypeCheckMonad (TypedAST abt)
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
AST -> TypeCheckMonad (TypedAST abt)
inferType (AST' Text -> AST
resolveAST AST' Text
x) in
    TypeCheckMonad (TypedAST abt)
-> Input -> TypeCheckMode -> Either Text (TypedAST abt)
forall a.
TypeCheckMonad a -> Input -> TypeCheckMode -> Either Text a
runTCM TypeCheckMonad (TypedAST abt)
m Input
forall a. Maybe a
Nothing TypeCheckMode
mode'

               
splitLines :: Text.Text -> Maybe (V.Vector Text.Text)
splitLines :: Text -> Input
splitLines = Vector Text -> Input
forall a. a -> Maybe a
Just (Vector Text -> Input) -> (Text -> Vector Text) -> Text -> Input
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Text] -> Vector Text
forall a. [a] -> Vector a
V.fromList ([Text] -> Vector Text) -> (Text -> [Text]) -> Text -> Vector Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> [Text]
Text.lines

whenE :: MonadIO m => Either Text.Text b -> m () -> m ()
whenE :: Either Text b -> m () -> m ()
whenE (Left  Text
err) m ()
_ = IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ Text -> IO ()
IO.putStrLn Text
err
whenE (Right b
_)   m ()
m = m ()
m 
             
illustrate :: Sing a -> MWC.GenIO -> Value a -> IO ()
illustrate :: Sing a -> GenIO -> Value a -> IO ()
illustrate (SMeasure s) GenIO
g (VMeasure Value 'HProb -> GenIO -> IO (Maybe (Value a, Value 'HProb))
m) = do
    Maybe (Value a, Value 'HProb)
x <- Value 'HProb -> GenIO -> IO (Maybe (Value a, Value 'HProb))
m (LogFloat -> Value 'HProb
VProb LogFloat
1) GenIO
g
    case Maybe (Value a, Value 'HProb)
x of
      Just (Value a
samp, Value 'HProb
_) -> Sing a -> GenIO -> Value a -> IO ()
forall (a :: Hakaru). Sing a -> GenIO -> Value a -> IO ()
illustrate Sing a
s GenIO
g Value a
Value a
samp
      Maybe (Value a, Value 'HProb)
Nothing        -> Sing ('HMeasure a) -> GenIO -> Value ('HMeasure a) -> IO ()
forall (a :: Hakaru). Sing a -> GenIO -> Value a -> IO ()
illustrate (Sing a -> Sing ('HMeasure a)
forall (a :: Hakaru). Sing a -> Sing ('HMeasure a)
SMeasure Sing a
s) GenIO
g ((Value 'HProb -> GenIO -> IO (Maybe (Value a, Value 'HProb)))
-> Value ('HMeasure a)
forall (a :: Hakaru).
(Value 'HProb -> GenIO -> IO (Maybe (Value a, Value 'HProb)))
-> Value ('HMeasure a)
VMeasure Value 'HProb -> GenIO -> IO (Maybe (Value a, Value 'HProb))
m)

illustrate Sing a
_ GenIO
_ Value a
x = Value a -> IO ()
forall (a :: Hakaru). Value a -> IO ()
renderLn Value a
x

renderLn :: Value a -> IO ()
renderLn :: Value a -> IO ()
renderLn = String -> IO ()
putStrLn (String -> IO ()) -> (Value a -> String) -> Value a -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Style -> Doc -> String
renderStyle Style
style {mode :: Mode
mode = Mode
LeftMode} (Doc -> String) -> (Value a -> Doc) -> Value a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value a -> Doc
forall (a :: Hakaru). Value a -> Doc
prettyValue
             
runOnce :: MWC.GenIO -> U.AST' Text.Text -> IO ()
runOnce :: GenIO -> AST' Text -> IO ()
runOnce GenIO
g AST' Text
prog =
  case AST' Text -> Either Text (TypedAST (TrivialABT Term))
resolveAndInfer AST' Text
prog of
    Left Text
err -> Text -> IO ()
IO.putStrLn Text
err
    Right (TypedAST Sing b
typ TrivialABT Term '[] b
ast) ->
        Sing b -> GenIO -> Value b -> IO ()
forall (a :: Hakaru). Sing a -> GenIO -> Value a -> IO ()
illustrate Sing b
typ GenIO
g (TrivialABT Term '[] b -> Value b
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Value a
runEvaluate TrivialABT Term '[] b
ast)

type_ :: Cmd ReplM
type_ :: Cmd ReplM
type_ String
prog =
    case Text -> Either ParseError (AST' Text)
parseHakaru (String -> Text
Text.pack String
prog) of
      Left ParseError
err -> IO () -> ReplM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> ReplM ()) -> IO () -> ReplM ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (ParseError -> String
forall a. Show a => a -> String
show ParseError
err)
      Right AST' Text
e  -> do
        Binding
bindings <- HaskelineT (StateT Binding IO) Binding
forall s (m :: * -> *). MonadState s m => m s
get
        let prog' :: AST' Text
prog' = Binding
bindings (Text -> Binding
forall a. a -> AST' a -> AST' a
app1 Text
"dirac" AST' Text
e)
        case AST' Text -> Either Text (TypedAST (TrivialABT Term))
resolveAndInfer AST' Text
prog' of
          Left Text
err -> IO () -> ReplM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> ReplM ()) -> IO () -> ReplM ()
forall a b. (a -> b) -> a -> b
$ Text -> IO ()
IO.putStrLn Text
err
          Right (TypedAST (SMeasure typ) TrivialABT Term '[] b
_) -> IO () -> ReplM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> ReplM ()) -> IO () -> ReplM ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (Sing a -> String
forall (a :: Hakaru). Sing a -> String
prettyTypeS Sing a
typ)
          Either Text (TypedAST (TrivialABT Term))
_        -> IO () -> ReplM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> ReplM ()) -> IO () -> ReplM ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"the impossible happened"
                   
initM :: ReplM ()
initM :: ReplM ()
initM = IO () -> ReplM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> ReplM ()) -> IO () -> ReplM ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
introBanner
                   
-- Evaluation

-- No Typechecking of bindings
cmd :: MWC.GenIO -> String -> ReplM ()
cmd :: GenIO -> Cmd ReplM
cmd GenIO
g String
x =
    case Text -> Either ParseError (Either Binding (AST' Text))
parseReplLine (String -> Text
Text.pack String
x) of
      Left ParseError
err         -> IO () -> ReplM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> ReplM ()) -> IO () -> ReplM ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (ParseError -> String
forall a. Show a => a -> String
show ParseError
err)
      Right (Left Binding
b)   -> (Binding -> Binding) -> ReplM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (Binding -> Binding -> Binding
extendBindings Binding
b) 
      Right (Right AST' Text
e)  -> do
        Binding
bindings <- HaskelineT (StateT Binding IO) Binding
forall s (m :: * -> *). MonadState s m => m s
get
        let prog' :: AST' Text
prog' = Binding
bindings (Text -> Binding
forall a. a -> AST' a -> AST' a
app1 Text
"dirac" AST' Text
e)
        IO () -> ReplM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> ReplM ()) -> IO () -> ReplM ()
forall a b. (a -> b) -> a -> b
$ GenIO -> AST' Text -> IO ()
runOnce GenIO
g AST' Text
prog'


-- Typecheck bindings before adding them
cmd2 :: MWC.GenIO -> Cmd ReplM
cmd2 :: GenIO -> Cmd ReplM
cmd2 GenIO
g String
x =
    case Text -> Either ParseError (Either Binding (AST' Text))
parseReplLine (String -> Text
Text.pack String
x) of
      Left ParseError
err  -> IO () -> ReplM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> ReplM ()) -> IO () -> ReplM ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (ParseError -> String
forall a. Show a => a -> String
show ParseError
err)
      Right Either Binding (AST' Text)
e   -> do
        Binding
bindings <- HaskelineT (StateT Binding IO) Binding
forall s (m :: * -> *). MonadState s m => m s
get
        case Either Binding (AST' Text)
e of
          Left Binding
b   -> let prog :: AST' Text
prog = Binding
bindings Binding -> Binding -> Binding
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Binding
b Binding -> Binding
forall a b. (a -> b) -> a -> b
$ (Text -> Binding
forall a. a -> AST' a -> AST' a
app1 Text
"dirac" AST' Text
forall a. AST' a
U.Unit) in
                      Either Text (TypedAST (TrivialABT Term)) -> ReplM () -> ReplM ()
forall (m :: * -> *) b. MonadIO m => Either Text b -> m () -> m ()
whenE (AST' Text -> Either Text (TypedAST (TrivialABT Term))
resolveAndInfer AST' Text
prog) ((Binding -> Binding) -> ReplM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Binding -> Binding) -> ReplM ())
-> (Binding -> Binding) -> ReplM ()
forall a b. (a -> b) -> a -> b
$ Binding -> Binding -> Binding
extendBindings Binding
b)
          Right AST' Text
e' -> let prog :: AST' Text
prog = Binding
bindings (Text -> Binding
forall a. a -> AST' a -> AST' a
app1 Text
"dirac" AST' Text
e') in
                      IO () -> ReplM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> ReplM ()) -> IO () -> ReplM ()
forall a b. (a -> b) -> a -> b
$ GenIO -> AST' Text -> IO ()
runOnce GenIO
g AST' Text
prog
               
repl :: MWC.GenIO -> IO ()
repl :: GenIO -> IO ()
repl GenIO
g = (StateT Binding IO () -> Binding -> IO ())
-> Binding -> StateT Binding IO () -> IO ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT Binding IO () -> Binding -> IO ()
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT Binding
initialReplState
        (StateT Binding IO () -> IO ()) -> StateT Binding IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ ReplOpts (StateT Binding IO) -> StateT Binding IO ()
forall (m :: * -> *).
(MonadMask m, MonadIO m) =>
ReplOpts m -> m ()
evalReplOpts (ReplOpts (StateT Binding IO) -> StateT Binding IO ())
-> ReplOpts (StateT Binding IO) -> StateT Binding IO ()
forall a b. (a -> b) -> a -> b
$ ReplOpts :: forall (m :: * -> *).
(MultiLine -> HaskelineT m String)
-> Command (HaskelineT m)
-> Options (HaskelineT m)
-> Maybe Char
-> Maybe String
-> CompleterStyle m
-> HaskelineT m ()
-> HaskelineT m ExitDecision
-> ReplOpts m
ReplOpts
         { banner :: MultiLine -> HaskelineT (StateT Binding IO) String
banner           = HaskelineT (StateT Binding IO) String
-> MultiLine -> HaskelineT (StateT Binding IO) String
forall a b. a -> b -> a
const (String -> HaskelineT (StateT Binding IO) String
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
">>> ")
         , command :: Cmd ReplM
command          = GenIO -> Cmd ReplM
cmd2 GenIO
g
         , options :: Options ReplM
options          = Options ReplM
opts
         , prefix :: Maybe Char
prefix           = Char -> Maybe Char
forall a. a -> Maybe a
Just Char
':'
         , multilineCommand :: Maybe String
multilineCommand = Maybe String
forall a. Maybe a
Nothing
         , tabComplete :: CompleterStyle (StateT Binding IO)
tabComplete      = (WordCompleter (StateT Binding IO)
-> CompleterStyle (StateT Binding IO)
forall (m :: * -> *). WordCompleter m -> CompleterStyle m
Word WordCompleter (StateT Binding IO)
forall (m :: * -> *). Monad m => WordCompleter m
comp)
         , initialiser :: ReplM ()
initialiser      = ReplM ()
initM
         , finaliser :: HaskelineT (StateT Binding IO) ExitDecision
finaliser        = ExitDecision -> HaskelineT (StateT Binding IO) ExitDecision
forall (m :: * -> *) a. Monad m => a -> m a
return ExitDecision
Exit
         }

                   
-- Completion
comp :: Monad m => WordCompleter m
comp :: WordCompleter m
comp = [String] -> WordCompleter m
forall (m :: * -> *). Monad m => [String] -> WordCompleter m
listWordCompleter [String
":help", String
":expand", String
":hist", String
":type"]

-- Commands
help :: Cmd ReplM
help :: Cmd ReplM
help String
_ = IO () -> ReplM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> ReplM ()) -> IO () -> ReplM ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"Help!"

expand :: Cmd ReplM
expand :: Cmd ReplM
expand String
prog =
    case Text -> Either ParseError (Either Binding (AST' Text))
parseReplLine (String -> Text
Text.pack String
prog) of
      Left ParseError
err         -> IO () -> ReplM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> ReplM ()) -> IO () -> ReplM ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (ParseError -> String
forall a. Show a => a -> String
show ParseError
err)
      Right (Left Binding
b)   -> (Binding -> Binding) -> ReplM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (Binding -> Binding -> Binding
extendBindings Binding
b) 
      Right (Right AST' Text
e)  -> do
        Binding
bindings <- HaskelineT (StateT Binding IO) Binding
forall s (m :: * -> *). MonadState s m => m s
get
        let prog' :: AST' Text
prog' = Binding
bindings AST' Text
e
        case AST' Text -> Either Text (TypedAST (TrivialABT Term))
resolveAndInfer AST' Text
prog' of
          Left Text
err -> IO () -> ReplM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> ReplM ()) -> IO () -> ReplM ()
forall a b. (a -> b) -> a -> b
$ Text -> IO ()
IO.putStrLn Text
err
          Right (TypedAST Sing b
_ TrivialABT Term '[] b
ast) -> IO () -> ReplM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> ReplM ()) -> IO () -> ReplM ()
forall a b. (a -> b) -> a -> b
$ Doc -> IO ()
forall a. Show a => a -> IO ()
print (TrivialABT Term '[] b -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Doc
pretty (TrivialABT Term '[] b -> TrivialABT Term '[] b
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> abt '[] a
expandTransformations TrivialABT Term '[] b
ast))


hist :: Cmd ReplM
hist :: Cmd ReplM
hist = Cmd ReplM
forall a. HasCallStack => a
undefined

opts :: Options ReplM
opts :: Options ReplM
opts = [
    (String
"help", Cmd ReplM
help),
    (String
"expand", Cmd ReplM
expand),
    (String
"hist", Cmd ReplM
hist),
    (String
"type", Cmd ReplM
type_)
  ]

introBanner :: String
introBanner :: String
introBanner = [String] -> String
unlines
  [String
"    __  __      __",
   String
"   / / / /___ _/ /______ ________  __",
   String
"  / /_/ / __ `/ //_/ __ `/ ___/ / / /",
   String
" / __  / /_/ / ,< / /_/ / /  / /_/ /",
   String
"/_/ /_/\\__,_/_/|_|\\__,_/_/   \\__,_/"
  ]

main :: IO ()
main :: IO ()
main = IO (Gen RealWorld)
IO GenIO
MWC.createSystemRandom IO (Gen RealWorld) -> (Gen RealWorld -> IO ()) -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Gen RealWorld -> IO ()
GenIO -> IO ()
repl