3b297bc · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Parsing declarations, keeping track of fixities

commit3b297bc8604c41f7f54208a11df988b6197c2f66 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateWed 5 Oct 2011, 00:46 (15 years ago) parent50d24ec

6 files changed+95−35

compare with master

unifiedsplit

src/Core/CoreParser.hs+19−15 src/Idris/AbsSyntax.hs+3−3 src/Idris/Parser.hs+56−10 src/Idris/REPL.hs+8−3 src/Idris/REPLParser.hs+5−4 src/Main.hs+4

src/Core/CoreParser.hs+19−15

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

55import Core.TT

77import Text.ParserCombinators.Parsec

8+import Text.Parsec.Prim(Parsec)

89import Text.ParserCombinators.Parsec.Expr

910import Text.ParserCombinators.Parsec.Language

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

@@ -13,7 +14,7 @@ import Debug.Trace

1314

1415type TokenParser a = PTok.TokenParser a

1516

16−lexer :: TokenParser ()

17+lexer :: TokenParser a

1718lexer = PTok.makeTokenParser haskellDef

1819

1920whiteSpace= PTok.whiteSpace lexer

@@ -29,18 +30,21 @@ operator = PTok.operator lexer

2930reservedOp= PTok.reservedOp lexer

3031lchar = lexeme.char

3132

32−parseFile = parse pTestFile "(input)"

33−parseDef = parse pDef "(input)"

34−parseTerm = parse pTerm "(input)"

33+type CParser a = Parsec String a

3534

36−pTestFile :: Parser RProgram

35+parseFile = runParser pTestFile () "(input)"

36+parseDef = runParser pDef () "(input)"

37+parseTerm = runParser pTerm () "(input)"

38+

39+pTestFile :: CParser a RProgram

3740pTestFile = do p <- many1 pDef ; eof

3841 return p

3942

40−iName :: Parser Name

41−iName = identifier >>= (\n -> return (UN [n]))

43+iName :: CParser a Name

44+iName = do x <- identifier

45+ return (UN [x])

4246

43−pDef :: Parser (Name, RDef)

47+pDef :: CParser a (Name, RDef)

