Module RGroupBy

Section RGroupBy.
  Require Import List.

  Require Import Utils.
  Require Import RBag.
  Require Import RDomain.
  Require Import RData.
  Require Import ForeignData.
  Require Import RRelation.

  Context {fdata:foreign_data}.

  Fixpoint add_in_groups (key: data) (d: data) (l: list (data * (list data))) : list (data * (list data)) :=
    match l with
    | nil => (key, (d :: nil)) :: nil
    | (key', group) :: l' =>
      if data_eq_dec key key'
      then
        (key', d::group) :: l'
      else
        let l'' := add_in_groups key d l' in
        (key', group) :: l''
    end.


  Definition group_by_iter_eval (get_key: data -> option data) (l: list data) : option (list (data * (list data))) :=
    fold_right
      (fun d acc =>
         match acc with
         | Some acc' => lift (fun k => add_in_groups k d acc') (get_key d)
         | None => None
         end)
      (Some nil) l.

  Definition group_by_iter_eval_alt (l: list (data * data)) : list (data * (list data)) :=
    fold_right
      (fun (d:data*data) acc => add_in_groups (fst d) (snd d) acc)
      nil l.




  Definition key_is_eq (eval_key: data -> option data) (d1 d2:data) : option bool :=
    olift2 (fun x y => if data_eq_dec x y then Some true else Some false)
           (eval_key d1)
           (eval_key d2).

  Definition key_is_eq_r (eval_key: data -> option data) (d1 d2:data) : option bool :=
    olift2 (fun x y => if data_eq_dec x y then Some true else Some false)
           (eval_key d1)
           (Some d2).

  Lemma key_is_eq_with_project_eq sl d l :
    key_is_eq_r
      (fun d0 : data =>
         match d0 with
         | dunit => None
         | dnat _ => None
         | dbool _ => None
         | dstring _ => None
         | dcoll _ => None
         | drec r => Some (drec (rproject r sl))
         | dleft _ => None
         | dright _ => None
         | dbrand _ _ => None
         | dforeign _ => None
         end) (drec l) d =
    Some (if data_eq_dec (drec (rproject l sl)) d then true else false).

  Require Import String.
  
  Definition group_of_key (eval_key: data -> option data) (k:data) (l: list data) :=
    (lift_filter (fun d => key_is_eq_r eval_key d k) l).

  Definition group_by_nested_eval (eval_key: data -> option data) (l: list data) : option (list (data * (list data))) :=
    let dupkeys := rmap (fun d => eval_key d) l in
    let keys := lift bdistinct dupkeys in
    olift (rmap (fun k => olift (fun group => Some (k, group)) (group_of_key eval_key k l))) keys.

  Definition to_kv (l: list (data * list data)) :=
    map (fun x => drec (("key"%string,(fst x))::("value"%string,dcoll (snd x)) :: nil)) l.
  
  Definition group_by_nested_eval_kv (eval_key:data -> option data) (l: list data) : option (list data) :=
    lift to_kv (group_by_nested_eval eval_key l).


  Definition group_to_partitions (g:string) (group: data * list data) : option data :=
    match (fst group) with
    | drec keys =>
      Some (drec (rec_sort ((g,(dcoll (snd group)))::keys)))
    | _ => None
    end.

  Definition to_partitions (g:string) (l: list (data * list data)) :=
    lift_map (group_to_partitions g) l.
  
  Definition group_by_nested_eval_keys_partition
             (g:string) (eval_keys:data -> option data) (l: list data) : option (list data) :=
    olift (to_partitions g) (group_by_nested_eval eval_keys l).

  Section tableform.
    Definition group_by_nested_eval_table
               (g:string) (sl:list string) (l:list data) : option (list data) :=
      group_by_nested_eval_keys_partition
        g
        (fun d =>
           match d with
           | drec r => Some (drec (rproject r sl))
           | _ => None
           end) l.

    Lemma group_of_key_over_table_correct sl d incoll :
      olift (fun group : list data => Some (dcoll group))
            (group_of_key
               (fun d : data =>
                  match d with
                  | dunit => None
                  | dnat _ => None
                  | dbool _ => None
                  | dstring _ => None
                  | dcoll _ => None
                  | drec r => Some (drec (rproject r sl))
                  | dleft _ => None
                  | dright _ => None
                  | dbrand _ _ => None
                  | dforeign _ => None
                  end) d incoll)
      =
(olift
              (fun d1 : data =>
               lift_oncoll
                 (fun l2 : list data => lift dcoll (rflatten l2)) d1)
              (lift dcoll
                 (rmap
                    (fun d1 : data =>
                     olift
                       (fun d0 : data =>
                        match d0 with
                        | dunit => None
                        | dnat _ => None
                        | dbool true => Some (dcoll (d1 :: nil))
                        | dbool false => Some (dcoll nil)
                        | dstring _ => None
                        | dcoll _ => None
                        | drec _ => None
                        | dleft _ => None
                        | dright _ => None
                        | dbrand _ _ => None
                        | dforeign _ => None
                        end)
                       (olift2
                          (fun d0 d2 : data =>
                           unbdata
                             (fun x y : data =>
                              if data_eq_dec x y then true else false) d0
                             d2)
                          match d1 with
                          | dunit => None
                          | dnat _ => None
                          | dbool _ => None
                          | dstring _ => None
                          | dcoll _ => None
                          | drec r => Some (drec (rproject r sl))
                          | dleft _ => None
                          | dright _ => None
                          | dbrand _ _ => None
                          | dforeign _ => None
                          end (Some d))) incoll))).

    Lemma group_of_key_destruct_drec_inv g sl d l0 l1 incoll:
      match d with
      | dunit => None
      | dnat _ => None
      | dbool _ => None
      | dstring _ => None
      | dcoll _ => None
      | drec r2 =>
        Some
          (drec
             (insertion_sort_insert rec_field_lt_dec
                                    (g, dcoll l1) (rec_sort r2)))
      | dleft _ => None
      | dright _ => None
      | dbrand _ _ => None
      | dforeign _ => None
      end = None ->
      olift (to_partitions g)
            (lift (fun t' : list (data * list data) => (d, l1) :: t')
                  (rmap
                     (fun k : data =>
                        olift (fun group : list data => Some (k, group))
                              (group_of_key
                                 (fun d : data =>
                                    match d with
                                    | dunit => None
                                    | dnat _ => None
                      | dbool _ => None
                      | dstring _ => None
                      | dcoll _ => None
                      | drec r => Some (drec (rproject r sl))
                      | dleft _ => None
                      | dright _ => None
                      | dbrand _ _ => None
                      | dforeign _ => None
                                    end) k incoll)) l0)) = None.

    Lemma test l0 g sl l1 l2 incoll :
      olift (to_partitions g)
            (lift (fun t' : list (data * list data) => (drec l2, l1) :: t')
                  (rmap
                     (fun k : data =>
                        olift (fun group : list data => Some (k, group))
                              (group_of_key
                                 (fun d : data =>
                                    match d with
                                    | dunit => None
                                    | dnat _ => None
                                    | dbool _ => None
                                    | dstring _ => None
                                    | dcoll _ => None
                                    | drec r => Some (drec (rproject r sl))
                                    | dleft _ => None
                                    | dright _ => None
                                    | dbrand _ _ => None
                                    | dforeign _ => None
                                    end) k incoll)) l0))
      =
      lift
        (fun t' : list data =>
           drec
             (insertion_sort_insert rec_field_lt_dec
                                    (g, dcoll l1) (rec_sort l2)) :: t')
        (rmap
           (fun d1 : data =>
              olift2
                (fun d0 d2 : data =>
                   match d0 with
                   | dunit => None
                   | dnat _ => None
                   | dbool _ => None
                   | dstring _ => None
                   | dcoll _ => None
                   | drec r1 =>
                     match d2 with
                     | dunit => None
                     | dnat _ => None
                     | dbool _ => None
                     | dstring _ => None
                     | dcoll _ => None
                     | drec r2 => Some (drec (rec_sort (r1 ++ r2)))
                     | dleft _ => None
                     | dright _ => None
                     | dbrand _ _ => None
                     | dforeign _ => None
                     end
                   | dleft _ => None
                   | dright _ => None
                   | dbrand _ _ => None
                   | dforeign _ => None
                   end)
                (olift (fun d0 : data => Some (drec ((g, d0) :: nil)))
                       (olift
                          (fun d0 : data =>
                             lift_oncoll
                               (fun l3 : list data => lift dcoll (rflatten l3)) d0)
                          (lift dcoll
                                (rmap
                                   (fun d0 : data =>
                                      olift
                                        (fun d2 : data =>
                                           match d2 with
                                           | dunit => None
                                           | dnat _ => None
                                           | dbool true => Some (dcoll (d0 :: nil))
                                           | dbool false => Some (dcoll nil)
                                           | dstring _ => None
                                           | dcoll _ => None
                                           | drec _ => None
                                           | dleft _ => None
                                           | dright _ => None
                                           | dbrand _ _ => None
                                           | dforeign _ => None
                                           end)
                                        (olift2
                                           (fun d2 d3 : data =>
                                              unbdata
                                                (fun x y : data =>
                                                   if data_eq_dec x y then true else false)
                                                d2 d3)
                                           match d0 with
                                           | dunit => None
                                           | dnat _ => None
                                           | dbool _ => None
                                           | dstring _ => None
                                           | dcoll _ => None
                                           | drec r => Some (drec (rproject r sl))
                                           | dleft _ => None
                                           | dright _ => None
                                           | dbrand _ _ => None
                                           | dforeign _ => None
                                           end (Some d1))) incoll))))
                (Some d1)) l0).

    Lemma group_by_table_correct
          (g:string) (sl:list string)
          (incoll outcoll:list data):
      group_by_nested_eval_table g sl incoll = Some outcoll ->
      match
        olift (fun d1 : data => rondcoll bdistinct d1)
              (lift dcoll
                    (rmap
                       (fun d1 : data =>
                          match d1 with
                          | dunit => None
                          | dnat _ => None
                          | dbool _ => None
                          | dstring _ => None
                          | dcoll _ => None
                          | drec r => Some (drec (rproject r sl))
                          | dleft _ => None
                          | dright _ => None
                          | dbrand _ _ => None
                          | dforeign _ => None
                          end) incoll))
      with
      | Some dunit => None
      | Some (dnat _) => None
      | Some (dbool _) => None
      | Some (dstring _) => None
      | Some (dcoll c1) =>
        lift dcoll
             (rmap
                (fun d1 : data =>
                   olift2
                     (fun d0 d2 : data =>
                        match d0 with
                        | dunit => None
                        | dnat _ => None
                        | dbool _ => None
                        | dstring _ => None
                        | dcoll _ => None
                        | drec r1 =>
                          match d2 with
                          | dunit => None
                          | dnat _ => None
                          | dbool _ => None
                          | dstring _ => None
                          | dcoll _ => None
                          | drec r2 => Some (drec (rec_sort (r1 ++ r2)))
                          | dleft _ => None
                          | dright _ => None
                          | dbrand _ _ => None
                          | dforeign _ => None
                          end
                        | dleft _ => None
                        | dright _ => None
                        | dbrand _ _ => None
                        | dforeign _ => None
                        end)
                     (olift (fun d0 : data => Some (drec ((g, d0) :: nil)))
                            (olift
                               (fun d0 : data =>
                                  lift_oncoll
                                    (fun l : list data => lift dcoll (rflatten l)) d0)
                               (lift dcoll
                                     (rmap
                                        (fun d0 : data =>
                                           olift
                                             (fun d2 : data =>
                                                match d2 with
                                                | dunit => None
                                                | dnat _ => None
                                                | dbool true => Some (dcoll (d0 :: nil))
                                                | dbool false => Some (dcoll nil)
                                                | dstring _ => None
                                                | dcoll _ => None
                                                | drec _ => None
                                                | dleft _ => None
                                                | dright _ => None
                                                | dbrand _ _ => None
                                                | dforeign _ => None
                                                end)
                                             (olift2
                                                (fun d2 d3 : data =>
                                                   unbdata
                                                     (fun x y : data =>
                                                        if data_eq_dec x y
                                                        then true
                                                        else false) d2 d3)
                                                match d0 with
                                                | dunit => None
                                                | dnat _ => None
                                                | dbool _ => None
                                                | dstring _ => None
                                                | dcoll _ => None
                                                | drec r => Some (drec (rproject r sl))
                                                | dleft _ => None
                                                | dright _ => None
                                                | dbrand _ _ => None
                                                | dforeign _ => None
                                                end (Some d1))) incoll))))
                     (Some d1)) c1)
      | Some (drec _) => None
      | Some (dleft _) => None
      | Some (dright _) => None
      | Some (dbrand _ _) => None
      | Some (dforeign _) => None
      | None => None
      end = Some (dcoll outcoll).
    
  End tableform.
  
  Section normalized.
    Require Import BrandRelation.
    Require Import RDataNorm.
    Context (h:brand_relation_t).

    Lemma bdistinct_normalized l :
      Forall (data_normalized h) l ->
      Forall (data_normalized h) (bdistinct l).

    Lemma rmap_rproject_normalized l l0 o :
      Forall (data_normalized h) l0 ->
      (rmap
         (fun d : data =>
            match d with
            | dunit => None
            | dnat _ => None
            | dbool _ => None
            | dstring _ => None
            | dcoll _ => None
            | drec r => Some (drec (rproject r l))
            | dleft _ => None
            | dright _ => None
            | dbrand _ _ => None
            | dforeign _ => None
            end) l0) = Some o ->
      Forall (data_normalized h) o.

    Lemma group_of_key_normalized a l l1 l2 :
      Forall (data_normalized h) l1 ->
      group_of_key
           (fun d : data =>
            match d with
            | dunit => None
            | dnat _ => None
            | dbool _ => None
            | dstring _ => None
            | dcoll _ => None
            | drec r => Some (drec (rproject r l))
            | dleft _ => None
            | dright _ => None
            | dbrand _ _ => None
            | dforeign _ => None
            end) a l1 = Some l2 ->
      Forall (data_normalized h) l2.

    Lemma group_by_nested_eval_normalized l0 l o :
      Forall (data_normalized h) l0 ->
      (group_by_nested_eval
         (fun d : data =>
            match d with
            | dunit => None
            | dnat _ => None
            | dbool _ => None
            | dstring _ => None
            | dcoll _ => None
            | drec r => Some (drec (rproject r l))
            | dleft _ => None
            | dright _ => None
            | dbrand _ _ => None
            | dforeign _ => None
            end) l0) = Some o ->
      Forall (fun dd => data_normalized h (fst dd)
                        /\ Forall (data_normalized h) (snd dd)) o.
    
    Lemma group_to_partitions_normalized s a d :
      data_normalized h (fst a) ->
      Forall (data_normalized h) (snd a) ->
      group_to_partitions s a = Some d ->
      data_normalized h d.

    Lemma group_by_nested_eval_keys_partition_normalized l0 s l o :
      data_normalized h (dcoll l0) ->
      lift dcoll
           (group_by_nested_eval_keys_partition
              s
              (fun d : data =>
                 match d with
                 | dunit => None
                 | dnat _ => None
                 | dbool _ => None
                 | dstring _ => None
                 | dcoll _ => None
                 | drec r => Some (drec (rproject r l))
                 | dleft _ => None
                 | dright _ => None
                 | dbrand _ _ => None
                 | dforeign _ => None
                 end) l0) = Some o
      -> data_normalized h o.

  End normalized.

End RGroupBy.