git.iko.soy/Idris-dev
on 9c6ea4a help sign in
Idris-dev/src/CoreParser.hs
111 lines 3.4 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)
51app :: Parser (Raw -> Raw -> Raw)
52app = do whiteSpace ; return RApp
54arrow :: Parser (Raw -> Raw -> Raw)
55arrow = do symbol "->" ; return $ \s t -> RBind (MN 0 "X") (Pi s) t
57pTerm :: Parser Raw
58pTerm = try (do chainl1 pNoApp app)
59 <|> pNoApp
61pNoApp :: Parser Raw
62pNoApp = try (chainr1 pExp arrow)
63 <|> pExp
65pExp :: Parser Raw
66pExp = do lchar '\\'; x <- iName; lchar ':'; ty <- pTerm
67 symbol "=>";
68 sc <- pTerm
69 return (RBind x (Lam ty) sc)
70 <|> try (do lchar '?'; x <- iName; lchar ':'; ty <- pTerm
71 lchar '.';
72 sc <- pTerm
73 return (RBind x (Lam ty) sc))
74 <|> try (do lchar '(';
75 x <- iName; lchar ':'; ty <- pTerm
76 lchar ')';
77 symbol "->";
78 sc <- pTerm
79 return (RBind x (Pi ty) sc))
80 <|> try (do lchar '(';
81 t <- pTerm
82 lchar ')'
83 return t)
84 <|> try (do lchar '?';
85 x <- iName; lchar ':'; ty <- pTerm
86 lchar '.';
87 sc <- pTerm
88 return (RBind x (Hole ty) sc))
89 <|> try (do symbol "??";
90 x <- iName; lchar ':'; ty <- pTerm
91 lchar '=';
92 val <- pTerm
93 sc <- pTerm
94 return (RBind x (Guess ty val) sc))
95 <|> try (do reserved "let";
96 x <- iName; lchar ':'; ty <- pTerm
97 lchar '=';
98 val <- pTerm
99 reserved "in";
100 sc <- pTerm
101 return (RBind x (Let ty val) sc))
102 <|> try (do lchar '_';
103 x <- iName; lchar ':'; ty <- pTerm
104 lchar '.';
105 sc <- pTerm
106 return (RBind x (PVar ty) sc))
107 <|> try (do reserved "Set"; i <- natural
108 return (RSet (fromInteger i)))
109 <|> try (do x <- iName
110 return (Var x))