8c9ec38 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Added 'implicit bind' syntax

8c9ec38Edwin Brady13 years ago

effects/Effects.idr+2

compare with master

unifiedsplit

@@ -130,6 +130,8 @@ data EffM : (m : Type -> Type) ->

130 EffM m xs xs' a

131 (:-) : (l : ty) -> EffM m [x] [y] t -> EffM m [l ::: x] [l ::: y] t

132

133+syntax [tag] ":!" [val] = !(tag :- val)

134+

133-- Eff : List (EFFECT m) -> Type -> Type

135-- Eff : List (EFFECT m) -> Type -> Type

134

136

135implicit

137implicit

src/Idris/AbsSyntax.hs+7

@@ -699,6 +699,11 @@ expandParams dec ps ns infs tm = en tm

699 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))

700 | n `nselem` ns = PApp fc (PRef fc' (dec n))

701 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))

702+ en (PAppBind fc (PRef fc' n) as)

703+ | n `elem` infs = PAppBind fc (PInferRef fc' (dec n))

704+ (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))

705+ | n `nselem` ns = PAppBind fc (PRef fc' (dec n))

706+ (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))

702 en (PRef fc n)

707 en (PRef fc n)

703 | n `elem` infs = PApp fc (PInferRef fc (dec n))

708 | n `elem` infs = PApp fc (PInferRef fc (dec n))

704 (map (pexp . (PRef fc)) (map fst ps))

709 (map (pexp . (PRef fc)) (map fst ps))

@@ -708,6 +713,7 @@ expandParams dec ps ns infs tm = en tm

708 | n `nselem` ns = PApp fc (PInferRef fc (dec n))

713 | n `nselem` ns = PApp fc (PInferRef fc (dec n))

709 (map (pexp . (PRef fc)) (map fst ps))

714 (map (pexp . (PRef fc)) (map fst ps))

710 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)

715 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)

716+ en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)

711 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)

717 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)

712 en t = t

718 en t = t

713

719

@@ -829,6 +835,7 @@ getPriority i tm = 1 -- pri tm

829 pri (PEq _ l r) = max 1 (max (pri l) (pri r))

835 pri (PEq _ l r) = max 1 (max (pri l) (pri r))

830 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))

836 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))

831 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))

837 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))

838+ pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))

832 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))

839 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))

833 pri (PTyped l r) = pri l

840 pri (PTyped l r) = pri l

834 pri (PPair _ l r) = max 1 (max (pri l) (pri r))

841 pri (PPair _ l r) = max 1 (max (pri l) (pri r))

src/Idris/AbsSyntaxTree.hs+14

@@ -533,6 +533,7 @@ data PTerm = PQuote Raw

533 | PLet Name PTerm PTerm PTerm

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

535 | PApp FC PTerm [PArg]

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

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

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

537 | PCase FC PTerm [(PTerm, PTerm)]

538 | PCase FC PTerm [(PTerm, PTerm)]

538 | PTrue FC

539 | PTrue FC

@@ -573,6 +574,7 @@ mapPT f t = f (mpt t) where

573 mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s)

574 mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s)

574 (fmap (mapPT f) g)

575 (fmap (mapPT f) g)

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

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

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

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

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

577 mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)

579 mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)

578 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)

580 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)

@@ -957,6 +959,8 @@ prettyImp impl = prettySe 10

957 rbrace <+> text "->" <+> prettySe 10 sc

959 rbrace <+> text "->" <+> prettySe 10 sc

958 prettySe p (PApp _ (PRef _ f) [])

960 prettySe p (PApp _ (PRef _ f) [])

959 | not impl = pretty f

961 | not impl = pretty f

962+ prettySe p (PAppBind _ (PRef _ f) [])

963+ | not impl = pretty f <+> text "!"

960 prettySe p (PApp _ (PRef _ op@(UN (f:_))) args)

964 prettySe p (PApp _ (PRef _ op@(UN (f:_))) args)

961 | length (getExps args) == 2 && (not impl) && (not $ isAlpha f) =

965 | length (getExps args) == 2 && (not impl) && (not $ isAlpha f) =

962 let [l, r] = getExps args in

966 let [l, r] = getExps args in

@@ -1142,6 +1146,8 @@ showImp ist impl colour tm = se 10 [] tm where

1142 se p bnd (PMatchApp _ f) = "match " ++ show f

1146 se p bnd (PMatchApp _ f) = "match " ++ show f

1143 se p bnd (PApp _ hd@(PRef _ f) [])

1147 se p bnd (PApp _ hd@(PRef _ f) [])

1144 | not impl = se p bnd hd

1148 | not impl = se p bnd hd

1149+ se p bnd (PAppBind _ hd@(PRef _ f) [])

