never executed always true always false
1 {-# LANGUAGE DeriveGeneric, DeriveDataTypeable #-}
2
3 module Conjure.Language.Type
4 ( Type(..)
5 , IntTag(..), reTag
6 , TypeCheckerMode(..)
7 , typeUnify
8 , typesUnify
9 , mostDefined
10 , homoType
11 , matrixNumDims
12 , innerTypeOf
13 , isPrimitiveType
14 , typeCanIndexMatrix
15 , morphing
16 , containsTypeFunctorially
17 , containsProductType
18 , containsType
19 ) where
20
21 -- conjure
22 import Conjure.Prelude
23 import Conjure.Bug
24 import Conjure.Language.Name
25 import Conjure.Language.Pretty
26
27
28 data Type
29 = TypeAny
30 | TypeBool
31 | TypeInt IntTag
32 | TypeEnum Name
33 | TypeUnnamed Name
34 | TypeTuple [Type]
35 | TypeRecord [(Name, Type)]
36 | TypeRecordMember Name [(Name, Type)]
37 | TypeVariant [(Name, Type)]
38 | TypeVariantMember Name [(Name, Type)]
39 | TypeList Type
40 | TypeMatrix Type Type
41 | TypeSet Type
42 | TypeMSet Type
43 | TypeFunction Type Type
44 | TypeSequence Type
45 | TypeRelation [Type]
46 | TypePartition Type
47 deriving (Eq, Ord, Show, Data, Typeable, Generic)
48
49
50 instance Serialize Type
51 instance Hashable Type
52 instance ToJSON Type where toJSON = genericToJSON jsonOptions
53 instance FromJSON Type where parseJSON = genericParseJSON jsonOptions
54
55 instance Pretty Type where
56 pretty TypeAny = "?"
57 pretty TypeBool = "bool"
58 pretty (TypeInt (TagEnum n)) = pretty n
59 pretty (TypeInt (TagUnnamed n)) = pretty n
60 pretty TypeInt{} = "int"
61 pretty (TypeEnum nm ) = pretty nm
62 pretty (TypeUnnamed nm) = pretty nm
63 pretty (TypeTuple xs) = (if length xs <= 1 then "tuple" else prEmpty)
64 <> prettyList prParens "," xs
65 pretty (TypeRecord xs) = "record" <+> prettyList prBraces ","
66 [ pretty nm <+> ":" <+> pretty ty | (nm, ty) <- xs ]
67 pretty (TypeRecordMember n ts) = "member" <+> pretty n <+> "of" <+> pretty (TypeRecord ts)
68 pretty (TypeVariant xs) = "variant" <+> prettyList prBraces ","
69 [ pretty nm <+> ":" <+> pretty ty | (nm, ty) <- xs ]
70 pretty (TypeVariantMember n ts) = "member" <+> pretty n <+> "of" <+> pretty (TypeVariant ts)
71 pretty (TypeList x) = prBrackets (pretty x)
72 pretty (TypeMatrix index innerNested)
73 = "matrix indexed by" <+> prettyList prBrackets "," indices
74 <+> "of" <+> pretty inner
75 where
76 (indices,inner) = first (index:) $ collect innerNested
77 collect (TypeMatrix i j) = first (i:) $ collect j
78 collect x = ([],x)
79 pretty (TypeSet x) = "set of" <+> pretty x
80 pretty (TypeMSet x) = "mset of" <+> pretty x
81 pretty (TypeFunction fr to) = "function" <+> pretty fr <+> "-->" <+> pretty to
82 pretty (TypeSequence x) = "sequence of" <+> pretty x
83 pretty (TypePartition x) = "partition from" <+> pretty x
84 pretty (TypeRelation xs) = "relation of" <+> prettyList prParens " *" xs
85
86
87 data IntTag = TagInt -- was an integer in the input
88 | TagEnum Text -- was an enum in the input
89 | TagUnnamed Text -- was an unnamed in the input
90 deriving (Eq, Ord, Show, Data, Typeable, Generic)
91
92 instance Serialize IntTag
93 instance Hashable IntTag
94 instance ToJSON IntTag where toJSON = genericToJSON jsonOptions
95 instance FromJSON IntTag where parseJSON = genericParseJSON jsonOptions
96
97 reTag :: Data a => IntTag -> a -> a
98 reTag t = transformBi (const t)
99
100
101 -- This parameter will decide the mode of the type checker.
102 -- There are two modes: StronglyTyped and RelaxedIntegerTags.
103 -- StronglyTyped is used for user input.
104 -- RelaxedIntegerTags is for internal use only and it ignores the integer tags during type checking.
105
106 data TypeCheckerMode = StronglyTyped | RelaxedIntegerTags
107 deriving (Eq, Ord, Show, Data, Typeable, Generic)
108
109 instance Serialize TypeCheckerMode
110 instance Hashable TypeCheckerMode
111 instance ToJSON TypeCheckerMode where toJSON = genericToJSON jsonOptions
112 instance FromJSON TypeCheckerMode where parseJSON = genericParseJSON jsonOptions
113
114 instance Pretty TypeCheckerMode where
115 pretty = pretty . show
116
117
118 -- | Check whether two types unify or not.
119 typeUnify :: (?typeCheckerMode :: TypeCheckerMode) => Type -> Type -> Bool
120 typeUnify TypeAny _ = True
121 typeUnify _ TypeAny = True
122 typeUnify TypeBool TypeBool = True
123 typeUnify (TypeInt t1) (TypeInt t2) = case ?typeCheckerMode of
124 StronglyTyped -> t1 == t2
125 RelaxedIntegerTags -> True
126 typeUnify (TypeEnum a) (TypeEnum b) = a == b
127 typeUnify (TypeUnnamed a) (TypeUnnamed b) = a == b
128 typeUnify (TypeTuple [TypeAny]) TypeTuple{} = True
129 typeUnify TypeTuple{} (TypeTuple [TypeAny]) = True
130 typeUnify (TypeTuple as) (TypeTuple bs) = (length as == length bs) && and (zipWith typeUnify as bs)
131 typeUnify (TypeRecord as) (TypeRecord bs)
132 | length as /= length bs = False
133 | otherwise = and [ case lookup n bs of
134 Nothing -> False
135 Just b -> typeUnify a b
136 | (n,a) <- as
137 ]
138 --special cases for when one is an instance
139 -- TODO: Not the best solution so might need looking at
140 typeUnify (TypeVariant as) (TypeVariant [(n,a)])
141 = case lookup n as of
142 Nothing -> False
143 Just b -> typeUnify a b
144 typeUnify (TypeVariant [(n,a)]) (TypeVariant as)
145 = case lookup n as of
146 Nothing -> False
147 Just b -> typeUnify a b
148
149 typeUnify (TypeVariant as) (TypeVariant bs)
150 | length as /= length bs = False
151 | otherwise = and [ case lookup n bs of
152 Nothing -> False
153 Just b -> typeUnify a b
154 | (n,a) <- as
155 ]
156 typeUnify (TypeList a) (TypeList b) = typeUnify a b
157 typeUnify (TypeList a) (TypeMatrix _ b) = typeUnify a b
158 typeUnify (TypeList a) (TypeSequence b) = typeUnify a b
159 typeUnify (TypeMatrix a1 a2) (TypeMatrix b1 b2) = and (zipWith typeUnify [a1,a2] [b1,b2])
160 typeUnify (TypeMatrix _ a) (TypeList b) = typeUnify a b
161 typeUnify (TypeMatrix _ a) (TypeSequence b) = typeUnify a b
162 typeUnify (TypeSequence a) (TypeSequence b) = typeUnify a b
163 typeUnify (TypeSequence a) (TypeList b) = typeUnify a b
164 typeUnify (TypeSequence a) (TypeMatrix _ b) = typeUnify a b
165 typeUnify (TypeSet a) (TypeSet b) = typeUnify a b
166 typeUnify (TypeMSet a) (TypeMSet b) = typeUnify a b
167 typeUnify (TypeFunction a1 a2) (TypeFunction b1 b2) = and (zipWith typeUnify [a1,a2] [b1,b2])
168 typeUnify (TypeRelation [TypeAny]) TypeRelation{} = True -- hack to make sameToSameToBool work
169 typeUnify TypeRelation{} (TypeRelation [TypeAny]) = True
170 typeUnify (TypeRelation as) (TypeRelation bs) = (length as == length bs) && and (zipWith typeUnify as bs)
171 typeUnify (TypePartition a) (TypePartition b) = typeUnify a b
172 typeUnify _ _ = False
173
174 -- | Check whether a given list of types unify with each other or not.
175 typesUnify :: (?typeCheckerMode :: TypeCheckerMode) => [Type] -> Bool
176 typesUnify ts = and [ typeUnify i j | i <- ts, j <- ts ]
177
178 -- | Given a list of types, return "the most defined" one in this list.
179 -- This is to get rid of TypeAny's if there are any.
180 -- Precondition: `typesUnify`
181 mostDefined :: (?typeCheckerMode :: TypeCheckerMode) => [Type] -> Type
182 mostDefined = foldr f TypeAny
183 where
184 f :: Type -> Type -> Type
185 f TypeAny x = x
186 f x TypeAny = x
187 f _ x@TypeBool{} = x
188 f _ x@TypeInt{} = x
189 f _ x@TypeEnum{} = x
190 f _ x@TypeUnnamed{} = x
191 f (TypeTuple [TypeAny]) x = x
192 f x (TypeTuple [TypeAny]) = x
193 f (TypeTuple as) (TypeTuple bs) | length as == length bs = TypeTuple (zipWith f as bs)
194 f (TypeRecord as) (TypeRecord bs)
195 | sort (map fst as) == sort (map fst bs) =
196 TypeRecord [ case lookup n bs of
197 Nothing -> bug "mostDefined.TypeRecord"
198 Just b -> (n, f a b)
199 | (n,a) <- as
200 ]
201 | typeUnify (TypeRecord as) (TypeRecord bs) = TypeAny
202 | otherwise = TypeAny
203 f (TypeVariant as) (TypeVariant bs)
204 | sort (map fst as) == sort (map fst bs) =
205 TypeVariant [ case lookup n bs of
206 Nothing -> bug "mostDefined.TypeVariant"
207 Just b -> (n, f a b)
208 | (n,a) <- as
209 ]
210 | typeUnify (TypeVariant as) (TypeVariant bs) = TypeAny
211 | otherwise = TypeAny
212 f (TypeList a) (TypeList b) = TypeList (f a b)
213 f (TypeMatrix a1 a2) (TypeMatrix b1 b2) = TypeMatrix (f a1 b1) (f a2 b2)
214 f (TypeList a) (TypeMatrix _ b) = TypeList (f a b)
215 f (TypeMatrix _ a) (TypeList b) = TypeList (f a b)
216 f (TypeSet a) (TypeSet b) = TypeSet (f a b)
217 f (TypeMSet a) (TypeMSet b) = TypeMSet (f a b)
218 f (TypeFunction a1 a2) (TypeFunction b1 b2) = TypeFunction (f a1 b1) (f a2 b2)
219 f (TypeSequence a) (TypeSequence b) = TypeSequence (f a b)
220 f (TypeRelation [TypeAny]) x = x
221 f x (TypeRelation [TypeAny]) = x
222 f (TypeRelation as) (TypeRelation bs) | length as == length bs = TypeRelation (zipWith f as bs)
223 f (TypePartition a) (TypePartition b) = TypePartition (f a b)
224 f _ _ = TypeAny
225
226 matrixNumDims :: Type -> Int
227 matrixNumDims (TypeMatrix _ t) = 1 + matrixNumDims t
228 matrixNumDims (TypeList t) = 1 + matrixNumDims t
229 matrixNumDims _ = 0
230
231 homoType ::
232 MonadFailDoc m =>
233 (?typeCheckerMode :: TypeCheckerMode) =>
234 Doc -> [Type] -> m Type
235 homoType msg [] = failDoc $ "empty collection, what's the type?" <++> ("When working on:" <+> msg)
236 homoType msg xs =
237 if typesUnify xs
238 then return (mostDefined xs)
239 else failDoc $ vcat [ "Not uniformly typed:" <+> msg
240 , "Involved types are:" <+> vcat (map pretty xs)
241 ]
242
243 innerTypeOf :: MonadFailDoc m => Type -> m Type
244 innerTypeOf (TypeList t) = return t
245 innerTypeOf (TypeMatrix _ t) = return t
246 innerTypeOf (TypeSet t) = return t
247 innerTypeOf (TypeMSet t) = return t
248 innerTypeOf (TypeFunction a b) = return (TypeTuple [a,b])
249 innerTypeOf (TypeSequence t) = return (TypeTuple [TypeInt TagInt,t])
250 innerTypeOf (TypeRelation ts) = return (TypeTuple ts)
251 innerTypeOf (TypePartition t) = return (TypeSet t)
252 innerTypeOf t = failDoc ("innerTypeOf:" <+> pretty (show t))
253
254 isPrimitiveType :: Type -> Bool
255 isPrimitiveType TypeBool{} = True
256 isPrimitiveType TypeInt{} = True
257 isPrimitiveType (TypeMatrix index inner) = and [isPrimitiveType index, isPrimitiveType inner]
258 isPrimitiveType (TypeList inner) = isPrimitiveType inner
259 isPrimitiveType _ = False
260
261 typeCanIndexMatrix :: Type -> Bool
262 typeCanIndexMatrix TypeBool{} = True
263 typeCanIndexMatrix TypeInt {} = True
264 typeCanIndexMatrix TypeEnum{} = True
265 typeCanIndexMatrix _ = False
266
267 -- ||| Traversals that tell us if a type (of a certain form) is contained in a Type
268 -- This allows us to abort transform early if we can see it will have no effect
269
270 typeComplex :: Type -> Bool
271 typeComplex TypeSequence{} = True
272 typeComplex TypePartition{} = True
273 typeComplex TypeList{} = True
274 typeComplex TypeMatrix{} = True
275 typeComplex _ = False
276
277 containsTypeFunctorially :: (?typeCheckerMode :: TypeCheckerMode) => Type -> Type -> Bool
278 containsTypeFunctorially container containee =
279 if typesUnify [container, containee] || typeComplex containee
280 then False
281 else case innerTypeOf container of
282 Nothing -> False
283 Just so -> unifiesOrContains so containee
284
285
286 containsProductType :: (?typeCheckerMode :: TypeCheckerMode) => Type -> Type -> Bool
287 containsProductType ot@(TypeTuple ts) t =
288 (not $ typesUnify [ot, t]) && (any id ((\x -> unifiesOrContains x t) <$> ts))
289 containsProductType ot@(TypeRecord ts) t =
290 (not $ typesUnify [ot, t]) && (any id ((\x -> unifiesOrContains (snd x) t) <$> ts))
291 containsProductType _ _ = False
292
293
294 -- Is the type
295 containsType :: (?typeCheckerMode :: TypeCheckerMode) => Type -> Type -> Bool
296 containsType container containee = containee `elem` universeBi container
297
298
299 unifiesOrContains :: (?typeCheckerMode :: TypeCheckerMode) => Type -> Type -> Bool
300 unifiesOrContains container containee =
301 typesUnify [container, containee] || containsType container containee
302
303
304 -- as in "this homomorphism is morphing"
305 morphing :: (?typeCheckerMode :: TypeCheckerMode)
306 => (MonadFailDoc m)
307 => Type -> m Type
308 morphing (TypeFunction a _) = return a
309 morphing (TypeSequence a) = return a
310 morphing t = failDoc ("morphing:" <+> pretty (show t))