]> Git — Sourcephile - comptalang.git/blob - lcc/Hcompta/LCC/Run.hs
Remove old Yesod scaffolding.
[comptalang.git] / lcc / Hcompta / LCC / Run.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 (($), (.), id)
12 import Data.Maybe (Maybe(..))
13 import Data.Semigroup ((<>))
14 import Data.Text (Text)
15 import System.IO (IO, putStrLn)
16 import Text.Show (Show(..))
17 import qualified Control.Monad.Trans.State.Strict as SS
18 import qualified Data.Text as Text
19 import qualified Data.Text.IO as Text
20 import qualified System.Environment as Env
21 import qualified Text.Megaparsec as P
22
23 import Language.Symantic.Grammar
24 import Language.Symantic as Sym
25 import qualified Language.Symantic.Lib as Sym
26
27 -- import qualified Hcompta.LCC as LCC
28 import qualified Hcompta.LCC.Sym as LCC.Sym
29 import Hcompta.LCC.Megaparsec ()
30
31 import Control.Applicative (Applicative(..))
32 import Data.Functor (Functor(..))
33 import Data.Functor.Identity (Identity(..))
34 import Data.Proxy (Proxy(..))
35 import qualified Control.Monad.Classes.Run as MC
36 import Prelude (error)
37
38 type SS = LCC.Sym.SS
39 type SRC = ()
40
41 main :: IO ()
42 main = do
43 args <- Env.getArgs
44 forM_ args $ \arg -> do
45 ast <- printError $ parseTe @SS @SRC (Text.pack arg)
46 te <- printError $ readTe ast
47 runTe te
48
49 printError :: Show err => Either err a -> IO a
50 printError (Left err) = error $ show err
51 printError (Right a) = return a
52
53 parseTe ::
54 forall ss src.
55 Inj_Modules src ss =>
56 Gram_Term src ss (P.ParsecT P.Dec Text (SS.StateT (Sym.Imports, Modules src ss) Identity)) =>
57 Text ->
58 Either (P.ParseError Char P.Dec) (AST_Term src ss)
59 parseTe inp =
60 let mods::Modules src ss =
61 either (error . show) id $
62 Sym.deleteDefTermInfix ([] `Mod` "$") `fmap`
63 inj_Modules in
64 let imps = importModulesAs [] mods in
65 fmap reduceTeApp $
66 runIdentity $
67 MC.evalStateStrict (imps, mods) $
68 P.runParserT g "" inp
69 where
70 g = unCF $ g_term <* eoi
71
72 readTe ::
73 forall src ss.
74 ( Gram_Term src ss (P.ParsecT P.Dec Text (SS.StateT (Sym.Imports, Modules src ss) Identity))
75 , Syms ss Eval
76 , Syms ss View
77 , Syms ss (BetaT View)
78 , Inj_Modules src ss
79 , Eq src
80 , Show src
81 , Inj_Source (TypeVT src) src
82 , Inj_Source (TypeT src '[]) src
83 , Inj_Source (KindK src) src
84 , Inj_Source (AST_Type src) src
85 , Inj_Name2Type ss
86 ) =>
87 AST_Term src ss ->
88 Either (Error_Term src) (TermVT src ss '[])
89 readTe ast =
90 let tys = inj_Name2Type (Proxy @ss) in
91 Sym.readTerm tys CtxTyZ ast
92
93 runTe ::
94 Source src =>
95 Syms ss View =>
96 Syms ss Eval =>
97 Syms ss (BetaT View) =>
98 TermVT src ss '[] ->
99 IO ()
100 runTe (TermVT (Term q t (TeSym te))) = do
101 putStrLn $ "Type = " <> show (q #> t)
102 case proveConstraint q of
103 Nothing -> putStrLn $ "Cannot prove Constraint: " <> show q
104 Just Dict -> do
105 Text.putStrLn $ "View = " <> view (betaT $ te CtxTeZ)
106 case proveConstraint $ Sym.tyShow t of
107 Nothing -> putStrLn $ "No Show instance for type: " <> show t
108 Just Dict -> putStrLn $ "Eval = " <> show (eval $ te CtxTeZ)
109
110 -- dbg :: Show a => String -> a -> a
111 -- dbg msg x = trace (msg ++ " = " ++ show x) x
112
113 {-
114 parse :: Text -> IO (Sym.EToken LCC.Meta SS)
115 parse inp = do
116 print inp
117 let mods = Sym.inj_Modules @SS
118 {-
119 let mods' = mods
120 { Sym.tokenizers_infix =
121 ins [] (Sym.tokenize2 "&" (Sym.infixR 0) Sym.Token_Term_App) $
122 del [] "$" $
123 Sym.tokenizers_infix mods
124 }
125 -}
126 print mods
127 (lr, ctx_tks) <-
128 S.runState mods' $
129 P.runParserT (Gram.unCF $ Sym.g_term <* Gram.eoi) "" inp
130 case lr of
131 Left (err::P.ParseError (P.Token Text) P.Dec) -> error $ P.parseErrorPretty err
132 Right to -> return to
133 where
134 del m n = Map.adjust (Map.delete n) m
135 ins m (n, a) = Map.insertWith (<>) m (Map.singleton n a)
136
137 compile :: Sym.EToken LCC.Meta SS -> IO (Sym.TermVT SRC SS)
138 compile to = do
139 case Sym.compileWithoutCtx to of
140 Left err -> error $ show err
141 Right te -> return te
142
143 -- Sym.Tokenizers
144 type instance MC.CanDo (S.StateT (Sym.Tokenizers LCC.Meta is) m)
145 (MC.EffState (Sym.Tokenizers LCC.Meta is)) = 'True
146 instance Monad m => MC.MonadStateN 'MC.Zero (Sym.Tokenizers LCC.Meta is) (S.StateT (Sym.Tokenizers LCC.Meta is) m) where
147 stateN _px = S.StateT . g.state
148 -}