@@ -170,9 +170,17 @@ pSyntaxDecl :: SyntaxInfo -> IParser PDecl
170170pSyntaxDecl syn
171171 = do s <- pSyntaxRule syn
172172 i <- getState
173− setState (i { syntax_rules = s : syntax_rules i })
173+ let rs = syntax_rules i
174+ let ns = syntax_keywords i
175+ let ks = map show (names s)
176+ setState (i { syntax_rules = s : rs,
177+ syntax_keywords = ks ++ ns })
174178 fc <- pfc
175179 return (PSyntax fc s)
180+ where
181+ names (Rule syms _) = mapMaybe ename syms
182+ ename (Keyword n) = Just n
183+ ename _ = Nothing
176184
177185pSyntaxRule :: SyntaxInfo -> IParser Syntax
178186pSyntaxRule syn
@@ -201,8 +209,8 @@ pSynSym = try (do lchar '['; n <- pName; lchar ']'
201209 return (Symbol sym)
202210
203211pFunDecl' :: SyntaxInfo -> IParser PDecl
204−pFunDecl' syn = try (do fc <- pfc
205− n <- pfName; ty <- pTSig syn
212+pFunDecl' syn = try (do n <- pfName; ty <- pTSig syn
213+ fc <- pfc
206214 lchar ';'
207215 ty' <- implicit syn n ty
208216 return (PTy fc n ty'))
@@ -268,8 +276,8 @@ pNoExtExpr syn =
268276 <|> pSimpleExpr syn
269277 <|> try (pLambda syn)
270278 <|> try (pLet syn)
271− <|> try (pPi syn)
272− <|> try (pDoBlock syn)
279+ <|> pPi syn
280+ <|> pDoBlock syn
273281
274282pExtensions :: SyntaxInfo -> [Syntax] -> IParser PTerm
275283pExtensions syn rules = choice (map (\x -> try (pExt syn x)) rules)
@@ -308,12 +316,8 @@ pExt syn (Rule (s:ssym) ptm)
308316 update ns t = t
309317
310318pName = do i <- getState
311− iName (map show (names (syntax_rules i)))
319+ iName (syntax_keywords i)
312320 where
313− names rs = concatMap namesR rs
314− namesR (Rule syms _) = mapMaybe ename syms
315− ename (Keyword n) = Just n
316− ename _ = Nothing
317321
318322pfName = try pName
319323 <|> do lchar '('; o <- operator; lchar ')'; return (UN [o])
@@ -322,21 +326,24 @@ pSimpleExpr syn =
322326 try (do symbol "!["; t <- pTerm; lchar ']'
323327 return $ PQuote t)
324328 <|> try (do lchar '?'; x <- pName; return (PMetavar x))
325− <|> try (do fc <- pfc; reserved "refl"; return (PRefl fc))
326− <|> try (do fc <- pfc; reserved "return"; return (PReturn fc))
327− <|> try (do fc <- pfc; x <- pfName; return (PRef fc x))
328− <|> try (do lchar '('; l <- pExpr syn; lchar ','; fc <- pfc
329− r <- pExpr syn; lchar ')';
330− return (PPair fc l r))
331− <|> try (do lchar '('; l <- pExpr syn; reservedOp "**"; fc <- pfc
332− r <- pExpr syn; lchar ')';
333− return (PDPair fc l r))
329+ <|> try (do reserved "refl"; fc <- pfc; return (PRefl fc))
330+ <|> try (do reserved "return"; fc <- pfc; return (PReturn fc))
331+ <|> try (do x <- pfName; fc <- pfc; return (PRef fc x))
332+ <|> try (pPair syn)
334333 <|> try (do lchar '('; e <- pExpr syn; lchar ')'; return e)
335334 <|> try (do c <- pConstant; return (PConstant c))
336− <|> try (do reserved "Set"; return PSet)
337− <|> try (do fc <- pfc; symbol "()"; return (PTrue fc))
338− <|> try (do fc <- pfc; symbol "_|_"; return (PFalse fc))
339− <|> try (do lchar '_'; return Placeholder)
335+ <|> do reserved "Set"; return PSet
336+ <|> try (do symbol "()"; fc <- pfc; return (PTrue fc))
337+ <|> try (do symbol "_|_"; fc <- pfc; return (PFalse fc))
338+ <|> do lchar '_'; return Placeholder
339+
340+pPair syn = do lchar '('; l <- pExpr syn; op <- pairOp
341+ fc <- pfc
342+ r <- pExpr syn; lchar ')';
343+ return (op fc l r)
344+ where
345+ pairOp = do lchar ','; return PPair
346+ <|> do reservedOp "**"; return PDPair
340347
341348pHSimpleExpr syn
342349 = try (pSimpleExpr syn)
@@ -352,13 +359,13 @@ pApp syn = do f <- pSimpleExpr syn
352359pArg :: SyntaxInfo -> IParser PArg
353360pArg syn = pImplicitArg syn
354361 <|> do e <- pSimpleExpr syn
355− return (PExp e)
362+ return (pexp e)
356363
357364pImplicitArg syn = do lchar '{'; n <- pName
358365 fc <- pfc
359366 v <- option (PRef fc n) (do lchar '='; pExpr syn)
360367 lchar '}'
361− return (PImp n v)
368+ return (pimp n v)
362369
363370pTSig syn = do lchar ':'
364371 pExpr syn
@@ -373,14 +380,16 @@ pLet syn = do reserved "let"; n <- pName; lchar '='; v <- pExpr syn
373380 reserved "in"; sc <- pExpr syn
374381 return (PLet n Placeholder v sc)
375382
376−pPi syn = do lchar '('; xt <- tyDeclList syn; lchar ')'
383+pPi syn = do lazy <- option False (do lchar '|'; return True)
384+ lchar '('; xt <- tyDeclList syn; lchar ')'
377385 symbol "->"
378386 sc <- pExpr syn
379− return (bindList (PPi Exp) xt sc)
380− <|> do lchar '{'; xt <- tyDeclList syn; lchar '}'
387+ return (bindList (PPi (Exp lazy)) xt sc)
388+ <|> do lazy <- option False (do lchar '|'; return True)
389+ lchar '{'; xt <- tyDeclList syn; lchar '}'
381390 symbol "->"
382391 sc <- pExpr syn
383− return (bindList (PPi Imp) xt sc)
392+ return (bindList (PPi (Imp lazy)) xt sc)
384393
385394tyDeclList syn = sepBy1 (do x <- pfName; t <- pTSig syn; return (x,t))
386395 (lchar ',')
@@ -399,14 +408,14 @@ pDoBlock syn
399408 return (PDoBlock ds)
400409
401410pDo syn
402− = try (do fc <- pfc
403− i <- pName; symbol "<-"; e <- pExpr syn;
411+ = try (do i <- pName; symbol "<-"; fc <- pfc
412+ e <- pExpr syn;
404413 return (DoBind fc i e))
405− <|> try (do fc <- pfc
406− reserved "let"; i <- pName; reservedOp "="; e <- pExpr syn
414+ <|> try (do reserved "let"; i <- pName; reservedOp "="; fc <- pfc
415+ e <- pExpr syn
407416 return (DoLet fc i e))
408− <|> try (do fc <- pfc
409− e <- pExpr syn; return (DoExp fc e))
417+ <|> try (do e <- pExpr syn; fc <- pfc
418+ return (DoExp fc e))
410419
411420pConstant :: IParser Const
412421pConstant = do reserved "Int"; return IType
@@ -420,38 +429,38 @@ pConstant = do reserved "Int"; return IType
420429 <|> try (do c <- chlit; return $ Ch c)
421430
422431table fixes
423− = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN ["-"])) [PExp (PConstant (I 0)), PExp x])]]
432+ = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN ["-"])) [pexp (PConstant (I 0)), pexp x])]]
424433 ++ toTable (reverse fixes) ++
425434 [[binary "=" (\fc x y -> PEq fc x y) AssocLeft],
426− [binary "->" (\fc x y -> PPi Exp (MN 0 "X") x y) AssocRight]]
435+ [binary "->" (\fc x y -> PPi expl (MN 0 "X") x y) AssocRight]]
427436
428437toTable fs = map (map toBin)
429438 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)
430439 where toBin (Fix (PrefixN _) op) = prefix op
431− (\fc x -> PApp fc (PRef fc (UN [op])) [PExp x])
440+ (\fc x -> PApp fc (PRef fc (UN [op])) [pexp x])
432441 toBin (Fix f op)
433− = binary op (\fc x y -> PApp fc (PRef fc (UN [op])) [PExp x,PExp y]) (assoc f)
442+ = binary op (\fc x y -> PApp fc (PRef fc (UN [op])) [pexp x,pexp y]) (assoc f)
434443 assoc (Infixl _) = AssocLeft
435444 assoc (Infixr _) = AssocRight
436445 assoc (InfixN _) = AssocNone
437446
438−binary name f assoc = Infix (do { fc <- pfc;
439− reservedOp name; return (f fc) }) assoc
440−prefix name f = Prefix (do { fc <- pfc;
441− reservedOp name; return (f fc) })
447+binary name f assoc = Infix (do { reservedOp name; fc <- pfc;
448+ return (f fc) }) assoc
449+prefix name f = Prefix (do { reservedOp name; fc <- pfc;
450+ return (f fc) })
442451
443452--------- Data declarations ---------
444453
445454pData :: SyntaxInfo -> IParser PDecl
446−pData syn = try (do fc <- pfc
447− reserved "data"; tyn <- pfName; ty <- pTSig syn
455+pData syn = try (do reserved "data"; fc <- pfc
456+ tyn <- pfName; ty <- pTSig syn
448457 reserved "where"
449458 ty' <- implicit syn tyn ty
450459 cons <- sepBy (pConstructor syn) (lchar '|')
451460 lchar ';'
452461 return $ PData fc (PDatadecl tyn ty' cons))
453− <|> do fc <- pfc
454− reserved "data"; tyn <- pfName; args <- many pName
462+ <|> do reserved "data"; fc <- pfc
463+ tyn <- pfName; args <- many pName
455464 lchar '='
456465 cons <- sepBy1 (pSimpleCon syn) (lchar '|')
457466 lchar ';'
@@ -465,31 +474,31 @@ pData syn = try (do fc <- pfc
465474 return $ PData fc (PDatadecl tyn ty' cons')
466475
467476mkPApp fc t [] = t
468−mkPApp fc t xs = PApp fc t (map PExp xs)
477+mkPApp fc t xs = PApp fc t (map pexp xs)
469478
470479bindArgs :: [PTerm] -> PTerm -> PTerm
471480bindArgs [] t = t
472−bindArgs (x:xs) t = PPi Exp (MN 0 "t") x (bindArgs xs t)
481+bindArgs (x:xs) t = PPi expl (MN 0 "t") x (bindArgs xs t)
473482
474483pConstructor :: SyntaxInfo -> IParser (Name, PTerm, FC)
475484pConstructor syn
476− = do fc <- pfc
477− cn <- pfName; ty <- pTSig syn
485+ = do cn <- pfName; fc <- pfc
486+ ty <- pTSig syn
478487 ty' <- implicit syn cn ty
479488 return (cn, ty', fc)
480489
481490pSimpleCon :: SyntaxInfo -> IParser (Name, [PTerm], FC)
482491pSimpleCon syn
483− = do fc <- pfc
484− cn <- pfName
492+ = do cn <- pfName
493+ fc <- pfc
485494 args <- many (pSimpleExpr syn)
486495 return (cn, args, fc)
487496
488497--------- Pattern match clauses ---------
489498
490499pPattern :: SyntaxInfo -> IParser PDecl
491−pPattern syn = do fc <- pfc
492− clause <- pClause syn
500+pPattern syn = do clause <- pClause syn
501+ fc <- pfc
493502 return (PClauses fc (MN 2 "_") [clause]) -- collect together later
494503
495504whereSyn :: Name -> SyntaxInfo -> [PTerm] -> SyntaxInfo
@@ -511,7 +520,7 @@ pClause syn
511520 let wsyn = whereSyn n syn (map getTm iargs ++ args ++ wargs)
512521 wheres <- choice [pWhereblock wsyn, do lchar ';'; return []]
513522 return $ PClause n (PApp fc (PRef fc n)
514− (iargs ++ map PExp args)) wargs rhs wheres)
523+ (iargs ++ map pexp args)) wargs rhs wheres)
515524 <|> try (do n <- pfName
516525 iargs <- many (pImplicitArg syn)
517526 fc <- pfc
@@ -524,7 +533,7 @@ pClause syn
524533 let withs = concat ds
525534 lchar '}'
526535 return $ PWith n (PApp fc (PRef fc n)
527− (iargs ++ map PExp args)) wargs wval withs)
536+ (iargs ++ map pexp args)) wargs wval withs)
528537
529538 <|> do l <- pSimpleExpr syn
530539 op <- operator
@@ -535,7 +544,7 @@ pClause syn
535544 lchar '='
536545 rhs <- pExpr syn
537546 wheres <- choice [pWhereblock syn, do lchar ';'; return []]
538− return $ PClause n (PApp fc (PRef fc n) [PExp l,PExp r]) wargs rhs wheres
547+ return $ PClause n (PApp fc (PRef fc n) [pexp l,pexp r]) wargs rhs wheres
539548
540549 <|> do l <- pSimpleExpr syn
541550 op <- operator
@@ -549,7 +558,7 @@ pClause syn
549558 ds <- many1 $ pFunDecl syn
550559 let withs = concat ds
551560 lchar '}'
552− return $ PWith n (PApp fc (PRef fc n) [PExp l, PExp r]) wargs wval withs
561+ return $ PWith n (PApp fc (PRef fc n) [pexp l, pexp r]) wargs wval withs
553562
554563pWExpr :: SyntaxInfo -> IParser PTerm
555564pWExpr syn = do lchar '|'; pExpr' syn
@@ -587,11 +596,11 @@ expandDo dsl (PDoBlock ds) = expandDo dsl $ block (dsl_bind dsl) ds
587596 block b [DoExp fc tm] = tm
588597 block b [a] = PElabError "Last statement in do block must be an expression"
589598 block b (DoBind fc n tm : rest)
590− = PApp fc (PRef fc b) [PExp tm, PExp (PLam n Placeholder (block b rest))]
599+ = PApp fc (PRef fc b) [pexp tm, pexp (PLam n Placeholder (block b rest))]
591600 block b (DoExp fc tm : rest)
592601 = PApp fc (PRef fc b)
593− [PExp tm,
594− PExp (PLam (MN 0 "bindx") Placeholder (block b rest))]
602+ [pexp tm,
603+ pexp (PLam (MN 0 "bindx") Placeholder (block b rest))]
595604expandDo dsl t = t
596605
597606