751a6ee · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Comment cleanup.

commit751a6eedd94dab101b85f7ca33a3a9847a37ceab authorTimo Petteri Sinnemäki <timo.sinnemaki@helsinki.fi> dateFri 4 Apr 2014, 20:44 (13 years ago) parentc78fb14

4 files changed+60−69

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+4−13 src/Idris/AbsSyntaxTree.hs+3−3 src/Idris/ElabDecls.hs+33−33 src/Idris/ElabTerm.hs+20−20

src/Idris/AbsSyntax.hs+4−13

@@ -1419,7 +1419,7 @@ addImpl' inpat env infns ist ptm

14191419 PApp fc (PInferRef fc f) as'

14201420 ai env ds (PApp fc ftm@(PRef _ f) as)

14211421 | f `elem` infns = ai env ds (PApp fc (PInferRef fc f) as)

1422− | not (f `elem` map fst env) -- notelocal

1422+ | not (f `elem` map fst env)

14231423 = let as' = map (fmap (ai env ds)) as in

14241424 handleErr $ aiFn inpat False ist fc f ds as'

14251425 | Just (Just ty) <- lookup f env =

@@ -1526,18 +1526,9 @@ aiFn inpat expat ist fc f ds as

15261526 insertImpl :: [PArg] -> [PArg] -> [PArg]

15271527 insertImpl ps as = insImpAcc M.empty ps as

15281528

1529− -- TODO WIP substitution into default arg expressions.

1530− -- - An extra accumulator parameter here?

1531− -- - Accumulator of what?

1532− -- - Map of param names and their corresponding arg terms?

1533− -- - Perhaps in an 'inner' function, though?

1534− -- - Though OTOH perhaps this one should become the inner

1535− -- function?

1536− -- - Check for existing call sites of insertImpl.

1537− -- - Well, easy: this is in a where block :-).

1538− insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms

1539− -> [PArg] -- parameters

1540− -> [PArg] -- arguments

1529+ insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms

1530+ -> [PArg] -- parameters

1531+ -> [PArg] -- arguments

15411532 -> [PArg]

15421533 insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) =

15431534 PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given

src/Idris/AbsSyntaxTree.hs+3−3

@@ -1497,7 +1497,7 @@ getPArity _ = 0

14971497

14981498allNamesIn :: PTerm -> [Name]

14991499allNamesIn tm = nub $ ni [] tm

1500− where -- FIXME added niTacImp, but is it right?

1500+ where -- TODO THINK added niTacImp, but is it right?

15011501 ni env (PRef _ n)

15021502 | not (n `elem` env) = [n]

15031503 ni env (PPatvar _ n) = [n]

@@ -1525,7 +1525,7 @@ allNamesIn tm = nub $ ni [] tm

15251525-- Return all names defined in binders in the given term

15261526boundNamesIn :: PTerm -> [Name]

15271527boundNamesIn tm = nub $ ni tm

1528− where -- FIXME Added niTacImp, but is it right?

1528+ where -- TODO THINK Added niTacImp, but is it right?

15291529 ni (PApp _ f as) = ni f ++ concatMap (ni) (map getTm as)

15301530 ni (PAppBind _ f as) = ni f ++ concatMap (ni) (map getTm as)

15311531 ni (PCase _ c os) = ni c ++ concatMap (ni) (map snd os)

@@ -1582,7 +1582,7 @@ namesIn uvars ist tm = nub $ ni [] tm

15821582

15831583usedNamesIn :: [Name] -> IState -> PTerm -> [Name]

15841584usedNamesIn vars ist tm = nub $ ni [] tm

1585− where -- FIXME added niTacImp, but is it right?

1585+ where -- TODO THINK added niTacImp, but is it right?

15861586 ni env (PRef _ n)

15871587 | n `elem` vars && not (n `elem` env)

15881588 = case lookupTy n (tt_ctxt ist) of

src/Idris/ElabDecls.hs+33−33

@@ -526,13 +526,13 @@ elabEliminator paramPos n ty cons info = do

526526 findRecArgs (ty:rs) = findRecArgs rs

527527

528528 applyCons :: Name -> [(Name, Plicity, PTerm)] -> PTerm

529− applyCons tn targs = PApp elimFC (PRef elimFC tn) (map convertArg targs) -- ipapp

529+ applyCons tn targs = PApp elimFC (PRef elimFC tn) (map convertArg targs)

530530

531531 convertArg :: (Name, Plicity, PTerm) -> PArg

