Module Qcert.EJson.Operators.EJsonGroupBy

Require Import List.
Require Import String.
Require Import Utils.
Require Import Bindings.
Require Import ForeignEJson.
Require Import EJson.

Section EJsonGroupBy.
  Context {foreign_ejson_model:Set}.
  Context {fejson:foreign_ejson foreign_ejson_model}.

  Import ListNotations.




  Definition ejson_key_is_eq_r (eval_key: @ejson foreign_ejson_model -> option ejson) (d1 d2:@ejson foreign_ejson_model) : option bool :=
    olift2 (fun x y => if ejson_eq_dec x y then Some true else Some false)
           (eval_key d1)
           (Some d2).

  Definition ejson_group_of_key (eval_key: ejson -> option ejson) (k:ejson) (l: list ejson) :=
    (lift_filter (fun d => ejson_key_is_eq_r eval_key d k) l).

  Definition ejson_group_by_nested_eval (eval_key: ejson -> option ejson) (l: list ejson) : option (list (ejson * (list ejson))) :=
    let dupkeys := lift_map (fun d => eval_key d) l in
    let keys := lift bdistinct dupkeys in
    olift (lift_map (fun k => olift (fun group => Some (k, group)) (ejson_group_of_key eval_key k l))) keys.

  Definition ejson_group_to_partitions (g:string) (group: @ejson foreign_ejson_model * list ejson) : option ejson :=
    match ejson_is_record (fst group) with
    | Some keys =>
      Some (ejobject (rec_concat_sort keys [(g, ejarray (snd group))]))
    | _ => None
    end.

  Definition ejson_to_partitions (g:string) (l: list (ejson * list ejson)) :=
    lift_map (ejson_group_to_partitions g) l.

  Definition ejson_group_by_nested_eval_keys_partition
             (g:string) (eval_keys:ejson -> option ejson) (l: list ejson) : option (list ejson) :=
    olift (ejson_to_partitions g) (ejson_group_by_nested_eval eval_keys l).

  Section tableform.
    Definition ejson_group_by_nested_eval_table
               (g:string) (sl:list string) (l:list ejson) : option (list ejson) :=
      ejson_group_by_nested_eval_keys_partition
        g
        (fun j =>
           match ejson_is_record j with
           | Some r => Some (ejobject (rproject r sl))
           | _ => None
           end) l.

  End tableform.

End EJsonGroupBy.