git.iko.soy/Idris-dev
on master help sign in
Merge branch 'master' into NullPtr
2130030Jan Bessai
benchmarks/trivial/sortvec.idr+1
compare with master
unifiedsplit
@@ -18,6 +18,7 @@ mkSortVec (S k) = return (fromInteger !(rndInt 0 10000) :: !(mkSortVec k))
18
18
19main : IO ()
19main : IO ()
20main = do (_ :: arg :: _) <- getArgs
20main = do (_ :: arg :: _) <- getArgs
21+-- let arg = "2000"
21 let vec = runPure [123456789] (mkSortVec (fromInteger (cast arg)))
22 let vec = runPure [123456789] (mkSortVec (fromInteger (cast arg)))
22 putStrLn "Made vector"
23 putStrLn "Made vector"
23 print (vsort vec)
24 print (vsort vec)
idris.cabal+2−1
@@ -57,7 +57,6 @@ Data-files: jsrts/Runtime-browser.js
57 rts/idris_rts.h
57 rts/idris_rts.h
58 rts/idris_stdfgn.h
58 rts/idris_stdfgn.h
59 rts/libtest.c
59 rts/libtest.c
60− java/*.xml
61
60
62Extra-source-files:
61Extra-source-files:
63 Makefile
62 Makefile
@@ -359,6 +358,7 @@ Executable idris
359 , IRTS.Java.ASTBuilding
358 , IRTS.Java.ASTBuilding
360 , IRTS.Java.JTypes
359 , IRTS.Java.JTypes
361 , IRTS.Java.Mangling
360 , IRTS.Java.Mangling
361+ , IRTS.Java.Pom
362 , IRTS.LParser
362 , IRTS.LParser
363 , IRTS.Lang
363 , IRTS.Lang
364 , IRTS.Simplified
364 , IRTS.Simplified
@@ -401,6 +401,7 @@ Executable idris
401 , vector
401 , vector
402 , vector-binary-instances
402 , vector-binary-instances
403 , network
403 , network
404+ , xml
404
405
405 Extensions: MultiParamTypeClasses
406 Extensions: MultiParamTypeClasses
406 , FunctionalDependencies
407 , 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
12
12
13FalseElim : _|_ -> a
13FalseElim : _|_ -> a
14
14
15−-- For rewrite tactic
15+-- ------------------------------------------------------ [ For rewrite tactic ]
16replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y
16replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y
17replace refl prf = prf
17replace refl prf = prf
18
18
@@ -42,36 +42,45 @@ public %assert_total -- reduces at compile time, use with extreme care!
42really_believe_me : a -> b
42really_believe_me : a -> b
43really_believe_me x = prim__believe_me _ _ x
43really_believe_me x = prim__believe_me _ _ x
44
44
45+-- ---------------------------------------------------------------- [ Builtins ]
45namespace Builtins {
46namespace Builtins {
46
47
47Not : Type -> Type
48Not : Type -> Type
48Not a = a -> _|_
49Not a = a -> _|_
49
50
51+-- | Identity function.
50id : a -> a
52id : a -> a
51id x = x
53id x = x
52
54
55+-- | Manually assign a type to an expression.
53the : (a : Type) -> a -> a
56the : (a : Type) -> a -> a
54the _ = id
57the _ = id
55
58
59+-- | Constant function.
56const : a -> b -> a
60const : a -> b -> a
57const x _ = x
61const x _ = x
58
62
63+-- | Return the first element of a pair.
59fst : (s, t) -> s
64fst : (s, t) -> s
60fst (x, y) = x
65fst (x, y) = x
61
66
67+-- | Return the second element of a pair.
62snd : (a, b) -> b
68snd : (a, b) -> b
63snd (x, y) = y
69snd (x, y) = y
64
70
65infixl 9 .
71infixl 9 .
66
72
73+-- | Function composition
67(.) : (b -> c) -> (a -> b) -> a -> c
74(.) : (b -> c) -> (a -> b) -> a -> c
68(.) f g x = f (g x)
75(.) f g x = f (g x)
69
76
77+-- | Takes in the first two arguments in reverse order.
70flip : (a -> b -> c) -> b -> a -> c
78flip : (a -> b -> c) -> b -> a -> c
71flip f x y = f y x
79flip f x y = f y x
72
80
73infixr 1 $
81infixr 1 $
74
82
83+-- | Function application.
75($) : (a -> b) -> a -> b
84($) : (a -> b) -> a -> b
76f $ a = f a
85f $ a = f a
77
86
@@ -82,39 +91,47 @@ data Dec : Type -> Type where
82 Yes : {A : Type} -> A -> Dec A
91 Yes : {A : Type} -> A -> Dec A
83 No : {A : Type} -> (A -> _|_) -> Dec A
92 No : {A : Type} -> (A -> _|_) -> Dec A
84
93
94+-- | Boolean Data Type
85data Bool = False | True
95data Bool = False | True
86
96
97+-- | Boolean elimination
87boolElim : Bool -> |(t : a) -> |(f : a) -> a
98boolElim : Bool -> |(t : a) -> |(f : a) -> a
88boolElim True t e = t
99boolElim True t e = t
89boolElim False t e = e
100boolElim False t e = e
90
101
102+-- | Defines a predicate on Bool which guarantees that the value is true.
91data so : Bool -> Type where oh : so True
103data so : Bool -> Type where oh : so True
92
104
105+-- Syntaxtic sugar for boolean elimination.
93syntax if [test] then [t] else [e] = boolElim test t e
106syntax if [test] then [t] else [e] = boolElim test t e
94syntax [test] "?" [t] ":" [e] = if test then t else e
107syntax [test] "?" [t] ":" [e] = if test then t else e
95
108
109+-- Boolean Operator Precedence
96infixl 4 &&, ||
110infixl 4 &&, ||
97
111
112+-- | Boolean OR
98(||) : Bool -> Bool -> Bool
113(||) : Bool -> Bool -> Bool
99(||) False x = x
114(||) False x = x
100(||) True _ = True
115(||) True _ = True
101
116
117+-- | Boolean AND
102(&&) : Bool -> Bool -> Bool
118(&&) : Bool -> Bool -> Bool
103(&&) True x = x
119(&&) True x = x
104(&&) False _ = False
120(&&) False _ = False
105
121
122+-- | Boolean NOT
106not : Bool -> Bool
123not : Bool -> Bool
107not True = False
124not True = False
108not False = True
125not False = True
109
126
127+-- Numerical Operator Precedence
110infixl 5 ==, /=
128infixl 5 ==, /=
111infixl 6 <, <=, >, >=
129infixl 6 <, <=, >, >=
112infixl 7 <<, >>
130infixl 7 <<, >>
113infixl 8 +,-,++
131infixl 8 +,-,++
114infixl 9 *,/
132infixl 9 *,/
115
133
116−--- Numeric operators
134+-- ------------------------------------------------------- [ Numeric Operators ]
117−
118intToBool : Int -> Bool
135intToBool : Int -> Bool
119intToBool 0 = False
136intToBool 0 = False
120intToBool x = True
137intToBool x = True
@@ -122,6 +139,7 @@ intToBool x = True
122boolOp : (a -> a -> Int) -> a -> a -> Bool
139boolOp : (a -> a -> Int) -> a -> a -> Bool
123boolOp op x y = intToBool (op x y)
140boolOp op x y = intToBool (op x y)
124
141
142+-- | The Eq class defines inequality and equality.
125class Eq a where
143class Eq a where
126 (==) : a -> a -> Bool
144 (==) : a -> a -> Bool
127 (/=) : a -> a -> Bool
145 (/=) : a -> a -> Bool
@@ -162,6 +180,7 @@ instance Eq Ordering where
162 GT == GT = True
180 GT == GT = True
163 _ == _ = False
181 _ == _ = False
164
182
183+-- | The Ord class defines comparison operations on ordered data types.
165class Eq a => Ord a where
184class Eq a => Ord a where
166 compare : a -> a -> Ordering
185 compare : a -> a -> Ordering
167
186
@@ -224,13 +243,14 @@ instance (Ord a, Ord b) => Ord (a, b) where
224 then compare xl yl
243 then compare xl yl
225 else compare xr yr
244 else compare xr yr
226
245
227−
246+-- | The Num class defines basic numerical arithmetic.
228class Num a where
247class Num a where
229 (+) : a -> a -> a
248 (+) : a -> a -> a
230 (-) : a -> a -> a
249 (-) : a -> a -> a
231 (*) : a -> a -> a
250 (*) : a -> a -> a
232−
251+ -- | Absolute value
233 abs : a -> a
252 abs : a -> a
253+ -- | Conversion from Integer.
234 fromInteger : Integer -> a
254 fromInteger : Integer -> a
235
255
236instance Num Integer where
256instance Num Integer where
@@ -334,38 +354,45 @@ instance Ord Bits64 where
334 else if l > r then GT
354 else if l > r then GT
335 else EQ
355 else EQ
336
356
357+-- | Integer division.
337partial
358partial
338div : Integer -> Integer -> Integer
359div : Integer -> Integer -> Integer
339div = prim__sdivBigInt
360div = prim__sdivBigInt
340
361
362+-- | Integer modulus.
341partial
363partial
342mod : Integer -> Integer -> Integer
364mod : Integer -> Integer -> Integer
343mod = prim__sremBigInt
365mod = prim__sremBigInt
344
366
345−
367+-- | Fractional division of two Floats.
346(/) : Float -> Float -> Float
368(/) : Float -> Float -> Float
347(/) = prim__divFloat
369(/) = prim__divFloat
348
370
349−--- string operators
371+-- -------------------------------------------------------- [ String Operators ]
350−
372+-- | Appends two strings together.
351(++) : String -> String -> String
373(++) : String -> String -> String
352(++) = prim__concat
374(++) = prim__concat
353
375
376+-- | Returns the first character in the specified string.
354partial
377partial
355strHead : String -> Char
378strHead : String -> Char
356strHead = prim__strHead
379strHead = prim__strHead
357
380
381+-- | Returns the characters specified after the head of the string.
358partial
382partial
359strTail : String -> String
383strTail : String -> String
360strTail = prim__strTail
384strTail = prim__strTail
361
385
386+-- | Adds a character to the from of the specified string.
362strCons : Char -> String -> String
387strCons : Char -> String -> String
363strCons = prim__strCons
388strCons = prim__strCons
364
389
390+-- | Returns the nth character (starting from 0) of the specified string.
365partial
391partial
366strIndex : String -> Int -> Char
392strIndex : String -> Int -> Char
367strIndex = prim__strIndex
393strIndex = prim__strIndex
368
394
395+-- | Reverses the elements within a String.
369reverse : String -> String
396reverse : String -> String
370reverse = prim__strRev
397reverse = prim__strRev
371
398
src/Core/CaseTree.hs+12−1
@@ -136,6 +136,7 @@ findCalls sc topargs = nub $ nu' topargs sc where
136 | (P Ref n _, args) <- unApply fn
136 | (P Ref n _, args) <- unApply fn
137 = if n `elem` ps then nut ps f ++ nut ps a
137 = if n `elem` ps then nut ps f ++ nut ps a
138 else [(n, map argNames args)] ++ concatMap (nut ps) args
138 else [(n, map argNames args)] ++ concatMap (nut ps) args
139+ | (P (TCon _ _) n _, _) <- unApply fn = []
139 | otherwise = nut ps f ++ nut ps a
140 | otherwise = nut ps f ++ nut ps a
140 nut ps (Bind n (Let t v) sc) = nut ps v ++ nut (n:ps) sc
141 nut ps (Bind n (Let t v) sc) = nut ps v ++ nut (n:ps) sc
141 nut ps (Proj t _) = nut ps t
142 nut ps (Proj t _) = nut ps t
@@ -502,6 +503,9 @@ prune proj (Case n alts)
502 [] -> ImpossibleCase
503 [] -> ImpossibleCase
503 as@[ConCase cn i args sc] -> if proj then mkProj n 0 args sc
504 as@[ConCase cn i args sc] -> if proj then mkProj n 0 args sc
504 else Case n as
505 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
505 -- Bit of a hack here! The default case will always be 0, make sure
509 -- Bit of a hack here! The default case will always be 0, make sure
506 -- it gets caught first.
510 -- it gets caught first.
507 [s@(SucCase _ _), DefaultCase dc]
511 [s@(SucCase _ _), DefaultCase dc]
@@ -517,9 +521,16 @@ prune proj (Case n alts)
517 notErased (DefaultCase ImpossibleCase) = False
521 notErased (DefaultCase ImpossibleCase) = False
518 notErased _ = True
522 notErased _ = True
519
523
520− mkProj n i [] sc = sc
524+ mkProj n i [] sc = prune proj sc
521 mkProj n i (x : xs) sc = mkProj n (i + 1) xs (projRep x n i sc)
525 mkProj n i (x : xs) sc = mkProj n (i + 1) xs (projRep x n i sc)
522
526
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+
523 projRep :: Name -> Name -> Int -> SC -> SC
534 projRep :: Name -> Name -> Int -> SC -> SC
524 projRep arg n i (Case x alts)
535 projRep arg n i (Case x alts)
525 | x == arg = ProjCase (Proj (P Bound n Erased) i)
536 | x == arg = ProjCase (Proj (P Bound n Erased) i)
src/Core/Evaluate.hs+71−14
@@ -2,7 +2,7 @@
2 PatternGuards #-}
2 PatternGuards #-}
3
3
4module Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,
4module Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,
5− simplify, specialise, hnf, convEq, convEq',
5+ rt_simplify, simplify, specialise, hnf, convEq, convEq',
6 Def(..), CaseInfo(..), CaseDefs(..),
6 Def(..), CaseInfo(..), CaseDefs(..),
7 Accessibility(..), Totality(..), PReason(..),
7 Accessibility(..), Totality(..), PReason(..),
8 Context, initContext, ctxtAlist, uconstraints, next_tvar,
8 Context, initContext, ctxtAlist, uconstraints, next_tvar,
@@ -22,6 +22,7 @@ import Core.CaseTree
22
22
23data EvalState = ES { limited :: [(Name, Int)],
23data EvalState = ES { limited :: [(Name, Int)],
24 nexthole :: Int }
24 nexthole :: Int }
25+ deriving Show
25
26
26type Eval a = State EvalState a
27type Eval a = State EvalState a
27
28
@@ -29,6 +30,7 @@ data EvalOpt = Spec
29 | HNF
30 | HNF
30 | Simplify
31 | Simplify
31 | AtREPL
32 | AtREPL
33+ | RunTT
32 deriving (Show, Eq)
34 deriving (Show, Eq)
33
35
34initEval = ES [] 0
36initEval = ES [] 0
@@ -44,7 +46,9 @@ data Value = VP NameType Name Value
44 | VApp Value Value
46 | VApp Value Value
45 | VType UExp
47 | VType UExp
46 | VErased
48 | VErased
49+ | VImpossible
47 | VConstant Const
50 | VConstant Const
51+ | VProj Value Int
48-- | VLazy Env [Value] Term
52-- | VLazy Env [Value] Term
49 | VTmp Int
53 | VTmp Int
50
54
@@ -103,6 +107,18 @@ simplify ctxt env t
103 [Simplify]
107 [Simplify]
104 quote 0 val) initEval
108 quote 0 val) initEval
105
109
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+
106-- | Reduce a term to head normal form
122-- | Reduce a term to head normal form
107hnf :: Context -> Env -> TT Name -> TT Name
123hnf :: Context -> Env -> TT Name -> TT Name
108hnf ctxt env t
124hnf ctxt env t
@@ -162,17 +178,24 @@ eval :: Bool -> Context -> [(Name, Int)] -> Env -> TT Name ->
162eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
178eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
163 spec = Spec `elem` opts
179 spec = Spec `elem` opts
164 simpl = Simplify `elem` opts
180 simpl = Simplify `elem` opts
181+ runtime = RunTT `elem` opts
165 atRepl = AtREPL `elem` opts
182 atRepl = AtREPL `elem` opts
166 hnf = HNF `elem` opts
183 hnf = HNF `elem` opts
167
184
168 -- returns 'True' if the function should block
185 -- returns 'True' if the function should block
169 -- normal evaluation should return false
186 -- normal evaluation should return false
170 blockSimplify (CaseInfo inl dict) n stk
187 blockSimplify (CaseInfo inl dict) n stk
188+ | RunTT `elem` opts
189+ = not (inl || dict) || elem n stk
171 | Simplify `elem` opts
190 | Simplify `elem` opts
172 = (not (inl || dict) || elem n stk)
191 = (not (inl || dict) || elem n stk)
173 || (n == UN "prim__syntactic_eq")
192 || (n == UN "prim__syntactic_eq")
174 | otherwise = False
193 | otherwise = False
175
194
195+ getCases cd | simpl = cases_totcheck cd
196+ | runtime = cases_runtime cd
197+ | otherwise = cases_compiletime cd
198+
176 ev ntimes stk top env (P _ n ty)
199 ev ntimes stk top env (P _ n ty)
177 | Just (Let t v) <- lookup n genv = ev ntimes stk top env v
200 | Just (Let t v) <- lookup n genv = ev ntimes stk top env v
178 ev ntimes_in stk top env (P Ref n ty)
201 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
189 [(CaseOp ci _ _ _ cd, acc)]
212 [(CaseOp ci _ _ _ cd, acc)]
190 | acc == Public &&
213 | acc == Public &&
191 null (fst (cases_totcheck cd)) -> -- unoptimised version
214 null (fst (cases_totcheck cd)) -> -- unoptimised version
192− let (_, tree) = if simpl then cases_totcheck cd
215+ let (ns, tree) = getCases cd in
193− else cases_compiletime cd in
194 if blockSimplify ci n stk
216 if blockSimplify ci n stk
195 then liftM (VP Ref n) (ev ntimes stk top env ty)
217 then liftM (VP Ref n) (ev ntimes stk top env ty)
218+ else -- traceWhen runtime (show (n, ns, tree)) $
196− else do c <- evCase ntimes n (n:stk) top env [] [] tree
219+ do c <- evCase ntimes n (n:stk) top env ns [] tree
197 case c of
220 case c of
198 (Nothing, _) -> liftM (VP Ref n) (ev ntimes stk top env ty)
221 (Nothing, _) -> liftM (VP Ref n) (ev ntimes stk top env ty)
199 (Just v, _) -> return v
222 (Just v, _) -> return v
@@ -237,8 +260,17 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
237 = do f' <- ev ntimes stk False env f
260 = do f' <- ev ntimes stk False env f
238 a' <- ev ntimes stk False env a
261 a' <- ev ntimes stk False env a
239 evApply ntimes stk top env [a'] f'
262 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+
240 ev ntimes stk top env (Constant c) = return $ VConstant c
271 ev ntimes stk top env (Constant c) = return $ VConstant c
241 ev ntimes stk top env Erased = return VErased
272 ev ntimes stk top env Erased = return VErased
273+ ev ntimes stk top env Impossible = return VImpossible
242 ev ntimes stk top env (TType i) = return $ VType i
274 ev ntimes stk top env (TType i) = return $ VType i
243
275
244 evApply ntimes stk top env args (VApp f a)
276 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
246 evApply ntimes stk top env args f
278 evApply ntimes stk top env args f
247 = apply ntimes stk top env f args
279 = apply ntimes stk top env f args
248
280
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+
249 apply ntimes stk top env (VBind True n (Lam t) sc) (a:as)
297 apply ntimes stk top env (VBind True n (Lam t) sc) (a:as)
250 = do a' <- sc a
298 = do a' <- sc a
251 app <- apply ntimes stk top env a' as
299 app <- apply ntimes stk top env a' as
@@ -261,11 +309,11 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
261 case val of
309 case val of
262 [(CaseOp ci _ _ _ cd, acc)]
310 [(CaseOp ci _ _ _ cd, acc)]
263 | acc == Public -> -- unoptimised version
311 | acc == Public -> -- unoptimised version
264− let (ns, tree) = if simpl then cases_totcheck cd
312+ let (ns, tree) = getCases cd in
265− else cases_compiletime cd in
266 if blockSimplify ci n stk
313 if blockSimplify ci n stk
267 then return $ unload env (VP Ref n ty) args
314 then return $ unload env (VP Ref n ty) args
315+ else -- traceWhen runtime (show (n, ns, tree)) $
268− else do c <- evCase ntimes n (n:stk) top env ns args tree
316+ do c <- evCase ntimes n (n:stk) top env ns args tree
269 case c of
317 case c of
270 (Nothing, _) -> return $ unload env (VP Ref n ty) args
318 (Nothing, _) -> return $ unload env (VP Ref n ty) args
271 (Just v, rest) -> evApply ntimes stk top env rest v
319 (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
315 etm' <- ev ntimes stk (not (conHeaded tm))
363 etm' <- ev ntimes stk (not (conHeaded tm))
316 (map snd amap ++ env) etm
364 (map snd amap ++ env) etm
317 return $ Just etm'
365 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
318 evTree ntimes stk top env amap (Case n alts)
369 evTree ntimes stk top env amap (Case n alts)
319 = case lookup n amap of
370 = case lookup n amap of
320− Just v -> do c <- chooseAlt env v (getValArgs v) alts amap
371+ Just v -> doCase ntimes stk top env amap v alts
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
327 _ -> return Nothing
372 _ -> return Nothing
328 evTree ntimes stk top env amap ImpossibleCase = return Nothing
373 evTree ntimes stk top env amap ImpossibleCase = return Nothing
329
374
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+
330 conHeaded tm@(App _ _)
384 conHeaded tm@(App _ _)
331 | (P (DCon _ _) _ _, args) <- unApply tm = True
385 | (P (DCon _ _) _ _, args) <- unApply tm = True
332 conHeaded t = False
386 conHeaded t = False
@@ -439,6 +493,9 @@ instance Quote Value where
439 quote i (VApp f a) = liftM2 App (quote i f) (quote i a)
493 quote i (VApp f a) = liftM2 App (quote i f) (quote i a)
440 quote i (VType u) = return $ TType u
494 quote i (VType u) = return $ TType u
441 quote i VErased = return $ Erased
495 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)
442 quote i (VConstant c) = return $ Constant c
499 quote i (VConstant c) = return $ Constant c
443 quote i (VTmp x) = return $ V (i - x - 1)
500 quote i (VTmp x) = return $ V (i - x - 1)
444
501
src/Core/TT.hs+1
@@ -572,6 +572,7 @@ data TT n = P NameType n (TT n) -- ^ named references
572 | App (TT n) (TT n) -- ^ function, function type, arg
572 | App (TT n) (TT n) -- ^ function, function type, arg
573 | Constant Const -- ^ constant
573 | Constant Const -- ^ constant
574 | Proj (TT n) Int -- ^ argument projection; runtime only
574 | Proj (TT n) Int -- ^ argument projection; runtime only
575+ -- (-1) is a special case for 'subtract one from BI'
575 | Erased -- ^ an erased term
576 | Erased -- ^ an erased term
576 | Impossible -- ^ special case for totality checking
577 | Impossible -- ^ special case for totality checking
577 | TType UExp -- ^ the type of types at some level
578 | 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
80bc reg (SLet (Loc i) e sc) r = bc (L i) e False ++ bc reg sc r
80bc reg (SLet (Loc i) e sc) r = bc (L i) e False ++ bc reg sc r
81bc reg (SUpdate (Loc i) sc) r = bc reg sc False ++ [ASSIGN (L i) reg]
81bc reg (SUpdate (Loc i) sc) r = bc reg sc False ++ [ASSIGN (L i) reg]
82 ++ clean r
82 ++ clean r
83+-- bc reg (SUpdate x sc) r = bc reg sc r -- can't update, just do it
83bc reg (SCon i _ vs) r = MKCON reg i (map getL vs) : clean r
84bc reg (SCon i _ vs) r = MKCON reg i (map getL vs) : clean r
84 where getL (Loc x) = L x
85 where getL (Loc x) = L x
85bc reg (SProj (Loc l) i) r = PROJECTINTO reg (L l) i : clean r
86bc reg (SProj (Loc l) i) r = PROJECTINTO reg (L l) i : clean r
@@ -93,6 +94,7 @@ bc reg (SCase (Loc l) alts) r
93 | otherwise = conCase True reg (L l) alts r
94 | otherwise = conCase True reg (L l) alts r
94bc reg (SChkCase (Loc l) alts) r
95bc reg (SChkCase (Loc l) alts) r
95 = conCase False reg (L l) alts r
96 = conCase False reg (L l) alts r
97+bc reg t r = error $ "Can't compile " ++ show t
96
98
97isConst [] = False
99isConst [] = False
98isConst (SConstCase _ _ : xs) = True
100isConst (SConstCase _ _ : xs) = True
src/IRTS/CodegenJava.hs+10−39
@@ -2,14 +2,13 @@
2module IRTS.CodegenJava (codegenJava) where
2module IRTS.CodegenJava (codegenJava) where
3
3
4import Core.TT hiding (mkApp)
4import Core.TT hiding (mkApp)
5−import IRTS.BCImp
6import IRTS.CodegenCommon
5import IRTS.CodegenCommon
7import IRTS.Java.ASTBuilding
6import IRTS.Java.ASTBuilding
8import IRTS.Java.JTypes
7import IRTS.Java.JTypes
9import IRTS.Java.Mangling
8import IRTS.Java.Mangling
9+import IRTS.Java.Pom (pomString)
10import IRTS.Lang
10import IRTS.Lang
11import IRTS.Simplified
11import IRTS.Simplified
12−import Paths_idris
13import Util.System
12import Util.System
14
13
15import Control.Applicative hiding (Const)
14import Control.Applicative hiding (Const)
@@ -18,10 +17,7 @@ import Control.Monad
18import Control.Monad.Error
17import Control.Monad.Error
19import qualified Control.Monad.Trans as T
18import qualified Control.Monad.Trans as T
20import Control.Monad.Trans.State
19import Control.Monad.Trans.State
21−import Data.Int
22−import Data.List (foldl', intercalate, isPrefixOf,
23− isSuffixOf)
20+import Data.List (foldl', isSuffixOf)
24−import Data.Maybe (fromJust)
25import qualified Data.Text as T
21import qualified Data.Text as T
26import qualified Data.Text.IO as TIO
22import qualified Data.Text.IO as TIO
27import qualified Data.Vector.Unboxed as V
23import qualified Data.Vector.Unboxed as V
@@ -104,20 +100,11 @@ generatePom :: FilePath -> -- tgt dir
104 FilePath -> -- output target
100 FilePath -> -- output target
105 [String] -> -- libs
101 [String] -> -- libs
106 IO ()
102 IO ()
107−generatePom tgtDir out libs = do
103+generatePom tgtDir out libs = writeFile (pomFileName tgtDir) execPom
108− execPom <- getExecutablePom
104+ where
109− execPomTemplate <- TIO.readFile execPom
110− let (Ident clsName) = either error id (mkClassName out)
105+ (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)
106+ execPom = pomString clsName (takeBaseName out) libs
115− (T.replace (T.pack "$DEPENDENCIES$")
107+
116− (mkPomDependencies libs)
117− execPomTemplate
118− )
119− )
120− TIO.writeFile (pomFileName tgtDir) execPom
121
108
122invokeMvn :: FilePath -> String -> IO ()
109invokeMvn :: FilePath -> String -> IO ()
123invokeMvn tgtDir command = do
110invokeMvn tgtDir command = do
@@ -179,24 +166,6 @@ jarHeader =
179 ++ "exec \"$java\" $java_args -jar $MYSELF \"$@\""
166 ++ "exec \"$java\" $java_args -jar $MYSELF \"$@\""
180 ++ "exit 1\n"
167 ++ "exit 1\n"
181
168
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−
200-----------------------------------------------------------------------
169-----------------------------------------------------------------------
201-- Code generation environment
170-- Code generation environment
202
171
@@ -485,8 +454,10 @@ mkExp pp (SApp pushTail name args) =
485-- Bindings
454-- Bindings
486mkExp pp (SLet var newExp inExp) =
455mkExp pp (SLet var newExp inExp) =
487 mkLet pp var newExp inExp
456 mkLet pp var newExp inExp
488−mkExp pp (SUpdate var newExp) =
457+mkExp pp (SUpdate var@(Loc i) newExp) = -- can only update locals
489 mkUpdate pp var newExp
458 mkUpdate pp var newExp
459+mkExp pp (SUpdate var newExp) =
460+ mkExp pp newExp
490
461
491-- Objects
462-- Objects
492mkExp pp (SCon conId _ args) =
463mkExp pp (SCon conId _ args) =
src/IRTS/CodegenJavaScript.hs+1−1
@@ -1047,7 +1047,7 @@ translateExpression (SCon i name vars) =
1047 , JSArray $ map JSVar vars
1047 , JSArray $ map JSVar vars
1048 ]
1048 ]
1049
1049
1050−translateExpression (SUpdate var e) =
1050+translateExpression (SUpdate var@(Loc i) e) =
1051 JSAssign (JSVar var) (translateExpression e)
1051 JSAssign (JSVar var) (translateExpression e)
1052
1052
1053translateExpression (SProj var i) =
1053translateExpression (SProj var i) =
src/IRTS/CodegenLLVM.hs+3−1
@@ -447,6 +447,7 @@ cgExpr (SUpdate (Loc level) expr) = do
447 val <- cgExpr expr
447 val <- cgExpr expr
448 modify $ \s -> s { lexenv = replaceElt level val (lexenv s) }
448 modify $ \s -> s { lexenv = replaceElt level val (lexenv s) }
449 return val
449 return val
450+cgExpr (SUpdate x expr) = cgExpr expr
450cgExpr (SCon tag name args) = do
451cgExpr (SCon tag name args) = do
451 argSlots <- mapM var args
452 argSlots <- mapM var args
452 case sequence argSlots of
453 case sequence argSlots of
@@ -775,7 +776,8 @@ cgConst c@(TT.Str s) = do
775 str <- addGlobal' (ArrayType (1 + fromIntegral (length s)) (IntegerType 8)) (cgConst' c)
776 str <- addGlobal' (ArrayType (1 + fromIntegral (length s)) (IntegerType 8)) (cgConst' c)
776 box FString (ConstantOperand $ C.GetElementPtr True str [C.Int 32 0, C.Int 32 0])
777 box FString (ConstantOperand $ C.GetElementPtr True str [C.Int 32 0, C.Int 32 0])
777cgConst c@(TT.BI i) = do
778cgConst 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)
779 mpz <- alloc mpzTy
781 mpz <- alloc mpzTy
780 inst $ simpleCall "__gmpz_init_set_str" [mpz
782 inst $ simpleCall "__gmpz_init_set_str" [mpz
781 , ConstantOperand $ C.GetElementPtr True str [ C.Int 32 0, C.Int 32 0]
783 , 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
67 dumpDefun <- getDumpDefun
67 dumpDefun <- getDumpDefun
68 case dumpCases of
68 case dumpCases of
69 Nothing -> return ()
69 Nothing -> return ()
70− Just f -> runIO $ writeFile f (showCaseTrees tagged)
70+ Just f -> runIO $ writeFile f (showCaseTrees defs)
71 case dumpDefun of
71 case dumpDefun of
72 Nothing -> return ()
72 Nothing -> return ()
73 Just f -> runIO $ writeFile f (dumpDefuns defuns)
73 Just f -> runIO $ writeFile f (dumpDefuns defuns)
@@ -217,6 +217,8 @@ instance ToIR (TT Name) where
217-- return (LOp LBPlus [k', LConst (BI 1)])
217-- return (LOp LBPlus [k', LConst (BI 1)])
218 | (P (DCon t a) n _, args) <- unApply tm
218 | (P (DCon t a) n _, args) <- unApply tm
219 = irCon env t a n args
219 = irCon env t a n args
220+ | (P (TCon t a) n _, args) <- unApply tm
221+ = return LNothing
220 | (P _ n _, args) <- unApply tm
222 | (P _ n _, args) <- unApply tm
221 = do i <- getIState
223 = do i <- getIState
222 args' <- mapM (ir' env) args
224 args' <- mapM (ir' env) args
@@ -259,6 +261,10 @@ instance ToIR (TT Name) where
259 v' <- ir' env v
261 v' <- ir' env v
260 return $ LLet n v' sc'
262 return $ LLet n v' sc'
261 ir' env (Bind _ _ _) = return $ LNothing
263 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)]
262 ir' env (Proj t i) = do t' <- ir' env t
268 ir' env (Proj t i) = do t' <- ir' env t
263 return $ LProj t' i
269 return $ LProj t' i
264 ir' env (Constant c) = return $ LConst c
270 ir' env (Constant c) = return $ LConst c
src/IRTS/Defunctionalise.hs+2−2
@@ -97,8 +97,8 @@ addApps defs (n, LFun _ _ args e)
97 aa env (LLet n v sc) = liftM2 (DLet n) (aa env v) (aa (n : env) sc)
97 aa env (LLet n v sc) = liftM2 (DLet n) (aa env v) (aa (n : env) sc)
98 aa env (LCon i n args) = liftM (DC i n) (mapM (aa env) args)
98 aa env (LCon i n args) = liftM (DC i n) (mapM (aa env) args)
99 aa env (LProj t@(LV (Glob n)) i)
99 aa env (LProj t@(LV (Glob n)) i)
100− = do t' <- aa env t
100+ | n `elem` env = do t' <- aa env t
101− return $ DProj (DUpdate n (eEVAL t')) i
101+ return $ DProj (DUpdate n (eEVAL t')) i
102 aa env (LProj t i) = do t' <- aa env t
102 aa env (LProj t i) = do t' <- aa env t
103 return $ DProj (eEVAL t') i
103 return $ DProj (eEVAL t') i
104 aa env (LCase e alts) = do e' <- aa env e
104 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
642 let pcover = null pmissing
642 let pcover = null pmissing
643
643
644 -- pdef' is the version that gets compiled for run-time
644 -- 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+
646 logLvl 5 $ "After data structure transformations:\n" ++ show pdef'
648 logLvl 5 $ "After data structure transformations:\n" ++ show pdef'
647
649
648 ist <- getIState
650 ist <- getIState
@@ -728,6 +730,8 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
728 simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x, y)
730 simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x, y)
729 simple_lhs ctxt t = t
731 simple_lhs ctxt t = t
730
732
733+ simple_rt ctxt (p, x, y) = (p, x, rt_simplify ctxt [] y)
734+
731 specNames [] = Nothing
735 specNames [] = Nothing
732 specNames (Specialise ns : _) = Just ns
736 specNames (Specialise ns : _) = Just ns
733 specNames (_ : xs) = specNames xs
737 specNames (_ : xs) = specNames xs
src/Idris/Help.hs+1
@@ -26,6 +26,7 @@ help =
26 [ (["<expr>"], NoArg, "Evaluate an expression"),
26 [ (["<expr>"], NoArg, "Evaluate an expression"),
27 ([":t"], ExprArg, "Check the type of an expression"),
27 ([":t"], ExprArg, "Check the type of an expression"),
28 ([":miss", ":missing"], NameArg, "Show missing clauses"),
28 ([":miss", ":missing"], NameArg, "Show missing clauses"),
29+ ([":doc"], NameArg, "Show internal documentation"),
29 ([":i", ":info"], NameArg, "Display information about a type class"),
30 ([":i", ":info"], NameArg, "Display information about a type class"),
30 ([":total"], NameArg, "Check the totality of a name"),
31 ([":total"], NameArg, "Check the totality of a name"),
31 ([":r",":reload"], NoArg, "Reload current file"),
32 ([":r",":reload"], NoArg, "Reload current file"),
test/reg016/expected+1−6
@@ -1,6 +1 @@
1−4294967295
1+429496729500000000000000
2−4294967296
3−4294967297
4−-1
5−0
6−1
test/reg016/reg016.idr+6−6
@@ -1,11 +1,11 @@
1module Main
1module Main
2
2
3main : IO ()
3main : IO ()
4−main = do print $ the Integer 4294967295
4+main = do print $ the Integer 429496729500000000000000
5− print $ the Integer 4294967296
5+-- print $ the Integer 4294967296
6− print $ the Integer 4294967297
6+-- print $ the Integer 4294967297
7− print $ the Int 4294967295
7+-- print $ the Int 4294967295
8− print $ the Int 4294967296
8+-- print $ the Int 4294967296
9− print $ the Int 4294967297
9+-- print $ the Int 4294967297
10
10
11
11