symantic-lib 0.0.2.20170703 → 0.0.3.20180213

raw patch · 49 files changed

+974/−1135 lines, 49 filesdep +bytestringdep +tasty-goldendep −ghc-primdep ~containersdep ~megaparsecdep ~monad-classesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: bytestring, tasty-golden

Dependencies removed: ghc-prim

Dependency ranges changed: containers, megaparsec, monad-classes, mono-traversable, symantic, tasty-hunit, text, transformers

API changes (from Hackage documentation)

Files

• Language/Symantic/Compiling/Test.hs +0/−112
• Language/Symantic/Grammar/EBNF.hs +0/−15
• Language/Symantic/Grammar/Megaparsec.hs +0/−167
• Language/Symantic/Lib/Alternative.hs +1/−1
• Language/Symantic/Lib/Applicative.hs +1/−1
• Language/Symantic/Lib/Applicative/Test.hs +0/−30
• Language/Symantic/Lib/Bool.hs +2/−2
• Language/Symantic/Lib/Bool/Test.hs +0/−86
• Language/Symantic/Lib/Char.hs +3/−3
• Language/Symantic/Lib/Either.hs +12/−12
• Language/Symantic/Lib/Foldable.hs +1/−1
• Language/Symantic/Lib/Foldable/Test.hs +0/−32
• Language/Symantic/Lib/Function.hs +14/−11
• Language/Symantic/Lib/Functor/Test.hs +0/−28
• Language/Symantic/Lib/IO.hs +7/−7
• Language/Symantic/Lib/Int.hs +1/−1
• Language/Symantic/Lib/Integer.hs +1/−1
• Language/Symantic/Lib/List.hs +6/−6
• Language/Symantic/Lib/Map.hs +12/−12
• Language/Symantic/Lib/Map/Test.hs +0/−44
• Language/Symantic/Lib/Maybe.hs +12/−12
• Language/Symantic/Lib/MonoFunctor.hs +6/−6
• Language/Symantic/Lib/MonoFunctor/Test.hs +0/−28
• Language/Symantic/Lib/NonNull.hs +8/−8
• Language/Symantic/Lib/Num/Test.hs +0/−98
• Language/Symantic/Lib/Ord.hs +1/−1
• Language/Symantic/Lib/Ratio.hs +3/−3
• Language/Symantic/Lib/Test.hs +0/−42
• Language/Symantic/Lib/Text.hs +9/−9
• Language/Symantic/Lib/Tuple2.hs +17/−17
• Language/Symantic/Lib/Tuple2/Test.hs +0/−29
• Language/Symantic/Lib/Unit.hs +1/−3
• Language/Symantic/Test.hs +0/−14
• Language/Symantic/Typing/Test.hs +0/−185
• stack.yaml +13/−0
• symantic-lib.cabal +79/−108
• test/Golden.hs +46/−0
• test/HUnit.hs +41/−0
• test/HUnit/Applicative.hs +28/−0
• test/HUnit/Bool.hs +84/−0
• test/HUnit/Foldable.hs +30/−0
• test/HUnit/Functor.hs +26/−0
• test/HUnit/Map.hs +42/−0
• test/HUnit/MonoFunctor.hs +26/−0
• test/HUnit/Num.hs +105/−0
• test/HUnit/Tuple2.hs +27/−0
• test/Main.hs +15/−0
• test/Testing/Compiling.hs +113/−0
• test/Testing/Megaparsec.hs +181/−0

