c7bac29 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Extended syntax for 'with' blocks

EXPERIMENTAL: I'm not sure this is a good idea or how it will turn out to affect some other things, but let's see how it works out. This allow calling functions defined by 'with' directly (i.e., the generated auxiliary function) by allowing the additional argument syntax on the right hand side. For example: data SnocList : List a -> Type where Empty : SnocList [] Snoc : SnocList xs -> SnocList (xs ++ [x]) snocList : (xs : List a) -> SnocList a my_reverse : List a -> List a my_reverse xs with (snocList xs) my_reverse [] | Empty = [] my_reverse (ys ++ [x]) | (Snoc p) = x :: my_reverse ys | p The '| p' on the right hand side means that the with block function will be called directly, so the recursive structure of SnocList can direct the recursion structure of my_reverse.

commitc7bac2978501f075ebaaf327cda5b403a8ba00e0 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 29 Mar 2016, 19:29 (11 years ago) parent8df6b32

11 files changed+131−26

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+2 src/Idris/AbsSyntaxTree.hs+12−3 src/Idris/DSL.hs+7 src/Idris/DeepSeq.hs+3−2 src/Idris/Elab/Clause.hs+73−5 src/Idris/ElabDecls.hs+1−1 src/Idris/Error.hs+1 src/Idris/IBC.hs+10−2 src/Idris/Parser/Data.hs+1−1 src/Idris/Parser/Expr.hs+20−11 src/Idris/Parser/Ops.hs+1−1

src/Idris/AbsSyntax.hs+2

@@ -1742,6 +1742,8 @@ addImpl' inpat env infns imp_meths ist ptm

17421742 = let f' = ai inpat qq env ds f

17431743 as' = map (fmap (ai inpat qq env ds)) as in

17441744 mkPApp fc 1 f' as'

1745+ ai inpat qq env ds (PWithApp fc f a)

1746+ = PWithApp fc (ai inpat qq env ds f) (ai inpat qq env ds a)

17451747 ai inpat qq env ds (PCase fc c os)

17461748 = let c' = ai inpat qq env ds c in

17471749 -- leave os alone, because they get lifted into a new pattern match

src/Idris/AbsSyntaxTree.hs+12−3

@@ -59,11 +59,15 @@ data ElabInfo = EInfo { params :: [(Name, PTerm)],

5959 liftname :: Name -> Name,

6060 namespace :: Maybe [String],

6161 elabFC :: Maybe FC,

62+ -- We may, recursively, collect transformations to

63+ -- do on the rhs, e.g. rewriting recursive calls to

64+ -- functions defined by 'with'

65+ rhs_trans :: PTerm -> PTerm,

6266 rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl ->

6367 Idris () }

6468

6569toplevel :: ElabInfo

66−toplevel = EInfo [] emptyContext id Nothing Nothing (\_ _ _ -> fail "Not implemented")

70+toplevel = EInfo [] emptyContext id Nothing Nothing id (\_ _ _ -> fail "Not implemented")

6771

6872eInfoNames :: ElabInfo -> [Name]

6973eInfoNames info = map fst (params info) ++ M.keys (inblock info)

@@ -1012,6 +1016,7 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua

10121016 | PLet FC Name FC PTerm PTerm PTerm -- ^ A let binding (second FC is precise name location)

10131017 | PTyped PTerm PTerm -- ^ Term with explicit type

10141018 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x

1019+ | PWithApp FC PTerm PTerm -- ^ Application plus a 'with' argument

10151020 | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)

10161021 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application

10171022 | PMatchApp FC Name -- ^ Make an application by type matching

