Change Term to be a GADT, to avoid type applications and allow TypeOf Term.
authorJulien Moutinho <julm+symantic@autogeree.net>
Thu, 22 Jun 2017 15:48:44 +0000 (17:48 +0200)
committerJulien Moutinho <julm+symantic@autogeree.net>
Thu, 22 Jun 2017 15:49:51 +0000 (17:49 +0200)
20 files changed:
symantic-lib/Language/Symantic/Lib/Bool.hs
symantic-lib/Language/Symantic/Lib/Char.hs
symantic-lib/Language/Symantic/Lib/Either.hs
symantic-lib/Language/Symantic/Lib/Function.hs
symantic-lib/Language/Symantic/Lib/IO.hs
symantic-lib/Language/Symantic/Lib/If.hs
symantic-lib/Language/Symantic/Lib/Int.hs
symantic-lib/Language/Symantic/Lib/Integer.hs
symantic-lib/Language/Symantic/Lib/List.hs
symantic-lib/Language/Symantic/Lib/Map.hs
symantic-lib/Language/Symantic/Lib/Maybe.hs
symantic-lib/Language/Symantic/Lib/Ord.hs
symantic-lib/Language/Symantic/Lib/Ratio.hs
symantic-lib/Language/Symantic/Lib/Text.hs
symantic-lib/Language/Symantic/Lib/Tuple2.hs
symantic-lib/Language/Symantic/Lib/Unit.hs
symantic/Language/Symantic/Compiling/Beta.hs
symantic/Language/Symantic/Compiling/Read.hs
symantic/Language/Symantic/Compiling/Term.hs
symantic/Language/Symantic/Typing/Type.hs

index 9a6198f271774b57c5f61edaef1458ad3b548447..5f2056b893ead8c8094462f4c0ac8265360ca17d 100644 (file)
@@ -86,13 +86,13 @@ tyBool :: Source src => Inj_Len 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 => Inj_Sym ss Bool => Bool -> Term src ss ts '[] (() #> Bool)
 teBool b = Term noConstraint tyBool $ teSym @Bool $ bool b
 
-teBool_not :: TermDef Bool '[] (Bool -> Bool)
+teBool_not :: TermDef Bool '[] (() #> (Bool -> Bool))
 teBool_not = Term noConstraint (tyBool ~> tyBool) $ teSym @Bool $ lam1 not
 
-teBool_and, teBool_or, teBool_xor :: TermDef Bool '[] (Bool -> Bool -> Bool)
+teBool_and, teBool_or, teBool_xor :: TermDef Bool '[] (() #> (Bool -> Bool -> Bool))
 teBool_and = Term noConstraint (tyBool ~> tyBool ~> tyBool) $ teSym @Bool $ lam2 (&&)
 teBool_or  = Term noConstraint (tyBool ~> tyBool ~> tyBool) $ teSym @Bool $ lam2 (||)
 teBool_xor = Term noConstraint (tyBool ~> tyBool ~> tyBool) $ teSym @Bool $ lam2 xor
index 9c4b1ef0ef47d36424ecc0120f71bfc61a8a804b..184d14de11531257c52391f82034c7349807a5b7 100644 (file)
@@ -92,9 +92,9 @@ tyString :: Source src => Inj_Len 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 => Inj_Sym 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)
+teChar_toUpper, teChar_toLower :: TermDef Char '[] (() #> (Char -> Char))
 teChar_toUpper = Term noConstraint (tyChar ~> tyChar) $ teSym @Char $ lam1 char_toUpper
 teChar_toLower = Term noConstraint (tyChar ~> tyChar) $ teSym @Char $ lam1 char_toLower