@@ -1,112 +0,0 @@-{-# LANGUAGE AllowAmbiguousTypes #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE TypeInType #-}-{-# LANGUAGE UndecidableInstances #-}-{-# OPTIONS_GHC -fno-warn-orphans #-}-module Compiling.Test where--import Test.Tasty-import Test.Tasty.HUnit-import Debug.Trace (trace)--import Control.Arrow (left)-import Data.Functor.Identity (Identity(..))-import Data.Text (Text)-import Data.Type.Equality-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 Language.Symantic.Lib ()--import Grammar.Megaparsec ()--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 (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 (impsTy, modsTy) $-	MC.evalStateStrict (impsTe, modsTe) $-	P.runParserT g "" inp-	where g = unCF $ g_term <* eoi--readTe ::- forall src ss t.- ( Eq t- , 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- ) =>- Text ->- Either ( Type src '[] t-        , Either (P.ParseError Char P.Dec)-                 (Error_Term src) )-        (Type src '[] t, t, Text) ->- TestTree-readTe inp expected =-	testCase (elide inp) $-	case reduceTeApp <$> parseTe @ss inp of-	 Left err -> Left (Left err) @?= snd `left` expected-	 Right ast ->-		case readTerm CtxTyZ ast of-		 Left err -> Left (Right err) @?= snd `left` expected-		 Right term ->-			case term of-			 TermVT (Term q t (TeSym te)) ->-				case expected of-				 Left (_, err) -> Right ("…"::Text) @?= Left err-				 Right (ty_expected::Type src '[] t, _::t, _::Text) ->-					(>>= (@?= (\(_::Type src '[] t, err) -> err) `left` expected)) $-					case lenVars t of-					 LenS{} -> return $ Left $ Right $ Error_Term_polymorphic (TypeVT t)-					 LenZ ->-						case proveConstraint q 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 ->-								return $ Right (t, eval $ te CtxTeZ, view $ betaT $ te CtxTeZ)--maybeRight :: Either l r -> Maybe r-maybeRight (Right r) = Just r-maybeRight Left{}    = Nothing--elide :: Text -> String-elide s | Text.length s > 42 = List.take 42 (Text.unpack s) List.++ ['…']-elide s = Text.unpack s--dbg :: Show a => String -> a -> a-dbg msg x = trace (msg ++ " = " ++ Prelude.show x) x

@@ -1,15 +0,0 @@-module Grammar.EBNF where--import Data.Text.IO as Text-import Control.Monad--import Language.Symantic.Grammar-import Language.Symantic-import Language.Symantic.Lib ()--main :: IO ()-main = do-	forM_ gram_comment render-	forM_ gram_type render-	forM_ gram_term render-	where render = Text.putStrLn . renderEBNF . unCF

@@ -1,167 +0,0 @@-{-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE UndecidableInstances #-}-{-# OPTIONS_GHC -fno-warn-orphans #-}--- | Symantic instances for Megaparsec-module Grammar.Megaparsec where--import Control.Applicative (Applicative(..))-import Control.Monad (Monad(..))-import Data.Char (Char)-import Data.Either (Either(..))-import Data.Function (($), (.))-import Data.Functor (Functor(..), (<$>))-import Data.List.NonEmpty (NonEmpty(..))-import Data.Ord (Ord(..))-import Data.String (IsString(..))-import Data.Typeable ()-import Text.Show (Show(..))-import qualified Control.Applicative as Alt-import qualified Control.Monad.Classes as MC-import qualified Data.Char as Char-import qualified Data.Text as Text-import qualified Text.Megaparsec as P--import Language.Symantic.Grammar as Sym-import qualified Language.Symantic as Sym-import Language.Symantic.Lib ()---- * Type 'ParsecC'--- | Convenient alias for defining instances involving 'P.ParsecT'.-type ParsecC e s = (P.Token s ~ Char, P.Stream s, P.ErrorComponent e)-instance ParsecC e s => IsString (P.ParsecT e s m [Char]) where-	fromString = P.string------- Readers------- NonEmpty P.SourcePos-instance ParsecC e s => Sym.Gram_Reader (NonEmpty P.SourcePos) (P.ParsecT e s m) where-	askBefore g = do-		s <- P.statePos <$> P.getParserState-		($ s) <$> g-	askAfter g = do-		f <- g-		f . P.statePos <$> P.getParserState-type instance MC.CanDo (P.ParsecT e s m) (MC.EffReader (NonEmpty P.SourcePos)) = 'True-instance ParsecC e s => MC.MonadReaderN 'MC.Zero (NonEmpty P.SourcePos) (P.ParsecT e s m) where-	askN _n = P.statePos <$> P.getParserState--- P.SourcePos-instance ParsecC e s => Sym.Gram_Reader P.SourcePos (P.ParsecT e s m) where-	askBefore g = do-		s <- P.getPosition-		($ s) <$> g-	askAfter g = do-		f <- g-		f <$> P.getPosition-type instance MC.CanDo (P.ParsecT e s m) (MC.EffReader P.SourcePos) = 'True-instance ParsecC e s => MC.MonadReaderN 'MC.Zero P.SourcePos (P.ParsecT e s m) where-	askN _n = P.getPosition--- ()-instance ParsecC e s => Sym.Gram_Reader () (P.ParsecT e s m) where-	askBefore = fmap ($ ())-	askAfter  = fmap ($ ())------- States------- st-type instance MC.CanDo (P.ParsecT e s m) (MC.EffState st) = 'False-instance (Monad m, MC.MonadState st m) => Sym.Gram_State st m where-	stateBefore g = do-		s <- MC.get-		f <- g-		let (s', a) = f s-		MC.put s'-		return a-	stateAfter g = do-		f <- g-		s <- MC.get-		let (s_, a) = f s-		MC.put s_-		return a-	getBefore g = do-		s <- MC.get-		f <- g-		return (f s)-	getAfter g = do-		f <- g-		s <- MC.get-		return (f s)-	put g = do-		(s, a) <- g-		MC.put s-		return a------- Sym instances----instance (ParsecC e s, Show err) => Sym.Gram_Error err (P.ParsecT e s m) where-	catch me {- if you can :-} = do-		e <- me-		case e of-		 Left err -> fail $ show err-		 Right a -> return a-instance ParsecC e s => Sym.Gram_Rule (P.ParsecT e s m) where-	rule = P.label . Text.unpack-instance ParsecC e s => Sym.Gram_Terminal (P.ParsecT e s m) where-	any          = P.anyChar-	eoi          = P.eof-	char         = P.char-	string       = P.string-	unicat cat   = P.satisfy $ (`elem` cats) . Char.generalCategory-		where cats = unicode_categories cat-	range (l, h) = P.satisfy $ \c -> l <= c && c <= h-	Terminal f `but` Terminal p = Terminal $ P.notFollowedBy (P.try p) *> f-instance ParsecC e s => Sym.Gram_Alt (P.ParsecT e s m) where-	empty  = Alt.empty-	(<+>)  = (Alt.<|>)-	choice = P.choice-instance ParsecC e s => Sym.Gram_Try (P.ParsecT e s m) where-	try = P.try-instance ParsecC e s => Sym.Gram_RegR (P.ParsecT e s m) where-	Terminal f .*> Reg x = Reg $ f <*> x-instance ParsecC e s => Sym.Gram_RegL (P.ParsecT e s m) where-	Reg f <*. Terminal x = Reg $ f <*> x-instance ParsecC e s => Sym.Gram_App (P.ParsecT e s m) where-	between = P.between-instance ParsecC e s => Sym.Gram_AltApp (P.ParsecT e s m) where-	option   = P.option-	optional = P.optional-	many     = P.many-	some     = P.some-	skipMany = P.skipMany-instance ParsecC e s => Sym.Gram_CF (P.ParsecT e s m) where-	CF f <& Reg p        = CF $ P.lookAhead f <*> p-	Reg f &> CF p        = CF $ P.lookAhead f <*> p-	minus (CF f) (Reg p) = CF $ P.notFollowedBy (P.try p) *> f-instance ParsecC e s => Sym.Gram_Comment (P.ParsecT e s m)-instance ParsecC e s => Sym.Gram_Op (P.ParsecT e s m)-instance ParsecC e s => Sym.Gram_Mod (P.ParsecT e s m)-instance ParsecC e s => Sym.Gram_Type_Name (P.ParsecT e s m)-instance ParsecC e s => Sym.Gram_Term_Name (P.ParsecT e s m)-instance -- Sym.Gram_Type- ( ParsecC e s- , Gram_Source src (P.ParsecT e s m)- , Show src- , MC.MonadState ( Sym.Imports Sym.NameTy-                 , Sym.ModulesTy src ) (P.ParsecT e s m)- ) => Sym.Gram_Type src (P.ParsecT e s m)-instance -- Sym.Gram_Term_Type- ( ParsecC e s- , Show src- , MC.MonadState ( Sym.Imports Sym.NameTy-                 , Sym.ModulesTy src ) (P.ParsecT e s m)- , Gram_Source src           (P.ParsecT e s m)- ) => Sym.Gram_Term_Type src (P.ParsecT e s m)-instance -- Sym.Gram_Term- ( ParsecC e s- , Show src- , MC.MonadState ( Sym.Imports Sym.NameTy-                 , Sym.ModulesTy src )  (P.ParsecT e s m)- , MC.MonadState ( Sym.Imports Sym.NameTe-                 , Sym.Modules src ss ) (P.ParsecT e s m)- , Sym.Gram_Source src        (P.ParsecT e s m)- , Sym.Gram_Term_Atoms src ss (P.ParsecT e s m)- ) => Sym.Gram_Term src ss    (P.ParsecT e s m)

@@ -4,7 +4,7 @@ module Language.Symantic.Lib.Alternative where  import Control.Applicative (Alternative)-import Prelude hiding (Functor(..), (<$>), id, const)+import Prelude hiding (Functor(..)) import qualified Control.Applicative as Alternative  import Language.Symantic

@@ -4,7 +4,7 @@ module Language.Symantic.Lib.Applicative where  import Control.Applicative (Applicative)-import Prelude hiding (Functor(..), (<$>), Applicative(..), id, const)+import Prelude hiding (Functor(..), (<$>), Applicative(..)) import qualified Control.Applicative as Applicative import qualified Data.Function as Fun 

@@ -1,30 +0,0 @@-{-# OPTIONS_GHC -fno-warn-missing-signatures #-}-module Lib.Applicative.Test where--import Test.Tasty--import Data.Proxy (Proxy(..))-import Prelude hiding ((&&), not, (||))--import Language.Symantic.Lib-import Compiling.Test-import Lib.Bool.Test ()--type SS =- [ Proxy (->)- , Proxy Integer- , Proxy Bool- , Proxy Maybe- , Proxy Functor- , Proxy Applicative- ]-(==>) = readTe @() @SS--tests :: TestTree-tests = testGroup "Applicative"- [ "Just (xor True) <*> Just True"    ==> Right (tyMaybe tyBool, Just False, "Just (\\x0 -> True `xor` x0) <*> Just True")- , "Just (xor True) <*> Nothing"      ==> Right (tyMaybe tyBool, Nothing   , "Just (\\x0 -> True `xor` x0) <*> Nothing")- , "xor <$> Just True <*> Just False" ==> Right (tyMaybe tyBool, Just True , "(\\x0 -> (\\x1 -> x0 `xor` x1)) <$> Just True <*> Just False")- , "Just False <* Just True"          ==> Right (tyMaybe tyBool, Just False, "Just False <* Just True")- , "Just False *> Just True"          ==> Right (tyMaybe tyBool, Just True , "Just False *> Just True")- ]

@@ -58,8 +58,8 @@ instance NameTyOf Bool where 	nameTyOf _c = ["Bool"] `Mod` "Bool" instance ClassInstancesFor Bool where-	proveConstraintFor _ (TyApp _ (TyConst _ _ q) c)-	 | Just HRefl <- proj_ConstKiTy @_ @Bool c+	proveConstraintFor _ (TyConst _ _ q :@ b)+	 | Just HRefl <- proj_ConstKiTy @_ @Bool b 	 = case () of 		 _ | Just Refl <- proj_Const @Bounded q -> Just Dict 		   | Just Refl <- proj_Const @Enum    q -> Just Dict

@@ -1,86 +0,0 @@-{-# OPTIONS_GHC -fno-warn-missing-signatures #-}-module Lib.Bool.Test where--import Test.Tasty--import Data.Proxy (Proxy(..))-import Prelude hiding ((&&), not, (||))--import Language.Symantic-import Language.Symantic.Lib--- import Language.Symantic.Lib.Lambda ((~>))-import Compiling.Test--type SS =- [ Proxy Bool- , Proxy (->)- , Proxy Integer- , Proxy []- , Proxy Char- ]-(==>) = readTe @() @SS--tests :: TestTree-tests = testGroup "Bool" $- [ "True"                           ==> Right (tyBool, True , "True")- , "xor True True"                  ==> Right (tyBool, False, "True `xor` True")- , "xor False True"                 ==> Right (tyBool, True , "False `xor` True")- , "True `xor` True"                ==> Right (tyBool, False, "True `xor` True")- , "(\\(xy:Bool) -> xy) True"       ==> Right (tyBool, True , "(\\x0 -> x0) True")- , "(\\(False:Bool) -> False) True" ==> Right (tyBool, True , "(\\x0 -> x0) True")- , "(\\(lett:Bool) -> lett) True"   ==> Right (tyBool, True , "(\\x0 -> x0) True")- , "(\\(x:Bool) -> xor x x) True"   ==> Right (tyBool, False, "(\\x0 -> x0 `xor` x0) True")- , "let x = True in xor x True"     ==> Right (tyBool, False, "let x0 = True in x0 `xor` True")- , "(\\(False:Bool) -> False) (False `xor` True)" ==> Right (tyBool, True, "(\\x0 -> x0) (False `xor` True)")- , testGroup "Error_Term"-	 [ "True True" ==> Left (tyBool,-		Right $ Error_Term_Beta $-		Error_Beta_Term_not_a_function $-		TypeVT $ tyBool @_ @'[])-	 , "x" ==> Left (tyBool,-		Right $ Error_Term_unknown $ NameTe "x")-	 , "x `xor` True" ==> Left (tyBool,-		Right $ Error_Term_unknown $ NameTe "x")-	 , "(\\(x:Bool) -> x `xor` True) Bool" ==> Left (tyBool,-		Right $ Error_Term_unknown $ NameTe "Bool")-	 , "(\\(x:Bool) -> x) True True" ==> Left (tyBool,-		Right $ Error_Term_Beta $-		Error_Beta_Term_not_a_function $-		TypeVT $ tyBool @_ @'[])-	 , "(\\(x:Bool -> Bool) -> x True) True" ==> Left (tyBool,-		Right $ Error_Term_Beta $ Error_Beta_Unify $-		Error_Unify_Const_mismatch-		 (TypeVT $ tyFun @_ @'[])-		 (TypeVT $ tyBool @_ @'[]))-	 ]- ]---- * Class 'Sym_Bool_Vars'--- | A few boolean variables.-class Sym_Bool_Vars repr where-	x :: repr Bool-	y :: repr Bool-	z :: repr Bool-instance Sym_Bool_Vars View where-	x = View $ \_p _v -> "x"-	y = View $ \_p _v -> "y"-	z = View $ \_p _v -> "z"-{--instance -- Trans_Boo_Const- ( Sym_Bool repr- , Sym_Bool_Vars repr- ) => Sym_Bool_Vars (Trans_Bool_Const repr) where-	x = trans_lift x-	y = trans_lift y-	z = trans_lift z--}---- * EDSL tests-te1 = bool True && bool False-te2 = (bool True && bool False) ||  (bool True && bool True)-te3 = (bool True ||  bool False) && (bool True ||  bool True)-te4 = bool True && not (bool False)-te5 = bool True && not x-te6 = x `xor` y-te7 = (x `xor` y) `xor` z-te8 = x `xor` (y `xor` bool True)

@@ -6,7 +6,7 @@ import qualified Data.Char as Char import qualified Data.Text as Text -import Language.Symantic.Grammar hiding (char, any)+import Language.Symantic.Grammar hiding (char) import qualified Language.Symantic.Grammar as G import Language.Symantic import Language.Symantic.Lib.List (tyList)@@ -48,7 +48,7 @@ instance NameTyOf Char where 	nameTyOf _c = ["Char"] `Mod` "Char" instance ClassInstancesFor Char where-	proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)+	proveConstraintFor _ (TyConst _ _ q :@ z) 	 | Just HRefl <- proj_ConstKiTy @_ @Char z 	 = case () of 		 _ | Just Refl <- proj_Const @Bounded q -> Just Dict@@ -78,7 +78,7 @@ 		 ) 	 ] 		where-		tickG :: Gram_Terminal g' => g' Char+		tickG :: Gram_Char g' => g' Char 		tickG = G.char '\'' instance (Source src, SymInj ss Char) => ModuleFor src ss Char where 	moduleFor = ["Char"] `moduleWhere`

@@ -48,8 +48,8 @@ 	nameTyOf _c = ["Either"] `Mod` "Either" instance FixityOf Either instance ClassInstancesFor Either where-	proveConstraintFor _ (TyApp _ (TyConst _ _ q) (TyApp _ c _l))-	 | Just HRefl <- proj_ConstKiTy @_ @Either c+	proveConstraintFor _ (TyConst _ _ q :$ e:@_l)+	 | Just HRefl <- proj_ConstKiTy @_ @Either e 	 = case () of 		 _ | Just Refl <- proj_Const @Functor     q -> Just Dict 		   | Just Refl <- proj_Const @Applicative q -> Just Dict@@ -57,26 +57,26 @@ 		   | Just Refl <- proj_Const @Foldable    q -> Just Dict 		   | Just Refl <- proj_Const @Traversable q -> Just Dict 		 _ -> Nothing-	proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ (TyApp _ c l) r))-	 | Just HRefl <- proj_ConstKiTy @_ @Either c+	proveConstraintFor _ (tq@(TyConst _ _ q) :$ e:@l:@r)+	 | Just HRefl <- proj_ConstKiTy @_ @Either e 	 = case () of 		 _ | Just Refl <- proj_Const @Eq q-		   , Just Dict <- proveConstraint (tq `tyApp` l)-		   , Just Dict <- proveConstraint (tq `tyApp` r) -> Just Dict+		   , Just Dict <- proveConstraint (tq`tyApp`l)+		   , Just Dict <- proveConstraint (tq`tyApp`r) -> Just Dict 		   | Just Refl <- proj_Const @Ord q-		   , Just Dict <- proveConstraint (tq `tyApp` l)-		   , Just Dict <- proveConstraint (tq `tyApp` r) -> Just Dict+		   , Just Dict <- proveConstraint (tq`tyApp`l)+		   , Just Dict <- proveConstraint (tq`tyApp`r) -> Just Dict 		   | Just Refl <- proj_Const @Show q-		   , Just Dict <- proveConstraint (tq `tyApp` l)-		   , Just Dict <- proveConstraint (tq `tyApp` r) -> Just Dict+		   , Just Dict <- proveConstraint (tq`tyApp`l)+		   , Just Dict <- proveConstraint (tq`tyApp`r) -> Just Dict 		   | Just Refl <- proj_Const @MT.MonoFoldable q -> Just Dict 		   | Just Refl <- proj_Const @MT.MonoFunctor  q -> Just Dict 		 _ -> Nothing 	proveConstraintFor _c _q = Nothing instance TypeInstancesFor Either where-	expandFamFor _c _len f (TyApp _ (TyApp _ c _ty_l) r `TypesS` TypesZ)+	expandFamFor _c _len f (e:@_ty_l:@r `TypesS` TypesZ) 	 | Just HRefl <- proj_ConstKi @_ @Element f-	 , Just HRefl <- proj_ConstKiTy @_ @Either c+	 , Just HRefl <- proj_ConstKiTy @_ @Either e 	 = Just r 	expandFamFor _c _len _fam _as = Nothing 

@@ -10,7 +10,7 @@ import qualified Data.Foldable as Foldable import Prelude hiding (Foldable(..)  , all, and, any, concat, concatMap- , mapM_, notElem, or, sequence, sequence_)+ , mapM_, notElem, or, sequence_)  import Language.Symantic import Language.Symantic.Lib.Alternative (tyAlternative)

