@@ -322,10 +322,24 @@ pExpr syn = do i <- getState
323pExpr' :: SyntaxInfo -> IParser PTerm
323pExpr' :: SyntaxInfo -> IParser PTerm
324pExpr' syn
324pExpr' syn
325− = try (do i <- getState
325+ = try (pExtExpr syn)
326− pExtensions syn (syntax_rules i))
327 <|> pNoExtExpr syn
326 <|> pNoExtExpr syn
328+pExtExpr :: SyntaxInfo -> IParser PTerm
329+pExtExpr syn = do i <- getState
330+ pExtensions syn (syntax_rules i)
332+pSimpleExtExpr :: SyntaxInfo -> IParser PTerm
333+pSimpleExtExpr syn = do i <- getState
334+ pExtensions syn (filter simple (syntax_rules i))
336+ simple (Rule (Expr x:xs) _) = False
337+ simple (Rule (_:xs) _) = case (last xs) of
329pNoExtExpr syn =
343pNoExtExpr syn =
330 try (pApp syn)
344 try (pApp syn)
331 <|> pSimpleExpr syn
345 <|> pSimpleExpr syn
@@ -398,6 +412,7 @@ pSimpleExpr syn =
398 <|> try (do symbol "()"; fc <- pfc; return (PTrue fc))
412 <|> try (do symbol "()"; fc <- pfc; return (PTrue fc))
399 <|> try (do symbol "_|_"; fc <- pfc; return (PFalse fc))
413 <|> try (do symbol "_|_"; fc <- pfc; return (PFalse fc))
400 <|> do lchar '_'; return Placeholder
414 <|> do lchar '_'; return Placeholder
415+ <|> pSimpleExtExpr syn
402pPair syn = do lchar '('; l <- pExpr syn; op <- pairOp
417pPair syn = do lchar '('; l <- pExpr syn; op <- pairOp
403 fc <- pfc
418 fc <- pfc
@@ -601,13 +616,15 @@ whereSyn n syn args = let ns = concatMap allNamesIn args
601 no_imp = nub (ni ++ ns) }
616 no_imp = nub (ni ++ ns) }
602 where decorate n x = UN [(show n ++ "_" ++ show x)]
617 where decorate n x = UN [(show n ++ "_" ++ show x)]
619+pArgExpr syn = try (pHSimpleExpr syn) <|> pSimpleExtExpr syn
604pClause :: SyntaxInfo -> IParser PClause
621pClause :: SyntaxInfo -> IParser PClause
605pClause syn
622pClause syn
606 = try (do n <- pfName
623 = try (do n <- pfName
607 cargs <- many (pConstraintArg syn)
624 cargs <- many (pConstraintArg syn)
608 iargs <- many (pImplicitArg syn)
625 iargs <- many (pImplicitArg syn)
609 fc <- pfc
626 fc <- pfc
610− args <- many (pHSimpleExpr syn)
627+ args <- many (pArgExpr syn)
611 wargs <- many (pWExpr syn)
628 wargs <- many (pWExpr syn)
612 lchar '='
629 lchar '='
613 rhs <- pExpr syn
630 rhs <- pExpr syn
@@ -624,7 +641,7 @@ pClause syn
624 cargs <- many (pConstraintArg syn)
641 cargs <- many (pConstraintArg syn)
625 iargs <- many (pImplicitArg syn)
642 iargs <- many (pImplicitArg syn)
626 fc <- pfc
643 fc <- pfc
627− args <- many (pHSimpleExpr syn)
644+ args <- many (pArgExpr syn)
628 wargs <- many (pWExpr syn)
645 wargs <- many (pWExpr syn)
629 reserved "with"
646 reserved "with"
630 wval <- pExpr syn
647 wval <- pExpr syn
@@ -635,10 +652,10 @@ pClause syn
635 return $ PWith n (PApp fc (PRef fc n)
652 return $ PWith n (PApp fc (PRef fc n)
636 (iargs ++ cargs ++ map pexp args)) wargs wval withs)
653 (iargs ++ cargs ++ map pexp args)) wargs wval withs)
638− <|> do l <- pSimpleExpr syn
655+ <|> do l <- pArgExpr syn
639 op <- operator
656 op <- operator
640 let n = UN [op]
657 let n = UN [op]
641− r <- pSimpleExpr syn
658+ r <- pArgExpr syn
642 fc <- pfc
659 fc <- pfc
643 wargs <- many (pWExpr syn)
660 wargs <- many (pWExpr syn)
644 lchar '='
661 lchar '='
@@ -649,10 +666,10 @@ pClause syn
649 return $ PClause n (PApp fc (PRef fc n) [pexp l,pexp r])
666 return $ PClause n (PApp fc (PRef fc n) [pexp l,pexp r])
650 wargs rhs wheres
667 wargs rhs wheres
652− <|> do l <- pSimpleExpr syn
669+ <|> do l <- pArgExpr syn
653 op <- operator
670 op <- operator
654 let n = UN [op]
671 let n = UN [op]
655− r <- pSimpleExpr syn
672+ r <- pArgExpr syn
656 fc <- pfc
673 fc <- pfc
657 wargs <- many (pWExpr syn)
674 wargs <- many (pWExpr syn)
658 reserved "with"
675 reserved "with"