lcc/Hcompta/LCC/Run.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 module Main where
   4
   5 -- import qualified Control.Monad.Classes as MC
   6 import Control.Monad (Monad(..), forM_)
   7 import Data.Char (Char)
   8 import Data.Either (Either(..))
   9 import Data.Either (either)
  10 import Data.Eq (Eq)
  11 import Data.Function (($), (.), id)
  12 import Data.Maybe (Maybe(..))
  13 import Data.Semigroup ((<>))
  14 import Data.Text (Text)
  15 import System.IO (IO, putStrLn)
  16 import Text.Show (Show(..))
  17 import qualified Control.Monad.Trans.State.Strict as SS
  18 import qualified Data.Text as Text
  19 import qualified Data.Text.IO as Text
  20 import qualified System.Environment as Env
  21 import qualified Text.Megaparsec as P
  22
  23 import Language.Symantic.Grammar
  24 import Language.Symantic as Sym
  25 import qualified Language.Symantic.Lib as Sym
  26
  27 -- import qualified Hcompta.LCC as LCC
  28 import qualified Hcompta.LCC.Sym as LCC.Sym
  29 import Hcompta.LCC.Megaparsec ()
  30
  31 import Control.Applicative (Applicative(..))
  32 import Data.Functor (Functor(..))
  33 import Data.Functor.Identity (Identity(..))
  34 import Data.Proxy (Proxy(..))
  35 import qualified Control.Monad.Classes.Run as MC
  36 import Prelude (error)
  37
  38 type SS = LCC.Sym.SS
  39 type SRC = ()
  40
  41 main :: IO ()
  42 main = do
  43         args <- Env.getArgs
  44         forM_ args $ \arg -> do
  45                 ast <- printError $ parseTe @SS @SRC (Text.pack arg)
  46                 te  <- printError $ readTe ast
  47                 runTe te
  48
  49 printError :: Show err => Either err a -> IO a
  50 printError (Left err) = error $ show err
  51 printError (Right a)  = return a
  52
  53 parseTe ::
  54  forall ss src.
  55  Inj_Modules src ss =>
  56  Gram_Term src ss (P.ParsecT P.Dec Text (SS.StateT (Sym.Imports, Modules src ss) Identity)) =>
  57  Text ->
  58  Either (P.ParseError Char P.Dec) (AST_Term src ss)
  59 parseTe inp =
  60         let mods::Modules src ss =
  61                 either (error . show) id $
  62                 Sym.deleteDefTermInfix ([] `Mod` "$") `fmap`
  63                 inj_Modules in
  64         let imps = importModulesAs [] mods in
  65         fmap reduceTeApp $
  66         runIdentity $
  67         MC.evalStateStrict (imps, mods) $
  68         P.runParserT g "" inp
  69         where
  70         g = unCF $ g_term <* eoi
  71
  72 readTe ::
  73  forall src ss.
  74  ( Gram_Term src ss (P.ParsecT P.Dec Text (SS.StateT (Sym.Imports, Modules src ss) Identity))
  75  , Syms ss Eval
  76  , Syms ss View
  77  , Syms ss (BetaT View)
  78  , Inj_Modules src ss
  79  , Eq src
  80  , Show src
  81  , Inj_Source (TypeVT src) src
  82  , Inj_Source (TypeT src '[]) src
  83  , Inj_Source (KindK src) src
  84  , Inj_Source (AST_Type src) src
  85  , Inj_Name2Type ss
  86  ) =>
  87  AST_Term src ss ->
  88  Either (Error_Term src) (TermVT src ss '[])
  89 readTe ast =
  90         let tys = inj_Name2Type (Proxy @ss) in
  91         Sym.readTerm tys CtxTyZ ast
  92
  93 runTe ::
  94  Source src =>
  95  Syms ss View =>
  96  Syms ss Eval =>
  97  Syms ss (BetaT View) =>
  98  TermVT src ss '[] ->
  99  IO ()
 100 runTe (TermVT (Term q t (TeSym te))) = do
 101         putStrLn $ "Type = " <> show (q #> t)
 102         case proveConstraint q of
 103          Nothing -> putStrLn $ "Cannot prove Constraint: " <> show q
 104          Just Dict -> do
 105                 Text.putStrLn $ "View = " <> view (betaT $ te CtxTeZ)
 106                 case proveConstraint $ Sym.tyShow t of
 107                  Nothing -> putStrLn $ "No Show instance for type: " <> show t
 108                  Just Dict -> putStrLn $ "Eval = " <> show (eval $ te CtxTeZ)
 109
 110 -- dbg :: Show a => String -> a -> a
 111 -- dbg msg x = trace (msg ++ " = " ++ show x) x
 112
 113 {-
 114 parse :: Text -> IO (Sym.EToken LCC.Meta SS)
 115 parse inp = do
 116         print inp
 117         let mods = Sym.inj_Modules @SS
 118         {-
 119         let mods' = mods
 120                  { Sym.tokenizers_infix =
 121                         ins [] (Sym.tokenize2 "&" (Sym.infixR 0) Sym.Token_Term_App) $
 122                         del [] "$" $
 123                         Sym.tokenizers_infix mods
 124                  }
 125         -}
 126         print mods
 127         (lr, ctx_tks) <-
 128                 S.runState mods' $
 129                 P.runParserT (Gram.unCF $ Sym.g_term <* Gram.eoi) "" inp
 130         case lr of
 131          Left (err::P.ParseError (P.Token Text) P.Dec) -> error $ P.parseErrorPretty err
 132          Right to -> return to
 133         where
 134         del m n      = Map.adjust (Map.delete n) m
 135         ins m (n, a) = Map.insertWith (<>) m (Map.singleton n a)
 136
 137 compile :: Sym.EToken LCC.Meta SS -> IO (Sym.TermVT SRC SS)
 138 compile to = do
 139         case Sym.compileWithoutCtx to of
 140          Left err -> error $ show err
 141          Right te -> return te
 142
 143 -- Sym.Tokenizers
 144 type instance MC.CanDo (S.StateT (Sym.Tokenizers LCC.Meta is) m)
 145                        (MC.EffState (Sym.Tokenizers LCC.Meta is)) = 'True
 146 instance Monad m => MC.MonadStateN 'MC.Zero (Sym.Tokenizers LCC.Meta is) (S.StateT (Sym.Tokenizers LCC.Meta is) m) where
 147         stateN _px = S.StateT . g.state
 148 -}