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