7572017 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge branch 'markuspf-negate'

commit7572017643968bb5fe81bf90b227ac198abffcf1 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 22 Sep 2014, 17:08 (12 years ago) parentf50a883 9b51ca6

8 files changed+32−3

compare with master

unifiedsplit

CHANGELOG+4 libs/prelude/Prelude/Classes.idr+15 src/IRTS/CodegenC.hs+1 src/IRTS/Lang.hs+1−1 src/Idris/ParseOps.hs+2−2 src/Idris/Primitives.hs+6 test/primitives002/expected+2 test/primitives002/run+1

CHANGELOG+4

@@ -12,6 +12,10 @@ New in 0.9.15:

1212* More efficient representation of proof state, leading to faster elaboration

1313 of large expressions.

1414* EXPERIMENTAL Implementation of uniqueness types

15+* Unary negation now desugars to "negate", which is a method of the Neg type class.

16+ This allows instances of Num that can't be negative, like Nat, and it makes correct

17+ IEEE Float operations easier to encode. Additionally, unary negation is now available

18+ to DSL authors.

1519

1620New in 0.9.14:

1721--------------

libs/prelude/Prelude/Classes.idr+15

@@ -137,6 +137,21 @@ instance (Ord a, Ord b) => Ord (a, b) where

137137 then compare xl yl

138138 else compare xr yr

139139

140+-- --------------------------------------------------------- [ Negatable Class ]

141+||| The `Neg` class defines unary negation (-).

142+class Neg a where

143+ ||| The underlying implementation of unary minus. `-5` desugars to `negate (fromInteger 5)`.

144+ negate : a -> a

145+

146+instance Neg Integer where

147+ negate x = prim__subBigInt 0 x

148+

149+instance Neg Int where

150+ negate x = prim__subInt 0 x

151+

152+instance Neg Float where

153+ negate x = prim__negFloat x

154+

140155-- --------------------------------------------------------- [ Numerical Class ]

141156||| The Num class defines basic numerical arithmetic.

142157class Num a where

src/IRTS/CodegenC.hs+1

@@ -474,6 +474,7 @@ doOp v LFATan [x] = v ++ flUnOp "atan" (creg x)

474474doOp v LFSqrt [x] = v ++ flUnOp "sqrt" (creg x)

475475doOp v LFFloor [x] = v ++ flUnOp "floor" (creg x)

476476doOp v LFCeil [x] = v ++ flUnOp "ceil" (creg x)

477+doOp v LFNegate [x] = v ++ "MKFLOAT(vm, -GETFLOAT(" ++ (creg x) ++ "))"

477478

478479doOp v LStrHead [x] = v ++ "idris_strHead(vm, " ++ creg x ++ ")"

479480doOp v LStrTail [x] = v ++ "idris_strTail(vm, " ++ creg x ++ ")"

src/IRTS/Lang.hs+1−1

@@ -52,7 +52,7 @@ data PrimFn = LPlus ArithTy | LMinus ArithTy | LTimes ArithTy

5252 | LBitCast ArithTy ArithTy -- Only for values of equal width

5353

55− | LFSqrt | LFFloor | LFCeil

55+ | LFSqrt | LFFloor | LFCeil | LFNegate

5656

5757 -- construction element extraction element insertion

5858 | LMkVec NativeTy Int | LIdxVec NativeTy Int | LUpdateVec NativeTy Int

src/Idris/ParseOps.hs+2−2

@@ -33,8 +33,8 @@ import qualified Data.ByteString.UTF8 as UTF8

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

3434table :: [FixDecl] -> OperatorTable IdrisParser PTerm

3535table fixes

36− = [[prefix "-" (\fc x -> PApp fc (PRef fc (sUN "-"))

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

36+ =

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

3838 ++ toTable (reverse fixes) ++

3939 [[backtick],

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

src/Idris/Primitives.hs+6

@@ -153,6 +153,8 @@ primitives =

153153 (1, LFFloor) total,

154154 Prim (sUN "prim__floatCeil") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatCeil)

155155 (1, LFCeil) total,

156+ Prim (sUN "prim__negFloat") (ty [(AType ATFloat)] (AType ATFloat)) 1 (c_negFloat)

157+ (1, LFNegate) total,

156158

157159 Prim (sUN "prim__strHead") (ty [StrType] (AType (ATInt ITChar))) 1 (p_strHead)

158160 (1, LStrHead) partial,

@@ -660,6 +662,10 @@ c_intToChar _ = Nothing

660662c_charToInt [(Ch x)] = Just . I . fromEnum $ x

661663c_charToInt _ = Nothing

662664

665+c_negFloat :: [Const] -> Maybe Const

666+c_negFloat [Fl x] = Just $ Fl (negate x)

667+c_negFloat _ = Nothing

668+

663669c_floatToStr :: [Const] -> Maybe Const

664670c_floatToStr [Fl x] = Just $ Str (show x)

665671c_floatToStr _ = Nothing

test/primitives002/expected+2

@@ -42,3 +42,5 @@ prim__floatLog 1.0

42420.0

4343prim__floatSqrt 1.0

44441.0

45+prim__negFloat 1.0

46+-1.0

test/primitives002/run+1

@@ -31,6 +31,7 @@ TESTS=("prim__floatToStr 0.0"

3131"prim__floatExp 1.0"

3232"prim__floatLog 1.0"

3333"prim__floatSqrt 1.0"

34+"prim__negFloat 1.0"

3435)

3536

3637generate_testfile()