Type.hs revision caf9cbd08ac84499a343bbd0eac79e9bb47a40e5
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskimodule Type where
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiimport List (isPrefixOf)
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiimport Lexer (signChars, caslLetters)
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski-- ----------------------------------------------
601dc92e4c128d23a726593357c654fb776a63a7Till Mossakowski-- we want to have (at least some builtin) type constructors
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski-- for uniformity/generalization sorts get type "Sort"
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski-- "Sort -> Sort" would be the type/kind of a type constructor
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski-- ----------------------------------------------
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskidata Type = Type { typeConst :: Id, typeArgs :: [Type] } -- [Pos] ?
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski | PartialType { partialTypeId :: Id } -- for partial constants
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski deriving (Eq, Ord)
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiinstance Show Type where
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski showsPrec _ = showType False -- without parenthesis
047de69319a752b9c467166b1264f9e121459e2dTill MossakowskipartialSuffix = "?"
047de69319a752b9c467166b1264f9e121459e2dTill MossakowskitotalSuffix = "!" -- for total lambda
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski-- same predefined type constructors
047de69319a752b9c467166b1264f9e121459e2dTill MossakowskitotalFunArrow = "->"
047de69319a752b9c467166b1264f9e121459e2dTill MossakowskipartialFunArrow = totalFunArrow ++ partialSuffix
047de69319a752b9c467166b1264f9e121459e2dTill MossakowskiproductSign = "*"
047de69319a752b9c467166b1264f9e121459e2dTill MossakowskialtProductSign = "\215"
047de69319a752b9c467166b1264f9e121459e2dTill MossakowskisimpleTok :: String -> Token
047de69319a752b9c467166b1264f9e121459e2dTill MossakowskisimpleTok s = Token s nullPos
047de69319a752b9c467166b1264f9e121459e2dTill MossakowskisimpleId :: String -> Id
047de69319a752b9c467166b1264f9e121459e2dTill MossakowskisimpleId(s) = Id [simpleTok s] [] []
da955132262baab309a50fdffe228c9efe68251dCui JianisSign c = c `elem` signChars
047de69319a752b9c467166b1264f9e121459e2dTill MossakowskiisAlpha c = c `elem` ['0'..'9'] ++ "'" ++ caslLetters
047de69319a752b9c467166b1264f9e121459e2dTill MossakowskishowSign i "" = show i
da955132262baab309a50fdffe228c9efe68251dCui JianshowSign i s = let r = show i in
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski if not (null r) && (isSign (last r) && isSign (head s)
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski || isAlpha (last r) && isAlpha (head s)
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski || r == "=" && "e=" `isPrefixOf` s)
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski then r ++ " " ++ s else r ++ s
da955132262baab309a50fdffe228c9efe68251dCui JianshowSignStr s = showSign (simpleId s)
047de69319a752b9c467166b1264f9e121459e2dTill MossakowskishowType :: Bool -> Type -> ShowS
047de69319a752b9c467166b1264f9e121459e2dTill MossakowskishowType _ (PartialType i) = showSignStr partialSuffix . showSign i
da955132262baab309a50fdffe228c9efe68251dCui JianshowType _ Sort = showString "!SORT!" -- should not be shown
047de69319a752b9c467166b1264f9e121459e2dTill MossakowskishowType _ t@(Type i []) = if isProduct t then showString "()" else showSign i
047de69319a752b9c467166b1264f9e121459e2dTill MossakowskishowType b t@(Type i (x:r)) = showParen b
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski (if isFunType t
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski then if isPredicate t then showType False x
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski else showType (isFunType x) x . showSign i . shows (head r)
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski else if isProduct t
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski then let f x = showType (isFunType x || isProduct x) x
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski in showSepList (showSign i) f (x:r)
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski else shows i . showSepList (showChar ' ') shows (x:r)
047de69319a752b9c467166b1264f9e121459e2dTill MossakowskiasType s = Type s []
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski-- ----------------------------------------------
da955132262baab309a50fdffe228c9efe68251dCui Jian-- builtin type
da955132262baab309a50fdffe228c9efe68251dCui JianinternalBool = crossProduct [] -- unit
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski-- function types, product type and the internal bool for predicates
da955132262baab309a50fdffe228c9efe68251dCui JiantotalFun :: (Type, Type) -> Type
da955132262baab309a50fdffe228c9efe68251dCui JiantotalFun(t1,t2) = Type (simpleId totalFunArrow) [t1,t2]
047de69319a752b9c467166b1264f9e121459e2dTill MossakowskipartialFun(t1,t2) = Type (simpleId partialFunArrow) [t1,t2]
da955132262baab309a50fdffe228c9efe68251dCui Jianpredicate t = totalFun(t, internalBool)
047de69319a752b9c467166b1264f9e121459e2dTill MossakowskiisFunType(Type s [_, _]) = show s == totalFunArrow || show s == partialFunArrow
047de69319a752b9c467166b1264f9e121459e2dTill MossakowskiisFunType _ = False
047de69319a752b9c467166b1264f9e121459e2dTill MossakowskiisPartialFunType(Type s [_, _]) = show s == partialFunArrow
047de69319a752b9c467166b1264f9e121459e2dTill MossakowskiisPartialFunType _ = False
047de69319a752b9c467166b1264f9e121459e2dTill MossakowskiargType(Type _ [t, _]) = t
047de69319a752b9c467166b1264f9e121459e2dTill MossakowskiresType(Type _ [_, t]) = t
047de69319a752b9c467166b1264f9e121459e2dTill MossakowskiisPredicate t = isFunType t && (resType(t) == internalBool)
047de69319a752b9c467166b1264f9e121459e2dTill MossakowskicrossProduct = Type (simpleId productSign)
047de69319a752b9c467166b1264f9e121459e2dTill MossakowskiisProduct(Type s _) = show s == productSign || show s == altProductSign
047de69319a752b9c467166b1264f9e121459e2dTill MossakowskiisPoduct _ = False
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski-- test if a type is first-order
047de69319a752b9c467166b1264f9e121459e2dTill MossakowskiisBaseType (Type _ l) = case l of {[] -> True ; _ -> False}
da955132262baab309a50fdffe228c9efe68251dCui JianisBaseType Sort = False -- not the type of a proper function
da955132262baab309a50fdffe228c9efe68251dCui Jian-- first order types are products with 0, 1 or more arguments
047de69319a752b9c467166b1264f9e121459e2dTill MossakowskiisFOArgType(t) = isProduct t &&
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski case t of { Type _ l -> all isBaseType l }
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski-- constants are functions with the empty product as argument