1150+ | not impl = se p bnd hd ++ "!"

1145 se p bnd (PApp _ op@(PRef _ (UN (f:_))) args)

1151 se p bnd (PApp _ op@(PRef _ (UN (f:_))) args)

1146 | length (getExps args) == 2 && not impl && not (isAlpha f)

1152 | length (getExps args) == 2 && not impl && not (isAlpha f)

1147 = let [l, r] = getExps args in

1153 = let [l, r] = getExps args in

@@ -1150,6 +1156,10 @@ showImp ist impl colour tm = se 10 [] tm where

1150 = let args = getExps as in

1156 = let args = getExps as in

1151 bracket p 1 $ se 1 bnd f ++ if impl then concatMap (sArg bnd) as

1157 bracket p 1 $ se 1 bnd f ++ if impl then concatMap (sArg bnd) as

1152 else concatMap (seArg bnd) args

1158 else concatMap (seArg bnd) args

1159+ se p bnd (PAppBind _ f as)

1160+ = let args = getExps as in

1161+ bracket p 1 $ se 1 bnd f ++ "!" ++ if impl then concatMap (sArg bnd) as

1162+ else concatMap (seArg bnd) args

1153 se p bnd (PCase _ scr opts) = "case " ++ se 10 bnd scr ++ " of " ++ showSep " | " (map sc opts)

1163 se p bnd (PCase _ scr opts) = "case " ++ se 10 bnd scr ++ " of " ++ showSep " | " (map sc opts)

1154 where sc (l, r) = se 10 bnd l ++ " => " ++ se 10 bnd r

1164 where sc (l, r) = se 10 bnd l ++ " => " ++ se 10 bnd r

1155 se p bnd (PHidden tm) = "." ++ se 0 bnd tm

1165 se p bnd (PHidden tm) = "." ++ se 0 bnd tm

@@ -1238,6 +1248,7 @@ instance Sized PTerm where

1238 size (PLet name ty def bdy) = 1 + size ty + size def + size bdy

1248 size (PLet name ty def bdy) = 1 + size ty + size def + size bdy

1239 size (PTyped trm ty) = 1 + size trm + size ty

1249 size (PTyped trm ty) = 1 + size trm + size ty

1240 size (PApp fc name args) = 1 + size args

1250 size (PApp fc name args) = 1 + size args

1251+ size (PAppBind fc name args) = 1 + size args

1241 size (PCase fc trm bdy) = 1 + size trm + size bdy

1252 size (PCase fc trm bdy) = 1 + size trm + size bdy

1242 size (PTrue fc) = 1

1253 size (PTrue fc) = 1

1243 size (PFalse fc) = 1

1254 size (PFalse fc) = 1

@@ -1274,6 +1285,7 @@ allNamesIn tm = nub $ ni [] tm

1274 ni env (PRef _ n)

1285 ni env (PRef _ n)

1275 | not (n `elem` env) = [n]

1286 | not (n `elem` env) = [n]

1276 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1287 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1288+ ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1277 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)

1289 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)

1278 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1290 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1279 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc

1291 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc

@@ -1300,6 +1312,7 @@ namesIn uvars ist tm = nub $ ni [] tm

1300 [] -> [n]

1312 [] -> [n]

1301 _ -> if n `elem` (map fst uvars) then [n] else []

1313 _ -> if n `elem` (map fst uvars) then [n] else []

1302 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1314 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1315+ ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1303 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)

1316 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)

1304 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1317 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1305 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc

1318 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc

@@ -1326,6 +1339,7 @@ usedNamesIn vars ist tm = nub $ ni [] tm

1326 [] -> [n]

1339 [] -> [n]

1327 _ -> []

1340 _ -> []

1328 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1341 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1342+ ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1329 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)

1343 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)

1330 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1344 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1331 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc

1345 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc

src/Idris/DSL.hs+50−1

@@ -9,8 +9,12 @@ import Core.CoreParser

9import Core.TT

10import Core.Evaluate

12+import Control.Monad.State

12import Debug.Trace

13import Debug.Trace

15+debindApp :: SyntaxInfo -> PTerm -> PTerm

16+debindApp syn t = debind (dsl_bind (dsl_info syn)) t

17+

14desugar :: SyntaxInfo -> IState -> PTerm -> PTerm

18desugar :: SyntaxInfo -> IState -> PTerm -> PTerm

15desugar syn i t = let t' = expandDo (dsl_info syn) t in

19desugar syn i t = let t' = expandDo (dsl_info syn) t in

16 t' -- addImpl i t'

20 t' -- addImpl i t'

@@ -29,6 +33,8 @@ expandDo dsl (PLet n ty v tm) = PLet n (expandDo dsl ty) (expandDo dsl v) (expan

29expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm)

33expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm)

