on master help sign in
fromInteger tweak

If an integer is applied to something, it's certainly an application of fromInteger rather than a constant. This can be useful for some generic programming trickery.

commitfd80612efc2609b466111ebef1858511792faf74 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 8 Jul 2015, 13:20 (11 years ago) parent62bb361
1 file changed+14−1
src/Idris/ParseExpr.hs+14−1
src/Idris/ParseExpr.hs+14−1
@@ -576,8 +576,21 @@ app syn = do f <- simpleExpr syn
576576 args <- many (do notEndApp; arg syn)
577577 case args of
578578 [] -> return f
579− _ -> return (PApp fc f args))
579+ _ -> return (flattenFromInt fc f args))
580580 <?> "function application"
581+ where
582+ -- bit of a hack to deal with the situation where we're applying a
583+ -- literal to an argument, which we may want for obscure applications
584+ -- of fromInteger, and this will help disambiguate better.
585+ -- We know, at least, it won't be one of the constants!
586+ flattenFromInt fc (PAlternative x alts) args
587+ | Just i <- getFromInt alts
588+ = PApp fc (PRef fc (sUN "fromInteger")) (i : args)
589+ flattenFromInt fc f args = PApp fc f args
590+
591+ getFromInt ((PApp _ (PRef _ n) [a]) : _) | n == sUN "fromInteger" = Just a
592+ getFromInt (_ : xs) = getFromInt xs
593+ getFromInt _ = Nothing
581594
582595{-| Parses a function argument
583596@