fa364ca · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Check for cyclic solutions in unification

Fixes #602

commitfa364ca3c7cedb4aef1eba45b3d937179f0da7ee authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 9 Jan 2014, 18:05 (13 years ago) parentfef1207

2 files changed+25−8

compare with master

unifiedsplit

src/Idris/Core/ProofState.hs+9 src/Idris/Core/Unify.hs+16−8

src/Idris/Core/ProofState.hs+9

@@ -190,6 +190,7 @@ unify' ctxt env topx topy =

190190 traceWhen (unifylog ps)

191191 ("Unified " ++ show (topx, topy) ++ " without " ++ show dont ++

192192 "\nSolved: " ++ show u ++ "\nNew problems: " ++ qshow fails

193+ ++ "\nNot unified:\n" ++ show (notunified ps)

193194 ++ "\nCurrent problems:\n" ++ qshow (problems ps)

194195-- ++ show (pterm ps)

195196 ++ "\n----------") $

@@ -761,6 +762,11 @@ solveInProblems x val ((l, r, env, err) : ps)

761762 = ((instantiate val (pToV x l), instantiate val (pToV x r),

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

763764

765+updateNotunified ns nu = up nu where

766+ up [] = []

767+ up ((n, t) : ns) = let t' = updateSolved ns t in

768+ ((n, t') : up ns)

769+

764770updateProblems ctxt ns ps inj holes = up ns ps where

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

766772 up ns ((x, y, env, err) : ps) =

@@ -810,6 +816,7 @@ processTactic EndUnify ps

810816 return (ps { pterm = tm',

811817 unified = (h, []),

812818 problems = probs',

819+ notunified = updateNotunified ns (notunified ps),

813820 holes = holes ps \\ map fst ns'' }, "")

814821processTactic (Reorder n) ps

815822 = do ps' <- execStateT (tactic (Just n) reorder_claims) ps

@@ -824,6 +831,7 @@ processTactic UnifyProblems ps

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

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

826833 previous = Just ps, plog = "",

834+ notunified = updateNotunified ns' (notunified ps),

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

828836processTactic MatchProblems ps

829837 = let (ns', probs') = matchProblems (context ps)

@@ -851,6 +859,7 @@ processTactic t ps

851859 return (ps' { pterm = pterm'',

852860 solved = Nothing,

853861 problems = probs',

862+ notunified = updateNotunified ns' (notunified ps'),

854863 previous = Just ps, plog = "",

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

856865

src/Idris/Core/Unify.hs+16−8

@@ -35,20 +35,20 @@ match_unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] ->

3535 TC [(Name, TT Name)]

3636match_unify ctxt env topx topy dont holes =

3737 case runStateT (un [] topx topy) (UI 0 []) of

38− OK (v, UI _ []) -> return (filter notTrivial v)

38+ OK (v, UI _ []) -> return (trimSolutions v)

3939 res ->

4040 let topxn = normalise ctxt env topx

4141 topyn = normalise ctxt env topy in

4242 case runStateT (un [] topxn topyn)

4343 (UI 0 []) of

4444 OK (v, UI _ fails) ->

45− return (filter notTrivial v)

45+ return (trimSolutions v)

4646 Error e ->

4747 -- just normalise the term we're matching against

4848 case runStateT (un [] topxn topy)

4949 (UI 0 []) of

5050 OK (v, UI _ fails) ->

51− return (filter notTrivial v)

51+ return (trimSolutions v)

5252 _ -> tfail e

5353 where

5454 un names (P _ x _) tm

@@ -128,9 +128,17 @@ match_unify ctxt env topx topy dont holes =

128128 where inst [] tm = tm

129129 inst ((n, _) : ns) tm = inst ns (substV (P Bound n Erased) tm)

130130

131−notTrivial (x, P _ x' _) = x /= x'

132−notTrivial _ = True

133−

131+trimSolutions ns = dropPairs ns

132+ where dropPairs [] = []

133+ dropPairs (n@(x, P _ x' _) : ns)

134+ | x == x' = dropPairs ns

135+ | otherwise

136+ = n : dropPairs

137+ (filter (\t -> case t of

138+ (n, P _ n' _) -> not (n == x' && n' == x)

139+ _ -> True) ns)

140+ dropPairs (n : ns) = n : dropPairs ns

141+

134142expandLets env (x, tm) = (x, doSubst (reverse env) tm)

135143 where

136144 doSubst [] tm = tm

@@ -146,7 +154,7 @@ unify ctxt env topx topy dont holes =

146154-- trace ("Unifying " ++ show (topx, topy)) $

147155 -- don't bother if topx and topy are different at the head

148156 case runStateT (un False [] topx topy) (UI 0 []) of

149− OK (v, UI _ []) -> return (filter notTrivial v,

157+ OK (v, UI _ []) -> return (trimSolutions v,

150158 [])

151159 res ->

152160 let topxn = normalise ctxt env topx

@@ -155,7 +163,7 @@ unify ctxt env topx topy dont holes =

155163 case runStateT (un False [] topxn topyn)

156164 (UI 0 []) of

157165 OK (v, UI _ fails) ->

158− return (filter notTrivial v, reverse fails)

166+ return (trimSolutions v, reverse fails)

159167-- Error e@(CantUnify False _ _ _ _ _) -> tfail e

160168 Error e -> tfail e

161169 where