Require Import Program. (* for compose, identity *)
Require Import Arith.  (* for leb, negb *)
Require Import List. (* for filter *)

Definition ident x := x.
Error: Cannot infer the type of x.

Definition ident_n (x:nat) := x.
Compute ident_n 3.

Definition ident (X:Type) (x:X) := x.

Compute ident nat 3.
Compute ident bool true.
Compute ident nat true.
Error: The term “true” has type “bool” while
it is expected to have type “nat”.

Definition ident2 {X:Type} (x:X) := x.
ident2 is defined
Compute ident2 3.
Compute ident2 true.

(*alternately, define them after the fact: *)

Implicit Arguments ident [X].
Compute ident 3.
Compute ident true.
Print Implicit ident.
Print Implicit ident2.



(* pass functions around *)
Check map.
Check mult 2.
Compute map (mult 2) (1::2::3::4::nil).
Compute map ident [1;2;3;4].  (* doesn't work - not maximally inserted *)
Compute map ident2 [1;2;3;4].

(* return functions *)
Check leb.
Compute map (leb 3) [1;2;3;4;5;6].
Compute map (fun x => (leb x 3)) [1;2;3;4;5;6].

Definition mycompose {A B C : Type} (g : B -> C) (f : A -> B) :=  
   fun x => g (f x).

(* Check mycompose negb leb. *)
Check mycompose negb (leb 3).
Compute mycompose negb (leb 3).

Definition mycompose2 {A B C : Type} (g : B -> C) (f : A -> B) (x : A) :=  
   g (f x).

Check mycompose negb (leb 3).
Check mycompose2 negb (leb 3).

(* we think they're the same... let's see! [don't take my word for it]*)
Theorem compose_uncurry_eq : forall (A B C : Type) (f : B -> C) (g : A -> B) (x : A),
       mycompose f g x = mycompose2 f g x.
intros.
(* simpl. *)
compute.
reflexivity.
Qed.

(* generalizing *)
Fixpoint sum (l : list nat) := 
  match l with 
     nil => 0
   | n :: ns => plus n (sum ns)
  end.

Check plus.

Fixpoint product (l: list nat) :=
  match l with 
     nil => 1
   | n :: ns => mult n (product ns)
  end.

Fixpoint fold_rt {A B:Type} (f:A->B->B) (z:B) (l:list A) := 
  match l with 
     nil => z
   | n :: ns => f n (fold_rt f z ns)
  end.

Definition sum2 l := fold_rt plus 0 l.
Definition prod2 := fold_rt mult 1.

Compute sum2 [1;2;4].
Compute prod2 [1;2;4].

Check fold_right.
Check fold_left. 

(* passing 'cons' and 'nil' gives the identity on lists *)
Compute fold_right cons nil [true;false;false].

(* using fold_left with the same gives a reverse on lists *)
(*   ['flip' swaps the first two arguments of a function] *)
Compute fold_left (flip cons) [true;false;false] nil.

(* 
(* A good excercise to do ?  *)
Theorem fl_fr_assoc_equiv : forall (A:Type) (f:A->A->A) (l:list A),
  (forall (x y z:A), (f x (f y z)) = (f (f x y) z)) ->
  (forall (z:A), fold_left f l z = fold_right f z l).

(* end excercise *) *)

Check filter
Check compose.
Print Implicit compose.
SearchAbout compose.
Infix "o" := compose (at level 40, left associativity).
SearchAbout compose.
Locate "_ o _".

(*
Fixpoint quicksort_n xs := 
  match xs with
     nil => nil
   | cons p xs' => 
        let less := filter (compose negb (leb p)) xs' in
        let more := filter (leb p) xs' in 
        (quicksort_n less) ++ (p :: nil) ++ (quicksort_n more)
  end.
(* doesn't work! *) *)

Inductive Len := 
   Lnnil : Len
 | Lncons : Len -> Len.

Fixpoint toLen (l : list nat) : Len :=
  match l with
     nil => Lnnil
   | (x::xs) => Lncons (toLen xs) 
  end.

(* not needed yet!*)
Fixpoint fromLen (len : Len) :=
  match len with
     Lnnil => 0
   | Lncons l' => S (fromLen l')
  end.

Fixpoint quicksort_nl lst len := 
  match len with
     Lnnil => nil
   | Lncons l => 
       match lst with 
          nil => nil 
        | cons x xs => 
           let less := filter (compose negb (leb x)) xs in 
           let more := filter (leb x) xs in
           (quicksort_nl less l) ++ (cons x nil) ++ (quicksort_nl more l)
       end
  end.

Definition quicksort_n lst := quicksort_nl lst (toLen lst).

Compute quicksort_n (4::2::77::23::1::0::34::nil).
Compute quicksort_n [34; 23;1;6;2;4;7;2;234;7;2].

(* polymorphic version *)

Fixpoint quicksort_l {A:Type} (leb:A->A->bool) (lst:list A) (len:Len) := 
  match len with
     Lnnil => nil
   | Lncons l => 
       match lst with 
          nil => nil 
        | cons x xs => 
           let less := filter (compose negb (leb x)) xs in 
           let more := filter (leb x) xs in
           (quicksort_l leb less l) ++ (cons x nil) ++ (quicksort_l leb more l)
       end
  end.

Check toLen.
Fixpoint toLenA {A:Type} (l:list A) :=
  match l with
     nil => Lnnil
   | cons _ l' => Lncons (toLenA l')
  end. 

Definition quicksort {A:Type} cmp (lst:list A) := quicksort_l cmp lst (toLenA lst).
Check quicksort.
Check quicksort_l.

Compute quicksort leb (4::2::77::23::1::0::34::nil).
Compute quicksort leb [34; 23;1;6;2;4;7;2;234;7;2].

Compute quicksort (fun x => negb o (leb x)) [34;23;1;6;2;4;7;2;234;7;2].