@@ -71,7 +71,7 @@ split n t'
7171 logLvl 3 ("Split:\n" ++
7272 (showSep "\n" (map show (mapMaybe id newPats))))
7373 logLvl 3 "----"
74− let newPats' = mergeAllPats ctxt t (mapMaybe id newPats)
74+ let newPats' = mergeAllPats ist n t (mapMaybe id newPats)
7575 iLOG ("Name updates " ++ showSep "\n"
7676 (map (\ (p, u) -> show u ++ " " ++ show p) newPats'))
7777 return (map snd newPats')
@@ -84,47 +84,55 @@ data MergeState = MS { namemap :: [(Name, Name)],
8484addUpdate n tm = do ms <- get
8585 put (ms { updates = ((n, stripNS tm) : updates ms) } )
8686
87−inventName n =
87+inventName ist ty n =
8888 do ms <- get
89+ let supp = case ty of
90+ Nothing -> []
91+ Just t -> getNameHints ist t
92+ let nsupp = case n of
93+ MN i ('_':_) -> mkSupply (supp ++ varlist)
94+ MN i n -> mkSupply (UN n : supp ++ varlist)
95+ x -> mkSupply (x : supp)
8996 let badnames = map snd (namemap ms) ++ map snd (invented ms) ++
9097 explicit ms
9198 case lookup n (invented ms) of
9299 Just n' -> return n'
93100 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
101+ do let n' = uniqueNameFrom nsupp badnames
99102 put (ms { invented = (n, n') : invented ms })
100103 return n'
104+
105+mkSupply ns = mkSupply' ns (map nextName ns)
106+ where mkSupply' xs ns' = xs ++ mkSupply ns'
107+
108+varlist = map (UN . (:[])) "xyzwstuv" -- EB's personal preference :)
101109
102110stripNS tm = mapPT dens tm where
103111 dens (PRef fc n) = PRef fc (nsroot n)
104112 dens t = t
105113
106−mergeAllPats :: Context -> PTerm -> [PTerm] -> [(PTerm, [(Name, PTerm)])]
107−mergeAllPats ctxt t [] = []
108−mergeAllPats ctxt t (p : ps)
109− = let (p', MS _ _ _ u) = runState (mergePat ctxt t p)
110− (MS [] [] (patvars t) [])
111− ps' = mergeAllPats ctxt t ps in
114+mergeAllPats :: IState -> Name -> PTerm -> [PTerm] -> [(PTerm, [(Name, PTerm)])]
115+mergeAllPats ist cv t [] = []
116+mergeAllPats ist cv t (p : ps)
117+ = let (p', MS _ _ _ u) = runState (mergePat ist t p Nothing)
118+ (MS [] [] (filter (/=cv) (patvars t)) [])
119+ ps' = mergeAllPats ist cv t ps in
112120 ((p, u) : ps')
113121 where patvars (PRef _ n) = [n]
114122 patvars (PApp _ _ as) = concatMap (patvars . getTm) as
115123 patvars (PPatvar _ n) = [n]
116124 patvars _ = []
117125
118−mergePat :: Context -> PTerm -> PTerm -> State MergeState PTerm
126+mergePat :: IState -> PTerm -> PTerm -> Maybe Name -> State MergeState PTerm
119127-- If any names are unified, make sure they stay unified. Always prefer
120128-- user provided name (first pattern)
121−mergePat ctxt (PPatvar fc n) new
122− = mergePat ctxt (PRef fc n) new
123−mergePat ctxt old (PPatvar fc n)
124− = mergePat ctxt old (PRef fc n)
125−mergePat ctxt orig@(PRef fc n) new@(PRef _ n')
126− | isDConName n' ctxt = do addUpdate n new;
127− return new
129+mergePat ist (PPatvar fc n) new t
130+ = mergePat ist (PRef fc n) new t
131+mergePat ist old (PPatvar fc n) t
132+ = mergePat ist old (PRef fc n) t
133+mergePat ist orig@(PRef fc n) new@(PRef _ n') t
134+ | isDConName n' (tt_ctxt ist) = do addUpdate n new
135+ return new
128136 | otherwise
129137 = do ms <- get
130138 case lookup n' (namemap ms) of
@@ -132,37 +140,49 @@ mergePat ctxt orig@(PRef fc n) new@(PRef _ n')
132140 return (PRef fc x)
133141 Nothing -> do put (ms { namemap = ((n', n) : namemap ms) })
134142 return (PRef fc n)
135−mergePat ctxt (PApp _ _ args) (PApp fc f args')
136− = do newArgs <- zipWithM mergeArg args args'
143+mergePat ist (PApp _ _ args) (PApp fc f args') t
144+ = do newArgs <- zipWithM mergeArg args (zip args' (argTys ist f))
137145 return (PApp fc f newArgs)
138− where mergeArg x y = do tm' <- mergePat ctxt (getTm x) (getTm y)
139− case x of
140− (PImp _ _ _ _ _ _) ->
141− return (y { machine_inf = machine_inf x,
142− getTm = tm' })
143− _ -> return (y { getTm = tm' })
144−mergePat ctxt (PRef fc n) t = do tm <- tidy t
145− addUpdate n tm
146− return tm
147−mergePat ctxt x y = return y
146+ where mergeArg x (y, t)
147+ = do tm' <- mergePat ist (getTm x) (getTm y) t
148+ case x of
149+ (PImp _ _ _ _ _ _) ->
150+ return (y { machine_inf = machine_inf x,
151+ getTm = tm' })
152+ _ -> return (y { getTm = tm' })
153+mergePat ist (PRef fc n) tm ty = do tm <- tidy ist tm ty
154+ addUpdate n tm
155+ return tm
156+mergePat ist x y t = return y
148157
149158mergeUserImpl :: PTerm -> PTerm -> PTerm
150159mergeUserImpl x y = x
151160
152−tidy orig@(PRef fc n)
161+argTys :: IState -> PTerm -> [Maybe Name]
162+argTys ist (PRef fc n)
163+ = case lookupTy n (tt_ctxt ist) of
164+ [ty] -> map (tyName . snd) (getArgTys ty) ++ repeat Nothing
165+ _ -> repeat Nothing
166+ where tyName (Bind _ (Pi _) _) = Just (UN "->")
167+ tyName t | (P _ n _, _) <- unApply t = Just n
168+ | otherwise = Nothing
169+argTys _ _ = repeat Nothing
170+
171+tidy :: IState -> PTerm -> Maybe Name -> State MergeState PTerm
172+tidy ist orig@(PRef fc n) ty
153173 = do ms <- get
154174 case lookup n (namemap ms) of
155175 Just x -> return (PRef fc x)
156176 Nothing -> case n of
157177 (UN _) -> return orig
158− _ -> do n' <- inventName n
178+ _ -> do n' <- inventName ist ty n
159179 return (PRef fc n')
160−tidy (PApp fc f args)
161− = do args' <- mapM tidyArg args
180+tidy ist (PApp fc f args) ty
181+ = do args' <- zipWithM tidyArg args (argTys ist f)
162182 return (PApp fc f args')
163− where tidyArg x = do tm' <- tidy (getTm x)
164− return (x { getTm = tm' })
165−tidy tm = return tm
183+ where tidyArg x ty' = do tm' <- tidy ist (getTm x) ty'
184+ return (x { getTm = tm' })
185+tidy ist tm ty = return tm
166186
167187
168188-- mapPT tidyVar tm
@@ -291,15 +311,26 @@ getClause :: Int -- ^ line number that the type is declared on
291311 -> FilePath -- ^ Source file name
292312 -> Idris String
293313getClause l fn fp = do ty <- getInternalApp fp l
294− let ap = mkApp ty [1..]
314+ ist <- get
315+ let ap = mkApp ist ty []
295316 return (show fn ++ " " ++ ap ++
296317 "= ?" ++ show fn ++ "_rhs")
297− where mkApp (PPi (Exp _ _ _ False) (MN _ _) _ sc) (n : ns)
298− = "x" ++ show n ++ " " ++ mkApp sc ns
299− mkApp (PPi (Exp _ _ _ False) n _ sc) ns
300− = show n ++ " " ++ mkApp sc ns
301− mkApp (PPi _ _ _ sc) ns = mkApp sc ns
302− mkApp _ _ = ""
318+ where mkApp i (PPi (Exp _ _ _ False) (MN _ _) ty sc) used
319+ = let n = getNameFrom i used ty in
320+ show n ++ " " ++ mkApp i sc (n : used)
321+ mkApp i (PPi (Exp _ _ _ False) n _ sc) used
322+ = show n ++ " " ++ mkApp i sc (n : used)
323+ mkApp i (PPi _ _ _ sc) used = mkApp i sc used
324+ mkApp i _ _ = ""
325+
326+ getNameFrom i used (PPi _ _ _ _)
327+ = uniqueNameFrom (mkSupply [UN "f", UN "g"]) used
328+ getNameFrom i used (PApp fc f as) = getNameFrom i used f
329+ getNameFrom i used (PRef fc f)
330+ = case getNameHints i f of
331+ [] -> uniqueName (UN "x") used
332+ ns -> uniqueNameFrom (mkSupply ns) used
333+ getNameFrom i used _ = uniqueName (UN "x") used
303334
304335getProofClause :: Int -- ^ line number that the type is declared
305336 -> Name -- ^ Function name
@@ -326,4 +357,3 @@ mkWith str n = let str' = replaceRHS str "with (_)"
326357 | not ('=' `elem` rest) = str
327358 replaceRHS (x : rest) str = x : replaceRHS rest str
328359
329−