Make stack flags customizable in GNUmakefile.

[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 541043cb36e65d9a87e505b83adc98f0150916ce..5bb79829b861b307131ddbc56054b7683dbf4604 100644 (file)
--- a/symantic-lib/Language/Symantic/Compiling/Test.hs
+++ b/symantic-lib/Language/Symantic/Compiling/Test.hs
@@ -1,7 +1,6 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE TypeInType #-}
-{-# LANGUAGE ViewPatterns #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 module Compiling.Test where
@@ -12,95 +11,61 @@ import Debug.Trace (trace)
 
 import Control.Arrow (left)
 import Data.Functor.Identity (Identity(..))
-import Data.Proxy (Proxy(..))
 import Data.Text (Text)
 import Data.Type.Equality
-import qualified Control.Monad.Classes as MC
 import qualified Control.Monad.Classes.Run as MC
 import qualified Control.Monad.Trans.State.Strict as SS
 import qualified Data.List as List
 import qualified Data.Text as Text
 import qualified Text.Megaparsec as P
 
+import Language.Symantic.Grammar
 import Language.Symantic
-import qualified Language.Symantic.Grammar as Gram
+import Language.Symantic.Lib ()
 
-import Grammar.MegaParsec
-import Typing.Test ()
+import Grammar.Megaparsec ()
 
--- P.ParsecT instances
-type instance MC.CanDo (P.ParsecT e s m) eff = 'False
-instance ParsecC e s => Gram_Name (P.ParsecT e s m)
-instance ParsecC e s => Gram.Gram_Meta () (P.ParsecT e s m) where
-       withMeta = (($ ()) <$>)
-instance
- ( ParsecC e s
- , Gram.Gram_Meta (Gram.Text_of_Source src) (P.ParsecT e s m)
- , Gram.Gram_Meta src (P.ParsecT e s m)
- , Inj_Source (Gram.Text_of_Source src) src
- ) => Gram_Term_Type src (P.ParsecT e s m)
-instance ParsecC e s => Gram.Gram_Error (Error_Term_Gram) (P.ParsecT e s m) where
-       catch me = do
-               e <- me
-               case e of
-                Left err -> fail $ show err
-                Right a -> return a
-instance
- ( ParsecC e s
- , Source src, Show src
- ) => Gram.Gram_Error (Error_Term src) (P.ParsecT e s m) where
-       catch me = do
-               e <- me
-               case e of
-                Left err -> fail $ show err
-                Right a -> return a
-instance
- ( ParsecC e s
- , Show src
- , Gram.Gram_Meta (Gram.Text_of_Source src) (P.ParsecT e s m)
- , Gram.Gram_Meta src (P.ParsecT e s m)
- , Gram_Term_Atoms src ss (P.ParsecT e s m)
- , Gram.Gram_Error Error_Term_Gram (P.ParsecT e s m)
- , MC.MonadState (Modules src ss) m
- , Inj_Source (Gram.Text_of_Source src) src
- ) => Gram_Term src ss (P.ParsecT e s m) where
-       modules_get (Gram.CF g) = Gram.CF $ do
-               toks <- MC.get
-               f <- g
-               return $ f toks
-       modules_put (Gram.CF g) = Gram.CF $ do
-               (toks, a) <- g
-               () <- MC.put toks
-               return a
+type G src ss =
+ P.ParsecT P.Dec Text
+           (SS.StateT (Imports NameTe, Modules src ss)
+                      ((SS.StateT (Imports NameTy, ModulesTy src))
+                                  Identity))
 
-test_modules ::
+parseTe ::
  forall ss src.
- Inj_Modules src ss =>
- Gram_Term src ss (P.ParsecT P.Dec Text (SS.StateT (Modules src ss) Identity)) =>
- Text ->
- Either (P.ParseError Char P.Dec) (AST_Term src ss)
-test_modules inp =
+ ImportTypes ss =>
+ ModulesTyInj ss =>
+ ModulesInj src ss =>
+ 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 (inj_modules::Modules src ss) $
+       MC.evalStateStrict (impsTy, modsTy) $
+       MC.evalStateStrict (impsTe, modsTe) $
        P.runParserT g "" inp
-       where g = Gram.unCF $ g_term <* Gram.eoi
+       where g = unCF $ g_term <* eoi
 
-test_readTe ::
+readTe ::
  forall src ss t.
  ( Eq t
- , Gram_Term src ss (P.ParsecT P.Dec Text (SS.StateT (Modules src ss) Identity))
+ , Eq src
+ , Gram_Term src ss (G src ss)
+ , ImportTypes ss
+ , ModulesInj src ss
+ , ModulesTyInj ss
+ , Show src
  , Show t
+ , SourceInj (AST_Type src) src
+ , SourceInj (KindK src) src
+ , SourceInj (TypeT src '[]) src
+ , SourceInj (TypeVT src) src
+ , Syms ss (BetaT View)
  , Syms ss Eval
  , Syms ss View
- , Syms ss (BetaT View)
- , Inj_Modules src ss
- , Eq src
- , Show src
- , Inj_Source (TypeVT src) src
- , Inj_Source (TypeT src '[]) src
- , Inj_Source (KindK src) src
- , Inj_Source (AST_Type src) src
- , Inj_Name2Type ss
  ) =>
  Text ->
  Either ( Type src '[] t
@@ -108,13 +73,12 @@ test_readTe ::
                  (Error_Term src) )
         (Type src '[] t, t, Text) ->
  TestTree
-test_readTe inp expected =
+readTe inp expected =
        testCase (elide inp) $
-       case reduceTeApp <$> test_modules @ss inp of
+       case reduceTeApp <$> parseTe @ss inp of
         Left err -> Left (Left err) @?= snd `left` expected
         Right ast ->
-               let tys = inj_Name2Type (Proxy @ss) in
-               case readTe tys ast CtxTyZ of
+               case readTerm CtxTyZ ast of
                 Left err -> Left (Right err) @?= snd `left` expected
                 Right term ->
                        case term of
@@ -127,13 +91,13 @@ test_readTe inp expected =
                                         LenS{} -> return $ Left $ Right $ Error_Term_polymorphic (TypeVT t)
                                         LenZ ->
                                                case proveConstraint q of
-                                                Nothing -> return $ Left $ Right $ Error_Term_qualified $ TypeVT t
-                                                Just Dict -> do
-                                                       case t `eqTy` ty_expected of
+                                                Nothing -> return $ Left $ Right $ Error_Term_proofless $ TypeVT t
+                                                Just Dict ->
+                                                       case t `eqType` ty_expected of
                                                         Nothing -> return $ Left $ Right $
                                                                Error_Term_Beta $ Error_Beta_Unify $
                                                                Error_Unify_mismatch (TypeVT t) (TypeVT ty_expected)
-                                                        Just Refl -> do
+                                                        Just Refl ->
                                                                return $ Right (t, eval $ te CtxTeZ, view $ betaT $ te CtxTeZ)
 
 maybeRight :: Either l r -> Maybe r