9b74595 · Idris-dev · git.iko.soy

effects/Effects.idr+1−1

compare with master

unifiedsplit

@@ -130,7 +130,7 @@ 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)!

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

134

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

136

src/Idris/DSL.hs+12−9

@@ -13,7 +13,7 @@ import Control.Monad.State

13import Debug.Trace

14

15debindApp :: SyntaxInfo -> PTerm -> PTerm

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

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

17

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

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

@@ -127,15 +127,18 @@ 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 _ (PApp fc t args) [])

131+ = db' (PAppBind fc t args)

130 db' (PAppBind fc t args)

132 db' (PAppBind fc t args)

131− = do args' <- dbs args

133+ = do args' <- dbs args

132− (bs, n) <- get

134+ (bs, n) <- get

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

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

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

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

135− return (PRef fc nm)

137+ return (PRef fc nm)

136 db' (PApp fc t args)

138 db' (PApp fc t args)

139+ = do t' <- db' t

137− = do args' <- mapM dbArg args

140+ args' <- mapM dbArg args

138− return (PApp fc t args')

141+ return (PApp fc t' args')

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

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

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

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

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

144 return (PLet n ty v' (debind b sc))

@@ -147,7 +150,7 @@ debind b tm = let (tm', (bs, _)) = runState (db' tm) ([], 0) in

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

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

148 r' <- db' r

151 r' <- db' r

149 return (PDPair fc l' t r')

152 return (PDPair fc l' t r')

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

153+ db' t = return t

151

154

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

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

153 return (a { getTm = t' })

156 return (a { getTm = t' })

src/Idris/ElabTerm.hs+1−1

@@ -514,7 +514,7 @@ elab ist info pattern tcgen fn tm

514 elab' ina (PUnifyLog t) = do unifyLog True

515 elab' ina t

516 unifyLog False

517− elab' ina x = fail $ "Something's gone wrong. Did you miss a semi-colon somewhere?"

517+ elab' ina x = fail $ "Unelaboratable syntactic form " ++ show x

518

519 caseBlock :: FC -> Name -> [(Name, Binder Term)] ->

520 [(PTerm, PTerm)] -> [PClause]

src/Idris/ParseExpr.hs+12−13

@@ -31,6 +31,8 @@ import qualified Data.HashSet as HS

31import qualified Data.Text as T

32import qualified Data.ByteString.UTF8 as UTF8

33

34+import Debug.Trace

35+

34-- | Allow implicit type declarations

36-- | Allow implicit type declarations

35allowImp :: SyntaxInfo -> SyntaxInfo

37allowImp :: SyntaxInfo -> SyntaxInfo

36allowImp syn = syn { implicitAllowed = True }

38allowImp syn = syn { implicitAllowed = True }

@@ -186,12 +188,7 @@ internalExpr syn =

186 <|> rewriteTerm syn

188 <|> rewriteTerm syn

187 <|> try(pi syn)

189 <|> try(pi syn)

188 <|> doBlock syn

190 <|> doBlock syn

189− <|> do s <- simpleExpr syn

191+ <|> simpleExpr syn

190− fc <- getFC

191− bang <- option False (do lchar '!'; return True)

192− if bang then return (PAppBind fc s [])

193− else return s

194−

195 <?> "expression"

192 <?> "expression"

196

193

197{- | Parses a case expression

194{- | Parses a case expression

@@ -275,13 +272,15 @@ simpleExpr syn =

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

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

276 <|> do fc <- getFC

273 <|> do fc <- getFC

277 x <- fnName

274 x <- fnName

278− bang <- option False (do lchar '!'; return True)

279− if bang then return (PAppBind fc (PRef fc x) [])

280− else return (PRef fc x)

275+ return (PRef fc x)

281 <|> try (listExpr syn)

276 <|> try (listExpr syn)

282 <|> try (comprehension syn)

277 <|> try (comprehension syn)

283 <|> alt syn

278 <|> alt syn

284 <|> idiom syn

279 <|> idiom syn

280+ <|> do lchar '!'

281+ s <- simpleExpr syn

282+ fc <- getFC

283+ return (PAppBind fc s [])

285 <|> do lchar '('

284 <|> do lchar '('

286 bracketed (disallowImp syn)

285 bracketed (disallowImp syn)

287 <|> do c <- constant

286 <|> do c <- constant

@@ -487,10 +486,10 @@ app syn = do f <- reserved "mkForeign"

487 fc <- getFC

486 fc <- getFC

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

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

489 i <- get

488 i <- get

490− case f of

489+-- case f of

491− PAppBind fc ref [] ->

490+-- PAppBind fc ref [] ->

492− return (dslify i (PAppBind fc ref args))

491+-- return (dslify i (PAppBind fc ref args))

493− _ -> return (dslify i (PApp fc f args))

492+ return (dslify i (PApp fc f args))

494 <?> "function application"

493 <?> "function application"

495 where

494 where

496 dslify :: IState -> PTerm -> PTerm

495 dslify :: IState -> PTerm -> PTerm

src/Idris/ParseOps.hs+1−5

@@ -34,16 +34,12 @@ 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)]]

39 ++ toTable (reverse fixes) ++

38 ++ toTable (reverse fixes) ++

40 [[backtick],

39 [[backtick],

41 [binary "=" PEq AssocLeft],

40 [binary "=" PEq AssocLeft],

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

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

43

42

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

45−bindApp fc t = PAppBind fc t []

46−

47{- |Calculates table for fixtiy declarations -}

43{- |Calculates table for fixtiy declarations -}

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

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

49toTable fs = map (map toBin)

45toTable fs = map (map toBin)