6e715db · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #1277 from jfdm/doc/libs

6e715dbDavid Christiansen12 years ago

libs/base/Data/Buffer.idr+28−28

compare with master

unifiedsplit

@@ -36,15 +36,15 @@ bitsFromFin : Fin n -> Bits64

36bitsFromFin fZ = 0

37bitsFromFin (fS k) = 1 + bitsFromFin k

39−-- Allocate an empty Buffer. The size hint can be used to avoid

39+||| Allocate an empty Buffer. The size hint can be used to avoid

40−-- unnecessary reallocations and copies under the hood if the

40+||| unnecessary reallocations and copies under the hood if the

41−-- approximate ultimate size of the Buffer is known. Users can assume

41+||| approximate ultimate size of the Buffer is known. Users can assume

42−-- the new Buffer is word-aligned.

42+||| the new Buffer is word-aligned.

43public

44allocate : ( hint : Nat ) -> Buffer Z

45allocate = MkBuffer Z . prim__allocate . bitsFromNat

47−-- Append count repetitions of a Buffer to another Buffer

47+||| Append count repetitions of a Buffer to another Buffer

48%assert_total

49public

50appendBuffer : Buffer n ->

@@ -63,13 +63,13 @@ appendBuffer { n } { m } ( MkBuffer o1 r1 ) c ( MkBuffer o2 r2 ) =

63 off : Bits64

64 off = bitsFromNat o2

66−-- Copy a buffer, potentially allowing the (potentially large) space it

66+||| Copy a buffer, potentially allowing the (potentially large) space it

67−-- pointed to to be freed

67+||| pointed to to be freed

68public

69copy : Buffer n -> Buffer n

70copy { n } = replace ( plusZeroRightNeutral n ) . appendBuffer ( allocate n ) 1

72−-- Create a view over a buffer

72+||| Create a view over a buffer

73public

74peekBuffer : { n : Nat } -> { offset : Nat } -> Buffer ( n + offset ) -> ( offset : Nat ) -> Buffer n

75peekBuffer ( MkBuffer o r ) off = MkBuffer ( o + off ) r

@@ -93,7 +93,7 @@ appendBits { n } prim ( MkBuffer o r ) count =

93 MkBuffer o . prim r ( bitsFromNat $ n + o ) ( bitsFromNat count )

96−-- Read a Bits8 from a Buffer starting at offset

96+||| Read a Bits8 from a Buffer starting at offset

97%assert_total

98public

99peekBits8 : Buffer ( 1 + n ) ->

@@ -101,7 +101,7 @@ peekBits8 : Buffer ( 1 + n ) ->

101 Bits8

102peekBits8 = peekBits { m = 1 } prim__peekB8Native

103

104−-- Append count repetitions of a Bits8 to a Buffer

104+||| Append count repetitions of a Bits8 to a Buffer

105%assert_total

106public

107appendBits8 : Buffer n ->

@@ -110,7 +110,7 @@ appendBits8 : Buffer n ->

110 Buffer ( n + count * 1 )

111appendBits8 = appendBits prim__appendB8Native

112

113−-- Read a Bits16 in native byte order from a Buffer starting at offset

113+||| Read a Bits16 in native byte order from a Buffer starting at offset

114%assert_total

115public

116peekBits16Native : Buffer ( 2 + n ) ->

@@ -118,19 +118,19 @@ peekBits16Native : Buffer ( 2 + n ) ->

118 Bits16

119peekBits16Native = peekBits { m = 2 } prim__peekB16Native

120

121−-- Read a little-endian Bits16 from a Buffer starting at offset

121+||| Read a little-endian Bits16 from a Buffer starting at offset

122%assert_total

123public

124peekBits16LE : Buffer ( 2 + n ) -> ( offset : Fin ( S n ) ) -> Bits16

125peekBits16LE = peekBits { m = 2 } prim__peekB16LE

126

127−-- Read a big-endian Bits16 from a Buffer starting at offset

127+||| Read a big-endian Bits16 from a Buffer starting at offset

128%assert_total

129public

130peekBits16BE : Buffer ( 2 + n ) -> ( offset : Fin ( S n ) ) -> Bits16

131peekBits16BE = peekBits { m = 2 } prim__peekB16BE

132

133−-- Append count repetitions of a Bits16 in native byte order to a Buffer

133+||| Append count repetitions of a Bits16 in native byte order to a Buffer

134%assert_total

135public

136appendBits16Native : Buffer n ->

@@ -139,7 +139,7 @@ appendBits16Native : Buffer n ->

139 Buffer ( n + count * 2 )

140appendBits16Native = appendBits prim__appendB16Native

141

142−-- Append count repetitions of a little-endian Bits16 to a Buffer

142+||| Append count repetitions of a little-endian Bits16 to a Buffer

143%assert_total

144public

145appendBits16LE : Buffer n ->

@@ -148,7 +148,7 @@ appendBits16LE : Buffer n ->

148 Buffer ( n + count * 2 )

149appendBits16LE = appendBits prim__appendB16LE

150

151−-- Append count repetitions of a big-endian Bits16 to a Buffer