532532 convertArg (n, _, _) = pexp (PRef elimFC n)

533533

534534 applyMotive :: [PTerm] -> PTerm -> PTerm

535− applyMotive idxs t = PApp elimFC (PRef elimFC motiveName) (map pexp idxs ++ [pexp t]) -- ipapp

535+ applyMotive idxs t = PApp elimFC (PRef elimFC motiveName) (map pexp idxs ++ [pexp t])

536536

537537 getPiName :: (Name, Plicity, PTerm) -> Name

538538 getPiName (name,_,_) = name

@@ -550,13 +550,13 @@ elabEliminator paramPos n ty cons info = do

550550 let (_, generalIdxs') = splitArgPms resTy

551551 let generalIdxs = map pexp generalIdxs'

552552 consArgs <- namePis True args

553− let lhsPattern = PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ generalIdxs ++ [pexp $ applyCons cnm consArgs]) -- ipapp

553+ let lhsPattern = PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ generalIdxs ++ [pexp $ applyCons cnm consArgs])

554554 let recArgs = findRecArgs consArgs

555555 let recElims = map applyRecElim recArgs

556− let rhsExpr = PApp elimFC (PRef elimFC cnsElim) (map convertArg implidxs ++ map convertArg consArgs ++ recElims) -- ipapp

556+ let rhsExpr = PApp elimFC (PRef elimFC cnsElim) (map convertArg implidxs ++ map convertArg consArgs ++ recElims)

557557 return $ PClause elimFC elimDeclName lhsPattern [] rhsExpr []

558558 where applyRecElim :: (Name, Plicity, PTerm) -> PArg

559− applyRecElim (constr@(recCnm,_,recTy)) = pexp $ PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ map pexp idxs ++ [pexp $ PRef elimFC recCnm]) -- ipapp

559+ applyRecElim (constr@(recCnm,_,recTy)) = pexp $ PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ map pexp idxs ++ [pexp $ PRef elimFC recCnm])

560560 where (_, idxs) = splitArgPms recTy

561561

562562-- | Elaborate primitives

@@ -668,7 +668,7 @@ elabProvider info syn fc what n ty tm

668668 | what `elem` [ProvTerm, ProvAny] ->

669669 do -- Finally add a top-level definition of the provided term

670670 elabType info syn emptyDocstring [] fc [] n ty

671− elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []] -- ipapp

671+ elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []]

672672 logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm

673673 | otherwise ->

674674 ierror . Msg $ "Attempted to provide a term where a postulate was expected."

@@ -741,7 +741,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

741741 let ptys_u = getProjs [] cty

742742 let recty = getRecTy cty

743743 logLvl 6 $ show (recty, ptys)

744− let substs = map (\ (n, _) -> (n, PApp fc (PRef fc n) -- ipapp

744+ let substs = map (\ (n, _) -> (n, PApp fc (PRef fc n)

745745 [pexp (PRef fc rec)])) ptys

746746 proj_decls <- mapM (mkProj recty substs cimp) (zip ptys [0..])

747747 let nonImp = mapMaybe isNonImp (zip cimp ptys_u)

@@ -807,8 +807,8 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

807807 let after = length substs - (pos + 1)

808808 let args = take before pls ++ PRef fc (mkp pn) : take after pls

809809 let iargs = map implicitise (zip cimp args)

810− let lhs = PApp fc (PRef fc pn) -- ipapp

811− [pexp (PApp fc (PRef fc cn) iargs)] -- ipapp

810+ let lhs = PApp fc (PRef fc pn)

811+ [pexp (PApp fc (PRef fc cn) iargs)]

812812 let rhs = PRef fc (mkp pn)

813813 let pclause = PClause fc pn lhs [] rhs []

814814 return [pfnTy, PClauses fc [] pn [pclause]]

@@ -826,12 +826,12 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

826826 let rhsArgs = take pos pls ++ (PRef fc valname) :

827827 drop (pos + 1) pls

828828 let before = pos

829− let pclause = PClause fc setname (PApp fc (PRef fc setname) -- ipapp

829+ let pclause = PClause fc setname (PApp fc (PRef fc setname)

830830 [pexp (PRef fc valname),

831− pexp (PApp fc (PRef fc cn) -- ipapp

831+ pexp (PApp fc (PRef fc cn)

832832 (map pexp lhsArgs))])

833833 []

834− (PApp fc (PRef fc cn) -- ipapp

834+ (PApp fc (PRef fc cn)

835835 (map pexp rhsArgs)) []

836836 return (pn, pfnTy, PClauses fc [] setname [pclause])

837837

@@ -876,7 +876,7 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)

876876

877877 mkLazy (PPi pl n ty sc)

878878 = let ty' = if getTyName ty

879− then PApp fc (PRef fc (sUN "Lazy'")) -- ipapp

879+ then PApp fc (PRef fc (sUN "Lazy'"))

880880 [pexp (PRef fc (sUN "LazyCodata")),

881881 pexp ty]

882882 else ty in

@@ -1341,7 +1341,7 @@ paramNames args env (p : ps)

13411341

13421342propagateParams :: [Name] -> Type -> PTerm -> PTerm

13431343propagateParams ps t tm@(PApp _ (PRef fc n) args)

1344− = PApp fc (PRef fc n) (addP t args) -- tpapp

1344+ = PApp fc (PRef fc n) (addP t args)

13451345 where addP (Bind n _ sc) (t : ts)

13461346 | Placeholder <- getTm t,

13471347 n `elem` ps,

@@ -1350,7 +1350,7 @@ propagateParams ps t tm@(PApp _ (PRef fc n) args)

13501350 addP (Bind n _ sc) (t : ts) = t : addP sc ts

13511351 addP _ ts = ts

13521352propagateParams ps t (PRef fc n)

1353− = PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x) True) ps) -- ipapp

1353+ = PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x) True) ps)

