]> Git — Sourcephile - comptalang.git/blob - lcc/Hcompta/LCC/Eval.hs
Sync with symantic.
[comptalang.git] / lcc / Hcompta / LCC / Eval.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# LANGUAGE NoMonomorphismRestriction #-}
3 {-# OPTIONS_GHC -fno-warn-orphans #-}
4 module Main where
5
6 import Control.Applicative (Applicative(..))
7 import Control.Monad (Monad(..), forM_)
8 import Data.Bool (Bool(..))
9 import Data.Char (Char)
10 import Data.Either (Either(..), either)
11 import Data.Eq (Eq)
12 import Data.Function (($), (.), id)
13 import Data.Functor (Functor(..), (<$>))
14 import Data.Functor.Identity (Identity(..))
15 import Data.Maybe (Maybe(..), maybe)
16 import Data.Semigroup ((<>))
17 import Data.Text (Text)
18 import Prelude (error)
19 import System.IO (IO, putStrLn)
20 import Text.Show (Show(..))
21 import qualified Control.Monad.Classes.Run as MC
22 import qualified Control.Monad.Trans.State.Strict as SS
23 import qualified Data.Char as Char
24 import qualified Data.List as L
25 import qualified Data.Map.Strict as Map
26 import qualified Data.Text as T
27 import qualified Data.Text as Text
28 import qualified Data.Text.IO as Text
29 import qualified System.Environment as Env
30 import qualified System.IO as IO
31 import qualified Text.Megaparsec as P
32
33 import Language.Symantic as Sym
34 import qualified Language.Symantic.Document as D
35 import qualified Language.Symantic.Grammar as G
36 import qualified Language.Symantic.Lib as Sym
37
38 import qualified Hcompta.LCC.Sym as LCC.Sym
39 -- import qualified Hcompta.LCC as LCC
40 import Hcompta.LCC.Megaparsec ()
41
42
43 main :: IO ()
44 main = do
45 args <- Env.getArgs
46 let modsTy = Sym.modulesTyInj @LCC.Sym.SS @LCC.Sym.SRC
47 let impsTy = Sym.importTypes @LCC.Sym.SS []
48 let modsTe :: Modules LCC.Sym.SRC LCC.Sym.SS =
49 either (error . show) id $
50 Sym.deleteDefTermInfix ([] `Mod` "$") `fmap`
51 modulesInj
52 let impsTe = [] `Sym.importModules` modsTe
53 (`D.ansiIO` IO.stderr) $ docModules impsTy modsTe
54 forM_ args $ \arg -> do
55 ast <- printError $ parseTe (impsTy, modsTy) (impsTe, modsTe) $ Text.pack arg
56 te <- printError $ readTe ast
57 evalTe te
58
59 printError :: Show err => Either err a -> IO a
60 printError (Left err) = error $ show err
61 printError (Right a) = return a
62
63 docModules ::
64 Source src =>
65 D.Doc_Text d =>
66 D.Doc_Color d =>
67 D.Doc_Decoration d =>
68 ReadTe src ss =>
69 Sym.Imports Sym.NameTy ->
70 Sym.Modules src ss -> d
71 docModules imps (Sym.Modules mods) =
72 Map.foldrWithKey
73 (\p m doc -> docModule imps p m <> doc)
74 D.empty
75 mods
76
77 docModule ::
78 forall src ss d.
79 Source src =>
80 D.Doc_Text d =>
81 D.Doc_Color d =>
82 D.Doc_Decoration d =>
83 ReadTe src ss =>
84 Sym.Imports Sym.NameTy ->
85 Sym.PathMod -> Sym.Module src ss -> d
86 docModule imps m Sym.ByFixity
87 { Sym.byPrefix
88 , Sym.byInfix
89 , Sym.byPostfix
90 } =
91 go docFixityInfix byInfix <>
92 go docFixityPrefix byPrefix <>
93 go docFixityPostfix byPostfix
94 where
95 go :: (fixy -> d) -> ModuleFixy src ss fixy -> d
96 go docFixy =
97 Map.foldrWithKey
98 (\n Sym.Tokenizer
99 { Sym.token_fixity
100 , Sym.token_term = t
101 } doc ->
102 docPathTe m n <>
103 docFixy token_fixity <>
104 D.space <> D.bold (D.yellower "::") <> D.space <>
105 docTokenTerm imps (t Sym.noSource) <>
106 D.eol <> doc)
107 D.empty
108
109 docTokenTerm ::
110 forall src ss d.
111 Source src =>
112 D.Doc_Text d =>
113 D.Doc_Color d =>
114 ReadTe src ss =>
115 Sym.Imports Sym.NameTy ->
116 Sym.Token_Term src ss -> d
117 docTokenTerm imps t =
118 case Sym.readTerm CtxTyZ (G.BinTree0 t) of
119 Left{} -> error "[BUG] docTokenTerm: readTerm failed"
120 Right (Sym.TermVT te) ->
121 Sym.docType Sym.config_Doc_Type
122 { config_Doc_Type_vars_numbering = False
123 , config_Doc_Type_imports = imps
124 } 0 $ Sym.typeOfTerm te
125
126 docFixityInfix :: (D.Doc_Decoration t, D.Doc_Color t, D.Doc_Text t) => Infix -> t
127 docFixityInfix = \case
128 Sym.Infix Nothing 5 -> D.empty
129 Sym.Infix a p ->
130 let docAssoc = \case
131 Sym.AssocL -> "l"
132 Sym.AssocR -> "r"
133 Sym.AssocB Sym.SideL -> "l"
134 Sym.AssocB Sym.SideR -> "r" in
135 D.magenta $ " infix" <> maybe D.empty docAssoc a <>
136 D.space <> D.bold (D.bluer (D.int p))
137 docFixityPrefix :: (D.Doc_Decoration t, D.Doc_Color t, D.Doc_Text t) => Unifix -> t
138 docFixityPrefix p = D.magenta $ " prefix " <> D.bold (D.bluer (D.int $ Sym.unifix_prece p))
139 docFixityPostfix :: (D.Doc_Decoration t, D.Doc_Color t, D.Doc_Text t) => Unifix -> t
140 docFixityPostfix p = D.magenta $ " postfix " <> D.bold (D.bluer (D.int $ Sym.unifix_prece p))
141
142 docPathTe ::
143 D.Doc_Text d =>
144 D.Doc_Color d =>
145 Sym.PathMod -> Sym.NameTe -> d
146 docPathTe (ms::Sym.PathMod) (Sym.NameTe n) =
147 D.catH $
148 L.intersperse (D.charH '.') $
149 ((\(Sym.NameMod m) -> D.textH m) <$> ms) <>
150 [(if isOp n then id else D.yellower) $ D.text n]
151 where
152 isOp = T.all $ \case '_' -> True; '\'' -> True; c -> Char.isAlphaNum c
153
154
155 type G src ss =
156 P.ParsecT P.Dec Text
157 (SS.StateT (Imports NameTe, Modules src ss)
158 ((SS.StateT (Imports NameTy, ModulesTy src))
159 Identity))
160
161 parseTe ::
162 forall ss src.
163 Gram_Term src ss (G src ss) =>
164 (Imports NameTy, ModulesTy src) ->
165 (Imports NameTe, Modules src ss) ->
166 Text -> Either (P.ParseError Char P.Dec) (AST_Term src ss)
167 parseTe tys tes inp =
168 runIdentity $
169 MC.evalStateStrict tys $
170 MC.evalStateStrict tes $
171 P.runParserT g "" inp
172 where g = G.unCF $ Sym.g_term <* G.eoi
173
174
175 type ReadTe src ss =
176 ( Gram_Term src ss (G src ss)
177 , ImportTypes ss
178 , ModulesInj src ss
179 , ModulesTyInj ss
180 , SourceInj (TypeVT src) src
181 , SourceInj (KindK src) src
182 , SourceInj (AST_Type src) src
183 )
184
185 readTe ::
186 forall src ss.
187 ( Syms ss Eval
188 , Syms ss View
189 , Syms ss (BetaT View)
190 , ReadTe src ss
191 , Eq src
192 , Show src
193 ) =>
194 AST_Term src ss ->
195 Either (Error_Term src) (TermVT src ss '[])
196 readTe = Sym.readTerm CtxTyZ
197
198 evalTe ::
199 Source src =>
200 Syms ss View =>
201 Syms ss Eval =>
202 Syms ss (BetaT View) =>
203 TermVT src ss '[] ->
204 IO ()
205 evalTe (TermVT (Term q t (TeSym te))) = do
206 putStrLn $ "Type = " <> show (q #> t)
207 case proveConstraint q of
208 Nothing -> putStrLn $ "Cannot prove Constraint: " <> show q
209 Just Dict -> do
210 Text.putStrLn $ "View = " <> view (betaT $ te CtxTeZ)
211 case proveConstraint $ Sym.tyShow t of
212 Nothing -> putStrLn $ "No Show instance for type: " <> show t
213 Just Dict -> putStrLn $ "Eval = " <> show (eval $ te CtxTeZ)
214
215 -- dbg :: Show a => String -> a -> a
216 -- dbg msg x = trace (msg ++ " = " ++ show x) x