@@ -124,7 +124,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
124 [oi] -> putIState ist{ idris_optimisation = addDef n oi{ detaggable = True } opt }
124 [oi] -> putIState ist{ idris_optimisation = addDef n oi{ detaggable = True } opt }
125 _ -> putIState ist{ idris_optimisation = addDef n (Optimise [] True) opt }
125 _ -> putIState ist{ idris_optimisation = addDef n (Optimise [] True) opt }
127− checkDefinedAs fc n t ctxt
127+ checkDefinedAs fc n t ctxt
128 = case lookupDef n ctxt of
128 = case lookupDef n ctxt of
129 [] -> return ()
129 [] -> return ()
130 [TyDecl _ ty] ->
130 [TyDecl _ ty] ->
@@ -204,14 +204,9 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
204 liftname = id -- Is this appropriate?
204 liftname = id -- Is this appropriate?
207−-- FIXME: 'forcenames' is an almighty hack! Need a better way of
208−-- erasing non-forceable things
210−-- TODO: the above is a comment from the past;
211−-- forcenames is probably no longer needed
212elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
207elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
213 Type -> -- for kind checking
208 Type -> -- for kind checking
214− (Docstring (Maybe PTerm), [(Name, Docstring (Maybe PTerm))], Name, PTerm, FC, [Name]) ->
209+ (Docstring (Maybe PTerm), [(Name, Docstring (Maybe PTerm))], Name, PTerm, FC, [Name]) ->
215 Idris (Name, Type)
210 Idris (Name, Type)
216elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)
211elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)
217 = do checkUndefined fc n
212 = do checkUndefined fc n
@@ -244,7 +239,7 @@ elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)
244 else return ()
239 else return ()
245 tyIs con t = tclift $ tfail (At fc (Elaborating "constructor " con (Msg (show t ++ " is not " ++ show tn))))
240 tyIs con t = tclift $ tfail (At fc (Elaborating "constructor " con (Msg (show t ++ " is not " ++ show tn))))
247− mkLazy (PPi pl n ty sc)
242+ mkLazy (PPi pl n ty sc)
248 = let ty' = if getTyName ty
243 = let ty' = if getTyName ty
249 then PApp fc (PRef fc (sUN "Lazy'"))
244 then PApp fc (PRef fc (sUN "Lazy'"))
250 [pexp (PRef fc (sUN "LazyCodata")),
245 [pexp (PRef fc (sUN "LazyCodata")),
@@ -417,7 +412,7 @@ elabCaseFun ind paramPos n ty cons info = do
417 case findIndex (== n) oldParams of
412 case findIndex (== n) oldParams of
418 Nothing -> (PPi pl n (removeParamPis oldParams params tyb) (removeParamPis oldParams params tyr))
413 Nothing -> (PPi pl n (removeParamPis oldParams params tyb) (removeParamPis oldParams params tyr))
419 Just i -> (removeParamPis oldParams params tyr)
414 Just i -> (removeParamPis oldParams params tyr)
420− removeParamPis oldParams params (PRef _ n) =
415+ removeParamPis oldParams params (PRef _ n) =
421 case findIndex (== n) oldParams of
416 case findIndex (== n) oldParams of
422 Nothing -> (PRef elimFC n)
417 Nothing -> (PRef elimFC n)
423 Just i -> let (newname,_,_) = params !! i in (PRef elimFC (newname))
418 Just i -> let (newname,_,_) = params !! i in (PRef elimFC (newname))
@@ -518,4 +513,3 @@ elabCaseFun ind paramPos n ty cons info = do
518 where applyRecElim :: (Name, Plicity, PTerm) -> PArg
513 where applyRecElim :: (Name, Plicity, PTerm) -> PArg
519 applyRecElim (constr@(recCnm,_,recTy)) = pexp $ PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ map pexp idxs ++ [pexp $ PRef elimFC recCnm])
514 applyRecElim (constr@(recCnm,_,recTy)) = pexp $ PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ map pexp idxs ++ [pexp $ PRef elimFC recCnm])
520 where (_, idxs) = splitArgPms recTy
515 where (_, idxs) = splitArgPms recTy