13541354propagateParams ps t x = x

13551355

13561356elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->

@@ -1509,7 +1509,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

15091509 addErrRev (crhs, clhs)

15101510 return $ Right (clhs, crhs)

15111511 where

1512− mkLHSapp t@(PRef _ _) = trace ("APP " ++ show t) $ PApp fc t [] -- ipapp

1512+ mkLHSapp t@(PRef _ _) = trace ("APP " ++ show t) $ PApp fc t []

15131513 mkLHSapp t = t

15141514

15151515 decorate (NS x ns)

@@ -1640,7 +1640,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

16401640 mapM_ (elabDecl EAll info) wb

16411641

16421642 -- rhs becomes: fname' ps wval

1643− let rhs = PApp fc (PRef fc wname) -- ipapp

1643+ let rhs = PApp fc (PRef fc wname)

16441644 (map (pexp . (PRef fc) . fst) bargs_pre ++

16451645 pexp wval :

16461646 (map (pexp . (PRef fc) . fst) bargs_post))

@@ -1697,14 +1697,14 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

16971697 mkAux wname toplhs ns ns' c

16981698 = ifail $ show fc ++ "badly formed with clause"

16991699

1700− addArg (PApp fc f args) w = PApp fc f (args ++ [pexp w]) -- tpapp

1701− addArg (PRef fc f) w = PApp fc (PRef fc f) [pexp w] -- ipapp

1700+ addArg (PApp fc f args) w = PApp fc f (args ++ [pexp w])

1701+ addArg (PRef fc f) w = PApp fc (PRef fc f) [pexp w]

17021702

17031703 updateLHS n wname mvars ns_in ns_in' (PApp fc (PRef fc' n') args) w

17041704 = let ns = map (keepMvar (map fst mvars) fc') ns_in

17051705 ns' = map (keepMvar (map fst mvars) fc') ns_in' in

17061706 return $ substMatches mvars $

1707− PApp fc (PRef fc' wname) -- tpapp

1707+ PApp fc (PRef fc' wname)

17081708 (map pexp ns ++ pexp w : (map pexp ns'))

17091709 updateLHS n wname mvars ns ns' tm w

17101710 = ifail $ "Not implemented match " ++ show tm

@@ -1712,7 +1712,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

17121712 keepMvar mvs fc v | v `elem` mvs = PRef fc v

17131713 | otherwise = Placeholder

17141714

1715− fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs)) -- tpapp

1715+ fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))

17161716 fullApp x = x

17171717

17181718 split [] rest pre = (reverse pre, rest)

@@ -1731,7 +1731,7 @@ elabClass :: ElabInfo -> SyntaxInfo -> Docstring ->

17311731elabClass info syn doc fc constraints tn ps ds

17321732 = do let cn = SN (InstanceCtorN tn) -- sUN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)

17331733 let tty = pibind ps PType

1734− let constraint = PApp fc (PRef fc tn) -- ipapp

1734+ let constraint = PApp fc (PRef fc tn)

17351735 (map (pexp . PRef fc) (map fst ps))

17361736 -- build data declaration

17371737 let mdecls = filter tydecl ds -- method declarations

