@@ -125,25 +125,42 @@ updateSolvedTerm :: [(Name, Term)] -> Term -> Term
125125updateSolvedTerm [] x = x
126126updateSolvedTerm xs x = -- updateSolved' xs x where
127127-- This version below saves allocations, because it doesn't need to reallocate
128−-- the term if there are no updates to do, but costs an extra pass. Below
129−-- version works better on larger terms...
130− if noneOf (map fst xs) x
131− then x
132− else updateSolved' xs x where
133− updateSolved' [] x = x
128+-- the term if there are no updates to do.
129+-- The Bool is ugly, and probably 'Maybe' would be less ugly, but >>= is
130+-- the wrong combinator. Feel free to tidy up as long as it's still as cheap :).
131+ fst $ updateSolved' xs x where
132+ updateSolved' [] x = (x, False)
134133 updateSolved' xs (Bind n (Hole ty) t)
135134 | Just v <- lookup n xs
136135 = case xs of
137− [_] -> substV v $ psubst n v t -- some may be Vs! Can't assume
138− -- explicit names
139− _ -> substV v $ psubst n v (updateSolved' xs t)
140− updateSolved' xs (Bind n b t)
141− | otherwise = Bind n (fmap (updateSolved' xs) b) (updateSolved' xs t)
142− updateSolved' xs (App f a)
143− = App (updateSolved' xs f) (updateSolved' xs a)
144− updateSolved' xs (P _ n@(MN _ _) _)
145− | Just v <- lookup n xs = v
146− updateSolved' xs t = t
136+ [_] -> (substV v $ psubst n v t, True) -- some may be Vs! Can't assume
137+ -- explicit names
138+ _ -> let (t', _) = updateSolved' xs t in
139+ (substV v $ psubst n v t', True)
140+ updateSolved' xs tm@(Bind n b t)
141+ | otherwise = let (t', ut) = updateSolved' xs t
142+ (b', ub) = updateSolvedB' xs b in
143+ if ut || ub then (Bind n b' t', True)
144+ else (tm, False)
145+ updateSolved' xs t@(App f a)
146+ = let (f', uf) = updateSolved' xs f
147+ (a', ua) = updateSolved' xs a in
148+ if uf || ua then (App f' a', True)
149+ else (t, False)
150+ updateSolved' xs t@(P _ n@(MN _ _) _)
151+ | Just v <- lookup n xs = (v, True)
152+ updateSolved' xs t = (t, False)
153+
154+ updateSolvedB' xs b@(Let t v) = let (t', ut) = updateSolved' xs t
155+ (v', uv) = updateSolved' xs v in
156+ if ut || uv then (Let t' v', True)
157+ else (b, False)
158+ updateSolvedB' xs b@(Guess t v) = let (t', ut) = updateSolved' xs t
159+ (v', uv) = updateSolved' xs v in
160+ if ut || uv then (Guess t' v', True)
161+ else (b, False)
162+ updateSolvedB' xs b = let (ty', u) = updateSolved' xs (binderTy b) in
163+ if u then (b { binderTy = ty' }, u) else (b, False)
147164
148165 noneOf ns (P _ n _) | n `elem` ns = False
149166 noneOf ns (App f a) = noneOf ns a && noneOf ns f