c7bac29 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Extended syntax for 'with' blocks

c7bac29Edwin Brady11 years ago

src/Idris/AbsSyntax.hs+2

compare with master

unifiedsplit

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

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

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

1744 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)

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

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

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

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

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

1749 -- 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)],

59 liftname :: Name -> Name,

60 namespace :: Maybe [String],

61 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,

62 rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl ->

66 rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl ->

63 Idris () }

67 Idris () }

65toplevel :: ElabInfo

69toplevel :: ElabInfo

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

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

68eInfoNames :: ElabInfo -> [Name]

72eInfoNames :: ElabInfo -> [Name]

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

73eInfoNames 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

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

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

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

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

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

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

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

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

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

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

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

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

1022 | 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

1067mapPTermFC 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)

1072mapPTermFC 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)

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

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

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

1074mapPTermFC 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)

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

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

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

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

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

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

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

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

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

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

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

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

1129 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)

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

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

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

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

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

1133 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],

1515 mut_nesting :: Int,

1522 mut_nesting :: Int,

1516 dsl_info :: DSL,

1523 dsl_info :: DSL,

1517 syn_in_quasiquote :: Int,

1524 syn_in_quasiquote :: Int,

1518− syn_toplevel :: Bool }

1525+ syn_toplevel :: Bool,

1526+ withAppAllowed :: Bool }

1519 deriving Show

1527 deriving Show

1520{-!

1528{-!

1521deriving instance NFData SyntaxInfo

1529deriving instance NFData SyntaxInfo

1522deriving instance Binary SyntaxInfo

1530deriving instance Binary SyntaxInfo

1523!-}

1531!-}

1524

1532

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

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

1526

1534

1527expandNS :: SyntaxInfo -> Name -> Name

1535expandNS :: SyntaxInfo -> Name -> Name

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

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

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

1840 if null shownArgs

1848 if null shownArgs

1841 then fp

1849 then fp

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

1850 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

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

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

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

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

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

1854 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)

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

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

69 (map (fmap (expandSugar dsl)) args)

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

71+ (expandSugar dsl arg)

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

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

71 (map (fmap (expandSugar dsl)) args)

73 (map (fmap (expandSugar dsl)) args)

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

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

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

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

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

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

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

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

144 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)

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

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

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

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

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

148 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

191 = do t' <- db' t

194 = do t' <- db' t

192 args' <- mapM dbArg args

195 args' <- mapM dbArg args

193 return (PApp fc t' args')

196 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')

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

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

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

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

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

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

src/Idris/DeepSeq.hs+3−2

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

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

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

532 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` ()

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

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

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

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

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

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

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

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

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

682

683

683instance NFData SyntaxInfo where

684instance 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)

685 = rnf x1 `seq`

686 = rnf x1 `seq`

686 rnf x2 `seq`

687 rnf x2 `seq`

687 rnf x3 `seq`

688 rnf x3 `seq`

688 rnf x4 `seq`

689 rnf x4 `seq`

689 rnf x5 `seq`

690 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` ()

691

692

692instance NFData OutputMode where

693instance NFData OutputMode where

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

694 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

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

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

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

670+ let rhs = rhs_trans info $

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

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

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

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

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

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

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

674 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)

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

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

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

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

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

864 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

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

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

866 -- Elaborate wval in this context

867 -- Elaborate wval in this context

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

868 ((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)

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

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

960 -- propagate totality assertion to the new definitions

961 -- propagate totality assertion to the new definitions

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

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

963+ i <- getIState

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

965+ . rhs_trans info

962− mapM_ (rec_elabDecl info EAll info) wb

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

963

967

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

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

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

969 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)

1001 getImps _ = []

1005 getImps _ = []

1002

1006

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

1007 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

1005 return $ PClauses fc o wname cs'

1009 return $ PClauses fc o wname cs'

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

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

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

1008

1011

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

1012 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)

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

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

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

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

1036

1039

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

1041+ -- ns', arguments which do

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

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

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

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

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

1044 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)

1046 updateLHS n pn wname mvars ns_in ns_in' tm w

1051 updateLHS n pn wname mvars ns_in ns_in' tm w

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

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

1048

1053

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

1055+ -- matched in the top level pattern

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

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

1050 | otherwise = Placeholder

1057 | otherwise = Placeholder

1051

1058

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+

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

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

1053 fullApp x = x

1105 fullApp x = x

1054

1106

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

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

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

1060

1112

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

1113 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)

65-- Top level elaborator info, supporting recursive elaboration

66recinfo :: ElabInfo

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

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

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

70elabMain :: Idris Term

src/Idris/Error.hs+1

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

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

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

99 mapM_ (warnDisamb ist . getTm) args

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

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

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

