5a8536a · Idris-dev · git.iko.soy

CONTRIBUTORS+1

compare with master

unifiedsplit

@@ -15,6 +15,7 @@ Jason Dagit

15Guglielmo Fachini

16Simon Fowler

17Google

18+Zack Grannan

18Cezar Ionescu

19Cezar Ionescu

19Heath Johns

20Heath Johns

20Irene Knapp

21Irene Knapp

idris.cabal+3

@@ -538,6 +538,9 @@ Extra-source-files:

538 test/interactive009/input

539 test/interactive009/*.idr

540 test/interactive009/expected

541+ test/interactive010/expected

542+ test/interactive010/input

543+ test/interactive010/run

541

544

542 test/io001/run

545 test/io001/run

543 test/io001/*.idr

546 test/io001/*.idr

src/Idris/REPLParser.hs+12−3

@@ -174,10 +174,9 @@ pCmd :: P.IdrisParser (Either String Command)

174pCmd = choice [ do c <- cmd names; parser c

175 | (names, _, _, parser) <- parserCommandsForHelp ++ parserCommands ]

176 <|> unrecognized

177− <|> nop

177+ <|> nop

178 <|> eval

179 where nop = do eof; return (Right NOP)

180− eval = exprArg Eval ""

181 unrecognized = do

180 unrecognized = do

182 P.lchar ':'

181 P.lchar ':'

183 cmd <- many anyChar

182 cmd <- many anyChar

@@ -205,16 +204,26 @@ noArgs cmd name = do

205

204

206 emptyArgs <|> failure

205 emptyArgs <|> failure

207

206

207+eval :: P.IdrisParser (Either String Command)

208+eval = do

209+ t <- P.fullExpr defaultSyntax

210+ return $ Right (Eval t)

211+

208exprArg :: (PTerm -> Command) -> String -> P.IdrisParser (Either String Command)

212exprArg :: (PTerm -> Command) -> String -> P.IdrisParser (Either String Command)

209exprArg cmd name = do

213exprArg cmd name = do

210 let noArg = do

214 let noArg = do

211 eof

215 eof

212 return $ Left ("Usage is :" ++ name ++ " <expression>")

216 return $ Left ("Usage is :" ++ name ++ " <expression>")

213

217

218+ let justOperator = do

219+ (op, fc) <- P.operatorFC

220+ eof

221+ return $ Right $ cmd (PRef fc [] (sUN op))

222+

214 let properArg = do

223 let properArg = do

215 t <- P.fullExpr defaultSyntax

224 t <- P.fullExpr defaultSyntax

216 return $ Right (cmd t)

225 return $ Right (cmd t)

217− try noArg <|> properArg

226+ try noArg <|> try justOperator <|> properArg

218

227

219

228

220

229

test/interactive010/expectednew file+22

@@ -0,0 +1,22 @@

1+Prelude.List.(++) : List a -> List a -> List a

2+Prelude.Strings.(++) : String -> String -> String

3+Prelude.Classes./ : (__pi_arg : Float) →

4+ (__pi_arg1 : Float) → Float

5+Usage is :doc <functionname>

6+Usage is :wc <functionname>

7+Usage is :printdef <functionname>

8+prim__divFloat

9+Prelude.Classes./

10+

11+ : Float -> Float -> Float

12+(input):1:1: error: expected: ":",

13+ dependent type signature,

14+ end of input

15+/<EOF>

16+^

17+(input):1:1: error: expected: ":",

18+ dependent type signature,

19+ end of input

20+++<EOF>

21+^

22+prim__divFloat

test/interactive010/inputnew file+10

@@ -0,0 +1,10 @@

1+:type ++

2+:core /

3+:doc +

4+:wc +

5+:printdef -

6+:spec /

7+:patt /

8+/

9+++

10+:whnf /

test/interactive010/runnew file+2

@@ -0,0 +1,2 @@

1+#!/usr/bin/env bash

2+idris --quiet --nobanner --nocolor --consolewidth 80 < input