@@ -1,32 +0,0 @@-{-# OPTIONS_GHC -fno-warn-missing-signatures #-}-module Lib.Foldable.Test where--import Test.Tasty--import Data.Proxy (Proxy(..))-import Prelude hiding ((&&), not, (||))--import Language.Symantic.Lib-import Compiling.Test--type SS =- [ Proxy (->)- , Proxy Int- , Proxy Integer- , Proxy []- , Proxy ()- , Proxy (,)- , Proxy Foldable- ]-(==>) = readTe @() @SS--tests :: TestTree-tests = testGroup "Foldable"- [ {-"[]" ==> Right (tyList (tyVar "a" varZ), [], "[]")- ,-} "[1, 2, 3]" ==> Right (tyList tyInteger, [1, 2, 3], "1 : 2 : 3 : []")- , "1 : 2 : 3 : []" ==> Right (tyList tyInteger, [1, 2, 3], "1 : 2 : 3 : []")- , "foldMap (\\(x0:Integer) -> [x0, x0]) [1, 2, 3]" ==> Right-	 ( tyList tyInteger-	 , [1, 1, 2, 2, 3, 3]-	 , "foldMap (\\x0 -> x0 : x0 : []) (1 : 2 : 3 : [])" )- ]

@@ -49,19 +49,19 @@ instance NameTyOf (->) where 	nameTyOf _c = [] `Mod` "->" instance ClassInstancesFor (->) where-	proveConstraintFor _c (TyApp _ q (TyApp _ z _r))-	 | Just HRefl <- proj_ConstKiTy @_ @(->) z+	proveConstraintFor _c (TyConst _ _ q :$ f:@_r)+	 | Just HRefl <- proj_ConstKiTy @_ @(->) f 	 = case () of-		 _ | Just HRefl <- proj_ConstKiTy @_ @Functor     q -> Just Dict-		   | Just HRefl <- proj_ConstKiTy @_ @Applicative q -> Just Dict-		   | Just HRefl <- proj_ConstKiTy @_ @Monad       q -> Just Dict+		 _ | Just Refl <- proj_Const @Functor     q -> Just Dict+		   | Just Refl <- proj_Const @Applicative q -> Just Dict+		   | Just Refl <- proj_Const @Monad       q -> Just Dict 		 _ -> Nothing-	proveConstraintFor _c (TyApp _ q (TyApp _ (TyApp _ z _a) b))-	 | Just HRefl <- proj_ConstKiTy @_ @(->) z+	proveConstraintFor _c (tq@(TyConst _ _ q) :$ f:@_a:@b)+	 | Just HRefl <- proj_ConstKiTy @_ @(->) f 	 = case () of-		 _ | Just HRefl <- proj_ConstKiTy @_ @Monoid q-		   , Just Dict  <- proveConstraint (q `tyApp` b) -> Just Dict-		   | Just HRefl <- proj_ConstKiTy @_ @MT.MonoFunctor q -> Just Dict+		 _ | Just Refl <- proj_Const @Monoid q+		   , Just Dict <- proveConstraint (tq`tyApp`b) -> Just Dict+		   | Just Refl <- proj_Const @MT.MonoFunctor q -> Just Dict 		 _ -> Nothing 	proveConstraintFor _c _q = Nothing instance TypeInstancesFor (->)@@ -74,7 +74,7 @@ 	 , "flip"  := teFunction_flip 	 , "id"    := teFunction_id 	 , "." `withInfixR` 9 := teFunction_compose-	 -- , "$" `withInfixR` 0 := teFunction_app+	 , "$" `withInfixR` 0 := teFunction_apply 	 ]  -- ** 'Type's@@ -105,3 +105,6 @@  teFunction_id :: TermDef (->) '[Proxy a] (() #> (a -> a)) teFunction_id = Term noConstraint (a0 ~> a0) $ teSym @(->) $ lam1 id++teFunction_apply :: TermDef (->) '[Proxy a, Proxy b] (() #> ((a -> b) -> a -> b))+teFunction_apply = Term noConstraint ((a0 ~> b1) ~> a0 ~> b1) $ teSym @(->) apply

@@ -1,28 +0,0 @@-{-# OPTIONS_GHC -fno-warn-missing-signatures #-}-module Lib.Functor.Test where--import Test.Tasty--import Data.Proxy (Proxy(..))-import Prelude hiding ((&&), not, (||))--import Language.Symantic ()-import Language.Symantic.Lib-import Compiling.Test--type SS =- [ Proxy (->)- , Proxy Bool- , Proxy Functor- , Proxy Integer- , Proxy Maybe- ]-(==>) = readTe @() @SS--tests :: TestTree-tests = testGroup "Functor"- [ "fmap not (Just True)" ==> Right (tyMaybe tyBool, Just False, "fmap (\\x0 -> not x0) (Just True)")- , "not `fmap` Just True" ==> Right (tyMaybe tyBool, Just False, "fmap (\\x0 -> not x0) (Just True)")- , "not <$> Just True"    ==> Right (tyMaybe tyBool, Just False, "(\\x0 -> not x0) <$> Just True")- , "False <$ Just True"   ==> Right (tyMaybe tyBool, Just False, "False <$ Just True")- ]

@@ -60,28 +60,28 @@ 	nameTyOf _c = ["IO"] `Mod` "IOMode" instance FixityOf IO instance ClassInstancesFor IO where-	proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)+	proveConstraintFor _ (TyConst _ _ q :$ z) 	 | Just HRefl <- proj_ConstKiTy @_ @IO z 	 = case () of 		 _ | Just Refl <- proj_Const @Applicative q -> Just Dict 		   | Just Refl <- proj_Const @Functor     q -> Just Dict 		   | Just Refl <- proj_Const @Monad       q -> Just Dict 		 _ -> Nothing-	proveConstraintFor _ (TyApp _ q (TyApp _ z _a))+	proveConstraintFor _ (TyConst _ _ q :$ z:@_a) 	 | Just HRefl <- proj_ConstKiTy @_ @IO z 	 = case () of-		 _ | Just Refl <- proj_ConstTy @MT.MonoFunctor q -> Just Dict+		 _ | Just Refl <- proj_Const @MT.MonoFunctor q -> Just Dict 		 _ -> Nothing 	proveConstraintFor _c _q = Nothing instance ClassInstancesFor IO.Handle where-	proveConstraintFor _ (TyApp _ q z)+	proveConstraintFor _ (TyConst _ _ q :$ z) 	 | Just HRefl <- proj_ConstKiTy @_ @IO.Handle z 	 = case () of-		 _ | Just Refl <- proj_ConstTy @Eq q -> Just Dict+		 _ | Just Refl <- proj_Const @Eq q -> Just Dict 		 _ -> Nothing 	proveConstraintFor _c _q = Nothing instance ClassInstancesFor IO.IOMode where-	proveConstraintFor _ (TyApp _ (TyConst _ _ q) c)+	proveConstraintFor _ (TyConst _ _ q :$ c) 	 | Just HRefl <- proj_ConstKiTy @_ @IO.IOMode c 	 = case () of 		 _ | Just Refl <- proj_Const @Enum q -> Just Dict@@ -90,7 +90,7 @@ 		 _ -> Nothing 	proveConstraintFor _c _q = Nothing instance TypeInstancesFor IO where-	expandFamFor _c _len f (TyApp _ z a `TypesS` TypesZ)+	expandFamFor _c _len f (z:@a `TypesS` TypesZ) 	 | Just HRefl <- proj_ConstKi @_ @Element f 	 , Just HRefl <- proj_ConstKiTy @_ @IO z 	 = Just a

@@ -30,7 +30,7 @@ instance NameTyOf Int where 	nameTyOf _c = ["Int"] `Mod` "Int" instance ClassInstancesFor Int where-	proveConstraintFor _c (TyApp _ (TyConst _ _ q) z)+	proveConstraintFor _c (TyConst _ _ q :$ z) 	 | Just HRefl <- proj_ConstKiTy @_ @Int z 	 = case () of 		 _ | Just Refl <- proj_Const @Bounded  q -> Just Dict

@@ -31,7 +31,7 @@ instance NameTyOf Integer where 	nameTyOf _c = ["Integer"] `Mod` "Integer" instance ClassInstancesFor Integer where-	proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)+	proveConstraintFor _ (TyConst _ _ q :$ z) 	 | Just HRefl <- proj_ConstKiTy @_ @Integer z 	 = case () of 		 _ | Just Refl <- proj_Const @Enum     q -> Just Dict

@@ -66,7 +66,7 @@ 	nameTyOf _c = [] `Mod` "[]" instance FixityOf [] instance ClassInstancesFor [] where-	proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)+	proveConstraintFor _ (TyConst _ _ q :$ z) 	 | Just HRefl <- proj_ConstKiTy @_ @[] z 	 = case () of 		 _ | Just Refl <- proj_Const @Applicative q -> Just Dict@@ -75,16 +75,16 @@ 		   | Just Refl <- proj_Const @Monad       q -> Just Dict 		   | Just Refl <- proj_Const @Traversable q -> Just Dict 		 _ -> Nothing-	proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ z a))+	proveConstraintFor _ (tq@(TyConst _ _ q) :$ z:@a) 	 | Just HRefl <- proj_ConstKiTy @_ @[] z 	 = case () of 		 _ | Just Refl <- proj_Const @Eq q-		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict+		   , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict 		   | Just Refl <- proj_Const @Monoid q -> Just Dict 		   | Just Refl <- proj_Const @Show q-		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict+		   , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict 		   | Just Refl <- proj_Const @Ord q-		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict+		   , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict 		   | Just Refl <- proj_Const @MT.MonoFoldable   q -> Just Dict 		   | Just Refl <- proj_Const @MT.MonoFunctor    q -> Just Dict 		   | Just Refl <- proj_Const @Seqs.IsSequence   q -> Just Dict@@ -92,7 +92,7 @@ 		 _ -> Nothing 	proveConstraintFor _c _q = Nothing instance TypeInstancesFor [] where-	expandFamFor _c _len f ((TyApp _ z a) `TypesS` TypesZ)+	expandFamFor _c _len f (z:@a `TypesS` TypesZ) 	 | Just HRefl <- proj_ConstKi   @_ @Element f 	 , Just HRefl <- proj_ConstKiTy @_ @[] z 	 = Just a

@@ -89,34 +89,34 @@ 	nameTyOf _c = ["Map"] `Mod` "Map" instance FixityOf Map instance ClassInstancesFor Map where-	proveConstraintFor _ (TyApp _ (TyConst _ _ q) (TyApp _ c _k))-	 | Just HRefl <- proj_ConstKiTy @_ @Map c+	proveConstraintFor _ (TyConst _ _ q :$ m:@_k)+	 | Just HRefl <- proj_ConstKiTy @_ @Map m 	 = case () of 		 _ | Just Refl <- proj_Const @Functor     q -> Just Dict 		   | Just Refl <- proj_Const @Foldable    q -> Just Dict 		   | Just Refl <- proj_Const @Traversable q -> Just Dict 		 _ -> Nothing-	proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ (TyApp _ c k) a))-	 | Just HRefl <- proj_ConstKiTy @_ @Map c+	proveConstraintFor _ (tq@(TyConst _ _ q) :$ m:@k:@a)+	 | Just HRefl <- proj_ConstKiTy @_ @Map m 	 = case () of 		 _ | Just Refl <- proj_Const @Eq q-		   , Just Dict <- proveConstraint (tq `tyApp` k)-		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict+		   , Just Dict <- proveConstraint (tq`tyApp`k)+		   , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict 		   | Just Refl <- proj_Const @Ord q-		   , Just Dict <- proveConstraint (tq `tyApp` k)-		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict+		   , Just Dict <- proveConstraint (tq`tyApp`k)+		   , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict 		   | Just Refl <- proj_Const @Monoid q 		   , Just Dict <- proveConstraint (tyConstLen @(K Ord) @Ord (lenVars k) `tyApp` k) -> Just Dict 		   | Just Refl <- proj_Const @Show q-		   , Just Dict <- proveConstraint (tq `tyApp` k)-		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict+		   , Just Dict <- proveConstraint (tq`tyApp`k)+		   , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict 		   | Just Refl <- proj_Const @MonoFunctor q -> Just Dict 		 _ -> Nothing 	proveConstraintFor _c _q = Nothing instance TypeInstancesFor Map where-	expandFamFor _c _len f (TyApp _ (TyApp _ c _k) a `TypesS` TypesZ)+	expandFamFor _c _len f (m:@_k:@a `TypesS` TypesZ) 	 | Just HRefl <- proj_ConstKi @_ @Element f-	 , Just HRefl <- proj_ConstKiTy @_ @Map c+	 , Just HRefl <- proj_ConstKiTy @_ @Map m 	 = Just a 	expandFamFor _c _len _fam _as = Nothing 

@@ -1,44 +0,0 @@-{-# OPTIONS_GHC -fno-warn-missing-signatures #-}-module Lib.Map.Test where--import Test.Tasty--import Data.Map.Strict (Map)-import Data.Proxy (Proxy(..))-import Data.Text as Text-import Prelude hiding (zipWith)-import qualified Data.Map.Strict as Map--import Language.Symantic.Lib-import Compiling.Test--type SS =- [ Proxy (->)- , Proxy []- , Proxy Int- , Proxy Integer- , Proxy Map- , Proxy Char- , Proxy (,)- , Proxy Num- , Proxy Monoid- ]-(==>) = readTe @() @SS--tests :: TestTree-tests = testGroup "Map"- [ "Map.fromList (zipWith (,) [1, 2, 3] ['a', 'b', 'c'])" ==> Right-	 ( tyMap tyInteger tyChar-	 , Map.fromList [(1, 'a'), (2, 'b'), (3, 'c')]-	 , "Map.fromList (zipWith (\\x0 -> (\\x1 -> (x0, x1))) (1 : 2 : 3 : []) ('a' : 'b' : 'c' : []))" )- , Text.concat-	[ "Map.foldrWithKey"-	, " (\\(k:Integer) (v:Char) (acc:(Integer,[Char])) ->"-	, "  (k + fst acc, v : snd acc))"-	, " (0, [])"-	, " (Map.fromList (zipWith (,) [1, 2, 3] ['a', 'b', 'c']))"-	] ==> Right-	 ( tyInteger `tyTuple2` tyString-	 , (6, "abc")-	 , "Map.foldrWithKey (\\x0 -> (\\x1 -> (\\x2 -> (x0 + fst x2, x1 : snd x2)))) (0, []) (Map.fromList (zipWith (\\x0 -> (\\x1 -> (x0, x1))) (1 : 2 : 3 : []) ('a' : 'b' : 'c' : [])))" )- ]

@@ -49,32 +49,32 @@ 	nameTyOf _c = ["Maybe"] `Mod` "Maybe" instance FixityOf Maybe instance ClassInstancesFor Maybe where-	proveConstraintFor _ (TyApp _ (TyConst _ _ q) c)-	 | Just HRefl <- proj_ConstKiTy @_ @Maybe c+	proveConstraintFor _ (TyConst _ _ q :$ m)+	 | Just HRefl <- proj_ConstKiTy @_ @Maybe m 	 = case () of 		 _ | Just Refl <- proj_Const @Applicative q -> Just Dict-		   | Just Refl <- proj_Const @Foldable q    -> Just Dict-		   | Just Refl <- proj_Const @Functor q     -> Just Dict-		   | Just Refl <- proj_Const @Monad q       -> Just Dict+		   | Just Refl <- proj_Const @Foldable    q -> Just Dict+		   | Just Refl <- proj_Const @Functor     q -> Just Dict+		   | Just Refl <- proj_Const @Monad       q -> Just Dict 		   | Just Refl <- proj_Const @Traversable q -> Just Dict 		 _ -> Nothing-	proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ c a))-	 | Just HRefl <- proj_ConstKiTy @_ @Maybe c+	proveConstraintFor _ (tq@(TyConst _ _ q) :$ m:@a)+	 | Just HRefl <- proj_ConstKiTy @_ @Maybe m 	 = case () of 		 _ | Just Refl <- proj_Const @Eq q-		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict+		   , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict 		   | Just Refl <- proj_Const @Monoid q-		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict+		   , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict 		   | Just Refl <- proj_Const @Show q-		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict+		   , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict 		   | Just Refl <- proj_Const @MT.MonoFoldable q -> Just Dict 		   | Just Refl <- proj_Const @MT.MonoFunctor q  -> Just Dict 		 _ -> Nothing 	proveConstraintFor _c _q = Nothing instance TypeInstancesFor Maybe where-	expandFamFor _c _len f (TyApp _ c a `TypesS` TypesZ)+	expandFamFor _c _len f (m:@a `TypesS` TypesZ) 	 | Just HRefl <- proj_ConstKi @_ @Element f-	 , Just HRefl <- proj_ConstKiTy @_ @Maybe c+	 , Just HRefl <- proj_ConstKiTy @_ @Maybe m 	 = Just a 	expandFamFor _c _len _fam _as = Nothing 

