Module Qcert.Data.Operators.OperatorsUtils

Require Import List.
Require Import String.
Require Import Utils.
Require Import ZArith.
Require Import BrandRelation.
Require Import ForeignData.
Require Import Data.
Require Import DataLift.
Require Import Iterators.

Section OperatorsUtils.
  Context {fdata:foreign_data}.

  Definition string_sort := insertion_sort StringOrder.le_dec.

  Fixpoint dsum (ns:list data) : option Z
    := match ns with
         | nil => Some 0%Z
         | dnat n::ls => lift (Zplus n) (dsum ls)
         | _ => None
       end.

  Lemma dsum_nil :
    dsum nil = Some (0%Z).

  Lemma Zquot_zero n :
    Z.quot n 0%Z = 0%Z.
    
  Definition darithmean_alt (ns:list data) : option Z
    := match ns with
       | nil => Some (0%Z)
       | _ => lift (fun x => Z.quot x (Z_of_nat (List.length ns))) (dsum ns)
       end.

  Definition darithmean (ns:list data) : option Z
    := lift (fun x => Z.quot x (Z_of_nat (List.length ns))) (dsum ns).

  Lemma darithmean_alt_correct (ns:list data):
    darithmean_alt ns = darithmean ns.
           
  Definition lifted_stringbag (l : list data) : option (list string) :=
    lift_map (ondstring (fun x => x)) l.
  Definition lifted_zbag (l : list data) : option (list Z) :=
    lift_map (ondnat (fun x => x)) l.
  Definition lifted_min (l : list data) : option data :=
    lift dnat (lift bnummin (lifted_zbag l)).
  Definition lifted_max (l : list data) : option data :=
    lift dnat (lift bnummax (lifted_zbag l)).

  Definition lifted_fbag (l : list data) : option (list float) :=
    lift_map (ondfloat (fun x => x)) l.

  Definition lifted_fsum (l:list data) : option data :=
    lift dfloat (lift float_list_sum (lifted_fbag l)).
  Definition lifted_farithmean (l:list data) : option data :=
    lift dfloat (lift float_list_arithmean (lifted_fbag l)).
  Definition lifted_fmin (l : list data) : option data :=
    lift dfloat (lift float_list_min (lifted_fbag l)).
  Definition lifted_fmax (l : list data) : option data :=
    lift dfloat (lift float_list_max (lifted_fbag l)).

  Definition lifted_join (sep : string) (l : list data) : option data :=
    lift dstring (lift (concat sep) (lifted_stringbag l)).

End OperatorsUtils.