git.iko.soy/Idris-dev
on master help sign in
Fix optimisation IBC stuff.
405fa1eMatus Tejiscak
src/Idris/ElabDecls.hs+5−4
compare with master
unifiedsplit
@@ -284,7 +284,6 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
284 checkDocs fc argDocs t_in
284 checkDocs fc argDocs t_in
285 addDocStr n doc argDocs
285 addDocStr n doc argDocs
286 addIBC (IBCDoc n)
286 addIBC (IBCDoc n)
287− addIBC (IBCOpt n)
288 let metainf = DataMI params
287 let metainf = DataMI params
289 addIBC (IBCMetaInformation n metainf)
288 addIBC (IBCMetaInformation n metainf)
290 -- TMP HACK! Make this a data option
289 -- TMP HACK! Make this a data option
@@ -293,13 +292,15 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
293 updateContext (setMetaInformation n metainf)
292 updateContext (setMetaInformation n metainf)
294 mapM_ (checkPositive n) cons
293 mapM_ (checkPositive n) cons
295
294
295+ -- if there's exactly one constructor, mark both the type and the constructor
296 case cons of
296 case cons of
297 [(cn,ct)] -> setDetaggable cn >> setDetaggable n
297 [(cn,ct)] -> setDetaggable cn >> setDetaggable n
298+ >> addIBC (IBCOpt cn) >> addIBC (IBCOpt n)
298 _ -> return ()
299 _ -> return ()
299
300
301+ -- create an eliminator
300− if DefaultEliminator `elem` opts
302+ when (DefaultEliminator `elem` opts) $
301− then evalStateT (elabEliminator params n t dcons info) Map.empty
303+ evalStateT (elabEliminator params n t dcons info) Map.empty
302− else return ()
303 where
304 where
304 setDetaggable :: Name -> Idris ()
305 setDetaggable :: Name -> Idris ()
305 setDetaggable n = do
306 setDetaggable n = do