Qcert.Basic.Operators.RBinaryOpsSem

Section RBinaryOpsSem.




  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.