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