Qcert.Basic.Operators.RBinaryOps

Section RBinaryOps.



  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.


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.


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].