]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/test/Testing/Compiling.hs
Reorganize symantic-document modules.
[haskell/symantic.git] / symantic-lib / test / Testing / Compiling.hs
1 {-# LANGUAGE AllowAmbiguousTypes #-}
2 {-# LANGUAGE PolyKinds #-}
3 {-# LANGUAGE TypeInType #-}
4 {-# LANGUAGE UndecidableInstances #-}
5 {-# OPTIONS_GHC -fno-warn-orphans #-}
6 module Testing.Compiling where
7
8 import Test.Tasty
9 import Test.Tasty.HUnit
10 import Debug.Trace (trace)
11
12 import Control.Arrow (left)
13 import Data.Functor.Identity (Identity(..))
14 import Data.Text (Text)
15 import Data.Type.Equality
16 import Data.Void (Void)
17 import qualified Control.Monad.Classes.Run as MC
18 import qualified Control.Monad.Trans.State.Strict as S
19 import qualified Data.List as List
20 import qualified Data.Text as Text
21 import qualified Text.Megaparsec as P
22
23 import Language.Symantic.Grammar
24 import Language.Symantic
25 import Language.Symantic.Lib ()
26
27 import Testing.Megaparsec ()
28
29 type G src ss =
30 P.ParsecT Void Text
31 (S.StateT (Imports NameTe, Modules src ss)
32 ((S.StateT (Imports NameTy, ModulesTy src))
33 Identity))
34
35 parseTe ::
36 forall ss src.
37 ImportTypes ss =>
38 ModulesTyInj ss =>
39 ModulesInj src ss =>
40 Gram_Term src ss (G src ss) =>
41 Text -> Either (P.ParseError Char Void) (AST_Term src ss)
42 parseTe inp =
43 let modsTe :: Modules src ss = either (error . show) id modulesInj in
44 let impsTe = [] `importModules` modsTe in
45 let modsTy = modulesTyInj @ss @src in
46 let impsTy = importTypes @ss [] in
47 runIdentity $
48 MC.evalStateStrict (impsTy, modsTy) $
49 MC.evalStateStrict (impsTe, modsTe) $
50 P.runParserT g "" inp
51 where g = unCF $ g_term <* eoi
52
53 readTe ::
54 forall src ss t.
55 ( Eq t
56 , Eq src
57 , Gram_Term src ss (G src ss)
58 , ImportTypes ss
59 , ModulesInj src ss
60 , ModulesTyInj ss
61 , Show src
62 , Show t
63 , SourceInj (AST_Type src) src
64 , SourceInj (KindK src) src
65 , SourceInj (TypeT src '[]) src
66 , SourceInj (TypeVT src) src
67 , Syms ss (BetaT View)
68 , Syms ss Eval
69 , Syms ss View
70 ) =>
71 Text ->
72 Either ( Type src '[] t
73 , Either (P.ParseError Char Void)
74 (Error_Term src) )
75 (Type src '[] t, t, Text) ->
76 TestTree
77 readTe inp expected =
78 testCase (elide inp) $
79 case reduceTeApp <$> parseTe @ss inp of
80 Left err -> Left (Left err) @?= snd `left` expected
81 Right ast ->
82 case readTerm CtxTyZ ast of
83 Left err -> Left (Right err) @?= snd `left` expected
84 Right term ->
85 case term of
86 TermVT (Term q t (TeSym te)) ->
87 case expected of
88 Left (_, err) -> Right ("…"::Text) @?= Left err
89 Right (ty_expected::Type src '[] t, _::t, _::Text) ->
90 (>>= (@?= (\(_::Type src '[] t, err) -> err) `left` expected)) $
91 case lenVars t of
92 LenS{} -> return $ Left $ Right $ Error_Term_polymorphic (TypeVT t)
93 LenZ ->
94 case proveConstraint q of
95 Nothing -> return $ Left $ Right $ Error_Term_proofless $ TypeVT t
96 Just Dict ->
97 case t `eqType` ty_expected of
98 Nothing -> return $ Left $ Right $
99 Error_Term_Beta $ Error_Beta_Unify $
100 Error_Unify_mismatch (TypeVT t) (TypeVT ty_expected)
101 Just Refl ->
102 return $ Right (t, eval $ te CtxTeZ, view $ betaT $ te CtxTeZ)
103
104 maybeRight :: Either l r -> Maybe r
105 maybeRight (Right r) = Just r
106 maybeRight Left{} = Nothing
107
108 elide :: Text -> String
109 elide s | Text.length s > 42 = List.take 42 (Text.unpack s) List.++ ['…']
110 elide s = Text.unpack s
111
112 dbg :: Show a => String -> a -> a
113 dbg msg x = trace (msg ++ " = " ++ Prelude.show x) x