30expandDo dsl (PApp fc t args) = PApp fc (expandDo dsl t)

34expandDo dsl (PApp fc t args) = PApp fc (expandDo dsl t)

31 (map (fmap (expandDo dsl)) args)

35 (map (fmap (expandDo dsl)) args)

36+expandDo dsl (PAppBind fc t args) = PAppBind fc (expandDo dsl t)

37+ (map (fmap (expandDo dsl)) args)

32expandDo dsl (PCase fc s opts) = PCase fc (expandDo dsl s)

38expandDo dsl (PCase fc s opts) = PCase fc (expandDo dsl s)

33 (map (pmap (expandDo dsl)) opts)

39 (map (pmap (expandDo dsl)) opts)

34expandDo dsl (PEq fc l r) = PEq fc (expandDo dsl l) (expandDo dsl r)

40expandDo dsl (PEq fc l r) = PEq fc (expandDo dsl l) (expandDo dsl r)

@@ -44,7 +50,8 @@ expandDo dsl (PRewrite fc r t ty)

44 = PRewrite fc r (expandDo dsl t) ty

50 = PRewrite fc r (expandDo dsl t) ty

45expandDo dsl (PGoal fc r n sc)

51expandDo dsl (PGoal fc r n sc)

46 = PGoal fc (expandDo dsl r) n (expandDo dsl sc)

52 = PGoal fc (expandDo dsl r) n (expandDo dsl sc)

53+expandDo dsl (PDoBlock ds)

47−expandDo dsl (PDoBlock ds) = expandDo dsl $ block (dsl_bind dsl) ds

54+ = expandDo dsl $ debind (dsl_bind dsl) (block (dsl_bind dsl) ds)

48 where

55 where

49 block b [DoExp fc tm] = tm

56 block b [DoExp fc tm] = tm

50 block b [a] = PElabError (Msg "Last statement in do block must be an expression")

57 block b [a] = PElabError (Msg "Last statement in do block must be an expression")

@@ -114,3 +121,45 @@ unIdiom ap pure fc e@(PApp _ _ _) = let f = getFn e in

114

121

115unIdiom ap pure fc e = PApp fc pure [pexp e]

122unIdiom ap pure fc e = PApp fc pure [pexp e]

116

123

124+debind :: PTerm -> PTerm -> PTerm

125+-- For every arg which is an AppBind, lift it out

126+debind b tm = let (tm', (bs, _)) = runState (db' tm) ([], 0) in

127+ bindAll (reverse bs) tm'

128+ where

129+ db' :: PTerm -> State ([(Name, FC, PTerm)], Int) PTerm

130+ db' (PAppBind fc t args)

131+ = do args' <- dbs args

132+ (bs, n) <- get

133+ let nm = MN n ("bindApp" ++ show n)