151+||| Append count repetitions of a big-endian Bits16 to a Buffer

152%assert_total

153public

154appendBits16BE : Buffer n ->

@@ -157,7 +157,7 @@ appendBits16BE : Buffer n ->

157 Buffer ( n + count * 2 )

158appendBits16BE = appendBits prim__appendB16BE

159

160−-- Read a Bits32 in native byte order from a Buffer starting at offset

160+||| Read a Bits32 in native byte order from a Buffer starting at offset

161%assert_total

162public

163peekBits32Native : Buffer ( 4 + n ) ->

@@ -165,19 +165,19 @@ peekBits32Native : Buffer ( 4 + n ) ->

165 Bits32

166peekBits32Native = peekBits { m = 4 } prim__peekB32Native

167

168−-- Read a little-endian Bits32 from a Buffer starting at offset

168+||| Read a little-endian Bits32 from a Buffer starting at offset

169%assert_total

170public

171peekBits32LE : Buffer ( 4 + n ) -> ( offset : Fin ( S n ) ) -> Bits32

172peekBits32LE = peekBits { m = 4 } prim__peekB32LE

173

174−-- Read a big-endian Bits32 from a Buffer starting at offset

174+||| Read a big-endian Bits32 from a Buffer starting at offset

175%assert_total

176public

177peekBits32BE : Buffer ( 4 + n ) -> ( offset : Fin ( S n ) ) -> Bits32

178peekBits32BE = peekBits { m = 4 } prim__peekB32BE

179

180−-- Append count repetitions of a Bits32 in native byte order to a Buffer

180+||| Append count repetitions of a Bits32 in native byte order to a Buffer

181%assert_total

182public

183appendBits32Native : Buffer n ->

@@ -186,7 +186,7 @@ appendBits32Native : Buffer n ->

186 Buffer ( n + count * 4 )

187appendBits32Native = appendBits prim__appendB32Native

188

189−-- Append count repetitions of a little-endian Bits32 to a Buffer

189+||| Append count repetitions of a little-endian Bits32 to a Buffer

190%assert_total

191public

192appendBits32LE : Buffer n ->

@@ -195,7 +195,7 @@ appendBits32LE : Buffer n ->

195 Buffer ( n + count * 4 )

196appendBits32LE = appendBits prim__appendB32LE

197

198−-- Append count repetitions of a big-endian Bits32 to a Buffer

198+||| Append count repetitions of a big-endian Bits32 to a Buffer

199%assert_total

200public

201appendBits32BE : Buffer n ->

@@ -204,7 +204,7 @@ appendBits32BE : Buffer n ->

204 Buffer ( n + count * 4 )

205appendBits32BE = appendBits prim__appendB32BE

206

207−-- Read a Bits64 in native byte order from a Buffer starting at offset

207+||| Read a Bits64 in native byte order from a Buffer starting at offset

208%assert_total

209public

210peekBits64Native : Buffer ( 8 + n ) ->

@@ -212,19 +212,19 @@ peekBits64Native : Buffer ( 8 + n ) ->

212 Bits64

213peekBits64Native = peekBits { m = 8 } prim__peekB64Native

214

215−-- Read a little-endian Bits64 from a Buffer starting at offset

215+||| Read a little-endian Bits64 from a Buffer starting at offset

216%assert_total

217public

218peekBits64LE : Buffer ( 8 + n ) -> ( offset : Fin ( S n ) ) -> Bits64

219peekBits64LE = peekBits { m = 8 } prim__peekB64LE

220

221−-- Read a big-endian Bits64 from a Buffer starting at offset

221+||| Read a big-endian Bits64 from a Buffer starting at offset

222%assert_total

223public

224peekBits64BE : Buffer ( 8 + n ) -> ( offset : Fin ( S n ) ) -> Bits64

225peekBits64BE = peekBits { m = 8 } prim__peekB64BE

226

227−-- Append count repetitions of a Bits64 in native byte order to a Buffer

227+||| Append count repetitions of a Bits64 in native byte order to a Buffer

228%assert_total

229public

230appendBits64Native : Buffer n ->

@@ -233,7 +233,7 @@ appendBits64Native : Buffer n ->

233 Buffer ( n + count * 8 )

234appendBits64Native = appendBits prim__appendB64Native

235

236−-- Append count repetitions of a little-endian Bits64 to a Buffer

236+||| Append count repetitions of a little-endian Bits64 to a Buffer

237%assert_total

238public

239appendBits64LE : Buffer n ->

@@ -242,7 +242,7 @@ appendBits64LE : Buffer n ->

242 Buffer ( n + count * 8 )

243appendBits64LE = appendBits prim__appendB64LE

244

245−-- Append count repetitions of a big-endian Bits64 to a Buffer

245+||| Append count repetitions of a big-endian Bits64 to a Buffer

246%assert_total

247public

248appendBits64BE : Buffer n ->

libs/base/Data/Fun.idr+2−5

@@ -2,9 +2,7 @@ module Data.Fun

3%default total

5−--------------------------------------------------------------------------------

6−-- Build an n-ary function type from a Vect of Types and a result type

