d53154a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add documentation in new format for various libs

commitd53154a87d6342f9d44f5ac7cc88c09734d27a5a authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 3 Mar 2014, 13:29 (13 years ago) parentdc6b9cb

16 files changed+169−44

compare with master

unifiedsplit

libs/base/Data/ZZ.idr+1−1

@@ -8,7 +8,7 @@ import Data.Sign

1010||| 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.

1212data ZZ = Pos Nat | NegS Nat

1313

1414instance Signed ZZ where

libs/base/Debug/Trace.idr+4−1

@@ -1,6 +1,9 @@

11module Debug.Trace

3−trace : String -> a -> a

3+||| Print a message for debugging purposes as a side effect

4+||| @ msg what to print

5+||| @ result the final result

6+trace : (msg : String) -> (result : a) -> a

47trace x val = unsafePerformIO (do putStrLn x; return val)

libs/base/Decidable/Order.idr+1−1

@@ -21,7 +21,7 @@ class (Preorder t po) => Poset t (po : t -> t -> Type) where

2121 total antisymmetric : (a : t) -> (b : t) -> po a b -> po b a -> a = b

2222

2323class (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)

2525

2626minimum : (Ordered t to) => t -> t -> t

2727minimum x y with (order x y)

libs/base/Providers.idr+12−1

@@ -1,7 +1,18 @@

11module Providers

3+||| Type providers must build one of these in an IO computation.

34public

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

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

516

617-- instances

718instance Functor Provider where

libs/base/System.idr+9−6

@@ -5,6 +5,7 @@ import Prelude

55%default partial

66%access public

8+||| Get the command-line arguments that the program was called with.

89getArgs : IO (List String)

910getArgs = do n <- numArgs

1011 ga' [] 0 n

@@ -20,8 +21,8 @@ getArgs = do n <- numArgs

2021 do arg <- getArg i

2122 ga' (arg :: acc) (i+1) n

2223

23−-- Retrieves an value from the environment, if the given key is present,

24−-- otherwise it returns Nothing.

24+||| Retrieves an value from the environment, if the given key is present,

25+||| otherwise it returns Nothing.

2526getEnv : String -> IO (Maybe String)

2627getEnv key = do

2728 str_ptr <- getEnv'

@@ -33,15 +34,15 @@ getEnv key = do

3334 getEnv' : IO String

3435 getEnv' = mkForeign (FFun "getenv" [FString] FString) key

3536

36−-- Sets an environment variable with a given value.

37−-- Returns true if the operation was successful.

37+||| Sets an environment variable with a given value.

38+||| Returns true if the operation was successful.

3839setEnv : String -> String -> IO Bool

3940setEnv key value = do

4041 ok <- mkForeign (FFun "setenv" [FString, FString, FInt] FInt) key value 1

4142 return (ok == 0)

4243

43−-- Unsets an environment variable.

44−-- Returns true if the variable was able to be unset.

44+||| Unsets an environment variable.

45+||| Returns true if the variable was able to be unset.

4546unsetEnv : String -> IO Bool

4647unsetEnv key = do

4748 ok <- mkForeign (FFun "unsetenv" [FString] FInt) key

@@ -68,9 +69,11 @@ getEnvironment = getAllPairs 0 []

6869 then return $ reverse $ map splitEq acc

6970 else getAllPairs (n + 1) (envPair :: acc)

7071

72+||| Quit with a particular exit code

7173exit : Int -> IO ()

7274exit code = mkForeign (FFun "exit" [FInt] FUnit) code

7375

76+||| Get the Unix time

7477time : IO Int

7578time = mkForeign (FFun "idris_time" [] FInt)

7679

libs/prelude/Builtins.idr+22−8

@@ -3,27 +3,35 @@

33%access public

44%default total

6+||| Dependent pairs, in their internal representation

7+||| @ a the type of the witness

8+||| @ P the type of the proof

69data Exists : (a : Type) -> (P : a -> Type) -> Type where

710 Ex_intro : {P : a -> Type} -> (x : a) -> P x -> Exists a P

811

12+||| The first projection from a dependent pair

913getWitness : {P : a -> Type} -> Exists a P -> a

1014getWitness (a ** v) = a

1115

16+||| The second projection from a dependent pair

1217getProof : {P : a -> Type} -> (s : Exists a P) -> P (getWitness s)

