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