2e170bf · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Remove dubious matching rule

2e170bfEdwin Brady11 years ago

src/Idris/Core/ProofState.hs+5−2

compare with master

unifiedsplit

@@ -1022,13 +1022,16 @@ processTactic UnifyProblems ps

1022processTactic (MatchProblems all) ps

1023 = do let (ns', probs') = matchProblems all ps [] (problems ps)

1024 (ns'', probs'') = matchProblems all ps ns' probs'

1025− pterm' = updateSolved ns'' (pterm ps)

1025+ pterm' = orderUpdateSolved ns'' (resetProofTerm (pterm ps))

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

1026+ traceWhen (unifylog ps) ("(MatchProblems) Dropping holes: " ++ show ns'') $

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

1028 previous = Just ps, plog = "",

1029 notunified = updateNotunified ns'' (notunified ps),

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

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

1032+ where

1033+ orderUpdateSolved [] t = t

1034+ orderUpdateSolved (n : ns) t = orderUpdateSolved ns (updateSolved [n] t)

1032processTactic t ps

1035processTactic t ps

1033 = case holes ps of

1036 = case holes ps of

1034 [] -> case t of

1037 [] -> case t of

src/Idris/Core/ProofTerm.hs+4

@@ -6,6 +6,7 @@ evaluation/checking inside the proof system, etc.

6-}

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

9+ resetProofTerm,

9 updateSolved, updateSolvedTerm, updateSolvedTerm',

10 updateSolved, updateSolvedTerm, updateSolvedTerm',

10 bound_in, bound_in_term, refocus, updsubst,

11 bound_in, bound_in_term, refocus, updsubst,

11 Hole, RunTactic',

12 Hole, RunTactic',

@@ -129,6 +130,9 @@ mkProofTerm tm = PT Top [] tm []

129getProofTerm :: ProofTerm -> Term

130getProofTerm :: ProofTerm -> Term

130getProofTerm (PT path _ sub ups) = rebuildTerm sub (updateSolvedPath ups path)

131getProofTerm (PT path _ sub ups) = rebuildTerm sub (updateSolvedPath ups path)

131

132

133+resetProofTerm :: ProofTerm -> ProofTerm

134+resetProofTerm = mkProofTerm . getProofTerm

135+

132same :: Eq a => Maybe a -> a -> Bool

136same :: Eq a => Maybe a -> a -> Bool

133same Nothing n = True

137same Nothing n = True

134same (Just x) n = x == n

138same (Just x) n = x == n

src/Idris/Core/Unify.hs−25

@@ -92,31 +92,6 @@ match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =

92 StateT UInfo

93 TC [(Name, TT Name)]

95− -- This rule is highly dubious... it certainly produces a valid answer

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)

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

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)

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

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

116− holeIn env f || f `elem` holes

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

118− checkCycle names (f, Bind n' (Lam t) x)

119−

120 un names tx@(P _ x _) tm

95 un names tx@(P _ x _) tm

121 | tx /= tm && holeIn env x || x `elem` holes

96 | tx /= tm && holeIn env x || x `elem` holes

122 = do sc 1; checkCycle names (x, tm)

97 = do sc 1; checkCycle names (x, tm)