1318getProof (a ** v) = v

1419

1520FalseElim : _|_ -> a

1621

17−-- For 'symbol syntax. 'foo becomes Symbol_ "foo"

22+||| For 'symbol syntax. 'foo becomes Symbol_ "foo"

1823data Symbol_ : String -> Type where

1924

2025-- ------------------------------------------------------ [ For rewrite tactic ]

26+||| Perform substitution in a term. This is used by the `rewrite` tactic and term.

2127replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y

2228replace refl prf = prf

2329

30+||| Symmetry of propositional equality

2431sym : {l:a} -> {r:a} -> l = r -> r = l

2532sym refl = refl

2633

34+||| Transitivity of propositional equality

2735trans : {a:x} -> {b:x} -> {c:x} -> a = b -> b = c -> a = c

2836trans refl refl = refl

2937

@@ -48,21 +56,27 @@ malloc size x = x -- compiled specially

4856trace_malloc : a -> a

4957trace_malloc x = x -- compiled specially

5058

51−-- Assert to the totality checker than y is always structureally smaller than

52−-- x (which is typically a pattern argument)

53−assert_smaller : a -> a -> a

59+||| Assert to the totality checker than y is always structurally smaller than

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)

63+assert_smaller : (x, y : a) -> a

5464assert_smaller x y = y

5565

56−-- Assert to the totality checker than the given expression will always

57−-- terminate.

66+||| Assert to the totality checker than the given expression will always

67+||| terminate.

5868assert_total : a -> a

5969assert_total x = x

6070

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!

6173abstract %assert_total -- need to pretend

62−believe_me : a -> b -- compiled specially as id, use with care!

74+believe_me : a -> b

6375believe_me x = prim__believe_me _ _ x

6476

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

6680really_believe_me : a -> b

6781really_believe_me x = prim__believe_me _ _ x

6882

libs/prelude/Prelude/Applicative.idr+3

@@ -19,12 +19,15 @@ infixl 2 $>

1919($>) : Applicative f => f a -> f b -> f b

2020a $> b = map (const id) a <$> b

2121

22+||| Lift a function to an applicative

2223liftA : Applicative f => (a -> b) -> f a -> f b

2324liftA f a = pure f <$> a

2425

26+||| Lift a two-argument function to an applicative

2527liftA2 : Applicative f => (a -> b -> c) -> f a -> f b -> f c

2628liftA2 f a b = (map f a) <$> b

2729

30+||| Lift a three-argument function to an applicative

2831liftA3 : Applicative f => (a -> b -> c -> d) -> f a -> f b -> f c -> f d

2932liftA3 f a b c = (map f a) <$> b <$> c

3033

libs/prelude/Prelude/Basics.idr+16−5

@@ -8,10 +8,12 @@ id : a -> a

88id x = x

1010||| Manually assign a type to an expression.

11−the : (a : Type) -> a -> a

11+||| @ a the type to assign

12+||| @ x the element to get the type

13+the : (a : Type) -> (x : a) -> a

1214the _ = id

1315

14−||| Constant function.

16+||| Constant function. Ignores its second argument.

1517const : a -> b -> a

1618const x = \v => x

1719

@@ -30,17 +32,26 @@ infixl 9 .

3032(.) f g x = f (g x)

3133

3234||| Takes in the first two arguments in reverse order.

33−flip : (a -> b -> c) -> b -> a -> c

35+||| @ f the function to flip

36+flip : (f : a -> b -> c) -> b -> a -> c

3437flip f x y = f y x

3538

3639||| Function application.

3740apply : (a -> b) -> a -> b

3841apply f a = f a

3942

43+||| Equality is a congruence.

4044cong : {f : t -> u} -> (a = b) -> f a = f b

4145cong refl = refl

4246

47+||| Decidability. A decidable property either holds or is a contradiction.

4348data Dec : Type -> Type where

44− Yes : {A : Type} -> A -> Dec A

45− No : {A : Type} -> (A -> _|_) -> Dec A

49+

50+ ||| The case where the property holds

51+ ||| @ prf the proof

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

56+ No : {A : Type} -> (contra : A -> _|_) -> Dec A

4657

libs/prelude/Prelude/Bool.idr+5−2

@@ -3,8 +3,11 @@ module Prelude.Bool

33||| Boolean Data Type

44data Bool = False | True

6−||| Boolean elimination

