6b6aae0 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Avoid retrying unification problems constantly

If solved metavariables do nothing to a unification problem, there's no point in trying it again - this can lead to a massive slowdown if there's a lot of evaluation in the type. Partially addresses #1219. Fixes #1716 on the way by tidying up type of updateProblems.

commit6b6aae0bd82ac728836d907c9fc5e8b66c7e04b7 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 5 Dec 2014, 19:38 (12 years ago) parentbcd2db1

7 files changed+79−78

compare with master

unifiedsplit

src/Idris/Core/Elaborate.hs+3−3 src/Idris/Core/ProofState.hs+47−54 src/Idris/Core/ProofTerm.hs+6−4 src/Idris/Core/Unify.hs+15−9 src/Idris/Elab/Clause.hs+2−2 src/Idris/ElabTerm.hs+5−5 src/Idris/Prover.hs+1−1

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

@@ -687,7 +687,7 @@ no_errors tac err

687687 ps' <- get_probs

688688 if (length ps' > length ps) then

689689 case reverse ps' of

690− ((x, y, env, inerr, while, _) : _) ->

690+ ((x, y, _, env, inerr, while, _) : _) ->

691691 let env' = map (\(x, b) -> (x, binderTy b)) env in

692692 lift $ tfail $

693693 case err of

@@ -796,12 +796,12 @@ prunStateT pmax zok ps x s

796796 newpmax = if newps < 0 then 0 else newps in

797797 if (newpmax > pmax || (not zok && newps > 0)) -- length ps == 0 && newpmax > 0))

798798 then case reverse (problems p) of

799− ((_,_,_,e,_,_):_) -> Error e

799+ ((_,_,_,_,e,_,_):_) -> Error e

