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
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
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
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
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
-- ** '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_
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
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
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
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
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'
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'
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
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
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
tyUnit = tyConst @(K ()) @()
-- ** 'Term's
-teUnit ::
- Source src => Inj_Sym ss () =>
- Term src ss ts '[] ()
+teUnit :: TermDef () '[] (() #> ())
teUnit = Term noConstraint tyUnit $ teSym @() $ unit
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)
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
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 ::
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
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
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
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)
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
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'
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
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