82585e7 · Idris-dev · git.iko.soy

src/Core/CoreParser.hs+1−2

compare with master

unifiedsplit

@@ -5,7 +5,6 @@ module Core.CoreParser(parseTerm, parseFile, parseDef, pTerm, iName, idrisDef) w

5import Core.TT

6

7import Text.ParserCombinators.Parsec

8−import Text.Parsec.Prim(Parsec)

9import Text.ParserCombinators.Parsec.Expr

8import Text.ParserCombinators.Parsec.Expr

10import Text.ParserCombinators.Parsec.Language

9import Text.ParserCombinators.Parsec.Language

11import qualified Text.ParserCombinators.Parsec.Token as PTok

10import qualified Text.ParserCombinators.Parsec.Token as PTok

@@ -38,7 +37,7 @@ operator = PTok.operator lexer

38reservedOp= PTok.reservedOp lexer

37reservedOp= PTok.reservedOp lexer

39lchar = lexeme.char

38lchar = lexeme.char

40

39

41−type CParser a = Parsec String a

40+type CParser a = GenParser Char a

42

41

43parseFile = runParser pTestFile () "(input)"

42parseFile = runParser pTestFile () "(input)"

44parseDef = runParser pDef () "(input)"

43parseDef = runParser pDef () "(input)"

src/Core/Evaluate.hs+2−1

@@ -1,4 +1,5 @@

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

1+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances,

2+ PatternGuards #-}

2

3

3module Core.Evaluate(normalise,

4module Core.Evaluate(normalise,

4 Fun(..), Def(..), Context,

5 Fun(..), Def(..), Context,

src/Core/ShellParser.hs+1−2

@@ -10,7 +10,6 @@ import Text.ParserCombinators.Parsec

10import Text.ParserCombinators.Parsec.Expr

11import Text.ParserCombinators.Parsec.Language

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

13−import Control.Monad

14

13

15import Debug.Trace

14import Debug.Trace

16

15

@@ -66,7 +65,7 @@ pTactic = do reserved "attack"; return attack

66 <|> do reserved "focus"; n <- iName; return (focus n)

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

67 <|> do reserved "state"; return proofstate

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

68 <|> do reserved "undo"; return undo

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

69− <|> do reserved "qed"; return (void qed)

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

70

69

71pArgType :: Parser Bool

70pArgType :: Parser Bool

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

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

src/Core/TT.hs+3

@@ -47,6 +47,9 @@ instance MonadPlus TC where

47 _ `mplus` (OK y) = OK y

48 err `mplus` _ = err

49

50+discard :: Monad m => m a -> m ()

51+discard f = f >> return ()

52+

50-- RAW TERMS ----------------------------------------------------------------

53-- RAW TERMS ----------------------------------------------------------------

51

54

52-- Names are hierarchies of strings, describing scope (so no danger of

55-- Names are hierarchies of strings, describing scope (so no danger of

src/Core/Typecheck.hs+2−1

@@ -1,4 +1,5 @@

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

1+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,

2+ PatternGuards #-}

2

3

3module Core.Typecheck where

4module Core.Typecheck where

4

5

src/Idris/Parser.hs+1−2

@@ -6,7 +6,6 @@ import Core.CoreParser

6import Core.TT

7

8import Text.ParserCombinators.Parsec

9−import Text.Parsec.Prim(Parsec)

10import Text.ParserCombinators.Parsec.Expr

9import Text.ParserCombinators.Parsec.Expr

11import Text.ParserCombinators.Parsec.Language

10import Text.ParserCombinators.Parsec.Language

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

11import qualified Text.ParserCombinators.Parsec.Token as PTok

@@ -17,7 +16,7 @@ import Debug.Trace

17

16

18type TokenParser a = PTok.TokenParser a

17type TokenParser a = PTok.TokenParser a

19

18

20−type IParser = Parsec String IState

19+type IParser = GenParser Char IState

21

20

22lexer :: TokenParser IState

21lexer :: TokenParser IState

23lexer = PTok.makeTokenParser idrisDef

22lexer = PTok.makeTokenParser idrisDef

src/Idris/REPLParser.hs+2−2

@@ -2,7 +2,7 @@ module Idris.REPLParser(parseCmd) where

2

3import Idris.Parser

4import Idris.AbsSyntax

5−import Control.Monad

5+import Core.TT

6

7import Text.ParserCombinators.Parsec

8import Text.ParserCombinators.Parsec.Expr

@@ -16,7 +16,7 @@ parseCmd i = runParser pCmd i "(input)"

16cmd :: [String] -> IParser ()

17cmd xs = do lchar ':'; docmd xs

18 where docmd [] = fail "No such command"

19− docmd (x:xs) = try (void (symbol x)) <|> docmd xs

19+ docmd (x:xs) = try (discard (symbol x)) <|> docmd xs

20

21pCmd :: IParser Command

22pCmd = try (do cmd ["q", "quit"]; return Quit)