800800 else OK ((v, newpmax, problems p), s')

801801 Error e -> Error e

802802

803803qshow :: Fails -> String

804−qshow fs = show (map (\ (x, y, _, _, _, _) -> (x, y)) fs)

804+qshow fs = show (map (\ (x, y, _, _, _, _, _) -> (x, y)) fs)

805805

806806dumpprobs [] = ""

807807dumpprobs ((_,_,_,e):es) = show e ++ "\n" ++ dumpprobs es

src/Idris/Core/ProofState.hs+47−54

@@ -144,7 +144,7 @@ instance Pretty ProofState OutputAnnotation where

144144holeName i = sMN i "hole"

145145

146146qshow :: Fails -> String

147−qshow fs = show (map (\ (x, y, _, _, _, t) -> (t, x, y)) fs)

147+qshow fs = show (map (\ (x, y, hs, _, _, _, t) -> (t, x, y, hs)) fs)

148148

149149match_unify' :: Context -> Env -> TT Name -> TT Name ->

150150 StateT TState TC [(Name, TT Name)]

@@ -168,7 +168,8 @@ match_unify' ctxt env topx topy =

168168 return u

169169 Error e -> traceWhen (unifylog ps)

170170 ("No match " ++ show e) $

171− do put (ps { problems = (topx, topy, env, e, while, Match) :

171+ do put (ps { problems = (topx, topy, True,

172+ env, e, while, Match) :

172173 problems ps })

173174 return []

174175-- traceWhen (unifylog ps)

@@ -186,7 +187,7 @@ mergeSolutions env ns = merge [] ns

186187 | Just t' <- lookup n ns

187188 = do ps <- get

188189 let probs = problems ps

189− put (ps { problems = probs ++ [(t,t',env,Msg "New problem",

190+ put (ps { problems = probs ++ [(t,t',True,env,Msg "New problem",

190191 [], Unify)] })

191192 merge acc ns

192193 | otherwise = merge ((n, t): acc) ns

@@ -225,12 +226,8 @@ unify' ctxt env topx topy =

225226 -- problem for each.

226227 uns <- mergeSolutions env (u' ++ ns)

227228 ps <- get

228− let (ns', probs') = updateProblems (context ps) uns

229− (fails ++ problems ps)

230− (injective ps)

231− (holes ps)

232− (map fst (notunified ps))

233− let (notu', probs_notu) = mergeNotunified env (notu ++ notunified ps)

229+ let (ns', probs') = updateProblems ps uns (fails ++ problems ps)

230+ let (notu', probs_notu) = mergeNotunified env (holes ps) (notu ++ notunified ps)

234231 traceWhen (unifylog ps)

235232 ("Now solved: " ++ show ns' ++

236233 "\nNow problems: " ++ qshow (probs' ++ probs_notu)) $

@@ -780,7 +777,8 @@ keepGiven du (u : us) hs = keepGiven du us hs

780777

781778updateEnv [] e = e

782779updateEnv ns [] = []

783−updateEnv ns ((n, b) : env) = (n, fmap (updateSolvedTerm ns) b) : updateEnv ns env

780+updateEnv ns ((n, b) : env)

781+ = (n, fmap (updateSolvedTerm ns) b) : updateEnv ns env

784782

785783updateError [] err = err

786784updateError ns (At f e) = At f (updateError ns e)

@@ -796,13 +794,13 @@ solveInProblems x val ((l, r, env, err) : ps)

796794 = ((psubst x val l, psubst x val r,

797795 updateEnv [(x, val)] env, err) : solveInProblems x val ps)

798796

799−mergeNotunified :: Env -> [(Name, Term)] -> ([(Name, Term)], Fails)

800−mergeNotunified env ns = mnu ns [] [] where

797+mergeNotunified :: Env -> [Name] -> [(Name, Term)] -> ([(Name, Term)], Fails)

798+mergeNotunified env holes ns = mnu ns [] [] where

801799 mnu [] ns_acc ps_acc = (reverse ns_acc, reverse ps_acc)

802800 mnu ((n, t):ns) ns_acc ps_acc

803801 | Just t' <- lookup n ns, t /= t'

804802 = mnu ns ((n,t') : ns_acc)

805− ((t,t',env,CantUnify True t t' (Msg "") [] 0, [],Match) : ps_acc)

803+ ((t,t',True, env,CantUnify True t t' (Msg "") [] 0, [],Match) : ps_acc)

806804 | otherwise = mnu ns ((n,t) : ns_acc) ps_acc

807805

808806updateNotunified [] nu = nu

@@ -811,42 +809,53 @@ updateNotunified ns nu = up nu where

811809 up ((n, t) : nus) = let t' = updateSolvedTerm ns t in

812810 ((n, t') : up nus)

813811

814−-- FIXME: Why not just pass the whole proof state?

815−-- Issue #1716 on the issue tracker.

816−-- https://github.com/idris-lang/Idris-dev/issues/1716

817−updateProblems :: Context -> [(Name, TT Name)] -> Fails -> [Name] -> [Name] -> [Name]

818− -> ([(Name, TT Name)], Fails)

812+updateProblems :: ProofState -> [(Name, TT Name)] -> Fails

813+ -> ([(Name, TT Name)], Fails)

819814-- updateProblems ctxt [] ps inj holes = ([], ps)

820−updateProblems ctxt ns ps inj holes usupp = up ns ps where

815+updateProblems ps updates probs = up updates probs where

816+ hs = holes ps

817+ inj = injective ps

818+ ctxt = context ps

819+ usupp = map fst (notunified ps)

820+

821821 up ns [] = (ns, [])

822− up ns ((x, y, env, err, while, um) : ps) =

823− let x' = updateSolvedTerm ns x

824− y' = updateSolvedTerm ns y

822+ up ns (prob@(x, y, ready, env, err, while, um) : ps) =

823+ let (x', newx) = updateSolvedTerm' ns x

824+ (y', newy) = updateSolvedTerm' ns y

825825 err' = updateError ns err

826826 env' = updateEnv ns env in

827−-- trace ("Updating " ++ show (x',y')) $

828− case unify ctxt env' x' y' inj holes usupp while of

829− OK (v, []) -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $

827+ if newx || newy || ready ||

828+ any (\n -> n `elem` inj) (refsIn x ++ refsIn y) then

829+ case unify ctxt env' x' y' inj hs usupp while of

830+ OK (v, []) -> -- trace ("DID " ++ show (x',y',ready,v)) $

830831 up (ns ++ v) ps

831− e -> -- trace ("Failed " ++ show e) $

832− let (ns', ps') = up ns ps in

833− (ns', (x',y',env',err', while, um) : ps')

832+ e -> -- trace ("FAILED " ++ show (x',y',ready,e)) $

833+ let (ns', ps') = up ns ps in

834+ (ns', (x',y', False, env',err', while, um) : ps')

835+ else -- trace ("SKIPPING " ++ show (x,y,ready)) $

836+ let (ns', ps') = up ns ps in

837+ (ns', (x',y', False, env',err', while, um) : ps')

834838

835839-- attempt to solve remaining problems with match_unify

836−-- matchProblems :: Bool -> Elab' aux ()

837−matchProblems all ns ctxt ps inj holes = up ns ps where

840+matchProblems :: Bool -> ProofState -> [(Name, TT Name)] -> Fails

841+ -> ([(Name, TT Name)], Fails)

842+matchProblems all ps updates probs = up updates probs where

843+ hs = holes ps

844+ inj = injective ps

845+ ctxt = context ps

846+

838847 up ns [] = (ns, [])

839− up ns ((x, y, env, err, while, um) : ps)

848+ up ns ((x, y, ready, env, err, while, um) : ps)

840849 | all || um == Match =

841850 let x' = updateSolvedTerm ns x

842851 y' = updateSolvedTerm ns y

843852 err' = updateError ns err

844853 env' = updateEnv ns env in

845− case match_unify ctxt env' x' y' inj holes while of

854+ case match_unify ctxt env' x' y' inj hs while of

846855 OK v -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $

847856 up (ns ++ v) ps

848857 _ -> let (ns', ps') = up ns ps in

849− (ns', (x', y', env', err', while, um) : ps')

858+ (ns', (x', y', True, env', err', while, um) : ps')

850859 up ns (p : ps) = let (ns', ps') = up ns ps in

851860 (ns', p : ps')

852861

@@ -865,9 +874,7 @@ processTactic EndUnify ps

865874 = let (h, ns_in) = unified ps

866875 ns = dropGiven (dontunify ps) ns_in (holes ps)

867876 ns' = map (\ (n, t) -> (n, updateSolvedTerm ns t)) ns

868− (ns'', probs') = updateProblems (context ps) ns' (problems ps)

869− (injective ps) (holes ps)

870− (map fst (notunified ps))

877+ (ns'', probs') = updateProblems ps ns' (problems ps)

871878 tm' = updateSolved ns'' (pterm ps) in

872879 traceWhen (unifylog ps) ("Dropping holes: " ++ show (map fst ns'')) $

873880 return (ps { pterm = tm',

@@ -890,11 +897,7 @@ processTactic (ComputeLet n) ps

890897 computeLet (context ps) n

891898 (getProofTerm (pterm ps)) }, "")

892899processTactic UnifyProblems ps

893− = let (ns', probs') = updateProblems (context ps) []

894− (problems ps)

895− (injective ps)

896− (holes ps)

897− (map fst (notunified ps))

900+ = let (ns', probs') = updateProblems ps [] (problems ps)

898901 pterm' = updateSolved ns' (pterm ps) in

899902 traceWhen (unifylog ps) ("Dropping holes: " ++ show (map fst ns')) $

900903 return (ps { pterm = pterm', solved = Nothing, problems = probs',

@@ -903,14 +906,8 @@ processTactic UnifyProblems ps

903906 recents = recents ps ++ map fst ns',

904907 holes = holes ps \\ (map fst ns') }, plog ps)

905908processTactic (MatchProblems all) ps

906− = let (ns', probs') = matchProblems all [] (context ps)

907− (problems ps)

908− (injective ps)

909− (holes ps)

910− (ns'', probs'') = matchProblems all ns' (context ps)

911− probs'

912− (injective ps)

913− (holes ps)

909+ = let (ns', probs') = matchProblems all ps [] (problems ps)

910+ (ns'', probs'') = matchProblems all ps ns' probs'

914911 pterm' = updateSolved ns'' (pterm ps) in

915912 traceWhen (unifylog ps) ("Dropping holes: " ++ show (map fst ns'')) $

916913 return (ps { pterm = pterm', solved = Nothing, problems = probs'',

@@ -926,11 +923,7 @@ processTactic t ps

926923 = case solved ps' of

927924 Just s -> traceWhen (unifylog ps')

928925 ("SOLVED " ++ show s) $

929− updateProblems (context ps')

930− [s] (problems ps')

931− (injective ps')

932− (holes ps')

933− (map fst (notunified ps))

926+ updateProblems ps [s] (problems ps')

934927 _ -> ([], problems ps')

935928 -- rechecking problems may find more solutions, so

936929 -- apply them here

src/Idris/Core/ProofTerm.hs+6−4

@@ -5,7 +5,7 @@

55 evaluation/checking inside the proof system, etc. --}

77module Idris.Core.ProofTerm(ProofTerm, Goal(..), mkProofTerm, getProofTerm,

8− updateSolved, updateSolvedTerm,

8+ updateSolved, updateSolvedTerm, updateSolvedTerm',

99 bound_in, bound_in_term, refocus,

1010 Hole, RunTactic',

1111 goal, atHole) where

@@ -124,13 +124,15 @@ hole (Guess _ _) = True

124124hole _ = False

125125

126126updateSolvedTerm :: [(Name, Term)] -> Term -> Term

127−updateSolvedTerm [] x = x

128−updateSolvedTerm xs x = -- updateSolved' xs x where

127+updateSolvedTerm xs x = fst $ updateSolvedTerm' xs x

128+

129+updateSolvedTerm' [] x = (x, False)

130+updateSolvedTerm' xs x = -- updateSolved' xs x where

129131-- This version below saves allocations, because it doesn't need to reallocate

130132-- the term if there are no updates to do.

131133-- The Bool is ugly, and probably 'Maybe' would be less ugly, but >>= is

132134-- the wrong combinator. Feel free to tidy up as long as it's still as cheap :).

133− fst $ updateSolved' xs x where

135+ updateSolved' xs x where

134136 updateSolved' [] x = (x, False)

135137 updateSolved' xs (Bind n (Hole ty) t)

136138 | Just v <- lookup n xs

src/Idris/Core/Unify.hs+15−9

@@ -29,11 +29,13 @@ data FailContext = FailContext { fail_sourceloc :: FC,

2929 deriving (Eq, Show)

3030

3131type Injs = [(TT Name, TT Name, TT Name)]

32−type Fails = [(TT Name, TT Name, Env, Err, [FailContext], FailAt)]

32+type Fails = [(TT Name, TT Name, -- unification error

33+ Bool, -- ready to retry yet

34+ Env, Err, [FailContext], FailAt)]

3335

3436unrecoverable :: Fails -> Bool

3537unrecoverable = any bad

36− where bad (_,_,_, err, _, _) = unrec err

38+ where bad (_,_,_,_, err, _, _) = unrec err

3739

3840 unrec (CantUnify r _ _ _ _ _) = not r

3941 unrec (At _ e) = unrec e

@@ -129,7 +131,7 @@ match_unify ctxt env topx topy inj holes from =

129131 let err = cantUnify from r

130132 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

131133 if (not r) then lift $ tfail err

132− else do put (UI s ((x, y, env, err, from, Match) : f))

134+ else do put (UI s ((x, y, True, env, err, from, Match) : f))

133135 lift $ tfail err

134136

135137

@@ -144,7 +146,9 @@ match_unify ctxt env topx topy inj holes from =

144146 let err = cantUnify from r topx topy

145147 (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)

146148 (errEnv env) s

147− put (UI s ((binderTy x, binderTy y, env, err, from, Match) : f))

149+ put (UI s ((binderTy x, binderTy y,

150+ False,

151+ env, err, from, Match) : f))

148152 return []

149153

150154 notHole (Hole _) = False

@@ -162,7 +166,7 @@ match_unify ctxt env topx topy inj holes from =

162166 (normalise ctxt env y)

163167 let err = cantUnify from r

164168 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

165− put (UI s ((x, y, env, err, from, Match) : f))

169+ put (UI s ((x, y, True, env, err, from, Match) : f))

166170 lift $ tfail err

167171 combine bnames as [] = return as

168172 combine bnames as ((n, t) : bs)

@@ -446,7 +450,7 @@ unify ctxt env topx topy inj holes usersupp from =

446450 let err = cantUnify from r

447451 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

448452 if (not r) then lift $ tfail err

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

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

450454 return [] -- lift $ tfail err

451455

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

@@ -540,7 +544,7 @@ unify ctxt env topx topy inj holes usersupp from =

540544 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)

541545 let err = cantUnify from r

542546 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

543− put (UI s ((topx, topy, env, err, from, Unify) : f))

547+ put (UI s ((topx, topy, True, env, err, from, Unify) : f))

544548 return []

545549

546550 -- shortcut failure, if we *know* nothing can fix it

@@ -548,7 +552,7 @@ unify ctxt env topx topy inj holes usersupp from =

548552 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)

549553 let err = cantUnify from r

550554 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

551− put (UI s ((topx, topy, env, err, from, Unify) : f))

555+ put (UI s ((topx, topy, True, env, err, from, Unify) : f))

552556 lift $ tfail err

553557

554558

@@ -572,7 +576,9 @@ unify ctxt env topx topy inj holes usersupp from =

572576 let err = cantUnify from r topx topy

573577 (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)

574578 (errEnv env) s

575− put (UI s ((binderTy x, binderTy y, env, err, from, Unify) : f))

579+ put (UI s ((binderTy x, binderTy y,

580+ False,

581+ env, err, from, Unify) : f))

576582 return [] -- lift $ tfail err

577583

578584 checkCycle ns p@(x, P _ _ _) = return [p]

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

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

573573 inj <- get_inj

574574 return (res, probs, inj))

575575

576− when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_) -> (x,y)) probs)

576+ when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)

577577

578578 let lhs_tm = orderPats (getInferTerm lhs')

579579 let lhs_ty = getInferType lhs'

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

656656 probs <- get_probs

657657 return (tm, ds, is, probs))

658658

659− when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_) -> (x,y)) probs)

659+ when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)

660660

661661 logLvl 5 "DONE CHECK"

662662 logLvl 2 $ "---> " ++ show rhs'

src/Idris/ElabTerm.hs+5−5

@@ -87,9 +87,9 @@ build ist info emode opts fn tm

8787 probs <- get_probs

8888 case probs of

8989 [] -> return ()

90− ((_,_,_,e,_,_):es) -> traceWhen u ("Final problems:\n" ++ show probs) $

91− if inf then return ()

92− else lift (Error e)

90+ ((_,_,_,_,e,_,_):es) -> traceWhen u ("Final problems:\n" ++ show probs) $

91+ if inf then return ()

92+ else lift (Error e)

9393

9494 when tydecl (do update_term orderPats

9595 mkPat)

@@ -128,8 +128,8 @@ buildTC ist info emode opts fn tm

128128 tm <- get_term

129129 case probs of

130130 [] -> return ()

131− ((_,_,_,e,_,_):es) -> if inf then return ()

132− else lift (Error e)

131+ ((_,_,_,_,e,_,_):es) -> if inf then return ()

132+ else lift (Error e)

133133 is <- getAux

134134 tt <- get_term

135135 let (tm, ds) = runState (collectDeferred (Just fn) tt) []

src/Idris/Prover.hs+1−1

@@ -111,7 +111,7 @@ elabStep st e = case runStateT eCheck st of

111111 ctxt <- get_context

112112 lift $ check ctxt [] (forget tm)

113113 return res

114− ((_,_,_,e,_,_):_) -> lift $ Error e

114+ ((_,_,_,_,e,_,_):_) -> lift $ Error e

115115

116116dumpState :: IState -> ProofState -> Idris ()

117117dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) =