text:
= Poly : Polymorphism and Higher-Order Functions

> module Poly

> import Basics

> %hide Prelude.List.length
> %hide Prelude.List.filter
> %hide Prelude.List.partition
> %hide Prelude.Functor.map
> %hide Prelude.Nat.pred
> %hide Basics.Playground2.plus

> %access public export

> %default total

== Polymorphism

In this chapter we continue our development of basic concepts of functional
programming. The critical new ideas are _polymorphism_ (abstracting functions
over the types of the data they manipulate) and _higher-order functions_
(treating functions as data). We begin with polymorphism.

=== Polymorphic Lists

For the last couple of chapters, we've been working just with lists of numbers.
Obviously, interesting programs also need to be able to manipulate lists with
elements from other types -- lists of strings, lists of booleans, lists of
lists, etc. We _could_ just define a new inductive datatype for each of these,
for example...

> data BoolList : Type where
>   BoolNil : BoolList
>   BoolCons : Bool -> BoolList -> BoolList

... but this would quickly become tedious, partly because we have to make up
different constructor names for each datatype, but mostly because we would also
need to define new versions of all our list manipulating functions
(\idr{length}, \idr{rev}, etc.) for each new datatype definition.

To avoid all this repetition, Idris supports _polymorphic_ inductive type
definitions. For example, here is a _polymorphic list_ datatype.

```idris
data List : (x : Type) -> Type where
  Nil : List x
  Cons : x -> List x -> List x
```

(This type is already defined in Idris' standard library, but the \idr{Cons}
constructor is named \idr{(::)}).

This is exactly like the definition of \idr{NatList} from the previous chapter,
except that the \idr{Nat} argument to the \idr{Cons} constructor has been
replaced by an arbitrary type \idr{x}, a binding for \idr{x} has been added to
the header, and the occurrences of \idr{NatList} in the types of the
constructors have been replaced by \idr{List x}. (We can re-use the constructor
names \idr{Nil} and \idr{Cons} because the earlier definition of \idr{NatList}
was inside of a \idr{namespace} definition that is now out of scope.)

What sort of thing is \idr{List} itself? One good way to think about it is that
\idr{List} is a _function_ from \idr{Type}s to inductive definitions; or, to put
it another way, \idr{List} is a function from \idr{Type}s to \idr{Type}s. For
any particular type \idr{x}, the type \idr{List x} is an inductively defined set
of lists whose elements are of type \idr{x}.

With this definition, when we use the constructors \idr{Nil} and \idr{Cons} to
build lists, we need to tell Idris the type of the elements in the lists we are
building -- that is, \idr{Nil} and \idr{Cons} are now _polymorphic
constructors_. Observe the types of these constructors:

```idris
λΠ> :t Nil
Prelude.List.Nil : List elem
λΠ> :t (::)
Prelude.List.(::) : elem -> List elem -> List elem
```

\todo[inline]{How to edit these 3 paragraphs? Implicits are defined later in
this chapter, and Idris doesn't require type parameters to constructors}

(Side note on notation: In .v files, the "forall" quantifier is spelled out in
letters. In the generated HTML files and in the way various IDEs show .v files
(with certain settings of their display controls), ∀ is usually typeset as the
usual mathematical "upside down A," but you'll still see the spelled-out
"forall" in a few places. This is just a quirk of typesetting: there is no
difference in meaning.)

The "∀ X" in these types can be read as an additional argument to the
constructors that determines the expected types of the arguments that follow.
When \idr{Nil} and \idr{Cons} are used, these arguments are supplied in the same
way as the others. For example, the list containing \idr{2} and \idr{1} is
written like this:

Check (cons nat 2 (cons nat 1 (nil nat))).

(We've written \idr{Nil} and \idr{Cons} explicitly here because we haven't yet
defined the \idr{[]} and \idr{::} notations for the new version of lists. We'll
do that in a bit.)

We can now go back and make polymorphic versions of all the list-processing
functions that we wrote before. Here is \idr{repeat}, for example:

> repeat : (x_ty : Type) -> (x : x_ty) -> (count : Nat) -> List x_ty
> repeat x_ty x Z = Nil
> repeat x_ty x (S count') = x :: repeat x_ty x count'

As with \idr{Nil} and \idr{Cons}, we can use \idr{repeat} by applying it first
to a type and then to its list argument:

> test_repeat1 : repeat Nat 4 2 = 4 :: (4 :: Nil)
> test_repeat1 = Refl

To use \idr{repeat} to build other kinds of lists, we simply instantiate it with
an appropriate type parameter:

> test_repeat2 : repeat Bool False 1 = False :: Nil
> test_repeat2 = Refl

==== Exercise: 2 stars (mumble_grumble)

\ \todo[inline]{Explain implicits and \idr{{x=foo}} syntax first? Move after the
"Supplying Type Arguments Explicitly" section?}

> namespace MumbleGrumble

Consider the following two inductively defined types.

>   data Mumble : Type where
>     A : Mumble
>     B : Mumble -> Nat -> Mumble
>     C : Mumble

>   data Grumble : (x : Type) -> Type where
>     D : Mumble -> Grumble x
>     E : x -> Grumble x

Which of the following are well-typed elements of \idr{Grumble x} for some type
\idr{x}?

  - \idr{D (B A 5)}
  - \idr{D (B A 5) {x=Mumble}}
  - \idr{D (B A 5) {x=Bool}}
  - \idr{E True {x=Bool}}
  - \idr{E (B C 0) {x=Mumble}}
  - \idr{E (B C 0) {x=Bool}}
  - \idr{C}

> -- FILL IN HERE

$\square$

\todo[inline]{Merge 3 following sections into one about Idris implicits? Mention
the lowercase/uppercase distinction.}

==== Type Annotation Inference

\todo[inline]{This has already happened earlier at \idr{repeat}, delete most of
this?}

Let's write the definition of \idr{repeat} again, but this time we won't specify
the types of any of the arguments. Will Idris still accept it?

Fixpoint repeat' X x count : list X :=
  match count with | 0 ⇒ nil X | S count' ⇒ cons X x (repeat' X x count') end.

Indeed it will. Let's see what type Idris has assigned to \idr{repeat'}:

Check repeat'. (* ===> forall X : Type, X -> nat -> list X *) Check repeat. (*
===> forall X : Type, X -> nat -> list X *)

It has exactly the same type type as \idr{repeat}. Idris was able to use _type
inference_ to deduce what the types of \idr{X}, \idr{x}, and \idr{count} must
be, based on how they are used. For example, since \idr{X} is used as an
argument to \idr{Cons}, it must be a \idr{Type}, since \idr{Cons} expects a
\idr{Type} as its first argument; matching \idr{count} with \idr{Z} and \idr{S}
means it must be a \idr{Nat}; and so on.

This powerful facility means we don't always have to write explicit type
annotations everywhere, although explicit type annotations are still quite
useful as documentation and sanity checks, so we will continue to use them most
of the time. You should try to find a balance in your own code between too many
type annotations (which can clutter and distract) and too few (which forces
readers to perform type inference in their heads in order to understand your
code).

==== Type Argument Synthesis

\todo[inline]{We should mention the \idr{_} parameters but it won't work like
this in Idris}

To use a polymorphic function, we need to pass it one or more types in addition
to its other arguments. For example, the recursive call in the body of the
\idr{repeat} function above must pass along the type \idr{x_ty}. But since the
second argument to \idr{repeat} is an element of \idr{x_ty}, it seems entirely
obvious that the first argument can only be \idr{x_ty} — why should we have to
write it explicitly?

Fortunately, Idris permits us to avoid this kind of redundancy. In place of any
type argument we can write the "implicit argument" \idr{_}, which can be read as
"Please try to figure out for yourself what belongs here." More precisely, when
Idris encounters a \idr{_}, it will attempt to _unify_ all locally available
information -- the type of the function being applied, the types of the other
arguments, and the type expected by the context in which the application appears
-- to determine what concrete type should replace the \idr{_}.

This may sound similar to type annotation inference -- indeed, the two
procedures rely on the same underlying mechanisms. Instead of simply omitting
the types of some arguments to a function, like

      repeat' X x count : list X :=

we can also replace the types with \idr{_}

      repeat' (X : _) (x : _) (count : _) : list X :=

to tell Idris to attempt to infer the missing information.

Using implicit arguments, the \idr{count} function can be written like this:

Fixpoint repeat'' X x count : list X :=
  match count with | 0 ⇒ nil _ | S count' ⇒ cons _ x (repeat'' _ x count') end.

In this instance, we don't save much by writing \idr{_} instead of \idr{x}. But
in many cases the difference in both keystrokes and readability is nontrivial.
For example, suppose we want to write down a list containing the numbers
\idr{1}, \idr{2}, and \idr{3}. Instead of writing this...

Definition list123 :=
  cons nat 1 (cons nat 2 (cons nat 3 (nil nat))).

...we can use argument synthesis to write this:

Definition list123' :=
  cons _ 1 (cons _ 2 (cons _ 3 (nil _))).

==== Implicit Arguments

We can go further and even avoid writing \idr{_}'s in most cases by telling
Idris _always_ to infer the type argument(s) of a given function. The Arguments
directive specifies the name of the function (or constructor) and then lists its
argument names, with curly braces around any arguments to be treated as
implicit. (If some arguments of a definition don't have a name, as is often the
case for constructors, they can be marked with a wildcard pattern \idr{_}.)

Arguments nil {X}. Arguments cons {X} _ _. Arguments repeat {X} x count.

Now, we don't have to supply type arguments at all:

Definition list123'' := cons 1 (cons 2 (cons 3 nil)).

Alternatively, we can declare an argument to be implicit when defining the
function itself, by surrounding it in curly braces instead of parens. For
example:

> repeat' : {x_ty : Type} -> (x : x_ty) -> (count : Nat) -> List x_ty
> repeat' x Z = Nil
> repeat' x (S count') = x :: repeat' x count'

