(* -*- coq-prog-args: ("-emacs-U" "-R" "." "FingerTree" "-R" "../safe" "Safe") -*- *)
Require Import FingerTree.Reduce.
Require Import Safe.List.
Set Implicit Arguments.

Section Nodes.
  Variable A : Type.

  Inductive node : Type :=
  | Node2 : A -> A -> node
  | Node3 : A -> A -> A -> node.    
End Nodes.

Section NodesReduce.
  Variables X Y : Type.
  Variable reducer : X -> Y -> Y.
  Variable reducel : Y -> X -> Y.
  Notation " x < y " := (reducer x y).
  Notation " x > y " := (reducel x y).

  Definition node_reducer n w :=
      match n with
        | Node2 x y => x < (y < w)
        | Node3 x y z => x < (y < (z < w))
      end.
      

  Definition node_reducel w n :=
      match n with
        | Node2 x y => (w > y) > x
        | Node3 x y z => ((w > z) > y) > x
      end.
End NodesReduce.

Definition nodeReduce := mkReduce node_reducer node_reducel.

Section Tree.

  Inductive tree : Type -> Type :=
  | Zero : forall A : Type, A -> tree A
  | Succ : forall A : Type, tree (node A) -> tree A.

  Definition digit (A : Type) : Type := list A.
    

  Inductive fingertree (A : Type) : Type :=
  | Empty : fingertree A
  | Single : A -> fingertree A
  | Deep : { d : digit A | d <> nil } -> fingertree (node A) -> { d : digit A | d <> nil } -> fingertree A.
  
  Notation empty := (Empty _).

  Section TreeReduce.
    
    Program Fixpoint tree_reducer (X Y : Type) (redr : X -> Y -> Y) (n : fingertree X) (w : Y) {struct n} : Y :=
      match n with
        | Empty => w
        | Single x => redr x w
        | Deep pr m sf => 
          let rd := reducer listReduce redr in
          let rt := tree_reducer (reducer nodeReduce redr) in
            rd pr (rt m (rd sf w))
      end.

    Program Fixpoint tree_reducel (X Y : Type) (redl : Y -> X -> Y) (w : Y) (n : fingertree X) {struct n} : Y :=
      match n with
        | Empty => w
        | Single x => redl w x
        | Deep pr m sf => 
          let rd := reducel listReduce redl in
          let rt := tree_reducel (reducel nodeReduce redl) in
            rd (rt (rd w pr) m) sf
      end.
  
    Definition treeReduce := mkReduce tree_reducer tree_reducel.

  End TreeReduce.
      
  Section add.