@@ -1782,7 +1782,7 @@ elabClass info syn doc fc constraints tn ps ds

17821782 = do when (not $ null cs) . tclift

17831783 $ tfail (At fc (Msg $ "Default superclass instances can't have constraints."))

17841784 i <- getIState

1785− let t = PApp fc (PRef fc n) (map pexp ps) -- ipapp

1785+ let t = PApp fc (PRef fc n) (map pexp ps)

17861786 let isConstrained = any (== t) constraints

17871787 when (not isConstrained) . tclift

17881788 $ tfail (At fc (Msg $ "Default instances must be for a superclass constraint on the containing class."))

@@ -1829,8 +1829,8 @@ elabClass info syn doc fc constraints tn ps ds

18291829 = do let cfn = sUN ('@':'@':show cn ++ "#" ++ show con)

18301830 -- SN (ParentN cn (show con))

18311831 let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]

1832− let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames) -- ipapp

1833− let lhs = PApp fc (PRef fc cfn) [pconst capp] -- ipapp

1832+ let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)

1833+ let lhs = PApp fc (PRef fc cfn) [pconst capp]

18341834 let rhs = PResolveTC (fileFC "HACK")

18351835 let ty = PPi constraint (sMN 0 "pc") c con

18361836 iLOG (showTmImpls ty)

@@ -1853,11 +1853,11 @@ elabClass info syn doc fc constraints tn ps ds

18531853 tfun cn c syn all (m, (doc, o, ty))

18541854 = do let ty' = insertConstraint c ty

18551855 let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]

1856− let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames) -- ipapp

1856+ let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)

18571857 let margs = getMArgs ty

18581858 let anames = map (\x -> sMN x "arg") [0..]

1859− let lhs = PApp fc (PRef fc m) (pconst capp : lhsArgs margs anames) -- ipapp

1860− let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames) -- ipapp

1859+ let lhs = PApp fc (PRef fc m) (pconst capp : lhsArgs margs anames)

1860+ let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames)

18611861 iLOG (showTmImpls ty)

18621862 iLOG (show (m, ty', capp, margs))

18631863 iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)

@@ -1906,7 +1906,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

19061906 (n, ci) <- case lookupCtxtName n (idris_classes i) of

19071907 [c] -> return c

19081908 _ -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"

1909− let constraint = PApp fc (PRef fc n) (map pexp ps) -- ipapp

1909+ let constraint = PApp fc (PRef fc n) (map pexp ps)

19101910 let iname = mkiname n ps expn

19111911 when (what /= EDefns) $ do

19121912 nty <- elabType' True info syn emptyDocstring [] fc [] iname t

@@ -1961,9 +1961,9 @@ elabInstance info syn what fc cs n ps t expn ds = do

19611961 _ -> Nothing

19621962 _ -> Nothing) ps

19631963-- let lhs = PRef fc iname

1964− let lhs = PApp fc (PRef fc iname) -- ipapp

1964+ let lhs = PApp fc (PRef fc iname)

19651965 (map (\n -> pimp n (PRef fc n) True) headVars)

1966− let rhs = PApp fc (PRef fc (instanceName ci)) -- ipapp

1966+ let rhs = PApp fc (PRef fc (instanceName ci))

19671967 (map (pexp . mkMethApp) mtys)

19681968

19691969 logLvl 5 $ "Instance LHS " ++ show lhs

@@ -2044,7 +2044,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

20442044 methArgs i _ = []

20452045

20462046 papp fc f [] = f

2047− papp fc f as = PApp fc f as -- ipapp

2047+ papp fc f as = PApp fc f as

20482048

20492049 getWParams [] = return []

20502050 getWParams (p : ps)

@@ -2129,7 +2129,7 @@ decorateid decorate (PClauses f o n cs)

21292129 dc (PWith fc n t as w ds)

21302130 = PWith fc (decorate n) (dappname t) as w

21312131 (map (decorateid decorate) ds)

