2130030 · Idris-dev · git.iko.soy

benchmarks/trivial/sortvec.idr+1

@@ -18,6 +18,7 @@ mkSortVec (S k) = return (fromInteger !(rndInt 0 10000) :: !(mkSortVec k))

1818

1919main : IO ()

2020main = do (_ :: arg :: _) <- getArgs

21+-- let arg = "2000"

2122 let vec = runPure [123456789] (mkSortVec (fromInteger (cast arg)))

2223 putStrLn "Made vector"

2324 print (vsort vec)

idris.cabal+2−1

@@ -57,7 +57,6 @@ Data-files: jsrts/Runtime-browser.js

5757 rts/idris_rts.h

5858 rts/idris_stdfgn.h

5959 rts/libtest.c

60− java/*.xml

6160

6261Extra-source-files:

6362 Makefile

@@ -359,6 +358,7 @@ Executable idris

359358 , IRTS.Java.ASTBuilding

360359 , IRTS.Java.JTypes

361360 , IRTS.Java.Mangling

361+ , IRTS.Java.Pom

362362 , IRTS.LParser

363363 , IRTS.Lang

364364 , IRTS.Simplified

@@ -401,6 +401,7 @@ Executable idris

401401 , vector

402402 , vector-binary-instances

403403 , network

404+ , xml

404405

405406 Extensions: MultiParamTypeClasses

406407 , FunctionalDependencies

java/executable_pom.xmldeleted−66

@@ -1,66 +0,0 @@

1−<project xmlns="http://maven.apache.org/POM/4.0.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"

2− xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/maven-v4_0_0.xsd">

3− <modelVersion>4.0.0</modelVersion>

4− <groupId>org.idris-lang</groupId>

5− <artifactId>$ARTIFACT-NAME$</artifactId>

6− <packaging>jar</packaging>

7− <version>1.0</version>

8− <name>$ARTIFACT-NAME$</name>

9−

10− <properties>

11− <project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>

12− <skipTests>true</skipTests>

13− </properties>

14− <dependencies>

15− <dependency>

16− <groupId>org.idris-lang</groupId>

17− <artifactId>idris</artifactId>

18− <version>0.9.10-alpha-2</version>

19− </dependency>

20−$DEPENDENCIES$

21− </dependencies>

22−

23−

24− <build>

25− <finalName>$ARTIFACT-NAME$</finalName>

26− <plugins>

27− <plugin>

28− <groupId>org.apache.maven.plugins</groupId>

29− <artifactId>maven-compiler-plugin</artifactId>

30− <version>3.0</version>

31− <configuration>

32− <source>1.7</source>

33− <target>1.7</target>

34− </configuration>

35− </plugin>

36− <plugin>

37− <groupId>org.apache.maven.plugins</groupId>

38− <artifactId>maven-surefire-plugin</artifactId>

39− <version>2.14</version>

40− <configuration>

41− <skipTests>${skipTests}</skipTests>

42− </configuration>

43− </plugin>

44− <plugin>

45− <groupId>org.apache.maven.plugins</groupId>

46− <artifactId>maven-shade-plugin</artifactId>

47− <version>2.1</version>

48− <executions>

49− <execution>

50− <phase>package</phase>

51− <goals>

52− <goal>shade</goal>

53− </goals>

54− <configuration>

55− <transformers>

56− <transformer implementation="org.apache.maven.plugins.shade.resource.ManifestResourceTransformer">

57− <mainClass>$MAIN-CLASS$</mainClass>

58− </transformer>

59− </transformers>

60− </configuration>

61− </execution>

62− </executions>

63− </plugin>

64− </plugins>

65− </build>

66−</project>

lib/Builtins.idr+35−8

@@ -12,7 +12,7 @@ getProof (a ** v) = v

1212

1313FalseElim : _|_ -> a

1414

15−-- For rewrite tactic

15+-- ------------------------------------------------------ [ For rewrite tactic ]

1616replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y

1717replace refl prf = prf

1818

@@ -42,36 +42,45 @@ public %assert_total -- reduces at compile time, use with extreme care!

4242really_believe_me : a -> b

4343really_believe_me x = prim__believe_me _ _ x

4444

45+-- ---------------------------------------------------------------- [ Builtins ]

4546namespace Builtins {

4647

4748Not : Type -> Type

4849Not a = a -> _|_

4950

51+-- | Identity function.

5052id : a -> a

5153id x = x

5254

55+-- | Manually assign a type to an expression.

5356the : (a : Type) -> a -> a

5457the _ = id

5558

59+-- | Constant function.

5660const : a -> b -> a

5761const x _ = x

5862

63+-- | Return the first element of a pair.

5964fst : (s, t) -> s

6065fst (x, y) = x

6166

67+-- | Return the second element of a pair.

6268snd : (a, b) -> b

6369snd (x, y) = y

6470

6571infixl 9 .

6672

73+-- | Function composition

6774(.) : (b -> c) -> (a -> b) -> a -> c

6875(.) f g x = f (g x)

6976

77+-- | Takes in the first two arguments in reverse order.

7078flip : (a -> b -> c) -> b -> a -> c

7179flip f x y = f y x

7280

7381infixr 1 $

7482

83+-- | Function application.

7584($) : (a -> b) -> a -> b

7685f $ a = f a

7786

@@ -82,39 +91,47 @@ data Dec : Type -> Type where

8291 Yes : {A : Type} -> A -> Dec A

8392 No : {A : Type} -> (A -> _|_) -> Dec A

8493

94+-- | Boolean Data Type

8595data Bool = False | True

8696

97+-- | Boolean elimination

8798boolElim : Bool -> |(t : a) -> |(f : a) -> a

8899boolElim True t e = t

89100boolElim False t e = e

90101

102+-- | Defines a predicate on Bool which guarantees that the value is true.

91103data so : Bool -> Type where oh : so True

92104

105+-- Syntaxtic sugar for boolean elimination.

93106syntax if [test] then [t] else [e] = boolElim test t e

94107syntax [test] "?" [t] ":" [e] = if test then t else e

95108

109+-- Boolean Operator Precedence

96110infixl 4 &&, ||

97111

112+-- | Boolean OR

98113(||) : Bool -> Bool -> Bool

99114(||) False x = x

100115(||) True _ = True

101116

117+-- | Boolean AND

102118(&&) : Bool -> Bool -> Bool

103119(&&) True x = x

104120(&&) False _ = False

105121

122+-- | Boolean NOT

106123not : Bool -> Bool

107124not True = False

108125not False = True

109126

127+-- Numerical Operator Precedence

110128infixl 5 ==, /=

111129infixl 6 <, <=, >, >=

112130infixl 7 <<, >>

113131infixl 8 +,-,++

114132infixl 9 *,/

115133

116−--- Numeric operators

117−

134+-- ------------------------------------------------------- [ Numeric Operators ]

118135intToBool : Int -> Bool

119136intToBool 0 = False

120137intToBool x = True

@@ -122,6 +139,7 @@ intToBool x = True

122139boolOp : (a -> a -> Int) -> a -> a -> Bool

123140boolOp op x y = intToBool (op x y)

124141

142+-- | The Eq class defines inequality and equality.

125143class Eq a where

126144 (==) : a -> a -> Bool

127145 (/=) : a -> a -> Bool

@@ -162,6 +180,7 @@ instance Eq Ordering where

162180 GT == GT = True

163181 _ == _ = False

164182

183+-- | The Ord class defines comparison operations on ordered data types.

165184class Eq a => Ord a where

166185 compare : a -> a -> Ordering

167186

@@ -224,13 +243,14 @@ instance (Ord a, Ord b) => Ord (a, b) where

224243 then compare xl yl

225244 else compare xr yr

226245

227−

246+-- | The Num class defines basic numerical arithmetic.

228247class Num a where

229248 (+) : a -> a -> a

230249 (-) : a -> a -> a

231250 (*) : a -> a -> a

232−

251+ -- | Absolute value

233252 abs : a -> a

253+ -- | Conversion from Integer.

234254 fromInteger : Integer -> a

235255

236256instance Num Integer where

@@ -334,38 +354,45 @@ instance Ord Bits64 where

334354 else if l > r then GT

335355 else EQ

336356

357+-- | Integer division.

337358partial

338359div : Integer -> Integer -> Integer

339360div = prim__sdivBigInt

340361

362+-- | Integer modulus.

341363partial

342364mod : Integer -> Integer -> Integer

343365mod = prim__sremBigInt

344366

345−

367+-- | Fractional division of two Floats.

346368(/) : Float -> Float -> Float

347369(/) = prim__divFloat

348370

349−--- string operators

350−

371+-- -------------------------------------------------------- [ String Operators ]

372+-- | Appends two strings together.

351373(++) : String -> String -> String

352374(++) = prim__concat

353375

376+-- | Returns the first character in the specified string.

354377partial

355378strHead : String -> Char

356379strHead = prim__strHead

357380

381+-- | Returns the characters specified after the head of the string.

358382partial

359383strTail : String -> String

360384strTail = prim__strTail

361385

386+-- | Adds a character to the from of the specified string.

362387strCons : Char -> String -> String

363388strCons = prim__strCons

364389

390+-- | Returns the nth character (starting from 0) of the specified string.

365391partial

366392strIndex : String -> Int -> Char

367393strIndex = prim__strIndex

368394

395+-- | Reverses the elements within a String.

369396reverse : String -> String

370397reverse = prim__strRev

371398

src/Core/CaseTree.hs+12−1

@@ -136,6 +136,7 @@ findCalls sc topargs = nub $ nu' topargs sc where

136136 | (P Ref n _, args) <- unApply fn

137137 = if n `elem` ps then nut ps f ++ nut ps a

138138 else [(n, map argNames args)] ++ concatMap (nut ps) args

139+ | (P (TCon _ _) n _, _) <- unApply fn = []

139140 | otherwise = nut ps f ++ nut ps a

140141 nut ps (Bind n (Let t v) sc) = nut ps v ++ nut (n:ps) sc

141142 nut ps (Proj t _) = nut ps t

@@ -502,6 +503,9 @@ prune proj (Case n alts)

502503 [] -> ImpossibleCase

503504 as@[ConCase cn i args sc] -> if proj then mkProj n 0 args sc

504505 else Case n as

506+ as@[SucCase cn sc] -> if proj then mkProj n (-1) [cn] sc

507+ else Case n as

508+ as@[ConstCase _ sc] -> prune proj sc

505509 -- Bit of a hack here! The default case will always be 0, make sure

506510 -- it gets caught first.

507511 [s@(SucCase _ _), DefaultCase dc]

@@ -517,9 +521,16 @@ prune proj (Case n alts)

517521 notErased (DefaultCase ImpossibleCase) = False

518522 notErased _ = True

519523

520− mkProj n i [] sc = sc

524+ mkProj n i [] sc = prune proj sc

521525 mkProj n i (x : xs) sc = mkProj n (i + 1) xs (projRep x n i sc)

522526

527+ -- Change every 'n' in sc to 'n-1'

528+-- mkProjS n cn sc = prune proj (fmap projn sc) where

529+-- projn pn@(P _ n' _)

530+-- | cn == n' = App (App (P Ref (UN "prim__subBigInt") Erased)

531+-- (P Bound n Erased)) (Constant (BI 1))

532+-- projn t = t

533+

523534 projRep :: Name -> Name -> Int -> SC -> SC

524535 projRep arg n i (Case x alts)

525536 | x == arg = ProjCase (Proj (P Bound n Erased) i)

src/Core/Evaluate.hs+71−14

@@ -2,7 +2,7 @@

22 PatternGuards #-}

33

44module Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,

5− simplify, specialise, hnf, convEq, convEq',

5+ rt_simplify, simplify, specialise, hnf, convEq, convEq',

66 Def(..), CaseInfo(..), CaseDefs(..),

77 Accessibility(..), Totality(..), PReason(..),

88 Context, initContext, ctxtAlist, uconstraints, next_tvar,

@@ -22,6 +22,7 @@ import Core.CaseTree

2222

2323data EvalState = ES { limited :: [(Name, Int)],

2424 nexthole :: Int }

25+ deriving Show

2526

2627type Eval a = State EvalState a

2728

@@ -29,6 +30,7 @@ data EvalOpt = Spec

2930 | HNF

3031 | Simplify

3132 | AtREPL

33+ | RunTT

3234 deriving (Show, Eq)

3335

3436initEval = ES [] 0

@@ -44,7 +46,9 @@ data Value = VP NameType Name Value

4446 | VApp Value Value

4547 | VType UExp

4648 | VErased

49+ | VImpossible

4750 | VConstant Const

51+ | VProj Value Int

4852-- | VLazy Env [Value] Term

4953 | VTmp Int

5054

@@ -103,6 +107,18 @@ simplify ctxt env t

103107 [Simplify]

104108 quote 0 val) initEval

105109

110+-- | Simplify for run-time (i.e. basic inlining)

111+rt_simplify :: Context -> Env -> TT Name -> TT Name

112+rt_simplify ctxt env t

113+ = evalState (do val <- eval False ctxt [(UN "lazy", 0),

114+ (UN "assert_smaller", 0),

115+ (UN "par", 0),

116+ (UN "prim__syntactic_eq", 0),

117+ (UN "prim_fork", 0)]

118+ (map finalEntry env) (finalise t)

119+ [RunTT]

120+ quote 0 val) initEval

121+

106122-- | Reduce a term to head normal form

107123hnf :: Context -> Env -> TT Name -> TT Name

108124hnf ctxt env t

@@ -162,17 +178,24 @@ eval :: Bool -> Context -> [(Name, Int)] -> Env -> TT Name ->

162178eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

163179 spec = Spec `elem` opts

164180 simpl = Simplify `elem` opts

181+ runtime = RunTT `elem` opts

165182 atRepl = AtREPL `elem` opts

166183 hnf = HNF `elem` opts

167184

168185 -- returns 'True' if the function should block

169186 -- normal evaluation should return false

170187 blockSimplify (CaseInfo inl dict) n stk

188+ | RunTT `elem` opts

189+ = not (inl || dict) || elem n stk

171190 | Simplify `elem` opts

172191 = (not (inl || dict) || elem n stk)

173192 || (n == UN "prim__syntactic_eq")

174193 | otherwise = False

175194

195+ getCases cd | simpl = cases_totcheck cd

196+ | runtime = cases_runtime cd

197+ | otherwise = cases_compiletime cd

198+

176199 ev ntimes stk top env (P _ n ty)

177200 | Just (Let t v) <- lookup n genv = ev ntimes stk top env v

178201 ev ntimes_in stk top env (P Ref n ty)

@@ -189,11 +212,11 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

189212 [(CaseOp ci _ _ _ cd, acc)]

190213 | acc == Public &&

191214 null (fst (cases_totcheck cd)) -> -- unoptimised version

192− let (_, tree) = if simpl then cases_totcheck cd

193− else cases_compiletime cd in

215+ let (ns, tree) = getCases cd in

194216 if blockSimplify ci n stk

195217 then liftM (VP Ref n) (ev ntimes stk top env ty)

196− else do c <- evCase ntimes n (n:stk) top env [] [] tree

218+ else -- traceWhen runtime (show (n, ns, tree)) $

219+ do c <- evCase ntimes n (n:stk) top env ns [] tree

197220 case c of

198221 (Nothing, _) -> liftM (VP Ref n) (ev ntimes stk top env ty)

199222 (Just v, _) -> return v

@@ -237,8 +260,17 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

237260 = do f' <- ev ntimes stk False env f

238261 a' <- ev ntimes stk False env a

239262 evApply ntimes stk top env [a'] f'

263+ ev ntimes stk top env (Proj t i)

264+ = do -- evaluate dictionaries if it means the projection works

265+ t' <- ev ntimes stk top env t

266+-- tfull' <- reapply ntimes stk top env t' []

267+ return (doProj t' (getValArgs t'))

268+ where doProj t' (VP (DCon _ _) _ _, args) | i < length args = args!!i

269+ doProj t' _ = VProj t' i

270+

240271 ev ntimes stk top env (Constant c) = return $ VConstant c

241272 ev ntimes stk top env Erased = return VErased

273+ ev ntimes stk top env Impossible = return VImpossible

242274 ev ntimes stk top env (TType i) = return $ VType i

243275

244276 evApply ntimes stk top env args (VApp f a)

@@ -246,6 +278,22 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

246278 evApply ntimes stk top env args f

247279 = apply ntimes stk top env f args

248280

281+ reapply ntimes stk top env f@(VP Ref n ty) args

282+ = let val = lookupDefAcc n atRepl ctxt in

283+ case val of

284+ [(CaseOp ci _ _ _ cd, acc)] ->

285+ let (ns, tree) = getCases cd in

286+ do c <- evCase ntimes n (n:stk) top env ns args tree

287+ case c of

288+ (Nothing, _) -> return $ unload env (VP Ref n ty) args

289+ (Just v, rest) -> evApply ntimes stk top env rest v

290+ _ -> case args of

291+ (a : as) -> return $ unload env f (a : as)

292+ [] -> return f

293+ reapply ntimes stk top env (VApp f a) args

294+ = reapply ntimes stk top env f (a : args)

295+ reapply ntimes stk top env v args = return v

296+

249297 apply ntimes stk top env (VBind True n (Lam t) sc) (a:as)

250298 = do a' <- sc a

251299 app <- apply ntimes stk top env a' as

@@ -261,11 +309,11 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

261309 case val of

262310 [(CaseOp ci _ _ _ cd, acc)]

263311 | acc == Public -> -- unoptimised version

264− let (ns, tree) = if simpl then cases_totcheck cd

265− else cases_compiletime cd in

312+ let (ns, tree) = getCases cd in

266313 if blockSimplify ci n stk

267314 then return $ unload env (VP Ref n ty) args

268− else do c <- evCase ntimes n (n:stk) top env ns args tree

315+ else -- traceWhen runtime (show (n, ns, tree)) $

316+ do c <- evCase ntimes n (n:stk) top env ns args tree

269317 case c of

270318 (Nothing, _) -> return $ unload env (VP Ref n ty) args

271319 (Just v, rest) -> evApply ntimes stk top env rest v

@@ -315,18 +363,24 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

315363 etm' <- ev ntimes stk (not (conHeaded tm))

316364 (map snd amap ++ env) etm

317365 return $ Just etm'

366+ evTree ntimes stk top env amap (ProjCase t alts)

367+ = do t' <- ev ntimes stk top env t

368+ doCase ntimes stk top env amap t' alts

318369 evTree ntimes stk top env amap (Case n alts)

319370 = case lookup n amap of

320− Just v -> do c <- chooseAlt env v (getValArgs v) alts amap

321− case c of

322− Just (altmap, sc) -> evTree ntimes stk top env altmap sc

323− _ -> do c' <- chooseAlt' ntimes stk env v (getValArgs v) alts amap

324− case c' of

325− Just (altmap, sc) -> evTree ntimes stk top env altmap sc

326− _ -> return Nothing

371+ Just v -> doCase ntimes stk top env amap v alts

327372 _ -> return Nothing

328373 evTree ntimes stk top env amap ImpossibleCase = return Nothing

329374

375+ doCase ntimes stk top env amap v alts =

376+ do c <- chooseAlt env v (getValArgs v) alts amap

377+ case c of

378+ Just (altmap, sc) -> evTree ntimes stk top env altmap sc

379+ _ -> do c' <- chooseAlt' ntimes stk env v (getValArgs v) alts amap

380+ case c' of

381+ Just (altmap, sc) -> evTree ntimes stk top env altmap sc

382+ _ -> return Nothing

383+

330384 conHeaded tm@(App _ _)

331385 | (P (DCon _ _) _ _, args) <- unApply tm = True

332386 conHeaded t = False

@@ -439,6 +493,9 @@ instance Quote Value where

439493 quote i (VApp f a) = liftM2 App (quote i f) (quote i a)

440494 quote i (VType u) = return $ TType u

441495 quote i VErased = return $ Erased

496+ quote i VImpossible = return $ Impossible

497+ quote i (VProj v j) = do v' <- quote i v

498+ return (Proj v' j)

442499 quote i (VConstant c) = return $ Constant c

443500 quote i (VTmp x) = return $ V (i - x - 1)

444501

src/Core/TT.hs+1

@@ -572,6 +572,7 @@ data TT n = P NameType n (TT n) -- ^ named references

572572 | App (TT n) (TT n) -- ^ function, function type, arg

573573 | Constant Const -- ^ constant

574574 | Proj (TT n) Int -- ^ argument projection; runtime only

575+ -- (-1) is a special case for 'subtract one from BI'

575576 | Erased -- ^ an erased term

576577 | Impossible -- ^ special case for totality checking

577578 | TType UExp -- ^ the type of types at some level

src/IRTS/Bytecode.hs+2

@@ -80,6 +80,7 @@ bc reg (SForeign l t fname args) r

8080bc reg (SLet (Loc i) e sc) r = bc (L i) e False ++ bc reg sc r

8181bc reg (SUpdate (Loc i) sc) r = bc reg sc False ++ [ASSIGN (L i) reg]

8282 ++ clean r

83+-- bc reg (SUpdate x sc) r = bc reg sc r -- can't update, just do it

8384bc reg (SCon i _ vs) r = MKCON reg i (map getL vs) : clean r

8485 where getL (Loc x) = L x

8586bc reg (SProj (Loc l) i) r = PROJECTINTO reg (L l) i : clean r

@@ -93,6 +94,7 @@ bc reg (SCase (Loc l) alts) r

9394 | otherwise = conCase True reg (L l) alts r

9495bc reg (SChkCase (Loc l) alts) r

9596 = conCase False reg (L l) alts r

97+bc reg t r = error $ "Can't compile " ++ show t

9698

9799isConst [] = False

98100isConst (SConstCase _ _ : xs) = True

src/IRTS/CodegenJava.hs+10−39

@@ -2,14 +2,13 @@

22module IRTS.CodegenJava (codegenJava) where

33

44import Core.TT hiding (mkApp)

5−import IRTS.BCImp

65import IRTS.CodegenCommon

76import IRTS.Java.ASTBuilding

87import IRTS.Java.JTypes

98import IRTS.Java.Mangling

9+import IRTS.Java.Pom (pomString)

1010import IRTS.Lang

1111import IRTS.Simplified

12−import Paths_idris

1312import Util.System

1413

1514import Control.Applicative hiding (Const)

@@ -18,10 +17,7 @@ import Control.Monad

1817import Control.Monad.Error

1918import qualified Control.Monad.Trans as T

2019import Control.Monad.Trans.State

21−import Data.Int

22−import Data.List (foldl', intercalate, isPrefixOf,

23− isSuffixOf)

24−import Data.Maybe (fromJust)

20+import Data.List (foldl', isSuffixOf)

2521import qualified Data.Text as T

2622import qualified Data.Text.IO as TIO

2723import qualified Data.Vector.Unboxed as V

@@ -104,20 +100,11 @@ generatePom :: FilePath -> -- tgt dir

104100 FilePath -> -- output target

105101 [String] -> -- libs

106102 IO ()

107−generatePom tgtDir out libs = do

108− execPom <- getExecutablePom

109− execPomTemplate <- TIO.readFile execPom

110− let (Ident clsName) = either error id (mkClassName out)

111− let execPom = T.replace (T.pack "$MAIN-CLASS$")

112− (T.pack clsName)

113− (T.replace (T.pack "$ARTIFACT-NAME$")

114− (T.pack $ takeBaseName out)

115− (T.replace (T.pack "$DEPENDENCIES$")

116− (mkPomDependencies libs)

117− execPomTemplate

118− )

119− )

120− TIO.writeFile (pomFileName tgtDir) execPom

103+generatePom tgtDir out libs = writeFile (pomFileName tgtDir) execPom

104+ where

105+ (Ident clsName) = either error id (mkClassName out)

106+ execPom = pomString clsName (takeBaseName out) libs

107+

121108

122109invokeMvn :: FilePath -> String -> IO ()

123110invokeMvn tgtDir command = do

@@ -179,24 +166,6 @@ jarHeader =

179166 ++ "exec \"$java\" $java_args -jar $MYSELF \"$@\""

180167 ++ "exit 1\n"

181168

182−mkPomDependencies :: [String] -> T.Text

183−mkPomDependencies deps =

184− T.concat $ map (T.concat . map (T.append (T.pack " ")) . mkDependency . T.pack) deps

185− where

186− mkDependency s =

187− case T.splitOn (T.pack ":") s of

188− [g, a, v] ->

189− [ T.pack $ "<dependency>\n"

190− , T.append (T.pack " ") $ mkGroupId g

191− , T.append (T.pack " ") $ mkArtifactId a

192− , T.append (T.pack " ") $ mkVersion v

193− , T.pack $ "</dependency>\n"

194− ]

195− _ -> []

196− mkGroupId g = T.append (T.pack $ "<groupId>") (T.append g $ T.pack "</groupId>\n")

197− mkArtifactId a = T.append (T.pack $ "<artifactId>") (T.append a $ T.pack "</artifactId>\n")

198− mkVersion v = T.append (T.pack $ "<version>") (T.append v $ T.pack "</version>\n")

199−

200169-----------------------------------------------------------------------

201170-- Code generation environment

202171

@@ -485,8 +454,10 @@ mkExp pp (SApp pushTail name args) =

485454-- Bindings

486455mkExp pp (SLet var newExp inExp) =

487456 mkLet pp var newExp inExp

488−mkExp pp (SUpdate var newExp) =

457+mkExp pp (SUpdate var@(Loc i) newExp) = -- can only update locals

489458 mkUpdate pp var newExp

459+mkExp pp (SUpdate var newExp) =

460+ mkExp pp newExp

490461

491462-- Objects

492463mkExp pp (SCon conId _ args) =

src/IRTS/CodegenJavaScript.hs+1−1

@@ -1047,7 +1047,7 @@ translateExpression (SCon i name vars) =

10471047 , JSArray $ map JSVar vars

10481048 ]

10491049

1050−translateExpression (SUpdate var e) =

1050+translateExpression (SUpdate var@(Loc i) e) =

10511051 JSAssign (JSVar var) (translateExpression e)

10521052

10531053translateExpression (SProj var i) =

src/IRTS/CodegenLLVM.hs+3−1

@@ -447,6 +447,7 @@ cgExpr (SUpdate (Loc level) expr) = do

447447 val <- cgExpr expr

448448 modify $ \s -> s { lexenv = replaceElt level val (lexenv s) }

449449 return val

450+cgExpr (SUpdate x expr) = cgExpr expr

450451cgExpr (SCon tag name args) = do

451452 argSlots <- mapM var args

452453 case sequence argSlots of

@@ -775,7 +776,8 @@ cgConst c@(TT.Str s) = do

775776 str <- addGlobal' (ArrayType (1 + fromIntegral (length s)) (IntegerType 8)) (cgConst' c)

776777 box FString (ConstantOperand $ C.GetElementPtr True str [C.Int 32 0, C.Int 32 0])

777778cgConst c@(TT.BI i) = do

778− str <- addGlobal' (ArrayType (1 + fromInteger (numDigits 10 i)) (IntegerType 8)) (cgConst' c)

779+ let stringRepLen = (if i < 0 then 2 else 1) + fromInteger (numDigits 10 i)

780+ str <- addGlobal' (ArrayType stringRepLen (IntegerType 8)) (cgConst' c)

779781 mpz <- alloc mpzTy

780782 inst $ simpleCall "__gmpz_init_set_str" [mpz

781783 , ConstantOperand $ C.GetElementPtr True str [ C.Int 32 0, C.Int 32 0]

src/IRTS/Compiler.hs+7−1

@@ -67,7 +67,7 @@ compile codegen f tm

6767 dumpDefun <- getDumpDefun

6868 case dumpCases of

6969 Nothing -> return ()

70− Just f -> runIO $ writeFile f (showCaseTrees tagged)

70+ Just f -> runIO $ writeFile f (showCaseTrees defs)

7171 case dumpDefun of

7272 Nothing -> return ()

7373 Just f -> runIO $ writeFile f (dumpDefuns defuns)

@@ -217,6 +217,8 @@ instance ToIR (TT Name) where

217217-- return (LOp LBPlus [k', LConst (BI 1)])

218218 | (P (DCon t a) n _, args) <- unApply tm

219219 = irCon env t a n args

220+ | (P (TCon t a) n _, args) <- unApply tm

221+ = return LNothing

220222 | (P _ n _, args) <- unApply tm

221223 = do i <- getIState

222224 args' <- mapM (ir' env) args

@@ -259,6 +261,10 @@ instance ToIR (TT Name) where

259261 v' <- ir' env v

260262 return $ LLet n v' sc'

261263 ir' env (Bind _ _ _) = return $ LNothing

264+ ir' env (Proj t i) | i == -1

265+ = do t' <- ir' env t

266+ return $ LOp (LMinus (ATInt ITBig))

267+ [t', LConst (BI 1)]

262268 ir' env (Proj t i) = do t' <- ir' env t

263269 return $ LProj t' i

264270 ir' env (Constant c) = return $ LConst c

src/IRTS/Defunctionalise.hs+2−2

@@ -97,8 +97,8 @@ addApps defs (n, LFun _ _ args e)

9797 aa env (LLet n v sc) = liftM2 (DLet n) (aa env v) (aa (n : env) sc)

9898 aa env (LCon i n args) = liftM (DC i n) (mapM (aa env) args)

9999 aa env (LProj t@(LV (Glob n)) i)

100− = do t' <- aa env t

101− return $ DProj (DUpdate n (eEVAL t')) i

100+ | n `elem` env = do t' <- aa env t

101+ return $ DProj (DUpdate n (eEVAL t')) i

102102 aa env (LProj t i) = do t' <- aa env t

103103 return $ DProj (eEVAL t') i

104104 aa env (LCase e alts) = do e' <- aa env e

src/IRTS/Java/Pom.hsnew file+89

@@ -0,0 +1,89 @@

1+module IRTS.Java.Pom (pomString) where

2+

3+import Data.List (unfoldr)

4+import Text.XML.Light

5+

6+uattr :: String -> String -> Attr

7+uattr k v = Attr (QName k Nothing Nothing) v

8+

9+-- from http://stackoverflow.com/a/4978733/283260

10+splitOn :: Eq a => a -> [a] -> [[a]]

11+splitOn chr = unfoldr sep where

12+ sep [] = Nothing

13+ sep l = Just . fmap (drop 1) . break (==chr) $ l

14+

15+parseToDep :: String -> Element

16+parseToDep tuple =

17+ case splitOn ':' tuple of

18+ [g, a, v] -> dependency g a v

19+ _ -> blank_element

20+

21+dependency :: String -> String -> String -> Element

22+dependency g a v = unode "dependency" (groupArtifactVersion g a v)

23+

24+groupArtifactVersion :: String -> String -> String -> [Element]

25+groupArtifactVersion g a v = [

26+ unode "groupId" g,

27+ unode "artifactId" a,

28+ unode "version" v

29+ ]

30+

31+pomString :: String -> String -> [String] -> String

32+pomString c a d = ppElement $ pom c a d

33+

34+pom :: String -> String -> [String] -> Element

35+pom clsName artifactName dependencies = unode "project" ([

36+ uattr "xmlns" "http://maven.apache.org/POM/4.0.0",

37+ uattr "xmlns:xsi" "http://www.w3.org/2001/XMLSchema-instance",

38+ uattr "xsi:schemaLocation" "http://maven.apache.org/POM/4.0.0 http://maven.apache.org/maven-v4_0_0.xsd"

39+ ],

40+ [

41+ unode "modelVersion" "4.0.0",

42+ unode "groupId" "org.idris-lang",

43+ unode "artifactId" artifactName,

44+ unode "packaging" "jar",

45+ unode "version" "1.0",

46+ unode "name" artifactName,

47+ unode "properties" [

48+ unode "project.build.sourceEncoding" "UTF-8",

49+ unode "skipTest" "true"

50+ ],

51+ unode "dependencies" (

52+ dependency "org.idris-lang" "idris" "0.9.10-alpha-2" :

53+ map parseToDep dependencies

54+ ),

55+ unode "build" [

56+ unode "finalName" artifactName,

57+ unode "plugins" [

58+ unode "plugin" (

59+ unode "configuration" [

60+ unode "source" "1.7",

61+ unode "target" "1.7"

62+ ] : groupArtifactVersion "org.apache.maven.plugins" "maven-compiler-plugin" "3.0"

63+ ),

64+ unode "plugin" (

65+ unode "configuration" (

66+ unode "skipTests" "${skipTests}"

67+ ) : groupArtifactVersion "org.apache.maven.plugins" "maven-surefile-plugin" "2.14"

68+ ),

69+ unode "plugin" (

70+ unode "executions" [

71+ unode "execution" [

72+ unode "phase" "package",

73+ unode "goals" (

74+ unode "goal" "shade"

75+ ),

76+ unode "configuration" (

77+ unode "transformers" (

78+ unode "transformer" (

79+ uattr "implementation" "org.apache.maven.plugins.shade.resource.ManifestResourceTransformer",

80+ unode "mainClass" clsName

81+ )

82+ )

83+ )

84+ ]

85+ ] : groupArtifactVersion "org.apache.maven.plugins" "maven-shade-plugin" "2.1"

86+ )

87+ ]

88+ ]

89+ ])

src/Idris/ElabDecls.hs+5−1

@@ -642,7 +642,9 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

642642 let pcover = null pmissing

643643

644644 -- pdef' is the version that gets compiled for run-time

645− pdef' <- applyOpts optpdef

645+ pdef_in' <- applyOpts optpdef

646+ let pdef' = map (simple_rt (tt_ctxt ist)) pdef_in'

647+

646648 logLvl 5 $ "After data structure transformations:\n" ++ show pdef'

647649

648650 ist <- getIState

@@ -728,6 +730,8 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

728730 simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x, y)

729731 simple_lhs ctxt t = t

730732

733+ simple_rt ctxt (p, x, y) = (p, x, rt_simplify ctxt [] y)

734+

731735 specNames [] = Nothing

732736 specNames (Specialise ns : _) = Just ns

733737 specNames (_ : xs) = specNames xs

src/Idris/Help.hs+1

@@ -26,6 +26,7 @@ help =

2626 [ (["<expr>"], NoArg, "Evaluate an expression"),

2727 ([":t"], ExprArg, "Check the type of an expression"),

2828 ([":miss", ":missing"], NameArg, "Show missing clauses"),

29+ ([":doc"], NameArg, "Show internal documentation"),

2930 ([":i", ":info"], NameArg, "Display information about a type class"),

3031 ([":total"], NameArg, "Check the totality of a name"),

3132 ([":r",":reload"], NoArg, "Reload current file"),

test/reg016/expected+1−6

@@ -1,6 +1 @@

1−4294967295

2−4294967296

3−4294967297

4−-1

5−0

6−1

1+429496729500000000000000

test/reg016/reg016.idr+6−6

@@ -1,11 +1,11 @@

11module Main

22

33main : IO ()

4−main = do print $ the Integer 4294967295

5− print $ the Integer 4294967296

6− print $ the Integer 4294967297

7− print $ the Int 4294967295

8− print $ the Int 4294967296

9− print $ the Int 4294967297

4+main = do print $ the Integer 429496729500000000000000

5+-- print $ the Integer 4294967296

6+-- print $ the Integer 4294967297

7+-- print $ the Int 4294967295

8+-- print $ the Int 4294967296

9+-- print $ the Int 4294967297

1010

1111