6c0ae32 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #637 from ahmadsalim/feature/pparser-trifecta

6c0ae32Edwin Brady13 years ago

idris.cabal+1−5

compare with master

unifiedsplit

@@ -299,13 +299,10 @@ Executable idris

299 Other-modules:

300 Core.CaseTree

301 , Core.Constraints

302− , Core.CoreParser

303 , Core.Elaborate

302 , Core.Elaborate

304 , Core.Evaluate

303 , Core.Evaluate

305 , Core.Execute

304 , Core.Execute

306− , Core.ProofShell

307 , Core.ProofState

305 , Core.ProofState

308− , Core.ShellParser

309 , Core.TT

306 , Core.TT

310 , Core.Typecheck

307 , Core.Typecheck

311 , Core.Unify

308 , Core.Unify

@@ -359,7 +356,6 @@ Executable idris

359 , IRTS.Java.JTypes

356 , IRTS.Java.JTypes

360 , IRTS.Java.Mangling

357 , IRTS.Java.Mangling

361 , IRTS.Java.Pom

358 , IRTS.Java.Pom

362− , IRTS.LParser

363 , IRTS.Lang

359 , IRTS.Lang

364 , IRTS.Simplified

360 , IRTS.Simplified

365

361

@@ -387,7 +383,7 @@ Executable idris

387 , haskeline >= 0.7

383 , haskeline >= 0.7

388 , language-java >= 0.2.2

384 , language-java >= 0.2.2

389 , mtl

385 , mtl

390− , parsec >= 3

386+ --, parsec >= 3

391 , parsers == 0.9

387 , parsers == 0.9

392 , pretty

388 , pretty

393 , process

389 , process

src/Core/CoreParser.hsdeleted−575

@@ -1,575 +0,0 @@

