git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2769 from lenary/annotate-prelude-with-used

Annotate the Prelude with %used for backends

commitc34329d3697ac045de9fb29e1c2555183d4d4e2c authorEdwin Brady <edwin.brady@gmail.com> dateMon 14 Dec 2015, 10:02 (11 years ago) parent10a22ebf59d80b
7 files changed+41−15
compare with master
unifiedsplit
libs/prelude/Builtins.idr+8 libs/prelude/Prelude/Either.idr+7−3 libs/prelude/Prelude/File.idr+5−1 libs/prelude/Prelude/List.idr+7−3 libs/prelude/Prelude/Maybe.idr+8−5 libs/prelude/Prelude/Stream.idr+4−1 test/quasiquote001/expected+2−2
libs/prelude/Builtins.idr+8
@@ -19,6 +19,10 @@ namespace Builtins
1919 ||| @b the right element of the pair
2020 MkPair : {A, B : Type} -> (a : A) -> (b : B) -> Pair A B
2121
22+ -- Usage hints for erasure analysis
23+ %used MkPair a
24+ %used MkPair b
25+
2226 ||| The non-dependent pair type, also known as conjunction, usable with
2327 ||| UniqueTypes.
2428 ||| @A the type of the left elements in the pair
@@ -29,6 +33,10 @@ namespace Builtins
2933 ||| @b the right element of the pair
3034 MkUPair : {A, B : AnyType} -> (a : A) -> (b : B) -> UPair A B
3135
36+ -- Usage hints for erasure analysis
37+ %used MkUPair a
38+ %used MkUPair b
39+
3240 ||| Dependent pairs
3341 |||
3442 ||| Dependent pairs represent existential quantification - they consist of a
libs/prelude/Prelude/Either.idr+7−3
@@ -9,11 +9,15 @@ import Prelude.Maybe
99import Prelude.List
1010
1111||| A sum type
12−%elim data Either a b =
12+%elim data Either : (a, b : Type) -> Type where
1313 ||| One possibility of the sum, conventionally used to represent errors
14− Left a |
14+ Left : (l : a) -> Either a b
1515 ||| The other possibility, conventionally used to represent success
16− Right b
16+ Right : (r : b) -> Either a b
17+
18+-- Usage hints for erasure analysis
19+%used Left l
20+%used Right r
1721
1822--------------------------------------------------------------------------------
1923-- Syntactic tests
libs/prelude/Prelude/File.idr+5−1
@@ -18,7 +18,11 @@ import IO
1818
1919||| A file handle
2020abstract
21−data File = FHandle Ptr
21+data File : Type where
22+ FHandle : (p : Ptr) -> File
23+
24+-- Usage hints for erasure analysis
25+%used FHandle p
2226
2327||| An error from a file operation
2428-- This is built in idris_mkFileError() in rts/idris_stdfgn.c. Make sure
libs/prelude/Prelude/List.idr+7−3
@@ -19,16 +19,20 @@ infix 5 \\
1919infixr 7 ::,++
2020
2121||| Generic lists
22−%elim data List elem =
22+%elim data List : (elem : Type) -> Type where
2323 ||| Empty list
24− Nil |
24+ Nil : List elem
2525 ||| A non-empty list, consisting of a head element and the rest of
2626 ||| the list.
27− (::) elem (List elem)
27+ (::) : (x : elem) -> (xs : List elem) -> List elem
2828
2929-- Name hints for interactive editing
3030%name List xs, ys, zs, ws
3131
32+-- Usage hints for erasure analysis
33+%used List.(::) x
34+%used List.(::) xs
35+
3236--------------------------------------------------------------------------------
3337-- Syntactic tests
3438--------------------------------------------------------------------------------
libs/prelude/Prelude/Maybe.idr+8−5
@@ -13,11 +13,14 @@ import Prelude.Foldable
1313
1414||| An optional value. This can be used to represent the possibility of
1515||| failure, where a function may return a value, or not.
16−data Maybe a
17− = ||| No value stored
18− Nothing
19− | ||| A value of type `a` is stored
20− Just a
16+data Maybe : (a : Type) -> Type where
17+ ||| No value stored
18+ Nothing : Maybe a
19+ ||| A value of type `a` is stored
20+ Just : (x : a) -> Maybe a
21+
22+-- Used hints for erasure analysis
23+%used Just x
2124
2225--------------------------------------------------------------------------------
2326-- Syntactic tests
libs/prelude/Prelude/Stream.idr+4−1
@@ -14,11 +14,14 @@ import Prelude.List
1414
1515||| An infinite stream
1616codata Stream : Type -> Type where
17− (::) : a -> Stream a -> Stream a
17+ (::) : (e : a) -> Stream a -> Stream a
1818
1919-- Hints for interactive editing
2020%name Stream xs,ys,zs,ws
2121
22+-- Usage hints for erasure analysis
23+%used Stream.(::) e
24+
2225instance Functor Stream where
2326 map f (x::xs) = f x :: map f xs
2427
test/quasiquote001/expected+2−2
@@ -1,5 +1,5 @@
1−App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar (-1)))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar (-1))))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar (-1)))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar (-1))))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 8 0) (UN "Unit") (TType (UVar (-1))))))
1+App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "x") (Pi (V 0) (TType (UVar (-1)))) (Bind (UN "xs") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar (-1))))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "x") (Pi (V 0) (TType (UVar (-1)))) (Bind (UN "xs") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar (-1))))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 8 0) (UN "Unit") (TType (UVar (-1))))))
22--------------
3−App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar (-1)))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 24))) (TType (UVar 25))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar (-1)))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 26))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "B") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "a") (Pi (V 1) (TType (UVar (-1)))) (Bind (UN "b") (Pi (V 1) (TType (UVar (-1)))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar (-1))))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar (-1)))))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 27))))
3+App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "x") (Pi (V 0) (TType (UVar (-1)))) (Bind (UN "xs") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 24))) (TType (UVar 25))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "x") (Pi (V 0) (TType (UVar (-1)))) (Bind (UN "xs") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 26))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "B") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "a") (Pi (V 1) (TType (UVar (-1)))) (Bind (UN "b") (Pi (V 1) (TType (UVar (-1)))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar (-1))))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar (-1)))))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 27))))
44--------------
55App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "B") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "a") (Pi (V 1) (TType (UVar (-1)))) (Bind (UN "b") (Pi (V 1) (TType (UVar (-1)))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "B") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "a") (Pi (V 1) (TType (UVar (-1)))) (Bind (UN "b") (Pi (V 1) (TType (UVar (-1)))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (TType (UVar 24))) (TType (UVar 24)))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "B") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "a") (Pi (V 1) (TType (UVar (-1)))) (Bind (UN "b") (Pi (V 1) (TType (UVar (-1)))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (TType (UVar 24))) (TType (UVar 24)))