lcc/Hcompta/LCC/Load.hs

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