09249711700a6acbc40a2e337688b434d7aafa28Christian MaederDescription : some utilities for the abstract syntax
76647324ed70f33b95a881b536d883daccf9568dChristian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003-2005
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederStability : experimental
76647324ed70f33b95a881b536d883daccf9568dChristian MaederPortability : portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maederutility functions and computations of meaningful positions for
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder various data types of the abstract syntax
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Set as Set
0a39036fa485579a7b7c81cdd44a412392571927Christian Maederimport qualified Text.ParserCombinators.Parsec as P
d48085f765fca838c1d972d2123601997174583dChristian Maeder-- | the string for the universe type
76647324ed70f33b95a881b536d883daccf9568dChristian MaedertypeUniverseS :: String
d48085f765fca838c1d972d2123601997174583dChristian MaedertypeUniverseS = "Type"
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder-- | the id of the universe type
d48085f765fca838c1d972d2123601997174583dChristian MaederuniverseId :: Id
05ae87b9efa19655024b0b6ac344d250b96567cdChristian MaederuniverseId = stringToId typeUniverseS
d48085f765fca838c1d972d2123601997174583dChristian Maeder-- | the type universe
d48085f765fca838c1d972d2123601997174583dChristian Maederuniverse :: Kind
d48085f765fca838c1d972d2123601997174583dChristian Maederuniverse = ClassKind universeId
a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder-- | the type universe
a39a820684c1974350f46593025e0bb279f41bc6Christian MaederuniverseWithRange :: Range -> Kind
72b9099aeec0762bae4546db3bc4b48721027bf4Christian MaederuniverseWithRange = ClassKind . simpleIdToId . Token typeUniverseS
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder-- | the name for the Unit type
d48085f765fca838c1d972d2123601997174583dChristian MaederunitTypeS :: String
d48085f765fca838c1d972d2123601997174583dChristian MaederunitTypeS = "Unit"
d48085f765fca838c1d972d2123601997174583dChristian Maeder-- | the identifier for the Unit type
d48085f765fca838c1d972d2123601997174583dChristian MaederunitTypeId :: Id
05ae87b9efa19655024b0b6ac344d250b96567cdChristian MaederunitTypeId = stringToId unitTypeS
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder-- | single step beta reduce type abstractions
a716971174535184da7713ed308423e355a4aa66Christian MaederredStep :: Type -> Maybe Type
793945d4ac7c0f22760589c87af8e71427c76118Christian MaederredStep ty = case ty of
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder TypeAppl t1 t2 -> case t1 of
5e5c3fbbf8c22b883d551d83429b9f8d8041f1e0Christian Maeder TypeAbs (TypeArg _ _ _ _ c _ _) b _ -> return $
feab655b0275874012c3cf9859064c177860cc70Christian Maeder foldType mapTypeRec
f2c2b420e386a90d940c758c631d16f12952d2b7Christian Maeder { foldTypeName = \ t _ _ n -> if n == c then t2 else t
f2c2b420e386a90d940c758c631d16f12952d2b7Christian Maeder , foldTypeAbs = \ t v1@(TypeArg _ _ _ _ n _ _) tb p ->
f2c2b420e386a90d940c758c631d16f12952d2b7Christian Maeder if n == c then t else TypeAbs v1 tb p } b
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder ExpandedType _ t -> redStep $ TypeAppl t t2
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder KindedType t _ _ -> redStep $ TypeAppl t t2
a716971174535184da7713ed308423e355a4aa66Christian Maeder r1 <- redStep t1
5e5c3fbbf8c22b883d551d83429b9f8d8041f1e0Christian Maeder redStep $ TypeAppl r1 t2
a716971174535184da7713ed308423e355a4aa66Christian Maeder ExpandedType e t -> fmap (ExpandedType e) $ redStep t
a716971174535184da7713ed308423e355a4aa66Christian Maeder KindedType t k ps -> do
a716971174535184da7713ed308423e355a4aa66Christian Maeder r <- redStep t
a716971174535184da7713ed308423e355a4aa66Christian Maeder return $ KindedType r k ps
5e5c3fbbf8c22b883d551d83429b9f8d8041f1e0Christian Maeder _ -> fail "unreducible"
ee6c748be810b24e3c70ffd74f291c7394e389f5Christian MaederstrippedType :: Type -> Type
ee6c748be810b24e3c70ffd74f291c7394e389f5Christian MaederstrippedType = foldType mapTypeRec
9884c7cef7e5a2c8595d5ef8c7d32b9b44a3fad8Christian Maeder { foldTypeAppl = \ trm f a -> let t = TypeAppl f a in
9884c7cef7e5a2c8595d5ef8c7d32b9b44a3fad8Christian Maeder case redStep trm of
fd2dcd5c071e938c07338fd3a32296819b8a2333Christian Maeder Nothing -> case f of
81d3d451a2543ca1f8ab00c229466c983bb08748Christian Maeder TypeName i _ 0
81d3d451a2543ca1f8ab00c229466c983bb08748Christian Maeder | i == lazyTypeId -> a
81d3d451a2543ca1f8ab00c229466c983bb08748Christian Maeder | isArrow i -> TypeAppl (toFunType PFunArr) a
9884c7cef7e5a2c8595d5ef8c7d32b9b44a3fad8Christian Maeder Just r -> strippedType r
ee6c748be810b24e3c70ffd74f291c7394e389f5Christian Maeder , foldTypeName = \ _ i k v -> TypeName (if v >= 0 then i else typeId) k v
ee6c748be810b24e3c70ffd74f291c7394e389f5Christian Maeder , foldKindedType = \ _ t _ _ -> t
ee6c748be810b24e3c70ffd74f291c7394e389f5Christian Maeder , foldExpandedType = \ _ _ t -> t }
ee6c748be810b24e3c70ffd74f291c7394e389f5Christian MaedereqStrippedType :: Type -> Type -> Bool
ee6c748be810b24e3c70ffd74f291c7394e389f5Christian MaedereqStrippedType t1 t2 = strippedType t1 == strippedType t2
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder-- | get top-level type constructor and its arguments and beta reduce
d48085f765fca838c1d972d2123601997174583dChristian MaedergetTypeAppl :: Type -> (Type, [Type])
793945d4ac7c0f22760589c87af8e71427c76118Christian MaedergetTypeAppl = getTypeApplAux True
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder-- | get top-level type constructor and its arguments and beta reduce if True
793945d4ac7c0f22760589c87af8e71427c76118Christian MaedergetTypeApplAux :: Bool -> Type -> (Type, [Type])
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian MaedergetTypeApplAux b ty = let (t, args) = getTyAppl ty in (t, reverse args) where
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder getTyAppl typ =
a716971174535184da7713ed308423e355a4aa66Christian Maeder TypeAppl t1 t2 -> case redStep typ of
a716971174535184da7713ed308423e355a4aa66Christian Maeder Just r | b -> getTyAppl r
a716971174535184da7713ed308423e355a4aa66Christian Maeder _ -> let (t, args) = getTyAppl t1 in (t, t2 : args)
67a14e04c885a87e4273a300eef60e680531088cChristian Maeder ExpandedType _ te -> let (t, args) = getTyAppl te in case t of
81d3d451a2543ca1f8ab00c229466c983bb08748Christian Maeder TypeName {} -> (t, args)
67a14e04c885a87e4273a300eef60e680531088cChristian Maeder _ -> if null args then (typ, []) else (t, args)
d48085f765fca838c1d972d2123601997174583dChristian Maeder KindedType t _ _ -> getTyAppl t
d48085f765fca838c1d972d2123601997174583dChristian Maeder _ -> (typ, [])
d48085f765fca838c1d972d2123601997174583dChristian Maeder-- | the builtin function arrows
81d3d451a2543ca1f8ab00c229466c983bb08748Christian Maederdata Arrow = FunArr | PFunArr | ContFunArr | PContFunArr deriving (Eq, Ord)
d48085f765fca838c1d972d2123601997174583dChristian Maederinstance Show Arrow where
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder show a = case a of
d48085f765fca838c1d972d2123601997174583dChristian Maeder FunArr -> funS
d48085f765fca838c1d972d2123601997174583dChristian Maeder PFunArr -> pFun
d48085f765fca838c1d972d2123601997174583dChristian Maeder ContFunArr -> contFun
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder PContFunArr -> pContFun
81d3d451a2543ca1f8ab00c229466c983bb08748Christian MaederarrowIdRange :: Range -> Arrow -> Id
81d3d451a2543ca1f8ab00c229466c983bb08748Christian MaederarrowIdRange r a = mkId $ map (`Token` r) [place, show a, place]
d48085f765fca838c1d972d2123601997174583dChristian Maeder-- | construct an infix identifier for a function arrow
d48085f765fca838c1d972d2123601997174583dChristian MaederarrowId :: Arrow -> Id
81d3d451a2543ca1f8ab00c229466c983bb08748Christian MaederarrowId = arrowIdRange nullRange
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder-- | test for a function identifier
d48085f765fca838c1d972d2123601997174583dChristian MaederisArrow :: Id -> Bool
d48085f765fca838c1d972d2123601997174583dChristian MaederisArrow i = isPartialArrow i || elem i (map arrowId [FunArr, ContFunArr])
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder-- | test for a partial function identifier
d48085f765fca838c1d972d2123601997174583dChristian MaederisPartialArrow :: Id -> Bool
d48085f765fca838c1d972d2123601997174583dChristian MaederisPartialArrow i = elem i $ map arrowId [PFunArr, PContFunArr]
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder-- | construct a mixfix product identifier with n places
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian MaederproductId :: Int -> Range -> Id
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian MaederproductId n r = if n > 1 then
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder mkId $ placeTok : concat (replicate (n - 1) [Token prodS r, placeTok])
d48085f765fca838c1d972d2123601997174583dChristian Maeder else error "productId"
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder-- | test for a product identifier
d48085f765fca838c1d972d2123601997174583dChristian MaederisProductId :: Id -> Bool
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian MaederisProductId i = isProductIdWithArgs i 0
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder-- | test for a product identifier
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian MaederisProductIdWithArgs :: Id -> Int -> Bool
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian MaederisProductIdWithArgs (Id ts cs _) m = let n = length ts in
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder null cs && (if m > 1 then m == div (n + 1) 2 else n > 2) && altPlaceProd ts
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder where altPlaceProd l = case l of
d48085f765fca838c1d972d2123601997174583dChristian Maeder t : r -> isPlace t && altProdPlace r
d48085f765fca838c1d972d2123601997174583dChristian Maeder altProdPlace l = case l of
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder t : r -> tokStr t == prodS && altPlaceProd r
3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maeder-- | map a kind and its variance
3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian MaedermapKindV :: (Variance -> Variance) -> (a -> b) -> AnyKind a -> AnyKind b
3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian MaedermapKindV g f k = case k of
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder ClassKind a -> ClassKind $ f a
d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian Maeder FunKind v a b r -> FunKind (g v) (mapKindV g f a) (mapKindV g f b) r
3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maeder-- | map a kind and keep variance the same
3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian MaedermapKind :: (a -> b) -> AnyKind a -> AnyKind b
3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian MaedermapKind = mapKindV id
d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian Maeder-- | ignore variances of raw kinds
6b1153c560b677f9f5da2a60ee8a10de75ff90c5Christian MaedernonVarRawKind :: RawKind -> RawKind
6b1153c560b677f9f5da2a60ee8a10de75ff90c5Christian MaedernonVarRawKind = mapKindV (const NonVar) id
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder-- | compute raw kind (if class ids or no higher kinds)
76647324ed70f33b95a881b536d883daccf9568dChristian MaedertoRaw :: Kind -> RawKind
81946e2b3f6dde6167f48769bd02c7a634736856Christian MaedertoRaw = mapKind $ const ()
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder-- | the type universe as raw kind
76647324ed70f33b95a881b536d883daccf9568dChristian MaederrStar :: RawKind
9a44a07ffc79da9852b6319bd6d9df81efe99809Christian MaederrStar = ClassKind ()
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder-- | the Unit type (name)
76647324ed70f33b95a881b536d883daccf9568dChristian MaederunitType :: Type
e47d29b522739fbf08aac80c6faa447dde113fbcChristian MaederunitType = toType unitTypeId
a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder-- | the Unit type (name)
a39a820684c1974350f46593025e0bb279f41bc6Christian MaederunitTypeWithRange :: Range -> Type
72b9099aeec0762bae4546db3bc4b48721027bf4Christian MaederunitTypeWithRange = toType . simpleIdToId . Token unitTypeS
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder-- | the prefix name for lazy types
d48085f765fca838c1d972d2123601997174583dChristian MaederlazyTypeId :: Id
d48085f765fca838c1d972d2123601997174583dChristian MaederlazyTypeId = mkId [mkSimpleId "?"]
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder-- | the kind of the lazy type constructor
e47d29b522739fbf08aac80c6faa447dde113fbcChristian MaedercoKind :: Kind
e47d29b522739fbf08aac80c6faa447dde113fbcChristian MaedercoKind = FunKind CoVar universe universe nullRange
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder-- | the lazy type constructor
d48085f765fca838c1d972d2123601997174583dChristian MaederlazyTypeConstr :: Type
e47d29b522739fbf08aac80c6faa447dde113fbcChristian MaederlazyTypeConstr = TypeName lazyTypeId (toRaw coKind) 0
d48085f765fca838c1d972d2123601997174583dChristian Maeder-- | make a type lazy
d48085f765fca838c1d972d2123601997174583dChristian MaedermkLazyType :: Type -> Type
72b9099aeec0762bae4546db3bc4b48721027bf4Christian MaedermkLazyType = TypeAppl lazyTypeConstr
d48085f765fca838c1d972d2123601997174583dChristian Maeder-- | function type
d48085f765fca838c1d972d2123601997174583dChristian MaedermkFunArrType :: Type -> Arrow -> Type -> Type
81d3d451a2543ca1f8ab00c229466c983bb08748Christian MaedermkFunArrType = mkFunArrTypeWithRange nullRange
a39a820684c1974350f46593025e0bb279f41bc6Christian MaedermkFunArrTypeWithRange :: Range -> Type -> Arrow -> Type -> Type
81d3d451a2543ca1f8ab00c229466c983bb08748Christian MaedermkFunArrTypeWithRange r t1 a t2 = mkTypeAppl (toFunTypeRange r a) [t1, t2]
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder-- | construct a product type
d48085f765fca838c1d972d2123601997174583dChristian MaedermkProductType :: [Type] -> Type
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian MaedermkProductType ts = mkProductTypeWithRange ts nullRange
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder-- | construct a product type
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian MaedermkProductTypeWithRange :: [Type] -> Range -> Type
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian MaedermkProductTypeWithRange ts r = case ts of
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder [] -> unitType
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder _ -> let n = length ts in
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder mkTypeAppl (toProdType n r) ts
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder-- | convert a type with unbound variables to a scheme
81946e2b3f6dde6167f48769bd02c7a634736856Christian MaedersimpleTypeScheme :: Type -> TypeScheme
81946e2b3f6dde6167f48769bd02c7a634736856Christian MaedersimpleTypeScheme t = TypeScheme [] t nullRange
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder{- | add the unit type as result type or convert a parsed empty tuple
98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maeder to the unit type -}
a39a820684c1974350f46593025e0bb279f41bc6Christian MaederpredType :: Range -> Type -> Type
a39a820684c1974350f46593025e0bb279f41bc6Christian MaederpredType r t = case t of
c9fd6322389afc35c1803a0614f094298bc7cba3Christian Maeder BracketType Parens [] _ -> mkLazyType $ unitTypeWithRange r
a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder _ -> mkFunArrTypeWithRange r t PFunArr $ unitTypeWithRange r
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder-- | change the type of the scheme to a 'predType'
a39a820684c1974350f46593025e0bb279f41bc6Christian MaederpredTypeScheme :: Range -> TypeScheme -> TypeScheme
72b9099aeec0762bae4546db3bc4b48721027bf4Christian MaederpredTypeScheme = mapTypeOfScheme . predType
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder-- | check for and remove predicate arrow
98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian MaederunPredType :: Type -> (Bool, Type)
98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian MaederunPredType t = case getTypeAppl t of
c9fd6322389afc35c1803a0614f094298bc7cba3Christian Maeder (TypeName at _ 0, [ty, TypeName ut (ClassKind _) 0])
c9fd6322389afc35c1803a0614f094298bc7cba3Christian Maeder | ut == unitTypeId && at == arrowId PFunArr -> (True, ty)
c9fd6322389afc35c1803a0614f094298bc7cba3Christian Maeder (TypeName lt _ 0, [TypeName ut (ClassKind _) 0])
c9fd6322389afc35c1803a0614f094298bc7cba3Christian Maeder | ut == unitTypeId && lt == lazyTypeId ->
3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maeder (True, BracketType Parens [] nullRange) -- for printing only
98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maeder _ -> (False, t)
98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maeder-- | test if type is a predicate type
98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian MaederisPredType :: Type -> Bool
98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian MaederisPredType = fst . unPredType
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder-- | remove predicate arrow in a type scheme
98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian MaederunPredTypeScheme :: TypeScheme -> TypeScheme
98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian MaederunPredTypeScheme = mapTypeOfScheme (snd . unPredType)
17889a13fbcd155040fa0323ffe82393d53051fcChristian MaederfunKindWithRange3 :: Range -> Kind -> Kind -> Kind -> Kind
17889a13fbcd155040fa0323ffe82393d53051fcChristian MaederfunKindWithRange3 r a b c = FunKind ContraVar a (FunKind CoVar b c r) r
17889a13fbcd155040fa0323ffe82393d53051fcChristian MaederfunKind3 :: Kind -> Kind -> Kind -> Kind
17889a13fbcd155040fa0323ffe82393d53051fcChristian MaederfunKind3 = funKindWithRange3 nullRange
a39a820684c1974350f46593025e0bb279f41bc6Christian MaederfunKindWithRange :: Range -> Kind
17889a13fbcd155040fa0323ffe82393d53051fcChristian MaederfunKindWithRange r = let c = universeWithRange r in funKindWithRange3 r c c c
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder-- | the kind of the function type
81946e2b3f6dde6167f48769bd02c7a634736856Christian MaederfunKind :: Kind
a39a820684c1974350f46593025e0bb279f41bc6Christian MaederfunKind = funKindWithRange nullRange
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder-- | construct higher order kind from arguments and result kind
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian MaedermkFunKind :: Range -> [(Variance, AnyKind a)] -> AnyKind a -> AnyKind a
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian MaedermkFunKind r args res = foldr ( \ (v, a) k -> FunKind v a k r) res args
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder-- | the 'Kind' of the product type
17889a13fbcd155040fa0323ffe82393d53051fcChristian MaederprodKind1 :: Int -> Range -> Kind -> Kind
17889a13fbcd155040fa0323ffe82393d53051fcChristian MaederprodKind1 n r c =
17889a13fbcd155040fa0323ffe82393d53051fcChristian Maeder if n > 1 then mkFunKind r (replicate n (CoVar, c)) c
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder else error "prodKind"
17889a13fbcd155040fa0323ffe82393d53051fcChristian MaederprodKind :: Int -> Range -> Kind
17889a13fbcd155040fa0323ffe82393d53051fcChristian MaederprodKind n r = prodKind1 n r universe
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder-- | a type name with a universe kind
81946e2b3f6dde6167f48769bd02c7a634736856Christian MaedertoType :: Id -> Type
81946e2b3f6dde6167f48769bd02c7a634736856Christian MaedertoType i = TypeName i rStar 0
81d3d451a2543ca1f8ab00c229466c983bb08748Christian MaedertoFunTypeRange :: Range -> Arrow -> Type
81d3d451a2543ca1f8ab00c229466c983bb08748Christian MaedertoFunTypeRange r a = TypeName (arrowIdRange r a) (toRaw $ funKindWithRange r) 0
e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maeder-- | the type name for a function arrow
e47d29b522739fbf08aac80c6faa447dde113fbcChristian MaedertoFunType :: Arrow -> Type
81d3d451a2543ca1f8ab00c229466c983bb08748Christian MaedertoFunType = toFunTypeRange nullRange
e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maeder-- | the type name for a function arrow
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian MaedertoProdType :: Int -> Range -> Type
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian MaedertoProdType n r = TypeName (productId n r) (toRaw $ prodKind n r) 0
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder-- | the brackets as tokens with positions
81946e2b3f6dde6167f48769bd02c7a634736856Christian MaedermkBracketToken :: BracketKind -> Range -> [Token]
76647324ed70f33b95a881b536d883daccf9568dChristian MaedermkBracketToken k ps =
10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maeder map (flip Token ps) $ (\ (o, c) -> [o, c]) $ getBrackets k
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder-- | construct a tuple from non-singleton lists
81946e2b3f6dde6167f48769bd02c7a634736856Christian MaedermkTupleTerm :: [Term] -> Range -> Term
81946e2b3f6dde6167f48769bd02c7a634736856Christian MaedermkTupleTerm ts ps = if isSingle ts then head ts else TupleTerm ts ps
19f104861f1832b452c9f98e59880d05e865d9bdChristian Maeder-- | try to extract tuple arguments
76647324ed70f33b95a881b536d883daccf9568dChristian MaedergetTupleArgs :: Term -> Maybe [Term]
19f104861f1832b452c9f98e59880d05e865d9bdChristian MaedergetTupleArgs t = case t of
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder TypedTerm trm qt _ _ -> case qt of
19f104861f1832b452c9f98e59880d05e865d9bdChristian Maeder InType -> Nothing
19f104861f1832b452c9f98e59880d05e865d9bdChristian Maeder _ -> getTupleArgs trm
19f104861f1832b452c9f98e59880d05e865d9bdChristian Maeder TupleTerm ts _ -> Just ts
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder{- | decompose an 'ApplTerm' into an application of an operation and a
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder list of arguments -}
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedergetAppl :: Term -> Maybe (Id, TypeScheme, [Term])
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian MaedergetAppl = thrdM reverse . getRevAppl where
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder thrdM :: (c -> c) -> Maybe (a, b, c) -> Maybe (a, b, c)
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder thrdM f = fmap ( \ (a, b, c) -> (a, b, f c))
62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder getRevAppl :: Term -> Maybe (Id, TypeScheme, [Term])
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder getRevAppl t = case t of
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder TypedTerm trm q _ _ -> case q of
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder InType -> Nothing
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder _ -> getRevAppl trm
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian Maeder QualOp _ (PolyId i _ _) sc _ _ _ -> Just (i, sc, [])
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder QualVar (VarDecl v ty _ _) -> Just (v, simpleTypeScheme ty, [])
81d3d451a2543ca1f8ab00c229466c983bb08748Christian Maeder ApplTerm t1 t2 _ -> thrdM (t2 :) $ getRevAppl t1
70a7281955f0c5e8ab0181166731a5c801ed6cc8Ewaryst Schulz-- | split the list of generic variables into values and type variables
70a7281955f0c5e8ab0181166731a5c801ed6cc8Ewaryst SchulzsplitVars :: [GenVarDecl] -> ([VarDecl], [TypeArg])
81d3d451a2543ca1f8ab00c229466c983bb08748Christian MaedersplitVars l = let f x (vs, tvs) =
81d3d451a2543ca1f8ab00c229466c983bb08748Christian Maeder GenVarDecl vd -> (vd : vs, tvs)
81d3d451a2543ca1f8ab00c229466c983bb08748Christian Maeder GenTypeVarDecl tv -> (vs, tv : tvs)
81d3d451a2543ca1f8ab00c229466c983bb08748Christian Maeder in foldr f ([], []) l
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder-- | extract bindings from an analysed pattern
d1012ae182d765c4e6986029d210b9e7b48de205Christian MaederextractVars :: Term -> [VarDecl]
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian MaederextractVars pat = case pat of
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder QualVar vd -> getVd vd
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder ApplTerm p1 p2 _ ->
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder extractVars p1 ++ extractVars p2
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder TupleTerm pats _ -> concatMap extractVars pats
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder TypedTerm p _ _ _ -> extractVars p
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder AsPattern v p2 _ -> getVd v ++ extractVars p2
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder ResolvedMixTerm _ _ pats _ -> concatMap extractVars pats
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder where getVd vd@(VarDecl v _ _ _) = if showId v "" == "_" then [] else [vd]
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder-- | construct term from id
715ffaf874309df081d1e1cd8e05073fc1227729Christian MaedermkOpTerm :: Id -> TypeScheme -> Term
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian MaedermkOpTerm i sc = QualOp Op (PolyId i [] nullRange) sc [] Infer nullRange
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder-- | bind a term
715ffaf874309df081d1e1cd8e05073fc1227729Christian MaedermkForall :: [GenVarDecl] -> Term -> Term
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill MossakowskimkForall vl f = if null vl then f else QuantifiedTerm Universal vl f nullRange
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder-- | construct application with curried arguments
715ffaf874309df081d1e1cd8e05073fc1227729Christian MaedermkApplTerm :: Term -> [Term] -> Term
76647324ed70f33b95a881b536d883daccf9568dChristian MaedermkApplTerm = foldl ( \ t a -> ApplTerm t a nullRange)
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder-- | make function arrow partial after some arguments
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian MaederaddPartiality :: [a] -> Type -> Type
76647324ed70f33b95a881b536d883daccf9568dChristian MaederaddPartiality args t = case args of
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder [] -> mkLazyType t
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder _ : rs -> case getTypeAppl t of
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder (TypeName a _ _, [t1, t2]) | a == arrowId FunArr ->
8134af4b37c4ad27e30d57b6fbfefd0f91ee6d3cChristian Maeder if null rs then case getTypeAppl t2 of
8134af4b37c4ad27e30d57b6fbfefd0f91ee6d3cChristian Maeder (TypeName l _ _, [t3]) | l == lazyTypeId
8134af4b37c4ad27e30d57b6fbfefd0f91ee6d3cChristian Maeder -> mkFunArrType t1 PFunArr t3
8134af4b37c4ad27e30d57b6fbfefd0f91ee6d3cChristian Maeder _ -> mkFunArrType t1 PFunArr t2
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder else mkFunArrType t1 FunArr $ addPartiality rs t2
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder _ -> error "addPartiality"
9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maeder-- | convert a type argument to a type
9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian MaedertypeArgToType :: TypeArg -> Type
81946e2b3f6dde6167f48769bd02c7a634736856Christian MaedertypeArgToType (TypeArg i _ _ rk c _ _) = TypeName i rk c
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder{- | convert a parameterized type identifier with a result raw kind
9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maeder to a type application -}
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederpatToType :: Id -> [TypeArg] -> RawKind -> Type
94b34b35075c9115a22b512fd4ec3fb290f13d59Christian MaederpatToType i args rk =
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder mkTypeAppl (TypeName i (typeArgsListToRawKind args rk) 0)
9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maeder $ map typeArgToType args
9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maeder-- | create the (raw if True) kind from type arguments
76647324ed70f33b95a881b536d883daccf9568dChristian MaedertypeArgsListToRawKind :: [TypeArg] -> RawKind -> RawKind
61e38a4f194d3adc66646326c938eb9263a2f39bChristian MaedertypeArgsListToRawKind tArgs = mkFunKind (getRange tArgs) $
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder map (\ (TypeArg _ v _ rk _ _ _) -> (v, rk)) tArgs
9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maeder-- | create the kind from type arguments
76647324ed70f33b95a881b536d883daccf9568dChristian MaedertypeArgsListToKind :: [TypeArg] -> Kind -> Kind
61e38a4f194d3adc66646326c938eb9263a2f39bChristian MaedertypeArgsListToKind tArgs = mkFunKind (getRange tArgs) $
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder map ( \ (TypeArg _ v ak _ _ _ _) -> (v, toKind ak)) tArgs
9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maeder-- | get the type of a constructor with given curried argument types
d5c415f6373274fed04d83b9322891f3b82e9c26Christian MaedergetFunType :: Type -> Partiality -> [Type] -> Type
d5c415f6373274fed04d83b9322891f3b82e9c26Christian MaedergetFunType rty p ts = (case p of
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder Partial -> addPartiality ts)
81d3d451a2543ca1f8ab00c229466c983bb08748Christian Maeder $ foldr (`mkFunArrType` FunArr) rty ts
9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maeder-- | get the type of a selector given the data type as first arguemnt
9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian MaedergetSelType :: Type -> Partiality -> Type -> Type
72b9099aeec0762bae4546db3bc4b48721027bf4Christian MaedergetSelType dt p = (case p of
9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maeder Partial -> addPartiality [dt]
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder Total -> id) . mkFunArrType dt FunArr
4c3e4edfc4b76a19a0025a8c8aae533ed127f71fChristian Maeder-- | make type argument non-variant
6b1153c560b677f9f5da2a60ee8a10de75ff90c5Christian MaedernonVarTypeArg :: TypeArg -> TypeArg
6b1153c560b677f9f5da2a60ee8a10de75ff90c5Christian MaedernonVarTypeArg (TypeArg i _ vk rk c o p) = TypeArg i NonVar vk rk c o p
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder-- | get the type variable
717686b54b9650402e2ebfbaadf433eab8ba5171Christian MaedergetTypeVar :: TypeArg -> Id
81d3d451a2543ca1f8ab00c229466c983bb08748Christian MaedergetTypeVar (TypeArg v _ _ _ _ _ _) = v
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder-- | construct application left-associative
717686b54b9650402e2ebfbaadf433eab8ba5171Christian MaedermkTypeAppl :: Type -> [Type] -> Type
72b9099aeec0762bae4546db3bc4b48721027bf4Christian MaedermkTypeAppl = foldl TypeAppl
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder-- | get the kind of an analyzed type variable
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedertoKind :: VarKind -> Kind
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedertoKind vk = case vk of
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder VarKind k -> k
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder Downset t -> case t of
72909c6c1cfe9702f5910d0a135c8b55729c7917Christian Maeder KindedType _ k _ | Set.size k == 1 -> Set.findMin k
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder _ -> error "toKind: Downset"
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder MissingKind -> error "toKind: Missing"
0a39036fa485579a7b7c81cdd44a412392571927Christian Maeder-- | try to reparse the pretty printed input as an identifier
0a39036fa485579a7b7c81cdd44a412392571927Christian MaederreparseAsId :: Pretty a => a -> Maybe Id
0a39036fa485579a7b7c81cdd44a412392571927Christian MaederreparseAsId t = case P.parse (opId << P.eof) "" $ showDoc t "" of
0a39036fa485579a7b7c81cdd44a412392571927Christian Maeder Right x -> Just x
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder-- | generate a comparison string
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederexpected :: Pretty a => a -> a -> String
76647324ed70f33b95a881b536d883daccf9568dChristian Maederexpected a b =
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder "\n expected: " ++ showDoc a
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder "\n found: " ++ showDoc b "\n"