7−boolElim : Bool -> (t : Lazy a) -> (e : Lazy a) -> a

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

10+boolElim : (b : Bool) -> (t : Lazy a) -> (e : Lazy a) -> a

811boolElim True t e = t

912boolElim False t e = e

1013

libs/prelude/Prelude/Chars.idr+1−1

@@ -66,4 +66,4 @@ isHexDigit x = elem (toUpper x) hexChars where

6666isOctDigit : Char -> Bool

6767isOctDigit x = (x >= '0' && x <= '7')

6868

69−-- --------------------------------------------------------------------- [ EOF ]

69+

libs/prelude/Prelude/Either.idr+13−5

@@ -1,13 +1,16 @@

1−module Prelude.Either

1+ module Prelude.Either

33import Builtins

55import Prelude.Maybe

66import Prelude.List

8−data Either a b

9− = Left a

10− | Right b

8+||| A sum type

9+data Either a b =

10+ ||| One possibility of the sum, conventionally used to represent errors

11+ Left a |

12+ ||| The other possibility, conventionally used to represent success

13+ Right b

1114

1215--------------------------------------------------------------------------------

1316-- Syntactic tests

@@ -25,11 +28,16 @@ isRight (Right r) = True

2528-- Misc.

2629--------------------------------------------------------------------------------

2730

31+||| Perform a case analysis on a Boolean, providing clients with a `so` proof

2832choose : (b : Bool) -> Either (so b) (so (not b))

2933choose True = Left oh

3034choose False = Right oh

3135

32−either : (a -> c) -> (b -> c) -> Either a b -> c

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

40+either : (f : a -> c) -> (g : b -> c) -> (e : Either a b) -> c

3341either l r (Left x) = l x

3442either l r (Right x) = r x

3543

libs/prelude/Prelude/Fin.idr+11−1

@@ -5,7 +5,9 @@ import Prelude.Either

66%default total

8−data Fin : Nat -> Type where

8+||| Numbers strictly less than some bound. The name comes from "finite sets"

9+||| @ n the upper bound

10+data Fin : (n : Nat) -> Type where

911 fZ : Fin (S k)

1012 fS : Fin k -> Fin (S k)

1113

@@ -44,14 +46,18 @@ finToInteger (fS k) = 1 + finToInteger k

4446instance Cast (Fin n) Integer where

4547 cast x = finToInteger x

4648

49+||| Weaken the bound on a Fin by 1

4750weaken : Fin n -> Fin (S n)

4851weaken fZ = fZ

4952weaken (fS k) = fS (weaken k)

5053

54+||| Weaken the bound on a Fin by some amount

5155weakenN : (n : Nat) -> Fin m -> Fin (m + n)

5256weakenN n fZ = fZ

5357weakenN n (fS f) = fS (weakenN n f)

5458

59+||| Attempt to tighten the bound on a Fin.

60+||| Return `Left` if the bound could not be tightened, or `Right` if it could.

5561strengthen : Fin (S n) -> Either (Fin (S n)) (Fin n)

5662strengthen {n = S k} fZ = Right fZ

5763strengthen {n = S k} (fS i) with (strengthen i)

@@ -59,10 +65,14 @@ strengthen {n = S k} (fS i) with (strengthen i)

5965 strengthen (fS k) | Right x = Right (fS x)

6066strengthen f = Left f

6167

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

6271shift : (m : Nat) -> Fin n -> Fin (m + n)

6372shift Z f = f

6473shift {n=n} (S m) f = fS {k = (m + n)} (shift m f)

6574

75+||| The largest element of some Fin type

6676last : Fin (S n)

6777last {n=Z} = fZ

6878last {n=S _} = fS last

libs/prelude/Prelude/Functor.idr+6−1

@@ -1,4 +1,9 @@

11module Prelude.Functor

3+||| Functors

4+||| @ f the action of the functor on objects

35class Functor (f : Type -> Type) where

4− map : (a -> b) -> f a -> f b

6+ ||| The action of the functor on morphisms

7+ ||| @ f the functor

8+ ||| @ m the morphism

9+ map : (m : a -> b) -> f a -> f b

libs/prelude/Prelude/Nat.idr+38−5

@@ -10,9 +10,12 @@ import Prelude.Classes

1010%access public

1111%default total

1212

13−%elim data Nat

14− = Z

15− | S Nat

13+||| Unary natural numbers