134+ put ((nm, fc, PApp fc t args') : bs, n+1)

135+ return (PRef fc nm)

136+ db' (PApp fc t args)

137+ = do args' <- mapM dbArg args

138+ return (PApp fc t args')

139+ db' (PLam n ty sc) = return (PLam n ty (debind b sc))

140+ db' (PLet n ty v sc) = do v' <- db' v

141+ return (PLet n ty v' (debind b sc))

142+ db' (PCase fc s opts) = do s' <- db' s

143+ return (PCase fc s' (map (pmap (debind b)) opts))

144+ db' (PPair fc l r) = do l' <- db' l

145+ r' <- db' r

146+ return (PPair fc l' r')

147+ db' (PDPair fc l t r) = do l' <- db' l

148+ r' <- db' r

149+ return (PDPair fc l' t r')

150+ db' t = return t -- TODO, finish

151+

152+ dbArg a = do t' <- db' (getTm a)

153+ return (a { getTm = t' })

154+

155+ dbs [] = return []

156+ dbs (a : as) = do let t = getTm a

157+ t' <- db' t

158+ as' <- dbs as

159+ return (a { getTm = t' } : as')

160+

161+ bindAll [] tm = tm

162+ bindAll ((n, fc, t) : bs) tm

163+ = PApp fc b [pexp t, pexp (PLam n Placeholder (bindAll bs tm))]

164+

165+

src/Idris/IBC.hs+8

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

1400 put x2

1401 put x3

1402 put x4

1403+ PAppBind x1 x2 x3 -> do putWord8 32

1404+ put x1

1405+ put x2

1406+ put x3

1403 get

1407 get

1404 = do i <- getWord8

1408 = do i <- getWord8

1405 case i of

1409 case i of

@@ -1494,6 +1498,10 @@ instance Binary PTerm where

1494 x3 <- get

1498 x3 <- get

1495 x4 <- get

1499 x4 <- get

1496 return (PGoal x1 x2 x3 x4)

1500 return (PGoal x1 x2 x3 x4)

1501+ 32 -> do x1 <- get

1502+ x2 <- get

1503+ x3 <- get

1504+ return (PAppBind x1 x2 x3)

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

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

1498

1506

1499instance (Binary t) => Binary (PTactic' t) where

1507instance (Binary t) => Binary (PTactic' t) where

src/Idris/ParseExpr.hs+9−3

@@ -138,6 +138,7 @@ extension syn (Rule ssym ptm _)

138 update ns (PLet n ty val sc) = PLet (updateB ns n) (update ns ty) (update ns val)

139 (update (dropn n ns) sc)

140 update ns (PApp fc t args) = PApp fc (update ns t) (map (fmap (update ns)) args)

141+ update ns (PAppBind fc t args) = PAppBind fc (update ns t) (map (fmap (update ns)) args)

141 update ns (PCase fc c opts) = PCase fc (update ns c) (map (pmap (update ns)) opts)

142 update ns (PCase fc c opts) = PCase fc (update ns c) (map (pmap (update ns)) opts)

142 update ns (PPair fc l r) = PPair fc (update ns l) (update ns r)

143 update ns (PPair fc l r) = PPair fc (update ns l) (update ns r)

143 update ns (PDPair fc l t r) = PDPair fc (update ns l) (update ns t) (update ns r)

144 update ns (PDPair fc l t r) = PDPair fc (update ns l) (update ns t) (update ns r)

@@ -185,7 +186,7 @@ internalExpr syn =

185 <|> rewriteTerm syn

186 <|> rewriteTerm syn

186 <|> try(pi syn)

187 <|> try(pi syn)

187 <|> doBlock syn

188 <|> doBlock syn

188− <|> simpleExpr syn

189+ <|> do simpleExpr syn

189 <?> "expression"

190 <?> "expression"

190

191

191{- | Parses a case expression

192{- | Parses a case expression

@@ -268,8 +269,10 @@ simpleExpr syn =

268 <|> caseExpr syn

269 <|> caseExpr syn

269 <|> do reserved "Type"; return PType

270 <|> do reserved "Type"; return PType

270 <|> do fc <- getFC

271 <|> do fc <- getFC

272+ bang <- option False (do lchar '!'; return True)

271 x <- fnName

273 x <- fnName

274+ if bang then return (PAppBind fc (PRef fc x) [])

272− return (PRef fc x)

275+ else return (PRef fc x)

273 <|> try (listExpr syn)

276 <|> try (listExpr syn)

274 <|> try (comprehension syn)

277 <|> try (comprehension syn)

275 <|> alt syn

278 <|> alt syn

@@ -479,7 +482,10 @@ app syn = do f <- reserved "mkForeign"

479 fc <- getFC

482 fc <- getFC

480 args <- some (do notEndApp; arg syn)

483 args <- some (do notEndApp; arg syn)

481 i <- get

484 i <- get

485+ case f of

486+ PAppBind fc ref [] ->

482− return (dslify i $ PApp fc f args)

487+ return (dslify i (PAppBind fc ref args))

488+ _ -> return (dslify i (PApp fc f args))

483 <?> "function application"

489 <?> "function application"

484 where

490 where

485 dslify :: IState -> PTerm -> PTerm

491 dslify :: IState -> PTerm -> PTerm

src/Idris/ParseOps.hs+5−1

@@ -34,12 +34,16 @@ import qualified Data.ByteString.UTF8 as UTF8

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

35table fixes

36 = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN "-"))

37− [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (BI 0))]), pexp x])]]

37+ [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (BI 0))]), pexp x])],

38+ [prefix "!" (\fc x -> bindApp fc x)]]

38 ++ toTable (reverse fixes) ++

39 ++ toTable (reverse fixes) ++

39 [[backtick],

40 [[backtick],

40 [binary "=" PEq AssocLeft],

41 [binary "=" PEq AssocLeft],

41 [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]]

42 [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]]

44+bindApp _ (PApp fc ref@(PRef _ _) args) = PAppBind fc ref args

45+bindApp fc t = PAppBind fc t []

46+

43{- |Calculates table for fixtiy declarations -}

47{- |Calculates table for fixtiy declarations -}

44toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm

48toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm

45toTable fs = map (map toBin)

49toTable fs = map (map toBin)

src/Idris/Parser.hs+1−1

@@ -137,7 +137,7 @@ decl syn = do notEndBlock

137 declBody' :: IdrisParser [PDecl]

138 declBody' = do d <- decl' syn

139 i <- get

140− let d' = fmap (desugar syn i) d

140+ let d' = fmap (debindApp syn . (desugar syn i)) d

141 return [d']

142

143{- | Parses a top-level declaration with possible syntax sugar