never executed always true always false
1 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
2
3 module Conjure.Language.Instantiate
4 ( instantiateExpression
5 , instantiateDomain
6 , trySimplify
7 , entailed
8 ) where
9
10 -- conjure
11 import Conjure.Prelude
12 import Conjure.Bug
13 import Conjure.UserError
14 import Conjure.Language.Definition
15 import Conjure.Language.Expression.Op
16 import Conjure.Language.Domain
17 import Conjure.Language.Constant
18 import Conjure.Language.Type
19 import Conjure.Language.TypeOf
20 import Conjure.Language.Pretty
21 import Conjure.Language.EvaluateOp ( evaluateOp )
22 import Conjure.Process.Enumerate ( EnumerateDomain, enumerateDomain, enumerateInConstant )
23
24
25 -- | Try to simplify an expression recursively.
26 trySimplify ::
27 MonadUserError m =>
28 EnumerateDomain m =>
29 NameGen m =>
30 (?typeCheckerMode :: TypeCheckerMode) =>
31 [(Name, Expression)] -> Expression -> m Expression
32 trySimplify ctxt x = do
33 res <- runMaybeT $ instantiateExpression ctxt x
34 case res of
35 Just c -- if the expression can be evaluated into a Constant
36 | null [() | ConstantUndefined{} <- universe c] -- and if it doesn't contain undefined's in it
37 -> return (Constant c) -- evaluate to the constant
38 _ -> descendM (trySimplify ctxt) x -- otherwise, try the same on its children
39
40
41 instantiateExpression ::
42 MonadFailDoc m =>
43 EnumerateDomain m =>
44 NameGen m =>
45 (?typeCheckerMode :: TypeCheckerMode) =>
46 [(Name, Expression)] -> Expression -> m Constant
47 instantiateExpression ctxt x = do
48 constant <- normaliseConstant <$> evalStateT (instantiateE x) ctxt
49 case (emptyCollection constant, constant) of
50 (_, TypedConstant{}) -> return constant
51 (True, _) -> do
52 ty <- typeOf x
53 return (TypedConstant constant ty)
54 (False, _) -> return constant
55
56
57 instantiateDomain ::
58 MonadFailDoc m =>
59 EnumerateDomain m =>
60 NameGen m =>
61 Pretty r =>
62 Default r =>
63 (?typeCheckerMode :: TypeCheckerMode) =>
64 [(Name, Expression)] -> Domain r Expression -> m (Domain r Constant)
65 instantiateDomain ctxt x = normaliseDomain normaliseConstant <$> evalStateT (instantiateD x) ctxt
66
67
68 newtype HasUndef = HasUndef Any
69 deriving (Semigroup, Monoid)
70
71 instantiateE ::
72 MonadFailDoc m =>
73 MonadState [(Name, Expression)] m =>
74 EnumerateDomain m =>
75 NameGen m =>
76 (?typeCheckerMode :: TypeCheckerMode) =>
77 Expression -> m Constant
78 instantiateE (Comprehension body gensOrConds) = do
79 let
80 loop ::
81 MonadFailDoc m =>
82 MonadState [(Name, Expression)] m =>
83 EnumerateDomain m =>
84 NameGen m =>
85 [GeneratorOrCondition] -> WriterT HasUndef m [Constant]
86 loop [] = return <$> instantiateE body
87 loop (Generator (GenDomainNoRepr pat domain) : rest) = do
88 DomainInConstant domainConstant <- instantiateE (Domain domain)
89 let undefinedsInsideTheDomain =
90 [ und
91 | und@ConstantUndefined{} <- universeBi domainConstant
92 ]
93 if null undefinedsInsideTheDomain
94 then do
95 enumeration <- enumerateDomain domainConstant
96 concatMapM
97 (\ val -> scope $ do
98 valid <- bind pat val
99 if valid
100 then loop rest
101 else return [] )
102 enumeration
103 else do
104 tell (HasUndef (Any True))
105 return []
106 loop (Generator (GenDomainHasRepr pat domain) : rest) =
107 loop (Generator (GenDomainNoRepr (Single pat) (forgetRepr domain)) : rest)
108 loop (Generator (GenInExpr pat expr) : rest) = do
109 exprConstant <- instantiateE expr
110 enumeration <- enumerateInConstant exprConstant
111 concatMapM
112 (\ val -> scope $ do
113 valid <- bind pat val
114 if valid
115 then loop rest
116 else return [] )
117 enumeration
118 loop (Condition expr : rest) = do
119 constant <- instantiateE expr
120 if constant == ConstantBool True
121 then loop rest
122 else return []
123 loop (ComprehensionLetting pat expr : rest) = do
124 constant <- instantiateE expr
125 valid <- bind pat constant
126 unless valid (bug "ComprehensionLetting.bind expected to be valid")
127 loop rest
128
129
130 (constants, HasUndef (Any undefinedsInsideGeneratorDomains)) <- runWriterT (loop gensOrConds)
131 if undefinedsInsideGeneratorDomains
132 then do
133 ty <- typeOf (Comprehension body gensOrConds)
134 return $ ConstantUndefined
135 "Comprehension contains undefined values inside generator domains."
136 ty
137 else
138 return $ ConstantAbstract $ AbsLitMatrix
139 (DomainInt TagInt [RangeBounded 1 (fromInt (genericLength constants))])
140 constants
141
142 instantiateE (Reference name (Just (RecordField _ ty))) = return $ ConstantField name ty
143 instantiateE (Reference name (Just (VariantField _ ty))) = return $ ConstantField name ty
144 instantiateE (Reference name refto) = do
145 ctxt <- gets id
146 case name `lookup` ctxt of
147 Just x -> instantiateE x
148 Nothing ->
149 case refto of
150 Just (Alias x) ->
151 -- we do not have this name in context, but we have it stored in the Reference itself
152 -- reuse that
153 instantiateE x
154 _ ->
155 failDoc $ vcat
156 $ ("No value for:" <+> pretty name)
157 : "Bindings in context:"
158 : prettyContext ctxt
159
160 instantiateE (Constant c) = return c
161 instantiateE (AbstractLiteral lit) = instantiateAbsLit lit
162 instantiateE (Typed x ty) = TypedConstant <$> instantiateE x <*> pure ty
163 instantiateE (Op op) = instantiateOp op
164
165 -- "Domain () Expression"s inside expressions are handled specially
166 instantiateE (Domain (DomainReference _ (Just d))) = instantiateE (Domain d)
167 instantiateE (Domain (DomainReference name Nothing)) = do
168 ctxt <- gets id
169 case name `lookup` ctxt of
170 Just (Domain d) -> instantiateE (Domain d)
171 _ -> failDoc $ vcat
172 $ ("No value for:" <+> pretty name)
173 : "Bindings in context:"
174 : prettyContext ctxt
175 instantiateE (Domain domain) = DomainInConstant <$> instantiateD domain
176
177 instantiateE (WithLocals b (AuxiliaryVars locals)) = do
178 forM_ locals $ \ local -> case local of
179 SuchThat xs -> forM_ xs $ \ x -> do
180 constant <- instantiateE x
181 case constant of
182 ConstantBool True -> return ()
183 _ -> failDoc $ "local:" <+> pretty constant
184 _ -> failDoc $ "local:" <+> pretty local
185 instantiateE b
186
187 instantiateE (WithLocals b (DefinednessConstraints locals)) = do
188 forM_ locals $ \ x -> do
189 constant <- instantiateE x
190 case constant of
191 ConstantBool True -> return ()
192 _ -> failDoc $ "local:" <+> pretty constant
193 instantiateE b
194
195 instantiateE x = failDoc $ "instantiateE:" <+> pretty (show x)
196
197
198 instantiateOp ::
199 MonadFailDoc m =>
200 MonadState [(Name, Expression)] m =>
201 EnumerateDomain m =>
202 NameGen m =>
203 (?typeCheckerMode :: TypeCheckerMode) =>
204 Op Expression -> m Constant
205 instantiateOp opx = mapM instantiateE opx >>= evaluateOp . fmap normaliseConstant
206
207
208 instantiateAbsLit ::
209 MonadFailDoc m =>
210 MonadState [(Name, Expression)] m =>
211 EnumerateDomain m =>
212 NameGen m =>
213 (?typeCheckerMode :: TypeCheckerMode) =>
214 AbstractLiteral Expression -> m Constant
215 instantiateAbsLit x = do
216 c <- mapM instantiateE x
217 case c of
218 -- for functions, if the same thing is mapped to multiple values, the result is undefined
219 AbsLitFunction vals -> do
220 let nubVals = sortNub vals
221 if length (sortNub (map fst nubVals)) == length nubVals
222 then return $ ConstantAbstract $ AbsLitFunction nubVals
223 else do
224 ty <- typeOf c
225 return $ ConstantUndefined "Multiple mappings for the same value." ty
226 _ -> return $ ConstantAbstract c
227
228
229 instantiateD ::
230 MonadFailDoc m =>
231 MonadState [(Name, Expression)] m =>
232 EnumerateDomain m =>
233 NameGen m =>
234 Pretty r =>
235 Default r =>
236 (?typeCheckerMode :: TypeCheckerMode) =>
237 Domain r Expression -> m (Domain r Constant)
238 instantiateD (DomainAny t ty) = return (DomainAny t ty)
239 instantiateD DomainBool = return DomainBool
240 instantiateD (DomainIntE x) = do
241 x' <- instantiateE x
242 let vals = case (x', viewConstantMatrix x', viewConstantSet x') of
243 (ConstantInt{}, _, _) -> [x']
244 (_, Just (_, xs), _) -> xs
245 (_, _, Just xs) -> xs
246 _ -> []
247 return (DomainInt TagInt (map RangeSingle vals))
248 instantiateD (DomainInt t ranges) = DomainInt t <$> mapM instantiateR ranges
249 instantiateD (DomainEnum nm Nothing _) = do
250 st <- gets id
251 case lookup nm st of
252 Just (Domain dom) -> instantiateD (defRepr dom)
253 Just _ -> failDoc $ ("DomainEnum not found in state, Just:" <+> pretty nm) <++> vcat (map pretty st)
254 Nothing -> failDoc $ ("DomainEnum not found in state, Nothing:" <+> pretty nm) <++> vcat (map pretty st)
255 instantiateD (DomainEnum nm rs0 _) = do
256 let fmap4 = fmap . fmap . fmap . fmap
257 let e2c' x = either bug id (e2c x)
258 rs <- transformBiM (fmap Constant . instantiateE ) (rs0 :: Maybe [Range Expression])
259 |> fmap4 e2c'
260 st <- gets id
261 mp <- forM (universeBi rs :: [Name]) $ \ n -> case lookup n st of
262 Just (Constant (ConstantInt _ i)) -> return (n, i)
263 Nothing -> failDoc $ "No value for member of enum domain:" <+> pretty n
264 Just c -> failDoc $ vcat [ "Incompatible value for member of enum domain:" <+> pretty nm
265 , " Looking up for member:" <+> pretty n
266 , " Expected an integer, but got:" <+> pretty c
267 ]
268 return (DomainEnum nm (rs :: Maybe [Range Constant]) (Just mp))
269 instantiateD (DomainUnnamed nm s) = DomainUnnamed nm <$> instantiateE s
270 instantiateD (DomainTuple inners) = DomainTuple <$> mapM instantiateD inners
271 instantiateD (DomainRecord inners) = DomainRecord <$> sequence [ do d' <- instantiateD d ; return (n,d')
272 | (n,d) <- inners ]
273 instantiateD (DomainVariant inners) = DomainVariant <$> sequence [ do d' <- instantiateD d ; return (n,d')
274 | (n,d) <- inners ]
275 instantiateD (DomainMatrix index inner) = DomainMatrix <$> instantiateD index <*> instantiateD inner
276 instantiateD (DomainSet r attrs inner) = DomainSet r <$> instantiateSetAttr attrs <*> instantiateD inner
277 instantiateD (DomainMSet r attrs inner) = DomainMSet r <$> instantiateMSetAttr attrs <*> instantiateD inner
278 instantiateD (DomainFunction r attrs innerFr innerTo) = DomainFunction r <$> instantiateFunctionAttr attrs <*> instantiateD innerFr <*> instantiateD innerTo
279 instantiateD (DomainSequence r attrs inner) = DomainSequence r <$> instantiateSequenceAttr attrs <*> instantiateD inner
280 instantiateD (DomainRelation r attrs inners) = DomainRelation r <$> instantiateRelationAttr attrs <*> mapM instantiateD inners
281 instantiateD (DomainPartition r attrs inner) = DomainPartition r <$> instantiatePartitionAttr attrs <*> instantiateD inner
282 instantiateD (DomainOp nm ds) = DomainOp nm <$> mapM instantiateD ds
283 instantiateD (DomainReference _ (Just d)) = instantiateD d
284 instantiateD (DomainReference name Nothing) = do
285 ctxt <- gets id
286 case name `lookup` ctxt of
287 Just (Domain d) -> instantiateD (defRepr d)
288 _ -> failDoc $ vcat
289 $ ("No value for:" <+> pretty name)
290 : "Bindings in context:"
291 : prettyContext ctxt
292 instantiateD DomainMetaVar{} = bug "instantiateD DomainMetaVar"
293
294
295 instantiateSetAttr ::
296 MonadFailDoc m =>
297 MonadState [(Name, Expression)] m =>
298 EnumerateDomain m =>
299 NameGen m =>
300 (?typeCheckerMode :: TypeCheckerMode) =>
301 SetAttr Expression -> m (SetAttr Constant)
302 instantiateSetAttr (SetAttr s) = SetAttr <$> instantiateSizeAttr s
303
304
305 instantiateSizeAttr ::
306 MonadFailDoc m =>
307 MonadState [(Name, Expression)] m =>
308 EnumerateDomain m =>
309 NameGen m =>
310 (?typeCheckerMode :: TypeCheckerMode) =>
311 SizeAttr Expression -> m (SizeAttr Constant)
312 instantiateSizeAttr SizeAttr_None = return SizeAttr_None
313 instantiateSizeAttr (SizeAttr_Size x) = SizeAttr_Size <$> instantiateE x
314 instantiateSizeAttr (SizeAttr_MinSize x) = SizeAttr_MinSize <$> instantiateE x
315 instantiateSizeAttr (SizeAttr_MaxSize x) = SizeAttr_MaxSize <$> instantiateE x
316 instantiateSizeAttr (SizeAttr_MinMaxSize x y) = SizeAttr_MinMaxSize <$> instantiateE x <*> instantiateE y
317
318
319 instantiateMSetAttr ::
320 MonadFailDoc m =>
321 MonadState [(Name, Expression)] m =>
322 EnumerateDomain m =>
323 NameGen m =>
324 (?typeCheckerMode :: TypeCheckerMode) =>
325 MSetAttr Expression -> m (MSetAttr Constant)
326 instantiateMSetAttr (MSetAttr s o) = MSetAttr <$> instantiateSizeAttr s <*> instantiateOccurAttr o
327
328
329 instantiateOccurAttr ::
330 MonadFailDoc m =>
331 MonadState [(Name, Expression)] m =>
332 EnumerateDomain m =>
333 NameGen m =>
334 (?typeCheckerMode :: TypeCheckerMode) =>
335 OccurAttr Expression -> m (OccurAttr Constant)
336 instantiateOccurAttr OccurAttr_None = return OccurAttr_None
337 instantiateOccurAttr (OccurAttr_MinOccur x) = OccurAttr_MinOccur <$> instantiateE x
338 instantiateOccurAttr (OccurAttr_MaxOccur x) = OccurAttr_MaxOccur <$> instantiateE x
339 instantiateOccurAttr (OccurAttr_MinMaxOccur x y) = OccurAttr_MinMaxOccur <$> instantiateE x <*> instantiateE y
340
341
342 instantiateFunctionAttr ::
343 MonadFailDoc m =>
344 MonadState [(Name, Expression)] m =>
345 EnumerateDomain m =>
346 NameGen m =>
347 (?typeCheckerMode :: TypeCheckerMode) =>
348 FunctionAttr Expression -> m (FunctionAttr Constant)
349 instantiateFunctionAttr (FunctionAttr s p j) =
350 FunctionAttr <$> instantiateSizeAttr s
351 <*> pure p
352 <*> pure j
353
354
355 instantiateSequenceAttr ::
356 MonadFailDoc m =>
357 MonadUserError m =>
358 MonadState [(Name, Expression)] m =>
359 EnumerateDomain m =>
360 NameGen m =>
361 (?typeCheckerMode :: TypeCheckerMode) =>
362 SequenceAttr Expression -> m (SequenceAttr Constant)
363 instantiateSequenceAttr (SequenceAttr s j) =
364 SequenceAttr <$> instantiateSizeAttr s
365 <*> pure j
366
367
368 instantiateRelationAttr ::
369 MonadFailDoc m =>
370 MonadUserError m =>
371 MonadState [(Name, Expression)] m =>
372 EnumerateDomain m =>
373 NameGen m =>
374 (?typeCheckerMode :: TypeCheckerMode) =>
375 RelationAttr Expression -> m (RelationAttr Constant)
376 instantiateRelationAttr (RelationAttr s b) = RelationAttr <$> instantiateSizeAttr s <*> pure b
377
378
379 instantiatePartitionAttr ::
380 MonadFailDoc m =>
381 MonadUserError m =>
382 MonadState [(Name, Expression)] m =>
383 EnumerateDomain m =>
384 NameGen m =>
385 (?typeCheckerMode :: TypeCheckerMode) =>
386 PartitionAttr Expression -> m (PartitionAttr Constant)
387 instantiatePartitionAttr (PartitionAttr a b r) =
388 PartitionAttr <$> instantiateSizeAttr a
389 <*> instantiateSizeAttr b
390 <*> pure r
391
392
393 instantiateR ::
394 MonadFailDoc m =>
395 MonadState [(Name, Expression)] m =>
396 EnumerateDomain m =>
397 NameGen m =>
398 (?typeCheckerMode :: TypeCheckerMode) =>
399 Range Expression -> m (Range Constant)
400 instantiateR RangeOpen = return RangeOpen
401 instantiateR (RangeSingle x) = RangeSingle <$> instantiateE x
402 instantiateR (RangeLowerBounded x) = RangeLowerBounded <$> instantiateE x
403 instantiateR (RangeUpperBounded x) = RangeUpperBounded <$> instantiateE x
404 instantiateR (RangeBounded x y) = RangeBounded <$> instantiateE x <*> instantiateE y
405
406
407 bind :: (Functor m, MonadState [(Name, Expression)] m)
408 => AbstractPattern
409 -> Constant
410 -> m Bool -- False means skip
411 bind (Single nm) val = modify ((nm, Constant val) :) >> return True
412 bind (AbsPatTuple pats) (viewConstantTuple -> Just vals)
413 | length pats == length vals = and <$> zipWithM bind pats vals
414 bind (AbsPatMatrix pats) (viewConstantMatrix -> Just (_, vals))
415 | length pats == length vals = and <$> zipWithM bind pats vals
416 bind (AbsPatSet pats) (viewConstantSet -> Just vals)
417 | length pats == length vals = and <$> zipWithM bind pats vals
418 | otherwise = return False
419 bind pat val = bug $ "Instantiate.bind:" <++> vcat ["pat:" <+> pretty pat, "val:" <+> pretty val]
420
421
422 -- check if the given expression can be evaluated to True
423 -- False means it is not entailed, as opposed to "it is known to be false"
424 entailed ::
425 MonadUserError m =>
426 EnumerateDomain m =>
427 NameGen m =>
428 (?typeCheckerMode :: TypeCheckerMode) =>
429 Expression -> m Bool
430 entailed x = do
431 -- traceM $ show $ "entailed x:" <+> pretty x
432 c <- trySimplify [] x
433 -- traceM $ show $ "entailed c:" <+> pretty c
434 case c of
435 Constant (ConstantBool True) -> return True
436 _ -> return False
437