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