@@ -77,11 +77,28 @@ split n t'
7777 return (map snd newPats')
7878
7979data MergeState = MS { namemap :: [(Name, Name)],
80+ invented :: [(Name, Name)],
81+ explicit :: [Name],
8082 updates :: [(Name, PTerm)] }
8183
8284addUpdate n tm = do ms <- get
8385 put (ms { updates = ((n, stripNS tm) : updates ms) } )
8486
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+
85102stripNS tm = mapPT dens tm where
86103 dens (PRef fc n) = PRef fc (nsroot n)
87104 dens t = t
@@ -89,9 +106,14 @@ stripNS tm = mapPT dens tm where
89106mergeAllPats :: Context -> PTerm -> [PTerm] -> [(PTerm, [(Name, PTerm)])]
90107mergeAllPats ctxt t [] = []
91108mergeAllPats 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) [])
93111 ps' = mergeAllPats ctxt t ps in
94112 ((p, u) : ps')
113+ where patvars (PRef _ n) = [n]
114+ patvars (PApp _ _ as) = concatMap (patvars . getTm) as
115+ patvars (PPatvar _ n) = [n]
116+ patvars _ = []
95117
96118mergePat :: Context -> PTerm -> PTerm -> State MergeState PTerm
97119-- If any names are unified, make sure they stay unified. Always prefer
@@ -133,7 +155,8 @@ tidy orig@(PRef fc n)
133155 Just x -> return (PRef fc x)
134156 Nothing -> case n of
135157 (UN _) -> return orig
136− _ -> return Placeholder
158+ _ -> do n' <- inventName n
159+ return (PRef fc n')
137160tidy (PApp fc f args)
138161 = do args' <- mapM tidyArg args
139162 return (PApp fc f args')
@@ -292,16 +315,12 @@ getProofClause l fn fp
292315-- match clause
293316
294317mkWith :: String -> Name -> String
295−mkWith str n = let ind = getIndent str
296− str' = replicate ind ' ' ++
297− replaceRHS str "with (_)"
298− newpat = replicate (ind + 2) ' ' ++
318+mkWith str n = let str' = replaceRHS str "with (_)"
319+ newpat = " " ++
299320 replaceRHS str "| with_pat = ?" ++ show n ++ "_rhs" in
300321 str' ++ "\n" ++ newpat
301322
302− where getIndent s = length (takeWhile isSpace s)
303−
304− replaceRHS [] str = str
323+ where replaceRHS [] str = str
305324 replaceRHS ('?':'=': rest) str = str
306325 replaceRHS ('=': rest) str
307326 | not ('=' `elem` rest) = str