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

git.iko.soy/Idris-dev

on master help sign in

Comment cleanup.

751a6eeTimo Petteri Sinnemäki13 years ago

src/Idris/AbsSyntax.hs+4−13

compare with master

unifiedsplit

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

1419 PApp fc (PInferRef fc f) as'

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

1421 | 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)

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

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

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

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

1526 insertImpl :: [PArg] -> [PArg] -> [PArg]

1527 insertImpl ps as = insImpAcc M.empty ps as

1528

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

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

1539− -> [PArg] -- parameters

1530+ -> [PArg] -- parameters

1540− -> [PArg] -- arguments

1531+ -> [PArg] -- arguments

1541 -> [PArg]

1532 -> [PArg]

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

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

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

1534 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

1497

1498allNamesIn :: PTerm -> [Name]

1499allNamesIn tm = nub $ ni [] tm

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

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

1501 ni env (PRef _ n)

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

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

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

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

1526boundNamesIn :: PTerm -> [Name]

1527boundNamesIn tm = nub $ ni tm

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

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

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

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

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

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

1582

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

1584usedNamesIn 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?

1586 ni env (PRef _ n)

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

1588 = case lookupTy n (tt_ctxt ist) of

src/Idris/ElabDecls.hs+33−33

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

526 findRecArgs (ty:rs) = findRecArgs rs

527

528 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)

530

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

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

533

534 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])

536

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

538 getPiName (name,_,_) = name

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

550 let (_, generalIdxs') = splitArgPms resTy

551 let generalIdxs = map pexp generalIdxs'

552 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])

554 let recArgs = findRecArgs consArgs

555 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)

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

558 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])

560 where (_, idxs) = splitArgPms recTy

561

562-- | Elaborate primitives

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

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

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

670 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) []]

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

673 | otherwise ->

674 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

741 let ptys_u = getProjs [] cty

742 let recty = getRecTy cty

743 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)

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

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

747 let nonImp = mapMaybe isNonImp (zip cimp ptys_u)

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

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

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

809 let iargs = map implicitise (zip cimp args)

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

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

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

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

812 let rhs = PRef fc (mkp pn)

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

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

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

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

827 drop (pos + 1) pls

828 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)

830 [pexp (PRef fc valname),

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

831+ pexp (PApp fc (PRef fc cn)

832 (map pexp lhsArgs))])

833 []

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

834+ (PApp fc (PRef fc cn)

835 (map pexp rhsArgs)) []

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

837

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

876

877 mkLazy (PPi pl n ty sc)

878 = let ty' = if getTyName ty

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

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

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

881 pexp ty]

882 else ty in

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

1341

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

1343propagateParams 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)

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

1346 | Placeholder <- getTm t,

1347 n `elem` ps,

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

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

1351 addP _ ts = ts

1352propagateParams 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)

1354propagateParams ps t x = x

1355

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

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

1509 addErrRev (crhs, clhs)

1510 return $ Right (clhs, crhs)

1511 where

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

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

1513 mkLHSapp t = t

1514

1515 decorate (NS x ns)

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

1640 mapM_ (elabDecl EAll info) wb

1641

1642 -- rhs becomes: fname' ps wval

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

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

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

1645 pexp wval :

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

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

1697 mkAux wname toplhs ns ns' c

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

1699

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

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] -- ipapp

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

1702

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

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

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

1706 return $ substMatches mvars $

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

1707+ PApp fc (PRef fc' wname)

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

1709 updateLHS n wname mvars ns ns' tm w

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

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

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

1713 | otherwise = Placeholder

1714

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))

1716 fullApp x = x

1717

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

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

1731elabClass info syn doc fc constraints tn ps ds

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

1733 let tty = pibind ps PType

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

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

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

1736 -- build data declaration

1737 let mdecls = filter tydecl ds -- method declarations

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

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

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

1784 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)

1786 let isConstrained = any (== t) constraints

1787 when (not isConstrained) . tclift

1788 $ 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

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

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

1831 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

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

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

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

1834 let rhs = PResolveTC (fileFC "HACK")

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

1836 iLOG (showTmImpls ty)

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

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

1854 = do let ty' = insertConstraint c ty

1855 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)

1857 let margs = getMArgs ty

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

1859− let lhs = PApp fc (PRef fc m) (pconst capp : lhsArgs 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) -- ipapp

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

1861 iLOG (showTmImpls ty)

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

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

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

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

1907 [c] -> return c

1908 _ -> 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)

1910 let iname = mkiname n ps expn

1911 when (what /= EDefns) $ do

1912 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

1961 _ -> Nothing

1962 _ -> Nothing) ps

1963-- let lhs = PRef fc iname

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

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

1965 (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))

1967 (map (pexp . mkMethApp) mtys)

1968

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

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

2044 methArgs i _ = []

2045

2046 papp fc f [] = f

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

2047+ papp fc f as = PApp fc f as

2048

2049 getWParams [] = return []

2050 getWParams (p : ps)

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

2129 dc (PWith fc n t as w ds)

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

2131 (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

2133 dappname t = t

2134

2135

src/Idris/ElabTerm.hs+20−20

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

167 env <- get_env

168 handleError (forceErr env)

169 (elab' ina t')

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

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

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

172 pimp (sUN "a") Placeholder True,

173 pexp ct])) True

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

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

221 instanceArg c)

222 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,

224 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)

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

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

228 pexp l, pexp r])

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

230 = do hnf_compute

231 g <- goal

232 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)

234 [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)

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

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

238 pexp l, pexp r])

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

245 TType _ -> asType

246 _ -> asValue

247 _ -> asType

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

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

249 [pexp t,

250 pexp (PLam n Placeholder r)])

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

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

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

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

254 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)

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

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

258 pexp l, pexp r])

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

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

296 [] -> False

297 _ -> 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 [])

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

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

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

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

367 claim valn (Var tyn)

368 letbind n (Var tyn) (Var valn)

369 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)])

371 env <- get_env

372 computeLet n

373 elabE (True, a, inty) sc

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

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

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

434 = 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)

436 then -- simple app, as below

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

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

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

656 -- old ones with an _

657 mkClause args (l, r)

658 = 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)

660 (map (mkLHSarg l) args') in

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

662

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

672 getFC d x = d

673

674 insertLazy :: PTerm -> ElabD PTerm

675− insertLazy t@(PApp _ (PRef _ (UN l)) _) | l == txt "Delay" = 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 -- tpapp

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

677 insertLazy (PCoerced t) = return t

678 insertLazy t =

679 do ty <- goal

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

687 where

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

689 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"))

691 [pexp t])

692

693 insertCoerce ina t =

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

705 return t'

706 where

707 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)])

709

710 -- | Elaborate the arguments to a function

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

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

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

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

725 | lazy && not pattern

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

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

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

728 pexp t])

729 | otherwise = elabArg argName holeName t

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

761pruneAlt xs = map prune xs

762 where

763 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)

765 prune t = t

766

767 choose f (PAlternative a as)

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

771 [a] -> a

772 _ -> PAlternative a as'

773

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)

775 choose f t = t

776

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

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

1097 focus script

1098 ptm <- get_term

1099 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)])

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

1102 -- now that we have the script apply

1103 -- it to the reflected goal