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