@@ -1067,6 +1072,7 @@ mapPTermFC f g (PPi plic n fc t1 t2) = PPi plic n (g fc) (mapPTermFC f

10671072mapPTermFC f g (PLet fc n fc' t1 t2 t3) = PLet (f fc) n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)

10681073mapPTermFC f g (PTyped t1 t2) = PTyped (mapPTermFC f g t1) (mapPTermFC f g t2)

10691074mapPTermFC f g (PApp fc t args) = PApp (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)

1075+mapPTermFC f g (PWithApp fc t arg) = PWithApp (f fc) (mapPTermFC f g t) (mapPTermFC f g arg)

10701076mapPTermFC f g (PAppImpl t1 impls) = PAppImpl (mapPTermFC f g t1) impls

10711077mapPTermFC f g (PAppBind fc t args) = PAppBind (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)

10721078mapPTermFC f g (PMatchApp fc n) = PMatchApp (f fc) n

@@ -1121,6 +1127,7 @@ mapPT f t = f (mpt t) where

11211127 mpt (PLet fc n nfc ty v s) = PLet fc n nfc (mapPT f ty) (mapPT f v) (mapPT f s)

11221128 mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s) (fmap (mapPT f) g)

11231129 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)

1130+ mpt (PWithApp fc t a) = PWithApp fc (mapPT f t) (mapPT f a)

11241131 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)

11251132 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)

11261133 mpt (PIfThenElse fc c t e) = PIfThenElse fc (mapPT f c) (mapPT f t) (mapPT f e)

@@ -1515,14 +1522,15 @@ data SyntaxInfo = Syn { using :: [Using],

15151522 mut_nesting :: Int,

15161523 dsl_info :: DSL,

15171524 syn_in_quasiquote :: Int,

1518− syn_toplevel :: Bool }

1525+ syn_toplevel :: Bool,

1526+ withAppAllowed :: Bool }

15191527 deriving Show

15201528{-!

15211529deriving instance NFData SyntaxInfo

15221530deriving instance Binary SyntaxInfo

15231531!-}

15241532

1525−defaultSyntax = Syn [] [] [] [] [] id False False Nothing 0 initDSL 0 True

1533+defaultSyntax = Syn [] [] [] [] [] id False False Nothing 0 initDSL 0 True True

15261534

15271535expandNS :: SyntaxInfo -> Name -> Name

15281536expandNS syn n@(NS _ _) = n

@@ -1840,6 +1848,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

18401848 if null shownArgs

18411849 then fp

18421850 else fp <+> align (vsep (map (prettyArgS d bnd) shownArgs))

1851+ prettySe d p bnd (PWithApp _ f a) = prettySe d p bnd f <+> text "|" <+> prettySe d p bnd a

18431852 prettySe d p bnd (PCase _ scr cases) =

18441853 align $ kwd "case" <+> prettySe (decD d) startPrec bnd scr <+> kwd "of" <$>

18451854 depth d (indent 2 (vsep (map ppcase cases)))

src/Idris/DSL.hs+7

@@ -67,6 +67,8 @@ expandSugar dsl (PPi p n fc ty tm)

6767expandSugar dsl (PPi p n fc ty tm) = PPi p n fc (expandSugar dsl ty) (expandSugar dsl tm)

6868expandSugar dsl (PApp fc t args) = PApp fc (expandSugar dsl t)

6969 (map (fmap (expandSugar dsl)) args)

70+expandSugar dsl (PWithApp fc t arg) = PWithApp fc (expandSugar dsl t)

71+ (expandSugar dsl arg)

7072expandSugar dsl (PAppBind fc t args) = PAppBind fc (expandSugar dsl t)

7173 (map (fmap (expandSugar dsl)) args)

7274expandSugar dsl (PCase fc s opts) = PCase fc (expandSugar dsl s)

@@ -140,6 +142,7 @@ var dsl n t i = v' i t where

140142 | otherwise = PPi p n fc (v' i ty) (v' (i+1) sc)

