dd44389 · Idris-dev · git.iko.soy

.travis.yml+2

@@ -6,6 +6,8 @@ before_install:

6 - sudo apt-get install -qq libghc-unordered-containers-dev libghc-mtl-dev libghc-network-dev libghc-xml-dev libghc-transformers-dev libghc-text-dev libghc-utf8-string-dev libghc-vector-dev libghc-split-dev libghc-ansi-terminal-dev libghc-ansi-wl-pprint-dev

7 # trifecta dependencies

8 - sudo apt-get install -qq libghc-blaze-builder-dev libghc-blaze-html-dev libghc-data-lens-dev libghc-bifunctors-dev libghc-hashable-dev libghc-semigroups-dev libghc-semigroupoids-dev libghc-parallel-dev libghc-comonad-dev libghc-terminfo-dev libghc-keys-dev

9+ # test dependency

10+ - sudo apt-get install -qq expect

9install:

11install:

10 - cabal install -f FFI -f LLVM --only-dependencies --enable-tests

12 - cabal install -f FFI -f LLVM --only-dependencies --enable-tests

11before_script:

13before_script:

CHANGELOG+7−3

@@ -1,3 +1,7 @@

1+New in 0.9.13:

2+--------------

3+* IDE support for retrieving structured information about metavariables

4+

1New in 0.9.12:

5New in 0.9.12:

2--------------

6--------------

3

7

@@ -5,7 +9,7 @@ New in 0.9.12:

5 type inference.

9 type inference.

6* New 'Lazy' type, replacing laziness annotations.

10* New 'Lazy' type, replacing laziness annotations.

7* JavaScript and Node codegen now understand the %include directive.

11* JavaScript and Node codegen now understand the %include directive.

8−* Concept up 'null' is now understood in the JavaScript and Node codegen.

12+* Concept of 'null' is now understood in the JavaScript and Node codegen.

9* Lots of performance patches for generated JavaScript.

13* Lots of performance patches for generated JavaScript.

10* New commands :eval (:e) and :type (:t) in the prover, which either normalise

14* New commands :eval (:e) and :type (:t) in the prover, which either normalise

11 or show the type of expressions.

15 or show the type of expressions.

@@ -17,8 +21,8 @@ New in 0.9.12:

17 ||| @ n the first number (examined by the function)

21 ||| @ n the first number (examined by the function)

18 ||| @ m the second number (not examined)

22 ||| @ m the second number (not examined)

19 plus (n, m : Nat) -> Nat

23 plus (n, m : Nat) -> Nat

20−* Allow the auto-solve behavior in the prover to be disabled, for easier debugging

24+* Allow the auto-solve behaviour in the prover to be disabled, for easier

21− of proof automation. Use ":set autosolve" and ":unset autosolve".

25+ debugging of proof automation. Use ":set autosolve" and ":unset autosolve".

22* Updated 'effects' library

26* Updated 'effects' library

23* New :apropos command at REPL to search documentation, names, and types

27* New :apropos command at REPL to search documentation, names, and types

24* Unification errors are now slightly more informative

28* Unification errors are now slightly more informative

README+1−1

@@ -1,4 +1,4 @@

1−Idris (http://idris-lang.org/) is an experimental functional programming

1+Idris (http://idris-lang.org/) is a general-purpose functional programming

2language with dependent types.

3

4To configure, edit config.mk. The default values should work for most people.

examples/binary.idrdeleted−62

@@ -1,62 +0,0 @@

1−module Main

2−

3−data Binary : Nat -> Type where

4− bEnd : Binary Z

5− bO : Binary n -> Binary (n + n)

6− bI : Binary n -> Binary (S (n + n))

7−

8−instance Show (Binary n) where

9− show (bO x) = show x ++ "0"

10− show (bI x) = show x ++ "1"

11− show bEnd = ""

12−

13−data Parity : Nat -> Type where

14− even : Parity (n + n)

15− odd : Parity (S (n + n))

16−

17−parity : (n:Nat) -> Parity n

18−parity Z = even {n=Z}

19−parity (S Z) = odd {n=Z}

20−parity (S (S k)) with (parity k)

21− parity (S (S (j + j))) | even ?= even {n=S j}

22− parity (S (S (S (j + j)))) | odd ?= odd {n=S j}

23−

24−natToBin : (n:Nat) -> Binary n

25−natToBin Z = bEnd

26−natToBin (S k) with (parity k)

27− natToBin (S (j + j)) | even = bI (natToBin j)

28− natToBin (S (S (j + j))) | odd ?= bO (natToBin (S j))

29−

30−intToNat : Int -> Nat

31−intToNat 0 = Z

32−intToNat x = if (x>0) then (S (intToNat (x-1))) else Z

33−

34−main : IO ()

35−main = do putStr "Enter a number: "

36− x <- getLine

37− print (natToBin (fromInteger (cast x)))

38−

39−---------- Proofs ----------

40−

41−parity_lemma_1 = proof {

42− intros;

43− rewrite sym (plusSuccRightSucc j j);

44− trivial;

45−}

46−

47−natToBin_lemma_1 = proof {

48− intro;

49− intro;

50− rewrite sym (plusSuccRightSucc j j);

51− trivial;

52−}

53−

54−parity_lemma_2 = proof {

55− intro;

56− intro;

57− rewrite sym (plusSuccRightSucc j j);

58− trivial;

59−}

60−

61−

62−

examples/bmain.idrdeleted−8

@@ -1,8 +0,0 @@

1−module Main

2−

3−import btree

4−

5−main : IO ()

6−main = do let t = toTree [1,8,2,7,9,3]

7− print (btree.toList t)

8−

examples/btree.idrdeleted−18

@@ -1,18 +0,0 @@

1−module btree

2−

3−data BTree a = Leaf

4− | Node (BTree a) a (BTree a)

5−

6−insert : Ord a => a -> BTree a -> BTree a

7−insert x Leaf = Node Leaf x Leaf

8−insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)

9− else (Node l v (insert x r))

10−

11−toList : BTree a -> List a

12−toList Leaf = []

13−toList (Node l v r) = btree.toList l ++ (v :: btree.toList r)

14−

15−toTree : Ord a => List a -> BTree a

16−toTree [] = Leaf

17−toTree (x :: xs) = insert x (toTree xs)

18−

examples/classes.idrdeleted−10

@@ -1,10 +0,0 @@

1−m_add : Maybe Int -> Maybe Int -> Maybe Int

2−m_add x y = do x' <- x -- Extract value from x

3− y' <- y -- Extract value from y

4− return (x' + y') -- Add them

5−

6−m_add' : Maybe Int -> Maybe Int -> Maybe Int

7−m_add' x y = [ x' + y' | x' <- x, y' <- y ]

8−

9−sortAndShow : (Ord a, Show a) => List a -> String

10−sortAndShow xs = show (sort xs)

examples/foo.idrdeleted−10

@@ -1,10 +0,0 @@

1−module foo

2−

3−namespace x

4− test : Int -> Int

5− test x = x * 2

6−

7−namespace y

8− test : String -> String

9− test x = x ++ x

10−

examples/hello.idrdeleted−5

@@ -1,5 +0,0 @@

1−module Main

2−

3−main : IO ()

4−main = putStrLn "Hello world"

5−

examples/idiom.idrdeleted−38

@@ -1,38 +0,0 @@

1−module idiom

2−

3−data Expr = Var String

4− | Val Int

5− | Add Expr Expr

6−

7−data Eval : Type -> Type where

8− MkEval : (List (String, Int) -> Maybe a) -> Eval a

9−

10−fetch : String -> Eval Int

11−fetch x = MkEval (\e => fetchVal e) where

12− fetchVal : List (String, Int) -> Maybe Int

13− fetchVal [] = Nothing

14− fetchVal ((v, val) :: xs) = if (x == v) then (Just val) else (fetchVal xs)

15−

16−instance Functor Eval where

17− map f (MkEval g) = MkEval (\e => map f (g e))

18−

19−instance Applicative Eval where

20− pure x = MkEval (\e => Just x)

21−

22− (<$>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where

23− app : Maybe (a -> b) -> Maybe a -> Maybe b

24− app (Just fx) (Just gx) = Just (fx gx)

25− app _ _ = Nothing

26−

27−eval : Expr -> Eval Int

28−eval (Var x) = fetch x

29−eval (Val x) = [| x |]

30−eval (Add x y) = [| eval x + eval y |]

31−

32−runEval : List (String, Int) -> Expr -> Maybe Int

33−runEval env e = case eval e of

34− MkEval envFn => envFn env

35−

36−m_add' : Maybe Int -> Maybe Int -> Maybe Int

37−m_add' x y = [| x + y |]

38−

examples/interp.idrdeleted−71

@@ -1,71 +0,0 @@

1−module Main

2−

3−data Ty = TyInt | TyBool| TyFun Ty Ty

4−

5−interpTy : Ty -> Type

6−interpTy TyInt = Int

7−interpTy TyBool = Bool

8−interpTy (TyFun s t) = interpTy s -> interpTy t

9−

10−using (G : Vect n Ty)

11−

12− data Env : Vect n Ty -> Type where

13− Nil : Env Nil

14− (::) : interpTy a -> Env G -> Env (a :: G)

15−

16− data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where

17− stop : HasType fZ (t :: G) t

18− pop : HasType k G t -> HasType (fS k) (u :: G) t

19−

20− lookup : HasType i G t -> Env G -> interpTy t

21− lookup stop (x :: xs) = x

22− lookup (pop k) (x :: xs) = lookup k xs

23−

24− data Expr : Vect n Ty -> Ty -> Type where

25− Var : HasType i G t -> Expr G t

26− Val : (x : Int) -> Expr G TyInt

27− Lam : Expr (a :: G) t -> Expr G (TyFun a t)

28− App : Expr G (TyFun a t) -> Expr G a -> Expr G t

29− Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->

30− Expr G c

31− If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a

32−

33− interp : Env G -> {static} Expr G t -> interpTy t

34− interp env (Var i) = lookup i env

35− interp env (Val x) = x

36− interp env (Lam sc) = \x => interp (x :: env) sc

37− interp env (App f s) = interp env f (interp env s)

38− interp env (Op op x y) = op (interp env x) (interp env y)

39− interp env (If x t e) = if interp env x then interp env t

40− else interp env e

41−

42− eId : Expr G (TyFun TyInt TyInt)

43− eId = Lam (Var stop)

44−

45− eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt))

46− eAdd = Lam (Lam (Op (+) (Var stop) (Var (pop stop))))

47−

48− eEq : Expr G (TyFun TyInt (TyFun TyInt TyBool))

49− eEq = Lam (Lam (Op (==) (Var stop) (Var (pop stop))))

50−

51− eDouble : Expr G (TyFun TyInt TyInt)

52− eDouble = Lam (App (App eAdd (Var stop)) (Var stop))

53−

54− app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t

55− app = \f, a => App f a

56−

57− fact : Expr G (TyFun TyInt TyInt)

58− fact = Lam (If (Op (==) (Var stop) (Val 0))

59− (Val 1) (Op (*) (app fact (Op (-) (Var stop) (Val 1))) (Var stop)))

60−

61−testFac : Int

62−testFac = interp [] fact 4

63−

64−unitTestFac : so (interp [] fact 4 == 24)

65−unitTestFac = oh

66−

67−main : IO ()

68−main = do putStr "Enter a number: "

69− x <- getLine

70− print (interp [] fact (cast x))

71−

examples/letbind.idrdeleted−16

@@ -1,16 +0,0 @@

1−module letbind

2−

3−mirror : List a -> List a

4−mirror xs = let xs' = reverse xs in

5− xs ++ xs'

6−

7−data Person = MkPerson String Int

8−

9−showPerson : Person -> String

10−showPerson p = let MkPerson name age = p in

11− name ++ " is " ++ show age ++ " years old"

12−

13−splitAt : Char -> String -> (String, String)

14−splitAt c x = case break (== c) x of

15− (x, y) => (x, strTail y)

16−

examples/prims.idrdeleted−14

@@ -1,14 +0,0 @@

1−module prims

2−

3−x : Int

4−x = 42

5−

6−foo : String

7−foo = "Sausage machine"

8−

9−bar : Char

10−bar = 'Z'

11−

12−quux : Bool

13−quux = False

14−

examples/theorems.idrdeleted−57

@@ -1,57 +0,0 @@

1−

2−fiveIsFive : 5 = 5

3−fiveIsFive = refl

4−

5−twoPlusTwo : 2 + 2 = 4

6−twoPlusTwo = refl

7−

8−total disjoint : (n : Nat) -> Z = S n -> _|_

9−disjoint n p = replace {P = disjointTy} p ()

10− where

11− disjointTy : Nat -> Type

12− disjointTy Z = ()

13− disjointTy (S k) = _|_

14−

15−total acyclic : (n : Nat) -> n = S n -> _|_

16−acyclic Z p = disjoint _ p

17−acyclic (S k) p = acyclic k (succInjective _ _ p)

18−

19−empty1 : _|_

20−empty1 = hd [] where

21− hd : List a -> a

22− hd (x :: xs) = x

23−

24−empty2 : _|_

25−empty2 = empty2

26−

27−plusReduces : (n:Nat) -> plus Z n = n

28−plusReduces n = refl

29−

30−plusReducesZ : (n:Nat) -> n = plus n Z

31−plusReducesZ Z = refl

32−plusReducesZ (S k) = cong (plusReducesZ k)

33−

34−plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)

35−plusReducesS Z m = refl

36−plusReducesS (S k) m = cong (plusReducesS k m)

37−

38−plusReducesZ' : (n:Nat) -> n = plus n Z

39−plusReducesZ' Z = ?plusredZ_Z

40−plusReducesZ' (S k) = let ih = plusReducesZ' k in

41− ?plusredZ_S

42−

43−

44−---------- Proofs ----------

45−

46−plusredZ_S = proof {

47− intro;

48− intro;

49− rewrite ih;

50− trivial;

51−}

52−

53−plusredZ_Z = proof {

54− compute;

55− trivial;

56−}

57−

examples/universe.idrdeleted−7

@@ -1,7 +0,0 @@

1−myid : (a : Type) -> a -> a

2−myid _ x = x

3−

4−idid : (a : Type) -> a -> a

5−idid = myid _ myid

6−

7−

examples/usefultypes.idrdeleted−20

@@ -1,20 +0,0 @@

1−

2−intVec : Vect 5 Int

3−intVec = [1, 2, 3, 4, 5]

4−

5−double : Int -> Int

6−double x = x * 2

7−

8−vec : (n ** Vect n Int)

9−vec = (_ ** [3, 4])

10−

11−list_lookup : Nat -> List a -> Maybe a

12−list_lookup _ Nil = Nothing

13−list_lookup Z (x :: xs) = Just x

14−list_lookup (S k) (x :: xs) = list_lookup k xs

15−

16−lookup_default : Nat -> List a -> a -> a

17−lookup_default i xs def = case list_lookup i xs of

18− Nothing => def

19− Just x => x

20−

examples/vbroken.idrdeleted−5

@@ -1,5 +0,0 @@

1−vapp : Vect n a -> Vect m a -> Vect (n + m) a

2−vapp Nil ys = ys

3−vapp (x :: xs) ys = x :: vapp xs xs -- BROKEN

4−

5−

examples/views.idrdeleted−37

@@ -1,37 +0,0 @@

1−module views

2−

3−data Parity : Nat -> Type where

4− even : Parity (n + n)

5− odd : Parity (S (n + n))

6−

7−parity : (n:Nat) -> Parity n

8−parity Z = even {n=Z}

9−parity (S Z) = odd {n=Z}

10−parity (S (S k)) with (parity k)

11− parity (S (S (j + j))) | even ?= even {n=S j}

12− parity (S (S (S (j + j)))) | odd ?= odd {n=S j}

13−

14−natToBin : Nat -> List Bool

15−natToBin Z = Nil

16−natToBin k with (parity k)

17− natToBin (j + j) | even = False :: natToBin j

18− natToBin (S (j + j)) | odd = True :: natToBin j

19−

20−

21−---------- Proofs ----------

22−

23−views.parity_lemma_2 = proof {

24− intro;

25− intro;

26− rewrite sym (plusSuccRightSucc j j);

27− trivial;

28−}

29−

30−views.parity_lemma_1 = proof {

31− intro;

32− intro;

33− rewrite sym (plusSuccRightSucc j j);

34− trivial;

35−}

36−

37−

examples/wheres.idrdeleted−14

@@ -1,14 +0,0 @@

1−module wheres

2−

3−even : Nat -> Bool

4−even Z = True

5−even (S k) = odd k where

6− odd Z = False

7− odd (S k) = even k

8−

9−test : List Nat

10−test = [c (S 1), c Z, d (S Z)]

11− where c x = 42 + x

12− d y = c (y + 1 + z y)

13− where z w = y + w

14−

idris.cabal+2−2

@@ -1,5 +1,5 @@

1Name: idris

2−Version: 0.9.11.2

2+Version: 0.9.12

3License: BSD3

4License-file: LICENSE

5Author: Edwin Brady

@@ -469,6 +469,7 @@ Library

469 , Idris.Docstrings

470 , Idris.ElabDecls

471 , Idris.ElabTerm

472+ , Idris.Erasure

472 , Idris.Error

473 , Idris.Error

473 , Idris.ErrReverse

474 , Idris.ErrReverse

474 , Idris.Help

475 , Idris.Help

@@ -492,7 +493,6 @@ Library

492 , Idris.REPLParser

493 , Idris.REPLParser

493 , Idris.Transforms

494 , Idris.Transforms

494 , Idris.Unlit

495 , Idris.Unlit

495− , Idris.UnusedArgs

496

497 , IRTS.BCImp

498 , IRTS.Bytecode

libs/Makefile−3

@@ -2,7 +2,6 @@ build:

2 $(MAKE) -C prelude build

3 $(MAKE) -C base build

4 $(MAKE) -C effects build

5− $(MAKE) -C oldeffects build

6 $(MAKE) -C javascript build

5 $(MAKE) -C javascript build

7

6

8

7

@@ -10,14 +9,12 @@ install:

10 $(MAKE) -C prelude install

9 $(MAKE) -C prelude install

11 $(MAKE) -C base install

10 $(MAKE) -C base install

12 $(MAKE) -C effects install

11 $(MAKE) -C effects install

13− $(MAKE) -C oldeffects install

14 $(MAKE) -C javascript install

12 $(MAKE) -C javascript install

15

13

16clean:

14clean:

17 $(MAKE) -C prelude clean

15 $(MAKE) -C prelude clean

18 $(MAKE) -C base clean

16 $(MAKE) -C base clean

19 $(MAKE) -C effects clean

17 $(MAKE) -C effects clean

20− $(MAKE) -C oldeffects clean

21 $(MAKE) -C javascript clean

18 $(MAKE) -C javascript clean

22

19

23.PHONY: build install clean

20.PHONY: build install clean

libs/base/Control/Arrow.idr+1−2

@@ -1,4 +1,4 @@

1−module Category.Arrow

1+module Control.Arrow

2

3import Data.Morphisms

4import Control.Category

@@ -37,4 +37,3 @@ instance Monad m => Arrow (Kleislimorphism m) where

37 (Kleisli f) &&& (Kleisli g) = Kleisli $ \a => do x <- f a

38 y <- g a

39 return (x, y)

40−

libs/base/Control/Catchable.idr+1−1

@@ -1,4 +1,4 @@

1−module Prelude.Catchable

1+module Control.Catchable

2

3import Control.IOExcept

4

libs/effects/Effects.idr+2

@@ -96,6 +96,8 @@ rebuildEnv [] SubNil env = env

96rebuildEnv (x :: xs) (Keep rest) (y :: env) = x :: rebuildEnv xs rest env

97rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env

98rebuildEnv (x :: xs) SubNil [] = x :: xs

99+rebuildEnv [] (Keep x) (x :: xs) = []

100+

99

101

100-- -------------------------------------------------- [ The Effect EDSL itself ]

102-- -------------------------------------------------- [ The Effect EDSL itself ]

101-- some proof automation

103-- some proof automation

libs/prelude/Decidable/Equality.idr+11−1

@@ -174,13 +174,23 @@ total

174vectInjective2 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> xs = ys

175vectInjective2 {x=x} {y=x} {xs=xs} {ys=xs} refl = refl

176

177+instance DecEq a => DecEq (Vect n a) where

178+ decEq [] [] = Yes refl

179+ decEq (x :: xs) (y :: ys) with (decEq x y)

180+ decEq (x :: xs) (x :: ys) | Yes refl with (decEq xs ys)

181+ decEq (x :: xs) (x :: xs) | Yes refl | Yes refl = Yes refl

182+ decEq (x :: xs) (x :: ys) | Yes refl | No neq = No (neq . vectInjective2)

183+ decEq (x :: xs) (y :: ys) | No neq = No (neq . vectInjective1)

184+

185+{- The following definition is elaborated in a wrong case-tree. Examination pending.

186+

177instance DecEq a => DecEq (Vect n a) where

187instance DecEq a => DecEq (Vect n a) where

178 decEq [] [] = Yes refl

188 decEq [] [] = Yes refl

179 decEq (x :: xs) (y :: ys) with (decEq x y, decEq xs ys)

189 decEq (x :: xs) (y :: ys) with (decEq x y, decEq xs ys)

180 decEq (x :: xs) (x :: xs) | (Yes refl, Yes refl) = Yes refl

190 decEq (x :: xs) (x :: xs) | (Yes refl, Yes refl) = Yes refl

181 decEq (x :: xs) (y :: ys) | (_, No nEqTl) = No (\p => nEqTl (vectInjective2 p))

191 decEq (x :: xs) (y :: ys) | (_, No nEqTl) = No (\p => nEqTl (vectInjective2 p))

182 decEq (x :: xs) (y :: ys) | (No nEqHd, _) = No (\p => nEqHd (vectInjective1 p))

192 decEq (x :: xs) (y :: ys) | (No nEqHd, _) = No (\p => nEqHd (vectInjective1 p))

183−

193+-}

184

194

185-- For the primitives, we have to cheat because we don't have access to their

195-- For the primitives, we have to cheat because we don't have access to their

186-- internal implementations.

196-- internal implementations.

libs/prelude/IO.idr+3−6

@@ -132,16 +132,13 @@ io_return : a -> IO a

132io_return x = MkIO (\w => prim_io_return x)

133

134liftPrimIO : (World -> PrimIO a) -> IO a

135−liftPrimIO f = MkIO (\w => prim_io_bind (f w)

135+liftPrimIO = MkIO

136− (\x => prim_io_return x))

137

136

138run__IO : IO () -> PrimIO ()

137run__IO : IO () -> PrimIO ()

139−run__IO (MkIO f) = prim_io_bind (f TheWorld)

138+run__IO (MkIO f) = f TheWorld

140− (\ b => prim_io_return b)

141

139

142run__provider : IO a -> PrimIO a

140run__provider : IO a -> PrimIO a

143−run__provider (MkIO f) = prim_io_bind (f TheWorld)

141+run__provider (MkIO f) = f TheWorld

144− (\ b => prim_io_return b)

145

142

146-- io_bind v (\v' => io_return v')

143-- io_bind v (\v' => io_return v')

147

144

main/Main.hs+1

@@ -113,6 +113,7 @@ usagemsg = usagemsghdr ++ "\n" ++

113 "\t --check Undocumented\n" ++

114 "\t --total Require functions to be total by default\n" ++

115 "\t --partial Undocumented\n" ++

116+ "\t --warnreach Warn about reachable but inaccessible arguments\n" ++

116 "\t --warnpartial Warn about undeclared partial functions.\n" ++

117 "\t --warnpartial Warn about undeclared partial functions.\n" ++

117 "\t --warn Undocumented\n" ++

118 "\t --warn Undocumented\n" ++

118 "\t --typecase Undocumented\n" ++

119 "\t --typecase Undocumented\n" ++

src/IRTS/CodegenJavaScript.hs+6−1

@@ -1154,7 +1154,7 @@ unfoldLookupTable input =

1154

1155removeInstanceChecks :: JS -> JS

1156removeInstanceChecks (JSCond conds) =

