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

git.iko.soy/Idris-dev

Change '!' syntax and semantics to be uniform

! now prefixes a simple expression (most likely a name or a bracketed application). !x means that the expression x (of type 'm a') will be bound using >>= in the current scope. i.e. foo !x becomes x >>= (\tmp => foo tmp)

commit9b74595de36d58fb039bdfabd0b05da630bbc18e authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 18 Oct 2013, 17:44 (13 years ago) parent1aa559f

5 files changed+27−29

compare with master

unifiedsplit

effects/Effects.idr+1−1 src/Idris/DSL.hs+12−9 src/Idris/ElabTerm.hs+1−1 src/Idris/ParseExpr.hs+12−13 src/Idris/ParseOps.hs+1−5

effects/Effects.idr+1−1

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

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

134134

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

136136

src/Idris/DSL.hs+12−9

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

1313import Debug.Trace

1414

1515debindApp :: 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

1717

1818desugar :: SyntaxInfo -> IState -> PTerm -> PTerm

1919desugar 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

127127 bindAll (reverse bs) tm'

128128 where

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

130+ db' (PAppBind _ (PApp fc t args) [])

131+ = db' (PAppBind fc t args)

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

133+ = do args' <- dbs args

134+ (bs, n) <- get

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

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

137+ return (PRef fc nm)

136138 db' (PApp fc t args)

137− = do args' <- mapM dbArg args

138− return (PApp fc t args')

139+ = do t' <- db' t

140+ args' <- mapM dbArg args

141+ return (PApp fc t' args')

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

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

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

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

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

148151 r' <- db' r

149152 return (PDPair fc l' t r')

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

153+ db' t = return t

151154

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

153156 return (a { getTm = t' })

src/Idris/ElabTerm.hs+1−1

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

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

515515 elab' ina t

516516 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

518518

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

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

src/Idris/ParseExpr.hs+12−13

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

3131import qualified Data.Text as T

3232import qualified Data.ByteString.UTF8 as UTF8

3333

34+import Debug.Trace

35+

3436-- | Allow implicit type declarations

3537allowImp :: SyntaxInfo -> SyntaxInfo

3638allowImp syn = syn { implicitAllowed = True }

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

186188 <|> rewriteTerm syn

187189 <|> try(pi syn)

188190 <|> doBlock syn

189− <|> do s <- 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−

191+ <|> simpleExpr syn

195192 <?> "expression"

196193

197194{- | Parses a case expression

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

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

276273 <|> do fc <- getFC

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

281276 <|> try (listExpr syn)

282277 <|> try (comprehension syn)

283278 <|> alt syn

284279 <|> idiom syn

280+ <|> do lchar '!'

281+ s <- simpleExpr syn

282+ fc <- getFC

283+ return (PAppBind fc s [])

285284 <|> do lchar '('

286285 bracketed (disallowImp syn)

287286 <|> do c <- constant

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

487486 fc <- getFC

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

489488 i <- get

490− case f of

491− PAppBind fc ref [] ->

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

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

489+-- case f of

490+-- PAppBind fc ref [] ->

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

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

494493 <?> "function application"

495494 where

496495 dslify :: IState -> PTerm -> PTerm

src/Idris/ParseOps.hs+1−5

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

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

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

3938 ++ toTable (reverse fixes) ++

4039 [[backtick],

4140 [binary "=" PEq AssocLeft],

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

4342

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

45−bindApp fc t = PAppBind fc t []

46−

4743{- |Calculates table for fixtiy declarations -}

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

4945toTable fs = map (map toBin)