git.iko.soy/Idris-dev
on master help sign in
Invent names when case splitting
96234a3Edwin Brady
libs/prelude/Prelude/Vect.idr+1−1
compare with master
unifiedsplit
@@ -13,7 +13,7 @@ infixr 7 ::
13
13
14%elim data Vect : Nat -> Type -> Type where
14%elim data Vect : Nat -> Type -> Type where
15 Nil : Vect Z a
15 Nil : Vect Z a
16− (::) : a -> Vect n a -> Vect (S n) a
16+ (::) : (x : a) -> (xs : Vect n a) -> Vect (S n) a
17
17
18--------------------------------------------------------------------------------
18--------------------------------------------------------------------------------
19-- Indexing into vectors
19-- Indexing into vectors
src/Idris/CaseSplit.hs+28−9
@@ -77,11 +77,28 @@ split n t'
77 return (map snd newPats')
77 return (map snd newPats')
78
78
79data MergeState = MS { namemap :: [(Name, Name)],
79data MergeState = MS { namemap :: [(Name, Name)],
80+ invented :: [(Name, Name)],
81+ explicit :: [Name],
80 updates :: [(Name, PTerm)] }
82 updates :: [(Name, PTerm)] }
81
83
82addUpdate n tm = do ms <- get
84addUpdate n tm = do ms <- get
83 put (ms { updates = ((n, stripNS tm) : updates ms) } )
85 put (ms { updates = ((n, stripNS tm) : updates ms) } )
84
86
87+inventName n =
88+ do ms <- get
89+ let badnames = map snd (namemap ms) ++ map snd (invented ms) ++
90+ explicit ms
91+ case lookup n (invented ms) of
92+ Just n' -> return n'
93+ Nothing ->
94+ do let n' = case n of
95+ MN i ('_':_) ->
96+ uniqueName (UN "var") badnames
97+ MN i n -> uniqueName (UN n) badnames
98+ x -> x
99+ put (ms { invented = (n, n') : invented ms })
100+ return n'
101+
85stripNS tm = mapPT dens tm where
102stripNS tm = mapPT dens tm where
86 dens (PRef fc n) = PRef fc (nsroot n)
103 dens (PRef fc n) = PRef fc (nsroot n)
87 dens t = t
104 dens t = t
@@ -89,9 +106,14 @@ stripNS tm = mapPT dens tm where
89mergeAllPats :: Context -> PTerm -> [PTerm] -> [(PTerm, [(Name, PTerm)])]
106mergeAllPats :: Context -> PTerm -> [PTerm] -> [(PTerm, [(Name, PTerm)])]
90mergeAllPats ctxt t [] = []
107mergeAllPats ctxt t [] = []
91mergeAllPats ctxt t (p : ps)
108mergeAllPats ctxt t (p : ps)
92− = let (p', MS _ u) = runState (mergePat ctxt t p) (MS [] [])
109+ = let (p', MS _ _ _ u) = runState (mergePat ctxt t p)
110+ (MS [] [] (patvars t) [])
93 ps' = mergeAllPats ctxt t ps in
111 ps' = mergeAllPats ctxt t ps in
94 ((p, u) : ps')
112 ((p, u) : ps')
113+ where patvars (PRef _ n) = [n]
114+ patvars (PApp _ _ as) = concatMap (patvars . getTm) as
115+ patvars (PPatvar _ n) = [n]
116+ patvars _ = []
95
117
96mergePat :: Context -> PTerm -> PTerm -> State MergeState PTerm
118mergePat :: Context -> PTerm -> PTerm -> State MergeState PTerm
97-- If any names are unified, make sure they stay unified. Always prefer
119-- If any names are unified, make sure they stay unified. Always prefer
@@ -133,7 +155,8 @@ tidy orig@(PRef fc n)
133 Just x -> return (PRef fc x)
155 Just x -> return (PRef fc x)
134 Nothing -> case n of
156 Nothing -> case n of
135 (UN _) -> return orig
157 (UN _) -> return orig
136− _ -> return Placeholder
158+ _ -> do n' <- inventName n
159+ return (PRef fc n')
137tidy (PApp fc f args)
160tidy (PApp fc f args)
138 = do args' <- mapM tidyArg args
161 = do args' <- mapM tidyArg args
139 return (PApp fc f args')
162 return (PApp fc f args')
@@ -292,16 +315,12 @@ getProofClause l fn fp
292-- match clause
315-- match clause
293
316
294mkWith :: String -> Name -> String
317mkWith :: String -> Name -> String
295−mkWith str n = let ind = getIndent str
296− str' = replicate ind ' ' ++
297− replaceRHS str "with (_)"
318+mkWith str n = let str' = replaceRHS str "with (_)"
298− newpat = replicate (ind + 2) ' ' ++
319+ newpat = " " ++
299 replaceRHS str "| with_pat = ?" ++ show n ++ "_rhs" in
320 replaceRHS str "| with_pat = ?" ++ show n ++ "_rhs" in
300 str' ++ "\n" ++ newpat
321 str' ++ "\n" ++ newpat
301
322
302− where getIndent s = length (takeWhile isSpace s)
303−
304− replaceRHS [] str = str
323+ where replaceRHS [] str = str
305 replaceRHS ('?':'=': rest) str = str
324 replaceRHS ('?':'=': rest) str = str
306 replaceRHS ('=': rest) str
325 replaceRHS ('=': rest) str
307 | not ('=' `elem` rest) = str
326 | not ('=' `elem` rest) = str
test/test032/expected+3−3
@@ -1,8 +1,8 @@
1Type checking ./test032.idr
1Type checking ./test032.idr
2isElem x [] = ?isElem_rhs_1
2isElem x [] = ?isElem_rhs_1
3−isElem x (_ :: _) = ?isElem_rhs_3
3+isElem x (t :: t1) = ?isElem_rhs_3
4
4
5− localZipWith f (_ :: _) (_ :: _) = ?localZipWith_rhs_1
5+ localZipWith f (_ :: _) (x :: xs1) = ?localZipWith_rhs_1
6
6
7f x :: (map f xs)
7f x :: (map f xs)
8isElem2 x (y :: ys) with (_)
8isElem2 x (y :: ys) with (_)
@@ -10,5 +10,5 @@ isElem2 x (y :: ys) with (_)
10 isElem3 x (x :: ys) | (Yes refl) = ?isElem3_rhs_3
10 isElem3 x (x :: ys) | (Yes refl) = ?isElem3_rhs_3
11
11
12 [] => ?bar_1
12 [] => ?bar_1
13− (_ :: _) => ?bar_2
13+ (t :: t1) => ?bar_2
14
14