1 {-# LANGUAGE UndecidableInstances #-}
2 {-# LANGUAGE NoMonomorphismRestriction #-}
3 {-# OPTIONS_GHC -fno-warn-orphans #-}
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)
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
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
38 import qualified Hcompta.LCC.Sym as LCC.Sym
39 -- import qualified Hcompta.LCC as LCC
40 import Hcompta.LCC.Megaparsec ()
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`
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
59 printError :: Show err => Either err a -> IO a
60 printError (Left err) = error $ show err
61 printError (Right a) = return a
69 Sym.Imports Sym.NameTy ->
70 Sym.Modules src ss -> d
71 docModules imps (Sym.Modules mods) =
73 (\p m doc -> docModule imps p m <> doc)
84 Sym.Imports Sym.NameTy ->
85 Sym.PathMod -> Sym.Module src ss -> d
86 docModule imps m Sym.ByFixity
91 go docFixityInfix byInfix <>
92 go docFixityPrefix byPrefix <>
93 go docFixityPostfix byPostfix
95 go :: (fixy -> d) -> ModuleFixy src ss fixy -> d
103 docFixy token_fixity <>
104 D.space <> D.bold (D.yellower "::") <> D.space <>
105 docTokenTerm imps (t Sym.noSource) <>
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
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
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))
145 Sym.PathMod -> Sym.NameTe -> d
146 docPathTe (ms::Sym.PathMod) (Sym.NameTe n) =
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]
152 isOp = T.all $ \case '_' -> True; '\'' -> True; c -> Char.isAlphaNum c
157 (SS.StateT (Imports NameTe, Modules src ss)
158 ((SS.StateT (Imports NameTy, ModulesTy 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 =
169 MC.evalStateStrict tys $
170 MC.evalStateStrict tes $
171 P.runParserT g "" inp
172 where g = G.unCF $ Sym.g_term <* G.eoi
176 ( Gram_Term src ss (G src ss)
180 , SourceInj (TypeVT src) src
181 , SourceInj (KindK src) src
182 , SourceInj (AST_Type src) src
189 , Syms ss (BetaT View)
195 Either (Error_Term src) (TermVT src ss '[])
196 readTe = Sym.readTerm CtxTyZ
202 Syms ss (BetaT View) =>
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
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)
215 -- dbg :: Show a => String -> a -> a
216 -- dbg msg x = trace (msg ++ " = " ++ show x) x