834a5e0 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix bug in applying syntax rules

commit834a5e0ccb676571cc6658438be3b5d9fd5fc70e authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSun 16 Oct 2011, 21:49 (15 years ago) parentb0248ea

4 files changed+55−42

compare with master

unifiedsplit

interp.idr−1 src/Core/CoreParser.hs+16−14 src/Core/ShellParser.hs+9−9 src/Idris/Parser.hs+30−18

interp.idr−1

@@ -1,4 +1,3 @@

1−

21data Ty = TyNat | TyFun Ty Ty;

43interpTy : Ty -> Set;

src/Core/CoreParser.hs+16−14

@@ -9,6 +9,7 @@ import Text.ParserCombinators.Parsec.Expr

99import Text.ParserCombinators.Parsec.Language

1010import qualified Text.ParserCombinators.Parsec.Token as PTok

1111

12+import Control.Monad.State

1213import Debug.Trace

1314

1415type TokenParser a = PTok.TokenParser a

@@ -55,17 +56,18 @@ pTestFile :: CParser a RProgram

5556pTestFile = do p <- many1 pDef ; eof

5657 return p

5758

58−iName :: CParser a Name

59−iName = do x <- identifier

60− return (UN [x])

59+iName :: [String] -> CParser a Name

60+iName bad = do x <- identifier

61+ when (x `elem` bad) $ fail "Reserved identifier"

62+ return (UN [x])

6163

6264pDef :: CParser a (Name, RDef)

63−pDef = try (do x <- iName; lchar ':'; ty <- pTerm

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

6466 lchar '='

6567 tm <- pTerm

6668 lchar ';'

6769 return (x, RFunction (RawFun ty tm)))

68− <|> do x <- iName; lchar ':'; ty <- pTerm; lchar ';'

70+ <|> do x <- iName []; lchar ':'; ty <- pTerm; lchar ';'

6971 return (x, RConst ty)

7072 <|> do (x, d) <- pData; lchar ';'

7173 return (x, RData d)

@@ -84,16 +86,16 @@ pNoApp :: CParser a Raw

8486pNoApp = try (chainr1 pExp arrow)

8587 <|> pExp

8688pExp :: CParser a Raw

87−pExp = do lchar '\\'; x <- iName; lchar ':'; ty <- pTerm

89+pExp = do lchar '\\'; x <- iName []; lchar ':'; ty <- pTerm

8890 symbol "=>";

8991 sc <- pTerm

9092 return (RBind x (Lam ty) sc)

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

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

9294 lchar '.';

9395 sc <- pTerm

9496 return (RBind x (Hole ty) sc))

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

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

98+ x <- iName []; lchar ':'; ty <- pTerm

9799 lchar ')';

98100 symbol "->";

99101 sc <- pTerm

@@ -103,35 +105,35 @@ pExp = do lchar '\\'; x <- iName; lchar ':'; ty <- pTerm

103105 lchar ')'

104106 return t)

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

106− x <- iName; lchar ':'; ty <- pTerm

108+ x <- iName []; lchar ':'; ty <- pTerm

107109 lchar '=';

108110 val <- pTerm

109111 sc <- pTerm

110112 return (RBind x (Guess ty val) sc))

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

112− x <- iName; lchar ':'; ty <- pTerm

114+ x <- iName []; lchar ':'; ty <- pTerm

113115 lchar '=';

114116 val <- pTerm

115117 reserved "in";

116118 sc <- pTerm

117119 return (RBind x (Let ty val) sc))

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

119− x <- iName; lchar ':'; ty <- pTerm

121+ x <- iName []; lchar ':'; ty <- pTerm

120122 lchar '.';

121123 sc <- pTerm

122124 return (RBind x (PVar ty) sc))

123125 <|> try (do reserved "Set"; i <- option 0 natural

124126 return (RSet (fromInteger i)))

