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