git.iko.soy/Idris-dev
on master help sign in
Annotate the Prelude with %used for backends
b257e4bSam Elliott
libs/prelude/Builtins.idr+8
compare with master
unifiedsplit
@@ -19,6 +19,10 @@ namespace Builtins
19 ||| @b the right element of the pair
19 ||| @b the right element of the pair
20 MkPair : {A, B : Type} -> (a : A) -> (b : B) -> Pair A B
20 MkPair : {A, B : Type} -> (a : A) -> (b : B) -> Pair A B
21
21
22+ -- Usage hints for erasure analysis
23+ %used MkPair a
24+ %used MkPair b
25+
22 ||| The non-dependent pair type, also known as conjunction, usable with
26 ||| The non-dependent pair type, also known as conjunction, usable with
23 ||| UniqueTypes.
27 ||| UniqueTypes.
24 ||| @A the type of the left elements in the pair
28 ||| @A the type of the left elements in the pair
@@ -29,6 +33,10 @@ namespace Builtins
29 ||| @b the right element of the pair
33 ||| @b the right element of the pair
30 MkUPair : {A, B : AnyType} -> (a : A) -> (b : B) -> UPair A B
34 MkUPair : {A, B : AnyType} -> (a : A) -> (b : B) -> UPair A B
31
35
36+ -- Usage hints for erasure analysis
37+ %used MkUPair a
38+ %used MkUPair b
39+
32 ||| Dependent pairs
40 ||| Dependent pairs
33 |||
41 |||
34 ||| Dependent pairs represent existential quantification - they consist of a
42 ||| Dependent pairs represent existential quantification - they consist of a
libs/prelude/Prelude/Either.idr+7−3
@@ -9,11 +9,15 @@ import Prelude.Maybe
9import Prelude.List
9import Prelude.List
10
10
11||| A sum type
11||| A sum type
12−%elim data Either a b =
12+%elim data Either : (a, b : Type) -> Type where
13 ||| One possibility of the sum, conventionally used to represent errors
13 ||| One possibility of the sum, conventionally used to represent errors
14− Left a |
14+ Left : (l : a) -> Either a b
15 ||| The other possibility, conventionally used to represent success
15 ||| 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
17
21
18--------------------------------------------------------------------------------
22--------------------------------------------------------------------------------
19-- Syntactic tests
23-- Syntactic tests
libs/prelude/Prelude/File.idr+5−1
@@ -17,7 +17,11 @@ import IO
17
17
18||| A file handle
18||| A file handle
19abstract
19abstract
20+data File : Type where
20−data File = FHandle Ptr
21+ FHandle : (p : Ptr) -> File
22+
23+-- Usage hints for erasure analysis
24+%used FHandle p
21
25
22||| Standard input
26||| Standard input
23stdin : File
27stdin : File
libs/prelude/Prelude/List.idr+7−3
@@ -19,16 +19,20 @@ infix 5 \\
19infixr 7 ::,++
19infixr 7 ::,++
20
20
21||| Generic lists
21||| Generic lists
22−%elim data List elem =
22+%elim data List : (elem : Type) -> Type where
23 ||| Empty list
23 ||| Empty list
24− Nil |
24+ Nil : List elem
25 ||| A non-empty list, consisting of a head element and the rest of
25 ||| A non-empty list, consisting of a head element and the rest of
26 ||| the list.
26 ||| the list.
27− (::) elem (List elem)
27+ (::) : (x : elem) -> (xs : List elem) -> List elem
28
28
29-- Name hints for interactive editing
29-- Name hints for interactive editing
30%name List xs, ys, zs, ws
30%name List xs, ys, zs, ws
31
31
32+-- Usage hints for erasure analysis
33+%used List.(::) x
34+%used List.(::) xs
35+
32--------------------------------------------------------------------------------
36--------------------------------------------------------------------------------
33-- Syntactic tests
37-- Syntactic tests
34--------------------------------------------------------------------------------
38--------------------------------------------------------------------------------
libs/prelude/Prelude/Maybe.idr+8−5
@@ -13,11 +13,14 @@ import Prelude.Foldable
13
13
14||| An optional value. This can be used to represent the possibility of
14||| An optional value. This can be used to represent the possibility of
15||| failure, where a function may return a value, or not.
15||| failure, where a function may return a value, or not.
16−data Maybe a
16+data Maybe : (a : Type) -> Type where
17− = ||| No value stored
17+ ||| No value stored
18− Nothing
18+ Nothing : Maybe a
19− | ||| A value of type `a` is stored
19+ ||| A value of type `a` is stored
20− Just a
20+ Just : (x : a) -> Maybe a
21+
22+-- Used hints for erasure analysis
23+%used Just x
21
24
22--------------------------------------------------------------------------------
25--------------------------------------------------------------------------------
23-- Syntactic tests
26-- Syntactic tests
libs/prelude/Prelude/Stream.idr+4−1
@@ -14,11 +14,14 @@ import Prelude.List
14
14
15||| An infinite stream
15||| An infinite stream
16codata Stream : Type -> Type where
16codata Stream : Type -> Type where
17− (::) : a -> Stream a -> Stream a
17+ (::) : (e : a) -> Stream a -> Stream a
18
18
19-- Hints for interactive editing
19-- Hints for interactive editing
20%name Stream xs,ys,zs,ws
20%name Stream xs,ys,zs,ws
21
21
22+-- Usage hints for erasure analysis
23+%used Stream.(::) e
24+
22instance Functor Stream where
25instance Functor Stream where
23 map f (x::xs) = f x :: map f xs
26 map f (x::xs) = f x :: map f xs
24
27