Module Qcert.Translation.Lang.SQLPPtoNRAEnv

Require Import String.
Require Import ZArith.
Require Import List.
Require Import Arith.
Require Import EquivDec.
Require Import Utils.
Require Import DataRuntime.
Require Import SQLPPRuntime.
Require Import NRAEnvRuntime.
Require Import SQLtoNRAEnv.

Section SQLPPtoNRAEnv.
  Context {fruntime:foreign_runtime}.

Definition sqlpp_to_nraenv_SPEq sqlpp_to_nraenv (e1 e2:sqlpp_expr) : nraenv
  := NRAEnvBinop OpEqual (sqlpp_to_nraenv e1) (sqlpp_to_nraenv e2).
  
Definition sqlpp_to_nraenv_not_implemented (what : string) : nraenv :=
 NRAEnvConst (dstring ("NRAEnv translation not Implemented: " ++ what)).
           
Fixpoint sqlpp_to_nraenv (q:sqlpp) : nraenv :=
   match q with
 | SPPositive expr
  => NRAEnvBinop (OpNatBinary NatPlus) (NRAEnvConst (dnat 0)) (sqlpp_to_nraenv expr)
 | SPNegative expr
        => NRAEnvBinop (OpNatBinary NatMinus) (NRAEnvConst (dnat 0)) (sqlpp_to_nraenv expr)
   | SPExists expr
        => NRAEnvUnop OpNeg (NRAEnvBinop OpLe (NRAEnvUnop OpCount (sqlpp_to_nraenv expr)) (NRAEnvConst (dnat 0)))
   | SPNot expr
    => NRAEnvUnop OpNeg (sqlpp_to_nraenv expr)
   | SPIsNull expr
   | SPIsMissing expr
   | SPIsUnknown expr
  => NRAEnvBinop OpEqual (sqlpp_to_nraenv expr) (NRAEnvConst dunit)
 | SPPlus e1 e2
        => NRAEnvBinop (OpNatBinary NatPlus) (sqlpp_to_nraenv e1) (sqlpp_to_nraenv e2)
   | SPMinus e1 e2
        => NRAEnvBinop (OpNatBinary NatMinus) (sqlpp_to_nraenv e1) (sqlpp_to_nraenv e2)
   | SPMult e1 e2
        => NRAEnvBinop (OpNatBinary NatMult) (sqlpp_to_nraenv e1) (sqlpp_to_nraenv e2)
   | SPDiv e1 e2
        => NRAEnvBinop (OpNatBinary NatDiv) (sqlpp_to_nraenv e1) (sqlpp_to_nraenv e2)
   | SPMod e1 e2
        => NRAEnvBinop (OpNatBinary NatRem) (sqlpp_to_nraenv e1) (sqlpp_to_nraenv e2)
   | SPExp e1 e2
  => sqlpp_to_nraenv_not_implemented "exp operator"
   | SPConcat e1 e2
        => NRAEnvBinop OpStringConcat (sqlpp_to_nraenv e1) (sqlpp_to_nraenv e2)
   | SPIn e1 e2
        => NRAEnvBinop OpContains (sqlpp_to_nraenv e1) (sqlpp_to_nraenv e2)
   | SPEq e1 e2
   | SPFuzzyEq e1 e2
    => sqlpp_to_nraenv_SPEq sqlpp_to_nraenv e1 e2
   | SPNeq e1 e2
        => NRAEnvUnop OpNeg (NRAEnvBinop OpEqual (sqlpp_to_nraenv e1) (sqlpp_to_nraenv e2))
   | SPLt e1 e2
    => NRAEnvBinop OpLt (sqlpp_to_nraenv e1) (sqlpp_to_nraenv e2)
   | SPGt e1 e2
    => NRAEnvBinop OpLt (sqlpp_to_nraenv e2) (sqlpp_to_nraenv e1)
   | SPLe e1 e2
    => NRAEnvBinop OpLe (sqlpp_to_nraenv e1) (sqlpp_to_nraenv e2)
   | SPGe e1 e2
    => NRAEnvBinop OpLe (sqlpp_to_nraenv e2) (sqlpp_to_nraenv e1)
   | SPLike e s
    => NRAEnvUnop (OpLike s) (sqlpp_to_nraenv e)
   | SPAnd e1 e2
    => NRAEnvBinop OpAnd (sqlpp_to_nraenv e1) (sqlpp_to_nraenv e2)
   | SPOr e1 e2
    => NRAEnvBinop OpOr (sqlpp_to_nraenv e1) (sqlpp_to_nraenv e2)
 | SPBetween e1 e2 e3
    => NRAEnvBinop OpAnd (NRAEnvBinop OpLe (sqlpp_to_nraenv e2) (sqlpp_to_nraenv e1))
                         (NRAEnvBinop OpLe (sqlpp_to_nraenv e1) (sqlpp_to_nraenv e3))
 | SPSimpleCase value whenthens deflt
   =>
           let last := match deflt with
                    | Some dflt => sqlpp_to_nraenv dflt
                    | None => NRAEnvConst dunit
                    end
           in
    List.fold_right (fun wt acc =>
                              match
                                wt
                              with
                                SPWhenThen whn thn =>
                                nraenv_if (sqlpp_to_nraenv_SPEq sqlpp_to_nraenv whn value) (sqlpp_to_nraenv thn) acc
                              end)
             last whenthens
 | SPSearchedCase whenthens deflt
  => let last := match deflt with
                    | Some dflt => sqlpp_to_nraenv dflt
                    | None => NRAEnvConst dunit
                    end
           in
     List.fold_right (fun wt acc => match wt with SPWhenThen w t => nraenv_if (sqlpp_to_nraenv w) (sqlpp_to_nraenv t) acc end)
       last whenthens
 | SPSome _ _
    | SPEvery _ _
     => sqlpp_to_nraenv_not_implemented "quantified expressions (SOME | EVERY)"
 | SPDot expr name
  => NRAEnvUnop (OpDot name) (sqlpp_to_nraenv expr)
 | SPIndex _ _
 | SPIndexAny _
     => sqlpp_to_nraenv_not_implemented "indexing expressions"
 | SPLiteral d
  => NRAEnvConst d
   | SPNull
   | SPMissing
    => NRAEnvConst dunit
 | SPVarRef name
  => NRAEnvUnop (OpDot name) NRAEnvID
 | SPFunctionCall name args
  => match name with
  | SPFget_year
  | SPFget_month
  | SPFget_day
  | SPFget_hour
  | SPFget_minute
  | SPFget_second
  | SPFget_millisecond
  | SPFavg
  | SPFmin
  | SPFmax
  | SPFcount
  | SPFsum
  | SPFcoll_avg
  | SPFcoll_min
  | SPFcoll_max
  | SPFcoll_count
  | SPFcoll_sum
  | SPFarray_avg
  | SPFarray_min
  | SPFarray_max
  | SPFarray_count
  | SPFarray_sum
  | SPFsqrt
  | SPFsubstring
  | SPFregexp_contains
  | SPFcontains
     => sqlpp_to_nraenv_not_implemented "function call expressions"
     end
 | SPArray items
 | SPBag items
  => List.fold_right (fun expr acc => NRAEnvBinop OpBagUnion (sqlpp_to_nraenv expr) acc) (NRAEnvConst (dcoll nil)) items
 | SPObject items
        => List.fold_right (fun (item : (string * sqlpp)) acc => let (name , expr) := item in
   NRAEnvBinop OpRecConcat (NRAEnvUnop (OpRec name) (sqlpp_to_nraenv expr)) acc) (NRAEnvConst (drec nil)) items
 | SPQuery stmt
  => sqlpp_to_nraenv_not_implemented "select"
 end.

Definition sqlpp_to_nraenv_top := sqlpp_to_nraenv.

End SQLPPtoNRAEnv.