141143 v' i (PTyped l r) = PTyped (v' i l) (v' i r)

142144 v' i (PApp f x as) = PApp f (v' i x) (fmap (fmap (v' i)) as)

145+ v' i (PWithApp f x a) = PWithApp f (v' i x) (v' i a)

143146 v' i (PCase f t as) = PCase f (v' i t) (fmap (pmap (v' i)) as)

144147 v' i (PPair f hls p l r) = PPair f hls p (v' i l) (v' i r)

145148 v' i (PDPair f hls p l t r) = PDPair f hls p (v' i l) (v' i t) (v' i r)

@@ -191,6 +194,10 @@ debind b tm = let (tm', (bs, _)) = runState (db' tm) ([], 0) in

191194 = do t' <- db' t

192195 args' <- mapM dbArg args

193196 return (PApp fc t' args')

197+ db' (PWithApp fc t arg)

198+ = do t' <- db' t

199+ arg' <- db' arg

200+ return (PWithApp fc t' arg')

194201 db' (PLam fc n nfc ty sc) = return (PLam fc n nfc ty (debind b sc))

195202 db' (PLet fc n nfc ty v sc) = do v' <- db' v

196203 return (PLet fc n nfc ty v' (debind b sc))

src/Idris/DeepSeq.hs+3−2

@@ -530,6 +530,7 @@ instance NFData PTerm where

530530 rnf (PTyped x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

531531 rnf (PAppImpl x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

532532 rnf (PApp x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

533+ rnf (PWithApp x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

533534 rnf (PAppBind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

534535 rnf (PMatchApp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

535536 rnf (PCase x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

@@ -681,13 +682,13 @@ instance NFData Using where

681682 rnf (UConstraint x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

682683

683684instance NFData SyntaxInfo where

684− rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)

685+ rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14)

685686 = rnf x1 `seq`

686687 rnf x2 `seq`

687688 rnf x3 `seq`

688689 rnf x4 `seq`

689690 rnf x5 `seq`

690− rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` rnf x13 `seq` ()

691+ rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` rnf x13 `seq` rnf x14 `seq` ()

691692

692693instance NFData OutputMode where

693694 rnf (RawOutput x) = () -- no instance for Handle, so this is a bit wrong

src/Idris/Elab/Clause.hs+73−5

@@ -667,7 +667,8 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

667667 -- Now build the RHS, using the type of the LHS as the goal.

668668 i <- getIState -- new implicits from where block

669669 logElab 5 (showTmImpls (expandParams decorate newargs defs (defs \\ decls) rhs_in))

670− let rhs = addImplBoundInf i (map fst newargs_all) (defs \\ decls)

670+ let rhs = rhs_trans info $

671+ addImplBoundInf i (map fst newargs_all) (defs \\ decls)

671672 (expandParams decorate newargs defs (defs \\ decls) rhs_in)

672673 logElab 2 $ "RHS: " ++ show (map fst newargs_all) ++ " " ++ showTmImpls rhs

673674 ctxt <- getContext -- new context with where block added

@@ -861,7 +862,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

861862 (clhs, clhsty) <- recheckC fc id [] lhs_tm

862863 logElab 5 ("Checked " ++ show clhs)

863864 let bargs = getPBtys (explicitNames (normalise ctxt [] lhs_tm))

864− let wval = addImplBound i (map fst bargs) wval_in

865+ let wval = rhs_trans info $ addImplBound i (map fst bargs) wval_in

865866 logElab 5 ("Checking " ++ showTmImpls wval)

866867 -- Elaborate wval in this context

867868 ((wval', defer, is, ctxt', newDecls, highlights, newGName), _) <-

@@ -959,7 +960,10 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

959960 logElab 3 ("with block " ++ show wb)

960961 -- propagate totality assertion to the new definitions

961962 when (AssertTotal `elem` opts) $ setFlags wname [AssertTotal]

962− mapM_ (rec_elabDecl info EAll info) wb

963+ i <- getIState

964+ let rhstrans' = updateWithTerm i mpn wname lhs (map fst bargs_pre) (map fst (bargs_post))

965+ . rhs_trans info

966+ mapM_ (rec_elabDecl info EAll (info { rhs_trans = rhstrans' })) wb

963967

964968 -- rhs becomes: fname' ps_pre wval ps_post Refl

965969 let rhs = PApp fc (PRef fc [] wname)

@@ -1001,9 +1005,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

10011005 getImps _ = []

10021006

10031007 mkAuxC pn wname lhs ns ns' (PClauses fc o n cs)

1004− | True = do cs' <- mapM (mkAux pn wname lhs ns ns') cs

1008+ = do cs' <- mapM (mkAux pn wname lhs ns ns') cs

10051009 return $ PClauses fc o wname cs'

1006− | otherwise = ifail $ show fc ++ "with clause uses wrong function name " ++ show n

10071010 mkAuxC pn wname lhs ns ns' d = return $ d

10081011

10091012 mkAux pn wname toplhs ns ns' (PClause fc n tm_in (w:ws) rhs wheres)

@@ -1034,6 +1037,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

10341037 addArg (PApp fc f args) w = PApp fc f (args ++ [pexp w])

10351038 addArg (PRef fc hls f) w = PApp fc (PRef fc hls f) [pexp w]

10361039

1040+ -- ns, arguments which don't depend on the with argument

1041+ -- ns', arguments which do

10371042 updateLHS n pn wname mvars ns_in ns_in' (PApp fc (PRef fc' hls' n') args) w

10381043 = let ns = map (keepMvar (map fst mvars) fc') ns_in

10391044 ns' = map (keepMvar (map fst mvars) fc') ns_in' in

@@ -1046,9 +1051,56 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

10461051 updateLHS n pn wname mvars ns_in ns_in' tm w

10471052 = updateLHS n pn wname mvars ns_in ns_in' (PApp fc tm []) w

10481053

1054+ -- Only keep a var as a pattern variable in the with block if it's

1055+ -- matched in the top level pattern

10491056 keepMvar mvs fc v | v `elem` mvs = PRef fc [] v

10501057 | otherwise = Placeholder

10511058

1059+ updateWithTerm :: IState -> Maybe Name -> Name -> PTerm -> [Name] -> [Name] -> PTerm -> PTerm

1060+ updateWithTerm ist pn wname toplhs ns_in ns_in' tm

1061+ = mapPT updateApp tm

1062+ where

1063+ arity (PApp _ _ as) = length as

1064+ arity _ = 0

1065+

1066+ lhs_arity = arity toplhs

1067+

1068+ updateApp wtm@(PWithApp fcw tm warg) =

1069+ case matchClause ist toplhs tm of

1070+ Left _ -> PElabError (Msg (show fc ++ ":with application does not match top level"))

1071+ Right mvars ->

1072+ let ns = map (keepMvar (map fst mvars) fcw) ns_in

1073+ ns' = map (keepMvar (map fst mvars) fcw) ns_in'

1074+ wty = lookupTyExact wname (tt_ctxt ist)

1075+ res = substMatches mvars $

1076+ PApp fcw (PRef fcw [] wname)

1077+ (map pexp ns ++ pexp warg : (map pexp ns') ++

1078+ case pn of

1079+ Nothing -> []

1080+ Just pnm -> [pexp (PRef fc [] pnm)]) in

1081+ case wty of

1082+ Nothing -> res -- can't happen!

1083+ Just ty -> addResolves ty res

1084+ updateApp tm = tm

1085+

1086+ addResolves ty (PApp fc f args) = PApp fc f (addResolvesArgs fc ty args)

1087+ addResolves ty tm = tm

1088+

1089+ -- if an argument's type is a type class, and is otherwise to

1090+ -- be inferred, then resolve it with instance search

1091+ -- This is something of a hack, because matching on the top level

1092+ -- application won't find this information for us

1093+ addResolvesArgs :: FC -> Term -> [PArg] -> [PArg]

1094+ addResolvesArgs fc (Bind n (Pi _ ty _) sc) (a : args)

1095+ | (P _ cn _, _) <- unApply ty,

1096+ getTm a == Placeholder

1097+ = case lookupCtxtExact cn (idris_classes ist) of

1098+ Just _ -> a { getTm = PResolveTC fc } : addResolvesArgs fc sc args

1099+ Nothing -> a : addResolvesArgs fc sc args

1100+ addResolvesArgs fc (Bind n (Pi _ ty _) sc) (a : args)

1101+ = a : addResolvesArgs fc sc args

1102+ addResolvesArgs fc _ args = args

1103+

10521104 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))

10531105 fullApp x = x

10541106

@@ -1059,3 +1111,19 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

10591111 split deps [] pre = (reverse pre, [])

10601112

10611113 abstract wn wv wty (n, argty) = (n, substTerm wv (P Bound wn wty) argty)

1114+

1115+-- Apply a transformation to all RHSes and nested RHSs

1116+mapRHS :: (PTerm -> PTerm) -> PClause -> PClause

1117+mapRHS f (PClause fc n lhs args rhs ws)

1118+ = PClause fc n lhs args (f rhs) (map (mapRHSdecl f) ws)

1119+mapRHS f (PWith fc n lhs args warg prf ws)

1120+ = PWith fc n lhs args (f warg) prf (map (mapRHSdecl f) ws)

1121+mapRHS f (PClauseR fc args rhs ws)

1122+ = PClauseR fc args (f rhs) (map (mapRHSdecl f) ws)

1123+mapRHS f (PWithR fc args warg prf ws)

1124+ = PWithR fc args (f warg) prf (map (mapRHSdecl f) ws)

1125+

1126+mapRHSdecl :: (PTerm -> PTerm) -> PDecl -> PDecl

1127+mapRHSdecl f (PClauses fc opt n cs)

1128+ = PClauses fc opt n (map (mapRHS f) cs)

1129+mapRHSdecl f t = t

src/Idris/ElabDecls.hs+1−1

@@ -64,7 +64,7 @@ import Util.Pretty(pretty, text)

6464

6565-- Top level elaborator info, supporting recursive elaboration

6666recinfo :: ElabInfo

67−recinfo = EInfo [] emptyContext id Nothing Nothing elabDecl'

67+recinfo = EInfo [] emptyContext id Nothing Nothing id elabDecl'

6868

6969-- | Return the elaborated term which calls 'main'

7070elabMain :: Idris Term

src/Idris/Error.hs+1

@@ -97,6 +97,7 @@ warnDisamb ist (PLet _ _ _ x t b) = warnDisamb ist x >> warnDisamb ist t >> warn

9797warnDisamb ist (PTyped x t) = warnDisamb ist x >> warnDisamb ist t

9898warnDisamb ist (PApp _ t args) = warnDisamb ist t >>

9999 mapM_ (warnDisamb ist . getTm) args

100+warnDisamb ist (PWithApp _ t a) = warnDisamb ist t >> warnDisamb ist a

100101warnDisamb ist (PAppBind _ f args) = warnDisamb ist f >>

101102 mapM_ (warnDisamb ist . getTm) args

102103warnDisamb ist (PMatchApp _ _) = return ()

src/Idris/IBC.hs+10−2

@@ -1471,7 +1471,7 @@ instance Binary Using where

14711471 _ -> error "Corrupted binary data for Using"

14721472

14731473instance Binary SyntaxInfo where

1474− put (Syn x1 x2 x3 x4 _ _ x5 x6 _ _ x7 _ _)

1474+ put (Syn x1 x2 x3 x4 _ _ x5 x6 _ _ x7 _ _ _)

14751475 = do put x1

14761476 put x2

14771477 put x3

@@ -1487,7 +1487,7 @@ instance Binary SyntaxInfo where

14871487 x5 <- get

14881488 x6 <- get

14891489 x7 <- get

1490− return (Syn x1 x2 x3 x4 [] id x5 x6 Nothing 0 x7 0 True)

1490+ return (Syn x1 x2 x3 x4 [] id x5 x6 Nothing 0 x7 0 True True)

14911491

14921492instance (Binary t) => Binary (PClause' t) where

14931493 put x

@@ -1736,6 +1736,10 @@ instance Binary PTerm where

17361736 PConstSugar x1 x2 -> do putWord8 46

17371737 put x1

17381738 put x2

1739+ PWithApp x1 x2 x3 -> do putWord8 47

1740+ put x1

1741+ put x2

1742+ put x3

17391743

17401744 get

17411745 = do i <- getWord8

@@ -1883,6 +1887,10 @@ instance Binary PTerm where

18831887 46 -> do x1 <- get

18841888 x2 <- get

18851889 return (PConstSugar x1 x2)

1890+ 47 -> do x1 <- get

1891+ x2 <- get

1892+ x3 <- get

1893+ return (PWithApp x1 x2 x3)

18861894 _ -> error "Corrupted binary data for PTerm"

18871895

18881896instance Binary PAltType where

src/Idris/Parser/Data.hs+1−1

@@ -227,7 +227,7 @@ data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do

227227 let fix2 = s ++ ": " ++ ns ++ " -> Type where\n ..."

228228 let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..."

229229 fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]

230− cons <- sepBy1 (simpleConstructor syn) (reservedOp "|")

230+ cons <- sepBy1 (simpleConstructor (syn { withAppAllowed = False })) (reservedOp "|")

231231 terminator

232232 let conty = mkPApp fc (PRef fc [] tyn) (map (PRef fc []) args)

233233 cons' <- mapM (\ (doc, argDocs, x, xfc, cargs, cfc, fs) ->

src/Idris/Parser/Expr.hs+20−11

@@ -74,7 +74,8 @@ expr = pi

7474-}

7575opExpr :: SyntaxInfo -> IdrisParser PTerm

7676opExpr syn = do i <- get

77− buildExpressionParser (table (idris_infixes i)) (expr' syn)

77+ buildExpressionParser (table (idris_infixes i))

78+ (expr' syn)

7879

7980{- | Parses either an internally defined expression or

8081 a user-defined one

@@ -439,7 +440,7 @@ Bracketed ::= '(' Bracketed'

439440bracketed :: SyntaxInfo -> IdrisParser PTerm

440441bracketed syn = do (FC fn (sl, sc) _) <- getFC

441442 lchar '(' <?> "parenthesized expression"

442− bracketed' (FC fn (sl, sc) (sl, sc+1)) syn

443+ bracketed' (FC fn (sl, sc) (sl, sc+1)) (syn { withAppAllowed = True })

443444

444445{- |Parses the rest of an expression in braces

445446@

@@ -572,7 +573,7 @@ modifyConst syn fc x = x

572573@

573574-}

574575alt :: SyntaxInfo -> IdrisParser PTerm

575−alt syn = do symbol "(|"; alts <- sepBy1 (expr' syn) (lchar ','); symbol "|)"

576+alt syn = do symbol "(|"; alts <- sepBy1 (expr' (syn { withAppAllowed = False })) (lchar ','); symbol "|)"

576577 return (PAlternative [] FirstSuccess alts)

577578

578579{- | Parses a possibly hidden simple expression

@@ -668,9 +669,12 @@ app syn = do f <- simpleExpr syn

668669 fc <- getFC

669670 i <- get

670671 args <- many (do notEndApp; arg syn)

672+ wargs <- if withAppAllowed syn && not (inPattern syn)

673+ then many (do notEndApp; reservedOp "|"; expr' syn)

674+ else return []

671675 case args of

672676 [] -> return f

673− _ -> return (flattenFromInt fc f args))

677+ _ -> return (withApp fc (flattenFromInt fc f args) wargs))

674678 <?> "function application"

675679 where

676680 -- bit of a hack to deal with the situation where we're applying a

@@ -682,6 +686,9 @@ app syn = do f <- simpleExpr syn

682686 = PApp fc (PRef fc [] (sUN "fromInteger")) (i : args)

683687 flattenFromInt fc f args = PApp fc f args

684688

689+ withApp fc tm [] = tm

690+ withApp fc tm (a : as) = withApp fc (PWithApp fc tm a) as

691+

685692 getFromInt ((PApp _ (PRef _ _ n) [a]) : _) | n == sUN "fromInteger" = Just a

686693 getFromInt (_ : xs) = getFromInt xs

687694 getFromInt _ = Nothing

@@ -978,10 +985,12 @@ let_binding syn = do fc <- getFC;

978985 pat <- expr' (syn { inPattern = True })

979986 ty <- option Placeholder (do lchar ':'; expr' syn)

980987 lchar '='

981− v <- expr syn

988+ v <- expr (syn { withAppAllowed = isVar pat })

982989 ts <- option [] (do lchar '|'

983990 sepBy1 (do_alt syn) (lchar '|'))

984991 return (fc,pat,ty,v,ts)

992+ where isVar (PRef _ _ _) = True

993+ isVar _ = False

985994

986995{- | Parses a conditional expression

987996@

@@ -1227,7 +1236,7 @@ listExpr syn = do (FC f (l, c) _) <- getFC

12271236 (try . token $ do (char ']' <?> "end of list expression")

12281237 (FC _ _ (l', c')) <- getFC

12291238 return (mkNil (FC f (l, c) (l', c'))))

1230− <|> (do x <- expr syn <?> "expression"

1239+ <|> (do x <- expr (syn { withAppAllowed = False }) <?> "expression"

12311240 (do try (lchar '|') <?> "list comprehension"

12321241 qs <- sepBy1 (do_ syn) (lchar ',')

12331242 lchar ']'

@@ -1306,18 +1315,18 @@ do_ syn

13061315 <|> try (do (i, ifc) <- name

13071316 symbol "<-"

13081317 fc <- getFC

1309− e <- expr syn;

1318+ e <- expr (syn { withAppAllowed = False });

13101319 option (DoBind fc i ifc e)

13111320 (do lchar '|'

1312− ts <- sepBy1 (do_alt syn) (lchar '|')

1321+ ts <- sepBy1 (do_alt (syn { withAppAllowed = False })) (lchar '|')

13131322 return (DoBindP fc (PRef ifc [ifc] i) e ts)))

13141323 <|> try (do i <- expr' syn

13151324 symbol "<-"

13161325 fc <- getFC

1317− e <- expr syn;

1326+ e <- expr (syn { withAppAllowed = False });

13181327 option (DoBindP fc i e [])

13191328 (do lchar '|'

1320− ts <- sepBy1 (do_alt syn) (lchar '|')

1329+ ts <- sepBy1 (do_alt (syn { withAppAllowed = False })) (lchar '|')

13211330 return (DoBindP fc i e ts)))

13221331 <|> do e <- expr syn

13231332 fc <- getFC

@@ -1339,7 +1348,7 @@ idiom :: SyntaxInfo -> IdrisParser PTerm

13391348idiom syn

13401349 = do symbol "[|"

13411350 fc <- getFC

1342− e <- expr syn

1351+ e <- expr (syn { withAppAllowed = False })

13431352 symbol "|]"

13441353 return (PIdiom fc e)

13451354 <?> "expression in idiom brackets"

src/Idris/Parser/Ops.hs+1−1

@@ -36,7 +36,7 @@ import Debug.Trace

3636table :: [FixDecl] -> OperatorTable IdrisParser PTerm

3737table fixes

3838 = [[prefix "-" (\fc x -> PApp fc (PRef fc [fc] (sUN "negate")) [pexp x])]] ++

39− toTable (reverse fixes) ++

39+ toTable (reverse fixes) ++

4040 [[backtick],

4141 [binary "$" (\fc x y -> flatten $ PApp fc x [pexp y]) AssocRight],

4242 [binary "=" (\fc x y -> PApp fc (PRef fc [fc] eqTy) [pexp x, pexp y]) AssocLeft],