f987aec · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add info field to App

f987aecEdwin Brady12 years ago

src/IRTS/Compiler.hs+3−3

compare with master

unifiedsplit

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

235type Vars = M.Map Name VarInfo

236

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

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

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

239 ist <- getIState

240 case unApply tm of

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

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

297

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

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

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

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

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

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

302 | be == txt "boolElim"

303 , d == txt "Delay"

304 , d' == txt "Delay"

src/Idris/AbsSyntaxTree.hs+2−2

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

1253

1254getInferTerm, getInferType :: Term -> Term

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

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

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

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

1258

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

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

1261 toTy (PVar t) = PVTy t

1262 toTy b = b

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

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

1264

1265

1266

src/Idris/Apropos.hs+1−1

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

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

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

79 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

81 isApropos str (Constant const) = isApropos str const

82 isApropos str _ = False

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

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

555 put x1

556 put x2

557 put x3

558− App x1 x2 -> do putWord8 3

558+ App _ x1 x2 -> do putWord8 3

559− put x1

559+ put x1

560− put x2

560+ put x2

561 Constant x1 -> do putWord8 4

562 put x1

563 Proj x1 x2 -> do putWord8 5

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

584 return (Bind x1 x2 x3)

585 3 -> do x1 <- get

586 x2 <- get

587− return (App x1 x2)

587+ return (App Complete x1 x2)

588 4 -> do x1 <- get

589 return (Constant x1)

590 5 -> do x1 <- get

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

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

130

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

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

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

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

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

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

155

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

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

158− nut ps fn@(App f a)

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

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

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

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

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

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

177 ++ directUse t

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

179−directUse fn@(App f a)

179+directUse fn@(App _ f a)

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

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

181 pfk == txt "prim_fork"

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

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

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

337

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

339toPats 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

341 getArgs _ = []

342

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

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

362 = PSuc $ toPat' [] p

363

364 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

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

367 | otherwise = PConst x

368

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

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

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

641

642− applyMaps ms f@(App _ _)

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

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

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

645 applyMap ms nt cn pty args'

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

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

653 same _ _ = False

654

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)

656 applyMaps ms t = t

657

658-- FIXME: Do this for SucCase too

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

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

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

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

