git.iko.soy/Idris-dev
on master help sign in
Add detaggability recognition.
05643faMatus Tejiscak
src/Idris/ElabDecls.hs+15−1
compare with master
unifiedsplit
@@ -284,6 +284,7 @@ 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)
287 let metainf = DataMI params
288 let metainf = DataMI params
288 addIBC (IBCMetaInformation n metainf)
289 addIBC (IBCMetaInformation n metainf)
289 -- TMP HACK! Make this a data option
290 -- TMP HACK! Make this a data option
@@ -291,11 +292,24 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
291 updateContext (addDatatype (Data n ttag cty cons))
292 updateContext (addDatatype (Data n ttag cty cons))
292 updateContext (setMetaInformation n metainf)
293 updateContext (setMetaInformation n metainf)
293 mapM_ (checkPositive n) cons
294 mapM_ (checkPositive n) cons
295+
296+ case cons of
297+ [(cn,ct)] -> setDetaggable cn >> setDetaggable n
298+ _ -> return ()
299+
294 if DefaultEliminator `elem` opts
300 if DefaultEliminator `elem` opts
295 then evalStateT (elabEliminator params n t dcons info) Map.empty
301 then evalStateT (elabEliminator params n t dcons info) Map.empty
296 else return ()
302 else return ()
297 where
303 where
304+ setDetaggable :: Name -> Idris ()
305+ setDetaggable n = do
306+ ist <- getIState
307+ let opt = idris_optimisation ist
308+ case lookupCtxt n opt of
309+ [oi] -> putIState ist{ idris_optimisation = addDef n oi{ detaggable = True } opt }
310+ _ -> putIState ist{ idris_optimisation = addDef n (Optimise False False [] [] [] True) opt }
311+
298− checkDefinedAs fc n t ctxt
312+ checkDefinedAs fc n t ctxt
299 = case lookupDef n ctxt of
313 = case lookupDef n ctxt of
300 [] -> return ()
314 [] -> return ()
301 [TyDecl _ ty] ->
315 [TyDecl _ ty] ->