lcc/Hcompta/LCC/Eval.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# LANGUAGE NoMonomorphismRestriction #-}
   3 {-# OPTIONS_GHC -fno-warn-orphans #-}
   4 module Main where
   5
   6 import Control.Applicative (Applicative(..))
   7 import Control.Monad (Monad(..), forM)
   8 import Data.Bool (Bool(..))
   9 import Data.Char (Char)
  10 import Data.Either (Either(..), either)
  11 import Data.Eq (Eq)
  12 import Data.Function (($), (.), id)
  13 import Data.Functor (Functor(..), (<$>))
  14 import Data.Functor.Identity (Identity(..))
  15 import Data.Foldable (foldr1)
  16 import Data.Maybe (Maybe(..), maybe)
  17 import Data.Semigroup ((<>))
  18 import Data.Text (Text)
  19 import Prelude (error)
  20 import System.IO (IO, putStrLn)
  21 import Text.Show (Show(..))
  22 import qualified Control.Monad.Classes.Run as MC
  23 import qualified Control.Monad.Trans.State.Strict as SS
  24 import qualified Data.Char as Char
  25 import qualified Data.List as L
  26 import qualified Data.Map.Strict as Map
  27 import qualified Data.Text as T
  28 import qualified Data.Text as Text
  29 import qualified Data.Text.IO as Text
  30 import qualified System.Environment as Env
  31 import qualified System.IO as IO
  32 import qualified Text.Megaparsec as P
  33
  34 import Language.Symantic as Sym
  35 import qualified Language.Symantic.Document as D
  36 import qualified Language.Symantic.Grammar as G
  37 import qualified Language.Symantic.Lib as Sym
  38
  39 import qualified Hcompta.LCC.Sym as LCC.Sym
  40 -- import qualified Hcompta.LCC as LCC
  41 import Hcompta.LCC.Read ()
  42
  43 -- dbg :: Show a => String -> a -> a
  44 -- dbg msg x = trace (msg ++ " = " ++ show x) x
  45
  46
  47 main :: IO ()
  48 main = do
  49         args <- Env.getArgs
  50         let modsTy = Sym.modulesTyInj @LCC.Sym.SS @LCC.Sym.SRC
  51         let impsTy = Sym.importTypes @LCC.Sym.CS []
  52         let modsTe :: Modules LCC.Sym.SRC LCC.Sym.SS =
  53                 either (error . show) id $
  54                 Sym.deleteDefTermInfix ([] `Mod` "$") `fmap`
  55                 modulesInj
  56         let impsTe = [] `Sym.importModules` modsTe
  57         (`D.ansiIO` IO.stderr) $ docModules impsTy modsTe
  58         let arg = Text.unwords $ Text.pack <$> args
  59         ast <- printError $ parseTe (impsTy, modsTy) (impsTe, modsTe) arg
  60         {-
  61         ast <- (foldr1 G.BinTree2 <$>) $ forM args $ \arg -> do
  62                 printError $ parseTe (impsTy, modsTy) (impsTe, modsTe) $ Text.pack arg
  63         -}
  64         te <- printError $ readTe ast
  65         evalTe impsTy te
  66         {-
  67         forM_ args $ \arg -> do
  68                 ast <- printError $ parseTe (impsTy, modsTy) (impsTe, modsTe) $ Text.pack arg
  69                 te  <- printError $ readTe ast
  70                 evalTe impsTy te
  71         -}
  72
  73 printError :: Show err => Either err a -> IO a
  74 printError (Left err) = error $ show err
  75 printError (Right a)  = return a
  76
  77
  78 type G src ss =
  79  P.ParsecT P.Dec Text
  80            (SS.StateT (Imports NameTe, Modules src ss)
  81                       ((SS.StateT (Imports NameTy, ModulesTy src))
  82                                   Identity))
  83
  84 parseTe ::
  85  forall ss src.
  86  Gram_Term src ss (G src ss) =>
  87  (Imports NameTy, ModulesTy src) ->
  88  (Imports NameTe, Modules src ss) ->
  89  Text -> Either (P.ParseError Char P.Dec) (AST_Term src ss)
  90 parseTe tys tes inp =
  91         runIdentity $
  92         MC.evalStateStrict tys $
  93         MC.evalStateStrict tes $
  94         P.runParserT g "" inp
  95         where g = G.unCF $ Sym.g_term <* G.eoi
  96
  97 type ReadTe src ss =
  98  ( Gram_Term    src ss (G src ss)
  99  , ImportTypes      ss
 100  , ModulesInj   src ss
 101  , ModulesTyInj     ss
 102  , SourceInj    (TypeVT src)    src
 103  , SourceInj    (KindK src)     src
 104  , SourceInj    (AST_Type src)  src
 105  )
 106
 107 readTe ::
 108  forall src ss.
 109  ( Syms ss Eval
 110  , Syms ss View
 111  , Syms ss (BetaT View)
 112  , ReadTe src ss
 113  , Eq src
 114  , Show src
 115  ) =>
 116  AST_Term src ss ->
 117  Either (Error_Term src) (TermVT src ss '[])
 118 readTe = Sym.readTerm CtxTyZ
 119
 120 evalTe ::
 121  Source src =>
 122  Syms ss View =>
 123  Syms ss Eval =>
 124  Syms ss (BetaT View) =>
 125  Sym.Imports Sym.NameTy ->
 126  TermVT src ss '[] ->
 127  IO ()
 128 evalTe imps (TermVT (Term q t (TeSym te))) = do
 129         (`D.ansiIO` IO.stdout) $ "Type = " <> Sym.docType
 130                 Sym.config_Doc_Type
 131                  { config_Doc_Type_vars_numbering = False
 132                  , config_Doc_Type_imports        = imps
 133                  } 0 (q #> t) <> D.eol
 134         case proveConstraint q of
 135          Nothing -> putStrLn $ "Cannot prove Constraint: " <> show q
 136          Just Dict -> do
 137                 Text.putStrLn $ "View = " <> view (betaT $ te CtxTeZ)
 138                 case t of
 139                  TyApp _ io aTy | Just HRefl <- proj_ConstKiTy @_ @IO io -> do
 140                         a <- eval $ te CtxTeZ
 141                         case proveConstraint $ Sym.tyShow aTy of
 142                          Nothing -> putStrLn $ "No Show instance for type: " <> show aTy
 143                          Just Dict -> putStrLn $ "Eval = " <> show a
 144                  _ ->
 145                         let a = eval $ te CtxTeZ in
 146                         case proveConstraint $ Sym.tyShow t of
 147                          Nothing -> putStrLn $ "No Show instance for type: " <> show t
 148                          Just Dict -> putStrLn $ "Eval = " <> show a
 149
 150 {-
 151 main :: IO ()
 152 main = do
 153         args <- Env.getArgs
 154         forM_ args $ \arg ->
 155                 readCompta @LCC.Sym.SRC @SS arg >>= \case
 156                  Left (Error_Read_Syntax err) ->
 157                         showParseError err >>=
 158                         (`Doc.ansiIO` stderr)
 159                  Left (Error_Read_Semantic err) -> error $ show err
 160                  Right (r, warns) -> do
 161                         print warns
 162                         -- print r
 163                         (`Doc.ansiIO` stdout) $
 164                                 d_compta context_write r
 165
 166 printError :: Show err => Either err a -> IO a
 167 printError (Left err) = error $ show err
 168 printError (Right a)  = return a
 169
 170 printErrorS :: Show err => S.Either err a -> IO a
 171 printErrorS (S.Left err) = error $ show err
 172 printErrorS (S.Right a)  = return a
 173 -}
 174
 175 docModules ::
 176  Source src =>
 177  D.Doc_Text d =>
 178  D.Doc_Color d =>
 179  D.Doc_Decoration d =>
 180  ReadTe src ss =>
 181  Sym.Imports Sym.NameTy ->
 182  Sym.Modules src ss -> d
 183 docModules imps (Sym.Modules mods) =
 184         Map.foldrWithKey
 185          (\p m doc -> docModule imps p m <> doc)
 186          D.empty
 187          mods
 188
 189 docModule ::
 190  forall src ss d.
 191  Source src =>
 192  D.Doc_Text d =>
 193  D.Doc_Color d =>
 194  D.Doc_Decoration d =>
 195  ReadTe src ss =>
 196  Sym.Imports Sym.NameTy ->
 197  Sym.PathMod -> Sym.Module src ss -> d
 198 docModule imps m Sym.ByFixity
 199  { Sym.byPrefix
 200  , Sym.byInfix
 201  , Sym.byPostfix
 202  } =
 203         go docFixityInfix   byInfix <>
 204         go docFixityPrefix  byPrefix <>
 205         go docFixityPostfix byPostfix
 206         where
 207         go :: (fixy -> d) -> ModuleFixy src ss fixy -> d
 208         go docFixy =
 209                 Map.foldrWithKey
 210                  (\n Sym.Tokenizer
 211                          { Sym.token_fixity
 212                          , Sym.token_term = t
 213                          } doc ->
 214                         docPathTe m n <>
 215                         docFixy token_fixity <>
 216                         D.space <> D.bold (D.yellower "::") <> D.space <>
 217                         docTokenTerm imps (t Sym.noSource) <>
 218                         D.eol <> doc)
 219                  D.empty
 220
 221 docTokenTerm ::
 222  forall src ss d.
 223  Source src =>
 224  D.Doc_Text d =>
 225  D.Doc_Color d =>
 226  ReadTe src ss =>
 227  Sym.Imports Sym.NameTy ->
 228  Sym.Token_Term src ss -> d
 229 docTokenTerm imps t =
 230         case Sym.readTerm CtxTyZ (G.BinTree0 t) of
 231          Left{} -> error "[BUG] docTokenTerm: readTerm failed"
 232          Right (Sym.TermVT te) ->
 233                 Sym.docType Sym.config_Doc_Type
 234                  { config_Doc_Type_vars_numbering = False
 235                  , config_Doc_Type_imports        = imps
 236                  } 0 $ Sym.typeOfTerm te
 237
 238 docFixityInfix :: (D.Doc_Decoration t, D.Doc_Color t, D.Doc_Text t) => Infix -> t
 239 docFixityInfix = \case
 240          Sym.Infix Nothing 5 -> D.empty
 241          Sym.Infix a p ->
 242                 let docAssoc = \case
 243                          Sym.AssocL -> "l"
 244                          Sym.AssocR -> "r"
 245                          Sym.AssocB Sym.SideL -> "l"
 246                          Sym.AssocB Sym.SideR -> "r" in
 247                 D.magenta $ " infix" <> maybe D.empty docAssoc a <>
 248                 D.space <> D.bold (D.bluer (D.int p))
 249 docFixityPrefix :: (D.Doc_Decoration t, D.Doc_Color t, D.Doc_Text t) => Unifix -> t
 250 docFixityPrefix p = D.magenta $ " prefix "  <> D.bold (D.bluer (D.int $ Sym.unifix_prece p))
 251 docFixityPostfix :: (D.Doc_Decoration t, D.Doc_Color t, D.Doc_Text t) => Unifix -> t
 252 docFixityPostfix p = D.magenta $ " postfix " <> D.bold (D.bluer (D.int $ Sym.unifix_prece p))
 253
 254 docPathTe ::
 255  D.Doc_Text d =>
 256  D.Doc_Color d =>
 257  Sym.PathMod -> Sym.NameTe -> d
 258 docPathTe (ms::Sym.PathMod) (Sym.NameTe n) =
 259         D.catH $
 260         L.intersperse (D.charH '.') $
 261         ((\(Sym.NameMod m) -> D.textH m) <$> ms) <>
 262         [(if isOp n then id else D.yellower) $ D.text n]
 263         where
 264         isOp = T.all $ \case '_' -> True; '\'' -> True; c -> Char.isAlphaNum c
 265