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