Module RUnaryOpsSem

Section RUnaryOpsSem.

  Require Import String List Compare_dec ZArith.
  
  Require Import Utils.
  Require Import RBag RData RDataNorm RDataSort RRelation.
  Require Import RUtilOps.
  Require Export RUnaryOps.
  Require Import BrandRelation.
  Require Import ForeignData.
  Require Import ForeignOps.

  Require Import ZArith.

  Context {fdata:foreign_data}.
  
  Definition lifted_zbag (l : list data) : option (list Z) :=
    rmap (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 fun_of_arithuop (op:ArithUOp) : Z -> Z
  := match op with
         | ArithAbs => Z.abs
         | ArithLog2 => Z.log2
         | ArithSqrt => Z.sqrt
     end.

  Context {fuop:foreign_unary_op}.

  Context (h:brand_relation_t).

  Definition fun_of_unaryop (uop:unaryOp) : data -> option data :=
    match uop with
    | AIdOp =>
      fun d => Some d
    | ANeg =>
      fun d => unudbool negb d
    | AColl =>
      fun d => Some (dcoll (d :: nil))
    | ASingleton =>
      fun d =>
        match d with
        | dcoll (d'::nil) => Some (dsome d')
        | dcoll _ => Some dnone
        | _ => None
        end
    | AFlatten =>
      fun d => lift_oncoll (fun l => (lift dcoll (rflatten l))) d
    | ADistinct =>
      fun d => rondcoll (@bdistinct data data_eq_dec) d
    | AOrderBy sc =>
      fun d => data_sort sc d
    | ARec s =>
      fun d => Some (drec ((s,d) :: nil))
    | ADot s =>
      fun d =>
        match d with
        | drec r => edot r s
        | _ => None
        end
    | ARecRemove s =>
      fun d =>
        match d with
        | drec r => Some (drec (rremove r s))
        | _ => None
        end
    | ARecProject sl =>
      fun d =>
        match d with
        | drec r => Some (drec (rproject r sl))
        | _ => None
        end
    | ACount =>
      fun d => lift dnat (ondcoll (fun z => Z_of_nat (bcount z)) d)
    | ASum =>
      fun d => lift dnat (lift_oncoll dsum d)
    | ANumMin =>
      fun d => match d with
               | dcoll l => lifted_min l
               | _ => None
               end
    | ANumMax =>
      fun d => match d with
               | dcoll l => lifted_max l
               | _ => None
               end
    | AArithMean =>
      fun d => lift dnat (lift_oncoll darithmean d)
    | AToString =>
      fun d => Some (dstring (dataToString d))
    | ASubstring start olen =>
      fun d =>
                (match d with
                 | dstring s =>
                   Some (dstring (
                   let real_start :=
                       (match start with
                        | 0%Z => 0
                     | Z.pos p => Pos.to_nat p
                     | Z.neg n => (String.length s) - (Pos.to_nat n)
                        end) in
                   let real_olen :=
                       match olen with
                       | Some len =>
                         match len with
                         | 0%Z => 0
                         | Z.pos p => Pos.to_nat p
                         | Z.neg n => 0
                         end
                       | None => (String.length s) - real_start
                       end in
                   (substring real_start real_olen s)))
                 | _ => None
                 end)
    | ALike pat oescape =>
      fun d =>
        match d with
        | dstring s => Some (dbool (string_like s pat oescape))
        | _ => None
        end
    | ALeft =>
      fun d => Some (dleft d)
    | ARight =>
      fun d => Some (dright d)
    | ABrand b =>
      fun d => Some (dbrand (canon_brands h b) d)
    | AUnbrand =>
      fun d => match d with
               | dbrand _ d' => Some d'
               | _ => None
               end
    | ACast b =>
      fun d =>
        match d with
        | dbrand b' _ =>
          if (sub_brands_dec h b' b)
          then
            Some (dsome d)
          else
            Some (dnone)
        | _ => None
        end
    | AUArith op =>
      fun d =>
        match d with
        | dnat n => Some (dnat (fun_of_arithuop op n))
        | _ => None
        end
    | AForeignUnaryOp fu => foreign_unary_op_interp h fu
    end.

  Lemma data_normalized_edot l s o :
    edot l s = Some o ->
    data_normalized h (drec l) ->
    data_normalized h o.

  Lemma data_normalized_filter l :
    data_normalized h (drec l) ->
    forall f, data_normalized h (drec (filter f l)).

  Lemma data_normalized_rremove l :
    data_normalized h (drec l) ->
    forall s, data_normalized h (drec (rremove l s)).

   Lemma data_normalized_rproject l :
    data_normalized h (drec l) ->
    forall l2, data_normalized h (drec (rproject l l2)).

  Lemma data_normalized_bdistinct l :
    data_normalized h (dcoll l) -> data_normalized h (dcoll (bdistinct l)).

  Lemma dnnone : data_normalized h dnone.

  Lemma dnsome d :
    data_normalized h d ->
    data_normalized h (dsome d).

  Lemma fun_of_unaryop_normalized {u d o} :
    fun_of_unaryop u d = Some o ->
    data_normalized h d ->
    data_normalized h o.

End RUnaryOpsSem.