Module RBinaryOps

Section RBinaryOps.

  Require Import EquivDec.
  Require Import String.

  Require Import Utils.
  Require Import ForeignData.
  Require Import ForeignOps.

  Context {fdata:foreign_data}.
  Context {fbop:foreign_binary_op}.

  Inductive ArithBOp
    := ArithPlus
     | ArithMinus
     | ArithMult
     | ArithMin
     | ArithMax
     | ArithDivide
     | ArithRem.
  
  Inductive binOp : Set :=
  | AEq: binOp
  | AConcat : binOp
  | AMergeConcat : binOp
  | AAnd : binOp
  | AOr : binOp
  | ABArith : ArithBOp -> binOp
  | ALt : binOp
  | ALe : binOp
  | AUnion: binOp
  | AMinus: binOp
  | AMin: binOp
  | AMax: binOp
  | AContains : binOp
  | ASConcat : binOp
  | AForeignBinaryOp (fb : foreign_binary_op_type) : binOp
  .

Global Instance ArithBOp_eqdec : EqDec ArithBOp eq.

Global Instance binOp_eqdec : EqDec binOp eq.

Local Open Scope string.

Global Instance ToString_ArithBOp : ToString ArithBOp
  := {toString :=
        fun (op:ArithBOp) =>
          match op with
            | ArithPlus => "ArithPlus"
            | ArithMinus => "ArithMinus"
            | ArithMult => "ArithMult"
            | ArithMin => "ArithMin"
            | ArithMax => "ArithMax"
            | ArithDivide => "ArithDivide"
            | ArithRem => "ArithRem"
          end
     }.

Global Instance ToString_binOp : ToString binOp
  := {toString :=
        fun (op:binOp) =>
          match op with
            | AEq => "AEq"
            | AUnion => "AUnion"
            | AConcat => "AConcat"
            | AMergeConcat => "AMergeConcat"
            | AAnd => "AAnd"
            | AOr => "AOr"
            | ABArith aop => "(ABArith " ++ (toString aop) ++ ")"
            | ALt => "ALt"
            | ALe => "ALe"
            | AMinus => "AMinus"
            | AMin => "AMin"
            | AMax => "AMax"
            | AContains => "AContains"
            | ASConcat => "ASConcat"
            | AForeignBinaryOp fb => toString fb
          end
     }.

End RBinaryOps.

Require Import String RUtil.

Tactic Notation "binOp_cases" tactic(first) ident(c) :=
  first;
  [ Case_aux c "AEq"%string
  | Case_aux c "AConcat"%string
  | Case_aux c "AMergeConcat"%string
  | Case_aux c "AAnd"%string
  | Case_aux c "AOr"%string
  | Case_aux c "ABArith"%string
  | Case_aux c "ALt"%string
  | Case_aux c "ALe"%string
  | Case_aux c "AUnion"%string
  | Case_aux c "AMinus"%string
  | Case_aux c "AMin"%string
  | Case_aux c "AMax"%string
  | Case_aux c "AContains"%string
  | Case_aux c "ASConcat"%string
  | Case_aux c "AForeignBinaryOp"%string].