ab3985a · Idris-dev · git.iko.soy

src/Idris/Parser/Ops.hs+10−1

compare with master

unifiedsplit

@@ -30,13 +30,22 @@ import qualified Text.Megaparsec.Expr as P

30-- using pre-build and user-defined operator/fixity declarations

31table :: [FixDecl] -> [[P.Operator IdrisParser PTerm]]

32table fixes

33− = [[prefix "-" (\fc x -> PApp fc (PRef fc [fc] (sUN "negate")) [pexp x])]] ++

33+ = [[prefix "-" negateExpr]] ++

34 toTable (reverse fixes) ++

35 [[noFixityBacktickOperator],

36 [binary "$" P.InfixR $ \fc _ x y -> flatten $ PApp fc x [pexp y]],

37 [binary "=" P.InfixL $ \fc _ x y -> PApp fc (PRef fc [fc] eqTy) [pexp x, pexp y]],

38 [noFixityOperator]]

39 where

40+

41+ negateExpr :: FC -> PTerm -> PTerm

42+ negateExpr _ (PConstant fc (I int)) = PConstant fc $ I $ negate int

43+ negateExpr _ (PConstant fc (BI bigInt)) = PConstant fc $ BI $ negate bigInt

44+ negateExpr _ (PConstant fc (Fl dbl)) = PConstant fc $ Fl $ negate dbl

45+ negateExpr _ (PConstSugar fc term) = negateExpr fc term

46+ negateExpr fc (PAlternative ns tp terms) = PAlternative ns tp $ map (negateExpr fc) terms

47+ negateExpr fc x = PApp fc (PRef fc [fc] (sUN "negate")) [pexp x]

48+

40 flatten :: PTerm -> PTerm -- flatten application

49 flatten :: PTerm -> PTerm -- flatten application

41 flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))

50 flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))

42 flatten t = t

51 flatten t = t

test/regression002/Negation.idrnew file+2

@@ -0,0 +1,2 @@

1+f : Int -> Int

2+f (-1) = 1

test/regression002/expected+1−1

@@ -346,7 +346,7 @@ When checking argument value to function Prelude.Basics.the:

346 Type mismatch between

347 x = x (Type of Refl)

348 and

349− (-0.0) = 0.0 (Expected type)

349+ -0.0 = 0.0 (Expected type)

350

351 Specifically:

352 Type mismatch between

test/regression002/run+1

@@ -35,6 +35,7 @@ ${IDRIS:-idris} $@ --nobanner --nocolour --quiet --port none <<!

35:load reg077.idr

36:load DoubleEquality.idr

37:load Canonicity.idr

38+:load Negation.idr

38!

39!

39

40

40rm -f *.ibc

41rm -f *.ibc