lcc/exe/eval/Main.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# LANGUAGE ViewPatterns #-}
   3 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
   4 {-# LANGUAGE NoMonomorphismRestriction #-}
   5 {-# LANGUAGE ScopedTypeVariables #-}
   6 {-# OPTIONS_GHC -fno-warn-orphans #-}
   7 module Main where
   8
   9 import Control.Applicative (Applicative(..))
  10 import Control.Monad (Monad(..), void)
  11 import Control.Monad.IO.Class (MonadIO(..))
  12 import Control.Monad.Trans.Class as MT (MonadTrans(..))
  13 import Data.Bool (Bool(..))
  14 import Data.Char (Char)
  15 import Data.Either (Either(..))
  16 import Data.Eq (Eq(..))
  17 import Data.Function (($), (.), id)
  18 import Data.Functor (Functor(..), (<$>))
  19 import Data.Maybe (Maybe(..), maybe)
  20 import Data.Semigroup ((<>))
  21 import Data.String (String)
  22 import Data.Text (Text)
  23 import Prelude (error, succ, Integer)
  24 import System.Console.Haskeline as HL
  25 import System.IO (IO, putStr, putStrLn, print)
  26 import Text.Show (Show(..))
  27 import qualified Control.Monad.Classes as MC
  28 import qualified Control.Monad.Trans.State.Strict as SS
  29 import qualified Data.Char as Char
  30 import qualified Data.List as L
  31 import qualified Data.Map.Strict as Map
  32 import qualified Data.Text as T
  33 import qualified Data.Text as Text
  34 import qualified Data.Text.IO as Text
  35 import qualified System.Console.Haskeline.History as HL
  36 import qualified System.IO as IO
  37 import qualified Text.Megaparsec as P
  38
  39 import Language.Symantic as Sym
  40 import qualified Language.Symantic.Document as D
  41 import qualified Language.Symantic.Grammar as G
  42 import qualified Language.Symantic.Lib as Sym
  43
  44 import qualified Hcompta.LCC.Sym as LCC.Sym
  45 import qualified Hcompta.LCC as LCC
  46 import qualified Hcompta.LCC.Lib.Strict as S
  47 import Hcompta.LCC.Read ()
  48 import Hcompta.LCC.Write (Writeable(..), context_write)
  49
  50 -- dbg :: Show a => String -> a -> a
  51 -- dbg msg x = trace (msg ++ " = " ++ show x) x
  52
  53 main :: IO ()
  54 main = do
  55         runInputT defaultSettings
  56          { historyFile    = Just ".hcompta.history"
  57          , autoAddHistory = False
  58          } $
  59                 S.evalState (LCC.state_sym @LCC.Sym.SRC @LCC.Sym.SS) $
  60                 unREPL (loop True 0)
  61         where
  62         loop :: forall src ss.
  63          Show src =>
  64          Syms ss Eval =>
  65          Syms ss View =>
  66          Syms ss (BetaT View) =>
  67          ReadTe src ss =>
  68          Gram_Term src ss (G src ss (InputT IO)) =>
  69          Bool -> Integer -> REPL src ss ()
  70         loop ok i = do
  71                 let prompt =
  72                         "\SOH\ESC["
  73                          <> (if ok then "32" else "31")
  74                          <> ";1m\STX"
  75                          <> show i
  76                          <> "\SOH\ESC[34;1m\STX>\SOH\ESC[0;48;05;233m\STX "
  77                 -- Σ
  78                 line <- readLine prompt
  79                 case line of
  80                  Nothing -> loop ok i
  81                  Just l -> do
  82                         void $ REPL $ lift $
  83                                 HL.modifyHistory $
  84                                 HL.addHistoryRemovingAllDupes l
  85                         REPL (parseTe $ Text.pack l) >>= \case
  86                          Left err -> do
  87                                 liftIO $ putStr $ P.parseErrorPretty err
  88                                 loop False (succ i)
  89                          Right expr ->
  90                                 case expr of
  91                                  Command_Def nam ast -> runTe nam ast
  92                                  Command_Eval    ast -> runTe "it" ast
  93                 where
  94                 runTe nam ast =
  95                         case readTe ast of
  96                          Left err -> do
  97                                 liftIO $ print err
  98                                 loop False (succ i)
  99                          Right te -> do
 100                                 REPL $ do
 101                                         MC.modify $ \(imps::Imports NameTe, mods) ->
 102                                                 (imps, insTerm nam te mods)
 103                                         evalTe te
 104                                 loop True (succ i)
 105                 insTerm :: Sym.NameTe -> Sym.TermVT src ss '[] -> Sym.Modules src ss -> Sym.Modules src ss
 106                 insTerm n t = Sym.insertTermVT ([] `Sym.Mod` t) n (Sym.Fixity2 Sym.infixN5)
 107
 108 type G src ss m =
 109  P.ParsecT P.Dec Text
 110            (S.StateT (LCC.State_Sym src ss) m)
 111
 112 data Command src ss
 113  =   Command_Eval (AST_Term src ss)
 114  |   Command_Def  NameTe (AST_Term src ss)
 115  deriving (Eq, Show)
 116
 117 parseTe ::
 118  forall ss src m.
 119  Monad m =>
 120  Gram_Term src ss (G src ss m) =>
 121  Text -> S.StateT (LCC.State_Sym src ss) m
 122                   (Either (P.ParseError Char P.Dec) (Command src ss))
 123 parseTe = P.runParserT g ""
 124         where
 125         g :: G src ss m (Command src ss)
 126         g = G.unCF $ G.try gCmdLet G.<+> gCmdEval
 127         gCmdLet =
 128                 Command_Def
 129                  <$  G.optional (G.try $ G.symbol "let")
 130                  <*> Sym.g_NameTe
 131                  <*  G.symbol "="
 132                  <*> Sym.g_term
 133                  <*  G.eoi
 134         gCmdEval =
 135                 Command_Eval
 136                  <$> Sym.g_term
 137                  <*  G.eoi
 138
 139 -- * Type 'ReadTe'
 140 type ReadTe src ss =
 141  ( SourceInj (TypeVT src)    src
 142  , SourceInj (KindK src)     src
 143  , SourceInj (AST_Type src)  src
 144  )
 145
 146 readTe ::
 147  forall src ss.
 148  ( Syms ss Eval
 149  , Syms ss View
 150  , Syms ss (BetaT View)
 151  , ReadTe src ss
 152  ) =>
 153  AST_Term src ss ->
 154  Either (Error_Term src) (TermVT src ss '[])
 155 readTe = Sym.readTerm CtxTyZ
 156
 157 -- | Lifted 'D.ansiIO' on 'IO.stdout'. Helper.
 158 ansiIO :: MonadIO m => D.ANSI_IO -> m ()
 159 ansiIO = liftIO . (`D.ansiIO` IO.stdout)
 160
 161 evalTe ::
 162  forall src ss m.
 163  Source src =>
 164  Syms ss View =>
 165  Syms ss Eval =>
 166  Syms ss (BetaT View) =>
 167  MonadIO m =>
 168  TermVT src ss '[] ->
 169  S.StateT (LCC.State_Sym src ss) m ()
 170 evalTe (TermVT (Term q t (TeSym te))) = do
 171         printTy (q #> t) >>= ansiIO . ("Type: " <>)
 172         case proveConstraint q of
 173          Nothing -> printTy q >>= ansiIO . ("Cannot prove Constraint: " <>)
 174          Just Dict -> liftIO $ do
 175                 Text.putStrLn $ "View: " <> view (betaT $ te CtxTeZ)
 176                 case t of
 177                  io:@aTy | Just HRefl <- proj_ConstKiTy @_ @IO io -> do
 178                         a <- eval $ te CtxTeZ
 179                         printTe aTy a
 180                  aTy ->
 181                         let a = eval $ te CtxTeZ in
 182                         printTe aTy a
 183
 184 printTy ::
 185  forall src ss m vs t d.
 186  Source src =>
 187  D.Doc_Text d =>
 188  D.Doc_Color d =>
 189  MonadIO m =>
 190  Type src vs t ->
 191  S.StateT (LCC.State_Sym src ss) m d
 192 printTy ty = do
 193         (impsTy, _ :: Sym.ModulesTy src) <- MC.get
 194         return $ Sym.docType
 195                 Sym.config_Doc_Type
 196                  { config_Doc_Type_vars_numbering = False
 197                  , config_Doc_Type_imports        = impsTy
 198                  } 0 ty <> D.eol
 199
 200 printTe :: Source src => Type src vs a -> a -> IO ()
 201 printTe aTy a =
 202         case proveConstraint $ LCC.Sym.tyWriteable
 203          (allocVarsR (lenVars aTy) $ LCC.Sym.tyContext_Write @_ @'[] ~> LCC.Sym.tyANSI_IO) aTy of
 204          Just Dict -> (`D.ansiIO` IO.stdout) $ write a context_write
 205          Nothing ->
 206                 case proveConstraint $ Sym.tyShow aTy of
 207                  Nothing -> putStrLn $ "No Show instance for type: " <> show aTy
 208                  Just Dict -> print a
 209
 210
 211 -- * Type 'REPL'
 212 -- /Read Eval Print Loop/ monad.
 213 newtype REPL src ss a
 214  =      REPL
 215  {    unREPL :: S.StateT (LCC.State_Sym src ss) (InputT IO) a }
 216  deriving ( Functor
 217           , Applicative
 218           , Monad
 219           , MonadIO
 220           -- , MonadState State_REPL
 221           )
 222 {-
 223 instance MonadTrans (REPL src ss) where
 224         lift = REPL . lift . lift
 225 -}
 226 type instance MC.CanDo (REPL src ss) (MC.EffState (LCC.State_Sym src ss)) = 'False
 227 type instance MC.CanDo (REPL src ss) (MC.EffState (Sym.Imports ns, Sym.Modules src ss)) = 'False
 228 type instance MC.CanDo (REPL src ss) (MC.EffState (Sym.Imports ns, Sym.ModulesTy src))  = 'False
 229
 230 -- * Type 'State_REPL'
 231 data State_REPL
 232  =   State_REPL
 233  {   state_repl_env :: ()
 234  }
 235
 236
 237
 238 readLine :: String -> REPL src ss (Maybe String)
 239 readLine prompt = do
 240         line <- REPL . lift $ getInputLine prompt
 241         case line of
 242          Just l@(':':_) -> return $ Just l
 243          Just l@(_:_) | L.last l == ' ' -> readLines l
 244          Just l  -> return $ Just l
 245          Nothing -> return Nothing
 246         where
 247         readLines :: String -> REPL src ss (Maybe String)
 248         readLines acc = do
 249                 line <- REPL . lift $ getInputLine ""
 250                 case line of
 251                  Just l@(_:_) | L.last l == ' ' -> readLines $ acc <> l
 252                  Just l  -> return $ Just $ acc <> l
 253                  Nothing -> return $ Just acc
 254
 255
 256
 257
 258 docModules ::
 259  Source src =>
 260  D.Doc_Text d =>
 261  D.Doc_Color d =>
 262  D.Doc_Decoration d =>
 263  ReadTe src ss =>
 264  Sym.Imports Sym.NameTy ->
 265  Sym.Modules src ss -> d
 266 docModules imps (Sym.Modules mods) =
 267         Map.foldrWithKey
 268          (\p m doc -> docModule imps p m <> doc)
 269          D.empty
 270          mods
 271
 272 docModule ::
 273  forall src ss d.
 274  Source src =>
 275  D.Doc_Text d =>
 276  D.Doc_Color d =>
 277  D.Doc_Decoration d =>
 278  ReadTe src ss =>
 279  Sym.Imports Sym.NameTy ->
 280  Sym.PathMod -> Sym.Module src ss -> d
 281 docModule imps m Sym.ByFixity
 282  { Sym.byPrefix
 283  , Sym.byInfix
 284  , Sym.byPostfix
 285  } =
 286         go docFixityInfix   byInfix <>
 287         go docFixityPrefix  byPrefix <>
 288         go docFixityPostfix byPostfix
 289         where
 290         go :: (fixy -> d) -> ModuleFixy src ss fixy -> d
 291         go docFixy =
 292                 Map.foldrWithKey
 293                  (\n Sym.Tokenizer
 294                          { Sym.token_fixity
 295                          , Sym.token_term = t
 296                          } doc ->
 297                         docPathTe m n <>
 298                         docFixy token_fixity <>
 299                         D.space <> D.bold (D.yellower "::") <> D.space <>
 300                         docTokenTerm imps (t Sym.noSource) <>
 301                         D.eol <> doc)
 302                  D.empty
 303
 304 docTokenTerm ::
 305  forall src ss d.
 306  Source src =>
 307  D.Doc_Text d =>
 308  D.Doc_Color d =>
 309  ReadTe src ss =>
 310  Sym.Imports Sym.NameTy ->
 311  Sym.Token_Term src ss -> d
 312 docTokenTerm imps t =
 313         case Sym.readTerm CtxTyZ (G.BinTree0 t) of
 314          Left{} -> error "[BUG] docTokenTerm: readTerm failed"
 315          Right (Sym.TermVT te) ->
 316                 Sym.docType Sym.config_Doc_Type
 317                  { config_Doc_Type_vars_numbering = False
 318                  , config_Doc_Type_imports        = imps
 319                  } 0 $ Sym.typeOfTerm te
 320
 321 docFixityInfix :: (D.Doc_Decoration t, D.Doc_Color t, D.Doc_Text t) => Infix -> t
 322 docFixityInfix = \case
 323          Sym.Infix Nothing 5 -> D.empty
 324          Sym.Infix a p ->
 325                 let docAssoc = \case
 326                          Sym.AssocL -> "l"
 327                          Sym.AssocR -> "r"
 328                          Sym.AssocB Sym.SideL -> "l"
 329                          Sym.AssocB Sym.SideR -> "r" in
 330                 D.magenta $ " infix" <> maybe D.empty docAssoc a <>
 331                 D.space <> D.bold (D.bluer (D.int p))
 332 docFixityPrefix :: (D.Doc_Decoration t, D.Doc_Color t, D.Doc_Text t) => Unifix -> t
 333 docFixityPrefix p = D.magenta $ " prefix "  <> D.bold (D.bluer (D.int $ Sym.unifix_prece p))
 334 docFixityPostfix :: (D.Doc_Decoration t, D.Doc_Color t, D.Doc_Text t) => Unifix -> t
 335 docFixityPostfix p = D.magenta $ " postfix " <> D.bold (D.bluer (D.int $ Sym.unifix_prece p))
 336
 337 docPathTe ::
 338  D.Doc_Text d =>
 339  D.Doc_Color d =>
 340  PathMod -> NameTe -> d
 341 docPathTe ms (NameTe n) =
 342         D.catH $
 343         L.intersperse (D.charH '.') $
 344         ((\(NameMod m) -> D.textH m) <$> ms) <>
 345         [(if isOp n then id else D.yellower) $ D.text n]
 346         where
 347         isOp = T.all $ \case '_' -> True; '\'' -> True; c -> Char.isAlphaNum c
 348
 349
 350 {-
 351 mainSym :: IO ()
 352 mainSym = do
 353         args <- Env.getArgs
 354         let sym@(LCC.State_Sym (impsTy,_modsTy) (_impsTe,patchModsTe -> modsTe)) =
 355                 LCC.state_sym @LCC.Sym.SRC @LCC.Sym.SS
 356         (`D.ansiIO` IO.stderr) $ docModules impsTy modsTe
 357         let arg = Text.unwords $ Text.pack <$> args
 358         ast <- printError $ parseTe sym arg
 359         {-
 360         ast <- (foldr1 G.BinTree2 <$>) $ forM args $ \arg -> do
 361                 printError $ parseTe sym $ Text.pack arg
 362         -}
 363         _te <- printError $ readTe ast
 364         return ()
 365         {-
 366         evalTe impsTy te
 367         forM_ args $ \arg -> do
 368                 ast <- printError $ parseTe (impsTy, modsTy) (impsTe, modsTe) $ Text.pack arg
 369                 te  <- printError $ readTe ast
 370                 evalTe impsTy te
 371         -}
 372         where
 373         patchModsTe = Sym.deleteDefTermInfix ([] `Mod` "$")
 374
 375 printError :: Show err => MonadIO m => Either err a -> m a
 376 printError (Left err) = liftIO $ error $ show err
 377 printError (Right a)  = return a
 378
 379 parseTe ::
 380  forall ss src m.
 381  m ~ Identity =>
 382  Show src =>
 383  G.Gram_Source src (G src ss m) =>
 384  Gram_Term src ss (G src ss m) =>
 385  LCC.State_Sym src ss ->
 386  Text -> Either (P.ParseError Char P.Dec) (Command src ss)
 387 parseTe sym inp =
 388         runIdentity $
 389         S.evalState sym $
 390         P.runParserT g "" inp
 391         where
 392         g :: G src ss Identity (Command src ss)
 393         g = G.unCF $
 394                 G.try (Command_Def <$> Sym.g_NameTe <* G.lexeme (G.char '=') <*> Sym.g_term <* G.eoi) G.<+>
 395                 (Command_Eval <$> Sym.g_term <* G.eoi)
 396 -}