lcc/Hcompta/LCC/Load.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 (($))
  12 import Data.Functor ((<$>))
  13 -- import Data.Maybe (Maybe(..))
  14 -- import Data.Semigroup ((<>))
  15 -- import Data.Text (Text)
  16 import System.IO (IO, stdout, stderr)
  17 import Text.Show (Show(..))
  18 import qualified Data.Strict as S
  19 -- import qualified Control.Monad.Trans.State.Strict as SS
  20 -- import qualified Data.Text as Text
  21 -- import qualified Data.Text.IO as Text
  22 import qualified System.Environment as Env
  23 -- import qualified Text.Megaparsec as P
  24
  25 import qualified Language.Symantic.Document as Doc
  26 -- import Language.Symantic.Grammar
  27 -- import Language.Symantic as Sym
  28 -- import qualified Language.Symantic.Lib as Sym
  29
  30 -- import qualified Hcompta.LCC as LCC
  31 import qualified Hcompta.LCC.Sym as LCC.Sym
  32 import Hcompta.LCC.Megaparsec (showParseError)
  33 -- import Hcompta.LCC.Grammar
  34 import Hcompta.LCC.Read
  35 import Hcompta.LCC.Document
  36
  37 -- import Control.Applicative (Applicative(..))
  38 -- import Data.Functor (Functor(..))
  39 -- import Data.Functor.Identity (Identity(..))
  40 -- import Data.Proxy (Proxy(..))
  41 -- import qualified Control.Monad.Classes.Run as MC
  42 import Prelude (error)
  43
  44 type SS = LCC.Sym.SS
  45 type SRC = ()
  46
  47 main :: IO ()
  48 main = do
  49         args <- Env.getArgs
  50         forM_ args $ \arg ->
  51                 readCompta @SRC @SS arg >>= \case
  52                  Left (Error_Read_Syntax err) ->
  53                         showParseError err >>=
  54                         (`Doc.ansiIO` stderr)
  55                  Left (Error_Read_Semantic err) -> error $ show err
  56                  Right r -> do
  57                         -- print r
  58                         (`Doc.ansiIO` stdout) $
  59                                 d_compta context_write r
  60
  61 printError :: Show err => Either err a -> IO a
  62 printError (Left err) = error $ show err
  63 printError (Right a)  = return a
  64
  65 printErrorS :: Show err => S.Either err a -> IO a
  66 printErrorS (S.Left err) = error $ show err
  67 printErrorS (S.Right a)  = return a
  68
  69 {-
  70 parseTe ::
  71  forall ss src.
  72  Inj_Modules src ss =>
  73  Gram_Term src ss (P.ParsecT P.Dec Text (SS.StateT (Sym.Imports, Modules src ss) Identity)) =>
  74  Text ->
  75  Either (P.ParseError Char P.Dec) (AST_Term src ss)
  76 parseTe inp =
  77         let mods::Modules src ss =
  78                 either (error . show) id $
  79                 Sym.deleteDefTermInfix ([] `Mod` "$") `fmap`
  80                 inj_Modules in
  81         let imps = importModulesAs [] mods in
  82         fmap reduceTeApp $
  83         runIdentity $
  84         MC.evalStateStrict (imps, mods) $
  85         P.runParserT g "" inp
  86         where
  87         g = unCF $ g_term <* eoi
  88
  89 readTe ::
  90  forall src ss.
  91  ( Gram_Term src ss (P.ParsecT P.Dec Text (SS.StateT (Sym.Imports, Modules src ss) Identity))
  92  , Syms ss Eval
  93  , Syms ss View
  94  , Syms ss (BetaT View)
  95  , Inj_Modules src ss
  96  , Eq src
  97  , Show src
  98  , Inj_Source (TypeVT src) src
  99  , Inj_Source (TypeT src '[]) src
 100  , Inj_Source (KindK src) src
 101  , Inj_Source (AST_Type src) src
 102  , Inj_Name2Type ss
 103  ) =>
 104  AST_Term src ss ->
 105  Either (Error_Term src) (TermVT src ss '[])
 106 readTe ast =
 107         let tys = inj_Name2Type (Proxy @ss) in
 108         Sym.readTerm tys CtxTyZ ast
 109
 110 evalTe ::
 111  Source src =>
 112  Syms ss View =>
 113  Syms ss Eval =>
 114  Syms ss (BetaT View) =>
 115  TermVT src ss '[] ->
 116  IO ()
 117 evalTe (TermVT (Term q t (TeSym te))) = do
 118         putStrLn $ "Type = " <> show (q #> t)
 119         case proveConstraint q of
 120          Nothing -> putStrLn $ "Cannot prove Constraint: " <> show q
 121          Just Dict -> do
 122                 Text.putStrLn $ "View = " <> view (betaT $ te CtxTeZ)
 123                 case proveConstraint $ Sym.tyShow t of
 124                  Nothing -> putStrLn $ "No Show instance for type: " <> show t
 125                  Just Dict -> putStrLn $ "Eval = " <> show (eval $ te CtxTeZ)
 126
 127 -- dbg :: Show a => String -> a -> a
 128 -- dbg msg x = trace (msg ++ " = " ++ show x) x
 129 -}