Qcert.Basic.Operators.RUnaryOpsSem

Section RUnaryOpsSem.




  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) →
    ∀ f, data_normalized h (drec (filter f l)).

  Lemma data_normalized_rremove l :
    data_normalized h (drec l) →
    ∀ s, data_normalized h (drec (rremove l s)).

   Lemma data_normalized_rproject l :
    data_normalized h (drec l) →
    ∀ 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.