101 mapM_ (warnDisamb ist . getTm) args

102 mapM_ (warnDisamb ist . getTm) args

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

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

src/Idris/IBC.hs+10−2

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

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

1472

1473instance Binary SyntaxInfo where

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

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

1475 = do put x1

1476 put x2

1477 put x3

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

1487 x5 <- get

1488 x6 <- get

1489 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)

1491

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

1493 put x

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

1736 PConstSugar x1 x2 -> do putWord8 46

1737 put x1

1738 put x2

1739+ PWithApp x1 x2 x3 -> do putWord8 47

1740+ put x1

1741+ put x2

1742+ put x3

1739

1743

1740 get

1744 get

1741 = do i <- getWord8

1745 = do i <- getWord8

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

1883 46 -> do x1 <- get

1887 46 -> do x1 <- get

1884 x2 <- get

1888 x2 <- get

1885 return (PConstSugar x1 x2)

1889 return (PConstSugar x1 x2)

1890+ 47 -> do x1 <- get

1891+ x2 <- get

1892+ x3 <- get

1893+ return (PWithApp x1 x2 x3)

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

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

1887

1895

1888instance Binary PAltType where

1896instance Binary PAltType where

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

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

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

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

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

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

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

231 terminator

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

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

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

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

74-}

75opExpr :: SyntaxInfo -> IdrisParser PTerm

76opExpr syn = do i <- get

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

77+ buildExpressionParser (table (idris_infixes i))

78+ (expr' syn)

79{- | Parses either an internally defined expression or

80{- | Parses either an internally defined expression or

80 a user-defined one

81 a user-defined one

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

439bracketed :: SyntaxInfo -> IdrisParser PTerm

440bracketed :: SyntaxInfo -> IdrisParser PTerm

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

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

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

442 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 })

443

444

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

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

445@

446@

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

572@

573@

573-}

574-}

574alt :: SyntaxInfo -> IdrisParser PTerm

575alt :: 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 "|)"

576 return (PAlternative [] FirstSuccess alts)

577 return (PAlternative [] FirstSuccess alts)

577

578

578{- | Parses a possibly hidden simple expression

579{- | Parses a possibly hidden simple expression

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

668 fc <- getFC

669 fc <- getFC

669 i <- get

670 i <- get

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

671 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 []

671 case args of

675 case args of

672 [] -> return f

676 [] -> return f

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

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

674 <?> "function application"

678 <?> "function application"

675 where

679 where

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

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

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

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

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

683 flattenFromInt fc f args = PApp fc f args

687 flattenFromInt fc f args = PApp fc f args

684

688

689+ withApp fc tm [] = tm

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

691+

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

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

686 getFromInt (_ : xs) = getFromInt xs

693 getFromInt (_ : xs) = getFromInt xs

687 getFromInt _ = Nothing

694 getFromInt _ = Nothing

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

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

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

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

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

980 lchar '='

987 lchar '='

981− v <- expr syn

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

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

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

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

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

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

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

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

993+ isVar _ = False

985

994

986{- | Parses a conditional expression

995{- | Parses a conditional expression

987@

996@

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

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

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

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

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

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

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

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

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

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

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

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

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

1233 lchar ']'

1242 lchar ']'

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

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

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

1307 symbol "<-"

1316 symbol "<-"

1308 fc <- getFC

1317 fc <- getFC

1309− e <- expr syn;

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

1310 option (DoBind fc i ifc e)

1319 option (DoBind fc i ifc e)

1311 (do lchar '|'

1320 (do lchar '|'

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

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

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

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

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

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

1315 symbol "<-"

1324 symbol "<-"

1316 fc <- getFC

1325 fc <- getFC

1317− e <- expr syn;

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

1318 option (DoBindP fc i e [])

1327 option (DoBindP fc i e [])

1319 (do lchar '|'

1328 (do lchar '|'

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

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

1321 return (DoBindP fc i e ts)))

1330 return (DoBindP fc i e ts)))

1322 <|> do e <- expr syn

1331 <|> do e <- expr syn

1323 fc <- getFC

1332 fc <- getFC

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

1339idiom syn

1348idiom syn

1340 = do symbol "[|"

1349 = do symbol "[|"

1341 fc <- getFC

1350 fc <- getFC

1342− e <- expr syn

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

1343 symbol "|]"

1352 symbol "|]"

1344 return (PIdiom fc e)

1353 return (PIdiom fc e)

1345 <?> "expression in idiom brackets"

1354 <?> "expression in idiom brackets"

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

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

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

37table fixes

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

39− toTable (reverse fixes) ++

39+ toTable (reverse fixes) ++

40 [[backtick],

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

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