lcc/Hcompta/LCC/Eval.hs

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