eed742e · Idris-dev · git.iko.soy

CHANGELOG.md+1

@@ -19,6 +19,7 @@

19+ Added `discriminate` and `construct` tactics to Pruviloj.

20+ Added `IsSucc` type to `Prelude`, which proves that a `Nat` is a successor.

21+ Added `Data.IOArray`, containing primitives for mutable arrays.

22++ The operator `<|>` is now right-associative (it retains the same precedence).

22+ Reworked operator fixity for `&&` and `||`, as well as the comparison operators: `==`, `/=`, `<`, `<=`, `>`, and `>=`.

23+ Reworked operator fixity for `&&` and `||`, as well as the comparison operators: `==`, `/=`, `<`, `<=`, `>`, and `>=`.

23

24

24## Tool Updates

25## Tool Updates

libs/prelude/Prelude/Applicative.idr+1−1

@@ -38,7 +38,7 @@ liftA2 f a b = (map f a) <*> b

38liftA3 : Applicative f => (a -> b -> c -> d) -> f a -> f b -> f c -> f d

39liftA3 f a b c = (map f a) <*> b <*> c

40

41−infixl 3 <|>

41+infixr 3 <|>

42interface Applicative f => Alternative (f : Type -> Type) where

43 empty : f a

44 (<|>) : f a -> f a -> f a

src/IRTS/CodegenC.hs+1−1

@@ -179,7 +179,7 @@ bcc i (ASSIGNCONST l c)

179 = indent i ++ creg l ++ " = " ++ mkConst c ++ ";\n"

180 where

181 mkConst (I i) = "MKINT(" ++ show i ++ ")"

182− mkConst (BI i) | i < (2^30) = "MKINT(" ++ show i ++ ")"

182+ mkConst (BI i) | i > ((-2)^30) && i < (2^30) = "MKINT(" ++ show i ++ ")"

183 | otherwise = "MKBIGC(vm,\"" ++ show i ++ "\")"

184 mkConst (Fl f) = "MKFLOAT(vm, " ++ (map toUpper $ show f) ++ ")"

185 mkConst (Ch c) = "MKINT(" ++ show (fromEnum c) ++ ")"

test/bignum002/bignum002.idr+1

@@ -3,3 +3,4 @@ module Main

3main : IO ()

4main = do

5 putStrLn $ show $ divNat 1809022195644390369852458 91238741987

6+ putStrLn $ show $ div (-432642342742368327462378462387) 36473264372

test/bignum002/expected+1

@@ -1 +1,2 @@

119827346982734

2+-11861903511836511836