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

git.iko.soy/Idris-dev

on master help sign in

Fix bug in applying syntax rules

834a5e0Edwin Brady15 years ago

interp.idr−1

compare with master

unifiedsplit

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

1−

2data Ty = TyNat | TyFun Ty Ty;

1data Ty = TyNat | TyFun Ty Ty;

4interpTy : Ty -> Set;

3interpTy : Ty -> Set;

src/Core/CoreParser.hs+16−14

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

9import Text.ParserCombinators.Parsec.Language

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

12+import Control.Monad.State

12import Debug.Trace

13import Debug.Trace

14type TokenParser a = PTok.TokenParser a

15type TokenParser a = PTok.TokenParser a

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

55pTestFile = do p <- many1 pDef ; eof

56pTestFile = do p <- many1 pDef ; eof

56 return p

57 return p

58−iName :: CParser a Name

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

59−iName = do x <- identifier

60+iName bad = do x <- identifier

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

60− return (UN [x])

62+ return (UN [x])

62pDef :: CParser a (Name, RDef)

64pDef :: CParser a (Name, RDef)

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

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

64 lchar '='

66 lchar '='

65 tm <- pTerm

67 tm <- pTerm

66 lchar ';'

68 lchar ';'

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

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

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

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

69 return (x, RConst ty)

71 return (x, RConst ty)

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

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

71 return (x, RData d)

73 return (x, RData d)

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

84pNoApp = try (chainr1 pExp arrow)

86pNoApp = try (chainr1 pExp arrow)

85 <|> pExp

87 <|> pExp

86pExp :: CParser a Raw

88pExp :: CParser a Raw

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

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

88 symbol "=>";

90 symbol "=>";

89 sc <- pTerm

91 sc <- pTerm

90 return (RBind x (Lam ty) sc)

92 return (RBind x (Lam ty) sc)

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

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

92 lchar '.';

94 lchar '.';

93 sc <- pTerm

95 sc <- pTerm

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

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

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

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

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

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

97 lchar ')';

99 lchar ')';

98 symbol "->";

100 symbol "->";

99 sc <- pTerm

101 sc <- pTerm

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

103 lchar ')'

105 lchar ')'

104 return t)

106 return t)

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

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

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

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

107 lchar '=';

109 lchar '=';

108 val <- pTerm

110 val <- pTerm

109 sc <- pTerm

111 sc <- pTerm

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

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

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

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

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

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

113 lchar '=';

115 lchar '=';

114 val <- pTerm

116 val <- pTerm

115 reserved "in";

117 reserved "in";

116 sc <- pTerm

118 sc <- pTerm

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

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

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

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

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

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

120 lchar '.';

122 lchar '.';

121 sc <- pTerm

123 sc <- pTerm

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

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

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

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

124 return (RSet (fromInteger i)))

126 return (RSet (fromInteger i)))

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

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

126 return (Var x))

128 return (Var x))

127

129

128pData :: CParser a (Name, RawDatatype)

130pData :: 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"

130 cs <- many pConstructor

132 cs <- many pConstructor

131 return (x, RDatatype x ty cs)

133 return (x, RDatatype x ty cs)

132

134

133pConstructor :: CParser a (Name, Raw)

135pConstructor :: CParser a (Name, Raw)

134pConstructor = do lchar '|'

136pConstructor = do lchar '|'

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

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

136 return (c, ty)

138 return (c, ty)

137

139

src/Core/ShellParser.hs+9−9

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

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

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)

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

41 return (Eval tm)

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

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

43 <|> do reserved "quit";

44 return Quit

46pTactic :: Parser (Elab ())

47pTactic = do reserved "attack"; return attack

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

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

49 return (claim n ty)

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

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

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

54 return (discard (apply tm args))

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

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

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

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

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

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

59 return (forall n ty)

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

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

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

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

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

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

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

64 <|> 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)

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

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

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

src/Idris/Parser.hs+30−18

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

172 name _ = Nothing

173

174pSynSym :: IParser SSymbol

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

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

176 return (Expr n))

177− <|> do n <- iName

177+ <|> do n <- pName

178 return (Keyword n)

179 <|> do sym <- strlit

180 return (Symbol sym)

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

237pExpr' syn

238 = try (do i <- getState

239 pExtensions syn (syntax_rules i))

240+ <|> pNoExtExpr syn

241+

242+pNoExtExpr syn =

240− <|> try (pApp syn)

243+ try (pApp syn)

241 <|> pSimpleExpr syn

244 <|> pSimpleExpr syn

242 <|> try (pLambda syn)

245 <|> try (pLambda syn)

243 <|> try (pPi syn)

246 <|> try (pPi syn)

244 <|> try (pDoBlock syn)

247 <|> try (pDoBlock syn)

245

248

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

249pExtensions :: 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)

248

251

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

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

250−pExt syn (Rule ssym ptm)

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

254+ = do s1 <- pSymbol pSimpleExpr s

251− = do smap <- mapM pSymbol ssym

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

252− let ns = mapMaybe id smap

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

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

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

254 where

258 where

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

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

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

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

257− return $ Just (n, tm)

261+ return $ Just (n, tm)

258− pSymbol (Symbol s) = do symbol s

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

259− return Nothing

263+ return Nothing

260 dropn n [] = []

264 dropn n [] = []

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

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

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

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

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

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

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

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

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

278

282

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+

279−pfName = try iName

291+pfName = try pName

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

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

281

293

282pSimpleExpr syn =

294pSimpleExpr syn =

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

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

284 return $ PQuote t)

296 return $ PQuote t)

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

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

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

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

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

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

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

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

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

309 <|> do e <- pSimpleExpr syn

321 <|> do e <- pSimpleExpr syn

310 return (PExp e)

322 return (PExp e)

311

323

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

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

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

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

314 lchar '}'

326 lchar '}'

315 return (PImp n v)

327 return (PImp n v)

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

349 return (PDoBlock ds)

361 return (PDoBlock ds)

350

362

351pDo syn

363pDo syn

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

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

353 return (DoBind i e))

365 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

355 return (DoLet i e))

367 return (DoLet i e))

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

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

357

369

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

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

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

395 lchar ';'

407 lchar ';'

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

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

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

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

398 lchar '='

410 lchar '='

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

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

400 lchar ';'

412 lchar ';'