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