never executed always true always false
1 {-# LANGUAGE TupleSections #-}
2 {-# LANGUAGE QuasiQuotes #-}
3
4 module Conjure.Language.NameResolution
5 ( resolveNames
6 , resolveNamesMulti
7 , resolveNamesX
8 , resolveX, resolveD -- actually internal, use with care
9 ) where
10
11 import Conjure.Prelude
12 import Data.Traversable (traverse)
13 import Conjure.Bug
14 import Conjure.UserError
15 import Conjure.Language.Definition
16 import Conjure.Language.Domain
17 ( changeRepr,
18 typeOfDomain,
19 Domain(DomainUnnamed, DomainReference, DomainRecord,
20 DomainVariant) )
21 import Conjure.Language.Constant
22 import Conjure.Language.Type
23 import Conjure.Language.Pretty
24 import Conjure.Language.TH
25
26
27
28 resolveNamesMulti ::
29 MonadLog m =>
30 MonadUserError m =>
31 NameGen m =>
32 (?typeCheckerMode :: TypeCheckerMode) =>
33 [Model] -> m [Model]
34 resolveNamesMulti = flip evalStateT [] . go
35 where
36 go [] = return []
37 go (m:ms) = (:) <$> resolveNames_ m <*> go ms
38
39 resolveNames ::
40 MonadLog m =>
41 MonadUserError m =>
42 NameGen m =>
43 (?typeCheckerMode :: TypeCheckerMode) =>
44 Model -> m Model
45 resolveNames = flip evalStateT [] . resolveNames_
46
47 resolveNames_ ::
48 MonadLog m =>
49 MonadState [(Name, ReferenceTo)] m =>
50 MonadUserError m =>
51 NameGen m =>
52 (?typeCheckerMode :: TypeCheckerMode) =>
53 Model -> m Model
54 resolveNames_ model = failToUserError $ do
55 statements <- mapM resolveStatement (mStatements model)
56 mapM_ check (universeBi statements)
57 return model { mStatements = toTaggedInt statements }
58
59 -- this is for when a name will shadow an already existing name that is outside of this expression
60 -- we rename the new names to avoid name shadowing
61 shadowing ::
62 MonadFailDoc m =>
63 MonadState [(Name, ReferenceTo)] m =>
64 NameGen m =>
65 Expression -> m Expression
66 shadowing p@(Comprehension _ is) = do
67 -- list of names originating from this comprehension
68 let generators = concat
69 [ names
70 | Generator gen <- is
71 , let pat = generatorPat gen
72 , let names = [ n | n@Name{} <- universeBi pat ]
73 ]
74 ctxt <- gets id
75 -- a subset of names originating from this comprehension that will shadow already existing names
76 let shadows = [ g | g <- generators, g `elem` map fst ctxt ]
77 shadowsNew <- forM shadows $ \ s -> do n <- nextName "shadow" ; return (s,n)
78 let f n = fromMaybe n (lookup n shadowsNew)
79 return (transformBi f p)
80 shadowing p = return p
81
82
83 addName ::
84 MonadState [(Name, ReferenceTo)] m =>
85 MonadUserError m =>
86 Name -> ReferenceTo -> m ()
87 addName (Name "_") _ = return ()
88 addName (Name "UNDERSCORE__") _ = return ()
89 addName n thing = do
90 ctxt <- gets id
91 let
92 allowed DeclNoRepr{} Alias{} = True -- needed when instantiating stuff
93 allowed DeclHasRepr{} Alias{} = True -- needed when instantiating stuff
94 allowed old new = old == new
95 let mdefined = [ thing' | (n', thing') <- ctxt, n == n' && not (allowed thing' thing) ]
96 case mdefined of
97 [] -> return ()
98 (thing':_) -> userErr1 $ vcat [ "Redefinition of name:" <+> pretty n
99 , "When trying to define it as" <+> pretty thing
100 , "It was already defined as" <+> pretty thing'
101 ]
102 modify ((n, thing) :)
103
104
105 resolveNamesX ::
106 MonadFailDoc m =>
107 MonadUserError m =>
108 NameGen m =>
109 (?typeCheckerMode :: TypeCheckerMode) =>
110 Expression -> m Expression
111 resolveNamesX x = do
112 x' <- evalStateT (resolveX x) []
113 mapM_ check (universe x')
114 return x'
115
116
117 toTaggedInt :: Data a => a -> a
118 toTaggedInt = transformBi f
119 where
120 f :: Type -> Type
121 f (TypeEnum (Name nm)) = TypeInt (TagEnum nm)
122 f ty = ty
123
124
125 check :: MonadFailDoc m => Expression -> m ()
126 check (Reference nm Nothing) = failDoc ("Undefined:" <+> pretty nm)
127 check _ = return ()
128
129
130 resolveStatement ::
131 MonadFailDoc m =>
132 MonadState [(Name, ReferenceTo)] m =>
133 MonadUserError m =>
134 NameGen m =>
135 (?typeCheckerMode :: TypeCheckerMode) =>
136 Statement -> m Statement
137 resolveStatement st =
138 case st of
139 Declaration decl ->
140 case decl of
141 FindOrGiven forg nm dom -> do
142 when (nm == Name "_") $ userErr1 "Cannot use _ as the name in a find/given statement."
143 dom' <- resolveD dom
144 addName nm $ DeclNoRepr forg nm dom' NoRegion
145 return (Declaration (FindOrGiven forg nm dom'))
146 Letting nm x -> do
147 when (nm == Name "_") $ userErr1 "Cannot use _ as the name in a letting statement."
148 x' <- resolveX x
149 addName nm $ Alias x'
150 return (Declaration (Letting nm x'))
151 LettingDomainDefnUnnamed nm x -> do
152 when (nm == Name "_") $ userErr1 "Cannot use _ as the name in a letting statement."
153 x' <- resolveX x
154 addName nm $ Alias (Domain (DomainUnnamed nm x'))
155 return (Declaration (LettingDomainDefnUnnamed nm x'))
156 LettingDomainDefnEnum (Name ename) nms -> do
157 when (ename == "_") $ userErr1 "Cannot use _ as the name in a letting statement."
158 sequence_ [ addName nm $ Alias (Constant (ConstantInt (TagEnum ename) i))
159 | (nm, i) <- zip nms [1..]
160 ]
161 return st
162 LettingDomainDefnEnum{} -> bug "resolveStatement, Name"
163 GivenDomainDefnEnum{} -> return st -- ignoring
164 SearchOrder xs -> SearchOrder <$> mapM resolveSearchOrder xs
165 SearchHeuristic nm -> do
166 let allowed = ["static", "sdf", "conflict", "srf", "ldf", "wdeg", "domoverwdeg"]
167 if nm `elem` allowed
168 then return (SearchHeuristic nm)
169 else userErr1 $ vcat [ "Invalid heuristic:" <+> pretty nm
170 , "Allowed values are:" <+> prettyList id "," allowed
171 ]
172 Where xs -> Where <$> mapM resolveX xs
173 Objective obj x -> Objective obj <$> resolveX x
174 SuchThat xs -> SuchThat <$> mapM resolveX xs
175
176
177 resolveSearchOrder ::
178 MonadFailDoc m =>
179 MonadState [(Name, ReferenceTo)] m =>
180 MonadUserError m =>
181 NameGen m =>
182 (?typeCheckerMode :: TypeCheckerMode) =>
183 SearchOrder -> m SearchOrder
184 resolveSearchOrder (BranchingOn nm) = do
185 ctxt <- gets id
186 mval <- gets (lookup nm)
187 case mval of
188 Nothing -> userErr1 $ vcat $ ("Undefined reference:" <+> pretty nm)
189 : ("Bindings in context:" : prettyContext ctxt)
190 Just{} -> return (BranchingOn nm)
191 resolveSearchOrder (Cut x) =
192 let f Find = CutFind
193 f forg = forg
194 in Cut . transformBi f <$> resolveX x
195
196
197 resolveX ::
198 MonadFailDoc m =>
199 MonadState [(Name, ReferenceTo)] m =>
200 MonadUserError m =>
201 NameGen m =>
202 (?typeCheckerMode :: TypeCheckerMode) =>
203 Expression -> m Expression
204 resolveX (Reference nm Nothing) = do
205 ctxt <- gets id
206 mval <- gets (lookup nm)
207 case mval of
208 Nothing -> userErr1 $ vcat $ ("Undefined reference:" <+> pretty nm)
209 : ("Bindings in context:" : prettyContext ctxt)
210 Just r -> return (Reference nm (Just r))
211
212 resolveX p@(Reference nm (Just refto)) = do -- this is for re-resolving
213 mval <- gets (lookup nm)
214 case mval of
215 Nothing -> return p -- hence, do not failDoc if not in the context
216 Just DeclNoRepr{} -- if the newly found guy doesn't have a repr
217 | DeclHasRepr{} <- refto -- but the old one did, do not update
218 -> return p
219 Just (DeclNoRepr forg_ nm_ dom_ _) -- if the newly found guy doesn't have a repr
220 | DeclNoRepr _ _ _ region <- refto -- and the old one didn't have one either
221 -- preserve the region information
222 -> return (Reference nm (Just (DeclNoRepr forg_ nm_ dom_ region)))
223 Just (Alias r) -> do
224 r' <- resolveX r
225 return (Reference nm (Just (Alias r')))
226 Just r ->
227 return (Reference nm (Just r))
228
229 resolveX (AbstractLiteral lit) = AbstractLiteral <$> resolveAbsLit lit
230
231 resolveX (Constant c) = Constant <$> resolveConstant c
232
233 resolveX (Domain x) = Domain <$> resolveD x
234
235 resolveX p@Comprehension{} = scope $ do
236 p' <- shadowing p
237 case p' of
238 Comprehension x is -> do
239 is' <- forM is $ \case
240 Generator gen -> do
241 (gen', refto) <- case gen of
242 GenDomainNoRepr pat dom -> do
243 dom' <- resolveD dom
244 let gen'' = GenDomainNoRepr pat dom'
245 return
246 ( gen''
247 , case pat of
248 Single nm' -> DeclNoRepr Quantified nm' dom' NoRegion
249 _ -> InComprehension gen''
250 )
251 GenDomainHasRepr nm dom -> do
252 dom' <- resolveD dom
253 return
254 ( GenDomainHasRepr nm dom'
255 , DeclHasRepr Quantified nm dom'
256 )
257 GenInExpr pat expr -> do
258 expr' <- resolveX expr
259 let gen'' = GenInExpr pat expr'
260 return ( gen'' , InComprehension gen'' )
261 forM_ (universeBi (generatorPat gen)) $ \ nm ->
262 addName nm refto
263 return (Generator gen')
264 Condition y -> Condition <$> resolveX y
265 ComprehensionLetting pat expr -> do
266 expr' <- resolveX expr
267 resolveAbsPat p pat expr'
268 return (ComprehensionLetting pat expr')
269 x' <- resolveX x
270 return (Comprehension x' is')
271 _ -> bug "NameResolution.resolveX.shadowing"
272
273 resolveX (WithLocals body (AuxiliaryVars locals)) = scope $ do
274 locals' <- mapM resolveStatement locals
275 body' <- resolveX body
276 return (WithLocals body' (AuxiliaryVars locals'))
277
278 resolveX (WithLocals body (DefinednessConstraints locals)) = scope $ do
279 locals' <- mapM resolveX locals
280 body' <- resolveX body
281 return (WithLocals body' (DefinednessConstraints locals'))
282
283 resolveX x = descendM resolveX x
284
285
286 resolveD ::
287 MonadFailDoc m =>
288 MonadState [(Name, ReferenceTo)] m =>
289 MonadUserError m =>
290 NameGen m =>
291 Data r =>
292 Default r =>
293 Pretty r =>
294 (?typeCheckerMode :: TypeCheckerMode) =>
295 Domain r Expression -> m (Domain r Expression)
296 resolveD (DomainReference nm (Just d)) = DomainReference nm . Just <$> resolveD d
297 resolveD (DomainReference nm Nothing) = do
298 mval <- gets (lookup nm)
299 case mval of
300 Nothing -> userErr1 ("Undefined reference to a domain:" <+> pretty nm)
301 Just (Alias (Domain r)) -> DomainReference nm . Just <$> resolveD (changeRepr def r)
302 Just x -> userErr1 ("Expected a domain, but got an expression:" <+> pretty x)
303 resolveD (DomainRecord ds) = fmap DomainRecord $ forM ds $ \ (n, d) -> do
304 d' <- resolveD d
305 t <- typeOfDomain d'
306 addName n $ RecordField n t
307 return (n, d')
308 resolveD (DomainVariant ds) = fmap DomainVariant $ forM ds $ \ (n, d) -> do
309 d' <- resolveD d
310 t <- typeOfDomain d'
311 addName n $ VariantField n t
312 return (n, d')
313 resolveD d = do
314 d' <- descendM resolveD d
315 mapM resolveX d'
316
317
318 resolveAbsPat ::
319 MonadState [(Name, ReferenceTo)] m =>
320 MonadUserError m =>
321 Expression -> AbstractPattern -> Expression -> m ()
322 resolveAbsPat _ AbstractPatternMetaVar{} _ = bug "resolveAbsPat AbstractPatternMetaVar"
323 resolveAbsPat _ (Single nm) x = addName nm $ Alias x
324 resolveAbsPat context (AbsPatTuple ps) x =
325 sequence_ [ resolveAbsPat context p [essence| &x[&i] |]
326 | (p, i_) <- zip ps allNats
327 , let i = fromInt i_
328 ]
329 resolveAbsPat context (AbsPatMatrix ps) x =
330 sequence_ [ resolveAbsPat context p [essence| &x[&i] |]
331 | (p, i_) <- zip ps allNats
332 , let i = fromInt i_
333 ]
334 resolveAbsPat context (AbsPatSet ps) x = do
335 ys <- case x of
336 Constant (viewConstantSet -> Just xs) -> return (map Constant xs)
337 AbstractLiteral (AbsLitSet xs) -> return xs
338 _ -> userErr1 $ "Abstract set pattern cannot be used in this context:" <++> pretty context
339 sequence_ [ resolveAbsPat context p y
340 | (p,y) <- zip ps ys
341 ]
342
343
344 resolveAbsLit ::
345 MonadFailDoc m =>
346 MonadState [(Name, ReferenceTo)] m =>
347 MonadUserError m =>
348 NameGen m =>
349 (?typeCheckerMode :: TypeCheckerMode) =>
350 AbstractLiteral Expression -> m (AbstractLiteral Expression)
351 resolveAbsLit (AbsLitVariant Nothing n x) = do
352 x' <- resolveX x
353 mval <- gets id
354 let
355 isTheVariant (Alias (Domain d@(DomainVariant nms))) | Just{} <- lookup n nms = Just d
356 isTheVariant _ = Nothing
357 case mapMaybe (isTheVariant . snd) mval of
358 (DomainVariant dom:_) -> return (AbsLitVariant (Just dom) n x')
359 _ -> return (AbsLitVariant Nothing n x')
360 resolveAbsLit (AbsLitVariant (Just doms) n x) = do
361 doms' <- forM doms $ \ (nm, d) -> (nm,) <$> resolveD d
362 x' <- resolveX x
363 return $ AbsLitVariant (Just doms') n x'
364 resolveAbsLit (AbsLitMatrix ind xs) = do
365 ind' <- resolveD ind
366 xs' <- mapM resolveX xs
367 return $ AbsLitMatrix ind' xs'
368 resolveAbsLit lit = (descendBiM resolveX >=> descendBiM resolveD') lit
369 where
370 resolveD' d = resolveD (d :: Domain () Expression)
371
372
373 resolveConstant ::
374 MonadFailDoc m =>
375 MonadState [(Name, ReferenceTo)] m =>
376 MonadUserError m =>
377 NameGen m =>
378 (?typeCheckerMode :: TypeCheckerMode) =>
379 Constant -> m Constant
380 resolveConstant (ConstantAbstract (AbsLitMatrix ind xs))
381 | hasUnresolvedDomainReference ind = do
382 ind' <- resolveDConstant ind
383 return $ ConstantAbstract $ AbsLitMatrix ind' xs
384 resolveConstant (TypedConstant c ty) = TypedConstant <$> resolveConstant c <*> pure ty
385 resolveConstant c = return c
386
387 hasUnresolvedDomainReference :: Domain () a -> Bool
388 hasUnresolvedDomainReference (DomainReference _ Nothing) = True
389 hasUnresolvedDomainReference _ = False
390
391 resolveDConstant ::
392 MonadFailDoc m =>
393 MonadState [(Name, ReferenceTo)] m =>
394 MonadUserError m =>
395 NameGen m =>
396 (?typeCheckerMode :: TypeCheckerMode) =>
397 Domain () Constant -> m (Domain () Constant)
398 resolveDConstant (DomainReference nm (Just d)) =
399 DomainReference nm . Just <$> resolveDConstant d
400 resolveDConstant (DomainReference nm Nothing) = do
401 mval <- gets (lookup nm)
402 case mval of
403 Nothing -> userErr1 ("Undefined reference to a domain:" <+> pretty nm)
404 Just (Alias (Domain r)) -> do
405 r' <- resolveD (changeRepr def r)
406 traverse e2c r'
407 Just x -> userErr1 ("Expected a domain, but got an expression:" <+> pretty x)
408 resolveDConstant d = return d