@@ -16,7 +16,7 @@ 	nameTyOf _c = ["MonoFunctor"] `Mod` "Element" instance ClassInstancesFor Element instance TypeInstancesFor Element where-	expandFamFor _c _len f (TyApp _ (TyApp _ z _ty_r) a `TypesS` TypesZ)+	expandFamFor _c _len f (z:@_ty_r:@ a `TypesS` TypesZ) 	 | Just HRefl <- proj_ConstKi @_ @Element f 	 , Just HRefl <- proj_ConstKiTy @_ @(->) z 	 = Just a@@ -30,11 +30,11 @@ type instance Sym MonoFunctor = Sym_MonoFunctor class Sym_MonoFunctor term where 	omap :: MonoFunctor o => term (MT.Element o -> MT.Element o) -> term o -> term o-	default omap-	 :: Sym_MonoFunctor (UnT term)-	 => Trans term-	 => MonoFunctor o-	 => term (MT.Element o -> MT.Element o) -> term o -> term o+	default omap ::+	 Sym_MonoFunctor (UnT term) =>+	 Trans term =>+	 MonoFunctor o =>+	 term (MT.Element o -> MT.Element o) -> term o -> term o 	omap = trans2 omap  -- Interpreting

@@ -1,28 +0,0 @@-{-# OPTIONS_GHC -fno-warn-missing-signatures #-}-module Lib.MonoFunctor.Test where--import Test.Tasty--import Data.Proxy (Proxy(..))-import Prelude hiding (zipWith)-import qualified Data.MonoTraversable as MT--import Language.Symantic.Lib-import Compiling.Test--type SS =- [ Proxy (->)- , Proxy []- , Proxy Integer- , Proxy Bool- , Proxy Char- , Proxy MT.MonoFunctor- , Proxy Maybe- ]-(==>) = readTe @() @SS--tests :: TestTree-tests = testGroup "MonoFunctor"- [ "omap not (Just True)" ==> Right (tyMaybe tyBool, Just False, "omap (\\x0 -> not x0) (Just True)")- , "omap Char.toUpper ['a', 'b', 'c']" ==> Right (tyList tyChar, "ABC", "omap (\\x0 -> Char.toUpper x0) ('a' : 'b' : 'c' : [])" )- ]

@@ -89,27 +89,27 @@ 	nameTyOf _c = ["NonNull"] `Mod` "NonNull" instance FixityOf NonNull instance TypeInstancesFor NonNull where-	expandFamFor c len f (TyApp _ z o `TypesS` TypesZ)+	expandFamFor c len f (z:@o `TypesS` TypesZ) 	 | Just HRefl <- proj_ConstKi @_ @Element f 	 , Just HRefl <- proj_ConstKiTy @_ @NonNull z 	 = expandFamFor c len f (o `TypesS` TypesZ) 	expandFamFor _c _len _fam _as = Nothing instance ClassInstancesFor NonNull where-	proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ c o))+	proveConstraintFor _ (tq@(TyConst _ _ q) :$ c:@o) 	 | Just HRefl <- proj_ConstKiTy @_ @NonNull c 	 = case () of 		 _ | Just Refl <- proj_Const @Eq q-		   , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict+		   , Just Dict <- proveConstraint (tq`tyApp`o) -> Just Dict 		   | Just Refl <- proj_Const @MT.MonoFoldable q-		   , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict+		   , Just Dict <- proveConstraint (tq`tyApp`o) -> Just Dict 		   | Just Refl <- proj_Const @MT.MonoFunctor q-		   , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict+		   , Just Dict <- proveConstraint (tq`tyApp`o) -> Just Dict 		   | Just Refl <- proj_Const @Ord q-		   , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict+		   , Just Dict <- proveConstraint (tq`tyApp`o) -> Just Dict 		   | Just Refl <- proj_Const @SemiSequence q-		   , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict+		   , Just Dict <- proveConstraint (tq`tyApp`o) -> Just Dict 		   | Just Refl <- proj_Const @Show q-		   , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict+		   , Just Dict <- proveConstraint (tq`tyApp`o) -> Just Dict 		 _ -> Nothing 	proveConstraintFor _c _q = Nothing 

@@ -1,98 +0,0 @@-{-# LANGUAGE UndecidableInstances #-}-{-# OPTIONS_GHC -fno-warn-missing-signatures #-}-{-# OPTIONS_GHC -fno-warn-orphans #-}-module Lib.Num.Test where--import Test.Tasty--import Prelude (Num)-import Prelude hiding (Num(..))--import Language.Symantic-import Language.Symantic.Lib-import Compiling.Test---- * Tests-type SS =- [ Proxy (->)- , Proxy Integer- , Proxy Num- , Proxy Num2- , Proxy Int- , Proxy Integral- , Proxy Foldable- , Proxy Traversable- , Proxy []- ]-(==>) = readTe @() @SS--tests :: TestTree-tests = testGroup "Num"- [ "42"                        ==> Right (tyInteger,  42, "42")- , "-42"                       ==> Right (tyInteger, -42, "negate 42")- , "- -42"                     ==> Right (tyInteger,  42, "negate (negate 42)")- , "1 + -2"                    ==> Right (tyInteger,  -1, "1 + negate 2")- , "-1 + -2"                   ==> Right (tyInteger,  -3, "negate 1 + negate 2")- , "-(1 + -2)"                 ==> Right (tyInteger,   1, "negate (1 + negate 2)")- , "(+) 1 2"                   ==> Right (tyInteger,   3, "1 + 2")- , "1 + 2"                     ==> Right (tyInteger,   3, "1 + 2")- , "1 + 2 - 3"                 ==> Right (tyInteger,   0, "1 + 2 - 3")- , "1 + 2 * 3"                 ==> Right (tyInteger,   7, "1 + 2 * 3")- , "3 * 2 + 1"                 ==> Right (tyInteger,   7, "3 * 2 + 1")- , "3 * (2 + 1)"               ==> Right (tyInteger,   9, "3 * (2 + 1)")- , "4 + 3 * 2 + 1"             ==> Right (tyInteger,  11, "4 + 3 * 2 + 1")- , "5 * 4 + 3 * 2 + 1"         ==> Right (tyInteger,  27, "5 * 4 + 3 * 2 + 1")- , "negate`42"                 ==> Right (tyInteger, -42, "negate 42")- , "42`negate"                 ==> Right (tyInteger, -42, "negate 42")- , "42`negate "                ==> Right (tyInteger, -42, "negate 42")- , "42`negate`negate"          ==> Right (tyInteger,  42, "negate (negate 42)")- , "42`abs`negate"             ==> Right (tyInteger, -42, "negate (abs 42)")- , "42`negate`abs"             ==> Right (tyInteger,  42, "abs (negate 42)")- , "abs`negate`42"             ==> Right (tyInteger,  42, "abs (negate 42)")- , "negate`abs`42"             ==> Right (tyInteger, -42, "negate (abs 42)")- , "negate`abs`42`mod`9"       ==> Right (tyInteger,   3, "negate (abs 42) `mod` 9")- , "negate abs`42"             ==> Right (tyInteger, -42, "negate (abs 42)")- , "negate 42`abs"             ==> Right (tyInteger, -42, "negate (abs 42)")- , "(+) negate`2 44"           ==> Right (tyInteger,  42, "negate 2 + 44")- , "(+) 2`negate 44"           ==> Right (tyInteger,  42, "negate 2 + 44")- , "(+) (negate`2) 44"         ==> Right (tyInteger,  42, "negate 2 + 44")- , "abs negate`42"             ==> Right (tyInteger,  42, "abs (negate 42)")- , "(+) 40 2"                  ==> Right (tyInteger,  42, "40 + 2")- , "(+) 40 -2"                 ==> Right (tyInteger,  38, "40 + negate 2")- , "negate 42 + 42`negate"     ==> Right (tyInteger, -84, "negate 42 + negate 42")- , "(+) (negate 42) 42`negate" ==> Right (tyInteger, -84, "negate 42 + negate 42")- , "(+) negate`42 42`negate"   ==> Right (tyInteger, -84, "negate 42 + negate 42")- , "42`abs`negate`mod`abs`negate`9" ==> Right (tyInteger, 3, "negate (abs 42) `mod` abs (negate 9)")- , "abs`42`negate"             ==> Right (tyInteger,  42, "abs (negate 42)")- , "negate`42`abs"             ==> Right (tyInteger,  42, "abs (negate 42)")- , testGroup "Error_Term"-	 [ "(+) 40 - 2" ==> Left (tyInteger,-		Right $ Error_Term_Beta $ Error_Beta_Unify $-		Error_Unify_Const_mismatch-		 (TypeVT $ tyFun @_ @'[])-		 (TypeVT $ tyInteger @_ @'[]))-	 ]- ]---- | A newtype to test prefix and postfix.-newtype Num2 a = Num2 a-type instance Sym Num2 = Sym_Num2-class Sym_Num2 (term:: * -> *) where--instance Sym_Num2 Eval where-instance Sym_Num2 View where-instance Sym_Num2 (Dup r1 r2) where-instance Sym_Num2 term => Sym_Num2 (BetaT term) where-instance NameTyOf Num2 where-	nameTyOf _c = ["Num2"] `Mod` "Num2"-instance FixityOf Num2-instance ClassInstancesFor Num2-instance TypeInstancesFor Num2-instance Gram_Term_AtomsFor src ss g Num2-instance (Source src, SymInj ss Num) => ModuleFor src ss Num2 where-	moduleFor = ["Num2"] `moduleWhere`-	 [ "abs"    `withPrefix`   9 := teNum_abs-	 , "negate" `withPrefix`  10 := teNum_negate-	 , "abs"    `withPostfix`  9 := teNum_abs-	 , "negate" `withPostfix` 10 := teNum_negate-	 ]

@@ -116,7 +116,7 @@ 	nameTyOf _c = ["Ord"] `Mod` "Ord" instance FixityOf Ord instance ClassInstancesFor Ord where-	proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)+	proveConstraintFor _ (TyConst _ _ q :$ z) 	 | Just HRefl <- proj_ConstKiTy @_ @Ordering z 	 = case () of 		 _ | Just Refl <- proj_Const @Bounded q -> Just Dict

@@ -47,13 +47,13 @@ 	nameTyOf _c = ["Ratio"] `Mod` "Ratio" instance FixityOf Ratio instance ClassInstancesFor Ratio where-	proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ c a))+	proveConstraintFor _ (tq@(TyConst _ _ q) :$ c:@a) 	 | Just HRefl <- proj_ConstKiTy @_ @Ratio c 	 = case () of 		 _ | Just Refl <- proj_Const @Eq q-		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict+		   , Just Dict <- proveConstraint (tq`tyApp`a)   -> Just Dict 		   | Just Refl <- proj_Const @Show q-		   , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict+		   , Just Dict <- proveConstraint (tq`tyApp`a)   -> Just Dict 		   | Just Refl <- proj_Const @Real q 		   , Just Dict <- proveConstraint (tyIntegral a) -> Just Dict 		   | Just Refl <- proj_Const @Ord q

