Module RBinaryOpsSem

Section RBinaryOpsSem.

  Require Import String List Compare_dec.
  Require Import ZArith.

  Require Import Utils.
  Require Import RBag RData RDataNorm RRelation.
  Require Import RUtilOps.
  Require Export RBinaryOps.
  Require Import BrandRelation.
  Require Import RCompat.
  Require Import ForeignData.
  Require Import ForeignOps.
  

  Definition fun_of_arithbop (op:ArithBOp) : Z -> Z -> Z
    := match op with
       | ArithPlus => Z.add
       | ArithMinus=> Z.sub
       | ArithMult => Z.mul
       | ArithMin => Z.min
       | ArithMax => Z.max
       | ArithDivide=> Z.quot
       | ArithRem => Z.rem
       end.

  Context {fdata:foreign_data}.
  Context {fbop:foreign_binary_op}.
  Context (h:brand_relation_t).

  Definition fun_of_binop (bop:binOp) : data -> data -> option data :=
    match bop with
    | ABArith op =>
      fun d1 d2 =>
        match d1, d2 with
        | dnat n1, dnat n2 => Some (dnat (fun_of_arithbop op n1 n2))
        | _, _ => None
        end
    | AAnd => fun d1 d2 => unbdbool andb d1 d2
    | AOr => fun d1 d2 => unbdbool orb d1 d2
    | AEq => fun d1 d2 => unbdata (fun x y => if data_eq_dec x y then true else false) d1 d2
    | ALt => fun d1 d2 => unbdnat (fun x y => if Z_lt_dec x y then true else false) d1 d2
    | ALe => fun d1 d2 => unbdnat (fun x y => if Z_le_dec x y then true else false) d1 d2
    | AUnion => fun d1 d2 => rondcoll2 bunion d1 d2
    | AMinus => fun d1 d2 => rondcoll2 (@bminus data data_eq_dec) d1 d2
    | AMin => fun d1 d2 => rondcoll2 (@bmin data data_eq_dec) d1 d2
    | AMax => fun d1 d2 => rondcoll2 (@bmax data data_eq_dec) d1 d2
    | AContains => fun d1 d2 => ondcoll (fun l =>
                                           if in_dec data_eq_dec d1 l
                                           then dbool true else dbool false) d2
    | ASConcat => fun d1 d2 => unsdstring append d1 d2
    | AConcat =>
      fun d1 d2 =>
        match d1, d2 with
        | (drec r1), (drec r2) => Some (drec (rec_sort (r1++r2)))
        | _, _ => None
        end
    | AMergeConcat =>
      fun d1 d2 =>
        match d1, d2 with
        | (drec r1), (drec r2) =>
          match merge_bindings r1 r2 with
          | Some x => Some (dcoll ((drec x) :: nil))
          | None => Some (dcoll nil)
          end
        | _, _ => None
        end
    | AForeignBinaryOp fb => foreign_binary_op_interp h fb
    end.

  Lemma fun_of_binop_normalized {b d1 d2 o} :
    fun_of_binop b d1 d2 = Some o ->
    data_normalized h d1 -> data_normalized h d2 ->
    data_normalized h o.
  
End RBinaryOpsSem.