Module Qcert.Data.Operators.UnaryOperatorsSem

Require Import String.
Require Import List.
Require Import Compare_dec.
Require Import ZArith.
Require Import Utils.
Require Import BrandRelation.
Require Import ForeignData.
Require Import Data.
Require Import DataLift.
Require Import DataNorm.
Require Import ForeignOperators.
Require Import Iterators.
Require Import RecOperators.
Require Import OperatorsUtils.
Require Import SortBy.
Require Export UnaryOperators.

Section UnaryOperatorsSem.
  Context {fdata:foreign_data}.

  Definition nat_arith_unary_op_eval (op:nat_arith_unary_op) (z:Z) :=
    match op with
    | NatAbs => Z.abs z
    | NatLog2 => Z.log2 z
    | NatSqrt => Z.sqrt z
    end.

  Definition float_arith_unary_op_eval (op:float_arith_unary_op) (f:float) :=
    match op with
    | FloatNeg => float_neg f
    | FloatSqrt => float_sqrt f
    | FloatExp => float_exp f
    | FloatLog => float_log f
    | FloatLog10 => float_log10 f
    | FloatCeil => float_ceil f
    | FloatFloor => float_floor f
    | FloatAbs => float_absolute f
    end.

  Context (h:brand_relation_t).
  Context {foperators:foreign_operators}.

  Global Instance ToString_data : ToString data
    := { toString := foreign_operators_unary_data_tostring }.

  Fixpoint defaultDataToString (d:data) : string
    := match d with
       | dunit => "unit"%string
       | dnat n => toString n
       | dfloat n => toString n
       | dbool b => toString b
       | dstring s => stringToString s
       | dcoll l => string_bracket
                      "["%string
                      (String.concat ", "%string
                              (map defaultDataToString l))
                      "]"%string
       | drec lsd => string_bracket
                       "{"%string
                       (String.concat ", "%string
                               (map (fun xy => let '(x,y):=xy in
                                               (append (stringToString x) (append "->"%string
                                                                                  (defaultDataToString y)))
                                    ) lsd))
                       "}"%string
       | dleft d => string_bracket
                      "Left("%string
                      (defaultDataToString d)
                      ")"%string
       | dright d => string_bracket
                       "Right("%string
                       (defaultDataToString d)
                       ")"%string
       | dbrand b d => (string_bracket
                          "<"
                          (append (@toString _ ToString_brands b)
                                  (append ":" (defaultDataToString d)))
                          ">")
       | dforeign fd => toString fd
       end.

  Definition unary_op_eval (uop:unary_op) (d:data) : option data :=
    match uop with
    | OpIdentity => Some d
    | OpNeg => unudbool negb d
    | OpRec s => Some (drec ((s,d) :: nil))
    | OpDot s =>
      match d with
      | drec r => edot r s
      | _ => None
      end
    | OpRecRemove s =>
      match d with
      | drec r => Some (drec (rremove r s))
      | _ => None
      end
    | OpRecProject sl =>
      match d with
      | drec r => Some (drec (rproject r sl))
      | _ => None
      end
    | OpBag => Some (dcoll (d :: nil))
    | OpSingleton =>
      match d with
      | dcoll (d'::nil) => Some (dsome d')
      | dcoll _ => Some dnone
      | _ => None
      end
    | OpFlatten =>
      lift_oncoll (fun l => (lift dcoll (oflatten l))) d
    | OpDistinct =>
      rondcoll (@bdistinct data data_eq_dec) d
    | OpOrderBy sc =>
      data_sort (map get_criteria sc) d
    | OpCount =>
      lift dnat (ondcoll (fun z => Z_of_nat (bcount z)) d)
    | OpToString =>
      Some (dstring (foreign_operators_unary_data_tostring d))
    | OpToText =>
      Some (dstring (foreign_operators_unary_data_totext d))
    | OpLength =>
      unndstring (fun s => Z_of_nat (String.length s)) d
    | OpSubstring start olen =>
      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
    | OpLike pat =>
      match d with
      | dstring s => Some (dbool (string_like s pat None))
      | _ => None
      end
    | OpLeft => Some (dleft d)
    | OpRight => Some (dright d)
    | OpBrand b => Some (dbrand (canon_brands h b) d)
    | OpUnbrand =>
      match d with
      | dbrand _ d' => Some d'
      | _ => None
      end
    | OpCast b =>
      match d with
      | dbrand b' _ =>
        if (sub_brands_dec h b' b)
        then
          Some (dsome d)
        else
          Some (dnone)
      | _ => None
      end
    | OpNatUnary op =>
      match d with
      | dnat n => Some (dnat (nat_arith_unary_op_eval op n))
      | _ => None
      end
    | OpNatSum =>
      lift dnat (lift_oncoll dsum d)
    | OpNatMin =>
      match d with
      | dcoll l => lifted_min l
      | _ => None
      end
    | OpNatMax =>
      match d with
      | dcoll l => lifted_max l
      | _ => None
      end
    | OpNatMean =>
      lift dnat (lift_oncoll darithmean d)
    | OpFloatOfNat =>
      match d with
      | dnat n => Some (dfloat (float_of_int n))
      | _ => None
      end
    | OpFloatUnary op =>
      match d with
      | dfloat n => Some (dfloat (float_arith_unary_op_eval op n))
      | _ => None
      end
    | OpFloatTruncate =>
      match d with
      | dfloat f => Some (dnat (float_truncate f))
      | _ => None
      end
    | OpFloatSum =>
      lift_oncoll lifted_fsum d
    | OpFloatMean =>
      lift_oncoll lifted_farithmean d
    | OpFloatBagMin =>
      lift_oncoll lifted_fmin d
    | OpFloatBagMax =>
      lift_oncoll lifted_fmax d
    | OpForeignUnary fu => foreign_operators_unary_interp h fu d
    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).

  Local Hint Constructors data_normalized Forall : qcert.
  Local Hint Resolve dnnone dnsome : qcert.
  
  Lemma unary_op_eval_normalized {u d o} :
    unary_op_eval u d = Some o ->
    data_normalized h d ->
    data_normalized h o.

End UnaryOperatorsSem.