@@ -1,42 +0,0 @@-{-# LANGUAGE NoMonomorphismRestriction #-}-{-# OPTIONS_GHC -fno-warn-missing-signatures #-}-module Lib.Test where--import Test.Tasty--import Prelude hiding ((&&), not, (||), (==), id)--import Language.Symantic-import Language.Symantic.Lib--import qualified Lib.Applicative.Test as Applicative-import qualified Lib.Bool.Test as Bool-import qualified Lib.Foldable.Test as Foldable-import qualified Lib.Functor.Test as Functor-import qualified Lib.Map.Test as Map-import qualified Lib.MonoFunctor.Test as MonoFunctor-import qualified Lib.Num.Test as Num-import qualified Lib.Tuple2.Test as Tuple2---- * Tests-tests :: TestTree-tests = testGroup "Lib" $- [ Applicative.tests- , Bool.tests- , Foldable.tests- , Functor.tests- , Map.tests- , MonoFunctor.tests- , Num.tests- , Tuple2.tests- ]---- * EDSL tests-te1 = lam $ \x -> lam $ \y -> (x || y) && not (x && y)-te2 = lam $ \x -> lam $ \y -> (x && not y) || (not x && y)-te3 = let_ (bool True) $ \x -> x && x-te4 = let_ (lam $ \x -> x && x) $ \f -> f `app` bool True-te5 = lam $ \x0 -> lam $ \x1 -> x0 && x1-te6 = let_ (bool True) id && bool False-te7 = lam $ \f -> (f  `app` bool True) && bool True-te8 = lam $ \f -> f `app` (bool True && bool True)

@@ -8,7 +8,7 @@ import qualified Data.Sequences as Seqs import qualified Data.Text as Text -import Language.Symantic.Grammar+import Language.Symantic.Grammar hiding (text) import Language.Symantic import Language.Symantic.Lib.Char () import Language.Symantic.Lib.MonoFunctor (Element)@@ -36,17 +36,17 @@ instance NameTyOf Text where 	nameTyOf _c = ["Text"] `Mod` "Text" instance ClassInstancesFor Text where-	proveConstraintFor _ (TyApp _ (TyConst _ _ q) c)+	proveConstraintFor _ (TyConst _ _ q :$ c) 	 | Just HRefl <- proj_ConstKiTy @_ @Text c 	 = case () of-		 _ | Just Refl <- proj_Const @Eq q                -> Just Dict-		   | Just Refl <- proj_Const @MT.MonoFoldable q   -> Just Dict-		   | Just Refl <- proj_Const @MT.MonoFunctor q    -> Just Dict-		   | Just Refl <- proj_Const @Monoid q            -> Just Dict-		   | Just Refl <- proj_Const @Ord q               -> Just Dict-		   | Just Refl <- proj_Const @Seqs.IsSequence q   -> Just Dict+		 _ | Just Refl <- proj_Const @Eq                q -> Just Dict+		   | Just Refl <- proj_Const @MT.MonoFoldable   q -> Just Dict+		   | Just Refl <- proj_Const @MT.MonoFunctor    q -> Just Dict+		   | Just Refl <- proj_Const @Monoid            q -> Just Dict+		   | Just Refl <- proj_Const @Ord               q -> Just Dict+		   | Just Refl <- proj_Const @Seqs.IsSequence   q -> Just Dict 		   | Just Refl <- proj_Const @Seqs.SemiSequence q -> Just Dict-		   | Just Refl <- proj_Const @Show q              -> Just Dict+		   | Just Refl <- proj_Const @Show              q -> Just Dict 		 _ -> Nothing 	proveConstraintFor _c _q = Nothing instance TypeInstancesFor Text where

@@ -55,8 +55,8 @@ instance FixityOf (,) where 	fixityOf _c = Just $ Fixity2 $ infixN (-1) instance ClassInstancesFor (,) where-	proveConstraintFor _ (TyApp _ (TyConst _ _ q) (TyApp _ c a))-	 | Just HRefl <- proj_ConstKiTy @_ @(,) c+	proveConstraintFor _ (TyConst _ _ q :$ t:@a)+	 | Just HRefl <- proj_ConstKiTy @_ @(,) t 	 = case () of 		 _ | Just Refl <- proj_Const @Applicative q 		   , Just Dict <- proveConstraint (tyMonoid a) -> Just Dict@@ -66,32 +66,32 @@ 		   , Just Dict <- proveConstraint (tyMonoid a) -> Just Dict 		   | Just Refl <- proj_Const @Traversable q -> Just Dict 		 _ -> Nothing-	proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ (TyApp _ c a) b))-	 | Just HRefl <- proj_ConstKiTy @_ @(,) c+	proveConstraintFor _ (tq@(TyConst _ _ q) :$ t:@a:@b)+	 | Just HRefl <- proj_ConstKiTy @_ @(,) t 	 = case () of 		 _ | Just Refl <- proj_Const @Bounded q-		   , Just Dict <- proveConstraint (tq `tyApp` a)-		   , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict+		   , Just Dict <- proveConstraint (tq`tyApp`a)+		   , Just Dict <- proveConstraint (tq`tyApp`b) -> Just Dict 		   | Just Refl <- proj_Const @Eq q-		   , Just Dict <- proveConstraint (tq `tyApp` a)-		   , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict+		   , Just Dict <- proveConstraint (tq`tyApp`a)+		   , Just Dict <- proveConstraint (tq`tyApp`b) -> Just Dict 		   | Just Refl <- proj_Const @Monoid q-		   , Just Dict <- proveConstraint (tq `tyApp` a)-		   , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict+		   , Just Dict <- proveConstraint (tq`tyApp`a)+		   , Just Dict <- proveConstraint (tq`tyApp`b) -> Just Dict 		   | Just Refl <- proj_Const @Ord q-		   , Just Dict <- proveConstraint (tq `tyApp` a)-		   , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict+		   , Just Dict <- proveConstraint (tq`tyApp`a)+		   , Just Dict <- proveConstraint (tq`tyApp`b) -> Just Dict 		   | Just Refl <- proj_Const @Show q-		   , Just Dict <- proveConstraint (tq `tyApp` a)-		   , Just Dict <- proveConstraint (tq `tyApp` b) -> Just Dict+		   , Just Dict <- proveConstraint (tq`tyApp`a)+		   , Just Dict <- proveConstraint (tq`tyApp`b) -> Just Dict 		   | Just Refl <- proj_Const @MT.MonoFoldable q -> Just Dict-		   | Just Refl <- proj_Const @MT.MonoFunctor q  -> Just Dict+		   | Just Refl <- proj_Const @MT.MonoFunctor  q -> Just Dict 		 _ -> Nothing 	proveConstraintFor _c _q = Nothing instance TypeInstancesFor (,) where-	expandFamFor _c _len f (TyApp _ (TyApp _ c _a) b `TypesS` TypesZ)+	expandFamFor _c _len f (t:@_a:@b `TypesS` TypesZ) 	 | Just HRefl <- proj_ConstKi @_ @Element f-	 , Just HRefl <- proj_ConstKiTy @_ @(,) c+	 , Just HRefl <- proj_ConstKiTy @_ @(,) t 	 = Just b 	expandFamFor _c _len _fam _as = Nothing 

@@ -1,29 +0,0 @@-{-# OPTIONS_GHC -fno-warn-missing-signatures #-}-module Lib.Tuple2.Test where--import Test.Tasty--import Data.Proxy (Proxy(..))-import Prelude hiding ((&&), not, (||))--import Language.Symantic.Lib-import Compiling.Test--type SS =- [ Proxy (->)- , Proxy Integer- , Proxy ()- , Proxy (,)- ]-(==>) = readTe @() @SS--tests :: TestTree-tests = testGroup "Tuple2"- [ "()"             ==> Right (tyUnit, (), "()")- , "(,) 1 2"        ==> Right (tyTuple2 tyInteger tyInteger, (1,2), "(1, 2)")- , "(1,2)"          ==> Right (tyTuple2 tyInteger tyInteger, (1,2), "(1, 2)")- , "((1,2), (3,4))" ==> Right-	 ( let t = tyTuple2 tyInteger tyInteger in tyTuple2 t t-	 , ((1,2),(3,4))-	 , "((1, 2), (3, 4))" )- ]

@@ -3,8 +3,6 @@ -- | Symantic for '()'. module Language.Symantic.Lib.Unit where -import Prelude hiding ((&&), not, (||))- import Language.Symantic import Language.Symantic.Grammar @@ -30,7 +28,7 @@ instance NameTyOf () where 	nameTyOf _c = [] `Mod` "" instance ClassInstancesFor () where-	proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)+	proveConstraintFor _ (TyConst _ _ q :$ z) 	 | Just HRefl <- proj_ConstKiTy @_ @() z 	 = case () of 		 _ | Just Refl <- proj_Const @Bounded q -> Just Dict

@@ -1,14 +0,0 @@-module Test where--import Test.Tasty--import qualified Typing.Test as Typing-import qualified Lib.Test as Lib--main :: IO ()-main =-	defaultMain $-	testGroup "Language.Symantic"-	 [ Typing.tests-	 , Lib.tests-	 ]