162 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` ()

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

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

166 rnf Erased = ()

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

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

258 else lift $ tfail (NotInjective tm l r)

259 where isInj ctxt (P _ n _)

260 | isConName n ctxt = True

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

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

262 isInj ctxt (Constant _) = True

263 isInj ctxt (TType _) = True

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

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

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

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

433 foB b = findOuter h env (binderTy b)

434− findOuter h env (App f a)

434+ findOuter h env (App _ f a)

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

436 findOuter h env _ = []

437

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

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

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

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

545 rebind hs t = t

546

547apply, 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

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

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

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

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

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

291 let ntimes' = case f of

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

299 when spec $ setBlock False

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

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

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

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

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

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

308 a' <- ev ntimes stk False env a

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

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

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

435 _ -> return Nothing

436

437− conHeaded tm@(App _ _)

437+ conHeaded tm@(App _ _ _)

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

439 conHeaded t = False

440

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

540 v' <- quote i v

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

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

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

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

546 quote i VErased = return $ Erased

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

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

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

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

580 = 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

582 = 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' _)))

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

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

587

588 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

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

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

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

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

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

610 put (v, ULE x y : cs)

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

1083uniqueBindersCtxt ctxt ns (Bind n b sc)

1084 = let n' = uniqueNameCtxt ctxt n ns in

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

1087uniqueBindersCtxt ctxt ns t = t

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

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

103 return n'

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

105 e2' <- toTT e2

106− return $ App e1' e2'

106+ return $ App Complete e1' e2'

107toTT (EType u) = return $ TType u

108toTT (EUType u) = return $ UType u

109toTT EErased = return Erased

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

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

193 return $

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

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

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

196 do let (f, args) = unApply a

197 f' <- doExec env ctxt f

198 args' <- case f' of

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

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

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

329 Bind n' (Let t v') sc

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

332 cl env t = t

333

334attack :: RunTactic

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

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

662mkP :: TT Name -> TT Name -> TT Name -> TT Name -> TT Name

663mkP 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

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

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

666− App f' a'

666+ App s f' a'

667mkP lt l r (Bind n b sc)

668 = let b' = mkPB b

669 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

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

23data TermPath = Top

24− | AppL TermPath Term

24+ | AppL (AppStatus Name) TermPath Term

25− | AppR Term TermPath

25+ | AppR (AppStatus Name) Term TermPath

26 | InBind Name BinderPath Term

27 | InScope Name (Binder Term) TermPath

28 deriving Show

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

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

40replaceTop :: TermPath -> TermPath -> TermPath

41replaceTop p Top = p

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

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

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

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

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

45 where

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

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

54rebuildTerm :: Term -> TermPath -> Term

55rebuildTerm tm Top = tm

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

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

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

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

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

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

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

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

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

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

76− fh' env path (App f a)

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

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

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 p a, env', tm)

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

79 fh' env path (Bind x b sc)

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

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

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

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

167 else (tm, False)

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

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

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

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

172 else (t, False)

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

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

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

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

190

191 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

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

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

195 where

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

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

209updateSolvedPath [] t = t

210updateSolvedPath ns Top = Top

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

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

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

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

213updateSolvedPath ns (InBind n b sc)

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

215 where

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

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

247 | otherwise

248 = 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

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

251

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

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

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

293 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

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

296

297 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

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

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

310 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

312bound_in_term _ = []

313

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

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

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

808 _ == _ = False

809

810+data AppStatus n = Complete

811+ | MaybeHoles

812+ | Holes [n]

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

814+

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

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

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

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

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

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

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

815 -- Pure Type Systems Formalized)

820 -- Pure Type Systems Formalized)

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

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

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

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

819 | Constant Const -- ^ constant

824 | Constant Const -- ^ constant

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

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

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

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

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

851 termsize n (Bind n' b sc)

856 termsize n (Bind n' b sc)

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

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

853 termsize rn sc

858 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

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

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

856 termsize n _ = 1

861 termsize n _ = 1

857

862

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

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

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

860 size (V v) = 1

865 size (V v) = 1

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

866 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

863 size (Constant c) = size c

868 size (Constant c) = size c

864 size Erased = 1

869 size Erased = 1

865 size (TType u) = 1 + size u

870 size (TType u) = 1 + size u

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

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

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

881 (==) (V x) (V y) = x == y

886 (==) (V x) (V y) = x == y

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

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

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

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

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

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

885 (==) (Constant x) (Constant y) = x == y

890 (==) (Constant x) (Constant y) = x == y

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

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

887 (==) Erased _ = True

892 (==) Erased _ = True

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

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

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

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

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

899isInjective (Constant _) = True

904isInjective (Constant _) = True

900−isInjective (TType x) = True

905+isInjective (TType x) = True

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

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

902−isInjective (App f a) = isInjective f

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

903isInjective _ = False

908isInjective _ = False

904

909

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

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

906vinstances :: Int -> TT n -> Int

911vinstances :: Int -> TT n -> Int

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

912vinstances 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

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

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

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

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

911 instancesB _ = 0

916 instancesB _ = 0

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

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

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

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

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

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

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

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

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

922 subst i t = t

927 subst i t = t

923

928

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

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

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

931 | otherwise = V x

936 | otherwise = V x

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

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

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

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

935 dropV i t = t

940 dropV i t = t

936

941

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

941 Bind x b'

946 Bind x b'

942 (explicitNames (instantiate

947 (explicitNames (instantiate

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

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

945explicitNames (Proj x idx) = Proj (explicitNames x) idx

950explicitNames (Proj x idx) = Proj (explicitNames x) idx

946explicitNames t = t

951explicitNames t = t

947

952

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

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

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

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

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

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

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

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

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

960pToV' n i t = t

965pToV' n i t = t

961

966

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

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

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

967 | otherwise = V i

972 | otherwise = V i

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

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

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

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

971 ab top t = t

976 ab top t = t

972

977

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

985 P Bound n (binderTy b)

990 P Bound n (binderTy b)

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

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

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

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

989 vToP' env t = t

994 vToP' env t = t

990

995

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

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

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

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

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

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

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

999finalise (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)

996finalise t = t

1001finalise t = t

997

1002

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

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

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

1000

1005

1001pEraseType :: TT n -> TT n

1006pEraseType :: TT n -> TT n

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

1007pEraseType (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)

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

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

1005pEraseType t = t

1010pEraseType t = t

1006

1011

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

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

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

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

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

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

1034 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

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

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

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

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

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

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

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

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

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

1035 subst' i t = (t, False)

1040 subst' i t = (t, False)

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

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

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

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

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

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

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

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

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

1059 s' i t = t

1064 s' i t = t

1060

1065

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

1072 -> TT n

1077 -> TT n

1073substTerm old new = st where

1078substTerm old new = st where

1074 st t | t == old = new

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

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

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

1077 st t = t

1082 st t = t

1078

1083

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

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

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

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

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

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

1093 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

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

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

1091 no' i _ = return ()

1096 no' i _ = return ()

1092

1097

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

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

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

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

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

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

1107 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

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

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

1105 no' i _ = True

1110 no' i _ = True

1106

1111

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

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

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

1113 ++ freeNames' t

1118 ++ freeNames' t

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

1119 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

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

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

1117 freeNames' _ = []

1122 freeNames' _ = []

1118

1123

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

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

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

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

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

1126unApply t = ua [] t where

1131unApply t = ua [] t where

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

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

1128 ua args t = (t, args)

1133 ua args t = (t, args)

1129

1134

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

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

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

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

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

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

1133mkApp f [] = f

1138mkApp f [] = f

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

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

1135

1140

1136unList :: Term -> Maybe [Term]

1141unList :: Term -> Maybe [Term]

1137unList tm = case unApply tm of

1142unList tm = case unApply tm of

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

1172 (safeForgetEnv env v)

1177 (safeForgetEnv env v)

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

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

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

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

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

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

1177safeForgetEnv env (TType i) = Just RType

1182safeForgetEnv env (TType i) = Just RType

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

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

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

1225 = let n' = uniqueNameSet n ns

1230 = let n' = uniqueNameSet n ns

1226 ns' = insert n' ns in

1231 ns' = insert n' ns in

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

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

1229 ubSet ns t = t

1234 ubSet ns t = t

1230

1235

1231

1236

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

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

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

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

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

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

1325 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 =

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

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

1323 prettySe p env (Proj x i) debug =

1328 prettySe p env (Proj x i) debug =

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

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

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

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

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

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

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

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

1369 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

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

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

1367 se p env (Constant c) = show c

1372 se p env (Constant c) = show c

1368 se p env Erased = "[__]"

1373 se p env Erased = "[__]"

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

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

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

1388 | otherwise = str

1393 | otherwise = str

1389

1394

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

1391pureTerm :: TT Name -> Bool

1396pureTerm :: TT Name -> Bool

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

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

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

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

1394 pureBinder (Hole _) = False

1399 pureBinder (Hole _) = False

1395 pureBinder (Guess _ _) = False

1400 pureBinder (Guess _ _) = False

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

1405weakenTm :: Int -> TT n -> TT n

1410weakenTm :: Int -> TT n -> TT n

1406weakenTm i t = wk i 0 t

1411weakenTm i t = wk i 0 t

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

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

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

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

1410 wk i m t = t

1415 wk i m t = t

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

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

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

1430orderPats :: Term -> Term

1435orderPats :: Term -> Term

1431orderPats tm = op [] tm

1436orderPats tm = op [] tm

1432 where

1437 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

1434

1439

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

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

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

1441 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

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

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

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

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

1457 nb t = refsIn (binderTy t)

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

1459refsIn _ = []

1464refsIn _ = []

1460

1465

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

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

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

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

1493

1498

1494

1499

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

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

1496− a' <- getPats a

1501+ a' <- getPats a

1497− return (App f' a')

1502+ return (App s f' a')

1498 getPats t = return t

1503 getPats t = return t

1499

1504

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

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

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

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

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

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

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

1506 nb t = allNamesIn (binderTy t)

1511 nb t = allNamesIn (binderTy t)

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

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

1508 allNamesIn _ = []

1513 allNamesIn _ = []

1509

1514

1510

1515

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

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

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

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

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

1529 pp startPrec (n:bound) sc

1534 pp startPrec (n:bound) sc

1530− pp p bound (App tm1 tm2) =

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

1531 bracket p appPrec . group . hang 2 $

1536 bracket p appPrec . group . hang 2 $

1532 pp appPrec bound tm1 <> line <>

1537 pp appPrec bound tm1 <> line <>

1533 pp (appPrec + 1) bound tm2

1538 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

77 smaller _ (UType u) = UType u

78 smaller x _ = x

80+ astate | holes = MaybeHoles

81+ | otherwise = Complete

82+

80 chk :: Type -> -- uniqueness level

83 chk :: Type -> -- uniqueness level

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

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

82 chk u env (Var n)

85 chk u env (Var n)

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

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

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

102 let apty = simplify initContext env

105 let apty = simplify initContext env

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

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

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

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

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

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

107 convertsC ctxt env aty s

110 convertsC ctxt env aty s

108 let apty = simplify initContext env

111 let apty = simplify initContext env

109 (Bind x (Let aty av) t)

112 (Bind x (Let aty av) t)

110− return (App fv av, apty)

113+ return (App astate fv av, apty)

111 t -> lift $ tfail $ NonFunctionType fv fty

114 t -> lift $ tfail $ NonFunctionType fv fty

112 chk u env ap@(RApp f a)

115 chk u env ap@(RApp f a)

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

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

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

123 do convertsC ctxt env aty s

126 do convertsC ctxt env aty s

124 let apty = simplify initContext env

127 let apty = simplify initContext env

125 (Bind x (Let aty av) t)

128 (Bind x (Let aty av) t)

126− return (App fv av, apty)

129+ return (App astate fv av, apty)

127 t -> lift $ tfail $ NonFunctionType fv fty

130 t -> lift $ tfail $ NonFunctionType fv fty

128 chk u env RType

131 chk u env RType

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

308 chkBinders env a

311 chkBinders env a

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

312 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

311 chkBinders env (Bind n b t)

314 chkBinders env (Bind n b t)

312 = do chkBinderName env n b

315 = do chkBinderName env n b

313 st <- get

316 st <- get

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

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

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

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

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

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

101 holeIn env f || f `elem` holes

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

103 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

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

106 holeIn env f || f `elem` holes

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

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

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

111 holeIn env f || f `elem` holes

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

113 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

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

116 holeIn env f || f `elem` holes

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

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

135 = do h1 <- uB bnames bx by

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

137 combine bnames h1 h2

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

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

139 = do hf <- un names fx fy

140 ha <- un names ax ay

141 combine names hf ha

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

218 bind i ns tm

219 | i < 0 = tm

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

222 (P Bound x ty)

223

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

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

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

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

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

237 uniqueBinders env t = t

238

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

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

242 rename n n' t = t

243

244 explicitHole (Bind n (Hole ty) sc)

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

280

281hasv :: TT Name -> Bool

282hasv (V x) = True

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

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

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

285hasv _ = False

286

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

315

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

317 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

321 injective _ = False

319 injective _ = False

322

320

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

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

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

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

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

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

326 injectiveVar _ = False

324 injectiveVar _ = False

327

325

328 injectiveApp x = injective x || injectiveVar x

326 injectiveApp x = injective x || injectiveVar x

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

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

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

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

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

428

426

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

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

430 = unApp fn bnames appx appy

428 = unApp fn bnames appx appy

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

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

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

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

433

431

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

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

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

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

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

439 = un' False bnames x y

437 = 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

441 = un' False bnames x y

439 = un' False bnames x y

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

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

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

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

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

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

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

448 -- class resolution for type classes over functions.

446 -- class resolution for type classes over functions.

449

447

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)

451 | noOccurrence n y && injectiveApp f

449 | noOccurrence n y && injectiveApp f

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

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

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

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

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

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

455 combine bnames ux uf

453 combine bnames ux uf

456

454

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)

458 | noOccurrence n y && injectiveApp f

456 | noOccurrence n y && injectiveApp f

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

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

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

458 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 =

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

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

482 return [] -- lift $ tfail err

480 return [] -- lift $ tfail err

483

481

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

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

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

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

486 -- arguments are correct

484 -- arguments are correct

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

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

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

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

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

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

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

547 rigid (Constant _) = True

545 rigid (Constant _) = True

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

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

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

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

550

548

551 globmetavar t = case unApply t of

549 globmetavar t = case unApply t of

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

636 bind i ns tm

634 bind i ns tm

637 | i < 0 = tm

635 | i < 0 = tm

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

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

640 (P Bound x ty)

638 (P Bound x ty)

641

639

642 combineArgs bnames args = ca [] args where

640 combineArgs bnames args = ca [] args where

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

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

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

659 | otherwise = [j]

657 | otherwise = [j]

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

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

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

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

662− xs = boundVs i x in

660+ xs = boundVs i x in

663− nub (fs ++ xs)

661+ nub (fs ++ xs)

664boundVs i _ = []

662boundVs i _ = []

665

663

666highV :: Int -> Term -> Int

664highV :: Int -> Term -> Int

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

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

668 | otherwise = i

666 | otherwise = i

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

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

671highV i _ = i

669highV i _ = i

672

670

673envPos x i [] = 0

671envPos x i [] = 0

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

683--

681--

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

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

685--

683--

686−recoverable t@(App _ _) _

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

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

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

688−recoverable _ t@(App _ _)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

704 | f == f' = recoverable a a'

702 | f == f' = recoverable a a'

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

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

706 = recoverable f f' -- && recoverable a a'

704 = recoverable f f' -- && recoverable a a'

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

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

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

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

src/Idris/Coverage.hs+10−10

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

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

318

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

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

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

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

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

323 let ctxt = tt_ctxt i

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

329 return (and (ok : argsprod) )

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

331 return (and argsprod)

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

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

333− (prod n done False a)

333+ (prod n done False a)

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

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

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

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

368 = case lookupTotal fn (tt_ctxt i) of

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

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

372 checkLHS _ _ = Nothing

373

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

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

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

478

479delazy = delazy' False -- not lazy codata

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

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

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

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

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

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

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

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

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

489delazy' all t = t

490

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

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

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

500

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

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

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

503 -- that it is total.

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

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

519 else Unguarded in

520 mkChange n args pargs ++

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

522− findCalls guarded (App f a) pvs pargs

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

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

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

525 = findCalls Unguarded t pvs pargs ++

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

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

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

563 (fst (unApply (getRetTy tyt)))

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

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

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

566 = let tyn = getType n in

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

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

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

571 smaller _ _ _ = False

572

573 toJust (n, t) = Just t

src/Idris/DataOpts.hs+6−6

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

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

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

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

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

68 = applyOpts x

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

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

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

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

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

76 = return $ applyDataOptRT n t arity uniq []

77− applyOpts t@(App f a)

77+ applyOpts t@(App s f a)

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

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

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

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

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

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

83 applyOpts t = return t

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

103 = Constant (BI 0)

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

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

107

108 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

49 where

50 un = fileFC "(val)"

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

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

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

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

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

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

103 _ -> ns

104 dens n = n

105

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

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

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

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

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

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

163 | otherwise = tm

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

165 nonVar [x] = x

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

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

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

168 nonVar (x:xs) = nonVar xs

169-- | How far to indent sub-errors

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

256 y)) <>

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

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

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

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

263 flagUnique t = t

264pprintErr' i (CantSolveGoal x env) =

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

423

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

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

427 rename ns (Bind x b sc)

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

429 sc' = rename ns sc in

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

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

433 showArg _ = ""

434

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

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

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

437 qshow (P _ n _) = show n

438 qshow (Constant c) = show c

439 qshow _ = ""

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

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

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

496

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

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

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

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

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

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

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

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

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

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

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

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

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

749 | owner == txt "Ownership" &&

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

751 where

752 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

754 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

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

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

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

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

175

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

177− getDataApp f@(App _ _)

177+ getDataApp f@(App _ _ _)

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

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

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

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

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

317

318 isInj i (P Bound n _) = True

319 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

321 isInj i (V _) = True

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

323 isInj _ _ = True

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

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

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

112 -- error messages with less normalisation

113 providerOf :: Type -> Type

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

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

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

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

116 ty

117

118 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

215 errrep = txt "ErrorReportPart"

216

217 tyIsHandler (Bind _ (Pi _ (P _ (NS (UN e) ns1) _) _)

218− (App (P _ (NS (UN m) ns2) _)

218+ (App _ (P _ (NS (UN m) ns2) _)

219− (App (P _ (NS (UN l) ns3) _)

219+ (App _ (P _ (NS (UN l) ns3) _)

220 (P _ (NS (UN r) ns4) _))))

221 | e == err && m == maybe && l == lst && r == errrep

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

171 _ -> []

172getFixedInType i env (_ : is) (Bind n (Pi _ t _) sc)

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

175 | (P _ tn _, args) <- unApply tm

176 = case lookupCtxt tn (idris_datatypes i) of

177 [t] -> nub $ paramNames args env (param_pos t) ++

@@ -186,7 +186,7 @@ getFixedInType i _ _ _ = []

186getFlexInType i env ps (Bind n (Pi _ t _) sc)

187 = nub $ (if (not (n `elem` ps)) then getFlexInType i env ps t else []) ++

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

190 | (P _ tn _, args) <- unApply tm

191 = case lookupCtxt tn (idris_datatypes i) of

192 [t] -> nub $ paramNames args env [x | x <- [0..length args],

@@ -232,7 +232,7 @@ getUniqueUsed ctxt tm = execState (getUniq [] [] tm) []

232 _ -> False in

233 do getUniqB env us b

234 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

236 getUniq env us (V i)

237 | i < length us = if snd (us!!i) then use (fst (us!!i)) else return ()

238 getUniq env us (P _ n _)

src/Idris/ElabTerm.hs+24−24

@@ -430,7 +430,7 @@ elab ist info emode opts fn tm

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

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

432 pexp l, pexp r])

433− elab' ina fc (PAlternative True as)

433+ elab' ina fc (PAlternative True as)

434 = do hnf_compute

435 ty <- goal

436 ctxt <- get_context

@@ -967,7 +967,7 @@ elab ist info emode opts fn tm

967 _ -> n

968

969 inApp (P _ n _) = [n]

970− inApp (App f a) = inApp f ++ inApp a

970+ inApp (App _ f a) = inApp f ++ inApp a

971 inApp (Bind n (Let _ v) sc) = inApp v ++ inApp sc

972 inApp (Bind n (Guess _ v) sc) = inApp v ++ inApp sc

973 inApp (Bind n b sc) = inApp sc

@@ -1561,7 +1561,7 @@ collectDeferred top (Bind n b t) = do b' <- cdb b

1561 cdb (Guess t v) = liftM2 Guess (collectDeferred top t) (collectDeferred top v)

1562 cdb b = do ty' <- collectDeferred top (binderTy b)

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

1565collectDeferred top t = return t

1566

1567case_ :: Bool -> Bool -> IState -> Name -> PTerm -> ElabD ()

@@ -1638,7 +1638,7 @@ runTactical fc env tm = do tm' <- eval tm

1638 | n == tacN "prim__BindTactical", [_a, _b, first, andThen] <- args

1639 = do first' <- eval first

1640 res <- runTacTm first'

1641− next <- eval (App andThen res)

1641+ next <- eval (App Complete andThen res)

1642 runTacTm next

1643 | n == tacN "prim__Try", [_a, first, alt] <- args

1644 = do first' <- eval first

@@ -1983,7 +1983,7 @@ reify _ (P _ n _) | n == reflm "Compute" = return Compute

1983reify _ (P _ n _) | n == reflm "Skip" = return Skip

1984reify _ (P _ n _) | n == reflm "SourceFC" = return SourceFC

1985reify _ (P _ n _) | n == reflm "Unfocus" = return Unfocus

1986−reify ist t@(App _ _)

1986+reify ist t@(App _ _ _)

1987 | (P _ f _, args) <- unApply t = reifyApp ist f args

1988reify _ t = fail ("Unknown tactic " ++ show t)

1989

@@ -2043,7 +2043,7 @@ reifyReportParts errs =

2043

2044-- | Reify terms from their reflected representation

2045reifyTT :: Term -> ElabD Term

2046−reifyTT t@(App _ _)

2046+reifyTT t@(App _ _ _)

2047 | (P _ f _, args) <- unApply t = reifyTTApp f args

2048reifyTT t@(P _ n _)

2049 | n == reflm "Erased" = return $ Erased

@@ -2067,7 +2067,7 @@ reifyTTApp t [n, b, x]

2067reifyTTApp t [f, x]

2068 | t == reflm "App" = do f' <- reifyTT f

2069 x' <- reifyTT x

2070− return $ App f' x'

2070+ return $ App Complete f' x'

2071reifyTTApp t [c]

2072 | t == reflm "TConst" = liftM Constant (reifyTTConst c)

2073reifyTTApp t [t', Constant (I i)]

@@ -2079,7 +2079,7 @@ reifyTTApp t args = fail ("Unknown reflection term: " ++ show (t, args))

2079

2080-- | Reify raw terms from their reflected representation

2081reifyRaw :: Term -> ElabD Raw

2082−reifyRaw t@(App _ _)

2082+reifyRaw t@(App _ _ _)

2083 | (P _ f _, args) <- unApply t = reifyRawApp f args

2084reifyRaw t@(P _ n _)

2085 | n == reflm "RType" = return $ RType

@@ -2120,7 +2120,7 @@ reifyTTNameApp t []

2120reifyTTNameApp t args = fail ("Unknown reflection term name: " ++ show (t, args))

2121

2122reifyTTNamespace :: Term -> ElabD [String]

2123−reifyTTNamespace t@(App _ _)

2123+reifyTTNamespace t@(App _ _ _)

2124 = case unApply t of

2125 (P _ f _, [Constant StrType])

2126 | f == sNS (sUN "Nil") ["List", "Prelude"] -> return []

@@ -2132,7 +2132,7 @@ reifyTTNamespace t = fail ("Unknown reflection namespace arg: " ++ show t)

2132reifyTTNameType :: Term -> ElabD NameType

2133reifyTTNameType t@(P _ n _) | n == reflm "Bound" = return $ Bound

2134reifyTTNameType t@(P _ n _) | n == reflm "Ref" = return $ Ref

2135−reifyTTNameType t@(App _ _)

2135+reifyTTNameType t@(App _ _ _)

2136 = case unApply t of

2137 (P _ f _, [Constant (I tag), Constant (I num)])

2138 | f == reflm "DCon" -> return $ DCon tag num False -- FIXME: Uniqueness!

@@ -2141,7 +2141,7 @@ reifyTTNameType t@(App _ _)

2141reifyTTNameType t = fail ("Unknown reflection name type: " ++ show t)

2142

2143reifyTTBinder :: (Term -> ElabD a) -> Name -> Term -> ElabD (Binder a)

2144−reifyTTBinder reificator binderType t@(App _ _)

2144+reifyTTBinder reificator binderType t@(App _ _ _)

2145 = case unApply t of

2146 (P _ f _, bt:args) | forget bt == Var binderType

2147 -> reifyTTBinderApp reificator f args

@@ -2173,7 +2173,7 @@ reifyTTConst :: Term -> ElabD Const

2173reifyTTConst (P _ n _) | n == reflm "StrType" = return $ StrType

2174reifyTTConst (P _ n _) | n == reflm "VoidType" = return $ VoidType

2175reifyTTConst (P _ n _) | n == reflm "Forgot" = return $ Forgot

2176−reifyTTConst t@(App _ _)

2176+reifyTTConst t@(App _ _ _)

2177 | (P _ f _, [arg]) <- unApply t = reifyTTConstApp f arg

2178reifyTTConst t = fail ("Unknown reflection constant: " ++ show t)

2179

@@ -2201,7 +2201,7 @@ reifyTTConstApp f (Constant c@(B64 _))

2201reifyTTConstApp f arg = fail ("Unknown reflection constant: " ++ show (f, arg))

2202

2203reifyArithTy :: 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)

2205reifyArithTy (P _ n _) | n == reflm "ATFloat" = return ATFloat

2206reifyArithTy x = fail ("Couldn't reify reflected ArithTy: " ++ show x)

2207

@@ -2213,14 +2213,14 @@ reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8

2213reifyNativeTy x = fail $ "Couldn't reify reflected NativeTy " ++ show x

2214

2215reifyIntTy :: 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)

2217reifyIntTy (P _ n _) | n == reflm "ITNative" = return ITNative

2218reifyIntTy (P _ n _) | n == reflm "ITBig" = return ITBig

2219reifyIntTy (P _ n _) | n == reflm "ITChar" = return ITChar

2220reifyIntTy tm = fail $ "The term " ++ show tm ++ " is not a reflected IntTy"

2221

2222reifyTTUExp :: Term -> ElabD UExp

2223−reifyTTUExp t@(App _ _)

2223+reifyTTUExp t@(App _ _ _)

2224 = case unApply t of

2225 (P _ f _, [Constant (I i)]) | f == reflm "UVar" -> return $ UVar i

2226 (P _ f _, [Constant (I i)]) | f == reflm "UVal" -> return $ UVal i

@@ -2289,7 +2289,7 @@ reflectTTQuotePattern unq (Bind n b x)

2289 solve

2290 focus x'; reflectTTQuotePattern unq x

2291 focus b'; reflectBinderQuotePattern reflectTTQuotePattern unq b

2292−reflectTTQuotePattern unq (App f x)

2292+reflectTTQuotePattern unq (App _ f x)

2293 = do f' <- claimTT (sMN 0 "f"); movelast f'

2294 x' <- claimTT (sMN 0 "x"); movelast x'

2295 fill $ reflCall "App" [Var f', Var x']

@@ -2472,7 +2472,7 @@ reflectTTQuote unq (V n)

2472 = reflCall "V" [RConstant (I n)]

2473reflectTTQuote unq (Bind n b x)

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

2476 = reflCall "App" [reflectTTQuote unq f, reflectTTQuote unq x]

2477reflectTTQuote unq (Constant c)

2478 = reflCall "TConst" [reflectConstant c]

@@ -2814,7 +2814,7 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

2814 parts -> ReflectionError errorparts e

2815

2816fromTTMaybe :: 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)

2818 | just == txt "Just" = Just tm

2819fromTTMaybe x = Nothing

2820

@@ -2825,9 +2825,9 @@ reflErrName n = sNS (sUN n) ["Errors", "Reflection", "Language"]

2825-- representation. Not in Idris or ElabD monads because it should be usable

2826-- from either.

2827reifyReportPart :: 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" =

2829 Right (TextPart msg)

2830−reifyReportPart (App (P (DCon _ _ _) n _) ttn)

2830+reifyReportPart (App _ (P (DCon _ _ _) n _) ttn)

2831 | n == reflm "NamePart" =

2832 case runElab initEState (reifyTTName ttn) (initElaborator NErased initContext Erased) of

2833 Error e -> Left . InternalMsg $

@@ -2835,7 +2835,7 @@ reifyReportPart (App (P (DCon _ _ _) n _) ttn)

2835 show ttn ++

2836 " when reflecting an error:" ++ show e

2837 OK (n', _)-> Right $ NamePart n'

2838−reifyReportPart (App (P (DCon _ _ _) n _) tm)

2838+reifyReportPart (App _ (P (DCon _ _ _) n _) tm)

2839 | n == reflm "TermPart" =

2840 case runElab initEState (reifyTT tm) (initElaborator NErased initContext Erased) of

2841 Error e -> Left . InternalMsg $

@@ -2843,7 +2843,7 @@ reifyReportPart (App (P (DCon _ _ _) n _) tm)

2843 show tm ++

2844 " when reflecting an error:" ++ show e

2845 OK (tm', _) -> Right $ TermPart tm'

2846−reifyReportPart (App (P (DCon _ _ _) n _) tm)

2846+reifyReportPart (App _ (P (DCon _ _ _) n _) tm)

2847 | n == reflm "SubReport" =

2848 case unList tm of

2849 Just xs -> do subParts <- mapM reifyReportPart xs

@@ -2852,7 +2852,7 @@ reifyReportPart (App (P (DCon _ _ _) n _) tm)

2852reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x

2853

2854reifyTyDecl :: 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)

2856 | n == tacN "Declare" =

2857 do tyN' <- reifyTTName tyN

2858 args' <- case unList args of

@@ -2861,7 +2861,7 @@ reifyTyDecl (App (App (App (P (DCon _ _ _) n _) tyN) args) ret)

2861 ret' <- reifyRaw ret

2862 return $ RDeclare tyN' args' ret'

2863 where reifyRArg :: Term -> ElabD RArg

2864− reifyRArg (App (App (P (DCon _ _ _) n _) argN) argTy)

2864+ reifyRArg (App _ (App _ (P (DCon _ _ _) n _) argN) argTy)

2865 | n == tacN "Explicit" = liftM2 RExplicit

2866 (reifyTTName argN)

2867 (reifyRaw argTy)

src/Idris/Erasure.hs+6−6

@@ -279,7 +279,7 @@ buildDepMap ci used externs ctx startNames

279

280 etaExpand :: [Name] -> Term -> Term

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

283

284 getDepsSC :: Name -> [Name] -> Vars -> SC -> Deps

285 getDepsSC fn es vs ImpossibleCase = M.empty

@@ -370,7 +370,7 @@ buildDepMap ci used externs ctx startNames

370 var t cd = getDepsTerm vs bs cd t

371

372 -- applications may add items to Cond

373− getDepsTerm vs bs cd app@(App _ _)

373+ getDepsTerm vs bs cd app@(App _ _ _)

374 | (fun, args) <- unApply app = case fun of

375 -- instance constructors -> create metamethod deps

376 P (DCon _ _ _) ctorName@(SN (InstanceCtorN className)) _

@@ -418,8 +418,8 @@ buildDepMap ci used externs ctx startNames

418 Bind n (Lam ty) t -> getDepsTerm vs bs cd (lamToLet [] app)

419

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

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

423

424 Proj t i

425 -> error $ "cannot[0] analyse projection !" ++ show i ++ " of " ++ show t

@@ -493,9 +493,9 @@ buildDepMap ci used externs ctx startNames

493 -- convert applications of lambdas to lets

494 -- Note that this transformation preserves de bruijn numbering

495 lamToLet :: [Term] -> Term -> Term

496− lamToLet xs (App f x) = lamToLet (x:xs) f

496+ lamToLet xs (App _ f x) = lamToLet (x:xs) f

497 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

499 lamToLet [] t = t

500

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

36 matchTerm ns l r t

37 | Just nmap <- match ns l t = substNames nmap r

38− matchTerm ns l r (App f a) = let f' = matchTerm ns l r f

38+ matchTerm ns l r (App s f a) = let f' = matchTerm ns l r f

39− a' = matchTerm ns l r a in

39+ a' = matchTerm ns l r a in

40− App f' a'

40+ App s f' a'

41 matchTerm ns l r (Bind n b sc) = let b' = fmap (matchTerm ns l r) b

42 sc' = matchTerm ns l r sc in

43 Bind n b' sc'

@@ -54,16 +54,16 @@ errReverse ist t = rewrite 5 t -- (elideLambdas t)

54 Just ((x, t) : xs')

56 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'

57+ match' ns (App _ f a) (App _ f' a') = do fs <- match' ns f f'

58− as <- match' ns a a'

58+ as <- match' ns a a'

59− Just (fs ++ as)

59+ Just (fs ++ as)

60 -- no matching Binds, for now...

61 match' ns x y = if x == y then Just [] else Nothing

63 -- if the term under a lambda is huge, there's no much point in showing

64 -- it as it won't be very enlightening.

66− elideLambdas (App f a) = App (elideLambdas f) (elideLambdas a)

66+ elideLambdas (App s f a) = App s (elideLambdas f) (elideLambdas a)

67 elideLambdas (Bind n (Lam t) sc)

68 | size sc > 200 = P Ref (sUN "...") Erased

69 elideLambdas (Bind n b sc)

src/Idris/IBC.hs+1−1

@@ -501,7 +501,7 @@ pDefs reexp syms ds

501

502 update (P t n ty) = do n' <- getSymbol n

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

505 update (Bind n b sc) = do b' <- updateB b

506 sc' <- update sc

507 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

21inlineTerm :: IState -> Term -> Term

22inlineTerm ist tm = inl tm where

23 inl orig@(P _ n _) = inlApp n [] orig

24− inl orig@(App f a)

24+ inl orig@(App _ f a)

25 | (P _ fn _, args) <- unApply orig = inlApp fn args orig

26 inl (Bind n (Let t v) sc) = Bind n (Let t (inl v)) (inl sc)

27 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

322 guessImps ctxt _ = []

323

324 guarded ctxt n (P _ n' _) | n == n' = True

325− guarded ctxt n ap@(App _ _)

325+ guarded ctxt n ap@(App _ _ _)

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

327 isConName f ctxt = any (guarded ctxt n) args

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

146 = do nm <- get

147 put (nm + 1)

148 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

150 gen tm = return tm

151

152-- | Checks if a given argument is a type class constraint argument

@@ -291,7 +291,7 @@ getSpecApps ist env tm = ga env (explicitNames tm) where

291

292 -- if we have a *defined* function that has static arguments,

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

295 n `notElem` map fst (idris_metavars ist) =

296 ga env f ++ ga env a ++

297 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

128 toUN t@(P nt (MN i n) ty)

129 | ('_':xs) <- str n = t

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

132 toUN t = t

133

134 -- psRec counts depth and the local variable applications we're under

src/Idris/Transforms.hs+8−8

@@ -39,21 +39,21 @@ applyTransRulesWith rules tm

39 = finalise $ applyAll rules emptyContext (vToP tm)

41applyAll :: [(Term, Term)] -> Ctxt [(Term, Term)] -> Term -> Term

42−applyAll extra ts ap@(App f a)

42+applyAll extra ts ap@(App s f a)

43 | (P _ fn ty, args) <- unApply ap

44 = let rules = case lookupCtxtExact fn ts of

45 Just r -> extra ++ r

46 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

48 case rules of

49 [] -> ap'

50 rs -> case applyFnRules rs ap of

51− Just tm'@(App f' a') ->

51+ Just tm'@(App s f' a') ->

52− App (applyAll extra ts f')

52+ App s (applyAll extra ts f')

53− (applyAll extra ts a')

53+ (applyAll extra ts a')

54 Just tm' -> tm'

55− _ -> App (applyAll extra ts f)

55+ _ -> App s (applyAll extra ts f)

56− (applyAll extra ts a)

56+ (applyAll extra ts a)

57applyAll extra ts (Bind n b sc) = Bind n (fmap (applyAll extra ts) b)

58 (applyAll extra ts sc)

59applyAll extra ts t = t

@@ -94,7 +94,7 @@ matchTerm lhs tm = matchVars [] lhs tm

94 doMatch :: [Name] -> Term -> Term -> Maybe [(Name, Term)]

95 doMatch ns (P _ n _) tm

96 | n `elem` ns = return [(n, tm)]

97− doMatch ns (App f a) (App f' a')

97+ doMatch ns (App _ f a) (App _ f' a')

98 = do fm <- doMatch ns f f'

99 am <- doMatch ns a a'

100 return (fm ++ am)

src/Idris/TypeSearch.hs+7−6

@@ -104,9 +104,9 @@ typeFromDef (def, _, _, _) = get def where

104-- Replace all occurences of `Lazy' s t` with `t` in a type