4448pDef = try (do x <- iName; lchar ':'; ty <- pTerm

4549 lchar '='

4650 tm <- pTerm

@@ -51,20 +55,20 @@ pDef = try (do x <- iName; lchar ':'; ty <- pTerm

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

5256 return (x, RData d)

5357

54−app :: Parser (Raw -> Raw -> Raw)

58+app :: CParser a (Raw -> Raw -> Raw)

5559app = do whiteSpace ; return RApp

5660

57−arrow :: Parser (Raw -> Raw -> Raw)

61+arrow :: CParser a (Raw -> Raw -> Raw)

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

5963

60−pTerm :: Parser Raw

64+pTerm :: CParser a Raw

6165pTerm = try (do chainl1 pNoApp app)

6266 <|> pNoApp

6367

64−pNoApp :: Parser Raw

68+pNoApp :: CParser a Raw

6569pNoApp = try (chainr1 pExp arrow)

6670 <|> pExp

67−pExp :: Parser Raw

71+pExp :: CParser a Raw

6872pExp = do lchar '\\'; x <- iName; lchar ':'; ty <- pTerm

6973 symbol "=>";

7074 sc <- pTerm

@@ -106,12 +110,12 @@ pExp = do lchar '\\'; x <- iName; lchar ':'; ty <- pTerm

106110 <|> try (do x <- iName

107111 return (Var x))

108112

109−pData :: Parser (Name, RawDatatype)

113+pData :: CParser a (Name, RawDatatype)

110114pData = do reserved "data"; x <- iName; lchar ':'; ty <- pTerm; reserved "where"

111115 cs <- many pConstructor

112116 return (x, RDatatype x ty cs)

113117

114−pConstructor :: Parser (Name, Raw)

118+pConstructor :: CParser a (Name, Raw)

115119pConstructor = do lchar '|'

116120 c <- iName; lchar ':'; ty <- pTerm

117121 return (c, ty)

src/Idris/AbsSyntax.hs+3−3

@@ -41,8 +41,8 @@ iLOG str = do i <- get

4141

4242-- Commands in the REPL

4343

44−data Command = Quit

45− | Help

44+data Command = Quit | Help | Eval PTerm

45+ | NOP

4646

4747-- Parsed declarations

4848

@@ -59,7 +59,7 @@ instance Ord FixDecl where

5959

6060data Plicity = Imp | Exp deriving Show

6161

62−data PDecl = PFix Fixity String -- fixity declaration

62+data PDecl = PFix Fixity [String] -- fixity declaration

6363 | PTy Name PTerm -- type declaration

6464 | PClause PTerm PTerm -- pattern clause

6565 | PData PData -- data declaration

src/Idris/Parser.hs+56−10

@@ -6,10 +6,13 @@ import Core.CoreParser

66import Core.TT

88import Text.ParserCombinators.Parsec

9+import Text.Parsec.Prim(Parsec)

910import Text.ParserCombinators.Parsec.Expr

1011import Text.ParserCombinators.Parsec.Language

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

1213

14+import Data.List

15+import Control.Monad.State

1316import Debug.Trace

1417

1518type TokenParser a = PTok.TokenParser a

@@ -22,7 +25,9 @@ idrisDef = haskellDef {

2225 "using", "params", "namespace"]

2326 }

2427

25−lexer :: TokenParser ()

28+type IParser = Parsec String IState

29+

30+lexer :: TokenParser IState

2631lexer = PTok.makeTokenParser idrisDef

2732

2833whiteSpace= PTok.whiteSpace lexer

@@ -38,17 +43,48 @@ operator = PTok.operator lexer

3843reservedOp= PTok.reservedOp lexer

3944lchar = lexeme.char

4045

41−parseExpr = parse pFullExpr "(input)"

46+parseExpr i = runParser pFullExpr i "(input)"

47+

48+parseProg :: String -> Idris [PDecl]

49+parseProg fname = do file <- lift $ readFile fname

50+ i <- get

51+ case (runParser (do ps <- many1 pDecl

52+ i' <- getState

53+ return (ps, i')) i fname file) of

54+ Left err -> fail (show err)

55+ Right (x, i) -> do put i

56+ return x

57+

4258

4359pFullExpr = do x <- pExpr; eof; return x

4460

45−pExpr' :: Parser PTerm

61+pDecl :: IParser PDecl

62+pDecl = do d <- pDecl'; lchar ';'; return d

63+

64+pDecl' :: IParser PDecl

65+pDecl' = try (do f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')

66+ let prec = fromInteger i

67+ istate <- getState

68+ let fs = map (Fix (f prec)) ops

69+ setState (istate {

70+ idris_infixes = sort (fs ++ idris_infixes istate) })

71+ return (PFix (f prec) ops))

72+ <|> try (do n <- iName; ty <- pTSig

73+ return (PTy n ty))

74+

75+fixity :: IParser (Int -> Fixity)

76+fixity = try (do reserved "infixl"; return Infixl)

77+ <|> try (do reserved "infixr"; return Infixr)

78+ <|> try (do reserved "infix"; return InfixN)

79+

80+pExpr = do i <- getState

81+ buildExpressionParser (table (idris_infixes i)) pExpr'

82+

83+pExpr' :: IParser PTerm

4684pExpr' = try pApp

47− <|> pSimpleExpr

48− <|> try pLambda

49− <|> try pPi

50−

51−pExpr = buildExpressionParser table pExpr'

85+ <|> pSimpleExpr

86+ <|> try pLambda

87+ <|> try pPi

5288

5389pSimpleExpr =

5490 try (do symbol "!["; t <- pTerm; lchar ']'

@@ -79,8 +115,18 @@ pPi = do lchar '('; x <- iName; t <- pTSig; lchar ')'

79115 sc <- pExpr

80116 return (PPi Imp x t sc)

81117

82−table = [[binary "=" (\x y -> PApp (PRef (UN ["="])) [] [x,y]) AssocLeft],

83− [binary "->" (PPi Exp (MN 0 "X")) AssocRight]]

118+table fixes

119+ = toTable (reverse fixes) ++

120+ [[binary "=" (\x y -> PApp (PRef (UN ["="])) [] [x,y]) AssocLeft],

121+ [binary "->" (PPi Exp (MN 0 "X")) AssocRight]]

122+

123+toTable fs = map (map toBin)

124+ (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)

125+ where toBin (Fix f op) = binary op

126+ (\x y -> PApp (PRef (UN [op])) [] [x,y]) (assoc f)

127+ assoc (Infixl _) = AssocLeft

128+ assoc (Infixr _) = AssocRight

129+ assoc (InfixN _) = AssocNone

84130

85131binary name f assoc = Infix (do { reservedOp name; return f }) assoc

86132

src/Idris/REPL.hs+8−3

@@ -14,12 +14,14 @@ repl :: Idris ()

1414repl = do x <- lift $ readline "Idris> "

1515 case x of

1616 Nothing -> repl

17− Just input -> do continue <- processInput input

17+ Just input -> do lift $ addHistory input

18+ continue <- processInput input

1819 when continue repl

1920

2021processInput :: String -> Idris Bool

2122processInput cmd

22− = case parseCmd cmd of

23+ = do i <- get

24+ case parseCmd i cmd of

2325 Left err -> do lift $ print err

2426 return True

2527 Right Quit -> do iputStrLn "Bye bye"

@@ -28,5 +30,8 @@ processInput cmd

2830 return True

2931

3032process :: Command -> Idris ()

31−process Help = iputStrLn "At some point I'll write some help text. Thanks for asking though."

33+process Help

34+ = iputStrLn "At some point I'll write some help text. Thanks for asking though."

35+process (Eval t) = iputStrLn $ "Not implemented: " ++ show t

36+process NOP = return ()

3237

src/Idris/REPLParser.hs+5−4

@@ -11,14 +11,15 @@ import qualified Text.ParserCombinators.Parsec.Token as PTok

1111

1212import Debug.Trace

1313

14−parseCmd = parse pCmd "(input)"

14+parseCmd i = runParser pCmd i "(input)"

1515

16−cmd :: [String] -> Parser ()

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

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

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

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

2020

21−pCmd :: Parser Command

21+pCmd :: IParser Command

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

2323 <|> try (do cmd ["h", "?", "help"]; return Help)

24−

24+ <|> do t <- pFullExpr; return (Eval t)

25+ <|> do eof; return NOP

src/Main.hs+4

@@ -41,6 +41,10 @@ runIdris opts =

4141

4242loadModule :: FilePath -> Idris ()

4343loadModule f = do iLOG ("Reading " ++ show f)

44+ ds <- parseProg f

45+ iLOG (show ds)

46+ i <- get

47+ iLOG (show (idris_infixes i))

4448 return ()

4549

4650getFile :: Opt -> Maybe String