f987aec · Idris-dev · git.iko.soy

src/IRTS/Compiler.hs+3−3

@@ -235,7 +235,7 @@ data VarInfo = VI

235235type Vars = M.Map Name VarInfo

236236

237237irTerm :: Vars -> [Name] -> Term -> Idris LExp

238−irTerm vs env tm@(App f a) = do

238+irTerm vs env tm@(App _ f a) = do

239239 ist <- getIState

240240 case unApply tm of

241241 (P _ (UN m) _, args)

@@ -297,8 +297,8 @@ irTerm vs env tm@(App f a) = do

297297

298298 -- This case is here until we get more general inlining. It's just

299299 -- a really common case, and the laziness hurts...

300− (P _ (NS (UN be) [b,p]) _, [_,x,(App (App (App (P _ (UN d) _) _) _) t),

301− (App (App (App (P _ (UN d') _) _) _) e)])

300+ (P _ (NS (UN be) [b,p]) _, [_,x,(App _ (App _ (App _ (P _ (UN d) _) _) _) t),

301+ (App _ (App _ (App _ (P _ (UN d') _) _) _) e)])

302302 | be == txt "boolElim"

303303 , d == txt "Delay"

304304 , d' == txt "Delay"

src/Idris/AbsSyntaxTree.hs+2−2

@@ -1253,14 +1253,14 @@ infP = P (TCon 6 0) inferTy (TType (UVal 0))

12531253

12541254getInferTerm, getInferType :: Term -> Term

12551255getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc

1256−getInferTerm (App (App _ _) tm) = tm

1256+getInferTerm (App _ (App _ _ _) tm) = tm

12571257getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)

12581258

12591259getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc

12601260 where toTy (Lam t) = Pi Nothing t (TType (UVar 0))

12611261 toTy (PVar t) = PVTy t

12621262 toTy b = b

1263−getInferType (App (App _ ty) _) = ty

1263+getInferType (App _ (App _ _ ty) _) = ty

12641264

12651265

12661266

src/Idris/Apropos.hs+1−1

@@ -77,7 +77,7 @@ instance Apropos (TT Name) where

7777 isApropos str (P (DCon _ _ _) n ty) = isApropos str n || isApropos str ty

7878 isApropos str (P Bound _ ty) = isApropos str ty

7979 isApropos str (Bind n b tm) = isApropos str b || isApropos str tm

80− isApropos str (App t1 t2) = isApropos str t1 || isApropos str t2

80+ isApropos str (App _ t1 t2) = isApropos str t1 || isApropos str t2

8181 isApropos str (Constant const) = isApropos str const

8282 isApropos str _ = False

8383

src/Idris/Core/Binary.hs+4−4

@@ -555,9 +555,9 @@ instance {- (Binary n) => -} Binary (TT Name) where

555555 put x1

556556 put x2

557557 put x3

558− App x1 x2 -> do putWord8 3

559− put x1

560− put x2

558+ App _ x1 x2 -> do putWord8 3

559+ put x1

560+ put x2

561561 Constant x1 -> do putWord8 4

562562 put x1

563563 Proj x1 x2 -> do putWord8 5

@@ -584,7 +584,7 @@ instance {- (Binary n) => -} Binary (TT Name) where

584584 return (Bind x1 x2 x3)

585585 3 -> do x1 <- get

586586 x2 <- get

587− return (App x1 x2)

587+ return (App Complete x1 x2)

588588 4 -> do x1 <- get

589589 return (Constant x1)

590590 5 -> do x1 <- get

src/Idris/Core/CaseTree.hs+8−8

@@ -130,7 +130,7 @@ namesUsed sc = nub $ nu' [] sc where

130130

131131 nut ps (P _ n _) | n `elem` ps = []

132132 | otherwise = [n]

133− nut ps (App f a) = nut ps f ++ nut ps a

133+ nut ps (App _ f a) = nut ps f ++ nut ps a

134134 nut ps (Proj t _) = nut ps t

135135 nut ps (Bind n (Let t v) sc) = nut ps v ++ nut (n:ps) sc

136136 nut ps (Bind n b sc) = nut (n:ps) sc

@@ -155,7 +155,7 @@ findCalls sc topargs = nub $ nu' topargs sc where

155155

156156 nut ps (P Ref n _) | n `elem` ps = []

157157 | otherwise = [(n, [])] -- tmp

158− nut ps fn@(App f a)

158+ nut ps fn@(App _ f a)

159159 | (P Ref n _, args) <- unApply fn

160160 = if n `elem` ps then nut ps f ++ nut ps a

161161 else [(n, map argNames args)] ++ concatMap (nut ps) args

@@ -176,8 +176,8 @@ directUse (P _ n _) = [n]

176176directUse (Bind n (Let t v) sc) = nub $ directUse v ++ (directUse sc \\ [n])

177177 ++ directUse t

178178directUse (Bind n b sc) = nub $ directUse (binderTy b) ++ (directUse sc \\ [n])

179−directUse fn@(App f a)

180− | (P Ref (UN pfk) _, [App e w]) <- unApply fn,

179+directUse fn@(App _ f a)

180+ | (P Ref (UN pfk) _, [App _ e w]) <- unApply fn,

181181 pfk == txt "prim_fork"

182182 = directUse e ++ directUse w -- HACK so that fork works

183183 | (P Ref (UN fce) _, [_, _, a]) <- unApply fn,

@@ -337,7 +337,7 @@ data Pat = PCon Bool Name Int [Pat]

337337

338338toPats :: Bool -> Bool -> Term -> [Pat]

339339toPats reflect tc f = reverse (toPat reflect tc (getArgs f)) where

340− getArgs (App f a) = a : getArgs f

340+ getArgs (App _ f a) = a : getArgs f

341341 getArgs _ = []

342342

343343toPat :: Bool -> Bool -> [Term] -> [Pat]

@@ -362,7 +362,7 @@ toPat reflect tc = map $ toPat' []

362362 = PSuc $ toPat' [] p

363363

364364 toPat' [] (P Bound n ty) = PV n ty

365− toPat' args (App f a) = toPat' (a : args) f

365+ toPat' args (App _ f a) = toPat' (a : args) f

366366 toPat' [] (Constant x) | isTypeConst x = PTyPat

367367 | otherwise = PConst x

368368

@@ -639,7 +639,7 @@ depatt ns tm = dp [] tm

639639 dpa ms x (SucCase n sc) = SucCase n (dp ms sc)

640640 dpa ms x (DefaultCase sc) = DefaultCase (dp ms sc)

641641

642− applyMaps ms f@(App _ _)

642+ applyMaps ms f@(App _ _ _)

643643 | (P nt cn pty, args) <- unApply f

644644 = let args' = map (applyMaps ms) args in

645645 applyMap ms nt cn pty args'

@@ -652,7 +652,7 @@ depatt ns tm = dp [] tm

652652 same n (P _ n' _) = n == n'

653653 same _ _ = False

654654

655− applyMaps ms (App f a) = App (applyMaps ms f) (applyMaps ms a)

655+ applyMaps ms (App s f a) = App s (applyMaps ms f) (applyMaps ms a)

656656 applyMaps ms t = t

657657

658658-- FIXME: Do this for SucCase too

src/Idris/Core/DeepSeq.hs+1−1

@@ -160,7 +160,7 @@ instance (NFData n) => NFData (TT n) where

160160 rnf (P x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

161161 rnf (V x1) = rnf x1 `seq` ()

162162 rnf (Bind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

163− rnf (App x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

163+ rnf (App x1 x2 x3) = rnf x2 `seq` rnf x3 `seq` ()

164164 rnf (Constant x1) = rnf x1 `seq` ()

165165 rnf (Proj x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

166166 rnf Erased = ()

src/Idris/Core/Elaborate.hs+3−3

@@ -258,7 +258,7 @@ checkInjective (tm, l, r) = do ctxt <- get_context

258258 else lift $ tfail (NotInjective tm l r)

259259 where isInj ctxt (P _ n _)

260260 | isConName n ctxt = True

261− isInj ctxt (App f a) = isInj ctxt f

261+ isInj ctxt (App _ f a) = isInj ctxt f

262262 isInj ctxt (Constant _) = True

263263 isInj ctxt (TType _) = True

264264 isInj ctxt (Bind _ (Pi _ _ _) sc) = True

@@ -431,7 +431,7 @@ dotterm = do ES (p, a) s m <- get

431431 where foB (Guess t v) = union (findOuter h env t) (findOuter h (n:env) v)

432432 foB (Let t v) = union (findOuter h env t) (findOuter h env v)

433433 foB b = findOuter h env (binderTy b)

434− findOuter h env (App f a)

434+ findOuter h env (App _ f a)

435435 = union (findOuter h env f) (findOuter h env a)

436436 findOuter h env _ = []

437437

@@ -541,7 +541,7 @@ prepare_apply fn imps =

541541 | n `elem` hs = let n' = uniqueName n hs in

542542 Bind n' (fmap (rebind hs) t) (rebind (n':hs) sc)

543543 | otherwise = Bind n (fmap (rebind hs) t) (rebind (n:hs) sc)

544− rebind hs (App f a) = App (rebind hs f) (rebind hs a)

544+ rebind hs (App s f a) = App s (rebind hs f) (rebind hs a)

545545 rebind hs t = t

546546

547547apply, match_apply :: Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)]

src/Idris/Core/Evaluate.hs+11−11

@@ -285,7 +285,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

285285 = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t

286286 -- block reduction immediately under codata (and not forced)

287287 ev ntimes stk top env

288− (App (App (App d@(P _ (UN dly) _) l@(P _ (UN lco) _)) t) arg)

288+ (App _ (App _ (App _ d@(P _ (UN dly) _) l@(P _ (UN lco) _)) t) arg)

289289 | dly == txt "Delay" && lco == txt "LazyCodata" && not (simpl || atRepl)

290290 = do let (f, _) = unApply arg

291291 let ntimes' = case f of

@@ -299,11 +299,11 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

299299 when spec $ setBlock False

300300 evApply ntimes' stk top env [l',t',arg'] d'

301301 -- Treat "assert_total" specially, as long as it's defined!

302− ev ntimes stk top env (App (App (P _ n@(UN at) _) _) arg)

302+ ev ntimes stk top env (App _ (App _ (P _ n@(UN at) _) _) arg)

303303 | [(CaseOp _ _ _ _ _ _, _)] <- lookupDefAcc n (spec || atRepl) ctxt,

304304 at == txt "assert_total" && not simpl

305305 = ev ntimes (n : stk) top env arg

306− ev ntimes stk top env (App f a)

306+ ev ntimes stk top env (App _ f a)

307307 = do f' <- ev ntimes stk False env f

308308 a' <- ev ntimes stk False env a

309309 evApply ntimes stk top env [a'] f'

@@ -434,7 +434,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

434434 Just (altmap, sc) -> evTree ntimes stk top env altmap sc

435435 _ -> return Nothing

436436

437− conHeaded tm@(App _ _)

437+ conHeaded tm@(App _ _ _)

438438 | (P (DCon _ _ _) _ _, args) <- unApply tm = True

439439 conHeaded t = False

440440

@@ -540,7 +540,7 @@ instance Quote Value where

540540 v' <- quote i v

541541 let sc'' = pToV (sMN vd "vlet") (addBinder sc')

542542 return (Bind n (Let t' v') sc'')

543− quote i (VApp f a) = liftM2 App (quote i f) (quote i a)

543+ quote i (VApp f a) = liftM2 (App Complete) (quote i f) (quote i a)

544544 quote i (VType u) = return $ TType u

545545 quote i (VUType u) = return $ UType u

546546 quote i VErased = return $ Erased

@@ -576,13 +576,13 @@ convEq ctxt holes topx topy = ceq [] topx topy where

576576 | x `elem` holes || y `elem` holes = return True

577577 | x == y || (x, y) `elem` ps || (y,x) `elem` ps = return True

578578 | otherwise = sameDefs ps x y

579− ceq ps x (Bind n (Lam t) (App y (V 0)))

579+ ceq ps x (Bind n (Lam t) (App Complete y (V 0)))

580580 = ceq ps x (substV (P Bound n t) y)

581− ceq ps (Bind n (Lam t) (App x (V 0))) y

581+ ceq ps (Bind n (Lam t) (App Complete x (V 0))) y

582582 = ceq ps (substV (P Bound n t) x) y

583− ceq ps x (Bind n (Lam t) (App y (P Bound n' _)))

583+ ceq ps x (Bind n (Lam t) (App Complete y (P Bound n' _)))

584584 | n == n' = ceq ps x y

585− ceq ps (Bind n (Lam t) (App x (P Bound n' _))) y

585+ ceq ps (Bind n (Lam t) (App Complete x (P Bound n' _))) y

586586 | n == n' = ceq ps x y

587587

588588 ceq ps (Bind n (PVar t) sc) y = ceq ps sc y

@@ -604,7 +604,7 @@ convEq ctxt holes topx topy = ceq [] topx topy where

604604 ceqB ps (Guess v t) (Guess v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')

605605 ceqB ps (Pi i v t) (Pi i' v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')

606606 ceqB ps b b' = ceq ps (binderTy b) (binderTy b')

607− ceq ps (App fx ax) (App fy ay) = liftM2 (&&) (ceq ps fx fy) (ceq ps ax ay)

607+ ceq ps (App _ fx ax) (App _ fy ay) = liftM2 (&&) (ceq ps fx fy) (ceq ps ax ay)

608608 ceq ps (Constant x) (Constant y) = return (x == y)

609609 ceq ps (TType x) (TType y) = do (v, cs) <- get

610610 put (v, ULE x y : cs)

@@ -1083,5 +1083,5 @@ uniqueBindersCtxt :: Context -> [Name] -> TT Name -> TT Name

10831083uniqueBindersCtxt ctxt ns (Bind n b sc)

10841084 = let n' = uniqueNameCtxt ctxt n ns in

10851085 Bind n' (fmap (uniqueBindersCtxt ctxt (n':ns)) b) (uniqueBindersCtxt ctxt ns sc)

1086−uniqueBindersCtxt ctxt ns (App f a) = App (uniqueBindersCtxt ctxt ns f) (uniqueBindersCtxt ctxt ns a)

1086+uniqueBindersCtxt ctxt ns (App s f a) = App s (uniqueBindersCtxt ctxt ns f) (uniqueBindersCtxt ctxt ns a)

10871087uniqueBindersCtxt ctxt ns t = t

src/Idris/Core/Execute.hs+2−2

@@ -103,7 +103,7 @@ toTT (EBind n b body) = do n' <- newN n

103103 return n'

104104toTT (EApp e1 e2) = do e1' <- toTT e1

105105 e2' <- toTT e2

106− return $ App e1' e2'

106+ return $ App Complete e1' e2'

107107toTT (EType u) = return $ TType u

108108toTT (EUType u) = return $ UType u

109109toTT EErased = return Erased

@@ -192,7 +192,7 @@ doExec env ctxt (Bind n (NLet t v) body) = trace "NLet" $ undefined

192192doExec env ctxt tm@(Bind n b body) = do b' <- forM b (doExec env ctxt)

193193 return $

194194 EBind n b' (\arg -> doExec ((n, arg):env) ctxt body)

195−doExec env ctxt a@(App _ _) =

195+doExec env ctxt a@(App _ _ _) =

196196 do let (f, args) = unApply a

197197 f' <- doExec env ctxt f

198198 args' <- case f' of

src/Idris/Core/ProofState.hs+4−4

@@ -328,7 +328,7 @@ computeLet ctxt n tm = cl [] tm where

328328 | n' == n = let v' = normalise ctxt env v in

329329 Bind n' (Let t v') sc

330330 cl env (Bind n' b sc) = Bind n' (fmap (cl env) b) (cl ((n, b):env) sc)

331− cl env (App f a) = App (cl env f) (cl env a)

331+ cl env (App s f a) = App s (cl env f) (cl env a)

332332 cl env t = t

333333

334334attack :: RunTactic

@@ -661,9 +661,9 @@ rewrite _ _ _ _ = fail "Can't rewrite here"

661661-- an x, and put \x : lt in front

662662mkP :: TT Name -> TT Name -> TT Name -> TT Name -> TT Name

663663mkP lt l r ty | l == ty = lt

664−mkP lt l r (App f a) = let f' = if (r /= f) then mkP lt l r f else f

665− a' = if (r /= a) then mkP lt l r a else a in

666− App f' a'

664+mkP lt l r (App s f a) = let f' = if (r /= f) then mkP lt l r f else f

665+ a' = if (r /= a) then mkP lt l r a else a in

666+ App s f' a'

667667mkP lt l r (Bind n b sc)

668668 = let b' = mkPB b

669669 sc' = if (r /= sc) then mkP lt l r sc else sc in

src/Idris/Core/ProofTerm.hs+17−17

@@ -21,8 +21,8 @@ import Debug.Trace

2121

2222-- | A zipper over terms, in order to efficiently update proof terms.

2323data TermPath = Top

24− | AppL TermPath Term

25− | AppR Term TermPath

24+ | AppL (AppStatus Name) TermPath Term

25+ | AppR (AppStatus Name) Term TermPath

2626 | InBind Name BinderPath Term

2727 | InScope Name (Binder Term) TermPath

2828 deriving Show

@@ -39,8 +39,8 @@ data BinderPath = Binder (Binder TermPath)

3939-- words, "graft" one term path into another.

4040replaceTop :: TermPath -> TermPath -> TermPath

4141replaceTop p Top = p

42−replaceTop p (AppL l t) = AppL (replaceTop p l) t

43−replaceTop p (AppR t r) = AppR t (replaceTop p r)

42+replaceTop p (AppL s l t) = AppL s (replaceTop p l) t

43+replaceTop p (AppR s t r) = AppR s t (replaceTop p r)

4444replaceTop p (InBind n bp sc) = InBind n (replaceTopB p bp) sc

4545 where

4646 replaceTopB p (Binder b) = Binder (fmap (replaceTop p) b)

@@ -53,8 +53,8 @@ replaceTop p (InScope n b sc) = InScope n b (replaceTop p sc)

5353-- | Build a term from a zipper, given something to put in the hole.

5454rebuildTerm :: Term -> TermPath -> Term

5555rebuildTerm tm Top = tm

56−rebuildTerm tm (AppL p a) = App (rebuildTerm tm p) a

57−rebuildTerm tm (AppR f p) = App f (rebuildTerm tm p)

56+rebuildTerm tm (AppL s p a) = App s (rebuildTerm tm p) a

57+rebuildTerm tm (AppR s f p) = App s f (rebuildTerm tm p)

5858rebuildTerm tm (InScope n b p) = Bind n b (rebuildTerm tm p)

5959rebuildTerm tm (InBind n bp sc) = Bind n (rebuildBinder tm bp) sc

6060

@@ -73,9 +73,9 @@ findHole :: Name -> Env -> Term -> Maybe (TermPath, Env, Term)

7373findHole n env t = fh' env Top t where

7474 fh' env path tm@(Bind x h sc)

7575 | hole h && n == x = Just (path, env, tm)

76− fh' env path (App f a)

77− | Just (p, env', tm) <- fh' env path a = Just (AppR f p, env', tm)

78− | Just (p, env', tm) <- fh' env path f = Just (AppL p a, env', tm)

76+ fh' env path (App s f a)

77+ | Just (p, env', tm) <- fh' env path a = Just (AppR s f p, env', tm)

78+ | Just (p, env', tm) <- fh' env path f = Just (AppL s p a, env', tm)

7979 fh' env path (Bind x b sc)

8080 | Just (bp, env', tm) <- fhB env path b = Just (InBind x bp sc, env', tm)

8181 | Just (p, env', tm) <- fh' ((x,b):env) path sc = Just (InScope x b p, env', tm)

@@ -165,10 +165,10 @@ updateSolvedTerm' xs x = updateSolved' xs x where

165165 (b', ub) = updateSolvedB' xs b in

166166 if ut || ub then (Bind n b' t', True)

167167 else (tm, False)

168− updateSolved' xs t@(App f a)

168+ updateSolved' xs t@(App s f a)

169169 = let (f', uf) = updateSolved' xs f

170170 (a', ua) = updateSolved' xs a in

171− if uf || ua then (App f' a', True)

171+ if uf || ua then (App s f' a', True)

172172 else (t, False)

173173 updateSolved' xs t@(P _ n@(MN _ _) _)

174174 | Just v <- lookup n xs = (v, True)

@@ -189,7 +189,7 @@ updateSolvedTerm' xs x = updateSolved' xs x where

189189 if u then (b { binderTy = ty' }, u) else (b, False)

190190

191191 noneOf ns (P _ n _) | n `elem` ns = False

192− noneOf ns (App f a) = noneOf ns a && noneOf ns f

192+ noneOf ns (App s f a) = noneOf ns a && noneOf ns f

193193 noneOf ns (Bind n (Hole ty) t) = n `notElem` ns && noneOf ns ty && noneOf ns t

194194 noneOf ns (Bind n b t) = noneOf ns t && noneOfB ns b

195195 where

@@ -208,8 +208,8 @@ updateEnv ns ((n, b) : env) = (n, fmap (updateSolvedTerm ns) b) : updateEnv ns e

208208updateSolvedPath :: [(Name, Term)] -> TermPath -> TermPath

209209updateSolvedPath [] t = t

210210updateSolvedPath ns Top = Top

211−updateSolvedPath ns (AppL p r) = AppL (updateSolvedPath ns p) (updateSolvedTerm ns r)

212−updateSolvedPath ns (AppR l p) = AppR (updateSolvedTerm ns l) (updateSolvedPath ns p)

211+updateSolvedPath ns (AppL s p r) = AppL s (updateSolvedPath ns p) (updateSolvedTerm ns r)

212+updateSolvedPath ns (AppR s l p) = AppR s (updateSolvedTerm ns l) (updateSolvedPath ns p)

213213updateSolvedPath ns (InBind n b sc)

214214 = InBind n (updateSolvedPathB b) (updateSolvedTerm ns sc)

215215 where

@@ -246,7 +246,7 @@ goal h pt@(PT path env sub ups)

246246 g env (Bind n b sc) | hole b && same h n = return $ GD env b

247247 | otherwise

248248 = g ((n, b):env) sc `mplus` gb env b

249− g env (App f a) = g env a `mplus` g env f

249+ g env (App _ f a) = g env a `mplus` g env f

250250 g env t = fail "Can't find hole"

251251

252252 gb env (Let t v) = g env v `mplus` g env t

@@ -291,7 +291,7 @@ atHole h f c e pt -- @(PT path env sub)

291291 if u then return (Bind n b sc', True)

292292 else do (b', u) <- atHb f c env b

293293 return (Bind n b' sc', u)

294− atH tac c env (App f a) = ulift2 tac c env App f a

294+ atH tac c env (App s f a) = ulift2 tac c env (App s) f a

295295 atH tac c env t = return (t, False)

296296

297297 atHb f c env (Let t v) = ulift2 f c env Let t v

@@ -308,6 +308,6 @@ bound_in_term (Bind n b sc) = n : bi b ++ bound_in_term sc

308308 bi (Let t v) = bound_in_term t ++ bound_in_term v

309309 bi (Guess t v) = bound_in_term t ++ bound_in_term v

310310 bi b = bound_in_term (binderTy b)

311−bound_in_term (App f a) = bound_in_term f ++ bound_in_term a

311+bound_in_term (App _ f a) = bound_in_term f ++ bound_in_term a

312312bound_in_term _ = []

313313

src/Idris/Core/TT.hs+45−40

@@ -807,6 +807,11 @@ instance Eq NameType where

807807 TCon _ a == TCon _ b = (a == b) -- ignore tag

808808 _ == _ = False

809809

810+data AppStatus n = Complete

811+ | MaybeHoles

812+ | Holes [n]

813+ deriving (Eq, Ord, Functor, Data, Typeable, Show)

814+

810815-- | Terms in the core language. The type parameter is the type of

811816-- identifiers used for bindings and explicit named references;

812817-- usually we use @TT 'Name'@.

@@ -815,7 +820,7 @@ data TT n = P NameType n (TT n) -- ^ named references with type

815820 -- Pure Type Systems Formalized)

816821 | V !Int -- ^ a resolved de Bruijn-indexed variable

817822 | Bind n !(Binder (TT n)) (TT n) -- ^ a binding

818− | App !(TT n) (TT n) -- ^ function, function type, arg

823+ | App (AppStatus n) !(TT n) (TT n) -- ^ function, function type, arg

819824 | Constant Const -- ^ constant

820825 | Proj (TT n) !Int -- ^ argument projection; runtime only

821826 -- (-1) is a special case for 'subtract one from BI'

@@ -851,7 +856,7 @@ instance TermSize (TT Name) where

851856 termsize n (Bind n' b sc)

852857 = let rn = if n == n' then sMN 0 "noname" else n in

853858 termsize rn sc

854− termsize n (App f a) = termsize n f + termsize n a

859+ termsize n (App _ f a) = termsize n f + termsize n a

855860 termsize n (Proj t i) = termsize n t

856861 termsize n _ = 1

857862

@@ -859,7 +864,7 @@ instance Sized a => Sized (TT a) where

859864 size (P name n trm) = 1 + size name + size n + size trm

860865 size (V v) = 1

861866 size (Bind nm binder bdy) = 1 + size nm + size binder + size bdy

862− size (App l r) = 1 + size l + size r

867+ size (App _ l r) = 1 + size l + size r

863868 size (Constant c) = size c

864869 size Erased = 1

865870 size (TType u) = 1 + size u

@@ -880,8 +885,8 @@ instance Eq n => Eq (TT n) where

880885 (==) (P xt x _) (P yt y _) = x == y

881886 (==) (V x) (V y) = x == y

882887 (==) (Bind _ xb xs) (Bind _ yb ys) = xs == ys && xb == yb

883− (==) (App fx ax) (App fy ay) = ax == ay && fx == fy

884− (==) (TType _) (TType _) = True -- deal with constraints later

888+ (==) (App _ fx ax) (App _ fy ay) = ax == ay && fx == fy

889+ (==) (TType _) (TType _) = True -- deal with constraints later

885890 (==) (Constant x) (Constant y) = x == y

886891 (==) (Proj x i) (Proj y j) = x == y && i == j

887892 (==) Erased _ = True

@@ -897,15 +902,15 @@ isInjective :: TT n -> Bool

897902isInjective (P (DCon _ _ _) _ _) = True

898903isInjective (P (TCon _ _) _ _) = True

899904isInjective (Constant _) = True

900−isInjective (TType x) = True

905+isInjective (TType x) = True

901906isInjective (Bind _ (Pi _ _ _) sc) = True

902−isInjective (App f a) = isInjective f

907+isInjective (App _ f a) = isInjective f

903908isInjective _ = False

904909

905910-- | Count the number of instances of a de Bruijn index in a term

906911vinstances :: Int -> TT n -> Int

907912vinstances i (V x) | i == x = 1

908−vinstances i (App f a) = vinstances i f + vinstances i a

913+vinstances i (App _ f a) = vinstances i f + vinstances i a

909914vinstances i (Bind x b sc) = instancesB b + vinstances (i + 1) sc

910915 where instancesB (Let t v) = vinstances i v

911916 instancesB _ = 0

@@ -917,7 +922,7 @@ instantiate e = subst 0 where

917922 subst i (P nt x ty) = P nt x (subst i ty)

918923 subst i (V x) | i == x = e

919924 subst i (Bind x b sc) = Bind x (fmap (subst i) b) (subst (i+1) sc)

920− subst i (App f a) = App (subst i f) (subst i a)

925+ subst i (App s f a) = App s (subst i f) (subst i a)

921926 subst i (Proj x idx) = Proj (subst i x) idx

922927 subst i t = t

923928

@@ -930,7 +935,7 @@ substV x tm = dropV 0 (instantiate x tm) where

930935 dropV i (V x) | x > i = V (x - 1)

931936 | otherwise = V x

932937 dropV i (Bind x b sc) = Bind x (fmap (dropV i) b) (dropV (i+1) sc)

933− dropV i (App f a) = App (dropV i f) (dropV i a)

938+ dropV i (App s f a) = App s (dropV i f) (dropV i a)

934939 dropV i (Proj x idx) = Proj (dropV i x) idx

935940 dropV i t = t

936941

@@ -941,7 +946,7 @@ explicitNames (Bind x b sc) = let b' = fmap explicitNames b in

941946 Bind x b'

942947 (explicitNames (instantiate

943948 (P Bound x (binderTy b')) sc))

944−explicitNames (App f a) = App (explicitNames f) (explicitNames a)

949+explicitNames (App s f a) = App s (explicitNames f) (explicitNames a)

945950explicitNames (Proj x idx) = Proj (explicitNames x) idx

946951explicitNames t = t

947952

@@ -955,7 +960,7 @@ pToV' n i (Bind x b sc)

955960-- resolve names from the *outer* scope which may happen to have the same id.

956961 | n == x = Bind x (fmap (pToV' n i) b) sc

957962 | otherwise = Bind x (fmap (pToV' n i) b) (pToV' n (i+1) sc)

958−pToV' n i (App f a) = App (pToV' n i f) (pToV' n i a)

963+pToV' n i (App s f a) = App s (pToV' n i f) (pToV' n i a)

959964pToV' n i (Proj t idx) = Proj (pToV' n i t) idx

960965pToV' n i t = t

961966

@@ -966,7 +971,7 @@ addBinder t = ab 0 t

966971 ab top (V i) | i >= top = V (i + 1)

967972 | otherwise = V i

968973 ab top (Bind x b sc) = Bind x (fmap (ab top) b) (ab (top + 1) sc)

969− ab top (App f a) = App (ab top f) (ab top a)

974+ ab top (App s f a) = App s (ab top f) (ab top a)

970975 ab top (Proj t idx) = Proj (ab top t) idx

971976 ab top t = t

972977

@@ -985,14 +990,14 @@ vToP = vToP' [] where

985990 P Bound n (binderTy b)

986991 vToP' env (Bind n b sc) = let b' = fmap (vToP' env) b in

987992 Bind n b' (vToP' ((n, b'):env) sc)

988− vToP' env (App f a) = App (vToP' env f) (vToP' env a)

993+ vToP' env (App s f a) = App s (vToP' env f) (vToP' env a)

989994 vToP' env t = t

990995

991996-- | Replace every non-free reference to the name of a binding in

992997-- the given term with a de Bruijn index.

993998finalise :: Eq n => TT n -> TT n

994999finalise (Bind x b sc) = Bind x (fmap finalise b) (pToV x (finalise sc))

995−finalise (App f a) = App (finalise f) (finalise a)

1000+finalise (App s f a) = App s (finalise f) (finalise a)

9961001finalise t = t

9971002

9981003-- Once we've finished checking everything about a term we no longer need

@@ -1000,7 +1005,7 @@ finalise t = t

10001005

10011006pEraseType :: TT n -> TT n

10021007pEraseType (P nt t _) = P nt t Erased

1003−pEraseType (App f a) = App (pEraseType f) (pEraseType a)

1008+pEraseType (App s f a) = App s (pEraseType f) (pEraseType a)

10041009pEraseType (Bind n b sc) = Bind n (fmap pEraseType b) (pEraseType sc)

10051010pEraseType t = t

10061011

@@ -1027,9 +1032,9 @@ subst n v tm = fst $ subst' 0 tm

10271032 = let (b', ub) = substB' i b

10281033 (sc', usc) = subst' (i+1) sc in

10291034 if ub || usc then (Bind x b' sc', True) else (t, False)

1030− subst' i t@(App f a) = let (f', uf) = subst' i f

1031− (a', ua) = subst' i a in

1032− if uf || ua then (App f' a', True) else (t, False)

1035+ subst' i t@(App s f a) = let (f', uf) = subst' i f

1036+ (a', ua) = subst' i a in

1037+ if uf || ua then (App s f' a', True) else (t, False)

10331038 subst' i t@(Proj x idx) = let (x', u) = subst' i x in

10341039 if u then (Proj x' idx, u) else (t, False)

10351040 subst' i t = (t, False)

@@ -1054,7 +1059,7 @@ psubst n v tm = s' 0 tm where

10541059 s' i (P _ x _) | n == x = v

10551060 s' i (Bind x b sc) | n == x = Bind x (fmap (s' i) b) sc

10561061 | otherwise = Bind x (fmap (s' i) b) (s' (i+1) sc)

1057− s' i (App f a) = App (s' i f) (s' i a)

1062+ s' i (App st f a) = App st (s' i f) (s' i a)

10581063 s' i (Proj t idx) = Proj (s' i t) idx

10591064 s' i t = t

10601065

@@ -1072,7 +1077,7 @@ substTerm :: Eq n => TT n {-^ Old term -} ->

10721077 -> TT n

10731078substTerm old new = st where

10741079 st t | t == old = new

1075− st (App f a) = App (st f) (st a)

1080+ st (App s f a) = App s (st f) (st a)

10761081 st (Bind x b sc) = Bind x (fmap st b) (st sc)

10771082 st t = t

10781083

@@ -1086,7 +1091,7 @@ occurrences n t = execState (no' 0 t) 0

10861091 where noB' i (Let t v) = do no' i t; no' i v

10871092 noB' i (Guess t v) = do no' i t; no' i v

10881093 noB' i b = no' i (binderTy b)

1089− no' i (App f a) = do no' i f; no' i a

1094+ no' i (App _ f a) = do no' i f; no' i a

10901095 no' i (Proj x _) = no' i x

10911096 no' i _ = return ()

10921097

@@ -1100,7 +1105,7 @@ noOccurrence n t = no' 0 t

11001105 where noB' i (Let t v) = no' i t && no' i v

11011106 noB' i (Guess t v) = no' i t && no' i v

11021107 noB' i b = no' i (binderTy b)

1103− no' i (App f a) = no' i f && no' i a

1108+ no' i (App _ f a) = no' i f && no' i a

11041109 no' i (Proj x _) = no' i x

11051110 no' i _ = True

11061111

@@ -1112,7 +1117,7 @@ freeNames t = nub $ freeNames' t

11121117 freeNames' (Bind n (Let t v) sc) = freeNames' v ++ (freeNames' sc \\ [n])

11131118 ++ freeNames' t

11141119 freeNames' (Bind n b sc) = freeNames' (binderTy b) ++ (freeNames' sc \\ [n])

1115− freeNames' (App f a) = freeNames' f ++ freeNames' a

1120+ freeNames' (App _ f a) = freeNames' f ++ freeNames' a

11161121 freeNames' (Proj x i) = freeNames' x

11171122 freeNames' _ = []

11181123

@@ -1124,14 +1129,14 @@ arity _ = 0

11241129-- | Deconstruct an application; returns the function and a list of arguments

11251130unApply :: TT n -> (TT n, [TT n])

11261131unApply t = ua [] t where

1127− ua args (App f a) = ua (a:args) f

1132+ ua args (App _ f a) = ua (a:args) f

11281133 ua args t = (t, args)

11291134

11301135-- | Returns a term representing the application of the first argument

11311136-- (a function) to every element of the second argument.

11321137mkApp :: TT n -> [TT n] -> TT n

11331138mkApp f [] = f

1134−mkApp f (a:as) = mkApp (App f a) as

1139+mkApp f (a:as) = mkApp (App MaybeHoles f a) as

11351140

11361141unList :: Term -> Maybe [Term]

11371142unList tm = case unApply tm of

@@ -1172,7 +1177,7 @@ safeForgetEnv env (Bind n b sc)

11721177 (safeForgetEnv env v)

11731178 safeForgetEnvB env b = do ty' <- safeForgetEnv env (binderTy b)

11741179 Just $ fmap (\_ -> ty') b

1175−safeForgetEnv env (App f a) = liftM2 RApp (safeForgetEnv env f) (safeForgetEnv env a)

1180+safeForgetEnv env (App _ f a) = liftM2 RApp (safeForgetEnv env f) (safeForgetEnv env a)

11761181safeForgetEnv env (Constant c) = Just $ RConstant c

11771182safeForgetEnv env (TType i) = Just RType

11781183safeForgetEnv env (UType u) = Just $ RUType u

@@ -1225,7 +1230,7 @@ uniqueBinders ns = ubSet (fromList ns) where

12251230 = let n' = uniqueNameSet n ns

12261231 ns' = insert n' ns in

12271232 Bind n' (fmap (ubSet ns') b) (ubSet ns' sc)

1228− ubSet ns (App f a) = App (ubSet ns f) (ubSet ns a)

1233+ ubSet ns (App s f a) = App s (ubSet ns f) (ubSet ns a)

12291234 ubSet ns t = t

12301235

12311236

@@ -1318,7 +1323,7 @@ prettyEnv env t = prettyEnv' env t False

13181323 bracket p 2 $ prettySb env n b debug <> prettySe 10 ((n, b):env) sc debug

13191324 prettySe p env (Bind n b sc) debug =

13201325 bracket p 2 $ prettySb env n b debug <> prettySe 10 ((n, b):env) sc debug

1321− prettySe p env (App f a) debug =

1326+ prettySe p env (App _ f a) debug =

13221327 bracket p 1 $ prettySe 1 env f debug <+> prettySe 0 env a debug

13231328 prettySe p env (Proj x i) debug =

13241329 prettySe 1 env x debug <+> text ("!" ++ show i)

@@ -1362,7 +1367,7 @@ showEnv' env t dbg = se 10 env t where

13621367 where arrow (TType _) = " -> "

13631368 arrow u = " [" ++ show u ++ "] -> "

13641369 se p env (Bind n b sc) = bracket p 2 $ sb env n b ++ se 10 ((n,b):env) sc

1365− se p env (App f a) = bracket p 1 $ se 1 env f ++ " " ++ se 0 env a

1370+ se p env (App _ f a) = bracket p 1 $ se 1 env f ++ " " ++ se 0 env a

13661371 se p env (Proj x i) = se 1 env x ++ "!" ++ show i

13671372 se p env (Constant c) = show c

13681373 se p env Erased = "[__]"

@@ -1387,9 +1392,9 @@ showEnv' env t dbg = se 10 env t where

13871392 bracket outer inner str | inner > outer = "(" ++ str ++ ")"

13881393 | otherwise = str

13891394

1390−-- | Check whether a term has any holes in it - impure if so

1395+-- | Check whether a term has any hole bindings in it - impure if so

13911396pureTerm :: TT Name -> Bool

1392−pureTerm (App f a) = pureTerm f && pureTerm a

1397+pureTerm (App _ f a) = pureTerm f && pureTerm a

13931398pureTerm (Bind n b sc) = notClassName n && pureBinder b && pureTerm sc where

13941399 pureBinder (Hole _) = False

13951400 pureBinder (Guess _ _) = False

@@ -1405,7 +1410,7 @@ pureTerm _ = True

14051410weakenTm :: Int -> TT n -> TT n

14061411weakenTm i t = wk i 0 t

14071412 where wk i min (V x) | x >= min = V (i + x)

1408− wk i m (App f a) = App (wk i m f) (wk i m a)

1413+ wk i m (App s f a) = App s (wk i m f) (wk i m a)

14091414 wk i m (Bind x b sc) = Bind x (wkb i m b) (wk i (m + 1) sc)

14101415 wk i m t = t

14111416 wkb i m t = fmap (wk i m) t

@@ -1430,7 +1435,7 @@ weakenTmEnv i = map (\ (n, b) -> (n, fmap (weakenTm i) b))

14301435orderPats :: Term -> Term

14311436orderPats tm = op [] tm

14321437 where

1433− op [] (App f a) = App f (op [] a) -- for Infer terms

1438+ op [] (App s f a) = App s f (op [] a) -- for Infer terms

14341439

14351440 op ps (Bind n (PVar t) sc) = op ((n, PVar t) : ps) sc

14361441 op ps (Bind n (Hole t) sc) = op ((n, Hole t) : ps) sc

@@ -1455,7 +1460,7 @@ refsIn (Bind n b t) = nub $ nb b ++ refsIn t

14551460 where nb (Let t v) = nub (refsIn t) ++ nub (refsIn v)

14561461 nb (Guess t v) = nub (refsIn t) ++ nub (refsIn v)

14571462 nb t = refsIn (binderTy t)

1458−refsIn (App f a) = nub (refsIn f ++ refsIn a)

1463+refsIn (App s f a) = nub (refsIn f ++ refsIn a)

14591464refsIn _ = []

14601465

14611466-- Make sure all the pattern bindings are as far out as possible

@@ -1492,9 +1497,9 @@ liftPats tm = let (tm', ps) = runState (getPats tm) [] in

14921497 return (Bind n (Hole t') sc')

14931498

14941499

1495− getPats (App f a) = do f' <- getPats f

1496− a' <- getPats a

1497− return (App f' a')

1500+ getPats (App s f a) = do f' <- getPats f

1501+ a' <- getPats a

1502+ return (App s f' a')

14981503 getPats t = return t

14991504

15001505allTTNames :: Eq n => TT n -> [n]

@@ -1504,7 +1509,7 @@ allTTNames = nub . allNamesIn

15041509 where nb (Let t v) = allNamesIn t ++ allNamesIn v

15051510 nb (Guess t v) = allNamesIn t ++ allNamesIn v

15061511 nb t = allNamesIn (binderTy t)

1507− allNamesIn (App f a) = allNamesIn f ++ allNamesIn a

1512+ allNamesIn (App _ f a) = allNamesIn f ++ allNamesIn a

15081513 allNamesIn _ = []

15091514

15101515

@@ -1527,7 +1532,7 @@ pprintTT bound tm = pp startPrec bound tm

15271532 | otherwise = text ("{{{V" ++ show i ++ "}}}")

15281533 pp p bound (Bind n b sc) = ppb p bound n b $

15291534 pp startPrec (n:bound) sc

1530− pp p bound (App tm1 tm2) =

1535+ pp p bound (App _ tm1 tm2) =

15311536 bracket p appPrec . group . hang 2 $

15321537 pp appPrec bound tm1 <> line <>

15331538 pp (appPrec + 1) bound tm2

src/Idris/Core/Typecheck.hs+8−5

@@ -77,6 +77,9 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

7777 smaller _ (UType u) = UType u

7878 smaller x _ = x

7979

80+ astate | holes = MaybeHoles

81+ | otherwise = Complete

82+

8083 chk :: Type -> -- uniqueness level

8184 Env -> Raw -> StateT UCs TC (Term, Type)

8285 chk u env (Var n)

@@ -101,13 +104,13 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

101104 put (v+1, ULT (UVar v) v' : cs)

102105 let apty = simplify initContext env

103106 (Bind x (Let (TType v') (TType (UVar v))) t)

104− return (App fv (TType (UVar v)), apty)

107+ return (App Complete fv (TType (UVar v)), apty)

105108 Bind x (Pi i s k) t ->

106109 do (av, aty) <- chk u env RType

107110 convertsC ctxt env aty s

108111 let apty = simplify initContext env

109112 (Bind x (Let aty av) t)

110− return (App fv av, apty)

113+ return (App astate fv av, apty)

111114 t -> lift $ tfail $ NonFunctionType fv fty

112115 chk u env ap@(RApp f a)

113116 = do (fv, fty) <- chk u env f

@@ -123,7 +126,7 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

123126 do convertsC ctxt env aty s

124127 let apty = simplify initContext env

125128 (Bind x (Let aty av) t)

126− return (App fv av, apty)

129+ return (App astate fv av, apty)

127130 t -> lift $ tfail $ NonFunctionType fv fty

128131 chk u env RType

129132 | holes = return (TType (UVal 0), TType (UVal 0))

@@ -298,7 +301,7 @@ checkUnique borrowed ctxt env tm

298301 chkBinders env (P _ n _) = chkName n

299302 -- 'lending' a unique or nulltype variable doesn't count as a use,

300303 -- but we still can't lend something that's already been used.

301− chkBinders env (App (App (P _ (NS (UN lend) [owner]) _) t) a)

304+ chkBinders env (App _ (App _ (P _ (NS (UN lend) [owner]) _) t) a)

302305 | isVar a && owner == txt "Ownership" &&

303306 (lend == txt "lend" || lend == txt "Read")

304307 = do chkBinders env t -- Check the type normally

@@ -307,7 +310,7 @@ checkUnique borrowed ctxt env tm

307310 put (filter (\(n, (ok, _)) -> ok /= LendOnly) st)

308311 chkBinders env a

309312 put st -- Reset the old state after checking the argument

310− chkBinders env (App f a) = do chkBinders env f; chkBinders env a

313+ chkBinders env (App _ f a) = do chkBinders env f; chkBinders env a

311314 chkBinders env (Bind n b t)

312315 = do chkBinderName env n b

313316 st <- get

src/Idris/Core/Unify.hs+33−35

@@ -96,22 +96,22 @@ match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =

9696 -- but it scares me. However, matching is never guaranteed to give a unique

9797 -- answer, merely a valid one, so perhaps we're okay.

9898 -- In other words: it may vanish without warning some day :)

99− un names x tm@(App (P _ f (Bind fn (Pi _ t _) sc)) a)

99+ un names x tm@(App _ (P _ f (Bind fn (Pi _ t _) sc)) a)

100100 | (P (TCon _ _) _ _, _) <- unApply x,

101101 holeIn env f || f `elem` holes

102102 = let n' = uniqueName (sMN 0 "mv") (map fst env) in

103103 checkCycle names (f, Bind n' (Lam t) x)

104− un names tm@(App (P _ f (Bind fn (Pi _ t _) sc)) a) x

104+ un names tm@(App _ (P _ f (Bind fn (Pi _ t _) sc)) a) x

105105 | (P (TCon _ _) _ _, _) <- unApply x,

106106 holeIn env f || f `elem` holes

107107 = let n' = uniqueName fn (map fst env) in

108108 checkCycle names (f, Bind n' (Lam t) x)

109− un names x tm@(App (P _ f (Bind fn (Pi _ t _) sc)) a)

109+ un names x tm@(App _ (P _ f (Bind fn (Pi _ t _) sc)) a)

110110 | (P (DCon _ _ _) _ _, _) <- unApply x,

111111 holeIn env f || f `elem` holes

112112 = let n' = uniqueName (sMN 0 "mv") (map fst env) in

113113 checkCycle names (f, Bind n' (Lam t) x)

114− un names tm@(App (P _ f (Bind fn (Pi _ t _) sc)) a) x

114+ un names tm@(App _ (P _ f (Bind fn (Pi _ t _) sc)) a) x

115115 | (P (DCon _ _ _) _ _, _) <- unApply x,

116116 holeIn env f || f `elem` holes

117117 = let n' = uniqueName fn (map fst env) in

@@ -135,7 +135,7 @@ match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =

135135 = do h1 <- uB bnames bx by

136136 h2 <- un (((x, y), binderTy bx) : bnames) sx sy

137137 combine bnames h1 h2

138− un names (App fx ax) (App fy ay)

138+ un names (App _ fx ax) (App _ fy ay)

139139 = do hf <- un names fx fy

140140 ha <- un names ax ay

141141 combine names hf ha

@@ -218,7 +218,7 @@ match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =

218218 bind i ns tm

219219 | i < 0 = tm

220220 | otherwise = let ((x,y),ty) = ns!!i in

221− App (Bind y (Lam ty) (bind (i-1) ns tm))

221+ App MaybeHoles (Bind y (Lam ty) (bind (i-1) ns tm))

222222 (P Bound x ty)

223223

224224renameBinders env (x, t) = (x, renameBindersTm env t)

@@ -233,12 +233,12 @@ renameBindersTm env tm = uniqueBinders (map fst env) tm

233233 (uniqueBinders (n':env) (rename n n' sc))

234234 | otherwise = Bind n (fmap (uniqueBinders (n:env)) b)

235235 (uniqueBinders (n:env) sc)

236− uniqueBinders env (App f a) = App (uniqueBinders env f) (uniqueBinders env a)

236+ uniqueBinders env (App s f a) = App s (uniqueBinders env f) (uniqueBinders env a)

237237 uniqueBinders env t = t

238238

239239 rename n n' (P nt x ty) | n == x = P nt n' ty

240240 rename n n' (Bind x b sc) = Bind x (fmap (rename n n') b) (rename n n' sc)

241− rename n n' (App f a) = App (rename n n' f) (rename n n' a)

241+ rename n n' (App s f a) = App s (rename n n' f) (rename n n' a)

242242 rename n n' t = t

243243

244244 explicitHole (Bind n (Hole ty) sc)

@@ -280,7 +280,7 @@ expandLets env (x, tm) = (x, doSubst (reverse env) tm)

280280

281281hasv :: TT Name -> Bool

282282hasv (V x) = True

283−hasv (App f a) = hasv f || hasv a

283+hasv (App _ f a) = hasv f || hasv a

284284hasv (Bind x b sc) = hasv (binderTy b) || hasv sc

285285hasv _ = False

286286

@@ -315,14 +315,12 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

315315

316316 injective (P (DCon _ _ _) _ _) = True

317317 injective (P (TCon _ _) _ _) = True

318−-- injective (App f (P _ _ _)) = injective f

319−-- injective (App f (Constant _)) = injective f

320− injective (App f a) = injective f -- && injective a

318+ injective (App _ f a) = injective f -- && injective a

321319 injective _ = False

322320

323321-- injectiveVar (P _ (MN _ _) _) = True -- TMP HACK

324322 injectiveVar (P _ n _) = n `elem` inj

325− injectiveVar (App f a) = injectiveVar f -- && injective a

323+ injectiveVar (App _ f a) = injectiveVar f -- && injective a

326324 injectiveVar _ = False

327325

328326 injectiveApp x = injective x || injectiveVar x

@@ -426,18 +424,18 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

426424 un' fn names topx@(Bind n (Hole t) sc) y = unifyTmpFail topx y

427425 un' fn names x topy@(Bind n (Hole t) sc) = unifyTmpFail x topy

428426

429− un' fn bnames appx@(App _ _) appy@(App _ _)

427+ un' fn bnames appx@(App _ _ _) appy@(App _ _ _)

430428 = unApp fn bnames appx appy

431429-- = uplus (unApp fn bnames appx appy)

432430-- (unifyTmpFail appx appy) -- take the whole lot

433431

434− un' fn bnames x (Bind n (Lam t) (App y (P Bound n' _)))

432+ un' fn bnames x (Bind n (Lam t) (App _ y (P Bound n' _)))

435433 | n == n' = un' False bnames x y

436− un' fn bnames (Bind n (Lam t) (App x (P Bound n' _))) y

434+ un' fn bnames (Bind n (Lam t) (App _ x (P Bound n' _))) y

437435 | n == n' = un' False bnames x y

438− un' fn bnames x (Bind n (Lam t) (App y (V 0)))

436+ un' fn bnames x (Bind n (Lam t) (App _ y (V 0)))

439437 = un' False bnames x y

440− un' fn bnames (Bind n (Lam t) (App x (V 0))) y

438+ un' fn bnames (Bind n (Lam t) (App _ x (V 0))) y

441439 = un' False bnames x y

442440-- un' fn bnames (Bind x (PVar _) sx) (Bind y (PVar _) sy)

443441-- = un' False ((x,y):bnames) sx sy

@@ -447,14 +445,14 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

447445 -- f D unifies with t -> D. This is dubious, but it helps with type

448446 -- class resolution for type classes over functions.

449447

450− un' fn bnames (App f x) (Bind n (Pi i t k) y)

448+ un' fn bnames (App _ f x) (Bind n (Pi i t k) y)

451449 | noOccurrence n y && injectiveApp f

452450 = do ux <- un' False bnames x y

453451 uf <- un' False bnames f (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))

454452 (Bind n (Pi i t k) (V 1)))

455453 combine bnames ux uf

456454

457− un' fn bnames (Bind n (Pi i t k) y) (App f x)

455+ un' fn bnames (Bind n (Pi i t k) y) (App _ f x)

458456 | noOccurrence n y && injectiveApp f

459457 = do ux <- un' False bnames y x

460458 uf <- un' False bnames (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))

@@ -481,7 +479,7 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

481479 else do put (UI s ((x, y, True, env, err, from, Unify) : f))

482480 return [] -- lift $ tfail err

483481

484− unApp fn bnames appx@(App fx ax) appy@(App fy ay)

482+ unApp fn bnames appx@(App _ fx ax) appy@(App _ fy ay)

485483 -- shortcut for the common case where we just want to check the

486484 -- arguments are correct

487485 | (injectiveApp fx && fx == fy)

@@ -545,7 +543,7 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

545543 rigid (P (TCon _ _) _ _) = True

546544 rigid t@(P Ref _ _) = inenv t || globmetavar t

547545 rigid (Constant _) = True

548− rigid (App f a) = rigid f && rigid a

546+ rigid (App _ f a) = rigid f && rigid a

549547 rigid t = not (metavar t) || globmetavar t

550548

551549 globmetavar t = case unApply t of

@@ -636,7 +634,7 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

636634 bind i ns tm

637635 | i < 0 = tm

638636 | otherwise = let ((x,y),ty) = ns!!i in

639− App (Bind y (Lam ty) (bind (i-1) ns tm))

637+ App MaybeHoles (Bind y (Lam ty) (bind (i-1) ns tm))

640638 (P Bound x ty)

641639

642640 combineArgs bnames args = ca [] args where

@@ -658,16 +656,16 @@ boundVs :: Int -> Term -> [Int]

658656boundVs i (V j) | j < i = []

659657 | otherwise = [j]

660658boundVs i (Bind n b sc) = boundVs (i + 1) sc

661−boundVs i (App f x) = let fs = boundVs i f

662− xs = boundVs i x in

663− nub (fs ++ xs)

659+boundVs i (App _ f x) = let fs = boundVs i f

660+ xs = boundVs i x in

661+ nub (fs ++ xs)

664662boundVs i _ = []

665663

666664highV :: Int -> Term -> Int

667665highV i (V j) | j > i = j

668666 | otherwise = i

669667highV i (Bind n b sc) = maximum [i, highV i (binderTy b), (highV i sc - 1)]

670−highV i (App f x) = max (highV i f) (highV i x)

668+highV i (App _ f x) = max (highV i f) (highV i x)

671669highV i _ = i

672670

673671envPos x i [] = 0

@@ -683,9 +681,9 @@ envPos x i ((y, _) : ys) | x == y = i

683681--

684682-- Issue #1722 on the issue tracker https://github.com/idris-lang/Idris-dev/issues/1722

685683--

686−recoverable t@(App _ _) _

684+recoverable t@(App _ _ _) _

687685 | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy'" = False

688−recoverable _ t@(App _ _)

686+recoverable _ t@(App _ _ _)

689687 | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy'" = False

690688recoverable (P (DCon _ _ _) x _) (P (DCon _ _ _) y _) = x == y

691689recoverable (P (TCon _ _) x _) (P (TCon _ _) y _) = x == y

@@ -696,13 +694,13 @@ recoverable (Constant _) (P (TCon _ _) y _) = False

696694recoverable (P (TCon _ _) x _) (Constant _) = False

697695recoverable (P (DCon _ _ _) x _) (P (TCon _ _) y _) = False

698696recoverable (P (TCon _ _) x _) (P (DCon _ _ _) y _) = False

699−recoverable p@(Constant _) (App f a) = recoverable p f

700−recoverable (App f a) p@(Constant _) = recoverable f p

701−recoverable p@(P _ n _) (App f a) = recoverable p f

702−recoverable (App f a) p@(P _ _ _) = recoverable f p

703−recoverable (App f a) (App f' a')

697+recoverable p@(Constant _) (App _ f a) = recoverable p f

698+recoverable (App _ f a) p@(Constant _) = recoverable f p

699+recoverable p@(P _ n _) (App _ f a) = recoverable p f

700+recoverable (App _ f a) p@(P _ _ _) = recoverable f p

701+recoverable (App _ f a) (App _ f' a')

704702 | f == f' = recoverable a a'

705−recoverable (App f a) (App f' a')

703+recoverable (App _ f a) (App _ f' a')

706704 = recoverable f f' -- && recoverable a a'

707705recoverable f (Bind _ (Pi _ _ _) sc)

708706 | (P (DCon _ _ _) _ _, _) <- unApply f = False

src/Idris/Coverage.hs+10−10

@@ -317,7 +317,7 @@ calcProd i fc topn pats

317317 prodRec n done (_, _, tm) = prod n done False (delazy' True tm)

318318

319319 prod :: Name -> [Name] -> Bool -> Term -> Idris Bool

320− prod n done ok ap@(App _ _)

320+ prod n done ok ap@(App _ _ _)

321321 | (P nt f _, args) <- unApply ap

322322 = do recOK <- checkProdRec (n:done) f

323323 let ctxt = tt_ctxt i

@@ -329,8 +329,8 @@ calcProd i fc topn pats

329329 return (and (ok : argsprod) )

330330 else do argsprod <- mapM (prod n done co) args

331331 return (and argsprod)

332− prod n done ok (App f a) = liftM2 (&&) (prod n done False f)

333− (prod n done False a)

332+ prod n done ok (App _ f a) = liftM2 (&&) (prod n done False f)

333+ (prod n done False a)

334334 prod n done ok (Bind _ (Let t v) sc)

335335 = liftM2 (&&) (prod n done False v) (prod n done False v)

336336 prod n done ok (Bind _ b sc) = prod n done ok sc

@@ -368,7 +368,7 @@ calcTotality fc n pats

368368 = case lookupTotal fn (tt_ctxt i) of

369369 [Partial _] -> return (Partial (Other [fn]))

370370 _ -> Nothing

371− checkLHS i (App f a) = mplus (checkLHS i f) (checkLHS i a)

371+ checkLHS i (App _ f a) = mplus (checkLHS i f) (checkLHS i a)

372372 checkLHS _ _ = Nothing

373373

374374checkTotality :: [Name] -> FC -> Name -> Idris Totality

@@ -477,14 +477,14 @@ buildSCG (_, n) = do

477477 x -> error $ "buildSCG: " ++ show (n, x)

478478

479479delazy = delazy' False -- not lazy codata

480−delazy' all t@(App f a)

480+delazy' all t@(App _ f a)

481481 | (P _ (UN l) _, [_, _, arg]) <- unApply t,

482482 l == txt "Force" = delazy' all arg

483483 | (P _ (UN l) _, [P _ (UN lty) _, _, arg]) <- unApply t,

484484 l == txt "Delay" && (all || lty == txt "LazyEval") = delazy arg

485485 | (P _ (UN l) _, [P _ (UN lty) _, arg]) <- unApply t,

486486 l == txt "Lazy'" && (all || lty == txt "LazyEval") = delazy' all arg

487−delazy' all (App f a) = App (delazy' all f) (delazy' all a)

487+delazy' all (App s f a) = App s (delazy' all f) (delazy' all a)

488488delazy' all (Bind n b sc) = Bind n (fmap (delazy' all) b) (delazy' all sc)

489489delazy' all t = t

490490

@@ -498,7 +498,7 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where

498498 (f, pargs) = unApply (dePat lhs') in

499499 findCalls Toplevel (dePat rhs') (patvars lhs') pargs

500500

501− findCalls guarded ap@(App f a) pvs pargs

501+ findCalls guarded ap@(App _ f a) pvs pargs

502502 -- under a call to "assert_total", don't do any checking, just believe

503503 -- that it is total.

504504 | (P _ (UN at) _, [_, _]) <- unApply ap,

@@ -519,7 +519,7 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where

519519 else Unguarded in

520520 mkChange n args pargs ++

521521 concatMap (\x -> findCalls nguarded x pvs pargs) args

522− findCalls guarded (App f a) pvs pargs

522+ findCalls guarded (App _ f a) pvs pargs

523523 = findCalls Unguarded f pvs pargs ++ findCalls Unguarded a pvs pargs

524524 findCalls guarded (Bind n (Let t v) e) pvs pargs

525525 = findCalls Unguarded t pvs pargs ++

@@ -561,13 +561,13 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where

561561 smaller (Just tyn) a (t, Just tyt)

562562 | a == t = isInductive (fst (unApply (getRetTy tyn)))

563563 (fst (unApply (getRetTy tyt)))

564− smaller ty a (ap@(App f s), _)

564+ smaller ty a (ap@(App _ f s), _)

565565 | (P (DCon _ _ _) n _, args) <- unApply ap

566566 = let tyn = getType n in

567567 any (smaller (ty `mplus` Just tyn) a)

568568 (zip args (map toJust (getArgTys tyn)))

569569 -- check higher order recursive arguments

570− smaller ty (App f s) a = smaller ty f a

570+ smaller ty (App _ f s) a = smaller ty f a

571571 smaller _ _ _ = False

572572

573573 toJust (n, t) = Just t

src/Idris/DataOpts.hs+6−6

@@ -63,21 +63,21 @@ instance Optimisable (TT Name) where

6363 applyOpts (P _ (NS (UN fn) mod) _)

6464 | fn == txt "mult" && mod == prel

6565 = return (P Ref (sUN "prim__mulBigInt") Erased)

66− applyOpts (App (P _ (NS (UN fn) mod) _) x)

66+ applyOpts (App _ (P _ (NS (UN fn) mod) _) x)

6767 | fn == txt "fromIntegerNat" && mod == prel

6868 = applyOpts x

6969 applyOpts (P _ (NS (UN fn) mod) _)

7070 | fn == txt "fromIntegerNat" && mod == prel

71− = return (App (P Ref (sNS (sUN "id") ["Basics","Prelude"]) Erased) Erased)

71+ = return (App Complete (P Ref (sNS (sUN "id") ["Basics","Prelude"]) Erased) Erased)

7272 applyOpts (P _ (NS (UN fn) mod) _)

7373 | fn == txt "toIntegerNat" && mod == prel

74− = return (App (P Ref (sNS (sUN "id") ["Basics","Prelude"]) Erased) Erased)

74+ = return (App Complete (P Ref (sNS (sUN "id") ["Basics","Prelude"]) Erased) Erased)

7575 applyOpts c@(P (DCon t arity uniq) n _)

7676 = return $ applyDataOptRT n t arity uniq []

77− applyOpts t@(App f a)

77+ applyOpts t@(App s f a)

7878 | (c@(P (DCon t arity uniq) n _), args) <- unApply t

7979 = applyDataOptRT n t arity uniq <$> mapM applyOpts args

80− | otherwise = App <$> applyOpts f <*> applyOpts a

80+ | otherwise = App s <$> applyOpts f <*> applyOpts a

8181 applyOpts (Bind n b t) = Bind n <$> applyOpts b <*> applyOpts t

8282 applyOpts (Proj t i) = Proj <$> applyOpts t <*> pure i

8383 applyOpts t = return t

@@ -103,6 +103,6 @@ applyDataOptRT n tag arity uniq args

103103 = Constant (BI 0)

104104 doOpts (NS (UN s) [nat, prelude]) [k]

105105 | s == txt "S" && nat == txt "Nat" && prelude == txt "Prelude"

106− = App (App (P Ref (sUN "prim__addBigInt") Erased) k) (Constant (BI 1))

106+ = App Complete (App Complete (P Ref (sUN "prim__addBigInt") Erased) k) (Constant (BI 1))

107107

108108 doOpts n args = mkApp (P (DCon tag arity uniq) n Erased) args

src/Idris/Delaborate.hs+6−6

@@ -49,7 +49,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

4949 where

5050 un = fileFC "(val)"

5151

52− de env _ (App f a) = deFn env f [a]

52+ de env _ (App _ f a) = deFn env f [a]

5353 de env _ (V i) | i < length env = PRef un (snd (env!!i))

5454 | otherwise = PRef un (sUN ("v" ++ show i ++ ""))

5555 de env _ (P _ n _) | n == unitTy = PTrue un IsType

@@ -103,7 +103,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

103103 _ -> ns

104104 dens n = n

105105

106− deFn env (App f a) args = deFn env f (a:args)

106+ deFn env (App _ f a) args = deFn env f (a:args)

107107 deFn env (P _ n _) [l,r]

108108 | n == pairTy = PPair un IsType (de env [] l) (de env [] r)

109109 | n == eqCon = PRefl un (de env [] r)

@@ -163,7 +163,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

163163 | otherwise = tm

164164 nonVar [] = error "Tried to delaborate empty case list"

165165 nonVar [x] = x

166− nonVar (x@(App _ _) : _) = x

166+ nonVar (x@(App _ _ _) : _) = x

167167 nonVar (x@(P (DCon _ _ _) _ _) : _) = x

168168 nonVar (x:xs) = nonVar xs

169169-- | How far to indent sub-errors

@@ -256,9 +256,9 @@ pprintErr' i (CantConvert x_in y_in env) =

256256 y)) <>

257257 if (opt_errContext (idris_options i)) then line <> showSc i env else empty

258258 where flagUnique (Bind n (Pi i t k@(UType u)) sc)

259− = App (P Ref (sUN (show u)) Erased)

259+ = App Complete (P Ref (sUN (show u)) Erased)

260260 (Bind n (Pi i (flagUnique t) k) (flagUnique sc))

261− flagUnique (App f a) = App (flagUnique f) (flagUnique a)

261+ flagUnique (App s f a) = App s (flagUnique f) (flagUnique a)

262262 flagUnique (Bind n b sc) = Bind n (fmap flagUnique b) (flagUnique sc)

263263 flagUnique t = t

264264pprintErr' i (CantSolveGoal x env) =

@@ -423,7 +423,7 @@ renameMNs x y = let ns = nub $ allTTNames x ++ allTTNames y

423423

424424 rename :: [(Name, Name)] -> Term -> Term

425425 rename ns (P nt x t) | Just x' <- lookup x ns = P nt x' t

426− rename ns (App f a) = App (rename ns f) (rename ns a)

426+ rename ns (App s f a) = App s (rename ns f) (rename ns a)

427427 rename ns (Bind x b sc)

428428 = let b' = fmap (rename ns) b

429429 sc' = rename ns sc in

src/Idris/Elab/Clause.hs+7−7

@@ -433,7 +433,7 @@ elabPE info fc caller r =

433433 showArg _ = ""

434434

435435 qshow (Bind _ _ _) = "fn"

436− qshow (App f a) = qshow f ++ qshow a

436+ qshow (App _ f a) = qshow f ++ qshow a

437437 qshow (P _ n _) = show n

438438 qshow (Constant c) = show c

439439 qshow _ = ""

@@ -494,9 +494,9 @@ checkPossible info fc tcgen fname lhs_in

494494 -- have no metavars -- just looking to see if a constructor is failing

495495 -- to unify with a function that may be reduced later

496496

497− checkRec (App f a) p@(P _ _ _) = checkRec f p

498− checkRec p@(P _ _ _) (App f a) = checkRec p f

499− checkRec fa@(App _ _) fa'@(App _ _)

497+ checkRec (App _ f a) p@(P _ _ _) = checkRec f p

498+ checkRec p@(P _ _ _) (App _ f a) = checkRec p f

499+ checkRec fa@(App _ _ _) fa'@(App _ _ _)

500500 | (f, as) <- unApply fa,

501501 (f', as') <- unApply fa'

502502 = if (length as /= length as')

@@ -745,14 +745,14 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

745745 -- Find the variable names which appear under a 'Ownership.Read' so that

746746 -- we know they can't be used on the RHS

747747 borrowedNames :: [Name] -> Term -> [Name]

748− borrowedNames env (App (App (P _ (NS (UN lend) [owner]) _) _) arg)

748+ borrowedNames env (App _ (App _ (P _ (NS (UN lend) [owner]) _) _) arg)

749749 | owner == txt "Ownership" &&

750750 (lend == txt "lend" || lend == txt "Read") = getVs arg

751751 where

752752 getVs (V i) = [env!!i]

753− getVs (App f a) = nub $ getVs f ++ getVs a

753+ getVs (App _ f a) = nub $ getVs f ++ getVs a

754754 getVs _ = []

755− borrowedNames env (App f a) = nub $ borrowedNames env f ++ borrowedNames env a

755+ borrowedNames env (App _ f a) = nub $ borrowedNames env f ++ borrowedNames env a

756756 borrowedNames env (Bind n b sc) = nub $ borrowedB b ++ borrowedNames (n:env) sc

757757 where borrowedB (Let t v) = nub $ borrowedNames env t ++ borrowedNames env v

758758 borrowedB b = borrowedNames env (binderTy b)

src/Idris/Elab/Data.hs+1−1

@@ -174,7 +174,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

174174 update ((n, _) : as) (_ : args) = (n, Nothing) : update as args

175175

176176 getDataApp :: Type -> [[Maybe Name]]

177− getDataApp f@(App _ _)

177+ getDataApp f@(App _ _ _)

178178 | (P _ d _, args) <- unApply f

179179 = if (d == n) then [mParam args args] else []

180180 getDataApp (Bind n (Pi _ t _) sc)

src/Idris/Elab/Instance.hs+1−1

@@ -317,7 +317,7 @@ checkInjectiveArgs fc n ds (Just ty)

317317

318318 isInj i (P Bound n _) = True

319319 isInj i (P _ n _) = isConName n (tt_ctxt i)

320− isInj i (App f a) = isInj i f && isInj i a

320+ isInj i (App _ f a) = isInj i f && isInj i a

321321 isInj i (V _) = True

322322 isInj i (Bind n b sc) = isInj i sc

323323 isInj _ _ = True

src/Idris/Elab/Provider.hs+2−2

@@ -111,8 +111,8 @@ elabProvider doc info syn fc what n

111111 -- (MkFFI C_FFI) (Providers.Provider ty) in hopes of better

112112 -- error messages with less normalisation

113113 providerOf :: Type -> Type

114− providerOf ty = App (P Ref (sUN "IO") Erased) $

115− App (P Ref (sNS (sUN "Provider") ["Providers", "Prelude"]) Erased)

114+ providerOf ty = App Complete (P Ref (sUN "IO") Erased) $

115+ App Complete (P Ref (sNS (sUN "Provider") ["Providers", "Prelude"]) Erased)

116116 ty

117117

118118 isProviderOf :: Context -> TT Name -> TT Name -> Bool

src/Idris/Elab/Type.hs+2−2

@@ -215,8 +215,8 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

215215 errrep = txt "ErrorReportPart"

216216

217217 tyIsHandler (Bind _ (Pi _ (P _ (NS (UN e) ns1) _) _)

218− (App (P _ (NS (UN m) ns2) _)

219− (App (P _ (NS (UN l) ns3) _)

218+ (App _ (P _ (NS (UN m) ns2) _)

219+ (App _ (P _ (NS (UN l) ns3) _)

220220 (P _ (NS (UN r) ns4) _))))

221221 | e == err && m == maybe && l == lst && r == errrep

222222 , ns1 == map txt ["Errors","Reflection","Language"]

src/Idris/Elab/Utils.hs+3−3

@@ -171,7 +171,7 @@ getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi _ t _) sc)

171171 _ -> []

172172getFixedInType i env (_ : is) (Bind n (Pi _ t _) sc)

173173 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)

174−getFixedInType i env is tm@(App f a)

174+getFixedInType i env is tm@(App _ f a)

175175 | (P _ tn _, args) <- unApply tm

176176 = case lookupCtxt tn (idris_datatypes i) of

177177 [t] -> nub $ paramNames args env (param_pos t) ++

@@ -186,7 +186,7 @@ getFixedInType i _ _ _ = []

186186getFlexInType i env ps (Bind n (Pi _ t _) sc)

187187 = nub $ (if (not (n `elem` ps)) then getFlexInType i env ps t else []) ++

188188 getFlexInType i (n : env) ps (instantiate (P Bound n t) sc)

189−getFlexInType i env ps tm@(App f a)

189+getFlexInType i env ps tm@(App _ f a)

190190 | (P _ tn _, args) <- unApply tm

191191 = case lookupCtxt tn (idris_datatypes i) of

192192 [t] -> nub $ paramNames args env [x | x <- [0..length args],

@@ -232,7 +232,7 @@ getUniqueUsed ctxt tm = execState (getUniq [] [] tm) []

232232 _ -> False in

233233 do getUniqB env us b

234234 getUniq ((n,b):env) ((n, uniq):us) sc

235− getUniq env us (App f a) = do getUniq env us f; getUniq env us a

235+ getUniq env us (App _ f a) = do getUniq env us f; getUniq env us a

236236 getUniq env us (V i)

237237 | i < length us = if snd (us!!i) then use (fst (us!!i)) else return ()

238238 getUniq env us (P _ n _)

src/Idris/ElabTerm.hs+24−24

@@ -430,7 +430,7 @@ elab ist info emode opts fn tm

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

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

432432 pexp l, pexp r])

433− elab' ina fc (PAlternative True as)

433+ elab' ina fc (PAlternative True as)

434434 = do hnf_compute

435435 ty <- goal

436436 ctxt <- get_context

@@ -967,7 +967,7 @@ elab ist info emode opts fn tm

967967 _ -> n

968968

969969 inApp (P _ n _) = [n]

970− inApp (App f a) = inApp f ++ inApp a

970+ inApp (App _ f a) = inApp f ++ inApp a

971971 inApp (Bind n (Let _ v) sc) = inApp v ++ inApp sc

972972 inApp (Bind n (Guess _ v) sc) = inApp v ++ inApp sc

973973 inApp (Bind n b sc) = inApp sc

@@ -1561,7 +1561,7 @@ collectDeferred top (Bind n b t) = do b' <- cdb b

15611561 cdb (Guess t v) = liftM2 Guess (collectDeferred top t) (collectDeferred top v)

15621562 cdb b = do ty' <- collectDeferred top (binderTy b)

15631563 return (b { binderTy = ty' })

1564−collectDeferred top (App f a) = liftM2 App (collectDeferred top f) (collectDeferred top a)

1564+collectDeferred top (App s f a) = liftM2 (App s) (collectDeferred top f) (collectDeferred top a)

15651565collectDeferred top t = return t

15661566

15671567case_ :: Bool -> Bool -> IState -> Name -> PTerm -> ElabD ()

@@ -1638,7 +1638,7 @@ runTactical fc env tm = do tm' <- eval tm

16381638 | n == tacN "prim__BindTactical", [_a, _b, first, andThen] <- args

16391639 = do first' <- eval first

16401640 res <- runTacTm first'

1641− next <- eval (App andThen res)

1641+ next <- eval (App Complete andThen res)

16421642 runTacTm next

16431643 | n == tacN "prim__Try", [_a, first, alt] <- args

16441644 = do first' <- eval first

@@ -1983,7 +1983,7 @@ reify _ (P _ n _) | n == reflm "Compute" = return Compute

19831983reify _ (P _ n _) | n == reflm "Skip" = return Skip

19841984reify _ (P _ n _) | n == reflm "SourceFC" = return SourceFC

19851985reify _ (P _ n _) | n == reflm "Unfocus" = return Unfocus

1986−reify ist t@(App _ _)

1986+reify ist t@(App _ _ _)

19871987 | (P _ f _, args) <- unApply t = reifyApp ist f args

19881988reify _ t = fail ("Unknown tactic " ++ show t)

19891989

@@ -2043,7 +2043,7 @@ reifyReportParts errs =

20432043

20442044-- | Reify terms from their reflected representation

20452045reifyTT :: Term -> ElabD Term

2046−reifyTT t@(App _ _)

2046+reifyTT t@(App _ _ _)

20472047 | (P _ f _, args) <- unApply t = reifyTTApp f args

20482048reifyTT t@(P _ n _)

20492049 | n == reflm "Erased" = return $ Erased

@@ -2067,7 +2067,7 @@ reifyTTApp t [n, b, x]

20672067reifyTTApp t [f, x]

20682068 | t == reflm "App" = do f' <- reifyTT f

20692069 x' <- reifyTT x

2070− return $ App f' x'

2070+ return $ App Complete f' x'

20712071reifyTTApp t [c]

20722072 | t == reflm "TConst" = liftM Constant (reifyTTConst c)

20732073reifyTTApp t [t', Constant (I i)]

@@ -2079,7 +2079,7 @@ reifyTTApp t args = fail ("Unknown reflection term: " ++ show (t, args))

20792079

20802080-- | Reify raw terms from their reflected representation

20812081reifyRaw :: Term -> ElabD Raw

2082−reifyRaw t@(App _ _)

2082+reifyRaw t@(App _ _ _)

20832083 | (P _ f _, args) <- unApply t = reifyRawApp f args

20842084reifyRaw t@(P _ n _)

20852085 | n == reflm "RType" = return $ RType

@@ -2120,7 +2120,7 @@ reifyTTNameApp t []

21202120reifyTTNameApp t args = fail ("Unknown reflection term name: " ++ show (t, args))

21212121

21222122reifyTTNamespace :: Term -> ElabD [String]

2123−reifyTTNamespace t@(App _ _)

2123+reifyTTNamespace t@(App _ _ _)

21242124 = case unApply t of

21252125 (P _ f _, [Constant StrType])

21262126 | f == sNS (sUN "Nil") ["List", "Prelude"] -> return []

@@ -2132,7 +2132,7 @@ reifyTTNamespace t = fail ("Unknown reflection namespace arg: " ++ show t)

21322132reifyTTNameType :: Term -> ElabD NameType

21332133reifyTTNameType t@(P _ n _) | n == reflm "Bound" = return $ Bound

21342134reifyTTNameType t@(P _ n _) | n == reflm "Ref" = return $ Ref

2135−reifyTTNameType t@(App _ _)

2135+reifyTTNameType t@(App _ _ _)

21362136 = case unApply t of

21372137 (P _ f _, [Constant (I tag), Constant (I num)])

21382138 | f == reflm "DCon" -> return $ DCon tag num False -- FIXME: Uniqueness!

@@ -2141,7 +2141,7 @@ reifyTTNameType t@(App _ _)

21412141reifyTTNameType t = fail ("Unknown reflection name type: " ++ show t)

21422142

21432143reifyTTBinder :: (Term -> ElabD a) -> Name -> Term -> ElabD (Binder a)

2144−reifyTTBinder reificator binderType t@(App _ _)

2144+reifyTTBinder reificator binderType t@(App _ _ _)

21452145 = case unApply t of

21462146 (P _ f _, bt:args) | forget bt == Var binderType

21472147 -> reifyTTBinderApp reificator f args

@@ -2173,7 +2173,7 @@ reifyTTConst :: Term -> ElabD Const

21732173reifyTTConst (P _ n _) | n == reflm "StrType" = return $ StrType

21742174reifyTTConst (P _ n _) | n == reflm "VoidType" = return $ VoidType

21752175reifyTTConst (P _ n _) | n == reflm "Forgot" = return $ Forgot

2176−reifyTTConst t@(App _ _)

2176+reifyTTConst t@(App _ _ _)

21772177 | (P _ f _, [arg]) <- unApply t = reifyTTConstApp f arg

21782178reifyTTConst t = fail ("Unknown reflection constant: " ++ show t)

21792179

@@ -2201,7 +2201,7 @@ reifyTTConstApp f (Constant c@(B64 _))

22012201reifyTTConstApp f arg = fail ("Unknown reflection constant: " ++ show (f, arg))

22022202

22032203reifyArithTy :: Term -> ElabD ArithTy

2204−reifyArithTy (App (P _ n _) intTy) | n == reflm "ATInt" = fmap ATInt (reifyIntTy intTy)

2204+reifyArithTy (App _ (P _ n _) intTy) | n == reflm "ATInt" = fmap ATInt (reifyIntTy intTy)

22052205reifyArithTy (P _ n _) | n == reflm "ATFloat" = return ATFloat

22062206reifyArithTy x = fail ("Couldn't reify reflected ArithTy: " ++ show x)

22072207

@@ -2213,14 +2213,14 @@ reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8

22132213reifyNativeTy x = fail $ "Couldn't reify reflected NativeTy " ++ show x

22142214

22152215reifyIntTy :: Term -> ElabD IntTy

2216−reifyIntTy (App (P _ n _) nt) | n == reflm "ITFixed" = fmap ITFixed (reifyNativeTy nt)

2216+reifyIntTy (App _ (P _ n _) nt) | n == reflm "ITFixed" = fmap ITFixed (reifyNativeTy nt)

22172217reifyIntTy (P _ n _) | n == reflm "ITNative" = return ITNative

22182218reifyIntTy (P _ n _) | n == reflm "ITBig" = return ITBig

22192219reifyIntTy (P _ n _) | n == reflm "ITChar" = return ITChar

22202220reifyIntTy tm = fail $ "The term " ++ show tm ++ " is not a reflected IntTy"

22212221

22222222reifyTTUExp :: Term -> ElabD UExp

2223−reifyTTUExp t@(App _ _)

2223+reifyTTUExp t@(App _ _ _)

22242224 = case unApply t of

22252225 (P _ f _, [Constant (I i)]) | f == reflm "UVar" -> return $ UVar i

22262226 (P _ f _, [Constant (I i)]) | f == reflm "UVal" -> return $ UVal i

@@ -2289,7 +2289,7 @@ reflectTTQuotePattern unq (Bind n b x)

22892289 solve

22902290 focus x'; reflectTTQuotePattern unq x

22912291 focus b'; reflectBinderQuotePattern reflectTTQuotePattern unq b

2292−reflectTTQuotePattern unq (App f x)

2292+reflectTTQuotePattern unq (App _ f x)

22932293 = do f' <- claimTT (sMN 0 "f"); movelast f'

22942294 x' <- claimTT (sMN 0 "x"); movelast x'

22952295 fill $ reflCall "App" [Var f', Var x']

@@ -2472,7 +2472,7 @@ reflectTTQuote unq (V n)

24722472 = reflCall "V" [RConstant (I n)]

24732473reflectTTQuote unq (Bind n b x)

24742474 = reflCall "Bind" [reflectName n, reflectBinderQuote reflectTTQuote (reflm "TT") unq b, reflectTTQuote unq x]

2475−reflectTTQuote unq (App f x)

2475+reflectTTQuote unq (App _ f x)

24762476 = reflCall "App" [reflectTTQuote unq f, reflectTTQuote unq x]

24772477reflectTTQuote unq (Constant c)

24782478 = reflCall "TConst" [reflectConstant c]

@@ -2814,7 +2814,7 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

28142814 parts -> ReflectionError errorparts e

28152815

28162816fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a

2817−fromTTMaybe (App (App (P (DCon _ _ _) (NS (UN just) _) _) ty) tm)

2817+fromTTMaybe (App _ (App _ (P (DCon _ _ _) (NS (UN just) _) _) ty) tm)

28182818 | just == txt "Just" = Just tm

28192819fromTTMaybe x = Nothing

28202820

@@ -2825,9 +2825,9 @@ reflErrName n = sNS (sUN n) ["Errors", "Reflection", "Language"]

28252825-- representation. Not in Idris or ElabD monads because it should be usable

28262826-- from either.

28272827reifyReportPart :: Term -> Either Err ErrorReportPart

2828−reifyReportPart (App (P (DCon _ _ _) n _) (Constant (Str msg))) | n == reflm "TextPart" =

2828+reifyReportPart (App _ (P (DCon _ _ _) n _) (Constant (Str msg))) | n == reflm "TextPart" =

28292829 Right (TextPart msg)

2830−reifyReportPart (App (P (DCon _ _ _) n _) ttn)

2830+reifyReportPart (App _ (P (DCon _ _ _) n _) ttn)

28312831 | n == reflm "NamePart" =

28322832 case runElab initEState (reifyTTName ttn) (initElaborator NErased initContext Erased) of

28332833 Error e -> Left . InternalMsg $

@@ -2835,7 +2835,7 @@ reifyReportPart (App (P (DCon _ _ _) n _) ttn)

28352835 show ttn ++

28362836 " when reflecting an error:" ++ show e

28372837 OK (n', _)-> Right $ NamePart n'

2838−reifyReportPart (App (P (DCon _ _ _) n _) tm)

2838+reifyReportPart (App _ (P (DCon _ _ _) n _) tm)

28392839 | n == reflm "TermPart" =

28402840 case runElab initEState (reifyTT tm) (initElaborator NErased initContext Erased) of

28412841 Error e -> Left . InternalMsg $

@@ -2843,7 +2843,7 @@ reifyReportPart (App (P (DCon _ _ _) n _) tm)

28432843 show tm ++

28442844 " when reflecting an error:" ++ show e

28452845 OK (tm', _) -> Right $ TermPart tm'

2846−reifyReportPart (App (P (DCon _ _ _) n _) tm)

2846+reifyReportPart (App _ (P (DCon _ _ _) n _) tm)

28472847 | n == reflm "SubReport" =

28482848 case unList tm of

28492849 Just xs -> do subParts <- mapM reifyReportPart xs

@@ -2852,7 +2852,7 @@ reifyReportPart (App (P (DCon _ _ _) n _) tm)

28522852reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x

28532853

28542854reifyTyDecl :: Term -> ElabD RTyDecl

2855−reifyTyDecl (App (App (App (P (DCon _ _ _) n _) tyN) args) ret)

2855+reifyTyDecl (App _ (App _ (App _ (P (DCon _ _ _) n _) tyN) args) ret)

28562856 | n == tacN "Declare" =

28572857 do tyN' <- reifyTTName tyN

28582858 args' <- case unList args of

@@ -2861,7 +2861,7 @@ reifyTyDecl (App (App (App (P (DCon _ _ _) n _) tyN) args) ret)

28612861 ret' <- reifyRaw ret

28622862 return $ RDeclare tyN' args' ret'

28632863 where reifyRArg :: Term -> ElabD RArg

2864− reifyRArg (App (App (P (DCon _ _ _) n _) argN) argTy)

2864+ reifyRArg (App _ (App _ (P (DCon _ _ _) n _) argN) argTy)

28652865 | n == tacN "Explicit" = liftM2 RExplicit

28662866 (reifyTTName argN)

28672867 (reifyRaw argTy)

src/Idris/Erasure.hs+6−6

@@ -279,7 +279,7 @@ buildDepMap ci used externs ctx startNames

279279

280280 etaExpand :: [Name] -> Term -> Term

281281 etaExpand [] t = t

282− etaExpand (n : ns) t = etaExpand ns (App t (P Ref n Erased))

282+ etaExpand (n : ns) t = etaExpand ns (App Complete t (P Ref n Erased))

283283

284284 getDepsSC :: Name -> [Name] -> Vars -> SC -> Deps

285285 getDepsSC fn es vs ImpossibleCase = M.empty

@@ -370,7 +370,7 @@ buildDepMap ci used externs ctx startNames

370370 var t cd = getDepsTerm vs bs cd t

371371

372372 -- applications may add items to Cond

373− getDepsTerm vs bs cd app@(App _ _)

373+ getDepsTerm vs bs cd app@(App _ _ _)

374374 | (fun, args) <- unApply app = case fun of

375375 -- instance constructors -> create metamethod deps

376376 P (DCon _ _ _) ctorName@(SN (InstanceCtorN className)) _

@@ -418,8 +418,8 @@ buildDepMap ci used externs ctx startNames

418418 Bind n (Lam ty) t -> getDepsTerm vs bs cd (lamToLet [] app)

419419

420420 -- and we interpret applied lets as lambdas

421− Bind n ( Let ty t') t -> getDepsTerm vs bs cd (App (Bind n (Lam ty) t) t')

422− Bind n (NLet ty t') t -> getDepsTerm vs bs cd (App (Bind n (Lam ty) t) t')

421+ Bind n ( Let ty t') t -> getDepsTerm vs bs cd (App Complete (Bind n (Lam ty) t) t')

422+ Bind n (NLet ty t') t -> getDepsTerm vs bs cd (App Complete (Bind n (Lam ty) t) t')

423423

424424 Proj t i

425425 -> error $ "cannot[0] analyse projection !" ++ show i ++ " of " ++ show t

@@ -493,9 +493,9 @@ buildDepMap ci used externs ctx startNames

493493 -- convert applications of lambdas to lets

494494 -- Note that this transformation preserves de bruijn numbering

495495 lamToLet :: [Term] -> Term -> Term

496− lamToLet xs (App f x) = lamToLet (x:xs) f

496+ lamToLet xs (App _ f x) = lamToLet (x:xs) f

497497 lamToLet (x:xs) (Bind n (Lam ty) t) = Bind n (Let ty x) (lamToLet xs t)

498− lamToLet (x:xs) t = App (lamToLet xs t) x

498+ lamToLet (x:xs) t = App Complete (lamToLet xs t) x

499499 lamToLet [] t = t

500500

501501 -- split "\x_i -> T(x_i)" into [x_i] and T

src/Idris/ErrReverse.hs+7−7

@@ -35,9 +35,9 @@ errReverse ist t = rewrite 5 t -- (elideLambdas t)

3535

3636 matchTerm ns l r t

3737 | Just nmap <- match ns l t = substNames nmap r

38− matchTerm ns l r (App f a) = let f' = matchTerm ns l r f

39− a' = matchTerm ns l r a in

40− App f' a'

38+ matchTerm ns l r (App s f a) = let f' = matchTerm ns l r f

39+ a' = matchTerm ns l r a in

40+ App s f' a'

4141 matchTerm ns l r (Bind n b sc) = let b' = fmap (matchTerm ns l r) b

4242 sc' = matchTerm ns l r sc in

4343 Bind n b' sc'

@@ -54,16 +54,16 @@ errReverse ist t = rewrite 5 t -- (elideLambdas t)

5454 Just ((x, t) : xs')

5555

5656 match' ns (P Ref n _) t | n `elem` ns = Just [(n, t)]

57− match' ns (App f a) (App f' a') = do fs <- match' ns f f'

58− as <- match' ns a a'

59− Just (fs ++ as)

57+ match' ns (App _ f a) (App _ f' a') = do fs <- match' ns f f'

58+ as <- match' ns a a'

59+ Just (fs ++ as)

6060 -- no matching Binds, for now...

6161 match' ns x y = if x == y then Just [] else Nothing

6262

6363 -- if the term under a lambda is huge, there's no much point in showing

6464 -- it as it won't be very enlightening.

6565

66− elideLambdas (App f a) = App (elideLambdas f) (elideLambdas a)

66+ elideLambdas (App s f a) = App s (elideLambdas f) (elideLambdas a)

6767 elideLambdas (Bind n (Lam t) sc)

6868 | size sc > 200 = P Ref (sUN "...") Erased

6969 elideLambdas (Bind n b sc)

src/Idris/IBC.hs+1−1

@@ -501,7 +501,7 @@ pDefs reexp syms ds

501501

502502 update (P t n ty) = do n' <- getSymbol n

503503 return $ P t n' ty

504− update (App f a) = liftM2 App (update f) (update a)

504+ update (App s f a) = liftM2 (App s) (update f) (update a)

505505 update (Bind n b sc) = do b' <- updateB b

506506 sc' <- update sc

507507 return $ Bind n b' sc'

src/Idris/Inliner.hs+1−1

@@ -21,7 +21,7 @@ inlineDef ist ds = map (\ (ns, lhs, rhs) -> (ns, lhs, inlineTerm ist rhs)) ds

2121inlineTerm :: IState -> Term -> Term

2222inlineTerm ist tm = inl tm where

2323 inl orig@(P _ n _) = inlApp n [] orig

24− inl orig@(App f a)

24+ inl orig@(App _ f a)

2525 | (P _ fn _, args) <- unApply orig = inlApp fn args orig

2626 inl (Bind n (Let t v) sc) = Bind n (Let t (inl v)) (inl sc)

2727 inl (Bind n b sc) = Bind n b (inl sc)

src/Idris/Interactive.hs+1−1

@@ -322,7 +322,7 @@ makeLemma fn updatefile l n

322322 guessImps ctxt _ = []

323323

324324 guarded ctxt n (P _ n' _) | n == n' = True

325− guarded ctxt n ap@(App _ _)

325+ guarded ctxt n ap@(App _ _ _)

326326 | (P _ f _, args) <- unApply ap,

327327 isConName f ctxt = any (guarded ctxt n) args

328328-- guarded ctxt n (Bind (UN cn) (Pi t) sc) -- ignore shadows

src/Idris/PartialEval.hs+2−2

@@ -146,7 +146,7 @@ mkPE_TyDecl ist args ty = mkty args ty

146146 = do nm <- get

147147 put (nm + 1)

148148 return (P Bound (sMN nm "spec") Erased)

149− gen (App f a) = App <$> gen f <*> gen a

149+ gen (App s f a) = App s <$> gen f <*> gen a

150150 gen tm = return tm

151151

152152-- | Checks if a given argument is a type class constraint argument

@@ -291,7 +291,7 @@ getSpecApps ist env tm = ga env (explicitNames tm) where

291291

292292 -- if we have a *defined* function that has static arguments,

293293 -- it will become a specialised application

294− ga env tm@(App f a) | (P _ n _, args) <- unApply tm,

294+ ga env tm@(App _ f a) | (P _ n _, args) <- unApply tm,

295295 n `notElem` map fst (idris_metavars ist) =

296296 ga env f ++ ga env a ++

297297 case (lookupCtxtExact n (idris_statics ist),

src/Idris/ProofSearch.hs+1−1

@@ -128,7 +128,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

128128 toUN t@(P nt (MN i n) ty)

129129 | ('_':xs) <- str n = t

130130 | otherwise = P nt (UN n) ty

131− toUN (App f a) = App (toUN f) (toUN a)

131+ toUN (App s f a) = App s (toUN f) (toUN a)

132132 toUN t = t

133133

134134 -- psRec counts depth and the local variable applications we're under

src/Idris/Transforms.hs+8−8

@@ -39,21 +39,21 @@ applyTransRulesWith rules tm

3939 = finalise $ applyAll rules emptyContext (vToP tm)

4040

4141applyAll :: [(Term, Term)] -> Ctxt [(Term, Term)] -> Term -> Term

42−applyAll extra ts ap@(App f a)

42+applyAll extra ts ap@(App s f a)

4343 | (P _ fn ty, args) <- unApply ap

4444 = let rules = case lookupCtxtExact fn ts of

4545 Just r -> extra ++ r

4646 Nothing -> extra

47− ap' = App (applyAll extra ts f) (applyAll extra ts a) in

47+ ap' = App s (applyAll extra ts f) (applyAll extra ts a) in

4848 case rules of

4949 [] -> ap'

5050 rs -> case applyFnRules rs ap of

51− Just tm'@(App f' a') ->

52− App (applyAll extra ts f')

53− (applyAll extra ts a')

51+ Just tm'@(App s f' a') ->

52+ App s (applyAll extra ts f')

53+ (applyAll extra ts a')

5454 Just tm' -> tm'

55− _ -> App (applyAll extra ts f)

56− (applyAll extra ts a)

55+ _ -> App s (applyAll extra ts f)

56+ (applyAll extra ts a)

5757applyAll extra ts (Bind n b sc) = Bind n (fmap (applyAll extra ts) b)

5858 (applyAll extra ts sc)

5959applyAll extra ts t = t

@@ -94,7 +94,7 @@ matchTerm lhs tm = matchVars [] lhs tm

9494 doMatch :: [Name] -> Term -> Term -> Maybe [(Name, Term)]

9595 doMatch ns (P _ n _) tm

9696 | n `elem` ns = return [(n, tm)]

97− doMatch ns (App f a) (App f' a')

97+ doMatch ns (App _ f a) (App _ f' a')

9898 = do fm <- doMatch ns f f'

9999 am <- doMatch ns a a'

100100 return (fm ++ am)

src/Idris/TypeSearch.hs+7−6

@@ -104,9 +104,9 @@ typeFromDef (def, _, _, _) = get def where

104104-- Replace all occurences of `Lazy' s t` with `t` in a type

105105unLazy :: Type -> Type

106106unLazy typ = case typ of

107− App (App (P _ lazy _) _) ty | lazy == sUN "Lazy'" -> unLazy ty

107+ App _ (App _ (P _ lazy _) _) ty | lazy == sUN "Lazy'" -> unLazy ty

108108 Bind name binder ty -> Bind name (fmap unLazy binder) (unLazy ty)

109− App t1 t2 -> App (unLazy t1) (unLazy t2)

109+ App s t1 t2 -> App s (unLazy t1) (unLazy t2)

110110 Proj ty i -> Proj (unLazy ty) i

111111 _ -> typ

112112

@@ -146,7 +146,7 @@ usedVars = f True where

146146 Let t v -> f b t `M.union` f b v

147147 Guess t v -> f b t `M.union` f b v

148148 bind -> f b (binderTy bind)

149− f b (App t1 t2) = f b t1 `M.union` f (b && isInjective t1) t2

149+ f b (App _ t1 t2) = f b t1 `M.union` f (b && isInjective t1) t2

150150 f b (Proj t _) = f b t

151151 f _ (V _) = error "unexpected! run vToP first"

152152 f _ _ = M.empty

@@ -307,13 +307,14 @@ subsets (x : xs) = let ss = subsets xs in map (x :) ss ++ ss

307307-- recalls the number of flips that have been made

308308flipEqualities :: Type -> [(Int, Type)]

309309flipEqualities t = case t of

310− eq1@(App (App (App (App eq@(P _ eqty _) tyL) tyR) valL) valR) | eqty == eqTy ->

311− [(0, eq1), (1, App (App (App (App eq tyR) tyL) valR) valL)]

310+ eq1@(App _ (App _ (App _ (App _ eq@(P _ eqty _) tyL) tyR) valL) valR) | eqty == eqTy ->

311+ [(0, eq1), (1, app (app (app (app eq tyR) tyL) valR) valL)]

312312 Bind n binder sc -> (\bind' (j, sc') -> (fst (binderTy bind') + j, Bind n (fmap snd bind') sc'))

313313 <$> traverse flipEqualities binder <*> flipEqualities sc

314− App f x -> (\(i, f') (j, x') -> (i + j, App f' x'))

314+ App _ f x -> (\(i, f') (j, x') -> (i + j, app f' x'))

315315 <$> flipEqualities f <*> flipEqualities x

316316 t' -> [(0, t')]

317+ where app = App Complete

317318

318319--DONT run vToP first!

319320-- | Try to match two types together in a unification-like procedure.

src/Idris/WhoCalls.hs+2−2

@@ -13,7 +13,7 @@ occurs :: Name -> Term -> Bool

1313occurs n (P Bound _ _) = False

1414occurs n (P _ n' _) = n == n'

1515occurs n (Bind _ b sc) = occursBinder n b || occurs n sc

16−occurs n (App t1 t2) = occurs n t1 || occurs n t2

16+occurs n (App _ t1 t2) = occurs n t1 || occurs n t2

1717occurs n (Proj t _) = occurs n t

1818occurs n _ = False

1919

@@ -21,7 +21,7 @@ names :: Term -> [Name]

2121names (P Bound _ _) = []

2222names (P _ n _) = [n]

2323names (Bind _ b sc) = namesBinder b ++ names sc

24−names (App t1 t2) = names t1 ++ names t2

24+names (App _ t1 t2) = names t1 ++ names t2

2525names (Proj t _) = names t

2626names _ = []

2727