module Prelude.Types

import Builtin

import Prelude.Basics

import Prelude.EqOrd

import Prelude.Interfaces

import Prelude.Num

import Prelude.Uninhabited

%default total

-----------

-- NATS ---

-----------

||| Natural numbers: unbounded, unsigned integers which can be pattern matched.

public export

data Nat =

||| Zero.

Z

| ||| Successor.

S Nat

%name Nat k, j, i

-- This is used in the compiler as an efficient substitute for integerToNat.

prim__integerToNat : Integer -> Nat

prim__integerToNat i

= if intToBool (prim__lte_Integer 0 i)

then believe_me i

else Z

public export

integerToNat : Integer -> Nat

integerToNat 0 = Z -- Force evaluation and hence caching of x at compile time

integerToNat x

= if intToBool (prim__lte_Integer x 0)

then Z

else S (assert_total (integerToNat (prim__sub_Integer x 1)))

-- %builtin IntegerToNatural Prelude.Types.integerToNat

-- Define separately so we can spot the name when optimising Nats

||| Add two natural numbers.

||| @ x the number to case-split on

||| @ y the other number

public export

plus : (x : Nat) -> (y : Nat) -> Nat

plus Z y = y

plus (S k) y = S (plus k y)

||| Subtract natural numbers.

||| If the second number is larger than the first, return 0.

public export

minus : (left : Nat) -> Nat -> Nat

minus Z right = Z

minus left Z = left

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

||| Multiply natural numbers.

public export

mult : (x : Nat) -> Nat -> Nat

mult Z y = Z

mult (S k) y = plus y (mult k y)

public export

Num Nat where

(+) = plus

(*) = mult

fromInteger x = integerToNat x

-- used for nat hack

public export

equalNat : (m, n : Nat) -> Bool

equalNat Z Z = True

equalNat (S j) (S k) = equalNat j k

equalNat _ _ = False

public export

Eq Nat where

(==) = equalNat

-- used for nat hack

public export

compareNat : (m, n : Nat) -> Ordering

compareNat Z Z = EQ

compareNat Z (S k) = LT

compareNat (S k) Z = GT

compareNat (S j) (S k) = compareNat j k

public export

Ord Nat where

compare = compareNat

public export

natToInteger : Nat -> Integer

natToInteger Z = 0

natToInteger (S k) = 1 + natToInteger k

-- integer (+) may be non-linear in second

-- argument

-- %builtin NaturalToInteger Prelude.Types.natToInteger

||| Counts the number of elements that satify a predicate.

public export

count : Foldable t => (predicate : a -> Bool) -> t a -> Nat

count predicate = foldMap @{%search} @{Additive} (\x => if predicate x then 1 else 0)

-----------

-- PAIRS --

-----------

%inline

public export

Bifunctor Pair where

bimap f g (x, y) = (f x, g y)

%inline

public export

Bifoldable Pair where

bifoldr f g acc (x, y) = f x (g y acc)

bifoldl f g acc (x, y) = g (f acc x) y

binull _ = False

%inline

public export

Bitraversable Pair where

bitraverse f g (a,b) = [| (,) (f a) (g b) |]

%inline

public export

Functor (Pair a) where

map = mapSnd

%inline

public export

Foldable (Pair a) where

foldr op init (_, x) = x `op` init

foldl op init (_, x) = init `op` x

null _ = False

%inline

public export

Traversable (Pair a) where

traverse f (l, r) = (l,) <$> f r

%inline

public export

Monoid a => Applicative (Pair a) where

pure = (neutral,)

(a1,f) <*> (a2,v) = (a1 <+> a2, f v)

%inline

public export

Monoid a => Monad (Pair a) where

(a1,a) >>= f = let (a2,b) = f a in (a1 <+> a2, b)

-----------

-- MAYBE --

-----------

||| An optional value. This can be used to represent the possibility of

||| failure, where a function may return a value, or not.

public export

data Maybe : (ty : Type) -> Type where