1157− JSCond $ eliminateDeadBranches $ map (

1157+ removeNoopConds $ JSCond $ eliminateDeadBranches $ map (

1158 removeHelper *** removeInstanceChecks

1159 ) conds

1160 where

@@ -1169,6 +1169,11 @@ removeInstanceChecks (JSCond conds) =

1169 eliminateDeadBranches (x:xs) = x : eliminateDeadBranches xs

1170 eliminateDeadBranches [] = []

1171

1172+

1173+ removeNoopConds :: JS -> JS

1174+ removeNoopConds (JSCond [(JSNoop, js)]) = js

1175+ removeNoopConds js = js

1176+

1172removeInstanceChecks js = transformJS removeInstanceChecks js

1177removeInstanceChecks js = transformJS removeInstanceChecks js

1173

1178

1174

1179

src/IRTS/Compiler.hs+425−299

@@ -18,15 +18,25 @@ import Util.LLVMStubs

18import IRTS.Inliner

19

20import Idris.AbsSyntax

21−import Idris.UnusedArgs

21+import Idris.AbsSyntaxTree

22+import Idris.Erasure

22import Idris.Error

23import Idris.Error

23

24

25+import Debug.Trace

26+

24import Idris.Core.TT

27import Idris.Core.TT

25import Idris.Core.Evaluate

28import Idris.Core.Evaluate

26import Idris.Core.CaseTree

29import Idris.Core.CaseTree

27

30

31+import Control.Applicative

28import Control.Monad.State

32import Control.Monad.State

33+import Data.Maybe

29import Data.List

34import Data.List

35+import Data.Ord

36+import Data.IntSet (IntSet)

37+import qualified Data.IntSet as IS

38+import qualified Data.Map as M

39+import qualified Data.Set as S

30import System.Process

40import System.Process

31import System.IO

41import System.IO

32import System.Directory

42import System.Directory

@@ -37,18 +47,16 @@ import Paths_idris

37

47

38compile :: Codegen -> FilePath -> Term -> Idris ()

48compile :: Codegen -> FilePath -> Term -> Idris ()

39compile codegen f tm

49compile codegen f tm

40− = do checkMVs

50+ = do checkMVs -- check for undefined metavariables

41− let tmnames = namesUsed (STerm tm)

51+ reachableNames <- performUsageAnalysis

42− usedIn <- mapM (allNames []) tmnames

43− let used = [sUN "prim__subBigInt", sUN "prim__addBigInt"] : usedIn

44− defsIn <- mkDecls tm (concat used)

45− findUnusedArgs (concat used)

46 maindef <- irMain tm

52 maindef <- irMain tm

53+ iLOG $ "MAIN: " ++ show maindef

47 objs <- getObjectFiles codegen

54 objs <- getObjectFiles codegen

48 libs <- getLibs codegen

55 libs <- getLibs codegen

49 flags <- getFlags codegen

56 flags <- getFlags codegen

50 hdrs <- getHdrs codegen

57 hdrs <- getHdrs codegen

51 impdirs <- allImportDirs

58 impdirs <- allImportDirs

59+ defsIn <- mkDecls tm reachableNames

52 let defs = defsIn ++ [(sMN 0 "runMain", maindef)]

60 let defs = defsIn ++ [(sMN 0 "runMain", maindef)]

53 -- iputStrLn $ showSep "\n" (map show defs)

61 -- iputStrLn $ showSep "\n" (map show defs)

54 let (nexttag, tagged) = addTags 65536 (liftAll defs)

62 let (nexttag, tagged) = addTags 65536 (liftAll defs)

@@ -98,31 +106,48 @@ compile codegen f tm

98 if ex then return f else return h

106 if ex then return f else return h

99

107

100irMain :: TT Name -> Idris LDecl

108irMain :: TT Name -> Idris LDecl

101−irMain tm = do i <- ir tm

109+irMain tm = do

110+ i <- irTerm M.empty [] tm

102− return $ LFun [] (sMN 0 "runMain") [] (LForce i)

111+ return $ LFun [] (sMN 0 "runMain") [] (LForce i)

103

112

104mkDecls :: Term -> [Name] -> Idris [(Name, LDecl)]

113mkDecls :: Term -> [Name] -> Idris [(Name, LDecl)]

105mkDecls t used

114mkDecls t used

106 = do i <- getIState

115 = do i <- getIState

107− let ds = filter (\ (n, d) -> n `elem` used || isCon d) $ ctxtAlist (tt_ctxt i)

116+ let ds = filter (\(n, d) -> n `elem` used || isCon d) $ ctxtAlist (tt_ctxt i)

108− mapM traceUnused used

109 decls <- mapM build ds

117 decls <- mapM build ds

110 return decls

118 return decls

111

119

112showCaseTrees :: [(Name, LDecl)] -> String

120showCaseTrees :: [(Name, LDecl)] -> String

113−showCaseTrees ds = showSep "\n\n" (map showCT ds)

121+showCaseTrees = showSep "\n\n" . map showCT . sortBy (comparing defnRank)

114 where

122 where

115 showCT (n, LFun _ f args lexp)

123 showCT (n, LFun _ f args lexp)

116− = show n ++ " " ++ showSep " " (map show args) ++ " =\n\t "

124+ = show n ++ " " ++ showSep " " (map show args) ++ " =\n\t"

117 ++ show lexp

125 ++ show lexp

118 showCT (n, LConstructor c t a) = "data " ++ show n ++ " " ++ show a

126 showCT (n, LConstructor c t a) = "data " ++ show n ++ " " ++ show a

119

127

128+ defnRank :: (Name, LDecl) -> String

129+ defnRank (n, LFun _ _ _ _) = "1" ++ nameRank n

130+ defnRank (n, LConstructor _ _ _) = "2" ++ nameRank n

131+

132+ nameRank :: Name -> String

133+ nameRank (UN s) = "1" ++ show s

134+ nameRank (MN i s) = "2" ++ show s ++ show i

135+ nameRank (NS n ns) = "3" ++ concatMap show (reverse ns) ++ nameRank n

136+ nameRank (SN sn) = "4" ++ snRank sn

137+ nameRank n = "5" ++ show n

138+

139+ snRank :: SpecialName -> String

140+ snRank (WhereN i n n') = "1" ++ nameRank n' ++ nameRank n ++ show i

141+ snRank (InstanceN n args) = "2" ++ nameRank n ++ concatMap show args

142+ snRank (ParentN n s) = "3" ++ nameRank n ++ show s

143+ snRank (MethodN n) = "4" ++ nameRank n

144+ snRank (CaseN n) = "5" ++ nameRank n

145+ snRank (ElimN n) = "6" ++ nameRank n

146+ snRank (InstanceCtorN n) = "7" ++ nameRank n

147+

120isCon (TyDecl _ _) = True

148isCon (TyDecl _ _) = True

121isCon _ = False

149isCon _ = False

122

150

123−class ToIR a where

124− ir :: a -> Idris LExp

125−

126build :: (Name, Def) -> Idris (Name, LDecl)

151build :: (Name, Def) -> Idris (Name, LDecl)

127build (n, d)

152build (n, d)

128 = do i <- getIState

153 = do i <- getIState

@@ -135,295 +160,396 @@ build (n, d)

135 logLvl 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def

160 logLvl 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def

136 return (n, def)

161 return (n, def)

137

162

138−getPrim :: IState -> Name -> [LExp] -> Maybe LExp

139−getPrim i n args = case lookup n (idris_scprims i) of

140− Just (ar, op) ->

141− if (ar == length args)

142− then return (LOp op args)

143− else Nothing

144− _ -> Nothing

145−

146declArgs args inl n (LLam xs x) = declArgs (args ++ xs) inl n x

163declArgs args inl n (LLam xs x) = declArgs (args ++ xs) inl n x

147declArgs args inl n x = LFun (if inl then [Inline] else []) n args x

164declArgs args inl n x = LFun (if inl then [Inline] else []) n args x

148

165

149−mkLDecl n (Function tm _) = do e <- ir tm

166+mkLDecl n (Function tm _)

150− return (declArgs [] True n e)

167+ = declArgs [] True n <$> irTerm M.empty [] tm

168+

151mkLDecl n (CaseOp ci _ _ _ pats cd)

169mkLDecl n (CaseOp ci _ _ _ pats cd)

152− = let (args, sc) = cases_runtime cd in

153− do e <- ir (args, sc)

154− return (declArgs [] (case_inlinable ci) n e)

170+ = declArgs [] (case_inlinable ci) n <$> irTree args sc

171+ where

172+ (args, sc) = cases_runtime cd

173+

155−mkLDecl n (TyDecl (DCon t a) _) = return $ LConstructor n t a

174+mkLDecl n (TyDecl (DCon tag arity) _) =

175+ LConstructor n tag . erasedArity . lookup n <$> getIState

176+ where

177+ lookup n = lookupCtxtExact n . idris_callgraph

178+ erasedArity = maybe 0 (length . usedpos)

179+

156mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a

180mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a

157mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run

181mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run

158

182

159−instance ToIR (TT Name) where

183+data VarInfo = VI

160− ir tm = ir' [] tm where

184+ { viMethod :: Maybe Name

185+ }

186+ deriving Show

187+

188+type Vars = M.Map Name VarInfo

189+

190+irTerm :: Vars -> [Name] -> Term -> Idris LExp

161− ir' env tm@(App f a)

191+irTerm vs env tm@(App f a) = case unApply tm of

162− | (P _ (UN m) _, args) <- unApply tm,

192+ (P _ (UN m) _, args)

163− m == txt "mkForeignPrim"

193+ | m == txt "mkForeignPrim"

164− = doForeign env args

194+ -> doForeign vs env args

195+

165− | (P _ (UN u) _, [_, arg]) <- unApply tm,

196+ (P _ (UN u) _, [_, arg])

166− u == txt "unsafePerformPrimIO"

197+ | u == txt "unsafePerformPrimIO"

167− = ir' env arg

198+ -> irTerm vs env arg

199+

168− -- TMP HACK - until we get inlining.

200+ -- TMP HACK - until we get inlining.

169− | (P _ (UN r) _, [_, _, _, _, _, arg]) <- unApply tm,

201+ (P _ (UN r) _, [_, _, _, _, _, arg])

170− r == txt "replace"

202+ | r == txt "replace"

171− = ir' env arg

203+ -> irTerm vs env arg

204+

172− -- Laziness, the old way

205+ -- Laziness, the old way

173− | (P _ (UN l) _, [_, arg]) <- unApply tm,

206+ (P _ (UN l) _, [_, arg])

174− l == txt "lazy"

207+ | l == txt "lazy"

175− = do arg' <- ir' env arg

176− error "lazy has crept in somehow"

208+ -> error "lazy has crept in somehow"

177−-- return $ LLazyExp arg'

209+

178− | (P _ (UN l) _, [_, arg]) <- unApply tm,

210+ (P _ (UN l) _, [_, arg])

179− l == txt "force"

211+ | l == txt "force"

180− = do arg' <- ir' env arg

212+ -> LForce <$> irTerm vs env arg

181− return $ LForce arg'

213+

182− -- Laziness, the new way

214+ -- Laziness, the new way

183− | (P _ (UN l) _, [arg]) <- unApply tm,

215+ (P _ (UN l) _, [_, _, arg])

184− l == txt "Delay"

216+ | l == txt "Delay"

185− = do arg' <- ir' env arg

217+ -> LLazyExp <$> irTerm vs env arg

186− return $ LLazyExp arg'

218+

187− | (P _ (UN l) _, [_, _, arg]) <- unApply tm,

219+ (P _ (UN l) _, [_, _, arg])

188− l == txt "Force"

220+ | l == txt "Force"

189− = do arg' <- ir' env arg

221+ -> LForce <$> irTerm vs env arg

190− return $ LForce arg'

222+

191− | (P _ (UN a) _, [_, _, arg]) <- unApply tm,

223+ (P _ (UN a) _, [_, _, arg])

192− a == txt "assert_smaller"

224+ | a == txt "assert_smaller"

193− = ir' env arg

225+ -> irTerm vs env arg

226+

194− | (P _ (UN a) _, [_, arg]) <- unApply tm,

227+ (P _ (UN a) _, [_, arg])

195− a == txt "assert_total"

228+ | a == txt "assert_total"

196− = ir' env arg

229+ -> irTerm vs env arg

230+

197− | (P _ (UN p) _, [_, arg]) <- unApply tm,

231+ (P _ (UN p) _, [_, arg])

198− p == txt "par"

232+ | p == txt "par"

199− = do arg' <- ir' env arg

233+ -> do arg' <- irTerm vs env arg

200− return $ LOp LPar [LLazyExp arg']

234+ return $ LOp LPar [LLazyExp arg']

235+

201− | (P _ (UN pf) _, [arg]) <- unApply tm,

236+ (P _ (UN pf) _, [arg])

202− pf == txt "prim_fork"

237+ | pf == txt "prim_fork"

203− = do arg' <- ir' env arg

238+ -> do arg' <- irTerm vs env arg

204− return $ LOp LFork [LLazyExp arg']

239+ return $ LOp LFork [LLazyExp arg']

240+

205− | (P _ (UN m) _, [_,size,t]) <- unApply tm,

241+ (P _ (UN m) _, [_,size,t])

206− m == txt "malloc"

242+ | m == txt "malloc"

207− = do size' <- ir' env size

208− t' <- ir' env t

243+ -> irTerm vs env t

209− return t' -- TODO $ malloc_ size' t'

244+

210− | (P _ (UN tm) _, [_,t]) <- unApply tm,

245+ (P _ (UN tm) _, [_,t])

211− tm == txt "trace_malloc"

246+ | tm == txt "trace_malloc"

212− = do t' <- ir' env t

247+ -> irTerm vs env t -- TODO

213− return t' -- TODO

248+

214− -- This case is here until we get more general inlining. It's just

249+ -- This case is here until we get more general inlining. It's just

215− -- a really common case, and the laziness hurts...

250+ -- a really common case, and the laziness hurts...

216− | (P _ (NS (UN be) [b,p]) _, [_,x,(App (P _ (UN d) _) t),

251+ (P _ (NS (UN be) [b,p]) _, [_,x,(App (P _ (UN d) _) t),

217− (App (P _ (UN d') _) e)]) <- unApply tm,

252+ (App (P _ (UN d') _) e)])

218− be == txt "boolElim" && d == txt "Delay" && d' == txt "Delay"

253+ | be == txt "boolElim"

254+ , d == txt "Delay"

255+ , d' == txt "Delay"

256+ -> do

219− = do x' <- ir' env x

257+ x' <- irTerm vs env x

220− t' <- ir' env t

258+ t' <- irTerm vs env t

221− e' <- ir' env e

259+ e' <- irTerm vs env e

222− return (LCase x' [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e',

260+ return (LCase x' [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e'

223− LConCase 1 (sNS (sUN "True") ["Bool","Prelude"]) [] t'])

261+ ,LConCase 1 (sNS (sUN "True" ) ["Bool","Prelude"]) [] t'

262+ ])

263+

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

264+ (P (DCon t arity) n _, args) -> do

225− = irCon env t a n args

265+ ist <- getIState

226− | (P (TCon t a) n _, args) <- unApply tm

227− = return LNothing

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

229− = do i <- getIState

230− args' <- mapM (ir' env) args

231− case getPrim i n args' of

232− Just tm -> return tm

233− _ -> do

234− let collapse

235− = case lookupCtxtExact n

236− (idris_optimisation i) of

266+ let detag = maybe False detaggable . lookupCtxtExact n $ idris_optimisation ist

237− Just oi -> collapsible oi

267+ used = maybe [] (map fst . usedpos) . lookupCtxtExact n $ idris_callgraph ist

238− _ -> False

268+ args' = [a | (i,a) <- zip [0..] args, i `elem` used]

239− let unused

269+

240− = case lookupCtxtExact n

270+ when (length args > arity) $

241− (idris_callgraph i) of

271+ ifail ("oversaturated data ctor: " ++ show tm)

242− Just (CGInfo _ _ _ _ unusedpos) ->

272+

243− unusedpos

273+ if length args' == 1 && detag -- detaggable

244− _ -> []

274+ then irTerm vs env (head args') -- newtype

245− if collapse

275+ else irCon vs env (length used) n args'

246− then return LNothing

276+

277+ (P (TCon t a) n _, args) -> return LNothing

278+

279+ (P _ n _, args) -> do

280+ ist <- getIState

281+ case lookup n (idris_scprims ist) of

282+ -- if it's a primitive that is already saturated,

283+ -- compile to the corresponding op here already to save work

284+ Just (arity, op) | length args == arity

285+ -> LOp op <$> mapM (irTerm vs env) args

286+

287+ -- otherwise, just apply the name

288+ _ -> applyName n ist args

289+

290+ -- turn de bruijn vars into regular named references and try again

291+ (V i, args) -> irTerm vs env $ mkApp (P Bound (env !! i) Erased) args

292+

293+ (f, args)

247− else return (LApp False (LV (Glob n))

294+ -> LApp False

248− (mkUnused unused 0 args'))

295+ <$> irTerm vs env f

249− | (f, args) <- unApply tm

296+ <*> mapM (irTerm vs env) args

250− = do f' <- ir' env f

297+

251− args' <- mapM (ir' env) args

298+ where

252− return (LApp False f' args')

299+ applyName :: Name -> IState -> [Term] -> Idris LExp

253− where mkUnused u i [] = []

300+ applyName n ist args =

254− mkUnused u i (x : xs) | i `elem` u = LNothing : mkUnused u (i + 1) xs

301+ LApp False (LV $ Glob n) <$> mapM (irTerm vs env . erase) (zip [0..] args)

302+ where

303+ erase (i, x)

304+ | i >= arity || i `elem` used = x

305+ | otherwise = Erased

306+

307+ arity = case fst4 <$> lookupCtxtExact n (definitions . tt_ctxt $ ist) of

308+ Just (CaseOp ci ty tys def tot cdefs) -> length tys

309+ Just (TyDecl (DCon tag ar) _) -> ar

310+ Just (TyDecl Ref ty) -> length $ getArgTys ty

311+ Just (Operator ty ar op) -> ar

312+ Just def -> error $ "unknown arity: " ++ show (n, def)

313+ Nothing -> 0 -- no definition, probably local name => can't erase anything

314+

315+ -- name for purposes of usage info lookup

316+ uName

317+ | Just n' <- viMethod =<< M.lookup n vs = n'

255− | otherwise = x : mkUnused u (i + 1) xs

318+ | otherwise = n

256−-- ir' env (P _ (NS (UN "Z") ["Nat", "Prelude"]) _)

319+

257−-- = return $ LConst (BI 0)

320+ used = maybe [] (map fst . usedpos) $ lookupCtxtExact uName (idris_callgraph ist)

321+ fst4 (x,_,_,_) = x

322+

258− ir' env (P _ n _) = return $ LV (Glob n)

323+irTerm vs env (P _ n _) = return $ LV (Glob n)

324+irTerm vs env (V i)

259− ir' env (V i) | i >= 0 && i < length env = return $ LV (Glob (env!!i))

325+ | i >= 0 && i < length env = return $ LV (Glob (env!!i))

260− | otherwise = ifail $ "IR fail " ++ show i ++ " " ++ show tm

326+ | otherwise = ifail $ "bad de bruijn index: " ++ show i

327+

261− ir' env (Bind n (Lam _) sc)

328+irTerm vs env (Bind n (Lam _) sc) = LLam [n'] <$> irTerm vs (n':env) sc

329+ where

262− = do let n' = uniqueName n env

330+ n' = uniqueName n env

263− sc' <- ir' (n' : env) sc

331+

264− return $ LLam [n'] sc'

265− ir' env (Bind n (Let _ v) sc)

332+irTerm vs env (Bind n (Let _ v) sc)

266− = do sc' <- ir' (n : env) sc

333+ = LLet n <$> irTerm vs env v <*> irTerm vs (n : env) sc

267− v' <- ir' env v

334+

268− return $ LLet n v' sc'

269− ir' env (Bind _ _ _) = return $ LNothing

335+irTerm vs env (Bind _ _ _) = return $ LNothing

336+

270− ir' env (Proj t i) | i == -1

337+irTerm vs env (Proj t (-1)) = do

271− = do t' <- ir' env t

338+ t' <- irTerm vs env t

272− return $ LOp (LMinus (ATInt ITBig))

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

273− [t', LConst (BI 1)]

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

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

341+

275− return $ LProj t' i

342+irTerm vs env (Proj t i) = LProj <$> irTerm vs env t <*> pure i

276− ir' env (Constant c) = return $ LConst c

343+irTerm vs env (Constant c) = return $ LConst c

277− ir' env (TType _) = return $ LNothing

344+irTerm vs env (TType _) = return $ LNothing

278− ir' env Erased = return $ LNothing

345+irTerm vs env Erased = return $ LNothing

279− ir' env Impossible = return $ LNothing

346+irTerm vs env Impossible = return $ LNothing

280−-- ir' env _ = return $ LError "Impossible"

347+

281−

348+irCon :: Vars -> [Name] -> Int -> Name -> [Term] -> Idris LExp

282− irCon env t arity n args

349+irCon vs env arity n args

283− | length args == arity = buildApp env (LV (Glob n)) args

350+ | length args > arity

284− | otherwise = let extra = satArgs (arity - length args) in

351+ = error $ "oversaturated data constructor: " ++ show (n, args)

285− do sc' <- irCon env t arity n

352+

286− (args ++ map (\n -> P Bound n undefined) extra)

353+ -- saturated

287− return $ LLam extra sc'

354+ | length args == arity

288−

355+ = buildApp (LV (Glob n)) args

289− satArgs n = map (\i -> sMN i "sat") [1..n]

356+

290−

357+ -- undersaturated, wrap in lambdas

358+ | otherwise

359+ = let extraNs = [sMN i "sat" | i <- [length args .. arity-1]]

360+ extraTs = [P Bound n undefined | n <- extraNs]

361+ in LLam extraNs <$> irCon vs env arity n (args ++ extraTs)

362+ where

291− buildApp env e [] = return e

363+ buildApp e [] = return e

292− buildApp env e xs = do xs' <- mapM (ir' env) xs

364+ buildApp e xs = LApp False e <$> mapM (irTerm vs env) xs

293− return $ LApp False e xs'

365+

294−

295− doForeign :: [Name] -> [TT Name] -> Idris LExp

366+doForeign :: Vars -> [Name] -> [TT Name] -> Idris LExp

296− doForeign env (_ : fgn : args)

367+doForeign vs env (_ : fgn : args)

297− | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn

368+ | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn

298− = let maybeTys = getFTypes fgnArgTys

369+ = case getFTypes fgnArgTys of

299− rty = mkIty' ret in

300− case maybeTys of

301− Nothing -> ifail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)

370+ Nothing -> ifail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)

302− Just tys -> do

371+ Just tys -> do

303− args' <- mapM (ir' env) (init args)

372+ args' <- mapM (irTerm vs env) (init args)

304− -- wrap it in a prim__IO

305− -- return $ con_ 0 @@ impossible @@

306− return $ -- LLazyExp $

307− LForeign LANG_C rty fgnName (zip tys args')

373+ return $ LForeign LANG_C (mkIty' ret) fgnName (zip tys args')

374+

308− | otherwise = ifail "Badly formed foreign function call"

375+ | otherwise = ifail "Badly formed foreign function call"

309−

376+ where

310−getFTypes :: TT Name -> Maybe [FType]

377+ getFTypes :: TT Name -> Maybe [FType]

311−getFTypes tm = case unApply tm of

378+ getFTypes tm = case unApply tm of

379+ -- nil : {a : Type} -> List a

312− (nil, []) -> Just []

380+ (nil, [_]) -> Just []

313− (cons, [ty, xs]) ->

381+ -- cons : {a : Type} -> a -> List a -> List a

314− fmap (mkIty' ty :) (getFTypes xs)

382+ (cons, [_, ty, xs]) -> (mkIty' ty :) <$> getFTypes xs

315− _ -> Nothing

383+ _ -> Nothing

316−

384+

317−mkIty' (P _ (UN ty) _) = mkIty (str ty)

385+ mkIty' (P _ (UN ty) _) = mkIty (str ty)

318−mkIty' (App (P _ (UN fi) _) (P _ (UN intTy) _))

386+ mkIty' (App (P _ (UN fi) _) (P _ (UN intTy) _))

387+ | fi == txt "FIntT"

319− | fi == txt "FIntT" = mkIntIty (str intTy)

388+ = mkIntIty (str intTy)

389+

320−mkIty' (App (App (P _ (UN ff) _) _) (App (P _ (UN fa) _) (App (P _ (UN io) _) _)))

390+ mkIty' (App (App (P _ (UN ff) _) _) (App (P _ (UN fa) _) (App (P _ (UN io) _) _)))

321− | ff == txt "FFunction" && fa == txt "FAny" &&

391+ | ff == txt "FFunction"

392+ , fa == txt "FAny"

322− io == txt "IO"

393+ , io == txt "IO"

323 = FFunctionIO

394 = FFunctionIO

324−mkIty' (App (App (P _ (UN ff) _) _) _)

325− | ff == txt "FFunction" = FFunction

326−mkIty' _ = FAny

327−

328−-- would be better if these FInt types were evaluated at compile time

329−-- TODO: add %eval directive for such things

330−

331−mkIty "FFloat" = FArith ATFloat

332−mkIty "FInt" = mkIntIty "ITNative"

333−mkIty "FChar" = mkIntIty "ITChar"

334−mkIty "FByte" = mkIntIty "IT8"

335−mkIty "FShort" = mkIntIty "IT16"

336−mkIty "FLong" = mkIntIty "IT64"

337−mkIty "FBits8" = mkIntIty "IT8"

338−mkIty "FBits16" = mkIntIty "IT16"

339−mkIty "FBits32" = mkIntIty "IT32"

340−mkIty "FBits64" = mkIntIty "IT64"

341−mkIty "FString" = FString

342−mkIty "FPtr" = FPtr

343−mkIty "FManagedPtr" = FManagedPtr

344−mkIty "FUnit" = FUnit

345−mkIty "FFunction" = FFunction

346−mkIty "FFunctionIO" = FFunctionIO

347−mkIty "FBits8x16" = FArith (ATInt (ITVec IT8 16))

348−mkIty "FBits16x8" = FArith (ATInt (ITVec IT16 8))

349−mkIty "FBits32x4" = FArith (ATInt (ITVec IT32 4))

350−mkIty "FBits64x2" = FArith (ATInt (ITVec IT64 2))

351−mkIty x = error $ "Unknown type " ++ x

352−

353−mkIntIty "ITNative" = FArith (ATInt ITNative)

354−mkIntIty "ITChar" = FArith (ATInt ITChar)

355−mkIntIty "IT8" = FArith (ATInt (ITFixed IT8))

356−mkIntIty "IT16" = FArith (ATInt (ITFixed IT16))

357−mkIntIty "IT32" = FArith (ATInt (ITFixed IT32))

358−mkIntIty "IT64" = FArith (ATInt (ITFixed IT64))

359−

360−zname = sNS (sUN "Z") ["Nat","Prelude"]

361−sname = sNS (sUN "S") ["Nat","Prelude"]

362−

363−instance ToIR ([Name], SC) where

364− ir (args, tree) = do logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree

365− tree' <- ir tree

366− return $ LLam args tree'

367−

368−instance ToIR SC where

369− ir t = ir' t where

370−

371− ir' (STerm t) = ir t

372− ir' (UnmatchedCase str) = return $ LError str

373− ir' (ProjCase tm alts) = do tm' <- ir tm

374− alts' <- mapM (mkIRAlt tm') alts

375− return $ LCase tm' alts'

376− ir' (Case n alts) = do alts' <- mapM (mkIRAlt (LV (Glob n))) alts

377− return $ LCase (LV (Glob n)) alts'

378− ir' ImpossibleCase = return LNothing

379−

380− -- special cases for Z and S

381− -- Needs rethink: projections make this fail

382−-- mkIRAlt n (ConCase z _ [] rhs) | z == zname

383−-- = mkIRAlt n (ConstCase (BI 0) rhs)

384−-- mkIRAlt n (ConCase s _ [arg] rhs) | s == sname

385−-- = do n' <- ir n

386−-- rhs' <- ir rhs

387−-- return $ LDefaultCase

388−-- (LLet arg (LOp LBMinus [n', LConst (BI 1)])

389−-- rhs')

390− mkIRAlt _ (ConCase n t args rhs)

391− = do rhs' <- ir rhs

392− return $ LConCase (-1) n args rhs'

393− mkIRAlt _ (ConstCase x rhs)

394− | matchable x

395− = do rhs' <- ir rhs

396− return $ LConstCase x rhs'

397− | matchableTy x

398− = do rhs' <- ir rhs

399− return $ LDefaultCase rhs'

400− mkIRAlt tm (SucCase n rhs)

401− = do rhs' <- ir rhs

402− return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))

403− [tm,

404− LConst (BI 1)]) rhs')

405−-- return $ LSucCase n rhs'

406− mkIRAlt _ (ConstCase c rhs)

407− = ifail $ "Can't match on (" ++ show c ++ ")"

408− mkIRAlt _ (DefaultCase rhs)

409− = do rhs' <- ir rhs

410− return $ LDefaultCase rhs'

411−

412− matchable (I _) = True

413− matchable (BI _) = True

414− matchable (Ch _) = True

415− matchable (Str _) = True

416− matchable _ = False

417−

418− matchableTy (AType (ATInt ITNative)) = True

419− matchableTy (AType (ATInt ITBig)) = True

420− matchableTy (AType (ATInt ITChar)) = True

421− matchableTy StrType = True

422−

423− matchableTy (AType (ATInt (ITFixed IT8))) = True

424− matchableTy (AType (ATInt (ITFixed IT16))) = True

425− matchableTy (AType (ATInt (ITFixed IT32))) = True

426− matchableTy (AType (ATInt (ITFixed IT64))) = True

427−

428− matchableTy _ = False

429

395

396+ mkIty' (App (App (P _ (UN ff) _) _) _)

397+ | ff == txt "FFunction"

398+ = FFunction

399+

400+ mkIty' _ = FAny

401+

402+ -- would be better if these FInt types were evaluated at compile time

403+ -- TODO: add %eval directive for such things

404+

405+ mkIty "FFloat" = FArith ATFloat

406+ mkIty "FInt" = mkIntIty "ITNative"

407+ mkIty "FChar" = mkIntIty "ITChar"

408+ mkIty "FByte" = mkIntIty "IT8"

409+ mkIty "FShort" = mkIntIty "IT16"

410+ mkIty "FLong" = mkIntIty "IT64"

411+ mkIty "FBits8" = mkIntIty "IT8"

412+ mkIty "FBits16" = mkIntIty "IT16"

413+ mkIty "FBits32" = mkIntIty "IT32"

414+ mkIty "FBits64" = mkIntIty "IT64"

415+ mkIty "FString" = FString

416+ mkIty "FPtr" = FPtr

417+ mkIty "FManagedPtr" = FManagedPtr

418+ mkIty "FUnit" = FUnit

419+ mkIty "FFunction" = FFunction

420+ mkIty "FFunctionIO" = FFunctionIO

421+ mkIty "FBits8x16" = FArith (ATInt (ITVec IT8 16))

422+ mkIty "FBits16x8" = FArith (ATInt (ITVec IT16 8))

423+ mkIty "FBits32x4" = FArith (ATInt (ITVec IT32 4))

424+ mkIty "FBits64x2" = FArith (ATInt (ITVec IT64 2))

425+ mkIty x = error $ "Unknown type " ++ x

426+

427+ mkIntIty "ITNative" = FArith (ATInt ITNative)

428+ mkIntIty "ITChar" = FArith (ATInt ITChar)

429+ mkIntIty "IT8" = FArith (ATInt (ITFixed IT8))

430+ mkIntIty "IT16" = FArith (ATInt (ITFixed IT16))

431+ mkIntIty "IT32" = FArith (ATInt (ITFixed IT32))

432+ mkIntIty "IT64" = FArith (ATInt (ITFixed IT64))

433+

434+irTree :: [Name] -> SC -> Idris LExp

435+irTree args tree = do

436+ logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree

437+ LLam args <$> irSC M.empty tree

438+

439+irSC :: Vars -> SC -> Idris LExp

440+irSC vs (STerm t) = irTerm vs [] t

441+irSC vs (UnmatchedCase str) = return $ LError str

442+irSC vs (ProjCase tm alts) = do

443+ tm' <- irTerm vs [] tm

444+ alts' <- mapM (irAlt vs tm') alts

445+ return $ LCase tm' alts'

446+

447+-- Transform matching on Delay to applications of Force.

448+irSC vs (Case n [ConCase (UN delay) i [_, _, n'] sc])

449+ | delay == txt "Delay"

450+ = irSC vs $ mkForce n n' sc

451+

452+-- There are two transformations in this case:

453+--

454+-- 1. Newtype-case elimination:

455+-- case {e0} of

456+-- wrap({e1}) -> P({e1}) ==> P({e0})

457+--

458+-- This is important because newtyped constructors are compiled away entirely

459+-- and we need to do that everywhere.

460+--

461+-- 2. Unused-case elimination (only valid for singleton branches):

462+-- case {e0} of ==> P

463+-- C(x,y) -> P[... x,y not used ...]

464+--

465+-- This is important for runtime because sometimes we case on irrelevant data:

466+--

467+-- In the example above, {e0} will most probably have been erased

468+-- so this vain projection would make the resulting program segfault

469+-- because the code generator still emits a PROJECT(...) G-machine instruction.

470+--

471+-- Hence, we check whether the variables are used at all

472+-- and erase the casesplit if they are not.

473+irSC vs (Case n [alt]) = do

474+ replacement <- case alt of

475+ ConCase cn a ns sc -> do

476+ detag <- maybe False detaggable . lookupCtxtExact cn . idris_optimisation <$> getIState

477+ used <- maybe [] (map fst . usedpos) . lookupCtxtExact cn . idris_callgraph <$> getIState

478+ if detag && length used == 1

479+ then return . Just $ substSC (ns !! head used) n sc

480+ else return Nothing

481+ _ -> return Nothing

482+

483+ case replacement of

484+ Just sc -> irSC vs sc

485+ _ -> do

486+ alt' <- irAlt vs (LV (Glob n)) alt

487+ return $ case namesBoundIn alt' `usedIn` subexpr alt' of

488+ [] -> subexpr alt' -- strip the unused top-most case

489+ _ -> LCase (LV (Glob n)) [alt']

490+ where

491+ namesBoundIn :: LAlt -> [Name]

492+ namesBoundIn (LConCase cn i ns sc) = ns

493+ namesBoundIn (LConstCase c sc) = []

494+ namesBoundIn (LDefaultCase sc) = []

495+

496+ subexpr :: LAlt -> LExp

497+ subexpr (LConCase _ _ _ e) = e

498+ subexpr (LConstCase _ e) = e

499+ subexpr (LDefaultCase e) = e

500+

501+irSC vs (Case n alts) = LCase (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts

502+irSC vs ImpossibleCase = return LNothing

503+

504+irAlt :: Vars -> LExp -> CaseAlt -> Idris LAlt

505+

506+-- this leaves out all unused arguments of the constructor

507+irAlt vs _ (ConCase n t args sc) = do

508+ used <- getUsed . lookup n <$> getIState

509+ let usedArgs = [a | (i,a) <- zip [0..] args, i `elem` used]

510+ LConCase (-1) n usedArgs <$> irSC (methodVars `M.union` vs) sc

511+ where

512+ lookup n = lookupCtxtExact n . idris_callgraph

513+ getUsed = maybe [] (map fst . usedpos)

514+

515+ methodVars = case n of

516+ SN (InstanceCtorN className)

517+ -> M.fromList [(v, VI

518+ { viMethod = Just $ mkFieldName n i

519+ }) | (v,i) <- zip args [0..]]

520+ _

521+ -> M.empty -- not an instance constructor

522+

523+irAlt vs _ (ConstCase x rhs)

524+ | matchable x = LConstCase x <$> irSC vs rhs

525+ | matchableTy x = LDefaultCase <$> irSC vs rhs

526+ where

527+ matchable (I _) = True

528+ matchable (BI _) = True

529+ matchable (Ch _) = True

530+ matchable (Str _) = True

531+ matchable _ = False

532+

533+ matchableTy (AType (ATInt ITNative)) = True

534+ matchableTy (AType (ATInt ITBig)) = True

535+ matchableTy (AType (ATInt ITChar)) = True

536+ matchableTy StrType = True

537+

538+ matchableTy (AType (ATInt (ITFixed IT8))) = True

539+ matchableTy (AType (ATInt (ITFixed IT16))) = True

540+ matchableTy (AType (ATInt (ITFixed IT32))) = True

541+ matchableTy (AType (ATInt (ITFixed IT64))) = True

542+

543+ matchableTy _ = False

544+

545+irAlt vs tm (SucCase n rhs) = do

546+ rhs' <- irSC vs rhs

547+ return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))

548+ [tm,

549+ LConst (BI 1)]) rhs')

550+

551+irAlt vs _ (ConstCase c rhs)

552+ = ifail $ "Can't match on (" ++ show c ++ ")"

553+

554+irAlt vs _ (DefaultCase rhs)

555+ = LDefaultCase <$> irSC vs rhs

src/IRTS/Lang.hs+56−31

@@ -213,36 +213,61 @@ usedIn env (LOp f args) = concatMap (usedIn env) args

213usedIn env _ = []

214

215instance Show LExp where

216− show e = show' [] e where

216+ show e = show' [] "" e where

217− show' env (LV (Loc i)) = env!!i

217+ show' env ind (LV (Loc i)) = env!!i

218− show' env (LV (Glob n)) = show n

218+ show' env ind (LV (Glob n)) = show n

219+

219− show' env (LLazyApp e args) = show e ++ "|(" ++

220+ show' env ind (LLazyApp e args)

220− showSep ", " (map (show' env) args) ++")"

221+ = show e ++ "|(" ++ showSep ", " (map (show' env ind) args) ++")"

222+

221− show' env (LApp _ e args) = show' env e ++ "(" ++

223+ show' env ind (LApp _ e args)

222− showSep ", " (map (show' env) args) ++")"

224+ = show' env ind e ++ "(" ++ showSep ", " (map (show' env ind) args) ++")"

225+

223− show' env (LLazyExp e) = "%lazy(" ++ show' env e ++ ")"

226+ show' env ind (LLazyExp e) = "lazy{ " ++ show' env ind e ++ " }"

224− show' env (LForce e) = "%force(" ++ show' env e ++ ")"

227+ show' env ind (LForce e) = "force{ " ++ show' env ind e ++ " }"

228+ show' env ind (LLet n v e)

225− show' env (LLet n v e) = "let " ++ show n ++ " = " ++ show' env v ++ " in " ++

229+ = "let " ++ show n ++ " = " ++ show' env ind v

226− show' (env ++ [show n]) e

230+ ++ " in " ++ show' (env ++ [show n]) ind e

231+

232+ show' env ind (LLam args e)

227− show' env (LLam args e) = "\\ " ++ showSep "," (map show args) ++ " => " ++

233+ = "\\ " ++ showSep "," (map show args)

228− show' (env ++ (map show args)) e

234+ ++ " => " ++ show' (env ++ (map show args)) ind e

235+

229− show' env (LProj t i) = show t ++ "!" ++ show i

236+ show' env ind (LProj t i) = show t ++ "!" ++ show i

237+

238+ show' env ind (LCon i n args)

230− show' env (LCon i n args) = show n ++ ")" ++ showSep ", " (map (show' env) args) ++ ")"

239+ = show n ++ "(" ++ showSep ", " (map (show' env ind) args) ++ ")"

240+

231− show' env (LCase e alts) = "case " ++ show' env e ++ " of {\n\t" ++

241+ show' env ind (LCase e alts)

242+ = "case " ++ show' env ind e ++ " of \n" ++ fmt alts

243+ where

244+ fmt [] = ""

245+ fmt [alt]

246+ = "\t" ++ ind ++ "| " ++ showAlt env (ind ++ " ") alt

247+ fmt (alt:as)

232− showSep "\n\t| " (map (showAlt env) alts)

248+ = "\t" ++ ind ++ "| " ++ showAlt env (ind ++ ". ") alt

249+ ++ "\n" ++ fmt as

250+

233− show' env (LConst c) = show c

251+ show' env ind (LConst c) = show c

252+

234− show' env (LForeign lang ty n args)

253+ show' env ind (LForeign lang ty n args) = concat

254+ [ "foreign{ "

255+ , n ++ "("

235− = "foreign " ++ n ++ "(" ++ showSep ", " (map (show' env) (map snd args)) ++ ")"

256+ , showSep ", " (map (\(ty,x) -> show' env ind x ++ " : " ++ show ty) args)

257+ , ") : "

258+ , show ty

259+ , " }"

260+ ]

261+

262+ show' env ind (LOp f args)

236− show' env (LOp f args) = show f ++ "(" ++ showSep ", " (map (show' env) args) ++ ")"

263+ = show f ++ "(" ++ showSep ", " (map (show' env ind) args) ++ ")"

264+

237− show' env (LError str) = "error " ++ show str

265+ show' env ind (LError str) = "error " ++ show str

238− show' env LNothing = "____"

266+ show' env ind LNothing = "____"

239−

267+

240− showAlt env (LConCase _ n args e)

268+ showAlt env ind (LConCase _ n args e)

241 = show n ++ "(" ++ showSep ", " (map show args) ++ ") => "

269 = show n ++ "(" ++ showSep ", " (map show args) ++ ") => "

242− ++ show' env e

270+ ++ show' env ind e

243− showAlt env (LConstCase c e) = show c ++ " => " ++ show' env e

244− showAlt env (LDefaultCase e) = "_ => " ++ show' env e

245−

246−

247−

248

271

272+ showAlt env ind (LConstCase c e) = show c ++ " => " ++ show' env ind e

273+ showAlt env ind (LDefaultCase e) = "_ => " ++ show' env ind e

src/Idris/AbsSyntax.hs+91−37

@@ -388,6 +388,16 @@ getIState = get

388putIState :: IState -> Idris ()

389putIState = put

390

391+withContext :: (IState -> Ctxt a) -> Name -> b -> (a -> Idris b) -> Idris b

392+withContext ctx name dflt action = do

393+ ist <- getIState

394+ case lookupCtxt name (ctx ist) of

395+ [x] -> action x

396+ _ -> return dflt

397+

398+withContext_ :: (IState -> Ctxt a) -> Name -> (a -> Idris ()) -> Idris ()

399+withContext_ ctx name action = withContext ctx name () action

400+

391-- | A version of liftIO that puts errors into the exception type of the Idris monad

401-- | A version of liftIO that puts errors into the exception type of the Idris monad

392runIO :: IO a -> Idris a

402runIO :: IO a -> Idris a

393runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return

403runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return

@@ -819,9 +829,9 @@ expandParams dec ps ns infs tm = en tm

819 | otherwise = PLam n (en t) (en s)

829 | otherwise = PLam n (en t) (en s)

820 en (PPi p n t s)

830 en (PPi p n t s)

821 | n `elem` (map fst ps ++ ns)

831 | n `elem` (map fst ps ++ ns)

822− = let n' = mkShadow n in

832+ = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?

823− PPi p n' (en t) (en (shadow n n' s))

833+ PPi (enTacImp p) n' (en t) (en (shadow n n' s))

824− | otherwise = PPi p n (en t) (en s)

834+ | otherwise = PPi (enTacImp p) n (en t) (en s)

825 en (PLet n ty v s)

835 en (PLet n ty v s)

826 | n `elem` (map fst ps ++ ns)

836 | n `elem` (map fst ps ++ ns)

827 = let n' = mkShadow n in

837 = let n' = mkShadow n in

@@ -880,6 +890,9 @@ expandParams dec ps ns infs tm = en tm

880

890

881 nseq x y = nsroot x == nsroot y

891 nseq x y = nsroot x == nsroot y

882

892

893+ enTacImp (TacImp aos st scr) = TacImp aos st (en scr)

894+ enTacImp other = other

895+

883expandParamsD :: Bool -> -- True = RHS only

896expandParamsD :: Bool -> -- True = RHS only

884 IState ->

897 IState ->

885 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl

898 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl

@@ -1076,7 +1089,7 @@ addUsingConstraints syn fc t

1076 | otherwise = doAdd cs ns t

1089 | otherwise = doAdd cs ns t

1077

1090

1078 mkConst c args = PApp fc (PRef fc c)

1091 mkConst c args = PApp fc (PRef fc c)

1079− (map (\n -> PExp 0 [] (PRef fc n)) args)

1092+ (map (\n -> PExp 0 [] (sMN 0 "carg") (PRef fc n)) args)

1080

1093

1081 getConstraints (PPi (Constraint _ _) _ c sc)

1094 getConstraints (PPi (Constraint _ _) _ c sc)

1082 = getcapp c ++ getConstraints sc

1095 = getcapp c ++ getConstraints sc

@@ -1088,7 +1101,7 @@ addUsingConstraints syn fc t

1088 return (UConstraint c ns)

1101 return (UConstraint c ns)

1089 getcapp _ = []

1102 getcapp _ = []

1090

1103

1091− getName (PExp _ _ (PRef _ n)) = return n

1104+ getName (PExp _ _ _ (PRef _ n)) = return n

1092 getName _ = []

1105 getName _ = []

1093

1106

1094-- Add implicit Pi bindings for any names in the term which appear in an

1107-- Add implicit Pi bindings for any names in the term which appear in an

@@ -1096,13 +1109,14 @@ addUsingConstraints syn fc t

1096

1109

1097-- This has become a right mess already. Better redo it some time...

1110-- This has become a right mess already. Better redo it some time...

1098

1111

1099−implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm

1112+implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm

1100−implicit syn n ptm = implicit' syn [] n ptm

1113+implicit info syn n ptm = implicit' info syn [] n ptm

1101

1114

1102−implicit' :: SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm

1115+implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm

1103−implicit' syn ignore n ptm

1116+implicit' info syn ignore n ptm

1104 = do i <- getIState

1117 = do i <- getIState

1105 let (tm', impdata) = implicitise syn ignore i ptm

1118 let (tm', impdata) = implicitise syn ignore i ptm

1119+ defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata

1106-- let (tm'', spos) = findStatics i tm'

1120-- let (tm'', spos) = findStatics i tm'

1107 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }

1121 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }

1108 addIBC (IBCImp n)

1122 addIBC (IBCImp n)

@@ -1110,6 +1124,23 @@ implicit' syn ignore n ptm

1110-- i <- get

1124-- i <- get

1111-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }

1125-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }

1112 return tm'

1126 return tm'

1127+ where

1128+ -- Detect unknown names in default arguments and throw error if found.

1129+ defaultArgCheck :: [Name] -> [PArg] -> Idris ()

1130+ defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params

1131+

1132+ notFoundInDefault :: [Name] -> PArg -> Idris [Name]

1133+ notFoundInDefault kns (PTacImplicit _ _ n script _)

1134+ = do i <- getIState

1135+ case notFound kns (namesIn [] i script) of

1136+ Nothing -> return (n:kns)

1137+ Just name -> throwError (NoSuchVariable name)

1138+ notFoundInDefault kns p = return ((pname p):kns)

1139+

1140+ notFound :: [Name] -> [Name] -> Maybe Name

1141+ notFound kns [] = Nothing

1142+ notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already

1143+ notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n

1113

1144

1114implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])

1145implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])

1115implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

1146implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

@@ -1155,7 +1186,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

1155 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

1186 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

1156 _ -> [])

1187 _ -> [])

1157 (decls, ns) <- get -- ignore decls in HO types

1188 (decls, ns) <- get -- ignore decls in HO types

1158− put (PExp (getPriority ist ty) l Placeholder : decls,

1189+ put (PExp (getPriority ist ty) l n Placeholder : decls,

1159 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1190 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1160 imps True (n:env) sc

1191 imps True (n:env) sc

1161 imps top env (PPi (Constraint l _) n ty sc)

1192 imps top env (PPi (Constraint l _) n ty sc)

@@ -1163,7 +1194,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

1163 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

1194 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

1164 _ -> [])

1195 _ -> [])

1165 (decls, ns) <- get -- ignore decls in HO types

1196 (decls, ns) <- get -- ignore decls in HO types

1166− put (PConstraint 10 l Placeholder : decls,

1197+ put (PConstraint 10 l n Placeholder : decls,

1167 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1198 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1168 imps True (n:env) sc

1199 imps True (n:env) sc

1169 imps top env (PPi (TacImp l _ scr) n ty sc)

1200 imps top env (PPi (TacImp l _ scr) n ty sc)

@@ -1329,7 +1360,7 @@ aiFn inpat True ist fc f ds []

1329-- any constructor alts || any allImp ialts))

1360-- any constructor alts || any allImp ialts))

1330 then aiFn inpat False ist fc f ds [] -- use it as a constructor

1361 then aiFn inpat False ist fc f ds [] -- use it as a constructor

1331 else Right $ PPatvar fc f

1362 else Right $ PPatvar fc f

1332− where imp (PExp _ _ _) = False

1363+ where imp (PExp _ _ _ _) = False

1333 imp _ = True

1364 imp _ = True

1334-- allImp [] = False

1365-- allImp [] = False

1335 allImp xs = all imp xs

1366 allImp xs = all imp xs

@@ -1376,27 +1407,41 @@ aiFn inpat expat ist fc f ds as

1376 [(n,t)] -> t

1407 [(n,t)] -> t

1377 _ -> Public

1408 _ -> Public

1378

1409

1379−

1380 insertImpl :: [PArg] -> [PArg] -> [PArg]

1410 insertImpl :: [PArg] -> [PArg] -> [PArg]

1411+ insertImpl ps as = insImpAcc M.empty ps as

1412+

1413+ insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms

1414+ -> [PArg] -- parameters

1415+ -> [PArg] -- arguments

1416+ -> [PArg]

1381− insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =

1417+ insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) =

1382− PExp p l tm : insertImpl ps given

1418+ PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given

1383− insertImpl (PConstraint p l ty : ps) (PConstraint _ _ tm : given) =

1419+ insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) =

1384− PConstraint p l tm : insertImpl ps given

1420+ PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given

1385− insertImpl (PConstraint p l ty : ps) given =

1421+ insImpAcc pnas (PConstraint p l n ty : ps) given =

1386− PConstraint p l (PResolveTC fc) : insertImpl ps given

1422+ let rtc = PResolveTC fc in

1423+ PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given

1387− insertImpl (PImp p _ l n ty : ps) given =

1424+ insImpAcc pnas (PImp p _ l n ty : ps) given =

1388 case find n given [] of

1425 case find n given [] of

1426+ Just (tm, given') ->

1389− Just (tm, given') -> PImp p False l n tm : insertImpl ps given'

1427+ PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given'

1428+ Nothing ->

1390− Nothing -> PImp p True l n Placeholder : insertImpl ps given

1429+ PImp p True l n Placeholder :

1430+ insImpAcc (M.insert n Placeholder pnas) ps given

1391− insertImpl (PTacImplicit p l n sc' ty : ps) given =

1431+ insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given =

1392− let sc = addImpl ist sc' in

1432+ let sc = addImpl ist (substMatches (M.toList pnas) sc') in

1393 case find n given [] of

1433 case find n given [] of

1434+ Just (tm, given') ->

1394− Just (tm, given') -> PTacImplicit p l n sc tm : insertImpl ps given'

1435+ PTacImplicit p l n sc tm :

1436+ insImpAcc (M.insert n tm pnas) ps given'

1395− Nothing -> if inpat

1437+ Nothing ->

1438+ if inpat

1396− then PTacImplicit p l n sc Placeholder : insertImpl ps given

1439+ then PTacImplicit p l n sc Placeholder :

1440+ insImpAcc (M.insert n Placeholder pnas) ps given

1397− else PTacImplicit p l n sc sc : insertImpl ps given

1441+ else PTacImplicit p l n sc sc :

1442+ insImpAcc (M.insert n sc pnas) ps given

1398− insertImpl expected [] = []

1443+ insImpAcc _ expected [] = []

1399− insertImpl _ given = given

1444+ insImpAcc _ _ given = given

1400

1445

1401 find n [] acc = Nothing

1446 find n [] acc = Nothing

1402 find n (PImp _ _ _ n' t : gs) acc

1447 find n (PImp _ _ _ n' t : gs) acc

@@ -1433,11 +1478,11 @@ stripLinear i tm = evalState (sl tm) [] where

1433 return $ PApp fc fn args'

1478 return $ PApp fc fn args'

1434 where slA (PImp p m l n t) = do t' <- sl t

1479 where slA (PImp p m l n t) = do t' <- sl t

1435 return $ PImp p m l n t'

1480 return $ PImp p m l n t'

1436− slA (PExp p l t) = do t' <- sl t

1481+ slA (PExp p l n t) = do t' <- sl t

1437− return $ PExp p l t'

1482+ return $ PExp p l n t'

1438− slA (PConstraint p l t)

1483+ slA (PConstraint p l n t)

1439 = do t' <- sl t

1484 = do t' <- sl t

1440− return $ PConstraint p l t'

1485+ return $ PConstraint p l n t'

1441 slA (PTacImplicit p l n sc t)

1486 slA (PTacImplicit p l n sc t)

1442 = do t' <- sl t

1487 = do t' <- sl t

1443 return $ PTacImplicit p l n sc t'

1488 return $ PTacImplicit p l n sc t'

@@ -1695,6 +1740,12 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where

1695 mkUniqA arg = do t' <- mkUniq (getTm arg)

1740 mkUniqA arg = do t' <- mkUniq (getTm arg)

1696 return (arg { getTm = t' })

1741 return (arg { getTm = t' })

1697

1742

1743+ -- Initialise the unique name with the environment length (so we're not

1744+ -- looking for too long...)

1745+ initN (UN n) l = UN $ txt (str n ++ show l)

1746+ initN (MN i s) l = MN (i+l) s

1747+ initN n l = n

1748+

1698 -- FIXME: Probably ought to do this for completeness! It's fine as

1749 -- FIXME: Probably ought to do this for completeness! It's fine as

1699 -- long as there are no bindings inside tactics though.

1750 -- long as there are no bindings inside tactics though.

1700 mkUniqT tac = return tac

1751 mkUniqT tac = return tac

@@ -1704,7 +1755,8 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where

1704 = do env <- get

1755 = do env <- get

1705 (n', sc') <-

1756 (n', sc') <-

1706 if n `elem` env

1757 if n `elem` env

1707− then do let n' = uniqueName n (env ++ inScope)

1758+ then do let n' = uniqueName (initN n (length env))

1759+ (env ++ inScope)

1708 return (n', shadow n n' sc)

1760 return (n', shadow n n' sc)

1709 else return (n, sc)

1761 else return (n, sc)

1710 put (n' : env)

1762 put (n' : env)

@@ -1715,7 +1767,8 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where

1715 = do env <- get

1767 = do env <- get

1716 (n', sc') <-

1768 (n', sc') <-

1717 if n `elem` env

1769 if n `elem` env

1718− then do let n' = uniqueName n (env ++ inScope)

1770+ then do let n' = uniqueName (initN n (length env))

1771+ (env ++ inScope)

1719 return (n', shadow n n' sc)

1772 return (n', shadow n n' sc)

1720 else return (n, sc)

1773 else return (n, sc)

1721 put (n' : env)

1774 put (n' : env)

@@ -1726,7 +1779,8 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where

1726 = do env <- get

1779 = do env <- get

1727 (n', sc') <-

1780 (n', sc') <-

1728 if n `elem` env

1781 if n `elem` env

1729− then do let n' = uniqueName n (env ++ inScope)

1782+ then do let n' = uniqueName (initN n (length env))

1783+ (env ++ inScope)

1730 return (n', shadow n n' sc)

1784 return (n', shadow n n' sc)

1731 else return (n, sc)

1785 else return (n, sc)

1732 put (n' : env)

1786 put (n' : env)

src/Idris/AbsSyntaxTree.hs+64−54

@@ -36,6 +36,19 @@ import Debug.Trace

36

37import Text.PrettyPrint.Annotated.Leijen

38

39+-- Data to pass to recursively called elaborators; e.g. for where blocks,

40+-- paramaterised declarations, etc.

41+

42+data ElabInfo = EInfo { params :: [(Name, PTerm)],

43+ inblock :: Ctxt [Name], -- names in the block, and their params

44+ liftname :: Name -> Name,

45+ namespace :: Maybe [String] }

46+

47+toplevel = EInfo [] emptyContext id Nothing

48+

49+eInfoNames :: ElabInfo -> [Name]

50+eInfoNames info = map fst (params info) ++ M.keys (inblock info)

51+

39data IOption = IOption { opt_logLevel :: Int,

52data IOption = IOption { opt_logLevel :: Int,

40 opt_typecase :: Bool,

53 opt_typecase :: Bool,

41 opt_typeintype :: Bool,

54 opt_typeintype :: Bool,

@@ -152,7 +165,8 @@ data IState = IState {

152 idris_nameIdx :: (Int, Ctxt (Int, Name)),

165 idris_nameIdx :: (Int, Ctxt (Int, Name)),

153 idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)), -- ^ Specific error handlers

166 idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)), -- ^ Specific error handlers

154 module_aliases :: M.Map [T.Text] [T.Text],

167 module_aliases :: M.Map [T.Text] [T.Text],

155− idris_consolewidth :: ConsoleWidth -- ^ How many chars wide is the console?

168+ idris_consolewidth :: ConsoleWidth, -- ^ How many chars wide is the console?

169+ idris_postulates :: S.Set Name

156 }

170 }

157

171

158data SizeChange = Smaller | Same | Bigger | Unknown

172data SizeChange = Smaller | Same | Bigger | Unknown

@@ -168,7 +182,7 @@ data CGInfo = CGInfo { argsdef :: [Name],

168 calls :: [(Name, [[Name]])],

182 calls :: [(Name, [[Name]])],

169 scg :: [SCGEntry],

183 scg :: [SCGEntry],

170 argsused :: [Name],

184 argsused :: [Name],

171− unusedpos :: [Int] }

185+ usedpos :: [(Int, [(Name, Int)])] } -- (used_arg#, [(using_fn, its_arg#)])

172 deriving Show

186 deriving Show

173{-!

187{-!

174deriving instance Binary CGInfo

188deriving instance Binary CGInfo

@@ -212,6 +226,7 @@ data IBCWrite = IBCFix FixDecl

212 | IBCLineApp FilePath Int PTerm

226 | IBCLineApp FilePath Int PTerm

213 | IBCErrorHandler Name

227 | IBCErrorHandler Name

214 | IBCFunctionErrorHandler Name Name Name

228 | IBCFunctionErrorHandler Name Name Name

229+ | IBCPostulate Name

215 deriving Show

230 deriving Show

216

231

217-- | The initial state for the compiler

232-- | The initial state for the compiler

@@ -223,7 +238,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

223 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

238 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

224 [] [] Nothing [] Nothing [] [] Nothing [] Hidden False [] Nothing [] [] RawOutput

239 [] [] Nothing [] Nothing [] [] Nothing [] Hidden False [] Nothing [] [] RawOutput

225 True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty

240 True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty

226− AutomaticWidth

241+ AutomaticWidth S.empty

227

242

228-- | The monad for the main REPL - reading and processing files and updating

243-- | The monad for the main REPL - reading and processing files and updating

229-- global state (hence the IO inner monad).

244-- global state (hence the IO inner monad).

@@ -312,6 +327,7 @@ data Opt = Filename String

312 | DefaultTotal

327 | DefaultTotal

313 | DefaultPartial

328 | DefaultPartial

314 | WarnPartial

329 | WarnPartial

330+ | WarnReach

315 | NoCoverage

331 | NoCoverage

316 | ErrContext

332 | ErrContext

317 | ShowImpl

333 | ShowImpl

@@ -388,7 +404,7 @@ data Plicity = Imp { pargopts :: [ArgOpt],

388 pparam :: Bool }

404 pparam :: Bool }

389 | Exp { pargopts :: [ArgOpt],

405 | Exp { pargopts :: [ArgOpt],

390 pstatic :: Static,

406 pstatic :: Static,

391− pparam :: Bool }

407+ pparam :: Bool } -- this is a param (rather than index)

392 | Constraint { pargopts :: [ArgOpt],

408 | Constraint { pargopts :: [ArgOpt],

393 pstatic :: Static }

409 pstatic :: Static }

394 | TacImp { pargopts :: [ArgOpt],

410 | TacImp { pargopts :: [ArgOpt],

@@ -396,15 +412,12 @@ data Plicity = Imp { pargopts :: [ArgOpt],

396 pscript :: PTerm }

412 pscript :: PTerm }

397 deriving (Show, Eq)

413 deriving (Show, Eq)

398

414

399−plazy :: Plicity -> Bool

400−plazy tm = Lazy `elem` pargopts tm

401−

402{-!

415{-!

403deriving instance Binary Plicity

416deriving instance Binary Plicity

404deriving instance NFData Plicity

417deriving instance NFData Plicity

405!-}

418!-}

406

419

407−impl = Imp [Lazy] Dynamic False

420+impl = Imp [] Dynamic False

408expl = Exp [] Dynamic False

421expl = Exp [] Dynamic False

409expl_param = Exp [] Dynamic True

422expl_param = Exp [] Dynamic True

410constraint = Constraint [] Dynamic

423constraint = Constraint [] Dynamic

@@ -769,9 +782,11 @@ data PArg' t = PImp { priority :: Int,

769 pname :: Name, getTm :: t }

782 pname :: Name, getTm :: t }

770 | PExp { priority :: Int,

783 | PExp { priority :: Int,

771 argopts :: [ArgOpt],

784 argopts :: [ArgOpt],

785+ pname :: Name,

772 getTm :: t }

786 getTm :: t }

773 | PConstraint { priority :: Int,

787 | PConstraint { priority :: Int,

774 argopts :: [ArgOpt],

788 argopts :: [ArgOpt],

789+ pname :: Name,

775 getTm :: t }

790 getTm :: t }

776 | PTacImplicit { priority :: Int,

791 | PTacImplicit { priority :: Int,

777 argopts :: [ArgOpt],

792 argopts :: [ArgOpt],

@@ -780,16 +795,13 @@ data PArg' t = PImp { priority :: Int,

780 getTm :: t }

795 getTm :: t }

781 deriving (Show, Eq, Functor)

796 deriving (Show, Eq, Functor)

782

797

783−data ArgOpt = Lazy | HideDisplay

798+data ArgOpt = HideDisplay | InaccessibleArg

784 deriving (Show, Eq)

799 deriving (Show, Eq)

785

800

786−lazyarg :: PArg' t -> Bool

787−lazyarg tm = Lazy `elem` argopts tm

788−

789instance Sized a => Sized (PArg' a) where

801instance Sized a => Sized (PArg' a) where

790 size (PImp p _ l nm trm) = 1 + size nm + size trm

802 size (PImp p _ l nm trm) = 1 + size nm + size trm

791− size (PExp p l trm) = 1 + size trm

803+ size (PExp p l nm trm) = 1 + size nm + size trm

792− size (PConstraint p l trm) = 1 + size trm

804+ size (PConstraint p l nm trm) = 1 + size nm +size nm + size trm

793 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm

805 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm

794

806

795{-!

807{-!

@@ -797,10 +809,10 @@ deriving instance Binary PArg'

797deriving instance NFData PArg'

809deriving instance NFData PArg'

798!-}

810!-}

799

811

800−pimp n t mach = PImp 1 mach [Lazy] n t

812+pimp n t mach = PImp 1 mach [] n t

801−pexp t = PExp 1 [] t

813+pexp t = PExp 1 [] (sMN 0 "arg") t

802−pconst t = PConstraint 1 [] t

814+pconst t = PConstraint 1 [] (sMN 0 "carg") t

803−ptacimp n s t = PTacImplicit 2 [Lazy] n s t

815+ptacimp n s t = PTacImplicit 2 [] n s t

804

816

805type PArg = PArg' PTerm

817type PArg = PArg' PTerm

806

818

@@ -824,22 +836,8 @@ data TIData = TIPartial -- ^ a function with a partially defined type

824 | TISolution [Term] -- ^ possible solutions to a metavariable in a type

836 | TISolution [Term] -- ^ possible solutions to a metavariable in a type

825 deriving Show

837 deriving Show

826

838

827−-- An argument is conditionally forceable iff its forceability

839+data OptInfo = Optimise { inaccessible :: [(Int,Name)], -- includes names for error reporting

828−-- depends on the collapsibility of the whole type.

840+ detaggable :: Bool }

829−data Forceability = Conditional | Unconditional deriving (Show, Enum, Bounded, Eq, Ord)

830−

831−{-!

832−deriving instance Binary Forceability

833−deriving instance NFData Forceability

834−!-}

835−

836−data OptInfo = Optimise { collapsible :: Bool,

837− isnewtype :: Bool,

838− -- The following should actually be (IntMap Forceability)

839− -- but the corresponding Binary instance seems to be broken.

840− -- Let's store a list and convert it to IntMap whenever needed.

841− forceable :: [(Int, Forceability)],

842− recursive :: [Int] }

843 deriving Show

841 deriving Show

844{-!

842{-!

845deriving instance Binary OptInfo

843deriving instance Binary OptInfo

@@ -1112,10 +1110,9 @@ pprintPTerm impl bnd docArgs = prettySe 10 bnd

1112 prettySe 10 ((n, False):bnd) sc

1110 prettySe 10 ((n, False):bnd) sc

1113 prettySe p bnd (PPi (Exp l s _) n ty sc)

1111 prettySe p bnd (PPi (Exp l s _) n ty sc)

1114 | n `elem` allNamesIn sc || impl || n `elem` docArgs =

1112 | n `elem` allNamesIn sc || impl || n `elem` docArgs =

1115− let open = if Lazy `elem` l then text "|" <> lparen else lparen in

1116− bracket p 2 . group $

1113+ bracket p 2 . group $

1117− enclose open rparen (group . align $ bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>

1114+ enclose lparen rparen (group . align $ bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>

1118− st <> text "->" <$> prettySe 10 ((n, False):bnd) sc

1115+ st <> text "->" <$> prettySe 10 ((n, False):bnd) sc

1119 | otherwise =

1116 | otherwise =

1120 bracket p 2 . group $

1117 bracket p 2 . group $

1121 group (prettySe 0 bnd ty <+> st) <> text "->" <$> group (prettySe 10 ((n, False):bnd) sc)

1118 group (prettySe 0 bnd ty <+> st) <> text "->" <$> group (prettySe 10 ((n, False):bnd) sc)

@@ -1126,10 +1123,9 @@ pprintPTerm impl bnd docArgs = prettySe 10 bnd

1126 _ -> empty

1123 _ -> empty

1127 prettySe p bnd (PPi (Imp l s _) n ty sc)

1124 prettySe p bnd (PPi (Imp l s _) n ty sc)

1128 | impl =

1125 | impl =

1129− let open = if Lazy `elem` l then text "|" <> lbrace else lbrace in

1130− bracket p 2 $

1126+ bracket p 2 $

1131− open <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>

1127+ lparen <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>

1132− st <> text "->" </> prettySe 10 ((n, True):bnd) sc

1128+ st <> text "->" </> prettySe 10 ((n, True):bnd) sc

1133 | otherwise = prettySe 10 ((n, True):bnd) sc

1129 | otherwise = prettySe 10 ((n, True):bnd) sc

1134 where

1130 where

1135 st =

1131 st =

@@ -1257,8 +1253,8 @@ pprintPTerm impl bnd docArgs = prettySe 10 bnd

1257 prettySe p bnd _ = text "test"

1253 prettySe p bnd _ = text "test"

1258

1254

1259 prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)

1255 prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)

1260− prettyArgS bnd (PExp _ _ tm) = prettyArgSe bnd tm

1256+ prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm

1261− prettyArgS bnd (PConstraint _ _ tm) = prettyArgSc bnd tm

1257+ prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm

1262 prettyArgS bnd (PTacImplicit _ _ n _ tm) = prettyArgSti bnd (n, tm)

1258 prettyArgS bnd (PTacImplicit _ _ n _ tm) = prettyArgSti bnd (n, tm)

1263

1259

1264 prettyArgSe bnd arg = prettySe 0 bnd arg

1260 prettyArgSe bnd arg = prettySe 0 bnd arg

@@ -1390,12 +1386,12 @@ getImps (_ : xs) = getImps xs

1390

1386

1391getExps :: [PArg] -> [PTerm]

1387getExps :: [PArg] -> [PTerm]

1392getExps [] = []

1388getExps [] = []

1393−getExps (PExp _ _ tm : xs) = tm : getExps xs

1389+getExps (PExp _ _ _ tm : xs) = tm : getExps xs

1394getExps (_ : xs) = getExps xs

1390getExps (_ : xs) = getExps xs

1395

1391

1396getConsts :: [PArg] -> [PTerm]

1392getConsts :: [PArg] -> [PTerm]

1397getConsts [] = []

1393getConsts [] = []

1398−getConsts (PConstraint _ _ tm : xs) = tm : getConsts xs

1394+getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs

1399getConsts (_ : xs) = getConsts xs

1395getConsts (_ : xs) = getConsts xs

1400

1396

1401getAll :: [PArg] -> [PTerm]

1397getAll :: [PArg] -> [PTerm]

@@ -1434,7 +1430,9 @@ showName ist bnd impl colour n = case ist of

1434showTm :: IState -- ^^ the Idris state, for information about identifiers and colours

1430showTm :: IState -- ^^ the Idris state, for information about identifiers and colours

1435 -> PTerm -- ^^ the term to show

1431 -> PTerm -- ^^ the term to show

1436 -> String

1432 -> String

1437−showTm ist = displayDecorated (consoleDecorate ist) . renderCompact . prettyImp (opt_showimp (idris_options ist))

1433+showTm ist = displayDecorated (consoleDecorate ist) .

1434+ renderPretty 0.8 100000 .

1435+ prettyImp (opt_showimp (idris_options ist))

1438

1436

1439-- | Show a term with implicits, no colours

1437-- | Show a term with implicits, no colours

1440showTmImpls :: PTerm -> String

1438showTmImpls :: PTerm -> String

@@ -1483,7 +1481,7 @@ getPArity _ = 0

1483

1481

1484allNamesIn :: PTerm -> [Name]

1482allNamesIn :: PTerm -> [Name]

1485allNamesIn tm = nub $ ni [] tm

1483allNamesIn tm = nub $ ni [] tm

1486− where

1484+ where -- TODO THINK added niTacImp, but is it right?

1487 ni env (PRef _ n)

1485 ni env (PRef _ n)

1488 | not (n `elem` env) = [n]

1486 | not (n `elem` env) = [n]

1489 ni env (PPatvar _ n) = [n]

1487 ni env (PPatvar _ n) = [n]

@@ -1491,7 +1489,7 @@ allNamesIn tm = nub $ ni [] tm

1491 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1489 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1492 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)

1490 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)

1493 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1491 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1494− ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc

1492+ ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

1495 ni env (PHidden tm) = ni env tm

1493 ni env (PHidden tm) = ni env tm

1496 ni env (PEq _ l r) = ni env l ++ ni env r

1494 ni env (PEq _ l r) = ni env l ++ ni env r

1497 ni env (PRewrite _ l r _) = ni env l ++ ni env r

1495 ni env (PRewrite _ l r _) = ni env l ++ ni env r

@@ -1505,16 +1503,19 @@ allNamesIn tm = nub $ ni [] tm

1505 ni env (PNoImplicits tm) = ni env tm

1503 ni env (PNoImplicits tm) = ni env tm

1506 ni env _ = []

1504 ni env _ = []

1507

1505

1506+ niTacImp env (TacImp _ _ scr) = ni env scr

1507+ niTacImp _ _ = []

1508+

1508-- Return all names defined in binders in the given term

1509-- Return all names defined in binders in the given term

1509boundNamesIn :: PTerm -> [Name]

1510boundNamesIn :: PTerm -> [Name]

1510boundNamesIn tm = nub $ ni tm

1511boundNamesIn tm = nub $ ni tm

1511− where

1512+ where -- TODO THINK Added niTacImp, but is it right?

1512 ni (PApp _ f as) = ni f ++ concatMap (ni) (map getTm as)

1513 ni (PApp _ f as) = ni f ++ concatMap (ni) (map getTm as)

1513 ni (PAppBind _ f as) = ni f ++ concatMap (ni) (map getTm as)

1514 ni (PAppBind _ f as) = ni f ++ concatMap (ni) (map getTm as)

1514 ni (PCase _ c os) = ni c ++ concatMap (ni) (map snd os)

1515 ni (PCase _ c os) = ni c ++ concatMap (ni) (map snd os)

1515 ni (PLam n ty sc) = n : (ni ty ++ ni sc)

1516 ni (PLam n ty sc) = n : (ni ty ++ ni sc)

1516 ni (PLet n ty val sc) = n : (ni ty ++ ni val ++ ni sc)

1517 ni (PLet n ty val sc) = n : (ni ty ++ ni val ++ ni sc)

1517− ni (PPi _ n ty sc) = n : (ni ty ++ ni sc)

1518+ ni (PPi p n ty sc) = niTacImp p ++ (n : (ni ty ++ ni sc))

1518 ni (PEq _ l r) = ni l ++ ni r

1519 ni (PEq _ l r) = ni l ++ ni r

1519 ni (PRewrite _ l r _) = ni l ++ ni r

1520 ni (PRewrite _ l r _) = ni l ++ ni r

1520 ni (PTyped l r) = ni l ++ ni r

1521 ni (PTyped l r) = ni l ++ ni r

@@ -1528,6 +1529,9 @@ boundNamesIn tm = nub $ ni tm

1528 ni (PNoImplicits tm) = ni tm

1529 ni (PNoImplicits tm) = ni tm

1529 ni _ = []

1530 ni _ = []

1530

1531

1532+ niTacImp (TacImp _ _ scr) = ni scr

1533+ niTacImp _ = []

1534+

1531-- Return names which are free in the given term.

1535-- Return names which are free in the given term.

1532namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]

1536namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]

1533namesIn uvars ist tm = nub $ ni [] tm

1537namesIn uvars ist tm = nub $ ni [] tm

@@ -1541,7 +1545,7 @@ namesIn uvars ist tm = nub $ ni [] tm

1541 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1545 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1542 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)

1546 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)

1543 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1547 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1544− ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc

1548+ ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

1545 ni env (PEq _ l r) = ni env l ++ ni env r

1549 ni env (PEq _ l r) = ni env l ++ ni env r

1546 ni env (PRewrite _ l r _) = ni env l ++ ni env r

1550 ni env (PRewrite _ l r _) = ni env l ++ ni env r

1547 ni env (PTyped l r) = ni env l ++ ni env r

1551 ni env (PTyped l r) = ni env l ++ ni env r

@@ -1555,11 +1559,14 @@ namesIn uvars ist tm = nub $ ni [] tm

1555 ni env (PNoImplicits tm) = ni env tm

1559 ni env (PNoImplicits tm) = ni env tm

1556 ni env _ = []

1560 ni env _ = []

1557

1561

1562+ niTacImp env (TacImp _ _ scr) = ni env scr

1563+ niTacImp _ _ = []

1564+

1558-- Return which of the given names are used in the given term.

1565-- Return which of the given names are used in the given term.

1559

1566

1560usedNamesIn :: [Name] -> IState -> PTerm -> [Name]

1567usedNamesIn :: [Name] -> IState -> PTerm -> [Name]

1561usedNamesIn vars ist tm = nub $ ni [] tm

1568usedNamesIn vars ist tm = nub $ ni [] tm

1562− where

1569+ where -- TODO THINK added niTacImp, but is it right?

1563 ni env (PRef _ n)

1570 ni env (PRef _ n)

1564 | n `elem` vars && not (n `elem` env)

1571 | n `elem` vars && not (n `elem` env)

1565 = case lookupTy n (tt_ctxt ist) of

1572 = case lookupTy n (tt_ctxt ist) of

@@ -1569,7 +1576,7 @@ usedNamesIn vars ist tm = nub $ ni [] tm

1569 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1576 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1570 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)

1577 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)

1571 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1578 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1572− ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc

1579+ ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

1573 ni env (PEq _ l r) = ni env l ++ ni env r

1580 ni env (PEq _ l r) = ni env l ++ ni env r

1574 ni env (PRewrite _ l r _) = ni env l ++ ni env r

1581 ni env (PRewrite _ l r _) = ni env l ++ ni env r

1575 ni env (PTyped l r) = ni env l ++ ni env r

1582 ni env (PTyped l r) = ni env l ++ ni env r

@@ -1583,3 +1590,6 @@ usedNamesIn vars ist tm = nub $ ni [] tm

1583 ni env (PNoImplicits tm) = ni env tm

1590 ni env (PNoImplicits tm) = ni env tm

1584 ni env _ = []

1591 ni env _ = []

1585

1592

1593+ niTacImp env (TacImp _ _ scr) = ni env scr

1594+ niTacImp _ _ = []

1595+

src/Idris/Core/CaseTree.hs+144−105

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

2

3module Idris.Core.CaseTree(CaseDef(..), SC, SC'(..), CaseAlt, CaseAlt'(..),

4 Phase(..), CaseTree,

5− simpleCase, small, namesUsed, findCalls, findUsedArgs) where

5+ simpleCase, small, namesUsed, findCalls, findUsedArgs,

6+ substSC, substAlt, mkForce) where

6

7

7import Idris.Core.TT

8import Idris.Core.TT

8

9

@@ -14,8 +15,20 @@ import Debug.Trace

14data CaseDef = CaseDef [Name] !SC [Term]

15data CaseDef = CaseDef [Name] !SC [Term]

15 deriving Show

16 deriving Show

16

17

18+-- Note: The case-tree elaborator only produces (Case n alts)-cases;

19+-- in other words, it never inspects anything else than variables.

20+--

21+-- ProjCase is a special powerful case construct that allows inspection

22+-- of compound terms. Occurrences of ProjCase arise no earlier than

23+-- in the function `prune` as a means of optimisation

24+-- of already built case trees.

25+--

26+-- While the intermediate representation (follows in the pipeline)

27+-- allows casing on arbitrary terms, here we choose to maintain the distinction

28+-- in order to allow for better optimisation opportunities.

29+--

17−data SC' t = Case Name [CaseAlt' t] -- ^ invariant: lowest tags first

30+data SC' t = Case Name [CaseAlt' t] -- ^ invariant: lowest tags first

18− | ProjCase t [CaseAlt' t] -- ^ special case for projections

31+ | ProjCase t [CaseAlt' t] -- ^ special case for projections/thunk-forcing before inspection

19 | STerm !t

32 | STerm !t

20 | UnmatchedCase String -- ^ error message

33 | UnmatchedCase String -- ^ error message

21 | ImpossibleCase -- ^ already checked to be impossible

34 | ImpossibleCase -- ^ already checked to be impossible

@@ -96,8 +109,7 @@ small n args t = let as = findAllUsedArgs t args in

96namesUsed :: SC -> [Name]

109namesUsed :: SC -> [Name]

97namesUsed sc = nub $ nu' [] sc where

110namesUsed sc = nub $ nu' [] sc where

98 nu' ps (Case n alts) = nub (concatMap (nua ps) alts) \\ [n]

111 nu' ps (Case n alts) = nub (concatMap (nua ps) alts) \\ [n]

99− nu' ps (ProjCase t alts) = nub $ (nut ps t ++

112+ nu' ps (ProjCase t alts) = nub $ nut ps t ++ concatMap (nua ps) alts

100− (concatMap (nua ps) alts))

101 nu' ps (STerm t) = nub $ nut ps t

113 nu' ps (STerm t) = nub $ nut ps t

102 nu' ps _ = []

114 nu' ps _ = []

103

115

@@ -122,7 +134,7 @@ namesUsed sc = nub $ nu' [] sc where

122findCalls :: SC -> [Name] -> [(Name, [[Name]])]

134findCalls :: SC -> [Name] -> [(Name, [[Name]])]

123findCalls sc topargs = nub $ nu' topargs sc where

135findCalls sc topargs = nub $ nu' topargs sc where

124 nu' ps (Case n alts) = nub (concatMap (nua (n : ps)) alts)

136 nu' ps (Case n alts) = nub (concatMap (nua (n : ps)) alts)

125− nu' ps (ProjCase t alts) = nub (nut ps t ++ concatMap (nua ps) alts)

137+ nu' ps (ProjCase t alts) = nub $ nut ps t ++ concatMap (nua ps) alts

126 nu' ps (STerm t) = nub $ nut ps t

138 nu' ps (STerm t) = nub $ nut ps t

127 nu' ps _ = []

139 nu' ps _ = []

128

140

@@ -192,10 +204,10 @@ data Phase = CompileTime | RunTime

192-- Work Right to Left

204-- Work Right to Left

193

205

194simpleCase :: Bool -> Bool -> Bool ->

206simpleCase :: Bool -> Bool -> Bool ->

195− Phase -> FC -> [Type] ->

207+ Phase -> FC -> [Int] -> [Type] ->

196 [([Name], Term, Term)] ->

208 [([Name], Term, Term)] ->

197 TC CaseDef

209 TC CaseDef

198−simpleCase tc cover reflect phase fc argtys cs

210+simpleCase tc cover reflect phase fc inacc argtys cs

199 = sc' tc cover phase fc (filter (\(_, _, r) ->

211 = sc' tc cover phase fc (filter (\(_, _, r) ->

200 case r of

212 case r of

201 Impossible -> False

213 Impossible -> False

@@ -213,7 +225,7 @@ simpleCase tc cover reflect phase fc argtys cs

213 OK pats ->

225 OK pats ->

214 let numargs = length (fst (head pats))

226 let numargs = length (fst (head pats))

215 ns = take numargs args

227 ns = take numargs args

216− (ns', ps') = order ns pats

228+ (ns', ps') = order [(n, i `elem` inacc) | (i,n) <- zip [0..] ns] pats

217 (tree, st) = runState

229 (tree, st) = runState

218 (match ns' ps' (defaultCase cover))

230 (match ns' ps' (defaultCase cover))

219 ([], numargs, [])

231 ([], numargs, [])

@@ -382,21 +394,25 @@ partition xs = error $ "Partition " ++ show xs

382-- reorder the patterns so that the one with most distinct names

394-- reorder the patterns so that the one with most distinct names

383-- comes next. Take rightmost first, otherwise (i.e. pick value rather

395-- comes next. Take rightmost first, otherwise (i.e. pick value rather

384-- than dependency)

396-- than dependency)

385−

397+--

398+-- The first argument means [(Name, IsInaccessible)].

399+

386−order :: [Name] -> [Clause] -> ([Name], [Clause])

400+order :: [(Name, Bool)] -> [Clause] -> ([Name], [Clause])

387−order [] cs = ([], cs)

401+order [] cs = ([], cs)

388−order ns [] = (ns, [])

402+order ns' [] = (map fst ns', [])

389−order ns cs = let patnames = transpose (map (zip ns) (map fst cs))

403+order ns' cs = let patnames = transpose (map (zip ns') (map fst cs))

404+ -- note: sortBy . reverse is not nonsense because sortBy is stable

390− pats' = transpose (sortBy moreDistinct (reverse patnames)) in

405+ pats' = transpose (sortBy moreDistinct (reverse patnames)) in

391− (getNOrder pats', zipWith rebuild pats' cs)

406+ (getNOrder pats', zipWith rebuild pats' cs)

392 where

407 where

393− getNOrder [] = error $ "Failed order on " ++ show (ns, cs)

408+ getNOrder [] = error $ "Failed order on " ++ show (map fst ns', cs)

394− getNOrder (c : _) = map fst c

409+ getNOrder (c : _) = map (fst . fst) c

395

410

396 rebuild patnames clause = (map snd patnames, snd clause)

411 rebuild patnames clause = (map snd patnames, snd clause)

397

412

413+ -- this compares (+isInaccessible, -numberOfCases)

398− moreDistinct xs ys = compare (numNames [] (map snd ys))

414+ moreDistinct xs ys = compare (snd . fst . head $ xs, numNames [] (map snd ys))

399− (numNames [] (map snd xs))

415+ (snd . fst . head $ ys, numNames [] (map snd xs))

400

416

401 numNames xs (PCon n _ _ : ps)

417 numNames xs (PCon n _ _ : ps)

402 | not (Left n `elem` xs) = numNames (Left n : xs) ps

418 | not (Left n `elem` xs) = numNames (Left n : xs) ps

@@ -576,91 +592,71 @@ depatt ns tm = dp [] tm

576-- FIXME: Do this for SucCase too

592-- FIXME: Do this for SucCase too

577prune :: Bool -- ^ Convert single branches to projections (only useful at runtime)

593prune :: Bool -- ^ Convert single branches to projections (only useful at runtime)

578 -> SC -> SC

594 -> SC -> SC

579−prune proj (Case n alts)

595+prune proj (Case n alts) = case alts' of

580− = let alts' = filter notErased (map pruneAlt alts) in

596+ [] -> ImpossibleCase

581− case alts' of

597+

582− [] -> ImpossibleCase

598+ -- Projection transformations prevent us from seeing some uses of ctor fields

583− as@(ConCase (UN delay) i [arg] sc : _)

599+ -- because they delete information about which ctor is being used.

584− | delay == txt "Delay"

600+ -- Consider:

585− -> if proj then mkForce n arg sc

601+ -- f (X x) = ... x ...

586− else Case n as

602+ -- vs.

603+ -- f x = ... x!0 ...

604+ --

605+ -- Hence, we disable this step.

606+ -- TODO: re-enable this in toIR

607+ --

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

608+ -- as@[ConCase cn i args sc]

588− else Case n as

609+ -- | proj -> mkProj n 0 args (prune proj sc)

610+ -- mkProj n i xs sc = foldr (\x -> projRep x n i) sc xs

611+

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

612+ [SucCase cn sc]

590− else Case n as

613+ | proj

614+ -> projRep cn n (-1) $ prune proj sc

615+

591− as@[ConstCase _ sc] -> prune proj sc

616+ [ConstCase _ sc]

617+ -> prune proj sc

618+

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

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

593− -- it gets caught first.

620+ -- it gets caught first.

594− [s@(SucCase _ _), DefaultCase dc]

621+ [s@(SucCase _ _), DefaultCase dc]

595− -> Case n [ConstCase (BI 0) dc, s]

622+ -> Case n [ConstCase (BI 0) dc, s]

623+

596− as -> Case n as

624+ as -> Case n as

625+ where

626+ alts' = filter (not . erased) $ map pruneAlt alts

627+

597− where pruneAlt (ConCase cn i ns sc) = ConCase cn i ns (prune proj sc)

628+ pruneAlt (ConCase cn i ns sc) = ConCase cn i ns (prune proj sc)

598− pruneAlt (FnCase cn ns sc) = FnCase cn ns (prune proj sc)

629+ pruneAlt (FnCase cn ns sc) = FnCase cn ns (prune proj sc)

599− pruneAlt (ConstCase c sc) = ConstCase c (prune proj sc)

630+ pruneAlt (ConstCase c sc) = ConstCase c (prune proj sc)

600− pruneAlt (SucCase n sc) = SucCase n (prune proj sc)

631+ pruneAlt (SucCase n sc) = SucCase n (prune proj sc)

601− pruneAlt (DefaultCase sc) = DefaultCase (prune proj sc)

632+ pruneAlt (DefaultCase sc) = DefaultCase (prune proj sc)

602−

633+

603− notErased (DefaultCase (STerm Erased)) = False

634+ erased (DefaultCase (STerm Erased)) = True

604− notErased (DefaultCase ImpossibleCase) = False

635+ erased (DefaultCase ImpossibleCase) = True

605− notErased _ = True

636+ erased _ = False

606−

637+

607− mkForce n arg (Case x alts)

608− | x == arg = ProjCase (forceArg n)

609− (map (mkForceAlt n arg) alts)

610− | otherwise = Case x (map (mkForceAlt n arg) alts)

611− mkForce n arg (ProjCase t alts)

612− = ProjCase (forceTm n arg t) (map (mkForceAlt n arg) alts)

613− mkForce n arg (STerm t) = STerm (forceTm n arg t)

614− mkForce n arg c = c

615−

616− mkForceAlt n arg (ConCase cn t args rhs)

617− = ConCase cn t args (mkForce n arg rhs)

618− mkForceAlt n arg (FnCase cn args rhs)

619− = FnCase cn args (mkForce n arg rhs)

620− mkForceAlt n arg (ConstCase t rhs)

621− = ConstCase t (mkForce n arg rhs)

622− mkForceAlt n arg (SucCase sn rhs)

623− = SucCase sn (mkForce n arg rhs)

624− mkForceAlt n arg (DefaultCase rhs)

625− = DefaultCase (mkForce n arg rhs)

626−

627− forceTm n arg t = subst arg (forceArg n) t

628−

629− forceArg n = App (App (App (P Ref (sUN "Force") Erased) Erased) Erased)

630− (P Bound n Erased)

631−

632− mkProj n i [] sc = prune proj sc

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

634−

635− -- Change every 'n' in sc to 'n-1'

636−-- mkProjS n cn sc = prune proj (fmap projn sc) where

637−-- projn pn@(P _ n' _)

638−-- | cn == n' = App (App (P Ref (UN "prim__subBigInt") Erased)

639−-- (P Bound n Erased)) (Constant (BI 1))

640−-- projn t = t

641−

642− projRep :: Name -> Name -> Int -> SC -> SC

638+ projRep :: Name -> Name -> Int -> SC -> SC

643− projRep arg n i (Case x alts)

639+ projRep arg n i (Case x alts) | x == arg

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

640+ = ProjCase (Proj (P Bound n Erased) i) $ map (projRepAlt arg n i) alts

645− (map (projRepAlt arg n i) alts)

641+ projRep arg n i (Case x alts)

646− | otherwise = Case x (map (projRepAlt arg n i) alts)

642+ = Case x (map (projRepAlt arg n i) alts)

647− projRep arg n i (ProjCase t alts)

643+ projRep arg n i (ProjCase t alts)

648− = ProjCase (projRepTm arg n i t) (map (projRepAlt arg n i) alts)

644+ = ProjCase (projRepTm arg n i t) $ map (projRepAlt arg n i) alts

649− projRep arg n i (STerm t) = STerm (projRepTm arg n i t)

645+ projRep arg n i (STerm t) = STerm (projRepTm arg n i t)

650− projRep arg n i c = c -- unmatched

646+ projRep arg n i c = c

651−

647+

652− projRepAlt arg n i (ConCase cn t args rhs)

648+ projRepAlt arg n i (ConCase cn t args rhs)

653− = ConCase cn t args (projRep arg n i rhs)

649+ = ConCase cn t args (projRep arg n i rhs)

654− projRepAlt arg n i (FnCase cn args rhs)

650+ projRepAlt arg n i (FnCase cn args rhs)

655− = FnCase cn args (projRep arg n i rhs)

651+ = FnCase cn args (projRep arg n i rhs)

656− projRepAlt arg n i (ConstCase t rhs)

652+ projRepAlt arg n i (ConstCase t rhs)

657− = ConstCase t (projRep arg n i rhs)

653+ = ConstCase t (projRep arg n i rhs)

658− projRepAlt arg n i (SucCase sn rhs)

654+ projRepAlt arg n i (SucCase sn rhs)

659− = SucCase sn (projRep arg n i rhs)

655+ = SucCase sn (projRep arg n i rhs)

660− projRepAlt arg n i (DefaultCase rhs)

656+ projRepAlt arg n i (DefaultCase rhs)

661− = DefaultCase (projRep arg n i rhs)

657+ = DefaultCase (projRep arg n i rhs)

662−

658+

663− projRepTm arg n i t = subst arg (Proj (P Bound n Erased) i) t

659+ projRepTm arg n i t = subst arg (Proj (P Bound n Erased) i) t

664

660

665prune _ t = t

661prune _ t = t

666

662

@@ -669,6 +665,49 @@ stripLambdas (CaseDef ns (STerm (Bind x (Lam _) sc)) tm)

669 = stripLambdas (CaseDef (ns ++ [x]) (STerm (instantiate (P Bound x Erased) sc)) tm)

665 = stripLambdas (CaseDef (ns ++ [x]) (STerm (instantiate (P Bound x Erased) sc)) tm)

670stripLambdas x = x

666stripLambdas x = x

671

667

668+substSC :: Name -> Name -> SC -> SC

669+substSC n repl (Case n' alts)

670+ | n == n' = Case repl (map (substAlt n repl) alts)

671+ | otherwise = Case n' (map (substAlt n repl) alts)

672+substSC n repl (STerm t) = STerm $ subst n (P Bound repl Erased) t

673+substSC n repl sc = error $ "unsupported in substSC: " ++ show sc

674+

675+substAlt :: Name -> Name -> CaseAlt -> CaseAlt

676+substAlt n repl (ConCase cn a ns sc) = ConCase cn a ns (substSC n repl sc)

677+substAlt n repl (FnCase fn ns sc) = FnCase fn ns (substSC n repl sc)

678+substAlt n repl (ConstCase c sc) = ConstCase c (substSC n repl sc)

679+substAlt n repl (SucCase n' sc)

680+ | n == n' = SucCase n (substSC n repl sc)

681+ | otherwise = SucCase n' (substSC n repl sc)

682+substAlt n repl (DefaultCase sc) = DefaultCase (substSC n repl sc)

683+

684+mkForce :: Name -> Name -> SC -> SC

685+mkForce = mkForceSC

686+ where

687+ mkForceSC n arg (Case x alts) | x == arg

688+ = ProjCase (forceArg n) $ map (mkForceAlt n arg) alts

689+

690+ mkForceSC n arg (Case x alts)

691+ = Case x (map (mkForceAlt n arg) alts)

692+

693+ mkForceSC n arg (ProjCase t alts)

694+ = ProjCase (forceTm n arg t) $ map (mkForceAlt n arg) alts

695+

696+ mkForceSC n arg (STerm t) = STerm (forceTm n arg t)

697+ mkForceSC n arg c = c

672

698

699+ mkForceAlt n arg (ConCase cn t args rhs)

700+ = ConCase cn t args (mkForceSC n arg rhs)

701+ mkForceAlt n arg (FnCase cn args rhs)

702+ = FnCase cn args (mkForceSC n arg rhs)

703+ mkForceAlt n arg (ConstCase t rhs)

704+ = ConstCase t (mkForceSC n arg rhs)

705+ mkForceAlt n arg (SucCase sn rhs)

706+ = SucCase sn (mkForceSC n arg rhs)

707+ mkForceAlt n arg (DefaultCase rhs)

708+ = DefaultCase (mkForceSC n arg rhs)

673

709

710+ forceTm n arg t = subst arg (forceArg n) t

674

711

712+ forceArg n = App (App (App (P Ref (sUN "Force") Erased) Erased) Erased)

713+ (P Bound n Erased)

src/Idris/Core/Evaluate.hs+14−9

@@ -8,12 +8,13 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,

8 Context, initContext, ctxtAlist, uconstraints, next_tvar,

9 addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,

10 addDatatype, addCasedef, simplifyCasedef, addOperator,

11− lookupNames, lookupTy, lookupP, lookupDef, lookupDefAcc, lookupVal,

11+ lookupNames, lookupTy, lookupP, lookupDef, lookupDefExact, lookupDefAcc, lookupVal,

12 mapDefCtxt,

13 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isDConName, isTConName, isConName, isFnName,

14− Value(..), Quote(..), initEval, uniqueNameCtxt) where

14+ Value(..), Quote(..), initEval, uniqueNameCtxt, definitions) where

15

16import Debug.Trace

17+import Control.Applicative hiding (Const)

17import Control.Monad.State -- not Strict!

18import Control.Monad.State -- not Strict!

18import qualified Data.Binary as B

19import qualified Data.Binary as B

19import Data.Binary hiding (get, put)

20import Data.Binary hiding (get, put)

@@ -784,6 +785,7 @@ addDatatype (Data n tag ty cons) uctxt

784-- FIXME: Too many arguments! Refactor all these Bools.

785-- FIXME: Too many arguments! Refactor all these Bools.

785addCasedef :: Name -> CaseInfo -> Bool -> Bool -> Bool -> Bool ->

786addCasedef :: Name -> CaseInfo -> Bool -> Bool -> Bool -> Bool ->

786 [Type] -> -- argument types

787 [Type] -> -- argument types

788+ [Int] -> -- inaccessible arguments

787 [Either Term (Term, Term)] ->

789 [Either Term (Term, Term)] ->

788 [([Name], Term, Term)] -> -- totality

790 [([Name], Term, Term)] -> -- totality

789 [([Name], Term, Term)] -> -- compile time

791 [([Name], Term, Term)] -> -- compile time

@@ -791,16 +793,16 @@ addCasedef :: Name -> CaseInfo -> Bool -> Bool -> Bool -> Bool ->

791 [([Name], Term, Term)] -> -- run time

793 [([Name], Term, Term)] -> -- run time

792 Type -> Context -> Context

794 Type -> Context -> Context

793addCasedef n ci@(CaseInfo alwaysInline tcdict)

795addCasedef n ci@(CaseInfo alwaysInline tcdict)

794− tcase covering reflect asserted argtys

796+ tcase covering reflect asserted argtys inacc

795 ps_in ps_tot ps_inl ps_ct ps_rt ty uctxt

797 ps_in ps_tot ps_inl ps_ct ps_rt ty uctxt

796 = let ctxt = definitions uctxt

798 = let ctxt = definitions uctxt

797 access = case lookupDefAcc n False uctxt of

799 access = case lookupDefAcc n False uctxt of

798 [(_, acc)] -> acc

800 [(_, acc)] -> acc

799 _ -> Public

801 _ -> Public

800− ctxt' = case (simpleCase tcase covering reflect CompileTime emptyFC argtys ps_tot,

802+ ctxt' = case (simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_tot,

801− simpleCase tcase covering reflect CompileTime emptyFC argtys ps_ct,

803+ simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_ct,

802− simpleCase tcase covering reflect CompileTime emptyFC argtys ps_inl,

804+ simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_inl,

803− simpleCase tcase covering reflect RunTime emptyFC argtys ps_rt) of

805+ simpleCase tcase covering reflect RunTime emptyFC inacc argtys ps_rt) of

804 (OK (CaseDef args_tot sc_tot _),

806 (OK (CaseDef args_tot sc_tot _),

805 OK (CaseDef args_ct sc_ct _),

807 OK (CaseDef args_ct sc_ct _),

806 OK (CaseDef args_inl sc_inl _),

808 OK (CaseDef args_inl sc_inl _),

@@ -827,7 +829,7 @@ simplifyCasedef n uctxt

827 [(CaseOp ci ty atys ps_in ps cd, acc, tot, metainf)] ->

829 [(CaseOp ci ty atys ps_in ps cd, acc, tot, metainf)] ->

828 let ps_in' = map simpl ps_in

830 let ps_in' = map simpl ps_in

829 pdef = map debind ps_in' in

831 pdef = map debind ps_in' in

830− case simpleCase False True False CompileTime emptyFC atys pdef of

832+ case simpleCase False True False CompileTime emptyFC [] atys pdef of

831 OK (CaseDef args sc _) ->

833 OK (CaseDef args sc _) ->

832 addDef n (CaseOp ci

834 addDef n (CaseOp ci

833 ty atys ps_in' ps (cd { cases_totcheck = (args, sc) }),

835 ty atys ps_in' ps (cd { cases_totcheck = (args, sc) }),

@@ -908,8 +910,11 @@ lookupP n ctxt

908 Hidden -> []

910 Hidden -> []

909 _ -> return (fst p)

911 _ -> return (fst p)

910

912

913+lookupDefExact :: Name -> Context -> Maybe Def

914+lookupDefExact n ctxt = tfst <$> lookupCtxtExact n (definitions ctxt)

915+

911lookupDef :: Name -> Context -> [Def]

916lookupDef :: Name -> Context -> [Def]

912−lookupDef n ctxt = map tfst $ lookupCtxt n (definitions ctxt)

917+lookupDef n ctxt = tfst <$> lookupCtxt n (definitions ctxt)

913

918

914lookupDefAcc :: Name -> Bool -> Context ->

919lookupDefAcc :: Name -> Bool -> Context ->

915 [(Def, Accessibility)]

920 [(Def, Accessibility)]

src/Idris/Core/Execute.hs+96−135

@@ -47,11 +47,8 @@ readMay s = case reads s of

47

48data Lazy = Delayed ExecEnv Context Term | Forced ExecVal deriving Show

49

50−data ExecState = ExecState { exec_thunks :: M.Map Int Lazy -- ^ Thunks - the result of evaluating "lazy" or calling lazy funcs

51− , exec_next_thunk :: Int -- ^ Ensure thunk key uniqueness

52− , exec_implicits :: Ctxt [PArg] -- ^ Necessary info on laziness from idris monad

53− , exec_dynamic_libs :: [DynamicLib] -- ^ Dynamic libs from idris monad

50+newtype ExecState = ExecState { exec_dynamic_libs :: [DynamicLib] -- ^ Dynamic libs from idris monad

54− }

51+ }

55

52

56data ExecVal = EP NameType Name ExecVal

53data ExecVal = EP NameType Name ExecVal

57 | EV Int

54 | EV Int

@@ -61,20 +58,20 @@ data ExecVal = EP NameType Name ExecVal

61 | EErased

58 | EErased

62 | EConstant Const

59 | EConstant Const

63 | forall a. EPtr (Ptr a)

60 | forall a. EPtr (Ptr a)

64− | EThunk Int

61+ | EThunk Context ExecEnv Term

65 | EHandle Handle

62 | EHandle Handle

66

63

67instance Show ExecVal where

64instance Show ExecVal where

68− show (EP _ n _) = show n

65+ show (EP _ n _) = show n

69− show (EV i) = "!!V" ++ show i ++ "!!"

66+ show (EV i) = "!!V" ++ show i ++ "!!"

70− show (EBind n b body) = "EBind " ++ show b ++ " <<fn>>"

67+ show (EBind n b body) = "EBind " ++ show b ++ " <<fn>>"

71− show (EApp e1 e2) = show e1 ++ " (" ++ show e2 ++ ")"

68+ show (EApp e1 e2) = show e1 ++ " (" ++ show e2 ++ ")"

72− show (EType _) = "Type"

69+ show (EType _) = "Type"

73− show EErased = "[__]"

70+ show EErased = "[__]"

74− show (EConstant c) = show c

71+ show (EConstant c) = show c

75− show (EPtr p) = "<<ptr " ++ show p ++ ">>"

72+ show (EPtr p) = "<<ptr " ++ show p ++ ">>"

76− show (EThunk i) = "<<thunk " ++ show i ++ ">>"

73+ show (EThunk _ env tm) = "<<thunk " ++ show env ++ "||||" ++ show tm ++ ">>"

77− show (EHandle h) = "<<handle " ++ show h ++ ">>"

74+ show (EHandle h) = "<<handle " ++ show h ++ ">>"

78

75

79toTT :: ExecVal -> Exec Term

76toTT :: ExecVal -> Exec Term

80toTT (EP nt n ty) = (P nt n) <$> (toTT ty)

77toTT (EP nt n ty) = (P nt n) <$> (toTT ty)

@@ -82,22 +79,25 @@ toTT (EV i) = return $ V i

82toTT (EBind n b body) = do body' <- body $ EP Bound n EErased

79toTT (EBind n b body) = do body' <- body $ EP Bound n EErased

83 b' <- fixBinder b

80 b' <- fixBinder b

84 Bind n b' <$> toTT body'

81 Bind n b' <$> toTT body'

85− where fixBinder (Lam t) = Lam <$> toTT t

82+ where fixBinder (Lam t) = Lam <$> toTT t

86− fixBinder (Pi t) = Pi <$> toTT t

83+ fixBinder (Pi t) = Pi <$> toTT t

87− fixBinder (Let t1 t2) = Let <$> toTT t1 <*> toTT t2

84+ fixBinder (Let t1 t2) = Let <$> toTT t1 <*> toTT t2

88− fixBinder (NLet t1 t2) = NLet <$> toTT t1 <*> toTT t2

85+ fixBinder (NLet t1 t2) = NLet <$> toTT t1 <*> toTT t2

89− fixBinder (Hole t) = Hole <$> toTT t

86+ fixBinder (Hole t) = Hole <$> toTT t

90 fixBinder (GHole i t) = GHole i <$> toTT t

87 fixBinder (GHole i t) = GHole i <$> toTT t

91− fixBinder (Guess t1 t2) = Guess <$> toTT t1 <*> toTT t2

88+ fixBinder (Guess t1 t2) = Guess <$> toTT t1 <*> toTT t2

92− fixBinder (PVar t) = PVar <$> toTT t

89+ fixBinder (PVar t) = PVar <$> toTT t

93− fixBinder (PVTy t) = PVTy <$> toTT t

90+ fixBinder (PVTy t) = PVTy <$> toTT t

94toTT (EApp e1 e2) = do e1' <- toTT e1

91toTT (EApp e1 e2) = do e1' <- toTT e1

95 e2' <- toTT e2

92 e2' <- toTT e2

96 return $ App e1' e2'

93 return $ App e1' e2'

97toTT (EType u) = return $ TType u

94toTT (EType u) = return $ TType u

98toTT EErased = return Erased

95toTT EErased = return Erased

99toTT (EConstant c) = return (Constant c)

96toTT (EConstant c) = return (Constant c)

100−toTT (EThunk i) = return (P (DCon 0 0) (sMN i "THUNK") Erased) --(force i) >>= toTT

97+toTT (EThunk ctxt env tm) = do env' <- mapM toBinder env

98+ return $ normalise ctxt env' tm

99+ where toBinder (n, v) = do v' <- toTT v

100+ return (n, Let Erased v')

101toTT (EHandle _) = return Erased

102

103unApplyV :: ExecVal -> (ExecVal, [ExecVal])

@@ -111,7 +111,7 @@ mkEApp f (a:args) = mkEApp (EApp f a) args

111

112initState :: Idris ExecState

113initState = do ist <- getIState

114− return $ ExecState M.empty 0 (idris_implicits ist) (idris_dynamic_libs ist)

114+ return $ ExecState (idris_dynamic_libs ist)

115

116type Exec = ErrorT String (StateT ExecState IO)

117

@@ -130,45 +130,13 @@ execFail = throwError

130execIO :: IO a -> Exec a

131execIO = lift . lift

132

133−delay :: ExecEnv -> Context -> Term -> Exec ExecVal

134−delay env ctxt tm =

135− do st <- getExecState

136− let i = exec_next_thunk st

137− putExecState $ st { exec_thunks = M.insert i (Delayed env ctxt tm) (exec_thunks st)

138− , exec_next_thunk = exec_next_thunk st + 1

139− }

140− return $ EThunk i

141−

142−force :: Int -> Exec ExecVal

143−force i = do st <- getExecState

144− case M.lookup i (exec_thunks st) of

145− Just (Delayed env ctxt tm) -> do tm' <- doExec env ctxt tm

146− case tm' of

147− EThunk i ->

148− do res <- force i

149− update res i

150− return res

151− _ -> do update tm' i

152− return tm'

153− Just (Forced tm) -> return tm

154− Nothing -> execFail "Tried to exec non-existing thunk. This is a bug!"

155− where update :: ExecVal -> Int -> Exec ()

156− update tm i = do est <- getExecState

157− putExecState $ est { exec_thunks = M.insert i (Forced tm) (exec_thunks est) }

158−

159−tryForce :: ExecVal -> Exec ExecVal

160−tryForce (EThunk i) = force i

161−tryForce tm = return tm

162−

163−debugThunks :: Exec ()

164−debugThunks = do st <- getExecState

165− execIO $ putStrLn (take 4000 (show (exec_thunks st)))

166

133

167execute :: Term -> Idris Term

134execute :: Term -> Idris Term

168execute tm = do est <- initState

135execute tm = do est <- initState

169 ctxt <- getContext

136 ctxt <- getContext

170− res <- lift . lift $ flip runExec est $ do res <- doExec [] ctxt tm

137+ res <- lift . lift . flip runExec est $

138+ do res <- doExec [] ctxt tm

171− toTT res

139+ toTT res

172 case res of

140 case res of

173 Left err -> fail err

141 Left err -> fail err

174 Right tm' -> return tm'

142 Right tm' -> return tm'

@@ -208,7 +176,18 @@ doExec env ctxt (Bind n (NLet t v) body) = trace "NLet" $ undefined

208doExec env ctxt tm@(Bind n b body) = return $

176doExec env ctxt tm@(Bind n b body) = return $

209 EBind n (fmap (\_->EErased) b)

177 EBind n (fmap (\_->EErased) b)

210 (\arg -> doExec ((n, arg):env) ctxt body)

178 (\arg -> doExec ((n, arg):env) ctxt body)

211−doExec env ctxt a@(App _ _) = execApp env ctxt (unApply a)

179+doExec env ctxt a@(App _ _) =

180+ do let (f, args) = unApply a

181+ f' <- doExec env ctxt f

182+ args' <- case f' of

183+ (EP _ d _) | d == delay ->

184+ case args of

185+ [t,a,tm] -> do t' <- doExec env ctxt t

186+ a' <- doExec env ctxt a

187+ return [t', a', EThunk ctxt env tm]

188+ _ -> mapM (doExec env ctxt) args -- partial applications are fine to evaluate

189+ fun' -> do mapM (doExec env ctxt) args

190+ execApp env ctxt f' args'

212doExec env ctxt (Constant c) = return (EConstant c)

191doExec env ctxt (Constant c) = return (EConstant c)

213doExec env ctxt (Proj tm i) = let (x, xs) = unApply tm in

192doExec env ctxt (Proj tm i) = let (x, xs) = unApply tm in

214 doExec env ctxt ((x:xs) !! i)

193 doExec env ctxt ((x:xs) !! i)

@@ -216,55 +195,38 @@ doExec env ctxt Erased = return EErased

216doExec env ctxt Impossible = fail "Tried to execute an impossible case"

195doExec env ctxt Impossible = fail "Tried to execute an impossible case"

217doExec env ctxt (TType u) = return (EType u)

196doExec env ctxt (TType u) = return (EType u)

218

197

219−execApp :: ExecEnv -> Context -> (Term, [Term]) -> Exec ExecVal

198+execApp :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal

220−execApp env ctxt (f, args) = do newF <- doExec env ctxt f

221− laziness <- (++ repeat False) <$> (getLaziness newF)

222− newArgs <- mapM argExec (zip args laziness)

223− res <- execApp' env ctxt newF newArgs

224− return res

225− where getLaziness (EP _ l _) | l == sUN "lazy" = return [False, True]

226− getLaziness (EP _ n _) = do est <- getExecState

227− let argInfo = exec_implicits est

228− case lookupCtxtName n argInfo of

229− [] -> return (repeat False)

230− [ps] -> return $ map lazyarg (snd ps)

231− many -> execFail $ "Ambiguous " ++ show n ++ ", found " ++ (take 200 $ show many)

232− getLaziness _ = return (repeat False) -- ok due to zip above

233− argExec :: (Term, Bool) -> Exec ExecVal

234− argExec (tm, False) = doExec env ctxt tm

235− argExec (tm, True) = delay env ctxt tm

236−

237−

238−execApp' :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal

239−execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls

199+execApp env ctxt v [] = return v -- no args is just a constant! can result from function calls

200+execApp env ctxt (EP _ f _) (t:a:delayed:rest)

201+ | f == force

202+ , (_, [_, _, EThunk tmCtxt tmEnv tm]) <- unApplyV delayed =

203+ do tm' <- doExec tmEnv tmCtxt tm

204+ execApp env ctxt tm' rest

240−execApp' env ctxt (EP _ fp _) (ty:action:rest)

205+execApp env ctxt (EP _ fp _) (ty:action:rest)

241 | fp == upio,

206 | fp == upio,

242 (prim__IO, [_, v]) <- unApplyV action

207 (prim__IO, [_, v]) <- unApplyV action

243− = execApp' env ctxt v rest

208+ = execApp env ctxt v rest

244

209

245−execApp' env ctxt (EP _ fp _) args@(_:_:v:k:rest)

210+execApp env ctxt (EP _ fp _) args@(_:_:v:k:rest)

246 | fp == piobind,

211 | fp == piobind,

247 (prim__IO, [_, v']) <- unApplyV v =

212 (prim__IO, [_, v']) <- unApplyV v =

248− do v'' <- tryForce v'

249− res <- execApp' env ctxt k [v''] >>= tryForce

213+ do res <- execApp env ctxt k [v']

250− execApp' env ctxt res rest

214+ execApp env ctxt res rest

251−execApp' env ctxt con@(EP _ fp _) args@(tp:v:rest)

215+execApp env ctxt con@(EP _ fp _) args@(tp:v:rest)

252− | fp == pioret =

253− do v' <- tryForce v

254− execApp' env ctxt (mkEApp con [tp, v']) rest

216+ | fp == pioret = execApp env ctxt (mkEApp con [tp, v]) rest

255

217

256-- Special cases arising from not having access to the C RTS in the interpreter

218-- Special cases arising from not having access to the C RTS in the interpreter

257−execApp' env ctxt (EP _ fp _) (_:fn:EConstant (Str arg):_:rest)

219+execApp env ctxt (EP _ fp _) (_:fn:EConstant (Str arg):_:rest)

258 | fp == mkfprim,

220 | fp == mkfprim,

259 Just (FFun "putStr" _ _) <- foreignFromTT fn

221 Just (FFun "putStr" _ _) <- foreignFromTT fn

260 = do execIO (putStr arg)

222 = do execIO (putStr arg)

261− execApp' env ctxt ioUnit rest

223+ execApp env ctxt ioUnit rest

262−execApp' env ctxt (EP _ fp _) (_:fn:_:EHandle h:_:rest)

224+execApp env ctxt (EP _ fp _) (_:fn:_:EHandle h:_:rest)

263 | fp == mkfprim,

225 | fp == mkfprim,

264 Just (FFun "idris_readStr" _ _) <- foreignFromTT fn

226 Just (FFun "idris_readStr" _ _) <- foreignFromTT fn

265 = do contents <- execIO $ hGetLine h

227 = do contents <- execIO $ hGetLine h

266− execApp' env ctxt (EConstant (Str (contents ++ "\n"))) rest

228+ execApp env ctxt (EConstant (Str (contents ++ "\n"))) rest

267−execApp' env ctxt (EP _ fp _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)

229+execApp env ctxt (EP _ fp _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)

268 | fp == mkfprim,

230 | fp == mkfprim,

269 Just (FFun "fileOpen" _ _) <- foreignFromTT fn

231 Just (FFun "fileOpen" _ _) <- foreignFromTT fn

270 = do f <- execIO $

232 = do f <- execIO $

@@ -283,53 +245,53 @@ execApp' env ctxt (EP _ fp _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)

283 in return $ Right (ioWrap (EPtr nullPtr), tail rest))

245 in return $ Right (ioWrap (EPtr nullPtr), tail rest))

284 case f of

246 case f of

285 Left err -> execFail err

247 Left err -> execFail err

286− Right (res, rest) -> execApp' env ctxt res rest

248+ Right (res, rest) -> execApp env ctxt res rest

287

249

288−execApp' env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)

250+execApp env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)

289 | fp == mkfprim,

251 | fp == mkfprim,

290 Just (FFun "fileEOF" _ _) <- foreignFromTT fn

252 Just (FFun "fileEOF" _ _) <- foreignFromTT fn

291 = do eofp <- execIO $ hIsEOF h

253 = do eofp <- execIO $ hIsEOF h

292 let res = ioWrap (EConstant (I $ if eofp then 1 else 0))

254 let res = ioWrap (EConstant (I $ if eofp then 1 else 0))

293− execApp' env ctxt res (tail rest)

255+ execApp env ctxt res (tail rest)

294

256

295−execApp' env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)

257+execApp env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)

296 | fp == mkfprim,

258 | fp == mkfprim,

297 Just (FFun "fileClose" _ _) <- foreignFromTT fn

259 Just (FFun "fileClose" _ _) <- foreignFromTT fn

298 = do execIO $ hClose h

260 = do execIO $ hClose h

299− execApp' env ctxt ioUnit (tail rest)

261+ execApp env ctxt ioUnit (tail rest)

300

262

301−execApp' env ctxt (EP _ fp _) (_:fn:(EPtr p):rest)

263+execApp env ctxt (EP _ fp _) (_:fn:(EPtr p):rest)

302 | fp == mkfprim,

264 | fp == mkfprim,

303 Just (FFun "isNull" _ _) <- foreignFromTT fn

265 Just (FFun "isNull" _ _) <- foreignFromTT fn

304 = let res = ioWrap . EConstant . I $

266 = let res = ioWrap . EConstant . I $

305 if p == nullPtr then 1 else 0

267 if p == nullPtr then 1 else 0

306− in execApp' env ctxt res (tail rest)

268+ in execApp env ctxt res (tail rest)

307

269

308-- Handles will be checked as null pointers sometimes - but if we got a

270-- Handles will be checked as null pointers sometimes - but if we got a

309-- real Handle, then it's valid, so just return 1.

271-- real Handle, then it's valid, so just return 1.

310−execApp' env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)

272+execApp env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)

311 | fp == mkfprim,

273 | fp == mkfprim,

312 Just (FFun "isNull" _ _) <- foreignFromTT fn

274 Just (FFun "isNull" _ _) <- foreignFromTT fn

313 = let res = ioWrap . EConstant . I $ 0

275 = let res = ioWrap . EConstant . I $ 0

314− in execApp' env ctxt res (tail rest)

276+ in execApp env ctxt res (tail rest)

315

277

316-- A foreign-returned char* has to be tested for NULL sometimes

278-- A foreign-returned char* has to be tested for NULL sometimes

317−execApp' env ctxt (EP _ fp _) (_:fn:EConstant (Str s):rest)

279+execApp env ctxt (EP _ fp _) (_:fn:EConstant (Str s):rest)

318 | fp == mkfprim,

280 | fp == mkfprim,

319 Just (FFun "isNull" _ _) <- foreignFromTT fn

281 Just (FFun "isNull" _ _) <- foreignFromTT fn

320 = let res = ioWrap . EConstant . I $ 0

282 = let res = ioWrap . EConstant . I $ 0

321− in execApp' env ctxt res (tail rest)

283+ in execApp env ctxt res (tail rest)

322

284

323-- Right now, there's no way to send command-line arguments to the executor,

285-- Right now, there's no way to send command-line arguments to the executor,

324-- so just return 0.

286-- so just return 0.

325−execApp' env ctxt (EP _ fp _) (_:fn:rest)

287+execApp env ctxt (EP _ fp _) (_:fn:rest)

326 | fp == mkfprim,

288 | fp == mkfprim,

327 Just (FFun "idris_numArgs" _ _) <- foreignFromTT fn

289 Just (FFun "idris_numArgs" _ _) <- foreignFromTT fn

328 = let res = ioWrap . EConstant . I $ 0

290 = let res = ioWrap . EConstant . I $ 0

329− in execApp' env ctxt res (tail rest)

291+ in execApp env ctxt res (tail rest)

330-- Throw away the 'World' argument to the foreign function

292-- Throw away the 'World' argument to the foreign function

331

293

332−execApp' env ctxt f@(EP _ fp _) args@(ty:fn:xs) | fp == mkfprim

294+execApp env ctxt f@(EP _ fp _) args@(ty:fn:xs) | fp == mkfprim

333 = case foreignFromTT fn of

295 = case foreignFromTT fn of

334 Just (FFun f argTs retT) | length xs >= length argTs ->

296 Just (FFun f argTs retT) | length xs >= length argTs ->

335 do let (args', xs') = (take (length argTs) xs, -- foreign args

297 do let (args', xs') = (take (length argTs) xs, -- foreign args

@@ -341,43 +303,41 @@ execApp' env ctxt f@(EP _ fp _) args@(ty:fn:xs) | fp == mkfprim

341 Just r -> return (mkEApp r xs')

303 Just r -> return (mkEApp r xs')

342 Nothing -> return (mkEApp f args)

304 Nothing -> return (mkEApp f args)

343

305

344−execApp' env ctxt c@(EP (DCon _ arity) n _) args =

306+execApp env ctxt c@(EP (DCon _ arity) n _) args =

345− do args' <- mapM tryForce (take arity args)

307+ do let args' = take arity args

346 let restArgs = drop arity args

308 let restArgs = drop arity args

347− execApp' env ctxt (mkEApp c args') restArgs

309+ execApp env ctxt (mkEApp c args') restArgs

348

310

349−execApp' env ctxt c@(EP (TCon _ arity) n _) args =

311+execApp env ctxt c@(EP (TCon _ arity) n _) args =

350− do args' <- mapM tryForce (take arity args)

312+ do let args' = take arity args

351 let restArgs = drop arity args

313 let restArgs = drop arity args

352− execApp' env ctxt (mkEApp c args') restArgs

314+ execApp env ctxt (mkEApp c args') restArgs

353

315

354−execApp' env ctxt f@(EP _ n _) args =

316+execApp env ctxt f@(EP _ n _) args =

355 do let val = lookupDef n ctxt

317 do let val = lookupDef n ctxt

356 case val of

318 case val of

357 [Function _ tm] -> fail "should already have been eval'd"

319 [Function _ tm] -> fail "should already have been eval'd"

358 [TyDecl nt ty] -> return $ mkEApp f args

320 [TyDecl nt ty] -> return $ mkEApp f args

359 [Operator tp arity op] ->

321 [Operator tp arity op] ->

360 if length args >= arity

322 if length args >= arity

361− then do args' <- mapM tryForce $ take arity args

323+ then let args' = take arity args in

362− case getOp n args' of

324+ case getOp n args' of

363− Just res -> do r <- res

325+ Just res -> do r <- res

364− execApp' env ctxt r (drop arity args)

326+ execApp env ctxt r (drop arity args)

365− Nothing -> return (mkEApp f args)

327+ Nothing -> return (mkEApp f args)

366 else return (mkEApp f args)

328 else return (mkEApp f args)

367 [CaseOp _ _ _ _ _ (CaseDefs _ ([], STerm tm) _ _)] -> -- nullary fun

329 [CaseOp _ _ _ _ _ (CaseDefs _ ([], STerm tm) _ _)] -> -- nullary fun

368 do rhs <- doExec env ctxt tm

330 do rhs <- doExec env ctxt tm

369− execApp' env ctxt rhs args

331+ execApp env ctxt rhs args

370 [CaseOp _ _ _ _ _ (CaseDefs _ (ns, sc) _ _)] ->

332 [CaseOp _ _ _ _ _ (CaseDefs _ (ns, sc) _ _)] ->

371 do res <- execCase env ctxt ns sc args

333 do res <- execCase env ctxt ns sc args

372 return $ fromMaybe (mkEApp f args) res

334 return $ fromMaybe (mkEApp f args) res

373 thing -> return $ mkEApp f args

335 thing -> return $ mkEApp f args

374−execApp' env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg

336+execApp env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg

375− let (f', as) = unApplyV ret

337+ let (f', as) = unApplyV ret

376− execApp' env ctxt f' (as ++ args)

338+ execApp env ctxt f' (as ++ args)

377−execApp' env ctxt (EThunk i) args = do f <- force i

378− execApp' env ctxt f args

379−execApp' env ctxt app@(EApp _ _) args2 | (f, args1) <- unApplyV app = execApp' env ctxt f (args1 ++ args2)

339+execApp env ctxt app@(EApp _ _) args2 | (f, args1) <- unApplyV app = execApp env ctxt f (args1 ++ args2)

380−execApp' env ctxt f args = return (mkEApp f args)

340+execApp env ctxt f args = return (mkEApp f args)

381

341

382prs = sUN "prim__readString"

342prs = sUN "prim__readString"

383pbm = sUN "prim__believe_me"

343pbm = sUN "prim__believe_me"

@@ -386,6 +346,8 @@ mkfprim = sUN "mkForeignPrim"

386pioret = sUN "prim_io_return"

346pioret = sUN "prim_io_return"

387piobind = sUN "prim_io_bind"

347piobind = sUN "prim_io_bind"

388upio = sUN "unsafePerformPrimIO"

348upio = sUN "unsafePerformPrimIO"

349+delay = sUN "Delay"

350+force = sUN "Force"

389

351

390-- | Look up primitive operations in the global table and transform them into ExecVal functions

352-- | Look up primitive operations in the global table and transform them into ExecVal functions

391getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)

353getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)

@@ -426,7 +388,7 @@ execCase env ctxt ns sc args =

426-- trace ("Case " ++ show sc ++ "\n in " ++ show amap ++"\n in env " ++ show env ++ "\n\n" ) $ return ()

388-- trace ("Case " ++ show sc ++ "\n in " ++ show amap ++"\n in env " ++ show env ++ "\n\n" ) $ return ()

427 caseRes <- execCase' env ctxt amap sc

389 caseRes <- execCase' env ctxt amap sc

428 case caseRes of

390 case caseRes of

429− Just res -> Just <$> execApp' (map (\(n, tm) -> (n, tm)) amap ++ env) ctxt res (drop arity args)

391+ Just res -> Just <$> execApp (map (\(n, tm) -> (n, tm)) amap ++ env) ctxt res (drop arity args)

430 Nothing -> return Nothing

392 Nothing -> return Nothing

431 else return Nothing

393 else return Nothing

432

394

@@ -436,8 +398,7 @@ execCase' env ctxt amap (UnmatchedCase _) = return Nothing

436execCase' env ctxt amap (STerm tm) =

398execCase' env ctxt amap (STerm tm) =

437 Just <$> doExec (map (\(n, v) -> (n, v)) amap ++ env) ctxt tm

399 Just <$> doExec (map (\(n, v) -> (n, v)) amap ++ env) ctxt tm

438execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap =

400execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap =

439− do tm' <- tryForce tm

440− case chooseAlt tm' alts of

401+ case chooseAlt tm alts of

441 Just (newCase, newBindings) ->

402 Just (newCase, newBindings) ->

442 let amap' = newBindings ++ (filter (\(x,_) -> not (elem x (map fst newBindings))) amap) in

403 let amap' = newBindings ++ (filter (\(x,_) -> not (elem x (map fst newBindings))) amap) in

443 execCase' env ctxt amap' newCase

404 execCase' env ctxt amap' newCase

src/Idris/Coverage.hs+3−2

@@ -72,8 +72,9 @@ genClauses fc n xs given

72 -- there may be more case splitting that the idris_implicits record

73 -- suggests)

74 let parg = case lookupCtxt n (idris_implicits i) of

75+ (p : _) ->

75− (p : _) -> p ++ repeat (PExp 0 [] Placeholder)

76+ p ++ repeat (PExp 0 [] (sMN 0 "gcarg") Placeholder)

76− _ -> repeat (pexp Placeholder)

77+ _ -> repeat (pexp Placeholder)

77 let tryclauses = mkClauses parg all_args

78 let tryclauses = mkClauses parg all_args

78 logLvl 2 $ show (length tryclauses) ++ " initially to check"

79 logLvl 2 $ show (length tryclauses) ++ " initially to check"

79 logLvl 1 $ showSep "\n" (map (showTm i) tryclauses)

80 logLvl 1 $ showSep "\n" (map (showTm i) tryclauses)

src/Idris/DataOpts.hs+14−231

@@ -9,224 +9,48 @@ import Idris.AbsSyntaxTree

9import Idris.Core.TT

10

11import Control.Applicative

12−import qualified Data.IntMap as M

13import Data.List

12import Data.List

14import Data.Maybe

13import Data.Maybe

15import Debug.Trace

14import Debug.Trace

16

15

17−type ForceMap = M.IntMap Forceability

18−

19−-- Calculate the forceable arguments to a constructor

20−-- and update the set of optimisations.

21−forceArgs :: Name -> Name -> [Int] -> Type -> Idris ()

22−forceArgs typeName n expforce t = do

23− ist <- getIState

24− let fargs = getForcedArgs ist typeName t

25− copt = case lookupCtxt n (idris_optimisation ist) of

26− [] -> Optimise False False [] []

27− op:_ -> op

28− opts = addDef n (copt { forceable = M.toList fargs ++

29− zip expforce (repeat Unconditional) })

30− (idris_optimisation ist)

31− putIState (ist { idris_optimisation = opts })

32− addIBC (IBCOpt n)

33− iLOG $ "Forced: " ++ show n ++ " " ++ show fargs ++ "\n from " ++ show t

34−

35−getForcedArgs :: IState -> Name -> Type -> ForceMap

36−getForcedArgs ist typeName t = addCollapsibleArgs 0 t $ forcedInTarget 0 t

37− where

38− maxUnion = M.unionWith max

39−

40− -- Label all occurrences of the variable bound in Pi in the rest of

41− -- the term with the number i so that we can recognize them anytime later.

42− label i = instantiate $ P Bound (sMN i "ctor_arg") Erased

43−

44− addCollapsibleArgs :: Int -> Type -> ForceMap -> ForceMap

45− addCollapsibleArgs i (Bind vn (Pi ty) rest) alreadyForceable

46− = addCollapsibleArgs (i+1) (label i rest) (forceable $ unApply ty)

47− where

48− -- forceable takes an un-applied type of a ctor argument

49− forceable (P _ tn _, args)

50− -- if `ty' is collapsible, the argument is unconditionally forceable

51− | isCollapsible tn

52− = M.insert i Unconditional alreadyForceable

53−

54− -- a recursive occurrence with known indices is conditionally forceable

55− | tn == typeName

56− = M.insertWith max i Conditional alreadyForceable

57−

58− forceable _ = alreadyForceable

59−

60− isCollapsible :: Name -> Bool

61− isCollapsible n = case lookupCtxt n (idris_optimisation ist) of

62− [oi] -> collapsible oi

63− _ -> False

64−

65− addCollapsibleArgs _ _ fs = fs

66−

67− forcedInTarget :: Int -> Type -> ForceMap

68− forcedInTarget i (Bind _ (Pi _) rest) = forcedInTarget (i+1) (label i rest)

69− forcedInTarget i t@(App f a) | (_, as) <- unApply t = unionMap guardedArgs as

70− forcedInTarget _ _ = M.empty

71−

72− guardedArgs :: Term -> ForceMap

73− guardedArgs t@(App f a) | (P (DCon _ _) _ _, args) <- unApply t

74− = unionMap bareArg args `maxUnion` unionMap guardedArgs args

75− guardedArgs t = bareArg t

76−

77− bareArg :: Term -> ForceMap

78− bareArg (P _ (MN i ctor_arg) _)

79− | ctor_arg == txt "ctor_arg" = M.singleton i Unconditional

80− bareArg _ = M.empty

81−

82− unionMap :: (a -> ForceMap) -> [a] -> ForceMap

83− unionMap f = M.unionsWith max . map f

84−

85−-- Calculate whether a collection of constructors is collapsible

86−-- and update the state accordingly.

87−collapseCons :: Name -> [(Name, Type)] -> Idris ()

88−collapseCons tn ctors = do

89− ist <- getIState

90− case ctors of

91− _

92− | all (ctorCollapsible ist) ctors

93− , disjointTerms ctorTargetArgs

94− -> mapM_ setCollapsible (tn : map fst ctors)

95−

96− [(cn, ct)]

97− -> checkNewType ist cn ct

98−

99− _ -> return () -- nothing can be done

100− where

101− ctorTargetArgs = map (snd . unApply . getRetTy . snd) ctors

102−

103− ctorArity :: Type -> Int

104− ctorArity = length . getArgTys

105−

106− ctorCollapsible :: IState -> (Name, Type) -> Bool

107− ctorCollapsible ist (n, t) = all (`M.member` forceMap) [0 .. ctorArity t - 1]

108− where

109− forceMap = case lookupCtxt n (idris_optimisation ist) of

110− oi:_ -> M.fromList $ forceable oi

111− _ -> M.empty

112−

113− -- one constructor; if one remaining argument, treat as newtype

114− checkNewType :: IState -> Name -> Type -> Idris ()

115− checkNewType ist cn ct

116− | oi:_ <- lookupCtxt cn opt

117− , length (getArgTys ct) == 1 + forcedCnt (M.fromList $ forceable oi)

118− = putIState ist{ idris_optimisation = opt' oi }

119− | otherwise = return ()

120− where

121− opt = idris_optimisation ist

122− opt' oi = addDef cn oi{ isnewtype = True } opt

123−

124− setCollapsible :: Name -> Idris ()

125− setCollapsible n

126− = do i <- getIState

127− iLOG $ show n ++ " collapsible"

128− case lookupCtxt n (idris_optimisation i) of

129− (oi:_) -> do let oi' = oi { collapsible = True }

130− let opts = addDef n oi' (idris_optimisation i)

131− putIState (i { idris_optimisation = opts })

132− [] -> do let oi = Optimise True False [] []

133− let opts = addDef n oi (idris_optimisation i)

134− putIState (i { idris_optimisation = opts })

135− addIBC (IBCOpt n)

136−

137− disjointTerms :: [[Term]] -> Bool

138− disjointTerms [] = True

139− disjointTerms [xs] = True

140− disjointTerms (xs : xss) =

141− -- xs is disjoint with every pattern from xss

142− all (or . zipWith disjoint xs) xss

143− -- and xss is pairwise disjoint, too

144− && disjointTerms xss

145−

146− -- Return True if the two patterns are provably disjoint.

147− -- Return False if they're not or if unsure.

148− disjoint :: Term -> Term -> Bool

149− disjoint x y = case (cx, cy) of

150− -- data constructors -> compare their names

151− (P (DCon _ _) nx _, P (DCon _ _) ny _)

152− | nx /= ny -> True

153− | otherwise -> or $ zipWith disjoint xargs yargs

154− _ -> False

155− where

156− (cx, xargs) = unApply x

157− (cy, yargs) = unApply y

158−

159class Optimisable term where

16class Optimisable term where

160 applyOpts :: term -> Idris term

17 applyOpts :: term -> Idris term

161− stripCollapsed :: term -> Idris term

162

18

163instance (Optimisable a, Optimisable b) => Optimisable (a, b) where

19instance (Optimisable a, Optimisable b) => Optimisable (a, b) where

164 applyOpts (x, y) = (,) <$> applyOpts x <*> applyOpts y

20 applyOpts (x, y) = (,) <$> applyOpts x <*> applyOpts y

165− stripCollapsed (x, y) = (,) <$> stripCollapsed x <*> stripCollapsed y

166

21

167instance (Optimisable a, Optimisable b) => Optimisable (vs, a, b) where

22instance (Optimisable a, Optimisable b) => Optimisable (vs, a, b) where

168 applyOpts (v, x, y) = (,,) v <$> applyOpts x <*> applyOpts y

23 applyOpts (v, x, y) = (,,) v <$> applyOpts x <*> applyOpts y

169− stripCollapsed (v, x, y) = (,,) v <$> stripCollapsed x <*> stripCollapsed y

170

24

171instance Optimisable a => Optimisable [a] where

25instance Optimisable a => Optimisable [a] where

172 applyOpts = mapM applyOpts

26 applyOpts = mapM applyOpts

173− stripCollapsed = mapM stripCollapsed

174

27

175instance Optimisable a => Optimisable (Either a (a, a)) where

28instance Optimisable a => Optimisable (Either a (a, a)) where

176 applyOpts (Left t) = Left <$> applyOpts t

29 applyOpts (Left t) = Left <$> applyOpts t

177 applyOpts (Right t) = Right <$> applyOpts t

30 applyOpts (Right t) = Right <$> applyOpts t

178− stripCollapsed (Left t) = Left <$> stripCollapsed t

179− stripCollapsed (Right t) = Right <$> stripCollapsed t

180

31

181-- Raw is for compile time optimisation (before type checking)

32-- Raw is for compile time optimisation (before type checking)

182-- Term is for run time optimisation (after type checking, collapsing allowed)

33-- Term is for run time optimisation (after type checking, collapsing allowed)

183−

184-- Compile time: no collapsing

34-- Compile time: no collapsing

185

35

186instance Optimisable Raw where

36instance Optimisable Raw where

187 applyOpts t@(RApp f a)

37 applyOpts t@(RApp f a)

188 | (Var n, args) <- raw_unapply t -- MAGIC HERE

38 | (Var n, args) <- raw_unapply t -- MAGIC HERE

189− = do args' <- mapM applyOpts args

39+ = raw_apply (Var n) <$> mapM applyOpts args

190− i <- getIState

191− return $ case lookupCtxt n (idris_optimisation i) of

192− oi:_ -> applyDataOpt oi n args'

193− _ -> raw_apply (Var n) args'

194 | otherwise = RApp <$> applyOpts f <*> applyOpts a

40 | otherwise = RApp <$> applyOpts f <*> applyOpts a

195

41

196 applyOpts (RBind n b t) = RBind n <$> applyOpts b <*> applyOpts t

42 applyOpts (RBind n b t) = RBind n <$> applyOpts b <*> applyOpts t

197 applyOpts (RForce t) = applyOpts t

43 applyOpts (RForce t) = applyOpts t

198 applyOpts t = return t

44 applyOpts t = return t

199

45

200− stripCollapsed t = return t

201−

202-- Erase types (makes ibc smaller, and we don't need them)

46-- Erase types (makes ibc smaller, and we don't need them)

203instance Optimisable (Binder (TT Name)) where

47instance Optimisable (Binder (TT Name)) where

204 applyOpts (Let t v) = Let <$> return Erased <*> applyOpts v

48 applyOpts (Let t v) = Let <$> return Erased <*> applyOpts v

205 applyOpts b = return (b { binderTy = Erased })

49 applyOpts b = return (b { binderTy = Erased })

206− stripCollapsed (Let t v) = Let <$> return Erased <*> stripCollapsed v

207− stripCollapsed b = return (b { binderTy = Erased })

208

50

209instance Optimisable (Binder Raw) where

51instance Optimisable (Binder Raw) where

210 applyOpts b = do t' <- applyOpts (binderTy b)

52 applyOpts b = do t' <- applyOpts (binderTy b)

211 return (b { binderTy = t' })

53 return (b { binderTy = t' })

212− stripCollapsed (Let t v) = Let <$> stripCollapsed t <*> stripCollapsed v

213− stripCollapsed b = do t' <- stripCollapsed (binderTy b)

214− return (b { binderTy = t' })

215−

216−forcedArgSeq :: OptInfo -> [Maybe Forceability]

217−forcedArgSeq oi = map (\i -> M.lookup i forceMap) [0..]

218− where

219− forceMap = M.fromList $ forceable oi

220−

221−forcedCnt :: ForceMap -> Int

222−forcedCnt = length . filter (== Unconditional) . M.elems

223−

224−applyDataOpt :: OptInfo -> Name -> [Raw] -> Raw

225−applyDataOpt oi n args

226− = raw_apply (Var n) $ zipWith doForce (forcedArgSeq oi) args

227− where

228− doForce (Just Unconditional) a = RForce a

229− doForce _ a = a

230

54

231-- Run-time: do everything

55-- Run-time: do everything

232

56

@@ -249,54 +73,22 @@ instance Optimisable (TT Name) where

249 | fn == txt "toIntegerNat" && mod == prel

73 | fn == txt "toIntegerNat" && mod == prel

250 = return (App (P Ref (sNS (sUN "id") ["Basics","Prelude"]) Erased) Erased)

74 = return (App (P Ref (sNS (sUN "id") ["Basics","Prelude"]) Erased) Erased)

251 applyOpts c@(P (DCon t arity) n _)

75 applyOpts c@(P (DCon t arity) n _)

252− = do i <- getIState

253− case lookupCtxt n (idris_optimisation i) of

254− (oi:_) -> return $ applyDataOptRT oi n t arity []

76+ = return $ applyDataOptRT n t arity []

255− _ -> return c

256 applyOpts t@(App f a)

77 applyOpts t@(App f a)

257 | (c@(P (DCon t arity) n _), args) <- unApply t

78 | (c@(P (DCon t arity) n _), args) <- unApply t

258− = do args' <- mapM applyOpts args

259− i <- getIState

260− case lookupCtxt n (idris_optimisation i) of

261− (oi:_) -> do return $ applyDataOptRT oi n t arity args'

79+ = applyDataOptRT n t arity <$> mapM applyOpts args

262− _ -> return (mkApp c args')

80+ | otherwise = App <$> applyOpts f <*> applyOpts a

263− | otherwise = do f' <- applyOpts f

264− a' <- applyOpts a

265− return (App f' a')

266− applyOpts (Bind n b t) = do b' <- applyOpts b

81+ applyOpts (Bind n b t) = Bind n <$> applyOpts b <*> applyOpts t

267− t' <- applyOpts t

268− return (Bind n b' t')

269− applyOpts (Proj t i) = do t' <- applyOpts t

82+ applyOpts (Proj t i) = Proj <$> applyOpts t <*> pure i

270− return (Proj t' i)

271 applyOpts t = return t

83 applyOpts t = return t

272

84

273− stripCollapsed (Bind n (PVar x) t) | (P _ ty _, _) <- unApply x

274− = do i <- getIState

275− -- NOTE: This assumes that 'ty' is in normal form, which it

276− -- has to be before now because we're not keeping track of

277− -- an environment so we can't do it here.

278− case lookupCtxt ty (idris_optimisation i) of

279− [oi] -> if collapsible oi

280− then do t' <- stripCollapsed t

281− return (Bind n (PVar x) (instantiate Erased t'))

282− else do t' <- stripCollapsed t

283− return (Bind n (PVar x) t')

284− _ -> do t' <- stripCollapsed t

285− return (Bind n (PVar x) t')

286− stripCollapsed (Bind n (PVar x) t)

287− = do t' <- stripCollapsed t

288− return (Bind n (PVar x) t')

289− stripCollapsed t = return t

290−

291−-- Need to saturate arguments first to ensure that erasure happens uniformly

85+-- Need to saturate arguments first to ensure that optimisation happens uniformly

292−

293−applyDataOptRT :: OptInfo -> Name -> Int -> Int -> [Term] -> Term

86+applyDataOptRT :: Name -> Int -> Int -> [Term] -> Term

294−applyDataOptRT oi n tag arity args

87+applyDataOptRT n tag arity args

295− | length args == arity = doOpts n args (collapsible oi) (M.fromList $ forceable oi)

88+ | length args == arity = doOpts n args

296 | otherwise = let extra = satArgs (arity - length args)

89 | otherwise = let extra = satArgs (arity - length args)

297 tm = doOpts n (args ++ map (\n -> P Bound n Erased) extra)

90 tm = doOpts n (args ++ map (\n -> P Bound n Erased) extra)

298− (collapsible oi) (M.fromList $ forceable oi) in

299− bind extra tm

91+ in bind extra tm

300 where

92 where

301 satArgs n = map (\i -> sMN i "sat") [1..n]

93 satArgs n = map (\i -> sMN i "sat") [1..n]

302

94

@@ -305,20 +97,11 @@ applyDataOptRT oi n tag arity args

305

97

306 -- Nat special cases

98 -- Nat special cases

307 -- TODO: Would be nice if this was configurable in idris source!

99 -- TODO: Would be nice if this was configurable in idris source!

308− doOpts (NS (UN z) [nat, prelude]) [] _ _

100+ doOpts (NS (UN z) [nat, prelude]) []

309 | z == txt "Z" && nat == txt "Nat" && prelude == txt "Prelude"

101 | z == txt "Z" && nat == txt "Nat" && prelude == txt "Prelude"

310 = Constant (BI 0)

102 = Constant (BI 0)

311− doOpts (NS (UN s) [nat, prelude]) [k] _ _

103+ doOpts (NS (UN s) [nat, prelude]) [k]

312 | s == txt "S" && nat == txt "Nat" && prelude == txt "Prelude"

104 | s == txt "S" && nat == txt "Nat" && prelude == txt "Prelude"

313 = App (App (P Ref (sUN "prim__addBigInt") Erased) k) (Constant (BI 1))

105 = App (App (P Ref (sUN "prim__addBigInt") Erased) k) (Constant (BI 1))

314

106

315− doOpts n args True _ = Erased

316− doOpts n args _ forceMap

317− | isnewtype oi = case args' of

318− [val] -> val

319− _ -> error $ "Can't happen (newtype not a singleton): " ++ show args'

320− | otherwise = mkApp ctor' args'

321− where

322− ctor' = (P (DCon tag (arity - forcedCnt forceMap)) n Erased)

107+ doOpts n args = mkApp (P (DCon tag arity) n Erased) args

323− args' = [t | (f, t) <- zip (forcedArgSeq oi) args, f /= Just Unconditional]

324−

src/Idris/DeepSeq.hs+6−10

@@ -50,10 +50,6 @@ instance NFData CT.NumWrapper where

50

51-- All generated by 'derive'

52

53−instance NFData Forceability where

54− rnf Conditional = ()

55− rnf Unconditional = ()

56−

57instance NFData IntTy where

53instance NFData IntTy where

58 rnf (ITFixed x1) = rnf x1 `seq` ()

54 rnf (ITFixed x1) = rnf x1 `seq` ()

59 rnf ITNative = ()

55 rnf ITNative = ()

@@ -276,10 +272,10 @@ instance (NFData t) => NFData (PDo' t) where

276instance (NFData t) => NFData (PArg' t) where

272instance (NFData t) => NFData (PArg' t) where

277 rnf (PImp x1 x2 x3 x4 x5)

273 rnf (PImp x1 x2 x3 x4 x5)

278 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

274 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

279− rnf (PExp x1 x2 x3)

275+ rnf (PExp x1 x2 x3 x4)

280− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

276+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

281− rnf (PConstraint x1 x2 x3)

277+ rnf (PConstraint x1 x2 x3 x4)

282− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

278+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

283 rnf (PTacImplicit x1 x2 x3 x4 x5)

279 rnf (PTacImplicit x1 x2 x3 x4 x5)

284 = rnf x1 `seq`

280 = rnf x1 `seq`

285 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

281 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

@@ -290,8 +286,8 @@ instance NFData ClassInfo where

290 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

286 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

291

287

292instance NFData OptInfo where

288instance NFData OptInfo where

293− rnf (Optimise x1 x2 x3 x4)

289+ rnf (Optimise x1 x2)

294− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

290+ = rnf x1 `seq` rnf x2 `seq` ()

295

291

296instance NFData TypeInfo where

292instance NFData TypeInfo where

297 rnf (TI x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

293 rnf (TI x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

src/Idris/Delaborate.hs+3−3

@@ -58,7 +58,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

58 = PLam n (de env [] ty) (de ((n,n):env) [] sc)

59 de env ((PImp { argopts = opts }):is) (Bind n (Pi ty) sc)

60 = PPi (Imp opts Dynamic False) n (de env [] ty) (de ((n,n):env) is sc)

61− de env (PConstraint _ _ _:is) (Bind n (Pi ty) sc)

61+ de env (PConstraint _ _ _ _:is) (Bind n (Pi ty) sc)

62 = PPi constraint n (de env [] ty) (de ((n,n):env) is sc)

63 de env (PTacImplicit _ _ _ tac _:is) (Bind n (Pi ty) sc)

64 = PPi (tacimpl tac) n (de env [] ty) (de ((n,n):env) is sc)

@@ -121,8 +121,8 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

121 | otherwise = PApp un (PRef un n) (map pexp args)

122

123 imp (PImp p m l n _) arg = PImp p m l n arg

124− imp (PExp p l _) arg = PExp p l arg

124+ imp (PExp p l n _) arg = PExp p l n arg

125− imp (PConstraint p l _) arg = PConstraint p l arg

125+ imp (PConstraint p l n _) arg = PConstraint p l n arg

126 imp (PTacImplicit p l n sc _) arg = PTacImplicit p l n sc arg

127

128-- | How far to indent sub-errors

src/Idris/ElabDecls.hs+137−102

@@ -37,6 +37,7 @@ import Data.Maybe

37import Debug.Trace

38

39import qualified Data.Map as Map

40+import qualified Data.Set as S

40import qualified Data.Text as T

41import qualified Data.Text as T

41import Data.Char(isLetter, toLower)

42import Data.Char(isLetter, toLower)

42import Data.List.Split (splitOn)

43import Data.List.Split (splitOn)

@@ -82,10 +83,13 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

82

83

83 logLvl 3 $ show n ++ " pre-type " ++ showTmImpls ty'

84 logLvl 3 $ show n ++ " pre-type " ++ showTmImpls ty'

84 ty' <- addUsingConstraints syn fc ty'

85 ty' <- addUsingConstraints syn fc ty'

85− ty' <- implicit syn n ty'

86+ ty' <- implicit info syn n ty'

86

87

87− let ty = addImpl i ty'

88+ let ty = addImpl i ty'

89+ inacc = inaccessibleArgs 0 ty

88 logLvl 3 $ show n ++ " type " ++ showTmImpls ty

90 logLvl 3 $ show n ++ " type " ++ showTmImpls ty

91+ logLvl 5 $ "Inaccessible arguments: " ++ show inacc

92+

89 ((tyT, defer, is), log) <-

93 ((tyT, defer, is), log) <-

90 tclift $ elaborate ctxt n (TType (UVal 0)) []

94 tclift $ elaborate ctxt n (TType (UVal 0)) []

91 (errAt "type of " n (erun fc (build i info False [] n ty)))

95 (errAt "type of " n (erun fc (build i info False [] n ty)))

@@ -130,8 +134,10 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

130 addDocStr n doc argDocs

134 addDocStr n doc argDocs

131 addIBC (IBCDoc n)

135 addIBC (IBCDoc n)

132 addIBC (IBCFlags n opts')

136 addIBC (IBCFlags n opts')

137+ saveInaccArgs n inacc

133 when (Implicit `elem` opts') $ do addCoercion n

138 when (Implicit `elem` opts') $ do addCoercion n

134 addIBC (IBCCoercion n)

139 addIBC (IBCCoercion n)

140+

135 -- If the function is declared as an error handler and the language

141 -- If the function is declared as an error handler and the language

136 -- extension is enabled, then add it to the list of error handlers.

142 -- extension is enabled, then add it to the list of error handlers.

137 errorReflection <- fmap (elem ErrorReflection . idris_language_extensions) getIState

143 errorReflection <- fmap (elem ErrorReflection . idris_language_extensions) getIState

@@ -172,30 +178,40 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

172 , ns4 == map txt ["Errors","Reflection","Language"] = True

178 , ns4 == map txt ["Errors","Reflection","Language"] = True

173 tyIsHandler _ = False

179 tyIsHandler _ = False

174

180

181+-- Store the list of inaccessible arguments in the internal state.

182+saveInaccArgs :: Name -> [(Int,Name)] -> Idris ()

183+saveInaccArgs n is = do

184+ ist <- getIState

185+ case lookupCtxt n (idris_optimisation ist) of

186+ [oi] -> do

187+ putIState ist{ idris_optimisation =

188+ addDef n oi{ inaccessible = is } (idris_optimisation ist) }

189+

190+ _ -> do

191+ putIState ist{ idris_optimisation =

192+ addDef n (Optimise is False) (idris_optimisation ist) }

193+ addIBC (IBCOpt n)

194+

195+-- Get the list of (index, name) of inaccessible arguments from the type.

196+inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]

197+inaccessibleArgs i (PPi (Imp _ _ _) n Placeholder t)

198+ = (i,n) : inaccessibleArgs (i+1) t -- unbound implicit

199+inaccessibleArgs i (PPi plicity n ty t)

200+ | InaccessibleArg `elem` pargopts plicity

201+ = (i,n) : inaccessibleArgs (i+1) t -- an .{erased : Implicit}

202+ | otherwise

203+ = inaccessibleArgs (i+1) t -- a {regular : Implicit}

204+inaccessibleArgs _ _ = []

175

205

176elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring ->

206elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring ->

177 FC -> FnOpts -> Name -> PTerm -> Idris ()

207 FC -> FnOpts -> Name -> PTerm -> Idris ()

178−elabPostulate info syn doc fc opts n ty

208+elabPostulate info syn doc fc opts n ty = do

179− = do elabType info syn doc [] fc opts n ty

209+ elabType info syn doc [] fc opts n ty

180− -- make sure it's collapsible, so it is never needed at run time

210+ putIState . (\ist -> ist{ idris_postulates = S.insert n (idris_postulates ist) }) =<< getIState

181− -- start by getting the elaborated type

211+ addIBC (IBCPostulate n)

182− ctxt <- getContext

212+

183− fty <- case lookupTy n ctxt of

184− [] -> tclift $ tfail $ (At fc (NoTypeDecl n)) -- can't happen!

185− [ty] -> return ty

186− ist <- getIState

187− let (ap, _) = unApply (getRetTy (normalise ctxt [] fty))

188− logLvl 5 $ "Checking collapsibility of " ++ show (ap, fty)

189− let postOK = case ap of

190− P _ tn _ -> case lookupCtxt tn

191− (idris_optimisation ist) of

192− [oi] -> collapsible oi

193− _ -> False

194− _ -> False

195− when (not postOK)

196− $ tclift $ tfail (At fc (NonCollapsiblePostulate n))

197− -- remove it from the deferred definitions list

213+ -- remove it from the deferred definitions list

198− solveDeferred n

214+ solveDeferred n

199

215

200elabData :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] -> FC -> DataOpts -> PData -> Idris ()

216elabData :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] -> FC -> DataOpts -> PData -> Idris ()

201elabData info syn doc argDocs fc opts (PLaterdecl n t_in)

217elabData info syn doc argDocs fc opts (PLaterdecl n t_in)

@@ -204,13 +220,15 @@ elabData info syn doc argDocs fc opts (PLaterdecl n t_in)

204 checkUndefined fc n

220 checkUndefined fc n

205 ctxt <- getContext

221 ctxt <- getContext

206 i <- getIState

222 i <- getIState

223+ -- TODO think: something more in info?

207− t_in <- implicit syn n t_in

224+ t_in <- implicit info syn n t_in

208 let t = addImpl i t_in

225 let t = addImpl i t_in

209 ((t', defer, is), log) <- tclift $ elaborate ctxt n (TType (UVal 0)) []

226 ((t', defer, is), log) <- tclift $ elaborate ctxt n (TType (UVal 0)) []

210 (erun fc (build i info False [] n t))

227 (erun fc (build i info False [] n t))

211 def' <- checkDef fc defer

228 def' <- checkDef fc defer

212 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'

229 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'

213 addDeferredTyCon def''

230 addDeferredTyCon def''

231+ addIBC (IBCDef n)

214 mapM_ (elabCaseBlock info []) is

232 mapM_ (elabCaseBlock info []) is

215 (cty, _) <- recheckC fc [] t'

233 (cty, _) <- recheckC fc [] t'

216 logLvl 2 $ "---> " ++ show cty

234 logLvl 2 $ "---> " ++ show cty

@@ -222,7 +240,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

222 undef <- isUndefined fc n

240 undef <- isUndefined fc n

223 ctxt <- getContext

241 ctxt <- getContext

224 i <- getIState

242 i <- getIState

225− t_in <- implicit syn n t_in

243+ t_in <- implicit info syn n t_in

226 let t = addImpl i t_in

244 let t = addImpl i t_in

227 ((t', defer, is), log) <-

245 ((t', defer, is), log) <-

228 tclift $ elaborate ctxt n (TType (UVal 0)) []

246 tclift $ elaborate ctxt n (TType (UVal 0)) []

@@ -238,7 +256,8 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

238 logLvl 2 $ "---> " ++ show cty

256 logLvl 2 $ "---> " ++ show cty

239 -- temporary, to check cons

257 -- temporary, to check cons

240 when undef $ updateContext (addTyDecl n (TCon 0 0) cty)

258 when undef $ updateContext (addTyDecl n (TCon 0 0) cty)

259+ let cnameinfo = cinfo info (map cname dcons)

241− cons <- mapM (elabCon info syn n codata) dcons

260+ cons <- mapM (elabCon cnameinfo syn n codata) dcons

242 ttag <- getName

261 ttag <- getName

243 i <- getIState

262 i <- getIState

244 let as = map (const Nothing) (getArgTys cty)

263 let as = map (const Nothing) (getArgTys cty)

@@ -255,15 +274,30 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

255 let metainf = DataMI params

274 let metainf = DataMI params

256 addIBC (IBCMetaInformation n metainf)

275 addIBC (IBCMetaInformation n metainf)

257 -- TMP HACK! Make this a data option

276 -- TMP HACK! Make this a data option

258− when (n /= sUN "Lazy'") $ collapseCons n cons

259 updateContext (addDatatype (Data n ttag cty cons))

277 updateContext (addDatatype (Data n ttag cty cons))

260 updateContext (setMetaInformation n metainf)

278 updateContext (setMetaInformation n metainf)

261 mapM_ (checkPositive n) cons

279 mapM_ (checkPositive n) cons

280+

281+ -- if there's exactly one constructor,

282+ -- mark both the type and the constructor as detaggable

283+ case cons of

284+ [(cn,ct)] -> setDetaggable cn >> setDetaggable n

285+ >> addIBC (IBCOpt cn) >> addIBC (IBCOpt n)

286+ _ -> return ()

287+

288+ -- create an eliminator

262− if DefaultEliminator `elem` opts

289+ when (DefaultEliminator `elem` opts) $

263− then evalStateT (elabEliminator params n t dcons info) Map.empty

290+ evalStateT (elabEliminator params n t dcons info) Map.empty

264− else return ()

265 where

291 where

292+ setDetaggable :: Name -> Idris ()

293+ setDetaggable n = do

294+ ist <- getIState

295+ let opt = idris_optimisation ist

296+ case lookupCtxt n opt of

297+ [oi] -> putIState ist{ idris_optimisation = addDef n oi{ detaggable = True } opt }

298+ _ -> putIState ist{ idris_optimisation = addDef n (Optimise [] True) opt }

299+

266− checkDefinedAs fc n t ctxt

300+ checkDefinedAs fc n t ctxt

267 = case lookupDef n ctxt of

301 = case lookupDef n ctxt of

268 [] -> return ()

302 [] -> return ()

269 [TyDecl _ ty] ->

303 [TyDecl _ ty] ->

@@ -321,6 +355,21 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

321 | otherwise = count n ts

355 | otherwise = count n ts

322 mParam args (_ : rest) = Nothing : mParam args rest

356 mParam args (_ : rest) = Nothing : mParam args rest

323

357

358+ cname (_, _, n, _, _, _) = n

359+

360+ -- Abuse of ElabInfo.

361+ -- TODO Contemplate whether the ElabInfo type needs modification.

362+ cinfo :: ElabInfo -> [Name] -> ElabInfo

363+ cinfo info ds

364+ = let newps = params info

365+ dsParams = map (\n -> (n, [])) ds

366+ newb = addAlist dsParams (inblock info)

367+ l = liftname info in

368+ info { params = newps,

369+ inblock = newb,

370+ liftname = id -- Is this appropriate?

371+ }

372+

324type EliminatorState = StateT (Map.Map String Int) Idris

373type EliminatorState = StateT (Map.Map String Int) Idris

325

374

326-- TODO: Use uniqueName for generating names, rewrite everything to use idris_implicits instead of manual splitting, generally just rewrite

375-- TODO: Use uniqueName for generating names, rewrite everything to use idris_implicits instead of manual splitting, generally just rewrite

@@ -730,7 +779,8 @@ elabRecord :: ElabInfo -> SyntaxInfo -> Docstring -> FC -> Name ->

730 PTerm -> Docstring -> Name -> PTerm -> Idris ()

779 PTerm -> Docstring -> Name -> PTerm -> Idris ()

731elabRecord info syn doc fc tyn ty cdoc cn cty

780elabRecord info syn doc fc tyn ty cdoc cn cty

732 = do elabData info syn doc [] fc [] (PDatadecl tyn ty [(cdoc, [], cn, cty, fc, [])])

781 = do elabData info syn doc [] fc [] (PDatadecl tyn ty [(cdoc, [], cn, cty, fc, [])])

782+ -- TODO think: something more in info?

733− cty' <- implicit syn cn cty

783+ cty' <- implicit info syn cn cty

734 i <- getIState

784 i <- getIState

735 cty <- case lookupTy cn (tt_ctxt i) of

785 cty <- case lookupTy cn (tt_ctxt i) of

736 [t] -> return (delab i t)

786 [t] -> return (delab i t)

@@ -752,7 +802,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

752 where

802 where

753-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }

803-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }

754

804

755− isNonImp (PExp _ _ _, a) = Just a

805+ isNonImp (PExp _ _ _ _, a) = Just a

756 isNonImp _ = Nothing

806 isNonImp _ = Nothing

757

807

758 tryElabDecl info (fn, ty, val)

808 tryElabDecl info (fn, ty, val)

@@ -835,15 +885,22 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

835 (map pexp rhsArgs)) []

885 (map pexp rhsArgs)) []

836 return (pn, pfnTy, PClauses fc [] setname [pclause])

886 return (pn, pfnTy, PClauses fc [] setname [pclause])

837

887

888+-- FIXME: 'forcenames' is an almighty hack! Need a better way of

889+-- erasing non-forceable things

890+-- ^^^

891+-- TODO: the above is a comment from the past;

892+-- forcenames is probably no longer needed

838elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

893elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

839 (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> Idris (Name, Type)

894 (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> Idris (Name, Type)

840elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)

895elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)

841 = do checkUndefined fc n

896 = do checkUndefined fc n

842 ctxt <- getContext

897 ctxt <- getContext

843 i <- getIState

898 i <- getIState

844− t_in <- implicit syn n (if codata then mkLazy t_in else t_in)

899+ t_in <- implicit info syn n (if codata then mkLazy t_in else t_in)

845 let t = addImpl i t_in

900 let t = addImpl i t_in

846 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t

901 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t

902+ let inacc = inaccessibleArgs 0 t

903+ logLvl 5 $ "Inaccessible args: " ++ show inacc

847 ((t', defer, is), log) <-

904 ((t', defer, is), log) <-

848 tclift $ elaborate ctxt n (TType (UVal 0)) []

905 tclift $ elaborate ctxt n (TType (UVal 0)) []

849 (errAt "constructor " n (erun fc (build i info False [] n t)))

906 (errAt "constructor " n (erun fc (build i info False [] n t)))

@@ -861,10 +918,8 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)

861 checkDocs fc argDocs t_in

918 checkDocs fc argDocs t_in

862 addDocStr n doc argDocs

919 addDocStr n doc argDocs

863 addIBC (IBCDoc n)

920 addIBC (IBCDoc n)

864− let fs = map (getNamePos 0 t) forcenames

921+ saveInaccArgs n inacc

865− -- FIXME: 'forcenames' is an almighty hack! Need a better way of

922+ addIBC (IBCOpt n)

866− -- erasing non-forceable things

867− forceArgs tn n (mapMaybe (getNamePos 0 t) forcenames) cty'

868 return (n, cty')

923 return (n, cty')

869 where

924 where

870 tyIs (Bind n b sc) = tyIs sc

925 tyIs (Bind n b sc) = tyIs sc

@@ -875,7 +930,7 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)

875

930

876 mkLazy (PPi pl n ty sc)

931 mkLazy (PPi pl n ty sc)

877 = let ty' = if getTyName ty

932 = let ty' = if getTyName ty

878− then PApp fc (PRef fc (sUN "Lazy'"))

933+ then PApp fc (PRef fc (sUN "Lazy'"))

879 [pexp (PRef fc (sUN "LazyCodata")),

934 [pexp (PRef fc (sUN "LazyCodata")),

880 pexp ty]

935 pexp ty]

881 else ty in

936 else ty in

@@ -897,6 +952,10 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)

897elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

952elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

898elabClauses info fc opts n_in cs = let n = liftname info n_in in

953elabClauses info fc opts n_in cs = let n = liftname info n_in in

899 do ctxt <- getContext

954 do ctxt <- getContext

955+ ist <- getIState

956+ let inacc = case lookupCtxt n (idris_optimisation ist) of

957+ [Optimise inacc _] -> map fst inacc

958+ _ -> []

900 -- Check n actually exists, with no definition yet

959 -- Check n actually exists, with no definition yet

901 let tys = lookupTy n ctxt

960 let tys = lookupTy n ctxt

902 let reflect = Reflection `elem` opts

961 let reflect = Reflection `elem` opts

@@ -914,29 +973,13 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

914

973

915 logLvl 3 $ "Elaborated patterns:\n" ++ show pats_in

974 logLvl 3 $ "Elaborated patterns:\n" ++ show pats_in

916

975

917− -- if the return type of 'ty' is collapsible, the optimised version should

918− -- just do nothing

919− ist <- getIState

920− let (ap, _) = unApply (getRetTy fty)

921− logLvl 5 $ "Checking collapsibility of " ++ show (ap, fty)

922− -- FIXME: Really ought to only do this for total functions!

923− let doNothing = case ap of

924− P _ tn _ -> case lookupCtxt tn

925− (idris_optimisation ist) of

926− [oi] -> collapsible oi

927− _ -> False

928− _ -> False

929 solveDeferred n

976 solveDeferred n

977+

930 ist <- getIState

978 ist <- getIState

931− when doNothing $

932− case lookupCtxt n (idris_optimisation ist) of

933− [oi] -> do let opts = addDef n (oi { collapsible = True })

934− (idris_optimisation ist)

935− putIState (ist { idris_optimisation = opts })

936− _ -> do let opts = addDef n (Optimise True False [] [])

979+ let opts = addDef n (Optimise [] False) (idris_optimisation ist)

937− (idris_optimisation ist)

938− putIState (ist { idris_optimisation = opts })

980+ in putIState (ist { idris_optimisation = opts })

939− addIBC (IBCOpt n)

981+ addIBC (IBCOpt n)

982+

940 ist <- getIState

983 ist <- getIState

941 let pats = map (simple_lhs (tt_ctxt ist)) $ doTransforms ist pats_in

984 let pats = map (simple_lhs (tt_ctxt ist)) $ doTransforms ist pats_in

942

985

@@ -946,11 +989,8 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

946 let tcase = opt_typecase (idris_options ist)

989 let tcase = opt_typecase (idris_options ist)

947

990

948 -- Summary of what's about to happen: Definitions go:

991 -- Summary of what's about to happen: Definitions go:

949−

992+ --

950− -- pats_in -> pats -> optpats

993+ -- pats_in -> pats -> pdef -> pdef'

951− -- pdef comes from pats,

952− -- optpdef comes from optpats

953− -- Then pdef' is optpdef with forcing/collapsing applied everywhere

954

994

955 -- addCaseDef builds case trees from <pdef> and <pdef'>

995 -- addCaseDef builds case trees from <pdef> and <pdef'>

956

996

@@ -979,20 +1019,12 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

979

1019

980 numArgs <- tclift $ sameLength pdef

1020 numArgs <- tclift $ sameLength pdef

981

1021

982− -- patterns after collapsing optimisation applied

983− -- (i.e. check if the function should do nothing at run time)

984− optpats <- if doNothing

985− then return $ [Right (mkApp (P Bound n Erased)

986− (take numArgs (repeat Erased)), Erased)]

987− else stripCollapsed pats

988−

989 case specNames opts of

1022 case specNames opts of

990 Just _ -> logLvl 5 $ "Partially evaluated:\n" ++ show pats

1023 Just _ -> logLvl 5 $ "Partially evaluated:\n" ++ show pats

991 _ -> return ()

1024 _ -> return ()

992

1025

993− let optpdef = map debind optpats -- \$ map (simple_lhs (tt_ctxt ist)) optpats

994 tree@(CaseDef scargs sc _) <- tclift $

1026 tree@(CaseDef scargs sc _) <- tclift $

995− simpleCase tcase False reflect CompileTime fc atys pdef

1027+ simpleCase tcase False reflect CompileTime fc inacc atys pdef

996 cov <- coverage

1028 cov <- coverage

997 pmissing <-

1029 pmissing <-

998 if cov && not (hasDefault cs)

1030 if cov && not (hasDefault cs)

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

1014 let pcover = null pmissing

1046 let pcover = null pmissing

1015

1047

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

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

1017− pdef_in' <- applyOpts optpdef

1049+ pdef_in' <- applyOpts pdef

1018 let pdef' = map (simple_rt (tt_ctxt ist)) pdef_in'

1050 let pdef' = map (simple_rt (tt_ctxt ist)) pdef_in'

1019

1051

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

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

@@ -1041,11 +1073,12 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

1041 let knowncovering = (pcover && cov) || AssertTotal `elem` opts

1073 let knowncovering = (pcover && cov) || AssertTotal `elem` opts

1042

1074

1043 tree' <- tclift $ simpleCase tcase knowncovering reflect

1075 tree' <- tclift $ simpleCase tcase knowncovering reflect

1044− RunTime fc atys pdef'

1076+ RunTime fc inacc atys pdef'

1045− logLvl 3 (show tree)

1077+ logLvl 3 $ "Unoptimised " ++ show n ++ ": " ++ show tree

1046 logLvl 3 $ "Optimised: " ++ show tree'

1078 logLvl 3 $ "Optimised: " ++ show tree'

1047 ctxt <- getContext

1079 ctxt <- getContext

1048 ist <- getIState

1080 ist <- getIState

1081+ let opt = idris_optimisation ist

1049 putIState (ist { idris_patdefs = addDef n (force pdef', force pmissing)

1082 putIState (ist { idris_patdefs = addDef n (force pdef', force pmissing)

1050 (idris_patdefs ist) })

1083 (idris_patdefs ist) })

1051 let caseInfo = CaseInfo (inlinable opts) (dictionary opts)

1084 let caseInfo = CaseInfo (inlinable opts) (dictionary opts)

@@ -1055,6 +1088,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

1055 reflect

1088 reflect

1056 (AssertTotal `elem` opts)

1089 (AssertTotal `elem` opts)

1057 atys

1090 atys

1091+ inacc

1058 pats

1092 pats

1059 pdef pdef pdef_inl pdef' ty)

1093 pdef pdef pdef_inl pdef' ty)

1060 addIBC (IBCDef n)

1094 addIBC (IBCDef n)

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

1071 let used = findUsedArgs sc' scargs'

1105 let used = findUsedArgs sc' scargs'

1072 -- let scg = buildSCG i sc scargs

1106 -- let scg = buildSCG i sc scargs

1073 -- add SCG later, when checking totality

1107 -- add SCG later, when checking totality

1074− let cg = CGInfo scargs' calls [] used []

1108+ let cg = CGInfo scargs' calls [] used [] -- TODO: remove this, not needed anymore

1075 logLvl 2 $ "Called names: " ++ show cg

1109 logLvl 2 $ "Called names: " ++ show cg

1076 addToCG n cg

1110 addToCG n cg

1077 addToCalledG n (nub (map fst calls)) -- plus names in type!

1111 addToCalledG n (nub (map fst calls)) -- plus names in type!

@@ -1292,7 +1326,7 @@ checkPossible info fc tcgen fname lhs_in

1292 ((P _ x _, _), (P _ y _, _)) -> x == y

1326 ((P _ x _, _), (P _ y _, _)) -> x == y

1293 _ -> False

1327 _ -> False

1294

1328

1295−getFixedInType i env (PExp _ _ _ : is) (Bind n (Pi t) sc)

1329+getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi t) sc)

1296 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)

1330 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)

1297getFixedInType i env (_ : is) (Bind n (Pi t) sc)

1331getFixedInType i env (_ : is) (Bind n (Pi t) sc)

1298 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)

1332 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)

@@ -1423,10 +1457,10 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1423 -- Elaborate where block

1457 -- Elaborate where block

1424 ist <- getIState

1458 ist <- getIState

1425 windex <- getName

1459 windex <- getName

1426− let winfo = pinfo (pvars ist lhs_tm) whereblock windex

1427 let decls = nub (concatMap declared whereblock)

1460 let decls = nub (concatMap declared whereblock)

1428 let defs = nub (decls ++ concatMap defined whereblock)

1461 let defs = nub (decls ++ concatMap defined whereblock)

1429 let newargs = pvars ist lhs_tm

1462 let newargs = pvars ist lhs_tm

1463+ let winfo = pinfo info newargs defs windex

1430 let wb = map (expandParamsD False ist decorate newargs defs) whereblock

1464 let wb = map (expandParamsD False ist decorate newargs defs) whereblock

1431

1465

1432 -- Split the where block into declarations with a type, and those

1466 -- Split the where block into declarations with a type, and those

@@ -1435,7 +1469,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1435 let (wbefore, wafter) = sepBlocks wb

1469 let (wbefore, wafter) = sepBlocks wb

1436

1470

1437 logLvl 2 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter

1471 logLvl 2 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter

1438− mapM_ (elabDecl' EAll info) wbefore

1472+ mapM_ (elabDecl' EAll winfo) wbefore

1439 -- Now build the RHS, using the type of the LHS as the goal.

1473 -- Now build the RHS, using the type of the LHS as the goal.

1440 i <- getIState -- new implicits from where block

1474 i <- getIState -- new implicits from where block

1441 logLvl 5 (showTmImpls (expandParams decorate newargs defs (defs \\ decls) rhs_in))

1475 logLvl 5 (showTmImpls (expandParams decorate newargs defs (defs \\ decls) rhs_in))

@@ -1450,7 +1484,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1450 mapM_ setinj (nub (params ++ inj))

1484 mapM_ setinj (nub (params ++ inj))

1451 setNextName

1485 setNextName

1452 (_, _, is) <- errAt "right hand side of " fname

1486 (_, _, is) <- errAt "right hand side of " fname

1453− (erun fc (build i info False opts fname rhs))

1487+ (erun fc (build i winfo False opts fname rhs))

1454 errAt "right hand side of " fname

1488 errAt "right hand side of " fname

1455 (erun fc $ psolve lhs_tm)

1489 (erun fc $ psolve lhs_tm)

1456 hs <- get_holes

1490 hs <- get_holes

@@ -1478,8 +1512,8 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1478 -- Now the remaining deferred (i.e. no type declarations) clauses

1512 -- Now the remaining deferred (i.e. no type declarations) clauses

1479 -- from the where block

1513 -- from the where block

1480

1514

1481− mapM_ (elabDecl' EAll info) wafter

1515+ mapM_ (elabDecl' EAll winfo) wafter

1482− mapM_ (elabCaseBlock info opts) is

1516+ mapM_ (elabCaseBlock winfo opts) is

1483

1517

1484 ctxt <- getContext

1518 ctxt <- getContext

1485 logLvl 5 $ "Rechecking"

1519 logLvl 5 $ "Rechecking"

@@ -1509,6 +1543,19 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1509 addErrRev (crhs, clhs)

1543 addErrRev (crhs, clhs)

1510 return $ (Right (clhs, crhs), lhs)

1544 return $ (Right (clhs, crhs), lhs)

1511 where

1545 where

1546+ pinfo :: ElabInfo -> [(Name, PTerm)] -> [Name] -> Int -> ElabInfo

1547+ pinfo info ns ds i

1548+ = let newps = params info ++ ns

1549+ dsParams = map (\n -> (n, map fst newps)) ds

1550+ newb = addAlist dsParams (inblock info)

1551+ l = liftname info in

1552+ info { params = newps,

1553+ inblock = newb,

1554+ liftname = id -- (\n -> case lookupCtxt n newb of

1555+ -- Nothing -> n

1556+ -- _ -> MN i (show n)) . l

1557+ }

1558+

1512 mkLHSapp t@(PRef _ _) = trace ("APP " ++ show t) $ PApp fc t []

1559 mkLHSapp t@(PRef _ _) = trace ("APP " ++ show t) $ PApp fc t []

1513 mkLHSapp t = t

1560 mkLHSapp t = t

1514

1561

@@ -1531,19 +1578,6 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1531 (b : bf, af)

1578 (b : bf, af)

1532 sepBlocks' ns [] = ([], [])

1579 sepBlocks' ns [] = ([], [])

1533

1580

1534− pinfo ns ps i

1535− = let ds = concatMap declared ps

1536− newps = params info ++ ns

1537− dsParams = map (\n -> (n, map fst newps)) ds

1538− newb = addAlist dsParams (inblock info)

1539− l = liftname info in

1540− info { params = newps,

1541− inblock = newb,

1542− liftname = id -- (\n -> case lookupCtxt n newb of

1543− -- Nothing -> n

1544− -- _ -> MN i (show n)) . l

1545− }

1546−

1547

1581

1548 -- if a hole is just an argument/result of a case block, treat it as

1582 -- if a hole is just an argument/result of a case block, treat it as

1549 -- the unit type. Hack to help elaborate case in do blocks.

1583 -- the unit type. Hack to help elaborate case in do blocks.

@@ -1808,7 +1842,7 @@ elabClass info syn doc fc constraints tn ps ds

1808

1842

1809 getMName (PTy _ _ _ _ _ n _) = nsroot n

1843 getMName (PTy _ _ _ _ _ n _) = nsroot n

1810 tdecl allmeths (PTy doc _ syn _ o n t)

1844 tdecl allmeths (PTy doc _ syn _ o n t)

1811− = do t' <- implicit' syn allmeths n t

1845+ = do t' <- implicit' info syn allmeths n t

1812 logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

1846 logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

1813 return ( (n, (toExp (map fst ps) Exp t')),

1847 return ( (n, (toExp (map fst ps) Exp t')),

1814 (n, (doc, o, (toExp (map fst ps) Imp t'))),

1848 (n, (doc, o, (toExp (map fst ps) Imp t'))),

@@ -2012,7 +2046,8 @@ elabInstance info syn what fc cs n ps t expn ds = do

2012 -- TODO: largely based upon elabType' - should try to abstract

2046 -- TODO: largely based upon elabType' - should try to abstract

2013 elabFindOverlapping i ci iname syn t

2047 elabFindOverlapping i ci iname syn t

2014 = do ty' <- addUsingConstraints syn fc t

2048 = do ty' <- addUsingConstraints syn fc t

2049+ -- TODO think: something more in info?

2015− ty' <- implicit syn iname ty'

2050+ ty' <- implicit info syn iname ty'

2016 let ty = addImpl i ty'

2051 let ty = addImpl i ty'

2017 ctxt <- getContext

2052 ctxt <- getContext

2018 ((tyT, _, _), _) <-

2053 ((tyT, _, _), _) <-

@@ -2050,9 +2085,9 @@ elabInstance info syn what fc cs n ps t expn ds = do

2050 methArgs i (PPi (Imp _ _ _) n ty sc)

2085 methArgs i (PPi (Imp _ _ _) n ty sc)

2051 = PImp 0 True [] n (PRef fc (sMN i "meth")) : methArgs (i+1) sc

2086 = PImp 0 True [] n (PRef fc (sMN i "meth")) : methArgs (i+1) sc

2052 methArgs i (PPi (Exp _ _ _) n ty sc)

2087 methArgs i (PPi (Exp _ _ _) n ty sc)

2053− = PExp 0 [] (PRef fc (sMN i "meth")) : methArgs (i+1) sc

2088+ = PExp 0 [] (sMN 0 "marg") (PRef fc (sMN i "meth")) : methArgs (i+1) sc

2054 methArgs i (PPi (Constraint _ _) n ty sc)

2089 methArgs i (PPi (Constraint _ _) n ty sc)

2055− = PConstraint 0 [] (PResolveTC fc) : methArgs (i+1) sc

2090+ = PConstraint 0 [] (sMN 0 "marg") (PResolveTC fc) : methArgs (i+1) sc

2056 methArgs i _ = []

2091 methArgs i _ = []

2057

2092

2058 papp fc f [] = f

2093 papp fc f [] = f

@@ -2068,7 +2103,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

2068 _ -> return ps'

2103 _ -> return ps'

2069 getWParams (_ : ps) = getWParams ps

2104 getWParams (_ : ps) = getWParams ps

2070

2105

2071− decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns

2106+ decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns

2072 decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns

2107 decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns

2073

2108

2074 mkTyDecl (n, op, t, _) = PTy emptyDocstring [] syn fc op n t

2109 mkTyDecl (n, op, t, _) = PTy emptyDocstring [] syn fc op n t

src/Idris/ElabTerm.hs+4−13

@@ -3,6 +3,7 @@

3module Idris.ElabTerm where

4

5import Idris.AbsSyntax

6+import Idris.AbsSyntaxTree

6import Idris.DSL

7import Idris.DSL

7import Idris.Delaborate

8import Idris.Delaborate

8import Idris.Error

9import Idris.Error

@@ -27,16 +28,6 @@ import qualified Data.Text as T

27

28

28import Debug.Trace

29import Debug.Trace

29

30

30−-- Data to pass to recursively called elaborators; e.g. for where blocks,

31−-- paramaterised declarations, etc.

32−

33−data ElabInfo = EInfo { params :: [(Name, PTerm)],

34− inblock :: Ctxt [Name], -- names in the block, and their params

35− liftname :: Name -> Name,

36− namespace :: Maybe [String] }

37−

38−toplevel = EInfo [] emptyContext id Nothing

39−

40-- Using the elaborator, convert a term in raw syntax to a fully

31-- Using the elaborator, convert a term in raw syntax to a fully

41-- elaborated, typechecked term.

32-- elaborated, typechecked term.

42--

33--

@@ -474,7 +465,7 @@ elab ist info pattern opts fn tm

474 elabArgs ist (ina || not isinf, guarded, inty)

465 elabArgs ist (ina || not isinf, guarded, inty)

475 [] fc False f ns'

466 [] fc False f ns'

476 (f == sUN "Force")

467 (f == sUN "Force")

477− (map (\x -> (lazyarg x, getTm x)) eargs)

468+ (map (\x -> (False, getTm x)) eargs) -- TODO: remove this False arg

478 solve

469 solve

479 ivs' <- get_instances

470 ivs' <- get_instances

480 -- Attempt to resolve any type classes which have 'complete' types,

471 -- Attempt to resolve any type classes which have 'complete' types,

@@ -697,7 +688,7 @@ elab ist info pattern opts fn tm

697 where

688 where

698 mkDelay (PAlternative b xs) = PAlternative b (map mkDelay xs)

689 mkDelay (PAlternative b xs) = PAlternative b (map mkDelay xs)

699 mkDelay t = let fc = fileFC "Delay" in

690 mkDelay t = let fc = fileFC "Delay" in

700− addImpl ist (PApp fc (PRef fc (sUN "Delay"))

691+ addImpl ist (PApp fc (PRef fc (sUN "Delay"))

701 [pexp t])

692 [pexp t])

702

693

703 insertCoerce ina t =

694 insertCoerce ina t =

@@ -733,7 +724,7 @@ elab ist info pattern opts fn tm

733 = elabArgs ist ina failed fc r f ns force args

724 = elabArgs ist ina failed fc r f ns force args

734 elabArgs ist ina failed fc r f ((argName, holeName):ns) force ((lazy, t) : args)

725 elabArgs ist ina failed fc r f ((argName, holeName):ns) force ((lazy, t) : args)

735 | lazy && not pattern

726 | lazy && not pattern

736− = elabArg argName holeName (PApp bi (PRef bi (sUN "lazy"))

727+ = elabArg argName holeName (PApp bi (PRef bi (sUN "Delay"))

737 [pimp (sUN "a") Placeholder True,

728 [pimp (sUN "a") Placeholder True,

738 pexp t])

729 pexp t])

739 | otherwise = elabArg argName holeName t

730 | otherwise = elabArg argName holeName t

src/Idris/Erasure.hsnew file+505

@@ -0,0 +1,505 @@

1+{-# LANGUAGE PatternGuards #-}

2+

3+module Idris.Erasure (performUsageAnalysis, mkFieldName) where

4+

5+import Idris.AbsSyntax

6+import Idris.Core.CaseTree

7+import Idris.Core.TT

8+import Idris.Core.Evaluate

9+import Idris.Primitives

10+import Idris.Error

11+

12+import Debug.Trace

13+import System.IO.Unsafe

14+

15+import Control.Arrow

16+import Control.Applicative

17+import Control.Monad.State

18+import Data.Maybe

19+import Data.List

20+import qualified Data.Set as S

21+import qualified Data.IntSet as IS

22+import qualified Data.Map as M

23+import qualified Data.IntMap as IM

24+import Data.Set (Set)

25+import Data.IntSet (IntSet)

26+import Data.Map (Map)

27+import Data.IntMap (IntMap)

28+import Data.Text (pack)

29+import qualified Data.Text as T

30+

31+-- UseMap maps names to the set of used (reachable) argument positions.

32+type UseMap = Map Name (IntMap (Set Reason))

33+

34+data Arg = Arg Int | Result deriving (Eq, Ord)

35+

36+instance Show Arg where

37+ show (Arg i) = show i

38+ show Result = "*"

39+

40+type Node = (Name, Arg)

41+type Deps = Map Cond DepSet

42+type Reason = (Name, Int) -- function name, argument index

43+

44+-- Nodes along with sets of reasons for every one.

45+type DepSet = Map Node (Set Reason)

46+

47+-- "Condition" is the conjunction

48+-- of elementary assumptions along the path from the root.

49+-- Elementary assumption (f, i) means that "function f uses the argument i".

50+type Cond = Set Node

51+

52+-- Variables carry certain information with them.

53+data VarInfo = VI

54+ { viDeps :: DepSet -- dependencies drawn in by the variable

55+ , viFunArg :: Maybe Int -- which function argument this variable came from (defined only for patvars)

56+ , viMethod :: Maybe Name -- name of the metamethod represented by the var, if any

57+ }

58+ deriving Show

59+

60+type Vars = Map Name VarInfo

61+

62+-- Perform usage analysis, write the relevant information in the internal

63+-- structures, returning the list of reachable names.

64+performUsageAnalysis :: Idris [Name]

65+performUsageAnalysis = do

66+ ctx <- tt_ctxt <$> getIState

67+ mainName <- getMainName <$> getIState

68+

69+ case mainName of

70+ Left reason -> return [] -- no main -> not compiling -> reachability irrelevant

71+ Right main -> do

72+ ci <- idris_classes <$> getIState

73+ cg <- idris_callgraph <$> getIState

74+ opt <- idris_optimisation <$> getIState

75+

76+ -- Build the dependency graph.

77+ let depMap = buildDepMap ci ctx main

78+

79+ -- Search for reachable nodes in the graph.

80+ let (residDeps, (reachableNames, minUse)) = minimalUsage depMap

81+ usage = M.toList minUse

82+

83+ -- Print some debug info.

84+ logLvl 5 $ "Original deps:\n" ++ unlines (map fmtItem . M.toList $ depMap)

85+ logLvl 3 $ "Reachable names:\n" ++ unlines (map (indent . show) . S.toList $ reachableNames)

86+ logLvl 4 $ "Minimal usage:\n" ++ fmtUseMap usage

87+ logLvl 5 $ "Residual deps:\n" ++ unlines (map fmtItem . M.toList $ residDeps)

88+

89+ -- Check that everything reachable is accessible.

90+ checkEnabled <- (WarnReach `elem`) . opt_cmdline . idris_options <$> getIState

91+ when checkEnabled $

92+ mapM_ (checkAccessibility opt) usage

93+

94+ -- Check that no postulates are reachable.

95+ reachablePostulates <- S.intersection reachableNames . idris_postulates <$> getIState

96+ when (not . S.null $ reachablePostulates)

97+ $ ifail ("reachable postulates:\n" ++ intercalate "\n" [" " ++ show n | n <- S.toList reachablePostulates])

98+

99+ -- Store the usage info in the internal state.

100+ mapM_ (storeUsage cg) usage

101+

102+ return $ S.toList reachableNames

103+ where

104+ getMainName :: IState -> Either Err Name

105+ getMainName ist = case lookupCtxtName n (idris_implicits ist) of

106+ [(n', _)] -> Right n'

107+ [] -> Left (NoSuchVariable n)

108+ more -> Left (CantResolveAlts (map (show . fst) more))

109+ where

110+ n = sNS (sUN "main") ["Main"]

111+

112+ indent = (" " ++)

113+

114+ fmtItem :: (Cond, DepSet) -> String

115+ fmtItem (cond, deps) = indent $ show (S.toList cond) ++ " -> " ++ show (M.toList deps)

116+

117+ fmtUseMap :: [(Name, IntMap (Set Reason))] -> String

118+ fmtUseMap = unlines . map (\(n,is) -> indent $ show n ++ " -> " ++ fmtIxs is)

119+

120+ fmtIxs :: IntMap (Set Reason) -> String

121+ fmtIxs = intercalate ", " . map fmtArg . IM.toList

122+ where

123+ fmtArg (i, rs)

124+ | S.null rs = show i

125+ | otherwise = show i ++ " from " ++ intercalate ", " (map show $ S.toList rs)

126+

127+ storeUsage :: Ctxt CGInfo -> (Name, IntMap (Set Reason)) -> Idris ()

128+ storeUsage cg (n, args)

129+ | Just x <- lookupCtxtExact n cg

130+ = addToCG n x{ usedpos = flat } -- functions

131+

132+ | otherwise

133+ = addToCG n (CGInfo [] [] [] [] flat) -- data ctors

134+ where

135+ flat = [(i, S.toList rs) | (i,rs) <- IM.toList args]

136+

137+ checkAccessibility :: Ctxt OptInfo -> (Name, IntMap (Set Reason)) -> Idris ()

138+ checkAccessibility opt (n, reachable)

139+ | Just (Optimise inaccessible dt) <- lookupCtxtExact n opt

140+ , eargs@(_:_) <- [fmt n (S.toList rs) | (i,n) <- inaccessible, rs <- maybeToList $ IM.lookup i reachable]

141+ = warn $ show n ++ ": inaccessible arguments reachable:\n " ++ intercalate "\n " eargs

142+

143+ | otherwise = return ()

144+ where

145+ fmt n [] = show n ++ " (no more information available)"

146+ fmt n rs = show n ++ " from " ++ intercalate ", " [show rn ++ " arg# " ++ show ri | (rn,ri) <- rs]

147+ warn = logLvl 0

148+

149+-- Find the minimal consistent usage by forward chaining.

150+minimalUsage :: Deps -> (Deps, (Set Name, UseMap))

151+minimalUsage = second gather . forwardChain

152+ where

153+ gather :: DepSet -> (Set Name, UseMap)

154+ gather = foldr ins (S.empty, M.empty) . M.toList

155+ where

156+ ins :: (Node, Set Reason) -> (Set Name, UseMap) -> (Set Name, UseMap)

157+ ins ((n, Result), rs) (ns, umap) = (S.insert n ns, umap)

158+ ins ((n, Arg i ), rs) (ns, umap) = (ns, M.insertWith (IM.unionWith S.union) n (IM.singleton i rs) umap)

159+

160+forwardChain :: Deps -> (Deps, DepSet)

161+forwardChain deps

162+ | Just trivials <- M.lookup S.empty deps

163+ = (M.unionWith S.union trivials)

164+ `second` forwardChain (remove trivials . M.delete S.empty $ deps)

165+ | otherwise = (deps, M.empty)

166+ where

167+ -- Remove the given nodes from the Deps entirely,

168+ -- possibly creating new empty Conds.

169+ remove :: DepSet -> Deps -> Deps

170+ remove ds = M.mapKeysWith (M.unionWith S.union) (S.\\ M.keysSet ds)

171+

172+-- Build the dependency graph,

173+-- starting the depth-first search from a list of Names.

174+buildDepMap :: Ctxt ClassInfo -> Context -> Name -> Deps

175+buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

176+ where

177+ -- mark the result of Main.main as used with the empty assumption

178+ addPostulates :: Deps -> Deps

179+ addPostulates deps = foldr (\(ds, rs) -> M.insertWith (M.unionWith S.union) ds rs) deps postulates

180+ where

181+ -- mini-DSL for postulates

182+ (==>) ds rs = (S.fromList ds, M.fromList [(r, S.empty) | r <- rs])

183+ it n is = [(sUN n, Arg i) | i <- is]

184+ mn n is = [(MN 0 $ pack n, Arg i) | i <- is]

185+

186+ -- believe_me is special because it does not use all its arguments

187+ specialPrims = S.fromList [sUN "prim__believe_me"]

188+ usedNames = allNames deps S.\\ specialPrims

189+ usedPrims = [(p_name p, p_arity p) | p <- primitives, p_name p `S.member` usedNames]

190+

191+ postulates =

192+ [ [] ==> concat

193+ -- These two, Main.main and run__IO, are always evaluated

194+ -- but they elude analysis since they come from the seed term.

195+ [ [(mainName, Result)]

196+ , [(sUN "run__IO", Result), (sUN "run__IO", Arg 0)]

197+

198+ -- MkIO is read by run__IO,

199+ -- but this cannot be observed in the source code of programs.

200+ , it "MkIO" [1]

201+ , it "prim__IO" [1]

202+

203+ -- these have been discovered as builtins but are not listed

204+ -- among Idris.Primitives.primitives

205+ , mn "__MkPair" [2,3]

206+ , it "prim_fork" [0]

207+

208+ -- believe_me is a primitive but it only uses its third argument

209+ -- it is special-cased in usedNames above

210+ , it "prim__believe_me" [2]

211+

212+ -- in general, all other primitives use all their arguments

213+ , [(n, Arg i) | (n,arity) <- usedPrims, i <- [0..arity-1]]

214+

215+ -- mkForeign* functions are special-cased below

216+ ]

217+ ]

218+

219+ -- perform depth-first search

220+ -- to discover all the names used in the program

221+ -- and call getDeps for every name

222+ dfs :: Set Name -> Deps -> [Name] -> Deps

223+ dfs visited deps [] = deps

224+ dfs visited deps (n : ns)

225+ | n `S.member` visited = dfs visited deps ns

226+ | otherwise = dfs (S.insert n visited) (M.unionWith (M.unionWith S.union) deps' deps) (next ++ ns)

227+ where

228+ next = [n | n <- S.toList depn, n `S.notMember` visited]

229+ depn = S.delete n $ allNames deps'

230+ deps' = getDeps n

231+

232+ -- extract all names that a function depends on

233+ -- from the Deps of the function

234+ allNames :: Deps -> Set Name

235+ allNames = S.unions . map names . M.toList

236+ where

237+ names (cs, ns) = S.map fst cs `S.union` S.map fst (M.keysSet ns)

238+

239+ -- get Deps for a Name

240+ getDeps :: Name -> Deps

241+ getDeps (SN (WhereN i (SN (InstanceCtorN classN)) (MN i' field)))

242+ = M.empty -- these deps are created when applying instance ctors

243+ getDeps n = case lookupDefExact n ctx of

244+ Just def -> getDepsDef n def

245+ Nothing -> error $ "erasure checker: unknown reference: " ++ show n

246+

247+ getDepsDef :: Name -> Def -> Deps

248+ getDepsDef fn (Function ty t) = error "a function encountered" -- TODO

249+ getDepsDef fn (TyDecl ty t) = M.empty

250+ getDepsDef fn (Operator ty n' f) = M.empty -- TODO: what's this?

251+ getDepsDef fn (CaseOp ci ty tys def tot cdefs)

252+ = getDepsSC fn etaVars (etaMap `M.union` varMap) sc

253+ where

254+ -- we must eta-expand the definition with fresh variables

255+ -- to capture these dependencies as well

256+ etaIdx = [length vars .. length tys - 1]

257+ etaVars = [eta i | i <- etaIdx]

258+ etaMap = M.fromList [varPair (eta i) i | i <- etaIdx]

259+ eta i = MN i (pack "eta")

260+

261+ -- the variables that arose as function arguments only depend on (n, i)

262+ varMap = M.fromList [varPair v i | (v,i) <- zip vars [0..]]

263+

264+ varPair n argNo = (n, VI

265+ { viDeps = M.singleton (fn, Arg argNo) S.empty

266+ , viFunArg = Just argNo

267+ , viMethod = Nothing

268+ })

269+

270+ (vars, sc) = cases_runtime cdefs

271+ -- we use cases_runtime in order to have case-blocks

272+ -- resolved to top-level functions before our analysis

273+

274+ etaExpand :: [Name] -> Term -> Term

275+ etaExpand [] t = t

276+ etaExpand (n : ns) t = etaExpand ns (App t (P Ref n Erased))

277+

278+ getDepsSC :: Name -> [Name] -> Vars -> SC -> Deps

279+ getDepsSC fn es vs ImpossibleCase = M.empty

280+ getDepsSC fn es vs (UnmatchedCase msg) = M.empty

281+

282+ -- for the purposes of erasure, we can disregard the projection

283+ getDepsSC fn es vs (ProjCase (Proj t i) alts) = getDepsSC fn es vs (ProjCase t alts) -- step

284+ getDepsSC fn es vs (ProjCase (P _ n _) alts) = getDepsSC fn es vs (Case n alts) -- base

285+

286+ -- other ProjCase's are not supported

287+ getDepsSC fn es vs (ProjCase t alts) = error $ "ProjCase not supported:\n" ++ show (ProjCase t alts)

288+

289+ getDepsSC fn es vs (STerm t) = getDepsTerm vs [] (S.singleton (fn, Result)) (etaExpand es t)

290+ getDepsSC fn es vs (Case n alts)

291+ -- we case-split on this variable, which marks it as used

292+ -- (unless there is exactly one case branch)

293+ -- hence we add a new dependency, whose only precondition is

294+ -- that the result of this function is used at all

295+ = addTagDep $ unionMap (getDepsAlt fn es vs casedVar) alts -- coming from the whole subtree

296+ where

297+

298+ addTagDep = case alts of

299+ [_] -> id -- single branch, tag not used

300+ _ -> M.insertWith (M.unionWith S.union) (S.singleton (fn, Result)) (viDeps casedVar)

301+ casedVar = fromMaybe (error $ "nonpatvar in case: " ++ show n) (M.lookup n vs)

302+

303+ getDepsAlt :: Name -> [Name] -> Vars -> VarInfo -> CaseAlt -> Deps

304+ getDepsAlt fn es vs var (FnCase n ns sc) = error "an FnCase encountered" -- TODO: what's this?

305+ getDepsAlt fn es vs var (ConstCase c sc) = getDepsSC fn es vs sc

306+ getDepsAlt fn es vs var (DefaultCase sc) = getDepsSC fn es vs sc

307+ getDepsAlt fn es vs var (SucCase n sc)

308+ = getDepsSC fn es (M.insert n var vs) sc -- we're not inserting the S-dependency here because it's special-cased

309+

310+ -- data constructors

311+ getDepsAlt fn es vs var (ConCase n cnt ns sc)

312+ = getDepsSC fn es (vs' `M.union` vs) sc -- left-biased union

313+ where

314+ -- Here we insert dependencies that arose from pattern matching on a constructor.

315+ -- n = ctor name, j = ctor arg#, i = fun arg# of the cased var, cs = ctors of the cased var

316+ vs' = M.fromList [(v, VI

317+ { viDeps = M.insertWith S.union (n, Arg j) (S.singleton (fn, varIdx)) (viDeps var)

318+ , viFunArg = viFunArg var

319+ , viMethod = meth j

320+ })

321+ | (v, j) <- zip ns [0..]]

322+

323+ -- this is safe because it's certainly a patvar

324+ varIdx = fromJust (viFunArg var)

325+

326+ -- generate metamethod names, "n" is the instance ctor

327+ meth :: Int -> Maybe Name

328+ meth | SN (InstanceCtorN className) <- n = \j -> Just (mkFieldName n j)

329+ | otherwise = \j -> Nothing

330+

331+ -- Named variables -> DeBruijn variables -> Conds/guards -> Term -> Deps

332+ getDepsTerm :: Vars -> [Cond -> Deps] -> Cond -> Term -> Deps

333+

334+ -- named variables introduce dependencies as described in `vs'

335+ getDepsTerm vs bs cd (P _ n _)

336+ -- local variables

337+ | Just var <- M.lookup n vs

338+ = M.singleton cd (viDeps var)

339+

340+ -- sanity check: machine-generated names shouldn't occur at top-level

341+ | MN _ _ <- n

342+ , n `notElem` specialMNs

343+ = error $ "erasure analysis: variable " ++ show n ++ " unbound in " ++ show (S.toList cd)

344+

345+ -- assumed to be a global reference

346+ | otherwise = M.singleton cd (M.singleton (n, Result) S.empty)

347+ where

348+ specialMNs = map (sMN 0 . ("__" ++)) $ words "Unit True False II"

349+

350+ -- dependencies of de bruijn variables are described in `bs'

351+ getDepsTerm vs bs cd (V i) = (bs !! i) cd

352+

353+ getDepsTerm vs bs cd (Bind n bdr t)

354+ -- here we just push IM.empty on the de bruijn stack

355+ -- the args will be marked as used at the usage site

356+ | Lam ty <- bdr = getDepsTerm vs (const M.empty : bs) cd t

357+ | Pi ty <- bdr = getDepsTerm vs (const M.empty : bs) cd t

358+

359+ -- let-bound variables can get partially evaluated

360+ -- it is sufficient just to plug the Cond in when the bound names are used

361+ | Let ty t <- bdr = getDepsTerm vs (var t : bs) cd t

362+ | NLet ty t <- bdr = getDepsTerm vs (var t : bs) cd t

363+ where

364+ var t cd = getDepsTerm vs bs cd t

365+

366+ -- applications may add items to Cond

367+ getDepsTerm vs bs cd app@(App _ _)

368+ | (fun, args) <- unApply app = case fun of

369+ -- instance constructors -> create metamethod deps

370+ P (DCon _ _) ctorName@(SN (InstanceCtorN className)) _

371+ -> conditionalDeps ctorName args -- regular data ctor stuff

372+ `union` unionMap (methodDeps ctorName) (zip [0..] args) -- method-specific stuff

373+

374+ -- ordinary constructors

375+ P (TCon _ _) n _ -> unconditionalDeps args -- does not depend on anything

376+ P (DCon _ _) n _ -> conditionalDeps n args -- depends on whether (n,#) is used

377+

378+ -- mkForeign* calls must be special-cased because they are variadic

379+ -- All arguments must be marked as used, except for the first one,

380+ -- which is the (Foreign a) spec that defines the type

381+ -- and is not needed at runtime.

382+ P _ (UN n) _

383+ | n `elem` map T.pack ["mkForeign", "mkForeignPrim", "mkLazyForeignPrim"]

384+ -> unconditionalDeps (drop 1 args)

385+

386+ -- a bound variable might draw in additional dependencies,

387+ -- think: f x = x 0 <-- here, `x' _is_ used

388+ P _ n _

389+ -- local name that refers to a method

390+ | Just var <- M.lookup n vs

391+ , Just meth <- viMethod var

392+ -> viDeps var `ins` conditionalDeps meth args -- use the method instead

393+

394+ -- local name

395+ | Just var <- M.lookup n vs

396+ -- unconditional use

397+ -> viDeps var `ins` unconditionalDeps args

398+

399+ -- global name

400+ | otherwise

401+ -- depends on whether the referred thing uses its argument

402+ -> conditionalDeps n args

403+

404+ -- TODO: could we somehow infer how bound variables use their arguments?

405+ V i -> M.unionWith (M.unionWith S.union) ((bs !! i) cd) (unconditionalDeps args)

406+

407+ -- we interpret applied lambdas as lets in order to reuse code here

408+ Bind n (Lam ty) t -> getDepsTerm vs bs cd (lamToLet [] app)

409+

410+ -- and we interpret applied lets as lambdas

411+ Bind n ( Let ty t') t -> getDepsTerm vs bs cd (App (Bind n (Lam ty) t) t')

412+ Bind n (NLet ty t') t -> getDepsTerm vs bs cd (App (Bind n (Lam ty) t) t')

413+

414+ Proj t i

415+ -> error $ "cannot[0] analyse projection !" ++ show i ++ " of " ++ show t

416+

417+ Erased -> M.empty

418+

419+ _ -> error $ "cannot analyse application of " ++ show fun ++ " to " ++ show args

420+ where

421+ ins = M.insertWith (M.unionWith S.union) cd

422+

423+ unconditionalDeps :: [Term] -> Deps

424+ unconditionalDeps = unionMap (getDepsTerm vs bs cd)

425+

426+ conditionalDeps :: Name -> [Term] -> Deps

427+ conditionalDeps n

428+ = ins (M.singleton (n, Result) S.empty) . unionMap (getDepsArgs n) . zip indices

429+ where

430+ indices = map Just [0 .. getArity n - 1] ++ repeat Nothing

431+ getDepsArgs n (Just i, t) = getDepsTerm vs bs (S.insert (n, Arg i) cd) t -- conditional

432+ getDepsArgs n (Nothing, t) = getDepsTerm vs bs cd t -- unconditional

433+

434+ methodDeps :: Name -> (Int, Term) -> Deps

435+ methodDeps ctorName (methNo, t)

436+ = getDepsTerm (vars `M.union` vs) (bruijns ++ bs) cond body

437+ where

438+ vars = M.fromList [(v, VI

439+ { viDeps = deps i

440+ , viFunArg = Just i

441+ , viMethod = Nothing

442+ }) | (v, i) <- zip args [0..]]

443+ deps i = M.singleton (metameth, Arg i) S.empty

444+ bruijns = reverse [\cd -> M.singleton cd (deps i) | i <- [0 .. length args - 1]]

445+ cond = S.singleton (metameth, Result)

446+ metameth = mkFieldName ctorName methNo

447+ (args, body) = unfoldLams t

448+

449+ -- projections

450+ getDepsTerm vs bs cd (Proj t (-1)) = getDepsTerm vs bs cd t -- naturals, (S n) -> n

451+ getDepsTerm vs bs cd (Proj t i) = error $ "cannot[1] analyse projection !" ++ show i ++ " of " ++ show t

452+

453+ -- the easy cases

454+ getDepsTerm vs bs cd (Constant _) = M.empty

455+ getDepsTerm vs bs cd (TType _) = M.empty

456+ getDepsTerm vs bs cd Erased = M.empty

457+ getDepsTerm vs bs cd Impossible = M.empty

458+

459+ getDepsTerm vs bs cd t = error $ "cannot get deps of: " ++ show t

460+

461+ -- Get the number of arguments that might be considered for erasure.

462+ getArity :: Name -> Int

463+ getArity (SN (WhereN i' ctorName (MN i field)))

464+ | Just (TyDecl (DCon _ _) ty) <- lookupDefExact ctorName ctx

465+ = let argTys = map snd $ getArgTys ty

466+ in if i <= length argTys

467+ then length $ getArgTys (argTys !! i)

468+ else error $ "invalid field number " ++ show i ++ " for " ++ show ctorName

469+

470+ | otherwise = error $ "unknown instance constructor: " ++ show ctorName

471+

472+ getArity n = case lookupDefExact n ctx of

473+ Just (CaseOp ci ty tys def tot cdefs) -> length tys

474+ Just (TyDecl (DCon tag arity) _) -> arity

475+ Just (TyDecl (Ref) ty) -> length $ getArgTys ty

476+ Just (Operator ty arity op) -> arity

477+ Just df -> error $ "Erasure/getArity: unrecognised entity '"

478+ ++ show n ++ "' with definition: " ++ show df

479+ Nothing -> error $ "Erasure/getArity: definition not found for " ++ show n

480+

481+ -- convert applications of lambdas to lets

482+ -- Note that this transformation preserves de bruijn numbering

483+ lamToLet :: [Term] -> Term -> Term

484+ lamToLet xs (App f x) = lamToLet (x:xs) f

485+ lamToLet (x:xs) (Bind n (Lam ty) t) = Bind n (Let ty x) (lamToLet xs t)

486+ lamToLet (x:xs) t = App (lamToLet xs t) x

487+ lamToLet [] t = t

488+

489+ -- split "\x_i -> T(x_i)" into [x_i] and T

490+ unfoldLams :: Term -> ([Name], Term)

491+ unfoldLams (Bind n (Lam ty) t) = let (ns,t') = unfoldLams t in (n:ns, t')

492+ unfoldLams t = ([], t)

493+

494+ union :: Deps -> Deps -> Deps

495+ union = M.unionWith (M.unionWith S.union)

496+

497+ unions :: [Deps] -> Deps

498+ unions = M.unionsWith (M.unionWith S.union)

499+

500+ unionMap :: (a -> Deps) -> [a] -> Deps

501+ unionMap f = M.unionsWith (M.unionWith S.union) . map f

502+

503+-- Make a field name out of a data constructor name and field number.

504+mkFieldName :: Name -> Int -> Name

505+mkFieldName ctorName fieldNo = SN (WhereN fieldNo ctorName $ sMN fieldNo "field")

src/Idris/IBC.hs+30−23

@@ -19,6 +19,7 @@ import Data.Vector.Binary

19import Data.List

20import Data.ByteString.Lazy as B hiding (length, elem, map)

21import qualified Data.Text as T

22+import qualified Data.Set as S

22

23

23import Control.Monad

24import Control.Monad

24import Control.Monad.State.Strict hiding (get, put)

25import Control.Monad.State.Strict hiding (get, put)

@@ -29,7 +30,7 @@ import Codec.Compression.Zlib (compress)

29import Util.Zlib (decompressEither)

30import Util.Zlib (decompressEither)

30

31

31ibcVersion :: Word8

32ibcVersion :: Word8

32−ibcVersion = 65

33+ibcVersion = 67

33

34

34data IBCFile = IBCFile { ver :: Word8,

35data IBCFile = IBCFile { ver :: Word8,

35 sourcefile :: FilePath,

36 sourcefile :: FilePath,

@@ -65,7 +66,8 @@ data IBCFile = IBCFile { ver :: Word8,

65 ibc_errorhandlers :: [Name],

66 ibc_errorhandlers :: [Name],

66 ibc_function_errorhandlers :: [(Name, Name, Name)], -- fn, arg, handler

67 ibc_function_errorhandlers :: [(Name, Name, Name)], -- fn, arg, handler

67 ibc_metavars :: [(Name, (Maybe Name, Int, Bool))],

68 ibc_metavars :: [(Name, (Maybe Name, Int, Bool))],

68− ibc_patdefs :: [(Name, ([([Name], Term, Term)], [PTerm]))]

69+ ibc_patdefs :: [(Name, ([([Name], Term, Term)], [PTerm]))],

70+ ibc_postulates :: [Name]

69 }

71 }

70 deriving Show

72 deriving Show

71{-!

73{-!

@@ -73,7 +75,7 @@ deriving instance Binary IBCFile

73!-}

75!-}

74

76

75initIBC :: IBCFile

77initIBC :: IBCFile

76−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

78+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

77

79

78loadIBC :: FilePath -> Idris ()

80loadIBC :: FilePath -> Idris ()

79loadIBC fp = do imps <- getImported

81loadIBC fp = do imps <- getImported

@@ -236,6 +238,7 @@ ibc i (IBCMetavar n) f =

236 case lookup n (idris_metavars i) of

238 case lookup n (idris_metavars i) of

237 Nothing -> return f

239 Nothing -> return f

238 Just t -> return f { ibc_metavars = (n, t) : ibc_metavars f }

240 Just t -> return f { ibc_metavars = (n, t) : ibc_metavars f }

241+ibc i (IBCPostulate n) f = return f { ibc_postulates = n : ibc_postulates f }

239

242

240process :: IBCFile -> FilePath -> Idris ()

243process :: IBCFile -> FilePath -> Idris ()

241process i fn

244process i fn

@@ -278,6 +281,7 @@ process i fn

278 pErrorHandlers (ibc_errorhandlers i)

281 pErrorHandlers (ibc_errorhandlers i)

279 pFunctionErrorHandlers (ibc_function_errorhandlers i)

282 pFunctionErrorHandlers (ibc_function_errorhandlers i)

280 pMetavars (ibc_metavars i)

283 pMetavars (ibc_metavars i)

284+ pPostulates (ibc_postulates i)

281

285

282timestampOlder :: FilePath -> FilePath -> IO ()

286timestampOlder :: FilePath -> FilePath -> IO ()

283timestampOlder src ibc = do srct <- getModificationTime src

287timestampOlder src ibc = do srct <- getModificationTime src

@@ -286,6 +290,11 @@ timestampOlder src ibc = do srct <- getModificationTime src

286 then fail "Needs reloading"

290 then fail "Needs reloading"

287 else return ()

291 else return ()

288

292

293+pPostulates :: [Name] -> Idris ()

294+pPostulates ns = do

295+ i <- getIState

296+ putIState i{ idris_postulates = idris_postulates i `S.union` S.fromList ns }

297+

289pImports :: [FilePath] -> Idris ()

298pImports :: [FilePath] -> Idris ()

290pImports fs

299pImports fs

291 = do mapM_ (\f -> do i <- getIState

300 = do mapM_ (\f -> do i <- getIState

@@ -1093,10 +1102,6 @@ safeToEnum label x' = result

1093 = error $ label ++ ": corrupted binary representation in IBC"

1102 = error $ label ++ ": corrupted binary representation in IBC"

1094 | otherwise = toEnum x

1103 | otherwise = toEnum x

1095

1104

1096−instance Binary Forceability where

1097− put = putWord8 . fromIntegral . fromEnum

1098− get = safeToEnum "Forceability" `fmap` getWord8

1099−

1100instance Binary PReason where

1105instance Binary PReason where

1101 put x

1106 put x

1102 = case x of

1107 = case x of

@@ -1156,7 +1161,7 @@ instance Binary MetaInformation where

1156 return (DataMI x1)

1161 return (DataMI x1)

1157

1162

1158instance Binary IBCFile where

1163instance Binary IBCFile where

1159− put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35)

1164+ put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36)

1160 = {-# SCC "putIBCFile" #-}

1165 = {-# SCC "putIBCFile" #-}

1161 do put x1

1166 do put x1

1162 put x2

1167 put x2

@@ -1193,6 +1198,7 @@ instance Binary IBCFile where

1193 put x33

1198 put x33

1194 put x34

1199 put x34

1195 put x35

1200 put x35

1201+ put x36

1196

1202

1197 get

1203 get

1198 = do x1 <- get

1204 = do x1 <- get

@@ -1231,7 +1237,8 @@ instance Binary IBCFile where

1231 x33 <- get

1237 x33 <- get

1232 x34 <- get

1238 x34 <- get

1233 x35 <- get

1239 x35 <- get

1240+ x36 <- get

1234− return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35)

1241+ return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36)

1235 else return (initIBC { ver = x1 })

1242 else return (initIBC { ver = x1 })

1236

1243

1237instance Binary DataOpt where

1244instance Binary DataOpt where

@@ -1317,13 +1324,13 @@ instance Binary FixDecl where

1317instance Binary ArgOpt where

1324instance Binary ArgOpt where

1318 put x

1325 put x

1319 = case x of

1326 = case x of

1320− Lazy -> putWord8 0

1327+ HideDisplay -> putWord8 0

1321− HideDisplay -> putWord8 1

1328+ InaccessibleArg -> putWord8 1

1322 get

1329 get

1323 = do i <- getWord8

1330 = do i <- getWord8

1324 case i of

1331 case i of

1325− 0 -> return Lazy

1332+ 0 -> return HideDisplay

1326− 1 -> return HideDisplay

1333+ 1 -> return InaccessibleArg

1327 _ -> error "Corrupted binary data for Static"

1334 _ -> error "Corrupted binary data for Static"

1328

1335

1329instance Binary Static where

1336instance Binary Static where

@@ -2037,16 +2044,18 @@ instance (Binary t) => Binary (PArg' t) where

2037 put x3

2044 put x3

2038 put x4

2045 put x4

2039 put x5

2046 put x5

2040− PExp x1 x2 x3 ->

2047+ PExp x1 x2 x3 x4 ->

2041 do putWord8 1

2048 do putWord8 1

2042 put x1

2049 put x1

2043 put x2

2050 put x2

2044 put x3

2051 put x3

2052+ put x4

2045− PConstraint x1 x2 x3 ->

2053+ PConstraint x1 x2 x3 x4 ->

2046 do putWord8 2

2054 do putWord8 2

2047 put x1

2055 put x1

2048 put x2

2056 put x2

2049 put x3

2057 put x3

2058+ put x4

2050 PTacImplicit x1 x2 x3 x4 x5 ->

2059 PTacImplicit x1 x2 x3 x4 x5 ->

2051 do putWord8 3

2060 do putWord8 3

2052 put x1

2061 put x1

@@ -2066,11 +2075,13 @@ instance (Binary t) => Binary (PArg' t) where

2066 1 -> do x1 <- get

2075 1 -> do x1 <- get

2067 x2 <- get

2076 x2 <- get

2068 x3 <- get

2077 x3 <- get

2078+ x4 <- get

2069− return (PExp x1 x2 x3)

2079+ return (PExp x1 x2 x3 x4)

2070 2 -> do x1 <- get

2080 2 -> do x1 <- get

2071 x2 <- get

2081 x2 <- get

2072 x3 <- get

2082 x3 <- get

2083+ x4 <- get

2073− return (PConstraint x1 x2 x3)

2084+ return (PConstraint x1 x2 x3 x4)

2074 3 -> do x1 <- get

2085 3 -> do x1 <- get

2075 x2 <- get

2086 x2 <- get

2076 x3 <- get

2087 x3 <- get

@@ -2096,17 +2107,13 @@ instance Binary ClassInfo where

2096 return (CI x1 x2 x3 x4 x5 [])

2107 return (CI x1 x2 x3 x4 x5 [])

2097

2108

2098instance Binary OptInfo where

2109instance Binary OptInfo where

2099− put (Optimise x1 x2 x3 x4)

2110+ put (Optimise x1 x2)

2100 = do put x1

2111 = do put x1

2101 put x2

2112 put x2

2102− put x3

2103− put x4

2104 get

2113 get

2105 = do x1 <- get

2114 = do x1 <- get

2106 x2 <- get

2115 x2 <- get

2107− x3 <- get

2108− x4 <- get

2109− return (Optimise x1 x2 x3 x4)

2116+ return (Optimise x1 x2)

2110

2117

2111instance Binary TypeInfo where

2118instance Binary TypeInfo where

2112 put (TI x1 x2 x3 x4) = do put x1

2119 put (TI x1 x2 x3 x4) = do put x1

src/Idris/IdeSlave.hs+2

@@ -151,6 +151,7 @@ data IdeSlaveCommand = REPLCompletions String

151 | Apropos String

152 | GetOpts

153 | SetOpt Opt Bool

154+ | Metavariables Int -- ^^ the Int is the column count for pretty-printing

154 deriving Show

155 deriving Show

155

156

156sexpToCommand :: SExp -> Maybe IdeSlaveCommand

157sexpToCommand :: SExp -> Maybe IdeSlaveCommand

@@ -174,6 +175,7 @@ sexpToCommand (SymbolAtom "get-options")

174sexpToCommand (SexpList [SymbolAtom "set-option", SymbolAtom s, BoolAtom b])

175sexpToCommand (SexpList [SymbolAtom "set-option", SymbolAtom s, BoolAtom b])

175 | Just opt <- lookup s opts = Just (SetOpt opt b)

176 | Just opt <- lookup s opts = Just (SetOpt opt b)

176 where opts = [("show-implicits", ShowImpl), ("error-context", ErrContext)] --TODO support more

177 where opts = [("show-implicits", ShowImpl), ("error-context", ErrContext)] --TODO support more

178+sexpToCommand (SexpList [SymbolAtom "metavariables", IntegerAtom cols]) = Just (Metavariables (fromIntegral cols))

177sexpToCommand _ = Nothing

179sexpToCommand _ = Nothing

178

180

179parseMessage :: String -> Either Err (SExp, Integer)

181parseMessage :: String -> Either Err (SExp, Integer)

src/Idris/ParseExpr.hs+29−15

@@ -150,15 +150,23 @@ extension syn (Rule ssym ptm _)

150 update ns (PRef fc n) = case lookup n ns of

151 Just (SynTm t) -> t

152 _ -> PRef fc n

153+ update ns (PLam n ty sc)

153− update ns (PLam n ty sc) = PLam (updateB ns n) (update ns ty) (update (dropn n ns) sc)

154+ = PLam (updateB ns n) (update ns ty) (update (dropn n ns) sc)

155+ update ns (PPi p n ty sc)

156+ = PPi (updTacImp ns p) (updateB ns n)

154− update ns (PPi p n ty sc) = PPi p (updateB ns n) (update ns ty) (update (dropn n ns) sc)

157+ (update ns ty) (update (dropn n ns) sc)

158+ update ns (PLet n ty val sc)

155− update ns (PLet n ty val sc) = PLet (updateB ns n) (update ns ty) (update ns val)

159+ = PLet (updateB ns n) (update ns ty)

156− (update (dropn n ns) sc)

160+ (update ns val) (update (dropn n ns) sc)

161+ update ns (PApp fc t args)

157− update ns (PApp fc t args) = PApp fc (update ns t) (map (fmap (update ns)) args)

162+ = PApp fc (update ns t) (map (fmap (update ns)) args)

163+ update ns (PAppBind fc t args)

158− update ns (PAppBind fc t args) = PAppBind fc (update ns t) (map (fmap (update ns)) args)

164+ = PAppBind fc (update ns t) (map (fmap (update ns)) args)

165+ update ns (PCase fc c opts)

159− update ns (PCase fc c opts) = PCase fc (update ns c) (map (pmap (update ns)) opts)

166+ = PCase fc (update ns c) (map (pmap (update ns)) opts)

160 update ns (PPair fc p l r) = PPair fc p (update ns l) (update ns r)

167 update ns (PPair fc p l r) = PPair fc p (update ns l) (update ns r)

168+ update ns (PDPair fc p l t r)

161− update ns (PDPair fc p l t r) = PDPair fc p (update ns l) (update ns t) (update ns r)

169+ = PDPair fc p (update ns l) (update ns t) (update ns r)

162 update ns (PAlternative a as) = PAlternative a (map (update ns) as)

170 update ns (PAlternative a as) = PAlternative a (map (update ns) as)

163 update ns (PHidden t) = PHidden (update ns t)

171 update ns (PHidden t) = PHidden (update ns t)

164 update ns (PDoBlock ds) = PDoBlock $ upd ns ds

172 update ns (PDoBlock ds) = PDoBlock $ upd ns ds

@@ -176,6 +184,9 @@ extension syn (Rule ssym ptm _)

176 update ns (PGoal fc r n sc) = PGoal fc (update ns r) n (update ns sc)

184 update ns (PGoal fc r n sc) = PGoal fc (update ns r) n (update ns sc)

177 update ns t = t

185 update ns t = t

178

186

187+ updTacImp ns (TacImp o st scr) = TacImp o st (update ns scr)

188+ updTacImp _ x = x

189+

179{- | Parses a (normal) built-in expression

190{- | Parses a (normal) built-in expression

180@

191@

181InternalExpr ::=

192InternalExpr ::=

@@ -788,18 +799,15 @@ Pi ::=

788

799

789pi :: SyntaxInfo -> IdrisParser PTerm

800pi :: SyntaxInfo -> IdrisParser PTerm

790pi syn =

801pi syn =

791− do opts <- -- if implicitAllowed syn -- laziness is top level only

802+ do opts <- piOpts syn

792− -- then option [] (do lchar '|'; return [Lazy])

793− -- else return []

794− return []

795− st <- static

803+ st <- static

796 (do try (lchar '('); xt <- typeDeclList syn; lchar ')'

804 (do try (lchar '('); xt <- typeDeclList syn; lchar ')'

797 symbol "->"

805 symbol "->"

798 sc <- expr syn

806 sc <- expr syn

799 return (bindList (PPi (Exp opts st False)) xt sc)) <|> (do

807 return (bindList (PPi (Exp opts st False)) xt sc)) <|> (do

800 lchar '{'

808 lchar '{'

801 (do reserved "auto"

809 (do reserved "auto"

802− when (Lazy `elem` opts || (st == Static)) $ fail "auto type constraints can not be lazy or static"

810+ when (st == Static) $ fail "auto type constraints can not be lazy or static"

803 xt <- typeDeclList syn

811 xt <- typeDeclList syn

804 lchar '}'

812 lchar '}'

805 symbol "->"

813 symbol "->"

@@ -808,7 +816,7 @@ pi syn =

808 (TacImp [] Dynamic (PTactics [Trivial]))) xt sc))

816 (TacImp [] Dynamic (PTactics [Trivial]))) xt sc))

809 <|> (do

817 <|> (do

810 reserved "default"

818 reserved "default"

811− when (Lazy `elem` opts || (st == Static)) $ fail "default tactic constraints can not be lazy or static"

819+ when (st == Static) $ fail "default tactic constraints can not be lazy or static"

812 script <- simpleExpr syn

820 script <- simpleExpr syn

813 xt <- typeDeclList syn

821 xt <- typeDeclList syn

814 lchar '}'

822 lchar '}'

@@ -824,6 +832,12 @@ pi syn =

824 else do fail "no implicit arguments allowed here"))

832 else do fail "no implicit arguments allowed here"))

825 <?> "dependent type signature"

833 <?> "dependent type signature"

826

834

835+piOpts :: SyntaxInfo -> IdrisParser [ArgOpt]

836+piOpts syn | implicitAllowed syn =

837+ lchar '.' *> return [InaccessibleArg]

838+ <|> return []

839+piOpts syn = return []

840+

827{- | Parses a type constraint list

841{- | Parses a type constraint list

828

842

829@

843@

src/Idris/Parser.hs+9−3

@@ -17,14 +17,15 @@ import qualified Text.Parser.Char as Chr

17import qualified Text.Parser.Token.Highlight as Hi

18

19import Text.PrettyPrint.ANSI.Leijen (Doc, plain)

20+import qualified Text.PrettyPrint.ANSI.Leijen as ANSI

20

21

21−import Idris.AbsSyntax

22+import Idris.AbsSyntax hiding (namespace, params)

22import Idris.DSL

23import Idris.DSL

23import Idris.Imports

24import Idris.Imports

24import Idris.Delaborate

25import Idris.Delaborate

25import Idris.Error

26import Idris.Error

26import Idris.ElabDecls

27import Idris.ElabDecls

27−import Idris.ElabTerm hiding (namespace, params)

28+import Idris.ElabTerm

28import Idris.Coverage

29import Idris.Coverage

29import Idris.IBC

30import Idris.IBC

30import Idris.Unlit

31import Idris.Unlit

@@ -1120,6 +1121,11 @@ findFC x = let s = show (plain x) in

1120 (col, ':':msg) -> let pos = (read line, read col) in

1121 (col, ':':msg) -> let pos = (read line, read col) in

1121 (FC failname pos pos, msg)

1122 (FC failname pos pos, msg)

1122

1123

1124+-- | Check if the coloring matches the options and corrects if necessary

1125+fixColour :: Bool -> ANSI.Doc -> ANSI.Doc

1126+fixColour False doc = ANSI.plain doc

1127+fixColour True doc = doc

1128+

1123-- | A program is a list of declarations, possibly with associated

1129-- | A program is a list of declarations, possibly with associated

1124-- documentation strings.

1130-- documentation strings.

1125parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->

1131parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->

@@ -1132,7 +1138,7 @@ parseProg syn fname input mrk

1132 let (fc, msg) = findFC doc

1138 let (fc, msg) = findFC doc

1133 i <- getIState

1139 i <- getIState

1134 case idris_outputmode i of

1140 case idris_outputmode i of

1135− RawOutput -> ihputStrLn (idris_outh i) (show doc)

1141+ RawOutput -> ihputStrLn (idris_outh i) (show $ fixColour (idris_colourRepl i) doc)

1136 IdeSlave n -> ihWarn (idris_outh i) fc (P.text msg)

1142 IdeSlave n -> ihWarn (idris_outh i) fc (P.text msg)

1137 putIState (i { errSpan = Just fc })

1143 putIState (i { errSpan = Just fc })

1138 return []

1144 return []

src/Idris/PartialEval.hs+1−1

@@ -124,7 +124,7 @@ getSpecApps ist env tm = ga env (explicitNames tm) where

124 | imparg imp = (ImplicitD, tm)

125 | otherwise = (ExplicitD, (P Ref (sUN (show n ++ "arg")) Erased))

126

127− imparg (PExp _ _ _) = False

127+ imparg (PExp _ _ _ _) = False

128 imparg _ = True

129

130 buildApp env [] [] _ _ = []

src/Idris/Prover.hs+6−5

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

7import Idris.Core.Typecheck

8

9import Idris.AbsSyntax

10+import Idris.AbsSyntaxTree

10import Idris.Delaborate

11import Idris.Delaborate

11import Idris.ElabDecls

12import Idris.ElabDecls

12import Idris.ElabTerm

13import Idris.ElabTerm

@@ -33,7 +34,7 @@ prover lit x =

33 i <- getIState

34 i <- getIState

34 case lookupTy x ctxt of

35 case lookupTy x ctxt of

35 [t] -> if elem x (map fst (idris_metavars i))

36 [t] -> if elem x (map fst (idris_metavars i))

36− then prove ctxt lit x t

37+ then prove (idris_optimisation i) ctxt lit x t

37 else ifail $ show x ++ " is not a metavariable"

38 else ifail $ show x ++ " is not a metavariable"

38 _ -> fail "No such metavariable"

39 _ -> fail "No such metavariable"

39

40

@@ -56,8 +57,8 @@ assumptionNames e

56 names ((MN _ _, _) : bs) = names bs

57 names ((MN _ _, _) : bs) = names bs

57 names ((n, _) : bs) = show n : names bs

58 names ((n, _) : bs) = show n : names bs

58

59

59−prove :: Context -> Bool -> Name -> Type -> Idris ()

60+prove :: Ctxt OptInfo -> Context -> Bool -> Name -> Type -> Idris ()

60−prove ctxt lit n ty

61+prove opt ctxt lit n ty

61 = do let ps = initElaborator n ctxt ty

62 = do let ps = initElaborator n ctxt ty

62 ideslavePutSExp "start-proof-mode" n

63 ideslavePutSExp "start-proof-mode" n

63 (tm, prf) <- ploop n True ("-" ++ show n) [] (ES (ps, []) "" Nothing) Nothing

64 (tm, prf) <- ploop n True ("-" ++ show n) [] (ES (ps, []) "" Nothing) Nothing

@@ -67,7 +68,7 @@ prove ctxt lit n ty

67 ideslavePutSExp "end-proof-mode" n

68 ideslavePutSExp "end-proof-mode" n

68 let proofs = proof_list i

69 let proofs = proof_list i

69 putIState (i { proof_list = (n, prf) : proofs })

70 putIState (i { proof_list = (n, prf) : proofs })

70− let tree = simpleCase False True False CompileTime (fileFC "proof") [] [([], P Ref n ty, tm)]

71+ let tree = simpleCase False True False CompileTime (fileFC "proof") [] [] [([], P Ref n ty, tm)]

71 logLvl 3 (show tree)

72 logLvl 3 (show tree)

72 (ptm, pty) <- recheckC (fileFC "proof") [] tm

73 (ptm, pty) <- recheckC (fileFC "proof") [] tm

73 logLvl 5 ("Proof type: " ++ show pty ++ "\n" ++

74 logLvl 5 ("Proof type: " ++ show pty ++ "\n" ++

@@ -77,7 +78,7 @@ prove ctxt lit n ty

77 Error e -> ierror (CantUnify False ty pty e [] 0)

78 Error e -> ierror (CantUnify False ty pty e [] 0)

78 ptm' <- applyOpts ptm

79 ptm' <- applyOpts ptm

79 updateContext (addCasedef n (CaseInfo True False) False False True False

80 updateContext (addCasedef n (CaseInfo True False) False False True False

80− []

81+ [] [] -- argtys, inaccArgs

81 [Right (P Ref n ty, ptm)]

82 [Right (P Ref n ty, ptm)]

82 [([], P Ref n ty, ptm)]

83 [([], P Ref n ty, ptm)]

84 [([], P Ref n ty, ptm)]

src/Idris/Providers.hs+2−1

@@ -11,7 +11,8 @@ import Debug.Trace

11

12-- | Wrap a type provider in the type of type providers

13providerTy :: FC -> PTerm -> PTerm

14+providerTy fc tm

14−providerTy fc tm = PApp fc (PRef fc $ sUN "Provider") [PExp 0 [] tm]

15+ = PApp fc (PRef fc $ sUN "Provider") [PExp 0 [] (sMN 0 "pvarg") tm]

15

16

16ioret = sUN "prim_io_return"

17ioret = sUN "prim_io_return"

17ermod = sNS (sUN "Error") ["Providers"]

18ermod = sNS (sUN "Error") ["Providers"]

src/Idris/REPL.hs+154−103

@@ -8,16 +8,16 @@ import Idris.Apropos (apropos)

8import Idris.REPLParser

9import Idris.ElabDecls

10import Idris.ElabTerm

11+import Idris.Erasure

11import Idris.Error

12import Idris.Error

12import Idris.ErrReverse

13import Idris.ErrReverse

13import Idris.Delaborate

14import Idris.Delaborate

14import Idris.Docstrings (Docstring, overview, renderDocstring)

15import Idris.Docstrings (Docstring, overview, renderDocstring)

15import Idris.IdrisDoc

16import Idris.IdrisDoc

16import Idris.Prover

17import Idris.Prover

17−import Idris.Parser

18+import Idris.Parser hiding (indent)

18import Idris.Primitives

19import Idris.Primitives

19import Idris.Coverage

20import Idris.Coverage

20−import Idris.UnusedArgs

21import Idris.Docs hiding (Doc)

22import Idris.Help

23import Idris.Completion

@@ -81,8 +81,6 @@ import Data.Word (Word)

81import Data.Either (partitionEithers)

82import Control.DeepSeq

83

84−import qualified Text.PrettyPrint.ANSI.Leijen as ANSI

85−

86import Debug.Trace

84import Debug.Trace

87

85

88-- | Run the REPL

86-- | Run the REPL

@@ -220,83 +218,133 @@ ideslave orig mods

220 (f:_) -> f

218 (f:_) -> f

221 _ -> ""

219 _ -> ""

222 case IdeSlave.sexpToCommand sexp of

220 case IdeSlave.sexpToCommand sexp of

223− Just (IdeSlave.Interpret cmd) ->

221+ Just cmd -> runIdeSlaveCommand id orig fn mods cmd

224− do c <- colourise

225− case parseCmd i "(input)" cmd of

226− Failure err -> iPrintError $ show (fixColour c err)

227− Success (Prove n') -> do iPrintResult ""

228− idrisCatch

229− (process stdout fn (Prove n'))

230− (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)

231− isetPrompt (mkPrompt mods)

232− Success cmd -> idrisCatch

233− (ideslaveProcess fn cmd)

234− (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)

235− Just (IdeSlave.REPLCompletions str) ->

236− do (unused, compls) <- replCompletion (reverse str, "")

237− let good = IdeSlave.SexpList [IdeSlave.SymbolAtom "ok", IdeSlave.toSExp (map replacement compls, reverse unused)]

238− runIO $ putStrLn $ IdeSlave.convSExp "return" good id

239− Just (IdeSlave.LoadFile filename) ->

240− do clearErr

241− putIState (orig { idris_options = idris_options i,

242− idris_outputmode = (IdeSlave id) })

243− loadInputs stdout [filename]

244− isetPrompt (mkPrompt [filename])

245− -- Report either success or failure

246− i <- getIState

247− case (errSpan i) of

248− Nothing -> iPrintResult $ "loaded " ++ filename

249− Just x -> iPrintError $ "didn't load " ++ filename

250− ideslave orig [filename]

251− Just (IdeSlave.TypeOf name) ->

252− case splitName name of

253− Left err -> iPrintError err

254− Right n -> process stdout "(ideslave)"

255− (Check (PRef (FC "(ideslave)" (0,0) (0,0)) n))

256− Just (IdeSlave.DocsFor name) ->

257− case splitName name of

258− Left err -> iPrintError err

259− Right n -> process stdout "(ideslave)" (DocStr n)

260− Just (IdeSlave.CaseSplit line name) ->

261− process stdout fn (CaseSplitAt False line (sUN name))

262− Just (IdeSlave.AddClause line name) ->

263− process stdout fn (AddClauseFrom False line (sUN name))

264− Just (IdeSlave.AddProofClause line name) ->

265− process stdout fn (AddProofClauseFrom False line (sUN name))

266− Just (IdeSlave.AddMissing line name) ->

267− process stdout fn (AddMissing False line (sUN name))

268− Just (IdeSlave.MakeWithBlock line name) ->

269− process stdout fn (MakeWith False line (sUN name))

270− Just (IdeSlave.ProofSearch line name hints) ->

271− process stdout fn (DoProofSearch False line (sUN name) (map sUN hints))

272− Just (IdeSlave.Apropos a) ->

273− process stdout fn (Apropos a)

274− Just (IdeSlave.GetOpts) ->

275− do ist <- getIState

276− let opts = idris_options ist

277− let impshow = opt_showimp opts

278− let errCtxt = opt_errContext opts

279− let options = (IdeSlave.SymbolAtom "ok",

280− [(IdeSlave.SymbolAtom "show-implicits", impshow),

281− (IdeSlave.SymbolAtom "error-context", errCtxt)])

282− runIO . putStrLn $ IdeSlave.convSExp "return" options id

283− Just (IdeSlave.SetOpt IdeSlave.ShowImpl b) ->

284− do setImpShow b

285− let msg = (IdeSlave.SymbolAtom "ok", b)

286− runIO . putStrLn $ IdeSlave.convSExp "return" msg id

287− Just (IdeSlave.SetOpt IdeSlave.ErrContext b) ->

288− do setErrContext b

289− let msg = (IdeSlave.SymbolAtom "ok", b)

290− runIO . putStrLn $ IdeSlave.convSExp "return" msg id

291− Nothing -> do iPrintError "did not understand")

222+ Nothing -> iPrintError "did not understand" )

292 (\e -> do iPrintError $ show e))

223 (\e -> do iPrintError $ show e))

293 (\e -> do iPrintError $ show e)

224 (\e -> do iPrintError $ show e)

294 ideslave orig mods

225 ideslave orig mods

226+

227+-- | Run IDESlave commands

228+runIdeSlaveCommand :: Integer -- ^^ The continuation ID for the client

229+ -> IState -- ^^ The original IState

230+ -> FilePath -- ^^ The current open file

231+ -> [FilePath] -- ^^ The currently loaded modules

232+ -> IdeSlave.IdeSlaveCommand -- ^^ The command to process

233+ -> Idris ()

234+runIdeSlaveCommand id orig fn mods (IdeSlave.Interpret cmd) =

235+ do c <- colourise

236+ i <- getIState

237+ case parseCmd i "(input)" cmd of

238+ Failure err -> iPrintError $ show (fixColour c err)

239+ Success (Prove n') -> do iPrintResult ""

240+ idrisCatch

241+ (process stdout fn (Prove n'))

242+ (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)

243+ isetPrompt (mkPrompt mods)

244+ Success cmd -> idrisCatch

245+ (ideslaveProcess fn cmd)

246+ (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)

247+runIdeSlaveCommand id orig fn mods (IdeSlave.REPLCompletions str) =

248+ do (unused, compls) <- replCompletion (reverse str, "")

249+ let good = IdeSlave.SexpList [IdeSlave.SymbolAtom "ok",

250+ IdeSlave.toSExp (map replacement compls,

251+ reverse unused)]

252+ runIO $ putStrLn $ IdeSlave.convSExp "return" good id

253+runIdeSlaveCommand id orig fn mods (IdeSlave.LoadFile filename) =

254+ do i <- getIState

255+ clearErr

256+ putIState (orig { idris_options = idris_options i,

257+ idris_outputmode = (IdeSlave id) })

258+ loadInputs stdout [filename]

259+ isetPrompt (mkPrompt [filename])

260+ -- Report either success or failure

261+ i <- getIState

262+ case (errSpan i) of

263+ Nothing -> iPrintResult $ "loaded " ++ filename

264+ Just x -> iPrintError $ "didn't load " ++ filename

265+ ideslave orig [filename]

266+runIdeSlaveCommand id orig fn mods (IdeSlave.TypeOf name) =

267+ case splitName name of

268+ Left err -> iPrintError err

269+ Right n -> process stdout "(ideslave)"

270+ (Check (PRef (FC "(ideslave)" (0,0) (0,0)) n))

271+ where splitName :: String -> Either String Name

272+ splitName s = case reverse $ splitOn "." s of

273+ [] -> Left ("Didn't understand name '" ++ s ++ "'")

274+ [n] -> Right $ sUN n

275+ (n:ns) -> Right $ sNS (sUN n) ns

276+runIdeSlaveCommand id orig fn mods (IdeSlave.DocsFor name) =

277+ case splitName name of

278+ Left err -> iPrintError err

279+ Right n -> process stdout "(ideslave)" (DocStr n)

295 where splitName :: String -> Either String Name

280 where splitName :: String -> Either String Name

296 splitName s = case reverse $ splitOn "." s of

281 splitName s = case reverse $ splitOn "." s of

297 [] -> Left ("Didn't understand name '" ++ s ++ "'")

282 [] -> Left ("Didn't understand name '" ++ s ++ "'")

298 [n] -> Right $ sUN n

283 [n] -> Right $ sUN n

299 (n:ns) -> Right $ sNS (sUN n) ns

284 (n:ns) -> Right $ sNS (sUN n) ns

285+runIdeSlaveCommand id orig fn mods (IdeSlave.CaseSplit line name) =

286+ process stdout fn (CaseSplitAt False line (sUN name))

287+runIdeSlaveCommand id orig fn mods (IdeSlave.AddClause line name) =

288+ process stdout fn (AddClauseFrom False line (sUN name))

289+runIdeSlaveCommand id orig fn mods (IdeSlave.AddProofClause line name) =

290+ process stdout fn (AddProofClauseFrom False line (sUN name))

291+runIdeSlaveCommand id orig fn mods (IdeSlave.AddMissing line name) =

292+ process stdout fn (AddMissing False line (sUN name))

293+runIdeSlaveCommand id orig fn mods (IdeSlave.MakeWithBlock line name) =

294+ process stdout fn (MakeWith False line (sUN name))

295+runIdeSlaveCommand id orig fn mods (IdeSlave.ProofSearch line name hints) =

296+ process stdout fn (DoProofSearch False line (sUN name) (map sUN hints))

297+runIdeSlaveCommand id orig fn mods (IdeSlave.Apropos a) =

298+ process stdout fn (Apropos a)

299+runIdeSlaveCommand id orig fn mods (IdeSlave.GetOpts) =

300+ do ist <- getIState

301+ let opts = idris_options ist

302+ let impshow = opt_showimp opts

303+ let errCtxt = opt_errContext opts

304+ let options = (IdeSlave.SymbolAtom "ok",

305+ [(IdeSlave.SymbolAtom "show-implicits", impshow),

306+ (IdeSlave.SymbolAtom "error-context", errCtxt)])

307+ runIO . putStrLn $ IdeSlave.convSExp "return" options id

308+runIdeSlaveCommand id orig fn mods (IdeSlave.SetOpt IdeSlave.ShowImpl b) =

309+ do setImpShow b

310+ let msg = (IdeSlave.SymbolAtom "ok", b)

311+ runIO . putStrLn $ IdeSlave.convSExp "return" msg id

312+runIdeSlaveCommand id orig fn mods (IdeSlave.SetOpt IdeSlave.ErrContext b) =

313+ do setErrContext b

314+ let msg = (IdeSlave.SymbolAtom "ok", b)

315+ runIO . putStrLn $ IdeSlave.convSExp "return" msg id

316+runIdeSlaveCommand id orig fn mods (IdeSlave.Metavariables cols) =

317+ do ist <- getIState

318+ let mvs = reverse $ map fst (idris_metavars ist) \\ primDefs

319+ imp <- impShow

320+ let mvarTys = map (delabTy ist) mvs

321+ let res = (IdeSlave.SymbolAtom "ok",

322+ zipWith (\ n (prems, concl) -> (n, prems, concl))

323+ (map (IdeSlave.StringAtom . show) mvs)

324+ (map (sexpGoal ist cols imp [] . getGoal) mvarTys))

325+ runIO . putStrLn $ IdeSlave.convSExp "return" res id

326+ where getGoal :: PTerm -> ([(Name, PTerm)], PTerm)

327+ getGoal (PPi _ n t sc) = let (prems, conc) = getGoal sc

328+ in ((n, t):prems, conc)

329+ getGoal tm = ([], tm)

330+ sexpGoal :: IState -> Int -> Bool -> [Name] -> ([(Name, PTerm)], PTerm)

331+ -> ([(String, String, SpanList OutputAnnotation)],

332+ (String, SpanList OutputAnnotation))

333+ sexpGoal ist cols imp ns ([], concl) =

334+ let concl' = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $

335+ pprintPTerm imp (zip ns (repeat False)) [] concl

336+ in ([], concl')

337+ sexpGoal ist cols imp ns ((n, t):ps, concl) =

338+ let n' = case n of

339+ NS (UN nm) ns -> str nm

340+ UN nm | ('_':'_':_) <- str nm -> "_"

341+ | otherwise -> str nm

342+ _ -> "_"

343+ (t', spans) = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $

344+ pprintPTerm imp (zip ns (repeat False)) [] t

345+ rest = sexpGoal ist cols imp (n:ns) (ps, concl)

346+ in ((n', t', spans) : fst rest, snd rest)

347+

300

348

301ideslaveProcess :: FilePath -> Command -> Idris ()

349ideslaveProcess :: FilePath -> Command -> Idris ()

302ideslaveProcess fn Help = process stdout fn Help

350ideslaveProcess fn Help = process stdout fn Help

@@ -609,7 +657,6 @@ process h fn (DebugInfo n)

609 let d = lookupDef n (tt_ctxt i)

657 let d = lookupDef n (tt_ctxt i)

610 when (not (null d)) $ iputStrLn $ "Definition: " ++ (show (head d))

658 when (not (null d)) $ iputStrLn $ "Definition: " ++ (show (head d))

611 let cg = lookupCtxtName n (idris_callgraph i)

659 let cg = lookupCtxtName n (idris_callgraph i)

612− findUnusedArgs (map fst cg)

613 i <- getIState

660 i <- getIState

614 let cg' = lookupCtxtName n (idris_callgraph i)

661 let cg' = lookupCtxtName n (idris_callgraph i)

615 sc <- checkSizeChange n

662 sc <- checkSizeChange n

@@ -619,7 +666,8 @@ process h fn (DebugInfo n)

619process h fn (Info n)

666process h fn (Info n)

620 = do i <- getIState

667 = do i <- getIState

621 case lookupCtxt n (idris_classes i) of

668 case lookupCtxt n (idris_classes i) of

622− [c] -> classInfo c

669+ [c] -> do info <- classInfo c

670+ ihRenderResult h info

623 _ -> iPrintError "Not a class"

671 _ -> iPrintError "Not a class"

624process h fn (Search t) = iPrintError "Not implemented"

672process h fn (Search t) = iPrintError "Not implemented"

625-- FIXME: There is far too much repetition in the cases below!

673-- FIXME: There is far too much repetition in the cases below!

@@ -1009,28 +1057,31 @@ process h fn (MakeDoc s) =

1009 case result of Right _ -> iputStrLn "IdrisDoc generated"

1057 case result of Right _ -> iputStrLn "IdrisDoc generated"

1010 Left err -> iPrintError err

1058 Left err -> iPrintError err

1011

1059

1060+

1012−classInfo :: ClassInfo -> Idris ()

1061+classInfo :: ClassInfo -> Idris (Doc OutputAnnotation)

1013−classInfo ci = do iputStrLn "Methods:\n"

1062+classInfo ci = do ist <- getIState

1063+ ctxt <- getContext

1064+ return $

1065+ text "Parameters:" <+>

1066+ hsep (punctuate comma (map (prettyName False params') params)) <>

1067+ line <> line <>

1068+ text "Methods:" <> line <>

1014− mapM_ dumpMethod (class_methods ci)

1069+ indent 2 (vsep (map (dumpMethod ist) (class_methods ci))) <> line <> line <>

1015− iputStrLn ""

1016− iputStrLn "Default superclass instances:\n"

1070+ text "Default superclass instances:" <>

1071+ line <>

1017− mapM_ dumpDefaultInstance (class_default_superclasses ci)

1072+ indent 2 (vsep (map (dumpDefaultInstance ist) (class_default_superclasses ci))) <>

1018− iputStrLn ""

1073+ line <>

1019− iputStrLn "Instances:\n"

1074+ text "Instances:" <> line <>

1020− mapM_ dumpInstance (class_instances ci)

1075+ indent 2 (vsep (map (dumpInstance ist ctxt) (class_instances ci)))

1021− iPrintResult ""

1022−

1023−dumpMethod :: (Name, (FnOpts, PTerm)) -> Idris ()

1076+ where dumpMethod :: IState -> (Name, (FnOpts, PTerm)) -> Doc OutputAnnotation

1024−dumpMethod (n, (_, t)) = iputStrLn $ show n ++ " : " ++ show t

1077+ dumpMethod ist (n, (_, t)) = prettyName False [] n <+> colon <+> pp ist t

1025−

1026−dumpDefaultInstance :: PDecl -> Idris ()

1078+ dumpDefaultInstance :: IState -> PDecl -> Doc OutputAnnotation

1027−dumpDefaultInstance (PInstance _ _ _ _ _ t _ _) = iputStrLn $ show t

1079+ dumpDefaultInstance ist (PInstance _ _ _ _ _ t _ _) = pp ist t

1028−

1029−dumpInstance :: Name -> Idris ()

1080+ dumpInstance :: IState -> Context -> Name -> Doc OutputAnnotation

1030−dumpInstance n = do i <- getIState

1081+ dumpInstance ist ctxt n = pp ist $ delabTy ist n

1031− ctxt <- getContext

1082+ params = class_params ci

1032− case lookupTy n ctxt of

1083+ params' = zip params (repeat False)

1033− ts -> mapM_ (\t -> iputStrLn $ showTm i (delab i t)) ts

1084+ pp ist = pprintPTerm (opt_showimp (idris_options ist)) params' []

1034

1085

1035showTotal :: Totality -> IState -> String

1086showTotal :: Totality -> IState -> String

1036showTotal t@(Partial (Other ns)) i

1087showTotal t@(Partial (Other ns)) i

@@ -1076,6 +1127,7 @@ parseArgs ("--typeintype":ns) = TypeInType : (parseArgs ns)

1076parseArgs ("--total":ns) = DefaultTotal : (parseArgs ns)

1127parseArgs ("--total":ns) = DefaultTotal : (parseArgs ns)

1077parseArgs ("--partial":ns) = DefaultPartial : (parseArgs ns)

1128parseArgs ("--partial":ns) = DefaultPartial : (parseArgs ns)

1078parseArgs ("--warnpartial":ns) = WarnPartial : (parseArgs ns)

1129parseArgs ("--warnpartial":ns) = WarnPartial : (parseArgs ns)

1130+parseArgs ("--warnreach":ns) = WarnReach : (parseArgs ns)

1079parseArgs ("--nocoverage":ns) = NoCoverage : (parseArgs ns)

1131parseArgs ("--nocoverage":ns) = NoCoverage : (parseArgs ns)

1080parseArgs ("--errorcontext":ns) = ErrContext : (parseArgs ns)

1132parseArgs ("--errorcontext":ns) = ErrContext : (parseArgs ns)

1081parseArgs ("--help":ns) = Usage : (parseArgs ns)

1133parseArgs ("--help":ns) = Usage : (parseArgs ns)

@@ -1319,9 +1371,13 @@ idrisMain opts =

1319

1371

1320 ok <- noErrors

1372 ok <- noErrors

1321 when ok $ case output of

1373 when ok $ case output of

1322− [] -> return ()

1374+ -- just do the checks

1375+ [] -> performUsageAnalysis >> return ()

1376+

1377+ -- the compiler will run usage analysis itself

1323 (o:_) -> idrisCatch (process stdout "" (Compile cgn o))

1378 (o:_) -> idrisCatch (process stdout "" (Compile cgn o))

1324 (\e -> do ist <- getIState ; iputStrLn $ pshow ist e)

1379 (\e -> do ist <- getIState ; iputStrLn $ pshow ist e)

1380+

1325 case script of

1381 case script of

1326 Nothing -> return ()

1382 Nothing -> return ()

1327 Just expr -> execScript expr

1383 Just expr -> execScript expr

@@ -1366,11 +1422,6 @@ execScript expr = do i <- getIState

1366 res <- execute tm

1422 res <- execute tm

1367 runIO $ exitWith ExitSuccess

1423 runIO $ exitWith ExitSuccess

1368

1424

1369−-- | Check if the coloring matches the options and corrects if necessary

1370−fixColour :: Bool -> ANSI.Doc -> ANSI.Doc

1371−fixColour False doc = ANSI.plain doc

1372−fixColour True doc = doc

1373−

1374-- | Get the platform-specific, user-specific Idris dir

1425-- | Get the platform-specific, user-specific Idris dir

1375getIdrisUserDataDir :: Idris FilePath

1426getIdrisUserDataDir :: Idris FilePath

1376getIdrisUserDataDir = runIO $ getAppUserDataDirectory "idris"

1427getIdrisUserDataDir = runIO $ getAppUserDataDirectory "idris"

src/Idris/UnusedArgs.hsdeleted−65

@@ -1,65 +0,0 @@

1−module Idris.UnusedArgs where

2−

3−import Idris.AbsSyntax

4−

5−import Idris.Core.CaseTree

6−import Idris.Core.TT

7−

8−import Control.Monad.State

9−import Data.Maybe

10−import Data.List

11−

12−findUnusedArgs :: [Name] -> Idris ()

13−findUnusedArgs ns = mapM_ traceUnused ns

14−

15−traceUnused :: Name -> Idris ()

16−traceUnused n

17− = do i <- getIState

18− case lookupCtxt n (idris_callgraph i) of

19− [CGInfo args calls scg usedns _] ->

20− do let argpos = zip args [0..]

21− let fargs = concatMap (getFargpos calls) argpos

22− logLvl 3 $ show n ++ " used TRACE: " ++ show fargs

23− recused <- mapM (\ (argn, i, (g, j)) ->

24− do u <- used [(n, i)] g j

25− return (argn, u)) fargs

26− logLvl 4 $ show n ++ " recused TRACE: " ++ show recused

27− let fused = nub $ usedns ++ map fst (filter snd recused)

28− logLvl 1 $ show n ++ " used args: " ++ show fused

29− let unusedpos = mapMaybe (getUnused fused) (zip [0..] args)

30− logLvl 1 $ show n ++ " unused args: " ++ show (args, unusedpos)

31− addToCG n (CGInfo args calls scg usedns unusedpos) -- updates

32− _ -> return ()

33− where

34− getUnused fused (i,n) | n `elem` fused = Nothing

35− | otherwise = Just i

36−

37−used :: [(Name, Int)] -> Name -> Int -> Idris Bool

38−used path g j

39− | (g, j) `elem` path = return False -- cycle, never used on the way

40− | otherwise

41− = do logLvl 5 $ (show ((g, j) : path))

42− i <- getIState

43− case lookupCtxt g (idris_callgraph i) of

44− [CGInfo args calls scg usedns unused] ->

45− if (j >= length args)

46− then -- overapplied, assume used

47− return True

48− else do let directuse = args!!j `elem` usedns

49− let garg = getFargpos calls (args!!j, j)

50− logLvl 5 $ show (g, j, garg)

51− recused <- mapM (\ (argn, j, (g', j')) ->

52− used ((g,j):path) g' j') garg

53− -- used on any route from here, or not used recursively

54− return (directuse || or recused)

55− _ -> return True -- no definition, assume used

56−

57−getFargpos :: [(Name, [[Name]])] -> (Name, Int) -> [(Name, Int, (Name, Int))]

58−getFargpos calls (n, i) = concatMap (getCallArgpos n i) calls

59− where getCallArgpos :: Name -> Int -> (Name, [[Name]]) ->

60− [(Name, Int, (Name, Int))]

61− getCallArgpos n i (g, args)

62− = let argpos = zip [0..] args in

63− mapMaybe (\ (j, xs) -> if n `elem` xs then Just (n, i, (g, j))

64− else Nothing) argpos

65−

src/Pkg/Package.hs+1−1

@@ -20,7 +20,7 @@ import Data.List.Split(splitOn)

20import Idris.Core.TT

21import Idris.REPL

22import Idris.Parser (loadModule)

23−import Idris.Delaborate (pshow)

23+import Idris.Output (pshow)

24import Idris.AbsSyntax

25import Idris.IdrisDoc

26import Idris.Output

test/basic001/reg005.idr+15−16

@@ -1,17 +1,22 @@

1module Main

2

3+%flag C "-g3 -ggdb -O0"

4+

3rep : (n : Nat) -> Char -> Vect n Char

5rep : (n : Nat) -> Char -> Vect n Char

4rep Z x = []

6rep Z x = []

5rep (S k) x = x :: rep k x

7rep (S k) x = x :: rep k x

6

8

7data RLE : Vect n Char -> Type where

9data RLE : Vect n Char -> Type where

8 REnd : RLE []

10 REnd : RLE []

11+ RChar : .{k : Nat}

9− RChar : {xs : Vect k Char} ->

12+ -> {xs : Vect k Char}

13+ -> (n : Nat)

10− (n : Nat) -> (x : Char) -> RLE xs ->

14+ -> (x : Char)

15+ -> RLE xs

11− RLE (rep (S n) x ++ xs)

16+ -> RLE (rep (S n) x ++ xs)

12

17

13eq : (x : Char) -> (y : Char) -> Maybe (x = y)

18eq : (x : Char) -> (y : Char) -> Maybe (x = y)

14−eq x y = if x == y then Just ?eqCharOK else Nothing

19+eq x y = if x == y then Just (believe_me (refl {x})) else Nothing

15

20

16------------

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

17

22

@@ -32,20 +37,14 @@ compress xs with (rle xs)

32 = let ni : Integer = cast (S n) in

37 = let ni : Integer = cast (S n) in

33 show ni ++ strCons x (compress xs)

38 show ni ++ strCons x (compress xs)

34

39

40+{-

41+fmt : {xs : Vect n Char} -> RLE xs -> String

42+fmt REnd = ""

43+fmt (RChar n c xs) = show n ++ show c ++ fmt xs

44+-}

45+

35compressString : String -> String

46compressString : String -> String

36compressString xs = compress (fromList (unpack xs))

47compressString xs = compress (fromList (unpack xs))

37

48

38main : IO ()

49main : IO ()

39main = putStrLn (compressString "foooobaaaarbaaaz")

50main = putStrLn (compressString "foooobaaaarbaaaz")

40−

41−

42−

43−---------- Proofs ----------

44−

45−Main.eqCharOK = proof {

46− intros;

47− refine believe_me;

48− exact x = x;

49−}

50−

51−

test/basic002/test006.idr+2−2

@@ -1,8 +1,8 @@

1module Main

2

3data Parity : Nat -> Type where

4− even : Parity (n + n)

4+ even : {n : Nat} -> Parity (n + n)

5− odd : Parity (S (n + n))

5+ odd : {n : Nat} -> Parity (S (n + n))

6

7parity : (n:Nat) -> Parity n

8parity Z = even {n=Z}

test/basic007/test033.idr+1−1

@@ -1,4 +1,4 @@

1module Main

2

3main : IO ()

4−main = nullPtr null >>= (putStrLn . show)

4+main = nullPtr null >>= print

test/proof003/Parity.idr+2−2

@@ -1,8 +1,8 @@

1module Parity

2

3data Parity : Nat -> Type where

4− even : Parity (n + n)

4+ even : {n : Nat} -> Parity (n + n)

5− odd : Parity (S (n + n))

5+ odd : {n : Nat} -> Parity (S (n + n))

6

7parity : (n:Nat) -> Parity n

8parity Z = even {n=Z}

test/proof005/DefaultArgSubstitutionSuccess.idrnew file+44

@@ -0,0 +1,44 @@

1+module DefaultArgSubstitutionSuccess

2+

3+DecProofType : {a:Type} -> Dec a -> Type

4+DecProofType {a} (Yes _) = a

5+DecProofType {a} (No _) = a -> _|_

6+

7+decProof : {a:Type} -> (dec : Dec a) -> DecProofType dec

8+decProof (Yes x) = x

9+decProof (No x) = x

10+

11+DecType : {a:Type} -> Dec a -> Type

12+DecType {a} _ = a

13+

14+

15+argsAreSame : (n:Nat) -> (m:Nat)

16+ -> { default (decProof (decEq m n)) same : (m=n) } -> ()

17+argsAreSame _ _ = ()

18+

19+

20+argsAreDiff : (n:Nat) -> (m:Nat)

21+ -> { default (decProof (decEq m n)) same : (m=n) -> _|_ } -> ()

22+argsAreDiff _ _ = ()

23+

24+

25+data SameNats : Type where

26+ same : (n:Nat) -> (m:Nat) ->

27+ { default (decProof (decEq m n)) same : (m=n) } -> SameNats

28+

29+data DiffNats : Type where

30+ diff : (n:Nat) -> (m:Nat) ->

31+ { default (decProof (decEq m n)) same : (m=n) -> _|_ } -> DiffNats

32+

33+

34+zArgsAreSame : ()

35+zArgsAreSame = argsAreSame Z Z

36+

37+zszArgsAreDiff : ()

38+zszArgsAreDiff = argsAreDiff Z (S Z)

39+

40+sameNatZs : SameNats

41+sameNatZs = same Z Z

42+

43+diffNatsZSZ : DiffNats

44+diffNatsZSZ = diff Z (S Z)

test/proof005/expectednew file

No changes to the content.

test/proof005/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris --check $@ DefaultArgSubstitutionSuccess.idr

3+rm -f *.ibc

test/proof006/DefaultArgSubstitutionSyntax.idrnew file+49

@@ -0,0 +1,49 @@

1+module DefaultArgSubstitutionSyntax

2+

3+DecProofType : {a:Type} -> Dec a -> Type

4+DecProofType {a} (Yes _) = a

5+DecProofType {a} (No _) = a -> _|_

6+

7+decProof : {a:Type} -> (dec : Dec a) -> DecProofType dec

8+decProof (Yes x) = x

9+decProof (No x) = x

10+

11+DecType : {a:Type} -> Dec a -> Type

12+DecType {a} _ = a

13+

14+

15+syntax "{{" [prfname] ":" "accept" [dec] "}}" "->" [ret]

16+ = { default (decProof dec) prfname : DecType dec } -> ret

17+

18+syntax "{{" [prfname] ":" "reject" [dec] "}}" "->" [ret]

19+ = { default (decProof dec) prfname : DecType dec -> _|_ } -> ret

20+

21+

22+argsAreSame : (n:Nat) -> (m:Nat)

23+ -> {{ same : accept (decEq n m) }} -> ()

24+argsAreSame _ _ = ()

25+

26+

27+argsAreDiff : (n:Nat) -> (m:Nat)

28+ -> {{ diff : reject (decEq m n) }} -> ()

29+argsAreDiff _ _ = ()

30+

31+

32+data SameNats : Type where

33+ same : (n:Nat) -> (m:Nat) -> {{ same : accept (decEq m n) }} -> SameNats

34+

35+data DiffNats : Type where

36+ diff : (n:Nat) -> (m:Nat) -> {{ diff : reject (decEq m n) }} -> DiffNats

37+

38+

39+zArgsAreSame : ()

40+zArgsAreSame = argsAreSame Z Z

41+

42+zszArgsAreDiff : ()

43+zszArgsAreDiff = argsAreDiff Z (S Z)

44+

45+sameNatZs : SameNats

46+sameNatZs = same Z Z

47+

48+diffNatsZSZ : DiffNats

49+diffNatsZSZ = diff Z (S Z)

test/proof006/expectednew file

No changes to the content.

test/proof006/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris --check $@ DefaultArgSubstitutionSyntax.idr

3+rm -f *.ibc

test/proof007/DefaultArgUnknownName.idrnew file+4

@@ -0,0 +1,4 @@

1+module DefaultArgUnknownName

2+

3+funWithBadDefArg : { default sadgjhsag arg : () } -> ()

4+funWithBadDefArg : _ = ()

test/proof007/expectednew file+1

@@ -0,0 +1 @@

1+No such variable sadgjhsag

test/proof007/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris --check $@ DefaultArgUnknownName.idr

3+rm -f *.ibc

test/reg025/reg025.idr+1−1

@@ -9,7 +9,7 @@ Cell n = Maybe (Fin n)

9data Board : Nat -> Type where

10 MkBoard : {n : Nat} -> Vect n (Vect n (Cell n)) -> Board n

11

12−emptyBoard : Board n

12+emptyBoard : {n : Nat} -> Board n

13emptyBoard {n=n} = MkBoard (replicate n (replicate n Nothing))

14

15Empty : Cell n -> Type

test/reg039/expectednew file+2

@@ -0,0 +1,2 @@

1+Type checking ./reg039.idr

2+[3, 2, 1]

test/reg039/reg039.idrnew file+12

@@ -0,0 +1,12 @@

1+module LazyExec

2+

3+-- The regression that this tests for is broken laziness in the executor.

4+

5+covering

6+countdown : Int -> Lazy (List Int)

7+countdown n = if n > 0

8+ then (n :: countdown (n-1))

9+ else []

10+

11+go : IO ()

12+go = putStrLn $ show (Force (countdown 3))

test/reg039/runnew file+26

@@ -0,0 +1,26 @@

1+#!/usr/bin/env bash

2+

3+# From http://unix.stackexchange.com/questions/43340/how-to-introduce-timeout-for-shell-scripting

4+# Executes command with a timeout

5+# Params:

6+# $1 timeout in seconds

7+# $2 command

8+# Returns 1 if timed out 0 otherwise

9+timeout() {

10+

11+ time=$1

12+

13+ # start the command in a subshell to avoid problem with pipes

14+ # (spawn accepts one command)

15+ command="/bin/sh -c \"$2\""

16+

17+ expect -c "set echo \"-noecho\"; set timeout $time; spawn -noecho $command; expect timeout { exit 1 } eof { exit 0 }"

18+

19+ if [ $? = 1 ] ; then

20+ echo "Timeout after ${time} seconds"

21+ fi

22+

23+}

24+

25+timeout 60 "idris $@ --nocolour reg039.idr --exec go"

26+rm -f reg039 *.ibc