125− <|> try (do x <- iName

127+ <|> try (do x <- iName []

126128 return (Var x))

127129

128130pData :: CParser a (Name, RawDatatype)

129−pData = do reserved "data"; x <- iName; lchar ':'; ty <- pTerm; reserved "where"

131+pData = do reserved "data"; x <- iName []; lchar ':'; ty <- pTerm; reserved "where"

130132 cs <- many pConstructor

131133 return (x, RDatatype x ty cs)

132134

133135pConstructor :: CParser a (Name, Raw)

134136pConstructor = do lchar '|'

135− c <- iName; lchar ':'; ty <- pTerm

137+ c <- iName []; lchar ':'; ty <- pTerm

136138 return (c, ty)

137139

src/Core/ShellParser.hs+9−9

@@ -35,17 +35,17 @@ 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)

42− <|> do reserved "print"; n <- iName; return (Print n)

42+ <|> do reserved "print"; n <- iName []; return (Print n)

4343 <|> do reserved "quit";

4444 return Quit

4545

4646pTactic :: Parser (Elab ())

4747pTactic = do reserved "attack"; return attack

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

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

4949 return (claim n ty)

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

5151 <|> do reserved "exact"; tm <- pTerm; return (exact tm)

@@ -54,15 +54,15 @@ pTactic = do reserved "attack"; return attack

5454 return (discard (apply tm args))

5555 <|> do reserved "solve"; return solve

5656 <|> do reserved "compute"; return compute

57− <|> do reserved "intro"; n <- iName; return (intro n)

58− <|> do reserved "forall"; n <- iName; lchar ':'; ty <- pTerm

57+ <|> do reserved "intro"; n <- iName []; return (intro n)

58+ <|> do reserved "forall"; n <- iName []; lchar ':'; ty <- pTerm

5959 return (forall n ty)

60− <|> do reserved "arg"; n <- iName; t <- iName; return (arg n t)

61− <|> do reserved "patvar"; n <- iName; return (patvar n)

62−-- <|> do reserved "patarg"; n <- iName; t <- iName; return (patarg n t)

60+ <|> do reserved "arg"; n <- iName []; t <- iName []; return (arg n t)

61+ <|> do reserved "patvar"; n <- iName []; return (patvar n)

62+-- <|> do reserved "patarg"; n <- iName []; t <- iName []; return (patarg n t)

6363 <|> do reserved "eval"; t <- pTerm; return (eval_in t)

6464 <|> do reserved "check"; t <- pTerm; return (check_in t)

65− <|> do reserved "focus"; n <- iName; return (focus n)

65+ <|> do reserved "focus"; n <- iName []; return (focus n)

6666 <|> do reserved "state"; return proofstate

6767 <|> do reserved "undo"; return undo

6868 <|> do reserved "qed"; return (discard qed)

src/Idris/Parser.hs+30−18

@@ -172,9 +172,9 @@ pSyntaxRule syn

172172 name _ = Nothing

173173

174174pSynSym :: IParser SSymbol