||| No value stored

Nothing : Maybe ty

||| A value of type `ty` is stored

Just : (x : ty) -> Maybe ty

public export

Uninhabited (Nothing = Just x) where

uninhabited Refl impossible

public export

Uninhabited (Just x = Nothing) where

uninhabited Refl impossible

public export

maybe : Lazy b -> Lazy (a -> b) -> Maybe a -> b

maybe n j Nothing = n

maybe n j (Just x) = j x

||| Execute an applicative expression when the Maybe is Just

%inline public export

whenJust : Applicative f => Maybe a -> (a -> f ()) -> f ()

whenJust (Just a) k = k a

whenJust Nothing k = pure ()

public export

Eq a => Eq (Maybe a) where

Nothing == Nothing = True

Nothing == (Just _) = False

(Just _) == Nothing = False

(Just a) == (Just b) = a == b

public export

Ord a => Ord (Maybe a) where

compare Nothing Nothing = EQ

compare Nothing (Just _) = LT

compare (Just _) Nothing = GT

compare (Just a) (Just b) = compare a b

public export

Semigroup (Maybe a) where

Nothing <+> m = m

(Just x) <+> _ = Just x

public export

Monoid (Maybe a) where

neutral = Nothing

public export

Functor Maybe where

map f (Just x) = Just (f x)

map f Nothing = Nothing

public export

Applicative Maybe where

pure = Just

Just f <*> Just a = Just (f a)

_ <*> _ = Nothing

public export

Alternative Maybe where

empty = Nothing

(Just x) <|> _ = Just x

Nothing <|> v = v

public export

Monad Maybe where

Nothing >>= k = Nothing

(Just x) >>= k = k x

public export

Foldable Maybe where

foldr _ z Nothing = z

foldr f z (Just x) = f x z

null Nothing = True

null (Just _) = False

public export

Traversable Maybe where

traverse f Nothing = pure Nothing

traverse f (Just x) = Just <$> f x

-----------------

-- EQUIVALENCE --

-----------------

public export

record (<=>) (a, b : Type) where

constructor MkEquivalence

leftToRight : a -> b

rightToLeft : b -> a

---------

-- DEC --

---------

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

public export

data Dec : Type -> Type where

||| The case where the property holds.

||| @ prf the proof

Yes : (prf : prop) -> Dec prop

||| The case where the property holding would be a contradiction.

||| @ contra a demonstration that prop would be a contradiction

No : (contra : Not prop) -> Dec prop

export Uninhabited (Yes p === No q) where uninhabited eq impossible

export Uninhabited (No p === Yes q) where uninhabited eq impossible

public export

viaEquivalence : a <=> b -> Dec a -> Dec b

viaEquivalence f (Yes a) = Yes (f .leftToRight a)

viaEquivalence f (No na) = No (na . f .rightToLeft)

------------

-- EITHER --

------------

||| A sum type.

public export

data Either : (a : Type) -> (b : Type) -> Type where

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

Left : forall a, b. (x : a) -> Either a b

||| The other possibility, conventionally used to represent success.

Right : forall a, b. (x : b) -> Either a b

export Uninhabited (Left p === Right q) where uninhabited eq impossible

export Uninhabited (Right p === Left q) where uninhabited eq impossible

export

Either (Uninhabited a) (Uninhabited b) => Uninhabited (a, b) where

uninhabited (x, _) @{Left _} = uninhabited x

uninhabited (_, y) @{Right _} = uninhabited y

export

Uninhabited a => Uninhabited b => Uninhabited (Either a b) where

uninhabited (Left l) = uninhabited l

uninhabited (Right r) = uninhabited r

||| Simply-typed eliminator for Either.

||| @ f the action to take on Left

||| @ g the action to take on Right

||| @ e the sum to analyze

public export

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

either l r (Left x) = l x

either l r (Right x) = r x

public export

(Eq a, Eq b) => Eq (Either a b) where

Left x == Left x' = x == x'