1−{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

2−

3−module Core.CoreParser(parseTerm, parseFile, parseDef, pTerm, iName,

4− idrisLexer, maybeWithNS, pDocComment, opChars) where

5−

6−import Core.TT

7−

8−import Text.ParserCombinators.Parsec

9−import Text.ParserCombinators.Parsec.Expr

10−import Text.ParserCombinators.Parsec.Language

11−import Text.ParserCombinators.Parsec.Prim

12−import Text.ParserCombinators.Parsec.Char

13−import Text.ParserCombinators.Parsec.Combinator

14−import qualified Text.ParserCombinators.Parsec.Token as PTok

15−

16−import Control.Monad.State

17−import Control.Monad.Identity

18−import Data.Char

19−import Data.List

20−import Debug.Trace

21−

22−type TokenParser a = PTok.TokenParser a

23−

24−idrisDef = haskellDef {

25− opStart = iOpStart,

26− opLetter = iOpLetter,

27− identLetter = identLetter haskellDef <|> lchar '.',

28− reservedOpNames

29− = [":", "..", "=", "\\", "|", "<-", "->", "=>", "**"],

30− reservedNames

31− = ["let", "in", "data", "codata", "record", "Type",

32− "do", "dsl", "import", "impossible",

33− "case", "of", "total", "partial", "mutual",

34− "infix", "infixl", "infixr", "rewrite",

35− "where", "with", "syntax", "proof", "postulate",

36− "using", "namespace", "class", "instance",

37− "public", "private", "abstract", "implicit",

38− "quoteGoal"]

39− }

40−

41−-- | The characters allowed in operator names

42−opChars = ":!#$%&*+./<=>?@\\^|-~"

43−

44−iOpStart = oneOf opChars

45−iOpLetter = oneOf opChars

46−-- <|> letter

47−

48−idrisLexer :: TokenParser a

49−idrisLexer = idrisMakeTokenParser idrisDef

50−

51−lexer = idrisLexer

52−

53−-- Taken from Parsec source code

54−lexWS = do i <- getInput

55− skipMany (simpleSpace <|> oneLineComment <|> multiLineComment <?> "")

56− where

57−

58− simpleSpace = skipMany1 (satisfy isSpace)

59− oneLineComment =

60− try (void $ string "--\n") <|>

61− do try (do string "--"

62− satisfy (\x -> x /= '|' && x /= '^'))

63− skipMany (satisfy (/= '\n'))

64− multiLineComment =

65− try (void $ string "{--}") <|>

66− do try (do string "{-"

67− satisfy (\x -> x /= '|' && x /= '^'))

68− inCommentMulti

69−

70− inCommentMulti

71− = do{ try (string "-}") ; return () }

72− <|> do{ multiLineComment ; inCommentMulti }

73− <|> do{ skipMany1 (noneOf startEnd) ; inCommentMulti }

74− <|> do{ oneOf startEnd ; inCommentMulti }

75− <?> "end of comment"

76− where

77− startEnd = "-}{"

78−

79−whiteSpace= PTok.whiteSpace lexer

80−lexeme = PTok.lexeme lexer

81−symbol = PTok.symbol lexer

82−natural = PTok.natural lexer

83−parens = PTok.parens lexer

84−semi = PTok.semi lexer

85−comma = PTok.comma lexer

86−identifier= PTok.identifier lexer

87−reserved = PTok.reserved lexer

88−operator = PTok.operator lexer

89−reservedOp= PTok.reservedOp lexer

90−strlit = PTok.stringLiteral lexer

91−lchar = lexeme.char

92−

93−type CParser a = GenParser Char a

94−

95−parseFile = runParser pTestFile () "(input)"

96−parseDef = runParser pDef () "(input)"

97−parseTerm = runParser pTerm () "(input)"

98−

99−pTestFile :: CParser a RProgram

100−pTestFile = do p <- many1 pDef ; eof

101− return p

102−

103−iName :: [String] -> CParser a Name

104−iName bad = maybeWithNS identifier False bad

105−

106−-- Enhances a given parser to accept an optional namespace. All possible

107−-- namespace prefixes are tried in ascending / descending order, and

108−-- identifiers of a given list fail.

109−maybeWithNS :: CParser a String -> Bool -> [String] -> CParser a Name

110−maybeWithNS parser ascend bad = do

111− i <- option "" (lookAhead identifier)

112− when (i `elem` bad) $ fail "Reserved identifier"

113− let transf = if ascend then id else reverse

114− (x, xs) <- choice $ transf (parserNoNS : parsersNS i)

115− return $ mkName (x, xs)

116− where

117− parserNoNS = do x <- parser; return (x, "")

118− parserNS ns = do xs <- string ns; lchar '.'; x <- parser; return (x, xs)

119− parsersNS i = [try (parserNS ns) | ns <- (initsEndAt (=='.') i)]

120−

121−-- List of all initial segments in ascending order of a list. Every such

122−-- initial segment ends right before an element satisfying the given

123−-- condition.

124−initsEndAt :: (a -> Bool) -> [a] -> [[a]]

125−initsEndAt p [] = []

126−initsEndAt p (x:xs) | p x = [] : x_inits_xs

127− | otherwise = x_inits_xs

128− where x_inits_xs = [x : cs | cs <- initsEndAt p xs]

129−

130−-- Create a `Name' from a pair of strings representing a base name and its

131−-- namespace.

132−mkName :: (String, String) -> Name

133−mkName (n, "") = UN n

134−mkName (n, ns) = NS (UN n) (reverse (parseNS ns))

135− where parseNS x = case span (/= '.') x of

136− (x, "") -> [x]

137− (x, '.':y) -> x : parseNS y

138−

139−pDocComment :: Char -> CParser a String

140−pDocComment c

141− = try (do string ("--")

142− char c

143− skipMany simpleSpace

144− i <- getInput

145− let (doc, rest) = span (/='\n') i

146− setInput rest

147− whiteSpace

148− return doc)

149− <|> try (do string ("{-")

150− char c

151− skipMany simpleSpace

152− i <- getInput

153− -- read to '-}'

154− let (doc, rest) = spanComment "" i

155− setInput rest

156− whiteSpace

157− return doc)

158− where spanComment acc ('-':'}':xs) = (reverse acc, xs)

159− spanComment acc (x:xs) = spanComment (x : acc) xs

160− spanComment acc [] = (acc, [])

161− simpleSpace = skipMany1 (satisfy isSpace)

162−

163−pDef :: CParser a (Name, RDef)

164−pDef = try (do x <- iName []; lchar ':'; ty <- pTerm

165− lchar '='

166− tm <- pTerm

167− lchar ';'

168− return (x, RFunction (RawFun ty tm)))

169− <|> do x <- iName []; lchar ':'; ty <- pTerm; lchar ';'

170− return (x, RConst ty)

171− <|> do (x, d) <- pData; lchar ';'

172− return (x, RData d)

173−

174−app :: CParser a (Raw -> Raw -> Raw)

175−app = do whiteSpace ; return RApp

176−

177−arrow :: CParser a (Raw -> Raw -> Raw)

178−arrow = do symbol "->" ; return $ \s t -> RBind (MN 0 "X") (Pi s) t

179−

180−pTerm :: CParser a Raw

181−pTerm = try (do chainl1 pNoApp app)

182− <|> pNoApp

183−

184−pNoApp :: CParser a Raw

185−pNoApp = try (chainr1 pExp arrow)

186− <|> pExp

187−pExp :: CParser a Raw

188−pExp = do lchar '\\'; x <- iName []; lchar ':'; ty <- pTerm

189− symbol "=>";

190− sc <- pTerm

191− return (RBind x (Lam ty) sc)

192− <|> try (do lchar '?'; x <- iName []; lchar ':'; ty <- pTerm

193− lchar '.';

194− sc <- pTerm

195− return (RBind x (Hole ty) sc))

196− <|> try (do lchar '(';

197− x <- iName []; lchar ':'; ty <- pTerm

198− lchar ')';

199− symbol "->";

200− sc <- pTerm

201− return (RBind x (Pi ty) sc))

202− <|> try (do lchar '(';

203− t <- pTerm

204− lchar ')'

205− return t)

206− <|> try (do symbol "??";

207− x <- iName []; lchar ':'; ty <- pTerm

208− lchar '=';

209− val <- pTerm

210− sc <- pTerm

211− return (RBind x (Guess ty val) sc))

212− <|> try (do reserved "let";

213− x <- iName []; lchar ':'; ty <- pTerm

214− lchar '=';

215− val <- pTerm

216− reserved "in";

217− sc <- pTerm

218− return (RBind x (Let ty val) sc))

219− <|> try (do lchar '_';

220− x <- iName []; lchar ':'; ty <- pTerm

221− lchar '.';

222− sc <- pTerm

223− return (RBind x (PVar ty) sc))

224− <|> try (do reserved "Type"

225− return RType)

226− <|> try (do x <- iName []

227− return (Var x))

228−

229−pData :: CParser a (Name, RawDatatype)

230−pData = do reserved "data"; x <- iName []; lchar ':'; ty <- pTerm; reserved "where"

231− cs <- many pConstructor

232− return (x, RDatatype x ty cs)

233−

234−pConstructor :: CParser a (Name, Raw)

235−pConstructor = do lchar '|'

236− c <- iName []; lchar ':'; ty <- pTerm

237− return (c, ty)

238−

239−------ borrowed from Parsec

240−-- (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007

241−

242−idrisMakeTokenParser languageDef

243− = PTok.TokenParser{

244− PTok.identifier = identifier

245− , PTok.reserved = reserved

246− , PTok.operator = operator

247− , PTok.reservedOp = reservedOp

248−

249− , PTok.charLiteral = charLiteral

250− , PTok.stringLiteral = stringLiteral

251− , PTok.natural = natural

252− , PTok.integer = integer

253− , PTok.float = float

254− , PTok.naturalOrFloat = naturalOrFloat

255− , PTok.decimal = decimal

256− , PTok.hexadecimal = hexadecimal

257− , PTok.octal = octal

258−

259− , PTok.symbol = symbol

260− , PTok.lexeme = lexeme

261− , PTok.whiteSpace = lexWS

262−

263− , PTok.parens = parens

264− , PTok.braces = braces

265− , PTok.angles = angles

266− , PTok.brackets = brackets

267− , PTok.squares = brackets

268− , PTok.semi = semi

269− , PTok.comma = comma

270− , PTok.colon = colon

271− , PTok.dot = dot

272− , PTok.semiSep = semiSep

273− , PTok.semiSep1 = semiSep1

274− , PTok.commaSep = commaSep

275− , PTok.commaSep1 = commaSep1

276− }

277− where

278−

279− -----------------------------------------------------------

280− -- Bracketing

281− -----------------------------------------------------------

282− parens p = between (symbol "(") (symbol ")") p

283− braces p = between (symbol "{") (symbol "}") p

284− angles p = between (symbol "<") (symbol ">") p

285− brackets p = between (symbol "[") (symbol "]") p

286−

287− semi = symbol ";"

288− comma = symbol ","

289− dot = symbol "."

290− colon = symbol ":"

291−

292− commaSep p = sepBy p comma

293− semiSep p = sepBy p semi

294−

295− commaSep1 p = sepBy1 p comma

296− semiSep1 p = sepBy1 p semi

297−

298−

299− -----------------------------------------------------------

300− -- Chars & Strings

301− -----------------------------------------------------------

302− charLiteral = lexeme (between (char '\'')

303− (char '\'' <?> "end of character")

304− characterChar )

305− <?> "character"

306−

307− characterChar = charLetter <|> charEscape

308− <?> "literal character"

309−

310− charEscape = do{ char '\\'; escapeCode }

311− charLetter = satisfy (\c -> (c /= '\'') && (c /= '\\') && (c > '\026'))

312−

313−

314−

315− stringLiteral = lexeme (

316− do{ str <- between (char '"')

317− (char '"' <?> "end of string")

318− (many stringChar)

319− ; return (foldr (maybe id (:)) "" str)

320− }

321− <?> "literal string")

322−

323− stringChar = do{ c <- stringLetter; return (Just c) }

324− <|> stringEscape

325− <?> "string character"

326−

327− stringLetter = satisfy (\c -> (c /= '"') && (c /= '\\') && (c > '\026'))

328−

329− stringEscape = do{ char '\\'

330− ; do{ escapeGap ; return Nothing }

331− <|> do{ escapeEmpty; return Nothing }

332− <|> do{ esc <- escapeCode; return (Just esc) }

333− }

334−

335− escapeEmpty = char '&'

336− escapeGap = do{ many1 space

337− ; char '\\' <?> "end of string gap"

338− }

339−

340−

341−

342− -- escape codes

343− escapeCode = charEsc <|> charNum <|> charAscii <|> charControl

344− <?> "escape code"

345−

346− charControl = do{ char '^'

347− ; code <- upper

348− ; return (toEnum (fromEnum code - fromEnum 'A'))

349− }

350−

351− charNum = do{ code <- decimal

352− <|> do{ char 'o'; number 8 octDigit }

353− <|> do{ char 'x'; number 16 hexDigit }

354− ; return (toEnum (fromInteger code))

355− }

356−

357− charEsc = choice (map parseEsc escMap)

358− where

359− parseEsc (c,code) = do{ char c; return code }

360−

361− charAscii = choice (map parseAscii asciiMap)

362− where

363− parseAscii (asc,code) = try (do{ string asc; return code })

364−

365−

366− -- escape code tables

367− escMap = zip ("abfnrtv\\\"\'") ("\a\b\f\n\r\t\v\\\"\'")

368− asciiMap = zip (ascii3codes ++ ascii2codes) (ascii3 ++ ascii2)

369−

370− ascii2codes = ["BS","HT","LF","VT","FF","CR","SO","SI","EM",

371− "FS","GS","RS","US","SP"]

372− ascii3codes = ["NUL","SOH","STX","ETX","EOT","ENQ","ACK","BEL",

373− "DLE","DC1","DC2","DC3","DC4","NAK","SYN","ETB",

374− "CAN","SUB","ESC","DEL"]

375−

376− ascii2 = ['\BS','\HT','\LF','\VT','\FF','\CR','\SO','\SI',

377− '\EM','\FS','\GS','\RS','\US','\SP']

378− ascii3 = ['\NUL','\SOH','\STX','\ETX','\EOT','\ENQ','\ACK',

379− '\BEL','\DLE','\DC1','\DC2','\DC3','\DC4','\NAK',

380− '\SYN','\ETB','\CAN','\SUB','\ESC','\DEL']

381−

382−

383− -----------------------------------------------------------

384− -- Numbers

385− -----------------------------------------------------------

386− naturalOrFloat = lexeme (natFloat) <?> "number"

387−

388− float = lexeme floating <?> "float"

389− integer = lexeme int <?> "integer"

390− natural = lexeme nat <?> "natural"

391−

392−

393− -- floats

394− floating = do{ n <- decimal

395− ; fractExponent n

396− }

397−

398−

399− natFloat = do{ char '0'

400− ; zeroNumFloat

401− }

402− <|> decimalFloat

403−

404− zeroNumFloat = do{ n <- hexadecimal <|> octal

405− ; return (Left n)

406− }

407− <|> decimalFloat

408− <|> fractFloat 0

409− <|> return (Left 0)

410−

411− decimalFloat = do{ n <- decimal

412− ; option (Left n)

413− (fractFloat n)

414− }

415−

416− fractFloat n = do{ f <- fractExponent n

417− ; return (Right f)

418− }

419−

420− fractExponent n = do{ fract <- fraction

421− ; expo <- option 1.0 exponent'

422− ; return ((fromInteger n + fract)*expo)

423− }

424− <|>

425− do{ expo <- exponent'

426− ; return ((fromInteger n)*expo)

427− }

428−

429− fraction = do{ char '.'

430− ; digits <- many1 digit <?> "fraction"

431− ; return (foldr op 0.0 digits)

432− }

433− <?> "fraction"

434− where

435− op d f = (f + fromIntegral (digitToInt d))/10.0

436−

437− exponent' = do{ oneOf "eE"

438− ; f <- sign

439− ; e <- decimal <?> "exponent"

440− ; return (power (f e))

441− }

442− <?> "exponent"

443− where

444− power e | e < 0 = 1.0/power(-e)

445− | otherwise = fromInteger (10^e)

446−

447−

448− -- integers and naturals

449− int = do{ f <- lexeme sign

450− ; n <- nat

451− ; return (f n)

452− }

453−

454− sign = (char '-' >> return negate)

455− <|> (char '+' >> return id)

456− <|> return id

457−

458− nat = zeroNumber <|> decimal

459−

460− zeroNumber = do{ char '0'

461− ; hexadecimal <|> octal <|> decimal <|> return 0

462− }

463− <?> ""

464−

465− decimal = number 10 digit

466− hexadecimal = do{ oneOf "xX"; number 16 hexDigit }

467− octal = do{ oneOf "oO"; number 8 octDigit }

468−

469− number base baseDigit

470− = do{ digits <- many1 baseDigit

471− ; let n = foldl' (\x d -> base*x + toInteger (digitToInt d)) 0 digits

472− ; seq n (return n)

473− }

474−

475− -----------------------------------------------------------

476− -- Operators & reserved ops

477− -----------------------------------------------------------

478− reservedOp name =

479− lexeme $ try $

480− do{ string name

481− ; notFollowedBy (opLetter languageDef) <?> ("end of " ++ show name)

482− }

483−

484− operator =

485− lexeme $ try $

486− do{ name <- oper

487− ; if (isReservedOp name)

488− then unexpected ("reserved operator " ++ show name)

489− else return name

490− }

491−

492− oper =

493− do{ c <- (opStart languageDef)

494− ; cs <- many (opLetter languageDef)

495− ; return (c:cs)

496− }

497− <?> "operator"

498−

499− isReservedOp name =

500− isReserved (sort (reservedOpNames languageDef)) name

501−

502−

503− -----------------------------------------------------------

504− -- Identifiers & Reserved words

505− -----------------------------------------------------------

506− reserved name =

507− lexeme $ try $

508− do{ caseString name

509− ; notFollowedBy (identLetter languageDef) <?> ("end of " ++ show name)

510− }

511−

512− caseString name

513− | caseSensitive languageDef = string name

514− | otherwise = do{ walk name; return name }

515− where

516− walk [] = return ()

517− walk (c:cs) = do{ caseChar c <?> msg; walk cs }

518−

519− caseChar c | isAlpha c = char (toLower c) <|> char (toUpper c)

520− | otherwise = char c

521−

522− msg = show name

523−

524−

525− identifier =

526− lexeme $ try $

527− do{ name <- ident

528− ; if (isReservedName name)

529− then unexpected ("reserved word " ++ show name)

530− else return name

531− }

532−

533−

534− ident

535− = do{ c <- identStart languageDef

536− ; cs <- many (identLetter languageDef)

537− ; return (c:cs)

538− }

539− <?> "identifier"

540−

541− isReservedName name

542− = isReserved theReservedNames caseName

543− where

544− caseName | caseSensitive languageDef = name

545− | otherwise = map toLower name

546−

547−

548− isReserved names name

549− = scan names

550− where

551− scan [] = False

552− scan (r:rs) = case (compare r name) of

553− LT -> scan rs

554− EQ -> True

555− GT -> False

556−

557− theReservedNames

558− | caseSensitive languageDef = sortedNames

559− | otherwise = map (map toLower) sortedNames

560− where

561− sortedNames = sort (reservedNames languageDef)

562−

563−

564−

565− -----------------------------------------------------------

566− -- White space & symbols

567− -----------------------------------------------------------

568− symbol name

569− = lexeme (string name)

570−

571− lexeme p

572− = do{ x <- p; whiteSpace; return x }

573−

574− --whiteSpace

575− whiteSpace = lexWS

src/Core/ProofShell.hsdeleted−79

@@ -1,79 +0,0 @@

1−{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, PatternGuards #-}

2−

3−module Core.ProofShell where

4−

5−import Core.Typecheck

6−import Core.Evaluate

7−import Core.TT

8−import Core.ShellParser

9−import Core.Elaborate

10−

11−import Control.Monad.State

12−import System.Console.Haskeline

13−

14−import Idris.AbsSyntaxTree (Idris)

15−

16−import Util.Pretty

17−

18−data ShellState = ShellState

19− { ctxt :: Context,

20− prf :: Maybe ProofState,

21− deferred :: [(Name, ProofState)],

22− exitNow :: Bool

23− }

24−

25−initState c = ShellState c Nothing [] False

26−

27−processCommand :: Command -> ShellState -> (ShellState, String)

28−processCommand (Theorem n ty) state

29− = case check (ctxt state) [] ty of

30− OK (gl, t) ->

31− case isType (ctxt state) [] t of

32− OK _ -> (state { prf = Just (newProof n (ctxt state) gl) }, "")

33− _ -> (state, "Goal is not a type")

34− err -> (state, show err)

35−processCommand Quit state = (state { exitNow = True }, "Bye bye")

36−processCommand (Eval t) state =

37− case check (ctxt state) [] t of

38− OK (val, ty) ->

39− let nf = normalise (ctxt state) [] val

40− tnf = normalise (ctxt state) [] ty in

41− (state, show nf ++ " : " ++ show ty)

42− err -> (state, show err)

43−processCommand (Print n) state =

44− case lookupDef n (ctxt state) of

45− [tm] -> (state, show tm)

46− _ -> (state, "No such name")

47−processCommand (Tac e) state

48− | Just ps <- prf state = case execElab () e ps of

49− OK (ES (ps', _) resp _) ->

50− if (not (done ps'))

51− then (state { prf = Just ps' }, resp)

52− else (state { prf = Nothing,

53− ctxt = addToCtxt (thname ps')

54− (pterm ps')

55− (ptype ps')

56− (context ps') }, resp)

57− err -> (state, show err)

58− | otherwise = (state, "No proof in progress")

59−

60−runShell :: ShellState -> Idris ShellState

61−runShell st = runInputT defaultSettings $ runShell' st

62− where

63− runShell' st = do (prompt, parser) <-

64− maybe (return ("TT# ", parseCommand))

65− (\st -> do outputStrLn . render . pretty $ st

66− return (show (thname st) ++ "# ", parseTactic))

67− (prf st)

68− x <- getInputLine prompt

69− cmd <- case x of

70− Nothing -> return $ Right Quit

71− Just input -> return (parser input)

72− case cmd of

73− Left err -> do outputStrLn (show err)

74− runShell' st

75− Right cmd -> do let (st', r) = processCommand cmd st

76− outputStrLn r

77− if (not (exitNow st')) then runShell' st'

78− else return st'

79−

src/Core/ShellParser.hsdeleted−73

@@ -1,73 +0,0 @@

1−{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

2−

3−module Core.ShellParser(parseCommand, parseTactic) where

4−

5−import Core.TT

6−import Core.Elaborate

7−import Core.CoreParser

8−

9−import Text.ParserCombinators.Parsec

10−import Text.ParserCombinators.Parsec.Expr

11−import Text.ParserCombinators.Parsec.Language

12−import qualified Text.ParserCombinators.Parsec.Token as PTok

13−

14−import Debug.Trace

15−

16−type TokenParser a = PTok.TokenParser a

17−

18−lexer :: TokenParser ()

19−lexer = PTok.makeTokenParser haskellDef

20−

21−whiteSpace= PTok.whiteSpace lexer

22−lexeme = PTok.lexeme lexer

23−symbol = PTok.symbol lexer

24−natural = PTok.natural lexer

25−parens = PTok.parens lexer

26−semi = PTok.semi lexer

27−comma = PTok.comma lexer

28−identifier= PTok.identifier lexer

29−reserved = PTok.reserved lexer

30−operator = PTok.operator lexer

31−reservedOp= PTok.reservedOp lexer

32−lchar = lexeme.char

33−

34−parseCommand = parse pCommand "(input)"

35−parseTactic = parse (pTactic >>= return . Tac) "(input)"

36−

37−pCommand :: Parser Command

38−pCommand = do reserved "theorem"; n <- iName []; lchar ':'; ty <- pTerm

39− return (Theorem n ty)

40− <|> do reserved "eval"; tm <- pTerm

41− return (Eval tm)

42− <|> do reserved "print"; n <- iName []; return (Print n)

43− <|> do reserved "quit";

44− return Quit

45−

46−pTactic :: Parser (Elab ())

47−pTactic = do reserved "attack"; return attack

48− <|> do reserved "claim"; n <- iName []; lchar ':'; ty <- pTerm

49− return (claim n ty)

50− <|> do reserved "regret"; return regret

51− <|> do reserved "exact"; tm <- pTerm; return (exact tm)

52− <|> do reserved "fill"; tm <- pTerm; return (fill tm)

53− <|> do reserved "apply"; tm <- pTerm; args <- many pArgType;

54− return (discard (apply tm (map (\x -> (x,0)) args)))

55− <|> do reserved "solve"; return solve

56− <|> do reserved "compute"; return compute

57− <|> do reserved "intro"; n <- iName []; return (intro (Just n))

58− <|> do reserved "forall"; n <- iName []; lchar ':'; ty <- pTerm

59− return (forall n ty)

60− <|> do reserved "arg"; n <- iName []; t <- iName []; return (arg n t)

61− <|> do reserved "patvar"; n <- iName []; return (patvar n)

62−-- <|> do reserved "patarg"; n <- iName []; t <- iName []; return (patarg n t)

63− <|> do reserved "eval"; t <- pTerm; return (eval_in t)

64− <|> do reserved "check"; t <- pTerm; return (check_in t)

65− <|> do reserved "focus"; n <- iName []; return (focus n)

66− <|> do reserved "state"; return proofstate

67− <|> do reserved "undo"; return undo

68− <|> do reserved "qed"; return (discard qed)

69−

70−pArgType :: Parser Bool

71−pArgType = do lchar '_'; return True -- implicit (machine fills in)

72− <|> do lchar '?'; return False -- user fills in

73−

src/IRTS/LParser.hsdeleted−276

@@ -1,276 +0,0 @@

1−module IRTS.LParser where

2−

3−import Idris.AbsSyntaxTree

4−import Core.CoreParser

5−import Core.TT

6−import IRTS.Lang

7−import IRTS.Simplified

8−import IRTS.Bytecode

9−import IRTS.CodegenCommon

10−import IRTS.CodegenC

11−import IRTS.CodegenJava

12−import IRTS.CodegenJavaScript

13−import IRTS.Defunctionalise

14−import Paths_idris

15−

16−import Text.ParserCombinators.Parsec

17−import Text.ParserCombinators.Parsec.Error

18−import Text.ParserCombinators.Parsec.Expr

19−import Text.ParserCombinators.Parsec.Language

20−import qualified Text.ParserCombinators.Parsec.Token as PTok

21−

22−import Data.List

23−import Control.Monad.State

24−import Debug.Trace

25−import Data.Maybe

26−import System.FilePath

27−import Idris.Error

28−

29−type TokenParser a = PTok.TokenParser a

30−

31−type LParser = GenParser Char ()

32−

33−lexer :: TokenParser ()

34−lexer = idrisLexer

35−

36−whiteSpace= PTok.whiteSpace lexer

37−lexeme = PTok.lexeme lexer

38−symbol = PTok.symbol lexer

39−natural = PTok.natural lexer

40−parens = PTok.parens lexer

41−semi = PTok.semi lexer

42−comma = PTok.comma lexer

43−identifier= PTok.identifier lexer

44−reserved = PTok.reserved lexer

45−operator = PTok.operator lexer

46−reservedOp= PTok.reservedOp lexer

47−integer = PTok.integer lexer

48−float = PTok.float lexer

49−strlit = PTok.stringLiteral lexer

50−chlit = PTok.charLiteral lexer

51−lchar = lexeme.char

52−

53−fovm :: Codegen -> OutputType -> FilePath -> IO ()

54−fovm cgn outty f

55− = do defs <- parseFOVM f

56− let (nexttag, tagged) = addTags 0 (liftAll defs)

57− ctxtIn = addAlist tagged emptyContext

58− defuns = defunctionalise nexttag ctxtIn

59− putStrLn $ showSep "\n" (map show (toAlist defuns))

60− let checked = checkDefs defuns (toAlist defuns)

61−-- print checked

62− case checked of

63− OK c -> case cgn of

64− ViaC -> codegenC c "a.out" outty ["math.h"] "" "" "" TRACE

65− ViaJava -> codegenJava [] c "a.out" [] [] outty

66− Error e -> fail (show e)

67−

68−parseFOVM :: FilePath -> IO [(Name, LDecl)]

69−parseFOVM fname = do -- putStrLn $ "Reading " ++ fname

70− fp <- readFile fname

71− case runParser pProgram () fname fp of

72− Left err -> fail (show err)

73− Right x -> return x

74−

75−pProgram :: LParser [(Name, LDecl)]

76−pProgram = do fs <- many1 pLDecl

77− eof

78− return fs

79−

80−pLDecl :: LParser (Name, LDecl)

81−pLDecl = do reserved "data"

82− n <- iName []

83− ar <- natural

84− return (n, LConstructor n (-1) (fromInteger ar))

85− <|> do reserved "fun"

86− n <- iName []

87− lchar '('

88− args <- sepBy (iName []) (lchar ',')

89− lchar ')'

90− lchar '='

91− def <- pLExp

92− return (n, LFun [] n args def)

93−

94−pLExp = buildExpressionParser optable pLExp'

95−

96−optable = [[binary "*" (\x y -> LOp (LTimes (ATInt ITNative)) [x,y]) AssocLeft,

97− binary "/" (\x y -> LOp (LSDiv (ATInt ITNative)) [x,y]) AssocLeft,

98− binary "*." (\x y -> LOp (LTimes ATFloat) [x,y]) AssocLeft,

99− binary "/." (\x y -> LOp (LSDiv ATFloat) [x,y]) AssocLeft,

100− binary "*:" (\x y -> LOp (LTimes (ATInt ITBig)) [x,y]) AssocLeft,

101− binary "/:" (\x y -> LOp (LSDiv (ATInt ITBig)) [x,y]) AssocLeft,

102− binary "*," (\x y -> LOp (LTimes (ATInt ITChar)) [x, y]) AssocLeft,

103− binary "/," (\x y -> LOp (LSDiv (ATInt ITChar)) [x, y]) AssocLeft

104− ],

105− [

106− binary "+" (\x y -> LOp (LPlus (ATInt ITNative)) [x,y]) AssocLeft,

107− binary "-" (\x y -> LOp (LMinus (ATInt ITNative)) [x,y]) AssocLeft,

108− binary "++" (\x y -> LOp LStrConcat [x,y]) AssocLeft,

109− binary "+." (\x y -> LOp (LPlus ATFloat) [x,y]) AssocLeft,

110− binary "-." (\x y -> LOp (LMinus ATFloat) [x,y]) AssocLeft,

111− binary "+:" (\x y -> LOp (LPlus (ATInt ITBig)) [x,y]) AssocLeft,

112− binary "-:" (\x y -> LOp (LMinus (ATInt ITBig)) [x,y]) AssocLeft,

113− binary "+," (\x y -> LOp (LPlus (ATInt ITChar)) [x,y]) AssocLeft,

114− binary "-," (\x y -> LOp (LMinus (ATInt ITChar)) [x,y]) AssocLeft

115− ],

116− [

117− binary "==" (\x y -> LOp (LEq (ATInt ITNative)) [x, y]) AssocNone,

118− binary "==." (\x y -> LOp (LEq ATFloat) [x, y]) AssocNone,

119− binary "<" (\x y -> LOp (LSLt (ATInt ITNative)) [x, y]) AssocNone,

120− binary "<." (\x y -> LOp (LSLt ATFloat) [x, y]) AssocNone,

121− binary ">" (\x y -> LOp (LSGt (ATInt ITNative)) [x, y]) AssocNone,

122− binary ">." (\x y -> LOp (LSGt ATFloat) [x, y]) AssocNone,

123− binary "<=" (\x y -> LOp (LSLe (ATInt ITNative)) [x, y]) AssocNone,

124− binary "<=." (\x y -> LOp (LSLe ATFloat) [x, y]) AssocNone,

125− binary ">=" (\x y -> LOp (LSGe (ATInt ITNative)) [x, y]) AssocNone,

126− binary ">=." (\x y -> LOp (LSGe ATFloat) [x, y]) AssocNone,

127−

128− binary "==:" (\x y -> LOp (LEq (ATInt ITBig)) [x, y]) AssocNone,

129− binary "<:" (\x y -> LOp (LSLt (ATInt ITBig)) [x, y]) AssocNone,

130− binary ">:" (\x y -> LOp (LSGt (ATInt ITBig)) [x, y]) AssocNone,

131− binary "<=:" (\x y -> LOp (LSLe (ATInt ITBig)) [x, y]) AssocNone,

132− binary ">=:" (\x y -> LOp (LSGe (ATInt ITBig)) [x, y]) AssocNone,

133−

134− binary "==," (\x y -> LOp (LEq (ATInt ITChar)) [x, y]) AssocNone,

135− binary "<," (\x y -> LOp (LSLt (ATInt ITChar)) [x, y]) AssocNone,

136− binary ">," (\x y -> LOp (LSGt (ATInt ITChar)) [x, y]) AssocNone,

137− binary "<=," (\x y -> LOp (LSLe (ATInt ITChar)) [x, y]) AssocNone,

138− binary ">=," (\x y -> LOp (LSGe (ATInt ITChar)) [x, y]) AssocNone

139− ]]

140−

141−binary name f assoc = Infix (do reservedOp name; return f) assoc

142−

143−pLExp' :: LParser LExp

144−pLExp' = try (do lchar '%'; pCast)

145− <|> try (do lchar '%'; pPrim)

146− <|> try (do tc <- option False (do lchar '%'; reserved "tc"; return True)

147− x <- iName [];

148− lazy <- option False (do lchar '@'; return True)

149− lchar '('

150− args <- sepBy pLExp (lchar ',')

151− lchar ')'

152− if null args

153− then if lazy then return (LLazyApp x [])

154− else return (LV (Glob x))

155− else if lazy then return (LLazyApp x args)

156− else return (LApp tc (LV (Glob x)) args))

157− <|> do lchar '('; e <- pLExp; lchar ')'; return e

158− <|> pLConst

159− <|> do reserved "let"; x <- iName []; lchar '='; v <- pLExp

160− reserved "in"; e <- pLExp

161− return (LLet x v e)

162− <|> do lchar '\\'; xs <- sepBy (iName []) (lchar ',')

163− symbol "=>"

164− e <- pLExp

165− return (LLam xs e)

166− <|> do reserved "foreign"; l <- pLang; t <- pType

167− fname <- strlit

168− lchar '('

169− fargs <- sepBy (do t' <- pType; e <- pLExp; return (t', e)) (lchar ',')

170− lchar ')'

171− return (LForeign l t fname fargs)

172− <|> pCase

173− <|> do x <- iName []

174− return (LV (Glob x))

175−

176−pLang = do reserved "C"; return LANG_C

177−

178−pType = do reserved "Int"; return (FArith (ATInt ITNative))

179− <|> do reserved "Char"; return (FArith (ATInt ITChar))

180− <|> do reserved "Float"; return (FArith ATFloat)

181− <|> do reserved "String"; return FString

182− <|> do reserved "Unit"; return FUnit

183− <|> do reserved "Ptr"; return FPtr

184− <|> do reserved "Any"; return FAny

185−

186−pCase :: LParser LExp

187−pCase = do reserved "case"; e <- pLExp; reserved "of"

188− lchar '{'

189− alts <- sepBy1 pAlt (lchar '|')

190− lchar '}'

191− return (LCase e alts)

192−

193−pCast :: LParser LExp

194−pCast = do reserved "FloatString"; lchar '('; e <- pLExp; lchar ')'

195− return (LOp LFloatStr [e])

196− <|> do reserved "StringFloat"; lchar '('; e <- pLExp; lchar ')'

197− return (LOp LStrFloat [e])

198− <|> do reserved "FloatInt"; lchar '('; e <- pLExp; lchar ')'

199− return (LOp (LFloatInt ITNative) [e])

200− <|> do reserved "IntFloat"; lchar '('; e <- pLExp; lchar ')'

201− return (LOp (LIntFloat ITNative) [e])

202− <|> do reserved "StringInt"; lchar '('; e <- pLExp; lchar ')'

203− return (LOp (LStrInt ITNative) [e])

204− <|> do reserved "IntString"; lchar '('; e <- pLExp; lchar ')'

205− return (LOp (LIntStr ITNative) [e])

206− <|> do reserved "BigInt"; lchar '('; e <- pLExp; lchar ')'

207− return (LOp (LTrunc ITBig ITNative) [e])

208− <|> do reserved "IntBig"; lchar '('; e <- pLExp; lchar ')'

209− return (LOp (LSExt ITNative ITBig) [e])

210− <|> do reserved "BigString"; lchar '('; e <- pLExp; lchar ')'

211− return (LOp (LIntStr ITBig) [e])

212− <|> do reserved "StringBig"; lchar '('; e <- pLExp; lchar ')'

213− return (LOp (LStrInt ITBig) [e])

214−

215−pPrim :: LParser LExp

216−pPrim = do reserved "StrEq"; lchar '(';

217− e <- pLExp; lchar ',';

218− e' <- pLExp; lchar ')';

219− return (LOp LStrEq [e, e'])

220− <|> do reserved "StrLt"; lchar '('

221− e <- pLExp; lchar ','; e' <- pLExp;

222− lchar ')'

223− return (LOp LStrLt [e, e'])

224− <|> do reserved "StrLen"; lchar '('; e <- pLExp; lchar ')';

225− return (LOp LStrLen [e])

226− <|> do reserved "ReadString"; lchar '('; e <- pLExp; lchar ')';

227− return (LOp LReadStr [e])

228− <|> do reserved "WriteString"; lchar '(';

229− e <- pLExp; lchar ')'

230− return (LOp LPrintStr [e])

231− <|> do reserved "WriteInt"; lchar '(';

232− e <- pLExp; lchar ')';

233− return (LOp LPrintNum [e])

234− <|> do reserved "lazy"; lchar '(';

235− e <- pLExp; lchar ')';

236− return (LLazyExp e)

237− <|> do reserved "StrHead"; lchar '('; e <- pLExp; lchar ')';

238− return (LOp LStrHead [e])

239− <|> do reserved "StrTail"; lchar '('; e <- pLExp; lchar ')';

240− return (LOp LStrTail [e])

241− <|> do reserved "StrRev"; lchar '('; e <- pLExp; lchar ')';

242− return (LOp LStrRev [e])

243− <|> do reserved "StrCons"; lchar '('; x <- pLExp; lchar ',';

244− xs <- pLExp; lchar ')';

245− return (LOp LStrCons [x, xs])

246− <|> do reserved "StrIndex"; lchar '('; x <- pLExp; lchar ',';

247− i <- pLExp; lchar ')';

248− return (LOp LStrIndex [x, i])

249−

250−pAlt :: LParser LAlt

251−pAlt = try (do x <- iName []

252− lchar '('; args <- sepBy1 (iName []) (lchar ','); lchar ')'

253− symbol "=>"

254− rhs <- pLExp

255− return (LConCase (-1) x args rhs))

256− <|> do x <- iName [];

257− symbol "=>"

258− rhs <- pLExp

259− return (LConCase (-1) x [] rhs)

260− <|> do c <- natural

261− symbol "=>"

262− rhs <- pLExp

263− return (LConstCase (I (fromInteger c)) rhs)

264− <|> do symbol "_"

265− symbol "=>"

266− rhs <- pLExp

267− return (LDefaultCase rhs)

268−

269−

270−pLConst :: LParser LExp

271−pLConst = try (do f <- float; return $ LConst (Fl f))

272− <|> try (do i <- natural; lchar ':'; return $ LConst (BI i))

273− <|> try (do i <- natural; return $ LConst (I (fromInteger i)))

274− <|> try (do s <- strlit; return $ LConst (Str s))

275− <|> try (do c <- chlit; return $ LConst (Ch c))

276−

src/Idris/AbsSyntax.hs+1−1

@@ -8,8 +8,8 @@ import Core.Evaluate

8import Core.Elaborate hiding (Tactic(..))

9import Core.Typecheck

10import Idris.AbsSyntaxTree

11−import Idris.IdeSlave

12import Idris.Colours

11import Idris.Colours

12+import Idris.IdeSlave

13import IRTS.CodegenCommon

14import Util.DynamicLinker

src/Idris/AbsSyntaxTree.hs−2

@@ -226,7 +226,6 @@ data Command = Quit

226 | ShowProof Name

227 | Proofs

228 | Universes

229− | TTShell

230 | LogLvl Int

229 | LogLvl Int

231 | Spec PTerm

230 | Spec PTerm

232 | HNF PTerm

231 | HNF PTerm

@@ -284,7 +283,6 @@ data Opt = Filename String

284 | BCAsm String

283 | BCAsm String

285 | DumpDefun String

284 | DumpDefun String

286 | DumpCases String

285 | DumpCases String

287− | FOVM String

288 | UseCodegen Codegen

286 | UseCodegen Codegen

289 | OutputTy OutputType

287 | OutputTy OutputType

290 | Extension LanguageExt

288 | Extension LanguageExt

src/Idris/Completion.hs+1−1

@@ -3,11 +3,11 @@ module Idris.Completion (replCompletion, proverCompletion) where

4import Core.Evaluate (ctxtAlist)

5import Core.TT

6−import Core.CoreParser (opChars)

8import Idris.AbsSyntaxTree

7import Idris.AbsSyntaxTree

9import Idris.Help

8import Idris.Help

10import Idris.Colours

9import Idris.Colours

10+import Idris.ParseHelpers(opChars)

12import Control.Monad.State.Strict

src/Idris/DSL.hs−1

@@ -5,7 +5,6 @@ module Idris.DSL where

5import Idris.AbsSyntax

6import Paths_idris

8−import Core.CoreParser

9import Core.TT

8import Core.TT

10import Core.Evaluate

9import Core.Evaluate

src/Idris/IdeSlave.hs+10−6

@@ -5,11 +5,15 @@ module Idris.IdeSlave(parseMessage, convSExp, IdeSlaveCommand(..), sexpToCommand

5import Text.Printf

6import Numeric

7import Data.List

8+import qualified Data.ByteString.UTF8 as UTF8

8-- import qualified Data.Text as T

9-- import qualified Data.Text as T

9−import Text.Parsec

10+import Text.Trifecta hiding (Err)

11+import Text.Trifecta.Delta

11import Core.TT

13import Core.TT

15+import Control.Applicative

16+

13data SExp = SexpList [SExp]

17data SExp = SexpList [SExp]

14 | StringAtom String

18 | StringAtom String

15 | BoolAtom Bool

19 | BoolAtom Bool

@@ -76,7 +80,7 @@ pSExp = do xs <- between (char '(') (char ')') (pSExp `sepBy` (char ' '))

76atom = do string "nil"; return (SexpList [])

80atom = do string "nil"; return (SexpList [])

77 <|> do char ':'; x <- atomC; return x

81 <|> do char ':'; x <- atomC; return x

78 <|> do char '"'; xs <- many quotedChar; char '"'; return (StringAtom xs)

82 <|> do char '"'; xs <- many quotedChar; char '"'; return (StringAtom xs)

79− <|> do ints <- many1 digit

83+ <|> do ints <- some digit

80 case readDec ints of

84 case readDec ints of

81 ((num, ""):_) -> return (IntegerAtom (toInteger num))

85 ((num, ""):_) -> return (IntegerAtom (toInteger num))

82 _ -> return (StringAtom ints)

86 _ -> return (StringAtom ints)

@@ -89,8 +93,8 @@ quotedChar = try (string "\\\\" >> return '\\')

89 <|> try (string "\\\"" >> return '"')

93 <|> try (string "\\\"" >> return '"')

90 <|> noneOf "\""

94 <|> noneOf "\""

92−parseSExp :: String -> Either ParseError SExp

96+parseSExp :: String -> Result SExp

93−parseSExp = parse pSExp "(unknown)"

97+parseSExp = parseString pSExp (Directed (UTF8.fromString "(unknown)") 0 0 0 0)

95data IdeSlaveCommand = REPLCompletions String

99data IdeSlaveCommand = REPLCompletions String

96 | Interpret String

100 | Interpret String

@@ -134,8 +138,8 @@ receiveString x =

134 if (length msg) /= (num - 1)

138 if (length msg) /= (num - 1)

135 then Left . Msg $ "bad input length"

139 then Left . Msg $ "bad input length"

136 else (case parseSExp msg of

140 else (case parseSExp msg of

137− Left _ -> Left . Msg $ "parse failure"

141+ Failure _ -> Left . Msg $ "parse failure"

138− Right r -> Right r)

142+ Success r -> Right r)

139 _ -> Left . Msg $ "readHex failed"

143 _ -> Left . Msg $ "readHex failed"

140

144

141convSExp :: SExpable a => String -> a -> Integer -> String

145convSExp :: SExpable a => String -> a -> Integer -> String

src/Idris/ParseHelpers.hs+8−1

@@ -43,6 +43,10 @@ instance TokenParsing IdrisInnerParser where

43-- | Generalized monadic parsing constraint type

44type MonadicParsing m = (DeltaParsing m, LookAheadParsing m, TokenParsing m, Monad m)

46+-- | Helper to run Idris inner parser based stateT parsers

47+runparser :: StateT st IdrisInnerParser res -> st -> String -> String -> Result res

48+runparser p i inputname = parseString (runInnerParser (evalStateT p i)) (Directed (UTF8.fromString inputname) 0 0 0 0)

49+

46{- * Space, comments and literals (token/lexing like parsers) -}

50{- * Space, comments and literals (token/lexing like parsers) -}

48-- | Consumes any simple whitespace (any character which satisfies Char.isSpace)

52-- | Consumes any simple whitespace (any character which satisfies Char.isSpace)

@@ -232,8 +236,11 @@ mkName (n, ns) = NS (UN n) (reverse (parseNS ns))

232 (x, "") -> [x]

236 (x, "") -> [x]

233 (x, '.':y) -> x : parseNS y

237 (x, '.':y) -> x : parseNS y

234

238

239+opChars :: String

240+opChars = ":!#$%&*+./<=>?@\\^|-~"

241+

235operatorLetter :: MonadicParsing m => m Char

242operatorLetter :: MonadicParsing m => m Char

236−operatorLetter = oneOf ":!#$%&*+./<=>?@\\^|-~"

243+operatorLetter = oneOf opChars

237

244

238-- | Parses an operator

245-- | Parses an operator

239operator :: MonadicParsing m => m String

246operator :: MonadicParsing m => m String

src/Idris/Parser.hs+3−5

@@ -30,7 +30,6 @@ import Idris.ParseHelpers

30import Idris.ParseOps

31import Idris.ParseExpr

32import Idris.ParseData

33−import Core.CoreParser (opChars)

35import Paths_idris

34import Paths_idris

@@ -885,11 +884,11 @@ transform syn = do try (lchar '%' *> reserved "transform")

885{- * Loading and parsing -}

884{- * Loading and parsing -}

886{- | Parses an expression from input -}

885{- | Parses an expression from input -}

887parseExpr :: IState -> String -> Result PTerm

886parseExpr :: IState -> String -> Result PTerm

888−parseExpr st = parseString (runInnerParser (evalStateT (fullExpr defaultSyntax) st)) (Directed (UTF8.fromString "(input)") 0 0 0 0)

887+parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"

889

888

890{- | Parses a tactic from input -}

889{- | Parses a tactic from input -}

891parseTactic :: IState -> String -> Result PTactic

890parseTactic :: IState -> String -> Result PTactic

892−parseTactic st = parseString (runInnerParser (evalStateT (fullTactic defaultSyntax) st)) (Directed (UTF8.fromString "(input)") 0 0 0 0)

891+parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"

893

892

894-- | Parse module header and imports

893-- | Parse module header and imports

895parseImports :: FilePath -> String -> Idris ([String], [String], Maybe Delta)

894parseImports :: FilePath -> String -> Idris ([String], [String], Maybe Delta)

@@ -912,14 +911,13 @@ parseImports fname input

912 i <- get

911 i <- get

913 return ((mname, ps, mrk'), i)

912 return ((mname, ps, mrk'), i)

914

913

915−

916-- | A program is a list of declarations, possibly with associated

914-- | A program is a list of declarations, possibly with associated

917-- documentation strings.

915-- documentation strings.

918parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->

916parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->

919 Idris [PDecl]

917 Idris [PDecl]

920parseProg syn fname input mrk

918parseProg syn fname input mrk

921 = do i <- getIState

919 = do i <- getIState

922− case parseString (runInnerParser (evalStateT mainProg i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of

920+ case runparser mainProg i fname input of

923 Failure doc -> do -- FIXME: Get error location from trifecta

921 Failure doc -> do -- FIXME: Get error location from trifecta

924 --let errl = sourceLine (errorPos err)

922 --let errl = sourceLine (errorPos err)

925 i <- getIState

923 i <- getIState

src/Idris/REPL.hs−17

@@ -31,12 +31,10 @@ import Util.Net (listenOnLocalhost)

32import Core.Evaluate

33import Core.Execute (execute)

34−import Core.ProofShell

35import Core.TT

34import Core.TT

36import Core.Constraints

35import Core.Constraints

38import IRTS.Compiler

37import IRTS.Compiler

39−import IRTS.LParser

40import IRTS.CodegenCommon

38import IRTS.CodegenCommon

42import Text.Trifecta.Result(Result(..))

40import Text.Trifecta.Result(Result(..))

@@ -811,11 +809,6 @@ process h fn (TestInline t)

811 imp <- impShow

809 imp <- impShow

812 c <- colourise

810 c <- colourise

813 iPrintResult (showImp (Just ist) imp c (delab ist tm'))

811 iPrintResult (showImp (Just ist) imp c (delab ist tm'))

814−process h fn TTShell

815− = do ist <- getIState

816− let shst = initState (tt_ctxt ist)

817− runShell shst

818− return ()

819process h fn Execute

812process h fn Execute

820 = do (m, _) <- elabVal toplevel False

813 = do (m, _) <- elabVal toplevel False

821 (PApp fc

814 (PApp fc

@@ -966,7 +959,6 @@ parseArgs ("--build":n:ns) = PkgBuild n : (parseArgs ns)

966parseArgs ("--install":n:ns) = PkgInstall n : (parseArgs ns)

959parseArgs ("--install":n:ns) = PkgInstall n : (parseArgs ns)

967parseArgs ("--clean":n:ns) = PkgClean n : (parseArgs ns)

960parseArgs ("--clean":n:ns) = PkgClean n : (parseArgs ns)

968parseArgs ("--bytecode":n:ns) = NoREPL : BCAsm n : (parseArgs ns)

961parseArgs ("--bytecode":n:ns) = NoREPL : BCAsm n : (parseArgs ns)

969−parseArgs ("--fovm":n:ns) = NoREPL : FOVM n : (parseArgs ns)

970parseArgs ("-S":ns) = OutputTy Raw : (parseArgs ns)

962parseArgs ("-S":ns) = OutputTy Raw : (parseArgs ns)

971parseArgs ("-c":ns) = OutputTy Object : (parseArgs ns)

963parseArgs ("-c":ns) = OutputTy Object : (parseArgs ns)

972parseArgs ("--mvn":ns) = OutputTy MavenProject : (parseArgs ns)

964parseArgs ("--mvn":ns) = OutputTy MavenProject : (parseArgs ns)

@@ -1083,7 +1075,6 @@ idrisMain opts =

1083 let ibcsubdir = opt getIBCSubDir opts

1075 let ibcsubdir = opt getIBCSubDir opts

1084 let importdirs = opt getImportDir opts

1076 let importdirs = opt getImportDir opts

1085 let bcs = opt getBC opts

1077 let bcs = opt getBC opts

1086− let vm = opt getFOVM opts

1087 let pkgdirs = opt getPkgDir opts

1078 let pkgdirs = opt getPkgDir opts

1088 let optimize = case opt getOptLevel opts of

1079 let optimize = case opt getOptLevel opts of

1089 [] -> 2

1080 [] -> 2

@@ -1121,10 +1112,6 @@ idrisMain opts =

1121 setOptLevel optimize

1112 setOptLevel optimize

1122 when (Verbose `elem` opts) $ setVerbose True

1113 when (Verbose `elem` opts) $ setVerbose True

1123 mapM_ makeOption opts

1114 mapM_ makeOption opts

1124− -- if we have the --fovm flag, drop into the first order VM testing

1125− case vm of

1126− [] -> return ()

1127− xs -> runIO $ mapM_ (fovm cgn outty) xs

1128 -- if we have the --bytecode flag, drop into the bytecode assembler

1115 -- if we have the --bytecode flag, drop into the bytecode assembler

1129 case bcs of

1116 case bcs of

1130 [] -> return ()

1117 [] -> return ()

@@ -1245,10 +1232,6 @@ getBC :: Opt -> Maybe String

1245getBC (BCAsm str) = Just str

1232getBC (BCAsm str) = Just str

1246getBC _ = Nothing

1233getBC _ = Nothing

1247

1234

1248−getFOVM :: Opt -> Maybe String

1249−getFOVM (FOVM str) = Just str

1250−getFOVM _ = Nothing

1251−

1252getOutput :: Opt -> Maybe String

1235getOutput :: Opt -> Maybe String

1253getOutput (Output str) = Just str

1236getOutput (Output str) = Just str

1254getOutput _ = Nothing

1237getOutput _ = Nothing

src/Idris/REPLParser.hs+1−2

@@ -23,7 +23,7 @@ import Data.Char(toLower)

23import qualified Data.ByteString.UTF8 as UTF8

25parseCmd :: IState -> String -> String -> Result Command

26−parseCmd i inputname = parseString (P.runInnerParser (evalStateT pCmd i)) (Directed (UTF8.fromString inputname) 0 0 0 0)

26+parseCmd i inputname = P.runparser pCmd i inputname

28cmd :: [String] -> P.IdrisParser ()

29cmd xs = do P.lchar ':'; docmd (sortBy (\x y -> compare (length y) (length x)) xs)

@@ -38,7 +38,6 @@ pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)

38 return (ModImport (toPath f)))

39 <|> try (do cmd ["e", "edit"]; eof; return Edit)

40 <|> try (do cmd ["exec", "execute"]; eof; return Execute)

41− <|> try (do cmd ["ttshell"]; eof; return TTShell)

42 <|> try (do cmd ["c", "compile"]; f <- P.identifier; eof; return (Compile ViaC f))

41 <|> try (do cmd ["c", "compile"]; f <- P.identifier; eof; return (Compile ViaC f))

43 <|> try (do cmd ["jc", "newcompile"]; f <- P.identifier; eof; return (Compile ViaJava f))

42 <|> try (do cmd ["jc", "newcompile"]; f <- P.identifier; eof; return (Compile ViaJava f))

44 <|> try (do cmd ["js", "javascript"]; f <- P.identifier; eof; return (Compile ViaJavaScript f))

43 <|> try (do cmd ["js", "javascript"]; f <- P.identifier; eof; return (Compile ViaJavaScript f))

src/Main.hs−3

@@ -12,11 +12,8 @@ import Control.Monad.Trans.Error ( ErrorT(..) )

12import Control.Monad.Trans.State.Strict ( execStateT, get, put )

13import Control.Monad ( when )

15−import Core.CoreParser

16−import Core.ShellParser

17import Core.TT

15import Core.TT

18import Core.Typecheck

16import Core.Typecheck

19−import Core.ProofShell

20import Core.Evaluate

17import Core.Evaluate

21import Core.Constraints

18import Core.Constraints

src/Pkg/PParser.hs+30−52

@@ -1,41 +1,19 @@

1module Pkg.PParser where

3−import Core.CoreParser

3+import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace)

4import Core.TT

5import Core.TT

5import Idris.REPL

6import Idris.REPL

6import Idris.AbsSyntaxTree

7import Idris.AbsSyntaxTree

8+import Idris.ParseHelpers

8import Paths_idris

10import Paths_idris

10−import Text.ParserCombinators.Parsec

12+import Control.Monad.State.Strict

11−import Text.ParserCombinators.Parsec.Error

13+import Control.Applicative

12−import Text.ParserCombinators.Parsec.Expr

13−import Text.ParserCombinators.Parsec.Language

14−import qualified Text.ParserCombinators.Parsec.Token as PTok

15−

16−type TokenParser a = PTok.TokenParser a

17−

18−type PParser = GenParser Char PkgDesc

20−lexer :: TokenParser PkgDesc

21−lexer = idrisLexer

23−whiteSpace= PTok.whiteSpace lexer

16+type PParser = StateT PkgDesc IdrisInnerParser

24−lexeme = PTok.lexeme lexer

25−symbol = PTok.symbol lexer

26−natural = PTok.natural lexer

27−parens = PTok.parens lexer

28−semi = PTok.semi lexer

29−comma = PTok.comma lexer

30−identifier= PTok.identifier lexer

31−reserved = PTok.reserved lexer

32−operator = PTok.operator lexer

33−reservedOp= PTok.reservedOp lexer

34−integer = PTok.integer lexer

35−float = PTok.float lexer

36−strlit = PTok.stringLiteral lexer

37−chlit = PTok.charLiteral lexer

38−lchar = lexeme.char

40data PkgDesc = PkgDesc { pkgname :: String,

18data PkgDesc = PkgDesc { pkgname :: String,

41 libdeps :: [String],

19 libdeps :: [String],

@@ -53,50 +31,50 @@ defaultPkg = PkgDesc "" [] [] Nothing [] "" [] (UN "") Nothing

54parseDesc :: FilePath -> IO PkgDesc

32parseDesc :: FilePath -> IO PkgDesc

55parseDesc fp = do p <- readFile fp

33parseDesc fp = do p <- readFile fp

56− case runParser pPkg defaultPkg fp p of

34+ case runparser pPkg defaultPkg fp p of

57− Left err -> fail (show err)

35+ Failure err -> fail (show err)

58− Right x -> return x

36+ Success x -> return x

60pPkg :: PParser PkgDesc

38pPkg :: PParser PkgDesc

61pPkg = do reserved "package"; p <- identifier

39pPkg = do reserved "package"; p <- identifier

62− st <- getState

40+ st <- get

63− setState (st { pkgname = p })

41+ put (st { pkgname = p })

64− many1 pClause

42+ some pClause

65− st <- getState

43+ st <- get

66 return st

44 return st

68pClause :: PParser ()

46pClause :: PParser ()

69pClause = do reserved "executable"; lchar '=';

47pClause = do reserved "executable"; lchar '=';

70 exec <- iName []

48 exec <- iName []

71− st <- getState

49+ st <- get

72− setState (st { execout = Just (show exec) })

50+ put (st { execout = Just (show exec) })

73 <|> do reserved "main"; lchar '=';

51 <|> do reserved "main"; lchar '=';

74 main <- iName []

52 main <- iName []

75− st <- getState

53+ st <- get

76− setState (st { idris_main = main })

54+ put (st { idris_main = main })

77 <|> do reserved "sourcedir"; lchar '=';

55 <|> do reserved "sourcedir"; lchar '=';

78 src <- identifier

56 src <- identifier

79− st <- getState

57+ st <- get

80− setState (st { sourcedir = src })

58+ put (st { sourcedir = src })

81 <|> do reserved "opts"; lchar '=';

59 <|> do reserved "opts"; lchar '=';

82− opts <- strlit

60+ opts <- stringLiteral

83− st <- getState

61+ st <- get

84 let args = parseArgs (words opts)

62 let args = parseArgs (words opts)

85− setState (st { idris_opts = args })

63+ put (st { idris_opts = args })

86 <|> do reserved "modules"; lchar '=';

64 <|> do reserved "modules"; lchar '=';

87 ms <- sepBy1 (iName []) (lchar ',')

65 ms <- sepBy1 (iName []) (lchar ',')

88− st <- getState

66+ st <- get

89− setState (st { modules = modules st ++ ms })

67+ put (st { modules = modules st ++ ms })

90 <|> do reserved "libs"; lchar '=';

68 <|> do reserved "libs"; lchar '=';

91 ls <- sepBy1 identifier (lchar ',')

69 ls <- sepBy1 identifier (lchar ',')

92− st <- getState

70+ st <- get

93− setState (st { libdeps = libdeps st ++ ls })

71+ put (st { libdeps = libdeps st ++ ls })

94 <|> do reserved "objs"; lchar '=';

72 <|> do reserved "objs"; lchar '=';

95 ls <- sepBy1 identifier (lchar ',')

73 ls <- sepBy1 identifier (lchar ',')

96− st <- getState

74+ st <- get

97− setState (st { objs = libdeps st ++ ls })

75+ put (st { objs = libdeps st ++ ls })

98 <|> do reserved "makefile"; lchar '=';

76 <|> do reserved "makefile"; lchar '=';

99 mk <- iName []

77 mk <- iName []

100− st <- getState

78+ st <- get

101− setState (st { makefile = Just (show mk) })

79+ put (st { makefile = Just (show mk) })

102