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