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.
Proof.
    change (forall x y : ArithUOp, {x = y} + {x <> y}).
    decide equality.
  Defined.

  Global Instance SortCriterias_eqdec : EqDec SortCriterias eq.
Proof.
    change (forall x y : SortCriterias, {x = y} + {x <> y}).
    decide equality; try apply string_dec.
    decide equality; try apply string_dec.
    decide equality; try apply string_dec.
  Defined.

  Global Instance unaryOp_eqdec : EqDec unaryOp eq.
Proof.
    change (forall x y : unaryOp, {x = y} + {x <> y}).
    decide equality; try apply string_dec.
    - apply SortCriterias_eqdec.
    - induction l; decide equality; apply string_dec.
    - apply option_eqdec.
    - apply Z_eqdec.
    - apply equiv_dec.
    - induction b; decide equality; apply string_dec.
    - induction b; decide equality; apply string_dec.
    - apply ArithUOp_eqdec.
    - apply foreign_unary_op_dec.
  Defined.

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