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

git.iko.soy/Idris-dev

Some ghc 6.12 compatibility

commit82585e759af9b3c22fb79e43fa8c6296eeb7a663 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateWed 5 Oct 2011, 13:39 (15 years ago) parent64b7cfd

7 files changed+12−10

compare with master

unifiedsplit

src/Core/CoreParser.hs+1−2 src/Core/Evaluate.hs+2−1 src/Core/ShellParser.hs+1−2 src/Core/TT.hs+3 src/Core/Typecheck.hs+2−1 src/Idris/Parser.hs+1−2 src/Idris/REPLParser.hs+2−2

src/Core/CoreParser.hs+1−2

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

55import Core.TT

77import Text.ParserCombinators.Parsec

8−import Text.Parsec.Prim(Parsec)

98import Text.ParserCombinators.Parsec.Expr

109import Text.ParserCombinators.Parsec.Language

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

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

3837reservedOp= PTok.reservedOp lexer

3938lchar = lexeme.char

4039

41−type CParser a = Parsec String a

40+type CParser a = GenParser Char a

4241

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

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

src/Core/Evaluate.hs+2−1

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

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

1+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances,

2+ PatternGuards #-}

34module Core.Evaluate(normalise,

45 Fun(..), Def(..), Context,

src/Core/ShellParser.hs+1−2

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

1010import Text.ParserCombinators.Parsec.Expr

1111import Text.ParserCombinators.Parsec.Language

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

13−import Control.Monad

1413

1514import Debug.Trace

1615

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

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

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

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

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

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

7069

7170pArgType :: Parser Bool

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

src/Core/TT.hs+3

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

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

4848 err `mplus` _ = err

4949

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

51+discard f = f >> return ()

52+

5053-- RAW TERMS ----------------------------------------------------------------

5154

5255-- 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 #-}

34module Core.Typecheck where

src/Idris/Parser.hs+1−2

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

66import Core.TT

88import Text.ParserCombinators.Parsec

9−import Text.Parsec.Prim(Parsec)

109import Text.ParserCombinators.Parsec.Expr

1110import Text.ParserCombinators.Parsec.Language

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

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

1716

1817type TokenParser a = PTok.TokenParser a

1918

20−type IParser = Parsec String IState

19+type IParser = GenParser Char IState

2120

2221lexer :: TokenParser IState

2322lexer = PTok.makeTokenParser idrisDef

src/Idris/REPLParser.hs+2−2

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

33import Idris.Parser

44import Idris.AbsSyntax

5−import Control.Monad

5+import Core.TT

77import Text.ParserCombinators.Parsec

88import Text.ParserCombinators.Parsec.Expr

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

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

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

1818 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

2020

2121pCmd :: IParser Command

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