git.iko.soy/Idris-dev
on 07f3b19 help sign in
Idris-dev/src/CoreParser.hs
123 lines 3.8 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 = many1 pDef
39iName :: Parser Name
40iName = identifier >>= (\n -> return (UN [n]))
42pDef :: Parser (Name, RDef)
43pDef = try (do x <- iName; lchar ':'; ty <- pTerm
44 lchar '='
45 tm <- pTerm
46 lchar ';'
47 return (x, RFunction (RawFun ty tm)))
48 <|> do x <- iName; lchar ':'; ty <- pTerm; lchar ';'
49 return (x, RConst ty)
50 <|> do (x, d) <- pData
51 return (x, RData d)
53app :: Parser (Raw -> Raw -> Raw)
54app = do whiteSpace ; return RApp
56arrow :: Parser (Raw -> Raw -> Raw)
57arrow = do symbol "->" ; return $ \s t -> RBind (MN 0 "X") (Pi s) t
59pTerm :: Parser Raw
60pTerm = try (do chainl1 pNoApp app)
61 <|> pNoApp
63pNoApp :: Parser Raw
64pNoApp = try (chainr1 pExp arrow)
65 <|> pExp
67pExp :: Parser Raw
68pExp = do lchar '\\'; x <- iName; lchar ':'; ty <- pTerm
69 symbol "=>";
70 sc <- pTerm
71 return (RBind x (Lam ty) sc)
72 <|> try (do lchar '?'; x <- iName; lchar ':'; ty <- pTerm
73 lchar '.';
74 sc <- pTerm
75 return (RBind x (Lam ty) sc))
76 <|> try (do lchar '(';
77 x <- iName; lchar ':'; ty <- pTerm
78 lchar ')';
79 symbol "->";
80 sc <- pTerm
81 return (RBind x (Pi ty) sc))
82 <|> try (do lchar '(';
83 t <- pTerm
84 lchar ')'
85 return t)
86 <|> try (do lchar '?';
87 x <- iName; lchar ':'; ty <- pTerm
88 lchar '.';
89 sc <- pTerm
90 return (RBind x (Hole ty) sc))
91 <|> try (do symbol "??";
92 x <- iName; lchar ':'; ty <- pTerm
93 lchar '=';
94 val <- pTerm
95 sc <- pTerm
96 return (RBind x (Guess ty val) sc))
97 <|> try (do reserved "let";
98 x <- iName; lchar ':'; ty <- pTerm
99 lchar '=';
100 val <- pTerm
101 reserved "in";
102 sc <- pTerm
103 return (RBind x (Let ty val) sc))
104 <|> try (do lchar '_';
105 x <- iName; lchar ':'; ty <- pTerm
106 lchar '.';
107 sc <- pTerm
108 return (RBind x (PVar ty) sc))
109 <|> try (do reserved "Set"; i <- option 0 natural
110 return (RSet (fromInteger i)))
111 <|> try (do x <- iName
112 return (Var x))
114pData :: Parser (Name, RawDatatype)
115pData = do reserved "data"; x <- iName; lchar ':'; ty <- pTerm; reserved "where"
116 cs <- many pConstructor
117 return (x, RDatatype x ty cs)
119pConstructor :: Parser (Name, Raw)
120pConstructor = do lchar '|'
121 c <- iName; lchar ':'; ty <- pTerm
122 return (c, ty)