git.iko.soy/Idris-dev
on master help sign in
Merged with master
commitdd44389bb08d44ca8e979d236cd2bd81573fd9d9 authorPhilip Rasmussen <pjor@itu.dk> dateFri 11 Apr 2014, 20:22 (13 years ago) parentd34b7fc16f7da4
69 files changed+2001−1682
compare with master
unifiedsplit
.travis.yml+2 CHANGELOG+7−3 README+1−1 examples/binary.idr−62 examples/bmain.idr−8 examples/btree.idr−18 examples/classes.idr−10 examples/foo.idr−10 examples/hello.idr−5 examples/idiom.idr−38 examples/interp.idr−71 examples/letbind.idr−16 examples/prims.idr−14 examples/theorems.idr−57 examples/universe.idr−7 examples/usefultypes.idr−20 examples/vbroken.idr−5 examples/views.idr−37 examples/wheres.idr−14 idris.cabal+2−2 libs/Makefile−3 libs/base/Control/Arrow.idr+1−2 libs/base/Control/Catchable.idr+1−1 libs/effects/Effects.idr+2 libs/prelude/Decidable/Equality.idr+11−1 libs/prelude/IO.idr+3−6 main/Main.hs+1 src/IRTS/CodegenJavaScript.hs+6−1 src/IRTS/Compiler.hs+425−299 src/IRTS/Lang.hs+56−31 src/Idris/AbsSyntax.hs+91−37 src/Idris/AbsSyntaxTree.hs+64−54 src/Idris/Core/CaseTree.hs+144−105 src/Idris/Core/Evaluate.hs+14−9 src/Idris/Core/Execute.hs+96−135 src/Idris/Coverage.hs+3−2 src/Idris/DataOpts.hs+14−231 src/Idris/DeepSeq.hs+6−10 src/Idris/Delaborate.hs+3−3 src/Idris/ElabDecls.hs+137−102 src/Idris/ElabTerm.hs+4−13 src/Idris/Erasure.hs+505 src/Idris/IBC.hs+30−23 src/Idris/IdeSlave.hs+2 src/Idris/ParseExpr.hs+29−15 src/Idris/Parser.hs+9−3 src/Idris/PartialEval.hs+1−1 src/Idris/Prover.hs+6−5 src/Idris/Providers.hs+2−1 src/Idris/REPL.hs+154−103 src/Idris/UnusedArgs.hs−65 src/Pkg/Package.hs+1−1 test/basic001/reg005.idr+15−16 test/basic002/test006.idr+2−2 test/basic007/test033.idr+1−1 test/proof003/Parity.idr+2−2 test/proof005/DefaultArgSubstitutionSuccess.idr+44 test/proof005/expected test/proof005/run+3 test/proof006/DefaultArgSubstitutionSyntax.idr+49 test/proof006/expected test/proof006/run+3 test/proof007/DefaultArgUnknownName.idr+4 test/proof007/expected+1 test/proof007/run+3 test/reg025/reg025.idr+1−1 test/reg039/expected+2 test/reg039/reg039.idr+12 test/reg039/run+26
.travis.yml+2
@@ -6,6 +6,8 @@ before_install:
66 - 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
77 # trifecta dependencies
88 - 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
911install:
1012 - cabal install -f FFI -f LLVM --only-dependencies --enable-tests
1113before_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+
15New in 0.9.12:
26--------------
37
@@ -5,7 +9,7 @@ New in 0.9.12:
59 type inference.
610* New 'Lazy' type, replacing laziness annotations.
711* 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.
913* Lots of performance patches for generated JavaScript.
1014* New commands :eval (:e) and :type (:t) in the prover, which either normalise
1115 or show the type of expressions.
@@ -17,8 +21,8 @@ New in 0.9.12:
1721 ||| @ n the first number (examined by the function)
1822 ||| @ m the second number (not examined)
1923 plus (n, m : Nat) -> Nat
20−* Allow the auto-solve behavior in the prover to be disabled, for easier debugging
21− of proof automation. Use ":set autosolve" and ":unset autosolve".
24+* Allow the auto-solve behaviour in the prover to be disabled, for easier
25+ debugging of proof automation. Use ":set autosolve" and ":unset autosolve".
2226* Updated 'effects' library
2327* New :apropos command at REPL to search documentation, names, and types
2428* 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
22language with dependent types.
33
44To 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 @@
11Name: idris
2−Version: 0.9.11.2
2+Version: 0.9.12
33License: BSD3
44License-file: LICENSE
55Author: Edwin Brady
@@ -469,6 +469,7 @@ Library
469469 , Idris.Docstrings
470470 , Idris.ElabDecls
471471 , Idris.ElabTerm
472+ , Idris.Erasure
472473 , Idris.Error
473474 , Idris.ErrReverse
474475 , Idris.Help
@@ -492,7 +493,6 @@ Library
492493 , Idris.REPLParser
493494 , Idris.Transforms
494495 , Idris.Unlit
495− , Idris.UnusedArgs
496496
497497 , IRTS.BCImp
498498 , IRTS.Bytecode
libs/Makefile−3
@@ -2,7 +2,6 @@ build:
22 $(MAKE) -C prelude build
33 $(MAKE) -C base build
44 $(MAKE) -C effects build
5− $(MAKE) -C oldeffects build
65 $(MAKE) -C javascript build
76
87
@@ -10,14 +9,12 @@ install:
109 $(MAKE) -C prelude install
1110 $(MAKE) -C base install
1211 $(MAKE) -C effects install
13− $(MAKE) -C oldeffects install
1412 $(MAKE) -C javascript install
1513
1614clean:
1715 $(MAKE) -C prelude clean
1816 $(MAKE) -C base clean
1917 $(MAKE) -C effects clean
20− $(MAKE) -C oldeffects clean
2118 $(MAKE) -C javascript clean
2219
2320.PHONY: build install clean
libs/base/Control/Arrow.idr+1−2
@@ -1,4 +1,4 @@
1−module Category.Arrow
1+module Control.Arrow
22
33import Data.Morphisms
44import Control.Category
@@ -37,4 +37,3 @@ instance Monad m => Arrow (Kleislimorphism m) where
3737 (Kleisli f) &&& (Kleisli g) = Kleisli $ \a => do x <- f a
3838 y <- g a
3939 return (x, y)
40−
libs/base/Control/Catchable.idr+1−1
@@ -1,4 +1,4 @@
1−module Prelude.Catchable
1+module Control.Catchable
22
33import Control.IOExcept
44
libs/effects/Effects.idr+2
@@ -96,6 +96,8 @@ rebuildEnv [] SubNil env = env
9696rebuildEnv (x :: xs) (Keep rest) (y :: env) = x :: rebuildEnv xs rest env
9797rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env
9898rebuildEnv (x :: xs) SubNil [] = x :: xs
99+rebuildEnv [] (Keep x) (x :: xs) = []
100+
99101
100102-- -------------------------------------------------- [ The Effect EDSL itself ]
101103-- some proof automation
libs/prelude/Decidable/Equality.idr+11−1
@@ -174,13 +174,23 @@ total
174174vectInjective2 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> xs = ys
175175vectInjective2 {x=x} {y=x} {xs=xs} {ys=xs} refl = refl
176176
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+
177187instance DecEq a => DecEq (Vect n a) where
178188 decEq [] [] = Yes refl
179189 decEq (x :: xs) (y :: ys) with (decEq x y, decEq xs ys)
180190 decEq (x :: xs) (x :: xs) | (Yes refl, Yes refl) = Yes refl
181191 decEq (x :: xs) (y :: ys) | (_, No nEqTl) = No (\p => nEqTl (vectInjective2 p))
182192 decEq (x :: xs) (y :: ys) | (No nEqHd, _) = No (\p => nEqHd (vectInjective1 p))
183−
193+-}
184194
185195-- For the primitives, we have to cheat because we don't have access to their
186196-- internal implementations.
libs/prelude/IO.idr+3−6
@@ -132,16 +132,13 @@ io_return : a -> IO a
132132io_return x = MkIO (\w => prim_io_return x)
133133
134134liftPrimIO : (World -> PrimIO a) -> IO a
135−liftPrimIO f = MkIO (\w => prim_io_bind (f w)
136− (\x => prim_io_return x))
135+liftPrimIO = MkIO
137136
138137run__IO : IO () -> PrimIO ()
139−run__IO (MkIO f) = prim_io_bind (f TheWorld)
140− (\ b => prim_io_return b)
138+run__IO (MkIO f) = f TheWorld
141139
142140run__provider : IO a -> PrimIO a
143−run__provider (MkIO f) = prim_io_bind (f TheWorld)
144− (\ b => prim_io_return b)
141+run__provider (MkIO f) = f TheWorld
145142
146143-- io_bind v (\v' => io_return v')
147144
main/Main.hs+1
@@ -113,6 +113,7 @@ usagemsg = usagemsghdr ++ "\n" ++
113113 "\t --check Undocumented\n" ++
114114 "\t --total Require functions to be total by default\n" ++
115115 "\t --partial Undocumented\n" ++
116+ "\t --warnreach Warn about reachable but inaccessible arguments\n" ++
116117 "\t --warnpartial Warn about undeclared partial functions.\n" ++
117118 "\t --warn Undocumented\n" ++
118119 "\t --typecase Undocumented\n" ++
src/IRTS/CodegenJavaScript.hs+6−1
@@ -1154,7 +1154,7 @@ unfoldLookupTable input =
11541154
11551155removeInstanceChecks :: JS -> JS
11561156removeInstanceChecks (JSCond conds) =
1157− JSCond $ eliminateDeadBranches $ map (
1157+ removeNoopConds $ JSCond $ eliminateDeadBranches $ map (
11581158 removeHelper *** removeInstanceChecks
11591159 ) conds
11601160 where
@@ -1169,6 +1169,11 @@ removeInstanceChecks (JSCond conds) =
11691169 eliminateDeadBranches (x:xs) = x : eliminateDeadBranches xs
11701170 eliminateDeadBranches [] = []
11711171
1172+
1173+ removeNoopConds :: JS -> JS
1174+ removeNoopConds (JSCond [(JSNoop, js)]) = js
1175+ removeNoopConds js = js
1176+
11721177removeInstanceChecks js = transformJS removeInstanceChecks js
11731178
11741179
src/IRTS/Compiler.hs+425−299
@@ -18,15 +18,25 @@ import Util.LLVMStubs
1818import IRTS.Inliner
1919
2020import Idris.AbsSyntax
21−import Idris.UnusedArgs
21+import Idris.AbsSyntaxTree
22+import Idris.Erasure
2223import Idris.Error
2324
25+import Debug.Trace
26+
2427import Idris.Core.TT
2528import Idris.Core.Evaluate
2629import Idris.Core.CaseTree
2730
31+import Control.Applicative
2832import Control.Monad.State
33+import Data.Maybe
2934import 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
3040import System.Process
3141import System.IO
3242import System.Directory
@@ -37,18 +47,16 @@ import Paths_idris
3747
3848compile :: Codegen -> FilePath -> Term -> Idris ()
3949compile codegen f tm
40− = do checkMVs
41− let tmnames = namesUsed (STerm tm)
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)
50+ = do checkMVs -- check for undefined metavariables
51+ reachableNames <- performUsageAnalysis
4652 maindef <- irMain tm
53+ iLOG $ "MAIN: " ++ show maindef
4754 objs <- getObjectFiles codegen
4855 libs <- getLibs codegen
4956 flags <- getFlags codegen
5057 hdrs <- getHdrs codegen
5158 impdirs <- allImportDirs
59+ defsIn <- mkDecls tm reachableNames
5260 let defs = defsIn ++ [(sMN 0 "runMain", maindef)]
5361 -- iputStrLn $ showSep "\n" (map show defs)
5462 let (nexttag, tagged) = addTags 65536 (liftAll defs)
@@ -98,31 +106,48 @@ compile codegen f tm
98106 if ex then return f else return h
99107
100108irMain :: TT Name -> Idris LDecl
101−irMain tm = do i <- ir tm
102− return $ LFun [] (sMN 0 "runMain") [] (LForce i)
109+irMain tm = do
110+ i <- irTerm M.empty [] tm
111+ return $ LFun [] (sMN 0 "runMain") [] (LForce i)
103112
104113mkDecls :: Term -> [Name] -> Idris [(Name, LDecl)]
105114mkDecls t used
106115 = do i <- getIState
107− let ds = filter (\ (n, d) -> n `elem` used || isCon d) $ ctxtAlist (tt_ctxt i)
108− mapM traceUnused used
116+ let ds = filter (\(n, d) -> n `elem` used || isCon d) $ ctxtAlist (tt_ctxt i)
109117 decls <- mapM build ds
110118 return decls
111119
112120showCaseTrees :: [(Name, LDecl)] -> String
113−showCaseTrees ds = showSep "\n\n" (map showCT ds)
121+showCaseTrees = showSep "\n\n" . map showCT . sortBy (comparing defnRank)
114122 where
115123 showCT (n, LFun _ f args lexp)
116− = show n ++ " " ++ showSep " " (map show args) ++ " =\n\t "
124+ = show n ++ " " ++ showSep " " (map show args) ++ " =\n\t"
117125 ++ show lexp
118126 showCT (n, LConstructor c t a) = "data " ++ show n ++ " " ++ show a
119127
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+
120148isCon (TyDecl _ _) = True
121149isCon _ = False
122150
123−class ToIR a where
124− ir :: a -> Idris LExp
125−
126151build :: (Name, Def) -> Idris (Name, LDecl)
127152build (n, d)
128153 = do i <- getIState
@@ -135,295 +160,396 @@ build (n, d)
135160 logLvl 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def
136161 return (n, def)
137162
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−
146163declArgs args inl n (LLam xs x) = declArgs (args ++ xs) inl n x
147164declArgs args inl n x = LFun (if inl then [Inline] else []) n args x
148165
149−mkLDecl n (Function tm _) = do e <- ir tm
150− return (declArgs [] True n e)
166+mkLDecl n (Function tm _)
167+ = declArgs [] True n <$> irTerm M.empty [] tm
168+
151169mkLDecl 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)
155−mkLDecl n (TyDecl (DCon t a) _) = return $ LConstructor n t a
170+ = declArgs [] (case_inlinable ci) n <$> irTree args sc
171+ where
172+ (args, sc) = cases_runtime cd
173+
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+
156180mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
157181mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run
158182
159−instance ToIR (TT Name) where
160− ir tm = ir' [] tm where
161− ir' env tm@(App f a)
162− | (P _ (UN m) _, args) <- unApply tm,
163− m == txt "mkForeignPrim"
164− = doForeign env args
165− | (P _ (UN u) _, [_, arg]) <- unApply tm,
166− u == txt "unsafePerformPrimIO"
167− = ir' env arg
168− -- TMP HACK - until we get inlining.
169− | (P _ (UN r) _, [_, _, _, _, _, arg]) <- unApply tm,
170− r == txt "replace"
171− = ir' env arg
172− -- Laziness, the old way
173− | (P _ (UN l) _, [_, arg]) <- unApply tm,
174− l == txt "lazy"
175− = do arg' <- ir' env arg
176− error "lazy has crept in somehow"
177−-- return $ LLazyExp arg'
178− | (P _ (UN l) _, [_, arg]) <- unApply tm,
179− l == txt "force"
180− = do arg' <- ir' env arg
181− return $ LForce arg'
182− -- Laziness, the new way
183− | (P _ (UN l) _, [arg]) <- unApply tm,
184− l == txt "Delay"
185− = do arg' <- ir' env arg
186− return $ LLazyExp arg'
187− | (P _ (UN l) _, [_, _, arg]) <- unApply tm,
188− l == txt "Force"
189− = do arg' <- ir' env arg
190− return $ LForce arg'
191− | (P _ (UN a) _, [_, _, arg]) <- unApply tm,
192− a == txt "assert_smaller"
193− = ir' env arg
194− | (P _ (UN a) _, [_, arg]) <- unApply tm,
195− a == txt "assert_total"
196− = ir' env arg
197− | (P _ (UN p) _, [_, arg]) <- unApply tm,
198− p == txt "par"
199− = do arg' <- ir' env arg
200− return $ LOp LPar [LLazyExp arg']
201− | (P _ (UN pf) _, [arg]) <- unApply tm,
202− pf == txt "prim_fork"
203− = do arg' <- ir' env arg
204− return $ LOp LFork [LLazyExp arg']
205− | (P _ (UN m) _, [_,size,t]) <- unApply tm,
206− m == txt "malloc"
207− = do size' <- ir' env size
208− t' <- ir' env t
209− return t' -- TODO $ malloc_ size' t'
210− | (P _ (UN tm) _, [_,t]) <- unApply tm,
211− tm == txt "trace_malloc"
212− = do t' <- ir' env t
213− return t' -- TODO
214− -- This case is here until we get more general inlining. It's just
215− -- a really common case, and the laziness hurts...
216− | (P _ (NS (UN be) [b,p]) _, [_,x,(App (P _ (UN d) _) t),
217− (App (P _ (UN d') _) e)]) <- unApply tm,
218− be == txt "boolElim" && d == txt "Delay" && d' == txt "Delay"
219− = do x' <- ir' env x
220− t' <- ir' env t
221− e' <- ir' env e
222− return (LCase x' [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e',
223− LConCase 1 (sNS (sUN "True") ["Bool","Prelude"]) [] t'])
224− | (P (DCon t a) n _, args) <- unApply tm
225− = irCon env t a n args
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
237− Just oi -> collapsible oi
238− _ -> False
239− let unused
240− = case lookupCtxtExact n
241− (idris_callgraph i) of
242− Just (CGInfo _ _ _ _ unusedpos) ->
243− unusedpos
244− _ -> []
245− if collapse
246− then return LNothing
247− else return (LApp False (LV (Glob n))
248− (mkUnused unused 0 args'))
249− | (f, args) <- unApply tm
250− = do f' <- ir' env f
251− args' <- mapM (ir' env) args
252− return (LApp False f' args')
253− where mkUnused u i [] = []
254− mkUnused u i (x : xs) | i `elem` u = LNothing : mkUnused u (i + 1) xs
255− | otherwise = x : mkUnused u (i + 1) xs
256−-- ir' env (P _ (NS (UN "Z") ["Nat", "Prelude"]) _)
257−-- = return $ LConst (BI 0)
258− ir' env (P _ n _) = return $ LV (Glob n)
259− ir' env (V i) | i >= 0 && i < length env = return $ LV (Glob (env!!i))
260− | otherwise = ifail $ "IR fail " ++ show i ++ " " ++ show tm
261− ir' env (Bind n (Lam _) sc)
262− = do let n' = uniqueName n env
263− sc' <- ir' (n' : env) sc
264− return $ LLam [n'] sc'
265− ir' env (Bind n (Let _ v) sc)
266− = do sc' <- ir' (n : env) sc
267− v' <- ir' env v
268− return $ LLet n v' sc'
269− ir' env (Bind _ _ _) = return $ LNothing
270− ir' env (Proj t i) | i == -1
271− = do t' <- ir' env t
272− return $ LOp (LMinus (ATInt ITBig))
273− [t', LConst (BI 1)]
274− ir' env (Proj t i) = do t' <- ir' env t
275− return $ LProj t' i
276− ir' env (Constant c) = return $ LConst c
277− ir' env (TType _) = return $ LNothing
278− ir' env Erased = return $ LNothing
279− ir' env Impossible = return $ LNothing
280−-- ir' env _ = return $ LError "Impossible"
281−
282− irCon env t arity n args
283− | length args == arity = buildApp env (LV (Glob n)) args
284− | otherwise = let extra = satArgs (arity - length args) in
285− do sc' <- irCon env t arity n
286− (args ++ map (\n -> P Bound n undefined) extra)
287− return $ LLam extra sc'
288−
289− satArgs n = map (\i -> sMN i "sat") [1..n]
290−
291− buildApp env e [] = return e
292− buildApp env e xs = do xs' <- mapM (ir' env) xs
293− return $ LApp False e xs'
294−
295− doForeign :: [Name] -> [TT Name] -> Idris LExp
296− doForeign env (_ : fgn : args)
297− | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
298− = let maybeTys = getFTypes fgnArgTys
299− rty = mkIty' ret in
300− case maybeTys of
301− Nothing -> ifail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)
302− Just tys -> do
303− args' <- mapM (ir' 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')
308− | otherwise = ifail "Badly formed foreign function call"
309−
310−getFTypes :: TT Name -> Maybe [FType]
311−getFTypes tm = case unApply tm of
312− (nil, []) -> Just []
313− (cons, [ty, xs]) ->
314− fmap (mkIty' ty :) (getFTypes xs)
315− _ -> Nothing
316−
317−mkIty' (P _ (UN ty) _) = mkIty (str ty)
318−mkIty' (App (P _ (UN fi) _) (P _ (UN intTy) _))
319− | fi == txt "FIntT" = mkIntIty (str intTy)
320−mkIty' (App (App (P _ (UN ff) _) _) (App (P _ (UN fa) _) (App (P _ (UN io) _) _)))
321− | ff == txt "FFunction" && fa == txt "FAny" &&
322− io == txt "IO"
183+data VarInfo = VI
184+ { viMethod :: Maybe Name
185+ }
186+ deriving Show
187+
188+type Vars = M.Map Name VarInfo
189+
190+irTerm :: Vars -> [Name] -> Term -> Idris LExp
191+irTerm vs env tm@(App f a) = case unApply tm of
192+ (P _ (UN m) _, args)
193+ | m == txt "mkForeignPrim"
194+ -> doForeign vs env args
195+
196+ (P _ (UN u) _, [_, arg])
197+ | u == txt "unsafePerformPrimIO"
198+ -> irTerm vs env arg
199+
200+ -- TMP HACK - until we get inlining.
201+ (P _ (UN r) _, [_, _, _, _, _, arg])
202+ | r == txt "replace"
203+ -> irTerm vs env arg
204+
205+ -- Laziness, the old way
206+ (P _ (UN l) _, [_, arg])
207+ | l == txt "lazy"
208+ -> error "lazy has crept in somehow"
209+
210+ (P _ (UN l) _, [_, arg])
211+ | l == txt "force"
212+ -> LForce <$> irTerm vs env arg
213+
214+ -- Laziness, the new way
215+ (P _ (UN l) _, [_, _, arg])
216+ | l == txt "Delay"
217+ -> LLazyExp <$> irTerm vs env arg
218+
219+ (P _ (UN l) _, [_, _, arg])
220+ | l == txt "Force"
221+ -> LForce <$> irTerm vs env arg
222+
223+ (P _ (UN a) _, [_, _, arg])
224+ | a == txt "assert_smaller"
225+ -> irTerm vs env arg
226+
227+ (P _ (UN a) _, [_, arg])
228+ | a == txt "assert_total"
229+ -> irTerm vs env arg
230+
231+ (P _ (UN p) _, [_, arg])
232+ | p == txt "par"
233+ -> do arg' <- irTerm vs env arg
234+ return $ LOp LPar [LLazyExp arg']
235+
236+ (P _ (UN pf) _, [arg])
237+ | pf == txt "prim_fork"
238+ -> do arg' <- irTerm vs env arg
239+ return $ LOp LFork [LLazyExp arg']
240+
241+ (P _ (UN m) _, [_,size,t])
242+ | m == txt "malloc"
243+ -> irTerm vs env t
244+
245+ (P _ (UN tm) _, [_,t])
246+ | tm == txt "trace_malloc"
247+ -> irTerm vs env t -- TODO
248+
249+ -- This case is here until we get more general inlining. It's just
250+ -- a really common case, and the laziness hurts...
251+ (P _ (NS (UN be) [b,p]) _, [_,x,(App (P _ (UN d) _) t),
252+ (App (P _ (UN d') _) e)])
253+ | be == txt "boolElim"
254+ , d == txt "Delay"
255+ , d' == txt "Delay"
256+ -> do
257+ x' <- irTerm vs env x
258+ t' <- irTerm vs env t
259+ e' <- irTerm vs env e
260+ return (LCase x' [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e'
261+ ,LConCase 1 (sNS (sUN "True" ) ["Bool","Prelude"]) [] t'
262+ ])
263+
264+ (P (DCon t arity) n _, args) -> do
265+ ist <- getIState
266+ let detag = maybe False detaggable . lookupCtxtExact n $ idris_optimisation ist
267+ used = maybe [] (map fst . usedpos) . lookupCtxtExact n $ idris_callgraph ist
268+ args' = [a | (i,a) <- zip [0..] args, i `elem` used]
269+
270+ when (length args > arity) $
271+ ifail ("oversaturated data ctor: " ++ show tm)
272+
273+ if length args' == 1 && detag -- detaggable
274+ then irTerm vs env (head args') -- newtype
275+ else irCon vs env (length used) n args'
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)
294+ -> LApp False
295+ <$> irTerm vs env f
296+ <*> mapM (irTerm vs env) args
297+
298+ where
299+ applyName :: Name -> IState -> [Term] -> Idris LExp
300+ applyName n ist args =
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'
318+ | otherwise = n
319+
320+ used = maybe [] (map fst . usedpos) $ lookupCtxtExact uName (idris_callgraph ist)
321+ fst4 (x,_,_,_) = x
322+
323+irTerm vs env (P _ n _) = return $ LV (Glob n)
324+irTerm vs env (V i)
325+ | i >= 0 && i < length env = return $ LV (Glob (env!!i))
326+ | otherwise = ifail $ "bad de bruijn index: " ++ show i
327+
328+irTerm vs env (Bind n (Lam _) sc) = LLam [n'] <$> irTerm vs (n':env) sc
329+ where
330+ n' = uniqueName n env
331+
332+irTerm vs env (Bind n (Let _ v) sc)
333+ = LLet n <$> irTerm vs env v <*> irTerm vs (n : env) sc
334+
335+irTerm vs env (Bind _ _ _) = return $ LNothing
336+
337+irTerm vs env (Proj t (-1)) = do
338+ t' <- irTerm vs env t
339+ return $ LOp (LMinus (ATInt ITBig))
340+ [t', LConst (BI 1)]
341+
342+irTerm vs env (Proj t i) = LProj <$> irTerm vs env t <*> pure i
343+irTerm vs env (Constant c) = return $ LConst c
344+irTerm vs env (TType _) = return $ LNothing
345+irTerm vs env Erased = return $ LNothing
346+irTerm vs env Impossible = return $ LNothing
347+
348+irCon :: Vars -> [Name] -> Int -> Name -> [Term] -> Idris LExp
349+irCon vs env arity n args
350+ | length args > arity
351+ = error $ "oversaturated data constructor: " ++ show (n, args)
352+
353+ -- saturated
354+ | length args == arity
355+ = buildApp (LV (Glob n)) args
356+
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
363+ buildApp e [] = return e
364+ buildApp e xs = LApp False e <$> mapM (irTerm vs env) xs
365+
366+doForeign :: Vars -> [Name] -> [TT Name] -> Idris LExp
367+doForeign vs env (_ : fgn : args)
368+ | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
369+ = case getFTypes fgnArgTys of
370+ Nothing -> ifail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)
371+ Just tys -> do
372+ args' <- mapM (irTerm vs env) (init args)
373+ return $ LForeign LANG_C (mkIty' ret) fgnName (zip tys args')
374+
375+ | otherwise = ifail "Badly formed foreign function call"
376+ where
377+ getFTypes :: TT Name -> Maybe [FType]
378+ getFTypes tm = case unApply tm of
379+ -- nil : {a : Type} -> List a
380+ (nil, [_]) -> Just []
381+ -- cons : {a : Type} -> a -> List a -> List a
382+ (cons, [_, ty, xs]) -> (mkIty' ty :) <$> getFTypes xs
383+ _ -> Nothing
384+
385+ mkIty' (P _ (UN ty) _) = mkIty (str ty)
386+ mkIty' (App (P _ (UN fi) _) (P _ (UN intTy) _))
387+ | fi == txt "FIntT"
388+ = mkIntIty (str intTy)
389+
390+ mkIty' (App (App (P _ (UN ff) _) _) (App (P _ (UN fa) _) (App (P _ (UN io) _) _)))
391+ | ff == txt "FFunction"
392+ , fa == txt "FAny"
393+ , io == txt "IO"
323394 = 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
429395
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
213213usedIn env _ = []
214214
215215instance Show LExp where
216− show e = show' [] e where
217− show' env (LV (Loc i)) = env!!i
218− show' env (LV (Glob n)) = show n
219− show' env (LLazyApp e args) = show e ++ "|(" ++
220− showSep ", " (map (show' env) args) ++")"
221− show' env (LApp _ e args) = show' env e ++ "(" ++
222− showSep ", " (map (show' env) args) ++")"
223− show' env (LLazyExp e) = "%lazy(" ++ show' env e ++ ")"
224− show' env (LForce e) = "%force(" ++ show' env e ++ ")"
225− show' env (LLet n v e) = "let " ++ show n ++ " = " ++ show' env v ++ " in " ++
226− show' (env ++ [show n]) e
227− show' env (LLam args e) = "\\ " ++ showSep "," (map show args) ++ " => " ++
228− show' (env ++ (map show args)) e
229− show' env (LProj t i) = show t ++ "!" ++ show i
230− show' env (LCon i n args) = show n ++ ")" ++ showSep ", " (map (show' env) args) ++ ")"
231− show' env (LCase e alts) = "case " ++ show' env e ++ " of {\n\t" ++
232− showSep "\n\t| " (map (showAlt env) alts)
233− show' env (LConst c) = show c
234− show' env (LForeign lang ty n args)
235− = "foreign " ++ n ++ "(" ++ showSep ", " (map (show' env) (map snd args)) ++ ")"
236− show' env (LOp f args) = show f ++ "(" ++ showSep ", " (map (show' env) args) ++ ")"
237− show' env (LError str) = "error " ++ show str
238− show' env LNothing = "____"
239−
240− showAlt env (LConCase _ n args e)
216+ show e = show' [] "" e where
217+ show' env ind (LV (Loc i)) = env!!i
218+ show' env ind (LV (Glob n)) = show n
219+
220+ show' env ind (LLazyApp e args)
221+ = show e ++ "|(" ++ showSep ", " (map (show' env ind) args) ++")"
222+
223+ show' env ind (LApp _ e args)
224+ = show' env ind e ++ "(" ++ showSep ", " (map (show' env ind) args) ++")"
225+
226+ show' env ind (LLazyExp e) = "lazy{ " ++ show' env ind e ++ " }"
227+ show' env ind (LForce e) = "force{ " ++ show' env ind e ++ " }"
228+ show' env ind (LLet n v e)
229+ = "let " ++ show n ++ " = " ++ show' env ind v
230+ ++ " in " ++ show' (env ++ [show n]) ind e
231+
232+ show' env ind (LLam args e)
233+ = "\\ " ++ showSep "," (map show args)
234+ ++ " => " ++ show' (env ++ (map show args)) ind e
235+
236+ show' env ind (LProj t i) = show t ++ "!" ++ show i
237+
238+ show' env ind (LCon i n args)
239+ = show n ++ "(" ++ showSep ", " (map (show' env ind) args) ++ ")"
240+
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)
248+ = "\t" ++ ind ++ "| " ++ showAlt env (ind ++ ". ") alt
249+ ++ "\n" ++ fmt as
250+
251+ show' env ind (LConst c) = show c
252+
253+ show' env ind (LForeign lang ty n args) = concat
254+ [ "foreign{ "
255+ , n ++ "("
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)
263+ = show f ++ "(" ++ showSep ", " (map (show' env ind) args) ++ ")"
264+
265+ show' env ind (LError str) = "error " ++ show str
266+ show' env ind LNothing = "____"
267+
268+ showAlt env ind (LConCase _ n args e)
241269 = show n ++ "(" ++ showSep ", " (map show args) ++ ") => "
242− ++ show' env e
243− showAlt env (LConstCase c e) = show c ++ " => " ++ show' env e
244− showAlt env (LDefaultCase e) = "_ => " ++ show' env e
245−
246−
247−
270+ ++ show' env ind e
248271
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
388388putIState :: IState -> Idris ()
389389putIState = put
390390
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+
391401-- | A version of liftIO that puts errors into the exception type of the Idris monad
392402runIO :: IO a -> Idris a
393403runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return
@@ -819,9 +829,9 @@ expandParams dec ps ns infs tm = en tm
819829 | otherwise = PLam n (en t) (en s)
820830 en (PPi p n t s)
821831 | n `elem` (map fst ps ++ ns)
822− = let n' = mkShadow n in
823− PPi p n' (en t) (en (shadow n n' s))
824− | otherwise = PPi p n (en t) (en s)
832+ = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?
833+ PPi (enTacImp p) n' (en t) (en (shadow n n' s))
834+ | otherwise = PPi (enTacImp p) n (en t) (en s)
825835 en (PLet n ty v s)
826836 | n `elem` (map fst ps ++ ns)
827837 = let n' = mkShadow n in
@@ -880,6 +890,9 @@ expandParams dec ps ns infs tm = en tm
880890
881891 nseq x y = nsroot x == nsroot y
882892
893+ enTacImp (TacImp aos st scr) = TacImp aos st (en scr)
894+ enTacImp other = other
895+
883896expandParamsD :: Bool -> -- True = RHS only
884897 IState ->
885898 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
@@ -1076,7 +1089,7 @@ addUsingConstraints syn fc t
10761089 | otherwise = doAdd cs ns t
10771090
10781091 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)
10801093
10811094 getConstraints (PPi (Constraint _ _) _ c sc)
10821095 = getcapp c ++ getConstraints sc
@@ -1088,7 +1101,7 @@ addUsingConstraints syn fc t
10881101 return (UConstraint c ns)
10891102 getcapp _ = []
10901103
1091− getName (PExp _ _ (PRef _ n)) = return n
1104+ getName (PExp _ _ _ (PRef _ n)) = return n
10921105 getName _ = []
10931106
10941107-- Add implicit Pi bindings for any names in the term which appear in an
@@ -1096,13 +1109,14 @@ addUsingConstraints syn fc t
10961109
10971110-- This has become a right mess already. Better redo it some time...
10981111
1099−implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
1100−implicit syn n ptm = implicit' syn [] n ptm
1112+implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm
1113+implicit info syn n ptm = implicit' info syn [] n ptm
11011114
1102−implicit' :: SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1103−implicit' syn ignore n ptm
1115+implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1116+implicit' info syn ignore n ptm
11041117 = do i <- getIState
11051118 let (tm', impdata) = implicitise syn ignore i ptm
1119+ defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
11061120-- let (tm'', spos) = findStatics i tm'
11071121 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
11081122 addIBC (IBCImp n)
@@ -1110,6 +1124,23 @@ implicit' syn ignore n ptm
11101124-- i <- get
11111125-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
11121126 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
11131144
11141145implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
11151146implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
@@ -1155,7 +1186,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
11551186 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
11561187 _ -> [])
11571188 (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,
11591190 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
11601191 imps True (n:env) sc
11611192 imps top env (PPi (Constraint l _) n ty sc)
@@ -1163,7 +1194,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
11631194 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
11641195 _ -> [])
11651196 (decls, ns) <- get -- ignore decls in HO types
1166− put (PConstraint 10 l Placeholder : decls,
1197+ put (PConstraint 10 l n Placeholder : decls,
11671198 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
11681199 imps True (n:env) sc
11691200 imps top env (PPi (TacImp l _ scr) n ty sc)
@@ -1329,7 +1360,7 @@ aiFn inpat True ist fc f ds []
13291360-- any constructor alts || any allImp ialts))
13301361 then aiFn inpat False ist fc f ds [] -- use it as a constructor
13311362 else Right $ PPatvar fc f
1332− where imp (PExp _ _ _) = False
1363+ where imp (PExp _ _ _ _) = False
13331364 imp _ = True
13341365-- allImp [] = False
13351366 allImp xs = all imp xs
@@ -1376,27 +1407,41 @@ aiFn inpat expat ist fc f ds as
13761407 [(n,t)] -> t
13771408 _ -> Public
13781409
1379−
13801410 insertImpl :: [PArg] -> [PArg] -> [PArg]
1381− insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =
1382− PExp p l tm : insertImpl ps given
1383− insertImpl (PConstraint p l ty : ps) (PConstraint _ _ tm : given) =
1384− PConstraint p l tm : insertImpl ps given
1385− insertImpl (PConstraint p l ty : ps) given =
1386− PConstraint p l (PResolveTC fc) : insertImpl ps given
1387− insertImpl (PImp p _ l n ty : ps) given =
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]
1417+ insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) =
1418+ PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given
1419+ insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) =
1420+ PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given
1421+ insImpAcc pnas (PConstraint p l n ty : ps) given =
1422+ let rtc = PResolveTC fc in
1423+ PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given
1424+ insImpAcc pnas (PImp p _ l n ty : ps) given =
13881425 case find n given [] of
1389− Just (tm, given') -> PImp p False l n tm : insertImpl ps given'
1390− Nothing -> PImp p True l n Placeholder : insertImpl ps given
1391− insertImpl (PTacImplicit p l n sc' ty : ps) given =
1392− let sc = addImpl ist sc' in
1426+ Just (tm, given') ->
1427+ PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given'
1428+ Nothing ->
1429+ PImp p True l n Placeholder :
1430+ insImpAcc (M.insert n Placeholder pnas) ps given
1431+ insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given =
1432+ let sc = addImpl ist (substMatches (M.toList pnas) sc') in
13931433 case find n given [] of
1394− Just (tm, given') -> PTacImplicit p l n sc tm : insertImpl ps given'
1395− Nothing -> if inpat
1396− then PTacImplicit p l n sc Placeholder : insertImpl ps given
1397− else PTacImplicit p l n sc sc : insertImpl ps given
1398− insertImpl expected [] = []
1399− insertImpl _ given = given
1434+ Just (tm, given') ->
1435+ PTacImplicit p l n sc tm :
1436+ insImpAcc (M.insert n tm pnas) ps given'
1437+ Nothing ->
1438+ if inpat
1439+ then PTacImplicit p l n sc Placeholder :
1440+ insImpAcc (M.insert n Placeholder pnas) ps given
1441+ else PTacImplicit p l n sc sc :
1442+ insImpAcc (M.insert n sc pnas) ps given
1443+ insImpAcc _ expected [] = []
1444+ insImpAcc _ _ given = given
14001445
14011446 find n [] acc = Nothing
14021447 find n (PImp _ _ _ n' t : gs) acc
@@ -1433,11 +1478,11 @@ stripLinear i tm = evalState (sl tm) [] where
14331478 return $ PApp fc fn args'
14341479 where slA (PImp p m l n t) = do t' <- sl t
14351480 return $ PImp p m l n t'
1436− slA (PExp p l t) = do t' <- sl t
1437− return $ PExp p l t'
1438− slA (PConstraint p l t)
1481+ slA (PExp p l n t) = do t' <- sl t
1482+ return $ PExp p l n t'
1483+ slA (PConstraint p l n t)
14391484 = do t' <- sl t
1440− return $ PConstraint p l t'
1485+ return $ PConstraint p l n t'
14411486 slA (PTacImplicit p l n sc t)
14421487 = do t' <- sl t
14431488 return $ PTacImplicit p l n sc t'
@@ -1695,6 +1740,12 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where
16951740 mkUniqA arg = do t' <- mkUniq (getTm arg)
16961741 return (arg { getTm = t' })
16971742
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+
16981749 -- FIXME: Probably ought to do this for completeness! It's fine as
16991750 -- long as there are no bindings inside tactics though.
17001751 mkUniqT tac = return tac
@@ -1704,7 +1755,8 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where
17041755 = do env <- get
17051756 (n', sc') <-
17061757 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)
17081760 return (n', shadow n n' sc)
17091761 else return (n, sc)
17101762 put (n' : env)
@@ -1715,7 +1767,8 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where
17151767 = do env <- get
17161768 (n', sc') <-
17171769 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)
17191772 return (n', shadow n n' sc)
17201773 else return (n, sc)
17211774 put (n' : env)
@@ -1726,7 +1779,8 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where
17261779 = do env <- get
17271780 (n', sc') <-
17281781 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)
17301784 return (n', shadow n n' sc)
17311785 else return (n, sc)
17321786 put (n' : env)
src/Idris/AbsSyntaxTree.hs+64−54
@@ -36,6 +36,19 @@ import Debug.Trace
3636
3737import Text.PrettyPrint.Annotated.Leijen
3838
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+
3952data IOption = IOption { opt_logLevel :: Int,
4053 opt_typecase :: Bool,
4154 opt_typeintype :: Bool,
@@ -152,7 +165,8 @@ data IState = IState {
152165 idris_nameIdx :: (Int, Ctxt (Int, Name)),
153166 idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)), -- ^ Specific error handlers
154167 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
156170 }
157171
158172data SizeChange = Smaller | Same | Bigger | Unknown
@@ -168,7 +182,7 @@ data CGInfo = CGInfo { argsdef :: [Name],
168182 calls :: [(Name, [[Name]])],
169183 scg :: [SCGEntry],
170184 argsused :: [Name],
171− unusedpos :: [Int] }
185+ usedpos :: [(Int, [(Name, Int)])] } -- (used_arg#, [(using_fn, its_arg#)])
172186 deriving Show
173187{-!
174188deriving instance Binary CGInfo
@@ -212,6 +226,7 @@ data IBCWrite = IBCFix FixDecl
212226 | IBCLineApp FilePath Int PTerm
213227 | IBCErrorHandler Name
214228 | IBCFunctionErrorHandler Name Name Name
229+ | IBCPostulate Name
215230 deriving Show
216231
217232-- | The initial state for the compiler
@@ -223,7 +238,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
223238 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []
224239 [] [] Nothing [] Nothing [] [] Nothing [] Hidden False [] Nothing [] [] RawOutput
225240 True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty
226− AutomaticWidth
241+ AutomaticWidth S.empty
227242
228243-- | The monad for the main REPL - reading and processing files and updating
229244-- global state (hence the IO inner monad).
@@ -312,6 +327,7 @@ data Opt = Filename String
312327 | DefaultTotal
313328 | DefaultPartial
314329 | WarnPartial
330+ | WarnReach
315331 | NoCoverage
316332 | ErrContext
317333 | ShowImpl
@@ -388,7 +404,7 @@ data Plicity = Imp { pargopts :: [ArgOpt],
388404 pparam :: Bool }
389405 | Exp { pargopts :: [ArgOpt],
390406 pstatic :: Static,
391− pparam :: Bool }
407+ pparam :: Bool } -- this is a param (rather than index)
392408 | Constraint { pargopts :: [ArgOpt],
393409 pstatic :: Static }
394410 | TacImp { pargopts :: [ArgOpt],
@@ -396,15 +412,12 @@ data Plicity = Imp { pargopts :: [ArgOpt],
396412 pscript :: PTerm }
397413 deriving (Show, Eq)
398414
399−plazy :: Plicity -> Bool
400−plazy tm = Lazy `elem` pargopts tm
401−
402415{-!
403416deriving instance Binary Plicity
404417deriving instance NFData Plicity
405418!-}
406419
407−impl = Imp [Lazy] Dynamic False
420+impl = Imp [] Dynamic False
408421expl = Exp [] Dynamic False
409422expl_param = Exp [] Dynamic True
410423constraint = Constraint [] Dynamic
@@ -769,9 +782,11 @@ data PArg' t = PImp { priority :: Int,
769782 pname :: Name, getTm :: t }
770783 | PExp { priority :: Int,
771784 argopts :: [ArgOpt],
785+ pname :: Name,
772786 getTm :: t }
773787 | PConstraint { priority :: Int,
774788 argopts :: [ArgOpt],
789+ pname :: Name,
775790 getTm :: t }
776791 | PTacImplicit { priority :: Int,
777792 argopts :: [ArgOpt],
@@ -780,16 +795,13 @@ data PArg' t = PImp { priority :: Int,
780795 getTm :: t }
781796 deriving (Show, Eq, Functor)
782797
783−data ArgOpt = Lazy | HideDisplay
798+data ArgOpt = HideDisplay | InaccessibleArg
784799 deriving (Show, Eq)
785800
786−lazyarg :: PArg' t -> Bool
787−lazyarg tm = Lazy `elem` argopts tm
788−
789801instance Sized a => Sized (PArg' a) where
790802 size (PImp p _ l nm trm) = 1 + size nm + size trm
791− size (PExp p l trm) = 1 + size trm
792− size (PConstraint p l trm) = 1 + size trm
803+ size (PExp p l nm trm) = 1 + size nm + size trm
804+ size (PConstraint p l nm trm) = 1 + size nm +size nm + size trm
793805 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
794806
795807{-!
@@ -797,10 +809,10 @@ deriving instance Binary PArg'
797809deriving instance NFData PArg'
798810!-}
799811
800−pimp n t mach = PImp 1 mach [Lazy] n t
801−pexp t = PExp 1 [] t
802−pconst t = PConstraint 1 [] t
803−ptacimp n s t = PTacImplicit 2 [Lazy] n s t
812+pimp n t mach = PImp 1 mach [] n t
813+pexp t = PExp 1 [] (sMN 0 "arg") t
814+pconst t = PConstraint 1 [] (sMN 0 "carg") t
815+ptacimp n s t = PTacImplicit 2 [] n s t
804816
805817type PArg = PArg' PTerm
806818
@@ -824,22 +836,8 @@ data TIData = TIPartial -- ^ a function with a partially defined type
824836 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
825837 deriving Show
826838
827−-- An argument is conditionally forceable iff its forceability
828−-- depends on the collapsibility of the whole type.
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] }
839+data OptInfo = Optimise { inaccessible :: [(Int,Name)], -- includes names for error reporting
840+ detaggable :: Bool }
843841 deriving Show
844842{-!
845843deriving instance Binary OptInfo
@@ -1112,10 +1110,9 @@ pprintPTerm impl bnd docArgs = prettySe 10 bnd
11121110 prettySe 10 ((n, False):bnd) sc
11131111 prettySe p bnd (PPi (Exp l s _) n ty sc)
11141112 | 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 $
1117− enclose open rparen (group . align $ bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>
1118− st <> text "->" <$> prettySe 10 ((n, False):bnd) sc
1113+ bracket p 2 . group $
1114+ enclose lparen rparen (group . align $ bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>
1115+ st <> text "->" <$> prettySe 10 ((n, False):bnd) sc
11191116 | otherwise =
11201117 bracket p 2 . group $
11211118 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
11261123 _ -> empty
11271124 prettySe p bnd (PPi (Imp l s _) n ty sc)
11281125 | impl =
1129− let open = if Lazy `elem` l then text "|" <> lbrace else lbrace in
1130− bracket p 2 $
1131− open <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>
1132− st <> text "->" </> prettySe 10 ((n, True):bnd) sc
1126+ bracket p 2 $
1127+ lparen <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>
1128+ st <> text "->" </> prettySe 10 ((n, True):bnd) sc
11331129 | otherwise = prettySe 10 ((n, True):bnd) sc
11341130 where
11351131 st =
@@ -1257,8 +1253,8 @@ pprintPTerm impl bnd docArgs = prettySe 10 bnd
12571253 prettySe p bnd _ = text "test"
12581254
12591255 prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)
1260− prettyArgS bnd (PExp _ _ tm) = prettyArgSe bnd tm
1261− prettyArgS bnd (PConstraint _ _ tm) = prettyArgSc bnd tm
1256+ prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm
1257+ prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm
12621258 prettyArgS bnd (PTacImplicit _ _ n _ tm) = prettyArgSti bnd (n, tm)
12631259
12641260 prettyArgSe bnd arg = prettySe 0 bnd arg
@@ -1390,12 +1386,12 @@ getImps (_ : xs) = getImps xs
13901386
13911387getExps :: [PArg] -> [PTerm]
13921388getExps [] = []
1393−getExps (PExp _ _ tm : xs) = tm : getExps xs
1389+getExps (PExp _ _ _ tm : xs) = tm : getExps xs
13941390getExps (_ : xs) = getExps xs
13951391
13961392getConsts :: [PArg] -> [PTerm]
13971393getConsts [] = []
1398−getConsts (PConstraint _ _ tm : xs) = tm : getConsts xs
1394+getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
13991395getConsts (_ : xs) = getConsts xs
14001396
14011397getAll :: [PArg] -> [PTerm]
@@ -1434,7 +1430,9 @@ showName ist bnd impl colour n = case ist of
14341430showTm :: IState -- ^^ the Idris state, for information about identifiers and colours
14351431 -> PTerm -- ^^ the term to show
14361432 -> 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))
14381436
14391437-- | Show a term with implicits, no colours
14401438showTmImpls :: PTerm -> String
@@ -1483,7 +1481,7 @@ getPArity _ = 0
14831481
14841482allNamesIn :: PTerm -> [Name]
14851483allNamesIn tm = nub $ ni [] tm
1486− where
1484+ where -- TODO THINK added niTacImp, but is it right?
14871485 ni env (PRef _ n)
14881486 | not (n `elem` env) = [n]
14891487 ni env (PPatvar _ n) = [n]
@@ -1491,7 +1489,7 @@ allNamesIn tm = nub $ ni [] tm
14911489 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
14921490 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
14931491 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
14951493 ni env (PHidden tm) = ni env tm
14961494 ni env (PEq _ l r) = ni env l ++ ni env r
14971495 ni env (PRewrite _ l r _) = ni env l ++ ni env r
@@ -1505,16 +1503,19 @@ allNamesIn tm = nub $ ni [] tm
15051503 ni env (PNoImplicits tm) = ni env tm
15061504 ni env _ = []
15071505
1506+ niTacImp env (TacImp _ _ scr) = ni env scr
1507+ niTacImp _ _ = []
1508+
15081509-- Return all names defined in binders in the given term
15091510boundNamesIn :: PTerm -> [Name]
15101511boundNamesIn tm = nub $ ni tm
1511− where
1512+ where -- TODO THINK Added niTacImp, but is it right?
15121513 ni (PApp _ f as) = ni f ++ concatMap (ni) (map getTm as)
15131514 ni (PAppBind _ f as) = ni f ++ concatMap (ni) (map getTm as)
15141515 ni (PCase _ c os) = ni c ++ concatMap (ni) (map snd os)
15151516 ni (PLam n ty sc) = n : (ni ty ++ ni sc)
15161517 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))
15181519 ni (PEq _ l r) = ni l ++ ni r
15191520 ni (PRewrite _ l r _) = ni l ++ ni r
15201521 ni (PTyped l r) = ni l ++ ni r
@@ -1528,6 +1529,9 @@ boundNamesIn tm = nub $ ni tm
15281529 ni (PNoImplicits tm) = ni tm
15291530 ni _ = []
15301531
1532+ niTacImp (TacImp _ _ scr) = ni scr
1533+ niTacImp _ = []
1534+
15311535-- Return names which are free in the given term.
15321536namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
15331537namesIn uvars ist tm = nub $ ni [] tm
@@ -1541,7 +1545,7 @@ namesIn uvars ist tm = nub $ ni [] tm
15411545 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
15421546 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
15431547 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
15451549 ni env (PEq _ l r) = ni env l ++ ni env r
15461550 ni env (PRewrite _ l r _) = ni env l ++ ni env r
15471551 ni env (PTyped l r) = ni env l ++ ni env r
@@ -1555,11 +1559,14 @@ namesIn uvars ist tm = nub $ ni [] tm
15551559 ni env (PNoImplicits tm) = ni env tm
15561560 ni env _ = []
15571561
1562+ niTacImp env (TacImp _ _ scr) = ni env scr
1563+ niTacImp _ _ = []
1564+
15581565-- Return which of the given names are used in the given term.
15591566
15601567usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
15611568usedNamesIn vars ist tm = nub $ ni [] tm
1562− where
1569+ where -- TODO THINK added niTacImp, but is it right?
15631570 ni env (PRef _ n)
15641571 | n `elem` vars && not (n `elem` env)
15651572 = case lookupTy n (tt_ctxt ist) of
@@ -1569,7 +1576,7 @@ usedNamesIn vars ist tm = nub $ ni [] tm
15691576 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
15701577 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
15711578 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
15731580 ni env (PEq _ l r) = ni env l ++ ni env r
15741581 ni env (PRewrite _ l r _) = ni env l ++ ni env r
15751582 ni env (PTyped l r) = ni env l ++ ni env r
@@ -1583,3 +1590,6 @@ usedNamesIn vars ist tm = nub $ ni [] tm
15831590 ni env (PNoImplicits tm) = ni env tm
15841591 ni env _ = []
15851592
1593+ niTacImp env (TacImp _ _ scr) = ni env scr
1594+ niTacImp _ _ = []
1595+
src/Idris/Core/CaseTree.hs+144−105
@@ -2,7 +2,8 @@
22
33module Idris.Core.CaseTree(CaseDef(..), SC, SC'(..), CaseAlt, CaseAlt'(..),
44 Phase(..), CaseTree,
5− simpleCase, small, namesUsed, findCalls, findUsedArgs) where
5+ simpleCase, small, namesUsed, findCalls, findUsedArgs,
6+ substSC, substAlt, mkForce) where
67
78import Idris.Core.TT
89
@@ -14,8 +15,20 @@ import Debug.Trace
1415data CaseDef = CaseDef [Name] !SC [Term]
1516 deriving Show
1617
17−data SC' t = Case Name [CaseAlt' t] -- ^ invariant: lowest tags first
18− | ProjCase t [CaseAlt' t] -- ^ special case for projections
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+--
30+data SC' t = Case Name [CaseAlt' t] -- ^ invariant: lowest tags first
31+ | ProjCase t [CaseAlt' t] -- ^ special case for projections/thunk-forcing before inspection
1932 | STerm !t
2033 | UnmatchedCase String -- ^ error message
2134 | ImpossibleCase -- ^ already checked to be impossible
@@ -96,8 +109,7 @@ small n args t = let as = findAllUsedArgs t args in
96109namesUsed :: SC -> [Name]
97110namesUsed sc = nub $ nu' [] sc where
98111 nu' ps (Case n alts) = nub (concatMap (nua ps) alts) \\ [n]
99− nu' ps (ProjCase t alts) = nub $ (nut ps t ++
100− (concatMap (nua ps) alts))
112+ nu' ps (ProjCase t alts) = nub $ nut ps t ++ concatMap (nua ps) alts
101113 nu' ps (STerm t) = nub $ nut ps t
102114 nu' ps _ = []
103115
@@ -122,7 +134,7 @@ namesUsed sc = nub $ nu' [] sc where
122134findCalls :: SC -> [Name] -> [(Name, [[Name]])]
123135findCalls sc topargs = nub $ nu' topargs sc where
124136 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
126138 nu' ps (STerm t) = nub $ nut ps t
127139 nu' ps _ = []
128140
@@ -192,10 +204,10 @@ data Phase = CompileTime | RunTime
192204-- Work Right to Left
193205
194206simpleCase :: Bool -> Bool -> Bool ->
195− Phase -> FC -> [Type] ->
207+ Phase -> FC -> [Int] -> [Type] ->
196208 [([Name], Term, Term)] ->
197209 TC CaseDef
198−simpleCase tc cover reflect phase fc argtys cs
210+simpleCase tc cover reflect phase fc inacc argtys cs
199211 = sc' tc cover phase fc (filter (\(_, _, r) ->
200212 case r of
201213 Impossible -> False
@@ -213,7 +225,7 @@ simpleCase tc cover reflect phase fc argtys cs
213225 OK pats ->
214226 let numargs = length (fst (head pats))
215227 ns = take numargs args
216− (ns', ps') = order ns pats
228+ (ns', ps') = order [(n, i `elem` inacc) | (i,n) <- zip [0..] ns] pats
217229 (tree, st) = runState
218230 (match ns' ps' (defaultCase cover))
219231 ([], numargs, [])
@@ -382,21 +394,25 @@ partition xs = error $ "Partition " ++ show xs
382394-- reorder the patterns so that the one with most distinct names
383395-- comes next. Take rightmost first, otherwise (i.e. pick value rather
384396-- than dependency)
385−
386−order :: [Name] -> [Clause] -> ([Name], [Clause])
387−order [] cs = ([], cs)
388−order ns [] = (ns, [])
389−order ns cs = let patnames = transpose (map (zip ns) (map fst cs))
390− pats' = transpose (sortBy moreDistinct (reverse patnames)) in
391− (getNOrder pats', zipWith rebuild pats' cs)
397+--
398+-- The first argument means [(Name, IsInaccessible)].
399+
400+order :: [(Name, Bool)] -> [Clause] -> ([Name], [Clause])
401+order [] cs = ([], cs)
402+order ns' [] = (map fst ns', [])
403+order ns' cs = let patnames = transpose (map (zip ns') (map fst cs))
404+ -- note: sortBy . reverse is not nonsense because sortBy is stable
405+ pats' = transpose (sortBy moreDistinct (reverse patnames)) in
406+ (getNOrder pats', zipWith rebuild pats' cs)
392407 where
393− getNOrder [] = error $ "Failed order on " ++ show (ns, cs)
394− getNOrder (c : _) = map fst c
408+ getNOrder [] = error $ "Failed order on " ++ show (map fst ns', cs)
409+ getNOrder (c : _) = map (fst . fst) c
395410
396411 rebuild patnames clause = (map snd patnames, snd clause)
397412
398− moreDistinct xs ys = compare (numNames [] (map snd ys))
399− (numNames [] (map snd xs))
413+ -- this compares (+isInaccessible, -numberOfCases)
414+ moreDistinct xs ys = compare (snd . fst . head $ xs, numNames [] (map snd ys))
415+ (snd . fst . head $ ys, numNames [] (map snd xs))
400416
401417 numNames xs (PCon n _ _ : ps)
402418 | not (Left n `elem` xs) = numNames (Left n : xs) ps
@@ -576,91 +592,71 @@ depatt ns tm = dp [] tm
576592-- FIXME: Do this for SucCase too
577593prune :: Bool -- ^ Convert single branches to projections (only useful at runtime)
578594 -> SC -> SC
579−prune proj (Case n alts)
580− = let alts' = filter notErased (map pruneAlt alts) in
581− case alts' of
582− [] -> ImpossibleCase
583− as@(ConCase (UN delay) i [arg] sc : _)
584− | delay == txt "Delay"
585− -> if proj then mkForce n arg sc
586− else Case n as
587− as@[ConCase cn i args sc] -> if proj then mkProj n 0 args sc
588− else Case n as
589− as@[SucCase cn sc] -> if proj then mkProj n (-1) [cn] sc
590− else Case n as
591− as@[ConstCase _ sc] -> prune proj sc
592− -- Bit of a hack here! The default case will always be 0, make sure
593− -- it gets caught first.
594− [s@(SucCase _ _), DefaultCase dc]
595− -> Case n [ConstCase (BI 0) dc, s]
596− as -> Case n as
597− where 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)
599− pruneAlt (ConstCase c sc) = ConstCase c (prune proj sc)
600− pruneAlt (SucCase n sc) = SucCase n (prune proj sc)
601− pruneAlt (DefaultCase sc) = DefaultCase (prune proj sc)
602−
603− notErased (DefaultCase (STerm Erased)) = False
604− notErased (DefaultCase ImpossibleCase) = False
605− notErased _ = True
606−
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
643− projRep arg n i (Case x alts)
644− | x == arg = ProjCase (Proj (P Bound n Erased) i)
645− (map (projRepAlt arg n i) alts)
646− | otherwise = Case x (map (projRepAlt arg n i) alts)
647− projRep arg n i (ProjCase t alts)
648− = 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)
650− projRep arg n i c = c -- unmatched
651−
652− projRepAlt arg n i (ConCase cn t args rhs)
653− = ConCase cn t args (projRep arg n i rhs)
654− projRepAlt arg n i (FnCase cn args rhs)
655− = FnCase cn args (projRep arg n i rhs)
656− projRepAlt arg n i (ConstCase t rhs)
657− = ConstCase t (projRep arg n i rhs)
658− projRepAlt arg n i (SucCase sn rhs)
659− = SucCase sn (projRep arg n i rhs)
660− projRepAlt arg n i (DefaultCase rhs)
661− = DefaultCase (projRep arg n i rhs)
662−
663− projRepTm arg n i t = subst arg (Proj (P Bound n Erased) i) t
595+prune proj (Case n alts) = case alts' of
596+ [] -> ImpossibleCase
597+
598+ -- Projection transformations prevent us from seeing some uses of ctor fields
599+ -- because they delete information about which ctor is being used.
600+ -- Consider:
601+ -- f (X x) = ... x ...
602+ -- vs.
603+ -- f x = ... x!0 ...
604+ --
605+ -- Hence, we disable this step.
606+ -- TODO: re-enable this in toIR
607+ --
608+ -- as@[ConCase cn i args sc]
609+ -- | proj -> mkProj n 0 args (prune proj sc)
610+ -- mkProj n i xs sc = foldr (\x -> projRep x n i) sc xs
611+
612+ [SucCase cn sc]
613+ | proj
614+ -> projRep cn n (-1) $ prune proj sc
615+
616+ [ConstCase _ sc]
617+ -> prune proj sc
618+
619+ -- Bit of a hack here! The default case will always be 0, make sure
620+ -- it gets caught first.
621+ [s@(SucCase _ _), DefaultCase dc]
622+ -> Case n [ConstCase (BI 0) dc, s]
623+
624+ as -> Case n as
625+ where
626+ alts' = filter (not . erased) $ map pruneAlt alts
627+
628+ pruneAlt (ConCase cn i ns sc) = ConCase cn i ns (prune proj sc)
629+ pruneAlt (FnCase cn ns sc) = FnCase cn ns (prune proj sc)
630+ pruneAlt (ConstCase c sc) = ConstCase c (prune proj sc)
631+ pruneAlt (SucCase n sc) = SucCase n (prune proj sc)
632+ pruneAlt (DefaultCase sc) = DefaultCase (prune proj sc)
633+
634+ erased (DefaultCase (STerm Erased)) = True
635+ erased (DefaultCase ImpossibleCase) = True
636+ erased _ = False
637+
638+ projRep :: Name -> Name -> Int -> SC -> SC
639+ projRep arg n i (Case x alts) | x == arg
640+ = ProjCase (Proj (P Bound n Erased) i) $ map (projRepAlt arg n i) alts
641+ projRep arg n i (Case x alts)
642+ = Case x (map (projRepAlt arg n i) alts)
643+ projRep arg n i (ProjCase t alts)
644+ = ProjCase (projRepTm arg n i t) $ map (projRepAlt arg n i) alts
645+ projRep arg n i (STerm t) = STerm (projRepTm arg n i t)
646+ projRep arg n i c = c
647+
648+ projRepAlt arg n i (ConCase cn t args rhs)
649+ = ConCase cn t args (projRep arg n i rhs)
650+ projRepAlt arg n i (FnCase cn args rhs)
651+ = FnCase cn args (projRep arg n i rhs)
652+ projRepAlt arg n i (ConstCase t rhs)
653+ = ConstCase t (projRep arg n i rhs)
654+ projRepAlt arg n i (SucCase sn rhs)
655+ = SucCase sn (projRep arg n i rhs)
656+ projRepAlt arg n i (DefaultCase rhs)
657+ = DefaultCase (projRep arg n i rhs)
658+
659+ projRepTm arg n i t = subst arg (Proj (P Bound n Erased) i) t
664660
665661prune _ t = t
666662
@@ -669,6 +665,49 @@ stripLambdas (CaseDef ns (STerm (Bind x (Lam _) sc)) tm)
669665 = stripLambdas (CaseDef (ns ++ [x]) (STerm (instantiate (P Bound x Erased) sc)) tm)
670666stripLambdas x = x
671667
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
672698
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)
673709
710+ forceTm n arg t = subst arg (forceArg n) t
674711
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,
88 Context, initContext, ctxtAlist, uconstraints, next_tvar,
99 addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,
1010 addDatatype, addCasedef, simplifyCasedef, addOperator,
11− lookupNames, lookupTy, lookupP, lookupDef, lookupDefAcc, lookupVal,
11+ lookupNames, lookupTy, lookupP, lookupDef, lookupDefExact, lookupDefAcc, lookupVal,
1212 mapDefCtxt,
1313 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isDConName, isTConName, isConName, isFnName,
14− Value(..), Quote(..), initEval, uniqueNameCtxt) where
14+ Value(..), Quote(..), initEval, uniqueNameCtxt, definitions) where
1515
1616import Debug.Trace
17+import Control.Applicative hiding (Const)
1718import Control.Monad.State -- not Strict!
1819import qualified Data.Binary as B
1920import Data.Binary hiding (get, put)
@@ -784,6 +785,7 @@ addDatatype (Data n tag ty cons) uctxt
784785-- FIXME: Too many arguments! Refactor all these Bools.
785786addCasedef :: Name -> CaseInfo -> Bool -> Bool -> Bool -> Bool ->
786787 [Type] -> -- argument types
788+ [Int] -> -- inaccessible arguments
787789 [Either Term (Term, Term)] ->
788790 [([Name], Term, Term)] -> -- totality
789791 [([Name], Term, Term)] -> -- compile time
@@ -791,16 +793,16 @@ addCasedef :: Name -> CaseInfo -> Bool -> Bool -> Bool -> Bool ->
791793 [([Name], Term, Term)] -> -- run time
792794 Type -> Context -> Context
793795addCasedef n ci@(CaseInfo alwaysInline tcdict)
794− tcase covering reflect asserted argtys
796+ tcase covering reflect asserted argtys inacc
795797 ps_in ps_tot ps_inl ps_ct ps_rt ty uctxt
796798 = let ctxt = definitions uctxt
797799 access = case lookupDefAcc n False uctxt of
798800 [(_, acc)] -> acc
799801 _ -> Public
800− ctxt' = case (simpleCase tcase covering reflect CompileTime emptyFC argtys ps_tot,
801− simpleCase tcase covering reflect CompileTime emptyFC argtys ps_ct,
802− simpleCase tcase covering reflect CompileTime emptyFC argtys ps_inl,
803− simpleCase tcase covering reflect RunTime emptyFC argtys ps_rt) of
802+ ctxt' = case (simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_tot,
803+ simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_ct,
804+ simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_inl,
805+ simpleCase tcase covering reflect RunTime emptyFC inacc argtys ps_rt) of
804806 (OK (CaseDef args_tot sc_tot _),
805807 OK (CaseDef args_ct sc_ct _),
806808 OK (CaseDef args_inl sc_inl _),
@@ -827,7 +829,7 @@ simplifyCasedef n uctxt
827829 [(CaseOp ci ty atys ps_in ps cd, acc, tot, metainf)] ->
828830 let ps_in' = map simpl ps_in
829831 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
831833 OK (CaseDef args sc _) ->
832834 addDef n (CaseOp ci
833835 ty atys ps_in' ps (cd { cases_totcheck = (args, sc) }),
@@ -908,8 +910,11 @@ lookupP n ctxt
908910 Hidden -> []
909911 _ -> return (fst p)
910912
913+lookupDefExact :: Name -> Context -> Maybe Def
914+lookupDefExact n ctxt = tfst <$> lookupCtxtExact n (definitions ctxt)
915+
911916lookupDef :: Name -> Context -> [Def]
912−lookupDef n ctxt = map tfst $ lookupCtxt n (definitions ctxt)
917+lookupDef n ctxt = tfst <$> lookupCtxt n (definitions ctxt)
913918
914919lookupDefAcc :: Name -> Bool -> Context ->
915920 [(Def, Accessibility)]
src/Idris/Core/Execute.hs+96−135
@@ -47,11 +47,8 @@ readMay s = case reads s of
4747
4848data Lazy = Delayed ExecEnv Context Term | Forced ExecVal deriving Show
4949
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
54− }
50+newtype ExecState = ExecState { exec_dynamic_libs :: [DynamicLib] -- ^ Dynamic libs from idris monad
51+ }
5552
5653data ExecVal = EP NameType Name ExecVal
5754 | EV Int
@@ -61,20 +58,20 @@ data ExecVal = EP NameType Name ExecVal
6158 | EErased
6259 | EConstant Const
6360 | forall a. EPtr (Ptr a)
64− | EThunk Int
61+ | EThunk Context ExecEnv Term
6562 | EHandle Handle
6663
6764instance Show ExecVal where
68− show (EP _ n _) = show n
69− show (EV i) = "!!V" ++ show i ++ "!!"
70− show (EBind n b body) = "EBind " ++ show b ++ " <<fn>>"
71− show (EApp e1 e2) = show e1 ++ " (" ++ show e2 ++ ")"
72− show (EType _) = "Type"
73− show EErased = "[__]"
74− show (EConstant c) = show c
75− show (EPtr p) = "<<ptr " ++ show p ++ ">>"
76− show (EThunk i) = "<<thunk " ++ show i ++ ">>"
77− show (EHandle h) = "<<handle " ++ show h ++ ">>"
65+ show (EP _ n _) = show n
66+ show (EV i) = "!!V" ++ show i ++ "!!"
67+ show (EBind n b body) = "EBind " ++ show b ++ " <<fn>>"
68+ show (EApp e1 e2) = show e1 ++ " (" ++ show e2 ++ ")"
69+ show (EType _) = "Type"
70+ show EErased = "[__]"
71+ show (EConstant c) = show c
72+ show (EPtr p) = "<<ptr " ++ show p ++ ">>"
73+ show (EThunk _ env tm) = "<<thunk " ++ show env ++ "||||" ++ show tm ++ ">>"
74+ show (EHandle h) = "<<handle " ++ show h ++ ">>"
7875
7976toTT :: ExecVal -> Exec Term
8077toTT (EP nt n ty) = (P nt n) <$> (toTT ty)
@@ -82,22 +79,25 @@ toTT (EV i) = return $ V i
8279toTT (EBind n b body) = do body' <- body $ EP Bound n EErased
8380 b' <- fixBinder b
8481 Bind n b' <$> toTT body'
85− where fixBinder (Lam t) = Lam <$> toTT t
86− fixBinder (Pi t) = Pi <$> toTT t
87− fixBinder (Let t1 t2) = Let <$> toTT t1 <*> toTT t2
88− fixBinder (NLet t1 t2) = NLet <$> toTT t1 <*> toTT t2
89− fixBinder (Hole t) = Hole <$> toTT t
82+ where fixBinder (Lam t) = Lam <$> toTT t
83+ fixBinder (Pi t) = Pi <$> toTT t
84+ fixBinder (Let t1 t2) = Let <$> toTT t1 <*> toTT t2
85+ fixBinder (NLet t1 t2) = NLet <$> toTT t1 <*> toTT t2
86+ fixBinder (Hole t) = Hole <$> toTT t
9087 fixBinder (GHole i t) = GHole i <$> toTT t
91− fixBinder (Guess t1 t2) = Guess <$> toTT t1 <*> toTT t2
92− fixBinder (PVar t) = PVar <$> toTT t
93− fixBinder (PVTy t) = PVTy <$> toTT t
88+ fixBinder (Guess t1 t2) = Guess <$> toTT t1 <*> toTT t2
89+ fixBinder (PVar t) = PVar <$> toTT t
90+ fixBinder (PVTy t) = PVTy <$> toTT t
9491toTT (EApp e1 e2) = do e1' <- toTT e1
9592 e2' <- toTT e2
9693 return $ App e1' e2'
9794toTT (EType u) = return $ TType u
9895toTT EErased = return Erased
9996toTT (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')
101101toTT (EHandle _) = return Erased
102102
103103unApplyV :: ExecVal -> (ExecVal, [ExecVal])
@@ -111,7 +111,7 @@ mkEApp f (a:args) = mkEApp (EApp f a) args
111111
112112initState :: Idris ExecState
113113initState = do ist <- getIState
114− return $ ExecState M.empty 0 (idris_implicits ist) (idris_dynamic_libs ist)
114+ return $ ExecState (idris_dynamic_libs ist)
115115
116116type Exec = ErrorT String (StateT ExecState IO)
117117
@@ -130,45 +130,13 @@ execFail = throwError
130130execIO :: IO a -> Exec a
131131execIO = lift . lift
132132
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)))
166133
167134execute :: Term -> Idris Term
168135execute tm = do est <- initState
169136 ctxt <- getContext
170− res <- lift . lift $ flip runExec est $ do res <- doExec [] ctxt tm
171− toTT res
137+ res <- lift . lift . flip runExec est $
138+ do res <- doExec [] ctxt tm
139+ toTT res
172140 case res of
173141 Left err -> fail err
174142 Right tm' -> return tm'
@@ -208,7 +176,18 @@ doExec env ctxt (Bind n (NLet t v) body) = trace "NLet" $ undefined
208176doExec env ctxt tm@(Bind n b body) = return $
209177 EBind n (fmap (\_->EErased) b)
210178 (\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'
212191doExec env ctxt (Constant c) = return (EConstant c)
213192doExec env ctxt (Proj tm i) = let (x, xs) = unApply tm in
214193 doExec env ctxt ((x:xs) !! i)
@@ -216,55 +195,38 @@ doExec env ctxt Erased = return EErased
216195doExec env ctxt Impossible = fail "Tried to execute an impossible case"
217196doExec env ctxt (TType u) = return (EType u)
218197
219−execApp :: ExecEnv -> Context -> (Term, [Term]) -> 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
240−execApp' env ctxt (EP _ fp _) (ty:action:rest)
198+execApp :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
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
205+execApp env ctxt (EP _ fp _) (ty:action:rest)
241206 | fp == upio,
242207 (prim__IO, [_, v]) <- unApplyV action
243− = execApp' env ctxt v rest
208+ = execApp env ctxt v rest
244209
245−execApp' env ctxt (EP _ fp _) args@(_:_:v:k:rest)
210+execApp env ctxt (EP _ fp _) args@(_:_:v:k:rest)
246211 | fp == piobind,
247212 (prim__IO, [_, v']) <- unApplyV v =
248− do v'' <- tryForce v'
249− res <- execApp' env ctxt k [v''] >>= tryForce
250− execApp' env ctxt res rest
251−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
213+ do res <- execApp env ctxt k [v']
214+ execApp env ctxt res rest
215+execApp env ctxt con@(EP _ fp _) args@(tp:v:rest)
216+ | fp == pioret = execApp env ctxt (mkEApp con [tp, v]) rest
255217
256218-- 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)
258220 | fp == mkfprim,
259221 Just (FFun "putStr" _ _) <- foreignFromTT fn
260222 = do execIO (putStr arg)
261− execApp' env ctxt ioUnit rest
262−execApp' env ctxt (EP _ fp _) (_:fn:_:EHandle h:_:rest)
223+ execApp env ctxt ioUnit rest
224+execApp env ctxt (EP _ fp _) (_:fn:_:EHandle h:_:rest)
263225 | fp == mkfprim,
264226 Just (FFun "idris_readStr" _ _) <- foreignFromTT fn
265227 = do contents <- execIO $ hGetLine h
266− execApp' env ctxt (EConstant (Str (contents ++ "\n"))) rest
267−execApp' env ctxt (EP _ fp _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)
228+ execApp env ctxt (EConstant (Str (contents ++ "\n"))) rest
229+execApp env ctxt (EP _ fp _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)
268230 | fp == mkfprim,
269231 Just (FFun "fileOpen" _ _) <- foreignFromTT fn
270232 = do f <- execIO $
@@ -283,53 +245,53 @@ execApp' env ctxt (EP _ fp _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)
283245 in return $ Right (ioWrap (EPtr nullPtr), tail rest))
284246 case f of
285247 Left err -> execFail err
286− Right (res, rest) -> execApp' env ctxt res rest
248+ Right (res, rest) -> execApp env ctxt res rest
287249
288−execApp' env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)
250+execApp env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)
289251 | fp == mkfprim,
290252 Just (FFun "fileEOF" _ _) <- foreignFromTT fn
291253 = do eofp <- execIO $ hIsEOF h
292254 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)
294256
295−execApp' env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)
257+execApp env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)
296258 | fp == mkfprim,
297259 Just (FFun "fileClose" _ _) <- foreignFromTT fn
298260 = do execIO $ hClose h
299− execApp' env ctxt ioUnit (tail rest)
261+ execApp env ctxt ioUnit (tail rest)
300262
301−execApp' env ctxt (EP _ fp _) (_:fn:(EPtr p):rest)
263+execApp env ctxt (EP _ fp _) (_:fn:(EPtr p):rest)
302264 | fp == mkfprim,
303265 Just (FFun "isNull" _ _) <- foreignFromTT fn
304266 = let res = ioWrap . EConstant . I $
305267 if p == nullPtr then 1 else 0
306− in execApp' env ctxt res (tail rest)
268+ in execApp env ctxt res (tail rest)
307269
308270-- Handles will be checked as null pointers sometimes - but if we got a
309271-- 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)
311273 | fp == mkfprim,
312274 Just (FFun "isNull" _ _) <- foreignFromTT fn
313275 = let res = ioWrap . EConstant . I $ 0
314− in execApp' env ctxt res (tail rest)
276+ in execApp env ctxt res (tail rest)
315277
316278-- 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)
318280 | fp == mkfprim,
319281 Just (FFun "isNull" _ _) <- foreignFromTT fn
320282 = let res = ioWrap . EConstant . I $ 0
321− in execApp' env ctxt res (tail rest)
283+ in execApp env ctxt res (tail rest)
322284
323285-- Right now, there's no way to send command-line arguments to the executor,
324286-- so just return 0.
325−execApp' env ctxt (EP _ fp _) (_:fn:rest)
287+execApp env ctxt (EP _ fp _) (_:fn:rest)
326288 | fp == mkfprim,
327289 Just (FFun "idris_numArgs" _ _) <- foreignFromTT fn
328290 = let res = ioWrap . EConstant . I $ 0
329− in execApp' env ctxt res (tail rest)
291+ in execApp env ctxt res (tail rest)
330292-- Throw away the 'World' argument to the foreign function
331293
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
333295 = case foreignFromTT fn of
334296 Just (FFun f argTs retT) | length xs >= length argTs ->
335297 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
341303 Just r -> return (mkEApp r xs')
342304 Nothing -> return (mkEApp f args)
343305
344−execApp' env ctxt c@(EP (DCon _ arity) n _) args =
345− do args' <- mapM tryForce (take arity args)
306+execApp env ctxt c@(EP (DCon _ arity) n _) args =
307+ do let args' = take arity args
346308 let restArgs = drop arity args
347− execApp' env ctxt (mkEApp c args') restArgs
309+ execApp env ctxt (mkEApp c args') restArgs
348310
349−execApp' env ctxt c@(EP (TCon _ arity) n _) args =
350− do args' <- mapM tryForce (take arity args)
311+execApp env ctxt c@(EP (TCon _ arity) n _) args =
312+ do let args' = take arity args
351313 let restArgs = drop arity args
352− execApp' env ctxt (mkEApp c args') restArgs
314+ execApp env ctxt (mkEApp c args') restArgs
353315
354−execApp' env ctxt f@(EP _ n _) args =
316+execApp env ctxt f@(EP _ n _) args =
355317 do let val = lookupDef n ctxt
356318 case val of
357319 [Function _ tm] -> fail "should already have been eval'd"
358320 [TyDecl nt ty] -> return $ mkEApp f args
359321 [Operator tp arity op] ->
360322 if length args >= arity
361− then do args' <- mapM tryForce $ take arity args
362− case getOp n args' of
363− Just res -> do r <- res
364− execApp' env ctxt r (drop arity args)
365− Nothing -> return (mkEApp f args)
323+ then let args' = take arity args in
324+ case getOp n args' of
325+ Just res -> do r <- res
326+ execApp env ctxt r (drop arity args)
327+ Nothing -> return (mkEApp f args)
366328 else return (mkEApp f args)
367329 [CaseOp _ _ _ _ _ (CaseDefs _ ([], STerm tm) _ _)] -> -- nullary fun
368330 do rhs <- doExec env ctxt tm
369− execApp' env ctxt rhs args
331+ execApp env ctxt rhs args
370332 [CaseOp _ _ _ _ _ (CaseDefs _ (ns, sc) _ _)] ->
371333 do res <- execCase env ctxt ns sc args
372334 return $ fromMaybe (mkEApp f args) res
373335 thing -> return $ mkEApp f args
374−execApp' env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg
375− let (f', as) = unApplyV ret
376− 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)
380−execApp' env ctxt f args = return (mkEApp f args)
336+execApp env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg
337+ let (f', as) = unApplyV ret
338+ execApp env ctxt f' (as ++ args)
339+execApp env ctxt app@(EApp _ _) args2 | (f, args1) <- unApplyV app = execApp env ctxt f (args1 ++ args2)
340+execApp env ctxt f args = return (mkEApp f args)
381341
382342prs = sUN "prim__readString"
383343pbm = sUN "prim__believe_me"
@@ -386,6 +346,8 @@ mkfprim = sUN "mkForeignPrim"
386346pioret = sUN "prim_io_return"
387347piobind = sUN "prim_io_bind"
388348upio = sUN "unsafePerformPrimIO"
349+delay = sUN "Delay"
350+force = sUN "Force"
389351
390352-- | Look up primitive operations in the global table and transform them into ExecVal functions
391353getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)
@@ -426,7 +388,7 @@ execCase env ctxt ns sc args =
426388-- trace ("Case " ++ show sc ++ "\n in " ++ show amap ++"\n in env " ++ show env ++ "\n\n" ) $ return ()
427389 caseRes <- execCase' env ctxt amap sc
428390 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)
430392 Nothing -> return Nothing
431393 else return Nothing
432394
@@ -436,8 +398,7 @@ execCase' env ctxt amap (UnmatchedCase _) = return Nothing
436398execCase' env ctxt amap (STerm tm) =
437399 Just <$> doExec (map (\(n, v) -> (n, v)) amap ++ env) ctxt tm
438400execCase' 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
441402 Just (newCase, newBindings) ->
442403 let amap' = newBindings ++ (filter (\(x,_) -> not (elem x (map fst newBindings))) amap) in
443404 execCase' env ctxt amap' newCase
src/Idris/Coverage.hs+3−2
@@ -72,8 +72,9 @@ genClauses fc n xs given
7272 -- there may be more case splitting that the idris_implicits record
7373 -- suggests)
7474 let parg = case lookupCtxt n (idris_implicits i) of
75− (p : _) -> p ++ repeat (PExp 0 [] Placeholder)
76− _ -> repeat (pexp Placeholder)
75+ (p : _) ->
76+ p ++ repeat (PExp 0 [] (sMN 0 "gcarg") Placeholder)
77+ _ -> repeat (pexp Placeholder)
7778 let tryclauses = mkClauses parg all_args
7879 logLvl 2 $ show (length tryclauses) ++ " initially to check"
7980 logLvl 1 $ showSep "\n" (map (showTm i) tryclauses)
src/Idris/DataOpts.hs+14−231
@@ -9,224 +9,48 @@ import Idris.AbsSyntaxTree
99import Idris.Core.TT
1010
1111import Control.Applicative
12−import qualified Data.IntMap as M
1312import Data.List
1413import Data.Maybe
1514import Debug.Trace
1615
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−
15916class Optimisable term where
16017 applyOpts :: term -> Idris term
161− stripCollapsed :: term -> Idris term
16218
16319instance (Optimisable a, Optimisable b) => Optimisable (a, b) where
16420 applyOpts (x, y) = (,) <$> applyOpts x <*> applyOpts y
165− stripCollapsed (x, y) = (,) <$> stripCollapsed x <*> stripCollapsed y
16621
16722instance (Optimisable a, Optimisable b) => Optimisable (vs, a, b) where
16823 applyOpts (v, x, y) = (,,) v <$> applyOpts x <*> applyOpts y
169− stripCollapsed (v, x, y) = (,,) v <$> stripCollapsed x <*> stripCollapsed y
17024
17125instance Optimisable a => Optimisable [a] where
17226 applyOpts = mapM applyOpts
173− stripCollapsed = mapM stripCollapsed
17427
17528instance Optimisable a => Optimisable (Either a (a, a)) where
17629 applyOpts (Left t) = Left <$> applyOpts t
17730 applyOpts (Right t) = Right <$> applyOpts t
178− stripCollapsed (Left t) = Left <$> stripCollapsed t
179− stripCollapsed (Right t) = Right <$> stripCollapsed t
18031
18132-- Raw is for compile time optimisation (before type checking)
18233-- Term is for run time optimisation (after type checking, collapsing allowed)
183−
18434-- Compile time: no collapsing
18535
18636instance Optimisable Raw where
18737 applyOpts t@(RApp f a)
18838 | (Var n, args) <- raw_unapply t -- MAGIC HERE
189− = do args' <- 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'
39+ = raw_apply (Var n) <$> mapM applyOpts args
19440 | otherwise = RApp <$> applyOpts f <*> applyOpts a
19541
19642 applyOpts (RBind n b t) = RBind n <$> applyOpts b <*> applyOpts t
19743 applyOpts (RForce t) = applyOpts t
19844 applyOpts t = return t
19945
200− stripCollapsed t = return t
201−
20246-- Erase types (makes ibc smaller, and we don't need them)
20347instance Optimisable (Binder (TT Name)) where
20448 applyOpts (Let t v) = Let <$> return Erased <*> applyOpts v
20549 applyOpts b = return (b { binderTy = Erased })
206− stripCollapsed (Let t v) = Let <$> return Erased <*> stripCollapsed v
207− stripCollapsed b = return (b { binderTy = Erased })
20850
20951instance Optimisable (Binder Raw) where
21052 applyOpts b = do t' <- applyOpts (binderTy b)
21153 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
23054
23155-- Run-time: do everything
23256
@@ -249,54 +73,22 @@ instance Optimisable (TT Name) where
24973 | fn == txt "toIntegerNat" && mod == prel
25074 = return (App (P Ref (sNS (sUN "id") ["Basics","Prelude"]) Erased) Erased)
25175 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 []
255− _ -> return c
76+ = return $ applyDataOptRT n t arity []
25677 applyOpts t@(App f a)
25778 | (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'
262− _ -> return (mkApp c args')
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
267− t' <- applyOpts t
268− return (Bind n b' t')
269− applyOpts (Proj t i) = do t' <- applyOpts t
270− return (Proj t' i)
79+ = applyDataOptRT n t arity <$> mapM applyOpts args
80+ | otherwise = App <$> applyOpts f <*> applyOpts a
81+ applyOpts (Bind n b t) = Bind n <$> applyOpts b <*> applyOpts t
82+ applyOpts (Proj t i) = Proj <$> applyOpts t <*> pure i
27183 applyOpts t = return t
27284
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
292−
293−applyDataOptRT :: OptInfo -> Name -> Int -> Int -> [Term] -> Term
294−applyDataOptRT oi n tag arity args
295− | length args == arity = doOpts n args (collapsible oi) (M.fromList $ forceable oi)
85+-- Need to saturate arguments first to ensure that optimisation happens uniformly
86+applyDataOptRT :: Name -> Int -> Int -> [Term] -> Term
87+applyDataOptRT n tag arity args
88+ | length args == arity = doOpts n args
29689 | otherwise = let extra = satArgs (arity - length args)
29790 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
30092 where
30193 satArgs n = map (\i -> sMN i "sat") [1..n]
30294
@@ -305,20 +97,11 @@ applyDataOptRT oi n tag arity args
30597
30698 -- Nat special cases
30799 -- 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]) []
309101 | z == txt "Z" && nat == txt "Nat" && prelude == txt "Prelude"
310102 = Constant (BI 0)
311− doOpts (NS (UN s) [nat, prelude]) [k] _ _
103+ doOpts (NS (UN s) [nat, prelude]) [k]
312104 | s == txt "S" && nat == txt "Nat" && prelude == txt "Prelude"
313105 = App (App (P Ref (sUN "prim__addBigInt") Erased) k) (Constant (BI 1))
314106
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)
323− args' = [t | (f, t) <- zip (forcedArgSeq oi) args, f /= Just Unconditional]
324−
107+ doOpts n args = mkApp (P (DCon tag arity) n Erased) args
src/Idris/DeepSeq.hs+6−10
@@ -50,10 +50,6 @@ instance NFData CT.NumWrapper where
5050
5151-- All generated by 'derive'
5252
53−instance NFData Forceability where
54− rnf Conditional = ()
55− rnf Unconditional = ()
56−
5753instance NFData IntTy where
5854 rnf (ITFixed x1) = rnf x1 `seq` ()
5955 rnf ITNative = ()
@@ -276,10 +272,10 @@ instance (NFData t) => NFData (PDo' t) where
276272instance (NFData t) => NFData (PArg' t) where
277273 rnf (PImp x1 x2 x3 x4 x5)
278274 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
279− rnf (PExp x1 x2 x3)
280− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
281− rnf (PConstraint x1 x2 x3)
282− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
275+ rnf (PExp x1 x2 x3 x4)
276+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
277+ rnf (PConstraint x1 x2 x3 x4)
278+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
283279 rnf (PTacImplicit x1 x2 x3 x4 x5)
284280 = rnf x1 `seq`
285281 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
@@ -290,8 +286,8 @@ instance NFData ClassInfo where
290286 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()
291287
292288instance NFData OptInfo where
293− rnf (Optimise x1 x2 x3 x4)
294− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
289+ rnf (Optimise x1 x2)
290+ = rnf x1 `seq` rnf x2 `seq` ()
295291
296292instance NFData TypeInfo where
297293 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
5858 = PLam n (de env [] ty) (de ((n,n):env) [] sc)
5959 de env ((PImp { argopts = opts }):is) (Bind n (Pi ty) sc)
6060 = 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)
6262 = PPi constraint n (de env [] ty) (de ((n,n):env) is sc)
6363 de env (PTacImplicit _ _ _ tac _:is) (Bind n (Pi ty) sc)
6464 = 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
121121 | otherwise = PApp un (PRef un n) (map pexp args)
122122
123123 imp (PImp p m l n _) arg = PImp p m l n arg
124− imp (PExp p l _) arg = PExp p l arg
125− imp (PConstraint p l _) arg = PConstraint p l arg
124+ imp (PExp p l n _) arg = PExp p l n arg
125+ imp (PConstraint p l n _) arg = PConstraint p l n arg
126126 imp (PTacImplicit p l n sc _) arg = PTacImplicit p l n sc arg
127127
128128-- | How far to indent sub-errors
src/Idris/ElabDecls.hs+137−102
@@ -37,6 +37,7 @@ import Data.Maybe
3737import Debug.Trace
3838
3939import qualified Data.Map as Map
40+import qualified Data.Set as S
4041import qualified Data.Text as T
4142import Data.Char(isLetter, toLower)
4243import Data.List.Split (splitOn)
@@ -82,10 +83,13 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
8283
8384 logLvl 3 $ show n ++ " pre-type " ++ showTmImpls ty'
8485 ty' <- addUsingConstraints syn fc ty'
85− ty' <- implicit syn n ty'
86+ ty' <- implicit info syn n ty'
8687
87− let ty = addImpl i ty'
88+ let ty = addImpl i ty'
89+ inacc = inaccessibleArgs 0 ty
8890 logLvl 3 $ show n ++ " type " ++ showTmImpls ty
91+ logLvl 5 $ "Inaccessible arguments: " ++ show inacc
92+
8993 ((tyT, defer, is), log) <-
9094 tclift $ elaborate ctxt n (TType (UVal 0)) []
9195 (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
130134 addDocStr n doc argDocs
131135 addIBC (IBCDoc n)
132136 addIBC (IBCFlags n opts')
137+ saveInaccArgs n inacc
133138 when (Implicit `elem` opts') $ do addCoercion n
134139 addIBC (IBCCoercion n)
140+
135141 -- If the function is declared as an error handler and the language
136142 -- extension is enabled, then add it to the list of error handlers.
137143 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
172178 , ns4 == map txt ["Errors","Reflection","Language"] = True
173179 tyIsHandler _ = False
174180
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 _ _ = []
175205
176206elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring ->
177207 FC -> FnOpts -> Name -> PTerm -> Idris ()
178−elabPostulate info syn doc fc opts n ty
179− = do elabType info syn doc [] fc opts n ty
180− -- make sure it's collapsible, so it is never needed at run time
181− -- start by getting the elaborated type
182− ctxt <- getContext
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
198− solveDeferred n
208+elabPostulate info syn doc fc opts n ty = do
209+ elabType info syn doc [] fc opts n ty
210+ putIState . (\ist -> ist{ idris_postulates = S.insert n (idris_postulates ist) }) =<< getIState
211+ addIBC (IBCPostulate n)
212+
213+ -- remove it from the deferred definitions list
214+ solveDeferred n
199215
200216elabData :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] -> FC -> DataOpts -> PData -> Idris ()
201217elabData 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)
204220 checkUndefined fc n
205221 ctxt <- getContext
206222 i <- getIState
207− t_in <- implicit syn n t_in
223+ -- TODO think: something more in info?
224+ t_in <- implicit info syn n t_in
208225 let t = addImpl i t_in
209226 ((t', defer, is), log) <- tclift $ elaborate ctxt n (TType (UVal 0)) []
210227 (erun fc (build i info False [] n t))
211228 def' <- checkDef fc defer
212229 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'
213230 addDeferredTyCon def''
231+ addIBC (IBCDef n)
214232 mapM_ (elabCaseBlock info []) is
215233 (cty, _) <- recheckC fc [] t'
216234 logLvl 2 $ "---> " ++ show cty
@@ -222,7 +240,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
222240 undef <- isUndefined fc n
223241 ctxt <- getContext
224242 i <- getIState
225− t_in <- implicit syn n t_in
243+ t_in <- implicit info syn n t_in
226244 let t = addImpl i t_in
227245 ((t', defer, is), log) <-
228246 tclift $ elaborate ctxt n (TType (UVal 0)) []
@@ -238,7 +256,8 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
238256 logLvl 2 $ "---> " ++ show cty
239257 -- temporary, to check cons
240258 when undef $ updateContext (addTyDecl n (TCon 0 0) cty)
241− cons <- mapM (elabCon info syn n codata) dcons
259+ let cnameinfo = cinfo info (map cname dcons)
260+ cons <- mapM (elabCon cnameinfo syn n codata) dcons
242261 ttag <- getName
243262 i <- getIState
244263 let as = map (const Nothing) (getArgTys cty)
@@ -255,15 +274,30 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
255274 let metainf = DataMI params
256275 addIBC (IBCMetaInformation n metainf)
257276 -- TMP HACK! Make this a data option
258− when (n /= sUN "Lazy'") $ collapseCons n cons
259277 updateContext (addDatatype (Data n ttag cty cons))
260278 updateContext (setMetaInformation n metainf)
261279 mapM_ (checkPositive n) cons
262− if DefaultEliminator `elem` opts
263− then evalStateT (elabEliminator params n t dcons info) Map.empty
264− else return ()
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
289+ when (DefaultEliminator `elem` opts) $
290+ evalStateT (elabEliminator params n t dcons info) Map.empty
265291 where
266− checkDefinedAs fc n t ctxt
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+
300+ checkDefinedAs fc n t ctxt
267301 = case lookupDef n ctxt of
268302 [] -> return ()
269303 [TyDecl _ ty] ->
@@ -321,6 +355,21 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
321355 | otherwise = count n ts
322356 mParam args (_ : rest) = Nothing : mParam args rest
323357
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+
324373type EliminatorState = StateT (Map.Map String Int) Idris
325374
326375-- 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 ->
730779 PTerm -> Docstring -> Name -> PTerm -> Idris ()
731780elabRecord info syn doc fc tyn ty cdoc cn cty
732781 = do elabData info syn doc [] fc [] (PDatadecl tyn ty [(cdoc, [], cn, cty, fc, [])])
733− cty' <- implicit syn cn cty
782+ -- TODO think: something more in info?
783+ cty' <- implicit info syn cn cty
734784 i <- getIState
735785 cty <- case lookupTy cn (tt_ctxt i) of
736786 [t] -> return (delab i t)
@@ -752,7 +802,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
752802 where
753803-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }
754804
755− isNonImp (PExp _ _ _, a) = Just a
805+ isNonImp (PExp _ _ _ _, a) = Just a
756806 isNonImp _ = Nothing
757807
758808 tryElabDecl info (fn, ty, val)
@@ -835,15 +885,22 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
835885 (map pexp rhsArgs)) []
836886 return (pn, pfnTy, PClauses fc [] setname [pclause])
837887
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
838893elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
839894 (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> Idris (Name, Type)
840895elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)
841896 = do checkUndefined fc n
842897 ctxt <- getContext
843898 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)
845900 let t = addImpl i t_in
846901 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t
902+ let inacc = inaccessibleArgs 0 t
903+ logLvl 5 $ "Inaccessible args: " ++ show inacc
847904 ((t', defer, is), log) <-
848905 tclift $ elaborate ctxt n (TType (UVal 0)) []
849906 (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)
861918 checkDocs fc argDocs t_in
862919 addDocStr n doc argDocs
863920 addIBC (IBCDoc n)
864− let fs = map (getNamePos 0 t) forcenames
865− -- FIXME: 'forcenames' is an almighty hack! Need a better way of
866− -- erasing non-forceable things
867− forceArgs tn n (mapMaybe (getNamePos 0 t) forcenames) cty'
921+ saveInaccArgs n inacc
922+ addIBC (IBCOpt n)
868923 return (n, cty')
869924 where
870925 tyIs (Bind n b sc) = tyIs sc
@@ -875,7 +930,7 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)
875930
876931 mkLazy (PPi pl n ty sc)
877932 = let ty' = if getTyName ty
878− then PApp fc (PRef fc (sUN "Lazy'"))
933+ then PApp fc (PRef fc (sUN "Lazy'"))
879934 [pexp (PRef fc (sUN "LazyCodata")),
880935 pexp ty]
881936 else ty in
@@ -897,6 +952,10 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)
897952elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()
898953elabClauses info fc opts n_in cs = let n = liftname info n_in in
899954 do ctxt <- getContext
955+ ist <- getIState
956+ let inacc = case lookupCtxt n (idris_optimisation ist) of
957+ [Optimise inacc _] -> map fst inacc
958+ _ -> []
900959 -- Check n actually exists, with no definition yet
901960 let tys = lookupTy n ctxt
902961 let reflect = Reflection `elem` opts
@@ -914,29 +973,13 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
914973
915974 logLvl 3 $ "Elaborated patterns:\n" ++ show pats_in
916975
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
929976 solveDeferred n
977+
930978 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 [] [])
937− (idris_optimisation ist)
938− putIState (ist { idris_optimisation = opts })
939− addIBC (IBCOpt n)
979+ let opts = addDef n (Optimise [] False) (idris_optimisation ist)
980+ in putIState (ist { idris_optimisation = opts })
981+ addIBC (IBCOpt n)
982+
940983 ist <- getIState
941984 let pats = map (simple_lhs (tt_ctxt ist)) $ doTransforms ist pats_in
942985
@@ -946,11 +989,8 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
946989 let tcase = opt_typecase (idris_options ist)
947990
948991 -- Summary of what's about to happen: Definitions go:
949−
950− -- pats_in -> pats -> optpats
951− -- pdef comes from pats,
952− -- optpdef comes from optpats
953− -- Then pdef' is optpdef with forcing/collapsing applied everywhere
992+ --
993+ -- pats_in -> pats -> pdef -> pdef'
954994
955995 -- addCaseDef builds case trees from <pdef> and <pdef'>
956996
@@ -979,20 +1019,12 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
9791019
9801020 numArgs <- tclift $ sameLength pdef
9811021
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−
9891022 case specNames opts of
9901023 Just _ -> logLvl 5 $ "Partially evaluated:\n" ++ show pats
9911024 _ -> return ()
9921025
993− let optpdef = map debind optpats -- \$ map (simple_lhs (tt_ctxt ist)) optpats
9941026 tree@(CaseDef scargs sc _) <- tclift $
995− simpleCase tcase False reflect CompileTime fc atys pdef
1027+ simpleCase tcase False reflect CompileTime fc inacc atys pdef
9961028 cov <- coverage
9971029 pmissing <-
9981030 if cov && not (hasDefault cs)
@@ -1014,7 +1046,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
10141046 let pcover = null pmissing
10151047
10161048 -- pdef' is the version that gets compiled for run-time
1017− pdef_in' <- applyOpts optpdef
1049+ pdef_in' <- applyOpts pdef
10181050 let pdef' = map (simple_rt (tt_ctxt ist)) pdef_in'
10191051
10201052 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
10411073 let knowncovering = (pcover && cov) || AssertTotal `elem` opts
10421074
10431075 tree' <- tclift $ simpleCase tcase knowncovering reflect
1044− RunTime fc atys pdef'
1045− logLvl 3 (show tree)
1076+ RunTime fc inacc atys pdef'
1077+ logLvl 3 $ "Unoptimised " ++ show n ++ ": " ++ show tree
10461078 logLvl 3 $ "Optimised: " ++ show tree'
10471079 ctxt <- getContext
10481080 ist <- getIState
1081+ let opt = idris_optimisation ist
10491082 putIState (ist { idris_patdefs = addDef n (force pdef', force pmissing)
10501083 (idris_patdefs ist) })
10511084 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
10551088 reflect
10561089 (AssertTotal `elem` opts)
10571090 atys
1091+ inacc
10581092 pats
10591093 pdef pdef pdef_inl pdef' ty)
10601094 addIBC (IBCDef n)
@@ -1071,7 +1105,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
10711105 let used = findUsedArgs sc' scargs'
10721106 -- let scg = buildSCG i sc scargs
10731107 -- 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
10751109 logLvl 2 $ "Called names: " ++ show cg
10761110 addToCG n cg
10771111 addToCalledG n (nub (map fst calls)) -- plus names in type!
@@ -1292,7 +1326,7 @@ checkPossible info fc tcgen fname lhs_in
12921326 ((P _ x _, _), (P _ y _, _)) -> x == y
12931327 _ -> False
12941328
1295−getFixedInType i env (PExp _ _ _ : is) (Bind n (Pi t) sc)
1329+getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi t) sc)
12961330 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)
12971331getFixedInType i env (_ : is) (Bind n (Pi t) sc)
12981332 = 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)
14231457 -- Elaborate where block
14241458 ist <- getIState
14251459 windex <- getName
1426− let winfo = pinfo (pvars ist lhs_tm) whereblock windex
14271460 let decls = nub (concatMap declared whereblock)
14281461 let defs = nub (decls ++ concatMap defined whereblock)
14291462 let newargs = pvars ist lhs_tm
1463+ let winfo = pinfo info newargs defs windex
14301464 let wb = map (expandParamsD False ist decorate newargs defs) whereblock
14311465
14321466 -- 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)
14351469 let (wbefore, wafter) = sepBlocks wb
14361470
14371471 logLvl 2 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter
1438− mapM_ (elabDecl' EAll info) wbefore
1472+ mapM_ (elabDecl' EAll winfo) wbefore
14391473 -- Now build the RHS, using the type of the LHS as the goal.
14401474 i <- getIState -- new implicits from where block
14411475 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)
14501484 mapM_ setinj (nub (params ++ inj))
14511485 setNextName
14521486 (_, _, 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))
14541488 errAt "right hand side of " fname
14551489 (erun fc $ psolve lhs_tm)
14561490 hs <- get_holes
@@ -1478,8 +1512,8 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
14781512 -- Now the remaining deferred (i.e. no type declarations) clauses
14791513 -- from the where block
14801514
1481− mapM_ (elabDecl' EAll info) wafter
1482− mapM_ (elabCaseBlock info opts) is
1515+ mapM_ (elabDecl' EAll winfo) wafter
1516+ mapM_ (elabCaseBlock winfo opts) is
14831517
14841518 ctxt <- getContext
14851519 logLvl 5 $ "Rechecking"
@@ -1509,6 +1543,19 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
15091543 addErrRev (crhs, clhs)
15101544 return $ (Right (clhs, crhs), lhs)
15111545 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+
15121559 mkLHSapp t@(PRef _ _) = trace ("APP " ++ show t) $ PApp fc t []
15131560 mkLHSapp t = t
15141561
@@ -1531,19 +1578,6 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
15311578 (b : bf, af)
15321579 sepBlocks' ns [] = ([], [])
15331580
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−
15471581
15481582 -- if a hole is just an argument/result of a case block, treat it as
15491583 -- the unit type. Hack to help elaborate case in do blocks.
@@ -1808,7 +1842,7 @@ elabClass info syn doc fc constraints tn ps ds
18081842
18091843 getMName (PTy _ _ _ _ _ n _) = nsroot n
18101844 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
18121846 logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'
18131847 return ( (n, (toExp (map fst ps) Exp t')),
18141848 (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
20122046 -- TODO: largely based upon elabType' - should try to abstract
20132047 elabFindOverlapping i ci iname syn t
20142048 = do ty' <- addUsingConstraints syn fc t
2015− ty' <- implicit syn iname ty'
2049+ -- TODO think: something more in info?
2050+ ty' <- implicit info syn iname ty'
20162051 let ty = addImpl i ty'
20172052 ctxt <- getContext
20182053 ((tyT, _, _), _) <-
@@ -2050,9 +2085,9 @@ elabInstance info syn what fc cs n ps t expn ds = do
20502085 methArgs i (PPi (Imp _ _ _) n ty sc)
20512086 = PImp 0 True [] n (PRef fc (sMN i "meth")) : methArgs (i+1) sc
20522087 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
20542089 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
20562091 methArgs i _ = []
20572092
20582093 papp fc f [] = f
@@ -2068,7 +2103,7 @@ elabInstance info syn what fc cs n ps t expn ds = do
20682103 _ -> return ps'
20692104 getWParams (_ : ps) = getWParams ps
20702105
2071− decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns
2106+ decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns
20722107 decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns
20732108
20742109 mkTyDecl (n, op, t, _) = PTy emptyDocstring [] syn fc op n t
src/Idris/ElabTerm.hs+4−13
@@ -3,6 +3,7 @@
33module Idris.ElabTerm where
44
55import Idris.AbsSyntax
6+import Idris.AbsSyntaxTree
67import Idris.DSL
78import Idris.Delaborate
89import Idris.Error
@@ -27,16 +28,6 @@ import qualified Data.Text as T
2728
2829import Debug.Trace
2930
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−
4031-- Using the elaborator, convert a term in raw syntax to a fully
4132-- elaborated, typechecked term.
4233--
@@ -474,7 +465,7 @@ elab ist info pattern opts fn tm
474465 elabArgs ist (ina || not isinf, guarded, inty)
475466 [] fc False f ns'
476467 (f == sUN "Force")
477− (map (\x -> (lazyarg x, getTm x)) eargs)
468+ (map (\x -> (False, getTm x)) eargs) -- TODO: remove this False arg
478469 solve
479470 ivs' <- get_instances
480471 -- Attempt to resolve any type classes which have 'complete' types,
@@ -697,7 +688,7 @@ elab ist info pattern opts fn tm
697688 where
698689 mkDelay (PAlternative b xs) = PAlternative b (map mkDelay xs)
699690 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"))
701692 [pexp t])
702693
703694 insertCoerce ina t =
@@ -733,7 +724,7 @@ elab ist info pattern opts fn tm
733724 = elabArgs ist ina failed fc r f ns force args
734725 elabArgs ist ina failed fc r f ((argName, holeName):ns) force ((lazy, t) : args)
735726 | lazy && not pattern
736− = elabArg argName holeName (PApp bi (PRef bi (sUN "lazy"))
727+ = elabArg argName holeName (PApp bi (PRef bi (sUN "Delay"))
737728 [pimp (sUN "a") Placeholder True,
738729 pexp t])
739730 | 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
1919import Data.List
2020import Data.ByteString.Lazy as B hiding (length, elem, map)
2121import qualified Data.Text as T
22+import qualified Data.Set as S
2223
2324import Control.Monad
2425import Control.Monad.State.Strict hiding (get, put)
@@ -29,7 +30,7 @@ import Codec.Compression.Zlib (compress)
2930import Util.Zlib (decompressEither)
3031
3132ibcVersion :: Word8
32−ibcVersion = 65
33+ibcVersion = 67
3334
3435data IBCFile = IBCFile { ver :: Word8,
3536 sourcefile :: FilePath,
@@ -65,7 +66,8 @@ data IBCFile = IBCFile { ver :: Word8,
6566 ibc_errorhandlers :: [Name],
6667 ibc_function_errorhandlers :: [(Name, Name, Name)], -- fn, arg, handler
6768 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]
6971 }
7072 deriving Show
7173{-!
@@ -73,7 +75,7 @@ deriving instance Binary IBCFile
7375!-}
7476
7577initIBC :: IBCFile
76−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []
78+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []
7779
7880loadIBC :: FilePath -> Idris ()
7981loadIBC fp = do imps <- getImported
@@ -236,6 +238,7 @@ ibc i (IBCMetavar n) f =
236238 case lookup n (idris_metavars i) of
237239 Nothing -> return f
238240 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 }
239242
240243process :: IBCFile -> FilePath -> Idris ()
241244process i fn
@@ -278,6 +281,7 @@ process i fn
278281 pErrorHandlers (ibc_errorhandlers i)
279282 pFunctionErrorHandlers (ibc_function_errorhandlers i)
280283 pMetavars (ibc_metavars i)
284+ pPostulates (ibc_postulates i)
281285
282286timestampOlder :: FilePath -> FilePath -> IO ()
283287timestampOlder src ibc = do srct <- getModificationTime src
@@ -286,6 +290,11 @@ timestampOlder src ibc = do srct <- getModificationTime src
286290 then fail "Needs reloading"
287291 else return ()
288292
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+
289298pImports :: [FilePath] -> Idris ()
290299pImports fs
291300 = do mapM_ (\f -> do i <- getIState
@@ -1093,10 +1102,6 @@ safeToEnum label x' = result
10931102 = error $ label ++ ": corrupted binary representation in IBC"
10941103 | otherwise = toEnum x
10951104
1096−instance Binary Forceability where
1097− put = putWord8 . fromIntegral . fromEnum
1098− get = safeToEnum "Forceability" `fmap` getWord8
1099−
11001105instance Binary PReason where
11011106 put x
11021107 = case x of
@@ -1156,7 +1161,7 @@ instance Binary MetaInformation where
11561161 return (DataMI x1)
11571162
11581163instance 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)
11601165 = {-# SCC "putIBCFile" #-}
11611166 do put x1
11621167 put x2
@@ -1193,6 +1198,7 @@ instance Binary IBCFile where
11931198 put x33
11941199 put x34
11951200 put x35
1201+ put x36
11961202
11971203 get
11981204 = do x1 <- get
@@ -1231,7 +1237,8 @@ instance Binary IBCFile where
12311237 x33 <- get
12321238 x34 <- get
12331239 x35 <- 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)
1240+ x36 <- get
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)
12351242 else return (initIBC { ver = x1 })
12361243
12371244instance Binary DataOpt where
@@ -1317,13 +1324,13 @@ instance Binary FixDecl where
13171324instance Binary ArgOpt where
13181325 put x
13191326 = case x of
1320− Lazy -> putWord8 0
1321− HideDisplay -> putWord8 1
1327+ HideDisplay -> putWord8 0
1328+ InaccessibleArg -> putWord8 1
13221329 get
13231330 = do i <- getWord8
13241331 case i of
1325− 0 -> return Lazy
1326− 1 -> return HideDisplay
1332+ 0 -> return HideDisplay
1333+ 1 -> return InaccessibleArg
13271334 _ -> error "Corrupted binary data for Static"
13281335
13291336instance Binary Static where
@@ -2037,16 +2044,18 @@ instance (Binary t) => Binary (PArg' t) where
20372044 put x3
20382045 put x4
20392046 put x5
2040− PExp x1 x2 x3 ->
2047+ PExp x1 x2 x3 x4 ->
20412048 do putWord8 1
20422049 put x1
20432050 put x2
20442051 put x3
2045− PConstraint x1 x2 x3 ->
2052+ put x4
2053+ PConstraint x1 x2 x3 x4 ->
20462054 do putWord8 2
20472055 put x1
20482056 put x2
20492057 put x3
2058+ put x4
20502059 PTacImplicit x1 x2 x3 x4 x5 ->
20512060 do putWord8 3
20522061 put x1
@@ -2066,11 +2075,13 @@ instance (Binary t) => Binary (PArg' t) where
20662075 1 -> do x1 <- get
20672076 x2 <- get
20682077 x3 <- get
2069− return (PExp x1 x2 x3)
2078+ x4 <- get
2079+ return (PExp x1 x2 x3 x4)
20702080 2 -> do x1 <- get
20712081 x2 <- get
20722082 x3 <- get
2073− return (PConstraint x1 x2 x3)
2083+ x4 <- get
2084+ return (PConstraint x1 x2 x3 x4)
20742085 3 -> do x1 <- get
20752086 x2 <- get
20762087 x3 <- get
@@ -2096,17 +2107,13 @@ instance Binary ClassInfo where
20962107 return (CI x1 x2 x3 x4 x5 [])
20972108
20982109instance Binary OptInfo where
2099− put (Optimise x1 x2 x3 x4)
2110+ put (Optimise x1 x2)
21002111 = do put x1
21012112 put x2
2102− put x3
2103− put x4
21042113 get
21052114 = do x1 <- get
21062115 x2 <- get
2107− x3 <- get
2108− x4 <- get
2109− return (Optimise x1 x2 x3 x4)
2116+ return (Optimise x1 x2)
21102117
21112118instance Binary TypeInfo where
21122119 put (TI x1 x2 x3 x4) = do put x1
src/Idris/IdeSlave.hs+2
@@ -151,6 +151,7 @@ data IdeSlaveCommand = REPLCompletions String
151151 | Apropos String
152152 | GetOpts
153153 | SetOpt Opt Bool
154+ | Metavariables Int -- ^^ the Int is the column count for pretty-printing
154155 deriving Show
155156
156157sexpToCommand :: SExp -> Maybe IdeSlaveCommand
@@ -174,6 +175,7 @@ sexpToCommand (SymbolAtom "get-options")
174175sexpToCommand (SexpList [SymbolAtom "set-option", SymbolAtom s, BoolAtom b])
175176 | Just opt <- lookup s opts = Just (SetOpt opt b)
176177 where opts = [("show-implicits", ShowImpl), ("error-context", ErrContext)] --TODO support more
178+sexpToCommand (SexpList [SymbolAtom "metavariables", IntegerAtom cols]) = Just (Metavariables (fromIntegral cols))
177179sexpToCommand _ = Nothing
178180
179181parseMessage :: String -> Either Err (SExp, Integer)
src/Idris/ParseExpr.hs+29−15
@@ -150,15 +150,23 @@ extension syn (Rule ssym ptm _)
150150 update ns (PRef fc n) = case lookup n ns of
151151 Just (SynTm t) -> t
152152 _ -> PRef fc n
153− update ns (PLam n ty sc) = PLam (updateB ns n) (update ns ty) (update (dropn n ns) sc)
154− update ns (PPi p n ty sc) = PPi p (updateB ns n) (update ns ty) (update (dropn n ns) sc)
155− update ns (PLet n ty val sc) = PLet (updateB ns n) (update ns ty) (update ns val)
156− (update (dropn n ns) sc)
157− update ns (PApp fc t args) = PApp fc (update ns t) (map (fmap (update ns)) args)
158− update ns (PAppBind fc t args) = PAppBind fc (update ns t) (map (fmap (update ns)) args)
159− update ns (PCase fc c opts) = PCase fc (update ns c) (map (pmap (update ns)) opts)
153+ update ns (PLam n ty 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)
157+ (update ns ty) (update (dropn n ns) sc)
158+ update ns (PLet n ty val sc)
159+ = PLet (updateB ns n) (update ns ty)
160+ (update ns val) (update (dropn n ns) sc)
161+ update ns (PApp fc t args)
162+ = PApp fc (update ns t) (map (fmap (update ns)) args)
163+ update ns (PAppBind fc t args)
164+ = PAppBind fc (update ns t) (map (fmap (update ns)) args)
165+ update ns (PCase fc c opts)
166+ = PCase fc (update ns c) (map (pmap (update ns)) opts)
160167 update ns (PPair fc p l r) = PPair fc p (update ns l) (update ns r)
161− update ns (PDPair fc p l t r) = PDPair fc p (update ns l) (update ns t) (update ns r)
168+ update ns (PDPair fc p l t r)
169+ = PDPair fc p (update ns l) (update ns t) (update ns r)
162170 update ns (PAlternative a as) = PAlternative a (map (update ns) as)
163171 update ns (PHidden t) = PHidden (update ns t)
164172 update ns (PDoBlock ds) = PDoBlock $ upd ns ds
@@ -176,6 +184,9 @@ extension syn (Rule ssym ptm _)
176184 update ns (PGoal fc r n sc) = PGoal fc (update ns r) n (update ns sc)
177185 update ns t = t
178186
187+ updTacImp ns (TacImp o st scr) = TacImp o st (update ns scr)
188+ updTacImp _ x = x
189+
179190{- | Parses a (normal) built-in expression
180191@
181192InternalExpr ::=
@@ -788,18 +799,15 @@ Pi ::=
788799
789800pi :: SyntaxInfo -> IdrisParser PTerm
790801pi syn =
791− do opts <- -- if implicitAllowed syn -- laziness is top level only
792− -- then option [] (do lchar '|'; return [Lazy])
793− -- else return []
794− return []
795− st <- static
802+ do opts <- piOpts syn
803+ st <- static
796804 (do try (lchar '('); xt <- typeDeclList syn; lchar ')'
797805 symbol "->"
798806 sc <- expr syn
799807 return (bindList (PPi (Exp opts st False)) xt sc)) <|> (do
800808 lchar '{'
801809 (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"
803811 xt <- typeDeclList syn
804812 lchar '}'
805813 symbol "->"
@@ -808,7 +816,7 @@ pi syn =
808816 (TacImp [] Dynamic (PTactics [Trivial]))) xt sc))
809817 <|> (do
810818 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"
812820 script <- simpleExpr syn
813821 xt <- typeDeclList syn
814822 lchar '}'
@@ -824,6 +832,12 @@ pi syn =
824832 else do fail "no implicit arguments allowed here"))
825833 <?> "dependent type signature"
826834
835+piOpts :: SyntaxInfo -> IdrisParser [ArgOpt]
836+piOpts syn | implicitAllowed syn =
837+ lchar '.' *> return [InaccessibleArg]
838+ <|> return []
839+piOpts syn = return []
840+
827841{- | Parses a type constraint list
828842
829843@
src/Idris/Parser.hs+9−3
@@ -17,14 +17,15 @@ import qualified Text.Parser.Char as Chr
1717import qualified Text.Parser.Token.Highlight as Hi
1818
1919import Text.PrettyPrint.ANSI.Leijen (Doc, plain)
20+import qualified Text.PrettyPrint.ANSI.Leijen as ANSI
2021
21−import Idris.AbsSyntax
22+import Idris.AbsSyntax hiding (namespace, params)
2223import Idris.DSL
2324import Idris.Imports
2425import Idris.Delaborate
2526import Idris.Error
2627import Idris.ElabDecls
27−import Idris.ElabTerm hiding (namespace, params)
28+import Idris.ElabTerm
2829import Idris.Coverage
2930import Idris.IBC
3031import Idris.Unlit
@@ -1120,6 +1121,11 @@ findFC x = let s = show (plain x) in
11201121 (col, ':':msg) -> let pos = (read line, read col) in
11211122 (FC failname pos pos, msg)
11221123
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+
11231129-- | A program is a list of declarations, possibly with associated
11241130-- documentation strings.
11251131parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
@@ -1132,7 +1138,7 @@ parseProg syn fname input mrk
11321138 let (fc, msg) = findFC doc
11331139 i <- getIState
11341140 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)
11361142 IdeSlave n -> ihWarn (idris_outh i) fc (P.text msg)
11371143 putIState (i { errSpan = Just fc })
11381144 return []
src/Idris/PartialEval.hs+1−1
@@ -124,7 +124,7 @@ getSpecApps ist env tm = ga env (explicitNames tm) where
124124 | imparg imp = (ImplicitD, tm)
125125 | otherwise = (ExplicitD, (P Ref (sUN (show n ++ "arg")) Erased))
126126
127− imparg (PExp _ _ _) = False
127+ imparg (PExp _ _ _ _) = False
128128 imparg _ = True
129129
130130 buildApp env [] [] _ _ = []
src/Idris/Prover.hs+6−5
@@ -7,6 +7,7 @@ import Idris.Core.CaseTree
77import Idris.Core.Typecheck
88
99import Idris.AbsSyntax
10+import Idris.AbsSyntaxTree
1011import Idris.Delaborate
1112import Idris.ElabDecls
1213import Idris.ElabTerm
@@ -33,7 +34,7 @@ prover lit x =
3334 i <- getIState
3435 case lookupTy x ctxt of
3536 [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
3738 else ifail $ show x ++ " is not a metavariable"
3839 _ -> fail "No such metavariable"
3940
@@ -56,8 +57,8 @@ assumptionNames e
5657 names ((MN _ _, _) : bs) = names bs
5758 names ((n, _) : bs) = show n : names bs
5859
59−prove :: Context -> Bool -> Name -> Type -> Idris ()
60−prove ctxt lit n ty
60+prove :: Ctxt OptInfo -> Context -> Bool -> Name -> Type -> Idris ()
61+prove opt ctxt lit n ty
6162 = do let ps = initElaborator n ctxt ty
6263 ideslavePutSExp "start-proof-mode" n
6364 (tm, prf) <- ploop n True ("-" ++ show n) [] (ES (ps, []) "" Nothing) Nothing
@@ -67,7 +68,7 @@ prove ctxt lit n ty
6768 ideslavePutSExp "end-proof-mode" n
6869 let proofs = proof_list i
6970 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)]
7172 logLvl 3 (show tree)
7273 (ptm, pty) <- recheckC (fileFC "proof") [] tm
7374 logLvl 5 ("Proof type: " ++ show pty ++ "\n" ++
@@ -77,7 +78,7 @@ prove ctxt lit n ty
7778 Error e -> ierror (CantUnify False ty pty e [] 0)
7879 ptm' <- applyOpts ptm
7980 updateContext (addCasedef n (CaseInfo True False) False False True False
80− []
81+ [] [] -- argtys, inaccArgs
8182 [Right (P Ref n ty, ptm)]
8283 [([], P Ref n ty, ptm)]
8384 [([], P Ref n ty, ptm)]
src/Idris/Providers.hs+2−1
@@ -11,7 +11,8 @@ import Debug.Trace
1111
1212-- | Wrap a type provider in the type of type providers
1313providerTy :: FC -> PTerm -> PTerm
14−providerTy fc tm = PApp fc (PRef fc $ sUN "Provider") [PExp 0 [] tm]
14+providerTy fc tm
15+ = PApp fc (PRef fc $ sUN "Provider") [PExp 0 [] (sMN 0 "pvarg") tm]
1516
1617ioret = sUN "prim_io_return"
1718ermod = sNS (sUN "Error") ["Providers"]
src/Idris/REPL.hs+154−103
@@ -8,16 +8,16 @@ import Idris.Apropos (apropos)
88import Idris.REPLParser
99import Idris.ElabDecls
1010import Idris.ElabTerm
11+import Idris.Erasure
1112import Idris.Error
1213import Idris.ErrReverse
1314import Idris.Delaborate
1415import Idris.Docstrings (Docstring, overview, renderDocstring)
1516import Idris.IdrisDoc
1617import Idris.Prover
17−import Idris.Parser
18+import Idris.Parser hiding (indent)
1819import Idris.Primitives
1920import Idris.Coverage
20−import Idris.UnusedArgs
2121import Idris.Docs hiding (Doc)
2222import Idris.Help
2323import Idris.Completion
@@ -81,8 +81,6 @@ import Data.Word (Word)
8181import Data.Either (partitionEithers)
8282import Control.DeepSeq
8383
84−import qualified Text.PrettyPrint.ANSI.Leijen as ANSI
85−
8684import Debug.Trace
8785
8886-- | Run the REPL
@@ -220,83 +218,133 @@ ideslave orig mods
220218 (f:_) -> f
221219 _ -> ""
222220 case IdeSlave.sexpToCommand sexp of
223− Just (IdeSlave.Interpret 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")
221+ Just cmd -> runIdeSlaveCommand id orig fn mods cmd
222+ Nothing -> iPrintError "did not understand" )
292223 (\e -> do iPrintError $ show e))
293224 (\e -> do iPrintError $ show e)
294225 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)
295280 where splitName :: String -> Either String Name
296281 splitName s = case reverse $ splitOn "." s of
297282 [] -> Left ("Didn't understand name '" ++ s ++ "'")
298283 [n] -> Right $ sUN n
299284 (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+
300348
301349ideslaveProcess :: FilePath -> Command -> Idris ()
302350ideslaveProcess fn Help = process stdout fn Help
@@ -609,7 +657,6 @@ process h fn (DebugInfo n)
609657 let d = lookupDef n (tt_ctxt i)
610658 when (not (null d)) $ iputStrLn $ "Definition: " ++ (show (head d))
611659 let cg = lookupCtxtName n (idris_callgraph i)
612− findUnusedArgs (map fst cg)
613660 i <- getIState
614661 let cg' = lookupCtxtName n (idris_callgraph i)
615662 sc <- checkSizeChange n
@@ -619,7 +666,8 @@ process h fn (DebugInfo n)
619666process h fn (Info n)
620667 = do i <- getIState
621668 case lookupCtxt n (idris_classes i) of
622− [c] -> classInfo c
669+ [c] -> do info <- classInfo c
670+ ihRenderResult h info
623671 _ -> iPrintError "Not a class"
624672process h fn (Search t) = iPrintError "Not implemented"
625673-- FIXME: There is far too much repetition in the cases below!
@@ -1009,28 +1057,31 @@ process h fn (MakeDoc s) =
10091057 case result of Right _ -> iputStrLn "IdrisDoc generated"
10101058 Left err -> iPrintError err
10111059
1012−classInfo :: ClassInfo -> Idris ()
1013−classInfo ci = do iputStrLn "Methods:\n"
1014− mapM_ dumpMethod (class_methods ci)
1015− iputStrLn ""
1016− iputStrLn "Default superclass instances:\n"
1017− mapM_ dumpDefaultInstance (class_default_superclasses ci)
1018− iputStrLn ""
1019− iputStrLn "Instances:\n"
1020− mapM_ dumpInstance (class_instances ci)
1021− iPrintResult ""
1022−
1023−dumpMethod :: (Name, (FnOpts, PTerm)) -> Idris ()
1024−dumpMethod (n, (_, t)) = iputStrLn $ show n ++ " : " ++ show t
1025−
1026−dumpDefaultInstance :: PDecl -> Idris ()
1027−dumpDefaultInstance (PInstance _ _ _ _ _ t _ _) = iputStrLn $ show t
1028−
1029−dumpInstance :: Name -> Idris ()
1030−dumpInstance n = do i <- getIState
1031− ctxt <- getContext
1032− case lookupTy n ctxt of
1033− ts -> mapM_ (\t -> iputStrLn $ showTm i (delab i t)) ts
1060+
1061+classInfo :: ClassInfo -> Idris (Doc OutputAnnotation)
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 <>
1069+ indent 2 (vsep (map (dumpMethod ist) (class_methods ci))) <> line <> line <>
1070+ text "Default superclass instances:" <>
1071+ line <>
1072+ indent 2 (vsep (map (dumpDefaultInstance ist) (class_default_superclasses ci))) <>
1073+ line <>
1074+ text "Instances:" <> line <>
1075+ indent 2 (vsep (map (dumpInstance ist ctxt) (class_instances ci)))
1076+ where dumpMethod :: IState -> (Name, (FnOpts, PTerm)) -> Doc OutputAnnotation
1077+ dumpMethod ist (n, (_, t)) = prettyName False [] n <+> colon <+> pp ist t
1078+ dumpDefaultInstance :: IState -> PDecl -> Doc OutputAnnotation
1079+ dumpDefaultInstance ist (PInstance _ _ _ _ _ t _ _) = pp ist t
1080+ dumpInstance :: IState -> Context -> Name -> Doc OutputAnnotation
1081+ dumpInstance ist ctxt n = pp ist $ delabTy ist n
1082+ params = class_params ci
1083+ params' = zip params (repeat False)
1084+ pp ist = pprintPTerm (opt_showimp (idris_options ist)) params' []
10341085
10351086showTotal :: Totality -> IState -> String
10361087showTotal t@(Partial (Other ns)) i
@@ -1076,6 +1127,7 @@ parseArgs ("--typeintype":ns) = TypeInType : (parseArgs ns)
10761127parseArgs ("--total":ns) = DefaultTotal : (parseArgs ns)
10771128parseArgs ("--partial":ns) = DefaultPartial : (parseArgs ns)
10781129parseArgs ("--warnpartial":ns) = WarnPartial : (parseArgs ns)
1130+parseArgs ("--warnreach":ns) = WarnReach : (parseArgs ns)
10791131parseArgs ("--nocoverage":ns) = NoCoverage : (parseArgs ns)
10801132parseArgs ("--errorcontext":ns) = ErrContext : (parseArgs ns)
10811133parseArgs ("--help":ns) = Usage : (parseArgs ns)
@@ -1319,9 +1371,13 @@ idrisMain opts =
13191371
13201372 ok <- noErrors
13211373 when ok $ case output of
1322− [] -> return ()
1374+ -- just do the checks
1375+ [] -> performUsageAnalysis >> return ()
1376+
1377+ -- the compiler will run usage analysis itself
13231378 (o:_) -> idrisCatch (process stdout "" (Compile cgn o))
13241379 (\e -> do ist <- getIState ; iputStrLn $ pshow ist e)
1380+
13251381 case script of
13261382 Nothing -> return ()
13271383 Just expr -> execScript expr
@@ -1366,11 +1422,6 @@ execScript expr = do i <- getIState
13661422 res <- execute tm
13671423 runIO $ exitWith ExitSuccess
13681424
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−
13741425-- | Get the platform-specific, user-specific Idris dir
13751426getIdrisUserDataDir :: Idris FilePath
13761427getIdrisUserDataDir = 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)
2020import Idris.Core.TT
2121import Idris.REPL
2222import Idris.Parser (loadModule)
23−import Idris.Delaborate (pshow)
23+import Idris.Output (pshow)
2424import Idris.AbsSyntax
2525import Idris.IdrisDoc
2626import Idris.Output
test/basic001/reg005.idr+15−16
@@ -1,17 +1,22 @@
11module Main
22
3+%flag C "-g3 -ggdb -O0"
4+
35rep : (n : Nat) -> Char -> Vect n Char
46rep Z x = []
57rep (S k) x = x :: rep k x
68
79data RLE : Vect n Char -> Type where
810 REnd : RLE []
9− RChar : {xs : Vect k Char} ->
10− (n : Nat) -> (x : Char) -> RLE xs ->
11− RLE (rep (S n) x ++ xs)
11+ RChar : .{k : Nat}
12+ -> {xs : Vect k Char}
13+ -> (n : Nat)
14+ -> (x : Char)
15+ -> RLE xs
16+ -> RLE (rep (S n) x ++ xs)
1217
1318eq : (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
1520
1621------------
1722
@@ -32,20 +37,14 @@ compress xs with (rle xs)
3237 = let ni : Integer = cast (S n) in
3338 show ni ++ strCons x (compress xs)
3439
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+
3546compressString : String -> String
3647compressString xs = compress (fromList (unpack xs))
3748
3849main : IO ()
3950main = 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 @@
11module Main
22
33data Parity : Nat -> Type where
4− even : Parity (n + n)
5− odd : Parity (S (n + n))
4+ even : {n : Nat} -> Parity (n + n)
5+ odd : {n : Nat} -> Parity (S (n + n))
66
77parity : (n:Nat) -> Parity n
88parity Z = even {n=Z}
test/basic007/test033.idr+1−1
@@ -1,4 +1,4 @@
11module Main
22
33main : IO ()
4−main = nullPtr null >>= (putStrLn . show)
4+main = nullPtr null >>= print
test/proof003/Parity.idr+2−2
@@ -1,8 +1,8 @@
11module Parity
22
33data Parity : Nat -> Type where
4− even : Parity (n + n)
5− odd : Parity (S (n + n))
4+ even : {n : Nat} -> Parity (n + n)
5+ odd : {n : Nat} -> Parity (S (n + n))
66
77parity : (n:Nat) -> Parity n
88parity 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)
99data Board : Nat -> Type where
1010 MkBoard : {n : Nat} -> Vect n (Vect n (Cell n)) -> Board n
1111
12−emptyBoard : Board n
12+emptyBoard : {n : Nat} -> Board n
1313emptyBoard {n=n} = MkBoard (replicate n (replicate n Nothing))
1414
1515Empty : 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