@@ -12,7 +12,7 @@ getProof (a ** v) = v
13FalseElim : _|_ -> a
13FalseElim : _|_ -> a
15−-- For rewrite tactic
15+-- ------------------------------------------------------ [ For rewrite tactic ]
16replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y
16replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y
17replace refl prf = prf
17replace refl prf = prf
@@ -42,36 +42,45 @@ public %assert_total -- reduces at compile time, use with extreme care!
42really_believe_me : a -> b
42really_believe_me : a -> b
43really_believe_me x = prim__believe_me _ _ x
43really_believe_me x = prim__believe_me _ _ x
45+-- ---------------------------------------------------------------- [ Builtins ]
45namespace Builtins {
46namespace Builtins {
47Not : Type -> Type
48Not : Type -> Type
48Not a = a -> _|_
49Not a = a -> _|_
51+-- | Identity function.
50id : a -> a
52id : a -> a
55+-- | Manually assign a type to an expression.
53the : (a : Type) -> a -> a
56the : (a : Type) -> a -> a
59+-- | Constant function.
56const : a -> b -> a
60const : a -> b -> a
57const x _ = x
61const x _ = x
63+-- | Return the first element of a pair.
59fst : (s, t) -> s
64fst : (s, t) -> s
60fst (x, y) = x
65fst (x, y) = x
67+-- | Return the second element of a pair.
62snd : (a, b) -> b
68snd : (a, b) -> b
63snd (x, y) = y
69snd (x, y) = y
73+-- | Function composition
67(.) : (b -> c) -> (a -> b) -> a -> c
74(.) : (b -> c) -> (a -> b) -> a -> c
68(.) f g x = f (g x)
75(.) f g x = f (g x)
77+-- | Takes in the first two arguments in reverse order.
70flip : (a -> b -> c) -> b -> a -> c
78flip : (a -> b -> c) -> b -> a -> c
71flip f x y = f y x
79flip f x y = f y x
83+-- | Function application.
75($) : (a -> b) -> a -> b
84($) : (a -> b) -> a -> b
76f $ a = f a
85f $ a = f a
@@ -82,39 +91,47 @@ data Dec : Type -> Type where
82 Yes : {A : Type} -> A -> Dec A
91 Yes : {A : Type} -> A -> Dec A
83 No : {A : Type} -> (A -> _|_) -> Dec A
92 No : {A : Type} -> (A -> _|_) -> Dec A
94+-- | Boolean Data Type
85data Bool = False | True
95data Bool = False | True
97+-- | Boolean elimination
87boolElim : Bool -> |(t : a) -> |(f : a) -> a
98boolElim : Bool -> |(t : a) -> |(f : a) -> a
88boolElim True t e = t
99boolElim True t e = t
89boolElim False t e = e
100boolElim False t e = e
102+-- | Defines a predicate on Bool which guarantees that the value is true.
91data so : Bool -> Type where oh : so True
103data so : Bool -> Type where oh : so True
105+-- Syntaxtic sugar for boolean elimination.
93syntax if [test] then [t] else [e] = boolElim test t e
106syntax if [test] then [t] else [e] = boolElim test t e
94syntax [test] "?" [t] ":" [e] = if test then t else e
107syntax [test] "?" [t] ":" [e] = if test then t else e
109+-- Boolean Operator Precedence
96infixl 4 &&, ||
110infixl 4 &&, ||
98(||) : Bool -> Bool -> Bool
113(||) : Bool -> Bool -> Bool
99(||) False x = x
114(||) False x = x
100(||) True _ = True
115(||) True _ = True
102(&&) : Bool -> Bool -> Bool
118(&&) : Bool -> Bool -> Bool
103(&&) True x = x
119(&&) True x = x
104(&&) False _ = False
120(&&) False _ = False
106not : Bool -> Bool
123not : Bool -> Bool
107not True = False
124not True = False
108not False = True
125not False = True
127+-- Numerical Operator Precedence
110infixl 5 ==, /=
128infixl 5 ==, /=
111infixl 6 <, <=, >, >=
129infixl 6 <, <=, >, >=
112infixl 7 <<, >>
130infixl 7 <<, >>
113infixl 8 +,-,++
131infixl 8 +,-,++
114infixl 9 *,/
132infixl 9 *,/
116−--- Numeric operators
134+-- ------------------------------------------------------- [ Numeric Operators ]
118intToBool : Int -> Bool
135intToBool : Int -> Bool
119intToBool 0 = False
136intToBool 0 = False
120intToBool x = True
137intToBool x = True
@@ -122,6 +139,7 @@ intToBool x = True
122boolOp : (a -> a -> Int) -> a -> a -> Bool
139boolOp : (a -> a -> Int) -> a -> a -> Bool
123boolOp op x y = intToBool (op x y)
140boolOp op x y = intToBool (op x y)
142+-- | The Eq class defines inequality and equality.
125class Eq a where
143class Eq a where
126 (==) : a -> a -> Bool
144 (==) : a -> a -> Bool
127 (/=) : a -> a -> Bool
145 (/=) : a -> a -> Bool
@@ -162,6 +180,7 @@ instance Eq Ordering where
162 GT == GT = True
180 GT == GT = True
163 _ == _ = False
181 _ == _ = False
183+-- | The Ord class defines comparison operations on ordered data types.
165class Eq a => Ord a where
184class Eq a => Ord a where
166 compare : a -> a -> Ordering
185 compare : a -> a -> Ordering
@@ -224,13 +243,14 @@ instance (Ord a, Ord b) => Ord (a, b) where
224 then compare xl yl
243 then compare xl yl
225 else compare xr yr
244 else compare xr yr
227−
246+-- | The Num class defines basic numerical arithmetic.
228class Num a where
247class Num a where
229 (+) : a -> a -> a
248 (+) : a -> a -> a
230 (-) : a -> a -> a
249 (-) : a -> a -> a
231 (*) : a -> a -> a
250 (*) : a -> a -> a
232−
251+ -- | Absolute value
233 abs : a -> a
252 abs : a -> a
253+ -- | Conversion from Integer.
234 fromInteger : Integer -> a
254 fromInteger : Integer -> a
236instance Num Integer where
256instance Num Integer where
@@ -334,38 +354,45 @@ instance Ord Bits64 where
334 else if l > r then GT
354 else if l > r then GT
357+-- | Integer division.
338div : Integer -> Integer -> Integer
359div : Integer -> Integer -> Integer
339div = prim__sdivBigInt
360div = prim__sdivBigInt
362+-- | Integer modulus.
342mod : Integer -> Integer -> Integer
364mod : Integer -> Integer -> Integer
343mod = prim__sremBigInt
365mod = prim__sremBigInt
345−
367+-- | Fractional division of two Floats.
346(/) : Float -> Float -> Float
368(/) : Float -> Float -> Float
347(/) = prim__divFloat
369(/) = prim__divFloat
349−--- string operators
371+-- -------------------------------------------------------- [ String Operators ]
350−
372+-- | Appends two strings together.
351(++) : String -> String -> String
373(++) : String -> String -> String
352(++) = prim__concat
374(++) = prim__concat
376+-- | Returns the first character in the specified string.
355strHead : String -> Char
378strHead : String -> Char
356strHead = prim__strHead
379strHead = prim__strHead
381+-- | Returns the characters specified after the head of the string.
359strTail : String -> String
383strTail : String -> String
360strTail = prim__strTail
384strTail = prim__strTail
386+-- | Adds a character to the from of the specified string.
362strCons : Char -> String -> String
387strCons : Char -> String -> String
363strCons = prim__strCons
388strCons = prim__strCons
390+-- | Returns the nth character (starting from 0) of the specified string.
366strIndex : String -> Int -> Char
392strIndex : String -> Int -> Char
367strIndex = prim__strIndex
393strIndex = prim__strIndex
395+-- | Reverses the elements within a String.
369reverse : String -> String
396reverse : String -> String
370reverse = prim__strRev
397reverse = prim__strRev