git.iko.soy/Idris-dev
on master help sign in
Fix name unification in interactive case split
6c51f87Edwin Brady
libs/base/Data/Nat/Views.idr+1−1
compare with master
unifiedsplit
@@ -7,7 +7,7 @@ data Half : Nat -> Type where
7
7
8public export
8public export
9data HalfRec : Nat -> Type where
9data HalfRec : Nat -> Type where
10− HalfRecZ : HalfRec 0
10+ HalfRecZ : HalfRec Z
11 HalfRecEven : Lazy (HalfRec n) -> HalfRec (n + n)
11 HalfRecEven : Lazy (HalfRec n) -> HalfRec (n + n)
12 HalfRecOdd : Lazy (HalfRec n) -> HalfRec (S (n + n))
12 HalfRecOdd : Lazy (HalfRec n) -> HalfRec (S (n + n))
13
13
src/Idris/CaseSplit.hs+23−11
@@ -157,13 +157,25 @@ mergeAllPats ist cv t (p : ps)
157 patvars _ = []
157 patvars _ = []
158
158
159mergePat :: IState -> PTerm -> PTerm -> Maybe Name -> State MergeState PTerm
159mergePat :: IState -> PTerm -> PTerm -> Maybe Name -> State MergeState PTerm
160+mergePat ist orig new t =
161+ do -- collect user names for name map, by matching user pattern against
162+ -- the generated pattern
163+ case matchClause ist orig new of
164+ Left _ -> return ()
165+ Right ns -> mapM_ addNameMap ns
166+ mergePat' ist orig new t
167+ where
168+ addNameMap (n, PRef fc _ n') = do ms <- get
169+ put (ms { namemap = ((n', n) : namemap ms) })
170+ addNameMap _ = return ()
171+
160-- If any names are unified, make sure they stay unified. Always prefer
172-- If any names are unified, make sure they stay unified. Always prefer
161-- user provided name (first pattern)
173-- user provided name (first pattern)
162−mergePat ist (PPatvar fc n) new t
174+mergePat' ist (PPatvar fc n) new t
163− = mergePat ist (PRef fc [] n) new t
175+ = mergePat' ist (PRef fc [] n) new t
164−mergePat ist old (PPatvar fc n) t
176+mergePat' ist old (PPatvar fc n) t
165− = mergePat ist old (PRef fc [] n) t
177+ = mergePat' ist old (PRef fc [] n) t
166−mergePat ist orig@(PRef fc _ n) new@(PRef _ _ n') t
178+mergePat' ist orig@(PRef fc _ n) new@(PRef _ _ n') t
167 | isDConName n' (tt_ctxt ist) = do addUpdate n new
179 | isDConName n' (tt_ctxt ist) = do addUpdate n new
168 return new
180 return new
169 | otherwise
181 | otherwise
@@ -173,20 +185,20 @@ mergePat ist orig@(PRef fc _ n) new@(PRef _ _ n') t
173 return (PRef fc [] x)
185 return (PRef fc [] x)
174 Nothing -> do put (ms { namemap = ((n', n) : namemap ms) })
186 Nothing -> do put (ms { namemap = ((n', n) : namemap ms) })
175 return (PRef fc [] n)
187 return (PRef fc [] n)
176−mergePat ist (PApp _ _ args) (PApp fc f args') t
188+mergePat' ist (PApp _ _ args) (PApp fc f args') t
177 = do newArgs <- zipWithM mergeArg args (zip args' (argTys ist f))
189 = do newArgs <- zipWithM mergeArg args (zip args' (argTys ist f))
178 return (PApp fc f newArgs)
190 return (PApp fc f newArgs)
179 where mergeArg x (y, t)
191 where mergeArg x (y, t)
180− = do tm' <- mergePat ist (getTm x) (getTm y) t
192+ = do tm' <- mergePat' ist (getTm x) (getTm y) t
181 case x of
193 case x of
182 (PImp _ _ _ _ _) ->
194 (PImp _ _ _ _ _) ->
183 return (y { machine_inf = machine_inf x,
195 return (y { machine_inf = machine_inf x,
184 getTm = tm' })
196 getTm = tm' })
185 _ -> return (y { getTm = tm' })
197 _ -> return (y { getTm = tm' })
186−mergePat ist (PRef fc _ n) tm ty = do tm <- tidy ist tm ty
198+mergePat' ist (PRef fc _ n) tm ty = do tm <- tidy ist tm ty
187− addUpdate n tm
199+ addUpdate n tm
188− return tm
200+ return tm
189−mergePat ist x y t = return y
201+mergePat' ist x y t = return y
190
202
191mergeUserImpl :: PTerm -> PTerm -> PTerm
203mergeUserImpl :: PTerm -> PTerm -> PTerm
192mergeUserImpl x y = x
204mergeUserImpl x y = x
test/interactive001/expected+1−1
@@ -7,7 +7,7 @@ f x :: map f xs
7isElem2 x (y :: ys) with (_)
7isElem2 x (y :: ys) with (_)
8 isElem2 x (y :: ys) | with_pat = ?isElem2_rhs
8 isElem2 x (y :: ys) | with_pat = ?isElem2_rhs
9
9
10− isElem3 x (x :: ys) | (Yes Refl) = ?isElem3_rhs_3
10+ isElem3 y (y :: ys) | (Yes Refl) = ?isElem3_rhs_3
11
11
12 [] => ?bar_1
12 [] => ?bar_1
13 (x :: ys) => ?bar_2
13 (x :: ys) => ?bar_2