git.iko.soy/Idris-dev
on master help sign in
Add documentation in new format for various libs
d53154aDavid Raymond Christiansen
libs/base/Data/ZZ.idr+1−1
compare with master
unifiedsplit
@@ -8,7 +8,7 @@ import Data.Sign
8
8
9
9
10||| An integer is either a positive nat or the negated successor of a nat.
10||| An integer is either a positive nat or the negated successor of a nat.
11−||| Zero is chosen to be positive.
11+||| Zero is arbitrarily chosen to be positive.
12data ZZ = Pos Nat | NegS Nat
12data ZZ = Pos Nat | NegS Nat
13
13
14instance Signed ZZ where
14instance Signed ZZ where
libs/base/Debug/Trace.idr+4−1
@@ -1,6 +1,9 @@
1module Debug.Trace
1module Debug.Trace
2
2
3+||| Print a message for debugging purposes as a side effect
4+||| @ msg what to print
5+||| @ result the final result
3−trace : String -> a -> a
6+trace : (msg : String) -> (result : a) -> a
4trace x val = unsafePerformIO (do putStrLn x; return val)
7trace x val = unsafePerformIO (do putStrLn x; return val)
5
8
6
9
libs/base/Decidable/Order.idr+1−1
@@ -21,7 +21,7 @@ class (Preorder t po) => Poset t (po : t -> t -> Type) where
21 total antisymmetric : (a : t) -> (b : t) -> po a b -> po b a -> a = b
21 total antisymmetric : (a : t) -> (b : t) -> po a b -> po b a -> a = b
22
22
23class (Poset t to) => Ordered t (to : t -> t -> Type) where
23class (Poset t to) => Ordered t (to : t -> t -> Type) where
24− total order : (a : t) -> (b : t) -> Either (to a b) (to b a)
24+ total order : (a : t) -> (b : t) -> Either (to a b) (to b a)
25
25
26minimum : (Ordered t to) => t -> t -> t
26minimum : (Ordered t to) => t -> t -> t
27minimum x y with (order x y)
27minimum x y with (order x y)
libs/base/Providers.idr+12−1
@@ -1,7 +1,18 @@
1module Providers
1module Providers
2
2
3+||| Type providers must build one of these in an IO computation.
3public
4public
4−data Provider a = Provide a | Error String | Postulate
5+data Provider : (a : Type) -> Type where
6+ ||| Return a term to be spliced in
7+ ||| @ x the term to be spliced (i.e. the proof)
8+ Provide : (x : a) -> Provider a
9+
10+ ||| Report an error to the user and stop compilation
11+ ||| @ msg the error message
12+ Error : (msg : String) -> Provider a
13+
14+ ||| Postulate the goal type
15+ Postulate : Provider a
5
16
6-- instances
17-- instances
7instance Functor Provider where
18instance Functor Provider where
libs/base/System.idr+9−6
@@ -5,6 +5,7 @@ import Prelude
5%default partial
5%default partial
6%access public
6%access public
7
7
8+||| Get the command-line arguments that the program was called with.
8getArgs : IO (List String)
9getArgs : IO (List String)
9getArgs = do n <- numArgs
10getArgs = do n <- numArgs
10 ga' [] 0 n
11 ga' [] 0 n
@@ -20,8 +21,8 @@ getArgs = do n <- numArgs
20 do arg <- getArg i
21 do arg <- getArg i
21 ga' (arg :: acc) (i+1) n
22 ga' (arg :: acc) (i+1) n
22
23
23−-- Retrieves an value from the environment, if the given key is present,
24+||| Retrieves an value from the environment, if the given key is present,
24−-- otherwise it returns Nothing.
25+||| otherwise it returns Nothing.
25getEnv : String -> IO (Maybe String)
26getEnv : String -> IO (Maybe String)
26getEnv key = do
27getEnv key = do
27 str_ptr <- getEnv'
28 str_ptr <- getEnv'
@@ -33,15 +34,15 @@ getEnv key = do
33 getEnv' : IO String
34 getEnv' : IO String
34 getEnv' = mkForeign (FFun "getenv" [FString] FString) key
35 getEnv' = mkForeign (FFun "getenv" [FString] FString) key
35
36
36−-- Sets an environment variable with a given value.
37+||| Sets an environment variable with a given value.
37−-- Returns true if the operation was successful.
38+||| Returns true if the operation was successful.
38setEnv : String -> String -> IO Bool
39setEnv : String -> String -> IO Bool
39setEnv key value = do
40setEnv key value = do
40 ok <- mkForeign (FFun "setenv" [FString, FString, FInt] FInt) key value 1
41 ok <- mkForeign (FFun "setenv" [FString, FString, FInt] FInt) key value 1
41 return (ok == 0)
42 return (ok == 0)
42
43
43−-- Unsets an environment variable.
44+||| Unsets an environment variable.
44−-- Returns true if the variable was able to be unset.
45+||| Returns true if the variable was able to be unset.
45unsetEnv : String -> IO Bool
46unsetEnv : String -> IO Bool
46unsetEnv key = do
47unsetEnv key = do
47 ok <- mkForeign (FFun "unsetenv" [FString] FInt) key
48 ok <- mkForeign (FFun "unsetenv" [FString] FInt) key
@@ -68,9 +69,11 @@ getEnvironment = getAllPairs 0 []
68 then return $ reverse $ map splitEq acc
69 then return $ reverse $ map splitEq acc
69 else getAllPairs (n + 1) (envPair :: acc)
70 else getAllPairs (n + 1) (envPair :: acc)
70
71
72+||| Quit with a particular exit code
71exit : Int -> IO ()
73exit : Int -> IO ()
72exit code = mkForeign (FFun "exit" [FInt] FUnit) code
74exit code = mkForeign (FFun "exit" [FInt] FUnit) code
73
75
76+||| Get the Unix time
74time : IO Int
77time : IO Int
75time = mkForeign (FFun "idris_time" [] FInt)
78time = mkForeign (FFun "idris_time" [] FInt)
76
79
libs/prelude/Builtins.idr+22−8
@@ -3,27 +3,35 @@
3%access public
3%access public
4%default total
4%default total
5
5
6+||| Dependent pairs, in their internal representation
7+||| @ a the type of the witness
8+||| @ P the type of the proof
6data Exists : (a : Type) -> (P : a -> Type) -> Type where
9data Exists : (a : Type) -> (P : a -> Type) -> Type where
7 Ex_intro : {P : a -> Type} -> (x : a) -> P x -> Exists a P
10 Ex_intro : {P : a -> Type} -> (x : a) -> P x -> Exists a P
8
11
12+||| The first projection from a dependent pair
9getWitness : {P : a -> Type} -> Exists a P -> a
13getWitness : {P : a -> Type} -> Exists a P -> a
10getWitness (a ** v) = a
14getWitness (a ** v) = a
11
15
16+||| The second projection from a dependent pair
12getProof : {P : a -> Type} -> (s : Exists a P) -> P (getWitness s)
17getProof : {P : a -> Type} -> (s : Exists a P) -> P (getWitness s)
13getProof (a ** v) = v
18getProof (a ** v) = v
14
19
15FalseElim : _|_ -> a
20FalseElim : _|_ -> a
16
21
17−-- For 'symbol syntax. 'foo becomes Symbol_ "foo"
22+||| For 'symbol syntax. 'foo becomes Symbol_ "foo"
18data Symbol_ : String -> Type where
23data Symbol_ : String -> Type where
19
24
20-- ------------------------------------------------------ [ For rewrite tactic ]
25-- ------------------------------------------------------ [ For rewrite tactic ]
26+||| Perform substitution in a term. This is used by the `rewrite` tactic and term.
21replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y
27replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y
22replace refl prf = prf
28replace refl prf = prf
23
29
30+||| Symmetry of propositional equality
24sym : {l:a} -> {r:a} -> l = r -> r = l
31sym : {l:a} -> {r:a} -> l = r -> r = l
25sym refl = refl
32sym refl = refl
26
33
34+||| Transitivity of propositional equality
27trans : {a:x} -> {b:x} -> {c:x} -> a = b -> b = c -> a = c
35trans : {a:x} -> {b:x} -> {c:x} -> a = b -> b = c -> a = c
28trans refl refl = refl
36trans refl refl = refl
29
37
@@ -48,21 +56,27 @@ malloc size x = x -- compiled specially
48trace_malloc : a -> a
56trace_malloc : a -> a
49trace_malloc x = x -- compiled specially
57trace_malloc x = x -- compiled specially
50
58
51−-- Assert to the totality checker than y is always structureally smaller than
59+||| Assert to the totality checker than y is always structurally smaller than
52−-- x (which is typically a pattern argument)
60+||| x (which is typically a pattern argument)
61+||| @ x the larger value (typically a pattern argument)
62+||| @ y the smaller value (typically an argument to a recursive call)
53−assert_smaller : a -> a -> a
63+assert_smaller : (x, y : a) -> a
54assert_smaller x y = y
64assert_smaller x y = y
55
65
56−-- Assert to the totality checker than the given expression will always
66+||| Assert to the totality checker than the given expression will always
57−-- terminate.
67+||| terminate.
58assert_total : a -> a
68assert_total : a -> a
59assert_total x = x
69assert_total x = x
60
70
71+||| Subvert the type checker. This function is abstract, so it will not reduce in
72+||| the type checker. Use it with care - it can result in segfaults or worse!
61abstract %assert_total -- need to pretend
73abstract %assert_total -- need to pretend
62−believe_me : a -> b -- compiled specially as id, use with care!
74+believe_me : a -> b
63believe_me x = prim__believe_me _ _ x
75believe_me x = prim__believe_me _ _ x
64
76
65−public %assert_total -- reduces at compile time, use with extreme care!
77+||| Subvert the type checker. This function *will* reduce in the type checker.
78+||| Use it with extreme care - it can result in segfaults or worse!
79+public %assert_total
66really_believe_me : a -> b
80really_believe_me : a -> b
67really_believe_me x = prim__believe_me _ _ x
81really_believe_me x = prim__believe_me _ _ x
68
82
libs/prelude/Prelude/Applicative.idr+3
@@ -19,12 +19,15 @@ infixl 2 $>
19($>) : Applicative f => f a -> f b -> f b
19($>) : Applicative f => f a -> f b -> f b
20a $> b = map (const id) a <$> b
20a $> b = map (const id) a <$> b
21
21
22+||| Lift a function to an applicative
22liftA : Applicative f => (a -> b) -> f a -> f b
23liftA : Applicative f => (a -> b) -> f a -> f b
23liftA f a = pure f <$> a
24liftA f a = pure f <$> a
24
25
26+||| Lift a two-argument function to an applicative
25liftA2 : Applicative f => (a -> b -> c) -> f a -> f b -> f c
27liftA2 : Applicative f => (a -> b -> c) -> f a -> f b -> f c
26liftA2 f a b = (map f a) <$> b
28liftA2 f a b = (map f a) <$> b
27
29
30+||| Lift a three-argument function to an applicative
28liftA3 : Applicative f => (a -> b -> c -> d) -> f a -> f b -> f c -> f d
31liftA3 : Applicative f => (a -> b -> c -> d) -> f a -> f b -> f c -> f d
29liftA3 f a b c = (map f a) <$> b <$> c
32liftA3 f a b c = (map f a) <$> b <$> c
30
33
libs/prelude/Prelude/Basics.idr+16−5
@@ -8,10 +8,12 @@ id : a -> a
8id x = x
8id x = x
9
9
10||| Manually assign a type to an expression.
10||| Manually assign a type to an expression.
11+||| @ a the type to assign
12+||| @ x the element to get the type
11−the : (a : Type) -> a -> a
13+the : (a : Type) -> (x : a) -> a
12the _ = id
14the _ = id
13
15
14−||| Constant function.
16+||| Constant function. Ignores its second argument.
15const : a -> b -> a
17const : a -> b -> a
16const x = \v => x
18const x = \v => x
17
19
@@ -30,17 +32,26 @@ infixl 9 .
30(.) f g x = f (g x)
32(.) f g x = f (g x)
31
33
32||| Takes in the first two arguments in reverse order.
34||| Takes in the first two arguments in reverse order.
35+||| @ f the function to flip
33−flip : (a -> b -> c) -> b -> a -> c
36+flip : (f : a -> b -> c) -> b -> a -> c
34flip f x y = f y x
37flip f x y = f y x
35
38
36||| Function application.
39||| Function application.
37apply : (a -> b) -> a -> b
40apply : (a -> b) -> a -> b
38apply f a = f a
41apply f a = f a
39
42
43+||| Equality is a congruence.
40cong : {f : t -> u} -> (a = b) -> f a = f b
44cong : {f : t -> u} -> (a = b) -> f a = f b
41cong refl = refl
45cong refl = refl
42
46
47+||| Decidability. A decidable property either holds or is a contradiction.
43data Dec : Type -> Type where
48data Dec : Type -> Type where
49+
50+ ||| The case where the property holds
51+ ||| @ prf the proof
44− Yes : {A : Type} -> A -> Dec A
52+ Yes : {A : Type} -> (prf : A) -> Dec A
53+
54+ ||| The case where the property holding would be a contradiction
55+ ||| @ contra a demonstration that A would be a contradiction
45− No : {A : Type} -> (A -> _|_) -> Dec A
56+ No : {A : Type} -> (contra : A -> _|_) -> Dec A
46
57
libs/prelude/Prelude/Bool.idr+5−2
@@ -3,8 +3,11 @@ module Prelude.Bool
3||| Boolean Data Type
3||| Boolean Data Type
4data Bool = False | True
4data Bool = False | True
5
5
6−||| Boolean elimination
6+||| The underlying implementation of the if ... then ... else ... syntax
7+||| @ b the condition on the if
8+||| @ t the value if b is true
9+||| @ e the falue if b is false
7−boolElim : Bool -> (t : Lazy a) -> (e : Lazy a) -> a
10+boolElim : (b : Bool) -> (t : Lazy a) -> (e : Lazy a) -> a
8boolElim True t e = t
11boolElim True t e = t
9boolElim False t e = e
12boolElim False t e = e
10
13
libs/prelude/Prelude/Chars.idr+1−1
@@ -66,4 +66,4 @@ isHexDigit x = elem (toUpper x) hexChars where
66isOctDigit : Char -> Bool
66isOctDigit : Char -> Bool
67isOctDigit x = (x >= '0' && x <= '7')
67isOctDigit x = (x >= '0' && x <= '7')
68
68
69−-- --------------------------------------------------------------------- [ EOF ]
69+
libs/prelude/Prelude/Either.idr+13−5
@@ -1,13 +1,16 @@
1−module Prelude.Either
1+ module Prelude.Either
2
2
3import Builtins
3import Builtins
4
4
5import Prelude.Maybe
5import Prelude.Maybe
6import Prelude.List
6import Prelude.List
7
7
8+||| A sum type
8−data Either a b
9+data Either a b =
10+ ||| One possibility of the sum, conventionally used to represent errors
9− = Left a
11+ Left a |
12+ ||| The other possibility, conventionally used to represent success
10− | Right b
13+ Right b
11
14
12--------------------------------------------------------------------------------
15--------------------------------------------------------------------------------
13-- Syntactic tests
16-- Syntactic tests
@@ -25,11 +28,16 @@ isRight (Right r) = True
25-- Misc.
28-- Misc.
26--------------------------------------------------------------------------------
29--------------------------------------------------------------------------------
27
30
31+||| Perform a case analysis on a Boolean, providing clients with a `so` proof
28choose : (b : Bool) -> Either (so b) (so (not b))
32choose : (b : Bool) -> Either (so b) (so (not b))
29choose True = Left oh
33choose True = Left oh
30choose False = Right oh
34choose False = Right oh
31
35
36+||| Simply-typed eliminator for Either
37+||| @ f the action to take on Left
38+||| @ g the action to take on Right
39+||| @ e the sum to analyze
32−either : (a -> c) -> (b -> c) -> Either a b -> c
40+either : (f : a -> c) -> (g : b -> c) -> (e : Either a b) -> c
33either l r (Left x) = l x
41either l r (Left x) = l x
34either l r (Right x) = r x
42either l r (Right x) = r x
35
43
libs/prelude/Prelude/Fin.idr+11−1
@@ -5,7 +5,9 @@ import Prelude.Either
5
5
6%default total
6%default total
7
7
8+||| Numbers strictly less than some bound. The name comes from "finite sets"
9+||| @ n the upper bound
8−data Fin : Nat -> Type where
10+data Fin : (n : Nat) -> Type where
9 fZ : Fin (S k)
11 fZ : Fin (S k)
10 fS : Fin k -> Fin (S k)
12 fS : Fin k -> Fin (S k)
11
13
@@ -44,14 +46,18 @@ finToInteger (fS k) = 1 + finToInteger k
44instance Cast (Fin n) Integer where
46instance Cast (Fin n) Integer where
45 cast x = finToInteger x
47 cast x = finToInteger x
46
48
49+||| Weaken the bound on a Fin by 1
47weaken : Fin n -> Fin (S n)
50weaken : Fin n -> Fin (S n)
48weaken fZ = fZ
51weaken fZ = fZ
49weaken (fS k) = fS (weaken k)
52weaken (fS k) = fS (weaken k)
50
53
54+||| Weaken the bound on a Fin by some amount
51weakenN : (n : Nat) -> Fin m -> Fin (m + n)
55weakenN : (n : Nat) -> Fin m -> Fin (m + n)
52weakenN n fZ = fZ
56weakenN n fZ = fZ
53weakenN n (fS f) = fS (weakenN n f)
57weakenN n (fS f) = fS (weakenN n f)
54
58
59+||| Attempt to tighten the bound on a Fin.
60+||| Return `Left` if the bound could not be tightened, or `Right` if it could.
55strengthen : Fin (S n) -> Either (Fin (S n)) (Fin n)
61strengthen : Fin (S n) -> Either (Fin (S n)) (Fin n)
56strengthen {n = S k} fZ = Right fZ
62strengthen {n = S k} fZ = Right fZ
57strengthen {n = S k} (fS i) with (strengthen i)
63strengthen {n = S k} (fS i) with (strengthen i)
@@ -59,10 +65,14 @@ strengthen {n = S k} (fS i) with (strengthen i)
59 strengthen (fS k) | Right x = Right (fS x)
65 strengthen (fS k) | Right x = Right (fS x)
60strengthen f = Left f
66strengthen f = Left f
61
67
68+||| Add some natural number to a Fin, extending the bound accordingly
69+||| @ n the previous bound
70+||| @ m the number to increase the Fin by
62shift : (m : Nat) -> Fin n -> Fin (m + n)
71shift : (m : Nat) -> Fin n -> Fin (m + n)
63shift Z f = f
72shift Z f = f
64shift {n=n} (S m) f = fS {k = (m + n)} (shift m f)
73shift {n=n} (S m) f = fS {k = (m + n)} (shift m f)
65
74
75+||| The largest element of some Fin type
66last : Fin (S n)
76last : Fin (S n)
67last {n=Z} = fZ
77last {n=Z} = fZ
68last {n=S _} = fS last
78last {n=S _} = fS last
libs/prelude/Prelude/Functor.idr+6−1
@@ -1,4 +1,9 @@
1module Prelude.Functor
1module Prelude.Functor
2
2
3+||| Functors
4+||| @ f the action of the functor on objects
3class Functor (f : Type -> Type) where
5class Functor (f : Type -> Type) where
6+ ||| The action of the functor on morphisms
7+ ||| @ f the functor
8+ ||| @ m the morphism
4− map : (a -> b) -> f a -> f b
9+ map : (m : a -> b) -> f a -> f b
libs/prelude/Prelude/Nat.idr+38−5
@@ -10,9 +10,12 @@ import Prelude.Classes
10%access public
10%access public
11%default total
11%default total
12
12
13+||| Unary natural numbers
13−%elim data Nat
14+%elim data Nat =
15+ ||| Zero
14− = Z
16+ Z |
17+ ||| Successor
15− | S Nat
18+ S Nat
16
19
17-- name hints for interactive editing
20-- name hints for interactive editing
18%name Nat k,j,i,n,m
21%name Nat k,j,i,n,m
@@ -33,14 +36,19 @@ isSucc (S n) = True
33-- Basic arithmetic functions
36-- Basic arithmetic functions
34--------------------------------------------------------------------------------
37--------------------------------------------------------------------------------
35
38
39+||| Add two natural numbers.
40+||| @ n the number to case-split on
41+||| @ m the other number
36−total plus : Nat -> Nat -> Nat
42+total plus : (n, m : Nat) -> Nat
37plus Z right = right
43plus Z right = right
38plus (S left) right = S (plus left right)
44plus (S left) right = S (plus left right)
39
45
46+||| Multiply natural numbers
40total mult : Nat -> Nat -> Nat
47total mult : Nat -> Nat -> Nat
41mult Z right = Z
48mult Z right = Z
42mult (S left) right = plus right $ mult left right
49mult (S left) right = plus right $ mult left right
43
50
51+||| Convert an Integer to a Nat, mapping negative numbers to 0
44fromIntegerNat : Integer -> Nat
52fromIntegerNat : Integer -> Nat
45fromIntegerNat 0 = Z
53fromIntegerNat 0 = Z
46fromIntegerNat n =
54fromIntegerNat n =
@@ -49,15 +57,18 @@ fromIntegerNat n =
49 else
57 else
50 Z
58 Z
51
59
60+||| Convert a Nat to an Integer
52toIntegerNat : Nat -> Integer
61toIntegerNat : Nat -> Integer
53toIntegerNat Z = 0
62toIntegerNat Z = 0
54toIntegerNat (S k) = 1 + toIntegerNat k
63toIntegerNat (S k) = 1 + toIntegerNat k
55
64
65+||| Subtract natural numbers. If the second number is larger than the first, return 0.
56total minus : Nat -> Nat -> Nat
66total minus : Nat -> Nat -> Nat
57minus Z right = Z
67minus Z right = Z
58minus left Z = left
68minus left Z = left
59minus (S left) (S right) = minus left right
69minus (S left) (S right) = minus left right
60
70
71+||| Exponentiation of natural numbers
61total power : Nat -> Nat -> Nat
72total power : Nat -> Nat -> Nat
62power base Z = S Z
73power base Z = S Z
63power base (S exp) = mult base $ power base exp
74power base (S exp) = mult base $ power base exp
@@ -74,33 +85,46 @@ hyper (S pn) a (S pb) = hyper pn a (hyper (S pn) a pb)
74-- Comparisons
85-- Comparisons
75--------------------------------------------------------------------------------
86--------------------------------------------------------------------------------
76
87
88+||| Proofs that `n` is less than or equal to `m`
89+||| @ n the smaller number
90+||| @ m the larger number
77−data LTE : Nat -> Nat -> Type where
91+data LTE : (n, m : Nat) -> Type where
92+ ||| Zero is the smallest Nat
78 lteZero : LTE Z right
93 lteZero : LTE Z right
94+ ||| If n <= m, then n + 1 <= m + 1
79 lteSucc : LTE left right -> LTE (S left) (S right)
95 lteSucc : LTE left right -> LTE (S left) (S right)
80
96
97+||| Greater than or equal to
81total GTE : Nat -> Nat -> Type
98total GTE : Nat -> Nat -> Type
82GTE left right = LTE right left
99GTE left right = LTE right left
83
100
101+||| Strict less than
84total LT : Nat -> Nat -> Type
102total LT : Nat -> Nat -> Type
85LT left right = LTE (S left) right
103LT left right = LTE (S left) right
86
104
105+||| Strict greater than
87total GT : Nat -> Nat -> Type
106total GT : Nat -> Nat -> Type
88GT left right = LT right left
107GT left right = LT right left
89
108
109+||| Boolean test than one Nat is less than or equal to another
90total lte : Nat -> Nat -> Bool
110total lte : Nat -> Nat -> Bool
91lte Z right = True
111lte Z right = True
92lte left Z = False
112lte left Z = False
93lte (S left) (S right) = lte left right
113lte (S left) (S right) = lte left right
94
114
115+||| Boolean test than one Nat is greater than or equal to another
95total gte : Nat -> Nat -> Bool
116total gte : Nat -> Nat -> Bool
96gte left right = lte right left
117gte left right = lte right left
97
118
119+||| Boolean test than one Nat is strictly less than another
98total lt : Nat -> Nat -> Bool
120total lt : Nat -> Nat -> Bool
99lt left right = lte (S left) right
121lt left right = lte (S left) right
100
122
123+||| Boolean test than one Nat is strictly greater than another
101total gt : Nat -> Nat -> Bool
124total gt : Nat -> Nat -> Bool
102gt left right = lt right left
125gt left right = lt right left
103
126
127+||| Find the least of two natural numbers
104total minimum : Nat -> Nat -> Nat
128total minimum : Nat -> Nat -> Nat
105minimum left right =
129minimum left right =
106 if lte left right then
130 if lte left right then
@@ -108,6 +132,7 @@ minimum left right =
108 else
132 else
109 right
133 right
110
134
135+||| Find the greatest of two natural numbers
111total maximum : Nat -> Nat -> Nat
136total maximum : Nat -> Nat -> Nat
112maximum left right =
137maximum left right =
113 if lte left right then
138 if lte left right then
@@ -148,9 +173,11 @@ instance MinBound Nat where
148instance Cast Integer Nat where
173instance Cast Integer Nat where
149 cast = fromInteger
174 cast = fromInteger
150
175
176+||| A wrapper for Nat that specifies the semigroup and monad instances that use (+)
151record Multiplicative : Type where
177record Multiplicative : Type where
152 getMultiplicative : Nat -> Multiplicative
178 getMultiplicative : Nat -> Multiplicative
153
179
180+||| A wrapper for Nat that specifies the semigroup and monad instances that use (*)
154record Additive : Type where
181record Additive : Type where
155 getAdditive : Nat -> Additive
182 getAdditive : Nat -> Additive
156
183
@@ -210,6 +237,7 @@ instance Cast Nat Int where
210-- Auxilliary notions
237-- Auxilliary notions
211--------------------------------------------------------------------------------
238--------------------------------------------------------------------------------
212
239
240+||| The predecessor of a natural number. `pred Z` is `Z`.
213total pred : Nat -> Nat
241total pred : Nat -> Nat
214pred Z = Z
242pred Z = Z
215pred (S n) = n
243pred (S n) = n
@@ -218,11 +246,13 @@ pred (S n) = n
218-- Fibonacci and factorial
246-- Fibonacci and factorial
219--------------------------------------------------------------------------------
247--------------------------------------------------------------------------------
220
248
249+||| Fibonacci numbers
221total fib : Nat -> Nat
250total fib : Nat -> Nat
222fib Z = Z
251fib Z = Z
223fib (S Z) = S Z
252fib (S Z) = S Z
224fib (S (S n)) = fib (S n) + fib n
253fib (S (S n)) = fib (S n) + fib n
225
254
255+||| Factorial function
226total fact : Nat -> Nat
256total fact : Nat -> Nat
227fact Z = S Z
257fact Z = S Z
228fact (S n) = (S n) * fact n
258fact (S n) = (S n) * fact n
@@ -283,10 +313,13 @@ lcm x y = divNat (x * y) (gcd x y)
283--------------------------------------------------------------------------------
313--------------------------------------------------------------------------------
284
314
285-- Succ
315-- Succ
316+
317+||| S preserves equality
286total eqSucc : (left : Nat) -> (right : Nat) -> (p : left = right) ->
318total eqSucc : (left : Nat) -> (right : Nat) -> (p : left = right) ->
287 S left = S right
319 S left = S right
288eqSucc left _ refl = refl
320eqSucc left _ refl = refl
289
321
322+||| S is injective
290total succInjective : (left : Nat) -> (right : Nat) -> (p : S left = S right) ->
323total succInjective : (left : Nat) -> (right : Nat) -> (p : S left = S right) ->
291 left = right
324 left = right
292succInjective left _ refl = refl
325succInjective left _ refl = refl
libs/prelude/Prelude/Stream.idr+19−4
@@ -6,46 +6,61 @@ import Prelude.Vect
6%access public
6%access public
7%default total
7%default total
8
8
9+||| An infinite stream
9codata Stream : Type -> Type where
10codata Stream : Type -> Type where
10 (::) : a -> Stream a -> Stream a
11 (::) : a -> Stream a -> Stream a
11
12
12instance Functor Stream where
13instance Functor Stream where
13 map f (x::xs) = f x :: map f xs
14 map f (x::xs) = f x :: map f xs
14
15
16+||| The first element of an infinite stream
15head : Stream a -> a
17head : Stream a -> a
16head (x::xs) = x
18head (x::xs) = x
17
19
20+||| All but the first element
18tail : Stream a -> Stream a
21tail : Stream a -> Stream a
19tail (x::xs) = xs
22tail (x::xs) = xs
20
23
24+||| Take precisely n elements from the stream
25+||| @ n how many elements to take
26+||| @ xs the stream
21−take : (n : Nat) -> Stream a -> Vect n a
27+take : (n : Nat) -> (xs : Stream a) -> Vect n a
22take Z _ = []
28take Z _ = []
23take (S n) (x :: xs) = x :: (take n xs)
29take (S n) (x :: xs) = x :: (take n xs)
24
30
25%assert_total
31%assert_total
26drop : Nat -> Stream a -> Stream a
32drop : Nat -> Stream a -> Stream a
27−drop Z xs = xs
33+drop Z xs = xs
28drop (S k) (x::xs) = drop k xs
34drop (S k) (x::xs) = drop k xs
29
35
36+||| An infinite stream of repetitions of the same thing
30repeat : a -> Stream a
37repeat : a -> Stream a
31repeat x = x :: repeat x
38repeat x = x :: repeat x
32
39
40+||| Generate an infinite stream by repeatedly applying a function
41+||| @ f the function to iterate
42+||| @ x the initial value that will be the head of the stream
33−iterate : (a -> a) -> a -> Stream a
43+iterate : (f : a -> a) -> (x : a) -> Stream a
34iterate f x = x :: iterate f (f x)
44iterate f x = x :: iterate f (f x)
35
45
46+||| Get the nth element of a stream
36index : Nat -> Stream a -> a
47index : Nat -> Stream a -> a
37−index Z (x::xs) = x
48+index Z (x::xs) = x
38index (S k) (x::xs) = index k xs
49index (S k) (x::xs) = index k xs
39
50
51+||| Combine two streams element-wise using a function
40zipWith : (a -> b -> c) -> Stream a -> Stream b -> Stream c
52zipWith : (a -> b -> c) -> Stream a -> Stream b -> Stream c
41zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
53zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
42
54
55+||| Create a stream of pairs from two streams
43zip : Stream a -> Stream b -> Stream (a, b)
56zip : Stream a -> Stream b -> Stream (a, b)
44zip = zipWith (\x,y => (x,y))
57zip = zipWith (\x,y => (x,y))
45
58
59+||| Create a pair of streams from a stream of pairs
46unzip : Stream (a, b) -> (Stream a, Stream b)
60unzip : Stream (a, b) -> (Stream a, Stream b)
47unzip xs = (map fst xs, map snd xs)
61unzip xs = (map fst xs, map snd xs)
48
62
63+||| Return the diagonal elements of a stream of streams
49diag : Stream (Stream a) -> Stream a
64diag : Stream (Stream a) -> Stream a
50diag ((x::xs)::xss) = x :: diag (map tail xss)
65diag ((x::xs)::xss) = x :: diag (map tail xss)
51
66
libs/prelude/Prelude/Uninhabited.idr+8−2
@@ -1,6 +1,9 @@
1module Prelude.Uninhabited
1module Prelude.Uninhabited
2
2
3+||| A canonical proof that some type is empty
3class Uninhabited t where
4class Uninhabited t where
5+ ||| If I have a t, I've had a contradiction
6+ ||| @ t the uninhabited type
4 total uninhabited : t -> _|_
7 total uninhabited : t -> _|_
5
8
6instance Uninhabited (Fin Z) where
9instance Uninhabited (Fin Z) where
@@ -11,5 +14,8 @@ instance Uninhabited (Z = S n) where
11 uninhabited refl impossible
14 uninhabited refl impossible
12
15
13||| Use an absurd assumption to discharge a proof obligation
16||| Use an absurd assumption to discharge a proof obligation
17+||| @ t some empty type
18+||| @ a the goal type
19+||| @ h the contradictory hypothesis
14−absurd : Uninhabited t => t -> a
20+absurd : Uninhabited t => (h : t) -> a
15−absurd t = FalseElim (uninhabited t)
21+absurd h = FalseElim (uninhabited h)