git.iko.soy/Idris-dev
on master help sign in
Parsing declarations, keeping track of fixities
3b297bcEdwin Brady
src/Core/CoreParser.hs+19−15
compare with master
unifiedsplit
@@ -5,6 +5,7 @@ module Core.CoreParser(parseTerm, parseFile, parseDef, pTerm, iName) where
5import Core.TT
5import Core.TT
6
6
7import Text.ParserCombinators.Parsec
7import Text.ParserCombinators.Parsec
8+import Text.Parsec.Prim(Parsec)
8import Text.ParserCombinators.Parsec.Expr
9import Text.ParserCombinators.Parsec.Expr
9import Text.ParserCombinators.Parsec.Language
10import Text.ParserCombinators.Parsec.Language
10import qualified Text.ParserCombinators.Parsec.Token as PTok
11import qualified Text.ParserCombinators.Parsec.Token as PTok
@@ -13,7 +14,7 @@ import Debug.Trace
13
14
14type TokenParser a = PTok.TokenParser a
15type TokenParser a = PTok.TokenParser a
15
16
16−lexer :: TokenParser ()
17+lexer :: TokenParser a
17lexer = PTok.makeTokenParser haskellDef
18lexer = PTok.makeTokenParser haskellDef
18
19
19whiteSpace= PTok.whiteSpace lexer
20whiteSpace= PTok.whiteSpace lexer
@@ -29,18 +30,21 @@ operator = PTok.operator lexer
29reservedOp= PTok.reservedOp lexer
30reservedOp= PTok.reservedOp lexer
30lchar = lexeme.char
31lchar = lexeme.char
31
32
32−parseFile = parse pTestFile "(input)"
33+type CParser a = Parsec String a
33−parseDef = parse pDef "(input)"
34−parseTerm = parse pTerm "(input)"
35
34
35+parseFile = runParser pTestFile () "(input)"
36+parseDef = runParser pDef () "(input)"
37+parseTerm = runParser pTerm () "(input)"
38+
36−pTestFile :: Parser RProgram
39+pTestFile :: CParser a RProgram
37pTestFile = do p <- many1 pDef ; eof
40pTestFile = do p <- many1 pDef ; eof
38 return p
41 return p
39
42
40−iName :: Parser Name
43+iName :: CParser a Name
41−iName = identifier >>= (\n -> return (UN [n]))
44+iName = do x <- identifier
45+ return (UN [x])
42
46
43−pDef :: Parser (Name, RDef)
47+pDef :: CParser a (Name, RDef)
44pDef = try (do x <- iName; lchar ':'; ty <- pTerm
48pDef = try (do x <- iName; lchar ':'; ty <- pTerm
45 lchar '='
49 lchar '='
46 tm <- pTerm
50 tm <- pTerm
@@ -51,20 +55,20 @@ pDef = try (do x <- iName; lchar ':'; ty <- pTerm
51 <|> do (x, d) <- pData; lchar ';'
55 <|> do (x, d) <- pData; lchar ';'
52 return (x, RData d)
56 return (x, RData d)
53
57
54−app :: Parser (Raw -> Raw -> Raw)
58+app :: CParser a (Raw -> Raw -> Raw)
55app = do whiteSpace ; return RApp
59app = do whiteSpace ; return RApp
56
60
57−arrow :: Parser (Raw -> Raw -> Raw)
61+arrow :: CParser a (Raw -> Raw -> Raw)
58arrow = do symbol "->" ; return $ \s t -> RBind (MN 0 "X") (Pi s) t
62arrow = do symbol "->" ; return $ \s t -> RBind (MN 0 "X") (Pi s) t
59
63
60−pTerm :: Parser Raw
64+pTerm :: CParser a Raw
61pTerm = try (do chainl1 pNoApp app)
65pTerm = try (do chainl1 pNoApp app)
62 <|> pNoApp
66 <|> pNoApp
63
67
64−pNoApp :: Parser Raw
68+pNoApp :: CParser a Raw
65pNoApp = try (chainr1 pExp arrow)
69pNoApp = try (chainr1 pExp arrow)
66 <|> pExp
70 <|> pExp
67−pExp :: Parser Raw
71+pExp :: CParser a Raw
68pExp = do lchar '\\'; x <- iName; lchar ':'; ty <- pTerm
72pExp = do lchar '\\'; x <- iName; lchar ':'; ty <- pTerm
69 symbol "=>";
73 symbol "=>";
70 sc <- pTerm
74 sc <- pTerm
@@ -106,12 +110,12 @@ pExp = do lchar '\\'; x <- iName; lchar ':'; ty <- pTerm
106 <|> try (do x <- iName
110 <|> try (do x <- iName
107 return (Var x))
111 return (Var x))
108
112
109−pData :: Parser (Name, RawDatatype)
113+pData :: CParser a (Name, RawDatatype)
110pData = do reserved "data"; x <- iName; lchar ':'; ty <- pTerm; reserved "where"
114pData = do reserved "data"; x <- iName; lchar ':'; ty <- pTerm; reserved "where"
111 cs <- many pConstructor
115 cs <- many pConstructor
112 return (x, RDatatype x ty cs)
116 return (x, RDatatype x ty cs)
113
117
114−pConstructor :: Parser (Name, Raw)
118+pConstructor :: CParser a (Name, Raw)
115pConstructor = do lchar '|'
119pConstructor = do lchar '|'
116 c <- iName; lchar ':'; ty <- pTerm
120 c <- iName; lchar ':'; ty <- pTerm
117 return (c, ty)
121 return (c, ty)
src/Idris/AbsSyntax.hs+3−3
@@ -41,8 +41,8 @@ iLOG str = do i <- get
41
41
42-- Commands in the REPL
42-- Commands in the REPL
43
43
44−data Command = Quit
44+data Command = Quit | Help | Eval PTerm
45− | Help
45+ | NOP
46
46
47-- Parsed declarations
47-- Parsed declarations
48
48
@@ -59,7 +59,7 @@ instance Ord FixDecl where
59
59
60data Plicity = Imp | Exp deriving Show
60data Plicity = Imp | Exp deriving Show
61
61
62−data PDecl = PFix Fixity String -- fixity declaration
62+data PDecl = PFix Fixity [String] -- fixity declaration
63 | PTy Name PTerm -- type declaration
63 | PTy Name PTerm -- type declaration
64 | PClause PTerm PTerm -- pattern clause
64 | PClause PTerm PTerm -- pattern clause
65 | PData PData -- data declaration
65 | PData PData -- data declaration
src/Idris/Parser.hs+56−10
@@ -6,10 +6,13 @@ import Core.CoreParser
6import Core.TT
6import Core.TT
7
7
8import Text.ParserCombinators.Parsec
8import Text.ParserCombinators.Parsec
9+import Text.Parsec.Prim(Parsec)
9import Text.ParserCombinators.Parsec.Expr
10import Text.ParserCombinators.Parsec.Expr
10import Text.ParserCombinators.Parsec.Language
11import Text.ParserCombinators.Parsec.Language
11import qualified Text.ParserCombinators.Parsec.Token as PTok
12import qualified Text.ParserCombinators.Parsec.Token as PTok
12
13
14+import Data.List
15+import Control.Monad.State
13import Debug.Trace
16import Debug.Trace
14
17
15type TokenParser a = PTok.TokenParser a
18type TokenParser a = PTok.TokenParser a
@@ -22,7 +25,9 @@ idrisDef = haskellDef {
22 "using", "params", "namespace"]
25 "using", "params", "namespace"]
23 }
26 }
24
27
28+type IParser = Parsec String IState
29+
25−lexer :: TokenParser ()
30+lexer :: TokenParser IState
26lexer = PTok.makeTokenParser idrisDef
31lexer = PTok.makeTokenParser idrisDef
27
32
28whiteSpace= PTok.whiteSpace lexer
33whiteSpace= PTok.whiteSpace lexer
@@ -38,17 +43,48 @@ operator = PTok.operator lexer
38reservedOp= PTok.reservedOp lexer
43reservedOp= PTok.reservedOp lexer
39lchar = lexeme.char
44lchar = lexeme.char
40
45
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+
42
58
43pFullExpr = do x <- pExpr; eof; return x
59pFullExpr = do x <- pExpr; eof; return x
44
60
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
46pExpr' = try pApp
84pExpr' = try pApp
47− <|> pSimpleExpr
85+ <|> pSimpleExpr
48− <|> try pLambda
86+ <|> try pLambda
49− <|> try pPi
87+ <|> try pPi
50−
51−pExpr = buildExpressionParser table pExpr'
52
88
53pSimpleExpr =
89pSimpleExpr =
54 try (do symbol "!["; t <- pTerm; lchar ']'
90 try (do symbol "!["; t <- pTerm; lchar ']'
@@ -79,8 +115,18 @@ pPi = do lchar '('; x <- iName; t <- pTSig; lchar ')'
79 sc <- pExpr
115 sc <- pExpr
80 return (PPi Imp x t sc)
116 return (PPi Imp x t sc)
81
117
118+table fixes
119+ = toTable (reverse fixes) ++
82−table = [[binary "=" (\x y -> PApp (PRef (UN ["="])) [] [x,y]) AssocLeft],
120+ [[binary "=" (\x y -> PApp (PRef (UN ["="])) [] [x,y]) AssocLeft],
83− [binary "->" (PPi Exp (MN 0 "X")) AssocRight]]
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
84
130
85binary name f assoc = Infix (do { reservedOp name; return f }) assoc
131binary name f assoc = Infix (do { reservedOp name; return f }) assoc
86
132
src/Idris/REPL.hs+8−3
@@ -14,12 +14,14 @@ repl :: Idris ()
14repl = do x <- lift $ readline "Idris> "
14repl = do x <- lift $ readline "Idris> "
15 case x of
15 case x of
16 Nothing -> repl
16 Nothing -> repl
17+ Just input -> do lift $ addHistory input
17− Just input -> do continue <- processInput input
18+ continue <- processInput input
18 when continue repl
19 when continue repl
19
20
20processInput :: String -> Idris Bool
21processInput :: String -> Idris Bool
21processInput cmd
22processInput cmd
23+ = do i <- get
22− = case parseCmd cmd of
24+ case parseCmd i cmd of
23 Left err -> do lift $ print err
25 Left err -> do lift $ print err
24 return True
26 return True
25 Right Quit -> do iputStrLn "Bye bye"
27 Right Quit -> do iputStrLn "Bye bye"
@@ -28,5 +30,8 @@ processInput cmd
28 return True
30 return True
29
31
30process :: Command -> Idris ()
32process :: Command -> Idris ()
33+process Help
31−process Help = iputStrLn "At some point I'll write some help text. Thanks for asking though."
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 ()
32
37
src/Idris/REPLParser.hs+5−4
@@ -11,14 +11,15 @@ import qualified Text.ParserCombinators.Parsec.Token as PTok
11
11
12import Debug.Trace
12import Debug.Trace
13
13
14−parseCmd = parse pCmd "(input)"
14+parseCmd i = runParser pCmd i "(input)"
15
15
16−cmd :: [String] -> Parser ()
16+cmd :: [String] -> IParser ()
17cmd xs = do lchar ':'; docmd xs
17cmd xs = do lchar ':'; docmd xs
18 where docmd [] = fail "No such command"
18 where docmd [] = fail "No such command"
19 docmd (x:xs) = try (void (symbol x)) <|> docmd xs
19 docmd (x:xs) = try (void (symbol x)) <|> docmd xs
20
20
21−pCmd :: Parser Command
21+pCmd :: IParser Command
22pCmd = try (do cmd ["q", "quit"]; return Quit)
22pCmd = try (do cmd ["q", "quit"]; return Quit)
23 <|> try (do cmd ["h", "?", "help"]; return Help)
23 <|> 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 =
41
41
42loadModule :: FilePath -> Idris ()
42loadModule :: FilePath -> Idris ()
43loadModule f = do iLOG ("Reading " ++ show f)
43loadModule f = do iLOG ("Reading " ++ show f)
44+ ds <- parseProg f
45+ iLOG (show ds)
46+ i <- get
47+ iLOG (show (idris_infixes i))
44 return ()
48 return ()
45
49
46getFile :: Opt -> Maybe String
50getFile :: Opt -> Maybe String