(*     Program Fixpoint add_left A (a : A) (t : fingertree A) {struct t} : fingertree A := *)
(*       match t with *)
(*         | Empty => Single a *)
(*         | Single b => Deep [a] empty [b] *)
(*         | Deep (exist ([b ; c ; d ; e] as x) _)  m sf => Deep [ a ; b ] (add_left (Node3 c d e) m) sf *)
(*         | Deep pr m sf => Deep (a :: pr) m sf *)
(*       end. *)

    Program Fixpoint add_left A (a : A) (t : fingertree A) {struct t} : fingertree A :=
      match t with
        | Empty => Single a
        | Single b => Deep [a] empty [b]
        | Deep pr m sf => 
          match pr with
            | [b ; c ; d ; e] => Deep [ a ; b ] (add_left (Node3 c d e) m) sf
            | _ => Deep (a :: pr) m sf
          end
      end.

    Solve Obligations using red ; intros ; discriminate.

    Program Fixpoint add_right A (t : fingertree A) (a : A) {struct t} : fingertree A :=
      match t with
        | Empty => Single a
        | Single b => Deep [b] empty [a]
        | Deep pr m sf =>
          match sf with
            | [ b ; c ; d ; e ] => Deep pr (add_right m (Node3 b c d)) [ e ; a ]
            | _ => Deep pr m (sf ++ [a])
          end
      end.

    Next Obligation.
      red ; intros ; discriminate.
    Defined.
    
    Solve Obligations using red ; intros ; discriminate.
    Next Obligation.
    Proof.
      intros.
      red ; destruct x ; simpl ; intros ; discriminate.
    Defined.

    Section add_reduce.
      Variable f : Type -> Type.
      Variable red : Reduce f.
      Variable A : Type.

      Definition add_left_red := reducer red (@add_left A).
      Definition add_right_red := reducel red (@add_right A).

      Definition toTree s := add_left_red s empty.

    End add_reduce.

  End add.

  Section view_L.
    Inductive View_L (s : Type -> Type) (a : Type) : Type := 
    | nil_L : View_L s a
    | cons_L : a -> s a -> View_L s a.

    Program Fixpoint view_L (A : Type) (t : fingertree A) { struct t } : View_L fingertree A := 
      match t with
        | Empty => @nil_L _ _
        | Single x => cons_L _ x empty
        | Deep pr m sf => 
          let deep_L (l : list A) : fingertree A :=
            match l with
              | nil => match view_L m with
                        | nil_L => toTree listReduce _ sf
                        | cons_L a m' => Deep (toList nodeReduce _ a) m' sf
                      end
              | _ :: _ => Deep l m sf
            end
          in
            cons_L _ (head pr) (deep_L (tail pr))
      end.
    
    Next Obligation.
    Proof.
      intros.
      unfold reducer ; simpl ; red ; intros ; destruct a ; discriminate.      
    Defined.

    Next Obligation of view_L.
    Proof.
      intros.
      destruct x ; simpl in * ; auto with datatypes ; discriminate.
    Defined.

    Next Obligation of view_L.
    Proof.
      intros.
      destruct x0 ; simpl ; simpl in * ; auto with datatypes ; discriminate.
    Defined.
    
    Next Obligation.
    Proof.
      destruct x0 ; simpl ; simpl in * ; auto with datatypes ; discriminate.
    Defined.

  End view_L.

  Section view_R.

    Inductive View_R (s : Type -> Type) (a : Type) : Type := 
    | nil_R : View_R s a
    | cons_R : s a -> a -> View_R s a.

    Program Fixpoint view_R (A : Type) (t : fingertree A) { struct t } : View_R fingertree A := 
      match t with
        | Empty => @nil_R _ _
        | Single x => cons_R _ empty x
        | Deep pr m sf => 
          let deep_R (sf : digit A) : fingertree A :=
            match sf with
              | nil => match view_R m with
                        | nil_R => toTree listReduce _ pr
                        | cons_R m' a => Deep pr m' (toList nodeReduce _ a)
                      end
              | _ :: _ => Deep pr m sf
            end
          in
            cons_R _ (deep_R (liat sf)) (last sf)
      end.
    
    Next Obligation.
    Proof.
      intros.
      unfold reducer ; simpl ; red ; intros ; destruct a ; discriminate.      
    Defined.

    Next Obligation.
    Proof.
      intros.
      destruct x ; simpl in * ; auto with datatypes ; discriminate.
    Defined.

    Next Obligation.
    Proof.
      intros.
      destruct x ; simpl ; simpl in * ; auto with datatypes ; discriminate.
    Defined.
    
    Next Obligation.
    Proof.
      destruct x ; simpl ; simpl in * ; auto with datatypes ; discriminate.
    Defined.

  End view_R.

  Section View.
    Variable A : Type.

    Definition isEmpty t := match @view_L A t with
                              | nil_L => true
                              | cons_L _ _ => false
                            end.
    Require Import Coq.subtac.Utils.
  
    Program Definition head (t : fingertree A | isEmpty t = false) : A := 
      match @view_L A t with
        | cons_L hd _ => hd
        | nil_L => !
      end.

    Next Obligation.
    Proof.
      intros.
      destruct x ; unfold isEmpty in * ;  simpl in * ; try discriminate.
    Qed.
    
    Program Definition tail (t : fingertree A | isEmpty t = false) : fingertree A := 
      match @view_L A t with
        | cons_L _ tl => tl
        | nil_L => !
      end.

    Next Obligation.
    Proof.
      intros.
      destruct x ; unfold isEmpty in * ;  simpl in * ; try discriminate.
    Qed.

    Program Definition last (t : fingertree A | isEmpty t = false) : A :=
      match @view_R A t with
        | cons_R _ x => x
        | nil_R => !
      end.

    Next Obligation.
    Proof.
      intros.
      destruct x ; unfold isEmpty in * ;  simpl in * ; try discriminate.
    Qed.
    
    Program Definition liat (t : fingertree A | isEmpty t = false) : fingertree A := 
      match @view_R A t with
        | cons_R prev last => prev
        | nil_R => !
      end.

    Next Obligation.
    Proof.
      intros.
      destruct x ; unfold isEmpty in * ;  simpl in * ; try discriminate.
    Qed.

  End View.


  
End Tree.