11 | -----------
12 | -- NATS ---
13 | -----------
15 | ||| Natural numbers: unbounded, unsigned integers which can be pattern matched.
18 | ||| Zero.
19 | Z
25 | -- This is used in the compiler as an efficient substitute for integerToNat.
40 | -- %builtin IntegerToNatural Prelude.Types.integerToNat
42 | -- Define separately so we can spot the name when optimising Nats
43 | ||| Add two natural numbers.
44 | ||| @ x the number to case-split on
45 | ||| @ y the other number
51 | ||| Subtract natural numbers.
52 | ||| If the second number is larger than the first, return 0.
59 | ||| Multiply natural numbers.
72 | -- used for nat hack
83 | -- used for nat hack
99 | -- integer (+) may be non-linear in second
100 | -- argument
102 | -- %builtin NaturalToInteger Prelude.Types.natToInteger
104 | ||| Counts the number of elements that satisfy a predicate.
109 | -----------
110 | -- PAIRS --
111 | -----------
113 | %inline
118 | %inline
125 | %inline
130 | %inline
135 | %inline
142 | %inline
147 | %inline
153 | %inline
158 | -----------
159 | -- MAYBE --
160 | -----------
162 | ||| An optional value. This can be used to represent the possibility of
163 | ||| failure, where a function may return a value, or not.
166 | ||| No value stored
169 | ||| A value of type `ty` is stored
185 | ||| Execute an applicative expression when the Maybe is Just
250 | -----------------
251 | -- EQUIVALENCE --
252 | -----------------
260 | ---------
261 | -- DEC --
262 | ---------
264 | ||| Decidability. A decidable property either holds or is a contradiction.
267 | ||| The case where the property holds.
268 | ||| @ prf the proof
271 | ||| The case where the property holding would be a contradiction.
272 | ||| @ contra a demonstration that prop would be a contradiction
283 | ------------
284 | -- EITHER --
285 | ------------
287 | ||| A sum type.
290 | ||| One possibility of the sum, conventionally used to represent errors.
293 | ||| The other possibility, conventionally used to represent success.
299 | export
304 | export
309 | ||| Simply-typed eliminator for Either.
310 | ||| @ f the action to take on Left
311 | ||| @ g the action to take on Right
312 | ||| @ e the sum to analyze
331 | %inline
337 | %inline
343 | %inline
354 | %inline
360 | %inline
386 | -----------
387 | -- LISTS --
388 | -----------
411 | ||| 'fish': Action of lists on snoc-lists
417 | ||| 'chips': Action of snoc-lists on lists
433 | ||| Filters a snoc-list according to a simple classifying function
439 | ||| Apply a partial function to the elements of a list, keeping the ones at which
440 | ||| it is defined.
448 | ||| Reverse the second snoclist, prepending its elements to the first.
454 | ||| Reverses the given list.
459 | ||| Tail-recursive append. Uses of (++) are automatically transformed to
460 | ||| this. The only reason this is exported is that the proof of equivalence
461 | ||| lives in a different module.
466 | -- Always use tailRecAppend at runtime. Data.SnocList.tailRecAppendIsAppend
467 | -- proves these are equivalent.
470 | ||| Returns the first argument plus the length of the second.
476 | ||| `length` implementation that uses tail recursion. Exported so
477 | ||| lengthTRIsLength can see it.
482 | -- Data.List.lengthTRIsLength proves these are equivalent.
485 | ||| Utility for implementing `mapMaybeTR`
493 | ||| Tail recursive version of `mapMaybe`. This is automatically used
494 | ||| at runtime due to a `transform` rule.
499 | -- Data.List.mapMaybeTRIsMapMaybe proves these are equivalent.
502 | ||| Utility for implementing `filterTR`
510 | ||| Tail recursive version of `filter`. This is automatically used
511 | ||| at runtime due to a `transform` rule.
516 | -- Data.List.listTRIsList proves these are equivalent.
521 | ||| Concatenate one list with another.
527 | ||| Returns the length of the list.
533 | ||| Applied to a predicate and a list, returns the list of those elements that
534 | ||| satisfy the predicate.
543 | ||| Apply a partial function to the elements of a list, keeping the ones at which it is defined.
552 | ||| Reverse the second list, prepending its elements to the first.
558 | ||| Reverses the given list.
563 | ||| Tail-recursive append. Uses of (++) are automatically transformed to
564 | ||| this. The only reason this is exported is that the proof of equivalence
565 | ||| lives in a different module.
570 | -- Always use tailRecAppend at runtime. Data.List.tailRecAppendIsAppend
571 | -- proves these are equivalent.
574 | ||| Returns the first argument plus the length of the second.
580 | ||| `length` implementation that uses tail recursion. Exported so
581 | ||| lengthTRIsLength can see it.
586 | -- Data.List.lengthTRIsLength proves these are equivalent.
594 | ||| Utility for implementing `mapTR`
600 | ||| Tail recursive version of `map`. This is automatically used
601 | ||| at runtime due to a `transform` rule.
606 | -- Data.List.mapTRIsMap proves these are equivalent.
609 | ||| Utility for implementing `mapMaybeTR`
617 | ||| Tail recursive version of `mapMaybe`. This is automatically used
618 | ||| at runtime due to a `transform` rule.
623 | -- Data.List.mapMaybeTRIsMapMaybe proves these are equivalent.
626 | ||| Utility for implementing `filterTR`
634 | ||| Tail recursive version of `filter`. This is automatically used
635 | ||| at runtime due to a `transform` rule.
640 | -- Data.List.listTRIsList proves these are equivalent.
675 | -- tail recursive O(n) implementation of `(>>=)` for `List`
715 | -- This works quickly because when string-concat builds the result, it allocates
716 | -- enough room in advance so there's only one allocation, rather than lots!
717 | --
718 | -- Like fastUnpack, this function won't reduce at compile time.
719 | -- If you need to concatenate strings at compile time, use Prelude.concat.
720 | %foreign
721 | "scheme:string-concat"
722 | "RefC:fastConcat"
723 | "javascript:lambda:(xs)=>__prim_idris2js_array(xs).join('')"
724 | export
729 | ||| Check if something is a member of a list using a custom comparison.
734 | ||| Check if something is a member of a list using the default Boolean equality.
739 | ||| Lookup a value at a given position
740 | export
746 | -------------
747 | -- STREAMS --
748 | -------------
751 | ||| An infinite stream.
762 | ||| The first element of an infinite stream.
767 | ||| All but the first element.
772 | ||| Take precisely n elements from the stream.
773 | ||| @ n how many elements to take
774 | ||| @ xs the stream
780 | -------------
781 | -- STRINGS --
782 | -------------
789 | ||| Returns the length of the string.
790 | |||
791 | ||| ```idris example
792 | ||| length ""
793 | ||| ```
794 | ||| ```idris example
795 | ||| length "ABC"
796 | ||| ```
801 | ||| Reverses the elements within a string.
802 | |||
803 | ||| ```idris example
804 | ||| reverse "ABC"
805 | ||| ```
806 | ||| ```idris example
807 | ||| reverse ""
808 | ||| ```
813 | ||| Returns a substring of a given string
814 | |||
815 | ||| @ index The (zero based) index of the string to extract. If this is beyond
816 | ||| the end of the string, the function returns the empty string.
817 | ||| @ len The desired length of the substring. Truncated if this exceeds the
818 | ||| length of the input
819 | ||| @ subject The string to return a portion of
826 | subj
829 | ||| Adds a character to the front of the specified string.
830 | |||
831 | ||| ```idris example
832 | ||| strCons 'A' "B"
833 | ||| ```
834 | ||| ```idris example
835 | ||| strCons 'A' ""
836 | ||| ```
846 | ||| Turns a list of characters into a string.
852 | %foreign
853 | "scheme:string-pack"
854 | "RefC:fastPack"
855 | "javascript:lambda:(xs)=>__prim_idris2js_array(xs).join('')"
856 | export
859 | -- always use 'fastPack' at run time
862 | ||| Turns a string into a list of characters.
863 | |||
864 | ||| ```idris example
865 | ||| unpack "ABC"
866 | ||| ```
870 | where
877 | -- This function runs fast when compiled but won't compute at compile time.
878 | -- If you need to unpack strings at compile time, use Prelude.unpack.
879 | %foreign
880 | "scheme:string-unpack"
881 | "RefC:fastUnpack"
882 | "javascript:lambda:(str)=>__prim_js2idris_array(Array.from(str))"
883 | export
886 | -- always use 'fastPack' at run time
897 | ----------------
898 | -- CHARACTERS --
899 | ----------------
901 | ||| Returns true if the character is in the range [A-Z].
906 | ||| Returns true if the character is in the range [a-z].
911 | ||| Returns true if the character is in the ranges [A-Z][a-z].
916 | ||| Returns true if the character is in the range [0-9].
921 | ||| Returns true if the character is in the ranges [A-Z][a-z][0-9].
926 | ||| Returns true if the character is a whitespace character.
938 | ||| Returns true if the character represents a new line.
945 | ||| Convert a letter to the corresponding upper-case letter, if any.
946 | ||| Non-letters are ignored.
954 | ||| Convert a letter to the corresponding lower-case letter, if any.
955 | ||| Non-letters are ignored.
963 | ||| Returns true if the character is a hexadecimal digit i.e. in the range
964 | ||| [0-9][a-f][A-F].
969 | ||| Returns true if the character is an octal digit.
974 | ||| Returns true if the character is a control character.
981 | ||| Convert the number to its backend dependent (usually Unicode) Char
982 | ||| equivalent.
987 | ||| Return the backend dependent (usually Unicode) numerical equivalent of the Char.
992 | -----------------------
993 | -- DOUBLE PRIMITIVES --
994 | -----------------------
1064 | ------------
1065 | -- RANGES --
1066 | ------------
1068 | -- These functions are here to support the range syntax:
1069 | -- range expressions like `[a..b]` are desugared to `rangeFromXXX` calls.
1076 | covering
1084 | covering
1100 | -- Idris 1 went to great lengths to prove that these were total. I don't really
1101 | -- think it's worth going to those lengths! Let's keep it simple and assert.
1127 | -- Go down
1129 | -- Meaningless
1131 | -- Go up