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