git.iko.soy/Idris-dev
on bb6bba2 help sign in
Idris-dev/src/CoreParser.hs
107 lines 3.4 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
3module CoreParser(parseTerm, parseFile, parseDef, pTerm) 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
39pDef :: Parser (Name, RDef)
40pDef = try (do x <- identifier; lchar ':'; ty <- pTerm
41 lchar '='
42 tm <- pTerm
43 lchar ';'
44 return (UN [x], RFunction (RawFun ty tm)))
45 <|> do x <- identifier; lchar ':'; ty <- pTerm; lchar ';'
46 return (UN [x], RConst ty)
48app :: Parser (Raw -> Raw -> Raw)
49app = do whiteSpace ; return RApp
51arrow :: Parser (Raw -> Raw -> Raw)
52arrow = do symbol "->" ; return $ \s t -> RBind (MN 0 "X") (Pi s) t
54pTerm :: Parser Raw
55pTerm = try (do chainl1 pNoApp app)
56 <|> pNoApp
58pNoApp :: Parser Raw
59pNoApp = try (chainr1 pExp arrow)
60 <|> pExp
62pExp :: Parser Raw
63pExp = do lchar '\\'; x <- identifier; lchar ':'; ty <- pTerm
64 symbol "=>";
65 sc <- pTerm
66 return (RBind (UN [x]) (Lam ty) sc)
67 <|> try (do lchar '?'; x <- identifier; lchar ':'; ty <- pTerm
68 lchar '.';
69 sc <- pTerm
70 return (RBind (UN [x]) (Lam ty) sc))
71 <|> try (do lchar '(';
72 x <- identifier; lchar ':'; ty <- pTerm
73 lchar ')';
74 symbol "->";
75 sc <- pTerm
76 return (RBind (UN [x]) (Pi ty) sc))
77 <|> try (do lchar '(';
78 t <- pTerm
79 lchar ')'
80 return t)
81 <|> try (do lchar '?';
82 x <- identifier; lchar ':'; ty <- pTerm
83 lchar '.';
84 sc <- pTerm
85 return (RBind (UN [x]) (Hole ty) sc))
86 <|> try (do symbol "??";
87 x <- identifier; lchar ':'; ty <- pTerm
88 lchar '=';
89 val <- pTerm
90 sc <- pTerm
91 return (RBind (UN [x]) (Guess ty val) sc))
92 <|> try (do reserved "let";
93 x <- identifier; lchar ':'; ty <- pTerm
94 lchar '=';
95 val <- pTerm
96 sc <- pTerm
97 return (RBind (UN [x]) (Let ty val) sc))
98 <|> try (do lchar '_';
99 x <- identifier; lchar ':'; ty <- pTerm
100 lchar '.';
101 sc <- pTerm
102 return (RBind (UN [x]) (PVar ty) sc))
103 <|> try (do reserved "Set"; i <- natural
104 return (RSet (fromInteger i)))
105 <|> try (do x <- identifier
106 return (Var (UN [x])))