14+%elim data Nat =

15+ ||| Zero

16+ Z |

17+ ||| Successor

18+ S Nat

1619

1720-- name hints for interactive editing

1821%name Nat k,j,i,n,m

@@ -33,14 +36,19 @@ isSucc (S n) = True

3336-- Basic arithmetic functions

3437--------------------------------------------------------------------------------

3538

36−total plus : Nat -> Nat -> Nat

39+||| Add two natural numbers.

40+||| @ n the number to case-split on

41+||| @ m the other number

42+total plus : (n, m : Nat) -> Nat

3743plus Z right = right

3844plus (S left) right = S (plus left right)

3945

46+||| Multiply natural numbers

4047total mult : Nat -> Nat -> Nat

4148mult Z right = Z

4249mult (S left) right = plus right $ mult left right

4350

51+||| Convert an Integer to a Nat, mapping negative numbers to 0

4452fromIntegerNat : Integer -> Nat

4553fromIntegerNat 0 = Z

4654fromIntegerNat n =

@@ -49,15 +57,18 @@ fromIntegerNat n =

4957 else

5058 Z

5159

60+||| Convert a Nat to an Integer

5261toIntegerNat : Nat -> Integer

5362toIntegerNat Z = 0

5463toIntegerNat (S k) = 1 + toIntegerNat k

5564

65+||| Subtract natural numbers. If the second number is larger than the first, return 0.

5666total minus : Nat -> Nat -> Nat

5767minus Z right = Z

5868minus left Z = left

5969minus (S left) (S right) = minus left right

6070

71+||| Exponentiation of natural numbers

6172total power : Nat -> Nat -> Nat

6273power base Z = S Z

6374power 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)

7485-- Comparisons

7586--------------------------------------------------------------------------------

7687

77−data LTE : Nat -> Nat -> Type where

88+||| Proofs that `n` is less than or equal to `m`

89+||| @ n the smaller number

90+||| @ m the larger number

91+data LTE : (n, m : Nat) -> Type where

92+ ||| Zero is the smallest Nat

7893 lteZero : LTE Z right

94+ ||| If n <= m, then n + 1 <= m + 1

7995 lteSucc : LTE left right -> LTE (S left) (S right)

8096

97+||| Greater than or equal to

8198total GTE : Nat -> Nat -> Type

8299GTE left right = LTE right left

83100

101+||| Strict less than

84102total LT : Nat -> Nat -> Type

85103LT left right = LTE (S left) right

86104

105+||| Strict greater than

87106total GT : Nat -> Nat -> Type

88107GT left right = LT right left

89108

109+||| Boolean test than one Nat is less than or equal to another

90110total lte : Nat -> Nat -> Bool

91111lte Z right = True

92112lte left Z = False

93113lte (S left) (S right) = lte left right

94114

115+||| Boolean test than one Nat is greater than or equal to another

95116total gte : Nat -> Nat -> Bool

96117gte left right = lte right left

97118

119+||| Boolean test than one Nat is strictly less than another

98120total lt : Nat -> Nat -> Bool

99121lt left right = lte (S left) right

100122

123+||| Boolean test than one Nat is strictly greater than another

101124total gt : Nat -> Nat -> Bool

102125gt left right = lt right left

103126

127+||| Find the least of two natural numbers

104128total minimum : Nat -> Nat -> Nat

105129minimum left right =

106130 if lte left right then

@@ -108,6 +132,7 @@ minimum left right =

108132 else

109133 right

110134

135+||| Find the greatest of two natural numbers

111136total maximum : Nat -> Nat -> Nat

112137maximum left right =

113138 if lte left right then

@@ -148,9 +173,11 @@ instance MinBound Nat where

148173instance Cast Integer Nat where

149174 cast = fromInteger

150175

176+||| A wrapper for Nat that specifies the semigroup and monad instances that use (+)

151177record Multiplicative : Type where

152178 getMultiplicative : Nat -> Multiplicative

153179

180+||| A wrapper for Nat that specifies the semigroup and monad instances that use (*)

154181record Additive : Type where

155182 getAdditive : Nat -> Additive

156183

@@ -210,6 +237,7 @@ instance Cast Nat Int where

210237-- Auxilliary notions

211238--------------------------------------------------------------------------------

212239

240+||| The predecessor of a natural number. `pred Z` is `Z`.