175−pSynSym = try (do lchar '['; n <- iName; lchar ']'

175+pSynSym = try (do lchar '['; n <- pName; lchar ']'

176176 return (Expr n))

177− <|> do n <- iName

177+ <|> do n <- pName

178178 return (Keyword n)

179179 <|> do sym <- strlit

180180 return (Symbol sym)

@@ -237,26 +237,30 @@ pExpr' :: SyntaxInfo -> IParser PTerm

237237pExpr' syn

238238 = try (do i <- getState

239239 pExtensions syn (syntax_rules i))

240− <|> try (pApp syn)

240+ <|> pNoExtExpr syn

241+

242+pNoExtExpr syn =

243+ try (pApp syn)

241244 <|> pSimpleExpr syn

242245 <|> try (pLambda syn)

243246 <|> try (pPi syn)

244247 <|> try (pDoBlock syn)

245248

246249pExtensions :: SyntaxInfo -> [Syntax] -> IParser PTerm

247−pExtensions syn rules = choice (map (pExt syn) rules)

250+pExtensions syn rules = choice (map (\x -> try (pExt syn x)) rules)

248251

249252pExt :: SyntaxInfo -> Syntax -> IParser PTerm

250−pExt syn (Rule ssym ptm)

251− = do smap <- mapM pSymbol ssym

252− let ns = mapMaybe id smap

253+pExt syn (Rule (s:ssym) ptm)

254+ = do s1 <- pSymbol pSimpleExpr s

255+ smap <- mapM (pSymbol pExpr') ssym

256+ let ns = mapMaybe id (s1:smap)

253257 return (update ns ptm) -- updated with smap

254258 where

255− pSymbol (Keyword n) = do reserved (show n); return Nothing

256− pSymbol (Expr n) = do tm <- pSimpleExpr syn

257− return $ Just (n, tm)

258− pSymbol (Symbol s) = do symbol s

259− return Nothing

259+ pSymbol p (Keyword n) = do reserved (show n); return Nothing

260+ pSymbol p (Expr n) = do tm <- p syn

261+ return $ Just (n, tm)

262+ pSymbol p (Symbol s) = do symbol s

263+ return Nothing

260264 dropn n [] = []

261265 dropn n ((x,t) : xs) | n == x = xs

262266 | otherwise = (x,t):dropn n xs

@@ -276,13 +280,21 @@ pExt syn (Rule ssym ptm)

276280 upd ns (DoBind n t : ds) = DoBind n (update ns t) : upd (dropn n ns) ds

277281 upd ns (DoLet n t : ds) = DoLet n (update ns t) : upd (dropn n ns) ds

278282

279−pfName = try iName

283+pName = do i <- getState

284+ iName (map show (names (syntax_rules i)))

285+ where

286+ names rs = concatMap namesR rs

287+ namesR (Rule syms _) = mapMaybe ename syms

288+ ename (Keyword n) = Just n

289+ ename _ = Nothing

290+

291+pfName = try pName

280292 <|> do lchar '('; o <- operator; lchar ')'; return (UN [o])

281293

282294pSimpleExpr syn =

283295 try (do symbol "!["; t <- pTerm; lchar ']'

284296 return $ PQuote t)

285− <|> try (do lchar '?'; x <- iName; return (PMetavar x))

297+ <|> try (do lchar '?'; x <- pName; return (PMetavar x))

286298 <|> try (do reserved "return"; return PReturn)

287299 <|> try (do x <- pfName; return (PRef x))

288300 <|> try (do lchar '('; l <- pExpr syn; lchar ','; r <- pExpr syn; lchar ')';

@@ -309,7 +321,7 @@ pArg syn = pImplicitArg syn

309321 <|> do e <- pSimpleExpr syn

310322 return (PExp e)

311323

312−pImplicitArg syn = do lchar '{'; n <- iName

324+pImplicitArg syn = do lchar '{'; n <- pName

313325 v <- option (PRef n) (do lchar '='; pExpr syn)

314326 lchar '}'

315327 return (PImp n v)

@@ -349,9 +361,9 @@ pDoBlock syn

349361 return (PDoBlock ds)

350362

351363pDo syn

352− = try (do i <- iName; symbol "<-"; e <- pExpr syn;

364+ = try (do i <- pName; symbol "<-"; e <- pExpr syn;

353365 return (DoBind i e))

354− <|> try (do reserved "let"; i <- iName; reservedOp "="; e <- pExpr syn

366+ <|> try (do reserved "let"; i <- pName; reservedOp "="; e <- pExpr syn

355367 return (DoLet i e))

356368 <|> try (do e <- pExpr syn; return (DoExp e))

357369

@@ -394,7 +406,7 @@ pData syn = try (do reserved "data"; tyn <- pfName; ty <- pTSig syn

394406 cons <- sepBy (pConstructor syn) (lchar '|')

395407 lchar ';'

396408 return $ PData (PDatadecl tyn ty' cons))

397− <|> do reserved "data"; tyn <- pfName; args <- many iName

409+ <|> do reserved "data"; tyn <- pfName; args <- many pName

398410 lchar '='

399411 cons <- sepBy1 (pSimpleCon syn) (lchar '|')

400412 lchar ';'