git.iko.soy/Idris-dev
on master help sign in
Fix parsing of $
9cdfa26Edwin Brady
src/Idris/ParseOps.hs+6−1
compare with master
unifiedsplit
@@ -37,9 +37,14 @@ table fixes
37 [pexp (PApp fc (PRef fc (sUN "fromInteger")) [pexp (PConstant (BI 0))]), pexp x])]]
37 [pexp (PApp fc (PRef fc (sUN "fromInteger")) [pexp (PConstant (BI 0))]), pexp x])]]
38 ++ toTable (reverse fixes) ++
38 ++ toTable (reverse fixes) ++
39 [[backtick],
39 [[backtick],
40− [binary "$" (\fc x y -> PApp fc x [pexp y]) AssocRight],
40+ [binary "$" (\fc x y -> flatten $ PApp fc x [pexp y]) AssocRight],
41 [binary "=" PEq AssocLeft],
41 [binary "=" PEq AssocLeft],
42 [binary "->" (\fc x y -> PPi expl (sUN "__pi_arg") x y) AssocRight]]
42 [binary "->" (\fc x y -> PPi expl (sUN "__pi_arg") x y) AssocRight]]
43+ where
44+ flatten :: PTerm -> PTerm -- flatten application
45+ flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))
46+ flatten t = t
47+
43
48
44-- | Calculates table for fixtiy declarations
49-- | Calculates table for fixtiy declarations
45toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm
50toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm