Module RUnaryOps

Section RUnaryOps.

  Require Import Ascii.
  Require Import String.
  Require Import ZArith.
  Require Import EquivDec.
  Require Import Utils.
  Require Import BrandRelation.
  Require Import RUtilOps.
  Require Import RDataSort.
  Require Import ForeignData.
  Require Import ForeignOps.

  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.

  Local Open Scope string.

  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.

Require Import String RUtil.

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