Qcert.Basic.Operators.RUnaryOps

Section RUnaryOps.


  Context {fdata:foreign_data}.
  Context {fuop:foreign_unary_op}.

  Inductive ArithUOp
    := ArithAbs
     | ArithLog2
     | ArithSqrt
  .

  Inductive unaryOp : Set :=
  | AIdOp : unaryOp
  | ANeg: unaryOp
  | AColl : unaryOp
  | ASingleton : unaryOp
  | AFlatten : unaryOp
  | ADistinct: unaryOp
  | AOrderBy : SortCriterias → unaryOp
  | ARec : string → unaryOp
  | ADot : string → unaryOp
  | ARecRemove : string → unaryOp
  | ARecProject : list string → unaryOp
  | ACount: unaryOp
  | ASum : unaryOp
  | ANumMin : unaryOp
  | ANumMax : unaryOp
  | AArithMean : unaryOp
  | AToString : unaryOp
  | ASubstring : Z → option Z → unaryOp
  | ALike (pattern:string) (escape:option ascii) : unaryOp
  | ALeft : unaryOp
  | ARight : unaryOp
  | ABrand : brands → unaryOp
  | AUnbrand : unaryOp
  | ACast : brands → unaryOp
  | AUArith : ArithUOp → unaryOp
  | AForeignUnaryOp (fu:foreign_unary_op_type) : unaryOp
  .

  Global Instance ArithUOp_eqdec : EqDec ArithUOp eq.

  Global Instance SortCriterias_eqdec : EqDec SortCriterias eq.

  Global Instance unaryOp_eqdec : EqDec unaryOp eq.


  Global Instance ToString_ArithUOp : ToString ArithUOp
    := {toString :=
          fun (op:ArithUOp) ⇒
            match op with
            | ArithAbs ⇒ "ArithAbs"
            | ArithLog2 ⇒ "ArithLog2"
            | ArithSqrt ⇒ "Sqrt"
            end
       }.

  Definition ToString_SortDesc sd :=
    match sd with
    | Ascending ⇒ "asc"
    | Descending ⇒ "desc"
    end.

  Definition ToString_SortCriteria (sc : string × SortDesc) :=
    let (att,sd) := sc in
    bracketString "(" (att ++ "," ++ (ToString_SortDesc sd)) ")".

  Global Instance ToString_unaryOp : ToString unaryOp
    := {toString :=
          fun (op:unaryOp) ⇒
            match op with
            | AIdOp ⇒ "AIdOp"
            | ANeg ⇒ "ANeg"
            | AColl ⇒ "AColl"
            | ASingleton ⇒ "ASingleton"
            | AFlatten ⇒ "AFlatten"
            | ADistinct ⇒ "ADistinct"
            | AOrderBy ls ⇒
              "(AOrderBy"
                ++ (bracketString "[" (joinStrings "," (List.map ToString_SortCriteria ls)) "]")
                ++ ")"
            | ARec f ⇒ "(ARec " ++ f ++ ")"
            | ADot s ⇒ "(ADot " ++ s ++ ")"
            | ARecRemove s ⇒ "(ArecRemove " ++ s ++ ")"
            | ARecProject ls ⇒ "(ARecProject "
                                  ++ (bracketString "[" (joinStrings "," ls) "]")
                                  ++ ")"
            | ACount ⇒ "ACount"
            | ASum ⇒ "ASum"
            | ANumMin ⇒ "ANumMin"
            | ANumMax ⇒ "ANumMax"
            | AArithMean ⇒ "AArithMean"
            | AToString ⇒ "AToString"
            | ASubstring start len ⇒ "(ASubstring " ++ (toString start)
                                                     ++ (match len with
                                                         | None ⇒ ""
                                                         | Some len ⇒ " " ++ (toString len)
                                                         end
                                                        ) ++ ")"
            | ALike pattern oescape ⇒ "(ALike " ++ pattern
                                                     ++ (match oescape with
                                                         | None ⇒ ""
                                                         | Some escape ⇒ " ESCAPE " ++ (String escape EmptyString)
                                                         end
                                                        ) ++ ")"
                                                              
            | ALeft ⇒ "ALeft"
            | ARight ⇒ "ARight"
            | ABrand b ⇒ "(ABrand " ++ (@toString _ ToString_brands b)++ ")"
            | AUnbrand ⇒ "AUnbrand"
            | ACast b ⇒ "(ACast " ++ (@toString _ ToString_brands b) ++ ")"
            | AUArith aop ⇒ "(AUArith " ++ toString aop ++ ")"
            | AForeignUnaryOp fu ⇒ toString fu
          end
     }.

End RUnaryOps.


Tactic Notation "unaryOp_cases" tactic(first) ident(c) :=
  first;
  [ Case_aux c "AIdOp"%string
  | Case_aux c "ANeg"%string
  | Case_aux c "AColl"%string
  | Case_aux c "ASingleton"%string
  | Case_aux c "AFlatten"%string
  | Case_aux c "ADistinct"%string
  | Case_aux c "AOrderBy"%string
  | Case_aux c "ARec"%string
  | Case_aux c "ADot"%string
  | Case_aux c "ARecRemove"%string
  | Case_aux c "ARecProject"%string
  | Case_aux c "ACount"%string
  | Case_aux c "ASum"%string
  | Case_aux c "ANumMin"%string
  | Case_aux c "ANumMax"%string
  | Case_aux c "AArithMean"%string
  | Case_aux c "AToString"%string
  | Case_aux c "ASubstring"%string
  | Case_aux c "ALike"%string
  | Case_aux c "ALeft"%string
  | Case_aux c "ARight"%string
  | Case_aux c "ABrand"%string
  | Case_aux c "AUnbrand"%string
  | Case_aux c "ACast"%string
  | Case_aux c "AUArith"%string
  | Case_aux c "AForeignUnaryOp"%string
  ].