5+||| Build an n-ary function type from a Vect of Types and a result type

7−--------------------------------------------------------------------------------

8Fun : Vect n Type -> Type -> Type

6Fun : Vect n Type -> Type -> Type

9Fun [] r = r

7Fun [] r = r

10Fun (t::ts) r = t -> Fun ts r

8Fun (t::ts) r = t -> Fun ts r

@@ -14,5 +12,4 @@ chain {ts = []} g r = g r

14chain {ts = (_::_)} g f = \ x => chain g (f x)

12chain {ts = (_::_)} g f = \ x => chain g (f x)

16target : {ts : Vect n Type} -> Fun ts r -> Type

14target : {ts : Vect n Type} -> Fun ts r -> Type

17−target {r} _ = r

15+target {r} _ = r

18−

libs/base/Data/List.idr+7−6

@@ -7,11 +7,15 @@ using (xs : List a)

7 data Elem : a -> List a -> Type where

8 Here : Elem x (x :: xs)

9 There : Elem x xs -> Elem x (y :: xs)

10−

10+

11 instance Uninhabited (Elem {a} x []) where

12 uninhabited Here impossible

13 uninhabited (There p) impossible

14−

14+

15+ ||| Is the given element a member of the given list.

16+ |||

17+ ||| @x The element to be tested.

18+ ||| @xs The list to be checked against

15 isElem : DecEq a => (x : a) -> (xs : List a) -> Dec (Elem x xs)

19 isElem : DecEq a => (x : a) -> (xs : List a) -> Dec (Elem x xs)

16 isElem x [] = No absurd

20 isElem x [] = No absurd

17 isElem x (y :: xs) with (decEq x y)

21 isElem x (y :: xs) with (decEq x y)

@@ -21,10 +25,7 @@ using (xs : List a)

21 isElem x (y :: xs) | (No contra) | (No f) = No (mkNo contra f)

25 isElem x (y :: xs) | (No contra) | (No f) = No (mkNo contra f)

22 where

26 where

