never executed always true always false
1
2 module Conjure.Language.Expression.Op.Internal.Common
3 ( module X
4
5 , SimplifyOp(..)
6 , BinaryOperator(..)
7
8 , prettyPrecBinOp
9 , Fixity(..), operators, functionals
10 , overloadedFunctionals
11 , quantifiers
12 , EssenceOperatorParsingDescr(..)
13
14 , raiseTypeError
15
16 , intToInt
17 , intToIntToInt
18 , intToIntToIntStrict
19 , boolToBoolToBool
20 , sameToSameToBool
21 , sameToSameToSame
22 ) where
23
24 -- conjure
25 import Conjure.Prelude
26 import Conjure.Bug
27 import Conjure.Language.Name as X
28 import Conjure.Language.AbstractLiteral as X
29 import Conjure.Language.Constant as X
30 import Conjure.Language.Type as X
31 import Conjure.Language.Domain as X
32 import Conjure.Language.TypeOf as X
33 import Conjure.Language.Pretty as X
34 import Conjure.Language.AdHoc as X
35 import Conjure.Language.Lexemes as X (lexemeFaceDoc)
36 import Conjure.Language.Lexer as X ( Lexeme(..), textToLexeme )
37
38
39 class SimplifyOp op x where
40 simplifyOp ::
41 MonadFailDoc m =>
42 Eq x =>
43 Num x =>
44 ExpressionLike x =>
45 op x -> -- the input
46 m x -- the simplified output (or failure if it cannot be simplified)
47
48 class BinaryOperator op where
49 opLexeme :: proxy op -> Lexeme
50
51 -- | just the operator not the arguments
52 opPretty :: BinaryOperator op => proxy op -> Doc
53 opPretty = lexemeFaceDoc . opLexeme
54
55 opFixityPrec :: BinaryOperator op => proxy op -> (Fixity, Int)
56 opFixityPrec op =
57 case [ (f,p) | (BinaryOp l f, p) <- operators, l == opLexeme op ] of
58 [x] -> x
59 _ -> bug "opFixityPrec"
60
61 prettyPrecBinOp :: (BinaryOperator op, Pretty x) => Int -> proxy op -> x -> x -> Doc
62 prettyPrecBinOp envPrec op a b =
63 let
64 (fixity, prec) = opFixityPrec op
65 in
66 case fixity of
67 FLeft -> parensIf (envPrec > prec) $ fsep [ prettyPrec prec a
68 , opPretty op
69 , prettyPrec (prec+1) b
70 ]
71 FNone -> parensIf (envPrec > prec) $ fsep [ prettyPrec (prec+1) a
72 , opPretty op
73 , prettyPrec (prec+1) b
74 ]
75 FRight -> parensIf (envPrec > prec) $ fsep [ prettyPrec (prec+1) a
76 , opPretty op
77 , prettyPrec prec b
78 ]
79
80 intToInt :: (MonadFailDoc m, TypeOf a, Pretty p, ?typeCheckerMode :: TypeCheckerMode) => p -> a -> m Type
81 intToInt p a = do
82 tya <- typeOf a
83 case tya of
84 TypeInt t -> return (TypeInt t)
85 _ -> failDoc $ vcat
86 [ "When type checking:" <+> pretty p
87 , "Argument expected to be an int, but it is:" <++> pretty tya
88 ]
89
90
91 intToIntToInt :: (MonadFailDoc m, TypeOf a, Pretty p, ?typeCheckerMode :: TypeCheckerMode) => p -> a -> a -> m Type
92 intToIntToInt p a b = do
93 tya <- typeOf a
94 tyb <- typeOf b
95 case (tya, tyb) of
96 (TypeInt{}, TypeInt{}) ->
97 if typeUnify tya tyb
98 then return $ mostDefined [tya, tyb]
99 else failDoc $ vcat
100 [ "When type checking:" <+> pretty p
101 , "Types do not unify:" <++> pretty tya
102 ]
103 (_, TypeInt{}) -> failDoc $ vcat
104 [ "When type checking:" <+> pretty p
105 , "First argument expected to be an int, but it is:" <++> pretty tya
106 ]
107 _ -> failDoc $ vcat
108 [ "When type checking:" <+> pretty p
109 , "Second argument expected to be an int, but it is:" <++> pretty tyb
110 ]
111
112 intToIntToIntStrict :: (MonadFailDoc m, TypeOf a, Pretty p, ?typeCheckerMode :: TypeCheckerMode) => p -> a -> a -> m Type
113 intToIntToIntStrict p a b = do
114 tya <- typeOf a
115 tyb <- typeOf b
116 case (tya, tyb) of
117 (TypeInt TagInt, TypeInt TagInt) ->
118 if typeUnify tya tyb
119 then return $ mostDefined [tya, tyb]
120 else failDoc $ vcat
121 [ "When type checking:" <+> pretty p
122 , "Types do not unify:" <++> pretty tya
123 ]
124 (TypeInt TaggedInt{}, TypeInt TaggedInt{}) ->
125 if typeUnify tya tyb
126 then return $ mostDefined [tya, tyb]
127 else failDoc $ vcat
128 [ "When type checking:" <+> pretty p
129 , "Types do not unify:" <++> pretty tya
130 ]
131 (_, TypeInt{}) -> failDoc $ vcat
132 [ "When type checking:" <+> pretty p
133 , "First argument expected to be an int, but it is:" <++> pretty tya
134 ]
135 _ -> failDoc $ vcat
136 [ "When type checking:" <+> pretty p
137 , "Second argument expected to be an int, but it is:" <++> pretty tyb
138 ]
139
140
141
142 boolToBoolToBool :: (MonadFailDoc m, TypeOf a, Pretty p, ?typeCheckerMode :: TypeCheckerMode) => p -> a -> a -> m Type
143 boolToBoolToBool p a b = do
144 tya <- typeOf a
145 tyb <- typeOf b
146 case (tya, tyb) of
147 (TypeBool, TypeBool) -> return TypeBool
148 (_, TypeBool) -> failDoc $ vcat
149 [ "When type checking:" <+> pretty p
150 , "First argument expected to be a bool, but it is:" <++> pretty tya
151 ]
152 _ -> failDoc $ vcat
153 [ "When type checking:" <+> pretty p
154 , "Second argument expected to be a bool, but it is:" <++> pretty tyb
155 ]
156
157
158 -- if acceptableTypes is null, use checkType
159 -- if acceptableTypes is not null, either one of these is true or checkType
160 sameToSameToBool
161 :: ( MonadFailDoc m, ?typeCheckerMode :: TypeCheckerMode
162 , TypeOf a, Pretty a, Pretty p
163 ) => p -> a -> a -> [Type] -> (Type -> Bool) -> m Type
164 sameToSameToBool p a b acceptableTypes checkType = do
165 tyA <- typeOf a
166 tyB <- typeOf b
167 let tyAB = mostDefined [tyA,tyB]
168 let allowed = if null acceptableTypes
169 then checkType tyAB
170 else checkType tyAB || any (typeUnify tyAB) acceptableTypes
171 case (tyA `typeUnify` tyB, allowed) of
172 (True, True) -> return TypeBool
173 (False, _) -> failDoc $ vcat
174 [ "When type checking:" <+> pretty p
175 , "Cannot unify the types of the following."
176 , "lhs :" <+> pretty a
177 , "type of lhs:" <+> pretty tyA
178 , "rhs :" <+> pretty b
179 , "type of rhs:" <+> pretty tyB
180 ]
181 (_, False) -> failDoc $ vcat
182 [ "When type checking:" <+> pretty p
183 , "Arguments have unsupported types."
184 , "lhs :" <+> pretty a
185 , "type of lhs:" <+> pretty tyA
186 , "rhs :" <+> pretty b
187 , "type of rhs:" <+> pretty tyB
188 ]
189
190 -- See sameToSameToBool
191 sameToSameToSame
192 :: ( MonadFailDoc m
193 , ?typeCheckerMode :: TypeCheckerMode
194 , TypeOf a, Pretty a, Pretty p
195 ) => p -> a -> a -> [Type] -> (Type -> Bool) -> m Type
196 sameToSameToSame p a b acceptableTypes checkType = do
197 tyA <- typeOf a
198 tyB <- typeOf b
199 let tyAB = mostDefined [tyA,tyB]
200 let allowed = if null acceptableTypes
201 then checkType tyAB
202 else checkType tyAB || any (typeUnify tyAB) acceptableTypes
203 case (tyA `typeUnify` tyB, allowed) of
204 (True, True) -> return tyAB
205 (False, _) -> failDoc $ vcat
206 [ "When type checking:" <+> pretty p
207 , "Cannot unify the types of the following."
208 , "lhs :" <+> pretty a
209 , "type of lhs:" <+> pretty tyA
210 , "rhs :" <+> pretty b
211 , "type of rhs:" <+> pretty tyB
212 ]
213 (_, False) -> failDoc $ vcat
214 [ "When type checking:" <+> pretty p
215 , "Arguments have unsupported types."
216 , "lhs :" <+> pretty a
217 , "type of lhs:" <+> pretty tyA
218 , "rhs :" <+> pretty b
219 , "type of rhs:" <+> pretty tyB
220 ]
221
222
223 data Fixity = FNone | FLeft | FRight
224 deriving Show
225
226 data EssenceOperatorParsingDescr = BinaryOp Lexeme Fixity | UnaryPrefix Lexeme
227
228 operators :: [(EssenceOperatorParsingDescr, Int)]
229 operators =
230 [ ( BinaryOp L_Plus FLeft , 600 )
231 , ( BinaryOp L_Minus FLeft , 600 )
232 , ( BinaryOp L_Times FLeft , 700 )
233 , ( BinaryOp L_Div FLeft , 700 )
234 , ( BinaryOp L_Mod FLeft , 700 )
235 , ( BinaryOp L_Pow FRight , 2001 )
236 , ( BinaryOp L_Lt FNone , 400 )
237 , ( BinaryOp L_Leq FNone , 400 )
238 , ( BinaryOp L_Gt FNone , 400 )
239 , ( BinaryOp L_Geq FNone , 400 )
240 , ( BinaryOp L_Neq FNone , 400 )
241 , ( BinaryOp L_Eq FNone , 400 )
242 , ( BinaryOp L_Or FLeft , 110 )
243 , ( BinaryOp L_And FLeft , 120 )
244 , ( BinaryOp L_Imply FNone , 50 )
245 , ( BinaryOp L_Iff FNone , 50 )
246 , ( BinaryOp L_union FLeft , 600 )
247 , ( BinaryOp L_intersect FLeft , 700 )
248 , ( BinaryOp L_subset FNone , 400 )
249 , ( BinaryOp L_subsetEq FNone , 400 )
250 , ( BinaryOp L_supset FNone , 400 )
251 , ( BinaryOp L_supsetEq FNone , 400 )
252 , ( BinaryOp L_subsequence FNone , 400 )
253 , ( BinaryOp L_substring FNone , 400 )
254 , ( BinaryOp L_in FNone , 550 )
255 , ( BinaryOp L_HasRepr FNone , 10 )
256 , ( BinaryOp L_HasType FNone , 10 )
257 , ( BinaryOp L_HasDomain FNone , 10 )
258 , ( BinaryOp L_LexLt FNone , 400 )
259 , ( BinaryOp L_LexLeq FNone , 400 )
260 , ( BinaryOp L_LexGt FNone , 400 )
261 , ( BinaryOp L_LexGeq FNone , 400 )
262 , ( BinaryOp L_DotLt FNone , 400 )
263 , ( BinaryOp L_DotLeq FNone , 400 )
264 , ( BinaryOp L_DotGt FNone , 400 )
265 , ( BinaryOp L_DotGeq FNone , 400 )
266 , ( BinaryOp L_TildeLt FNone , 400 )
267 , ( BinaryOp L_TildeLeq FNone , 400 )
268 , ( BinaryOp L_TildeGt FNone , 400 )
269 , ( BinaryOp L_TildeGeq FNone , 400 )
270 , ( UnaryPrefix L_Minus , 2000 )
271 , ( UnaryPrefix L_ExclamationMark , 2000 )
272 ]
273 --Functional operators that clash with other constructs so require no spaces
274 overloadedFunctionals :: [Lexeme]
275 overloadedFunctionals = [
276 L_true,
277 L_Sum,
278 L_Product
279 ]
280
281 functionals :: [Lexeme]
282 functionals =
283 [ L_toInt
284 , L_makeTable
285 , L_table
286 , L_min
287 , L_max
288 , L_allDiff
289 , L_alldifferent_except
290 , L_compose
291 , L_gcc
292 , L_elementId
293 , L_atleast
294 , L_atmost
295 , L_catchUndef
296 , L_quickPermutationOrder
297 , L_dontCare
298 , L_hist
299 , L_factorial
300
301 , L_toSet
302 , L_toMSet
303 , L_toRelation
304 , L_defined
305 , L_range
306 , L_restrict
307 , L_image
308 , L_imageSet
309 , L_preImage
310 , L_inverse
311 , L_together
312 , L_apart
313 , L_party
314 , L_permInverse
315 , L_participants
316 , L_parts
317 , L_image
318 , L_freq
319 , L_toInt
320 , L_flatten
321 , L_concatenate
322 , L_normIndices
323 , L_indices
324 , L_inverse
325
326 , L_transform
327 , L_true
328
329 , L_fAnd
330 , L_fOr
331 , L_Sum
332 , L_Product
333 , L_fXor
334
335 , L_active
336
337 , L_pred
338 , L_succ
339
340 , L_powerSet
341
342 ]
343
344 quantifiers :: [Lexeme]
345 quantifiers = [
346 L_ForAll,
347 L_Exists,
348 L_Product,
349 L_Sum
350 ]
351
352 raiseTypeError :: MonadFailDoc m => Pretty a => a -> m b
353 raiseTypeError p = failDoc ("Type error in" <+> pretty p)