7572017 · Idris-dev · git.iko.soy

CHANGELOG+4

compare with master

unifiedsplit

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

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

13 of large expressions.

14* 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.

15

19

16New in 0.9.14:

20New in 0.9.14:

17--------------

21--------------

libs/prelude/Prelude/Classes.idr+15

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

137 then compare xl yl

138 else compare xr yr

139

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+

140-- --------------------------------------------------------- [ Numerical Class ]

155-- --------------------------------------------------------- [ Numerical Class ]

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

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

142class Num a where

157class Num a where

src/IRTS/CodegenC.hs+1

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

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

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

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

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

477

478

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

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

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

480doOp 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

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

53

55− | LFSqrt | LFFloor | LFCeil

55+ | LFSqrt | LFFloor | LFCeil | LFNegate

56

57 -- construction element extraction element insertion

58 | 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

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

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

35table fixes

36+ =

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

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

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

38 ++ toTable (reverse fixes) ++

39 [[backtick],

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

src/Idris/Primitives.hs+6

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

153 (1, LFFloor) total,

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

155 (1, LFCeil) total,

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

157+ (1, LFNegate) total,

156

158

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

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

158 (1, LStrHead) partial,

160 (1, LStrHead) partial,

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

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

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

661c_charToInt _ = Nothing

663c_charToInt _ = Nothing

662

664

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

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

667+c_negFloat _ = Nothing

668+

663c_floatToStr :: [Const] -> Maybe Const

669c_floatToStr :: [Const] -> Maybe Const

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

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

665c_floatToStr _ = Nothing

671c_floatToStr _ = Nothing

test/primitives002/expected+2

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

420.0

43prim__floatSqrt 1.0

441.0

45+prim__negFloat 1.0

46+-1.0

test/primitives002/run+1

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

31"prim__floatExp 1.0"

32"prim__floatLog 1.0"

33"prim__floatSqrt 1.0"

34+"prim__negFloat 1.0"

34)

35)

35

36

36generate_testfile()

37generate_testfile()