Module Qcert.Common.Operators.UnaryOperators

Section UnaryOperators.
  Require Import Ascii.
  Require Import String.
  Require Import ZArith.
  Require Import EquivDec.
  Require Import Utils.
  Require Import BrandRelation.
  Require Import ForeignData.
  Require Import DataSort.
  Require Import ForeignOperators.
  Require Import OperatorsUtils.

  Context {fdata:foreign_data}.
  Context {fuop:foreign_unary_op}.
  
  Inductive nat_arith_unary_op
    := NatAbs (* absolute value *)
     | NatLog2 (* base2 logarithm *)
     | NatSqrt (* square root *)
  .
  Inductive float_arith_unary_op
    := FloatNeg (* negative *)
     | FloatSqrt (* square root *)
     | FloatExp (* exponent *)
     | FloatLog (* logarithm base 2 *)
     | FloatLog10 (* logarithm base 10 *)
     | FloatCeil (* ceiling *)
     | FloatFloor (* floor *)
     | FloatAbs (* absolute value *)
  .

  Inductive unary_op : Set :=
  | OpIdentity : unary_op (* identity, returns its value *)
  | OpNeg : unary_op (* boolean negation *)
  | OpRec : string -> unary_op (* create a record with a single field *)
  | OpDot : string -> unary_op (* record field access *)
  | OpRecRemove : string -> unary_op (* record remove the given fields *)
  | OpRecProject : list string -> unary_op (* record projects on the given fields *)
  | OpBag : unary_op (* create a singleton bag *)
  | OpSingleton : unary_op (* value within a singleton bag *)
  | OpFlatten : unary_op (* flattens a bag of bags *)
  | OpDistinct: unary_op (* distinct values in a bag *)
  | OpOrderBy : SortCriterias -> unary_op (* sorts a collection of records *)
  | OpCount : unary_op (* bag count *)
  | OpToString : unary_op (* convert any data to a string *)
  | OpSubstring : Z -> option Z -> unary_op (* returns the substring starting with the nth character, for m characters (or the rest of the string) *)
  | OpLike (pattern:string)
              (escape:option ascii) : unary_op (* like expression (as in sql) *)
  | OpLeft : unary_op (* create a left value *)
  | OpRight : unary_op (* create a right value *)
  | OpBrand : brands -> unary_op (* brands a value *)
  | OpUnbrand : unary_op (* content of a branded value *)
  | OpCast : brands -> unary_op (* coerce a branded value into one of its sub-brands *)
  | OpNatUnary : nat_arith_unary_op -> unary_op (* arithmetic operations on natural floats *)
  | OpNatSum : unary_op (* sum of natural floats in a bag *)
  | OpNatMin : unary_op (* minimum of natural floats in a bag *)
  | OpNatMax : unary_op (* maximum of natural floats in a bag *)
  | OpNatMean : unary_op (* arithmetic mean of natural floats in a bag *)
  | OpFloatOfNat : unary_op (* coercion from natural float to float *)
  | OpFloatUnary : float_arith_unary_op -> unary_op (* arithmetic operations on floats *)
  | OpFloatTruncate : unary_op (* truncate *)
  | OpFloatSum : unary_op (* sum *)
  | OpFloatMean : unary_op (* arithmetic mean *)
  | OpFloatBagMin : unary_op (* minimum *)
  | OpFloatBagMax : unary_op (* maximum *)
  | OpForeignUnary
      (fu:foreign_unary_op_type) : unary_op (* foreign unary operators *)
  .

  Global Instance nat_arith_unary_op_eqdec : EqDec nat_arith_unary_op eq.

  Global Instance float_arith_unary_op_eqdec : EqDec float_arith_unary_op eq.

  Global Instance SortCriterias_eqdec : EqDec SortCriterias eq.

  Global Instance unary_op_eqdec : EqDec unary_op eq.

  Local Open Scope string.

  Global Instance ToString_nat_arith_unary_op : ToString nat_arith_unary_op
    := {toString :=
          fun (op:nat_arith_unary_op) =>
            match op with
            | NatAbs => "NatAbs"
            | NatLog2 => "NatLog2"
            | NatSqrt => "NatSqrt"
            end
       }.

  Global Instance ToString_float_arith_unary_op : ToString float_arith_unary_op
    := {toString :=
          fun (op:float_arith_unary_op) =>
            match op with
            | FloatNeg => "FloatNeg"
            | FloatSqrt => "FloatSqrt"
            | FloatExp => "FloatExp"
            | FloatLog => "FloatLog"
            | FloatLog10 => "FloatLog10"
            | FloatCeil => "FloatCeil"
            | FloatFloor => "FloatFloor"
            | FloatAbs => "FloatAbs"
            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_unary_op : ToString unary_op
    := {toString :=
          fun (op:unary_op) =>
            match op with
            | OpIdentity => "OpIdentity"
            | OpNeg => "OpNeg"
            | OpRec f => "(OpRec " ++ f ++ ")"
            | OpDot s => "(OpDot " ++ s ++ ")"
            | OpRecRemove s => "(OpRecRemove " ++ s ++ ")"
            | OpRecProject ls => "(OpRecProject "
                                      ++ (bracketString "[" (joinStrings "," ls) "]")
                                      ++ ")"
            | OpBag => "OpBag"
            | OpSingleton => "OpSingleton"
            | OpFlatten => "OpFlatten"
            | OpDistinct => "OpDistinct"
            | OpOrderBy ls =>
              "(OpOrderBy"
                ++ (bracketString "[" (joinStrings "," (List.map ToString_SortCriteria ls)) "]")
                ++ ")"
            | OpCount => "OpCount"
            | OpToString => "OpToString"
            | OpSubstring start len =>
              "(OpSubstring " ++ (toString start)
                                 ++ (match len with
                                     | None => ""
                                     | Some len => " " ++ (toString len)
                                     end
                                    ) ++ ")"
            | OpLike pattern oescape =>
              "(OpLike " ++ pattern
                            ++ (match oescape with
                                | None => ""
                                | Some escape => " ESCAPE " ++ (String escape EmptyString)
                                end
                               ) ++ ")"
            | OpLeft => "OpLeft"
            | OpRight => "OpRight"
            | OpBrand b => "(OpBrand " ++ (@toString _ ToString_brands b)++ ")"
            | OpUnbrand => "OpUnbrand"
            | OpCast b => "(OpCast " ++ (@toString _ ToString_brands b) ++ ")"
            | OpNatUnary aop => "(OpNatUnary " ++ toString aop ++ ")"
            | OpNatSum => "OpNatSum"
            | OpNatMin => "OpNatMin"
            | OpNatMax => "OpNatMax"
            | OpNatMean => "OpNatMean"
            | OpFloatOfNat => "OpFloatOfNat"
            | OpFloatUnary aop => "(OpFloatUnary " ++ toString aop ++ ")"
            | OpFloatTruncate => "OpFloatTruncate"
            | OpFloatSum => "OpFloatSum"
            | OpFloatMean => "OpFloatMean"
            | OpFloatBagMin => "OpFloatBagMin"
            | OpFloatBagMax => "OpFloatBagMax"
            | OpForeignUnary fu => toString fu
            end
       }.

End UnaryOperators.

Tactic Notation "unary_op_cases" tactic(first) ident(c) :=
  first;
  [ Case_aux c "OpIdentity"%string
  | Case_aux c "OpNeg"%string
  | Case_aux c "OpRec"%string
  | Case_aux c "OpDot"%string
  | Case_aux c "OpRecRemove"%string
  | Case_aux c "OpRecProject"%string
  | Case_aux c "OpBag"%string
  | Case_aux c "OpSingleton"%string
  | Case_aux c "OpFlatten"%string
  | Case_aux c "OpDistinct"%string
  | Case_aux c "OpOrderBy"%string
  | Case_aux c "OpCount"%string
  | Case_aux c "OpToString"%string
  | Case_aux c "OpSubstring"%string
  | Case_aux c "OpLike"%string
  | Case_aux c "OpLeft"%string
  | Case_aux c "OpRight"%string
  | Case_aux c "OpBrand"%string
  | Case_aux c "OpUnbrand"%string
  | Case_aux c "OpCast"%string
  | Case_aux c "OpNatUnary"%string
  | Case_aux c "OpNatSum"%string
  | Case_aux c "OpNatMin"%string
  | Case_aux c "OpNatMax"%string
  | Case_aux c "OpNatMean"%string
  | Case_aux c "OpFloatOfNat"%string
  | Case_aux c "OpFloatUnary"%string
  | Case_aux c "OpFloatTruncate"%string
  | Case_aux c "OpFloatSum"%string
  | Case_aux c "OpFloatMean"%string
  | Case_aux c "OpFloatBagMin"%string
  | Case_aux c "OpFloatBagMax"%string
  | Case_aux c "OpForeignUnary"%string
  ].