git.iko.soy/Idris-dev
on 264b67f help sign in
Idris-dev/src/Core/CoreParser.hs
174 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 reservedNames = ["let", "in", "data", "codata", "record", "Set",
24 "do", "dsl", "import", "impossible",
25 "case", "of", "total", "partial",
26 "infix", "infixl", "infixr",
27 "where", "with", "syntax", "proof", "postulate",
28 "using", "namespace", "class", "instance",
29 "public", "private", "abstract",
30 "Int", "Integer", "Float", "Char", "String", "Ptr"]
31 }
33iOpStart = oneOf ":!#$%&*+./<=>?@\\^|-~"
34iOpLetter = oneOf ":!#$%&*+./<=>?@\\^|-~"
35-- <|> letter
37lexer :: TokenParser a
38lexer = PTok.makeTokenParser idrisDef
40whiteSpace= PTok.whiteSpace lexer
41lexeme = PTok.lexeme lexer
42symbol = PTok.symbol lexer
43natural = PTok.natural lexer
44parens = PTok.parens lexer
45semi = PTok.semi lexer
46comma = PTok.comma lexer
47identifier= PTok.identifier lexer
48reserved = PTok.reserved lexer
49operator = PTok.operator lexer
50reservedOp= PTok.reservedOp lexer
51lchar = lexeme.char
53type CParser a = GenParser Char a
55parseFile = runParser pTestFile () "(input)"
56parseDef = runParser pDef () "(input)"
57parseTerm = runParser pTerm () "(input)"
59pTestFile :: CParser a RProgram
60pTestFile = do p <- many1 pDef ; eof
61 return p
63iName :: [String] -> CParser a Name
64iName bad = maybeWithNS identifier False bad
66-- Enhances a given parser to accept an optional namespace. All possible
67-- namespace prefixes are tried in ascending / descending order, and
68-- identifiers of a given list fail.
69maybeWithNS :: CParser a String -> Bool -> [String] -> CParser a Name
70maybeWithNS parser ascend bad = do
71 i <- option "" (lookAhead identifier)
72 when (i `elem` bad) $ fail "Reserved identifier"
73 let transf = if ascend then id else reverse
74 (x, xs) <- choice $ transf (parserNoNS : parsersNS i)
75 return $ mkName (x, xs)
76 where
77 parserNoNS = do x <- parser; return (x, "")
78 parserNS ns = do xs <- string ns; lchar '.'; x <- parser; return (x, xs)
79 parsersNS i = [try (parserNS ns) | ns <- (initsEndAt (=='.') i)]
81-- List of all initial segments in ascending order of a list. Every such
82-- initial segment ends right before an element satisfying the given
83-- condition.
84initsEndAt :: (a -> Bool) -> [a] -> [[a]]
85initsEndAt p [] = []
86initsEndAt p (x:xs) | p x = [] : x_inits_xs
87 | otherwise = x_inits_xs
88 where x_inits_xs = [x : cs | cs <- initsEndAt p xs]
90-- Create a `Name' from a pair of strings representing a base name and its
91-- namespace.
92mkName :: (String, String) -> Name
93mkName (n, "") = UN n
94mkName (n, ns) = NS (UN n) (reverse (parseNS ns))
95 where parseNS x = case span (/= '.') x of
96 (x, "") -> [x]
97 (x, '.':y) -> x : parseNS y
99pDef :: CParser a (Name, RDef)
100pDef = try (do x <- iName []; lchar ':'; ty <- pTerm
101 lchar '='
102 tm <- pTerm
103 lchar ';'
104 return (x, RFunction (RawFun ty tm)))
105 <|> do x <- iName []; lchar ':'; ty <- pTerm; lchar ';'
106 return (x, RConst ty)
107 <|> do (x, d) <- pData; lchar ';'
108 return (x, RData d)
110app :: CParser a (Raw -> Raw -> Raw)
111app = do whiteSpace ; return RApp
113arrow :: CParser a (Raw -> Raw -> Raw)
114arrow = do symbol "->" ; return $ \s t -> RBind (MN 0 "X") (Pi s) t
116pTerm :: CParser a Raw
117pTerm = try (do chainl1 pNoApp app)
118 <|> pNoApp
120pNoApp :: CParser a Raw
121pNoApp = try (chainr1 pExp arrow)
122 <|> pExp
123pExp :: CParser a Raw
124pExp = do lchar '\\'; x <- iName []; lchar ':'; ty <- pTerm
125 symbol "=>";
126 sc <- pTerm
127 return (RBind x (Lam ty) sc)
128 <|> try (do lchar '?'; x <- iName []; lchar ':'; ty <- pTerm
129 lchar '.';
130 sc <- pTerm
131 return (RBind x (Hole ty) sc))
132 <|> try (do lchar '(';
133 x <- iName []; lchar ':'; ty <- pTerm
134 lchar ')';
135 symbol "->";
136 sc <- pTerm
137 return (RBind x (Pi ty) sc))
138 <|> try (do lchar '(';
139 t <- pTerm
140 lchar ')'
141 return t)
142 <|> try (do symbol "??";
143 x <- iName []; lchar ':'; ty <- pTerm
144 lchar '=';
145 val <- pTerm
146 sc <- pTerm
147 return (RBind x (Guess ty val) sc))
148 <|> try (do reserved "let";
149 x <- iName []; lchar ':'; ty <- pTerm
150 lchar '=';
151 val <- pTerm
152 reserved "in";
153 sc <- pTerm
154 return (RBind x (Let ty val) sc))
155 <|> try (do lchar '_';
156 x <- iName []; lchar ':'; ty <- pTerm
157 lchar '.';
158 sc <- pTerm
159 return (RBind x (PVar ty) sc))
160 <|> try (do reserved "Set"
161 return RSet)
162 <|> try (do x <- iName []
163 return (Var x))
165pData :: CParser a (Name, RawDatatype)
166pData = do reserved "data"; x <- iName []; lchar ':'; ty <- pTerm; reserved "where"
167 cs <- many pConstructor
168 return (x, RDatatype x ty cs)
170pConstructor :: CParser a (Name, Raw)
171pConstructor = do lchar '|'
172 c <- iName []; lchar ':'; ty <- pTerm
173 return (c, ty)