git.iko.soy/Idris-dev
on 4863beb help sign in
Idris-dev/src/Core/CoreParser.hs
176 lines 6.2 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
3module Core.CoreParser(parseTerm, parseFile, parseDef, pTerm, iName, idrisDef,
4 maybeWithNS) where
6import Core.TT
8import Text.ParserCombinators.Parsec
9import Text.ParserCombinators.Parsec.Expr
10import Text.ParserCombinators.Parsec.Language
11import qualified Text.ParserCombinators.Parsec.Token as PTok
13import Control.Monad.State
14import Debug.Trace
16type TokenParser a = PTok.TokenParser a
18idrisDef = haskellDef {
19 opStart = iOpStart,
20 opLetter = iOpLetter,
21 identLetter = identLetter haskellDef <|> lchar '.',
22 reservedOpNames
23 = [":", "..", "=", "\\", "|", "<-", "->", "=>", "**"],
24 reservedNames
25 = ["let", "in", "data", "codata", "record", "Set",
26 "do", "dsl", "import", "impossible",
27 "case", "of", "total", "partial", "mutual",
28 "infix", "infixl", "infixr",
29 "where", "with", "syntax", "proof", "postulate",
30 "using", "namespace", "class", "instance",
31 "public", "private", "abstract",
32 "Int", "Integer", "Float", "Char", "String", "Ptr"]
33 }
35iOpStart = oneOf ":!#$%&*+./<=>?@\\^|-~"
36iOpLetter = oneOf ":!#$%&*+./<=>?@\\^|-~"
37-- <|> letter
39lexer :: TokenParser a
40lexer = PTok.makeTokenParser idrisDef
42whiteSpace= PTok.whiteSpace lexer
43lexeme = PTok.lexeme lexer
44symbol = PTok.symbol lexer
45natural = PTok.natural lexer
46parens = PTok.parens lexer
47semi = PTok.semi lexer
48comma = PTok.comma lexer
49identifier= PTok.identifier lexer
50reserved = PTok.reserved lexer
51operator = PTok.operator lexer
52reservedOp= PTok.reservedOp lexer
53lchar = lexeme.char
55type CParser a = GenParser Char a
57parseFile = runParser pTestFile () "(input)"
58parseDef = runParser pDef () "(input)"
59parseTerm = runParser pTerm () "(input)"
61pTestFile :: CParser a RProgram
62pTestFile = do p <- many1 pDef ; eof
63 return p
65iName :: [String] -> CParser a Name
66iName bad = maybeWithNS identifier False bad
68-- Enhances a given parser to accept an optional namespace. All possible
69-- namespace prefixes are tried in ascending / descending order, and
70-- identifiers of a given list fail.
71maybeWithNS :: CParser a String -> Bool -> [String] -> CParser a Name
72maybeWithNS parser ascend bad = do
73 i <- option "" (lookAhead identifier)
74 when (i `elem` bad) $ fail "Reserved identifier"
75 let transf = if ascend then id else reverse
76 (x, xs) <- choice $ transf (parserNoNS : parsersNS i)
77 return $ mkName (x, xs)
78 where
79 parserNoNS = do x <- parser; return (x, "")
80 parserNS ns = do xs <- string ns; lchar '.'; x <- parser; return (x, xs)
81 parsersNS i = [try (parserNS ns) | ns <- (initsEndAt (=='.') i)]
83-- List of all initial segments in ascending order of a list. Every such
84-- initial segment ends right before an element satisfying the given
85-- condition.
86initsEndAt :: (a -> Bool) -> [a] -> [[a]]
87initsEndAt p [] = []
88initsEndAt p (x:xs) | p x = [] : x_inits_xs
89 | otherwise = x_inits_xs
90 where x_inits_xs = [x : cs | cs <- initsEndAt p xs]
92-- Create a `Name' from a pair of strings representing a base name and its
93-- namespace.
94mkName :: (String, String) -> Name
95mkName (n, "") = UN n
96mkName (n, ns) = NS (UN n) (reverse (parseNS ns))
97 where parseNS x = case span (/= '.') x of
98 (x, "") -> [x]
99 (x, '.':y) -> x : parseNS y
101pDef :: CParser a (Name, RDef)
102pDef = try (do x <- iName []; lchar ':'; ty <- pTerm
103 lchar '='
104 tm <- pTerm
105 lchar ';'
106 return (x, RFunction (RawFun ty tm)))
107 <|> do x <- iName []; lchar ':'; ty <- pTerm; lchar ';'
108 return (x, RConst ty)
109 <|> do (x, d) <- pData; lchar ';'
110 return (x, RData d)
112app :: CParser a (Raw -> Raw -> Raw)
113app = do whiteSpace ; return RApp
115arrow :: CParser a (Raw -> Raw -> Raw)
116arrow = do symbol "->" ; return $ \s t -> RBind (MN 0 "X") (Pi s) t
118pTerm :: CParser a Raw
119pTerm = try (do chainl1 pNoApp app)
120 <|> pNoApp
122pNoApp :: CParser a Raw
123pNoApp = try (chainr1 pExp arrow)
124 <|> pExp
125pExp :: CParser a Raw
126pExp = do lchar '\\'; x <- iName []; lchar ':'; ty <- pTerm
127 symbol "=>";
128 sc <- pTerm
129 return (RBind x (Lam ty) sc)
130 <|> try (do lchar '?'; x <- iName []; lchar ':'; ty <- pTerm
131 lchar '.';
132 sc <- pTerm
133 return (RBind x (Hole ty) sc))
134 <|> try (do lchar '(';
135 x <- iName []; lchar ':'; ty <- pTerm
136 lchar ')';
137 symbol "->";
138 sc <- pTerm
139 return (RBind x (Pi ty) sc))
140 <|> try (do lchar '(';
141 t <- pTerm
142 lchar ')'
143 return t)
144 <|> try (do symbol "??";
145 x <- iName []; lchar ':'; ty <- pTerm
146 lchar '=';
147 val <- pTerm
148 sc <- pTerm
149 return (RBind x (Guess ty val) sc))
150 <|> try (do reserved "let";
151 x <- iName []; lchar ':'; ty <- pTerm
152 lchar '=';
153 val <- pTerm
154 reserved "in";
155 sc <- pTerm
156 return (RBind x (Let ty val) sc))
157 <|> try (do lchar '_';
158 x <- iName []; lchar ':'; ty <- pTerm
159 lchar '.';
160 sc <- pTerm
161 return (RBind x (PVar ty) sc))
162 <|> try (do reserved "Set"
163 return RSet)
164 <|> try (do x <- iName []
165 return (Var x))
167pData :: CParser a (Name, RawDatatype)
168pData = do reserved "data"; x <- iName []; lchar ':'; ty <- pTerm; reserved "where"
169 cs <- many pConstructor
170 return (x, RDatatype x ty cs)
172pConstructor :: CParser a (Name, Raw)
173pConstructor = do lchar '|'
174 c <- iName []; lchar ':'; ty <- pTerm
175 return (c, ty)