packages feed

symantic-lib 0.0.2.20170623 → 0.0.2.20170702

raw patch · 40 files changed

+273/−181 lines, 40 files

Files

Language/Symantic/Compiling/Test.hs view
@@ -27,13 +27,13 @@  test_parseTerm ::  forall ss src.- Inj_Modules src ss =>- Gram_Term src ss (P.ParsecT P.Dec Text (SS.StateT (Imports, Modules src ss) Identity)) =>+ ModulesInj src ss =>+ Gram_Term src ss (P.ParsecT P.Dec Text (SS.StateT (Imports NameTe, Modules src ss) Identity)) =>  Text ->  Either (P.ParseError Char P.Dec) (AST_Term src ss) test_parseTerm inp =-	let mods :: Modules src ss = either (error . show) id inj_Modules in-	let imps = importQualifiedAs [] mods in+	let mods :: Modules src ss = either (error . show) id modulesInj in+	let imps = [] `importModules` mods in 	runIdentity $ 	MC.evalStateStrict (imps, mods) $ 	P.runParserT g "" inp@@ -42,19 +42,20 @@ test_readTerm ::  forall src ss t.  ( Eq t- , Gram_Term src ss (P.ParsecT P.Dec Text (SS.StateT (Imports, Modules src ss) Identity))+ , Gram_Term src ss (P.ParsecT P.Dec Text (SS.StateT (Imports NameTe, Modules src ss) Identity))  , Show t  , Syms ss Eval  , Syms ss View  , Syms ss (BetaT View)- , Inj_Modules src ss+ , ModulesInj 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+ , SourceInj (TypeVT src) src+ , SourceInj (TypeT src '[]) src+ , SourceInj (KindK src) src+ , SourceInj (AST_Type src) src+ , ModulesTyInj ss+ , ImportTypes ss  ) =>  Text ->  Either ( Type src '[] t@@ -67,8 +68,9 @@ 	case reduceTeApp <$> test_parseTerm @ss inp of 	 Left err -> Left (Left err) @?= snd `left` expected 	 Right ast ->-		let tys = inj_Name2Type @ss in-		case readTerm tys CtxTyZ ast of+		let modsTy = modulesTyInj @ss in+		let imps = importTypes @ss [] in+		case readTerm imps modsTy CtxTyZ ast of 		 Left err -> Left (Right err) @?= snd `left` expected 		 Right term -> 			case term of
Language/Symantic/Grammar/Megaparsec.hs view
@@ -23,6 +23,7 @@  import Language.Symantic.Grammar as Sym import qualified Language.Symantic as Sym+import Language.Symantic.Lib ()  -- -- Readers@@ -30,10 +31,10 @@  -- NonEmpty P.SourcePos instance ParsecC e s => Sym.Gram_Reader (NonEmpty P.SourcePos) (P.ParsecT e s m) where-	g_ask_before g = do+	askBefore g = do 		s <- P.statePos <$> P.getParserState 		($ s) <$> g-	g_ask_after g = do+	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@@ -41,10 +42,10 @@ 	askN _n = P.statePos <$> P.getParserState -- P.SourcePos instance ParsecC e s => Sym.Gram_Reader P.SourcePos (P.ParsecT e s m) where-	g_ask_before g = do+	askBefore g = do 		s <- P.getPosition 		($ s) <$> g-	g_ask_after g = do+	askAfter g = do 		f <- g 		f <$> P.getPosition type instance MC.CanDo (P.ParsecT e s m) (MC.EffReader P.SourcePos) = 'True@@ -52,8 +53,8 @@ 	askN _n = P.getPosition -- () instance ParsecC e s => Sym.Gram_Reader () (P.ParsecT e s m) where-	g_ask_before = fmap ($ ())-	g_ask_after  = fmap ($ ())+	askBefore = fmap ($ ())+	askAfter  = fmap ($ ())  -- -- States@@ -62,27 +63,27 @@ -- 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-	g_state_before g = do+	stateBefore g = do 		s <- MC.get 		f <- g 		let (s', a) = f s 		MC.put s' 		return a-	g_state_after g = do+	stateAfter g = do 		f <- g 		s <- MC.get 		let (s_, a) = f s 		MC.put s_ 		return a-	g_get_before g = do+	getBefore g = do 		s <- MC.get 		f <- g 		return (f s)-	g_get_after g = do+	getAfter g = do 		f <- g 		s <- MC.get 		return (f s)-	g_put g = do+	put g = do 		(s, a) <- g 		MC.put s 		return a@@ -97,7 +98,7 @@ -- Sym instances -- instance (ParsecC e s, Show err) => Sym.Gram_Error err (P.ParsecT e s m) where-	g_catch me = do+	catch me {- if you can :-} = do 		e <- me 		case e of 		 Left err -> fail $ show err@@ -137,7 +138,9 @@ 	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_Name (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)@@ -149,7 +152,8 @@ instance -- Sym.Gram_Term  ( ParsecC e s  , Show src- , MC.MonadState (Sym.Imports, 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)+ , 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)
Language/Symantic/Lib/Alternative.hs view
@@ -12,7 +12,7 @@ import Language.Symantic.Lib.Function (a0)  -- * Class 'Sym_Alternative'-type instance Sym (Proxy Alternative) = Sym_Alternative+type instance Sym Alternative = Sym_Alternative class Sym_Functor term => Sym_Alternative term where 	empty :: Alternative f => term (f a) 	(<|>) :: Alternative f => term (f a) -> term (f a) -> term (f a)@@ -39,13 +39,15 @@ instance (Sym_Lambda term, Sym_Alternative term) => Sym_Alternative (BetaT term)  -- Typing+instance NameTyOf Alternative where+	nameTyOf _c = ["Alternative"] `Mod` "Alternative" instance FixityOf Alternative instance ClassInstancesFor Alternative instance TypeInstancesFor Alternative  -- Compiling instance Gram_Term_AtomsFor src ss g Alternative-instance (Source src, Inj_Sym ss Alternative) => ModuleFor src ss Alternative where+instance (Source src, SymInj ss Alternative) => ModuleFor src ss Alternative where 	moduleFor = ["Alternative"] `moduleWhere` 	 [ "empty" := teAlternative_empty 	 , "<|>" `withInfixL` 3 := teAlternative_alt
Language/Symantic/Lib/Applicative.hs view
@@ -13,7 +13,7 @@ import Language.Symantic.Lib.Functor (Sym_Functor(..), (<$>), f1, f2)  -- * Class 'Sym_Applicative'-type instance Sym (Proxy Applicative) = Sym_Applicative+type instance Sym Applicative = Sym_Applicative class Sym_Functor term => Sym_Applicative term where 	pure  :: Applicative f => term a -> term (f a) 	(<*>) :: Applicative f => term (f (a -> b)) -> term (f a) -> term (f b); infixl 4 <*>@@ -49,13 +49,15 @@ 	(*>) = trans2 (*>)  -- Typing+instance NameTyOf Applicative where+	nameTyOf _c = ["Applicative"] `Mod` "Applicative" instance FixityOf Applicative instance ClassInstancesFor Applicative instance TypeInstancesFor Applicative  -- Compiling instance Gram_Term_AtomsFor src ss g Applicative-instance (Source src, Inj_Sym ss Applicative) => ModuleFor src ss Applicative where+instance (Source src, SymInj ss Applicative) => ModuleFor src ss Applicative where 	moduleFor = ["Applicative"] `moduleWhere` 	 [ "<*>" `withInfixL` 4 := teApplicative_app 	 , "<*"  `withInfixL` 4 := teApplicative_const
Language/Symantic/Lib/Bool.hs view
@@ -4,7 +4,6 @@ module Language.Symantic.Lib.Bool where  import Control.Monad-import Data.Proxy import Prelude hiding ((&&), not, (||)) import qualified Data.Bool as Bool import qualified Data.Text as Text@@ -13,7 +12,7 @@ import Language.Symantic.Lib.Function ()  -- * Class 'Sym_Bool'-type instance Sym (Proxy Bool) = Sym_Bool+type instance Sym Bool = Sym_Bool class Sym_Bool term where 	bool ::      Bool -> term Bool 	not  :: term Bool -> term Bool@@ -56,6 +55,8 @@ 	xor = trans2 xor  -- Typing+instance NameTyOf Bool where+	nameTyOf _c = ["Bool"] `Mod` "Bool" instance ClassInstancesFor Bool where 	proveConstraintFor _ (TyApp _ (TyConst _ _ q) c) 	 | Just HRefl <- proj_ConstKiTy @_ @Bool c@@ -71,7 +72,7 @@  -- Compiling instance Gram_Term_AtomsFor src ss g Bool-instance (Source src, Inj_Sym ss Bool) => ModuleFor src ss Bool where+instance (Source src, SymInj ss Bool) => ModuleFor src ss Bool where 	moduleFor = ["Bool"] `moduleWhere` 	 [ "False" := teBool False 	 , "True"  := teBool True@@ -82,11 +83,11 @@ 	 ]  -- ** 'Type's-tyBool :: Source src => Inj_Len vs => Type src vs Bool+tyBool :: Source src => LenInj vs => Type src vs Bool tyBool = tyConst @(K Bool) @Bool  -- ** 'Term's-teBool :: Source src => Inj_Sym ss Bool => Bool -> Term src ss ts '[] (() #> Bool)+teBool :: Source src => SymInj ss Bool => Bool -> Term src ss ts '[] (() #> Bool) teBool b = Term noConstraint tyBool $ teSym @Bool $ bool b  teBool_not :: TermDef Bool '[] (() #> (Bool -> Bool))
Language/Symantic/Lib/Bounded.hs view
@@ -11,7 +11,7 @@ import Language.Symantic.Lib.Function (a0)  -- * Class 'Sym_Bounded'-type instance Sym (Proxy Bounded) = Sym_Bounded+type instance Sym Bounded = Sym_Bounded class Sym_Bounded term where 	minBound :: Bounded a => term a 	maxBound :: Bounded a => term a@@ -35,13 +35,15 @@ instance (Sym_Lambda term, Sym_Bounded term) => Sym_Bounded (BetaT term)  -- Typing+instance NameTyOf Bounded where+	nameTyOf _c = ["Bounded"] `Mod` "Bounded" instance FixityOf Bounded instance ClassInstancesFor Bounded instance TypeInstancesFor Bounded  -- Compiling instance Gram_Term_AtomsFor src ss g Bounded-instance (Source src, Inj_Sym ss Bounded) => ModuleFor src ss Bounded where+instance (Source src, SymInj ss Bounded) => ModuleFor src ss Bounded where 	moduleFor = ["Bounded"] `moduleWhere` 	 [ "minBound" := teBounded_minBound 	 , "maxBound" := teBounded_maxBound
Language/Symantic/Lib/Char.hs view
@@ -7,12 +7,12 @@ import qualified Data.Text as Text  import Language.Symantic.Grammar hiding (char, any)-import qualified Language.Symantic.Grammar as Gram+import qualified Language.Symantic.Grammar as G import Language.Symantic import Language.Symantic.Lib.List (tyList)  -- * Class 'Sym_Char'-type instance Sym (Proxy Char) = Sym_Char+type instance Sym Char = Sym_Char class Sym_Char term where 	char :: Char -> term Char 	char_toUpper :: term Char -> term Char@@ -45,6 +45,8 @@ instance (Sym_Char term, Sym_Lambda term) => Sym_Char (BetaT term)  -- Typing+instance NameTyOf Char where+	nameTyOf _c = ["Char"] `Mod` "Char" instance ClassInstancesFor Char where 	proveConstraintFor _ (TyApp _ (TyConst _ _ q) z) 	 | Just HRefl <- proj_ConstKiTy @_ @Char z@@ -64,35 +66,35 @@  , Gram_Alt g  , Gram_Rule g  , Gram_Comment g- , Inj_Sym ss Char+ , SymInj ss Char  ) => Gram_Term_AtomsFor src ss g Char where 	g_term_atomsFor = 	 [ rule "teChar" $-		lexeme $ g_source $+		lexeme $ source $ 		(\c src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teChar c) 		 <$> between tickG tickG (-			cf_of_Terminal (Gram.any `but` tickG) <+>+			cfOf (G.any `but` tickG) <+> 			'\'' <$ string "\\'" 		 ) 	 ] 		where 		tickG :: Gram_Terminal g' => g' Char-		tickG = Gram.char '\''-instance (Source src, Inj_Sym ss Char) => ModuleFor src ss Char where+		tickG = G.char '\''+instance (Source src, SymInj ss Char) => ModuleFor src ss Char where 	moduleFor = ["Char"] `moduleWhere` 	 [ "toLower" := teChar_toLower 	 , "toUpper" := teChar_toUpper 	 ]  -- ** 'Type's-tyChar :: Source src => Inj_Len vs => Type src vs Char+tyChar :: Source src => LenInj vs => Type src vs Char tyChar = tyConst @(K Char) @Char -tyString :: Source src => Inj_Len vs => Type src vs String+tyString :: Source src => LenInj vs => Type src vs String tyString = tyList tyChar  -- ** 'Term's-teChar :: Source src => Inj_Sym ss Char => Char -> Term src ss ts '[] (() #> Char)+teChar :: Source src => SymInj ss Char => Char -> Term src ss ts '[] (() #> Char) teChar b = Term noConstraint tyChar $ teSym @Char $ char b  teChar_toUpper, teChar_toLower :: TermDef Char '[] (() #> (Char -> Char))
Language/Symantic/Lib/Either.hs view
@@ -12,7 +12,7 @@ import Language.Symantic.Lib.Function (a0, b1, c2)  -- * Class 'Sym_Either'-type instance Sym (Proxy Either) = Sym_Either+type instance Sym Either = Sym_Either class Sym_Either term where 	_Left  :: term l -> term (Either l r) 	_Right :: term r -> term (Either l r)@@ -44,6 +44,8 @@ instance (Sym_Either term, Sym_Lambda term) => Sym_Either (BetaT term)  -- Typing+instance NameTyOf Either where+	nameTyOf _c = ["Either"] `Mod` "Either" instance FixityOf Either instance ClassInstancesFor Either where 	proveConstraintFor _ (TyApp _ (TyConst _ _ q) (TyApp _ c _l))@@ -80,7 +82,7 @@  -- Compiling instance Gram_Term_AtomsFor src ss g Either-instance (Source src, Inj_Sym ss Either) => ModuleFor src ss Either where+instance (Source src, SymInj ss Either) => ModuleFor src ss Either where 	moduleFor = ["Either"] `moduleWhere` 	 [ "Left"   := teEither_Left 	 , "Right"  := teEither_Right
Language/Symantic/Lib/Enum.hs view
@@ -12,7 +12,7 @@ import Language.Symantic.Lib.Int (tyInt)  -- * Class 'Sym_Enum'-type instance Sym (Proxy Enum) = Sym_Enum+type instance Sym Enum = Sym_Enum class Sym_Enum term where 	toEnum   :: Enum a => term Int -> term a 	fromEnum :: Enum a => term a -> term Int@@ -50,13 +50,15 @@ instance (Sym_Enum term, Sym_Lambda term) => Sym_Enum (BetaT term)  -- Typing+instance NameTyOf Enum where+	nameTyOf _c = ["Enum"] `Mod` "Enum" instance FixityOf Enum instance ClassInstancesFor Enum instance TypeInstancesFor Enum  -- Compiling instance Gram_Term_AtomsFor src ss g Enum-instance (Source src, Inj_Sym ss Enum) => ModuleFor src ss Enum where+instance (Source src, SymInj ss Enum) => ModuleFor src ss Enum where 	moduleFor = ["Enum"] `moduleWhere` 	 [ "succ"     := teEnum_succ 	 , "pred"     := teEnum_pred
Language/Symantic/Lib/Eq.hs view
@@ -11,7 +11,7 @@ import Language.Symantic.Lib.Function (a0)  -- * Class 'Sym_Eq'-type instance Sym (Proxy Eq) = Sym_Eq+type instance Sym Eq = Sym_Eq class Sym_Eq term where 	(==) :: Eq a => term a -> term a -> term Bool; infix 4 == 	(/=) :: Eq a => term a -> term a -> term Bool; infix 4 /=@@ -37,13 +37,15 @@ instance (Sym_Eq term, Sym_Lambda term) => Sym_Eq (BetaT term)  -- Typing+instance NameTyOf Eq where+	nameTyOf _c = ["Eq"] `Mod` "Eq" instance FixityOf Eq instance ClassInstancesFor Eq instance TypeInstancesFor Eq  -- Compiling instance Gram_Term_AtomsFor src ss g Eq-instance (Source src, Inj_Sym ss Eq) => ModuleFor src ss Eq where+instance (Source src, SymInj ss Eq) => ModuleFor src ss Eq where 	moduleFor = ["Eq"] `moduleWhere` 	 [ "==" `withInfixN` 4 := teEq_eq 	 , "/=" `withInfixN` 4 := teEq_ne
Language/Symantic/Lib/Foldable.hs view
@@ -25,7 +25,7 @@ import Language.Symantic.Lib.Ord (tyOrd)  -- * Class 'Sym_Foldable'-type instance Sym (Proxy Foldable) = Sym_Foldable+type instance Sym Foldable = Sym_Foldable class Sym_Foldable term where 	foldMap    :: Foldable f => Monoid m      => term (a -> m) -> term (f a) -> term m 	foldr      :: Foldable f                  => term (a -> b -> b) -> term b -> term (f a) -> term b@@ -237,13 +237,15 @@ instance (Sym_Foldable term, Sym_Lambda term) => Sym_Foldable (BetaT term)  -- Typing+instance NameTyOf Foldable where+	nameTyOf _c = ["Foldable"] `Mod` "Foldable" instance FixityOf Foldable instance ClassInstancesFor Foldable instance TypeInstancesFor Foldable  -- Compiling instance Gram_Term_AtomsFor src ss g Foldable-instance (Source src, Inj_Sym ss Foldable) => ModuleFor src ss Foldable where+instance (Source src, SymInj ss Foldable) => ModuleFor src ss Foldable where 	moduleFor = ["Foldable"] `moduleWhere` 	 [ "foldMap" := teFoldable_foldMap 	 , "foldr"   := teFoldable_foldr@@ -266,15 +268,15 @@ tyFoldable :: Source src => Type src vs a -> Type src vs (Foldable a) tyFoldable a = tyConstLen @(K Foldable) @Foldable (lenVars a) `tyApp` a -t0 :: Source src => Inj_Len vs => Inj_Kind (K t) =>+t0 :: Source src => LenInj vs => KindInj (K t) =>       Type src (Proxy t ': vs) t t0 = tyVar "t" $ varZ -t1 :: Source src => Inj_Len vs => Inj_Kind (K t) =>+t1 :: Source src => LenInj vs => KindInj (K t) =>       Type src (a ': Proxy t ': vs) t t1 = tyVar "t" $ VarS varZ -t2 :: Source src => Inj_Len vs => Inj_Kind (K t) =>+t2 :: Source src => LenInj vs => KindInj (K t) =>       Type src (a ': b ': Proxy t ': vs) t t2 = tyVar "t" $ VarS $ VarS varZ @@ -282,7 +284,7 @@ teFoldable_foldMap :: TermDef Foldable '[Proxy a, Proxy t, Proxy m] (Foldable t # Monoid m #> ((a -> m) -> t a -> m)) teFoldable_foldMap = Term (tyFoldable t1 # tyMonoid m) ((a0 ~> m) ~> t1 `tyApp` a0 ~> m) $ teSym @Foldable $ lam2 foldMap 	where-	m :: Source src => Inj_Len vs => Inj_Kind (K m) =>+	m :: Source src => LenInj vs => KindInj (K m) => 	     Type src (a ': b ': Proxy m ': vs) m 	m = tyVar "m" $ VarS $ VarS varZ @@ -330,7 +332,7 @@  {- TODO: when MonadPlus will be supported teFoldable_msum ::- Source src => Inj_Sym ss Foldable =>+ Source src => SymInj ss Foldable =>  Term src ss ts '[Proxy a, Proxy t, Proxy f] ((Foldable t # MonadPlus f) #> (t (f a) -> f a)) teFoldable_msum = 	Term ((tyFoldable t1 # (tyConst @(K MonadPlus) @MonadPlus `tyApp` f2))) (t1 `tyApp` (f2 `tyApp` a0) ~> (f2 `tyApp` a0)) $
Language/Symantic/Lib/Function.hs view
@@ -10,7 +10,7 @@ import Language.Symantic  -- * Class 'Sym_Function'-type instance Sym (Proxy (->)) = Sym_Function+type instance Sym (->) = Sym_Function class Sym_Function term where 	comp  :: term (b -> c) -> term (a -> b) -> term (a -> c); infixr 9 `comp` 	const :: term a -> term b -> term a@@ -46,6 +46,8 @@ instance (Sym_Function term, Sym_Lambda term) => Sym_Function (BetaT term)  -- Typing+instance NameTyOf (->) where+	nameTyOf _c = [] `Mod` "->" instance ClassInstancesFor (->) where 	proveConstraintFor _c (TyApp _ q (TyApp _ z _r)) 	 | Just HRefl <- proj_ConstKiTy @_ @(->) z@@ -66,7 +68,7 @@  -- Compiling instance Gram_Term_AtomsFor src ss g (->)-instance (Source src, Inj_Sym ss (->)) => ModuleFor src ss (->) where+instance (Source src, SymInj ss (->)) => ModuleFor src ss (->) where 	moduleFor = ["Function"] `moduleWhere` 	 [ "const" := teFunction_const 	 , "flip"  := teFunction_flip@@ -76,18 +78,18 @@ 	 ]  -- ** 'Type's-tyFun :: Source src => Inj_Len vs => Type src vs (->)+tyFun :: Source src => LenInj vs => Type src vs (->) tyFun = tyConst @(K (->)) @(->) -a0 :: Source src => Inj_Len vs => Inj_Kind (K a) =>+a0 :: Source src => LenInj vs => KindInj (K a) =>      Type src (Proxy a ': vs) a a0 = tyVar "a" varZ -b1 :: Source src => Inj_Len vs => Inj_Kind (K b) =>+b1 :: Source src => LenInj vs => KindInj (K b) =>      Type src (a ': Proxy b ': vs) b b1 = tyVar "b" $ VarS varZ -c2 :: Source src => Inj_Len vs => Inj_Kind (K c) =>+c2 :: Source src => LenInj vs => KindInj (K c) =>      Type src (a ': b ': Proxy c ': vs) c c2 = tyVar "c" $ VarS $ VarS varZ
Language/Symantic/Lib/Functor.hs view
@@ -13,7 +13,7 @@ import Language.Symantic.Lib.Function (a0, b1)  -- * Class 'Sym_Functor'-type instance Sym (Proxy Functor) = Sym_Functor+type instance Sym Functor = Sym_Functor class Sym_Functor term where 	fmap :: Functor f => term (a -> b) -> term (f a) -> term (f b) 	default fmap :: Sym_Functor (UnT term) => Trans term => Functor f => term (a -> b) -> term (f a) -> term (f b)@@ -44,13 +44,15 @@ 	(<$)  = trans2 (<$)  -- Typing+instance NameTyOf Functor where+	nameTyOf _c = ["Functor"] `Mod` "Functor" instance FixityOf Functor instance ClassInstancesFor Functor instance TypeInstancesFor Functor  -- Compiling instance Gram_Term_AtomsFor src ss g Functor-instance (Source src, Inj_Sym ss Functor) => ModuleFor src ss Functor where+instance (Source src, SymInj ss Functor) => ModuleFor src ss Functor where 	moduleFor = ["Functor"] `moduleWhere` 	 [ "fmap" := teFunctor_fmap 	 , "<$"  `withInfixL` 4 := teFunctor_const@@ -61,11 +63,11 @@ tyFunctor :: Source src => Type src vs a -> Type src vs (Functor a) tyFunctor a = tyConstLen @(K Functor) @Functor (lenVars a) `tyApp` a -f1 :: Source src => Inj_Len vs => Inj_Kind (K f) =>+f1 :: Source src => LenInj vs => KindInj (K f) =>       Type src (a ': Proxy f ': vs) f f1 = tyVar "f" $ VarS varZ -f2 :: Source src => Inj_Len vs => Inj_Kind (K f) =>+f2 :: Source src => LenInj vs => KindInj (K f) =>       Type src (a ': b ': Proxy f ': vs) f f2 = tyVar "f" $ VarS $ VarS varZ
Language/Symantic/Lib/IO.hs view
@@ -12,9 +12,9 @@ import Language.Symantic.Lib.Unit (tyUnit)  -- * Class 'Sym_IO'-type instance Sym (Proxy IO)        = Sym_IO-type instance Sym (Proxy IO.Handle) = Sym_IO_Handle-type instance Sym (Proxy IO.IOMode) = Sym_IO_Mode+type instance Sym IO        = Sym_IO+type instance Sym IO.Handle = Sym_IO_Handle+type instance Sym IO.IOMode = Sym_IO_Mode class Sym_IO (term:: * -> *) class Sym_IO_Handle (term:: * -> *) where 	io_hClose   :: term IO.Handle -> term (IO ())@@ -52,6 +52,12 @@ instance (Sym_IO_Mode term, Sym_Lambda term) => Sym_IO_Mode (BetaT term)  -- Typing+instance NameTyOf IO where+	nameTyOf _c = ["IO"] `Mod` "IO"+instance NameTyOf IO.Handle where+	nameTyOf _c = ["IO"] `Mod` "Handle"+instance NameTyOf IO.IOMode where+	nameTyOf _c = ["IO"] `Mod` "IOMode" instance FixityOf IO instance ClassInstancesFor IO where 	proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)@@ -94,7 +100,7 @@  -- Compiling instance ModuleFor src ss IO-instance (Source src, Inj_Sym ss IO.Handle) => ModuleFor src ss IO.Handle where+instance (Source src, SymInj ss IO.Handle) => ModuleFor src ss IO.Handle where 	moduleFor = ["IO"] `moduleWhere` 	 [ "hClose"   := teIO_hClose 	 , "openFile" := teIO_openFile@@ -108,13 +114,13 @@ tyIO :: Source src => Type src vs a -> Type src vs (IO a) tyIO a = tyConstLen @(K IO) @IO (lenVars a) `tyApp` a -tyIO_Handle :: Source src => Inj_Len vs => Type src vs IO.Handle+tyIO_Handle :: Source src => LenInj vs => Type src vs IO.Handle tyIO_Handle = tyConst @(K IO.Handle) @IO.Handle -tyIO_Mode :: Source src => Inj_Len vs => Type src vs IO.IOMode+tyIO_Mode :: Source src => LenInj vs => Type src vs IO.IOMode tyIO_Mode = tyConst @(K IO.IOMode) @IO.IOMode -tyFilePath :: Source src => Inj_Len vs => Type src vs FilePath+tyFilePath :: Source src => LenInj vs => Type src vs FilePath tyFilePath = tyString  -- ** 'Term's
Language/Symantic/Lib/If.hs view
@@ -13,7 +13,7 @@ data If  -- * Class 'Sym_If'-type instance Sym (Proxy If) = Sym_If+type instance Sym If = Sym_If class Sym_If term where 	if_ :: term Bool -> term a -> term a -> term a 	default if_ :: Sym_If (UnT term) => Trans term => term Bool -> term a -> term a -> term a@@ -38,6 +38,8 @@ instance (Sym_If term, Sym_Lambda term) => Sym_If (BetaT term)  -- Typing+instance NameTyOf If where+	nameTyOf _c = ["If"] `Mod` "If" instance ClassInstancesFor If instance TypeInstancesFor If
Language/Symantic/Lib/Int.hs view
@@ -8,7 +8,7 @@ import Language.Symantic  -- * Class 'Sym_Int'-type instance Sym (Proxy Int) = Sym_Int+type instance Sym Int = Sym_Int class Sym_Int term where 	int :: Int -> term Int 	default int :: Sym_Int (UnT term) => Trans term => Int -> term Int@@ -27,6 +27,8 @@ instance (Sym_Int term, Sym_Lambda term) => Sym_Int (BetaT term)  -- Typing+instance NameTyOf Int where+	nameTyOf _c = ["Int"] `Mod` "Int" instance ClassInstancesFor Int where 	proveConstraintFor _c (TyApp _ (TyConst _ _ q) z) 	 | Just HRefl <- proj_ConstKiTy @_ @Int z@@ -48,9 +50,9 @@ instance ModuleFor src ss Int  -- ** 'Type's-tyInt :: Source src => Inj_Len vs => Type src vs Int+tyInt :: Source src => LenInj vs => Type src vs Int tyInt = tyConst @(K Int) @Int  -- ** 'Term's-teInt :: Source src => Inj_Sym ss Int => Int -> Term src ss ts '[] (() #> Int)+teInt :: Source src => SymInj ss Int => Int -> Term src ss ts '[] (() #> Int) teInt i = Term noConstraint tyInt $ teSym @Int $ int i
Language/Symantic/Lib/Integer.hs view
@@ -9,7 +9,7 @@ import Language.Symantic.Grammar  -- * Class 'Sym_Integer'-type instance Sym (Proxy Integer) = Sym_Integer+type instance Sym Integer = Sym_Integer class Sym_Integer term where 	integer :: Integer -> term Integer 	default integer :: Sym_Integer (UnT term) => Trans term => Integer -> term Integer@@ -28,6 +28,8 @@ instance (Sym_Integer term, Sym_Lambda term) => Sym_Integer (BetaT term)  -- Typing+instance NameTyOf Integer where+	nameTyOf _c = ["Integer"] `Mod` "Integer" instance ClassInstancesFor Integer where 	proveConstraintFor _ (TyApp _ (TyConst _ _ q) z) 	 | Just HRefl <- proj_ConstKiTy @_ @Integer z@@ -50,19 +52,19 @@  , Gram_AltApp g  , Gram_Rule g  , Gram_Comment g- , Inj_Sym ss Integer+ , SymInj ss Integer  ) => Gram_Term_AtomsFor src ss g Integer where 	g_term_atomsFor = 	 [ rule "teinteger" $-		lexeme $ g_source $+		lexeme $ source $ 		(\i src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teInteger $ read i) 		 <$> some (choice $ char <$> ['0'..'9']) 	 ] instance ModuleFor src ss Integer  -- ** 'Term's-tyInteger :: Source src => Inj_Len vs => Type src vs Integer+tyInteger :: Source src => LenInj vs => Type src vs Integer tyInteger = tyConst @(K Integer) @Integer -teInteger :: Source src => Inj_Sym ss Integer => Integer -> Term src ss ts '[] (() #> Integer)+teInteger :: Source src => SymInj ss Integer => Integer -> Term src ss ts '[] (() #> Integer) teInteger i = Term noConstraint tyInteger $ teSym @Integer $ integer i
Language/Symantic/Lib/Integral.hs view
@@ -13,7 +13,7 @@ import Language.Symantic.Lib.Tuple2 (tyTuple2)  -- * Class 'Sym_Integral'-type instance Sym (Proxy Integral) = Sym_Integral+type instance Sym Integral = Sym_Integral class Sym_Integral term where 	quot      :: Integral i => term i -> term i -> term i; infixl 7 `quot` 	rem       :: Integral i => term i -> term i -> term i; infixl 7 `rem`@@ -69,13 +69,15 @@ instance (Sym_Integral term, Sym_Lambda term) => Sym_Integral (BetaT term)  -- Typing+instance NameTyOf Integral where+	nameTyOf _c = ["Integral"] `Mod` "Integral" instance FixityOf Integral instance ClassInstancesFor Integral instance TypeInstancesFor Integral  -- Compiling instance Gram_Term_AtomsFor src ss g Integral-instance (Source src, Inj_Sym ss Integral) => ModuleFor src ss Integral where+instance (Source src, SymInj ss Integral) => ModuleFor src ss Integral where 	moduleFor = ["Integral"] `moduleWhere` 	 [ "quot" `withInfixL` 7 := teIntegral_quot 	 , "rem"  `withInfixL` 7 := teIntegral_rem
Language/Symantic/Lib/List.hs view
@@ -13,12 +13,12 @@ import qualified Data.Traversable as Traversable  import Language.Symantic-import Language.Symantic.Grammar+import Language.Symantic.Grammar as G import Language.Symantic.Lib.Function (a0, b1, c2) import Language.Symantic.Lib.MonoFunctor (Element)  -- * Class 'Sym_List'-type instance Sym (Proxy []) = Sym_List+type instance Sym [] = Sym_List class Sym_List term where 	list_empty :: term [a] 	list_cons  :: term a -> term [a] -> term [a]; infixr 5 `list_cons`@@ -62,7 +62,9 @@ instance (Sym_List term, Sym_Lambda term) => Sym_List (BetaT term)  -- Typing-instance FixityOf [] where+instance NameTyOf [] where+	nameTyOf _c = [] `Mod` "[]"+instance FixityOf [] instance ClassInstancesFor [] where 	proveConstraintFor _ (TyApp _ (TyConst _ _ q) z) 	 | Just HRefl <- proj_ConstKiTy @_ @[] z@@ -102,13 +104,13 @@  , Gram_Rule g  , Gram_Comment g  , Gram_Term src ss g- , Inj_Sym ss []+ , SymInj ss []  ) => Gram_Term_AtomsFor src ss g [] where 	g_term_atomsFor = 	 [ rule "teList_list" $ 		between (symbol "[") (symbol "]") listG 	 , rule "teList_empty" $-		g_source $+		G.source $ 		(\src -> BinTree0 $ Token_Term $ TermAVT teList_empty `setSource` src) 		 <$ symbol "[" 		 <* symbol "]"@@ -116,7 +118,7 @@ 		where 		listG :: CF g (AST_Term src ss) 		listG = rule "list" $-			g_source $+			G.source $ 			(\a mb src -> 				case mb of 				 Just b  -> BinTree2 (BinTree2 (BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teList_cons) a) b@@ -126,7 +128,7 @@ 					 (BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teList_empty)) 			 <$> g_term 			 <*> option Nothing (Just <$ symbol "," <*> listG)-instance (Source src, Inj_Sym ss []) => ModuleFor src ss [] where+instance (Source src, SymInj ss []) => ModuleFor src ss [] where 	moduleFor = ["List"] `moduleWhere` 	 [ "[]"      := teList_empty 	 , "zipWith" := teList_zipWith@@ -134,15 +136,15 @@ 	 ]  -- ** 'Type's-tyList :: Source src => Inj_Len vs => Type src vs a -> Type src vs [a]+tyList :: Source src => LenInj vs => Type src vs a -> Type src vs [a] tyList = (tyConst @(K []) @[] `tyApp`)  -- ** 'Term's-teList_empty :: Source src => Inj_Sym ss [] => Term src ss ts '[Proxy a] (() #> [a])+teList_empty :: Source src => SymInj ss [] => Term src ss ts '[Proxy a] (() #> [a]) teList_empty = Term noConstraint (tyList a0) $ teSym @[] $ list_empty -teList_cons :: Source src => Inj_Sym ss [] => Term src ss ts '[Proxy a] (() #> (a -> [a] -> [a]))+teList_cons :: Source src => SymInj ss [] => Term src ss ts '[Proxy a] (() #> (a -> [a] -> [a])) teList_cons = Term noConstraint (a0 ~> tyList a0 ~> tyList a0) $ teSym @[] $ lam2 list_cons -teList_zipWith :: Source src => Inj_Sym ss [] => Term src ss ts '[Proxy a, Proxy b, Proxy c] (() #> ((a -> b -> c) -> [a] -> [b] -> [c]))+teList_zipWith :: Source src => SymInj ss [] => Term src ss ts '[Proxy a, Proxy b, Proxy c] (() #> ((a -> b -> c) -> [a] -> [b] -> [c])) teList_zipWith = Term noConstraint ((a0 ~> b1 ~> c2) ~> tyList a0 ~> tyList b1 ~> tyList c2) $ teSym @[] $ lam3 zipWith
Language/Symantic/Lib/Map.hs view
@@ -17,7 +17,7 @@ import Language.Symantic.Lib.Tuple2 (tyTuple2)  -- * Class 'Sym_Map'-type instance Sym (Proxy Map) = Sym_Map+type instance Sym Map = Sym_Map class Sym_Map term where 	map_fromList     :: Ord k => term [(k, a)] -> term (Map k a) 	map_mapWithKey   :: term (k -> a -> b) -> term (Map k a) -> term (Map k b)@@ -85,6 +85,8 @@ instance (Sym_Map term, Sym_Lambda term) => Sym_Map (BetaT term)  -- Typing+instance NameTyOf Map where+	nameTyOf _c = ["Map"] `Mod` "Map" instance FixityOf Map instance ClassInstancesFor Map where 	proveConstraintFor _ (TyApp _ (TyConst _ _ q) (TyApp _ c _k))@@ -120,7 +122,7 @@  -- Compiling instance Gram_Term_AtomsFor src ss g Map-instance (Source src, Inj_Sym ss Map) => ModuleFor src ss Map where+instance (Source src, SymInj ss Map) => ModuleFor src ss Map where 	moduleFor = ["Map"] `moduleWhere` 	 [ "delete"       := teMap_delete 	 , "difference"   := teMap_difference@@ -134,14 +136,14 @@ 	 ]  -- ** 'Type's-tyMap :: Source src => Inj_Len vs => Type src vs k -> Type src vs a -> Type src vs (Map k a)+tyMap :: Source src => LenInj vs => Type src vs k -> Type src vs a -> Type src vs (Map k a) tyMap k a = tyConst @(K Map) @Map `tyApp` k `tyApp` a -k1 :: Source src => Inj_Len vs => Inj_Kind (K k) =>+k1 :: Source src => LenInj vs => KindInj (K k) =>      Type src (a ': Proxy k ': vs) k k1 = tyVar "k" $ VarS varZ -k2 :: Source src => Inj_Len vs => Inj_Kind (K k) =>+k2 :: Source src => LenInj vs => KindInj (K k) =>      Type src (a ': b ': Proxy k ': vs) k k2 = tyVar "k" $ VarS $ VarS varZ
Language/Symantic/Lib/Maybe.hs view
@@ -13,7 +13,7 @@ import Language.Symantic.Lib.MonoFunctor (Element)  -- * Class 'Sym_Maybe'-type instance Sym (Proxy Maybe) = Sym_Maybe+type instance Sym Maybe = Sym_Maybe class Sym_Maybe term where 	_Nothing :: term (Maybe a) 	_Just    :: term a -> term (Maybe a)@@ -45,6 +45,8 @@ instance (Sym_Maybe term, Sym_Lambda term) => Sym_Maybe (BetaT term)  -- Typing+instance NameTyOf Maybe where+	nameTyOf _c = ["Maybe"] `Mod` "Maybe" instance FixityOf Maybe instance ClassInstancesFor Maybe where 	proveConstraintFor _ (TyApp _ (TyConst _ _ q) c)@@ -78,7 +80,7 @@  -- Compiling instance Gram_Term_AtomsFor src ss g Maybe-instance (Source src, Inj_Sym ss Maybe) => ModuleFor src ss Maybe where+instance (Source src, SymInj ss Maybe) => ModuleFor src ss Maybe where 	moduleFor = ["Maybe"] `moduleWhere` 	 [ "Nothing" := teMaybe_Nothing 	 , "Just"    := teMaybe_Just@@ -86,7 +88,7 @@ 	 ]  -- ** 'Type's-tyMaybe :: Source src => Inj_Len vs => Type src vs a -> Type src vs (Maybe a)+tyMaybe :: Source src => LenInj vs => Type src vs a -> Type src vs (Maybe a) tyMaybe = (tyConst @(K Maybe) @Maybe `tyApp`)  -- ** 'Term's
Language/Symantic/Lib/Monad.hs view
@@ -14,7 +14,7 @@ import Language.Symantic.Lib.Bool (tyBool)  -- * Class 'Sym_Monad'-type instance Sym (Proxy Monad) = Sym_Monad+type instance Sym Monad = Sym_Monad class Sym_Monad term where 	return :: Monad m       => term a -> term (m a) 	(>>=)  :: Monad m       => term (m a) -> term (a -> m b) -> term (m b); infixl 1 >>=@@ -58,13 +58,15 @@ instance (Sym_Monad term, Sym_Lambda term) => Sym_Monad (BetaT term)  -- Typing+instance NameTyOf Monad where+	nameTyOf _c = ["Monad"] `Mod` "Monad" instance FixityOf Monad instance ClassInstancesFor Monad instance TypeInstancesFor Monad  -- Compiling instance Gram_Term_AtomsFor src ss g Monad-instance (Source src, Inj_Sym ss Monad) => ModuleFor src ss Monad where+instance (Source src, SymInj ss Monad) => ModuleFor src ss Monad where 	moduleFor = ["Monad"] `moduleWhere` 	 [ "return" := teMonad_return 	 , "join"   := teMonad_join@@ -77,19 +79,19 @@ tyMonad :: Source src => Type src vs m -> Type src vs (Monad m) tyMonad m = tyConstLen @(K Monad) @Monad (lenVars m) `tyApp` m -m0 :: Source src => Inj_Len vs => Inj_Kind (K m) =>+m0 :: Source src => LenInj vs => KindInj (K m) =>      Type src (Proxy m ': vs) m m0 = tyVar "m" varZ -m1 :: Source src => Inj_Len vs => Inj_Kind (K m) =>+m1 :: Source src => LenInj vs => KindInj (K m) =>      Type src (a ': Proxy m ': vs) m m1 = tyVar "m" $ VarS varZ -m2 :: Source src => Inj_Len vs => Inj_Kind (K m) =>+m2 :: Source src => LenInj vs => KindInj (K m) =>      Type src (a ': b ': Proxy m ': vs) m m2 = tyVar "m" $ VarS $ VarS varZ -m3 :: Source src => Inj_Len vs => Inj_Kind (K m) =>+m3 :: Source src => LenInj vs => KindInj (K m) =>      Type src (a ': b ': c ': Proxy m ': vs) m m3 = tyVar "m" $ VarS $ VarS $ VarS varZ
Language/Symantic/Lib/MonoFoldable.hs view
@@ -15,7 +15,7 @@ import Language.Symantic.Lib.Monoid (tyMonoid)  -- * Class 'Sym_MonoFoldable'-type instance Sym (Proxy MonoFoldable) = Sym_MonoFoldable+type instance Sym MonoFoldable = Sym_MonoFoldable class Sym_MonoFoldable term where 	ofoldMap :: (MonoFoldable o, Monoid m) => term (MT.Element o -> m) -> term o -> term m 	ofoldr   :: MonoFoldable o => term (MT.Element o -> b -> b) -> term b -> term o -> term b@@ -75,13 +75,15 @@ instance (Sym_MonoFoldable term, Sym_Lambda term) => Sym_MonoFoldable (BetaT term)  -- Typing+instance NameTyOf MonoFoldable where+	nameTyOf _c = ["MonoFoldable"] `Mod` "MonoFoldable" instance FixityOf MonoFoldable instance ClassInstancesFor MonoFoldable instance TypeInstancesFor MonoFoldable  -- Compiling instance Gram_Term_AtomsFor src ss g MonoFoldable-instance (Source src, Inj_Sym ss MonoFoldable) => ModuleFor src ss MonoFoldable where+instance (Source src, SymInj ss MonoFoldable) => ModuleFor src ss MonoFoldable where 	moduleFor = ["MonoFoldable"] `moduleWhere` 	 [ "ofoldMap" := teMonoFoldable_ofoldMap 	 , "otoList"  := teMonoFoldable_otoList@@ -101,7 +103,7 @@ teMonoFoldable_ofoldMap :: TermDef MonoFoldable '[Proxy o, Proxy e, Proxy m] (MonoFoldable o # Monoid m # e #~ MT.Element o #> ((e -> m) -> o -> m)) teMonoFoldable_ofoldMap = Term (tyMonoFoldable o0 # tyMonoid m # e1 #~ famElement o0) ((e1 ~> m) ~> o0 ~> m) $ teSym @MonoFoldable $ lam2 ofoldMap 	where-	m :: Source src => Inj_Len vs => Inj_Kind (K m) => Type src (Proxy a ': Proxy b ': Proxy m ': vs) m+	m :: Source src => LenInj vs => KindInj (K m) => Type src (Proxy a ': Proxy b ': Proxy m ': vs) m 	m = tyVar "m" $ VarS $ VarS varZ  teMonoFoldable_otoList :: TermDef MonoFoldable '[Proxy o, Proxy e] (MonoFoldable o # e #~ MT.Element o #> (o -> [MT.Element o]))@@ -110,13 +112,13 @@ teMonoFoldable_ofoldr :: TermDef MonoFoldable '[Proxy o, Proxy e, Proxy a] (MonoFoldable o # e #~ MT.Element o #> ((e -> a -> a) -> a -> o -> a)) teMonoFoldable_ofoldr = Term (tyMonoFoldable o0 # e1 #~ famElement o0) ((e1 ~> a ~> a) ~> a ~> o0 ~> a) $ teSym @MonoFoldable $ lam1 $ \f -> lam $ lam . ofoldr f 	where-	a :: Source src => Inj_Len vs => Inj_Kind (K a) => Type src (Proxy _a ': Proxy b ': Proxy a ': vs) a+	a :: Source src => LenInj vs => KindInj (K a) => Type src (Proxy _a ': Proxy b ': Proxy a ': vs) a 	a = tyVar "a" $ VarS $ VarS varZ  teMonoFoldable_ofoldl' :: TermDef MonoFoldable '[Proxy o, Proxy e, Proxy a] (MonoFoldable o # e #~ MT.Element o #> ((a -> e -> a) -> a -> o -> a)) teMonoFoldable_ofoldl' = Term (tyMonoFoldable o0 # e1 #~ famElement o0) ((a ~> e1 ~> a) ~> a ~> o0 ~> a) $ teSym @MonoFoldable $ lam1 $ \f -> lam $ lam . ofoldl' f 	where-	a :: Source src => Inj_Len vs => Inj_Kind (K a) => Type src (Proxy _a ': Proxy b ': Proxy a ': vs) a+	a :: Source src => LenInj vs => KindInj (K a) => Type src (Proxy _a ': Proxy b ': Proxy a ': vs) a 	a = tyVar "a" $ VarS $ VarS varZ  teMonoFoldable_olength :: TermDef MonoFoldable '[Proxy o, Proxy e] (MonoFoldable o # e #~ MT.Element o #> (o -> Int))
Language/Symantic/Lib/MonoFunctor.hs view
@@ -12,6 +12,8 @@ -- * Type 'Element' data Element type instance Fam Element '[h] = MT.Element (UnProxy h)+instance NameTyOf Element where+	nameTyOf _c = ["MonoFunctor"] `Mod` "Element" instance ClassInstancesFor Element instance TypeInstancesFor Element where 	expandFamFor _c _len f (TyApp _ (TyApp _ z _ty_r) a `TypesS` TypesZ)@@ -22,10 +24,10 @@  -- ** 'Type's famElement :: Source src => Type src vs t -> Type src vs (MT.Element t)-famElement o = TyFam noSource (lenVars o) (inj_Const @Element) (o `TypesS` TypesZ)+famElement o = TyFam noSource (lenVars o) (constInj @Element) (o `TypesS` TypesZ)  -- * Class 'Sym_MonoFunctor'-type instance Sym (Proxy MonoFunctor) = Sym_MonoFunctor+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@@ -47,13 +49,15 @@ instance (Sym_MonoFunctor term, Sym_Lambda term) => Sym_MonoFunctor (BetaT term)  -- Typing+instance NameTyOf MonoFunctor where+	nameTyOf _c = ["MonoFunctor"] `Mod` "MonoFunctor" instance FixityOf MonoFunctor instance ClassInstancesFor MonoFunctor instance TypeInstancesFor MonoFunctor  -- Compiling instance Gram_Term_AtomsFor src ss g MonoFunctor-instance (Source src, Inj_Sym ss MonoFunctor) => ModuleFor src ss MonoFunctor where+instance (Source src, SymInj ss MonoFunctor) => ModuleFor src ss MonoFunctor where 	moduleFor = ["MonoFunctor"] `moduleWhere` 	 [ "omap" := teMonoFunctor_omap 	 ]@@ -62,11 +66,11 @@ tyMonoFunctor :: Source src => Type src vs a -> Type src vs (MonoFunctor a) tyMonoFunctor a = tyConstLen @(K MonoFunctor) @MonoFunctor (lenVars a) `tyApp` a -o0 :: Source src => Inj_Len vs => Inj_Kind (K o) =>+o0 :: Source src => LenInj vs => KindInj (K o) =>      Type src (Proxy o ': vs) o o0 = tyVar "o" varZ -e1 :: Source src => Inj_Len vs => Inj_Kind (K e) =>+e1 :: Source src => LenInj vs => KindInj (K e) =>      Type src (a ': Proxy e ': vs) e e1 = tyVar "e" $ VarS varZ
Language/Symantic/Lib/Monoid.hs view
@@ -11,7 +11,7 @@ import Language.Symantic.Lib.Function (a0)  -- * Class 'Sym_Monoid'-type instance Sym (Proxy Monoid) = Sym_Monoid+type instance Sym Monoid = Sym_Monoid class Sym_Monoid term where 	mempty  :: Monoid a => term a 	mappend :: Monoid a => term a -> term a -> term a@@ -35,13 +35,15 @@ instance (Sym_Monoid term, Sym_Lambda term) => Sym_Monoid (BetaT term)  -- Typing+instance NameTyOf Monoid where+	nameTyOf _c = ["Monoid"] `Mod` "Monoid" instance FixityOf Monoid instance ClassInstancesFor Monoid instance TypeInstancesFor Monoid  -- Compiling instance Gram_Term_AtomsFor src ss g Monoid-instance (Source src, Inj_Sym ss Monoid) => ModuleFor src ss Monoid where+instance (Source src, SymInj ss Monoid) => ModuleFor src ss Monoid where 	moduleFor = ["Monoid"] `moduleWhere` 	 [ "mempty"  := teMonoid_mempty 	 , "mappend" := teMonoid_mappend
Language/Symantic/Lib/NonNull.hs view
@@ -19,7 +19,7 @@ import Language.Symantic.Lib.Tuple2 (tyTuple2)  -- * Class 'Sym_NonNull'-type instance Sym (Proxy NonNull) = Sym_NonNull+type instance Sym NonNull = Sym_NonNull class Sym_NonNull term where 	fromNullable :: MonoFoldable o => term o -> term (Maybe (NonNull o)) 	toNullable   :: MonoFoldable o => term (NonNull o) -> term o@@ -85,6 +85,8 @@ instance (Sym_NonNull term, Sym_Lambda term) => Sym_NonNull (BetaT term)  -- Typing+instance NameTyOf NonNull where+	nameTyOf _c = ["NonNull"] `Mod` "NonNull" instance FixityOf NonNull instance TypeInstancesFor NonNull where 	expandFamFor c len f (TyApp _ z o `TypesS` TypesZ)@@ -113,7 +115,7 @@  -- Compiling instance Gram_Term_AtomsFor src ss g NonNull-instance (Source src, Inj_Sym ss NonNull) => ModuleFor src ss NonNull where+instance (Source src, SymInj ss NonNull) => ModuleFor src ss NonNull where 	moduleFor = ["NonNull"] `moduleWhere` 	 [ "fromNullable" := teNonNull_fromNullable 	 , "toNullable"   := teNonNull_toNullable
Language/Symantic/Lib/Num.hs view
@@ -12,7 +12,7 @@ import Language.Symantic.Lib.Integer (tyInteger)  -- * Class 'Sym_Num'-type instance Sym (Proxy Num) = Sym_Num+type instance Sym Num = Sym_Num class Sym_Num term where 	abs         :: Num n => term n -> term n 	negate      :: Num n => term n -> term n@@ -68,13 +68,15 @@ instance (Sym_Num term, Sym_Lambda term) => Sym_Num (BetaT term)  -- Typing+instance NameTyOf Num where+	nameTyOf _c = ["Num"] `Mod` "Num" instance FixityOf Num instance ClassInstancesFor Num instance TypeInstancesFor Num  -- Compiling instance Gram_Term_AtomsFor src ss g Num-instance (Source src, Inj_Sym ss Num) => ModuleFor src ss Num where+instance (Source src, SymInj ss Num) => ModuleFor src ss Num where 	moduleFor = ["Num"] `moduleWhere` 	 [ "abs"    := teNum_abs 	 , "negate" := teNum_negate
Language/Symantic/Lib/Num/Test.hs view
@@ -76,18 +76,20 @@  -- | A newtype to test prefix and postfix. newtype Num2 a = Num2 a-type instance Sym (Proxy Num2) = Sym_Num2+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, Inj_Sym ss Num) => ModuleFor src ss Num2 where+instance (Source src, SymInj ss Num) => ModuleFor src ss Num2 where 	moduleFor = ["Num2"] `moduleWhere` 	 [ "abs"    `withPrefix`   9 := teNum_abs 	 , "negate" `withPrefix`  10 := teNum_negate
Language/Symantic/Lib/Ord.hs view
@@ -14,7 +14,7 @@ import Language.Symantic.Lib.Eq (Sym_Eq)  -- * Class 'Sym_Ordering'-type instance Sym (Proxy Ordering) = Sym_Ordering+type instance Sym Ordering = Sym_Ordering class Sym_Eq term => Sym_Ordering term where 	ordering :: Ordering -> term Ordering 	default ordering :: Sym_Ordering (UnT term) => Trans term => Ordering -> term Ordering@@ -33,12 +33,14 @@ instance (Sym_Ordering term, Sym_Lambda term) => Sym_Ordering (BetaT term)  -- Typing+instance NameTyOf Ordering where+	nameTyOf _c = ["Ord"] `Mod` "Ordering" instance ClassInstancesFor Ordering instance TypeInstancesFor Ordering  -- Compiling instance Gram_Term_AtomsFor src ss g Ordering-instance (Source src, Inj_Sym ss Ordering) => ModuleFor src ss Ordering where+instance (Source src, SymInj ss Ordering) => ModuleFor src ss Ordering where 	moduleFor = [] `moduleWhere` 	 [ "LT" := teOrdering LT 	 , "EQ" := teOrdering EQ@@ -46,15 +48,15 @@ 	 ]  -- ** 'Type's-tyOrdering :: Source src => Inj_Len vs => Type src vs Ordering+tyOrdering :: Source src => LenInj vs => Type src vs Ordering tyOrdering = tyConst @(K Ordering) @Ordering  -- ** 'Term's-teOrdering :: Source src => Inj_Sym ss Ordering => Ordering -> Term src ss ts '[] (() #> Ordering)+teOrdering :: Source src => SymInj ss Ordering => Ordering -> Term src ss ts '[] (() #> Ordering) teOrdering o = Term noConstraint tyOrdering $ teSym @Ordering $ ordering o  -- * Class 'Sym_Ord'-type instance Sym (Proxy Ord) = Sym_Ord+type instance Sym Ord = Sym_Ord class Sym_Eq term => Sym_Ord term where 	compare  :: Ord a => term a -> term a -> term Ordering 	(<)      :: Ord a => term a -> term a -> term Bool; infix 4 <@@ -110,6 +112,8 @@ instance (Sym_Ord term, Sym_Lambda term) => Sym_Ord (BetaT term)  -- Typing+instance NameTyOf Ord where+	nameTyOf _c = ["Ord"] `Mod` "Ord" instance FixityOf Ord instance ClassInstancesFor Ord where 	proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)@@ -126,7 +130,7 @@  -- Compiling instance Gram_Term_AtomsFor src ss g Ord-instance (Source src, Inj_Sym ss Ord) => ModuleFor src ss Ord where+instance (Source src, SymInj ss Ord) => ModuleFor src ss Ord where 	moduleFor = ["Ord"] `moduleWhere` 	 [ "compare" := teOrd_compare 	 , "<"  `withInfixN` 4 := teOrd_lt
Language/Symantic/Lib/Ratio.hs view
@@ -11,7 +11,7 @@ import Language.Symantic.Lib.Integral (tyIntegral)  -- * Class 'Sym_Ratio'-type instance Sym (Proxy Ratio) = Sym_Ratio+type instance Sym Ratio = Sym_Ratio class Sym_Ratio term where 	ratio       :: Integral a => term a -> term a -> term (Ratio a) 	numerator   :: term (Ratio a) -> term a@@ -43,6 +43,8 @@ instance (Sym_Ratio term, Sym_Lambda term) => Sym_Ratio (BetaT term)  -- Typing+instance NameTyOf Ratio where+	nameTyOf _c = ["Ratio"] `Mod` "Ratio" instance FixityOf Ratio instance ClassInstancesFor Ratio where 	proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ c a))@@ -68,7 +70,7 @@  -- Compiling instance Gram_Term_AtomsFor src ss g Ratio-instance (Source src, Inj_Sym ss Ratio) => ModuleFor src ss Ratio where+instance (Source src, SymInj ss Ratio) => ModuleFor src ss Ratio where 	moduleFor = ["Ratio"] `moduleWhere` 	 [ "ratio"       := teRatio 	 , "numerator"   := teRatio_numerator
Language/Symantic/Lib/Real.hs view
@@ -13,7 +13,7 @@ import Language.Symantic.Lib.Ratio (tyRatio)  -- * Class 'Sym_Real'-type instance Sym (Proxy Real) = Sym_Real+type instance Sym Real = Sym_Real class Sym_Real term where 	toRational :: Real a => term a -> term Rational 	default toRational :: Sym_Real (UnT term) => Trans term => Real a => term a -> term Rational@@ -31,13 +31,15 @@ instance (Sym_Real term, Sym_Lambda term) => Sym_Real (BetaT term)  -- Typing+instance NameTyOf Real where+	nameTyOf _c = ["Real"] `Mod` "Real" instance FixityOf Real instance ClassInstancesFor Real instance TypeInstancesFor Real  -- Compiling instance Gram_Term_AtomsFor src ss g Real-instance (Source src, Inj_Sym ss Real) => ModuleFor src ss Real where+instance (Source src, SymInj ss Real) => ModuleFor src ss Real where 	moduleFor = ["Real"] `moduleWhere` 	 [ "toRational" := teReal_toRational 	 ]@@ -46,7 +48,7 @@ tyReal :: Source src => Type src vs a -> Type src vs (Real a) tyReal a = tyConstLen @(K Real) @Real (lenVars a) `tyApp` a -tyRational :: Source src => Inj_Len vs => Type src vs Rational+tyRational :: Source src => LenInj vs => Type src vs Rational tyRational = tyRatio tyInteger  -- ** 'Term's
Language/Symantic/Lib/Semigroup.hs view
@@ -11,7 +11,7 @@ import Language.Symantic.Lib.Integral (tyIntegral)  -- * Class 'Sym_Semigroup'-type instance Sym (Proxy Semigroup) = Sym_Semigroup+type instance Sym Semigroup = Sym_Semigroup class Sym_Semigroup term where 	(<>)   :: Semigroup a => term a -> term a -> term a 	stimes :: (Semigroup a, Integral b) => term b -> term a -> term a@@ -36,13 +36,15 @@ instance (Sym_Semigroup term, Sym_Lambda term) => Sym_Semigroup (BetaT term)  -- Typing+instance NameTyOf Semigroup where+	nameTyOf _c = ["Semigroup"] `Mod` "Semigroup" instance FixityOf Semigroup instance ClassInstancesFor Semigroup instance TypeInstancesFor Semigroup  -- Compiling instance Gram_Term_AtomsFor src ss g Semigroup-instance (Source src, Inj_Sym ss Semigroup) => ModuleFor src ss Semigroup where+instance (Source src, SymInj ss Semigroup) => ModuleFor src ss Semigroup where 	moduleFor = ["Semigroup"] `moduleWhere` 	 [ "<>" `withInfixR` 6 := teSemigroup_sappend 	 , "stimes" := teSemigroup_stimes
Language/Symantic/Lib/Sequences.hs view
@@ -14,7 +14,7 @@ import Language.Symantic.Lib.MonoFunctor (e1, famElement)  -- * Class 'Sym_SemiSequence'-type instance Sym (Proxy SemiSequence) = Sym_SemiSequence+type instance Sym SemiSequence = Sym_SemiSequence class Sym_SemiSequence term where 	intersperse :: SemiSequence s => term (MT.Element s) -> term s -> term s 	cons        :: SemiSequence s => term (MT.Element s) -> term s -> term s@@ -50,13 +50,15 @@ instance (Sym_SemiSequence term, Sym_Lambda term) => Sym_SemiSequence (BetaT term)  -- Typing+instance NameTyOf SemiSequence where+	nameTyOf _c = ["SemiSequence"] `Mod` "SemiSequence" instance FixityOf SemiSequence instance ClassInstancesFor SemiSequence instance TypeInstancesFor SemiSequence  -- Compiling instance Gram_Term_AtomsFor src ss g SemiSequence-instance (Source src, Inj_Sym ss SemiSequence) => ModuleFor src ss SemiSequence where+instance (Source src, SymInj ss SemiSequence) => ModuleFor src ss SemiSequence where 	moduleFor = ["SemiSequence"] `moduleWhere` 	 [ "intersperse" := teSemiSequence_intersperse 	 , "cons"        := teSemiSequence_cons@@ -68,7 +70,7 @@ tySemiSequence :: Source src => Type src vs a -> Type src vs (SemiSequence a) tySemiSequence a = tyConstLen @(K SemiSequence) @SemiSequence (lenVars a) `tyApp` a -s0 :: Source src => Inj_Len vs => Inj_Kind (K s) =>+s0 :: Source src => LenInj vs => KindInj (K s) =>       Type src (Proxy s ': vs) s s0 = tyVar "s" varZ @@ -84,7 +86,7 @@ teSemiSequence_snoc = Term (tySemiSequence s0 # e1 #~ famElement s0) (s0 ~> e1 ~> s0) $ teSym @SemiSequence $ lam2 snoc  -- * Class 'Sym_IsSequence'-type instance Sym (Proxy IsSequence) = Sym_IsSequence+type instance Sym IsSequence = Sym_IsSequence class Sym_IsSequence term where 	filter :: IsSequence s => term (MT.Element s -> Bool) -> term s -> term s 	default filter :: Sym_IsSequence (UnT term) => Trans term => IsSequence s => term (MT.Element s -> Bool) -> term s -> term s@@ -102,13 +104,15 @@ instance (Sym_IsSequence term, Sym_Lambda term) => Sym_IsSequence (BetaT term)  -- Typing+instance NameTyOf IsSequence where+	nameTyOf _c = ["IsSequence"] `Mod` "IsSequence" instance FixityOf IsSequence instance ClassInstancesFor IsSequence instance TypeInstancesFor IsSequence  -- Compiling instance Gram_Term_AtomsFor src ss g IsSequence-instance (Source src, Inj_Sym ss IsSequence) => ModuleFor src ss IsSequence where+instance (Source src, SymInj ss IsSequence) => ModuleFor src ss IsSequence where 	moduleFor = ["IsSequence"] `moduleWhere` 	 [ "filter" := teIsSequence_filter 	 ]
Language/Symantic/Lib/Show.hs view
@@ -14,7 +14,7 @@ import Language.Symantic.Lib.List (tyList)  -- * Class 'Sym_Show'-type instance Sym (Proxy Show) = Sym_Show+type instance Sym Show = Sym_Show class Sym_Show term where 	showsPrec :: Show a => term Int -> term a -> term ShowS 	show      :: Show a => term a -> term String@@ -45,13 +45,15 @@ instance (Sym_Show term, Sym_Lambda term) => Sym_Show (BetaT term)  -- Typing+instance NameTyOf Show where+	nameTyOf _c = ["Show"] `Mod` "Show" instance FixityOf Show instance ClassInstancesFor Show instance TypeInstancesFor Show  -- Compiling instance Gram_Term_AtomsFor src ss g Show-instance (Source src, Inj_Sym ss Show) => ModuleFor src ss Show where+instance (Source src, SymInj ss Show) => ModuleFor src ss Show where 	moduleFor = ["Show"] `moduleWhere` 	 [ "showsPrec" := teShow_showsPrec 	 , "show"      := teShow_show@@ -62,7 +64,7 @@ tyShow :: Source src => Type src vs a -> Type src vs (Show a) tyShow a = tyConstLen @(K Show) @Show (lenVars a) `tyApp` a -tyShowS :: Source src => Inj_Len vs => Type src vs ShowS+tyShowS :: Source src => LenInj vs => Type src vs ShowS tyShowS = tyString ~> tyString  -- ** 'Term's
Language/Symantic/Lib/Text.hs view
@@ -14,7 +14,7 @@ import Language.Symantic.Lib.MonoFunctor (Element)  -- * Class 'Sym_Text'-type instance Sym (Proxy Text) = Sym_Text+type instance Sym Text = Sym_Text class Sym_Text term where 	text :: Text -> term Text 	default text :: Sym_Text (UnT term) => Trans term => Text -> term Text@@ -33,6 +33,8 @@ instance (Sym_Text term, Sym_Lambda term) => Sym_Text (BetaT term)  -- Typing+instance NameTyOf Text where+	nameTyOf _c = ["Text"] `Mod` "Text" instance ClassInstancesFor Text where 	proveConstraintFor _ (TyApp _ (TyConst _ _ q) c) 	 | Just HRefl <- proj_ConstKiTy @_ @Text c@@ -59,9 +61,9 @@ instance ModuleFor src ss Text  -- ** 'Type's-tyText :: Source src => Inj_Len vs => Type src vs Text+tyText :: Source src => LenInj vs => Type src vs Text tyText = tyConst @(K Text) @Text  -- ** 'Term's-teText :: Source src => Inj_Sym ss Text => Text -> Term src ss ts '[] (() #> Text)+teText :: Source src => SymInj ss Text => Text -> Term src ss ts '[] (() #> Text) teText t = Term noConstraint tyText $ teSym @Text $ text t
Language/Symantic/Lib/Traversable.hs view
@@ -13,7 +13,7 @@ import Language.Symantic.Lib.Functor (f2)  -- * Class 'Sym_Traversable'-type instance Sym (Proxy Traversable) = Sym_Traversable+type instance Sym Traversable = Sym_Traversable class Sym_Traversable term where 	traverse :: Traversable t => Applicative f => term (a -> f b) -> term (t a) -> term (f (t b)) 	default traverse :: Sym_Traversable (UnT term) => Trans term => Traversable t => Applicative f => term (a -> f b) -> term (t a) -> term (f (t b))@@ -31,13 +31,15 @@ instance (Sym_Traversable term, Sym_Lambda term) => Sym_Traversable (BetaT term)  -- Typing+instance NameTyOf Traversable where+	nameTyOf _c = ["Traversable"] `Mod` "Traversable" instance FixityOf Traversable instance ClassInstancesFor Traversable instance TypeInstancesFor Traversable  -- Compiling instance Gram_Term_AtomsFor src ss g Traversable-instance (Source src, Inj_Sym ss Traversable) => ModuleFor src ss Traversable where+instance (Source src, SymInj ss Traversable) => ModuleFor src ss Traversable where 	moduleFor = ["Traversable"] `moduleWhere` 	 [ "traverse" := teTraversable_traverse 	 ]@@ -50,5 +52,5 @@ teTraversable_traverse :: TermDef Traversable '[Proxy a, Proxy b, Proxy f, Proxy t] (Traversable t # Applicative f #> ((a -> f b) -> t a -> f (t b))) teTraversable_traverse = Term (tyTraversable t # tyApplicative f2) ((a0 ~> f2 `tyApp` b1) ~> t `tyApp` a0 ~> f2 `tyApp` (t `tyApp` b1)) $ teSym @Traversable $ lam2 traverse 	where-	t :: Source src => Inj_Len vs => Inj_Kind (K t) => Type src (Proxy a ': Proxy b ': Proxy c ': Proxy t ': vs) t+	t :: Source src => LenInj vs => KindInj (K t) => Type src (Proxy a ': Proxy b ': Proxy c ': Proxy t ': vs) t 	t = tyVar "t" $ VarS $ VarS $ VarS varZ
Language/Symantic/Lib/Tuple2.hs view
@@ -15,7 +15,7 @@ import Language.Symantic.Lib.Monoid (tyMonoid)  -- * Class 'Sym_Tuple2'-type instance Sym (Proxy (,)) = Sym_Tuple2+type instance Sym (,) = Sym_Tuple2 class Sym_Tuple2 term where 	tuple2 :: term a -> term b -> term (a, b) 	fst :: term (a, b) -> term a@@ -50,6 +50,8 @@ instance (Sym_Tuple2 term, Sym_Lambda term) => Sym_Tuple2 (BetaT term)  -- Typing+instance NameTyOf (,) where+	nameTyOf _c = ["Tuple2"] `Mod` "," instance FixityOf (,) where 	fixityOf _c = Just $ Fixity2 $ infixN (-1) instance ClassInstancesFor (,) where@@ -100,30 +102,30 @@  , Gram_Rule g  , Gram_Comment g  , Gram_Term src ss g- , Inj_Sym ss (,)+ , SymInj ss (,)  ) => Gram_Term_AtomsFor src ss g (,) where 	g_term_atomsFor = 	 -- TODO: proper TupleSections 	 [ rule "teTuple2_2" $-		g_source $ parens $+		source $ parens $ 		(\a b src -> 			BinTree2 (BinTree2 (BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teTuple2) a) b) 		 <$> g_term 		 <*  symbol "," 		 <*> g_term 	 , rule "teTuple2" $-		g_source $+		source $ 		(\src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teTuple2) 		 <$ symbol "(,)" 	 ]-instance (Source src, Inj_Sym ss (,)) => ModuleFor src ss (,) where+instance (Source src, SymInj ss (,)) => ModuleFor src ss (,) where 	moduleFor = ["Tuple2"] `moduleWhere` 	 [ "fst" := teTuple2_fst 	 , "snd" := teTuple2_snd 	 ]  -- ** 'Term's-tyTuple2 :: Source src => Inj_Len vs => Type src vs a -> Type src vs b -> Type src vs (a, b)+tyTuple2 :: Source src => LenInj vs => Type src vs a -> Type src vs b -> Type src vs (a, b) tyTuple2 a b = tyConst @(K (,)) @(,) `tyApp` a `tyApp` b  teTuple2 :: TermDef (,) '[Proxy a, Proxy b] (() #> (a -> b -> (a, b)))
Language/Symantic/Lib/Unit.hs view
@@ -9,7 +9,7 @@ import Language.Symantic.Grammar  -- * Class 'Sym_Unit'-type instance Sym (Proxy ()) = Sym_Unit+type instance Sym () = Sym_Unit class Sym_Unit term where 	unit :: term () 	default unit :: Sym_Unit (UnT term) => Trans term => term ()@@ -27,6 +27,8 @@ instance (Sym_Unit term, Sym_Lambda term) => Sym_Unit (BetaT term)  -- Typing+instance NameTyOf () where+	nameTyOf _c = [] `Mod` "" instance ClassInstancesFor () where 	proveConstraintFor _ (TyApp _ (TyConst _ _ q) z) 	 | Just HRefl <- proj_ConstKiTy @_ @() z@@ -46,11 +48,11 @@  ( Gram_Source src g  , Gram_Rule g  , Gram_Comment g- , Inj_Sym ss ()+ , SymInj ss ()  ) => Gram_Term_AtomsFor src ss g () where 	g_term_atomsFor = 	 [ rule "teUnit" $-		g_source $+		source $ 		(\src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teUnit) 		 <$ symbol "(" 		 <* symbol ")"@@ -58,7 +60,7 @@ instance ModuleFor src ss ()  -- ** 'Type's-tyUnit :: Source src => Inj_Len vs => Type src vs ()+tyUnit :: Source src => LenInj vs => Type src vs () tyUnit = tyConst @(K ()) @()  -- ** 'Term's
Language/Symantic/Typing/Test.hs view
@@ -70,13 +70,16 @@  ] type SRC = SrcTe (NonEmpty P.SourcePos) SS -cs :: Source src => Name2Type src-cs =-	Map.insert "String"+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) $-	inj_Name2Type @SS+	modulesTyInj @SS  tests :: TestTree tests = testGroup "Typing" $@@ -86,7 +89,7 @@ 		where 		got :: Either (P.ParseError Char P.Dec) 		              (Either (Error_Type SRC) (TypeVT SRC))-		got = readType cs <$> P.runParser (unCF g) "" inp+		got = readType impsTy modsTy <$> P.runParser (unCF g) "" inp 		g :: Gram_Type SRC g => CF g (AST_Type SRC) 		g = g_type <* eoi in 	let (==>) = run; infixr 0 ==> in@@ -142,7 +145,7 @@ 		let run inp = testCase inp $ got @?= Right (Left ()) 			where 			got :: Either (P.ParseError Char P.Dec) (Either () (TypeVT SRC))-			got = left (Fun.const ()) . readType cs <$> P.runParser (unCF g) "" inp+			got = left (Fun.const ()) . readType impsTy modsTy <$> P.runParser (unCF g) "" inp 			g :: Gram_Type SRC g => CF g (AST_Type SRC) 			g = g_type <* eoi in 		run <$>@@ -154,8 +157,10 @@ 		 , "Monad Eq" 		 ]  , testGroup "proveConstraint" $-	let (==>) (typ::Type SRC '[] (t::Constraint)) expected =-		testCase (show typ) $+	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
symantic-lib.cabal view
@@ -19,7 +19,7 @@ -- PVP:  +-+------- breaking API changes --       | | +----- non-breaking API additions --       | | | +--- code changes with no API change-version: 0.0.2.20170623+version: 0.0.2.20170702  Source-Repository head   location: git://git.autogeree.net/symantic