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

effects/Effects.idr+2

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

130130 EffM m xs xs' a

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

132132

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

134+

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

134136

135137implicit

src/Idris/AbsSyntax.hs+7

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

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

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

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

702707 en (PRef fc n)

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

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

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

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

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

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

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

712718 en t = t

713719

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

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

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

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

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

833840 pri (PTyped l r) = pri l

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

src/Idris/AbsSyntaxTree.hs+14

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

533533 | PLet Name PTerm PTerm PTerm

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

535535 | PApp FC PTerm [PArg]

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

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

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

538539 | PTrue FC

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

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

574575 (fmap (mapPT f) g)

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

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

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

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

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

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

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

959961 | not impl = pretty f

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

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

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

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

962966 let [l, r] = getExps args in

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

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

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

11441148 | not impl = se p bnd hd

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

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

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

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

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

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

11501156 = let args = getExps as in

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

11521158 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

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

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

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

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

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

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

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

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

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

12421253 size (PTrue fc) = 1

12431254 size (PFalse fc) = 1

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

12741285 ni env (PRef _ n)

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

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

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

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

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

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

13001312 [] -> [n]

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

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

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

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

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

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

13261339 [] -> [n]

13271340 _ -> []

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

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

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

13311345 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

99import Core.TT

1010import Core.Evaluate

1111

12+import Control.Monad.State

1213import Debug.Trace

1314

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

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

17+

1418desugar :: SyntaxInfo -> IState -> PTerm -> PTerm

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

1620 t' -- addImpl i t'

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

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

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

3135 (map (fmap (expandDo dsl)) args)

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

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

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

3339 (map (pmap (expandDo dsl)) opts)

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

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

4450 = PRewrite fc r (expandDo dsl t) ty

4551expandDo dsl (PGoal fc r n sc)

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

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

53+expandDo dsl (PDoBlock ds)

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

4855 where

4956 block b [DoExp fc tm] = tm

5057 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

114121

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

116123

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

14001400 put x2

14011401 put x3

14021402 put x4

1403+ PAppBind x1 x2 x3 -> do putWord8 32

1404+ put x1

1405+ put x2

1406+ put x3

14031407 get

14041408 = do i <- getWord8

14051409 case i of

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

14941498 x3 <- get

14951499 x4 <- get

14961500 return (PGoal x1 x2 x3 x4)

1501+ 32 -> do x1 <- get

1502+ x2 <- get

1503+ x3 <- get

1504+ return (PAppBind x1 x2 x3)

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

14981506

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

src/Idris/ParseExpr.hs+9−3

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

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

139139 (update (dropn n ns) sc)

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

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

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

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

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

185186 <|> rewriteTerm syn

186187 <|> try(pi syn)

187188 <|> doBlock syn

188− <|> simpleExpr syn

189+ <|> do simpleExpr syn

189190 <?> "expression"

190191

191192{- | Parses a case expression

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

268269 <|> caseExpr syn

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

270271 <|> do fc <- getFC

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

271273 x <- fnName

272− return (PRef fc x)

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

275+ else return (PRef fc x)

273276 <|> try (listExpr syn)

274277 <|> try (comprehension syn)

275278 <|> alt syn

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

479482 fc <- getFC

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

481484 i <- get

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

485+ case f of

486+ PAppBind fc ref [] ->

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

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

483489 <?> "function application"

484490 where

485491 dslify :: IState -> PTerm -> PTerm

src/Idris/ParseOps.hs+5−1

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

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

3535table fixes

3636 = [[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)]]

3839 ++ toTable (reverse fixes) ++

3940 [[backtick],

4041 [binary "=" PEq AssocLeft],

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

4243

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

45+bindApp fc t = PAppBind fc t []

46+

4347{- |Calculates table for fixtiy declarations -}

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

4549toTable fs = map (map toBin)

src/Idris/Parser.hs+1−1

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

137137 declBody' :: IdrisParser [PDecl]

138138 declBody' = do d <- decl' syn

139139 i <- get

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

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

141141 return [d']

142142

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