9cdfa26 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix parsing of $

Needs to flatten applications so that elaboration does the right thing. Fixes #1020

commit9cdfa265013586590e19bb98212a97a2f6ee6c3e authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateWed 2 Apr 2014, 00:20 (13 years ago) parentfb6a0ed

1 file changed+6−1

unifiedsplit

src/Idris/ParseOps.hs+6−1

@@ -37,9 +37,14 @@ table fixes

3737 [pexp (PApp fc (PRef fc (sUN "fromInteger")) [pexp (PConstant (BI 0))]), pexp x])]]

3838 ++ toTable (reverse fixes) ++

3939 [[backtick],

40− [binary "$" (\fc x y -> PApp fc x [pexp y]) AssocRight],

40+ [binary "$" (\fc x y -> flatten $ PApp fc x [pexp y]) AssocRight],

4141 [binary "=" PEq AssocLeft],

4242 [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+

4348

4449-- | Calculates table for fixtiy declarations

4550toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm