git.iko.soy/Idris-dev
on 5dadd08 help sign in
Idris-dev/src/CoreParser.hs
124 lines 3.9 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
3module CoreParser(parseTerm, parseFile, parseDef, pTerm, iName) where
5import Core
7import Text.ParserCombinators.Parsec
8import Text.ParserCombinators.Parsec.Expr
9import Text.ParserCombinators.Parsec.Language
10import qualified Text.ParserCombinators.Parsec.Token as PTok
12import Debug.Trace
14type TokenParser a = PTok.TokenParser a
16lexer :: TokenParser ()
17lexer = PTok.makeTokenParser haskellDef
19whiteSpace= PTok.whiteSpace lexer
20lexeme = PTok.lexeme lexer
21symbol = PTok.symbol lexer
22natural = PTok.natural lexer
23parens = PTok.parens lexer
24semi = PTok.semi lexer
25comma = PTok.comma lexer
26identifier= PTok.identifier lexer
27reserved = PTok.reserved lexer
28operator = PTok.operator lexer
29reservedOp= PTok.reservedOp lexer
30lchar = lexeme.char
32parseFile = parse pTestFile "(input)"
33parseDef = parse pDef "(input)"
34parseTerm = parse pTerm "(input)"
36pTestFile :: Parser RProgram
37pTestFile = do p <- many1 pDef ; eof
38 return p
40iName :: Parser Name
41iName = identifier >>= (\n -> return (UN [n]))
43pDef :: Parser (Name, RDef)
44pDef = try (do x <- iName; lchar ':'; ty <- pTerm
45 lchar '='
46 tm <- pTerm
47 lchar ';'
48 return (x, RFunction (RawFun ty tm)))
49 <|> do x <- iName; lchar ':'; ty <- pTerm; lchar ';'
50 return (x, RConst ty)
51 <|> do (x, d) <- pData; lchar ';'
52 return (x, RData d)
54app :: Parser (Raw -> Raw -> Raw)
55app = do whiteSpace ; return RApp
57arrow :: Parser (Raw -> Raw -> Raw)
58arrow = do symbol "->" ; return $ \s t -> RBind (MN 0 "X") (Pi s) t
60pTerm :: Parser Raw
61pTerm = try (do chainl1 pNoApp app)
62 <|> pNoApp
64pNoApp :: Parser Raw
65pNoApp = try (chainr1 pExp arrow)
66 <|> pExp
68pExp :: Parser Raw
69pExp = do lchar '\\'; x <- iName; lchar ':'; ty <- pTerm
70 symbol "=>";
71 sc <- pTerm
72 return (RBind x (Lam ty) sc)
73 <|> try (do lchar '?'; x <- iName; lchar ':'; ty <- pTerm
74 lchar '.';
75 sc <- pTerm
76 return (RBind x (Lam ty) sc))
77 <|> try (do lchar '(';
78 x <- iName; lchar ':'; ty <- pTerm
79 lchar ')';
80 symbol "->";
81 sc <- pTerm
82 return (RBind x (Pi ty) sc))
83 <|> try (do lchar '(';
84 t <- pTerm
85 lchar ')'
86 return t)
87 <|> try (do lchar '?';
88 x <- iName; lchar ':'; ty <- pTerm
89 lchar '.';
90 sc <- pTerm
91 return (RBind x (Hole ty) sc))
92 <|> try (do symbol "??";
93 x <- iName; lchar ':'; ty <- pTerm
94 lchar '=';
95 val <- pTerm
96 sc <- pTerm
97 return (RBind x (Guess ty val) sc))
98 <|> try (do reserved "let";
99 x <- iName; lchar ':'; ty <- pTerm
100 lchar '=';
101 val <- pTerm
102 reserved "in";
103 sc <- pTerm
104 return (RBind x (Let ty val) sc))
105 <|> try (do lchar '_';
106 x <- iName; lchar ':'; ty <- pTerm
107 lchar '.';
108 sc <- pTerm
109 return (RBind x (PVar ty) sc))
110 <|> try (do reserved "Set"; i <- option 0 natural
111 return (RSet (fromInteger i)))
112 <|> try (do x <- iName
113 return (Var x))
115pData :: Parser (Name, RawDatatype)
116pData = do reserved "data"; x <- iName; lchar ':'; ty <- pTerm; reserved "where"
117 cs <- many pConstructor
118 return (x, RDatatype x ty cs)
120pConstructor :: Parser (Name, Raw)
121pConstructor = do lchar '|'
122 c <- iName; lchar ':'; ty <- pTerm
123 return (c, ty)