fa364ca · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Check for cyclic solutions in unification

fa364caEdwin Brady13 years ago

src/Idris/Core/ProofState.hs+9

compare with master

unifiedsplit

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

190 traceWhen (unifylog ps)

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

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

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

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

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

194-- ++ show (pterm ps)

195-- ++ show (pterm ps)

195 ++ "\n----------") $

196 ++ "\n----------") $

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

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

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

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

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

763

764

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+

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

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

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

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

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

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

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

810 return (ps { pterm = tm',

816 return (ps { pterm = tm',

811 unified = (h, []),

817 unified = (h, []),

812 problems = probs',

818 problems = probs',

819+ notunified = updateNotunified ns (notunified ps),

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

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

814processTactic (Reorder n) ps

821processTactic (Reorder n) ps

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

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

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

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

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

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

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

826 previous = Just ps, plog = "",

833 previous = Just ps, plog = "",

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

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

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

828processTactic MatchProblems ps

836processTactic MatchProblems ps

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

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

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

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

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

852 solved = Nothing,

860 solved = Nothing,

853 problems = probs',

861 problems = probs',

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

854 previous = Just ps, plog = "",

863 previous = Just ps, plog = "",

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

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

856

865

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

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

35 TC [(Name, TT Name)]

36match_unify ctxt env topx topy dont holes =

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

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

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

39 res ->

40 let topxn = normalise ctxt env topx

41 topyn = normalise ctxt env topy in

42 case runStateT (un [] topxn topyn)

43 (UI 0 []) of

44 OK (v, UI _ fails) ->

45− return (filter notTrivial v)

45+ return (trimSolutions v)

46 Error e ->

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

48 case runStateT (un [] topxn topy)

49 (UI 0 []) of

50 OK (v, UI _ fails) ->

51− return (filter notTrivial v)

51+ return (trimSolutions v)

52 _ -> tfail e

53 where

54 un names (P _ x _) tm

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

128 where inst [] tm = tm

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

130

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

131+trimSolutions ns = dropPairs ns

132−notTrivial _ = True

132+ where dropPairs [] = []

133−

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+

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

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

135 where

143 where

136 doSubst [] tm = tm

144 doSubst [] tm = tm

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

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

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

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

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

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

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

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

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

150 [])

158 [])

151 res ->

159 res ->

152 let topxn = normalise ctxt env topx

160 let topxn = normalise ctxt env topx

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

155 case runStateT (un False [] topxn topyn)

163 case runStateT (un False [] topxn topyn)

156 (UI 0 []) of

164 (UI 0 []) of

157 OK (v, UI _ fails) ->

165 OK (v, UI _ fails) ->

158− return (filter notTrivial v, reverse fails)

166+ return (trimSolutions v, reverse fails)

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

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

160 Error e -> tfail e

168 Error e -> tfail e

161 where

169 where