← Back to branch summary

~ubuntu-branches/ubuntu/trusty/agda/trusty

« back to all changes in this revision

Viewing changes to src/full/Agda/Syntax/Parser.hs

  • Committer: Package Import Robot
  • Author(s): Iain Lane, Kiwamu Okabe, Iain Lane
  • Date: 2013-04-10 11:46:43 UTC
  • mfrom: (4.1.5 experimental)
  • Revision ID: package-import@ubuntu.com-20130410114643-prunhsz59f0fhrdn
Tags: 2.3.2-1
[ Kiwamu Okabe ]
* New patch: Extend haskell-src-exts dependency and fix type miss.

[ Iain Lane ]
* [dfbca48] Imported Upstream version 2.3.2
* [7746bcc] Remove all patches — all upstream.
* [2cdb691] Update build-deps to match control file
* [868ebf4] agda-mode no longer depends on haskell-mode or GHCi.
  Remove dependency and update .el file accordingly
* [9e0ba22] Add agda-bin package here, as the separate package has been
  removed
* [75a240f] agda-mode needs to depend on agda-bin
* [d290f95] Allow Quickcheck up to 2.7. Fix haskeline build-dep.
* [79190e6] Add missing geniplate and parallel BDs

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/full/Agda/Syntax/Parser.hs
24
24
import qualified Agda.Syntax.Parser.Monad as M
25
25
import qualified Agda.Syntax.Parser.Parser as P
26
26
import Agda.Syntax.Parser.Lexer
27
 
import Agda.Syntax.Strict
28
27
import Agda.Syntax.Concrete
29
28
import Agda.Syntax.Parser.Tokens
30
29
 
33
32
------------------------------------------------------------------------
34
33
-- Wrapping parse results
35
34
 
36
 
wrap :: Strict a => ParseResult a -> a
 
35
wrap :: ParseResult a -> a
37
36
wrap (ParseOk _ x)      = x
38
37
wrap (ParseFailed err)  = throw err
39
38
 
40
 
wrapM:: (Strict a, Monad m) => m (ParseResult a) -> m a
 
39
wrapM:: Monad m => m (ParseResult a) -> m a
41
40
wrapM m =
42
41
    do  r <- m
43
42
        case r of
54
53
  , parseFlags :: ParseFlags
55
54
  }
56
55
 
57
 
parse :: Strict a => Parser a -> String -> IO a
 
56
parse :: Parser a -> String -> IO a
58
57
parse p = wrapM . return . M.parse (parseFlags p) [normal] (parser p)
59
58
 
60
 
parseFile :: Strict a => Parser a -> AbsolutePath -> IO a
 
59
parseFile :: Parser a -> AbsolutePath -> IO a
61
60
parseFile p = wrapM . M.parseFile (parseFlags p) [normal] (parser p)
62
61
 
63
 
parseLiterate :: Strict a => Parser a -> String -> IO a
 
62
parseLiterate :: Parser a -> String -> IO a
64
63
parseLiterate p =
65
64
  wrapM . return . M.parse (parseFlags p) [literate, code] (parser p)
66
65
 
67
 
parseLiterateFile :: Strict a => Parser a -> AbsolutePath -> IO a
 
66
parseLiterateFile :: Parser a -> AbsolutePath -> IO a
68
67
parseLiterateFile p =
69
68
  wrapM . M.parseFile (parseFlags p) [literate, code] (parser p)
70
69
 
71
 
parsePosString :: Strict a => Parser a -> Position -> String -> IO a
 
70
parsePosString :: Parser a -> Position -> String -> IO a
72
71
parsePosString p pos =
73
72
  wrapM . return . M.parsePosString pos (parseFlags p) [normal] (parser p)
74
73
 
75
 
parseFile' :: Strict a => Parser a -> AbsolutePath -> IO a
 
74
parseFile' :: Parser a -> AbsolutePath -> IO a
76
75
parseFile' p file =
77
76
  if "lagda" `isSuffixOf` filePath file then
78
77
    Agda.Syntax.Parser.parseLiterateFile p file