213241total pred : Nat -> Nat

214242pred Z = Z

215243pred (S n) = n

@@ -218,11 +246,13 @@ pred (S n) = n

218246-- Fibonacci and factorial

219247--------------------------------------------------------------------------------

220248

249+||| Fibonacci numbers

221250total fib : Nat -> Nat

222251fib Z = Z

223252fib (S Z) = S Z

224253fib (S (S n)) = fib (S n) + fib n

225254

255+||| Factorial function

226256total fact : Nat -> Nat

227257fact Z = S Z

228258fact (S n) = (S n) * fact n

@@ -283,10 +313,13 @@ lcm x y = divNat (x * y) (gcd x y)

283313--------------------------------------------------------------------------------

284314

285315-- Succ

316+

317+||| S preserves equality

286318total eqSucc : (left : Nat) -> (right : Nat) -> (p : left = right) ->

287319 S left = S right

288320eqSucc left _ refl = refl

289321

322+||| S is injective

290323total succInjective : (left : Nat) -> (right : Nat) -> (p : S left = S right) ->

291324 left = right

292325succInjective left _ refl = refl

libs/prelude/Prelude/Stream.idr+19−4

@@ -6,46 +6,61 @@ import Prelude.Vect

66%access public

77%default total

9+||| An infinite stream

910codata Stream : Type -> Type where

1011 (::) : a -> Stream a -> Stream a

1112

1213instance Functor Stream where

1314 map f (x::xs) = f x :: map f xs

1415

16+||| The first element of an infinite stream

1517head : Stream a -> a

1618head (x::xs) = x

1719

20+||| All but the first element

1821tail : Stream a -> Stream a

1922tail (x::xs) = xs

2023

21−take : (n : Nat) -> Stream a -> Vect n a

24+||| Take precisely n elements from the stream

25+||| @ n how many elements to take

26+||| @ xs the stream

27+take : (n : Nat) -> (xs : Stream a) -> Vect n a

2228take Z _ = []

2329take (S n) (x :: xs) = x :: (take n xs)

2430

2531%assert_total

2632drop : Nat -> Stream a -> Stream a

27−drop Z xs = xs

33+drop Z xs = xs

2834drop (S k) (x::xs) = drop k xs

2935

36+||| An infinite stream of repetitions of the same thing

3037repeat : a -> Stream a

3138repeat x = x :: repeat x

3239

33−iterate : (a -> a) -> a -> Stream a

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

43+iterate : (f : a -> a) -> (x : a) -> Stream a

3444iterate f x = x :: iterate f (f x)

3545

46+||| Get the nth element of a stream

3647index : Nat -> Stream a -> a

37−index Z (x::xs) = x

48+index Z (x::xs) = x

3849index (S k) (x::xs) = index k xs

3950

51+||| Combine two streams element-wise using a function

4052zipWith : (a -> b -> c) -> Stream a -> Stream b -> Stream c

4153zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys

4254

55+||| Create a stream of pairs from two streams

4356zip : Stream a -> Stream b -> Stream (a, b)

4457zip = zipWith (\x,y => (x,y))

4558

59+||| Create a pair of streams from a stream of pairs

4660unzip : Stream (a, b) -> (Stream a, Stream b)

4761unzip xs = (map fst xs, map snd xs)

4862

63+||| Return the diagonal elements of a stream of streams

4964diag : Stream (Stream a) -> Stream a

5065diag ((x::xs)::xss) = x :: diag (map tail xss)

5166

libs/prelude/Prelude/Uninhabited.idr+8−2

@@ -1,6 +1,9 @@

11module Prelude.Uninhabited

3+||| A canonical proof that some type is empty

34class Uninhabited t where

5+ ||| If I have a t, I've had a contradiction

6+ ||| @ t the uninhabited type

47 total uninhabited : t -> _|_

69instance Uninhabited (Fin Z) where

@@ -11,5 +14,8 @@ instance Uninhabited (Z = S n) where

1114 uninhabited refl impossible

1215

1316||| Use an absurd assumption to discharge a proof obligation

14−absurd : Uninhabited t => t -> a

15−absurd t = FalseElim (uninhabited t)

17+||| @ t some empty type

18+||| @ a the goal type

19+||| @ h the contradictory hypothesis

20+absurd : Uninhabited t => (h : t) -> a

21+absurd h = FalseElim (uninhabited h)