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