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