56309a5 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Minor parser changes

commit56309a5de5a13e090bbec1c3a531a3fe41dee94a authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 23 Sep 2011, 02:11 (15 years ago) parentbb6bba2

3 files changed+29−27

compare with master

unifiedsplit

src/CoreParser.hs+24−21 src/ProofState.hs+1−1 src/ShellParser.hs+4−5

src/CoreParser.hs+24−21

@@ -1,6 +1,6 @@

11{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

3−module CoreParser(parseTerm, parseFile, parseDef, pTerm) where

3+module CoreParser(parseTerm, parseFile, parseDef, pTerm, iName) where

55import Core

@@ -36,14 +36,17 @@ parseTerm = parse pTerm "(input)"

3636pTestFile :: Parser RProgram

3737pTestFile = many1 pDef

3838

39+iName :: Parser Name

40+iName = identifier >>= (\n -> return (UN [n]))

41+

3942pDef :: Parser (Name, RDef)

40−pDef = try (do x <- identifier; lchar ':'; ty <- pTerm

43+pDef = try (do x <- iName; lchar ':'; ty <- pTerm

4144 lchar '='

4245 tm <- pTerm

4346 lchar ';'

44− return (UN [x], RFunction (RawFun ty tm)))

45− <|> do x <- identifier; lchar ':'; ty <- pTerm; lchar ';'

46− return (UN [x], RConst ty)

47+ return (x, RFunction (RawFun ty tm)))

48+ <|> do x <- iName; lchar ':'; ty <- pTerm; lchar ';'

49+ return (x, RConst ty)

4750

4851app :: Parser (Raw -> Raw -> Raw)

4952app = do whiteSpace ; return RApp

@@ -60,48 +63,48 @@ pNoApp = try (chainr1 pExp arrow)

6063 <|> pExp

6164

6265pExp :: Parser Raw

63−pExp = do lchar '\\'; x <- identifier; lchar ':'; ty <- pTerm

66+pExp = do lchar '\\'; x <- iName; lchar ':'; ty <- pTerm

6467 symbol "=>";

6568 sc <- pTerm

66− return (RBind (UN [x]) (Lam ty) sc)

67− <|> try (do lchar '?'; x <- identifier; lchar ':'; ty <- pTerm

69+ return (RBind x (Lam ty) sc)

70+ <|> try (do lchar '?'; x <- iName; lchar ':'; ty <- pTerm

6871 lchar '.';

6972 sc <- pTerm

70− return (RBind (UN [x]) (Lam ty) sc))

73+ return (RBind x (Lam ty) sc))

7174 <|> try (do lchar '(';

72− x <- identifier; lchar ':'; ty <- pTerm

75+ x <- iName; lchar ':'; ty <- pTerm

7376 lchar ')';

7477 symbol "->";

7578 sc <- pTerm

76− return (RBind (UN [x]) (Pi ty) sc))

79+ return (RBind x (Pi ty) sc))

7780 <|> try (do lchar '(';

7881 t <- pTerm

7982 lchar ')'

8083 return t)

8184 <|> try (do lchar '?';

82− x <- identifier; lchar ':'; ty <- pTerm

85+ x <- iName; lchar ':'; ty <- pTerm

8386 lchar '.';

8487 sc <- pTerm

85− return (RBind (UN [x]) (Hole ty) sc))

88+ return (RBind x (Hole ty) sc))

8689 <|> try (do symbol "??";

87− x <- identifier; lchar ':'; ty <- pTerm

90+ x <- iName; lchar ':'; ty <- pTerm

8891 lchar '=';

8992 val <- pTerm

9093 sc <- pTerm

91− return (RBind (UN [x]) (Guess ty val) sc))

94+ return (RBind x (Guess ty val) sc))

9295 <|> try (do reserved "let";

93− x <- identifier; lchar ':'; ty <- pTerm

96+ x <- iName; lchar ':'; ty <- pTerm

9497 lchar '=';

9598 val <- pTerm

9699 sc <- pTerm

97− return (RBind (UN [x]) (Let ty val) sc))

100+ return (RBind x (Let ty val) sc))

98101 <|> try (do lchar '_';

99− x <- identifier; lchar ':'; ty <- pTerm

102+ x <- iName; lchar ':'; ty <- pTerm

100103 lchar '.';

101104 sc <- pTerm

102− return (RBind (UN [x]) (PVar ty) sc))

105+ return (RBind x (PVar ty) sc))

103106 <|> try (do reserved "Set"; i <- natural

104107 return (RSet (fromInteger i)))

105− <|> try (do x <- identifier

106− return (Var (UN [x])))

108+ <|> try (do x <- iName

109+ return (Var x))

107110

src/ProofState.hs+1−1

@@ -175,7 +175,7 @@ process :: Tactic -> Name -> ProofState -> StateT TState TC ProofState

175175process t h ps = tactic (Just h) ps (context ps) (mktac t)

176176 where mktac Attack = attack

177177 mktac (Claim n r) = claim n r

178− mktac (Fill r) = fill r

178+ mktac (Fill r) = fill r

179179 mktac Regret = regret

180180 mktac Solve = solve

181181 mktac (Intro n) = intro n

src/ShellParser.hs+4−5

@@ -35,7 +35,7 @@ parseCommand = parse pCommand "(input)"

3535parseTactic = parse (pTactic >>= return . Tac) "(input)"

3636

3737pCommand :: Parser Command

38−pCommand = do reserved "theorem"; n <- iname; lchar ':'; ty <- pTerm

38+pCommand = do reserved "theorem"; n <- iName; lchar ':'; ty <- pTerm

3939 return (Theorem n ty)

4040 <|> do reserved "eval"; tm <- pTerm

4141 return (Eval tm)

@@ -44,14 +44,13 @@ pCommand = do reserved "theorem"; n <- iname; lchar ':'; ty <- pTerm

4444

4545pTactic :: Parser Tactic

4646pTactic = do reserved "attack"; return Attack

47− <|> do reserved "claim"; n <- iname; lchar ':'; ty <- pTerm

47+ <|> do reserved "claim"; n <- iName; lchar ':'; ty <- pTerm

4848 return (Claim n ty)

4949 <|> do reserved "fill"; tm <- pTerm; return (Fill tm)

5050 <|> do reserved "regret"; return Regret

5151 <|> do reserved "solve"; return Solve

52− <|> do reserved "intro"; n <- iname; return (Intro n)

52+ <|> do reserved "intro"; n <- iName; return (Intro n)

5353 <|> do reserved "state"; return ProofState

5454 <|> do reserved "qed"; return QED

5555

56−iname :: Parser Name

57−iname = identifier >>= (\n -> return (UN [n]))

56+