a7d08ef · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

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

a7d08efEdwin Brady15 years ago

interp.idr+1−1

compare with master

unifiedsplit

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

51}

53test : Nat;

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

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

56natToStr : Nat -> String;

57natToStr O = "O";

src/Idris/AbsSyntax.hs+17−3

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

160 | PSet

161 | PConstant Const

162 | 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

163

170

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

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

165 | PExp { getTm :: t }

172 | PExp { getTm :: t }

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

167

174

168type PArg = PArg' PTerm

175type PArg = PArg' PTerm

169

176

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"])

171

184

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

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

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

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

187+ dsl_info :: DSL }

174 deriving Show

188 deriving Show

175

189

176−defaultSyntax = Syn [] []

190+defaultSyntax = Syn [] [] initDSL

177

191

178--- Pretty printing declarations and terms

192--- Pretty printing declarations and terms

179

193

src/Idris/ElabDecls.hs+1

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

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

236 solve

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

238+ elab' (PElabError e) = fail e

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

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

239

240

240 elabArgs [] _ = return ()

241 elabArgs [] _ = return ()

src/Idris/Parser.hs+45−5

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

112

113pFullExpr :: SyntaxInfo -> IParser PTerm

114pFullExpr syn

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

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

116 i <- getState

117− return (addImpl i x)

117+ return $ desugar syn i x

118

119pDecl :: SyntaxInfo -> IParser [PDecl]

120pDecl syn

121 = do d <- pDecl' syn

122 i <- getState

123− return [fmap (addImpl i) d]

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

124+ return [d']

124 <|> try (pUsing syn)

125 <|> try (pUsing syn)

125 <|> try (pParams syn)

126 <|> try (pParams syn)

126 <|> try (do reserved "import"

127 <|> try (do reserved "import"

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

132pFunDecl syn

133pFunDecl syn

133 = try (do d <- pFunDecl' syn

134 = try (do d <- pFunDecl' syn

134 i <- getState

135 i <- getState

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

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

137+ return [d'])

136

138

137--------- Top Level Declarations ---------

139--------- Top Level Declarations ---------

138

140

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

202 <|> pSimpleExpr syn

204 <|> pSimpleExpr syn

203 <|> try (pLambda syn)

205 <|> try (pLambda syn)

204 <|> try (pPi syn)

206 <|> try (pPi syn)

205−

207+ <|> try (pDoBlock syn)

208+

206pfName = try iName

209pfName = try iName

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

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

208

211

209pSimpleExpr syn =

212pSimpleExpr syn =

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

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

211 return $ PQuote t)

214 return $ PQuote t)

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

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

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

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

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

214 return (PPair l r))

218 return (PPair l r))

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

267bindList b [] sc = sc

271bindList b [] sc = sc

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

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

269

273

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+

270pConstant :: IParser Const

287pConstant :: IParser Const

271pConstant = do reserved "Int"; return IType

288pConstant = do reserved "Int"; return IType

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

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

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

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

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

377 return tm'

394 return tm'

378

395

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+

379

419