index 78fed3527f37af02417026fb0cd82ce12293fec3..463990d99d56ada5d7084738feafdc21f6288f34 100644 (file)
@@ -92,9 +92,9 @@ tyEither :: Source src => Type src vs l -> Type src vs r -> Type src vs (Either
 tyEither l r = tyConstLen @(K Either) @Either (lenVars l) `tyApp` l `tyApp` r
 
 -- ** 'Term's
-teEither_Left :: TermDef Either '[Proxy a, Proxy b] (a -> Either a b)
+teEither_Left :: TermDef Either '[Proxy a, Proxy b] (() #> (a -> Either a b))
 teEither_Left = Term noConstraint (a0 ~> tyEither a0 b1) $ teSym @Either $ lam1 _Left
-teEither_Right :: TermDef Either '[Proxy a, Proxy b] (b -> Either a b)
+teEither_Right :: TermDef Either '[Proxy a, Proxy b] (() #> (b -> Either a b))
 teEither_Right = Term noConstraint (b1 ~> tyEither a0 b1) $ teSym @Either $ lam1 _Right
-teEither_either :: TermDef Either '[Proxy a, Proxy b, Proxy c] ((a -> c) -> (b -> c) -> Either a b -> c)
+teEither_either :: TermDef Either '[Proxy a, Proxy b, Proxy c] (() #> ((a -> c) -> (b -> c) -> Either a b -> c))
 teEither_either = Term noConstraint ((a0 ~> c2) ~> (b1 ~> c2) ~> tyEither a0 b1 ~> c2) $ teSym @Either $ lam3 either
index f14b2f8cb973266da886800c83a35172a67ae61c..5a05381fb92a08776f7ade63c9c7bef364293ab4 100644 (file)
@@ -92,14 +92,14 @@ c2 :: Source src => Inj_Len vs => Inj_Kind (K c) =>
 c2 = tyVar "c" $ VarS $ VarS varZ
 
 -- ** 'Term's
-teFunction_compose :: TermDef (->) '[Proxy a, Proxy b, Proxy c] ((b -> c) -> (a -> b) -> (a -> c))
+teFunction_compose :: TermDef (->) '[Proxy a, Proxy b, Proxy c] (() #> ((b -> c) -> (a -> b) -> (a -> c)))
 teFunction_compose = Term noConstraint ((b1 ~> c2) ~> (a0 ~> b1) ~> (a0 ~> c2)) $ teSym @(->) $ lam2 comp
 
-teFunction_const :: TermDef (->) '[Proxy a, Proxy b] (a -> b -> a)
+teFunction_const :: TermDef (->) '[Proxy a, Proxy b] (() #> (a -> b -> a))
 teFunction_const = Term noConstraint (a0 ~> b1 ~> a0) $ teSym @(->) $ lam2 const
 
-teFunction_flip :: TermDef (->) '[Proxy a, Proxy b, Proxy c] ((a -> b -> c) -> (b -> a -> c))
+teFunction_flip :: TermDef (->) '[Proxy a, Proxy b, Proxy c] (() #> ((a -> b -> c) -> (b -> a -> c)))
 teFunction_flip = Term noConstraint ((a0 ~> b1 ~> c2) ~> (b1 ~> a0 ~> c2)) $ teSym @(->) $ lam1 flip
 
-teFunction_id :: TermDef (->) '[Proxy a] (a -> a)
+teFunction_id :: TermDef (->) '[Proxy a] (() #> (a -> a))
 teFunction_id = Term noConstraint (a0 ~> a0) $ teSym @(->) $ lam1 id
index e3ee59f9bc85dc1180d9717444ea6d7e27122087..5ac6dc6b5d5c0eb507a1636f929b52ac3ffc756c 100644 (file)
@@ -118,8 +118,8 @@ tyFilePath :: Source src => Inj_Len vs => Type src vs FilePath
 tyFilePath = tyString
 
 -- ** 'Term's
-teIO_hClose :: TermDef IO.Handle '[] (IO.Handle -> IO ())
+teIO_hClose :: TermDef IO.Handle '[] (() #> (IO.Handle -> IO ()))
 teIO_hClose = Term noConstraint (tyIO_Handle ~> tyIO tyUnit) $ teSym @IO.Handle $ lam1 io_hClose
 
-teIO_openFile :: TermDef IO.Handle '[] (FilePath -> IO.IOMode -> IO (IO.Handle))
+teIO_openFile :: TermDef IO.Handle '[] (() #> (FilePath -> IO.IOMode -> IO (IO.Handle)))
 teIO_openFile = Term noConstraint (tyFilePath ~> tyIO_Mode ~> tyIO tyIO_Handle) $ teSym @IO.Handle $ lam2 io_openFile
index 381a3f7bce4526faa243ddca8cd54f819cdac8ef..aebbb85cc70fd9906a19601fde78c73c9179f901 100644 (file)
@@ -49,5 +49,5 @@ instance ModuleFor src ss If
 -- ** 'Type's
 
 -- ** 'Term's
-teIf_if :: TermDef If '[Proxy a] (Bool -> a -> a -> a)
+teIf_if :: TermDef If '[Proxy a] (() #> (Bool -> a -> a -> a))
 teIf_if = Term noConstraint (tyBool ~> a0 ~> a0 ~> a0) $ teSym @If $ lam3 if_
index 1c41f2a25ab172aef29272ec7981bb3bcf88d51b..b442ee7e45b398f2e9c512bee74822f8ba3455ab 100644 (file)
@@ -52,5 +52,5 @@ tyInt :: Source src => Inj_Len 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 => Inj_Sym ss Int => Int -> Term src ss ts '[] (() #> Int)
 teInt i = Term noConstraint tyInt $ teSym @Int $ int i
index aa851b9e493681dd7a99d1c02e73e923732aece2..8c255859b04f504057323e3acbe354eab14d7656 100644 (file)
@@ -64,5 +64,5 @@ instance ModuleFor src ss Integer
 tyInteger :: Source src => Inj_Len 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 => Inj_Sym ss Integer => Integer -> Term src ss ts '[] (() #> Integer)
 teInteger i = Term noConstraint tyInteger $ teSym @Integer $ integer i
index db4b515d70e2b522d4f044ee501819108b9ccaa4..0a7d6a722d2df4b4c30df1e544a3b4b028af6a83 100644 (file)
@@ -138,22 +138,11 @@ tyList :: Source src => Inj_Len 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 => Inj_Sym 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 =
-       Term noConstraint (a0 ~> tyList a0 ~> tyList a0) $
-       teSym @[] $ lam2 list_cons
+teList_cons :: Source src => Inj_Sym 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 =
-       Term noConstraint ((a0 ~> b1 ~> c2) ~> tyList a0 ~> tyList b1 ~> tyList c2) $
-       teSym @[] $ lam3 zipWith
+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 = Term noConstraint ((a0 ~> b1 ~> c2) ~> tyList a0 ~> tyList b1 ~> tyList c2) $ teSym @[] $ lam3 zipWith
index 6b5f3c5619906d0bc0f42370e082f1609e6fae48..a385fdce4728796857a481906f94f0f8ec68c464 100644 (file)
@@ -164,11 +164,11 @@ teMap_lookup = Term (tyOrd k1) (k1 ~> tyMap k1 a0 ~> tyMaybe a0) $ teSym @Map $
 teMap_member :: TermDef Map '[Proxy a, Proxy k] (Ord k #> (k -> Map k a -> Bool))
 teMap_member = Term (tyOrd k1) (k1 ~> tyMap k1 a0 ~> tyBool) $ teSym @Map $ lam2 map_member
 
-teMap_foldrWithKey :: TermDef Map '[Proxy a, Proxy b, Proxy k] ((k -> a -> b -> b) -> b -> Map k a -> b)
+teMap_foldrWithKey :: TermDef Map '[Proxy a, Proxy b, Proxy k] (() #> ((k -> a -> b -> b) -> b -> Map k a -> b))
 teMap_foldrWithKey = Term noConstraint ((k2 ~> a0 ~> b1 ~> b1) ~> b1 ~> tyMap k2 a0 ~> b1) $ teSym @Map $ lam3 map_foldrWithKey
 
-teMap_mapWithKey :: TermDef Map '[Proxy a, Proxy b, Proxy k] ((k -> a -> b) -> Map k a -> Map k b)
+teMap_mapWithKey :: TermDef Map '[Proxy a, Proxy b, Proxy k] (() #> ((k -> a -> b) -> Map k a -> Map k b))
 teMap_mapWithKey = Term noConstraint ((k2 ~> a0 ~> b1) ~> tyMap k2 a0 ~> tyMap k2 b1) $ teSym @Map $ lam2 map_mapWithKey
 
-teMap_keys :: TermDef Map '[Proxy a, Proxy k] (Map k a -> [k])
+teMap_keys :: TermDef Map '[Proxy a, Proxy k] (() #> (Map k a -> [k]))
 teMap_keys = Term noConstraint (tyMap k1 a0 ~> tyList k1) $ teSym @Map $ lam1 map_keys
index dddacb7fa609d96d9cdea6bf0d72cce9f06e4178..6fc5ca2f6eaa8e91985418c0811fa1d0ae22c4b3 100644 (file)
@@ -90,11 +90,11 @@ tyMaybe :: Source src => Inj_Len vs => Type src vs a -> Type src vs (Maybe a)
 tyMaybe = (tyConst @(K Maybe) @Maybe `tyApp`)
 
 -- ** 'Term's
-teMaybe_Nothing :: TermDef Maybe '[Proxy a] (Maybe a)
+teMaybe_Nothing :: TermDef Maybe '[Proxy a] (() #> Maybe a)
 teMaybe_Nothing = Term noConstraint (tyMaybe a0) $ teSym @Maybe $ _Nothing
 
-teMaybe_Just :: TermDef Maybe '[Proxy a] (a -> Maybe a)
+teMaybe_Just :: TermDef Maybe '[Proxy a] (() #> (a -> Maybe a))
 teMaybe_Just = Term noConstraint (a0 ~> tyMaybe a0) $ teSym @Maybe $ lam1 _Just
 
-teMaybe_maybe :: TermDef Maybe '[Proxy a, Proxy b] (b -> (a -> b) -> Maybe a -> b)
+teMaybe_maybe :: TermDef Maybe '[Proxy a, Proxy b] (() #> (b -> (a -> b) -> Maybe a -> b))
 teMaybe_maybe = Term noConstraint (b1 ~> (a0 ~> b1) ~> tyMaybe a0 ~> b1) $ teSym @Maybe $ lam1 $ \b' -> lam $ lam . maybe b'
index ac6abd2bb436df4f4127b1ec52af7e6286173bfa..e2cb902eb5c7ff5090f19688a8bea55799d7eb74 100644 (file)
@@ -50,7 +50,7 @@ tyOrdering :: Source src => Inj_Len 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 => Inj_Sym ss Ordering => Ordering -> Term src ss ts '[] (() #> Ordering)
 teOrdering o = Term noConstraint tyOrdering $ teSym @Ordering $ ordering o
 
 -- * Class 'Sym_Ord'
index d63831d4295fd116450023d2fab9ba26e6ea8301..67b72b4bf2740b50e2c8a28da57c54e5d74e5a5a 100644 (file)
@@ -83,6 +83,6 @@ tyRatio a = tyConstLen @(K Ratio) @Ratio (lenVars a) `tyApp` a
 teRatio :: TermDef Ratio '[Proxy a] (Integral a #> (a -> a -> Ratio a))
 teRatio = Term (tyIntegral a0) (a0 ~> a0 ~> tyRatio a0) $ teSym @Ratio $ lam2 ratio
 
-teRatio_numerator, teRatio_denominator :: TermDef Ratio '[Proxy a] (Ratio a -> a)
+teRatio_numerator, teRatio_denominator :: TermDef Ratio '[Proxy a] (() #> (Ratio a -> a))
 teRatio_numerator   = Term noConstraint (tyRatio a0 ~> a0) $ teSym @Ratio $ lam1 numerator
 teRatio_denominator = Term noConstraint (tyRatio a0 ~> a0) $ teSym @Ratio $ lam1 denominator
index 9d5cec9bd734588e0d288577d2ee9666855f247c..a29962c1d9488a3f115e1c4db0a6292d046a0bb2 100644 (file)
@@ -63,5 +63,5 @@ tyText :: Source src => Inj_Len 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 => Inj_Sym ss Text => Text -> Term src ss ts '[] (() #> Text)
 teText t = Term noConstraint tyText $ teSym @Text $ text t
index 17042ad7a5e2d1ed2f44948b7b9eafcb602afb63..2d051fe7ce8bd088b7077ecaf46156185c32dac0 100644 (file)
@@ -126,9 +126,9 @@ instance (Source src, Inj_Sym ss (,)) => ModuleFor src ss (,) where
 tyTuple2 :: Source src => Inj_Len 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))