23 mkNo : {xs' : List a} ->

27 mkNo : {xs' : List a} ->

24− ((x' = y') -> _|_) -> (Elem x' xs' -> _|_) ->

28+ ((x' = y') -> _|_) -> (Elem x' xs' -> _|_) ->

25 Elem x' (y' :: xs') -> _|_

29 Elem x' (y' :: xs') -> _|_

26 mkNo f g Here = f refl

30 mkNo f g Here = f refl

27 mkNo f g (There x) = g x

31 mkNo f g (There x) = g x

28−

29−

30−

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

@@ -4,7 +4,7 @@ import Data.Bits

5%default total

7−-- Integers modulo 2^n

7+||| Integers modulo 2^n

8public

9data Mod2 : Nat -> Type where

10 MkMod2 : {n : Nat} -> Bits n -> Mod2 n

libs/base/Data/Rel.idr+2−3

@@ -2,9 +2,8 @@ module Data.Rel

3import Data.Fun

5−--------------------------------------------------------------------------------

6−-- Build an n-ary relation type from a Vect of Types

6+||| Build an n-ary relation type from a Vect of Types

7−--------------------------------------------------------------------------------

8Rel : Vect n Type -> Type

7Rel : Vect n Type -> Type

9Rel ts = Fun ts Type

8Rel ts = Fun ts Type

libs/base/System/Concurrency/Process.idr+7−14

@@ -9,9 +9,8 @@ import System.Concurrency.Raw

9abstract

10data ProcID msg = MkPID Ptr

12−-- Type safe message passing programs. Parameterised over the type of

12+||| Type safe message passing programs. Parameterised over the type of

13−-- message which can be send, and the return type.

13+||| message which can be send, and the return type.

14−

15data Process : (msgType : Type) -> Type -> Type where

14data Process : (msgType : Type) -> Type -> Type where

16 lift : IO a -> Process msg a

15 lift : IO a -> Process msg a

@@ -30,31 +29,26 @@ instance Monad (Process msg) where

30run : Process msg x -> IO x

29run : Process msg x -> IO x

31run (lift prog) = prog

30run (lift prog) = prog

33−-- Get current process ID

32+||| Get current process ID

34−

35myID : Process msg (ProcID msg)

33myID : Process msg (ProcID msg)

36myID = lift (return (MkPID prim__vm))

34myID = lift (return (MkPID prim__vm))

38−-- Send a message to another process

36+||| Send a message to another process

39−

40send : ProcID msg -> msg -> Process msg ()

37send : ProcID msg -> msg -> Process msg ()

41send (MkPID p) m = lift (sendToThread p (prim__vm, m))

38send (MkPID p) m = lift (sendToThread p (prim__vm, m))

43−-- Return whether a message is waiting in the queue

40+||| Return whether a message is waiting in the queue

44−

45msgWaiting : Process msg Bool

41msgWaiting : Process msg Bool

46msgWaiting = lift checkMsgs

42msgWaiting = lift checkMsgs

48−-- Receive a message - blocks if there is no message waiting

44+||| Receive a message - blocks if there is no message waiting

49−

50recv : Process msg msg

45recv : Process msg msg

51recv {msg} = do (senderid, m) <- lift get

46recv {msg} = do (senderid, m) <- lift get

52 return m

47 return m

53 where get : IO (Ptr, msg)

48 where get : IO (Ptr, msg)

54 get = getMsg

49 get = getMsg

56−-- receive a message, and return with the sender's process ID.

51+||| receive a message, and return with the sender's process ID.

57−

58recvWithSender : Process msg (ProcID msg, msg)

52recvWithSender : Process msg (ProcID msg, msg)

59recvWithSender {msg}

53recvWithSender {msg}

60 = do (senderid, m) <- lift get

54 = do (senderid, m) <- lift get

@@ -65,4 +59,3 @@ recvWithSender {msg}

65create : Process msg () -> Process msg (ProcID msg)

59create : Process msg () -> Process msg (ProcID msg)

66create (lift p) = do ptr <- lift (fork p)

60create (lift p) = do ptr <- lift (fork p)

67 return (MkPID ptr)

61 return (MkPID ptr)

68−

libs/base/System/Concurrency/Raw.idr+3−6

@@ -6,8 +6,7 @@ module System.Concurrency.Raw

7import System

9−-- Send a message of any type to the thread with the given thread id

9+||| Send a message of any type to the thread with the given thread id

10−

11sendToThread : (thread_id : Ptr) -> a -> IO ()

10sendToThread : (thread_id : Ptr) -> a -> IO ()

12sendToThread {a} dest val

11sendToThread {a} dest val

13 = mkForeign (FFun "idris_sendMessage"

12 = mkForeign (FFun "idris_sendMessage"

@@ -18,10 +17,8 @@ checkMsgs = do msgs <- mkForeign (FFun "idris_checkMessages"

18 [FPtr] FInt) prim__vm

17 [FPtr] FInt) prim__vm

19 return (intToBool msgs)

18 return (intToBool msgs)

21−-- Check inbox for messages. If there are none, blocks until a message

20+||| Check inbox for messages. If there are none, blocks until a message

22−-- arrives.

21+||| arrives.

23−

24getMsg : IO a

22getMsg : IO a

25getMsg {a} = mkForeign (FFun "idris_recvMessage"

23getMsg {a} = mkForeign (FFun "idris_recvMessage"

26 [FPtr] (FAny a)) prim__vm

24 [FPtr] (FAny a)) prim__vm

27−

libs/prelude/Prelude.idr+2−3

@@ -549,9 +549,9 @@ fgetc : File -> IO Char

549fgetc (FHandle h) = return (cast !(mkForeign (FFun "fgetc" [FPtr] FInt) h))

550

551fgetc' : File -> IO (Maybe Char)

552−fgetc' (FHandle h)

552+fgetc' (FHandle h)

553 = do x <- mkForeign (FFun "fgetc" [FPtr] FInt) h

554− if (x < 0) then return Nothing

554+ if (x < 0) then return Nothing

555 else return (Just (cast x))

556

557fflush : File -> IO ()

@@ -650,4 +650,3 @@ readFile fn = do h <- openFile fn Read

650 if not x then do l <- fread h

651 readFile' h (contents ++ l)

652 else return contents

653−

libs/prelude/Prelude/Algebra.idr+170−155

@@ -13,24 +13,26 @@ infixl 6 <*>

13-- A modest class hierarchy

14--------------------------------------------------------------------------------

16−-- Sets equipped with a single binary operation that is associative. Must

16+||| Sets equipped with a single binary operation that is associative. Must

17−-- satisfy the following laws:

17+||| satisfy the following laws:

18+|||

18−-- Associativity of <+>:

19+||| + Associativity of `<+>`:

19−-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c

20+||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c

20class Semigroup a where

21class Semigroup a where

21 (<+>) : a -> a -> a

22 (<+>) : a -> a -> a

23class Semigroup a => VerifiedSemigroup a where

24class Semigroup a => VerifiedSemigroup a where

24 total semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r

25 total semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r

26−-- Sets equipped with a single binary operation that is associative, along with

27+||| Sets equipped with a single binary operation that is associative, along with

27−-- a neutral element for that binary operation. Must satisfy the following

28+||| a neutral element for that binary operation. Must satisfy the following

28−-- laws:

29+||| laws:

30+|||

29−-- Associativity of <+>:

31+||| + Associativity of `<+>`:

30−-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c

32+||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c

31−-- Neutral for <+>:

33+||| + Neutral for `<+>`:

32−-- forall a, a <+> neutral == a

34+||| forall a, a <+> neutral == a

33−-- forall a, neutral <+> a == a

35+||| forall a, neutral <+> a == a

34class Semigroup a => Monoid a where

36class Semigroup a => Monoid a where

35 neutral : a

37 neutral : a

@@ -38,17 +40,17 @@ class (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where

38 total monoidNeutralIsNeutralL : (l : a) -> l <+> neutral = l

40 total monoidNeutralIsNeutralL : (l : a) -> l <+> neutral = l

39 total monoidNeutralIsNeutralR : (r : a) -> neutral <+> r = r

41 total monoidNeutralIsNeutralR : (r : a) -> neutral <+> r = r

41−-- Sets equipped with a single binary operation that is associative, along with

43+||| Sets equipped with a single binary operation that is associative, along with

42−-- a neutral element for that binary operation and inverses for all elements.

44+||| a neutral element for that binary operation and inverses for all elements.

43−-- Must satisfy the following laws:

45+||| Must satisfy the following laws:

44−-- Associativity of <+>:

46+||| + Associativity of `<+>`:

45−-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c

47+||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c

46−-- Neutral for <+>:

48+||| + Neutral for `<+>`:

47−-- forall a, a <+> neutral == a

49+||| forall a, a <+> neutral == a

48−-- forall a, neutral <+> a == a

50+||| forall a, neutral <+> a == a

49−-- Inverse for <+>:

51+||| + Inverse for `<+>`:

50−-- forall a, a <+> inverse a == neutral

52+||| forall a, a <+> inverse a == neutral

51−-- forall a, inverse a <+> a == neutral

53+||| forall a, inverse a <+> a == neutral

52class Monoid a => Group a where

54class Monoid a => Group a where

53 inverse : a -> a

55 inverse : a -> a

@@ -59,43 +61,45 @@ class (VerifiedMonoid a, Group a) => VerifiedGroup a where

59(<->) : Group a => a -> a -> a

61(<->) : Group a => a -> a -> a

60(<->) left right = left <+> (inverse right)

62(<->) left right = left <+> (inverse right)

62−-- Sets equipped with a single binary operation that is associative and

64+||| Sets equipped with a single binary operation that is associative and

63−-- commutative, along with a neutral element for that binary operation and

65+||| commutative, along with a neutral element for that binary operation and

64−-- inverses for all elements. Must satisfy the following laws:

66+||| inverses for all elements. Must satisfy the following laws:

67+|||

65−-- Associativity of <+>:

68+||| + Associativity of `<+>`:

66−-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c

69+||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c

67−-- Commutativity of <+>:

70+||| + Commutativity of `<+>`:

68−-- forall a b, a <+> b == b <+> a

71+||| forall a b, a <+> b == b <+> a

69−-- Neutral for <+>:

72+||| + Neutral for `<+>`:

70−-- forall a, a <+> neutral == a

73+||| forall a, a <+> neutral == a

71−-- forall a, neutral <+> a == a

74+||| forall a, neutral <+> a == a

72−-- Inverse for <+>:

75+||| + Inverse for `<+>`:

73−-- forall a, a <+> inverse a == neutral

76+||| forall a, a <+> inverse a == neutral

74−-- forall a, inverse a <+> a == neutral

77+||| forall a, inverse a <+> a == neutral

75class Group a => AbelianGroup a where { }

78class Group a => AbelianGroup a where { }

77class (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where

80class (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where

78 total abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l

81 total abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l

80−-- Sets equipped with two binary operations, one associative and commutative

83+||| Sets equipped with two binary operations, one associative and commutative

81−-- supplied with a neutral element, and the other associative, with

84+||| supplied with a neutral element, and the other associative, with

82−-- distributivity laws relating the two operations. Must satisfy the following

85+||| distributivity laws relating the two operations. Must satisfy the following

83−-- laws:

86+||| laws:

87+|||

84−-- Associativity of <+>:

88+||| + Associativity of `<+>`:

85−-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c

89+||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c

86−-- Commutativity of <+>:

90+||| + Commutativity of `<+>`:

87−-- forall a b, a <+> b == b <+> a

91+||| forall a b, a <+> b == b <+> a

88−-- Neutral for <+>:

92+||| + Neutral for `<+>`:

89−-- forall a, a <+> neutral == a

93+||| forall a, a <+> neutral == a

90−-- forall a, neutral <+> a == a

94+||| forall a, neutral <+> a == a

91−-- Inverse for <+>:

95+||| + Inverse for `<+>`:

92−-- forall a, a <+> inverse a == neutral

96+||| forall a, a <+> inverse a == neutral

93−-- forall a, inverse a <+> a == neutral

97+||| forall a, inverse a <+> a == neutral

94−-- Associativity of <*>:

98+||| + Associativity of `<*>`:

95−-- forall a b c, a <*> (b <*> c) == (a <*> b) <*> c

99+||| forall a b c, a <*> (b <*> c) == (a <*> b) <*> c

96−-- Distributivity of <*> and <->:

100+||| + Distributivity of `<*>` and `<->`:

97−-- forall a b c, a <*> (b <+> c) == (a <*> b) <+> (a <*> c)

101+||| forall a b c, a <*> (b <+> c) == (a <*> b) <+> (a <*> c)

98−-- forall a b c, (a <+> b) <*> c == (a <*> c) <+> (b <*> c)

102+||| forall a b c, (a <+> b) <*> c == (a <*> c) <+> (b <*> c)

99class AbelianGroup a => Ring a where

103class AbelianGroup a => Ring a where

100 (<*>) : a -> a -> a

104 (<*>) : a -> a -> a

101

105

@@ -104,28 +108,29 @@ class (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where

104 total ringOpIsDistributiveL : (l, c, r : a) -> l <*> (c <+> r) = (l <*> c) <+> (l <*> r)

108 total ringOpIsDistributiveL : (l, c, r : a) -> l <*> (c <+> r) = (l <*> c) <+> (l <*> r)

105 total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <*> r = (l <*> r) <+> (l <*> c)

109 total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <*> r = (l <*> r) <+> (l <*> c)

106

110

107−-- Sets equipped with two binary operations, one associative and commutative

111+||| Sets equipped with two binary operations, one associative and commutative

108−-- supplied with a neutral element, and the other associative supplied with a

112+||| supplied with a neutral element, and the other associative supplied with a

109−-- neutral element, with distributivity laws relating the two operations. Must

113+||| neutral element, with distributivity laws relating the two operations. Must

110−-- satisfy the following laws:

114+||| satisfy the following laws:

115+|||

111−-- Associativity of <+>:

116+||| + Associativity of `<+>`:

112−-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c

117+||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c

113−-- Commutativity of <+>:

118+||| + Commutativity of `<+>`:

114−-- forall a b, a <+> b == b <+> a

119+||| forall a b, a <+> b == b <+> a

115−-- Neutral for <+>:

120+||| + Neutral for `<+>`:

116−-- forall a, a <+> neutral == a

121+||| forall a, a <+> neutral == a

117−-- forall a, neutral <+> a == a

122+||| forall a, neutral <+> a == a

118−-- Inverse for <+>:

123+||| + Inverse for `<+>`:

119−-- forall a, a <+> inverse a == neutral

124+||| forall a, a <+> inverse a == neutral

120−-- forall a, inverse a <+> a == neutral

125+||| forall a, inverse a <+> a == neutral

121−-- Associativity of <*>:

126+||| + Associativity of `<*>a:

122−-- forall a b c, a <*> (b <*> c) == (a <*> b) <*> c

127+||| forall a b c, a <*> (b <*> c) == (a <*> b) <*> c

123−-- Neutral for <*>:

128+||| + Neutral for `<*>`:

124−-- forall a, a <*> unity == a

129+||| forall a, a <*> unity == a

125−-- forall a, unity <*> a == a

130+||| forall a, unity <*> a == a

126−-- Distributivity of <*> and <->:

131+||| + Distributivity of `<*>` and `<->`:

127−-- forall a b c, a <*> (b <+> c) == (a <*> b) <+> (a <*> c)

132+||| forall a b c, a <*> (b <+> c) == (a <*> b) <+> (a <*> c)

128−-- forall a b c, (a <+> b) <*> c == (a <*> c) <+> (b <*> c)

133+||| forall a b c, (a <+> b) <*> c == (a <*> c) <+> (b <*> c)

129class Ring a => RingWithUnity a where

134class Ring a => RingWithUnity a where

130 unity : a

135 unity : a

131

136

@@ -133,15 +138,17 @@ class (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where

133 total ringWithUnityIsUnityL : (l : a) -> l <*> unity = l

138 total ringWithUnityIsUnityL : (l : a) -> l <*> unity = l

134 total ringWithUnityIsUnityR : (r : a) -> unity <*> r = r

139 total ringWithUnityIsUnityR : (r : a) -> unity <*> r = r

135

140

136−-- Sets equipped with a binary operation that is commutative, associative and

141+||| Sets equipped with a binary operation that is commutative, associative and

137−-- idempotent. Must satisfy the following laws:

142+||| idempotent. Must satisfy the following laws:

143+|||

138−-- Associativity of join:

144+||| + Associativity of join:

139−-- forall a b c, join a (join b c) == join (join a b) c

145+||| forall a b c, join a (join b c) == join (join a b) c

140−-- Commutativity of join:

146+||| + Commutativity of join:

141−-- forall a b, join a b == join b a

147+||| forall a b, join a b == join b a

142−-- Idempotency of join:

148+||| + Idempotency of join:

143−-- forall a, join a a == a

149+||| forall a, join a a == a

150+|||

144−-- Join semilattices capture the notion of sets with a "least upper bound".

151+||| Join semilattices capture the notion of sets with a "least upper bound".

145class JoinSemilattice a where

152class JoinSemilattice a where

146 join : a -> a -> a

153 join : a -> a -> a

147

154

@@ -150,15 +157,17 @@ class JoinSemilattice a => VerifiedJoinSemilattice a where

150 total joinSemilatticeJoinIsCommutative : (l, r : a) -> join l r = join r l

157 total joinSemilatticeJoinIsCommutative : (l, r : a) -> join l r = join r l

151 total joinSemilatticeJoinIsIdempotent : (e : a) -> join e e = e

158 total joinSemilatticeJoinIsIdempotent : (e : a) -> join e e = e

152

159

153−-- Sets equipped with a binary operation that is commutative, associative and

160+||| Sets equipped with a binary operation that is commutative, associative and

154−-- idempotent. Must satisfy the following laws:

161+||| idempotent. Must satisfy the following laws:

162+|||

155−-- Associativity of meet:

163+||| + Associativity of meet:

156−-- forall a b c, meet a (meet b c) == meet (meet a b) c

164+||| forall a b c, meet a (meet b c) == meet (meet a b) c

157−-- Commutativity of meet:

165+||| + Commutativity of meet:

158−-- forall a b, meet a b == meet b a

166+||| forall a b, meet a b == meet b a

159−-- Idempotency of meet:

167+||| + Idempotency of meet:

160−-- forall a, meet a a == a

168+||| forall a, meet a a == a

169+|||

161−-- Meet semilattices capture the notion of sets with a "greatest lower bound".

170+||| Meet semilattices capture the notion of sets with a "greatest lower bound".

162class MeetSemilattice a where

171class MeetSemilattice a where

163 meet : a -> a -> a

172 meet : a -> a -> a

164

173

@@ -167,84 +176,90 @@ class MeetSemilattice a => VerifiedMeetSemilattice a where

167 total meetSemilatticeMeetIsCommutative : (l, r : a) -> meet l r = meet r l

176 total meetSemilatticeMeetIsCommutative : (l, r : a) -> meet l r = meet r l

168 total meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e

177 total meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e

169

178

170−-- Sets equipped with a binary operation that is commutative, associative and

179+||| Sets equipped with a binary operation that is commutative, associative and

171−-- idempotent and supplied with a neutral element. Must satisfy the following

180+||| idempotent and supplied with a neutral element. Must satisfy the following

172−-- laws:

181+||| laws:

182+|||

173−-- Associativity of join:

183+||| + Associativity of join:

174−-- forall a b c, join a (join b c) == join (join a b) c

184+||| forall a b c, join a (join b c) == join (join a b) c

175−-- Commutativity of join:

185+||| + Commutativity of join:

176−-- forall a b, join a b == join b a

186+||| forall a b, join a b == join b a

177−-- Idempotency of join:

187+||| + Idempotency of join:

178−-- forall a, join a a == a

188+||| forall a, join a a == a

179−-- Bottom:

189+||| + Bottom:

180−-- forall a, join a bottom == bottom

190+||| forall a, join a bottom == bottom

191+|||

181−-- Join semilattices capture the notion of sets with a "least upper bound"

192+||| Join semilattices capture the notion of sets with a "least upper bound"

182−-- equipped with a "bottom" element.

193+||| equipped with a "bottom" element.

183class JoinSemilattice a => BoundedJoinSemilattice a where

194class JoinSemilattice a => BoundedJoinSemilattice a where

184 bottom : a

195 bottom : a

185

196

186class (VerifiedJoinSemilattice a, BoundedJoinSemilattice a) => VerifiedBoundedJoinSemilattice a where

197class (VerifiedJoinSemilattice a, BoundedJoinSemilattice a) => VerifiedBoundedJoinSemilattice a where

187 total boundedJoinSemilatticeBottomIsBottom : (e : a) -> join e bottom = bottom

198 total boundedJoinSemilatticeBottomIsBottom : (e : a) -> join e bottom = bottom

188

199

189−-- Sets equipped with a binary operation that is commutative, associative and

200+||| Sets equipped with a binary operation that is commutative, associative and

190−-- idempotent and supplied with a neutral element. Must satisfy the following

201+||| idempotent and supplied with a neutral element. Must satisfy the following

191−-- laws:

202+||| laws:

203+|||

192−-- Associativity of meet:

204+||| + Associativity of meet:

193−-- forall a b c, meet a (meet b c) == meet (meet a b) c

205+||| forall a b c, meet a (meet b c) == meet (meet a b) c

194−-- Commutativity of meet:

206+||| + Commutativity of meet:

195−-- forall a b, meet a b == meet b a

207+||| forall a b, meet a b == meet b a

196−-- Idempotency of meet:

208+||| + Idempotency of meet:

197−-- forall a, meet a a == a

209+||| forall a, meet a a == a

198−-- Top:

210+||| + Top:

199−-- forall a, meet a top == top

211+||| forall a, meet a top == top

212+|||

200−-- Meet semilattices capture the notion of sets with a "greatest lower bound"

213+||| Meet semilattices capture the notion of sets with a "greatest lower bound"

201−-- equipped with a "top" element.

214+||| equipped with a "top" element.

202class MeetSemilattice a => BoundedMeetSemilattice a where

215class MeetSemilattice a => BoundedMeetSemilattice a where

203 top : a

216 top : a

204

217

205class (VerifiedMeetSemilattice a, BoundedMeetSemilattice a) => VerifiedBoundedMeetSemilattice a where

218class (VerifiedMeetSemilattice a, BoundedMeetSemilattice a) => VerifiedBoundedMeetSemilattice a where

206 total boundedMeetSemilatticeTopIsTop : (e : a) -> meet e top = top

219 total boundedMeetSemilatticeTopIsTop : (e : a) -> meet e top = top

207

220

208−-- Sets equipped with two binary operations that are both commutative,

221+||| Sets equipped with two binary operations that are both commutative,

209−-- associative and idempotent, along with absorbtion laws for relating the two

222+||| associative and idempotent, along with absorbtion laws for relating the two

210−-- binary operations. Must satisfy the following:

223+||| binary operations. Must satisfy the following:

224+|||

211−-- Associativity of meet and join:

225+||| + Associativity of meet and join:

212−-- forall a b c, meet a (meet b c) == meet (meet a b) c

226+||| forall a b c, meet a (meet b c) == meet (meet a b) c

213−-- forall a b c, join a (join b c) == join (join a b) c

227+||| forall a b c, join a (join b c) == join (join a b) c

214−-- Commutativity of meet and join:

228+||| + Commutativity of meet and join:

215−-- forall a b, meet a b == meet b a

229+||| forall a b, meet a b == meet b a

216−-- forall a b, join a b == join b a

230+||| forall a b, join a b == join b a

217−-- Idempotency of meet and join:

231+||| + Idempotency of meet and join:

218−-- forall a, meet a a == a

232+||| forall a, meet a a == a

219−-- forall a, join a a == a

233+||| forall a, join a a == a

220−-- Absorbtion laws for meet and join:

234+||| + Absorbtion laws for meet and join:

221−-- forall a b, meet a (join a b) == a

235+||| forall a b, meet a (join a b) == a

222−-- forall a b, join a (meet a b) == a

236+||| forall a b, join a (meet a b) == a

223class (JoinSemilattice a, MeetSemilattice a) => Lattice a where { }

237class (JoinSemilattice a, MeetSemilattice a) => Lattice a where { }

224

238

225class (VerifiedJoinSemilattice a, VerifiedMeetSemilattice a) => VerifiedLattice a where

239class (VerifiedJoinSemilattice a, VerifiedMeetSemilattice a) => VerifiedLattice a where

226 total latticeMeetAbsorbsJoin : (l, r : a) -> meet l (join l r) = l

240 total latticeMeetAbsorbsJoin : (l, r : a) -> meet l (join l r) = l

227 total latticeJoinAbsorbsMeet : (l, r : a) -> join l (meet l r) = l

241 total latticeJoinAbsorbsMeet : (l, r : a) -> join l (meet l r) = l

228

242

229−-- Sets equipped with two binary operations that are both commutative,

243+||| Sets equipped with two binary operations that are both commutative,

230−-- associative and idempotent and supplied with neutral elements, along with

244+||| associative and idempotent and supplied with neutral elements, along with

231−-- absorbtion laws for relating the two binary operations. Must satisfy the

245+||| absorbtion laws for relating the two binary operations. Must satisfy the

232−-- following:

246+||| following:

247+|||

233−-- Associativity of meet and join:

248+||| + Associativity of meet and join:

234−-- forall a b c, meet a (meet b c) == meet (meet a b) c

249+||| forall a b c, meet a (meet b c) == meet (meet a b) c

235−-- forall a b c, join a (join b c) == join (join a b) c

250+||| forall a b c, join a (join b c) == join (join a b) c

236−-- Commutativity of meet and join:

251+||| + Commutativity of meet and join:

237−-- forall a b, meet a b == meet b a

252+||| forall a b, meet a b == meet b a

238−-- forall a b, join a b == join b a

253+||| forall a b, join a b == join b a

239−-- Idempotency of meet and join:

254+||| + Idempotency of meet and join:

240−-- forall a, meet a a == a

255+||| forall a, meet a a == a

241−-- forall a, join a a == a

256+||| forall a, join a a == a

242−-- Absorbtion laws for meet and join:

257+||| + Absorbtion laws for meet and join:

243−-- forall a b, meet a (join a b) == a

258+||| forall a b, meet a (join a b) == a

244−-- forall a b, join a (meet a b) == a

259+||| forall a b, join a (meet a b) == a

245−-- Neutral for meet and join:

260+||| + Neutral for meet and join:

246−-- forall a, meet a top == top

261+||| forall a, meet a top == top

247−-- forall a, join a bottom == bottom

262+||| forall a, join a bottom == bottom

248class (BoundedJoinSemilattice a, BoundedMeetSemilattice a) => BoundedLattice a where { }

263class (BoundedJoinSemilattice a, BoundedMeetSemilattice a) => BoundedLattice a where { }

249

264

250class (VerifiedBoundedJoinSemilattice a, VerifiedBoundedMeetSemilattice a, VerifiedLattice a) => VerifiedBoundedLattice a where { }

265class (VerifiedBoundedJoinSemilattice a, VerifiedBoundedMeetSemilattice a, VerifiedLattice a) => VerifiedBoundedLattice a where { }

libs/prelude/Prelude/Cast.idr+5−3

@@ -1,7 +1,11 @@

1module Prelude.Cast

3+||| Type class for transforming a instance of a data type to another type.

3class Cast from to where

4class Cast from to where

5+ ||| Perform a cast operation.

6+ |||

7+ ||| @orig The original type.

4− cast : from -> to

8+ cast : (orig : from) -> to

6-- String casts

10-- String casts

@@ -45,5 +49,3 @@ instance Cast Integer String where

46instance Cast Char Int where

50instance Cast Char Int where

47 cast = prim__charToInt

51 cast = prim__charToInt

48−

49−