@@ -237,7 +237,9 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
237237 logLvl 2 $ "---> " ++ show cty
238238 -- temporary, to check cons
239239 when undef $ updateContext (addTyDecl n (TCon 0 0) cty)
240− cons <- mapM (elabCon info syn n codata) dcons
240+ --TODO WIP modify info for constructor names
241+ let cnameinfo = cinfo info (map cname dcons)
242+ cons <- mapM (elabCon cnameinfo syn n codata) dcons
241243 ttag <- getName
242244 i <- getIState
243245 let as = map (const Nothing) (getArgTys cty)
@@ -320,6 +322,21 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
320322 | otherwise = count n ts
321323 mParam args (_ : rest) = Nothing : mParam args rest
322324
325+ cname (_, _, n, _, _, _) = n
326+
327+ -- Abuse of ElabInfo.
328+ -- TODO Contemplate whether the ElabInfo type needs modification.
329+ cinfo :: ElabInfo -> [Name] -> ElabInfo
330+ cinfo info ds
331+ = let newps = params info
332+ dsParams = map (\n -> (n, [])) ds
333+ newb = addAlist dsParams (inblock info)
334+ l = liftname info in
335+ info { params = newps,
336+ inblock = newb,
337+ liftname = id -- Is this appropriate?
338+ }
339+
323340type EliminatorState = StateT (Map.Map String Int) Idris
324341
325342-- TODO: Use uniqueName for generating names, rewrite everything to use idris_implicits instead of manual splitting, generally just rewrite
@@ -841,7 +858,6 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)
841858 = do checkUndefined fc n
842859 ctxt <- getContext
843860 i <- getIState
844− -- TODO think: something more in info?
845861 t_in <- implicit info syn n (if codata then mkLazy t_in else t_in)
846862 let t = addImpl i t_in
847863 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t