gistfile1.v

(*Solution 1*)
Set Implicit Arguments.
Require Import String.

Inductive Tree :=
| Leaf : Tree
| Node : Tree -> Tree -> Tree.
Definition compTree (a b:Tree) : {a=b}+{a<>b}.
 decide equality.
Defined.

Class Serialize (A : Type) :=
{ fromTree : Tree -> A
; toTree : A -> Tree
; Serialize0 : forall a, fromTree (toTree a) = a
 (*that means, you cannot serialize functions*)
}.
Instance SUnit : Serialize unit :=
 { fromTree := fun _ => tt; toTree := fun _ => Leaf }.
Proof. (*Serialize0*)
 clear; abstract (intros []; split).
Defined.
Instance SPair A B `{Serialize A} `{Serialize B} : Serialize (prod A B) :=
{ fromTree := fun t => match t with Leaf => (fromTree Leaf, fromTree Leaf)
                                  | Node a b => (fromTree a, fromTree b)
                       end
; toTree := fun p => Node (toTree (fst p)) (toTree (snd p))
}.
Proof. (*Serialize0*)
 clear; abstract (intros [a b]; simpl; repeat rewrite Serialize0; split).
Defined.
Instance SNat : Serialize nat :=
{ fromTree := fix fT t := match t with Leaf => O
                                     | Node n _ => S (fT n)
                          end
; toTree := fix tT n := match n with O => Leaf | S n => Node (tT n) Leaf end
}.
Proof. (*Serialize0*)
 clear; abstract (intros n; induction n; simpl; [|rewrite IHn]; split).
Defined.

Class Monad (m : Type -> Type) :=
{ ret : forall A, A -> m A
; bind : forall A B, m A -> (A -> m B) -> m B
; Monad0 : forall A B (f:A->m B) (a:A), bind (ret a) f = f a
; Monad1 : forall A (x: m A), bind x (fun y => ret y) = x
; Monad2 : forall A B C (f:m A) (g:A->m B) (h:B->m C),
           bind (bind f g) h = bind f (fun x => bind (g x) h)
}.
Notation "m >>= f" := (@bind _ _ _ _ m f)
(at level 55, right associativity).

Inductive Maybe (A : Type) := Nothing : Maybe A | Just : A -> Maybe A.
Instance MMaybe : Monad Maybe :=
 { ret := Just
 ; bind := fun A B x f => match x with
                          | Nothing => Nothing B
                          | Just y => f y
                          end
 }.
Proof. (*Monad0*)
 clear; abstract (split).
Proof. (*Monad1*)
 clear; abstract (intros A [|a]; split).
Proof. (*Monad2*)
 clear; abstract (intros A B C [|a]; split).
Defined.

Inductive Res (A : Type) :=
| Exn : Tree ->     (* kind          *)
        Tree ->     (* value         *)
        Res A       (* EXceptioN     *)
| Nex : A -> Res A  (* Non-EXception *)
.

Instance MRes : Monad Res :=
 { ret := Nex
 ; bind := fun A B x f => match x with
                          | Nex a => f a
                          | Exn k v => Exn B k v
                          end
 }.
Proof. (*Monad0*)
 clear; abstract (split).
Proof. (*Monad1*)
 clear; abstract (intros A [k v|a]; split).
Proof. (*Monad2*)
 clear; abstract (intros A B C [k v|a] g h; split).
Defined.

Class Exception (A : Type) := { serialize : Serialize A; kind : Tree }.
Instance SException (A : Type) `{Exception A} : Serialize A := serialize.

Definition throw A B `{Exception B} (b:B): Res A :=
 Exn A kind (toTree b).

Definition catch A B `{Exception B} (m : Res A) (f : B -> Res A) : Res A :=
 match m with
 | Nex a => ret a
 | Exn k v => if compTree k kind
              then f (fromTree v)
              else m
 end.

(* Exemple of lemma *)
Lemma catch_throw : forall B `{Exception B} (b:B),
      catch (throw B b) (fun x => ret x) = ret b.
Proof.
 unfold catch, throw; intros.
 destruct (compTree kind kind).
  rewrite Serialize0.
  split.
 now destruct n.