Right x == Right x' = x == x'

_ == _ = False

public export

(Ord a, Ord b) => Ord (Either a b) where

compare (Left x) (Left x') = compare x x'

compare (Left _) (Right _) = LT

compare (Right _) (Left _) = GT

compare (Right x) (Right x') = compare x x'

%inline

public export

Functor (Either e) where

map f (Left x) = Left x

map f (Right x) = Right (f x)

%inline

public export

Bifunctor Either where

bimap f _ (Left x) = Left (f x)

bimap _ g (Right y) = Right (g y)

%inline

public export

Bifoldable Either where

bifoldr f _ acc (Left a) = f a acc

bifoldr _ g acc (Right b) = g b acc

bifoldl f _ acc (Left a) = f acc a

bifoldl _ g acc (Right b) = g acc b

binull _ = False

%inline

public export

Bitraversable Either where

bitraverse f _ (Left a) = Left <$> f a

bitraverse _ g (Right b) = Right <$> g b

%inline

public export

Applicative (Either e) where

pure = Right

(Left a) <*> _ = Left a

(Right f) <*> (Right r) = Right (f r)

(Right _) <*> (Left l) = Left l

public export

Monad (Either e) where

(Left n) >>= _ = Left n

(Right r) >>= f = f r

public export

Foldable (Either e) where

foldr f acc (Left _) = acc

foldr f acc (Right x) = f x acc

null (Left _) = True

null (Right _) = False

public export

Traversable (Either e) where

traverse f (Left x) = pure (Left x)

traverse f (Right x) = Right <$> f x

-----------

-- LISTS --

-----------

public export

Eq a => Eq (List a) where

[] == [] = True

x :: xs == y :: ys = x == y && xs == ys

_ == _ = False

public export

Ord a => Ord (List a) where

compare [] [] = EQ

compare [] (x :: xs) = LT

compare (x :: xs) [] = GT

compare (x :: xs) (y ::ys)

= case compare x y of

EQ => compare xs ys

c => c

namespace SnocList

export infixl 7 <><

export infixr 6 <>>

||| 'fish': Action of lists on snoc-lists

public export

(<><) : SnocList a -> List a -> SnocList a

sx <>< [] = sx

sx <>< (x :: xs) = sx :< x <>< xs

||| 'chips': Action of snoc-lists on lists

public export

(<>>) : SnocList a -> List a -> List a

Lin <>> xs = xs

(sx :< x) <>> xs = sx <>> x :: xs

public export

(++) : (sx, sy : SnocList a) -> SnocList a

(++) sx Lin = sx

(++) sx (sy :< y) = (sx ++ sy) :< y

public export

length : SnocList a -> Nat

length Lin = Z

length (sx :< x) = S $ length sx

||| Filters a snoc-list according to a simple classifying function

public export

filter : (a -> Bool) -> SnocList a -> SnocList a

filter f [<] = [<]

filter f (xs:<x) = let rest = filter f xs in if f x then rest :< x else rest

||| Apply a partial function to the elements of a list, keeping the ones at which

||| it is defined.

public export

mapMaybe : (a -> Maybe b) -> SnocList a -> SnocList b

mapMaybe f [<] = [<]

mapMaybe f (sx :< x) = case f x of

Nothing => mapMaybe f sx

Just j => mapMaybe f sx :< j

||| Reverse the second snoclist, prepending its elements to the first.

public export

reverseOnto : SnocList a -> SnocList a -> SnocList a

reverseOnto acc Lin = acc

reverseOnto acc (sx :< x) = reverseOnto (acc :< x) sx

||| Reverses the given list.

public export

reverse : SnocList a -> SnocList a

reverse = reverseOnto Lin

||| Tail-recursive append. Uses of (++) are automatically transformed to

||| this. The only reason this is exported is that the proof of equivalence

||| lives in a different module.

public export

tailRecAppend : (sx, sy : SnocList a) -> SnocList a

tailRecAppend sx sy = reverseOnto sx (reverse sy)

-- Always use tailRecAppend at runtime. Data.SnocList.tailRecAppendIsAppend

-- proves these are equivalent.

%transform "tailRecAppendSnocList" SnocList.(++) = SnocList.tailRecAppend

||| Returns the first argument plus the length of the second.

public export

lengthPlus : Nat -> SnocList a -> Nat

lengthPlus n Lin = n

lengthPlus n (sx :< _) = lengthPlus (S n) sx

||| `length` implementation that uses tail recursion. Exported so

||| lengthTRIsLength can see it.

public export

lengthTR : SnocList a -> Nat

lengthTR = lengthPlus Z

-- Data.List.lengthTRIsLength proves these are equivalent.

%transform "tailRecLengthSnocList" SnocList.length = SnocList.lengthTR

||| Utility for implementing `mapMaybeTR`

public export

mapMaybeAppend : List b -> (a -> Maybe b) -> SnocList a -> SnocList b

mapMaybeAppend xs f (sx :< x) = case f x of

Just v => mapMaybeAppend (v :: xs) f sx

Nothing => mapMaybeAppend xs f sx

mapMaybeAppend xs f Lin = Lin <>< xs

||| Tail recursive version of `mapMaybe`. This is automatically used

||| at runtime due to a `transform` rule.

public export %inline

mapMaybeTR : (a -> Maybe b) -> SnocList a -> SnocList b

mapMaybeTR = mapMaybeAppend []

-- Data.List.mapMaybeTRIsMapMaybe proves these are equivalent.

%transform "tailRecMapMaybeSnocList" SnocList.mapMaybe = SnocList.mapMaybeTR

||| Utility for implementing `filterTR`

public export

filterAppend : List a -> (a -> Bool) -> SnocList a -> SnocList a

filterAppend xs f (sx :< x) = case f x of

True => filterAppend (x :: xs) f sx

False => filterAppend xs f sx

filterAppend xs f Lin = Lin <>< xs

||| Tail recursive version of `filter`. This is automatically used

||| at runtime due to a `transform` rule.

public export %inline

filterTR : (a -> Bool) -> SnocList a -> SnocList a

filterTR = filterAppend []

-- Data.List.listTRIsList proves these are equivalent.

%transform "tailRecFilterSnocList" SnocList.filter = SnocList.filterTR

namespace List

||| Concatenate one list with another.

public export

(++) : (xs, ys : List a) -> List a

[] ++ ys = ys

(x :: xs) ++ ys = x :: xs ++ ys

||| Returns the length of the list.

public export

length : List a -> Nat

length [] = Z

length (x :: xs) = S (length xs)

||| Applied to a predicate and a list, returns the list of those elements that

||| satisfy the predicate.

public export

filter : (p : a -> Bool) -> List a -> List a

filter p [] = []

filter p (x :: xs)

= if p x

then x :: filter p xs

else filter p xs

||| Apply a partial function to the elements of a list, keeping the ones at which it is defined.

public export

mapMaybe : (a -> Maybe b) -> List a -> List b

mapMaybe f [] = []

mapMaybe f (x::xs) =

case f x of

Nothing => mapMaybe f xs

Just j => j :: mapMaybe f xs

||| Reverse the second list, prepending its elements to the first.

public export

reverseOnto : List a -> List a -> List a

reverseOnto acc [] = acc

reverseOnto acc (x::xs) = reverseOnto (x::acc) xs

||| Reverses the given list.

public export

reverse : List a -> List a

reverse = reverseOnto []

||| Tail-recursive append. Uses of (++) are automatically transformed to

||| this. The only reason this is exported is that the proof of equivalence

||| lives in a different module.

public export

tailRecAppend : (xs, ys : List a) -> List a

tailRecAppend xs ys = reverseOnto ys (reverse xs)

-- Always use tailRecAppend at runtime. Data.List.tailRecAppendIsAppend

-- proves these are equivalent.

%transform "tailRecAppend" List.(++) = List.tailRecAppend

||| Returns the first argument plus the length of the second.

public export

lengthPlus : Nat -> List a -> Nat

lengthPlus n [] = n

lengthPlus n (x::xs) = lengthPlus (S n) xs

||| `length` implementation that uses tail recursion. Exported so

||| lengthTRIsLength can see it.

public export

lengthTR : List a -> Nat

lengthTR = lengthPlus Z

-- Data.List.lengthTRIsLength proves these are equivalent.

%transform "tailRecLength" List.length = List.lengthTR

public export

mapImpl : (a -> b) -> List a -> List b

mapImpl f [] = []

mapImpl f (x :: xs) = f x :: mapImpl f xs

||| Utility for implementing `mapTR`

public export

mapAppend : SnocList b -> (a -> b) -> List a -> List b

mapAppend sx f (x :: xs) = mapAppend (sx :< f x) f xs

mapAppend sx f [] = sx <>> []

||| Tail recursive version of `map`. This is automatically used

||| at runtime due to a `transform` rule.

public export %inline

mapTR : (a -> b) -> List a -> List b

mapTR = mapAppend Lin

-- Data.List.mapTRIsMap proves these are equivalent.

%transform "tailRecMap" mapImpl = List.mapTR

||| Utility for implementing `mapMaybeTR`

public export

mapMaybeAppend : SnocList b -> (a -> Maybe b) -> List a -> List b

mapMaybeAppend sx f (x :: xs) = case f x of

Just v => mapMaybeAppend (sx :< v) f xs

Nothing => mapMaybeAppend sx f xs

mapMaybeAppend sx f [] = sx <>> []

||| Tail recursive version of `mapMaybe`. This is automatically used

||| at runtime due to a `transform` rule.

public export %inline

mapMaybeTR : (a -> Maybe b) -> List a -> List b

mapMaybeTR = mapMaybeAppend Lin

-- Data.List.mapMaybeTRIsMapMaybe proves these are equivalent.

%transform "tailRecMapMaybe" List.mapMaybe = List.mapMaybeTR

||| Utility for implementing `filterTR`

public export

filterAppend : SnocList a -> (a -> Bool) -> List a -> List a

filterAppend sx f (x :: xs) = case f x of

True => filterAppend (sx :< x) f xs

False => filterAppend sx f xs

filterAppend sx f [] = sx <>> []

||| Tail recursive version of `filter`. This is automatically used

||| at runtime due to a `transform` rule.

public export %inline

filterTR : (a -> Bool) -> List a -> List a

filterTR = filterAppend Lin

-- Data.List.listTRIsList proves these are equivalent.

%transform "tailRecFilter" List.filter = List.filterTR

public export %inline

Functor List where

map = mapImpl

public export

Semigroup (List a) where

(<+>) = (++)

public export

Monoid (List a) where

neutral = []

public export

Foldable List where

foldr c n [] = n

foldr c n (x::xs) = c x (foldr c n xs)

foldl f q [] = q

foldl f q (x::xs) = foldl f (f q x) xs

null [] = True

null (_::_) = False

toList = id

foldMap f = foldl (\acc, elem => acc <+> f elem) neutral

public export

listBindOnto : (a -> List b) -> List b -> List a -> List b

listBindOnto f xs [] = reverse xs

listBindOnto f xs (y :: ys) = listBindOnto f (reverseOnto xs (f y)) ys

-- tail recursive O(n) implementation of `(>>=)` for `List`

public export

listBind : List a -> (a -> List b) -> List b

listBind as f = listBindOnto f Nil as

public export

Applicative List where

pure x = [x]

fs <*> vs = listBind fs (\f => map f vs)

public export

Alternative List where

empty = []

xs <|> ys = xs ++ ys

public export

Monad List where

(>>=) = listBind

public export

Traversable List where

traverse f [] = pure []

traverse f (x::xs) = [| f x :: traverse f xs |]

public export

Eq a => Eq (SnocList a) where

(==) Lin Lin = True

(==) (sx :< x) (sy :< y) = x == y && sx == sy

(==) _ _ = False

public export

Ord a => Ord (SnocList a) where

compare Lin Lin = EQ

compare Lin (sx :< x) = LT

compare (sx :< x) Lin = GT

compare (sx :< x) (sy :< y)

= case compare sx sy of

EQ => compare x y

c => c

-- This works quickly because when string-concat builds the result, it allocates

-- enough room in advance so there's only one allocation, rather than lots!

--

-- Like fastUnpack, this function won't reduce at compile time.

-- If you need to concatenate strings at compile time, use Prelude.concat.

%foreign

"scheme:string-concat"

"RefC:fastConcat"

"javascript:lambda:(xs)=>__prim_idris2js_array(xs).join('')"

export

fastConcat : List String -> String

%transform "fastConcat" concat {t = List} {a = String} = fastConcat

||| Check if something is a member of a list using a custom comparison.

public export

elemBy : Foldable t => (a -> a -> Bool) -> a -> t a -> Bool

elemBy p e = any (p e)

||| Check if something is a member of a list using the default Boolean equality.

public export

elem : Foldable t => Eq a => a -> t a -> Bool

elem = elemBy (==)

||| Lookup a value at a given position

export

getAt : Nat -> List a -> Maybe a

getAt Z (x :: xs) = Just x

getAt (S k) (x :: xs) = getAt k xs

getAt _ [] = Nothing

-------------

-- STREAMS --

-------------

namespace Stream

||| An infinite stream.

public export

data Stream : Type -> Type where

(::) : a -> Inf (Stream a) -> Stream a

%name Stream xs, ys, zs

public export

Functor Stream where

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

||| The first element of an infinite stream.

public export

head : Stream a -> a

head (x :: xs) = x

||| All but the first element.

public export

tail : Stream a -> Stream a

tail (x :: xs) = xs

||| Take precisely n elements from the stream.

||| @ n how many elements to take

||| @ xs the stream

public export

take : (n : Nat) -> (xs : Stream a) -> List a

take Z xs = []

take (S k) (x :: xs) = x :: take k xs

-------------

-- STRINGS --

-------------

namespace String

public export

(++) : (x : String) -> (y : String) -> String

x ++ y = prim__strAppend x y

||| Returns the length of the string.

|||

||| ```idris example

||| length ""

||| ```

||| ```idris example

||| length "ABC"

||| ```

public export

length : String -> Nat

length str = fromInteger (prim__cast_IntInteger (prim__strLength str))

||| Reverses the elements within a string.

|||

||| ```idris example

||| reverse "ABC"

||| ```

||| ```idris example

||| reverse ""

||| ```

public export

reverse : String -> String

reverse = prim__strReverse

||| Returns a substring of a given string

|||

||| @ index The (zero based) index of the string to extract. If this is beyond

||| the end of the string, the function returns the empty string.

||| @ len The desired length of the substring. Truncated if this exceeds the

||| length of the input

||| @ subject The string to return a portion of

public export

substr : (index : Nat) -> (len : Nat) -> (subject : String) -> String

substr s e subj

= if natToInteger s < natToInteger (length subj)

then prim__strSubstr (prim__cast_IntegerInt (natToInteger s))

(prim__cast_IntegerInt (natToInteger e))

subj

else ""

||| Adds a character to the front of the specified string.

|||

||| ```idris example

||| strCons 'A' "B"

||| ```

||| ```idris example

||| strCons 'A' ""

||| ```

public export

strCons : Char -> String -> String

strCons = prim__strCons

public export

strUncons : String -> Maybe (Char, String)

strUncons "" = Nothing

strUncons str = assert_total $ Just (prim__strHead str, prim__strTail str)

||| Turns a list of characters into a string.

public export

pack : List Char -> String

pack [] = ""

pack (x :: xs) = strCons x (pack xs)

%foreign

"scheme:string-pack"

"RefC:fastPack"

"javascript:lambda:(xs)=>__prim_idris2js_array(xs).join('')"

export

fastPack : List Char -> String

-- always use 'fastPack' at run time

%transform "fastPack" pack = fastPack

||| Turns a string into a list of characters.

|||

||| ```idris example

||| unpack "ABC"

||| ```

public export

unpack : String -> List Char

unpack str = unpack' (prim__cast_IntegerInt (natToInteger (length str)) - 1) str []

where

unpack' : Int -> String -> List Char -> List Char

unpack' pos str acc

= if pos < 0

then acc

else unpack' (assert_smaller pos (pos - 1)) str $ (assert_total $ prim__strIndex str pos) :: acc

-- This function runs fast when compiled but won't compute at compile time.

-- If you need to unpack strings at compile time, use Prelude.unpack.

%foreign

"scheme:string-unpack"

"RefC:fastUnpack"

"javascript:lambda:(str)=>__prim_js2idris_array(Array.from(str))"

export

fastUnpack : String -> List Char

-- always use 'fastPack' at run time

%transform "fastUnpack" unpack = fastUnpack

public export

Semigroup String where

(<+>) = (++)

public export

Monoid String where

neutral = ""

----------------

-- CHARACTERS --

----------------

||| Returns true if the character is in the range [A-Z].

public export

isUpper : Char -> Bool

isUpper x = x >= 'A' && x <= 'Z'

||| Returns true if the character is in the range [a-z].

public export

isLower : Char -> Bool

isLower x = x >= 'a' && x <= 'z'

||| Returns true if the character is in the ranges [A-Z][a-z].

public export

isAlpha : Char -> Bool

isAlpha x = isUpper x || isLower x

||| Returns true if the character is in the range [0-9].

public export

isDigit : Char -> Bool

isDigit x = (x >= '0' && x <= '9')

||| Returns true if the character is in the ranges [A-Z][a-z][0-9].

public export

isAlphaNum : Char -> Bool

isAlphaNum x = isDigit x || isAlpha x

||| Returns true if the character is a whitespace character.

public export

isSpace : Char -> Bool

isSpace ' ' = True

isSpace '\t' = True

isSpace '\r' = True

isSpace '\n' = True

isSpace '\f' = True

isSpace '\v' = True

isSpace '\xa0' = True

isSpace _ = False

||| Returns true if the character represents a new line.

public export

isNL : Char -> Bool

isNL '\r' = True

isNL '\n' = True

isNL _ = False

||| Convert a letter to the corresponding upper-case letter, if any.

||| Non-letters are ignored.

public export

toUpper : Char -> Char

toUpper x

= if (isLower x)

then prim__cast_IntChar (prim__cast_CharInt x - 32)

else x

||| Convert a letter to the corresponding lower-case letter, if any.

||| Non-letters are ignored.

public export

toLower : Char -> Char

toLower x

= if (isUpper x)

then prim__cast_IntChar (prim__cast_CharInt x + 32)

else x

||| Returns true if the character is a hexadecimal digit i.e. in the range

||| [0-9][a-f][A-F].

public export

isHexDigit : Char -> Bool

isHexDigit x = isDigit x || ('a' <= x && x <= 'f') || ('A' <= x && x <= 'F')

||| Returns true if the character is an octal digit.

public export

isOctDigit : Char -> Bool

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

||| Returns true if the character is a control character.

public export

isControl : Char -> Bool

isControl x

= (x >= '\x0000' && x <= '\x001f')

|| (x >= '\x007f' && x <= '\x009f')

||| Convert the number to its backend dependent (usually Unicode) Char

||| equivalent.

public export

chr : Int -> Char

chr = prim__cast_IntChar

||| Return the backend dependent (usually Unicode) numerical equivalent of the Char.

public export

ord : Char -> Int

ord = prim__cast_CharInt

-----------------------

-- DOUBLE PRIMITIVES --

-----------------------

public export

pi : Double

pi = 3.14159265358979323846