@@ -1,185 +0,0 @@-{-# LANGUAGE AllowAmbiguousTypes #-}-{-# LANGUAGE UndecidableInstances #-}-{-# OPTIONS_GHC -fno-warn-orphans #-}-module Typing.Test where--import Test.Tasty-import Test.Tasty.HUnit--import Control.Applicative (Applicative(..))-import Control.Arrow (left)-import Data.Functor.Identity (Identity(..))-import Data.List.NonEmpty (NonEmpty)-import Data.Map.Strict (Map)-import Data.Maybe (isJust)-import Data.NonNull (NonNull)-import Data.Proxy-import Data.Ratio (Ratio)-import Data.Text (Text)-import GHC.Exts (Constraint)-import Prelude hiding (exp)-import qualified Control.Monad.Classes.Run as MC-import qualified Control.Monad.Trans.State.Strict as SS-import qualified Data.Function as Fun-import qualified Data.Map.Strict as Map-import qualified Data.MonoTraversable as MT-import qualified Data.Sequences as Seqs-import qualified System.IO as IO-import qualified Text.Megaparsec as P-import qualified Text.Megaparsec.Prim as P--import Language.Symantic.Grammar-import Language.Symantic-import Language.Symantic.Lib hiding ((<$>), (<*), show)--import Grammar.Megaparsec ()---- * Tests-type SS =- [ Proxy (->)- , Proxy Bool- , Proxy []- , Proxy ()- , Proxy (,)- , Proxy Char- , Proxy Either- , Proxy Int- , Proxy Integer- , Proxy IO- , Proxy IO.Handle- , Proxy IO.IOMode- , Proxy Ordering- , Proxy Map- , Proxy Maybe- , Proxy NonNull- , Proxy Ratio- , Proxy Text- , Proxy Applicative- , Proxy Bounded- , Proxy Enum- , Proxy Eq- , Proxy Foldable- , Proxy Functor- , Proxy Integral- , Proxy Monad- , Proxy Monoid- , Proxy MT.MonoFoldable- , Proxy MT.MonoFunctor- , Proxy Num- , Proxy Ord- , Proxy Real- , Proxy Seqs.IsSequence- , Proxy Seqs.SemiSequence- , Proxy Show- , Proxy Traversable- ]-type SRC = SrcTe (NonEmpty P.SourcePos) SS--impsTy :: Imports NameTy-impsTy = importTypes @SS []--modsTy :: Source src => ModulesTy src-modsTy =-	Map.insert ([] `Mod` "String")-	 (TypeTLen $ \len -> TypeT $-		tyConstLen @(K [])   @[]   len `tyApp`-		tyConstLen @(K Char) @Char len) $-	modulesTyInj @SS--parseTy ::- forall src g err inp.- g ~ P.ParsecT err inp (SS.StateT (Imports NameTy, ModulesTy src) Identity) =>- P.MonadParsec err inp (P.ParsecT err inp g) =>- Gram_Type src g =>- P.Token inp ~ Char =>- inp -> Either (P.ParseError Char err) (AST_Type src)-parseTy inp =-	runIdentity $-	MC.evalStateStrict (impsTy, modsTy @src) $-	P.runParserT g "" inp-	where g = unCF $ g_type <* eoi--tests :: TestTree-tests = testGroup "Typing" $- [ testGroup "readType" $-	let run inp (TypeT exp :: TypeT SRC '[]) =-		testCase inp $ got @?= Right (Right $ TypeVT exp)-		where-		got :: Either (P.ParseError Char P.Dec)-		              (Either (Error_Type SRC) (TypeVT SRC))-		got = readType <$> parseTy inp-		in-	let (==>) = run; infixr 0 ==> in-	 [ "Bool"                        ==> TypeT $ tyBool-	 , "(->) Bool"                   ==> TypeT $ tyFun `tyApp` tyBool-	 , "[]"                          ==> TypeT $ tyConst @(K []) @[]-	 , "[Char]"                      ==> TypeT $ tyList tyChar-	 , "[Char -> [Char]]"            ==> TypeT $ tyList (tyChar ~> tyList tyChar)-	 , "([])"                        ==> TypeT $ tyConst @(K []) @[]-	 , "[()]"                        ==> TypeT $ tyList tyUnit-	 , "()"                          ==> TypeT $ tyUnit-	 , "(())"                        ==> TypeT $ tyUnit-	 , "(,)"                         ==> TypeT $ tyConst @(K (,)) @(,)-	 , "((,))"                       ==> TypeT $ tyConst @(K (,)) @(,)-	 , "(,) Int"                     ==> TypeT $ tyConst @(K (,)) @(,) `tyApp` tyInt-	 , "(Bool)"                      ==> TypeT $ tyBool-	 , "((Bool))"                    ==> TypeT $ tyBool-	 , "(Bool, Int)"                 ==> TypeT $ tyBool `tyTuple2` tyInt-	 , "((Bool, Int))"               ==> TypeT $ tyBool `tyTuple2` tyInt-	 , "((Bool, Int), Char)"         ==> TypeT $ (tyBool `tyTuple2` tyInt) `tyTuple2` tyChar-	 , "(Bool, Int) -> Char"         ==> TypeT $ (tyBool `tyTuple2` tyInt) ~> tyChar-	 , "(Bool -> Int)"               ==> TypeT $ tyBool ~> tyInt-	 , "String"                      ==> TypeT $ tyList tyChar-	 , "[Char] -> String"            ==> TypeT $ tyList tyChar ~> tyList tyChar-	 , "String -> [Char]"            ==> TypeT $ tyList tyChar ~> tyList tyChar-	 , "Maybe Bool"                  ==> TypeT $ tyMaybe tyBool-	 , "Either Bool Int"             ==> TypeT $ tyEither tyBool tyInt-	 , "Bool -> Int"                 ==> TypeT $ tyBool ~> tyInt-	 , "(Bool -> Int) -> Char"       ==> TypeT $ (tyBool ~> tyInt) ~> tyChar-	 , "Bool -> (Int -> Char)"       ==> TypeT $ tyBool ~> (tyInt ~> tyChar)-	 , "Bool -> Int -> Char"         ==> TypeT $ tyBool ~> tyInt ~> tyChar-	 , "Bool -> (Int -> Char) -> ()" ==> TypeT $ tyBool ~> (tyInt ~> tyChar) ~> tyUnit-	 , "IO"                          ==> TypeT $ tyConst @(K IO) @IO-	 , "Traversable IO"              ==> TypeT $ tyTraversable (tyConst @(K IO) @IO)-	 , "Monad IO"                    ==> TypeT $ tyMonad (tyConst @(K IO) @IO)-	 , "(->) (IO Bool)"              ==> TypeT $ tyConst @(K (->)) @(->) `tyApp` (tyIO tyBool)-	 , "Monad IO"                    ==> TypeT $ tyMonad (tyConst @(K IO) @IO)-	 , "Eq"                          ==> TypeT $ tyConst @(K Eq) @Eq-	 , "Eq Bool"                     ==> TypeT $ tyEq tyBool-	 ]-	 , testGroup "Parsing errors" $-		let run inp = testCase inp $ got @?= Left ()-			where-			got :: Either () (AST_Type SRC)-			got = left (\(_::P.ParseError (P.Token String) P.Dec) -> ()) $ parseTy inp in-		run <$>-		 [ "Bool, Int"-		 , "(Bool -> Int) Char"-		 , "NonExistingType"-		 ]-	 , testGroup "Compiling errors" $-		let run inp = testCase inp $ got @?= Right (Left ())-			where-			got :: Either (P.ParseError Char P.Dec) (Either () (TypeVT SRC))-			got = left (Fun.const ()) . readType <$> parseTy inp in-		run <$>-		 [ "Bool Int"-		 , "[IO]"-		 , "(->) IO"-		 , "(->) Bool Int Char"-		 , "Monad Eq"-		 ]- , testGroup "proveConstraint" $-	let (==>) (typ::Type SRC SS (t::Constraint)) expected =-		let imps = importTypes @SS [] in-		let conf = config_Doc_Type{config_Doc_Type_imports = imps} in-		testCase (showType conf typ) $-		isJust (proveConstraint typ) @?= expected in-	 [ tyEq          tyBool                      ==> True-	 , tyOrd         tyBool                      ==> True-	 , tyFunctor     (tyConst @(K Maybe) @Maybe) ==> True-	 , tyFunctor     (tyConst @(K IO) @IO)       ==> True-	 , tyMonad       (tyConst @(K IO) @IO)       ==> True-	 , tyTraversable (tyConst @(K IO) @IO)       ==> False-	 ]- ]

@@ -0,0 +1,13 @@+resolver: lts-10.5+packages:+- '.'+- location: '../symantic'+  extra-dep: true+- location: '../symantic-grammar'+  extra-dep: true+- location: '../symantic-document'+  extra-dep: true+- location: '../monad-classes'+  extra-dep: true+extra-deps:+- peano-0.1.0.1

@@ -1,51 +1,33 @@-author: Julien Moutinho <julm+symantic@autogeree.net>+name: symantic-lib+-- PVP:  +-+------- breaking API changes+--       | | +----- non-breaking API additions+--       | | | +--- code changes with no API change+version: 0.0.3.20180213+category: Language+synopsis: Symantics for common types.+description: Symantics for common types,+             using <https://hackage.haskell.org/package/symantic symantic>.+extra-doc-files:+license: GPL-3+license-file: COPYING+stability: experimental+author:      Julien Moutinho <julm+symantic@autogeree.net>+maintainer:  Julien Moutinho <julm+symantic@autogeree.net> bug-reports: Julien Moutinho <julm+symantic@autogeree.net>+-- homepage:+ build-type: Simple cabal-version: >= 1.24-category: Language-description:-  Symantics for common types,-  using <https://hackage.haskell.org/package/symantic symantic>. extra-source-files:+  stack.yaml extra-tmp-files:--- homepage: -license: GPL-3-license-file: COPYING-maintainer: Julien Moutinho <julm+symantic@autogeree.net>-name: symantic-lib-stability: experimental-synopsis: Symantics for common types.-tested-with: GHC==8.0.2--- PVP:  +-+------- breaking API changes---       | | +----- non-breaking API additions---       | | | +--- code changes with no API change-version: 0.0.2.20170703+tested-with: GHC==8.2.2  Source-Repository head   location: git://git.autogeree.net/symantic   type:     git  Library-  default-extensions:-    DataKinds-    DefaultSignatures-    FlexibleContexts-    FlexibleInstances-    LambdaCase-    MultiParamTypeClasses-    NamedFieldPuns-    OverloadedStrings-    Rank2Types-    ScopedTypeVariables-    StandaloneDeriving-    TupleSections-    TypeApplications-    TypeFamilies-    TypeOperators-  ghc-options: -Wall-               -fno-warn-tabs-               -fprint-explicit-kinds-  default-language: Haskell2010   exposed-modules:     Language.Symantic.Lib     Language.Symantic.Lib.Alternative@@ -83,102 +65,91 @@     Language.Symantic.Lib.Traversable     Language.Symantic.Lib.Tuple2     Language.Symantic.Lib.Unit-  build-depends:-    base >= 4.6 && < 5-    , containers-    , ghc-prim-    , monad-classes-    , mono-traversable-    , symantic >= 6.0-    , symantic-grammar-    , transformers-    , text--Test-Suite symantic-test-  type: exitcode-stdio-1.0+  default-language: Haskell2010   default-extensions:     DataKinds+    DefaultSignatures     FlexibleContexts     FlexibleInstances+    LambdaCase     MultiParamTypeClasses-    NoMonomorphismRestriction+    NamedFieldPuns     OverloadedStrings+    Rank2Types     ScopedTypeVariables+    StandaloneDeriving     TupleSections     TypeApplications     TypeFamilies     TypeOperators-  default-language: Haskell2010-  ghc-options: -main-is Test-               -Wall-               -fno-warn-tabs-               -- -O0-               -- -fmax-simplifier-iterations=0-               -- -dshow-passes-  hs-source-dirs: Language/Symantic-  main-is: Test.hs-  other-modules:-    Compiling.Test-    Grammar.Megaparsec-    Lib.Applicative.Test-    Lib.Bool.Test-    Lib.Foldable.Test-    Lib.Functor.Test-    Lib.Map.Test-    Lib.MonoFunctor.Test-    Lib.Num.Test-    Lib.Test-    Lib.Tuple2.Test-    Typing.Test+  ghc-options:+    -Wall+    -Wincomplete-uni-patterns+    -Wincomplete-record-updates+    -fno-warn-tabs+    -fhide-source-paths+    -fprint-explicit-kinds   build-depends:-    base >= 4.6 && < 5-    , containers-    , megaparsec-    , monad-classes-    , mono-traversable+      symantic     , symantic-grammar-    , symantic-    , symantic-lib-    , tasty >= 0.11-    , tasty-hunit-    , text-    , transformers+    , base             >= 4.6 && < 5+    , containers       >= 0.5+    , mono-traversable >= 1.0+    , transformers     >= 0.5+    , text             >= 1.2 -Test-Suite ebnf+Test-Suite symantic-test   type: exitcode-stdio-1.0+  hs-source-dirs: test+  main-is: Main.hs+  other-modules:+    Golden+    HUnit+    HUnit.Applicative+    HUnit.Bool+    HUnit.Foldable+    HUnit.Functor+    HUnit.Map+    HUnit.MonoFunctor+    HUnit.Num+    HUnit.Tuple2+    Testing.Compiling+    Testing.Megaparsec+  default-language: Haskell2010   default-extensions:-    ConstraintKinds     DataKinds-    EmptyDataDecls     FlexibleContexts     FlexibleInstances     MultiParamTypeClasses-    NamedFieldPuns+    NoMonomorphismRestriction     OverloadedStrings-    PatternGuards-    PolyKinds-    Rank2Types     ScopedTypeVariables-    StandaloneDeriving     TupleSections-    TypeFamilies     TypeApplications+    TypeFamilies     TypeOperators-  ghc-options: -main-is Grammar.EBNF-               -Wall-               -fno-warn-tabs-               -fprint-potential-instances-  main-is: Grammar/EBNF.hs-  default-language: Haskell2010-  hs-source-dirs: Language/Symantic+  ghc-options:+    -Wall+    -Wincomplete-uni-patterns+    -Wincomplete-record-updates+    -fno-warn-tabs+    -fhide-source-paths+    -fprint-explicit-kinds+    -- -O0+    -- -fmax-simplifier-iterations=0+    -- -dshow-passes   build-depends:-    base >= 4.6 && < 5-    , containers-    , megaparsec+      symantic     , symantic-grammar-    , symantic     , symantic-lib-    , transformers-    , tasty >= 0.11-    , tasty-hunit-    , text+    , base             >= 4.6 && < 5+    , bytestring       >= 0.10+    , containers       >= 0.5+    , megaparsec       >= 6.3+    , monad-classes    >= 0.3.2+    , mono-traversable >= 1.0+    , tasty            >= 0.11+    , tasty-golden     >= 2.3+    , tasty-hunit      >= 0.9+    , text             >= 1.2+    , transformers     >= 0.5

@@ -0,0 +1,46 @@+module Golden where++import Control.Monad (Monad(..))+import Data.Function (($), (.))+import Data.Functor ((<$>))+import Data.Semigroup (Semigroup(..))+import Data.String (String)+-- import System.FilePath (FilePath)+import System.IO (IO)+import qualified Data.ByteString.Lazy as BSL+import qualified Data.List as List+import qualified Data.Text.Lazy          as TL+import qualified Data.Text.Lazy.Encoding as TL++import Test.Tasty+import Test.Tasty.Golden++import Language.Symantic.Grammar+import Language.Symantic+import Language.Symantic.Lib ()++-- * Golden testing utilities+testGolden :: TestName -> TestName -> IO BSL.ByteString -> TestTree+testGolden inputFile expectedExt =+	goldenVsStringDiff inputFile diffGolden (inputFile <> expectedExt)++diffGolden :: FilePath -> FilePath -> [String]+diffGolden ref new = ["diff", "-u", ref, new]++-- * All golden tests+goldensIO :: IO TestTree+goldensIO = do+	-- inputFiles <- List.sort <$> findByExtension [".sym"] "test/Golden"+	return $+		testGroup "Golden"+		 [ testGolden "grammar.ebnf" "" $ do+			return $+				TL.encodeUtf8 $+				TL.unlines $+				List.concat+				 [ render <$> gram_comment+				 , render <$> gram_type+				 , render <$> gram_term+				 ]+		 ]+	where render = TL.fromStrict . renderEBNF . unCF

@@ -0,0 +1,41 @@+{-# LANGUAGE NoMonomorphismRestriction #-}+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}+module HUnit where++import Test.Tasty+import Prelude hiding ((&&), not, (||), id)++import Language.Symantic+import Language.Symantic.Lib++import qualified HUnit.Applicative as Applicative+import qualified HUnit.Bool        as Bool+import qualified HUnit.Foldable    as Foldable+import qualified HUnit.Functor     as Functor+import qualified HUnit.Map         as Map+import qualified HUnit.MonoFunctor as MonoFunctor+import qualified HUnit.Num         as Num+import qualified HUnit.Tuple2      as Tuple2++-- * Tests+hunits :: TestTree+hunits = testGroup "HUnit" $+ [ Applicative.hunits+ , Bool.hunits+ , Foldable.hunits+ , Functor.hunits+ , Map.hunits+ , MonoFunctor.hunits+ , Num.hunits+ , Tuple2.hunits+ ]++-- * EDSL tests+te1 = lam $ \x -> lam $ \y -> (x || y) && not (x && y)+te2 = lam $ \x -> lam $ \y -> (x && not y) || (not x && y)+te3 = let_ (bool True) $ \x -> x && x+te4 = let_ (lam $ \x -> x && x) $ \f -> f `app` bool True+te5 = lam $ \x0 -> lam $ \x1 -> x0 && x1+te6 = let_ (bool True) id && bool False+te7 = lam $ \f -> (f  `app` bool True) && bool True+te8 = lam $ \f -> f `app` (bool True && bool True)

@@ -0,0 +1,28 @@+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}+module HUnit.Applicative where++import Test.Tasty+import Data.Proxy (Proxy(..))++import Language.Symantic.Lib+import Testing.Compiling+import HUnit.Bool ()++type SS =+ [ Proxy (->)+ , Proxy Integer+ , Proxy Bool+ , Proxy Maybe+ , Proxy Functor+ , Proxy Applicative+ ]+(==>) = readTe @() @SS++hunits :: TestTree+hunits = testGroup "Applicative"+ [ "Just (xor True) <*> Just True"    ==> Right (tyMaybe tyBool, Just False, "Just (\\x0 -> True `xor` x0) <*> Just True")+ , "Just (xor True) <*> Nothing"      ==> Right (tyMaybe tyBool, Nothing   , "Just (\\x0 -> True `xor` x0) <*> Nothing")+ , "xor <$> Just True <*> Just False" ==> Right (tyMaybe tyBool, Just True , "(\\x0 -> (\\x1 -> x0 `xor` x1)) <$> Just True <*> Just False")+ , "Just False <* Just True"          ==> Right (tyMaybe tyBool, Just False, "Just False <* Just True")+ , "Just False *> Just True"          ==> Right (tyMaybe tyBool, Just True , "Just False *> Just True")+ ]

@@ -0,0 +1,84 @@+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}+module HUnit.Bool where++import Test.Tasty+import Data.Proxy (Proxy(..))+import Prelude hiding ((&&), not, (||))++import Language.Symantic+import Language.Symantic.Lib+import Testing.Compiling++type SS =+ [ Proxy Bool+ , Proxy (->)+ , Proxy Integer+ , Proxy []+ , Proxy Char+ ]+(==>) = readTe @() @SS++hunits :: TestTree+hunits = testGroup "Bool" $+ [ "True"                           ==> Right (tyBool, True , "True")+ , "xor True True"                  ==> Right (tyBool, False, "True `xor` True")+ , "xor False True"                 ==> Right (tyBool, True , "False `xor` True")+ , "True `xor` True"                ==> Right (tyBool, False, "True `xor` True")+ , "(\\(xy:Bool) -> xy) True"       ==> Right (tyBool, True , "(\\x0 -> x0) True")+ , "(\\(False:Bool) -> False) True" ==> Right (tyBool, True , "(\\x0 -> x0) True")+ , "(\\(lett:Bool) -> lett) True"   ==> Right (tyBool, True , "(\\x0 -> x0) True")+ , "(\\(x:Bool) -> xor x x) True"   ==> Right (tyBool, False, "(\\x0 -> x0 `xor` x0) True")+ , "let x = True in xor x True"     ==> Right (tyBool, False, "let x0 = True in x0 `xor` True")+ , "(\\(False:Bool) -> False) (False `xor` True)" ==> Right (tyBool, True, "(\\x0 -> x0) (False `xor` True)")+ , testGroup "Error_Term"+	 [ "True True" ==> Left (tyBool,+		Right $ Error_Term_Beta $+		Error_Beta_Term_not_a_function $+		TypeVT $ tyBool @_ @'[])+	 , "x" ==> Left (tyBool,+		Right $ Error_Term_unknown $ NameTe "x")+	 , "x `xor` True" ==> Left (tyBool,+		Right $ Error_Term_unknown $ NameTe "x")+	 , "(\\(x:Bool) -> x `xor` True) Bool" ==> Left (tyBool,+		Right $ Error_Term_unknown $ NameTe "Bool")+	 , "(\\(x:Bool) -> x) True True" ==> Left (tyBool,+		Right $ Error_Term_Beta $+		Error_Beta_Term_not_a_function $+		TypeVT $ tyBool @_ @'[])+	 , "(\\(x:Bool -> Bool) -> x True) True" ==> Left (tyBool,+		Right $ Error_Term_Beta $ Error_Beta_Unify $+		Error_Unify_Const_mismatch+		 (TypeVT $ tyFun @_ @'[])+		 (TypeVT $ tyBool @_ @'[]))+	 ]+ ]++-- * Class 'Sym_Bool_Vars'+-- | A few boolean variables.+class Sym_Bool_Vars repr where+	x :: repr Bool+	y :: repr Bool+	z :: repr Bool+instance Sym_Bool_Vars View where+	x = View $ \_p _v -> "x"+	y = View $ \_p _v -> "y"+	z = View $ \_p _v -> "z"+{-+instance -- Trans_Boo_Const+ ( Sym_Bool repr+ , Sym_Bool_Vars repr+ ) => Sym_Bool_Vars (Trans_Bool_Const repr) where+	x = trans_lift x+	y = trans_lift y+	z = trans_lift z+-}++-- * EDSL tests+te1 = bool True && bool False+te2 = (bool True && bool False) ||  (bool True && bool True)+te3 = (bool True ||  bool False) && (bool True ||  bool True)+te4 = bool True && not (bool False)+te5 = bool True && not x+te6 = x `xor` y+te7 = (x `xor` y) `xor` z+te8 = x `xor` (y `xor` bool True)

