never executed always true always false
1 {-# OPTIONS_GHC -fno-warn-orphans #-}
2 {-# LANGUAGE DeriveGeneric, DeriveDataTypeable #-}
3
4 module Conjure.Language.Expression
5 ( Statement(..), SearchOrder(..), Objective(..)
6 , Declaration(..), FindOrGiven(..)
7 , Expression(..), ReferenceTo(..), Region(..), InBubble(..)
8 , AbstractLiteral(..)
9 , AbstractPattern(..)
10 , GeneratorOrCondition(..), Generator(..), generatorPat
11 , e2c
12 , quantifiedVar, quantifiedVarOverDomain, auxiliaryVar
13 , lambdaToFunction
14 , tupleLitIfNeeded
15 , patternToExpr
16 , emptyCollectionX
17 , nbUses
18 , reDomExp
19 , isDomainExpr
20 ) where
21
22 -- conjure
23 import Conjure.Prelude
24 import Conjure.Bug
25 import Conjure.Language.Pretty
26 import Conjure.Language.AdHoc
27
28 import Conjure.Language.Name
29 import Conjure.Language.NameGen ( NameGen(..) )
30 import Conjure.Language.Constant
31 import Conjure.Language.AbstractLiteral
32 import Conjure.Language.Type
33 import Conjure.Language.Domain
34 import Conjure.Language.Expression.Op
35
36 import Conjure.Language.TypeOf
37 import Conjure.Language.RepresentationOf
38
39 -- aeson
40 import qualified Data.Aeson as JSON
41 import qualified Data.Aeson.KeyMap as KM
42
43 import qualified Data.Vector as V -- vector
44
45 -- pretty
46 import Conjure.Language.Pretty as Pr ( cat )
47
48
49 ------------------------------------------------------------------------------------------------------------------------
50 -- Statement -----------------------------------------------------------------------------------------------------------
51 ------------------------------------------------------------------------------------------------------------------------
52
53 data Statement
54 = Declaration Declaration
55 | SearchOrder [SearchOrder]
56 | SearchHeuristic Name
57 | Where [Expression]
58 | Objective Objective Expression
59 | SuchThat [Expression]
60 deriving (Eq, Ord, Show, Data, Typeable, Generic)
61
62 instance Serialize Statement
63 instance Hashable Statement
64 instance ToJSON Statement where toJSON = genericToJSON jsonOptions
65 instance FromJSON Statement where parseJSON = genericParseJSON jsonOptions
66
67 instance SimpleJSON Statement where
68 toSimpleJSON st =
69 case st of
70 Declaration d -> toSimpleJSON d
71 _ -> noToSimpleJSON st
72 fromSimpleJSON = noFromSimpleJSON "Statement"
73
74 instance ToFromMiniZinc Statement where
75 toMiniZinc st =
76 case st of
77 Declaration d -> toMiniZinc d
78 _ -> noToMiniZinc st
79
80 instance Pretty Statement where
81 pretty (Declaration x) = pretty x
82 pretty (SearchOrder nms) = "branching on" <++> prettyList prBrackets "," nms
83 pretty (SearchHeuristic nm) = "heuristic" <+> pretty nm
84 pretty (Where xs) = "where" <++> vcat (punctuate "," $ map pretty xs)
85 pretty (Objective obj x) = pretty obj <++> pretty x
86 pretty (SuchThat xs) = "such that" <++> vcat (punctuate "," $ map pretty xs)
87
88 instance VarSymBreakingDescription Statement where
89 varSymBreakingDescription (Declaration x) = JSON.Object $ KM.fromList
90 [ ("type", JSON.String "Declaration")
91 , ("children", varSymBreakingDescription x)
92 ]
93 varSymBreakingDescription SearchOrder{} = JSON.Null
94 varSymBreakingDescription SearchHeuristic{} = JSON.Null
95 varSymBreakingDescription (Where xs) = JSON.Object $ KM.fromList
96 [ ("type", JSON.String "Where")
97 , ("symmetricChildren", JSON.Bool True)
98 , ("children", JSON.Array $ V.fromList $ map varSymBreakingDescription xs)
99 ]
100 varSymBreakingDescription (Objective obj x) = JSON.Object $ KM.fromList
101 [ ("type", JSON.String $ "Objective-" `mappend` stringToText (show obj))
102 , ("children", varSymBreakingDescription x)
103 ]
104 varSymBreakingDescription (SuchThat xs) = JSON.Object $ KM.fromList
105 [ ("type", JSON.String "SuchThat")
106 , ("symmetricChildren", JSON.Bool True)
107 , ("children", JSON.Array $ V.fromList $ map varSymBreakingDescription xs)
108 ]
109
110
111 ------------------------------------------------------------------------------------------------------------------------
112 -- SearchOrder ---------------------------------------------------------------------------------------------------------
113 ------------------------------------------------------------------------------------------------------------------------
114
115 data SearchOrder = BranchingOn Name | Cut Expression
116 deriving (Eq, Ord, Show, Data, Typeable, Generic)
117
118 instance Serialize SearchOrder
119 instance Hashable SearchOrder
120 instance ToJSON SearchOrder where toJSON = genericToJSON jsonOptions
121 instance FromJSON SearchOrder where parseJSON = genericParseJSON jsonOptions
122
123 instance Pretty SearchOrder where
124 pretty (BranchingOn x) = pretty x
125 pretty (Cut x) = pretty x
126
127
128 ------------------------------------------------------------------------------------------------------------------------
129 -- Objective -----------------------------------------------------------------------------------------------------------
130 ------------------------------------------------------------------------------------------------------------------------
131
132 data Objective = Minimising | Maximising
133 deriving (Eq, Ord, Show, Data, Typeable, Generic)
134
135 instance Serialize Objective
136 instance Hashable Objective
137 instance ToJSON Objective where toJSON = genericToJSON jsonOptions
138 instance FromJSON Objective where parseJSON = genericParseJSON jsonOptions
139
140 instance Pretty Objective where
141 pretty Minimising = "minimising"
142 pretty Maximising = "maximising"
143
144
145 ------------------------------------------------------------------------------------------------------------------------
146 -- Declaration ---------------------------------------------------------------------------------------------------------
147 ------------------------------------------------------------------------------------------------------------------------
148
149 data Declaration
150 = FindOrGiven FindOrGiven Name (Domain () Expression)
151 | Letting Name Expression
152 | GivenDomainDefnEnum Name
153 | LettingDomainDefnEnum Name [Name]
154 | LettingDomainDefnUnnamed Name Expression
155 deriving (Eq, Ord, Show, Data, Typeable, Generic)
156
157 instance Serialize Declaration
158 instance Hashable Declaration
159 instance ToJSON Declaration where toJSON = genericToJSON jsonOptions
160 instance FromJSON Declaration where parseJSON = genericParseJSON jsonOptions
161
162 instance SimpleJSON Declaration where
163 toSimpleJSON d =
164 case d of
165 Letting nm x -> do
166 x' <- toSimpleJSON x
167 return $ JSON.Object $ KM.fromList [(fromString (renderNormal nm), x')]
168 LettingDomainDefnEnum nm xs -> do
169 let xs' = map (fromString . renderNormal) xs
170 return $ JSON.Object $ KM.fromList [(fromString (renderNormal nm), JSON.Array (V.fromList xs'))]
171 _ -> noToSimpleJSON d
172 fromSimpleJSON = noFromSimpleJSON "Declaration"
173
174 instance SimpleJSON Name where
175 toSimpleJSON n =
176 case n of
177 Name nm -> do
178 return $ JSON.String nm
179 _ -> noToSimpleJSON n
180
181 fromSimpleJSON = noFromSimpleJSON "Name"
182
183 instance ToFromMiniZinc Declaration where
184 toMiniZinc st =
185 case st of
186 Letting nm x -> do
187 x' <- toMiniZinc x
188 return $ MZNNamed [(nm, x')]
189 _ -> noToSimpleJSON st
190
191 -- this is only used in the instance below
192 type Prim = Either Bool (Either Integer Constant)
193
194 instance Pretty Declaration where
195 pretty (FindOrGiven forg nm d) = hang (pretty forg <+> pretty nm <> ":" ) 8 (pretty d)
196 pretty (Letting nm (Domain x)) = hang ("letting" <+> pretty nm <+> "be domain") 8 (pretty x)
197 pretty (Letting nm x) =
198 let
199 extract :: Constant -> Maybe [Constant]
200 extract (viewConstantMatrix -> Just (_, rows)) = Just rows
201 extract (viewConstantTuple -> Just rows ) = Just rows
202 extract (viewConstantSet -> Just rows ) = Just rows
203 extract (viewConstantMSet -> Just rows ) = Just rows
204 extract (viewConstantFunction -> Just rows ) = Just (map snd rows)
205 extract (viewConstantSequence -> Just rows ) = Just rows
206 extract _ = Nothing
207
208 isPrim :: Constant -> Maybe Prim
209 isPrim (ConstantBool val) = Just (Left val)
210 isPrim (ConstantInt _ val) = Just (Right (Left val))
211 isPrim val@ConstantEnum{} = Just (Right (Right val))
212 isPrim _ = Nothing
213
214 isPrim1DT :: Constant -> Maybe [Prim]
215 -- isPrim1DT p@(viewConstantMatrix -> Just{}) = isPrim1D p
216 -- isPrim1DT p@(viewConstantTuple -> Just{}) = isPrim1D p
217 -- isPrim1DT p@(viewConstantSet -> Just{}) = isPrim1D p
218 -- isPrim1DT p@(viewConstantMSet -> Just{}) = isPrim1D p
219 -- isPrim1DT p@(viewConstantFunction -> Just{}) = isPrim1D p
220 -- isPrim1DT p@(viewConstantSequence -> Just{}) = isPrim1D p
221 isPrim1DT _ = Nothing
222
223 isPrim1D :: Constant -> Maybe [Prim]
224 isPrim1D (extract -> Just cells) = mapM isPrim cells
225 isPrim1D _ = Nothing
226
227 isPrim2D :: Constant -> Maybe [[Prim]]
228 isPrim2D (extract -> Just rows) = mapM isPrim1D rows
229 isPrim2D (viewConstantRelation -> Just table) = mapM (mapM isPrim) table
230 isPrim2D (viewConstantPartition -> Just table) = mapM (mapM isPrim) table
231 isPrim2D _ = Nothing
232
233 isPrim3D :: Constant -> Maybe [[[Prim]]]
234 isPrim3D (extract -> Just table) = mapM isPrim2D table
235 isPrim3D _ = Nothing
236
237 showPrim :: Int -> Prim -> String
238 showPrim _ (Left True) = "T"
239 showPrim _ (Left False) = "_"
240 showPrim n (Right (Left i)) = padLeft n ' ' (show i)
241 showPrim n (Right (Right i)) = padRight n ' ' (show (pretty i))
242
243 maxIntWidth :: Data a => a -> Int
244 maxIntWidth primTable =
245 maximum (0 : [ length (show i) | i <- universeBi primTable :: [Integer] ]
246 ++ [ length (show (pretty i)) | i@ConstantEnum{} <- universeBi primTable ])
247
248 comment1D :: Int -> [Prim] -> String
249 comment1D width primTable =
250 unlines
251 [ "$ Visualisation for " ++ show (pretty nm)
252 , "$ " ++ unwords [ showPrim width cell | cell <- primTable ]
253 ]
254
255 comment2D :: Int -> [[Prim]] -> String
256 comment2D width primTable =
257 unlines
258 $ ( "$ Visualisation for " ++ show (pretty nm))
259 : [ "$ " ++ unwords [ showPrim width cell | cell <- row ]
260 | row <- primTable ]
261
262 comment3D :: Int -> [[[Prim]]] -> String
263 comment3D width primTable =
264 unlines
265 $ ( "$ Visualisation for " ++ show (pretty nm))
266 : concat [ [ "$ " ++ unwords [ showPrim width cell | cell <- row ]
267 | row <- table
268 ] ++ ["$ "]
269 | table <- primTable ]
270
271 modifierX =
272 case x of
273 Constant c -> modifierC c
274 _ -> id
275
276 modifierC c
277 | Just primTable <- isPrim1DT c
278 , not (null primTable) = \ s ->
279 vcat [s, pretty (comment1D (maxIntWidth primTable) primTable)]
280 modifierC c
281 | Just primTable <- isPrim2D c
282 , not (null (concat primTable)) = \ s ->
283 vcat [s, pretty (comment2D (maxIntWidth primTable) primTable)]
284 modifierC c
285 | Just primTable <- isPrim3D c
286 , not (null (concat (concat primTable))) = \ s ->
287 vcat [s, pretty (comment3D (maxIntWidth primTable) primTable)]
288 modifierC _ = id
289
290 in
291 modifierX $ hang ("letting" <+> pretty nm <+> "be") 8 (pretty x)
292 pretty (GivenDomainDefnEnum name) =
293 hang ("given" <+> pretty name) 8 "new type enum"
294 pretty (LettingDomainDefnEnum name values) =
295 hang ("letting" <+> pretty name <+> "be new type enum") 8
296 (prettyList prBraces "," values)
297 pretty (LettingDomainDefnUnnamed name size) =
298 hang ("letting" <+> pretty name <+> "be new type of size") 8 (pretty size)
299
300 instance VarSymBreakingDescription Declaration where
301 varSymBreakingDescription (FindOrGiven forg name domain) = JSON.Object $ KM.fromList
302 [ ("type", JSON.String "FindOrGiven")
303 , ("forg", toJSON forg)
304 , ("name", toJSON name)
305 , ("domain", toJSON domain)
306 ]
307 varSymBreakingDescription (Letting name x) = JSON.Object $ KM.fromList
308 [ ("type", JSON.String "Letting")
309 , ("name", toJSON name)
310 , ("value", toJSON x)
311 ]
312 varSymBreakingDescription (GivenDomainDefnEnum name) = JSON.Object $ KM.fromList
313 [ ("type", JSON.String "GivenDomainDefnEnum")
314 , ("name", toJSON name)
315 ]
316 varSymBreakingDescription (LettingDomainDefnEnum name xs) = JSON.Object $ KM.fromList
317 [ ("type", JSON.String "GivenDomainDefnEnum")
318 , ("name", toJSON name)
319 , ("values", JSON.Array $ V.fromList $ map toJSON xs)
320 ]
321 varSymBreakingDescription (LettingDomainDefnUnnamed name x) = JSON.Object $ KM.fromList
322 [ ("type", JSON.String "LettingDomainDefnUnnamed")
323 , ("name", toJSON name)
324 , ("value", toJSON x)
325 ]
326
327
328 data FindOrGiven = Find | Given | Quantified
329 | CutFind -- references to variables used in the definition of a cut
330 | LocalFind -- references to variables used inside WithLocals. i.e. auxiliaries.
331 deriving (Eq, Ord, Show, Data, Typeable, Generic)
332
333 instance Serialize FindOrGiven
334 instance Hashable FindOrGiven
335 instance ToJSON FindOrGiven where toJSON = genericToJSON jsonOptions
336 instance FromJSON FindOrGiven where parseJSON = genericParseJSON jsonOptions
337
338 instance Pretty FindOrGiven where
339 pretty Find = "find"
340 pretty Given = "given"
341 pretty Quantified = "quantified"
342 pretty CutFind = "find"
343 pretty LocalFind = "find"
344
345
346 ------------------------------------------------------------------------------------------------------------------------
347 -- Expression ----------------------------------------------------------------------------------------------------------
348 ------------------------------------------------------------------------------------------------------------------------
349
350 data Expression
351 = Constant Constant
352 | AbstractLiteral (AbstractLiteral Expression)
353 | Domain (Domain () Expression)
354 | Reference Name (Maybe ReferenceTo)
355 | WithLocals Expression InBubble
356 | Comprehension Expression [GeneratorOrCondition]
357 | Typed Expression Type
358 | Op (Op Expression)
359 | ExpressionMetaVar String
360 deriving (Eq, Ord, Show, Data, Typeable, Generic)
361
362 instance Serialize Expression
363 instance Hashable Expression
364 instance ToJSON Expression where toJSON = genericToJSON jsonOptions
365 instance FromJSON Expression where parseJSON = genericParseJSON jsonOptions
366
367 instance SimpleJSON Expression where
368 toSimpleJSON x =
369 case x of
370 Reference nm _ -> return $ JSON.String $ stringToText $ show $ pretty nm
371 Constant c -> toSimpleJSON c
372 AbstractLiteral lit -> toSimpleJSON lit
373 Typed y _ -> toSimpleJSON y
374 Op (MkOpNegate (OpNegate a)) -> do
375 a' <- toSimpleJSON a
376 case a' of
377 JSON.Number a'' -> return (JSON.Number (0 - a''))
378 _ -> noToSimpleJSON x
379 Op (MkOpMinus (OpMinus a b)) -> do
380 a' <- toSimpleJSON a
381 b' <- toSimpleJSON b
382 case (a', b') of
383 (JSON.Number a'', JSON.Number b'') -> return (JSON.Number (a'' - b''))
384 _ -> noToSimpleJSON x
385 _ -> noToSimpleJSON x
386 fromSimpleJSON t x = Constant <$> fromSimpleJSON t x
387
388 instance ToFromMiniZinc Expression where
389 toMiniZinc x =
390 case x of
391 Constant c -> toMiniZinc c
392 AbstractLiteral lit -> toMiniZinc lit
393 Typed y _ -> toMiniZinc y
394 Op (MkOpMinus (OpMinus a b)) -> do
395 a' <- toMiniZinc a
396 b' <- toMiniZinc b
397 case (a', b') of
398 (MZNInt a'', MZNInt b'') -> return (MZNInt (a'' - b''))
399 _ -> noToMiniZinc x
400 _ -> noToMiniZinc x
401
402 viewIndexed :: Expression -> (Expression, [Doc])
403 viewIndexed (Op (MkOpIndexing (OpIndexing m i ))) =
404 let this = pretty i
405 in second (++ [this]) (viewIndexed m)
406 viewIndexed (Op (MkOpSlicing (OpSlicing m a b))) =
407 let this = maybe prEmpty pretty a <> ".." <> maybe prEmpty pretty b
408 in second (++ [this]) (viewIndexed m)
409 viewIndexed m = (m, [])
410
411 instance Pretty Expression where
412
413 prettyPrec _ (viewIndexed -> (m,is@(_:_))) = Pr.cat [pretty m, nest 4 (prettyList prBrackets "," is)]
414
415 -- mostly for debugging: print what a reference is pointing at
416 -- prettyPrec _ (Reference x Nothing) = pretty x <> "#`NOTHING`"
417 -- prettyPrec _ (Reference x (Just (DeclHasRepr _ _ dom))) = pretty x <> "#`" <> pretty dom <> "`"
418 -- prettyPrec _ (Reference x (Just r)) = pretty x <> "#`" <> pretty r <> "`"
419
420 prettyPrec _ (Constant x) = pretty x
421 prettyPrec _ (AbstractLiteral x) = pretty x
422 prettyPrec _ (Domain x) = "`" <> pretty x <> "`"
423 prettyPrec _ (Reference x _) = pretty x
424 prettyPrec _ (WithLocals x (AuxiliaryVars locals)) =
425 vcat
426 [ "{" <+> pretty x
427 , "@" <+> vcat (map pretty locals)
428 , "}"
429 ]
430 prettyPrec _ (WithLocals x (DefinednessConstraints locals)) =
431 vcat
432 [ "{" <+> pretty x
433 , "@" <+> pretty (SuchThat locals)
434 , "}"
435 ]
436 prettyPrec _ (Comprehension x is) = prBrackets $ pretty x <++> "|" <+> prettyList id "," is
437 prettyPrec _ (Typed x ty) = prParens $ pretty x <+> ":" <+> "`" <> pretty ty <> "`"
438 prettyPrec prec (Op op) = prettyPrec prec op
439 prettyPrec _ (ExpressionMetaVar x) = "&" <> pretty x
440
441 instance VarSymBreakingDescription Expression where
442 varSymBreakingDescription (Constant x) = toJSON x
443 varSymBreakingDescription (AbstractLiteral x) = varSymBreakingDescription x
444 varSymBreakingDescription (Domain domain) = varSymBreakingDescription domain
445 varSymBreakingDescription (Reference name _) = JSON.Object $ KM.singleton "Reference" (toJSON name)
446 varSymBreakingDescription (WithLocals h (AuxiliaryVars locs)) = JSON.Object $ KM.fromList
447 [ ("type", JSON.String "WithLocals")
448 , ("head", varSymBreakingDescription h)
449 , ("children", JSON.Array $ V.fromList $ map varSymBreakingDescription locs)
450 , ("symmetricChildren", JSON.Bool True)
451 ]
452 varSymBreakingDescription (WithLocals h (DefinednessConstraints locs)) = JSON.Object $ KM.fromList
453 [ ("type", JSON.String "WithLocals")
454 , ("head", varSymBreakingDescription h)
455 , ("children", JSON.Array $ V.fromList $ map varSymBreakingDescription locs)
456 , ("symmetricChildren", JSON.Bool True)
457 ]
458 varSymBreakingDescription (Comprehension h gocs) = JSON.Object $ KM.fromList
459 [ ("type", JSON.String "Comprehension")
460 , ("head", varSymBreakingDescription h)
461 , ("gocs", JSON.Array $ V.fromList $ map varSymBreakingDescription gocs)
462 ]
463 varSymBreakingDescription (Typed x _) = varSymBreakingDescription x
464 varSymBreakingDescription (Op op) = varSymBreakingDescription op
465 varSymBreakingDescription (ExpressionMetaVar s) = JSON.Object $ KM.fromList
466 [ ("type", JSON.String "ExpressionMetaVar")
467 , ("name", JSON.String (stringToText s))
468 ]
469
470 instance TypeOf Expression where
471 typeOf (Constant x) = typeOf x
472 typeOf (AbstractLiteral x) = typeOf x
473 typeOf (Domain x) = failDoc ("Expected an expression, but got a domain:" <++> pretty x)
474 typeOf (Reference nm Nothing) = failDoc ("Type error, identifier not bound:" <+> pretty nm)
475 typeOf (Reference nm (Just refTo)) =
476 case refTo of
477 Alias x -> typeOf x
478 InComprehension gen ->
479 let
480 lu pat ty = maybe
481 (bug $ vcat ["Type error, InComprehension:", pretty nm, pretty pat, pretty ty])
482 return
483 (lu' pat ty)
484 lu' (Single nm') ty | nm == nm' = Just ty
485 lu' (AbsPatTuple pats) (TypeTuple tys) = zipWith lu' pats tys |> catMaybes |> listToMaybe
486 lu' (AbsPatMatrix pats) (TypeMatrix _ ty ) = [lu' p ty | p <- pats] |> catMaybes |> listToMaybe
487 lu' (AbsPatSet pats) (TypeSet ty ) = [lu' p ty | p <- pats] |> catMaybes |> listToMaybe
488 lu' _ _ = Nothing
489 in
490 case gen of
491 GenDomainNoRepr pat domain -> typeOfDomain domain >>= lu pat
492 GenDomainHasRepr pat domain -> typeOfDomain domain >>= lu (Single pat)
493 GenInExpr pat expr ->
494 case project expr of
495 Just (d :: Domain () Expression) -> failDoc $ vcat
496 [ "Expected an expression, but got a domain:" <++> pretty d
497 , "In the generator of a comprehension or a quantified expression"
498 , "Consider using" <+> pretty pat <+> ":" <+> pretty expr
499 ]
500 Nothing -> do
501 tyExpr <- typeOf expr
502 case innerTypeOf tyExpr of
503 Just tyExprInner -> lu pat tyExprInner
504 Nothing -> failDoc $ vcat
505 [ "Type error in the generator of a comprehension or a quantified expression"
506 , "Consider using" <+> pretty pat <+> ":" <+> pretty expr
507 ]
508 DeclNoRepr _ _ dom _ -> typeOfDomain dom
509 DeclHasRepr _ _ dom -> typeOfDomain dom
510 RecordField _ ty -> return ty
511 VariantField _ ty -> return ty
512 typeOf p@(WithLocals h (DefinednessConstraints cs)) = do
513 forM_ cs $ \ c -> do
514 ty <- typeOf c
515 unless (typeUnify TypeBool ty) $ failDoc $ vcat
516 [ "Local constraint is not boolean."
517 , "Condition:" <+> pretty c
518 , "In:" <+> pretty p
519 ]
520 typeOf h
521 typeOf p@(WithLocals h (AuxiliaryVars stmts)) = do
522 forM_ stmts $ \ stmt ->
523 case stmt of
524 Declaration{} -> return () -- TODO: what other checks make sense?
525 SuchThat xs -> forM_ xs $ \ x -> do
526 ty <- typeOf x
527 case ty of
528 TypeBool{} -> return ()
529 _ -> failDoc $ vcat
530 [ "Inside a bubble, in a 'such that' statement:" <++> pretty x
531 , "Expected type `bool`, but got:" <++> pretty ty
532 ]
533 _ -> failDoc $ vcat
534 [ "Unexpected statement inside a bubble."
535 , "Expected type `find` or `such that`, but got:" <++> pretty stmt
536 , "The complete expression:" <+> pretty p
537 ]
538 typeOf h
539 typeOf p@(Comprehension x gensOrConds) = do
540 forM_ gensOrConds $ \case
541 Generator{} -> return ()
542 Condition c -> do
543 ty <- typeOf c
544 unless (typeUnify TypeBool ty) $ failDoc $ vcat
545 [ "Condition is not boolean."
546 , "Condition:" <+> pretty c
547 , "In:" <+> pretty p
548 ]
549 ComprehensionLetting{} -> return ()
550 let generators = [ gen | Generator gen <- gensOrConds ]
551 let conditions = [ cond | cond@Condition{} <- gensOrConds ]
552 case (generators, conditions) of
553 ([GenDomainNoRepr _ indexDom], []) -> do
554 indexTy <- typeOfDomain indexDom
555 if typeCanIndexMatrix indexTy
556 then TypeMatrix indexTy <$> typeOf x
557 else TypeList <$> typeOf x
558 ([GenDomainHasRepr _ indexDom], []) -> do
559 indexTy <- typeOfDomain indexDom
560 if typeCanIndexMatrix indexTy
561 then TypeMatrix indexTy <$> typeOf x
562 else TypeList <$> typeOf x
563 _ -> TypeList <$> typeOf x
564 typeOf (Typed _ ty) = return ty
565 typeOf (Op op) = typeOf op
566 typeOf x@ExpressionMetaVar{} = bug ("typeOf:" <+> pretty x)
567
568 instance RepresentationOf Expression where
569 representationTreeOf (Reference _ (Just (DeclHasRepr _ _ dom))) = return (reprTree dom)
570 representationTreeOf (Op (MkOpIndexing (OpIndexing m i))) = do
571 iType <- typeOf i
572 case iType of
573 TypeBool{} -> return ()
574 TypeInt{} -> return ()
575 _ -> failDoc "representationOf, OpIndexing, not a bool or int index"
576 mTree <- representationTreeOf m
577 case mTree of
578 Tree _ [r] -> return r
579 _ -> failDoc "domainOf, OpIndexing, not a matrix"
580 representationTreeOf _ = failDoc "doesn't seem to have a representation"
581
582 instance Domain () Expression :< Expression where
583 inject = Domain
584 project (Domain x) = return x
585 project (Reference _ (Just (Alias x))) = project x
586 project x = failDoc ("projecting Domain out of Expression:" <+> pretty x)
587
588 instance Op Expression :< Expression where
589 inject = Op
590 project (Op x) = return x
591 project x = failDoc ("projecting Op out of Expression:" <+> pretty x)
592
593 instance Op Constant :< Constant where
594 inject x = bug ("injecting Op into a Constant:" <+> pretty x)
595 project x = failDoc ("projecting Op out of a Constant:" <+> pretty x)
596
597 instance CanBeAnAlias Expression where
598 isAlias (Reference _ (Just (Alias x))) = Just x
599 isAlias _ = Nothing
600
601 instance ReferenceContainer Expression where
602 fromName nm = Reference nm Nothing
603 nameOut (Reference nm _) = return nm
604 nameOut (Constant (ConstantField nm _)) = return nm
605 nameOut p = failDoc ("This expression isn't a 'name':" <+> pretty p)
606
607 instance ExpressionLike Expression where
608 fromInt = Constant . fromInt
609 fromIntWithTag i t = Constant $ fromIntWithTag i t
610 intOut doc (Constant c) = intOut ("intOut{Expression}" <+> doc) c
611 intOut doc x = failDoc $ vcat [ "Expecting a constant, but got:" <++> pretty x
612 , "Called from:" <+> doc
613 ]
614
615 fromBool = Constant . fromBool
616 boolOut (Constant c) = boolOut c
617 boolOut x = failDoc ("Expecting a constant, but got:" <++> pretty x)
618
619 -- fromList [x] = x -- TODO: what would break if I do this?
620 fromList xs = AbstractLiteral $ AbsLitMatrix (mkDomainIntB 1 (fromInt $ genericLength xs)) xs
621 listOut (AbstractLiteral (AbsLitMatrix _ xs)) = return xs
622 listOut (Constant (ConstantAbstract (AbsLitMatrix _ xs))) = return (map Constant xs)
623 listOut c = failDoc ("Expecting a matrix literal, but found:" <+> pretty c)
624
625 instance Num Expression where
626 x + y = Op $ MkOpSum $ OpSum $ fromList [x,y]
627 x - y = Op $ MkOpMinus $ OpMinus x y
628 x * y = Op $ MkOpProduct $ OpProduct $ fromList [x,y]
629 abs x = Op $ MkOpTwoBars $ OpTwoBars x
630 signum _ = bug "signum {Expression}"
631 fromInteger = fromInt . fromInteger
632
633 instance Integral Expression where
634 divMod a b = ( Op $ MkOpDiv $ OpDiv a b
635 , Op $ MkOpMod $ OpMod a b )
636 quotRem = divMod
637 toInteger = bug "toInteger {Expression}"
638
639 instance Real Expression where
640 toRational = bug "toRational {Expression}"
641
642 instance Enum Expression where
643 fromEnum = bug "fromEnum {Expression}"
644 toEnum = fromInt . fromIntegral
645 succ a = a + 1
646 pred a = a - 1
647 enumFrom x = x : enumFrom (succ x)
648 enumFromThen x n = x : enumFromThen (x+n) n
649 enumFromTo _x _y = bug "enumFromTo {Expression}"
650 enumFromThenTo _x _n _y = bug "enumFromThenTo {Expression}"
651
652
653 ------------------------------------------------------------------------------------------------------------------------
654 -- InBubble ------------------------------------------------------------------------------------------------------------
655 ------------------------------------------------------------------------------------------------------------------------
656
657 data InBubble
658 = AuxiliaryVars [Statement] -- can only be a LocalFind or a SuchThat
659 -- the variable declarations are lifted to top level, eventually
660 | DefinednessConstraints [Expression] -- lifted to the closest relational context
661 deriving (Eq, Ord, Show, Data, Typeable, Generic)
662
663 instance Serialize InBubble
664 instance Hashable InBubble
665 instance ToJSON InBubble where toJSON = genericToJSON jsonOptions
666 instance FromJSON InBubble where parseJSON = genericParseJSON jsonOptions
667
668
669 ------------------------------------------------------------------------------------------------------------------------
670 -- some helper functions to do with Expressions ------------------------------------------------------------------------
671 ------------------------------------------------------------------------------------------------------------------------
672
673 -- | This is only for when you know the Expression you have is actually a Constant, but
674 -- is refusing to believe that it is one.
675 -- Remind it where it comes from!
676 -- (Srsly: Can be useful after parsing a solution file, for example.)
677 e2c :: MonadFailDoc m => Expression -> m Constant
678 e2c (Constant c) = return c
679 e2c (AbstractLiteral (AbsLitMatrix (DomainReference _ Nothing) _)) =
680 failDoc "Cannot convert a matrix literal with an unresolved index domain to a constant."
681 e2c (AbstractLiteral c) = ConstantAbstract <$> mapM e2c c
682 e2c (Op (MkOpNegate (OpNegate (Constant (ConstantInt t x))))) = return $ ConstantInt t $ negate x
683 e2c x = failDoc ("e2c, not a constant:" <+> pretty x)
684
685 -- | generate a fresh name for a quantified variable.
686 -- fst: the pattern to be used inside a generator
687 -- snd: the expression to be used everywhere else
688 quantifiedVar :: NameGen m => m (AbstractPattern, Expression)
689 quantifiedVar = do
690 nm <- nextName "q"
691 let pat = Single nm
692 ref = Reference nm Nothing
693 return (pat, ref)
694
695 -- | like `quantifiedVar`, but already name-resolved as a quantified variable over the given domain
696 quantifiedVarOverDomain :: NameGen m => Domain () Expression -> m (AbstractPattern, Expression)
697 quantifiedVarOverDomain domain = do
698 nm <- nextName "q"
699 let pat = Single nm
700 ref = Reference nm (Just (InComprehension (GenDomainNoRepr (Single nm) domain)))
701 return (pat, ref)
702
703 -- | generate a fresh name for an auxiliary variable.
704 -- fst: the name to be used when declaring the variable
705 -- snd: the expression to be used everywhere else
706 auxiliaryVar :: NameGen m => m (Name, Expression)
707 auxiliaryVar = do
708 -- Savile Row has a bug which is triggered when there are variables with names of the form aux*
709 nm <- nextName "conjure_aux"
710 let ref = Reference nm Nothing
711 return (nm, ref)
712
713
714 -- | pattern, template, argument, result
715 lambdaToFunction :: AbstractPattern -> Expression -> Expression -> Expression
716 lambdaToFunction (Single nm) body = \ p ->
717 let
718 replacer :: Expression -> Expression
719 replacer (Reference n _) | n == nm = p
720 replacer x = x
721 in
722 transform replacer body
723 lambdaToFunction (AbsPatTuple ts) body = \ p ->
724 let
725 unroll :: [AbstractPattern] -> [Expression] -> Expression -> Expression
726 unroll [] [] b = b
727 unroll (pat:pats) (val:vals) b = unroll pats vals (lambdaToFunction pat b val)
728 unroll _ _ _ = bug "lambdaToFunction, AbsPatTuple, unroll"
729
730 ps :: [Expression]
731 ps = case p of
732 Constant (ConstantAbstract (AbsLitTuple xs)) -> map Constant xs
733 AbstractLiteral (AbsLitTuple xs) -> xs
734 _ -> [ Op (MkOpIndexing (OpIndexing p i))
735 | i' <- [ 1 .. genericLength ts ]
736 , let i = fromInt i'
737 ]
738 in
739 unroll ts ps body
740 lambdaToFunction (AbsPatMatrix ts) body = \ p ->
741 let
742 unroll :: [AbstractPattern] -> [Expression] -> Expression -> Expression
743 unroll [] [] b = b
744 unroll (pat:pats) (val:vals) b = unroll pats vals (lambdaToFunction pat b val)
745 unroll _ _ _ = bug "lambdaToFunction, AbsPatMatrix, unroll"
746
747 ps :: [Expression]
748 ps = case p of
749 Constant (ConstantAbstract (AbsLitMatrix _ xs)) -> map Constant xs
750 AbstractLiteral (AbsLitMatrix _ xs) -> xs
751 _ -> bug $ "lambdaToFunction, AbsPatMatrix" <++> vcat [pretty p, pretty (show p)]
752 in
753 unroll ts ps body
754 lambdaToFunction (AbsPatSet ts) body = \ p ->
755 let
756 unroll :: [AbstractPattern] -> [Expression] -> Expression -> Expression
757 unroll [] [] b = b
758 unroll (pat:pats) (val:vals) b = unroll pats vals (lambdaToFunction pat b val)
759 unroll _ _ _ = bug "lambdaToFunction, AbsPatSet, unroll"
760
761 ps :: [Expression]
762 ps = case p of
763 Constant (viewConstantSet -> Just xs) -> map Constant xs
764 AbstractLiteral (AbsLitSet xs) -> xs
765 _ -> bug $ "lambdaToFunction, AbsPatSet" <++> vcat [pretty p, pretty (show p)]
766 in
767 unroll ts ps body
768 lambdaToFunction p@AbstractPatternMetaVar{} _ = bug $ "Unsupported AbstractPattern, got" <+> pretty (show p)
769
770
771 ------------------------------------------------------------------------------------------------------------------------
772 -- ReferenceTo ---------------------------------------------------------------------------------------------------------
773 ------------------------------------------------------------------------------------------------------------------------
774
775 data ReferenceTo
776 = Alias Expression
777 | InComprehension Generator
778 | DeclNoRepr FindOrGiven Name (Domain () Expression)
779 Region -- the region of this reference
780 -- references with the same region identifier will get the same representation
781 | DeclHasRepr FindOrGiven Name (Domain HasRepresentation Expression)
782 | RecordField Name Type -- the type of the field with this name
783 | VariantField Name Type -- the type of the variant with this name
784 deriving (Eq, Ord, Show, Data, Typeable, Generic)
785
786 instance Serialize ReferenceTo
787 instance Hashable ReferenceTo
788 instance ToJSON ReferenceTo where toJSON = genericToJSON jsonOptions
789 instance FromJSON ReferenceTo where parseJSON = genericParseJSON jsonOptions
790
791 instance Pretty ReferenceTo where
792 pretty (Alias x) = "an alias for" <++> pretty x
793 pretty (InComprehension gen) = "a comprehension generator" <++> pretty gen
794 pretty (DeclNoRepr forg nm dom _) = "declaration of" <++> pretty forg <+> pretty nm <> ":" <+> pretty dom
795 pretty (DeclHasRepr forg nm dom ) = "declaration of" <++> pretty forg <+> pretty nm <> ":" <+> pretty dom
796 pretty (RecordField nm ty) = "record field" <++> prParens (pretty nm <+> ":" <+> pretty ty)
797 pretty (VariantField nm ty) = "variant field" <++> prParens (pretty nm <+> ":" <+> pretty ty)
798
799 data Region
800 = NoRegion
801 | Region Int
802 deriving (Eq, Ord, Show, Data, Typeable, Generic)
803
804 instance Serialize Region
805 instance Hashable Region
806 instance ToJSON Region where toJSON = genericToJSON jsonOptions
807 instance FromJSON Region where parseJSON = genericParseJSON jsonOptions
808
809
810 ------------------------------------------------------------------------------------------------------------------------
811 -- AbstractPattern -----------------------------------------------------------------------------------------------------
812 ------------------------------------------------------------------------------------------------------------------------
813
814 data AbstractPattern
815 = Single Name
816 | AbsPatTuple [AbstractPattern]
817 | AbsPatMatrix
818 -- (Domain () a) -- TODO: Should there be a domain here?
819 [AbstractPattern]
820 | AbsPatSet [AbstractPattern]
821 -- | AbsPatMSet [a]
822 -- | AbsPatFunction [(a, a)]
823 -- | AbsPatRelation [[a]]
824 -- | AbsPatPartition [[a]]
825 -- TODO: Consider introducing the above as abstract patterns...
826 | AbstractPatternMetaVar String
827 deriving (Eq, Ord, Show, Data, Typeable, Generic)
828
829 instance Serialize AbstractPattern
830 instance Hashable AbstractPattern
831 instance ToJSON AbstractPattern where toJSON = genericToJSON jsonOptions
832 instance FromJSON AbstractPattern where parseJSON = genericParseJSON jsonOptions
833
834 instance Pretty AbstractPattern where
835 pretty (Single nm) = pretty nm
836 pretty (AbsPatTuple xs) = (if length xs <= 1 then "tuple" else prEmpty) <>
837 prettyList prParens "," xs
838 pretty (AbsPatMatrix xs) = prettyList prBrackets "," xs
839 pretty (AbsPatSet xs) = prettyList prBraces "," xs
840 pretty (AbstractPatternMetaVar s) = "&" <> pretty s
841
842 instance VarSymBreakingDescription AbstractPattern where
843 varSymBreakingDescription (Single nm) = toJSON nm
844 varSymBreakingDescription (AbsPatTuple xs) = JSON.Object $ KM.fromList
845 [ ("type", JSON.String "AbsPatTuple")
846 , ("children", JSON.Array $ V.fromList $ map varSymBreakingDescription xs)
847 ]
848 varSymBreakingDescription (AbsPatMatrix xs) = JSON.Object $ KM.fromList
849 [ ("type", JSON.String "AbsPatMatrix")
850 , ("children", JSON.Array $ V.fromList $ map varSymBreakingDescription xs)
851 ]
852 varSymBreakingDescription (AbsPatSet xs) = JSON.Object $ KM.fromList
853 [ ("type", JSON.String "AbsPatSet")
854 , ("children", JSON.Array $ V.fromList $ map varSymBreakingDescription xs)
855 , ("symmetricChildren", JSON.Bool True)
856 ]
857 varSymBreakingDescription (AbstractPatternMetaVar s) = JSON.Object $ KM.fromList
858 [ ("type", JSON.String "AbstractPatternMetaVar")
859 , ("name", JSON.String (stringToText s))
860 ]
861
862
863 patternToExpr :: AbstractPattern -> Expression
864 patternToExpr (Single nm) = Reference nm Nothing
865 patternToExpr (AbsPatTuple ts) = AbstractLiteral $ AbsLitTuple $ map patternToExpr ts
866 patternToExpr (AbsPatMatrix ts) = AbstractLiteral $ AbsLitMatrix
867 (DomainInt TagInt [RangeBounded 1 (fromInt (genericLength ts))])
868 $ map patternToExpr ts
869 patternToExpr (AbsPatSet ts) = AbstractLiteral $ AbsLitSet $ map patternToExpr ts
870 patternToExpr AbstractPatternMetaVar{} = bug "patternToExpr"
871
872 ------------------------------------------------------------------------------------------------------------------------
873 -- Generator -----------------------------------------------------------------------------------------------------------
874 ------------------------------------------------------------------------------------------------------------------------
875
876 data GeneratorOrCondition
877 = Generator Generator
878 | Condition Expression
879 | ComprehensionLetting AbstractPattern Expression
880 deriving (Eq, Ord, Show, Data, Typeable, Generic)
881
882 instance Pretty GeneratorOrCondition where
883 pretty (Generator x) = pretty x
884 pretty (Condition x) = pretty x
885 pretty (ComprehensionLetting n x) = "letting" <+> pretty n <+> "be" <+> pretty x
886
887 instance VarSymBreakingDescription GeneratorOrCondition where
888 varSymBreakingDescription (Generator x) = JSON.Object $ KM.fromList
889 [ ("type", JSON.String "Generator")
890 , ("child", varSymBreakingDescription x)
891 ]
892 varSymBreakingDescription (Condition x) = JSON.Object $ KM.fromList
893 [ ("type", JSON.String "Condition")
894 , ("child", varSymBreakingDescription x)
895 ]
896 varSymBreakingDescription (ComprehensionLetting n x) = JSON.Object $ KM.fromList
897 [ ("type", JSON.String "ComprehensionLetting")
898 , ("children", JSON.Array $ V.fromList [toJSON n, varSymBreakingDescription x])
899 ]
900
901 instance Serialize GeneratorOrCondition
902 instance Hashable GeneratorOrCondition
903 instance ToJSON GeneratorOrCondition where toJSON = genericToJSON jsonOptions
904 instance FromJSON GeneratorOrCondition where parseJSON = genericParseJSON jsonOptions
905
906
907 data Generator
908 = GenDomainNoRepr AbstractPattern (Domain () Expression)
909 | GenDomainHasRepr Name (Domain HasRepresentation Expression)
910 | GenInExpr AbstractPattern Expression
911 deriving (Eq, Ord, Show, Data, Typeable, Generic)
912
913 instance Pretty Generator where
914 pretty (GenDomainNoRepr pat x) = pretty pat <+> ":" <+> pretty x
915 pretty (GenDomainHasRepr pat x) = pretty pat <+> ":" <+> pretty x
916 pretty (GenInExpr pat x) = pretty pat <+> "<-" <+> pretty x
917
918 instance VarSymBreakingDescription Generator where
919 varSymBreakingDescription (GenDomainNoRepr pat x) = JSON.Object $ KM.fromList
920 [ ("type", JSON.String "GenDomainNoRepr")
921 , ("pattern", varSymBreakingDescription pat)
922 , ("generator", varSymBreakingDescription x)
923 ]
924 varSymBreakingDescription (GenDomainHasRepr pat x) = JSON.Object $ KM.fromList
925 [ ("type", JSON.String "GenDomainHasRepr")
926 , ("pattern", toJSON pat)
927 , ("generator", varSymBreakingDescription x)
928 ]
929 varSymBreakingDescription (GenInExpr pat x) = JSON.Object $ KM.fromList
930 [ ("type", JSON.String "GenInExpr")
931 , ("pattern", varSymBreakingDescription pat)
932 , ("generator", varSymBreakingDescription x)
933 ]
934
935 instance Serialize Generator
936 instance Hashable Generator
937 instance ToJSON Generator where toJSON = genericToJSON jsonOptions
938 instance FromJSON Generator where parseJSON = genericParseJSON jsonOptions
939
940 generatorPat :: Generator -> AbstractPattern
941 generatorPat (GenDomainNoRepr pat _) = pat
942 generatorPat (GenDomainHasRepr pat _) = Single pat
943 generatorPat (GenInExpr pat _) = pat
944
945
946 ------------------------------------------------------------------------------------------------------------------------
947 -- Misc ---------------------------------------------------------------------------------------------------------------
948 ------------------------------------------------------------------------------------------------------------------------
949
950 tupleLitIfNeeded :: [Expression] -> Expression
951 tupleLitIfNeeded [] = bug "tupleLitIfNeeded []"
952 tupleLitIfNeeded [x] = x
953 tupleLitIfNeeded xs = AbstractLiteral (AbsLitTuple xs)
954
955 nbUses :: Data x => Name -> x -> Int
956 nbUses nm here = length [ () | Reference nm2 _ <- universeBi here, nm == nm2 ]
957
958 emptyCollectionX :: Expression -> Bool
959 emptyCollectionX (Constant x) = emptyCollection x
960 emptyCollectionX (AbstractLiteral x) = emptyCollectionAbsLit x
961 emptyCollectionX (Typed x _) = emptyCollectionX x
962 emptyCollectionX _ = False
963
964
965 reDomExp :: Domain () Expression -> Domain () Expression
966 reDomExp exp = case exp of
967 DomainInt t _ -> reTag t exp
968 _ -> exp
969
970 isDomainExpr :: MonadFailDoc m => Expression -> m ()
971 isDomainExpr Domain{} = return ()
972 isDomainExpr x = na ("Not a domain expression: " <+> pretty x)