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 (MkOpNegate (OpNegate a)) -> do
365 a' <- toSimpleJSON a
366 case a' of
367 JSON.Number a'' -> return (JSON.Number (0 - a''))
368 _ -> noToSimpleJSON x
369 Op (MkOpMinus (OpMinus a b)) -> do
370 a' <- toSimpleJSON a
371 b' <- toSimpleJSON b
372 case (a', b') of
373 (JSON.Number a'', JSON.Number b'') -> return (JSON.Number (a'' - b''))
374 _ -> noToSimpleJSON x
375 _ -> noToSimpleJSON x
376 fromSimpleJSON t x = Constant <$> fromSimpleJSON t x
377
378 instance ToFromMiniZinc Expression where
379 toMiniZinc x =
380 case x of
381 Constant c -> toMiniZinc c
382 AbstractLiteral lit -> toMiniZinc lit
383 Typed y _ -> toMiniZinc y
384 Op (MkOpMinus (OpMinus a b)) -> do
385 a' <- toMiniZinc a
386 b' <- toMiniZinc b
387 case (a', b') of
388 (MZNInt a'', MZNInt b'') -> return (MZNInt (a'' - b''))
389 _ -> noToMiniZinc x
390 _ -> noToMiniZinc x
391
392 viewIndexed :: Expression -> (Expression, [Doc])
393 viewIndexed (Op (MkOpIndexing (OpIndexing m i ))) =
394 let this = pretty i
395 in second (++ [this]) (viewIndexed m)
396 viewIndexed (Op (MkOpSlicing (OpSlicing m a b))) =
397 let this = maybe prEmpty pretty a <> ".." <> maybe prEmpty pretty b
398 in second (++ [this]) (viewIndexed m)
399 viewIndexed m = (m, [])
400
401 instance Pretty Expression where
402
403 prettyPrec _ (viewIndexed -> (m,is@(_:_))) = Pr.cat [pretty m, nest 4 (prettyList prBrackets "," is)]
404
405 -- mostly for debugging: print what a reference is pointing at
406 -- prettyPrec _ (Reference x Nothing) = pretty x <> "#`NOTHING`"
407 -- prettyPrec _ (Reference x (Just (DeclHasRepr _ _ dom))) = pretty x <> "#`" <> pretty dom <> "`"
408 -- prettyPrec _ (Reference x (Just r)) = pretty x <> "#`" <> pretty r <> "`"
409
410 prettyPrec _ (Constant x) = pretty x
411 prettyPrec _ (AbstractLiteral x) = pretty x
412 prettyPrec _ (Domain x) = "`" <> pretty x <> "`"
413 prettyPrec _ (Reference x _) = pretty x
414 prettyPrec _ (WithLocals x (AuxiliaryVars locals)) =
415 vcat
416 [ "{" <+> pretty x
417 , "@" <+> vcat (map pretty locals)
418 , "}"
419 ]
420 prettyPrec _ (WithLocals x (DefinednessConstraints locals)) =
421 vcat
422 [ "{" <+> pretty x
423 , "@" <+> pretty (SuchThat locals)
424 , "}"
425 ]
426 prettyPrec _ (Comprehension x is) = prBrackets $ pretty x <++> "|" <+> prettyList id "," is
427 prettyPrec _ (Typed x ty) = prParens $ pretty x <+> ":" <+> "`" <> pretty ty <> "`"
428 prettyPrec prec (Op op) = prettyPrec prec op
429 prettyPrec _ (ExpressionMetaVar x) = "&" <> pretty x
430
431 instance VarSymBreakingDescription Expression where
432 varSymBreakingDescription (Constant x) = toJSON x
433 varSymBreakingDescription (AbstractLiteral x) = varSymBreakingDescription x
434 varSymBreakingDescription (Domain domain) = varSymBreakingDescription domain
435 varSymBreakingDescription (Reference name _) = JSON.Object $ KM.singleton "Reference" (toJSON name)
436 varSymBreakingDescription (WithLocals h (AuxiliaryVars locs)) = JSON.Object $ KM.fromList
437 [ ("type", JSON.String "WithLocals")
438 , ("head", varSymBreakingDescription h)
439 , ("children", JSON.Array $ V.fromList $ map varSymBreakingDescription locs)
440 , ("symmetricChildren", JSON.Bool True)
441 ]
442 varSymBreakingDescription (WithLocals h (DefinednessConstraints locs)) = JSON.Object $ KM.fromList
443 [ ("type", JSON.String "WithLocals")
444 , ("head", varSymBreakingDescription h)
445 , ("children", JSON.Array $ V.fromList $ map varSymBreakingDescription locs)
446 , ("symmetricChildren", JSON.Bool True)
447 ]
448 varSymBreakingDescription (Comprehension h gocs) = JSON.Object $ KM.fromList
449 [ ("type", JSON.String "Comprehension")
450 , ("head", varSymBreakingDescription h)
451 , ("gocs", JSON.Array $ V.fromList $ map varSymBreakingDescription gocs)
452 ]
453 varSymBreakingDescription (Typed x _) = varSymBreakingDescription x
454 varSymBreakingDescription (Op op) = varSymBreakingDescription op
455 varSymBreakingDescription (ExpressionMetaVar s) = JSON.Object $ KM.fromList
456 [ ("type", JSON.String "ExpressionMetaVar")
457 , ("name", JSON.String (stringToText s))
458 ]
459
460 instance TypeOf Expression where
461 typeOf (Constant x) = typeOf x
462 typeOf (AbstractLiteral x) = typeOf x
463 typeOf (Domain x) = failDoc ("Expected an expression, but got a domain:" <++> pretty x)
464 typeOf (Reference nm Nothing) = failDoc ("Type error, identifier not bound:" <+> pretty nm)
465 typeOf (Reference nm (Just refTo)) =
466 case refTo of
467 Alias x -> typeOf x
468 InComprehension gen ->
469 let
470 lu pat ty = maybe
471 (bug $ vcat ["Type error, InComprehension:", pretty nm, pretty pat, pretty ty])
472 return
473 (lu' pat ty)
474 lu' (Single nm') ty | nm == nm' = Just ty
475 lu' (AbsPatTuple pats) (TypeTuple tys) = zipWith lu' pats tys |> catMaybes |> listToMaybe
476 lu' (AbsPatMatrix pats) (TypeMatrix _ ty ) = [lu' p ty | p <- pats] |> catMaybes |> listToMaybe
477 lu' (AbsPatSet pats) (TypeSet ty ) = [lu' p ty | p <- pats] |> catMaybes |> listToMaybe
478 lu' _ _ = Nothing
479 in
480 case gen of
481 GenDomainNoRepr pat domain -> typeOfDomain domain >>= lu pat
482 GenDomainHasRepr pat domain -> typeOfDomain domain >>= lu (Single pat)
483 GenInExpr pat expr ->
484 case project expr of
485 Just (d :: Domain () Expression) -> failDoc $ vcat
486 [ "Expected an expression, but got a domain:" <++> pretty d
487 , "In the generator of a comprehension or a quantified expression"
488 , "Consider using" <+> pretty pat <+> ":" <+> pretty expr
489 ]
490 Nothing -> do
491 tyExpr <- typeOf expr
492 case innerTypeOf tyExpr of
493 Just tyExprInner -> lu pat tyExprInner
494 Nothing -> failDoc $ vcat
495 [ "Type error in the generator of a comprehension or a quantified expression"
496 , "Consider using" <+> pretty pat <+> ":" <+> pretty expr
497 ]
498 DeclNoRepr _ _ dom _ -> typeOfDomain dom
499 DeclHasRepr _ _ dom -> typeOfDomain dom
500 RecordField _ ty -> return ty
501 VariantField _ ty -> return ty
502 typeOf p@(WithLocals h (DefinednessConstraints cs)) = do
503 forM_ cs $ \ c -> do
504 ty <- typeOf c
505 unless (typeUnify TypeBool ty) $ failDoc $ vcat
506 [ "Local constraint is not boolean."
507 , "Condition:" <+> pretty c
508 , "In:" <+> pretty p
509 ]
510 typeOf h
511 typeOf p@(WithLocals h (AuxiliaryVars stmts)) = do
512 forM_ stmts $ \ stmt ->
513 case stmt of
514 Declaration{} -> return () -- TODO: what other checks make sense?
515 SuchThat xs -> forM_ xs $ \ x -> do
516 ty <- typeOf x
517 case ty of
518 TypeBool{} -> return ()
519 _ -> failDoc $ vcat
520 [ "Inside a bubble, in a 'such that' statement:" <++> pretty x
521 , "Expected type `bool`, but got:" <++> pretty ty
522 ]
523 _ -> failDoc $ vcat
524 [ "Unexpected statement inside a bubble."
525 , "Expected type `find` or `such that`, but got:" <++> pretty stmt
526 , "The complete expression:" <+> pretty p
527 ]
528 typeOf h
529 typeOf p@(Comprehension x gensOrConds) = do
530 forM_ gensOrConds $ \ goc -> case goc of
531 Generator{} -> return () -- TODO: do this properly
532 Condition c -> do
533 ty <- typeOf c
534 unless (typeUnify TypeBool ty) $ failDoc $ vcat
535 [ "Condition is not boolean."
536 , "Condition:" <+> pretty c
537 , "In:" <+> pretty p
538 ]
539 ComprehensionLetting{} -> return ()
540 TypeList <$> typeOf x
541 typeOf (Typed _ ty) = return ty
542 typeOf (Op op) = typeOf op
543 typeOf x@ExpressionMetaVar{} = bug ("typeOf:" <+> pretty x)
544
545 instance RepresentationOf Expression where
546 representationTreeOf (Reference _ (Just (DeclHasRepr _ _ dom))) = return (reprTree dom)
547 representationTreeOf (Op (MkOpIndexing (OpIndexing m i))) = do
548 iType <- typeOf i
549 case iType of
550 TypeBool{} -> return ()
551 TypeInt{} -> return ()
552 _ -> failDoc "representationOf, OpIndexing, not a bool or int index"
553 mTree <- representationTreeOf m
554 case mTree of
555 Tree _ [r] -> return r
556 _ -> failDoc "domainOf, OpIndexing, not a matrix"
557 representationTreeOf _ = failDoc "doesn't seem to have a representation"
558
559 instance Domain () Expression :< Expression where
560 inject = Domain
561 project (Domain x) = return x
562 project (Reference _ (Just (Alias x))) = project x
563 project x = failDoc ("projecting Domain out of Expression:" <+> pretty x)
564
565 instance Op Expression :< Expression where
566 inject = Op
567 project (Op x) = return x
568 project x = failDoc ("projecting Op out of Expression:" <+> pretty x)
569
570 instance Op Constant :< Constant where
571 inject x = bug ("injecting Op into a Constant:" <+> pretty x)
572 project x = failDoc ("projecting Op out of a Constant:" <+> pretty x)
573
574 instance CanBeAnAlias Expression where
575 isAlias (Reference _ (Just (Alias x))) = Just x
576 isAlias _ = Nothing
577
578 instance ReferenceContainer Expression where
579 fromName nm = Reference nm Nothing
580 nameOut (Reference nm _) = return nm
581 nameOut (Constant (ConstantField nm _)) = return nm
582 nameOut p = failDoc ("This expression isn't a 'name':" <+> pretty p)
583
584 instance ExpressionLike Expression where
585 fromInt = Constant . fromInt
586 fromIntWithTag i t = Constant $ fromIntWithTag i t
587 intOut doc (Constant c) = intOut ("intOut{Expression}" <+> doc) c
588 intOut doc x = failDoc $ vcat [ "Expecting a constant, but got:" <++> pretty x
589 , "Called from:" <+> doc
590 ]
591
592 fromBool = Constant . fromBool
593 boolOut (Constant c) = boolOut c
594 boolOut x = failDoc ("Expecting a constant, but got:" <++> pretty x)
595
596 -- fromList [x] = x -- TODO: what would break if I do this?
597 fromList xs = AbstractLiteral $ AbsLitMatrix (mkDomainIntB 1 (fromInt $ genericLength xs)) xs
598 listOut (AbstractLiteral (AbsLitMatrix _ xs)) = return xs
599 listOut (Constant (ConstantAbstract (AbsLitMatrix _ xs))) = return (map Constant xs)
600 listOut c = failDoc ("Expecting a matrix literal, but found:" <+> pretty c)
601
602 instance Num Expression where
603 x + y = Op $ MkOpSum $ OpSum $ fromList [x,y]
604 x - y = Op $ MkOpMinus $ OpMinus x y
605 x * y = Op $ MkOpProduct $ OpProduct $ fromList [x,y]
606 abs x = Op $ MkOpTwoBars $ OpTwoBars x
607 signum _ = bug "signum {Expression}"
608 fromInteger = fromInt . fromInteger
609
610 instance Integral Expression where
611 divMod a b = ( Op $ MkOpDiv $ OpDiv a b
612 , Op $ MkOpMod $ OpMod a b )
613 quotRem = divMod
614 toInteger = bug "toInteger {Expression}"
615
616 instance Real Expression where
617 toRational = bug "toRational {Expression}"
618
619 instance Enum Expression where
620 fromEnum = bug "fromEnum {Expression}"
621 toEnum = fromInt . fromIntegral
622 succ a = a + 1
623 pred a = a - 1
624 enumFrom x = x : enumFrom (succ x)
625 enumFromThen x n = x : enumFromThen (x+n) n
626 enumFromTo _x _y = bug "enumFromTo {Expression}"
627 enumFromThenTo _x _n _y = bug "enumFromThenTo {Expression}"
628
629
630 ------------------------------------------------------------------------------------------------------------------------
631 -- InBubble ------------------------------------------------------------------------------------------------------------
632 ------------------------------------------------------------------------------------------------------------------------
633
634 data InBubble
635 = AuxiliaryVars [Statement] -- can only be a LocalFind or a SuchThat
636 -- the variable declarations are lifted to top level, eventually
637 | DefinednessConstraints [Expression] -- lifted to the closest relational context
638 deriving (Eq, Ord, Show, Data, Typeable, Generic)
639
640 instance Serialize InBubble
641 instance Hashable InBubble
642 instance ToJSON InBubble where toJSON = genericToJSON jsonOptions
643 instance FromJSON InBubble where parseJSON = genericParseJSON jsonOptions
644
645
646 ------------------------------------------------------------------------------------------------------------------------
647 -- some helper functions to do with Expressions ------------------------------------------------------------------------
648 ------------------------------------------------------------------------------------------------------------------------
649
650 -- | This is only for when you know the Expression you have is actually a Constant, but
651 -- is refusing to believe that it is one.
652 -- Remind it where it comes from!
653 -- (Srsly: Can be useful after parsing a solution file, for example.)
654 e2c :: MonadFailDoc m => Expression -> m Constant
655 e2c (Constant c) = return c
656 e2c (AbstractLiteral c) = ConstantAbstract <$> mapM e2c c
657 e2c (Op (MkOpNegate (OpNegate (Constant (ConstantInt t x))))) = return $ ConstantInt t $ negate x
658 e2c x = failDoc ("e2c, not a constant:" <+> pretty x)
659
660 -- | generate a fresh name for a quantified variable.
661 -- fst: the pattern to be used inside a generator
662 -- snd: the expression to be used everywhere else
663 quantifiedVar :: NameGen m => m (AbstractPattern, Expression)
664 quantifiedVar = do
665 nm <- nextName "q"
666 let pat = Single nm
667 ref = Reference nm Nothing
668 return (pat, ref)
669
670 -- | like `quantifiedVar`, but already name-resolved as a quantified variable over the given domain
671 quantifiedVarOverDomain :: NameGen m => Domain () Expression -> m (AbstractPattern, Expression)
672 quantifiedVarOverDomain domain = do
673 nm <- nextName "q"
674 let pat = Single nm
675 ref = Reference nm (Just (InComprehension (GenDomainNoRepr (Single nm) domain)))
676 return (pat, ref)
677
678 -- | generate a fresh name for an auxiliary variable.
679 -- fst: the name to be used when declaring the variable
680 -- snd: the expression to be used everywhere else
681 auxiliaryVar :: NameGen m => m (Name, Expression)
682 auxiliaryVar = do
683 -- Savile Row has a bug which is triggered when there are variables with names of the form aux*
684 nm <- nextName "conjure_aux"
685 let ref = Reference nm Nothing
686 return (nm, ref)
687
688
689 -- | pattern, template, argument, result
690 lambdaToFunction :: AbstractPattern -> Expression -> Expression -> Expression
691 lambdaToFunction (Single nm) body = \ p ->
692 let
693 replacer :: Expression -> Expression
694 replacer (Reference n _) | n == nm = p
695 replacer x = x
696 in
697 transform replacer body
698 lambdaToFunction (AbsPatTuple ts) body = \ p ->
699 let
700 unroll :: [AbstractPattern] -> [Expression] -> Expression -> Expression
701 unroll [] [] b = b
702 unroll (pat:pats) (val:vals) b = unroll pats vals (lambdaToFunction pat b val)
703 unroll _ _ _ = bug "lambdaToFunction, AbsPatTuple, unroll"
704
705 ps :: [Expression]
706 ps = case p of
707 Constant (ConstantAbstract (AbsLitTuple xs)) -> map Constant xs
708 AbstractLiteral (AbsLitTuple xs) -> xs
709 _ -> [ Op (MkOpIndexing (OpIndexing p i))
710 | i' <- [ 1 .. genericLength ts ]
711 , let i = fromInt i'
712 ]
713 in
714 unroll ts ps body
715 lambdaToFunction (AbsPatMatrix ts) body = \ p ->
716 let
717 unroll :: [AbstractPattern] -> [Expression] -> Expression -> Expression
718 unroll [] [] b = b
719 unroll (pat:pats) (val:vals) b = unroll pats vals (lambdaToFunction pat b val)
720 unroll _ _ _ = bug "lambdaToFunction, AbsPatMatrix, unroll"
721
722 ps :: [Expression]
723 ps = case p of
724 Constant (ConstantAbstract (AbsLitMatrix _ xs)) -> map Constant xs
725 AbstractLiteral (AbsLitMatrix _ xs) -> xs
726 _ -> bug $ "lambdaToFunction, AbsPatMatrix" <++> vcat [pretty p, pretty (show p)]
727 in
728 unroll ts ps body
729 lambdaToFunction (AbsPatSet ts) body = \ p ->
730 let
731 unroll :: [AbstractPattern] -> [Expression] -> Expression -> Expression
732 unroll [] [] b = b
733 unroll (pat:pats) (val:vals) b = unroll pats vals (lambdaToFunction pat b val)
734 unroll _ _ _ = bug "lambdaToFunction, AbsPatSet, unroll"
735
736 ps :: [Expression]
737 ps = case p of
738 Constant (viewConstantSet -> Just xs) -> map Constant xs
739 AbstractLiteral (AbsLitSet xs) -> xs
740 _ -> bug $ "lambdaToFunction, AbsPatSet" <++> vcat [pretty p, pretty (show p)]
741 in
742 unroll ts ps body
743 lambdaToFunction p@AbstractPatternMetaVar{} _ = bug $ "Unsupported AbstractPattern, got" <+> pretty (show p)
744
745
746 ------------------------------------------------------------------------------------------------------------------------
747 -- ReferenceTo ---------------------------------------------------------------------------------------------------------
748 ------------------------------------------------------------------------------------------------------------------------
749
750 data ReferenceTo
751 = Alias Expression
752 | InComprehension Generator
753 | DeclNoRepr FindOrGiven Name (Domain () Expression)
754 Region -- the region of this reference
755 -- references with the same region identifier will get the same representation
756 | DeclHasRepr FindOrGiven Name (Domain HasRepresentation Expression)
757 | RecordField Name Type -- the type of the field with this name
758 | VariantField Name Type -- the type of the variant with this name
759 deriving (Eq, Ord, Show, Data, Typeable, Generic)
760
761 instance Serialize ReferenceTo
762 instance Hashable ReferenceTo
763 instance ToJSON ReferenceTo where toJSON = genericToJSON jsonOptions
764 instance FromJSON ReferenceTo where parseJSON = genericParseJSON jsonOptions
765
766 instance Pretty ReferenceTo where
767 pretty (Alias x) = "an alias for" <++> pretty x
768 pretty (InComprehension gen) = "a comprehension generator" <++> pretty gen
769 pretty (DeclNoRepr forg nm dom _) = "declaration of" <++> pretty forg <+> pretty nm <> ":" <+> pretty dom
770 pretty (DeclHasRepr forg nm dom ) = "declaration of" <++> pretty forg <+> pretty nm <> ":" <+> pretty dom
771 pretty (RecordField nm ty) = "record field" <++> prParens (pretty nm <+> ":" <+> pretty ty)
772 pretty (VariantField nm ty) = "variant field" <++> prParens (pretty nm <+> ":" <+> pretty ty)
773
774 data Region
775 = NoRegion
776 | Region Int
777 deriving (Eq, Ord, Show, Data, Typeable, Generic)
778
779 instance Serialize Region
780 instance Hashable Region
781 instance ToJSON Region where toJSON = genericToJSON jsonOptions
782 instance FromJSON Region where parseJSON = genericParseJSON jsonOptions
783
784
785 ------------------------------------------------------------------------------------------------------------------------
786 -- AbstractPattern -----------------------------------------------------------------------------------------------------
787 ------------------------------------------------------------------------------------------------------------------------
788
789 data AbstractPattern
790 = Single Name
791 | AbsPatTuple [AbstractPattern]
792 | AbsPatMatrix
793 -- (Domain () a) -- TODO: Should there be a domain here?
794 [AbstractPattern]
795 | AbsPatSet [AbstractPattern]
796 -- | AbsPatMSet [a]
797 -- | AbsPatFunction [(a, a)]
798 -- | AbsPatRelation [[a]]
799 -- | AbsPatPartition [[a]]
800 -- TODO: Consider introducing the above as abstract patterns...
801 | AbstractPatternMetaVar String
802 deriving (Eq, Ord, Show, Data, Typeable, Generic)
803
804 instance Serialize AbstractPattern
805 instance Hashable AbstractPattern
806 instance ToJSON AbstractPattern where toJSON = genericToJSON jsonOptions
807 instance FromJSON AbstractPattern where parseJSON = genericParseJSON jsonOptions
808
809 instance Pretty AbstractPattern where
810 pretty (Single nm) = pretty nm
811 pretty (AbsPatTuple xs) = (if length xs <= 1 then "tuple" else prEmpty) <>
812 prettyList prParens "," xs
813 pretty (AbsPatMatrix xs) = prettyList prBrackets "," xs
814 pretty (AbsPatSet xs) = prettyList prBraces "," xs
815 pretty (AbstractPatternMetaVar s) = "&" <> pretty s
816
817 instance VarSymBreakingDescription AbstractPattern where
818 varSymBreakingDescription (Single nm) = toJSON nm
819 varSymBreakingDescription (AbsPatTuple xs) = JSON.Object $ KM.fromList
820 [ ("type", JSON.String "AbsPatTuple")
821 , ("children", JSON.Array $ V.fromList $ map varSymBreakingDescription xs)
822 ]
823 varSymBreakingDescription (AbsPatMatrix xs) = JSON.Object $ KM.fromList
824 [ ("type", JSON.String "AbsPatMatrix")
825 , ("children", JSON.Array $ V.fromList $ map varSymBreakingDescription xs)
826 ]
827 varSymBreakingDescription (AbsPatSet xs) = JSON.Object $ KM.fromList
828 [ ("type", JSON.String "AbsPatSet")
829 , ("children", JSON.Array $ V.fromList $ map varSymBreakingDescription xs)
830 , ("symmetricChildren", JSON.Bool True)
831 ]
832 varSymBreakingDescription (AbstractPatternMetaVar s) = JSON.Object $ KM.fromList
833 [ ("type", JSON.String "AbstractPatternMetaVar")
834 , ("name", JSON.String (stringToText s))
835 ]
836
837
838 patternToExpr :: AbstractPattern -> Expression
839 patternToExpr (Single nm) = Reference nm Nothing
840 patternToExpr (AbsPatTuple ts) = AbstractLiteral $ AbsLitTuple $ map patternToExpr ts
841 patternToExpr (AbsPatMatrix ts) = AbstractLiteral $ AbsLitMatrix
842 (DomainInt TagInt [RangeBounded 1 (fromInt (genericLength ts))])
843 $ map patternToExpr ts
844 patternToExpr (AbsPatSet ts) = AbstractLiteral $ AbsLitSet $ map patternToExpr ts
845 patternToExpr AbstractPatternMetaVar{} = bug "patternToExpr"
846
847 ------------------------------------------------------------------------------------------------------------------------
848 -- Generator -----------------------------------------------------------------------------------------------------------
849 ------------------------------------------------------------------------------------------------------------------------
850
851 data GeneratorOrCondition
852 = Generator Generator
853 | Condition Expression
854 | ComprehensionLetting AbstractPattern Expression
855 deriving (Eq, Ord, Show, Data, Typeable, Generic)
856
857 instance Pretty GeneratorOrCondition where
858 pretty (Generator x) = pretty x
859 pretty (Condition x) = pretty x
860 pretty (ComprehensionLetting n x) = "letting" <+> pretty n <+> "be" <+> pretty x
861
862 instance VarSymBreakingDescription GeneratorOrCondition where
863 varSymBreakingDescription (Generator x) = JSON.Object $ KM.fromList
864 [ ("type", JSON.String "Generator")
865 , ("child", varSymBreakingDescription x)
866 ]
867 varSymBreakingDescription (Condition x) = JSON.Object $ KM.fromList
868 [ ("type", JSON.String "Condition")
869 , ("child", varSymBreakingDescription x)
870 ]
871 varSymBreakingDescription (ComprehensionLetting n x) = JSON.Object $ KM.fromList
872 [ ("type", JSON.String "ComprehensionLetting")
873 , ("children", JSON.Array $ V.fromList [toJSON n, varSymBreakingDescription x])
874 ]
875
876 instance Serialize GeneratorOrCondition
877 instance Hashable GeneratorOrCondition
878 instance ToJSON GeneratorOrCondition where toJSON = genericToJSON jsonOptions
879 instance FromJSON GeneratorOrCondition where parseJSON = genericParseJSON jsonOptions
880
881
882 data Generator
883 = GenDomainNoRepr AbstractPattern (Domain () Expression)
884 | GenDomainHasRepr Name (Domain HasRepresentation Expression)
885 | GenInExpr AbstractPattern Expression
886 deriving (Eq, Ord, Show, Data, Typeable, Generic)
887
888 instance Pretty Generator where
889 pretty (GenDomainNoRepr pat x) = pretty pat <+> ":" <+> pretty x
890 pretty (GenDomainHasRepr pat x) = pretty pat <+> ":" <+> pretty x
891 pretty (GenInExpr pat x) = pretty pat <+> "<-" <+> pretty x
892
893 instance VarSymBreakingDescription Generator where
894 varSymBreakingDescription (GenDomainNoRepr pat x) = JSON.Object $ KM.fromList
895 [ ("type", JSON.String "GenDomainNoRepr")
896 , ("pattern", varSymBreakingDescription pat)
897 , ("generator", varSymBreakingDescription x)
898 ]
899 varSymBreakingDescription (GenDomainHasRepr pat x) = JSON.Object $ KM.fromList
900 [ ("type", JSON.String "GenDomainHasRepr")
901 , ("pattern", toJSON pat)
902 , ("generator", varSymBreakingDescription x)
903 ]
904 varSymBreakingDescription (GenInExpr pat x) = JSON.Object $ KM.fromList
905 [ ("type", JSON.String "GenInExpr")
906 , ("pattern", varSymBreakingDescription pat)
907 , ("generator", varSymBreakingDescription x)
908 ]
909
910 instance Serialize Generator
911 instance Hashable Generator
912 instance ToJSON Generator where toJSON = genericToJSON jsonOptions
913 instance FromJSON Generator where parseJSON = genericParseJSON jsonOptions
914
915 generatorPat :: Generator -> AbstractPattern
916 generatorPat (GenDomainNoRepr pat _) = pat
917 generatorPat (GenDomainHasRepr pat _) = Single pat
918 generatorPat (GenInExpr pat _) = pat
919
920
921 ------------------------------------------------------------------------------------------------------------------------
922 -- Misc ---------------------------------------------------------------------------------------------------------------
923 ------------------------------------------------------------------------------------------------------------------------
924
925 tupleLitIfNeeded :: [Expression] -> Expression
926 tupleLitIfNeeded [] = bug "tupleLitIfNeeded []"
927 tupleLitIfNeeded [x] = x
928 tupleLitIfNeeded xs = AbstractLiteral (AbsLitTuple xs)
929
930 nbUses :: Data x => Name -> x -> Int
931 nbUses nm here = length [ () | Reference nm2 _ <- universeBi here, nm == nm2 ]
932
933 emptyCollectionX :: Expression -> Bool
934 emptyCollectionX (Constant x) = emptyCollection x
935 emptyCollectionX (AbstractLiteral x) = emptyCollectionAbsLit x
936 emptyCollectionX (Typed x _) = emptyCollectionX x
937 emptyCollectionX _ = False
938
939
940 isDomainExpr :: MonadFailDoc m => Expression -> m ()
941 isDomainExpr Domain{} = return ()
942 isDomainExpr x = na ("Not a domain expression: " <+> pretty x)