105unLazy :: Type -> Type

106unLazy 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

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

110 Proj ty i -> Proj (unLazy ty) i

111 _ -> typ

112

@@ -146,7 +146,7 @@ usedVars = f True where

146 Let t v -> f b t `M.union` f b v

147 Guess t v -> f b t `M.union` f b v

148 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

150 f b (Proj t _) = f b t

151 f _ (V _) = error "unexpected! run vToP first"

152 f _ _ = M.empty

@@ -307,13 +307,14 @@ subsets (x : xs) = let ss = subsets xs in map (x :) ss ++ ss

307-- recalls the number of flips that have been made

308flipEqualities :: Type -> [(Int, Type)]

309flipEqualities t = case t of

310− eq1@(App (App (App (App eq@(P _ eqty _) tyL) tyR) valL) valR) | eqty == eqTy ->

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

311+ [(0, eq1), (1, app (app (app (app eq tyR) tyL) valR) valL)]

312 Bind n binder sc -> (\bind' (j, sc') -> (fst (binderTy bind') + j, Bind n (fmap snd bind') sc'))

313 <$> 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'))

315 <$> flipEqualities f <*> flipEqualities x

316 t' -> [(0, t')]

317+ where app = App Complete

317

318

318--DONT run vToP first!

319--DONT run vToP first!

319-- | Try to match two types together in a unification-like procedure.

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

13occurs n (P Bound _ _) = False

14occurs n (P _ n' _) = n == n'

15occurs 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

17occurs n (Proj t _) = occurs n t

18occurs n _ = False

@@ -21,7 +21,7 @@ names :: Term -> [Name]

21names (P Bound _ _) = []

22names (P _ n _) = [n]

23names (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

25names (Proj t _) = names t

26names _ = []