@@ -0,0 +1,30 @@+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}+module HUnit.Foldable where++import Test.Tasty+import Data.Proxy (Proxy(..))++import Language.Symantic.Lib+import Testing.Compiling++type SS =+ [ Proxy (->)+ , Proxy Int+ , Proxy Integer+ , Proxy []+ , Proxy ()+ , Proxy (,)+ , Proxy Foldable+ ]+(==>) = readTe @() @SS++hunits :: TestTree+hunits = testGroup "Foldable"+ [ {-"[]" ==> Right (tyList (tyVar "a" varZ), [], "[]")+ ,-} "[1, 2, 3]" ==> Right (tyList tyInteger, [1, 2, 3], "1 : 2 : 3 : []")+ , "1 : 2 : 3 : []" ==> Right (tyList tyInteger, [1, 2, 3], "1 : 2 : 3 : []")+ , "foldMap (\\(x0:Integer) -> [x0, x0]) [1, 2, 3]" ==> Right+	 ( tyList tyInteger+	 , [1, 1, 2, 2, 3, 3]+	 , "foldMap (\\x0 -> x0 : x0 : []) (1 : 2 : 3 : [])" )+ ]

@@ -0,0 +1,26 @@+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}+module HUnit.Functor where++import Test.Tasty+import Data.Proxy (Proxy(..))++import Language.Symantic ()+import Language.Symantic.Lib+import Testing.Compiling++type SS =+ [ Proxy (->)+ , Proxy Bool+ , Proxy Functor+ , Proxy Integer+ , Proxy Maybe+ ]+(==>) = readTe @() @SS++hunits :: TestTree+hunits = testGroup "Functor"+ [ "fmap not (Just True)" ==> Right (tyMaybe tyBool, Just False, "fmap (\\x0 -> not x0) (Just True)")+ , "not `fmap` Just True" ==> Right (tyMaybe tyBool, Just False, "fmap (\\x0 -> not x0) (Just True)")+ , "not <$> Just True"    ==> Right (tyMaybe tyBool, Just False, "(\\x0 -> not x0) <$> Just True")+ , "False <$ Just True"   ==> Right (tyMaybe tyBool, Just False, "False <$ Just True")+ ]

@@ -0,0 +1,42 @@+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}+module HUnit.Map where++import Test.Tasty+import Data.Map.Strict (Map)+import Data.Proxy (Proxy(..))+import Data.Text as Text+import qualified Data.Map.Strict as Map++import Language.Symantic.Lib+import Testing.Compiling++type SS =+ [ Proxy (->)+ , Proxy []+ , Proxy Int+ , Proxy Integer+ , Proxy Map+ , Proxy Char+ , Proxy (,)+ , Proxy Num+ , Proxy Monoid+ ]+(==>) = readTe @() @SS++hunits :: TestTree+hunits = testGroup "Map"+ [ "Map.fromList (zipWith (,) [1, 2, 3] ['a', 'b', 'c'])" ==> Right+	 ( tyMap tyInteger tyChar+	 , Map.fromList [(1, 'a'), (2, 'b'), (3, 'c')]+	 , "Map.fromList (zipWith (\\x0 -> (\\x1 -> (x0, x1))) (1 : 2 : 3 : []) ('a' : 'b' : 'c' : []))" )+ , Text.concat+	[ "Map.foldrWithKey"+	, " (\\(k:Integer) (v:Char) (acc:(Integer,[Char])) ->"+	, "  (k + fst acc, v : snd acc))"+	, " (0, [])"+	, " (Map.fromList (zipWith (,) [1, 2, 3] ['a', 'b', 'c']))"+	] ==> Right+	 ( tyInteger `tyTuple2` tyString+	 , (6, "abc")+	 , "Map.foldrWithKey (\\x0 -> (\\x1 -> (\\x2 -> (x0 + fst x2, x1 : snd x2)))) (0, []) (Map.fromList (zipWith (\\x0 -> (\\x1 -> (x0, x1))) (1 : 2 : 3 : []) ('a' : 'b' : 'c' : [])))" )+ ]

@@ -0,0 +1,26 @@+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}+module HUnit.MonoFunctor where++import Test.Tasty+import Data.Proxy (Proxy(..))+import qualified Data.MonoTraversable as MT++import Language.Symantic.Lib+import Testing.Compiling++type SS =+ [ Proxy (->)+ , Proxy []+ , Proxy Integer+ , Proxy Bool+ , Proxy Char+ , Proxy MT.MonoFunctor+ , Proxy Maybe+ ]+(==>) = readTe @() @SS++hunits :: TestTree+hunits = testGroup "MonoFunctor"+ [ "omap not (Just True)" ==> Right (tyMaybe tyBool, Just False, "omap (\\x0 -> not x0) (Just True)")+ , "omap Char.toUpper ['a', 'b', 'c']" ==> Right (tyList tyChar, "ABC", "omap (\\x0 -> Char.toUpper x0) ('a' : 'b' : 'c' : [])" )+ ]

@@ -0,0 +1,105 @@+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+module HUnit.Num where++import Test.Tasty+import Prelude (Num)+import Prelude hiding (Num(..))++import Language.Symantic+import Language.Symantic.Lib+import Testing.Compiling++-- * Tests+type SS =+ [ Proxy (->)+ , Proxy Integer+ , Proxy Num+ , Proxy Num2+ , Proxy Int+ , Proxy Integral+ , Proxy Foldable+ , Proxy Traversable+ , Proxy []+ ]+(==>) = readTe @() @SS++hunits :: TestTree+hunits = testGroup "Num"+ [ "42"                        ==> Right (tyInteger,  42, "42")+ , "-42"                       ==> Right (tyInteger, -42, "negate 42")+ , "- -42"                     ==> Right (tyInteger,  42, "negate (negate 42)")+ , "1 + -2"                    ==> Right (tyInteger,  -1, "1 + negate 2")+ , "-1 + -2"                   ==> Right (tyInteger,  -3, "negate 1 + negate 2")+ , "-(1 + -2)"                 ==> Right (tyInteger,   1, "negate (1 + negate 2)")+ , "(+) 1 2"                   ==> Right (tyInteger,   3, "1 + 2")+ , "1+2"                       ==> Right (tyInteger,   3, "1 + 2")+ , "1 +2"                      ==> Right (tyInteger,   3, "1 + 2")+ , "1+ 2"                      ==> Right (tyInteger,   3, "1 + 2")+ , "1 + 2"                     ==> Right (tyInteger,   3, "1 + 2")+ , "1 + 2 - 3"                 ==> Right (tyInteger,   0, "1 + 2 - 3")+ , "1 + 2 * 3"                 ==> Right (tyInteger,   7, "1 + 2 * 3")+ , "3 * 2 + 1"                 ==> Right (tyInteger,   7, "3 * 2 + 1")+ , "3 * (2 + 1)"               ==> Right (tyInteger,   9, "3 * (2 + 1)")+ , "4 + 3 * 2 + 1"             ==> Right (tyInteger,  11, "4 + 3 * 2 + 1")+ , "5 * 4 + 3 * 2 + 1"         ==> Right (tyInteger,  27, "5 * 4 + 3 * 2 + 1")+ , "negate`42"                 ==> Right (tyInteger, -42, "negate 42")+ , "42`negate"                 ==> Right (tyInteger, -42, "negate 42")+ , "42`negate "                ==> Right (tyInteger, -42, "negate 42")+ , "42`negate`negate"          ==> Right (tyInteger,  42, "negate (negate 42)")+ , "42`abs`negate"             ==> Right (tyInteger, -42, "negate (abs 42)")+ , "42`negate`abs"             ==> Right (tyInteger,  42, "abs (negate 42)")+ , "abs`negate`42"             ==> Right (tyInteger,  42, "abs (negate 42)")+ , "negate`abs`42"             ==> Right (tyInteger, -42, "negate (abs 42)")+ , "negate`abs`42`mod`9"       ==> Right (tyInteger,   3, "negate (abs 42) `mod` 9")+ , "negate abs`42"             ==> Right (tyInteger, -42, "negate (abs 42)")+ , "negate 42`abs"             ==> Right (tyInteger, -42, "negate (abs 42)")+ , "(+) negate`2 44"           ==> Right (tyInteger,  42, "negate 2 + 44")+ , "(+) 2`negate 44"           ==> Right (tyInteger,  42, "negate 2 + 44")+ , "(+) (negate`2) 44"         ==> Right (tyInteger,  42, "negate 2 + 44")+ , "abs negate`42"             ==> Right (tyInteger,  42, "abs (negate 42)")+ , "(+) 40 2"                  ==> Right (tyInteger,  42, "40 + 2")+ , "(+) 40 $ -2"               ==> Right (tyInteger,  38, "(($) (\\x0 -> 40 + x0)) (negate 2)")+ , "negate 42 + 42`negate"     ==> Right (tyInteger, -84, "negate 42 + negate 42")+ , "(+) (negate 42) 42`negate" ==> Right (tyInteger, -84, "negate 42 + negate 42")+ , "(+) negate`42 42`negate"   ==> Right (tyInteger, -84, "negate 42 + negate 42")+ , "42`abs`negate`mod`abs`negate`9" ==> Right (tyInteger, 3, "negate (abs 42) `mod` abs (negate 9)")+ , "abs`42`negate"             ==> Right (tyInteger,  42, "abs (negate 42)")+ , "negate`42`abs"             ==> Right (tyInteger,  42, "abs (negate 42)")+ , testGroup "Error_Term"+   [ "(+) 40 -2"  ==> Left (tyInteger,+		Right $ Error_Term_Beta $ Error_Beta_Unify $+		Error_Unify_Const_mismatch+		 (TypeVT $ tyFun @_ @'[])+		 (TypeVT $ tyInteger @_ @'[]))+	 , "(+) 40 - 2" ==> Left (tyInteger,+		Right $ Error_Term_Beta $ Error_Beta_Unify $+		Error_Unify_Const_mismatch+		 (TypeVT $ tyFun @_ @'[])+		 (TypeVT $ tyInteger @_ @'[]))+	 ]+ ]++-- | A newtype to test prefix and postfix.+newtype Num2 a = Num2 a+type instance Sym Num2 = Sym_Num2+class Sym_Num2 (term:: * -> *) where++instance Sym_Num2 Eval where+instance Sym_Num2 View where+instance Sym_Num2 (Dup r1 r2) where+instance Sym_Num2 term => Sym_Num2 (BetaT term) where+instance NameTyOf Num2 where+	nameTyOf _c = ["Num2"] `Mod` "Num2"+instance FixityOf Num2+instance ClassInstancesFor Num2+instance TypeInstancesFor Num2+instance Gram_Term_AtomsFor src ss g Num2+instance (Source src, SymInj ss Num) => ModuleFor src ss Num2 where+	moduleFor = ["Num2"] `moduleWhere`+	 [ "abs"    `withPrefix`   9 := teNum_abs+	 , "negate" `withPrefix`  10 := teNum_negate+	 , "abs"    `withPostfix`  9 := teNum_abs+	 , "negate" `withPostfix` 10 := teNum_negate+	 ]

