git.iko.soy/Idris-dev
on ebcb29b help sign in
Idris-dev/src/Core/CoreParser.hs
139 lines 4.7 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
3module Core.CoreParser(parseTerm, parseFile, parseDef, pTerm, iName, idrisDef) where
5import Core.TT
7import Text.ParserCombinators.Parsec
8import Text.ParserCombinators.Parsec.Expr
9import Text.ParserCombinators.Parsec.Language
10import qualified Text.ParserCombinators.Parsec.Token as PTok
12import Control.Monad.State
13import Debug.Trace
15type TokenParser a = PTok.TokenParser a
17idrisDef = haskellDef {
18 opStart = iOpStart,
19 opLetter = iOpLetter,
20 reservedOpNames = [":", "..", "=", "\\", "|", "<-", "->", "=>", "**"],
21 reservedNames = ["let", "in", "data", "Set", -- "if", "then", "else",
22 "do", "dsl", "import", "return", "refl",
23 "infix", "infixl", "infixr", "prefix",
24 "where", "with", "forall", "syntax", "proof",
25 "using", "params", "namespace",
26 "Int", "Float", "Char", "String", "Ptr"]
27 }
29iOpStart = oneOf ":!#$%&*+./<=>?@\\^|-~"
30iOpLetter = oneOf ":!#$%&*+./<=>?@\\^|-~"
31 <|> letter
33lexer :: TokenParser a
34lexer = PTok.makeTokenParser idrisDef
36whiteSpace= PTok.whiteSpace lexer
37lexeme = PTok.lexeme lexer
38symbol = PTok.symbol lexer
39natural = PTok.natural lexer
40parens = PTok.parens lexer
41semi = PTok.semi lexer
42comma = PTok.comma lexer
43identifier= PTok.identifier lexer
44reserved = PTok.reserved lexer
45operator = PTok.operator lexer
46reservedOp= PTok.reservedOp lexer
47lchar = lexeme.char
49type CParser a = GenParser Char a
51parseFile = runParser pTestFile () "(input)"
52parseDef = runParser pDef () "(input)"
53parseTerm = runParser pTerm () "(input)"
55pTestFile :: CParser a RProgram
56pTestFile = do p <- many1 pDef ; eof
57 return p
59iName :: [String] -> CParser a Name
60iName bad = do x <- identifier
61 when (x `elem` bad) $ fail "Reserved identifier"
62 return (UN [x])
64pDef :: CParser a (Name, RDef)
65pDef = try (do x <- iName []; lchar ':'; ty <- pTerm
66 lchar '='
67 tm <- pTerm
68 lchar ';'
69 return (x, RFunction (RawFun ty tm)))
70 <|> do x <- iName []; lchar ':'; ty <- pTerm; lchar ';'
71 return (x, RConst ty)
72 <|> do (x, d) <- pData; lchar ';'
73 return (x, RData d)
75app :: CParser a (Raw -> Raw -> Raw)
76app = do whiteSpace ; return RApp
78arrow :: CParser a (Raw -> Raw -> Raw)
79arrow = do symbol "->" ; return $ \s t -> RBind (MN 0 "X") (Pi s) t
81pTerm :: CParser a Raw
82pTerm = try (do chainl1 pNoApp app)
83 <|> pNoApp
85pNoApp :: CParser a Raw
86pNoApp = try (chainr1 pExp arrow)
87 <|> pExp
88pExp :: CParser a Raw
89pExp = do lchar '\\'; x <- iName []; lchar ':'; ty <- pTerm
90 symbol "=>";
91 sc <- pTerm
92 return (RBind x (Lam ty) sc)
93 <|> try (do lchar '?'; x <- iName []; lchar ':'; ty <- pTerm
94 lchar '.';
95 sc <- pTerm
96 return (RBind x (Hole ty) sc))
97 <|> try (do lchar '(';
98 x <- iName []; lchar ':'; ty <- pTerm
99 lchar ')';
100 symbol "->";
101 sc <- pTerm
102 return (RBind x (Pi ty) sc))
103 <|> try (do lchar '(';
104 t <- pTerm
105 lchar ')'
106 return t)
107 <|> try (do symbol "??";
108 x <- iName []; lchar ':'; ty <- pTerm
109 lchar '=';
110 val <- pTerm
111 sc <- pTerm
112 return (RBind x (Guess ty val) sc))
113 <|> try (do reserved "let";
114 x <- iName []; lchar ':'; ty <- pTerm
115 lchar '=';
116 val <- pTerm
117 reserved "in";
118 sc <- pTerm
119 return (RBind x (Let ty val) sc))
120 <|> try (do lchar '_';
121 x <- iName []; lchar ':'; ty <- pTerm
122 lchar '.';
123 sc <- pTerm
124 return (RBind x (PVar ty) sc))
125 <|> try (do reserved "Set"; i <- option 0 natural
126 return (RSet (fromInteger i)))
127 <|> try (do x <- iName []
128 return (Var x))
130pData :: CParser a (Name, RawDatatype)
131pData = do reserved "data"; x <- iName []; lchar ':'; ty <- pTerm; reserved "where"
132 cs <- many pConstructor
133 return (x, RDatatype x ty cs)
135pConstructor :: CParser a (Name, Raw)
136pConstructor = do lchar '|'
137 c <- iName []; lchar ':'; ty <- pTerm
138 return (c, ty)