@@ -237,7 +237,9 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
237 logLvl 2 $ "---> " ++ show cty
237 logLvl 2 $ "---> " ++ show cty
238 -- temporary, to check cons
238 -- temporary, to check cons
239 when undef $ updateContext (addTyDecl n (TCon 0 0) cty)
239 when undef $ updateContext (addTyDecl n (TCon 0 0) cty)
240+ --TODO WIP modify info for constructor names
241+ let cnameinfo = cinfo info (map cname dcons)
240− cons <- mapM (elabCon info syn n codata) dcons
242+ cons <- mapM (elabCon cnameinfo syn n codata) dcons
241 ttag <- getName
243 ttag <- getName
242 i <- getIState
244 i <- getIState
243 let as = map (const Nothing) (getArgTys cty)
245 let as = map (const Nothing) (getArgTys cty)
@@ -320,6 +322,21 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
320 | otherwise = count n ts
322 | otherwise = count n ts
321 mParam args (_ : rest) = Nothing : mParam args rest
323 mParam args (_ : rest) = Nothing : mParam args rest
325+ cname (_, _, n, _, _, _) = n
327+ -- Abuse of ElabInfo.
328+ -- TODO Contemplate whether the ElabInfo type needs modification.
329+ cinfo :: ElabInfo -> [Name] -> ElabInfo
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,
337+ liftname = id -- Is this appropriate?
323type EliminatorState = StateT (Map.Map String Int) Idris
340type EliminatorState = StateT (Map.Map String Int) Idris
325-- TODO: Use uniqueName for generating names, rewrite everything to use idris_implicits instead of manual splitting, generally just rewrite
342-- 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)
841 = do checkUndefined fc n
858 = do checkUndefined fc n
842 ctxt <- getContext
859 ctxt <- getContext
843 i <- getIState
860 i <- getIState
844− -- TODO think: something more in info?
845 t_in <- implicit info syn n (if codata then mkLazy t_in else t_in)
861 t_in <- implicit info syn n (if codata then mkLazy t_in else t_in)
846 let t = addImpl i t_in
862 let t = addImpl i t_in
847 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t
863 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t