@@ -0,0 +1,27 @@+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}+module HUnit.Tuple2 where++import Test.Tasty+import Data.Proxy (Proxy(..))++import Language.Symantic.Lib+import Testing.Compiling++type SS =+ [ Proxy (->)+ , Proxy Integer+ , Proxy ()+ , Proxy (,)+ ]+(==>) = readTe @() @SS++hunits :: TestTree+hunits = testGroup "Tuple2"+ [ "()"             ==> Right (tyUnit, (), "()")+ , "(,) 1 2"        ==> Right (tyTuple2 tyInteger tyInteger, (1,2), "(1, 2)")+ , "(1,2)"          ==> Right (tyTuple2 tyInteger tyInteger, (1,2), "(1, 2)")+ , "((1,2), (3,4))" ==> Right+	 ( let t = tyTuple2 tyInteger tyInteger in tyTuple2 t t+	 , ((1,2),(3,4))+	 , "((1, 2), (3, 4))" )+ ]

@@ -0,0 +1,15 @@+module Main where++import Test.Tasty++import Golden+import HUnit++main :: IO ()+main = do+	goldens <- goldensIO+	defaultMain $+		testGroup "Symantic"+		 [ goldens+		 , hunits+		 ]

@@ -0,0 +1,113 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+module Testing.Compiling where++import Test.Tasty+import Test.Tasty.HUnit+import Debug.Trace (trace)++import Control.Arrow (left)+import Data.Functor.Identity (Identity(..))+import Data.Text (Text)+import Data.Type.Equality+import Data.Void (Void)+import qualified Control.Monad.Classes.Run as MC+import qualified Control.Monad.Trans.State.Strict as S+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 Language.Symantic.Lib ()++import Testing.Megaparsec ()++type G src ss =+ P.ParsecT Void Text+           (S.StateT (Imports NameTe, Modules src ss)+                     ((S.StateT (Imports NameTy, ModulesTy src))+                                Identity))++parseTe ::+ forall ss src.+ ImportTypes ss =>+ ModulesTyInj ss =>+ ModulesInj src ss =>+ Gram_Term src ss (G src ss) =>+ Text -> Either (P.ParseError Char Void) (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 (impsTy, modsTy) $+	MC.evalStateStrict (impsTe, modsTe) $+	P.runParserT g "" inp+	where g = unCF $ g_term <* eoi++readTe ::+ forall src ss t.+ ( Eq t+ , 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+ ) =>+ Text ->+ Either ( Type src '[] t+        , Either (P.ParseError Char Void)+                 (Error_Term src) )+        (Type src '[] t, t, Text) ->+ TestTree+readTe inp expected =+	testCase (elide inp) $+	case reduceTeApp <$> parseTe @ss inp of+	 Left err -> Left (Left err) @?= snd `left` expected+	 Right ast ->+		case readTerm CtxTyZ ast of+		 Left err -> Left (Right err) @?= snd `left` expected+		 Right term ->+			case term of+			 TermVT (Term q t (TeSym te)) ->+				case expected of+				 Left (_, err) -> Right ("…"::Text) @?= Left err+				 Right (ty_expected::Type src '[] t, _::t, _::Text) ->+					(>>= (@?= (\(_::Type src '[] t, err) -> err) `left` expected)) $+					case lenVars t of+					 LenS{} -> return $ Left $ Right $ Error_Term_polymorphic (TypeVT t)+					 LenZ ->+						case proveConstraint q 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 ->+								return $ Right (t, eval $ te CtxTeZ, view $ betaT $ te CtxTeZ)++maybeRight :: Either l r -> Maybe r+maybeRight (Right r) = Just r+maybeRight Left{}    = Nothing++elide :: Text -> String+elide s | Text.length s > 42 = List.take 42 (Text.unpack s) List.++ ['…']+elide s = Text.unpack s++dbg :: Show a => String -> a -> a+dbg msg x = trace (msg ++ " = " ++ Prelude.show x) x

@@ -0,0 +1,181 @@+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+-- | Symantic instances for Megaparsec+module Testing.Megaparsec where++import Control.Applicative (Applicative(..))+import Control.Monad (Monad(..))+import Data.Char (Char)+import Data.Either (Either(..))+import Data.Function (($), (.))+import Data.Functor (Functor(..), (<$>))+import Data.List.NonEmpty (NonEmpty(..))+import Data.Ord (Ord(..))+import Data.String (IsString(..))+import Data.Typeable ()+import Text.Show (Show(..))+import qualified Control.Applicative as Alt+import qualified Control.Monad.Classes as MC+import qualified Data.Char as Char+import qualified Data.Text as Text+import qualified Data.Text.Lazy as TL+import qualified Text.Megaparsec as P+import qualified Text.Megaparsec.Char as P++import Language.Symantic.Grammar as Sym+import qualified Language.Symantic as Sym+import Language.Symantic.Lib ()++-- * Type 'ParsecC'+-- | Convenient alias for defining instances involving 'P.ParsecT'.+type ParsecC e s = (P.Token s ~ Char, P.Stream s, Ord e)+instance ParsecC e [Char] => IsString (P.ParsecT e [Char] m [Char]) where+	fromString = P.string++--+-- Readers+--++-- NonEmpty P.SourcePos+instance ParsecC e s => Sym.Gram_Reader (NonEmpty P.SourcePos) (P.ParsecT e s m) where+	askBefore g = do+		s <- P.statePos <$> P.getParserState+		($ s) <$> g+	askAfter g = do+		f <- g+		f . P.statePos <$> P.getParserState+type instance MC.CanDo (P.ParsecT e s m) (MC.EffReader (NonEmpty P.SourcePos)) = 'True+instance ParsecC e s => MC.MonadReaderN 'MC.Zero (NonEmpty P.SourcePos) (P.ParsecT e s m) where+	askN _n = P.statePos <$> P.getParserState+-- P.SourcePos+instance ParsecC e s => Sym.Gram_Reader P.SourcePos (P.ParsecT e s m) where+	askBefore g = do+		s <- P.getPosition+		($ s) <$> g+	askAfter g = do+		f <- g+		f <$> P.getPosition+type instance MC.CanDo (P.ParsecT e s m) (MC.EffReader P.SourcePos) = 'True+instance ParsecC e s => MC.MonadReaderN 'MC.Zero P.SourcePos (P.ParsecT e s m) where+	askN _n = P.getPosition+-- ()+instance ParsecC e s => Sym.Gram_Reader () (P.ParsecT e s m) where+	askBefore = fmap ($ ())+	askAfter  = fmap ($ ())++--+-- States+--++-- st+type instance MC.CanDo (P.ParsecT e s m) (MC.EffState st) = 'False+instance (Monad m, MC.MonadState st m) => Sym.Gram_State st m where+	stateBefore g = do+		s <- MC.get+		f <- g+		let (s', a) = f s+		MC.put s'+		return a+	stateAfter g = do+		f <- g+		s <- MC.get+		let (s_, a) = f s+		MC.put s_+		return a+	getBefore g = do+		s <- MC.get+		f <- g+		return (f s)+	getAfter g = do+		f <- g+		s <- MC.get+		return (f s)+	put g = do+		(s, a) <- g+		MC.put s+		return a++--+-- Sym instances+--+instance (ParsecC e s, Show err) => Sym.Gram_Error err (P.ParsecT e s m) where+	catch me {- if you can :-} = do+		e <- me+		case e of+		 Left err -> fail $ show err+		 Right a -> return a+instance ParsecC e s => Sym.Gram_Rule (P.ParsecT e s m) where+	rule = P.label . Text.unpack+instance ParsecC e s => Sym.Gram_Char (P.ParsecT e s m) where+	any          = P.anyChar+	eoi          = P.eof+	char         = P.char+	unicat cat   = P.satisfy $ (`elem` cats) . Char.generalCategory+		where cats = unicode_categories cat+	range (l, h) = P.satisfy $ \c -> l <= c && c <= h+	Terminal f `but` Terminal p = Terminal $ P.notFollowedBy (P.try p) *> f+instance ParsecC e String => Sym.Gram_String (P.ParsecT e String m) where+	string = P.string+instance ParsecC e Text.Text => Sym.Gram_String (P.ParsecT e Text.Text m) where+	string t   = Text.unpack <$> P.string (Text.pack t)+	text       = P.string+	textLazy t = TL.fromStrict <$> P.string (TL.toStrict t)+instance ParsecC e s => Sym.Gram_Alt (P.ParsecT e s m) where+	empty  = Alt.empty+	(<+>)  = (Alt.<|>)+	choice = P.choice+instance ParsecC e s => Sym.Gram_Try (P.ParsecT e s m) where+	try = P.try+instance ParsecC e s => Sym.Gram_RegR (P.ParsecT e s m) where+	Terminal f .*> Reg x = Reg $ f <*> x+instance ParsecC e s => Sym.Gram_RegL (P.ParsecT e s m) where+	Reg f <*. Terminal x = Reg $ f <*> x+instance ParsecC e s => Sym.Gram_App (P.ParsecT e s m) where+	between = P.between+instance ParsecC e s => Sym.Gram_AltApp (P.ParsecT e s m) where+	option   = P.option+	optional = P.optional+	many     = P.many+	some     = P.some+	manySkip = P.skipMany+instance ParsecC e s => Sym.Gram_CF (P.ParsecT e s m) where+	CF f <& Reg p        = CF $ P.lookAhead f <*> p+	Reg f &> CF p        = CF $ P.lookAhead f <*> p+	minus (CF f) (Reg p) = CF $ P.notFollowedBy (P.try p) *> f+instance (ParsecC e s, Sym.Gram_String (P.ParsecT e s m)) => Sym.Gram_Comment (P.ParsecT e s m)+instance (ParsecC e s, Sym.Gram_String (P.ParsecT e s m)) => Sym.Gram_Op (P.ParsecT e s m)+instance (ParsecC e s, Sym.Gram_String (P.ParsecT e s m)) => Sym.Gram_Mod (P.ParsecT e s m)+instance (ParsecC e s, Sym.Gram_String (P.ParsecT e s m)) => Sym.Gram_Type_Name (P.ParsecT e s m)+instance (ParsecC e s, Sym.Gram_String (P.ParsecT e s m)) => Sym.Gram_Term_Name (P.ParsecT e s m)+instance -- Sym.Gram_Type+ ( ParsecC e s+ , Sym.Gram_String (P.ParsecT e s m)+ , Gram_Source src (P.ParsecT e s m)+ , Show src+ , MC.MonadState ( Sym.Imports Sym.NameTy+                 , Sym.ModulesTy src )+                 (P.ParsecT e s m)+ ) => Sym.Gram_Type src (P.ParsecT e s m)+instance -- Sym.Gram_Term_Type+ ( ParsecC e s+ , Sym.Gram_String (P.ParsecT e s m)+ , Show src+ , MC.MonadState ( Sym.Imports Sym.NameTy+                 , Sym.ModulesTy src )+                 (P.ParsecT e s m)+ , Gram_Source src           (P.ParsecT e s m)+ ) => Sym.Gram_Term_Type src (P.ParsecT e s m)+instance -- Sym.Gram_Term+ ( ParsecC e s+ , Sym.Gram_String (P.ParsecT e s m)+ , Show src+ , MC.MonadState ( Sym.Imports Sym.NameTy+                 , Sym.ModulesTy src )+                 (P.ParsecT e s m)+ , MC.MonadState ( Sym.Imports Sym.NameTe+                 , Sym.Modules src ss )+                 (P.ParsecT e s m)+ , Sym.Gram_Source src        (P.ParsecT e s m)+ , Sym.Gram_Term_Atoms src ss (P.ParsecT e s m)+ ) => Sym.Gram_Term src ss    (P.ParsecT e s m)