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

git.iko.soy/Idris-dev

Remove dubious matching rule

IIRC this was a hack for scoped implicits, but whatever it did isn't tripped up in the tests any more and it's a horrible hack anyway, so off it goes.

commit2e170bfd01fc4c757520b940bd6c1fbcc752e03b authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 1 Sep 2015, 15:17 (11 years ago) parent53ffd07

3 files changed+9−27

compare with master

unifiedsplit

src/Idris/Core/ProofState.hs+5−2 src/Idris/Core/ProofTerm.hs+4 src/Idris/Core/Unify.hs−25

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

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

10221022processTactic (MatchProblems all) ps

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

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

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

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

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

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

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

10281028 previous = Just ps, plog = "",

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

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

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

1032+ where

1033+ orderUpdateSolved [] t = t

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

10321035processTactic t ps

10331036 = case holes ps of

10341037 [] -> case t of

src/Idris/Core/ProofTerm.hs+4

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

66-}

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

9+ resetProofTerm,

910 updateSolved, updateSolvedTerm, updateSolvedTerm',

1011 bound_in, bound_in_term, refocus, updsubst,

1112 Hole, RunTactic',

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

129130getProofTerm :: ProofTerm -> Term

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

131132

133+resetProofTerm :: ProofTerm -> ProofTerm

134+resetProofTerm = mkProofTerm . getProofTerm

135+

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

133137same Nothing n = True

134138same (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 =

9292 StateT UInfo

9393 TC [(Name, TT Name)]

9494

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−

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

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

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