+teTuple2 :: TermDef (,) '[Proxy a, Proxy b] (() #> (a -> b -> (a, b)))
 teTuple2 = Term noConstraint (a0 ~> b1 ~> tyTuple2 a0 b1) $ teSym @(,) $ lam2 tuple2
-teTuple2_fst :: TermDef (,) '[Proxy a, Proxy b] ((a, b) -> a)
+teTuple2_fst :: TermDef (,) '[Proxy a, Proxy b] (() #> ((a, b) -> a))
 teTuple2_fst = Term noConstraint (tyTuple2 a0 b1 ~> a0) $ teSym @(,) $ lam1 fst
-teTuple2_snd :: TermDef (,) '[Proxy a, Proxy b] ((a, b) -> b)
+teTuple2_snd :: TermDef (,) '[Proxy a, Proxy b] (() #> ((a, b) -> b))
 teTuple2_snd = Term noConstraint (tyTuple2 a0 b1 ~> b1) $ teSym @(,) $ lam1 snd
index c260e61d05f43276e6659f2e0a503010766d9a28..222a47f7924ae731e7245c11c939bdc21369f954 100644 (file)
@@ -62,7 +62,5 @@ tyUnit :: Source src => Inj_Len vs => Type src vs ()
 tyUnit = tyConst @(K ()) @()
 
 -- ** 'Term's
