9330832 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Deal with unique types in 'do' better

9330832Edwin Brady12 years ago

src/Idris/ElabTerm.hs+14−3

@@ -868,9 +868,13 @@ elab ist info emode opts fn tm

868 envU <- mapM (getKind args) args

869 let namesUsedInRHS = nub $ scvn : concatMap (\(_,rhs) -> allNamesIn rhs) opts

870

871− -- Drop the unique arguments used in the scrutinee (since it's

871+ -- Drop the unique arguments used in the term already

872+ -- and in the scrutinee (since it's

872− -- not valid to use them again anyway)

873+ -- not valid to use them again anyway)

874+ ptm <- get_term

873− let argsDropped = filter (isUnique envU) (nub $ allNamesIn scr)

875+ let argsDropped = filter (isUnique envU)

876+ (nub $ allNamesIn scr ++ inApp ptm)

877+

874 let args' = filter (\(n, _) -> n `notElem` argsDropped) args

878 let args' = filter (\(n, _) -> n `notElem` argsDropped) args

875

879

876 cname <- unique_hole' True (mkCaseName fn)

880 cname <- unique_hole' True (mkCaseName fn)

@@ -897,6 +901,13 @@ elab ist info emode opts fn tm

897 Just xs@(_:_) -> sNS n xs

901 Just xs@(_:_) -> sNS n xs

898 _ -> n

902 _ -> n

899

903

904+ inApp (P _ n _) = [n]

905+ inApp (App f a) = inApp f ++ inApp a

906+ inApp (Bind n (Let _ v) sc) = inApp v ++ inApp sc

907+ inApp (Bind n (Guess _ v) sc) = inApp v ++ inApp sc

908+ inApp (Bind n b sc) = inApp sc

909+ inApp _ = []

910+

900 isUnique envk n = case lookup n envk of

911 isUnique envk n = case lookup n envk of

901 Just u -> u

912 Just u -> u

902 _ -> False

913 _ -> False