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 as LCC
  39 import qualified Hcompta.LCC.Sym as LCC.Sym
  40 import Hcompta.LCC.Megaparsec ()
  41
  42
  43 type SS = LCC.Sym.SS
  44 type SRC = ()
  45
  46 main :: IO ()
  47 main = do
  48         args <- Env.getArgs
  49         let mods::Modules SRC SS =
  50                 either (error . show) id $
  51                 Sym.deleteDefTermInfix ([] `Mod` "$") `fmap`
  52                 inj_Modules
  53         (`D.ansiIO` IO.stderr) $ docModules mods
  54         forM_ args $ \arg -> do
  55                 ast <- printError $ parseTe mods (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.Modules src ss -> d
  70 docModules (Sym.Modules mods) =
  71         Map.foldrWithKey
  72          (\p m doc -> docModule p m <> doc)
  73          D.empty
  74          mods
  75
  76 docModule ::
  77  forall src ss d.
  78  Source src =>
  79  D.Doc_Text d =>
  80  D.Doc_Color d =>
  81  D.Doc_Decoration d =>
  82  ReadTe src ss =>
  83  Sym.PathMod -> Sym.Module src ss -> d
  84 docModule m Sym.Module
  85  { Sym.module_infix
  86  , Sym.module_prefix
  87  , Sym.module_postfix
  88  } =
  89         go docFixityInfix   module_infix <>
  90         go docFixityPrefix  module_prefix <>
  91         go docFixityPostfix module_postfix
  92         where
  93         go :: (fixy -> d) -> ModuleFixy src ss fixy -> d
  94         go docFixy =
  95                 Map.foldrWithKey
  96                  (\n Sym.Tokenizer
  97                          { Sym.token_fixity
  98                          , Sym.token_term = t
  99                          } doc ->
 100                         docPathTe m n <>
 101                         docFixy token_fixity <>
 102                         D.space <> D.bold (D.yellower "::") <> D.space <>
 103                         docTokenTerm (t Sym.noSource) <>
 104                         D.eol <> doc)
 105                  D.empty
 106
 107 docTokenTerm ::
 108  forall src ss d.
 109  Source src =>
 110  D.Doc_Text d =>
 111  D.Doc_Color d =>
 112  ReadTe src ss =>
 113  Sym.Token_Term src ss -> d
 114 docTokenTerm t =
 115         let n2t = inj_Name2Type @ss in
 116         case Sym.readTerm n2t CtxTyZ (G.BinTree0 t) of
 117          Right (Sym.TermVT te) ->
 118                 Sym.docType Sym.config_doc_type
 119                  { config_Doc_Type_vars_numbering = False
 120                  } 0 $ Sym.typeOfTerm te
 121
 122 docFixityInfix :: (D.Doc_Decoration t, D.Doc_Color t, D.Doc_Text t) => Infix -> t
 123 docFixityInfix = \case
 124          Sym.Infix Nothing 5 -> D.empty
 125          Sym.Infix a p ->
 126                 let docAssoc = \case
 127                          Sym.AssocL -> "l"
 128                          Sym.AssocR -> "r"
 129                          Sym.AssocB Sym.SideL -> "l"
 130                          Sym.AssocB Sym.SideR -> "r" in
 131                 D.magenta $ " infix" <> maybe D.empty docAssoc a <>
 132                 D.space <> D.bold (D.bluer (D.int p))
 133 docFixityPrefix :: (D.Doc_Decoration t, D.Doc_Color t, D.Doc_Text t) => Unifix -> t
 134 docFixityPrefix (Sym.Prefix  p) = D.magenta $ " prefix "  <> D.bold (D.bluer (D.int p))
 135 docFixityPostfix :: (D.Doc_Decoration t, D.Doc_Color t, D.Doc_Text t) => Unifix -> t
 136 docFixityPostfix (Sym.Postfix p) = D.magenta $ " postfix " <> D.bold (D.bluer (D.int p))
 137
 138 docPathMod :: D.Doc_Text d => PathMod -> d
 139 docPathMod (p::Sym.PathMod) =
 140         D.catH $
 141         L.intersperse (D.charH '.') $
 142         (\(Sym.NameMod n) -> D.textH n) <$> p
 143
 144 docPathTe ::
 145  D.Doc_Text d =>
 146  D.Doc_Color d =>
 147  Sym.PathMod -> Sym.NameTe -> d
 148 docPathTe (ms::Sym.PathMod) (Sym.NameTe n) =
 149         D.catH $
 150         L.intersperse (D.charH '.') $
 151         ((\(Sym.NameMod m) -> D.textH m) <$> ms) <>
 152         [(if isOp n then id else D.yellower) $ D.text n]
 153         where
 154         isOp = T.all $ \case '_' -> True; '\'' -> True; c -> Char.isAlphaNum c
 155
 156
 157
 158 parseTe ::
 159  Gram_Term src ss (P.ParsecT P.Dec Text (SS.StateT (Sym.Imports, Modules src ss) Identity)) =>
 160  Sym.Modules src ss ->
 161  Text ->
 162  Either (P.ParseError Char P.Dec) (AST_Term src ss)
 163 parseTe mods inp =
 164         let imps = importQualifiedAs [] mods in
 165         fmap reduceTeApp $
 166         runIdentity $
 167         MC.evalStateStrict (imps, mods) $
 168         P.runParserT g "" inp
 169         where
 170         g = G.unCF $ Sym.g_term <* G.eoi
 171
 172 type ReadTe src ss =
 173  ( Gram_Term src ss (P.ParsecT P.Dec Text (SS.StateT (Sym.Imports, Modules src ss) Identity))
 174  , Inj_Modules src ss
 175  , Inj_Name2Type ss
 176  , Inj_Source (TypeVT src) src
 177  , Inj_Source (TypeT src '[]) src
 178  , Inj_Source (KindK src) src
 179  , Inj_Source (AST_Type src) src
 180  )
 181
 182 readTe ::
 183  forall src ss.
 184  ( Gram_Term src ss (P.ParsecT P.Dec Text (SS.StateT (Sym.Imports, Modules src ss) Identity))
 185  , Syms ss Eval
 186  , Syms ss View
 187  , Syms ss (BetaT View)
 188  , Inj_Modules src ss
 189  , Eq src
 190  , Show src
 191  , Inj_Source (TypeVT src) src
 192  , Inj_Source (TypeT src '[]) src
 193  , Inj_Source (KindK src) src
 194  , Inj_Source (AST_Type src) src
 195  , Inj_Name2Type ss
 196  ) =>
 197  AST_Term src ss ->
 198  Either (Error_Term src) (TermVT src ss '[])
 199 readTe ast =
 200         let n2t = inj_Name2Type @ss in
 201         Sym.readTerm n2t CtxTyZ ast
 202
 203 evalTe ::
 204  Source src =>
 205  Syms ss View =>
 206  Syms ss Eval =>
 207  Syms ss (BetaT View) =>
 208  TermVT src ss '[] ->
 209  IO ()
 210 evalTe (TermVT (Term q t (TeSym te))) = do
 211         putStrLn $ "Type = " <> show (q #> t)
 212         case proveConstraint q of
 213          Nothing -> putStrLn $ "Cannot prove Constraint: " <> show q
 214          Just Dict -> do
 215                 Text.putStrLn $ "View = " <> view (betaT $ te CtxTeZ)
 216                 case proveConstraint $ Sym.tyShow t of
 217                  Nothing -> putStrLn $ "No Show instance for type: " <> show t
 218                  Just Dict -> putStrLn $ "Eval = " <> show (eval $ te CtxTeZ)
 219
 220 -- dbg :: Show a => String -> a -> a
 221 -- dbg msg x = trace (msg ++ " = " ++ show x) x
 222
 223 {-
 224 parse :: Text -> IO (Sym.EToken LCC.Meta SS)
 225 parse inp = do
 226         print inp
 227         let mods = Sym.inj_Modules @SS
 228         {-
 229         let mods' = mods
 230                  { Sym.tokenizers_infix =
 231                         ins [] (Sym.tokenize2 "&" (Sym.infixR 0) Sym.Token_Term_App) $
 232                         del [] "$" $
 233                         Sym.tokenizers_infix mods
 234                  }
 235         -}
 236         print mods
 237         (lr, ctx_tks) <-
 238                 S.runState mods' $
 239                 P.runParserT (Gram.unCF $ Sym.g_term <* Gram.eoi) "" inp
 240         case lr of
 241          Left (err::P.ParseError (P.Token Text) P.Dec) -> error $ P.parseErrorPretty err
 242          Right to -> return to
 243         where
 244         del m n      = Map.adjust (Map.delete n) m
 245         ins m (n, a) = Map.insertWith (<>) m (Map.singleton n a)
 246
 247 compile :: Sym.EToken LCC.Meta SS -> IO (Sym.TermVT SRC SS)
 248 compile to = do
 249         case Sym.compileWithoutCtx to of
 250          Left err -> error $ show err
 251          Right te -> return te
 252
 253 -- Sym.Tokenizers
 254 type instance MC.CanDo (S.StateT (Sym.Tokenizers LCC.Meta is) m)
 255                        (MC.EffState (Sym.Tokenizers LCC.Meta is)) = 'True
 256 instance Monad m => MC.MonadStateN 'MC.Zero (Sym.Tokenizers LCC.Meta is) (S.StateT (Sym.Tokenizers LCC.Meta is) m) where
 257         stateN _px = S.StateT . g.state
 258 -}