2132− dappname (PApp fc (PRef fc' n) as) = PApp fc (PRef fc' (decorate n)) as -- tpapp

2132+ dappname (PApp fc (PRef fc' n) as) = PApp fc (PRef fc' (decorate n)) as

21332133 dappname t = t

21342134

21352135

src/Idris/ElabTerm.hs+20−20

@@ -167,7 +167,7 @@ elab ist info pattern opts fn tm

167167 env <- get_env

168168 handleError (forceErr env)

169169 (elab' ina t')

170− (elab' ina (PApp fc (PRef fc (sUN "Force")) -- ipapp

170+ (elab' ina (PApp fc (PRef fc (sUN "Force"))

171171 [pimp (sUN "t") Placeholder True,

172172 pimp (sUN "a") Placeholder True,

173173 pexp ct])) True

@@ -220,9 +220,9 @@ elab ist info pattern opts fn tm

220220 (do c <- getNameFrom (sMN 0 "class")

221221 instanceArg c)

222222 elab' ina (PRefl fc t)

223− = elab' ina (PApp fc (PRef fc eqCon) [pimp (sMN 0 "A") Placeholder True, -- ipapp

223+ = elab' ina (PApp fc (PRef fc eqCon) [pimp (sMN 0 "A") Placeholder True,

224224 pimp (sMN 0 "x") t False])

