]> Git — Sourcephile - comptalang.git/blob - lcc/Hcompta/LCC/Load.hs
Remove old Yesod scaffolding.
[comptalang.git] / 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 -}