a7d08ef · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

do notation (just IO at the moment - not yet overloadable)

commita7d08ef45c47f7ff11a49d40df9008ac138791f7 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSat 15 Oct 2011, 18:35 (15 years ago) parent1c9392e

4 files changed+64−9

compare with master

unifiedsplit

interp.idr+1−1 src/Idris/AbsSyntax.hs+17−3 src/Idris/ElabDecls.hs+1 src/Idris/Parser.hs+45−5

interp.idr+1−1

@@ -51,7 +51,7 @@ using (G : Vect Ty n) {

5151}

5252

5353test : Nat;

54−test = interp Empty eAdd (S (S O)) (S (S O));

54+test = interp Empty eProg (S (S O)) (S (S O));

5555

5656natToStr : Nat -> String;

5757natToStr O = "O";

src/Idris/AbsSyntax.hs+17−3

@@ -160,6 +160,13 @@ data PTerm = PQuote Raw

160160 | PSet

161161 | PConstant Const

162162 | Placeholder

163+ | PDoBlock [PDo]

164+ | PReturn

165+ | PElabError String -- error to report on elaboration

166+

167+data PDo = DoExp PTerm

168+ | DoBind Name PTerm

169+ | DoLet Name PTerm

163170

164171data PArg' t = PImp { pname :: Name, getTm :: t }

165172 | PExp { getTm :: t }

@@ -167,13 +174,20 @@ data PArg' t = PImp { pname :: Name, getTm :: t }

167174

168175type PArg = PArg' PTerm

169176

170−-- Syntactic sugar info (TODO: namespaces, parameters, modules)

177+-- Syntactic sugar info (TODO: namespaces, modules)

178+

179+data DSL = DSL { dsl_bind :: Name,

180+ dsl_return :: Name }

181+ deriving Show

182+

183+initDSL = DSL (UN ["io_bind"]) (UN ["io_return"])

171184

172185data SyntaxInfo = Syn { using :: [(Name, PTerm)],

173− syn_params :: [(Name, PTerm)] }

186+ syn_params :: [(Name, PTerm)],

187+ dsl_info :: DSL }

174188 deriving Show

175189

176−defaultSyntax = Syn [] []

190+defaultSyntax = Syn [] [] initDSL

177191

178192--- Pretty printing declarations and terms

179193

src/Idris/ElabDecls.hs+1

@@ -235,6 +235,7 @@ elab info pattern tm = do elab' tm

235235 = do simple_app (elab' f) (elab' (getTm arg))

236236 solve

237237 elab' Placeholder = fail $ "Can't deal with a placeholder here"

238+ elab' (PElabError e) = fail e

238239 elab' x = fail $ "Not implemented " ++ show x

239240

240241 elabArgs [] _ = return ()

src/Idris/Parser.hs+45−5

@@ -112,15 +112,16 @@ collect [] = []

112112

113113pFullExpr :: SyntaxInfo -> IParser PTerm

114114pFullExpr syn

115− = do x <- pExpr syn; eof;

115+ = do x <- pExpr syn; eof;

116116 i <- getState

117− return (addImpl i x)

117+ return $ desugar syn i x

118118

119119pDecl :: SyntaxInfo -> IParser [PDecl]

120120pDecl syn

121121 = do d <- pDecl' syn

122122 i <- getState

123− return [fmap (addImpl i) d]

123+ let d' = fmap (desugar syn i) d

124+ return [d']

124125 <|> try (pUsing syn)

125126 <|> try (pParams syn)

126127 <|> try (do reserved "import"

@@ -132,7 +133,8 @@ pFunDecl :: SyntaxInfo -> IParser [PDecl]

132133pFunDecl syn

133134 = try (do d <- pFunDecl' syn

134135 i <- getState

135− return [fmap (addImpl i) d])

136+ let d' = fmap (desugar syn i) d

137+ return [d'])

136138

137139--------- Top Level Declarations ---------

138140

@@ -202,13 +204,15 @@ pExpr' syn

202204 <|> pSimpleExpr syn

203205 <|> try (pLambda syn)

204206 <|> try (pPi syn)

205−

207+ <|> try (pDoBlock syn)

208+

206209pfName = try iName

207210 <|> do lchar '('; o <- operator; lchar ')'; return (UN [o])

208211

209212pSimpleExpr syn =

210213 try (do symbol "!["; t <- pTerm; lchar ']'

211214 return $ PQuote t)

215+ <|> try (do reserved "return"; return PReturn)

212216 <|> try (do x <- pfName; return (PRef x))

213217 <|> try (do lchar '('; l <- pExpr syn; lchar ','; r <- pExpr syn; lchar ')';

214218 return (PPair l r))

@@ -267,6 +271,19 @@ tyOptDeclList syn = sepBy1 (do x <- pfName; t <- option Placeholder (pTSig syn)

267271bindList b [] sc = sc

268272bindList b ((n, t):bs) sc = b n t (bindList b bs sc)

269273

274+pDoBlock syn

275+ = do reserved "do"; lchar '{'

276+ ds <- endBy1 (pDo syn) (lchar ';')

277+ lchar '}'

278+ return (PDoBlock ds)

279+

280+pDo syn

281+ = try (do i <- iName; symbol "<-"; e <- pExpr syn;

282+ return (DoBind i e))

283+ <|> try (do reserved "let"; i <- iName; reservedOp "="; e <- pExpr syn

284+ return (DoLet i e))

285+ <|> try (do e <- pExpr syn; return (DoExp e))

286+

270287pConstant :: IParser Const

271288pConstant = do reserved "Int"; return IType

272289 <|> do reserved "Char"; return ChType

@@ -376,4 +393,27 @@ implicit syn n ptm

376393 setState (i { idris_implicits = addDef n impdata (idris_implicits i) })

377394 return tm'

378395

396+desugar :: SyntaxInfo -> IState -> PTerm -> PTerm

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

398+ addImpl i t'

399+

400+expandDo :: DSL -> PTerm -> PTerm

401+expandDo dsl (PLam n ty tm) = PLam n (expandDo dsl ty) (expandDo dsl tm)

402+expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm)

403+expandDo dsl (PApp t args) = PApp (expandDo dsl t)

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

405+expandDo dsl (PPair l r) = PPair (expandDo dsl l) (expandDo dsl r)

406+expandDo dsl (PHidden t) = PHidden (expandDo dsl t)

407+expandDo dsl PReturn = PRef (dsl_return dsl)

408+expandDo dsl (PDoBlock ds) = expandDo dsl $ block (dsl_bind dsl) ds

409+ where

410+ block b [DoExp tm] = tm

411+ block b [a] = PElabError "Last statement in do block must be an expression"

412+ block b (DoBind n tm : rest)

413+ = PApp (PRef b) [PExp tm, PExp (PLam n Placeholder (block b rest))]

414+ block b (DoExp tm : rest)

415+ = PApp (PRef b) [PExp tm, PExp (PLam (MN 0 "bindx") Placeholder (block b rest))]

416+expandDo dsl t = t

417+

418+

379419