225− elab' ina (PEq fc l r) = elab' ina (PApp fc (PRef fc eqTy) -- ipapp

225+ elab' ina (PEq fc l r) = elab' ina (PApp fc (PRef fc eqTy)

226226 [pimp (sMN 0 "A") Placeholder True,

227227 pimp (sMN 0 "B") Placeholder False,

228228 pexp l, pexp r])

@@ -230,9 +230,9 @@ elab ist info pattern opts fn tm

230230 = do hnf_compute

231231 g <- goal

232232 case g of

233− TType _ -> elabE (True, a,inty) (PApp fc (PRef fc pairTy) -- ipapp

233+ TType _ -> elabE (True, a,inty) (PApp fc (PRef fc pairTy)

234234 [pexp l,pexp r])

235− _ -> elabE (True, a, inty) (PApp fc (PRef fc pairCon) -- ipapp

235+ _ -> elabE (True, a, inty) (PApp fc (PRef fc pairCon)

236236 [pimp (sMN 0 "A") Placeholder True,

237237 pimp (sMN 0 "B") Placeholder True,

238238 pexp l, pexp r])

@@ -245,14 +245,14 @@ elab ist info pattern opts fn tm

245245 TType _ -> asType

246246 _ -> asValue

247247 _ -> asType

248− where asType = elab' ina (PApp fc (PRef fc sigmaTy) -- ipapp

248+ where asType = elab' ina (PApp fc (PRef fc sigmaTy)

249249 [pexp t,

250250 pexp (PLam n Placeholder r)])

251− asValue = elab' ina (PApp fc (PRef fc existsCon) -- ipapp

251+ asValue = elab' ina (PApp fc (PRef fc existsCon)

252252 [pimp (sMN 0 "a") t False,

253253 pimp (sMN 0 "P") Placeholder True,

254254 pexp l, pexp r])

255− elab' ina (PDPair fc p l t r) = elab' ina (PApp fc (PRef fc existsCon) -- ipapp

255+ elab' ina (PDPair fc p l t r) = elab' ina (PApp fc (PRef fc existsCon)

256256 [pimp (sMN 0 "a") t False,

257257 pimp (sMN 0 "P") Placeholder True,

258258 pexp l, pexp r])

@@ -295,7 +295,7 @@ elab ist info pattern opts fn tm

295295 where inparamBlock n = case lookupCtxtName n (inblock info) of

296296 [] -> False

297297 _ -> True

298− elab' ina f@(PInferRef fc n) = elab' ina (PApp fc f []) -- ipapp

298+ elab' ina f@(PInferRef fc n) = elab' ina (PApp fc f [])

299299 elab' ina (PRef fc n) = erun fc $ do apply (Var n) []; solve

300300 elab' ina@(_, a, inty) (PLam n Placeholder sc)

301301 = do -- if n is a type constructor name, this makes no sense...

@@ -367,7 +367,7 @@ elab ist info pattern opts fn tm

367367 claim valn (Var tyn)

368368 letbind n (Var tyn) (Var valn)

369369 focus valn

370− elabE (True, a, True) (PApp fc r [pexp (delab ist rty)]) -- ipapp

370+ elabE (True, a, True) (PApp fc r [pexp (delab ist rty)])

371371 env <- get_env

372372 computeLet n

373373 elabE (True, a, inty) sc

@@ -432,7 +432,7 @@ elab ist info pattern opts fn tm

432432 -- if f is local, just do a simple_app

433433 elab' (ina, g, inty) tm@(PApp fc (PRef _ f) args)

434434 = do env <- get_env

435− if (f `elem` map fst env && length args == 1) -- notelocal

435+ if (f `elem` map fst env && length args == 1)

436436 then -- simple app, as below

437437 do simple_app (elabE (ina, g, inty) (PRef fc f))

438438 (elabE (True, g, inty) (getTm (head args)))

@@ -656,7 +656,7 @@ elab ist info pattern opts fn tm

656656 -- old ones with an _

657657 mkClause args (l, r)

658658 = let args' = map (shadowed (allNamesIn l)) args

659− lhs = PApp (getFC fc l) (PRef (getFC fc l) n) -- ipapp

659+ lhs = PApp (getFC fc l) (PRef (getFC fc l) n)

660660 (map (mkLHSarg l) args') in

661661 PClause (getFC fc l) n lhs [] r []

662662

@@ -672,8 +672,8 @@ elab ist info pattern opts fn tm

672672 getFC d x = d

673673

674674 insertLazy :: PTerm -> ElabD PTerm

675− insertLazy t@(PApp _ (PRef _ (UN l)) _) | l == txt "Delay" = return t -- tpapp

676− insertLazy t@(PApp _ (PRef _ (UN l)) _) | l == txt "Force" = return t -- tpapp

675+ insertLazy t@(PApp _ (PRef _ (UN l)) _) | l == txt "Delay" = return t

676+ insertLazy t@(PApp _ (PRef _ (UN l)) _) | l == txt "Force" = return t

677677 insertLazy (PCoerced t) = return t

678678 insertLazy t =

679679 do ty <- goal

@@ -687,7 +687,7 @@ elab ist info pattern opts fn tm

687687 where

688688 mkDelay (PAlternative b xs) = PAlternative b (map mkDelay xs)

689689 mkDelay t = let fc = fileFC "Delay" in

690− addImpl ist (PApp fc (PRef fc (sUN "Delay")) -- ipapp

690+ addImpl ist (PApp fc (PRef fc (sUN "Delay"))

691691 [pexp t])

692692

693693 insertCoerce ina t =

@@ -705,7 +705,7 @@ elab ist info pattern opts fn tm

705705 return t'

706706 where

707707 mkCoerce t n = let fc = fileFC "Coercion" in -- line never appears!

708− addImpl ist (PApp fc (PRef fc n) [pexp (PCoerced t)]) -- ipapp

708+ addImpl ist (PApp fc (PRef fc n) [pexp (PCoerced t)])

709709

710710 -- | Elaborate the arguments to a function

711711 elabArgs :: IState -- ^ The current Idris state

@@ -723,7 +723,7 @@ elab ist info pattern opts fn tm

723723 = elabArgs ist ina failed fc r f ns force args

724724 elabArgs ist ina failed fc r f ((argName, holeName):ns) force ((lazy, t) : args)

725725 | lazy && not pattern

726− = elabArg argName holeName (PApp bi (PRef bi (sUN "lazy")) -- ipapp

726+ = elabArg argName holeName (PApp bi (PRef bi (sUN "lazy"))

727727 [pimp (sUN "a") Placeholder True,

728728 pexp t])

729729 | otherwise = elabArg argName holeName t

@@ -761,7 +761,7 @@ pruneAlt :: [PTerm] -> [PTerm]

761761pruneAlt xs = map prune xs

762762 where

763763 prune (PApp fc1 (PRef fc2 f) as)

764− = PApp fc1 (PRef fc2 f) (fmap (fmap (choose f)) as) -- tpapp

764+ = PApp fc1 (PRef fc2 f) (fmap (fmap (choose f)) as)

765765 prune t = t

766766

767767 choose f (PAlternative a as)

@@ -771,7 +771,7 @@ pruneAlt xs = map prune xs

771771 [a] -> a

772772 _ -> PAlternative a as'

773773

774− choose f (PApp fc f' as) = PApp fc (choose f f') (fmap (fmap (choose f)) as) -- tpapp

774+ choose f (PApp fc f' as) = PApp fc (choose f f') (fmap (fmap (choose f)) as)

775775 choose f t = t

776776

777777 headIs f (PApp _ (PRef _ f') _) = f == f'

@@ -1097,7 +1097,7 @@ runTac autoSolve ist fn tac

10971097 focus script

10981098 ptm <- get_term

10991099 elab ist toplevel False [] (sMN 0 "tac")

1100− (PApp emptyFC tm [pexp (delabTy' ist [] tgoal True True)]) -- ipapp

1100+ (PApp emptyFC tm [pexp (delabTy' ist [] tgoal True True)])

11011101 (script', _) <- get_type_val (Var scriptvar)

11021102 -- now that we have the script apply

11031103 -- it to the reflected goal