(Note that we didn't even have to provide a type argument to the recursive call
to \idr{repeat'}; indeed, it would be invalid to provide one!)

We will use the latter style whenever possible, but we will continue to use
explicit declarations in data types. The reason for this is that marking the
parameter of an inductive type as implicit causes it to become implicit for the
type itself, not just for its constructors. For instance, consider the following
alternative definition of the \idr{List} type:

> data List' : {x : Type} -> Type where
>   Nil' : List'
>   Cons' : x -> List' -> List'

Because \idr{x} is declared as implicit for the _entire_ inductive definition
including \idr{List'} itself, we now have to write just \idr{List'} whether we
are talking about lists of numbers or booleans or anything else, rather than
\idr{List' Nat} or \idr{List' Bool} or whatever; this is a step too far.

\todo[inline]{Added the implicit inference explanation here}

There's another step towards conciseness that we can take in Idris -- drop the
implicit argument completely in function definitions! Idris will automatically
insert them for us when it encounters unknown variables. _Note that by
convention this will only happen for variables starting on a lowercase letter_.

> repeat'' : (x : x_ty) -> (count : Nat) -> List x_ty
> repeat'' x Z = Nil
> repeat'' x (S count') = x :: repeat'' x count'

Let's finish by re-implementing a few other standard list functions on our new
polymorphic lists...

> app : (l1, l2 : List x) -> List x
> app Nil l2 = l2
> app (h::t) l2 = h :: app t l2

> rev : (l : List x) -> List x
> rev [] = []
> rev (h::t) = app (rev t) (h::Nil)

> length : (l : List x) -> Nat
> length [] = Z
> length (_::l') = S (length l')

> test_rev1 : rev (1::2::[]) = 2::1::[]
> test_rev1 = Refl

> test_rev2 : rev (True::[]) = True::[]
> test_rev2 = Refl

> test_length1 : length (1::2::3::[]) = 3
> test_length1 = Refl

==== Supplying Type Arguments Explicitly

One small problem with declaring arguments implicit is that, occasionally, Idris
does not have enough local information to determine a type argument; in such
cases, we need to tell Idris that we want to give the argument explicitly just
this time. For example, suppose we write this:

```idris
λΠ> :let mynil = Nil
(input):Can't infer argument elem to []
```

Here, Idris gives us an error because it doesn't know what type argument to
supply to \idr{Nil}. We can help it by providing an explicit type declaration
via \idr{the} function (so that Idris has more information available when it
gets to the "application" of \idr{Nil}):

```idris
λΠ> :let mynil = the (List Nat) Nil
```

Alternatively, we can force the implicit arguments to be explicit by supplying
them as arguments in curly braces.

```idris
λΠ> :let mynil' = Nil {elem=Nat}
```

\todo[inline]{Describe here how to bring variables from the type into definition
scope via implicits?}

\todo[inline]{Explain that Idris has built-in notation for lists instead?}

Using argument synthesis and implicit arguments, we can define convenient
notation for lists, as before. Since we have made the constructor type arguments
implicit, Coq will know to automatically infer these when we use the notations.

Notation "x :: y" := (cons x y)
                     (at level 60, right associativity).
Notation "[ ]" := nil. Notation "[ x ; .. ; y ]" := (cons x .. (cons y []) ..).
Notation "x ++ y" := (app x y)
                     (at level 60, right associativity).

Now lists can be written just the way we'd hope:

> list123''' : List Nat
> list123''' = [1, 2, 3]

==== Exercise: 2 stars, optional (poly_exercises)

Here are a few simple exercises, just like ones in the \idr{Lists} chapter, for
practice with polymorphism. Complete the proofs below.

> app_nil_r : (l : List x) -> l ++ [] = l
> app_nil_r l = ?app_nil_r_rhs

> app_assoc : (l, m, n : List a) -> l ++ m ++ n = (l ++ m) ++ n
> app_assoc l m n = ?app_assoc_rhs

> app_length : (l1, l2 : List x) -> length (l1 ++ l2) = length l1 + length l2
> app_length l1 l2 = ?app_length_rhs

$\square$

==== Exercise: 2 stars, optional (more_poly_exercises)

Here are some slightly more interesting ones...

> rev_app_distr : (l1, l2 : List x) -> rev (l1 ++ l2) = rev l2 ++ rev l1
> rev_app_distr l1 l2 = ?rev_app_distr_rhs

> rev_involutive : (l : List x) -> rev (rev l) = l
> rev_involutive l = ?rev_involutive_rhs

$\square$

=== Polymorphic Pairs

Following the same pattern, the type definition we gave in the last chapter for
pairs of numbers can be generalized to _polymorphic pairs_, often called
_products_:

> data Prod : (x, y : Type) -> Type where
>   PPair : x -> y -> Prod x y

As with lists, we make the type arguments implicit and define the familiar
concrete notation.

\todo[inline]This sugar cannot be marked as private and messes up things when
imported, consider changing the notation}

> syntax "(" [x] "," [y] ")" = PPair x y

We can also use the \idr{syntax} mechanism to define the standard notation for
product _types_:

> syntax [x_ty] "*" [y_ty] = Prod x_ty y_ty

(The annotation : type_scope tells Coq that this abbreviation should only be
used when parsing types. This avoids a clash with the multiplication symbol.)

It is easy at first to get \idr{(x,y)} and \idr{x_ty*y_ty} confused. Remember
that \idr{(x,y)} is a value built from two other values, while \idr{x_ty*y_ty}
is a type built from two other types. If \idr{x} has type \idr{x_ty} and \idr{y}
has type \idr{y_ty}, then \idr{(x,y)} has type \idr{x_ty*y_ty}.

The first and second projection functions now look pretty much as they would in
any functional programming language.

> fst : (p : x*y) -> x
> fst (x,y) = x

> snd : (p : x*y) -> y
> snd (x,y) = y

\todo[inline]{Edit}

The following function takes two lists and combines them into a list of pairs.
In functional languages, it is usually called \idr{zip} (though the Coq's
standard library calls it \idr{combine}).

> zip : (lx : List x) -> (ly : List y) -> List (x*y)
> zip [] _ = []
> zip _ [] = []
> zip (x::tx) (y::ty) = (x,y) :: zip tx ty

==== Exercise: 1 star, optional (combine_checks)

Try answering the following questions on paper and checking your answers in
Idris:

- What is the type of \idr{zip} (i.e., what does \idr{:t zip} print?)

- What does \idr{combine [1,2] [False,False,True,True]} print?

$\square$

==== Exercise: 2 stars, recommended (split)

The function \idr{split} is the right inverse of \idr{zip}: it takes a list of
pairs and returns a pair of lists. In many functional languages, it is called
\idr{unzip}.

Fill in the definition of \idr{split} below. Make sure it passes the given unit
test.

> split : (l : List (x*y)) -> (List x) * (List y)
> split l = ?split_rhs

> test_split : split [(1,False),(2,False)] = ([1,2],[False,False])
> test_split = ?test_split_rhs

$\square$

==== Polymorphic Options

One last polymorphic type for now: _polymorphic options_, which generalize
\idr{NatOption} from the previous chapter:

> data Option : (x : Type) -> Type where
>  Some : x -> Option x
>  None : Option x

In Idris' standard library this type is called \idr{Maybe}, with constructors
\idr{Just x} and \idr{Nothing}.

We can now rewrite the \idr{nth_error} function so that it works with any type
of lists.

> nth_error : (l : List x) -> (n : Nat) -> Option x
> nth_error [] n = None
> nth_error (a::l') n = if n == 0
>                         then Some a
>                         else nth_error l' (pred n)

> test_nth_error1 : nth_error [4,5,6,7] 0 = Some 4
> test_nth_error1 = Refl

> test_nth_error2 : nth_error [[1],[2]] 1 = Some [2]
> test_nth_error2 = Refl

> test_nth_error3 : nth_error [True] 2 = None
> test_nth_error3 = Refl

==== Exercise: 1 star, optional (hd_error_poly)

Complete the definition of a polymorphic version of the \idr{hd_error} function
from the last chapter. Be sure that it passes the unit tests below.

> hd_error : (l : List x) -> Option x
> hd_error l = ?hd_error_rhs

> test_hd_error1 : hd_error [1,2] = Some 1
> test_hd_error1 = ?test_hd_error1_rhs

> test_hd_error2 : hd_error [[1],[2]] = Some [1]
> test_hd_error2 = ?test_hd_error2_rhs

$\square$

== Functions as Data

Like many other modern programming languages -- including all functional
languages (ML, Haskell, Scheme, Scala, Clojure etc.) -- Idris treats functions
as first-class citizens, allowing them to be passed as arguments to other
functions, returned as results, stored in data structures, etc.

=== Higher-Order Functions

Functions that manipulate other functions are often called _higher-order_
functions. Here's a simple one:

> doit3times : (f: x -> x) -> (n : x) -> x
> doit3times f n = f (f (f n))

The argument \idr{f} here is itself a function (from \idr{x} to \idr{x}); the
body of \idr{doit3times} applies \idr{f} three times to some value \idr{n}.

```idris
λΠ> :t doit3times
-- doit3times : (x -> x) -> x -> x
```

\todo[inline]{Explain that the prefixes are needed to avoid the implicit scoping
rule, seems that this fires up more often when passing functions as parameters
to other functions}

> test_doit3times : doit3times Numbers.minusTwo 9 = 3
> test_doit3times = Refl

> test_doit3times' : doit3times Bool.not True = False
> test_doit3times' = Refl

=== Filter

Here is a more useful higher-order function, taking a list of \idr{x}s and a
_predicate_ on \idr{x} (a function from \idr{x} to \idr{Bool}) and "filtering"
the list, returning a new list containing just those elements for which the
predicate returns \idr{True}.

> filter : (test : x -> Bool) -> (l: List x) -> List x
> filter test [] = []
> filter test (h::t) = if test h
>                       then h :: (filter test t)
>                       else filter test t

(This is how it's defined in Idris's stdlib, too.)

For example, if we apply \idr{filter} to the predicate \idr{evenb} and a list of
numbers \idr{l}, it returns a list containing just the even members of \idr{l}.

> test_filter1 : filter Numbers.evenb [1,2,3,4] = [2,4]
> test_filter1 = Refl

> length_is_1 : (l : List x) -> Bool
> length_is_1 l = length l == 1

> test_filter2 : filter Poly.length_is_1
>                       [ [1,2], [3], [4], [5,6,7], [], [8] ]
>                     = [        [3], [4],              [8] ]
> test_filter2 = Refl

We can use \idr{filter} to give a concise version of the \idr{countoddmembers}
function from the `Lists` chapter.

> countoddmembers' : (l: List Nat) -> Nat
> countoddmembers' l = length (filter Numbers.oddb l)

> test_countoddmembers'1 : countoddmembers' [1,0,3,1,4,5] = 4
> test_countoddmembers'1 = Refl

> test_countoddmembers'2 : countoddmembers' [0,2,4] = 0
> test_countoddmembers'2 = Refl

> test_countoddmembers'3 : countoddmembers' Nil = 0
> test_countoddmembers'3 = Refl

=== Anonymous Functions

It is arguably a little sad, in the example just above, to be forced to define
the function \idr{length_is_1} and give it a name just to be able to pass it as
an argument to \idr{filter}, since we will probably never use it again.
Moreover, this is not an isolated example: when using higher-order functions, we
often want to pass as arguments "one-off" functions that we will never use
again; having to give each of these functions a name would be tedious.

Fortunately, there is a better way. We can construct a function "on the fly"
without declaring it at the top level or giving it a name.

\todo[inline]{Can't use \idr{*} here due to the interference from our tuple
sugar}

> test_anon_fun' : doit3times (\n => mult n n) 2 = 256
> test_anon_fun' = Refl

The expression \idr{\n => mult n n} can be read as "the function that, given a
number \idr{n}, yields \idr{n * n}."

Here is the \idr{filter} example, rewritten to use an anonymous function.

> test_filter2' : filter (\l => length l == 1)
>                       [ [1,2], [3], [4], [5,6,7], [], [8] ]
>                     = [        [3], [4],              [8] ]
> test_filter2' = Refl

==== Exercise: 2 stars (filter_even_gt7)

Use \idr{filter} (instead of function definition) to write an Idris function
\idr{filter_even_gt7} that takes a list of natural numbers as input and returns
a list of just those that are even and greater than \idr{7}.

> filter_even_gt7 : (l : List Nat) -> List Nat
> filter_even_gt7 l = ?filter_even_gt7_rhs

> test_filter_even_gt7_1 : filter_even_gt7 [1,2,6,9,10,3,12,8] = [10,12,8]
> test_filter_even_gt7_1 = ?test_filter_even_gt7_1_rhs

> test_filter_even_gt7_2 : filter_even_gt7 [5,2,6,19,129] = []
> test_filter_even_gt7_2 = ?test_filter_even_gt7_2_rhs

$\square$

==== Exercise: 3 stars (partition)

Use \idr{filter} to write an Idris function \idr{partition}:

> partition : (test : x -> Bool) -> (l : List x) -> (List x) * (List x)
> partition f xs = ?partition_rhs

Given a set \idr{x}, a test function of type \idr{x -> Bool} and a \idr{List x},
\idr{partition} should return a pair of lists. The first member of the pair is
the sublist of the original list containing the elements that satisfy the test,
and the second is the sublist containing those that fail the test. The order of
elements in the two sublists should be the same as their order in the original
list.

> test_partition1 : partition Numbers.oddb [1,2,3,4,5] = ([1,3,5], [2,4])
> test_partition1 = ?test_partition1_rhs

> test_partition2 : partition (\x => False) [5,9,0] = (([], [5,9,0]))
> test_partition2 = ?test_partition2_rhs

$\square$

=== Map

Another handy higher-order function is called \idr{map}.

> map : (f : x -> y) -> (l : List x) -> List y
> map f [] = []
> map f (h::t) = (f h) :: map f t

It takes a function \idr{f} and a list \idr{l} = \idr{[n1, n2, n3, ...]} and
returns the list \idr{[f n1, f n2, f n3,...]}, where \idr{f} has been applied to
each element of \idr{l} in turn. For example:

> test_map1 : map (\x => plus 3 x) [2,0,2] = [5,3,5]
> test_map1 = Refl

The element types of the input and output lists need not be the same, since
\idr{map} takes _two_ type arguments, \idr{x} and \idr{y}; it can thus be
applied to a list of numbers and a function from numbers to booleans to yield a
list of booleans:

> test_map2 : map Numbers.oddb [2,1,2,5] = [False,True,False,True]
> test_map2 = Refl

It can even be applied to a list of numbers and a function from numbers to
_lists_ of booleans to yield a _list of lists_ of booleans:

> test_map3 : map (\n => [evenb n, oddb n]) [2,1,2,5]
>                   = [[True,False],[False,True],[True,False],[False,True]]
> test_map3 = Refl

==== Exercise: 3 stars (map_rev)

Show that \idr{map} and \idr{rev} commute. You may need to define an auxiliary
lemma.

> map_rev : (f : x -> y) -> (l : List x) -> map f (rev l) = rev (map f l)
> map_rev f l = ?map_rev_rhs

$\square$

==== Exercise: 2 stars, recommended (flat_map)

The function \idr{map} maps a \idr{List x} to a \idr{List y} using a function of
type \idr{x -> y}. We can define a similar function, \idr{flat_map}, which maps
a \idr{List x} to a \idr{List y} using a function \idr{f} of type \idr{x -> List
y}. Your definition should work by 'flattening' the results of \idr{f}, like so:

```idris
flat_map (\n => [n,n+1,n+2]) [1,5,10] = [1,2,3, 5,6,7, 10,11,12]
```

> flat_map : (f : x -> List y) -> (l : List x) -> List y
> flat_map f l = ?flat_map_rhs

> test_flat_map1 : flat_map (\n => [n,n,n]) [1,5,4] = [1,1,1, 5,5,5, 4,4,4]
> test_flat_map1 = ?test_flat_map1_rhs

$\square$

Lists are not the only inductive type that we can write a \idr{map} function
for. Here is the definition of \idr{map} for the \idr{Option} type:

> option_map : (f : x -> y) -> (xo : Option x) -> Option y
> option_map f None = None
> option_map f (Some x) = Some (f x)

==== Exercise: 2 stars, optional (implicit_args)

The definitions and uses of \idr{filter} and \idr{map} use implicit arguments in
many places. Add explicit type parameters where necessary and use Idris to check
that you've done so correctly. (This exercise is not to be turned in; it is
probably easiest to do it on a copy of this file that you can throw away
afterwards.)

$\square$

=== Fold

An even more powerful higher-order function is called \idr{fold}. This function
is the inspiration for the `"reduce"` operation that lies at the heart of
Google's map/reduce distributed programming framework.

> fold : (f : x -> y -> y) -> (l : List x) -> (b : y) -> y
> fold f [] b = b
> fold f (h::t) b = f h (fold f t b)

Intuitively, the behavior of the \idr{fold} operation is to insert a given
binary operator \idr{f} between every pair of elements in a given list. For
example, \idr{fold (+) [1,2,3,4]} intuitively means \idr{1+2+3+4}. To make this
precise, we also need a "starting element" that serves as the initial second
input to \idr{f}. So, for example,

\idr{fold (+) [1,2,3,4] 0}

yields

\idr{1 + (2 + (3 + (4 + 0)))}

Some more examples:

\todo[inline]{We go back to \idr{andb} here because \idr{(&&)}'s second
parameter is lazy, with the left fold the return type is inferred to be lazy
too, leading to type mismatch.}

```idris
λΠ> :t fold andb
fold andb : List Bool -> Bool -> Bool
```

> fold_example1 : fold (*) [1,2,3,4] 1 = 24
> fold_example1 = Refl

> fold_example2 : fold Booleans.andb [True,True,False,True] True = False
> fold_example2 = Refl

> fold_example3 : fold (++) [[1],[],[2,3],[4]] [] = [1,2,3,4]
> fold_example3 = Refl

==== Exercise: 1 star, advanced (fold_types_different)

Observe that the type of \idr{fold} is parameterized by _two_ type variables,
\idr{x} and \idr{y}, and the parameter \idr{f} is a binary operator that takes
an \idr{x} and a \idr{y} and returns a \idr{y}. Can you think of a situation
where it would be useful for \idr{x} and \idr{y} to be different?

> -- FILL IN HERE

$\square$

=== Functions That Construct Functions

Most of the higher-order functions we have talked about so far take functions as
arguments. Let's look at some examples that involve _returning_ functions as the
results of other functions. To begin, here is a function that takes a value
\idr{x} (drawn from some type \idr{x}) and returns a function from \idr{Nat} to
\idr{x} that yields \idr{x} whenever it is called, ignoring its \idr{Nat}
argument.

> constfun : (x : x_ty) -> Nat -> x_ty
> constfun x = \k => x

> ftrue : Nat -> Bool
> ftrue = constfun True

> constfun_example1 : ftrue 0 = True
> constfun_example1 = Refl

> constfun_example2 : (constfun 5) 99 = 5
> constfun_example2 = Refl

In fact, the multiple-argument functions we have already seen are also examples
of passing functions as data. To see why, recall the type of \idr{plus}.

```idris
λΠ> :t plus
Prelude.Nat.plus : Nat -> Nat -> Nat
```

Each \idr{->} in this expression is actually a _binary_ operator on types. This
operator is _right-associative_, so the type of \idr{plus} is really a shorthand
for \idr{Nat -> (Nat -> Nat)} -- i.e., it can be read as saying that "\idr{plus}
is a one-argument function that takes a \idr{Nat} and returns a one-argument
function that takes another \idr{Nat} and returns a \idr{Nat}." In the examples
above, we have always applied \idr{plus} to both of its arguments at once, but
if we like we can supply just the first. This is called _partial application_.

> plus3 : Nat -> Nat
> plus3 = plus 3

```idris
λΠ> :t plus3
```

> test_plus3 : plus3 4 = 7
> test_plus3 = Refl

> test_plus3' : doit3times Poly.plus3 0 = 9
> test_plus3' = Refl

> test_plus3'' : doit3times (plus 3) 0 = 9
> test_plus3'' = Refl

== Additional Exercises

> namespace Exercises

==== Exercise: 2 stars (fold_length)

Many common functions on lists can be implemented in terms of \idr{fold}. For
example, here is an alternative definition of \idr{length}:

>   fold_length : (l : List x) -> Nat
>   fold_length l = fold (\_, n => S n) l 0

>   test_fold_length1 : fold_length [4,7,0] = 3
>   test_fold_length1 = Refl

Prove the correctness of \idr{fold_length}.

>   fold_length_correct : (l : List x) -> fold_length l = length l
>   fold_length_correct l = ?fold_length_correct_rhs

$\square$

==== Exercise: 3 stars (fold_map)

We can also define \idr{map} in terms of fold. Finish \idr{fold_map} below.

>   fold_map : (f : x -> y) -> (l : List x) -> List y
>   fold_map f l = ?fold_map_rhs

Write down a theorem \idr{fold_map_correct} in Idris stating that \idr{fold_map}
is correct, and prove it.

>   fold_map_correct : ?fold_map_correct

$\square$

==== Exercise: 2 stars, advanced (currying)

In Idris, a function \idr{f: a -> b -> c} really has the type \idr{a -> (b ->
c)}. That is, if you give \idr{f} a value of type \idr{a}, it will give you
function \idr{f' : b -> c}. If you then give \idr{f'} a value of type \idr{b},
it will return a value of type \idr{c}. This allows for partial application, as
in \idr{plus3}. Processing a list of arguments with functions that return
functions is called _currying_, in honor of the logician Haskell Curry.

Conversely, we can reinterpret the type \idr{a -> b -> c} as \idr{(a * b) -> c}.
This is called _uncurrying_. With an uncurried binary function, both arguments
must be given at once as a pair; there is no partial application.

We can define currying as follows:

>   prod_curry : (f : (x * y) -> z) -> (x_val : x) -> (y_val : y) -> z
>   prod_curry f x_val y_val = f (x_val, y_val)

As an exercise, define its inverse, \idr{prod_uncurry}. Then prove the theorems
below to show that the two are inverses.

>   prod_uncurry : (f : x -> y -> z) -> (p : x * y) -> z
>   prod_uncurry f p = ?prod_uncurry_rhs

As a (trivial) example of the usefulness of currying, we can use it to shorten
one of the examples that we saw above:

\todo[inline]{Not sure what are they shortening here}

>   test_map2' : map (\x => plus 3 x) [2,0,2] = [5,3,5]
>   test_map2' = Refl

\todo[inline]{Didn't we just write out these types explicitly?}

Thought exercise: before running the following commands, can you calculate the
types of \idr{prod_curry} and \idr{prod_uncurry}?

```idris
λΠ> :t prod_curry
λΠ> :t prod_uncurry
```

>   uncurry_curry : (f : x -> y -> z) -> (x_val : x) -> (y_val : y) ->
>                   prod_curry (prod_uncurry f) x_val y_val = f x_val y_val
>   uncurry_curry f x_val y_val = ?uncurry_curry_rhs

>   curry_uncurry : (f : (x * y) -> z) -> (p : x * y) ->
>                   prod_uncurry (prod_curry f) p = f p
>   curry_uncurry f p = ?curry_uncurry_rhs

$\square$

==== Exercise: 2 stars, advanced (nth_error_informal)

Recall the definition of the \idr{nth_error} function:

```idris
  nth_error : (l : List x) -> (n : Nat) -> Option x
  nth_error [] n = None
  nth_error (a::l') n = if n == 0
                          then Some a
                          else nth_error l' (pred n)
```

Write an informal proof of the following theorem:

\idr{n -> l -> length l = n -> nth_error l n = None}

> -- FILL IN HERE

$\square$

==== Exercise: 4 stars, advanced (church_numerals)

This exercise explores an alternative way of defining natural numbers, using the
so-called _Church numerals_, named after mathematician Alonzo Church. We can
represent a natural number \idr{n} as a function that takes a function \idr{f}
as a parameter and returns \idr{f} iterated \idr{n} times.

> namespace Church

>   Nat' : {x : Type} -> Type
>   Nat' {x} = (x -> x) -> x -> x

Let's see how to write some numbers with this notation. Iterating a function
once should be the same as just applying it. Thus:

>   one : Nat'
>   one f x = f x

Similarly, \idr{two} should apply \idr{f} twice to its argument:

>   two : Nat'
>   two f x = f (f x)

Defining \idr{zero} is somewhat trickier: how can we "apply a function zero
times"? The answer is actually simple: just return the argument untouched.

>   zero : Nat'
>   zero f x = x

More generally, a number \idr{n} can be written as \idr{\f, x => f (f ... (f x)
...)}, with \idr{n} occurrences of \idr{f}. Notice in particular how the
\idr{doit3times} function we've defined previously is actually just the Church
representation of \idr{3}.

>   three : Nat'
>   three = doit3times

Complete the definitions of the following functions. Make sure that the
corresponding unit tests pass by proving them with \idr{Refl}.

Successor of a natural number:

>   succ' : (n : Nat' {x}) -> Nat' {x}
>   succ' n = ?succ__rhs

\todo[inline]{Even if you add \idr{f x} on both sides of \idr{=}, these "unit
tests" don't seem to work neither with \idr{Refl} nor with more advanced
techniques currently}

>   succ'_1 : succ' zero = one
>   succ'_1 = ?succ__1_rhs

>   succ'_2 : succ' one = two
>   succ'_2 = ?succ__2_rhs

>   succ'_3 : succ' two = three
>   succ'_3 = ?succ__3_rhs

Addition of two natural numbers:

>   plus' : (n, m : Nat' {x}) -> Nat' {x}
>   plus' n m = ?plus__rhs

>   plus'_1 : plus' zero one = one
>   plus'_1 = ?plus__1_rhs

>   plus'_2 : plus' two three = plus' three two
>   plus'_2 = ?plus__2_rhs

>   plus'_3 : plus' (plus' two two) three = plus' one (plus' three three)
>   plus'_3 = ?plus__3_rhs

Multiplication:

>   mult' : (n, m : Nat' {x}) -> Nat' {x}
>   mult' n m = ?mult__rhs

>   mult'_1 : mult' one one = one
>   mult'_1 = ?mult__1_rhs

>   mult'_2 : mult' zero (plus' three three) = zero
>   mult'_2 = ?mult__2_rhs

>   mult'_3 : mult' two three = plus' three three
>   mult'_3 = ?mult__3_rhs

Exponentiation:

\todo[inline]{Edit the hint. Can't make it work with \idr{exp' : (n, m : Nat'
{x}) -> Nat' {x}}.}

(Hint: Polymorphism plays a crucial role here. However, choosing the right type
to iterate over can be tricky. If you hit a "Universe inconsistency" error, try
iterating over a different type: \idr{Nat'} itself is usually problematic.)

>   exp' : (n : Nat' {x}) -> (m : Nat' {x=x->x}) -> Nat' {x}
>   exp' n m = ?exp__rhs

\todo[inline]{This won't typecheck under this signature of \idr{exp} because of
2 instances of \idr{two}}

>   -- exp'_1 : exp' two two = plus' two two
>   -- exp'_1 = ?exp__1_rhs

>   exp'_2 : exp' three two = plus' (mult' two (mult' two two)) one
>   exp'_2 = ?exp__2_rhs

>   exp'_3 : exp' three zero = one
>   exp'_3 = ?exp__3_rhs

$\square$

max_stars_repo_name: MarcelineVQ/software-foundations

max_issues_repo_name: MarcelineVQ/software-foundations

max_forks_repo_name: MarcelineVQ/software-foundations


text:
module ConfigProvider

import Lightyear
import Lightyear.Char
import Lightyear.Strings
import Lightyear.StringFile

import Prelude.Providers
%language TypeProviders

record Field where
  constructor MkField
  fname, fvalue : String

parseFields : Parser (List Field)
parseFields = many parseField
  where parseField : Parser Field
        parseField = do name <- many letter
                        spaces *> colon <* spaces
                        val <- quoted '"'
                        many newline
                        return $ MkField (pack name) val

getConfig : IO (Either String $ List Field)
getConfig = do Right file <- readFile "../config.cfg"
                     | Left err => return (Left "Couldn't read config file, using defaults!")
               return $ parse parseFields file

getConfigField : String -> String -> IO (Provider String)
getConfigField field d = do case !getConfig of
                              Left err  => do putStrLn $ show err
                                              return $ pure d
                              Right cfg => case filter (\i => fname i == field) cfg of
                                             []   => return $ pure d
                                             x::_ => return $ pure $ fvalue x

getPkgPath : IO (Provider String)
getPkgPath = getConfigField "defaultPkgPath" "./example/"

getPrimarySrc : IO (Provider String)
getPrimarySrc = getConfigField "primarySources" "db/"

getOverlays : IO (Provider String)
getOverlays = getConfigField "overlays" ".overlays"

ext: idr

max_stars_repo_name: nv-vn/Anvil

max_issues_repo_name: nv-vn/Anvil

max_forks_repo_name: nv-vn/Anvil


text:
module Algebra.Solver.Ring.SolvableRing

import Algebra.Ring

%default total

||| When normalizing arithmetic expressions, we must
||| make sure that factors that evaluate to zero must
||| be removed from the sum of products.
|||
||| For instance, the following example only works,
||| if the term `0 * x * y` gets removed before comparing
||| the normalized sums:
|||
||| ```idris example
||| 0 binom3 : {x,y : Bits8} -> (x + y) * (x - y) === x * x - y * y
||| binom3 = solve [x,y] ((x .+. y) * (x .-. y)) (x .*. x - y .*. y)
||| ```
|||
||| Because we cannot directly use a (primitive) pattern match
||| without having a concrete type, we need this interface.
||| (We *could* use `DecEq`, but this is not publicly exported
||| for the primitives; probably for good reasons since it is
||| implemented using `believe_me`).
public export
interface Ring a => SolvableRing a where

  ||| Checks if a value is propositionally equal to zero.
  isZero : (v : a) -> Maybe (v === 0)

public export
SolvableRing Bits8 where
  isZero 0 = Just Refl
  isZero _ = Nothing

public export
SolvableRing Bits16 where
  isZero 0 = Just Refl
  isZero _ = Nothing

public export
SolvableRing Bits32 where
  isZero 0 = Just Refl
  isZero _ = Nothing

public export
SolvableRing Bits64 where
  isZero 0 = Just Refl
  isZero _ = Nothing

public export
SolvableRing Int8 where
  isZero 0 = Just Refl
  isZero _ = Nothing

public export
SolvableRing Int16 where
  isZero 0 = Just Refl
  isZero _ = Nothing

public export
SolvableRing Int32 where
  isZero 0 = Just Refl
  isZero _ = Nothing

public export
SolvableRing Int64 where
  isZero 0 = Just Refl
  isZero _ = Nothing

public export
SolvableRing Int where
  isZero 0 = Just Refl
  isZero _ = Nothing

public export
SolvableRing Integer where
  isZero 0 = Just Refl
  isZero _ = Nothing


text:
module Queue

import Stack as Stack

%access export
%default total

-- | *Queue
data Queue : Type -> Nat -> Nat -> Nat -> Type where
     MkQueue : (front : Stack.Stack n ty)
             -> (back : Stack.Stack m ty)
             -> Queue ty n m (n + m)

%name Queue queue
-- .end

-- | *empty
empty : Queue ty Z Z Z
empty = MkQueue Stack.empty Stack.empty
-- .end

-- | *rotate
rotate : Queue ty m n k -> Queue ty n m k
rotate {m} {n} (MkQueue front back) =
       rewrite (plusCommutative m n) in MkQueue back front
-- .end

-- | *top
top : Queue ty n m (S k) -> ty
top {n = S n'} {m = _} (MkQueue front _) =
    Stack.head front
top {n = Z} {m = S m'} (MkQueue _ back) =
    Stack.head $ Stack.reverse back
top {n = Z} {m = Z} (MkQueue _ _) impossible
-- .end

-- | *back
bottom : Queue ty n m (S k) -> ty
bottom {m = S m'} {n = S n'} (MkQueue _ back) =
       Stack.head back
bottom {m = S m'} {n = Z} (MkQueue _ back) =
       Stack.head back
bottom {m = Z} {n = S j} (MkQueue front _) =
       Stack.head $ Stack.reverse front
bottom {m = Z} {n = Z} (MkQueue _ _) impossible
-- .end

-- | *inject
inject : (a : ty) -> Queue ty n m k -> Queue ty n (S m) (S k)
inject {n} {m} newVal (MkQueue front back) =
       rewrite (plusSuccRightSucc n m) in MkQueue front (Stack.cons newVal back)
-- .end

-- | *push
push : (a : ty) -> Queue ty n m k -> Queue ty (S n) m (S k)
push newVal (MkQueue front back) = MkQueue (Stack.cons newVal front) back
-- .end

max_stars_repo_name: nomicflux/okasaki-visualization

max_issues_repo_name: nomicflux/okasaki-visualization

max_forks_repo_name: nomicflux/okasaki-visualization


text:
data Tree elem = ||| A (sub-)tree with no data.
                 Empty
               | ||| A node with a left subtree, a value, and a right subtree.
                 Node (Tree elem) elem (Tree elem)

%name Tree tree, tree1, tree2

insert : Ord elem => elem -> Tree elem -> Tree elem
insert x Empty = Node Empty x Empty
insert x (Node left val right)
  = case compare x val of
      LT => Node (insert x left) val right
      EQ => Node left val right
      GT => Node left val (insert x right)


text:
import Data.List

ack : Nat -> Nat -> Nat
ack 0 n = S n
ack (S k) 0 = ack k 1
ack (S j) (S k) = ack j (ack (S j) k)

foo : Nat -> Nat
foo Z = Z
foo (S Z) = (S Z)
foo (S (S k)) = foo (S k)

data Ord = Zero | Suc Ord | Sup (Nat -> Ord)

ordElim : (x : Ord) ->
          (p : Ord -> Type) ->
          (p Zero) ->
          ((x : Ord) -> p x -> p (Suc x)) ->
          ((f : Nat -> Ord) -> ((n : Nat) -> p (f n)) ->
             p (Sup f)) -> p x
ordElim Zero p mZ mSuc mSup = mZ
ordElim (Suc o) p mZ mSuc mSup = mSuc o (ordElim o p mZ mSuc mSup)
ordElim (Sup f) p mZ mSuc mSup =
   mSup f (\n => ordElim (f n) p mZ mSuc mSup)

mutual
  bar : Nat -> Lazy Nat -> Nat
  bar x y = mp x y

  mp : Nat -> Nat -> Nat
  mp Z y = y
  mp (S k) y = S (bar k y)

mutual
    swapR : Nat -> Nat -> Nat
    swapR x (S y) = swapL y x
    swapR x Z = x

    swapL : Nat -> Nat -> Nat
    swapL (S x) y = swapR y (S x)
    swapL Z y = y

loopy : a
loopy = loopy

data Bin = EPS | C0 Bin | C1 Bin

foom : Bin -> Nat
foom EPS = Z
foom (C0 EPS) = Z
foom (C0 (C1 x)) = S (foom (C1 x))
foom (C0 (C0 x)) = foom (C0 x)
foom (C1 x) = S (foom x)

pfoom : Bin -> Nat
pfoom EPS = Z
pfoom (C0 EPS) = Z
pfoom (C0 (C1 x)) = S (pfoom (C0 x))
pfoom (C0 (C0 x)) = pfoom (C0 x)
pfoom (C1 x) = S (foom x)

even : Nat -> Bool
even Z = True
even (S k) = odd k
  where
    odd : Nat -> Bool
    odd Z = False
    odd (S k) = even k

data Vect : Nat -> Type -> Type where
     Nil : Vect Z a
     (::) : a -> Vect k a -> Vect (S k) a

vtrans : Vect n a -> Vect n a -> List a
vtrans [] _         = []
vtrans (x :: xs) ys = x :: vtrans ys ys

data GTree : Type -> Type where
     MkGTree : List (GTree a) -> GTree a

size : GTree a -> Nat
size (MkGTree []) = Z
size (MkGTree xs) = sizeAll xs
  where
    plus : Nat -> Nat -> Nat
    plus Z y = y
    plus (S k) y = S (plus k y)

    sizeAll : List (GTree a) -> Nat
    sizeAll [] = Z
    sizeAll (x :: xs) = plus (size x) (sizeAll xs)

qsortBad : Ord a => List a -> List a
qsortBad [] = []
qsortBad (x :: xs)
   = qsortBad (filter (< x) xs) ++ x :: qsortBad (filter (> x) xs)

qsort : Ord a => List a -> List a
qsort [] = []
qsort (x :: xs)
   = qsort (assert_smaller (x :: xs) (filter (< x) xs)) ++
         x :: qsort (assert_smaller (x :: xs) (filter (> x) xs))

qsort' : Ord a => List a -> List a
qsort' [] = []
qsort' (x :: xs)
   = let (xs_low, xs_high) = partition x xs in
         qsort' (assert_smaller (x :: xs) xs_low) ++
         x :: qsort' (assert_smaller (x :: xs) xs_high)
  where
    partition : a -> List a -> (List a, List a)
    partition x xs = (filter (< x) xs, filter (>= x) xs)

mySorted : Ord a => List a -> Bool
mySorted []      = True
mySorted (x::xs) =
  case xs of
    Nil     => True
    (y::ys) => x <= y && mySorted (y::ys)

myMergeBy : (a -> a -> Ordering) -> List a -> List a -> List a
myMergeBy order []      right   = right
myMergeBy order left    []      = left
myMergeBy order (x::xs) (y::ys) =
  case order x y of
       LT => x :: myMergeBy order xs (y::ys)
       _  => y :: myMergeBy order (x::xs) ys


text:
module Sphere

import Hittable
import Vec3
import Ray

%access export

public export

record Sphere where
    constructor MkSphere
    center : Vec3
    radius : Double

Hittable Sphere where
    hit sphere ray t_min t_max =
       if discriminant > 0
            then
                if temp < t_max && temp > t_min
                    then set_face_normal ray oNormal rec
                    else
                        if temp' < t_max && temp' > t_min
                            then set_face_normal ray oNormal' rec'
                            else MkHitRecord (0,0,0) (0,0,0) temp' False False
            else MkHitRecord (0,0,0) (0,0,0) 1 False False
    where
        oc : Vec3
        oc           = (orig ray) - center sphere
        a : Double
        a            = lengthSquared (dir ray)
        half_b : Double
        half_b       = dot oc (dir ray)
        c : Double
        c            = (lengthSquared oc) - radius sphere * radius sphere
        discriminant : Double
        discriminant = half_b*half_b - a*c

        root : Double
        root = sqrt discriminant
        temp : Double
        temp = (-half_b - root) / a
        temp' : Double
        temp' = (-half_b + root) / a

        rec_p : Vec3
        rec_p   = at ray temp
        rec : HitRecord
        rec     = MkHitRecord rec_p (0, 0, 0) temp False True
        oNormal : Vec3
        oNormal = (rec_p - center sphere) / radius sphere

        rec_p' : Vec3
        rec_p'   = at ray temp'
        rec' : HitRecord
        rec'     = MkHitRecord rec_p (0, 0, 0) temp' False True
        oNormal' : Vec3
        oNormal' = (rec_p' - center sphere) / radius sphere

max_stars_repo_name: MarkMarkyMarkus/YART

max_issues_repo_name: MarkMarkyMarkus/YART

max_forks_repo_name: MarkMarkyMarkus/YART


text:
module Vec3

%access export

public export
-- To RECORD ?
Vec3 : Type
Vec3 = (Double, Double, Double)

toColor : Int -> Int -> Double
toColor value size = 255.999 * (cast value / cast size)

getX : Vec3 -> Double
getX (x, _, _) = x

getY : Vec3 -> Double
getY (_, y, _) = y

getZ : Vec3 -> Double
getZ (_, _, z) = z

(+) : Vec3 -> Vec3 -> Vec3
(+) (x1, y1, z1) (x2, y2, z2) = (x1 + x2, y1 + y2, z1 + z2)

(-) : Vec3 -> Vec3 -> Vec3
(-) (x1, y1, z1) (x2, y2, z2) = (x1 - x2, y1 - y2, z1 - z2)

-- (*) : Vec3 -> Vec3 -> Vec3
-- (*) (x1, y1, z1) (x2, y2, z2) = (x1 * x2, y1 * y2, z1 * z2)

(*) : Double -> Vec3 -> Vec3
(*) t (x2, y2, z2) = (t * x2, t * y2, t * z2)

(/) : Vec3 -> Double -> Vec3
(/) v t = (1 / t) * v

dot : Vec3 -> Vec3 -> Double
dot (x1, y1, z1) (x2, y2, z2) = x1 * x2 + y1 * y2 + z1 * z2

length : Vec3 -> Double
length (x, y, z) = sqrt (x*x + y*y + z*z)

lengthSquared : Vec3 -> Double
lengthSquared (x, y, z) = x*x + y*y + z*z

unitVector : Vec3 -> Vec3
unitVector v = v / Vec3.length v

vecToStr : Vec3 -> String
vecToStr (x, y, z) = concat [show $ cast {to=Int} x, " ", show $ cast {to=Int} y, " ", show $ cast {to=Int} z]


text:
module squareRoot

square_root_approx : (number : Double) -> (approx : Double) -> Stream Double
square_root_approx number approx =
  let next = (approx + (number / approx)) / 2 in
      next :: square_root_approx number next

square_root_bound : (max : Nat) -> (number : Double) -> (bound : Double) -> (approxs : Stream Double) -> Double
square_root_bound Z number bound (value :: vs) = value
square_root_bound (S k) number bound (v :: vs) =
  case (v * v) < bound of
       False => square_root_bound k number bound vs
       True => v

square_root : (number : Double) -> Double
square_root number = square_root_bound 100 number 0.0000000001 (square_root_approx number number)

max_stars_repo_path: Chapter 11/squareRoot.idr

max_issues_repo_path: Chapter 11/squareRoot.idr

max_forks_repo_path: Chapter 11/squareRoot.idr


text:
module Main

import Network.Curl.Easy

main : IO ()
main = do
    CURLE_OK <- curl_global_init | c => do
        putStrLn $ "error in curl_global_init: " ++ show c

    Just cli <- curlEasyInit | Nothing => putStrLn "error in curlEasyInit"

    CURLE_OK <- curlEasySetopt cli CURLOPT_URL "https://google.com" | c => do
        putStrLn $ "error in curlEasySetopt: " ++ show c

    CURLE_OK <- curlEasyPerform cli | c => do
        putStrLn $ "error in curlEasyPerform: " ++ show c

    curlEasyCleanup cli
    curl_global_cleanup


text:
-- --------------------------------------------------------------- [ Model.idr ]
-- Module    : Model.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]

module Text.Markup.Edda.Model.Processed

import Data.AVL.Dict

import Text.Markup.Edda.Model.Common

%default total
%access public export

data Edda : EddaTy -> Type where
  Text : String -> Edda INLINE
  Sans : String -> Edda INLINE
  Scap : String -> Edda INLINE
  Mono : String -> Edda INLINE

  Verb : String -> Edda INLINE
  Code : String -> Edda INLINE
  Math : String -> Edda INLINE

  Emph   : List (Edda INLINE) -> Edda INLINE
  Bold   : List (Edda INLINE) -> Edda INLINE
  Strike : List (Edda INLINE) -> Edda INLINE
  Uline  : List (Edda INLINE) -> Edda INLINE

  Quote  : QuoteTy -> List (Edda INLINE) -> Edda INLINE
  Parens : ParenTy -> List (Edda INLINE) -> Edda INLINE

  Ref   : String  -> Edda INLINE
  Cite  : CiteSty -> String -> Edda INLINE
  Hyper : String  -> List (Edda INLINE) -> Edda INLINE
  FNote : String  -> List (Edda INLINE) -> Edda INLINE

  Space      : Edda INLINE
  Newline    : Edda INLINE
  Tab        : Edda INLINE

  Colon      : Edda INLINE
  Semi       : Edda INLINE
  FSlash     : Edda INLINE
  BSlash     : Edda INLINE
  Apostrophe : Edda INLINE
  SMark      : Edda INLINE
  Hyphen     : Edda INLINE
  Comma      : Edda INLINE
  Plus       : Edda INLINE
  Bang       : Edda INLINE
  Period     : Edda INLINE
  QMark      : Edda INLINE
  Hash       : Edda INLINE
  Equals     : Edda INLINE
  Dollar     : Edda INLINE
  Pipe       : Edda INLINE
  Ellipsis   : Edda INLINE
  EmDash     : Edda INLINE
  EnDash     : Edda INLINE

  LAngle     : Edda INLINE
  RAngle     : Edda INLINE

  LBrace     : Edda INLINE
  RBrace     : Edda INLINE

  LParen     : Edda INLINE
  RParen     : Edda INLINE

  LBrack     : Edda INLINE
  RBrack     : Edda INLINE

  MiscPunc   : Char -> Edda INLINE
-- ------------------------------------------------------------------ [ Blocks ]

  HRule : Edda BLOCK
  Empty : Edda BLOCK

  Figure : (label   : Maybe String)
        -> (caption : List (Edda INLINE))
        -> (attrs   : Dict String String)
        -> (url     : Edda INLINE)
        -> Edda BLOCK

  DList : (kvpairs : List (List (Edda INLINE), List (Edda INLINE)))
        -> Edda BLOCK

  Section : (depth : Nat)
         -> (label : Maybe String)
         -> (title : List (Edda INLINE))
         -> (attrs : Dict String String)
         -> (body  : List (Edda BLOCK))
         -> Edda BLOCK

  OList : List (List (Edda INLINE)) -> Edda BLOCK
  BList : List (List (Edda INLINE)) -> Edda BLOCK

  Comment : String -> Edda BLOCK

  Equation : (label : Maybe String) -> (eq : String) -> Edda BLOCK

  Literal : Maybe String
          -> List (Edda INLINE)
          -> String
          -> Edda BLOCK
  Listing : Maybe String
          -> (List (Edda INLINE))
          -> (Maybe String)
          -> (Maybe String)
          -> Dict String String
          -> String
          -> Edda BLOCK

  Para : List (Edda INLINE) -> Edda BLOCK
  Quotation   : Maybe String -> List (Edda INLINE)-> Edda BLOCK

  Theorem     : Maybe String -> List (Edda INLINE) -> List (Edda INLINE) -> Edda BLOCK
  Corollary   : Maybe String -> List (Edda INLINE) -> List (Edda INLINE) -> Edda BLOCK
  Lemma       : Maybe String -> List (Edda INLINE) -> List (Edda INLINE) -> Edda BLOCK
  Proposition : Maybe String -> List (Edda INLINE) -> List (Edda INLINE) -> Edda BLOCK
  Proof       : Maybe String -> List (Edda INLINE) -> List (Edda INLINE) -> Edda BLOCK
  Definition  : Maybe String -> List (Edda INLINE) -> List (Edda INLINE) -> Edda BLOCK
  Exercise    : Maybe String -> List (Edda INLINE) -> List (Edda INLINE) -> Edda BLOCK
  Note        : Maybe String -> List (Edda INLINE) -> List (Edda INLINE) -> Edda BLOCK
  Remark      : Maybe String -> List (Edda INLINE) -> List (Edda INLINE) -> Edda BLOCK
  Problem     : Maybe String -> List (Edda INLINE) -> List (Edda INLINE) -> Edda BLOCK
  Question    : Maybe String -> List (Edda INLINE) -> List (Edda INLINE) -> Edda BLOCK
  Solution    : Maybe String -> List (Edda INLINE) -> List (Edda INLINE) -> Edda BLOCK
  Example     : Maybe String -> List (Edda INLINE) -> List (Edda INLINE) -> Edda BLOCK

  Snippet : (snippet : List $ Edda ty)
         -> (prf : ValidSnippet ty)
         -> Edda SNIPPET

  Doc : (title : List (Edda INLINE))
     -> (attrs : Dict String String)
     -> (body  : List (Edda BLOCK))
     -> Edda DOC

-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: jfdm/edda

max_issues_repo_name: jfdm/edda

max_forks_repo_name: jfdm/edda


text:
module Main

import Syntax.Lexer
import Syntax.Tokens
import System.File
import Error
import Loc

main : IO ()
main = do
    readFile "input" >>= \res =>
      case res of
        Right input =>
          case lex input of
                Right res => putStr (concatMap ((++ "\n") . show) res)
                Left _ => putStrLn "Error"
        Left _ => print "File not found"

max_stars_repo_name: felipegchi/Yurei

max_issues_repo_name: felipegchi/Yurei

max_forks_repo_name: felipegchi/Yurei


text:
-- exercises in "Type-Driven Development with Idris"
-- chapter 6

-- check that all functions are total
%default total

--
-- section 6.2
-- see Matrix.idr
-- see Printf.idr
--

TupleVect : (n : Nat) -> Type -> Type
TupleVect Z t = ()
TupleVect (S k) t = (t, TupleVect k t)

test : TupleVect 4 Nat
test = (1,2,3,4,())

--
-- section 6.3
-- see DataStore.idr
--

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
module Core.Metadata

import Core.Binary
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Directory
import Core.Env
import Core.FC
import Core.Normalise
import Core.Options
import Core.TT
import Core.TTC

import Data.List
import System.File
import Libraries.Data.PosMap
import Libraries.Utils.Binary

%default covering

public export
data Decoration : Type where
  Typ       : Decoration
  Function  : Decoration
  Data      : Decoration
  Keyword   : Decoration
  Bound     : Decoration
  Namespace : Decoration
  Postulate : Decoration
  Module    : Decoration

export
nameDecoration : Name -> NameType -> Decoration
nameDecoration nm nt
  = ifThenElse (isUnsafeBuiltin nm) Postulate (nameTypeDecoration nt)

  where

  nameTypeDecoration : NameType -> Decoration
  nameTypeDecoration Bound         = Bound
  nameTypeDecoration Func          = Function
  nameTypeDecoration (DataCon _ _) = Data
  nameTypeDecoration (TyCon _ _  ) = Typ

public export
ASemanticDecoration : Type
ASemanticDecoration = (NonEmptyFC, Decoration, Maybe Name)

public export
SemanticDecorations : Type
SemanticDecorations = List ASemanticDecoration

public export
Eq Decoration where
  Typ       == Typ       = True
  Function  == Function  = True
  Data      == Data      = True
  Keyword   == Keyword   = True
  Bound     == Bound     = True
  Namespace == Namespace = True
  Postulate == Postulate = True
  Module    == Module    = True
  _         == _         = False

-- CAREFUL: this instance is used in SExpable Decoration. If you change
-- it then you need to fix the SExpable implementation in order not to
-- break the IDE mode.
public export
Show Decoration where
  show Typ       = "type"
  show Function  = "function"
  show Data      = "data"
  show Keyword   = "keyword"
  show Bound     = "bound"
  show Namespace = "namespace"
  show Postulate = "postulate"
  show Module    = "module"

TTC Decoration where
  toBuf b Typ       = tag 0
  toBuf b Function  = tag 1
  toBuf b Data      = tag 2
  toBuf b Keyword   = tag 3
  toBuf b Bound     = tag 4
  toBuf b Namespace = tag 5
  toBuf b Postulate = tag 6
  toBuf b Module    = tag 7
  fromBuf b
    = case !getTag of
        0 => pure Typ
        1 => pure Function
        2 => pure Data
        3 => pure Keyword
        4 => pure Bound
        5 => pure Namespace
        6 => pure Postulate
        7 => pure Module
        _ => corrupt "Decoration"

public export
record Metadata where
       constructor MkMetadata
       -- Mapping from source annotation (location, typically) to
       -- the LHS defined at that location. Also record the outer environment
       -- length, since we don't want to case split on these.
       lhsApps : List (NonEmptyFC, (Nat, ClosedTerm))
       -- Mapping from annotation to the name defined with that annotation,
       -- and its type (so, giving the ability to get the types of locally
       -- defined names)
       -- The type is abstracted over the whole environment; the Nat gives
       -- the number of names which were in the environment at the time.
       names : List (NonEmptyFC, (Name, Nat, ClosedTerm))
       -- Mapping from annotation to the name that's declared there and
       -- its type; the Nat is as above
       tydecls : List (NonEmptyFC, (Name, Nat, ClosedTerm))
       -- Current lhs, if applicable, and a mapping from hole names to the
       -- lhs they're under. This is for expression search, to ensure that
       -- recursive calls have a smaller value as an argument.
       -- Also use this to get the name of the function being defined (i.e.
       -- to know what the recursive call is, if applicable)
       currentLHS : Maybe ClosedTerm
       holeLHS : List (Name, ClosedTerm)
       nameLocMap : PosMap (NonEmptyFC, Name)
       sourceIdent : OriginDesc

       -- Semantic Highlighting
       -- Posmap of known semantic decorations
       semanticHighlighting : PosMap ASemanticDecoration
       -- Posmap of aliases (in `with` clauses the LHS disapear during
       -- elaboration after making sure that they match their parents'
       semanticAliases : PosMap (NonEmptyFC, NonEmptyFC)
       semanticDefaults : PosMap ASemanticDecoration

Show Metadata where
  show (MkMetadata apps names tydecls currentLHS holeLHS nameLocMap
                   fname semanticHighlighting semanticAliases semanticDefaults)
    = "Metadata:\n" ++
      " lhsApps: " ++ show apps ++ "\n" ++
      " names: " ++ show names ++ "\n" ++
      " type declarations: " ++ show tydecls ++ "\n" ++
      " current LHS: " ++ show currentLHS ++ "\n" ++
      " holes: " ++ show holeLHS ++ "\n" ++
      " nameLocMap: " ++ show nameLocMap ++ "\n" ++
      " sourceIdent: " ++ show fname ++
      " semanticHighlighting: " ++ show semanticHighlighting ++
      " semanticAliases: " ++ show semanticAliases ++
      " semanticDefaults: " ++ show semanticDefaults

export
initMetadata : OriginDesc -> Metadata
initMetadata finfo = MkMetadata
  { lhsApps = []
  , names = []
  , tydecls = []
  , currentLHS = Nothing
  , holeLHS = []
  , nameLocMap = empty
  , sourceIdent = finfo
  , semanticHighlighting = empty
  , semanticAliases = empty
  , semanticDefaults = empty
  }

-- A label for metadata in the global state
export
data MD : Type where

TTC Metadata where
  toBuf b m
      = do toBuf b (lhsApps m)
           toBuf b (names m)
           toBuf b (tydecls m)
           toBuf b (holeLHS m)
           toBuf b (nameLocMap m)
           toBuf b (sourceIdent m)
           toBuf b (semanticHighlighting m)
           toBuf b (semanticAliases m)
           toBuf b (semanticDefaults m)

  fromBuf b
      = do apps <- fromBuf b
           ns <- fromBuf b
           tys <- fromBuf b
           hlhs <- fromBuf b
           dlocs <- fromBuf b
           fname <- fromBuf b
           semhl <- fromBuf b
           semal <- fromBuf b
           semdef <- fromBuf b
           pure (MkMetadata apps ns tys Nothing hlhs dlocs fname semhl semal semdef)

export
addLHS : {vars : _} ->
         {auto c : Ref Ctxt Defs} ->
         {auto m : Ref MD Metadata} ->
         FC -> Nat -> Env Term vars -> Term vars -> Core ()
addLHS loc outerenvlen env tm
    = do meta <- get MD
         tm' <- toFullNames (bindEnv loc (toPat env) tm)
         -- Put the lhs on the metadata if it's not empty
         whenJust (isNonEmptyFC loc) $ \ neloc =>
           put MD $ record { lhsApps $= ((neloc, outerenvlen, tm') ::) } meta

  where
    toPat : Env Term vs -> Env Term vs
    toPat (Lam fc c p ty :: bs) = PVar fc c p ty :: toPat bs
    toPat (b :: bs) = b :: toPat bs
    toPat [] = []

-- For giving local variable names types, just substitute the name
-- rather than storing the whole environment, otherwise we'll repeatedly
-- store the environment and it'll get big.
-- We'll need to rethink a bit if we want interactive editing to show
-- the whole environment - perhaps store each environment just once
-- along with its source span?
-- In any case, one could always look at the other names to get their
-- types directly!
substEnv : {vars : _} ->
           FC -> Env Term vars -> (tm : Term vars) -> ClosedTerm
substEnv loc [] tm = tm
substEnv {vars = x :: _} loc (b :: env) tm
    = substEnv loc env (subst (Ref loc Bound x) tm)

export
addNameType : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              {auto m : Ref MD Metadata} ->
              FC -> Name -> Env Term vars -> Term vars -> Core ()
addNameType loc n env tm
    = do meta <- get MD
         n' <- getFullName n

         -- Add the name to the metadata if the file context is not empty
         whenJust (isNonEmptyFC loc) $ \ neloc => do
           put MD $ record { names $= ((neloc, (n', 0, substEnv loc env tm)) ::) } meta
           log "metadata.names" 7 $ show n' ++ " at line " ++ show (1 + startLine neloc)

export
addTyDecl : {vars : _} ->
            {auto c : Ref Ctxt Defs} ->
            {auto m : Ref MD Metadata} ->
            FC -> Name -> Env Term vars -> Term vars -> Core ()
addTyDecl loc n env tm
    = do meta <- get MD
         n' <- getFullName n

         -- Add the type declaration to the metadata if the file context is not empty
         whenJust (isNonEmptyFC loc) $ \ neloc =>
           put MD $ record { tydecls $= ( (neloc, (n', length env, bindEnv loc env tm)) ::) } meta

export
addNameLoc : {auto m : Ref MD Metadata} ->
             {auto c : Ref Ctxt Defs} ->
             FC -> Name -> Core ()
addNameLoc loc n
    = do meta <- get MD
         n' <- getFullName n
         whenJust (isNonEmptyFC loc) $ \neloc =>
           put MD $ record { nameLocMap $= insert (neloc, n') } meta

export
setHoleLHS : {auto m : Ref MD Metadata} ->
             ClosedTerm -> Core ()
setHoleLHS tm
    = do meta <- get MD
         put MD (record { currentLHS = Just tm } meta)

export
clearHoleLHS : {auto m : Ref MD Metadata} ->
               Core ()
clearHoleLHS
    = do meta <- get MD
         put MD (record { currentLHS = Nothing } meta)

export
withCurrentLHS : {auto c : Ref Ctxt Defs} ->
                 {auto m : Ref MD Metadata} ->
                 Name -> Core ()
withCurrentLHS n
    = do meta <- get MD
         n' <- getFullName n
         maybe (pure ())
               (\lhs => put MD (record { holeLHS $= ((n', lhs) ::) } meta))
               (currentLHS meta)

findEntryWith : (NonEmptyFC -> a -> Bool) -> List (NonEmptyFC, a) -> Maybe (NonEmptyFC, a)
findEntryWith = find . uncurry

export
findLHSAt : {auto m : Ref MD Metadata} ->
            (NonEmptyFC -> ClosedTerm -> Bool) ->
            Core (Maybe (NonEmptyFC, Nat, ClosedTerm))
findLHSAt p
    = do meta <- get MD
         pure (findEntryWith (\ loc, tm => p loc (snd tm)) (lhsApps meta))

export
findTypeAt : {auto m : Ref MD Metadata} ->
             (NonEmptyFC -> (Name, Nat, ClosedTerm) -> Bool) ->
             Core (Maybe (Name, Nat, ClosedTerm))
findTypeAt p
    = do meta <- get MD
         pure (map snd (findEntryWith p (names meta)))

export
findTyDeclAt : {auto m : Ref MD Metadata} ->
               (NonEmptyFC -> (Name, Nat, ClosedTerm) -> Bool) ->
               Core (Maybe (NonEmptyFC, Name, Nat, ClosedTerm))
findTyDeclAt p
    = do meta <- get MD
         pure (findEntryWith p (tydecls meta))

export
findHoleLHS : {auto m : Ref MD Metadata} ->
              Name -> Core (Maybe ClosedTerm)
findHoleLHS hn
    = do meta <- get MD
         pure (lookupBy (\x, y => dropNS x == dropNS y) hn (holeLHS meta))

export
addSemanticDefault : {auto m : Ref MD Metadata} ->
                     ASemanticDecoration -> Core ()
addSemanticDefault asem
  = do meta <- get MD
       put MD $ { semanticDefaults $= insert asem } meta

export
addSemanticAlias : {auto m : Ref MD Metadata} ->
                   NonEmptyFC -> NonEmptyFC -> Core ()
addSemanticAlias from to
  = do meta <- get MD
       put MD $ { semanticAliases $= insert (from, to) } meta

export
addSemanticDecorations : {auto m : Ref MD Metadata} ->
                         {auto c : Ref Ctxt Defs} ->
   SemanticDecorations -> Core ()
addSemanticDecorations decors
    = do meta <- get MD
         defs <- get Ctxt
         let posmap = meta.semanticHighlighting
         let (newDecors,droppedDecors) =
               span
                 ( (meta.sourceIdent ==)
                 . Builtin.fst
                 . Builtin.fst )
                 decors
         unless (isNil droppedDecors)
           $ log "ide-mode.highlight" 19 $ "ignored adding decorations to "
               ++ show meta.sourceIdent ++ ": " ++ show droppedDecors
         put MD $ record {semanticHighlighting
                            = (fromList newDecors) `union` posmap} meta

-- Normalise all the types of the names, since they might have had holes
-- when added and the holes won't necessarily get saved
normaliseTypes : {auto m : Ref MD Metadata} ->
                 {auto c : Ref Ctxt Defs} ->
                 Core ()
normaliseTypes
    = do meta <- get MD
         defs <- get Ctxt
         ns' <- traverse (nfType defs) (names meta)
         put MD (record { names = ns' } meta)
  where
    nfType : Defs -> (NonEmptyFC, (Name, Nat, ClosedTerm)) ->
             Core (NonEmptyFC, (Name, Nat, ClosedTerm))
    nfType defs (loc, (n, len, ty))
       = pure (loc, (n, len, !(normaliseArgHoles defs [] ty)))

record TTMFile where
  constructor MkTTMFile
  version : Int
  metadata : Metadata

TTC TTMFile where
  toBuf b file
      = do toBuf b "TTM"
           toBuf b (version file)
           toBuf b (metadata file)

  fromBuf b
      = do hdr <- fromBuf b
           when (hdr /= "TTM") $ corrupt "TTM header"
           ver <- fromBuf b
           checkTTCVersion "" ver ttcVersion -- maybe change the interface to get the filename
           md <- fromBuf b
           pure (MkTTMFile ver md)

HasNames Metadata where
  full gam md
      = pure $ record { lhsApps = !(traverse fullLHS $ md.lhsApps)
                      , names   = !(traverse fullTy $ md.names)
                      , tydecls = !(traverse fullTy $ md.tydecls)
                      , currentLHS = Nothing
                      , holeLHS = !(traverse fullHLHS $ md.holeLHS)
                      , nameLocMap = fromList !(traverse fullDecls (toList $ md.nameLocMap))
                      } md
    where
      fullLHS : (NonEmptyFC, (Nat, ClosedTerm)) -> Core (NonEmptyFC, (Nat, ClosedTerm))
      fullLHS (fc, (i, tm)) = pure (fc, (i, !(full gam tm)))

      fullTy : (NonEmptyFC, (Name, Nat, ClosedTerm)) -> Core (NonEmptyFC, (Name, Nat, ClosedTerm))
      fullTy (fc, (n, i, tm)) = pure (fc, (!(full gam n), i, !(full gam tm)))

      fullHLHS : (Name, ClosedTerm) -> Core (Name, ClosedTerm)
      fullHLHS (n, tm) = pure (!(full gam n), !(full gam tm))

      fullDecls : (NonEmptyFC, Name) -> Core (NonEmptyFC, Name)
      fullDecls (fc, n) = pure (fc, !(full gam n))

  resolved gam (MkMetadata lhs ns tys clhs hlhs dlocs fname semhl semal semdef)
      = pure $ MkMetadata !(traverse resolvedLHS lhs)
                          !(traverse resolvedTy ns)
                          !(traverse resolvedTy tys)
                          Nothing
                          !(traverse resolvedHLHS hlhs)
                          (fromList !(traverse resolvedDecls (toList dlocs)))
                          fname
                          semhl
                          semal
                          semdef
    where
      resolvedLHS : (NonEmptyFC, (Nat, ClosedTerm)) -> Core (NonEmptyFC, (Nat, ClosedTerm))
      resolvedLHS (fc, (i, tm)) = pure (fc, (i, !(resolved gam tm)))

      resolvedTy : (NonEmptyFC, (Name, Nat, ClosedTerm)) -> Core (NonEmptyFC, (Name, Nat, ClosedTerm))
      resolvedTy (fc, (n, i, tm)) = pure (fc, (!(resolved gam n), i, !(resolved gam tm)))

      resolvedHLHS : (Name, ClosedTerm) -> Core (Name, ClosedTerm)
      resolvedHLHS (n, tm) = pure (!(resolved gam n), !(resolved gam tm))

      resolvedDecls : (NonEmptyFC, Name) -> Core (NonEmptyFC, Name)
      resolvedDecls (fc, n) = pure (fc, !(resolved gam n))

export
writeToTTM : {auto c : Ref Ctxt Defs} ->
             {auto m : Ref MD Metadata} ->
             (fname : String) ->
             Core ()
writeToTTM fname
    = do normaliseTypes
         buf <- initBinary
         meta <- get MD
         defs <- get Ctxt
         toBuf buf (MkTTMFile ttcVersion !(full (gamma defs) meta))
         Right ok <- coreLift $ writeToFile fname !(get Bin)
             | Left err => throw (InternalError (fname ++ ": " ++ show err))
         pure ()

export
readFromTTM : {auto m : Ref MD Metadata} ->
              (fname : String) ->
              Core ()
readFromTTM fname
    = do Right buf <- coreLift $ readFromFile fname
             | Left err => throw (InternalError (fname ++ ": " ++ show err))
         bin <- newRef Bin buf
         ttm <- fromBuf bin
         put MD (metadata ttm)

||| Read Metadata from given file
export
readMetadata : (fname : String) -> Core Metadata
readMetadata fname
  = do Right buf <- coreLift $ readFromFile fname
             | Left err => throw (InternalError (fname ++ ": " ++ show err))
       bin <- newRef Bin buf
       MkTTMFile _ md <- fromBuf bin
       pure md

||| Dump content of a .ttm file in human-readable format
export
dumpTTM : (filename : String) -> Core ()
dumpTTM fname
    = do md <- readMetadata fname
         coreLift $ putStrLn $ show md


text:
import Data.Container.Mutable.Array
import Data.Container.Mutable.Stack
import Data.Container.Mutable.Queue
import Data.Container.Mutable.RingQueue
import Data.Container.Mutable.Hashtable
import Data.Container.Mutable.Interfaces
import Data.Container.Immutable.Queue
import Data.Hash

import Data.List
import Data.So
import Data.Fin

chk0 : HasIO io => Bool -> io ()
chk0 b = putStr $ if b then "✓" else "✗"

main : IO ()
main = do
  do
    putStr "Array:"
    arr <- newIOArray 100 0
    (for [0..99] $ \i => readIOArray (fromInteger i) arr) >>= chk0 . all (Just 0 ==)
    --
    for_ [0..99] $ \i => writeIOArray (fromInteger i) i arr
    traverse (\i => readIOArray (fromInteger i) arr) [0..99]
      >>= chk0 . (== map Just [0..99])
    --
    readIOArray 100 arr >>= chk0 . (== Nothing)
    readIOArray 101 arr >>= chk0 . (== Nothing)
    putStrLn ""

  do
    putStr "IOArrayStack:"
    stk <- newIOArrayStack
    --
    chk0 !(null stk)
    --
    push 0 stk; push 1 stk
    chk0 $ not !(null stk)
    pop stk >>= chk0 . (Just 1 ==)
    pop stk >>= chk0 . (Just 0 ==)
    chk0 !(null stk)
    --
    for_ [0..5000] $ \i => push i stk
    (for [0..5000] $ \_ => pop stk) >>= chk0 . ((map Just [5000..0]) ==)

    for_ [5000..6000] $ \i => push i stk
    (for [0..1000] $ \_ => pop stk) >>= chk0 . ((map Just [6000..5000]) ==)
    putStrLn ""

  do
    putStr "IOArrayQueue:"
    q <- newIOArrayQueue
    --
    chk0 !(null q)
    --
    _ <- push 0 q; _ <- push 1 q
    chk0 $ not !(null q)
    length q >>= chk0 . (2 ==)
    --
    pull q >>= chk0 . (Just 0 ==)
    pull q >>= chk0 . (Just 1 ==)
    chk0 !(null q)
    length q >>= chk0 . (0 ==)
    --
    for_ [0..5000] $ \i => push i q
    (for [0..5000] $ \_ => pull q) >>= chk0 . ((map Just [0..5000]) ==)

    for_ [5000..6000] $ \i => push i q
    (for [0..1000] $ \_ => pull q) >>= chk0 . ((map Just [5000..6000]) ==)
    putStrLn ""

  do
    putStr "IORingQueue:"
    q <- newIORingQueue 100
    --
    chk0 !(null q)
    --
    _ <- push 0 q; _ <- push 1 q
    chk0 $ not !(null q)
    length q >>= chk0 . (2 ==)
    --
    pull q >>= chk0 . (Just 0 ==)
    pull q >>= chk0 . (Just 1 ==)
    chk0 !(null q)
    length q >>= chk0 . (0 ==)
    --
    for_ [0..99] $ \i => push i q
    push 100 q >>= chk0 . (False ==)
    (for [0..99] $ \_ => pull q) >>= chk0 . ((map Just [0..99]) ==)
    putStrLn ""

  do
    putStr "Hash:"
    {-
    print $ saltedHash 0xdeadbeef "123"
    print $ saltedHash 0xdeadbeef "456"
    print $ saltedHash 0xdeadbeef 123
    print $ saltedHash 0xdeadbeef 456
    -}
    putStrLn ""

  do
    putStr "IOHashtable:"
    ht <- the (IO (IOHashtable String Int)) $ newIOHashtable 512
    --
    chk0 !(null ht)
    --
    _ <- insert "abc" 0 ht
    _ <- insert "def" 1 ht
    _ <- insert "ghi" 2 ht
    chk0 $ not !(null ht)
    length ht >>= chk0 . (3 ==)
    lookup "abc" ht >>= chk0 . (Just 0 ==)
    lookup "def" ht >>= chk0 . (Just 1 ==)
    lookup "ghi" ht >>= chk0 . (Just 2 ==)
    --
    _ <- insert "def" 20 ht
    length ht >>= chk0 . (3 ==)
    lookup "def" ht >>= chk0 . (Just 20 ==)
    --
    _ <- delete "abc" ht
    length ht >>= chk0 . (2 ==)
    lookup "abc" ht >>= chk0 . (Nothing ==)
    putStrLn ""

  do
    putStr "Queue:"
    --
    let q = the (Queue Int) newQueue
    chk0 $ null q
    chk0 $ length q == 0
    --
    let xs = [1..100]
    let q0 = foldl (\acc, x => push x acc) q xs
    let (q1, xs') = foldl (\(q, ys), _ =>
                    let (y, q') = pull q
                     in (q', y::ys) ) (q0, []) xs
    chk0 $ not $ null q0
    chk0 $ length q0 == 100
    chk0 $ null q1
    chk0 $ length q1 == 0
    chk0 $ xs == reverse (catMaybes xs')
    --
    putStrLn ""


text:
-- examples in "Type-Driven Development with Idris"
-- chapter 12, section 2, part 1

import Tree

-- check that all functions are total
%default total

data State : (stateType : Type) -> Type -> Type where
  Get : State stateType stateType
  Put : stateType -> State stateType ()
  Pure : ty -> State stateType ty
  Bind : State stateType a -> (a -> State stateType b) -> State stateType b

get : State stateType stateType
get = Get

put : stateType -> State stateType ()
put = Put

pure : ty -> State stateType ty
pure = Pure

(>>=) : State stateType a -> (a -> State stateType b) -> State stateType b
(>>=) = Bind

runState : State stateType a -> (st : stateType) -> (a, stateType)
runState Get st = (st, st)
runState (Put newState) st = ((), newState)
runState (Pure x) st = (x, st)
runState (Bind cmd prog) st = let (val, nextState) = runState cmd st in
                                  runState (prog val) nextState

treeLabelWith : Tree a -> State (Stream labelType) (Tree (labelType, a))
treeLabelWith Empty = pure Empty
treeLabelWith (Node left val right)
  = do lblleft <- treeLabelWith left
       (lblthis :: rest) <- get
       put rest
       lblright  <- treeLabelWith right
       pure (Node lblleft (lblthis, val) lblright)

treeLabel : Tree a -> Tree (Integer, a)
treeLabel tree = fst (runState (treeLabelWith tree) [1..])


text:
module Compiler.ES.Imperative

import public Compiler.ES.ImperativeAst

import Data.List

import Compiler.Common
import Compiler.CompileExpr

import public Core.Context

import Compiler.ES.RemoveUnused
import Compiler.ES.TailRec

mutual
  isNameUsed : Name -> NamedCExp -> Bool
  isNameUsed name (NmLocal fc n) = n == name
  isNameUsed name (NmRef fc n) = n == name
  isNameUsed name (NmLam fc n e) = isNameUsed name e
  isNameUsed name (NmApp fc x args) = isNameUsed name x || any (isNameUsed name) args
  isNameUsed name (NmPrimVal fc c) = False
  isNameUsed name (NmOp fc op args) = any (isNameUsed name) args
  isNameUsed name (NmConCase fc sc alts def) = isNameUsed name sc || any (isNameUsedConAlt name) alts  || maybe False (isNameUsed name) def
  isNameUsed name (NmConstCase fc sc alts def) = isNameUsed name sc || any (isNameUsedConstAlt name) alts  || maybe False (isNameUsed name) def
  isNameUsed name (NmExtPrim fc p args) = any (isNameUsed name) args
  isNameUsed name (NmCon fc x t args) = any (isNameUsed name) args
  isNameUsed name (NmDelay fc t) = isNameUsed name t
  isNameUsed name (NmForce fc t) = isNameUsed name t
  isNameUsed name (NmLet fc x val sc) =
    if x == name then isNameUsed name val
      else isNameUsed name val || isNameUsed name sc
  isNameUsed name (NmErased fc) = False
  isNameUsed name (NmCrash fc msg) = False

  isNameUsedConAlt : Name -> NamedConAlt -> Bool
  isNameUsedConAlt name (MkNConAlt n t args exp) = isNameUsed name exp

  isNameUsedConstAlt : Name -> NamedConstAlt -> Bool
  isNameUsedConstAlt name (MkNConstAlt c exp) = isNameUsed name exp

data Imps : Type where

record ImpSt where
  constructor MkImpSt
  nextName : Int

genName : {auto c : Ref Imps ImpSt} -> Core Name
genName =
  do
    s <- get Imps
    let i = nextName s
    put Imps (record { nextName = i + 1 } s)
    pure $ MN "imp_gen" i

mutual
  ifThenElse : Bool -> a -> a -> a
  ifThenElse True t e = t
  ifThenElse False t e = e

  pairToReturn : (toReturn : Bool) -> (ImperativeStatement, ImperativeExp) ->
                     Core (ifThenElse toReturn ImperativeStatement  (ImperativeStatement, ImperativeExp))
  pairToReturn False (s, e) = pure (s, e)
  pairToReturn True (s, e) = pure $ s <+> ReturnStatement e

  expToReturn : (toReturn : Bool) -> ImperativeExp ->
                     Core (ifThenElse toReturn ImperativeStatement  (ImperativeStatement, ImperativeExp))
  expToReturn False e = pure $ (DoNothing, e)
  expToReturn True e = pure $ ReturnStatement e

  impVectExp : {auto c : Ref Imps ImpSt} -> Vect n NamedCExp -> Core (ImperativeStatement, Vect n ImperativeExp)
  impVectExp args =
    do
      a <- traverseVect (impExp False) args
      pure (concat (map fst a), map snd a)

  impListExp : {auto c : Ref Imps ImpSt} -> List NamedCExp -> Core (ImperativeStatement, List ImperativeExp)
  impListExp args =
    do
      a <- traverse (impExp False) args
      pure (concat (map fst a), map snd a)

  impExp : {auto c : Ref Imps ImpSt} -> (toReturn : Bool) -> NamedCExp ->
                     Core (ifThenElse toReturn ImperativeStatement  (ImperativeStatement, ImperativeExp))
  impExp toReturn (NmLocal fc n) = expToReturn toReturn $ IEVar n
  impExp toReturn (NmRef fc n) = expToReturn toReturn $ IEVar n
  impExp toReturn (NmLam fc n e) = expToReturn toReturn $ IELambda [n] !(impExp True e)
  impExp toReturn (NmApp fc x args) =
    do
      (s1, f) <- impExp False x
      (s2, a) <- impListExp args
      pairToReturn toReturn (s1 <+> s2, IEApp f a)
  impExp toReturn (NmPrimVal fc c) = expToReturn toReturn $ IEConstant c
  impExp toReturn (NmOp fc op args) =
    do
      (s, a) <- impVectExp args
      pairToReturn toReturn (s, IEPrimFn op a)
  impExp False (NmConCase fc sc alts def) =
    do
      (s1, exp) <- impExp False sc
      res <- genName
      swalts <- traverse (impConAlt (Just res) exp) alts
      swdef <- case def of
                Nothing => pure $ ErrorStatement $ "unhandled con case on " ++ show fc
                Just x =>
                  do
                    (sd, r) <- impExp False x
                    pure $ sd <+> MutateStatement res r
      let switch = SwitchStatement (IEConstructorHead exp) swalts (Just swdef)
      pure (s1 <+> LetDecl res Nothing <+> switch, IEVar res)
  impExp True (NmConCase fc sc alts def) =
    do
      (s1, exp) <- impExp False sc
      swalts <- traverse (impConAlt Nothing exp) alts
      swdef <- case def of
                Nothing => pure $ ErrorStatement $ "unhandled con case on " ++ show fc
                Just x => impExp True x
      let switch = SwitchStatement (IEConstructorHead exp) swalts (Just swdef)
      pure (s1 <+> switch)
  impExp False (NmConstCase fc sc alts def) =
    do
      (s1, exp) <- impExp False sc
      res <- genName
      swalts <- traverse (impConstAlt $ Just res) alts
      swdef <- case def of
                Nothing => pure $ ErrorStatement $ "unhandled const case on " ++ show fc
                Just x =>
                  do
                    (sd, r) <- impExp False x
                    pure $ sd <+> MutateStatement res r
      let switch = SwitchStatement exp swalts (Just swdef)
      pure (s1 <+> LetDecl res Nothing <+> switch, IEVar res)
  impExp True (NmConstCase fc sc alts def) =
    do
      (s1, exp) <- impExp False sc
      swalts <- traverse (impConstAlt Nothing) alts
      swdef <- case def of
                Nothing => pure $ ErrorStatement $ "unhandled const case on " ++ show fc
                Just x => impExp True x
      let switch = SwitchStatement exp swalts (Just swdef)
      pure $ s1 <+> switch
  impExp toReturn (NmExtPrim fc p args) =
    do
      (s, a) <- impListExp args
      pairToReturn toReturn (s, IEPrimFnExt p a)
  impExp toReturn (NmCon fc x tag args) =
    do
      (s, a) <- impListExp args
      pairToReturn toReturn (s, IEConstructor (impTag x tag) a)
  impExp toReturn (NmDelay fc t) =
    do
      (s, x) <- impExp False t
      pairToReturn toReturn (s, IEDelay x)
  impExp toReturn (NmForce fc t) =
    do
      (s, x) <- impExp False t
      pairToReturn toReturn (s, IEForce x)
  impExp toReturn (NmLet fc x val sc) =
    do
      (s1, v) <- impExp False val
      (s2, sc_) <- impExp False sc
      let decl  = if isNameUsed x sc then ConstDecl x v else EvalExpStatement v
      pairToReturn toReturn (s1 <+> decl <+> s2, sc_)
  impExp toReturn (NmErased fc) =
    expToReturn toReturn $ IENull
  impExp toReturn (NmCrash fc msg) =
    pairToReturn toReturn (ErrorStatement msg, IENull)

  impTag : Name -> Maybe Int -> Either Int String
  impTag n Nothing = Right $ show n
  impTag n (Just i) = Left i

  impConAlt : {auto c : Ref Imps ImpSt} -> Maybe Name -> ImperativeExp -> NamedConAlt -> Core (ImperativeExp, ImperativeStatement)
  impConAlt (Just res) target (MkNConAlt n tag args exp) =
    do
      (s, r) <- impExp False exp
      let nargs = length args
      let reps = zipWith (\i, n => (n, IEConstructorArg (cast i) target)) [1..nargs] args
      pure (IEConstructorTag (impTag n tag), replaceNamesExpS reps $ s <+> MutateStatement res r)
  impConAlt Nothing target (MkNConAlt n tag args exp) =
    do
      (s, r) <- impExp False exp
      let nargs = length args
      let reps = zipWith (\i, n => (n, IEConstructorArg (cast i) target)) [1..nargs] args
      pure (IEConstructorTag (impTag n tag), replaceNamesExpS reps $ s <+> ReturnStatement r)

  impConstAlt : {auto c : Ref Imps ImpSt} -> Maybe Name -> NamedConstAlt -> Core (ImperativeExp, ImperativeStatement)
  impConstAlt (Just res) (MkNConstAlt c exp) =
    do
      (s, r) <- impExp False exp
      pure (IEConstant c, s <+> MutateStatement res r)
  impConstAlt Nothing (MkNConstAlt c exp) =
    do
      (s, r) <- impExp False exp
      pure (IEConstant c, s <+> ReturnStatement r)

getImp : {auto c : Ref Imps ImpSt} -> (Name, FC, NamedDef) -> Core ImperativeStatement
getImp (n, fc, MkNmFun args exp) =
  pure $ FunDecl fc n args !(impExp True exp)
getImp (n, fc, MkNmError exp) =
  throw $ (InternalError $ show exp)
getImp (n, fc, MkNmForeign cs args ret) =
  pure $ ForeignDecl fc n cs args ret
getImp (n, fc, MkNmCon _ _ _) =
  pure DoNothing

export
compileToImperative : Ref Ctxt Defs -> ClosedTerm -> Core (ImperativeStatement, ImperativeStatement)
compileToImperative c tm =
  do
    cdata <- getCompileData Cases tm
    let ndefs = namedDefs cdata
    let ctm = forget (mainExpr cdata)
    s <- newRef Imps (MkImpSt 0)
    lst_defs <- traverse getImp (defsUsedByNamedCExp ctm ndefs)
    let defs = concat lst_defs
    let defs_optim = tailRecOptim defs
    (s, main) <- impExp False ctm
    pure $ (defs_optim, s <+> EvalExpStatement main)


text:
module Dart.FFI.Upcast

||| Instances of type [subclass] can be [upcast] to type [superclass].
public export
interface IsAssignableFrom superclass subclass where
  %inline
  upcast : subclass -> superclass
  upcast sub = believe_me sub

public export
IsAssignableFrom a a where

-- public export
-- (IsAssignableFrom a b, IsAssignableFrom b c) => IsAssignableFrom a c where


text:
module Data.Map

%default total

export
data Map  : (key : Type) -> (VF : key -> Type) -> Type where
  MNil    : .{VF : key -> Type} -> Map key VF
  MBranch : (DecEq key, Ord key) =>
                       .{VF : key -> Type}
                    -> (k   : key)
                    -> (val : VF  k     )
                    -> (l   : Map key VF)
                    -> (r   : Map key VF)
                    -> Map key VF

%name Map map, map2, map3

empty : Map k p
empty = MNil

insert : (DecEq key, Ord key) => (k : key) -> p k -> Map key p -> Map key p
insert k x MNil = MBranch k x MNil MNil
insert k x (MBranch kr val l r) =
  case compare k kr of
    LT => MBranch kr val (insert k x l) r
    EQ => MBranch k x l r
    GT => MBranch kr val l (insert k x r)

lookup : (DecEq key, Ord key) => (k : key) -> Map key p -> Maybe (p k)
lookup _ MNil = Nothing
lookup k (MBranch kr val l r) =
  case decEq k kr of
    Yes prf => rewrite prf in Just val
    No  _   => case compare k kr of
                 LT => lookup k l
                 _  => lookup k r

insertWith : (DecEq key, Ord key) => (k : key) -> p k -> (p k -> p k -> p k) -> Map key p -> Map key p
insertWith k x f m =
  case lookup k m of
    Just v => insert k (f x v) m
    Nothing => insert k x m
-- it would be nice to implement this with one traversal,
-- but having a hard time rewriting some types
-- insertWith k x f MNil = MBranch k x MNil MNil
-- insertWith {p} k x f (MBranch kr val l r) =
--   case decEq kr k of
--     Yes prf => MBranch k (f x val) l r
--     No  _   => case compare k kr of
--                  LT => insertWith k x f l
--                  _  => insertWith k x f r

fromList : (DecEq key, Ord key) => List (k : key ** p k) -> Map key p
fromList [] = MNil
fromList ((k ** v) :: xs) = insert k v $ fromList xs

max_stars_repo_name: jhmcstanton/idris-sandbox

max_issues_repo_name: jhmcstanton/idris-sandbox

max_forks_repo_name: jhmcstanton/idris-sandbox


text:
import Data.Vect

Matrix : Nat -> Nat -> Type -> Type
Matrix m n elem = Vect m (Vect n elem)

qualify : (name : String) -> (adjective : String) -> String
qualify name adjective = name ++ " is " ++ adjective

repeat : (n : Nat) -> a -> Vect n a
repeat Z x = []
repeat (S k) x = x :: repeat k x

insertCol :    (x : Vect n elem)
            -> (xs : Matrix n len elem)
            -> Matrix n (S len) elem
insertCol [] [] = []
insertCol (x :: xs) (y :: ys) = (x :: y) :: insertCol xs ys

insertCol' : (x : Vect n elem) -> (xs : Matrix n len elem) -> Matrix n (S len) elem
insertCol' = zipWith (::)

-- The tutorial shows that just putting an underscore instead
-- of n does the job in this case
-- (An there would be no need for the {n} there)
transpose' : Matrix m n elem -> Matrix n m elem
transpose' {n} [] = repeat n []
transpose' (x :: xs) = insertCol x $ transpose' xs

addMatrix : Num e => Matrix m n e -> Matrix m n e -> Matrix m n e
addMatrix [] [] = []
addMatrix (x :: xs) (y :: ys) = [| x + y |] :: addMatrix xs ys

productSum : Num e => Vect n e -> Vect n e -> e
productSum xs ys = sum [| xs * ys |]

distributeOver : (a -> a -> c)
               -> a -> Vect m a -> Vect m c
distributeOver f x xs = map (f x) xs

multMatrixHelper : Num e => Matrix m n e
                         -> Matrix o n e
                         -> Matrix m o e
multMatrixHelper [] [] = []
multMatrixHelper [] (x :: xs) = []
multMatrixHelper (x :: xs) ys =
  -- let distributed = distributeOver productSum x ys
  let distributed = map (productSum x) ys
  in distributed :: multMatrixHelper xs ys

multMatrix : Num e => Matrix m n e
                   -> Matrix n o e
                   -> Matrix m o e
multMatrix x y = multMatrixHelper x (transpose' y)


text:
module SemVar.Lexer

import Text.Lexer
import Text.Token

import public SemVar.Tokens

%default total

private
semVarTokenMap : TokenMap SemVarToken
semVarTokenMap = toTokenMap $
  [ (is '~', Tilde)
  , (is '^', Caret)
  , (is '.', Dot)
  , (digits, Number)
  , (is '-', Hyphen)
  , (exact ">=", CmpGTE)
  , (exact "<=", CmpLTE)
  , (is '>', CmpGT)
  , (is '<', CmpLT)
  , (is '=', CmpEQ)
  , (exact "||", Pipe)
  , (is '+', Plus)
  , (some alphaNum, Text)
  , (is '*', Asterisk)
  , (spaces, Whitespace)
  ]

public export
lexSemVar : String -> Maybe (List $ WithBounds SemVarToken)
lexSemVar str
  = case lex semVarTokenMap str of
         (tokens, _, _, "") => Just $ tokens
         _ => Nothing

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
-- Prototype of RealizedAttributes as described in
-- https://blog.singularitynet.io/ai-dsl-toward-a-general-purpose-description-language-for-ai-agents-21459f691b9e

module RealizedAttributes

-- NEXT: used dependent types to type check attributes, take
-- inspiration from NonDTRealizedAttributes.idr and
-- SimpleRealizedFunction.idr


text:
libcb : String -> String
libcb f = "C:" ++ f ++", libcb"

%foreign libcb "add"
add : Int -> Int -> Int

%foreign libcb "applyIntFn"
prim_applyIntFn : Int -> Int -> (Int -> Int -> PrimIO Int) -> PrimIO Int

%foreign libcb "applyCharFn"
prim_applyCharFn : Char -> Int -> (Char -> Int -> PrimIO Char) -> PrimIO Char

%foreign libcb "applyIntFnPure"
applyIntFnPure : Int -> Int -> (Int -> Int -> Int) -> Int

applyIntFn : Int -> Int -> (Int -> Int -> IO Int) -> IO Int
applyIntFn x y fn
    = primIO $ prim_applyIntFn x y (\a, b => toPrim (fn a b))

applyCharFn : Char -> Int -> (Char -> Int -> IO Char) -> IO Char
applyCharFn x y fn
    = primIO $ prim_applyCharFn x y (\a, b => toPrim (fn a b))

cb : Int -> Int -> IO Int
cb x y
    = do putStrLn $ "In callback with " ++ show (x, y)
         pure (x + y)

main : IO ()
main
    = do printLn (add 4 5)
         res <- applyIntFn (add 4 5) 6 (\x, y => do putStrLn "In callback"
                                                    pure (x * 2 + y))
         printLn res
         res <- applyIntFn 1 2 cb
         printLn res
         printLn (applyIntFnPure 5 4 (\x, y => x + y))
         res <- applyCharFn 'a' 10 (\x, y => pure (cast (cast x + y)))
         printLn res

max_stars_repo_name: boxfire/rapid

max_issues_repo_name: boxfire/rapid

max_forks_repo_name: boxfire/rapid


text:
module Replica.Command.Version

import Data.List1

import Replica.Help
import Replica.Option.Types
import Replica.Version

public export
data Version = MkVersion String

export
parseVersion : List1 String -> ParseResult Version
parseVersion ("version" ::: xs) = Done $ MkVersion "replica version \{version}"
parseVersion xs = InvalidOption xs

export
helpVersion : Help
helpVersion = MkHelp
  "version" (Just "replica version")
  "Show replica version"
  []
  Nothing

max_stars_repo_name: claymager/REPLica

max_issues_repo_name: claymager/REPLica

max_forks_repo_name: claymager/REPLica


text:
module RingProperties

import Ring
import Monoid
import Group
import Group_property

%access public export

|||Auxiliary function that provzs that if a+a=a thzn a=0
total
aplusaZ: (r: Type) -> (pfr: Ring r) -> (a: r) -> ((Ring_Add r pfr a a) =a) -> (a = (DPair.fst(RingAdditive_id r pfr)))
aplusaZ r (MkRing r (+) (*) pfr) a prf = (Group_property_4 r (+) (Basics.fst (Basics.fst pfr)) a a z (trans prf (sym (Basics.fst (pfz a))) )) where
  z: r
  z = (DPair.fst(RingAdditive_id r (MkRing r (+) (*) pfr)))
  pfz: (a: r) -> (a+z=a, z+a=a)
  pfz = DPair.snd (RingAdditive_id r (MkRing r (+) (*) pfr))

|||Proof that 0*a = 0
total
Zmultleft: (r: Type) -> (pfr: Ring r) -> (a: r) -> ((Ring_Mult r pfr (DPair.fst(RingAdditive_id r pfr)) a) = (DPair.fst(RingAdditive_id r pfr)))
Zmultleft r (MkRing r (+) (*) pfr) a = (aplusaZ r (MkRing r (+) (*) pfr) (z*a) (
    trans (sym (pfd a z z)) (cong {f= \p => p*a} (pfz z))
  ) ) where
  z: r
  z = (DPair.fst(RingAdditive_id r (MkRing r (+) (*) pfr)))
  pfz: (a: r) -> (a+z=a)
  pfz a = Basics.fst ((DPair.snd (RingAdditive_id r (MkRing r (+) (*) pfr))) a)
  pfd: (a: r) -> (b: r) -> (c: r) -> ((b+c)*a = (b*a) + (c*a))
  pfd a b c = Basics.snd ((Basics.snd (Basics.snd pfr)) a b c)

|||Proof that a*0 = 0
total
Zmultright: (r: Type) -> (pfr: Ring r) -> (a: r) -> ((Ring_Mult r pfr a (DPair.fst(RingAdditive_id r pfr))) = (DPair.fst(RingAdditive_id r pfr)))
Zmultright r (MkRing r (+) (*) pfr) a = (aplusaZ r (MkRing r (+) (*) pfr) (a*z) (
    trans (sym (pfd a z z)) (cong {f= \p => a*p} (pfz z))
    ) ) where
    z: r
    z = (DPair.fst(RingAdditive_id r (MkRing r (+) (*) pfr)))
    pfz: (a: r) -> (a+z=a)
    pfz a = Basics.fst ((DPair.snd (RingAdditive_id r (MkRing r (+) (*) pfr))) a)
    pfd: (a: r) -> (b: r) -> (c: r) -> (a*(b+c) = (a*b) + (a*c))
    pfd a b c = Basics.fst ((Basics.snd (Basics.snd pfr)) a b c)

|||Proof that for a ring homomorphism f between rings with identity, f(0) = 0
total
RHomZtoZ: (r1: Type) -> (pf1: Ring r1) -> (r2: Type) -> (pf2: Ring r2) -> (f: r1 -> r2) -> RHom r1 pf1 r2 pf2 f -> f(fst(RingAdditive_id r1 pf1)) = fst (RingAdditive_id r2 pf2)
RHomZtoZ r1 (MkRing r1 ((+)) (m) pf1) r2 (MkRing r2 (*) m1 pf2) f pfhom = aplusaZ r2 (MkRing r2 (*) m1 pf2) (f z1) (
    trans
    (sym (Basics.fst(pfhom z1 z1)))
    (cong (Basics.fst(pfid1 z1)))
    ) where
  z1: r1
  z1 = fst(RingAdditive_id r1 (MkRing r1 ((+)) (m) pf1))
  pfid1: (a : r1) -> ((a+z1) = a, (z1+a) = a)
  pfid1 = snd(RingAdditive_id r1 (MkRing r1 ((+)) (m) pf1))

|||Proof that for a ring homomorphism f, f(0) = 0
total
IRHomZtoZ: (r1: Type) -> (pf1: Ring_with_identity r1) -> (r2: Type) -> (pf2: Ring_with_identity r2) -> (f: r1 -> r2) -> IRHom r1 pf1 r2 pf2 f -> f(fst(RingAdditive_id r1 (Ring_with_identity_isRing r1 pf1))) = fst (RingAdditive_id r2 (Ring_with_identity_isRing r2 pf2))
IRHomZtoZ r1 (MkRing_with_identity r1 ((((+)))) (m) (a, b)) r2 (MkRing_with_identity r2 (((*))) (m1) (a', b')) f pfhom = aplusaZ r2 prf2 (f z1) (
    trans
    (sym (Basics.fst(pfhom z1 z1)))
    (cong (Basics.fst(pfid1 z1)))
    ) where
  prf1: Ring r1
  prf1 = MkRing r1 (+) (m) (a, ((Basics.fst (Basics.fst b)), (Basics.snd b)))
  prf2: Ring r2
  prf2 = MkRing r2 (*) (m1) (a', ((Basics.fst (Basics.fst b')), (Basics.snd b')))
  z1: r1
  z1 = fst(RingAdditive_id r1 prf1)
  pfid1: (a : r1) -> ((a + z1) = a, (z1 + a) = a)
  pfid1 a = snd(RingAdditive_id r1 prf1) a


text:
-- Find the sum of all the multiples of 3 or 5 below 1000.

isMultiple : Int -> Int -> Bool
isMultiple n m = (mod n m) == 0

main : IO ()
main = print (sum [x | x <- [1..999], isMultiple x 3 || isMultiple x 5])

max_stars_repo_name: edu-di-wu/project-euler

max_issues_repo_name: edu-di-wu/project-euler

max_forks_repo_name: edu-di-wu/project-euler