git.iko.soy/Idris-dev
on be33671 help sign in
Idris-dev/src/Core/CoreParser.hs
146 lines 5.0 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 identLetter = identLetter haskellDef <|> lchar '.',
21 reservedOpNames = [":", "..", "=", "\\", "|", "<-", "->", "=>", "**"],
22 reservedNames = ["let", "in", "data", "Set", -- "if", "then", "else",
23 "do", "dsl", "import", -- "refl",
24 "infix", "infixl", "infixr", "prefix",
25 "where", "with", "forall", "syntax", "proof",
26 "using", "params", "namespace", "class", "instance",
27 "Int", "Integer", "Float", "Char", "String", "Ptr"]
28 }
30iOpStart = oneOf ":!#$%&*+./<=>?@\\^|-~"
31iOpLetter = oneOf ":!#$%&*+./<=>?@\\^|-~"
32-- <|> letter
34lexer :: TokenParser a
35lexer = PTok.makeTokenParser idrisDef
37whiteSpace= PTok.whiteSpace lexer
38lexeme = PTok.lexeme lexer
39symbol = PTok.symbol lexer
40natural = PTok.natural lexer
41parens = PTok.parens lexer
42semi = PTok.semi lexer
43comma = PTok.comma lexer
44identifier= PTok.identifier lexer
45reserved = PTok.reserved lexer
46operator = PTok.operator lexer
47reservedOp= PTok.reservedOp lexer
48lchar = lexeme.char
50type CParser a = GenParser Char a
52parseFile = runParser pTestFile () "(input)"
53parseDef = runParser pDef () "(input)"
54parseTerm = runParser pTerm () "(input)"
56pTestFile :: CParser a RProgram
57pTestFile = do p <- many1 pDef ; eof
58 return p
60iName :: [String] -> CParser a Name
61iName bad = do x <- identifier
62 when (x `elem` bad) $ fail "Reserved identifier"
63 return $ mkNS (reverse (parseName x))
64 where
65 mkNS [x] = UN x
66 mkNS (x:xs) = NS (UN x) xs
67 parseName x = case span (/= '.') x of
68 (x, "") -> [x]
69 (x, '.':y) -> x : parseName y
71pDef :: CParser a (Name, RDef)
72pDef = try (do x <- iName []; lchar ':'; ty <- pTerm
73 lchar '='
74 tm <- pTerm
75 lchar ';'
76 return (x, RFunction (RawFun ty tm)))
77 <|> do x <- iName []; lchar ':'; ty <- pTerm; lchar ';'
78 return (x, RConst ty)
79 <|> do (x, d) <- pData; lchar ';'
80 return (x, RData d)
82app :: CParser a (Raw -> Raw -> Raw)
83app = do whiteSpace ; return RApp
85arrow :: CParser a (Raw -> Raw -> Raw)
86arrow = do symbol "->" ; return $ \s t -> RBind (MN 0 "X") (Pi s) t
88pTerm :: CParser a Raw
89pTerm = try (do chainl1 pNoApp app)
90 <|> pNoApp
92pNoApp :: CParser a Raw
93pNoApp = try (chainr1 pExp arrow)
94 <|> pExp
95pExp :: CParser a Raw
96pExp = do lchar '\\'; x <- iName []; lchar ':'; ty <- pTerm
97 symbol "=>";
98 sc <- pTerm
99 return (RBind x (Lam ty) sc)
100 <|> try (do lchar '?'; x <- iName []; lchar ':'; ty <- pTerm
101 lchar '.';
102 sc <- pTerm
103 return (RBind x (Hole ty) sc))
104 <|> try (do lchar '(';
105 x <- iName []; lchar ':'; ty <- pTerm
106 lchar ')';
107 symbol "->";
108 sc <- pTerm
109 return (RBind x (Pi ty) sc))
110 <|> try (do lchar '(';
111 t <- pTerm
112 lchar ')'
113 return t)
114 <|> try (do symbol "??";
115 x <- iName []; lchar ':'; ty <- pTerm
116 lchar '=';
117 val <- pTerm
118 sc <- pTerm
119 return (RBind x (Guess ty val) sc))
120 <|> try (do reserved "let";
121 x <- iName []; lchar ':'; ty <- pTerm
122 lchar '=';
123 val <- pTerm
124 reserved "in";
125 sc <- pTerm
126 return (RBind x (Let ty val) sc))
127 <|> try (do lchar '_';
128 x <- iName []; lchar ':'; ty <- pTerm
129 lchar '.';
130 sc <- pTerm
131 return (RBind x (PVar ty) sc))
132 <|> try (do reserved "Set"
133 return RSet)
134 <|> try (do x <- iName []
135 return (Var x))
137pData :: CParser a (Name, RawDatatype)
138pData = do reserved "data"; x <- iName []; lchar ':'; ty <- pTerm; reserved "where"
139 cs <- many pConstructor
140 return (x, RDatatype x ty cs)
142pConstructor :: CParser a (Name, Raw)
143pConstructor = do lchar '|'
144 c <- iName []; lchar ':'; ty <- pTerm
145 return (c, ty)