-teUnit ::
- Source src => Inj_Sym ss () =>
- Term src ss ts '[] ()
+teUnit :: TermDef () '[] (() #> ())
 teUnit = Term noConstraint tyUnit $ teSym @() $ unit
index c08d57720aae00b508ed5ac7f94c8b7a61fb3288..dfc2cdf0496b20fe40bc6f715a7b62c8d3ca6d17 100644 (file)
@@ -27,13 +27,13 @@ betaTerm (Term qf tf (TeSym te_fun)) (Term qa ta (TeSym te_arg)) =
                        Right $
                        case (proveConstraint qf, proveConstraint qa) of
                         -- NOTE: remove provable Constraints to keep those smaller.
-                        (Just Dict, Just Dict) -> TermT $ Term @_ @_ @_ @_ @(_ #> _) (noConstraintLen (lenVars a2b_b)) a2b_b $
+                        (Just Dict, Just Dict) -> TermT $ Term (noConstraintLen (lenVars a2b_b)) a2b_b $
                                TeSym $ \c -> te_fun c `app` te_arg c
-                        (Just Dict, Nothing) -> TermT $ Term @_ @_ @_ @_ @(_ #> _) qa a2b_b $
+                        (Just Dict, Nothing) -> TermT $ Term qa a2b_b $
                                TeSym $ \c -> te_fun c `app` te_arg c
-                        (Nothing, Just Dict) -> TermT $ Term @_ @_ @_ @_ @(_ #> _) qf a2b_b $
+                        (Nothing, Just Dict) -> TermT $ Term qf a2b_b $
                                TeSym $ \c -> te_fun c `app` te_arg c
-                        (Nothing, Nothing)     -> TermT $ Term @_ @_ @_ @_ @(_ #> _) (qf # qa) a2b_b $
+                        (Nothing, Nothing)     -> TermT $ Term (qf # qa) a2b_b $
                                TeSym $ \c -> te_fun c `app` te_arg c
         _ -> Left $ Error_Beta_Term_not_a_function $ TypeVT (qf #> tf)
 
index f7195174f9b5952fc9d57913be3f960eff65aa58..89da97fef3451471df1b62807c5f1de1c594963e 100644 (file)
@@ -52,16 +52,16 @@ readTerm n2t ctxTy ast = do
                                        case (proveConstraint qa', proveConstraint qr') of
                                         -- NOTE: remove provable Constraints to keep those smaller.
                                         (Just Dict, Just Dict) -> TermVT $
-                                               Term @_ @_ @_ @_ @(_ #> _) (noConstraintLen (lenVars tr')) (ta' ~> tr') $
+                                               Term (noConstraintLen (lenVars tr')) (ta' ~> tr') $
                                                TeSym $ \c -> lam $ \arg -> res (arg `CtxTeS` c)
                                         (Just Dict, Nothing) -> TermVT $
-                                               Term @_ @_ @_ @_ @(_ #> _) qr' (ta' ~> tr') $
+                                               Term qr' (ta' ~> tr') $
                                                TeSym $ \c -> lam $ \arg -> res (arg `CtxTeS` c)
                                         (Nothing, Just Dict) -> TermVT $
-                                               Term @_ @_ @_ @_ @(_ #> _) qa' (ta' ~> tr') $
+                                               Term qa' (ta' ~> tr') $
                                                TeSym $ \c -> lam $ \arg -> res (arg `CtxTeS` c)
                                         (Nothing, Nothing) -> TermVT $
-                                               Term @_ @_ @_ @_ @(_ #> _) (qa' # qr') (ta' ~> tr') $
+                                               Term (qa' # qr') (ta' ~> tr') $
                                                TeSym $ \c -> lam $ \arg -> res (arg `CtxTeS` c)
        go ts (Token_Term_Let _src name ast_arg ast_body) = do
                TermVT (Term qa ta (TeSym arg)) <- readTerm n2t ts ast_arg
@@ -75,16 +75,16 @@ readTerm n2t ctxTy ast = do
                                case (proveConstraint qa', proveConstraint qr') of
                                 -- NOTE: remove provable Constraints to keep those smaller.
                                 (Just Dict, Just Dict) -> TermVT $
-                                       Term @_ @_ @_ @_ @(_ #> _) (noConstraintLen (lenVars tr')) tr' $
+                                       Term (noConstraintLen (lenVars tr')) tr' $
                                        TeSym $ \c -> let_ (arg c) $ \a -> res (a `CtxTeS` c)
                                 (Just Dict, Nothing) -> TermVT $
-                                       Term @_ @_ @_ @_ @(_ #> _) qr' tr' $
+                                       Term qr' tr' $
                                        TeSym $ \c -> let_ (arg c) $ \a -> res (a `CtxTeS` c)
                                 (Nothing, Just Dict) -> TermVT $
-                                       Term @_ @_ @_ @_ @(_ #> _) qa' tr' $
+                                       Term qa' tr' $
                                        TeSym $ \c -> let_ (arg c) $ \a -> res (a `CtxTeS` c)
                                 (Nothing, Nothing) -> TermVT $
-                                       Term @_ @_ @_ @_ @(_ #> _) (qa' # qr') tr' $
+                                       Term (qa' # qr') tr' $
                                        TeSym $ \c -> let_ (arg c) $ \a -> res (a `CtxTeS` c)
 
 teVar ::
@@ -93,16 +93,16 @@ teVar ::
  NameTe -> CtxTy src ts -> Either (Error_Term src) (TermVT src ss ts)
 teVar name CtxTyZ = Left $ Error_Term_unknown name
 teVar name (CtxTyS n ty _) | n == name =
-       Right $ TermVT $ Term @_ @_ @_ @_ @(_ #> _) noConstraint ty $
+       Right $ TermVT $ Term noConstraint ty $
                TeSym $ \(te `CtxTeS` _) -> te
 teVar name (CtxTyS _n _typ ts') = do
        TermVT (Term q t (TeSym te)) <- teVar @ss name ts'
-       Right $ TermVT $ Term @_ @_ @_ @_ @(_ #> _) q t $
+       Right $ TermVT $ Term q t $
                TeSym $ \(_ `CtxTeS` ts) -> te ts
 
 teApp ::
  Source src => Constable (->) =>
- Term src ss ts '[Proxy (a::K.Type), Proxy (b::K.Type)] ((a -> b) -> a -> b)
+ Term src ss ts '[Proxy (a::K.Type), Proxy (b::K.Type)] (() #> ((a -> b) -> a -> b))
 teApp =
        Term noConstraint ((a ~> b) ~> a ~> b) $
        TeSym $ const apply
@@ -170,7 +170,7 @@ readTermWithCtxPush1 (n, TermT (Term qn tn (TeSym te_n))) readTe n2t ctxTy ast =
        case proveConstraint qn of
         Nothing -> Left $ Error_Term_proofless $ TypeVT qn
         Just Dict ->
-               Right $ TermVT $ Term @_ @_ @_ @_ @(_ #> _) q t $ TeSym $ \c ->
+               Right $ TermVT $ Term q t $ TeSym $ \c ->
                        let cte = qual qn $ te_n CtxTeZ in
                        te $ cte `CtxTeS` c
 
index 1dc2b8ce7ac24cf9ed0cdb06248270d6287ddf18..3efbc96bfbe1b444c45e24832e2e8a1394470f90 100644 (file)
@@ -19,10 +19,11 @@ import Language.Symantic.Transforming.Trans
 import Language.Symantic.Typing
 
 -- * Type 'Term'
-data Term src ss ts vs (t::K.Type)
- =   Term (Type src vs (QualOf t))
-          (Type src vs (UnQualOf t))
-          (TeSym ss ts t)
+data Term src ss ts vs (t::K.Type) where
+ Term :: Type src vs       q
+      -> Type src vs       t
+      -> TeSym ss ts       (q #> t)
+      -> Term src ss ts vs (q #> t)
 instance Source src => Eq (Term src ss ts vs t) where
        Term qx tx _ == Term qy ty _ = qx == qy && tx == ty
 instance Source src => Show (Term src ss ts vs t) where
@@ -50,6 +51,13 @@ instance AllocVars (Term src ss ts) where
 instance ExpandFam (Term src ss ts vs t) where
        expandFam (Term q t te) = Term (expandFam q) (expandFam t) te
 
+-- Type
+instance Inj_Source (TermT src ss ts vs) src => TypeOf (Term src ss ts vs) where
+       typeOf t = typeOfTerm t `source` TermT t
+
+typeOfTerm :: Source src => Term src ss ts vs t -> Type src vs t
+typeOfTerm (Term q t _) = q #> t
+
 -- ** Type 'TermT'
 -- | 'Term' with existentialized 'Type'.
 data TermT src ss ts vs = forall t. TermT (Term src ss ts vs t)
@@ -61,8 +69,9 @@ instance Source src => Show (TermT src ss ts vs) where
 data TermVT src ss ts = forall vs t. TermVT (Term src ss ts vs t)
 instance Source src => Eq (TermVT src ss ts) where
        TermVT x == TermVT y =
-               let (Term qx' tx' _, Term qy' ty' _) = appendVars x y in
-               isJust $ (qx' #> tx') `eqTypeKi` (qy' #> ty')
+               case appendVars x y of
+                (Term qx' tx' _, Term qy' ty' _) ->
+                       isJust $ (qx' #> tx') `eqTypeKi` (qy' #> ty')
 instance Source src => Show (TermVT src ss ts) where
        showsPrec p (TermVT t) = showsPrec p t
 type instance SourceOf (TermVT src ss ts) = src
@@ -72,7 +81,7 @@ instance Source src => Sourced (TermVT src ss ts) where
 
 liftTermVT :: TermVT src ss '[] -> TermVT src ss ts
 liftTermVT (TermVT (Term q t (TeSym te))) =
-       TermVT $ Term @_ @_ @_ @_ @(_ #> _) q t $
+       TermVT $ Term q t $
        TeSym $ \_c -> te CtxTeZ
 
 -- ** Type 'TermAVT'
@@ -84,8 +93,9 @@ instance Source src => Sourced (TermAVT src ss) where
        setSource (TermAVT t) src = TermAVT (setSource t src)
 instance Source src => Eq (TermAVT src ss) where
        TermAVT x == TermAVT y =
-               let (Term qx' tx' _, Term qy' ty' _) = appendVars x y in
-               isJust $ (qx' #> tx') `eqTypeKi` (qy' #> ty')
+               case appendVars x y of
+                (Term qx' tx' _, Term qy' ty' _) ->
+                       isJust $ (qx' #> tx') `eqTypeKi` (qy' #> ty')
 instance Source src => Show (TermAVT src ss) where
        showsPrec p (TermAVT t) = showsPrec p t
 
index 08a90ea599e2447d39853590dacfdc3e9e519d42..f33e6bcd94d4d28c651ef22093f2d60ee31d88fa 100644 (file)
@@ -806,3 +806,7 @@ foldlTys ::
  Types src vs ts -> acc -> acc
 foldlTys _f TypesZ acc = acc
 foldlTys f (TypesS t ts) acc = foldlTys f ts (f t acc)
+
+-- * Class 'TypeOf'
+class TypeOf a where
+       typeOf :: a t -> Type (SourceOf (a t)) (VarsOf (a t)) t