Module Qcert.Data.Operators.BinaryOperators

Require Import EquivDec.
Require Import String.
Require Import Utils.
Require Import ForeignData.
Require Import ForeignOperators.

Section BinaryOperators.
  Context {fdata:foreign_data}.
  Context {foperators:foreign_operators}.

  Inductive nat_arith_binary_op
    := NatPlus (* addition *)
     | NatMinus (* substraction *)
     | NatMult (* multiplication *)
     | NatDiv (* division *)
     | NatRem (* remainder *)
     | NatMin (* smallest *)
     | NatMax. (* biggest *)
  
  Inductive float_arith_binary_op
    :=
    | FloatPlus (* addition *)
    | FloatMinus (* substraction *)
    | FloatMult (* multiplication *)
    | FloatDiv (* division *)
    | FloatPow (* exponent *)
    | FloatMin (* min *)
    | FloatMax (* max *)
  .

  Inductive float_compare_binary_op
    :=
    | FloatLt (* less than *)
    | FloatLe (* less than or equal to *)
    | FloatGt (* greater than *)
    | FloatGe (* greater than or equal to *)
  .

  Inductive binary_op : Set :=
  | OpEqual : binary_op (* equality *)
  | OpRecConcat : binary_op (* record concatenation *)
  | OpRecMerge : binary_op (* record merge-concatenation *)
  | OpAnd : binary_op (* boolean conjunction *)
  | OpOr : binary_op (* boolean disjunction *)
  | OpLt : binary_op (* less than *)
  | OpLe : binary_op (* less than or equal to *)
  | OpBagUnion : binary_op (* bag union *)
  | OpBagDiff : binary_op (* bag difference *)
  | OpBagMin : binary_op (* bag min *)
  | OpBagMax : binary_op (* bag max *)
  | OpBagNth : binary_op (* random element in a bag *)
  | OpContains : binary_op (* is an element in a collection *)
  | OpStringConcat : binary_op (* string concatenation *)
  | OpStringJoin : binary_op (* string join *)
  | OpNatBinary : nat_arith_binary_op -> binary_op (* arithmetic operators on integers *)
  | OpFloatBinary : float_arith_binary_op -> binary_op (* arithmetic operators on floats *)
  | OpFloatCompare : float_compare_binary_op -> binary_op (* comparison operators on floats *)
  | OpForeignBinary
      (fb : foreign_operators_binary) : binary_op (* foreign binary operators *)
  .

  Global Instance nat_arith_binary_op_eqdec : EqDec nat_arith_binary_op eq.

  Global Instance float_arith_binary_op_eqdec : EqDec float_arith_binary_op eq.

  Global Instance float_compare_binary_op_eqdec : EqDec float_compare_binary_op eq.

  Global Instance binary_op_eqdec : EqDec binary_op eq.

  Local Open Scope string.

  Global Instance ToString_nat_binary_op : ToString nat_arith_binary_op
    := {toString :=
          fun (op:nat_arith_binary_op) =>
            match op with
            | NatPlus => "NatPlus"
            | NatMinus => "NatMinus"
            | NatMult => "NatMult"
            | NatMin => "NatMin"
            | NatMax => "NatMax"
            | NatDiv => "NatDiv"
            | NatRem => "NatRem"
            end
       }.

  Global Instance ToString_float_arith_binary_op : ToString float_arith_binary_op
    := {toString :=
          fun (op:float_arith_binary_op) =>
            match op with
            | FloatPlus => "FloatPlus"
            | FloatMinus => "FloatMinus"
            | FloatMult => "FloatMult"
            | FloatDiv => "FloatDiv"
            | FloatPow => "FloatPow"
            | FloatMin => "FloatMin"
            | FloatMax => "FloatMax"
            end
       }.

  Global Instance ToString_float_compare_binary_op : ToString float_compare_binary_op
    := {toString :=
          fun (op:float_compare_binary_op) =>
            match op with
            | FloatLt => "FloatLt"
            | FloatLe => "FloatLe"
            | FloatGt => "FloatGt"
            | FloatGe => "FloatGe"
            end
       }.

  Global Instance ToString_binary_op : ToString binary_op
    := {toString :=
          fun (op:binary_op) =>
            match op with
            | OpEqual => "OpEqual"
            | OpRecConcat => "OpRecConcat"
            | OpRecMerge => "OpRecMerge"
            | OpAnd => "OpAnd"
            | OpOr => "OpOr"
            | OpLt => "OpLt"
            | OpLe => "OpLe"
            | OpBagUnion => "OpBagUnion"
            | OpBagDiff => "OpBagDiff"
            | OpBagMin => "OpBagMin"
            | OpBagMax => "OpBagMax"
            | OpBagNth => "OpBagNth"
            | OpContains => "OpContains"
            | OpStringConcat => "OpStringConcat"
            | OpStringJoin => "OpStringJoin"
            | OpNatBinary aop => "(OpNatBinary " ++ (toString aop) ++ ")"
            | OpFloatBinary aop => "(OpFloatBinary " ++ (toString aop) ++ ")"
            | OpFloatCompare aop => "(OpFloatCompare " ++ (toString aop) ++ ")"
            | OpForeignBinary fb => toString fb
            end
       }.

End BinaryOperators.

Tactic Notation "binary_op_cases" tactic(first) ident(c) :=
  first;
  [ Case_aux c "OpEqual"%string
  | Case_aux c "OpRecConcat"%string
  | Case_aux c "OpRecMerge"%string
  | Case_aux c "OpAnd"%string
  | Case_aux c "OpOr"%string
  | Case_aux c "OpLt"%string
  | Case_aux c "OpLe"%string
  | Case_aux c "OpBagUnion"%string
  | Case_aux c "OpBagDiff"%string
  | Case_aux c "OpBagMin"%string
  | Case_aux c "OpBagMax"%string
  | Case_aux c "OpBagNth"%string
  | Case_aux c "OpContains"%string
  | Case_aux c "OpStringConcat"%string
  | Case_aux c "OpStringJoin"%string
  | Case_aux c "OpNatBinary"%string
  | Case_aux c "OpFloatBinary"%string
  | Case_aux c "OpFloatCompare"%string
  | Case_aux c "OpForeignBinary"%string].