git.iko.soy/Idris-dev
on master help sign in
Minor parser changes
56309a5Edwin Brady
src/CoreParser.hs+24−21
compare with master
unifiedsplit
@@ -1,6 +1,6 @@
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
2
2
3−module CoreParser(parseTerm, parseFile, parseDef, pTerm) where
3+module CoreParser(parseTerm, parseFile, parseDef, pTerm, iName) where
4
4
5import Core
5import Core
6
6
@@ -36,14 +36,17 @@ parseTerm = parse pTerm "(input)"
36pTestFile :: Parser RProgram
36pTestFile :: Parser RProgram
37pTestFile = many1 pDef
37pTestFile = many1 pDef
38
38
39+iName :: Parser Name
40+iName = identifier >>= (\n -> return (UN [n]))
41+
39pDef :: Parser (Name, RDef)
42pDef :: Parser (Name, RDef)
40−pDef = try (do x <- identifier; lchar ':'; ty <- pTerm
43+pDef = try (do x <- iName; lchar ':'; ty <- pTerm
41 lchar '='
44 lchar '='
42 tm <- pTerm
45 tm <- pTerm
43 lchar ';'
46 lchar ';'
44− return (UN [x], RFunction (RawFun ty tm)))
47+ return (x, RFunction (RawFun ty tm)))
45− <|> do x <- identifier; lchar ':'; ty <- pTerm; lchar ';'
48+ <|> do x <- iName; lchar ':'; ty <- pTerm; lchar ';'
46− return (UN [x], RConst ty)
49+ return (x, RConst ty)
47
50
48app :: Parser (Raw -> Raw -> Raw)
51app :: Parser (Raw -> Raw -> Raw)
49app = do whiteSpace ; return RApp
52app = do whiteSpace ; return RApp
@@ -60,48 +63,48 @@ pNoApp = try (chainr1 pExp arrow)
60 <|> pExp
63 <|> pExp
61
64
62pExp :: Parser Raw
65pExp :: Parser Raw
63−pExp = do lchar '\\'; x <- identifier; lchar ':'; ty <- pTerm
66+pExp = do lchar '\\'; x <- iName; lchar ':'; ty <- pTerm
64 symbol "=>";
67 symbol "=>";
65 sc <- pTerm
68 sc <- pTerm
66− return (RBind (UN [x]) (Lam ty) sc)
69+ return (RBind x (Lam ty) sc)
67− <|> try (do lchar '?'; x <- identifier; lchar ':'; ty <- pTerm
70+ <|> try (do lchar '?'; x <- iName; lchar ':'; ty <- pTerm
68 lchar '.';
71 lchar '.';
69 sc <- pTerm
72 sc <- pTerm
70− return (RBind (UN [x]) (Lam ty) sc))
73+ return (RBind x (Lam ty) sc))
71 <|> try (do lchar '(';
74 <|> try (do lchar '(';
72− x <- identifier; lchar ':'; ty <- pTerm
75+ x <- iName; lchar ':'; ty <- pTerm
73 lchar ')';
76 lchar ')';
74 symbol "->";
77 symbol "->";
75 sc <- pTerm
78 sc <- pTerm
76− return (RBind (UN [x]) (Pi ty) sc))
79+ return (RBind x (Pi ty) sc))
77 <|> try (do lchar '(';
80 <|> try (do lchar '(';
78 t <- pTerm
81 t <- pTerm
79 lchar ')'
82 lchar ')'
80 return t)
83 return t)
81 <|> try (do lchar '?';
84 <|> try (do lchar '?';
82− x <- identifier; lchar ':'; ty <- pTerm
85+ x <- iName; lchar ':'; ty <- pTerm
83 lchar '.';
86 lchar '.';
84 sc <- pTerm
87 sc <- pTerm
85− return (RBind (UN [x]) (Hole ty) sc))
88+ return (RBind x (Hole ty) sc))
86 <|> try (do symbol "??";
89 <|> try (do symbol "??";
87− x <- identifier; lchar ':'; ty <- pTerm
90+ x <- iName; lchar ':'; ty <- pTerm
88 lchar '=';
91 lchar '=';
89 val <- pTerm
92 val <- pTerm
90 sc <- pTerm
93 sc <- pTerm
91− return (RBind (UN [x]) (Guess ty val) sc))
94+ return (RBind x (Guess ty val) sc))
92 <|> try (do reserved "let";
95 <|> try (do reserved "let";
93− x <- identifier; lchar ':'; ty <- pTerm
96+ x <- iName; lchar ':'; ty <- pTerm
94 lchar '=';
97 lchar '=';
95 val <- pTerm
98 val <- pTerm
96 sc <- pTerm
99 sc <- pTerm
97− return (RBind (UN [x]) (Let ty val) sc))
100+ return (RBind x (Let ty val) sc))
98 <|> try (do lchar '_';
101 <|> try (do lchar '_';
99− x <- identifier; lchar ':'; ty <- pTerm
102+ x <- iName; lchar ':'; ty <- pTerm
100 lchar '.';
103 lchar '.';
101 sc <- pTerm
104 sc <- pTerm
102− return (RBind (UN [x]) (PVar ty) sc))
105+ return (RBind x (PVar ty) sc))
103 <|> try (do reserved "Set"; i <- natural
106 <|> try (do reserved "Set"; i <- natural
104 return (RSet (fromInteger i)))
107 return (RSet (fromInteger i)))
105− <|> try (do x <- identifier
108+ <|> try (do x <- iName
106− return (Var (UN [x])))
109+ return (Var x))
107
110
src/ProofState.hs+1−1
@@ -175,7 +175,7 @@ process :: Tactic -> Name -> ProofState -> StateT TState TC ProofState
175process t h ps = tactic (Just h) ps (context ps) (mktac t)
175process t h ps = tactic (Just h) ps (context ps) (mktac t)
176 where mktac Attack = attack
176 where mktac Attack = attack
177 mktac (Claim n r) = claim n r
177 mktac (Claim n r) = claim n r
178− mktac (Fill r) = fill r
178+ mktac (Fill r) = fill r
179 mktac Regret = regret
179 mktac Regret = regret
180 mktac Solve = solve
180 mktac Solve = solve
181 mktac (Intro n) = intro n
181 mktac (Intro n) = intro n
src/ShellParser.hs+4−5
@@ -35,7 +35,7 @@ parseCommand = parse pCommand "(input)"
35parseTactic = parse (pTactic >>= return . Tac) "(input)"
35parseTactic = parse (pTactic >>= return . Tac) "(input)"
36
36
37pCommand :: Parser Command
37pCommand :: Parser Command
38−pCommand = do reserved "theorem"; n <- iname; lchar ':'; ty <- pTerm
38+pCommand = do reserved "theorem"; n <- iName; lchar ':'; ty <- pTerm
39 return (Theorem n ty)
39 return (Theorem n ty)
40 <|> do reserved "eval"; tm <- pTerm
40 <|> do reserved "eval"; tm <- pTerm
41 return (Eval tm)
41 return (Eval tm)
@@ -44,14 +44,13 @@ pCommand = do reserved "theorem"; n <- iname; lchar ':'; ty <- pTerm
44
44
45pTactic :: Parser Tactic
45pTactic :: Parser Tactic
46pTactic = do reserved "attack"; return Attack
46pTactic = do reserved "attack"; return Attack
47− <|> do reserved "claim"; n <- iname; lchar ':'; ty <- pTerm
47+ <|> do reserved "claim"; n <- iName; lchar ':'; ty <- pTerm
48 return (Claim n ty)
48 return (Claim n ty)
49 <|> do reserved "fill"; tm <- pTerm; return (Fill tm)
49 <|> do reserved "fill"; tm <- pTerm; return (Fill tm)
50 <|> do reserved "regret"; return Regret
50 <|> do reserved "regret"; return Regret
51 <|> do reserved "solve"; return Solve
51 <|> do reserved "solve"; return Solve
52− <|> do reserved "intro"; n <- iname; return (Intro n)
52+ <|> do reserved "intro"; n <- iName; return (Intro n)
53 <|> do reserved "state"; return ProofState
53 <|> do reserved "state"; return ProofState
54 <|> do reserved "qed"; return QED
54 <|> do reserved "qed"; return QED
55
55
56−iname :: Parser Name
56+
57−iname = identifier >>= (\n -> return (UN [n]))