@@ -304,7 +304,8 @@ elabData info syn doc fc opts (PDatadecl n t_in dcons)
304304type EliminatorState = StateT (Map.Map String Int) Idris
305305
306306-- TODO: Use uniqueName for generating names, rewrite everything to use idris_implicits instead of manual splitting, generally just rewrite
307−elabEliminator :: [Int] -> Name -> PTerm -> [(String, Name, PTerm, FC)] -> ElabInfo -> EliminatorState ()
307+elabEliminator :: [Int] -> Name -> PTerm -> [(String, Name, PTerm, FC, [Name])] ->
308+ ElabInfo -> EliminatorState ()
308309elabEliminator paramPos n ty cons info = do
309310 elimLog $ "Elaborating eliminator"
310311 let (cnstrs, _) = splitPi ty
@@ -312,7 +313,7 @@ elabEliminator paramPos n ty cons info = do
312313 generalParams <- namePis False pms
313314 motiveIdxs <- namePis False idxs
314315 let motive = mkMotive n paramPos generalParams motiveIdxs
315− consTerms <- mapM (\(c@(_,cnm,_,_)) -> do
316+ consTerms <- mapM (\(c@(_,cnm,_,_,_)) -> do
316317 name <- freshName $ "elim_" ++ simpleName cnm
317318 consTerm <- extractConsTerm c generalParams
318319 return (name, expl, consTerm)) cons
@@ -469,8 +470,8 @@ elabEliminator paramPos n ty cons info = do
469470 splitArgPms _ = ([],[])
470471
471472
472− implicitIndexes :: (String, Name, PTerm, FC) -> EliminatorState [(Name, Plicity, PTerm)]
473− implicitIndexes (cns@(doc, cnm, ty, fc)) = do
473+ implicitIndexes :: (String, Name, PTerm, FC, [Name]) -> EliminatorState [(Name, Plicity, PTerm)]
474+ implicitIndexes (cns@(doc, cnm, ty, fc, fs)) = do
474475 i <- State.lift getIState
475476 implargs' <- case lookupCtxt cnm (idris_implicits i) of
476477 [] -> do fail $ "Error while showing implicits for " ++ show cnm
@@ -484,11 +485,11 @@ elabEliminator paramPos n ty cons info = do
484485 in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs
485486 _ -> return implargs
486487
487− extractConsTerm :: (String, Name, PTerm, FC) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm
488− extractConsTerm (doc, cnm, ty, fc) generalParameters = do
488+ extractConsTerm :: (String, Name, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm
489+ extractConsTerm (doc, cnm, ty, fc, fs) generalParameters = do
489490 let cons' = replaceParams paramPos generalParameters ty
490491 let (args, resTy) = splitPi cons'
491− implidxs <- implicitIndexes (doc, cnm, ty, fc)
492+ implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)
492493 consArgs <- namePis True args
493494 let recArgs = findRecArgs consArgs
494495 let recMotives = map applyRecMotive recArgs
@@ -520,12 +521,12 @@ elabEliminator paramPos n ty cons info = do
520521 convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)
521522 convertImplPi _ = Nothing
522523
523− generateEliminatorClauses :: (String, Name, PTerm, FC) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause
524− generateEliminatorClauses (doc, cnm, ty, fc) cnsElim generalArgs generalParameters = do
524+ generateEliminatorClauses :: (String, Name, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause
525+ generateEliminatorClauses (doc, cnm, ty, fc, fs) cnsElim generalArgs generalParameters = do
525526 let cons' = replaceParams paramPos generalParameters ty
526527 let (args, resTy) = splitPi cons'
527528 i <- State.lift getIState
528− implidxs <- implicitIndexes (doc, cnm, ty, fc)
529+ implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)
529530 let (_, generalIdxs') = splitArgPms resTy
530531 let generalIdxs = map pexp generalIdxs'
531532 consArgs <- namePis True args
@@ -698,7 +699,7 @@ elabTransform info fc safe lhs_in rhs_in
698699elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->
699700 PTerm -> String -> Name -> PTerm -> Idris ()
700701elabRecord info syn doc fc tyn ty cdoc cn cty
701− = do elabData info syn doc fc [] (PDatadecl tyn ty [(cdoc, cn, cty, fc)])
702+ = do elabData info syn doc fc [] (PDatadecl tyn ty [(cdoc, cn, cty, fc, [])])
702703 cty' <- implicit syn cn cty
703704 i <- getIState
704705 cty <- case lookupTy cn (tt_ctxt i) of
@@ -805,8 +806,8 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
805806 return (pn, pfnTy, PClauses fc [] setname [pclause])
806807
807808elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
808− (String, Name, PTerm, FC) -> Idris (Name, Type)
809−elabCon info syn tn codata (doc, n, t_in, fc)
809+ (String, Name, PTerm, FC, [Name]) -> Idris (Name, Type)
810+elabCon info syn tn codata (doc, n, t_in, fc, forcenames)
810811 = do checkUndefined fc n
811812 ctxt <- getContext
812813 i <- getIState
@@ -829,7 +830,10 @@ elabCon info syn tn codata (doc, n, t_in, fc)
829830 addIBC (IBCDef n)
830831 addDocStr n doc
831832 addIBC (IBCDoc n)
832− forceArgs tn n cty'
833+ let fs = map (getNamePos 0 t) forcenames
834+ -- FIXME: 'forcenames' is an almighty hack! Need a better way of
835+ -- erasing non-forceable things
836+ forceArgs tn n (mapMaybe (getNamePos 0 t) forcenames) cty'
833837 return (n, cty')
834838 where
835839 tyIs (Bind n b sc) = tyIs sc
@@ -841,6 +845,11 @@ elabCon info syn tn codata (doc, n, t_in, fc)
841845 mkLazy (PPi pl n ty sc) = PPi (pl { plazy = True }) n ty (mkLazy sc)
842846 mkLazy t = t
843847
848+ getNamePos :: Int -> PTerm -> Name -> Maybe Int
849+ getNamePos i (PPi _ n _ sc) x | n == x = Just i
850+ | otherwise = getNamePos (i + 1) sc x
851+ getNamePos _ _ _ = Nothing
852+
844853-- | Elaborate a collection of left-hand and right-hand pairs - that is, a
845854-- top-level definition.
846855elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()
@@ -1628,7 +1637,7 @@ elabClass info syn doc fc constraints tn ps ds
16281637 let cty = impbind ps $ conbind constraints
16291638 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)
16301639 constraint
1631− let cons = [("", cn, cty, fc)]
1640+ let cons = [("", cn, cty, fc, [])]
16321641 let ddecl = PDatadecl tn tty cons
16331642 logLvl 5 $ "Class data " ++ showDImp True ddecl
16341643 elabData info (syn { no_imp = no_imp syn ++ mnames }) doc fc [] ddecl