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 c) = ConstantAbstract <$> mapM e2c c
680 e2c (Op (MkOpNegate (OpNegate (Constant (ConstantInt t x))))) = return $ ConstantInt t $ negate x
681 e2c x = failDoc ("e2c, not a constant:" <+> pretty x)
682
683 -- | generate a fresh name for a quantified variable.
684 -- fst: the pattern to be used inside a generator
685 -- snd: the expression to be used everywhere else
686 quantifiedVar :: NameGen m => m (AbstractPattern, Expression)
687 quantifiedVar = do
688 nm <- nextName "q"
689 let pat = Single nm
690 ref = Reference nm Nothing
691 return (pat, ref)
692
693 -- | like `quantifiedVar`, but already name-resolved as a quantified variable over the given domain
694 quantifiedVarOverDomain :: NameGen m => Domain () Expression -> m (AbstractPattern, Expression)
695 quantifiedVarOverDomain domain = do
696 nm <- nextName "q"
697 let pat = Single nm
698 ref = Reference nm (Just (InComprehension (GenDomainNoRepr (Single nm) domain)))
699 return (pat, ref)
700
701 -- | generate a fresh name for an auxiliary variable.
702 -- fst: the name to be used when declaring the variable
703 -- snd: the expression to be used everywhere else
704 auxiliaryVar :: NameGen m => m (Name, Expression)
705 auxiliaryVar = do
706 -- Savile Row has a bug which is triggered when there are variables with names of the form aux*
707 nm <- nextName "conjure_aux"
708 let ref = Reference nm Nothing
709 return (nm, ref)
710
711
712 -- | pattern, template, argument, result
713 lambdaToFunction :: AbstractPattern -> Expression -> Expression -> Expression
714 lambdaToFunction (Single nm) body = \ p ->
715 let
716 replacer :: Expression -> Expression
717 replacer (Reference n _) | n == nm = p
718 replacer x = x
719 in
720 transform replacer body
721 lambdaToFunction (AbsPatTuple ts) body = \ p ->
722 let
723 unroll :: [AbstractPattern] -> [Expression] -> Expression -> Expression
724 unroll [] [] b = b
725 unroll (pat:pats) (val:vals) b = unroll pats vals (lambdaToFunction pat b val)
726 unroll _ _ _ = bug "lambdaToFunction, AbsPatTuple, unroll"
727
728 ps :: [Expression]
729 ps = case p of
730 Constant (ConstantAbstract (AbsLitTuple xs)) -> map Constant xs
731 AbstractLiteral (AbsLitTuple xs) -> xs
732 _ -> [ Op (MkOpIndexing (OpIndexing p i))
733 | i' <- [ 1 .. genericLength ts ]
734 , let i = fromInt i'
735 ]
736 in
737 unroll ts ps body
738 lambdaToFunction (AbsPatMatrix ts) body = \ p ->
739 let
740 unroll :: [AbstractPattern] -> [Expression] -> Expression -> Expression
741 unroll [] [] b = b
742 unroll (pat:pats) (val:vals) b = unroll pats vals (lambdaToFunction pat b val)
743 unroll _ _ _ = bug "lambdaToFunction, AbsPatMatrix, unroll"
744
745 ps :: [Expression]
746 ps = case p of
747 Constant (ConstantAbstract (AbsLitMatrix _ xs)) -> map Constant xs
748 AbstractLiteral (AbsLitMatrix _ xs) -> xs
749 _ -> bug $ "lambdaToFunction, AbsPatMatrix" <++> vcat [pretty p, pretty (show p)]
750 in
751 unroll ts ps body
752 lambdaToFunction (AbsPatSet ts) body = \ p ->
753 let
754 unroll :: [AbstractPattern] -> [Expression] -> Expression -> Expression
755 unroll [] [] b = b
756 unroll (pat:pats) (val:vals) b = unroll pats vals (lambdaToFunction pat b val)
757 unroll _ _ _ = bug "lambdaToFunction, AbsPatSet, unroll"
758
759 ps :: [Expression]
760 ps = case p of
761 Constant (viewConstantSet -> Just xs) -> map Constant xs
762 AbstractLiteral (AbsLitSet xs) -> xs
763 _ -> bug $ "lambdaToFunction, AbsPatSet" <++> vcat [pretty p, pretty (show p)]
764 in
765 unroll ts ps body
766 lambdaToFunction p@AbstractPatternMetaVar{} _ = bug $ "Unsupported AbstractPattern, got" <+> pretty (show p)
767
768
769 ------------------------------------------------------------------------------------------------------------------------
770 -- ReferenceTo ---------------------------------------------------------------------------------------------------------
771 ------------------------------------------------------------------------------------------------------------------------
772
773 data ReferenceTo
774 = Alias Expression
775 | InComprehension Generator
776 | DeclNoRepr FindOrGiven Name (Domain () Expression)
777 Region -- the region of this reference
778 -- references with the same region identifier will get the same representation
779 | DeclHasRepr FindOrGiven Name (Domain HasRepresentation Expression)
780 | RecordField Name Type -- the type of the field with this name
781 | VariantField Name Type -- the type of the variant with this name
782 deriving (Eq, Ord, Show, Data, Typeable, Generic)
783
784 instance Serialize ReferenceTo
785 instance Hashable ReferenceTo
786 instance ToJSON ReferenceTo where toJSON = genericToJSON jsonOptions
787 instance FromJSON ReferenceTo where parseJSON = genericParseJSON jsonOptions
788
789 instance Pretty ReferenceTo where
790 pretty (Alias x) = "an alias for" <++> pretty x
791 pretty (InComprehension gen) = "a comprehension generator" <++> pretty gen
792 pretty (DeclNoRepr forg nm dom _) = "declaration of" <++> pretty forg <+> pretty nm <> ":" <+> pretty dom
793 pretty (DeclHasRepr forg nm dom ) = "declaration of" <++> pretty forg <+> pretty nm <> ":" <+> pretty dom
794 pretty (RecordField nm ty) = "record field" <++> prParens (pretty nm <+> ":" <+> pretty ty)
795 pretty (VariantField nm ty) = "variant field" <++> prParens (pretty nm <+> ":" <+> pretty ty)
796
797 data Region
798 = NoRegion
799 | Region Int
800 deriving (Eq, Ord, Show, Data, Typeable, Generic)
801
802 instance Serialize Region
803 instance Hashable Region
804 instance ToJSON Region where toJSON = genericToJSON jsonOptions
805 instance FromJSON Region where parseJSON = genericParseJSON jsonOptions
806
807
808 ------------------------------------------------------------------------------------------------------------------------
809 -- AbstractPattern -----------------------------------------------------------------------------------------------------
810 ------------------------------------------------------------------------------------------------------------------------
811
812 data AbstractPattern
813 = Single Name
814 | AbsPatTuple [AbstractPattern]
815 | AbsPatMatrix
816 -- (Domain () a) -- TODO: Should there be a domain here?
817 [AbstractPattern]
818 | AbsPatSet [AbstractPattern]
819 -- | AbsPatMSet [a]
820 -- | AbsPatFunction [(a, a)]
821 -- | AbsPatRelation [[a]]
822 -- | AbsPatPartition [[a]]
823 -- TODO: Consider introducing the above as abstract patterns...
824 | AbstractPatternMetaVar String
825 deriving (Eq, Ord, Show, Data, Typeable, Generic)
826
827 instance Serialize AbstractPattern
828 instance Hashable AbstractPattern
829 instance ToJSON AbstractPattern where toJSON = genericToJSON jsonOptions
830 instance FromJSON AbstractPattern where parseJSON = genericParseJSON jsonOptions
831
832 instance Pretty AbstractPattern where
833 pretty (Single nm) = pretty nm
834 pretty (AbsPatTuple xs) = (if length xs <= 1 then "tuple" else prEmpty) <>
835 prettyList prParens "," xs
836 pretty (AbsPatMatrix xs) = prettyList prBrackets "," xs
837 pretty (AbsPatSet xs) = prettyList prBraces "," xs
838 pretty (AbstractPatternMetaVar s) = "&" <> pretty s
839
840 instance VarSymBreakingDescription AbstractPattern where
841 varSymBreakingDescription (Single nm) = toJSON nm
842 varSymBreakingDescription (AbsPatTuple xs) = JSON.Object $ KM.fromList
843 [ ("type", JSON.String "AbsPatTuple")
844 , ("children", JSON.Array $ V.fromList $ map varSymBreakingDescription xs)
845 ]
846 varSymBreakingDescription (AbsPatMatrix xs) = JSON.Object $ KM.fromList
847 [ ("type", JSON.String "AbsPatMatrix")
848 , ("children", JSON.Array $ V.fromList $ map varSymBreakingDescription xs)
849 ]
850 varSymBreakingDescription (AbsPatSet xs) = JSON.Object $ KM.fromList
851 [ ("type", JSON.String "AbsPatSet")
852 , ("children", JSON.Array $ V.fromList $ map varSymBreakingDescription xs)
853 , ("symmetricChildren", JSON.Bool True)
854 ]
855 varSymBreakingDescription (AbstractPatternMetaVar s) = JSON.Object $ KM.fromList
856 [ ("type", JSON.String "AbstractPatternMetaVar")
857 , ("name", JSON.String (stringToText s))
858 ]
859
860
861 patternToExpr :: AbstractPattern -> Expression
862 patternToExpr (Single nm) = Reference nm Nothing
863 patternToExpr (AbsPatTuple ts) = AbstractLiteral $ AbsLitTuple $ map patternToExpr ts
864 patternToExpr (AbsPatMatrix ts) = AbstractLiteral $ AbsLitMatrix
865 (DomainInt TagInt [RangeBounded 1 (fromInt (genericLength ts))])
866 $ map patternToExpr ts
867 patternToExpr (AbsPatSet ts) = AbstractLiteral $ AbsLitSet $ map patternToExpr ts
868 patternToExpr AbstractPatternMetaVar{} = bug "patternToExpr"
869
870 ------------------------------------------------------------------------------------------------------------------------
871 -- Generator -----------------------------------------------------------------------------------------------------------
872 ------------------------------------------------------------------------------------------------------------------------
873
874 data GeneratorOrCondition
875 = Generator Generator
876 | Condition Expression
877 | ComprehensionLetting AbstractPattern Expression
878 deriving (Eq, Ord, Show, Data, Typeable, Generic)
879
880 instance Pretty GeneratorOrCondition where
881 pretty (Generator x) = pretty x
882 pretty (Condition x) = pretty x
883 pretty (ComprehensionLetting n x) = "letting" <+> pretty n <+> "be" <+> pretty x
884
885 instance VarSymBreakingDescription GeneratorOrCondition where
886 varSymBreakingDescription (Generator x) = JSON.Object $ KM.fromList
887 [ ("type", JSON.String "Generator")
888 , ("child", varSymBreakingDescription x)
889 ]
890 varSymBreakingDescription (Condition x) = JSON.Object $ KM.fromList
891 [ ("type", JSON.String "Condition")
892 , ("child", varSymBreakingDescription x)
893 ]
894 varSymBreakingDescription (ComprehensionLetting n x) = JSON.Object $ KM.fromList
895 [ ("type", JSON.String "ComprehensionLetting")
896 , ("children", JSON.Array $ V.fromList [toJSON n, varSymBreakingDescription x])
897 ]
898
899 instance Serialize GeneratorOrCondition
900 instance Hashable GeneratorOrCondition
901 instance ToJSON GeneratorOrCondition where toJSON = genericToJSON jsonOptions
902 instance FromJSON GeneratorOrCondition where parseJSON = genericParseJSON jsonOptions
903
904
905 data Generator
906 = GenDomainNoRepr AbstractPattern (Domain () Expression)
907 | GenDomainHasRepr Name (Domain HasRepresentation Expression)
908 | GenInExpr AbstractPattern Expression
909 deriving (Eq, Ord, Show, Data, Typeable, Generic)
910
911 instance Pretty Generator where
912 pretty (GenDomainNoRepr pat x) = pretty pat <+> ":" <+> pretty x
913 pretty (GenDomainHasRepr pat x) = pretty pat <+> ":" <+> pretty x
914 pretty (GenInExpr pat x) = pretty pat <+> "<-" <+> pretty x
915
916 instance VarSymBreakingDescription Generator where
917 varSymBreakingDescription (GenDomainNoRepr pat x) = JSON.Object $ KM.fromList
918 [ ("type", JSON.String "GenDomainNoRepr")
919 , ("pattern", varSymBreakingDescription pat)
920 , ("generator", varSymBreakingDescription x)
921 ]
922 varSymBreakingDescription (GenDomainHasRepr pat x) = JSON.Object $ KM.fromList
923 [ ("type", JSON.String "GenDomainHasRepr")
924 , ("pattern", toJSON pat)
925 , ("generator", varSymBreakingDescription x)
926 ]
927 varSymBreakingDescription (GenInExpr pat x) = JSON.Object $ KM.fromList
928 [ ("type", JSON.String "GenInExpr")
929 , ("pattern", varSymBreakingDescription pat)
930 , ("generator", varSymBreakingDescription x)
931 ]
932
933 instance Serialize Generator
934 instance Hashable Generator
935 instance ToJSON Generator where toJSON = genericToJSON jsonOptions
936 instance FromJSON Generator where parseJSON = genericParseJSON jsonOptions
937
938 generatorPat :: Generator -> AbstractPattern
939 generatorPat (GenDomainNoRepr pat _) = pat
940 generatorPat (GenDomainHasRepr pat _) = Single pat
941 generatorPat (GenInExpr pat _) = pat
942
943
944 ------------------------------------------------------------------------------------------------------------------------
945 -- Misc ---------------------------------------------------------------------------------------------------------------
946 ------------------------------------------------------------------------------------------------------------------------
947
948 tupleLitIfNeeded :: [Expression] -> Expression
949 tupleLitIfNeeded [] = bug "tupleLitIfNeeded []"
950 tupleLitIfNeeded [x] = x
951 tupleLitIfNeeded xs = AbstractLiteral (AbsLitTuple xs)
952
953 nbUses :: Data x => Name -> x -> Int
954 nbUses nm here = length [ () | Reference nm2 _ <- universeBi here, nm == nm2 ]
955
956 emptyCollectionX :: Expression -> Bool
957 emptyCollectionX (Constant x) = emptyCollection x
958 emptyCollectionX (AbstractLiteral x) = emptyCollectionAbsLit x
959 emptyCollectionX (Typed x _) = emptyCollectionX x
960 emptyCollectionX _ = False
961
962
963 reDomExp :: Domain () Expression -> Domain () Expression
964 reDomExp exp = case exp of
965 DomainInt t _ -> reTag t exp
966 _ -> exp
967
968 isDomainExpr :: MonadFailDoc m => Expression -> m ()
969 isDomainExpr Domain{} = return ()
970 isDomainExpr x = na ("Not a domain expression: " <+> pretty x)