Qed.

Module Examples.

Record DivisionByZero := DBZ.
Instance SDivisionByZero : Serialize DivisionByZero :=
 { fromTree := fun _ => DBZ; toTree := fun _ => Leaf }.
Proof. (*Serialize0*)
 clear; abstract (intros []; split).
Defined.
Instance EDivisionByZero : Exception DivisionByZero :=
{ serialize := SDivisionByZero
; kind := Leaf
}.

Record IndexOutOfBounds := IOOB { request : nat; max : nat }.
Instance SIndexOutOfBounds : Serialize IndexOutOfBounds :=
{ toTree := fun x => toTree (request x, max x)
; fromTree := fun t => let p:prod nat nat := fromTree t in
                       {|request := fst p; max := snd p|}
}.
Proof. (*Serialize0*)
 clear; abstract (intros a; rewrite Serialize0; destruct a; split).
Defined.
Instance EIndexOutOfBounds : Exception IndexOutOfBounds :=
{ serialize := SIndexOutOfBounds
; kind := Node Leaf Leaf
}.

Record NonPositiveResult := NPR.
Instance SNonPositiveResult : Serialize NonPositiveResult :=
 { fromTree := fun _ => NPR; toTree := fun _ => Leaf }.
Proof. (*Serialize0*)
 clear; abstract (intros []; split).
Defined.
Instance ENonPositiveResult : Exception NonPositiveResult :=
{ serialize := SNonPositiveResult
; kind := Leaf
}.

(* Example *)
Definition get (A:Type) : nat -> list A -> Res A :=
 (fix _get_ acc i l :=
      match l with
      | nil => throw A (IOOB (i+acc) acc)
      | cons a l => match i with
                    | O => ret a
                    | S i => _get_ (S acc) i l
                    end
      end) O.
Fixpoint predminus (m n : nat) : Res {o : nat | o < m} :=
(* computes m-n-1 *)
 match m as m0 return Res {o : nat | o < m0} with
 | O => throw _ NPR
 | S m => match n with
          | O => ret (exist _ m (le_n _))
          | S n => predminus m n >>=
                   (fun (s : sig _) =>
                    let (o, proof) := s in
                    ret (exist _ o (le_S _ _ proof)))
          end
 end
.

Lemma lt_acc : forall m, Acc (fun x y => x < y) m.
Proof.
 intros m; induction m; split; intros.
  change (match O with O => Acc (fun x y => x < y) y | _ => True end).
  destruct H; split.
 change (Acc (fun x y => x < y) (match S m with S m => m | O => O end)) in IHm.
 destruct H.
  assumption.
 destruct IHm; auto.
Defined.

Definition div (m n : nat) : Res nat :=
 match n with
 | O => throw nat DBZ
 | S n =>
 (fix _div_ m (acc : Acc (fun x y => x < y) m) {struct acc} : Res nat :=
  match acc with Acc_intro f =>
      catch ((predminus m n) >>=
              fun (s:sig _) => let (x, p) := s in _div_ x (f x p) >>=
              fun x => ret (S x))
            (fun (_:NonPositiveResult) => ret O)
  end) m (lt_acc m)
 end.

Fixpoint string_of_nat (n:nat) :=
 match n with
 | O => "0"%string
 | S n => append "1+"%string (string_of_nat n)
 end.

Definition div_in_list (divided:nat) (divider:list nat) (index:nat) : Res string :=
  catch
 (catch (get index divider >>=
         fun divi => div divided divi >>=
         fun quo => ret (string_of_nat quo))
 (fun (_:DivisionByZero) => ret "Division by zero!"%string))
 (fun (e:IndexOutOfBounds) =>
            ret (append "tried to access the "%string
                (append (string_of_nat (request e))
                (append " out of "%string
                        (string_of_nat (max e))))))
.

Example L := cons 3 (cons 0 (cons 1 nil)).
Compute (div_in_list 5 L 0).
Compute (div_in_list 5 L 1).
Compute (div_in_list 5 L 2).
Compute (div_in_list 5 L 3).

End Examples.