Add tar GNUmakefile target.

[haskell/symantic.git] / symantic-lib / Language / Symantic / Compiling / Test.hs

diff --git a/symantic-lib/Language/Symantic/Compiling/Test.hs b/symantic-lib/Language/Symantic/Compiling/Test.hs
index a3de8d3334eb560a60f9d39ceda699e905557522..5bb79829b861b307131ddbc56054b7683dbf4604 100644 (file)
--- a/symantic-lib/Language/Symantic/Compiling/Test.hs
+++ b/symantic-lib/Language/Symantic/Compiling/Test.hs
@@ -25,36 +25,47 @@ import Language.Symantic.Lib ()
 
 import Grammar.Megaparsec ()
 
-test_parseTerm ::
+type G src ss =
+ P.ParsecT P.Dec Text
+           (SS.StateT (Imports NameTe, Modules src ss)
+                      ((SS.StateT (Imports NameTy, ModulesTy src))
+                                  Identity))
+
+parseTe ::
  forall ss src.
+ ImportTypes ss =>
+ ModulesTyInj ss =>
  ModulesInj src ss =>
- Gram_Term src ss (P.ParsecT P.Dec Text (SS.StateT (Imports, Modules src ss) Identity)) =>
- Text ->
- Either (P.ParseError Char P.Dec) (AST_Term src ss)
-test_parseTerm inp =
-       let mods :: Modules src ss = either (error . show) id modulesInj in
-       let imps = importQualifiedAs [] mods in
+ Gram_Term src ss (G src ss) =>
+ Text -> Either (P.ParseError Char P.Dec) (AST_Term src ss)
+parseTe inp =
+       let modsTe :: Modules src ss = either (error . show) id modulesInj in
+       let impsTe = [] `importModules` modsTe in
+       let modsTy = modulesTyInj @ss @src in
+       let impsTy = importTypes @ss [] in
        runIdentity $
-       MC.evalStateStrict (imps, mods) $
+       MC.evalStateStrict (impsTy, modsTy) $
+       MC.evalStateStrict (impsTe, modsTe) $
        P.runParserT g "" inp
        where g = unCF $ g_term <* eoi
 
-test_readTerm ::
+readTe ::
  forall src ss t.
  ( Eq t
- , Gram_Term src ss (P.ParsecT P.Dec Text (SS.StateT (Imports, Modules src ss) Identity))
- , Show t
- , Syms ss Eval
- , Syms ss View
- , Syms ss (BetaT View)
- , ModulesInj src ss
  , Eq src
+ , Gram_Term src ss (G src ss)
+ , ImportTypes ss
+ , ModulesInj src ss
+ , ModulesTyInj ss
  , Show src
- , SourceInj (TypeVT src) src
- , SourceInj (TypeT src '[]) src
- , SourceInj (KindK src) src
+ , Show t
  , SourceInj (AST_Type src) src
- , Name2TypeInj ss
+ , SourceInj (KindK src) src
+ , SourceInj (TypeT src '[]) src
+ , SourceInj (TypeVT src) src
+ , Syms ss (BetaT View)
+ , Syms ss Eval
+ , Syms ss View
  ) =>
  Text ->
  Either ( Type src '[] t
@@ -62,13 +73,12 @@ test_readTerm ::
                  (Error_Term src) )
         (Type src '[] t, t, Text) ->
  TestTree
-test_readTerm inp expected =
+readTe inp expected =
        testCase (elide inp) $
-       case reduceTeApp <$> test_parseTerm @ss inp of
+       case reduceTeApp <$> parseTe @ss inp of
         Left err -> Left (Left err) @?= snd `left` expected
         Right ast ->
-               let tys = name2typeInj @ss in
-               case readTerm tys CtxTyZ ast of
+               case readTerm CtxTyZ ast of
                 Left err -> Left (Right err) @?= snd `left` expected
                 Right term ->
                        case term of