git.iko.soy/Idris-dev
on master help sign in
Annotate the Prelude with %used for backends
commitb257e4bfab04f0c38efd493cd40ee78677a40081 authorSam Elliott <ashe2@cs.washington.edu> dateMon 26 Oct 2015, 15:14 (11 years ago) parentd2f892b
6 files changed+39−13
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
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
@@ -17,7 +17,11 @@ import IO
1717
1818||| A file handle
1919abstract
20−data File = FHandle Ptr
20+data File : Type where
21+ FHandle : (p : Ptr) -> File
22+
23+-- Usage hints for erasure analysis
24+%used FHandle p
2125
2226||| Standard input
2327stdin : File
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